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

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

@@ -372,6 +372,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")
 		}
@@ -382,6 +385,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:
@@ -453,25 +464,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
+		// A bounded Always must reduce exactly as its dual does, so that
-		// closes without a breach it is vacuously satisfied. A pending inner at
+		// G<=n(f) and not F<=n(not f) agree on every trace. The dual of "the
-		// the closing step is a deferred obligation (a strong next, or an inner
+		// window closed on an inner that never definitely held, so violate" is
-		// liveness that has not discharged); it must be carried so a later step
+		// "the window closed on an inner that was never definitely breached, so
-		// or Finalize resolves it, never dropped to holds.
+		// 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 holds()
-			}
-			return pending(innerResult.formula)
 		}
 		if concrete.HasDeadline && !now.Before(concrete.Deadline) {
-			if innerResult.status == statusHolds {
+			return holds()
-				return holds()
-			}
-			return pending(innerResult.formula)
 		}
 		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
+// A bounded Always whose inner is definitely false inside the window violates.
-// carry that obligation past the window, not drop it to holds. The pre-fix
+// The pre-fix window-close branch returned holds() unconditionally and lost
-// window-close branch returned holds() unconditionally and lost the violation.
+// this; the breach check runs before the window check and must stay there.
-func TestBoundedAlways_PendingInnerCarried(t *testing.T) {
+func TestBoundedAlways_ViolatedInnerInsideWindow(t *testing.T) {
-	inner := AlwaysFormula{Inner: Next(Thunk(thunkSeq(false))), StepBound: 1, HasStepBound: true}
+	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)
 	}
 }