sanderling/internal/ltl/finalize_test.go

package ltl

import (
	"testing"
	"testing/quick"
	"time"
)

func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) {
	evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil })))
	for index := range 3 {
		if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending {
			t.Fatalf("step %d: got %v, want pending", index, got)
		}
	}
	if got := evaluator.Finalize(); got != VerdictViolated {
		t.Errorf("Finalize = %v, want violated", got)
	}
}

func TestFinalize_FinalStepNextIsVacuouslyHolds(t *testing.T) {
	// A next obligation pending at run end has no successor state to check;
	// the run ending before the check is not a failure (weak next at the
	// trace boundary).
	evaluator := NewEvaluator(Next(ThunkNamed("p", func() (bool, error) { return true, nil })))
	if got := evaluator.Observe(); got != VerdictPending {
		t.Fatalf("step 1: got %v, want pending", got)
	}
	if got := evaluator.Finalize(); got != VerdictHolds {
		t.Errorf("Finalize = %v, want holds", got)
	}
	if witness := evaluator.Violation(); witness != nil {
		t.Errorf("Violation = %+v, want nil for a vacuous next", witness)
	}
}

func TestFinalize_AlwaysNextNeverReportsAtRunEnd(t *testing.T) {
	// always(next(p)): every step spawns a deferred check and the last one is
	// always pending when the run ends. That residue must not surface as an
	// end-of-run violation.
	evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { return true, nil }))))
	for index := range 3 {
		evaluator.ObserveAt(time.Unix(int64(index), 0))
	}
	if got := evaluator.Finalize(); got != VerdictHolds {
		t.Errorf("Finalize = %v, want holds", got)
	}
}

func TestFinalize_HoldingRunStaysHolds(t *testing.T) {
	evaluator := NewEvaluator(Always(Pure(true)))
	evaluator.Observe()
	if got := evaluator.Finalize(); got != VerdictHolds {
		t.Errorf("Finalize = %v, want holds", got)
	}
}

func TestFinalize_AlreadyViolatedStaysViolated(t *testing.T) {
	evaluator := NewEvaluator(Always(Pure(false)))
	if got := evaluator.Observe(); got != VerdictViolated {
		t.Fatalf("expected violated, got %v", got)
	}
	if got := evaluator.Finalize(); got != VerdictViolated {
		t.Errorf("Finalize = %v, want violated", got)
	}
}

func TestFinalize_BoundedAlwaysVacuouslyHolds(t *testing.T) {
	// A bounded Always whose window never closed (still pending) is safe.
	evaluator := NewEvaluator(EventuallyWithinSteps(Pure(false), 5))
	evaluator.Observe()
	// The negated form of this is a bounded Always; build it directly.
	bounded := NewEvaluator(Always(Not(EventuallyWithinSteps(ThunkNamed("p", func() (bool, error) { return false, nil }), 5))))
	bounded.Observe()
	if got := bounded.Finalize(); got == VerdictViolated {
		t.Errorf("bounded always should not finalize to violated, got %v", got)
	}
}

// TestEventuallyWithin_ViolatesIffNConsecutiveFalse locks the bounded
// eventually contract: with a step bound of n and an inner that is false for
// the first n observations, the verdict violates exactly at step n, and with at
// least one true observation inside the window it holds.
func TestEventuallyWithin_ViolatesIffNConsecutiveFalse(t *testing.T) {
	law := func(boundSeed uint8, trueAtSeed uint8) bool {
		bound := int(boundSeed%5) + 1
		// trueAt < 0 means inner is never true.
		trueAt := int(trueAtSeed)%(bound+2) - 1
		step := 0
		inner := ThunkNamed("p", func() (bool, error) {
			current := trueAt >= 0 && step == trueAt
			return current, nil
		})
		evaluator := NewEvaluator(EventuallyWithinSteps(inner, bound))

		satisfiedInWindow := trueAt >= 0 && trueAt < bound
		var final Verdict = VerdictPending
		for index := range bound {
			step = index
			final = evaluator.ObserveAt(time.Unix(int64(index), 0))
			if final == VerdictHolds || final == VerdictViolated {
				break
			}
		}

		if satisfiedInWindow {
			return final == VerdictHolds
		}
		return final == VerdictViolated
	}
	if err := quick.Check(law, nil); err != nil {
		t.Error(err)
	}
}

// TestViolationLatchIsMonotonic locks: once an evaluator reports Violated, every
// subsequent observation (and Finalize) stays Violated regardless of inputs.
func TestViolationLatchIsMonotonic(t *testing.T) {
	law := func(seed uint64) bool {
		values := make([]bool, 8)
		for index := range values {
			values[index] = (seed>>uint(index))&1 == 1
		}
		step := 0
		evaluator := NewEvaluator(Always(ThunkNamed("p", func() (bool, error) {
			current := values[step%len(values)]
			step++
			return current, nil
		})))
		seenViolated := false
		for index := range 16 {
			got := evaluator.ObserveAt(time.Unix(int64(index), 0))
			if got == VerdictViolated {
				seenViolated = true
			} else if seenViolated {
				return false
			}
		}
		if seenViolated && evaluator.Finalize() != VerdictViolated {
			return false
		}
		return true
	}
	if err := quick.Check(law, nil); err != nil {
		t.Error(err)
	}
}

// TestFinalize_KleeneConnectives locks the soundness guarantee in finalize's
// doc comment: an indefinite (pending) operand must never let a connective
// manufacture a definite verdict. Bug class: a pending side collapsing to
// 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 := 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}}

	cases := []struct {
		name    string
		formula Formula
		want    residualStatus
	}{
		{"and-pending-violated", AndFormula{Left: pendingThunk, Right: eventuallyViolated}, statusViolated},
		{"and-violated-pending", AndFormula{Left: nextPending, Right: eventuallyViolated}, statusViolated},
		{"and-pending-holds", AndFormula{Left: pendingThunk, Right: alwaysHolds}, statusPending},
		{"and-holds-holds", AndFormula{Left: pure(true), Right: alwaysHolds}, statusHolds},

		{"or-pending-violated", OrFormula{Left: pendingThunk, Right: eventuallyViolated}, statusPending},
		{"or-pending-holds", OrFormula{Left: pendingThunk, Right: alwaysHolds}, statusHolds},
		{"or-violated-violated", OrFormula{Left: pure(false), Right: eventuallyViolated}, statusViolated},

		{"not-pending", NotFormula{Inner: pendingThunk}, statusPending},
		{"not-violated", NotFormula{Inner: eventuallyViolated}, statusHolds},
		{"not-holds", NotFormula{Inner: alwaysHolds}, statusViolated},

		{"implies-pending-violated", ImpliesFormula{Antecedent: pendingThunk, Consequent: eventuallyViolated}, statusPending},
		{"implies-holds-violated", ImpliesFormula{Antecedent: alwaysHolds, Consequent: eventuallyViolated}, statusViolated},
		{"implies-violated-pending", ImpliesFormula{Antecedent: eventuallyViolated, Consequent: nextPending}, statusHolds},

		{"now-violated", NowFormula{Inner: eventuallyViolated}, statusViolated},
		{"now-pending", NowFormula{Inner: nextPending}, statusPending},
	}
	for _, tc := range cases {
		if got := finalize(tc.formula); got != tc.want {
			t.Errorf("%s: finalize = %v, want %v", tc.name, got, tc.want)
		}
	}
}

func TestCollapse_IdenticalObligationsMerge(t *testing.T) {
	merged := collapse([]obligation{
		{formula: Next(Pure(true)), origin: 1},
		{formula: Next(Pure(true)), origin: 2},
		{formula: Next(Pure(true)), origin: 3},
	})
	if len(merged) != 1 {
		t.Errorf("expected 1 obligation after collapse, got %d", len(merged))
	}
	if merged[0].origin != 1 {
		t.Errorf("collapse must keep the earliest origin, got %d", merged[0].origin)
	}
}

func TestCollapse_DistinctPredicatesDoNotMerge(t *testing.T) {
	merged := collapse([]obligation{
		{formula: Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil }))},
		{formula: Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil }))},
	})
	if len(merged) != 2 {
		t.Errorf("distinct predicates must not merge, got %d", len(merged))
	}
}

func TestCollapse_NamedThunkLeakBoundsPendingSet(t *testing.T) {
	// Always(Eventually(sameThunk)): each step spawns an identical obligation.
	// Without collapse the pending set grows unboundedly.
	evaluator := NewEvaluator(Always(Eventually(ThunkNamed("p", func() (bool, error) { return false, nil }))))
	for index := range 20 {
		evaluator.ObserveAt(time.Unix(int64(index), 0))
	}
	if len(evaluator.pending) > 2 {
		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")
	}
}