fix(ltl): keep the authored window on a step-bounded obligation

reduce decremented StepBound into the residual, so the trace reported the
remaining window rather than the authored one: a within(1915, "steps") showed
up as 1875 after 40 steps, and the replay UI renders that string verbatim. The
duration case was fixed when bounded windows were made to serialize their
resolved deadline; the step case was not, and withinFor's comment claimed
otherwise.

The window is now immutable and the closing observation is resolved once, which
mirrors Deadline exactly. A step counts observations the evaluator reduced,
not steps the runner executed, because a skipped step gave the property no
chance to discharge and transitional-step rate is itself policy-dependent.

Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX

internal/ltl/evaluator.go

@@ -37,6 +37,11 @@ type Evaluator struct {
 	violated  bool
 	steps     int
 	violation *Violation
+	// observations counts the states this evaluator actually reduced, which is
+	// what a `within(n, "steps")` window is measured in. It differs from steps
+	// whenever the caller's numbering skipped an observation, and the two are
+	// told apart in the serialized AST by expiresAtObservation.
+	observations int
 	// oneShot marks a root that is armed once at the first observation rather
 	// than re-asserted at every one; armed records that it has been.
 	oneShot bool
@@ -93,6 +98,7 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict {
 		return VerdictViolated
 	}
 	e.steps = step
+	e.observations++
 
 	obligations := make([]obligation, 0, len(e.pending)+1)
 	obligations = append(obligations, e.pending...)
@@ -102,7 +108,7 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict {
 	e.pending = e.pending[:0]
 
 	for _, entry := range obligations {
-		result := reduce(entry.formula, now)
+		result := reduce(entry.formula, now, e.observations)
 		switch result.status {
 		case statusHolds:
 			// drop
@@ -374,7 +380,11 @@ func pending(f Formula) reduceResult {
 	return reduceResult{status: statusPending, formula: f}
 }
 
-func reduce(formula Formula, now time.Time) reduceResult {
+// reduce advances one obligation against the current state. `now` is the
+// observation's wall clock and `observation` its index in the sequence of
+// states this evaluator reduced; the two are the clocks a duration-bounded and
+// a step-bounded window are resolved against.
+func reduce(formula Formula, now time.Time, observation int) reduceResult {
 	switch concrete := formula.(type) {
 	case PureFormula:
 		if concrete.Value {
@@ -399,7 +409,7 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return violatedWith(concrete, "predicate false")
 
 	case NowFormula:
-		return reduce(concrete.Inner, now)
+		return reduce(concrete.Inner, now, observation)
 
 	case NextFormula:
 		// Next defers the inner obligation to the following step without
@@ -414,23 +424,24 @@ func reduce(formula Formula, now time.Time) reduceResult {
 			concrete.Deadline = now.Add(concrete.Duration)
 			concrete.HasDeadline = true
 		}
-		innerResult := reduce(concrete.Inner, now)
+		if concrete.HasStepBound && !concrete.HasExpiryObservation {
+			concrete.ExpiryObservation = observation + concrete.StepBound - 1
+			concrete.HasExpiryObservation = true
+		}
+		innerResult := reduce(concrete.Inner, now, observation)
 		if innerResult.status == statusHolds {
 			return holds()
 		}
 		// The window is measured in observations at which the inner could have
 		// discharged, so an inner that is merely pending has not discharged and
 		// the window closing on it is a violation.
-		if concrete.HasStepBound && concrete.StepBound <= 1 {
+		if concrete.HasExpiryObservation && observation >= concrete.ExpiryObservation {
 			return violatedFrom(innerResult, concrete, "eventually bound exhausted")
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
 			return violatedFrom(innerResult, concrete, "eventually deadline reached")
 		}
 		next := concrete
-		if concrete.HasStepBound {
-			next.StepBound = concrete.StepBound - 1
-		}
 		// F(inner) unrolls to inner or X F(inner). A pending inner is a
 		// deferred way of satisfying the promise, so it is kept as a disjunct
 		// rather than dropped; dropping it is what made an inner that only
@@ -449,11 +460,11 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return reduce(OrFormula{
 			Left:  pushNot(concrete.Antecedent),
 			Right: nnf(concrete.Consequent),
-		}, now)
+		}, now, observation)
 
 	case OrFormula:
-		left := reduce(concrete.Left, now)
-		right := reduce(concrete.Right, now)
+		left := reduce(concrete.Left, now, observation)
+		right := reduce(concrete.Right, now, observation)
 		if left.status == statusHolds || right.status == statusHolds {
 			return holds()
 		}
@@ -469,8 +480,8 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return pending(OrFormula{Left: left.formula, Right: right.formula})
 
 	case AndFormula:
-		left := reduce(concrete.Left, now)
-		right := reduce(concrete.Right, now)
+		left := reduce(concrete.Left, now, observation)
+		right := reduce(concrete.Right, now, observation)
 		if left.status == statusViolated {
 			return violatedFrom(left, concrete, "conjunct violated")
 		}
@@ -489,7 +500,7 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return pending(AndFormula{Left: left.formula, Right: right.formula})
 
 	case NotFormula:
-		inner := reduce(concrete.Inner, now)
+		inner := reduce(concrete.Inner, now, observation)
 		switch inner.status {
 		case statusHolds:
 			return violatedWith(concrete, "negated formula held")
@@ -506,7 +517,11 @@ func reduce(formula Formula, now time.Time) reduceResult {
 			concrete.Deadline = now.Add(concrete.Duration)
 			concrete.HasDeadline = true
 		}
-		innerResult := reduce(concrete.Inner, now)
+		if concrete.HasStepBound && !concrete.HasExpiryObservation {
+			concrete.ExpiryObservation = observation + concrete.StepBound - 1
+			concrete.HasExpiryObservation = true
+		}
+		innerResult := reduce(concrete.Inner, now, observation)
 		if innerResult.status == statusViolated {
 			return violatedFrom(innerResult, concrete, "always inner violated")
 		}
@@ -517,16 +532,13 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		// hold". A pending inner has not been breached inside the window, so it
 		// discharges vacuously here exactly as its negation violates on the
 		// Eventually side.
-		if concrete.HasStepBound && concrete.StepBound <= 1 {
+		if concrete.HasExpiryObservation && observation >= concrete.ExpiryObservation {
 			return holds()
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
 			return holds()
 		}
 		next := concrete
-		if concrete.HasStepBound {
-			next.StepBound = concrete.StepBound - 1
-		}
 		if innerResult.status == statusHolds {
 			return pending(next)
 		}

internal/ltl/formula.go

@@ -42,6 +42,8 @@ type AlwaysFormula struct {
 	Inner                Formula
 	StepBound            int
 	HasStepBound         bool
+	ExpiryObservation    int
+	HasExpiryObservation bool
 	Duration             time.Duration
 	Deadline             time.Time
 	HasDeadline          bool
@@ -91,10 +93,17 @@ type NextFormula struct {
 // resolves the absolute deadline on first reduction using the observation
 // time. This matches the "within N seconds of obligation instantiation"
 // semantics used by nested Always(Eventually(...).within(...)) formulas.
+//
+// StepBound is the step-domain counterpart: the window counts observations the
+// evaluator reduced, and ExpiryObservation is the absolute closing observation
+// the evaluator resolves on first reduction, exactly as Deadline is for
+// Duration.
 type EventuallyFormula struct {
 	Inner                Formula
 	StepBound            int
 	HasStepBound         bool
+	ExpiryObservation    int
+	HasExpiryObservation bool
 	Duration             time.Duration
 	Deadline             time.Time
 	HasDeadline          bool
@@ -179,6 +188,9 @@ func (a AlwaysFormula) describe() string {
 	if a.HasStepBound {
 		parts = append(parts, fmt.Sprintf("steps=%d", a.StepBound))
 	}
+	if a.HasExpiryObservation {
+		parts = append(parts, fmt.Sprintf("expiresAtObservation=%d", a.ExpiryObservation))
+	}
 	if a.HasDeadline {
 		parts = append(parts, "deadline="+a.Deadline.Format(time.RFC3339Nano))
 	} else if a.Duration > 0 {
@@ -197,6 +209,9 @@ func (e EventuallyFormula) describe() string {
 	if e.HasStepBound {
 		parts = append(parts, fmt.Sprintf("steps=%d", e.StepBound))
 	}
+	if e.HasExpiryObservation {
+		parts = append(parts, fmt.Sprintf("expiresAtObservation=%d", e.ExpiryObservation))
+	}
 	if e.HasDeadline {
 		parts = append(parts, "deadline="+e.Deadline.Format(time.RFC3339Nano))
 	} else if e.Duration > 0 {
@@ -229,33 +244,73 @@ type withinNode struct {
 	// the same duration differ only here, so without it they serialize
 	// identically and the trace erases the distinction the evaluator makes.
 	Deadline int64 `json:"deadline,omitempty"`
+	// ExpiresAtObservation is the step-domain counterpart of Deadline: the
+	// index of the observation the window closes at. It names observations
+	// rather than runner steps because a step the verifier skipped never
+	// reached the evaluator and so cannot close a window; the pair of fields
+	// is what lets a reader tell the two numberings apart.
+	ExpiresAtObservation int `json:"expiresAtObservation,omitempty"`
+}
+
+// boundWindow is the optional window shared by AlwaysFormula and
+// EventuallyFormula: the window the spec authored plus the absolute close the
+// evaluator resolved for this obligation.
+type boundWindow struct {
+	hasStepBound         bool
+	stepBound            int
+	hasExpiryObservation bool
+	expiryObservation    int
+	duration             time.Duration
+	hasDeadline          bool
+	deadline             time.Time
 }
 
 // withinFor renders the bound clause of a bounded Always or Eventually. The
 // authored window (steps or duration) stays in amount/unit so readers keep
-// seeing what the spec asked for; the resolved deadline rides alongside.
-func withinFor(
-	hasStepBound bool,
-	stepBound int,
-	duration time.Duration,
-	hasDeadline bool,
-	deadline time.Time,
-) *withinNode {
-	var node *withinNode
+// seeing what the spec asked for; the resolved close rides alongside.
+func withinFor(window boundWindow) *withinNode {
 	switch {
-	case hasStepBound:
-		node = &withinNode{Amount: int64(stepBound), Unit: "steps"}
-	case duration > 0:
-		node = &withinNode{Amount: duration.Milliseconds(), Unit: "milliseconds"}
-	case hasDeadline:
-		return &withinNode{Amount: deadline.UnixMilli(), Unit: "deadline"}
+	case window.hasStepBound:
+		node := &withinNode{Amount: int64(window.stepBound), Unit: "steps"}
+		if window.hasExpiryObservation {
+			node.ExpiresAtObservation = window.expiryObservation
+		}
+		return node
+	case window.duration > 0:
+		node := &withinNode{Amount: window.duration.Milliseconds(), Unit: "milliseconds"}
+		if window.hasDeadline {
+			node.Deadline = window.deadline.UnixMilli()
+		}
+		return node
+	case window.hasDeadline:
+		return &withinNode{Amount: window.deadline.UnixMilli(), Unit: "deadline"}
 	default:
 		return nil
 	}
-	if hasDeadline {
-		node.Deadline = deadline.UnixMilli()
+}
+
+func (a AlwaysFormula) boundWindow() boundWindow {
+	return boundWindow{
+		hasStepBound:         a.HasStepBound,
+		stepBound:            a.StepBound,
+		hasExpiryObservation: a.HasExpiryObservation,
+		expiryObservation:    a.ExpiryObservation,
+		duration:             a.Duration,
+		hasDeadline:          a.HasDeadline,
+		deadline:             a.Deadline,
+	}
+}
+
+func (e EventuallyFormula) boundWindow() boundWindow {
+	return boundWindow{
+		hasStepBound:         e.HasStepBound,
+		stepBound:            e.StepBound,
+		hasExpiryObservation: e.HasExpiryObservation,
+		expiryObservation:    e.ExpiryObservation,
+		duration:             e.Duration,
+		hasDeadline:          e.HasDeadline,
+		deadline:             e.Deadline,
 	}
-	return node
 }
 
 func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
@@ -264,9 +319,7 @@ func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "always", Arg: a.Inner}
-	payload.Within = withinFor(
-		a.HasStepBound, a.StepBound, a.Duration, a.HasDeadline, a.Deadline,
-	)
+	payload.Within = withinFor(a.boundWindow())
 	return json.Marshal(payload)
 }
 
@@ -297,9 +350,7 @@ func (e EventuallyFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "eventually", Arg: e.Inner}
-	payload.Within = withinFor(
-		e.HasStepBound, e.StepBound, e.Duration, e.HasDeadline, e.Deadline,
-	)
+	payload.Within = withinFor(e.boundWindow())
 	return json.Marshal(payload)
 }
 

internal/ltl/nnf.go

@@ -68,6 +68,8 @@ func pushNot(formula Formula) Formula {
 			Inner:                pushNot(concrete.Inner),
 			StepBound:            concrete.StepBound,
 			HasStepBound:         concrete.HasStepBound,
+			ExpiryObservation:    concrete.ExpiryObservation,
+			HasExpiryObservation: concrete.HasExpiryObservation,
 			Duration:             concrete.Duration,
 			Deadline:             concrete.Deadline,
 			HasDeadline:          concrete.HasDeadline,
@@ -77,6 +79,8 @@ func pushNot(formula Formula) Formula {
 			Inner:                pushNot(concrete.Inner),
 			StepBound:            concrete.StepBound,
 			HasStepBound:         concrete.HasStepBound,
+			ExpiryObservation:    concrete.ExpiryObservation,
+			HasExpiryObservation: concrete.HasExpiryObservation,
 			Duration:             concrete.Duration,
 			Deadline:             concrete.Deadline,
 			HasDeadline:          concrete.HasDeadline,

internal/ltl/step_bound_test.go

@@ -0,0 +1,195 @@
+package ltl
+
+import (
+	"encoding/json"
+	"strings"
+	"testing"
+	"time"
+)
+
+func alwaysFalse() func() (bool, error) {
+	return func() (bool, error) { return false, nil }
+}
+
+// A step-bounded window counts the observations the evaluator reduced, and the
+// residual has to keep saying which window the spec authored rather than the
+// part of it that is left. Bug class: the replay UI renders "within N steps"
+// straight off the residual, so a shrinking N tells the reader the spec asked
+// for a window it never asked for.
+func TestStepBoundedEventually_ResidualKeepsAuthoredWindow(t *testing.T) {
+	evaluator := NewEvaluator(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 5))
+	for index := range 3 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
+			t.Fatalf("observation %d: got %v, want pending", index+1, got)
+		}
+	}
+
+	body, err := json.Marshal(evaluator.Residual())
+	if err != nil {
+		t.Fatal(err)
+	}
+	if !strings.Contains(string(body), `"unit":"steps"`) || !strings.Contains(string(body), `"amount":5`) {
+		t.Errorf("authored window lost after reduction: %s", body)
+	}
+	if !strings.Contains(string(body), `"expiresAtObservation":5`) {
+		t.Errorf("resolved expiry missing: %s", body)
+	}
+}
+
+// Two obligations spawned at different observations from one `within(n,
+// "steps")` window close at different observations, and the serialized AST has
+// to keep them apart the way a resolved deadline keeps two duration-bounded
+// ones apart. Bug class: the trace shows one node where the evaluator holds
+// several distinct obligations.
+func TestStepBoundedEventually_ObligationsSerializeApart(t *testing.T) {
+	evaluator := NewEvaluator(Always(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 3)))
+	for index := range 2 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
+			t.Fatalf("observation %d: got %v, want pending", index+1, got)
+		}
+	}
+
+	body, err := json.Marshal(evaluator.Residual())
+	if err != nil {
+		t.Fatal(err)
+	}
+	text := string(body)
+	if strings.Count(text, `"amount":3`) != 2 {
+		t.Errorf("both obligations should report the authored window of 3: %s", text)
+	}
+	if !strings.Contains(text, `"expiresAtObservation":3`) || !strings.Contains(text, `"expiresAtObservation":4`) {
+		t.Errorf("obligations armed at different observations share a closing observation: %s", text)
+	}
+}
+
+// A bounded Always is the dual of a bounded Eventually, so its window resolves
+// and serializes the same way.
+func TestStepBoundedAlways_ResidualKeepsAuthoredWindow(t *testing.T) {
+	formula := AlwaysFormula{
+		Inner:        ThunkNamed("p", func() (bool, error) { return true, nil }),
+		StepBound:    4,
+		HasStepBound: true,
+	}
+	evaluator := NewEvaluator(formula)
+	for index := range 2 {
+		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
+			t.Fatalf("observation %d: got %v, want pending", index+1, got)
+		}
+	}
+
+	body, err := json.Marshal(evaluator.Residual())
+	if err != nil {
+		t.Fatal(err)
+	}
+	if !strings.Contains(string(body), `"amount":4`) {
+		t.Errorf("authored window lost after reduction: %s", body)
+	}
+	if !strings.Contains(string(body), `"expiresAtObservation":4`) {
+		t.Errorf("resolved expiry missing: %s", body)
+	}
+}
+
+// A step the verifier skipped (a transitional tree, an empty hierarchy) never
+// reached the evaluator, so the property was given no chance to discharge
+// there and the window must not charge for it. The runner's step numbering
+// only labels the witness; it does not drive the window.
+func TestStepBoundedEventually_SkippedRunnerStepsDoNotConsumeWindow(t *testing.T) {
+	observed := 0
+	inner := ThunkNamed("p", func() (bool, error) {
+		observed++
+		return observed == 3, nil
+	})
+	evaluator := NewEvaluator(EventuallyWithinSteps(inner, 3))
+
+	var verdict Verdict
+	for _, runnerStep := range []int{1, 7, 19} {
+		verdict = evaluator.ObserveAtStep(time.Unix(int64(runnerStep), 0), runnerStep)
+	}
+	if verdict != VerdictHolds {
+		t.Errorf("three observations inside a three-observation window: got %v, want holds", verdict)
+	}
+}
+
+// The witness still carries the runner's numbering, so a report names the step
+// that armed the obligation even though the window counted observations.
+func TestStepBoundedEventually_WitnessCarriesRunnerStep(t *testing.T) {
+	evaluator := NewEvaluator(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 2))
+	for _, runnerStep := range []int{4, 11} {
+		evaluator.ObserveAtStep(time.Unix(int64(runnerStep), 0), runnerStep)
+	}
+
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("no violation recorded")
+	}
+	if witness.Step != 4 {
+		t.Errorf("witness Step = %d, want the runner step that armed the obligation (4)", witness.Step)
+	}
+}
+
+// An undischarged bounded eventually is a broken liveness promise at run end
+// whatever unit bounded it. Bug class: choosing "steps" over "seconds" quietly
+// turning an unmet obligation into a vacuous pass.
+func TestFinalize_StepBoundedEventuallyMatchesWallClock(t *testing.T) {
+	byStep, stepEvaluator := runAndFinalize(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 50), 3)
+	byClock, clockEvaluator := runAndFinalize(EventuallyWithin(ThunkNamed("p", alwaysFalse()), time.Hour), 3)
+
+	if byStep != VerdictViolated || byClock != VerdictViolated {
+		t.Fatalf("step bound = %v, wall clock = %v, want both violated", byStep, byClock)
+	}
+	stepWitness, clockWitness := stepEvaluator.Violation(), clockEvaluator.Violation()
+	if stepWitness == nil || clockWitness == nil {
+		t.Fatal("both undischarged obligations must carry a witness")
+	}
+	if stepWitness.Reason != clockWitness.Reason {
+		t.Errorf("reasons diverge: step %q, wall clock %q", stepWitness.Reason, clockWitness.Reason)
+	}
+	if stepWitness.Step != clockWitness.Step {
+		t.Errorf("origin steps diverge: step %d, wall clock %d", stepWitness.Step, clockWitness.Step)
+	}
+}
+
+// The reason the unit exists. Two action-selection policies get the same
+// 300-step budget and reach the same state at the same step, but the model
+// policy takes 359 seconds where the seeded policy takes 47 because it makes a
+// provider call per step. A wall-clock bound fails the slow policy on elapsed
+// time alone; the same window written in steps decides both policies alike.
+func TestStepBound_SlowPolicyDoesNotFailOnTimeAlone(t *testing.T) {
+	const budget = 300
+	const satisfiedAtObservation = 260
+	seededCadence := 47 * time.Second / budget
+	modelCadence := 359 * time.Second / budget
+
+	run := func(cadence time.Duration, bound func(Formula) Formula) Verdict {
+		observed := 0
+		inner := ThunkNamed("someTransactionExists", func() (bool, error) {
+			observed++
+			return observed >= satisfiedAtObservation, nil
+		})
+		evaluator := NewEvaluator(bound(inner))
+		base := time.Unix(1780000000, 0)
+		for index := range budget {
+			verdict := evaluator.ObserveAtStep(base.Add(time.Duration(index)*cadence), index+1)
+			if verdict != VerdictPending {
+				return verdict
+			}
+		}
+		return evaluator.Finalize()
+	}
+
+	byClock := func(inner Formula) Formula { return EventuallyWithin(inner, 300*time.Second) }
+	bySteps := func(inner Formula) Formula { return EventuallyWithinSteps(inner, 1915) }
+
+	if got := run(seededCadence, byClock); got != VerdictHolds {
+		t.Errorf("wall-clock bound under the seeded policy: got %v, want holds", got)
+	}
+	if got := run(modelCadence, byClock); got != VerdictViolated {
+		t.Errorf("wall-clock bound under the model policy: got %v, want violated (the false positive this unit removes)", got)
+	}
+	if got := run(seededCadence, bySteps); got != VerdictHolds {
+		t.Errorf("step bound under the seeded policy: got %v, want holds", got)
+	}
+	if got := run(modelCadence, bySteps); got != VerdictHolds {
+		t.Errorf("step bound under the model policy: got %v, want holds", got)
+	}
+}