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

internal/ltl/evaluator.go

@@ -121,8 +121,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
+// Equal describe() keys mean the same operators over the same predicates with
-// its describe() key, so deduping cannot hide a violation.
+// 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
@@ -334,7 +337,7 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		return violatedWith(concrete, "pure false")
 
 	case ThunkFormula:
-		result, err := concrete.Func()
+		result, err := concrete.predicate()
 		if err != nil {
 			return violatedByError(concrete, err.Error())
 		}

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,41 @@ 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)
+	}
+}

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
+// PredicateLabel lets a ThunkFormula expose the caller's label for the closure
-// wraps. ThunkFormula satisfies it through its Name field; an empty name
+// it wraps. ThunkFormula satisfies it through the name passed to ThunkNamed;
-// serializes without a name.
+// 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
+// ThunkFormula wraps an opaque predicate closure. The closure returns the
-// boolean result and a non-nil error when the predicate threw; a thrown
+// predicate's boolean result and a non-nil error when the predicate threw; a
-// predicate is a witnessed violation distinct from a plain false. Name carries
+// thrown predicate is a witnessed violation distinct from a plain false.
-// the predicate's identity so two distinct predicates produce distinct
+//
-// describe() keys and are never merged during obligation collapse.
+// 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)
+	predicate func() (bool, error)
-	Name string
+	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 fmt.Sprintf("Thunk(%s#%d)", t.name, t.identity)
-		return "Thunk(" + t.Name + ")"
-	}
-	return "Thunk(...)"
 }
 func (n NowFormula) describe() string  { return "Now(" + n.Inner.describe() + ")" }
 func (n NextFormula) describe() string { return "Next(" + n.Inner.describe() + ")" }