fix ltl semantics and unify action enumeration (#71)

* fix(ltl): give every thunk a construction identity

Two distinct unnamed predicates both described as "Thunk(...)", so obligation
collapse merged their residuals and could drop a live violation. Identity is
assigned at construction and the fields are unexported, so a thunk cannot be
built without one.

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

* fix(ltl): reduce a thrown-predicate residual instead of panicking

The verifier substitutes an ErrorFormula for the residual of a property whose
predicate threw, and that residual is fed back in on the next step. reduce had
no case for it, so the run crashed. It re-reports the same failure now.

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

* fix(ltl): make a bounded always the dual of a bounded eventually

G<=n(f) and not F<=n(not f) disagreed on traces where the inner was still
pending when the window closed, so nnf's negation normal form was not semantics
preserving. Both sides now range over the observations at which their inner can
definitely resolve: the eventually keeps a pending inner as a disjunct, and the
always discharges vacuously at window close.

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

* 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

* fix(verifier): stop wrapping a top-level eventually in always

`eventually(p).within(300, "seconds")` as a property meant "within 300 seconds
of every step", which spawned an obligation per step with its own resolved
deadline. A 553-step run carried 553 of them and serialized a 75 KB residual.

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

* fix(ltl): serialize the resolved deadline of a bounded window

Two obligations spawned at different steps from one duration-bounded formula
differ only in the deadline the evaluator resolved for them, so they serialized
identically and the trace erased a distinction the evaluator makes. The authored
window stays in amount/unit; the resolved deadline rides alongside.

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

* fix(verifier): split a witness's origin step from its detection step

A deferred obligation spans two steps: the one that armed it and the one whose
reduction failed. They were conflated under one index, so the extractor snapshot
(which is the detecting step's state) was reported against the origin step.

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

* fix(runner): record a witness's detection step in the trace

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

* feat(replay-ui): show the step a violation was detected at

The witness evidence is the detecting step's state, so say which step that is
and let a reader jump to it.

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

* fix(verifier): record the extractor state the predicates actually read

On the web path extractor bodies are evaluated in V8 and injected here, but only
the goja value was replaced. The trace diff and the violation witness therefore
described a state no property ever saw.

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

* refactor(spec): one candidate producer over one target-eligibility rule

Both hosts routed verbs themselves and both policies enumerated their own
actions, and all four drifted. Web sent `swipes` to scrollable containers only,
so swipe-to-dismiss on a list row was reachable on native and unreachable on
web; the model policy folded gestures its own way and could not reach what the
seeded picker drew.

A host now reports facts about every element and never decides which verb may
act on it: targets.ts acceptsTarget owns that for both. pick.ts builtinCandidates
is the single enumeration, and the model policy reads it through
__sanderlingEnumerateBuiltin__ instead of reimplementing it in Go.

Gesture verbs change with it: scrolls stay vertical over scrollable containers,
swipes go free-form in all four directions from any element with real bounds.

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

* fix(runner): name a builtin scroll by its drag origin

A builtin gesture carries endpoints and no selector, so every scroll rendered as
"Scroll down " in the prompt's recent-action memory and two scrollable regions
were indistinguishable.

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

* fix(chrome): clear storage over cdp instead of scripting an opaque origin

Launch runs while the tab is still on about:blank, whose opaque origin denies
storage access, so localStorage.clear() threw SecurityError and every web run
died at launch. Storage.clearDataForOrigin needs no navigation. The exception
helper lands here because "Uncaught" is what hid this for so long.

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

* fix(chrome): enable the swiftshader webgl fallback

Headless Chrome runs with --disable-gpu, and without this flag it refuses the
software WebGL backend: getContext returns null, so a canvas-rendered app paints
nothing and every screenshot is identical black.

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

* fix(web): resolve testTag through data-testid or id

Compose Multiplatform emits its testTag into the element id, which the native
table already accepts via the resource-id alias. The two web selector tables
were the only place that rejected it.

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

* test(spec): type-check the spec api as part of make test

The fake runtime in api.test.ts did not return a chainable handle from extract,
so the file had not type-checked since named() was added. Wiring the check into
make test stops it drifting again.

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

* docs(manual): one-shot eventually and the gesture verbs

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

internal/ltl/duality_test.go

@@ -0,0 +1,170 @@
+package ltl
+
+import (
+	"math/rand/v2"
+	"testing"
+	"testing/quick"
+	"time"
+)
+
+// dualityTrace holds the per-step truth of each predicate. The thunks read the
+// current step out of the trace rather than counting their own invocations, so
+// a formula and its negation see the same values no matter how many times each
+// predicate is reduced.
+type dualityTrace struct {
+	step   int
+	values [2][]bool
+}
+
+func newDualityTrace(random *rand.Rand, steps int) *dualityTrace {
+	trace := &dualityTrace{}
+	for index := range trace.values {
+		trace.values[index] = make([]bool, steps)
+		for step := range trace.values[index] {
+			trace.values[index][step] = random.IntN(2) == 0
+		}
+	}
+	return trace
+}
+
+func (t *dualityTrace) atoms() []Formula {
+	return []Formula{
+		ThunkNamed("p0", func() (bool, error) { return t.values[0][t.step], nil }),
+		ThunkNamed("p1", func() (bool, error) { return t.values[1][t.step], nil }),
+		Pure(true),
+		Pure(false),
+	}
+}
+
+// randomFormula draws a formula of at most the given depth over the atoms.
+// Every operator the evaluator can reduce is reachable, including the bounded
+// Always that only nnf produces.
+func randomFormula(random *rand.Rand, depth int, atoms []Formula) Formula {
+	if depth == 0 {
+		return atoms[random.IntN(len(atoms))]
+	}
+	inner := func() Formula { return randomFormula(random, depth-1, atoms) }
+	bound := random.IntN(3) + 1
+	switch random.IntN(12) {
+	case 0, 1:
+		return atoms[random.IntN(len(atoms))]
+	case 2:
+		return Not(inner())
+	case 3:
+		return Next(inner())
+	case 4:
+		return Now(inner())
+	case 5:
+		return And(inner(), inner())
+	case 6:
+		return Or(inner(), inner())
+	case 7:
+		return Implies(inner(), inner())
+	case 8:
+		return Always(inner())
+	case 9:
+		return Eventually(inner())
+	case 10:
+		if random.IntN(2) == 0 {
+			return EventuallyWithinSteps(inner(), bound)
+		}
+		return EventuallyWithin(inner(), time.Duration(bound)*time.Second)
+	default:
+		if random.IntN(2) == 0 {
+			return AlwaysFormula{Inner: inner(), StepBound: bound, HasStepBound: true}
+		}
+		return AlwaysFormula{Inner: inner(), Duration: time.Duration(bound) * time.Second}
+	}
+}
+
+// TestNNF_ExcludedMiddleHoldsOnRandomTraces is the semantic counterpart to the
+// describe()-comparing laws in nnf_test.go: those check that nnf produces the
+// syntax the dual laws predict, this checks that the syntax it produces means
+// the same thing. If any operator pair reduces non-dually then some trace makes
+// a formula and its own nnf-negation both violate, so their disjunction
+// violates and their conjunction holds.
+func TestNNF_ExcludedMiddleHoldsOnRandomTraces(t *testing.T) {
+	const steps = 8
+	law := func(seed uint64) bool {
+		random := rand.New(rand.NewPCG(seed, 0x9e3779b97f4a7c15))
+		trace := newDualityTrace(random, steps)
+		formula := randomFormula(random, 3, trace.atoms())
+
+		tautology := NewEvaluator(Or(formula, nnf(Not(formula))))
+		contradiction := NewEvaluator(And(formula, nnf(Not(formula))))
+		for index := range steps {
+			trace.step = index
+			now := time.Unix(int64(index), 0)
+			if tautology.ObserveAtStep(now, index+1) == VerdictViolated {
+				t.Logf("seed %d: %s violated at step %d", seed, Describe(formula), index+1)
+				return false
+			}
+			if contradiction.ObserveAtStep(now, index+1) == VerdictHolds {
+				t.Logf("seed %d: %s held at step %d", seed, Describe(formula), index+1)
+				return false
+			}
+		}
+		return tautology.Finalize() != VerdictViolated
+	}
+	if err := quick.Check(law, &quick.Config{MaxCount: 2000}); err != nil {
+		t.Error(err)
+	}
+}
+
+// TestNNF_BoundedAlwaysOverNextIsDual is the counterexample that showed nnf was
+// not semantics preserving: phi = G<=1(X p) with p true only at the first step.
+// Before the bounded operators were made dual, phi violated at step 2 and
+// nnf(not phi) violated at step 1, so both a formula and its negation failed on
+// one trace. Exactly one of the pair may violate.
+func TestNNF_BoundedAlwaysOverNextIsDual(t *testing.T) {
+	step := 0
+	predicate := ThunkNamed("p", func() (bool, error) { return step == 0, nil })
+	formula := AlwaysFormula{Inner: Next(predicate), StepBound: 1, HasStepBound: true}
+	negated := nnf(Not(formula))
+
+	run := func(root Formula) Verdict {
+		step = 0
+		evaluator := NewEvaluator(root)
+		for index := range 3 {
+			step = index
+			if evaluator.ObserveAtStep(time.Unix(int64(index), 0), index+1) == VerdictViolated {
+				return VerdictViolated
+			}
+		}
+		return evaluator.Finalize()
+	}
+
+	if got := run(formula); got == VerdictViolated {
+		t.Errorf("G<=1(X p) = %v; the window closes on a deferred check, which is not a breach", got)
+	}
+	if got := run(negated); got != VerdictViolated {
+		t.Errorf("nnf(not G<=1(X p)) = %v, want violated", got)
+	}
+	if got := run(Or(formula, negated)); got == VerdictViolated {
+		t.Errorf("excluded middle violated: %v", got)
+	}
+	if got := run(And(formula, negated)); got != VerdictViolated {
+		t.Errorf("phi and not phi = %v, want violated", got)
+	}
+}
+
+// TestEventually_PendingInnerSurvivesAsDisjunct locks the conjunct/disjunct
+// mirror the duality rests on: Always keeps a pending inner as a conjunct of
+// its residual, so Eventually must keep one as a disjunct. Dropping it made an
+// inner that can only discharge on a later step unsatisfiable.
+func TestEventually_PendingInnerSurvivesAsDisjunct(t *testing.T) {
+	values := []bool{false, true, false}
+	step := 0
+	formula := EventuallyWithinSteps(Next(ThunkNamed("p", func() (bool, error) {
+		return values[step], nil
+	})), 2)
+	evaluator := NewEvaluator(formula)
+
+	if got := evaluator.ObserveAtStep(time.Unix(0, 0), 1); got != VerdictPending {
+		t.Fatalf("step 1: got %v, want pending", got)
+	}
+	step = 1
+	if got := evaluator.ObserveAtStep(time.Unix(1, 0), 2); got != VerdictHolds {
+		t.Errorf("step 2: got %v, want holds (X p armed at step 1 discharged here)", got)
+	}
+}

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 := append(e.pending, fresh)
+	obligations := make([]obligation, 0, len(e.pending)+1)
+	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 {
@@ -121,8 +129,11 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict {
 
 // collapse removes structurally-identical obligations, keeping the first
 // occurrence in order so the surviving entry carries the earliest origin step.
-// Distinct predicates never merge because ThunkFormula's name participates in
-// its describe() key, so deduping cannot hide a violation.
+// Equal describe() keys mean the same operators over the same predicates with
+// the same remaining bounds, so the merged obligations reduce identically on
+// every future and dropping one cannot hide a violation. Distinct predicates
+// never merge because every thunk's construction-time identity is part of its
+// key, whether or not the caller named it.
 func collapse(obligations []obligation) []obligation {
 	if len(obligations) < 2 {
 		return obligations
@@ -264,10 +275,48 @@ func (e *Evaluator) Residual() Formula {
 	return combined
 }
 
-// rootObligation returns the formula to instantiate 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).
+// instantiateRoot returns the obligation to register for this observation, and
+// whether there is one at all. A one-shot root is armed only at the first
+// observation; a recurring root is re-asserted at every one.
+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
@@ -333,8 +382,14 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		}
 		return violatedWith(concrete, "pure false")
 
+	case ErrorFormula:
+		// A thrown predicate substituted into a residual at the trace
+		// boundary. Reducing it re-reports the same failure rather than
+		// crashing the run.
+		return violatedByError(concrete, concrete.Message)
+
 	case ThunkFormula:
-		result, err := concrete.Func()
+		result, err := concrete.predicate()
 		if err != nil {
 			return violatedByError(concrete, err.Error())
 		}
@@ -363,6 +418,9 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		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 {
 			return violatedFrom(innerResult, concrete, "eventually bound exhausted")
 		}
@@ -373,6 +431,14 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		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
+		// resolves on a later step unsatisfiable, and it is the mirror of the
+		// conjunct Always keeps below.
+		if innerResult.status == statusPending {
+			return pending(OrFormula{Left: innerResult.formula, Right: next})
+		}
 		return pending(next)
 
 	case ImpliesFormula:
@@ -444,25 +510,20 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		if innerResult.status == statusViolated {
 			return violatedFrom(innerResult, concrete, "always inner violated")
 		}
-		// A bounded Always is the dual of a bounded Eventually: once the window
-		// closes without a breach it is vacuously satisfied. A pending inner at
-		// the closing step is a deferred obligation (a strong next, or an inner
-		// liveness that has not discharged); it must be carried so a later step
-		// or Finalize resolves it, never dropped to holds.
+		// A bounded Always must reduce exactly as its dual does, so that
+		// G<=n(f) and not F<=n(not f) agree on every trace. The dual of "the
+		// window closed on an inner that never definitely held, so violate" is
+		// "the window closed on an inner that was never definitely breached, so
+		// 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 innerResult.status == statusHolds {
-				return holds()
-			}
-			return pending(innerResult.formula)
+			return holds()
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
-			if innerResult.status == statusHolds {
-				return holds()
-			}
-			return pending(innerResult.formula)
+			return holds()
 		}
 		next := concrete
-		next.Inner = concrete.Inner
 		if concrete.HasStepBound {
 			next.StepBound = concrete.StepBound - 1
 		}

internal/ltl/false_negative_test.go

@@ -70,14 +70,32 @@ func TestImplies_TemporalAntecedent_FalseAntecedentHolds(t *testing.T) {
 	}
 }
 
-// A bounded Always whose inner is a still-pending deferred Next obligation must
-// carry that obligation past the window, not drop it to holds. The pre-fix
-// window-close branch returned holds() unconditionally and lost the violation.
-func TestBoundedAlways_PendingInnerCarried(t *testing.T) {
-	inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true}
+// A bounded Always whose inner is definitely false inside the window violates.
+// The pre-fix window-close branch returned holds() unconditionally and lost
+// this; the breach check runs before the window check and must stay there.
+func TestBoundedAlways_ViolatedInnerInsideWindow(t *testing.T) {
+	inner := AlwaysFormula{Inner: Thunk(thunkSeq(false)), StepBound: 1, HasStepBound: true}
 	formula := Always(inner)
 	if verdict, _ := runAndFinalize(formula, 3); verdict != VerdictViolated {
-		t.Fatalf("Always(boundedAlways(Next(false),1)): got %v, want violated", verdict)
+		t.Fatalf("Always(boundedAlways(false,1)): got %v, want violated", verdict)
+	}
+}
+
+// A bounded Always whose inner is still a deferred Next obligation when the
+// window closes discharges vacuously: nothing was breached inside the window.
+// This is the exact dual of the bounded Eventually violating when its inner has
+// not held by the time the window closes
+// (TestEventuallyWithinSteps_NextInnerHitsBoundFirstStep), and the pair is what
+// makes nnf's G/F dualisation semantics preserving. It costs the deferred check
+// the window closed on: G<=n and F<=n both range over the observations at which
+// their inner can definitely resolve, never past them.
+func TestBoundedAlways_PendingInnerDischargesAtWindowClose(t *testing.T) {
+	inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true}
+	if verdict, _ := runAndFinalize(Always(inner), 3); verdict != VerdictHolds {
+		t.Fatalf("Always(boundedAlways(Next(false),1)): got %v, want holds", verdict)
+	}
+	if verdict, _ := runAndFinalize(Always(nnf(Not(inner))), 3); verdict != VerdictViolated {
+		t.Fatalf("its negation: got %v, want violated", verdict)
 	}
 }
 

internal/ltl/finalize_test.go

@@ -152,7 +152,7 @@ func TestViolationLatchIsMonotonic(t *testing.T) {
 // holds/violated at run end, making sanderling lie about pass/fail.
 func TestFinalize_KleeneConnectives(t *testing.T) {
 	pure := func(v bool) Formula { return PureFormula{Value: v} }
-	pendingThunk := ThunkFormula{Name: "t", Func: func() (bool, error) { return true, nil }}
+	pendingThunk := ThunkNamed("t", func() (bool, error) { return true, nil })
 	eventuallyViolated := EventuallyFormula{Inner: PureFormula{Value: false}}
 	nextPending := NextFormula{Inner: PureFormula{Value: true}}
 	alwaysHolds := AlwaysFormula{Inner: PureFormula{Value: true}}
@@ -224,3 +224,61 @@ func TestCollapse_NamedThunkLeakBoundsPendingSet(t *testing.T) {
 		t.Errorf("pending set leaked to %d obligations", len(evaluator.pending))
 	}
 }
+
+// TestCollapse_UnnamedPredicatesDoNotMerge is the lost-violation counterexample
+// from the attribution analysis, run with unnamed thunks. Every unnamed thunk
+// used to print "Thunk(...)", so the four Eventually residuals below shared one
+// collapse key and the obligation spawned at step 2 was dropped: the run
+// reported holds while a genuine violation was outstanding.
+//
+//	root = And(Or(F a, c), Or(F b, d)), d = not c
+//	a never true, b true from step 6, c true except at steps 2 and 4
+//
+// At steps 1, 3 and 5 the left disjunct discharges via c and the right spawns
+// F b; at steps 2 and 4 the right discharges via d and the left spawns F a.
+// F a can never discharge, so the run violates with origin 2.
+func TestCollapse_UnnamedPredicatesDoNotMerge(t *testing.T) {
+	step := 0
+	a := Thunk(func() (bool, error) { return false, nil })
+	b := Thunk(func() (bool, error) { return step >= 6, nil })
+	c := Thunk(func() (bool, error) { return step != 2 && step != 4, nil })
+	d := Thunk(func() (bool, error) { return step == 2 || step == 4, nil })
+
+	evaluator := NewEvaluator(And(Or(Eventually(a), c), Or(Eventually(b), d)))
+	for index := 1; index <= 10; index++ {
+		step = index
+		if got := evaluator.ObserveAtStep(time.Unix(int64(index), 0), index); got == VerdictViolated {
+			t.Fatalf("step %d violated early", index)
+		}
+	}
+	if got := evaluator.Finalize(); got != VerdictViolated {
+		t.Fatalf("Finalize = %v, want violated (F a can never discharge)", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil, want non-nil")
+	}
+	if witness.Step != 2 {
+		t.Errorf("origin = %d, want 2", witness.Step)
+	}
+}
+
+// TestReduce_ErrorFormulaViolates: the verifier substitutes an ErrorFormula for
+// the residual of a property whose predicate threw, and that residual is fed
+// back into the evaluator on the next step. Reducing one used to panic.
+func TestReduce_ErrorFormulaViolates(t *testing.T) {
+	evaluator := NewEvaluator(Always(ErrorFormula{Message: "boom"}))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("got %v, want violated", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil, want non-nil")
+	}
+	if witness.Reason != "boom" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "boom")
+	}
+	if !witness.IsError {
+		t.Error("IsError = false, want true")
+	}
+}

internal/ltl/formula.go

@@ -4,6 +4,7 @@ import (
 	"encoding/json"
 	"fmt"
 	"strings"
+	"sync/atomic"
 	"time"
 )
 
@@ -13,9 +14,9 @@ type Formula interface {
 	describe() string
 }
 
-// PredicateLabel lets a ThunkFormula expose the identity of the closure it
-// wraps. ThunkFormula satisfies it through its Name field; an empty name
-// serializes without a name.
+// PredicateLabel lets a ThunkFormula expose the caller's label for the closure
+// it wraps. ThunkFormula satisfies it through the name passed to ThunkNamed;
+// an unnamed thunk serializes without a name.
 type PredicateLabel interface {
 	PredicateName() string
 }
@@ -50,17 +51,26 @@ type PureFormula struct {
 	Value bool
 }
 
-// ThunkFormula wraps an opaque predicate closure. Func returns the predicate's
-// boolean result and a non-nil error when the predicate threw; a thrown
-// predicate is a witnessed violation distinct from a plain false. Name carries
-// the predicate's identity so two distinct predicates produce distinct
-// describe() keys and are never merged during obligation collapse.
+// ThunkFormula wraps an opaque predicate closure. The closure returns the
+// predicate's boolean result and a non-nil error when the predicate threw; a
+// thrown predicate is a witnessed violation distinct from a plain false.
+//
+// Every thunk carries an identity assigned at construction, and the identity
+// is part of its describe() key. Two thunks are therefore equal keys only when
+// they are copies of the same constructed value, which is what lets obligation
+// collapse merge residuals without ever merging distinct predicates. The
+// fields are unexported so a thunk cannot be built without one.
 type ThunkFormula struct {
-	Func func() (bool, error)
-	Name string
+	predicate func() (bool, error)
+	name      string
+	identity  uint64
 }
 
-func (t ThunkFormula) PredicateName() string { return t.Name }
+func (t ThunkFormula) PredicateName() string { return t.name }
+
+// thunkIdentities hands out the per-thunk identity. It only has to separate
+// thunks within one process, so a counter is enough.
+var thunkIdentities atomic.Uint64
 
 // NowFormula marks its inner formula for evaluation at the current step only.
 // Primarily used so that now(...).implies(...) parses unambiguously.
@@ -113,10 +123,16 @@ func Always(inner Formula) Formula { return AlwaysFormula{Inner: inner} }
 
 func Pure(value bool) Formula { return PureFormula{Value: value} }
 
-func Thunk(function func() (bool, error)) Formula { return ThunkFormula{Func: function} }
+func Thunk(function func() (bool, error)) Formula {
+	return ThunkFormula{predicate: function, identity: thunkIdentities.Add(1)}
+}
 
 func ThunkNamed(name string, function func() (bool, error)) Formula {
-	return ThunkFormula{Func: function, Name: name}
+	return ThunkFormula{
+		predicate: function,
+		name:      name,
+		identity:  thunkIdentities.Add(1),
+	}
 }
 
 func Now(inner Formula) Formula { return NowFormula{Inner: inner} }
@@ -172,10 +188,7 @@ func (a AlwaysFormula) describe() string {
 }
 func (p PureFormula) describe() string { return fmt.Sprintf("Pure(%t)", p.Value) }
 func (t ThunkFormula) describe() string {
-	if t.Name != "" {
-		return "Thunk(" + t.Name + ")"
-	}
-	return "Thunk(...)"
+	return fmt.Sprintf("Thunk(%s#%d)", t.name, t.identity)
 }
 func (n NowFormula) describe() string  { return "Now(" + n.Inner.describe() + ")" }
 func (n NextFormula) describe() string { return "Next(" + n.Inner.describe() + ")" }
@@ -206,10 +219,43 @@ func (n NotFormula) describe() string { return "Not(" + n.Inner.describe() + ")"
 func Describe(formula Formula) string { return formula.describe() }
 
 // withinNode mirrors the optional `within` clause attached to bounded
-// Eventually nodes in the JSON AST.
+// Always/Eventually nodes in the JSON AST.
 type withinNode struct {
 	Amount int64  `json:"amount"`
 	Unit   string `json:"unit"`
+	// Deadline is the absolute instant the window closes, in unix
+	// milliseconds, present once the evaluator resolved a relative duration
+	// against an observation. Two obligations spawned at different steps from
+	// 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"`
+}
+
+// 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
+	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"}
+	default:
+		return nil
+	}
+	if hasDeadline {
+		node.Deadline = deadline.UnixMilli()
+	}
+	return node
 }
 
 func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
@@ -218,14 +264,9 @@ func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "always", Arg: a.Inner}
-	switch {
-	case a.HasStepBound:
-		payload.Within = &withinNode{Amount: int64(a.StepBound), Unit: "steps"}
-	case a.Duration > 0:
-		payload.Within = &withinNode{Amount: a.Duration.Milliseconds(), Unit: "milliseconds"}
-	case a.HasDeadline:
-		payload.Within = &withinNode{Amount: a.Deadline.UnixMilli(), Unit: "deadline"}
-	}
+	payload.Within = withinFor(
+		a.HasStepBound, a.StepBound, a.Duration, a.HasDeadline, a.Deadline,
+	)
 	return json.Marshal(payload)
 }
 
@@ -256,14 +297,9 @@ func (e EventuallyFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "eventually", Arg: e.Inner}
-	switch {
-	case e.HasStepBound:
-		payload.Within = &withinNode{Amount: int64(e.StepBound), Unit: "steps"}
-	case e.Duration > 0:
-		payload.Within = &withinNode{Amount: e.Duration.Milliseconds(), Unit: "milliseconds"}
-	case e.HasDeadline:
-		payload.Within = &withinNode{Amount: e.Deadline.UnixMilli(), Unit: "deadline"}
-	}
+	payload.Within = withinFor(
+		e.HasStepBound, e.StepBound, e.Duration, e.HasDeadline, e.Deadline,
+	)
 	return json.Marshal(payload)
 }
 

internal/ltl/formula_test.go

@@ -288,3 +288,32 @@ func TestResidual_HoldsViolatedPending(t *testing.T) {
 		t.Errorf("pending residual:\n got: %s\nwant: %s", body, want)
 	}
 }
+
+// TestMarshalJSON_ResolvedDeadlineDistinguishesObligations: obligations spawned
+// at different steps from one duration-bounded eventually differ only in the
+// deadline the evaluator resolved for them, and collapse keeps them apart on
+// exactly that. The serialized AST has to keep them apart too, or the trace
+// shows N copies of one node where the evaluator has N different obligations.
+func TestMarshalJSON_ResolvedDeadlineDistinguishesObligations(t *testing.T) {
+	base := time.UnixMilli(1700000000000)
+	first := EventuallyFormula{
+		Inner:       PureFormula{Value: false},
+		Duration:    300 * time.Second,
+		Deadline:    base.Add(300 * time.Second),
+		HasDeadline: true,
+	}
+	second := first
+	second.Deadline = base.Add(301 * time.Second)
+
+	firstBody, _ := json.Marshal(first)
+	secondBody, _ := json.Marshal(second)
+	if string(firstBody) == string(secondBody) {
+		t.Errorf("obligations with different deadlines serialize identically: %s", firstBody)
+	}
+	if !strings.Contains(string(firstBody), `"unit":"milliseconds"`) {
+		t.Errorf("authored window lost: %s", firstBody)
+	}
+	if !strings.Contains(string(firstBody), `"deadline":1700000300000`) {
+		t.Errorf("resolved deadline missing: %s", firstBody)
+	}
+}

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)
+	}
+}