fix(ltl): arm a one-shot root once per run

A root that carries its own horizon is one obligation for the whole run, not one
per observation. Re-instantiating a top-level eventually monitored G F<=n(p)
instead of F<=n(p) and left one live obligation per step behind; a bounded
always restarted its window every step and never closed.

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

internal/ltl/evaluator.go

@@ -37,6 +37,10 @@ type Evaluator struct {
 	violated  bool
 	steps     int
 	violation *Violation
+	// 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
+	armed   bool
 }
 
 // obligation pairs a residual formula with the step that spawned it, so a
@@ -62,7 +66,8 @@ type Violation struct {
 }
 
 func NewEvaluator(formula Formula) *Evaluator {
-	return &Evaluator{root: nnf(formula)}
+	normalized := nnf(formula)
+	return &Evaluator{root: normalized, oneShot: isOneShotRoot(normalized)}
 }
 
 // Observe evaluates the formula against the current state and returns the
@@ -89,8 +94,11 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict {
 	}
 	e.steps = step
 
-	fresh := obligation{formula: rootObligation(e.root), origin: step}
+	obligations := make([]obligation, 0, len(e.pending)+1)
-	obligations := append(e.pending, fresh)
+	obligations = append(obligations, e.pending...)
+	if formula, ok := e.instantiateRoot(); ok {
+		obligations = append(obligations, obligation{formula: formula, origin: step})
+	}
 	e.pending = e.pending[:0]
 
 	for _, entry := range obligations {
@@ -267,10 +275,48 @@ func (e *Evaluator) Residual() Formula {
 	return combined
 }
 
-// rootObligation returns the formula to instantiate at each step. An outer
+// instantiateRoot returns the obligation to register for this observation, and
-// Always is stripped so its inner is re-evaluated every step; any other root
+// whether there is one at all. A one-shot root is armed only at the first
-// formula is itself re-instantiated each step (matching the v0.1 semantics
+// observation; a recurring root is re-asserted at every one.
-// where a bare Thunk is re-observed on every call).
+func (e *Evaluator) instantiateRoot() (Formula, bool) {
+	if !e.oneShot {
+		return rootObligation(e.root), true
+	}
+	if e.armed {
+		return nil, false
+	}
+	e.armed = true
+	return e.root, true
+}
+
+// isOneShotRoot reports whether a root formula is a single obligation for the
+// whole run rather than one instance per observation.
+//
+// A root that carries its own horizon is one-shot: an eventually is a
+// reachability goal ("this happens at some point"), and a bounded always is a
+// single window. Re-instantiating either at every step would monitor a
+// different property -- G F<=n(p) instead of F<=n(p), and G(p) instead of
+// G<=n(p), the latter because a re-instantiated window restarts and never
+// closes -- and would leave one live obligation per step behind.
+//
+// Every other root keeps the implicit-always reading: an unbounded always
+// re-instantiates its inner (which is what gives each instance its own origin
+// step), and a bare predicate or connective is re-asserted each observation.
+func isOneShotRoot(root Formula) bool {
+	switch concrete := root.(type) {
+	case EventuallyFormula:
+		return true
+	case AlwaysFormula:
+		return concrete.HasStepBound || concrete.HasDeadline || concrete.Duration > 0
+	default:
+		return false
+	}
+}
+
+// rootObligation returns the formula a recurring root instantiates at each
+// step. An outer Always is stripped so its inner is re-evaluated every step;
+// any other root formula is itself re-instantiated each step (matching the
+// v0.1 semantics where a bare Thunk is re-observed on every call).
 func rootObligation(root Formula) Formula {
 	if always, ok := root.(AlwaysFormula); ok {
 		return always.Inner

internal/ltl/root_test.go

@@ -0,0 +1,106 @@
+package ltl
+
+import (
+	"testing"
+	"time"
+)
+
+// TestRoot_BoundedEventuallyStaysOneObligation locks the cost of the one-shot
+// root. A duration-bounded top-level eventually is one reachability goal, so
+// the pending set holds one obligation for the whole run. Re-instantiating it
+// every step monitored G F<=n(p) instead and left one live obligation per step
+// behind: a 553-step run carried 553 of them and re-ran the predicate once per
+// obligation per step.
+func TestRoot_BoundedEventuallyStaysOneObligation(t *testing.T) {
+	const steps = 600
+	calls := 0
+	formula := EventuallyWithin(ThunkNamed("p", func() (bool, error) {
+		calls++
+		return false, nil
+	}), 300*time.Second)
+
+	evaluator := NewEvaluator(formula)
+	base := time.Unix(0, 0)
+	for index := range steps {
+		if got := evaluator.ObserveAtStep(base.Add(time.Duration(index)*110*time.Millisecond), index+1); got != VerdictPending {
+			t.Fatalf("step %d: got %v, want pending", index+1, got)
+		}
+		if len(evaluator.pending) != 1 {
+			t.Fatalf("step %d: %d pending obligations, want 1", index+1, len(evaluator.pending))
+		}
+	}
+	if calls != steps {
+		t.Errorf("predicate ran %d times over %d steps, want one call per step", calls, steps)
+	}
+}
+
+// TestRoot_TopLevelEventuallyIsSatisfiedOnce pins the semantics behind that
+// bound: a top-level eventually is discharged for good the first time it is
+// satisfied. Under the old implicit-always reading it was re-armed at every
+// step, so a property that had already been reached could still violate later.
+func TestRoot_TopLevelEventuallyIsSatisfiedOnce(t *testing.T) {
+	reached := false
+	evaluator := NewEvaluator(EventuallyWithinSteps(ThunkNamed("p", func() (bool, error) {
+		return reached, nil
+	}), 2))
+
+	if got := evaluator.ObserveAtStep(time.Unix(0, 0), 1); got != VerdictPending {
+		t.Fatalf("step 1: got %v, want pending", got)
+	}
+	reached = true
+	if got := evaluator.ObserveAtStep(time.Unix(1, 0), 2); got != VerdictHolds {
+		t.Fatalf("step 2: got %v, want holds", got)
+	}
+	reached = false
+	for index := 3; index <= 6; index++ {
+		if got := evaluator.ObserveAtStep(time.Unix(int64(index), 0), index); got != VerdictHolds {
+			t.Fatalf("step %d: got %v, want holds (the goal was already reached)", index, got)
+		}
+	}
+	if got := evaluator.Finalize(); got != VerdictHolds {
+		t.Errorf("Finalize = %v, want holds", got)
+	}
+}
+
+// TestRoot_BoundedAlwaysKeepsItsBound: a bounded root Always is a single
+// window, not a recurrence. Stripping it and re-instantiating its inner every
+// step dropped the bound, so G<=1(p) behaved as G(p) and a false p after the
+// window closed still violated.
+func TestRoot_BoundedAlwaysKeepsItsBound(t *testing.T) {
+	values := []bool{true, true, false}
+	step := 0
+	formula := AlwaysFormula{
+		Inner:        ThunkNamed("p", func() (bool, error) { return values[step], nil }),
+		StepBound:    1,
+		HasStepBound: true,
+	}
+	evaluator := NewEvaluator(formula)
+	for index := range values {
+		step = index
+		if got := evaluator.ObserveAtStep(time.Unix(int64(index), 0), index+1); got == VerdictViolated {
+			t.Fatalf("step %d: violated outside the 1-step window", index+1)
+		}
+	}
+}
+
+// TestRoot_UnboundedAlwaysStillReInstantiates: the one-shot rule must not touch
+// the recurrence root every spec property is built on. Each step gets its own
+// instance of the inner, which is what gives a deferred failure the origin step
+// that armed it.
+func TestRoot_UnboundedAlwaysStillReInstantiates(t *testing.T) {
+	values := []bool{true, true, false}
+	step := 0
+	evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
+		return values[step], nil
+	})))
+	for index := range 2 {
+		step = index
+		if got := evaluator.ObserveAtStep(time.Unix(int64(index), 0), index+1); got != VerdictHolds {
+			t.Fatalf("step %d: got %v, want holds", index+1, got)
+		}
+	}
+	step = 2
+	if got := evaluator.ObserveAtStep(time.Unix(2, 0), 3); got != VerdictViolated {
+		t.Errorf("step 3: got %v, want violated", got)
+	}
+}