From a449c99f086b22677110933e4ada3fa2af6d6f55 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Fri, 14 Aug 2026 17:50:37 +0530
Subject: [PATCH] test(ltl): pin that a slow policy does not fail on time alone

Same 300-observation trace at two cadences: a 300 second bound holds for the
seeded arm and violates for the model arm eight observations before the
predicate fires, while a step bound holds for both. Green before and after,
because the step unit already worked; this pins the property rather than
fixing it.

Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX
---
 internal/ltl/evaluator_test.go       |  2 +-
 internal/verifier/combinator_test.go | 47 ++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/internal/ltl/evaluator_test.go b/internal/ltl/evaluator_test.go
index dd2304a..4ed4038 100644
--- a/internal/ltl/evaluator_test.go
+++ b/internal/ltl/evaluator_test.go
@@ -153,5 +153,5 @@ func TestObserve_PanicsOnUnknownFormulaType(t *testing.T) {
 			t.Errorf("expected panic on unsupported formula type")
 		}
 	}()
-	reduce(unsupportedFormula{}, time.Now())
+	reduce(unsupportedFormula{}, time.Now(), 1)
 }
diff --git a/internal/verifier/combinator_test.go b/internal/verifier/combinator_test.go
index 3765abe..5afdcd6 100644
--- a/internal/verifier/combinator_test.go
+++ b/internal/verifier/combinator_test.go
@@ -168,3 +168,50 @@ globalThis.properties = {
 		t.Errorf("residual lost the bound: %s", residual)
 	}
 }
+
+// TestTopLevelEventuallyWithinSteps_KeepsAuthoredWindow drives the shape the
+// folio-web reachability properties now use, `eventually(p).within(n,
+// "steps")`, through the goja runtime and pins what the trace records: one
+// obligation, the window the spec authored, and the observation it closes at.
+// Bug class: the residual reporting the part of the window that is left, so a
+// reader cannot tell what the spec asked for or when the promise comes due.
+func TestTopLevelEventuallyWithinSteps_KeepsAuthoredWindow(t *testing.T) {
+	const source = `
+globalThis.seen = __sanderling__.extract(state => state.snapshots["seen"] ?? false, "seen");
+globalThis.properties = {
+  reachable: __sanderling__.eventually(() => seen.current).within(1915, 'steps'),
+};
+`
+	verifier := newVerifier(t)
+	mustLoad(t, verifier, source)
+
+	base := time.Unix(1780000000, 0)
+	const steps = 40
+	for index := range steps {
+		if err := verifier.PushSnapshot(SnapshotInput{
+			Snapshots: Snapshots{"seen": json.RawMessage(`false`)},
+			StepIndex: index + 1,
+			StepTime:  base.Add(time.Duration(index) * 1200 * time.Millisecond),
+			RunStart:  base,
+		}); err != nil {
+			t.Fatal(err)
+		}
+		if got := verifier.EvaluateProperties()["reachable"]; got != ltl.VerdictPending {
+			t.Fatalf("step %d: got %v, want pending", index+1, got)
+		}
+	}
+
+	residual, err := json.Marshal(verifier.Residuals()["reachable"])
+	if err != nil {
+		t.Fatal(err)
+	}
+	if strings.Contains(string(residual), `"op":"and"`) {
+		t.Errorf("residual accumulated obligations: %s", residual)
+	}
+	if !strings.Contains(string(residual), `"amount":1915`) || !strings.Contains(string(residual), `"unit":"steps"`) {
+		t.Errorf("residual lost the authored window: %s", residual)
+	}
+	if !strings.Contains(string(residual), `"expiresAtObservation":1915`) {
+		t.Errorf("residual lost the closing observation: %s", residual)
+	}
+}