feat(oracle-reduction): replay stored traces under four reduced oracles

re-evaluates each trace offline under the full engine, a crash-only detector, a single-state check and a single-step property triple, and reports what each refutes: the oracles vary while the traces stay fixed, which separates a defect an oracle cannot express from one an explorer never reached. a disagreement with the verdicts a run recorded exits nonzero rather than being counted as a finding.

cmd/internal-tools/oracle-reduction/reduce.go

@@ -0,0 +1,281 @@
+package main
+
+import (
+	"fmt"
+	"time"
+
+	"github.com/priyanshujain/sanderling/internal/ltl"
+)
+
+// tripleWindow is the horizon a property triple has: an obligation armed at one
+// observation must discharge at the next, and nothing outlives that.
+const tripleWindow = 2
+
+// singleStateFormula is what a checker holding one observation can refute.
+// Every operator that defers or repeats an obligation is replaced by the
+// constant that makes the formula around it trivially satisfied, so the only
+// refutation left is a predicate read at a single observation. The outermost
+// always survives because it is what says "check this at each observation",
+// which costs no history.
+func singleStateFormula(formula ltl.Formula) ltl.Formula {
+	if always, ok := formula.(ltl.AlwaysFormula); ok {
+		always.Inner = stateless(always.Inner, true)
+		return always
+	}
+	return stateless(formula, true)
+}
+
+// singleStepFormula is the property triple: one step of history, and no
+// obligation surviving past the next observation. A next keeps its one-step
+// deferral, and an eventually of any window shrinks to the two observations a
+// triple spans.
+func singleStepFormula(formula ltl.Formula) ltl.Formula {
+	if always, ok := formula.(ltl.AlwaysFormula); ok {
+		always.Inner = oneStep(always.Inner, true)
+		return always
+	}
+	return oneStep(formula, true)
+}
+
+// singleStateExpresses and singleStepExpresses decide, from the property's form
+// alone, whether the reduced oracle can still state the property after its
+// rewrite. An oracle that cannot state a property does not get to refute it,
+// and is reported as silent on it rather than as either verdict.
+//
+// Two shapes defeat a reduction. The rewrite shortens an obligation window the
+// oracle's horizon cannot hold, leaving it to refute a property strictly
+// stronger than the one the author wrote. Or the rewrite leaves a formula whose
+// verdict no longer depends on the trace, leaving it to report the same answer
+// everywhere. Either way the column would carry a verdict about a property
+// nobody wrote, which is worth less than an admission that the oracle is out of
+// its depth.
+func singleStateExpresses(formula ltl.Formula) bool {
+	return dependsOnTrace(singleStateFormula(formula))
+}
+
+func singleStepExpresses(formula ltl.Formula) bool {
+	return !truncatesWindow(formula) &&
+		dependsOnTrace(singleStepFormula(formula))
+}
+
+// truncatesWindow reports whether the single-step rewrite had to shorten a
+// window to fit a triple. Where it did, the reduced oracle is checking a
+// stronger property than the author wrote, so a refutation of it is not the
+// same event as a refutation of the property.
+func truncatesWindow(formula ltl.Formula) bool {
+	if always, ok := formula.(ltl.AlwaysFormula); ok {
+		return shortensWindow(always.Inner, true)
+	}
+	return shortensWindow(formula, true)
+}
+
+// shortensWindow walks the same shape oneStep rewrites, and reports only the
+// shortening that strengthens the formula. Polarity is what separates the two:
+// a shorter window under an even number of negations demands the same thing
+// sooner, so a refutation of it need not be a refutation of the property, while
+// under an odd number it asks for less and its refutations stay sound. The
+// operators oneStep erases rather than shortens are erased to the constant its
+// position is satisfied by, which also only asks for less.
+func shortensWindow(formula ltl.Formula, positive bool) bool {
+	switch concrete := formula.(type) {
+	case ltl.EventuallyFormula:
+		return positive && windowOutlastsTriple(concrete)
+	case ltl.NowFormula:
+		return shortensWindow(concrete.Inner, positive)
+	case ltl.NotFormula:
+		return shortensWindow(concrete.Inner, !positive)
+	case ltl.AndFormula:
+		return shortensWindow(concrete.Left, positive) || shortensWindow(concrete.Right, positive)
+	case ltl.OrFormula:
+		return shortensWindow(concrete.Left, positive) || shortensWindow(concrete.Right, positive)
+	case ltl.ImpliesFormula:
+		return shortensWindow(concrete.Antecedent, !positive) || shortensWindow(concrete.Consequent, positive)
+	default:
+		return false
+	}
+}
+
+// windowOutlastsTriple asks whether an obligation can still be open after the
+// two observations a triple spans. A window counted in time is outside what a
+// triple can state whatever its length, because a triple has no clock: it can
+// say "at the next observation" and nothing about when that arrives.
+func windowOutlastsTriple(formula ltl.EventuallyFormula) bool {
+	if formula.HasStepBound {
+		return formula.StepBound > tripleWindow
+	}
+	return true
+}
+
+// dependsOnTrace reports whether a rewritten formula can still read the trace.
+// Constants fold through the connectives, and one that folds away to a constant
+// answers the same on every trace: silence that reads as "did not refute", or a
+// refutation of everything. Neither is a verdict about the run.
+func dependsOnTrace(formula ltl.Formula) bool {
+	_, constant := fold(formula).(ltl.PureFormula)
+	return !constant
+}
+
+// fold propagates the constants the rewrites substituted for erased operators.
+// An obligation whose inner formula folded to false keeps its shape, because a
+// deferred false is a refutation still owed; only the side that can no longer
+// fail folds away.
+func fold(formula ltl.Formula) ltl.Formula {
+	switch concrete := formula.(type) {
+	case ltl.AlwaysFormula:
+		concrete.Inner = fold(concrete.Inner)
+		if pure, ok := concrete.Inner.(ltl.PureFormula); ok {
+			return pure
+		}
+		return concrete
+	case ltl.EventuallyFormula:
+		concrete.Inner = fold(concrete.Inner)
+		if isPure(concrete.Inner, true) {
+			return ltl.Pure(true)
+		}
+		return concrete
+	case ltl.NextFormula:
+		inner := fold(concrete.Inner)
+		if isPure(inner, true) {
+			return ltl.Pure(true)
+		}
+		return ltl.Next(inner)
+	case ltl.NowFormula:
+		inner := fold(concrete.Inner)
+		if _, ok := inner.(ltl.PureFormula); ok {
+			return inner
+		}
+		return ltl.Now(inner)
+	case ltl.NotFormula:
+		inner := fold(concrete.Inner)
+		if pure, ok := inner.(ltl.PureFormula); ok {
+			return ltl.Pure(!pure.Value)
+		}
+		return ltl.Not(inner)
+	case ltl.AndFormula:
+		left, right := fold(concrete.Left), fold(concrete.Right)
+		switch {
+		case isPure(left, false) || isPure(right, false):
+			return ltl.Pure(false)
+		case isPure(left, true):
+			return right
+		case isPure(right, true):
+			return left
+		}
+		return ltl.And(left, right)
+	case ltl.OrFormula:
+		left, right := fold(concrete.Left), fold(concrete.Right)
+		switch {
+		case isPure(left, true) || isPure(right, true):
+			return ltl.Pure(true)
+		case isPure(left, false):
+			return right
+		case isPure(right, false):
+			return left
+		}
+		return ltl.Or(left, right)
+	case ltl.ImpliesFormula:
+		antecedent, consequent := fold(concrete.Antecedent), fold(concrete.Consequent)
+		switch {
+		case isPure(antecedent, false) || isPure(consequent, true):
+			return ltl.Pure(true)
+		case isPure(antecedent, true):
+			return consequent
+		}
+		return ltl.Implies(antecedent, consequent)
+	default:
+		return formula
+	}
+}
+
+func isPure(formula ltl.Formula, value bool) bool {
+	pure, ok := formula.(ltl.PureFormula)
+	return ok && pure.Value == value
+}
+
+// stateless erases every temporal operator. The replacement constant follows
+// the position's polarity: under an even number of negations a temporal
+// sub-formula is dropped as satisfied, and under an odd number as failed, so
+// that in both cases its negation cannot refute anything either.
+func stateless(formula ltl.Formula, positive bool) ltl.Formula {
+	switch concrete := formula.(type) {
+	case ltl.AlwaysFormula, ltl.NextFormula, ltl.EventuallyFormula:
+		return ltl.Pure(positive)
+	case ltl.NowFormula:
+		return ltl.Now(stateless(concrete.Inner, positive))
+	case ltl.NotFormula:
+		return ltl.Not(stateless(concrete.Inner, !positive))
+	case ltl.AndFormula:
+		return ltl.And(stateless(concrete.Left, positive), stateless(concrete.Right, positive))
+	case ltl.OrFormula:
+		return ltl.Or(stateless(concrete.Left, positive), stateless(concrete.Right, positive))
+	case ltl.ImpliesFormula:
+		return ltl.Implies(
+			stateless(concrete.Antecedent, !positive),
+			stateless(concrete.Consequent, positive),
+		)
+	default:
+		return formula
+	}
+}
+
+func oneStep(formula ltl.Formula, positive bool) ltl.Formula {
+	switch concrete := formula.(type) {
+	case ltl.AlwaysFormula:
+		return ltl.Pure(positive)
+	case ltl.NextFormula:
+		return ltl.Next(stateless(concrete.Inner, positive))
+	case ltl.EventuallyFormula:
+		return ltl.EventuallyWithinSteps(stateless(concrete.Inner, positive), tripleWindow)
+	case ltl.NowFormula:
+		return ltl.Now(oneStep(concrete.Inner, positive))
+	case ltl.NotFormula:
+		return ltl.Not(oneStep(concrete.Inner, !positive))
+	case ltl.AndFormula:
+		return ltl.And(oneStep(concrete.Left, positive), oneStep(concrete.Right, positive))
+	case ltl.OrFormula:
+		return ltl.Or(oneStep(concrete.Left, positive), oneStep(concrete.Right, positive))
+	case ltl.ImpliesFormula:
+		return ltl.Implies(
+			oneStep(concrete.Antecedent, !positive),
+			oneStep(concrete.Consequent, positive),
+		)
+	default:
+		return formula
+	}
+}
+
+// propertyClass splits safety from liveness by the property's top-level form:
+// a reachability goal is liveness, everything else is a safety obligation
+// re-asserted at each observation.
+func propertyClass(formula ltl.Formula) string {
+	if _, ok := formula.(ltl.EventuallyFormula); ok {
+		return "liveness"
+	}
+	return "safety"
+}
+
+func topLevelForm(formula ltl.Formula) string {
+	switch concrete := formula.(type) {
+	case ltl.AlwaysFormula:
+		return "always" + boundSuffix(concrete.HasStepBound, concrete.StepBound, concrete.Duration)
+	case ltl.EventuallyFormula:
+		return "eventually" + boundSuffix(concrete.HasStepBound, concrete.StepBound, concrete.Duration)
+	default:
+		return "predicate"
+	}
+}
+
+func boundSuffix(
+	hasStepBound bool,
+	stepBound int,
+	duration time.Duration,
+) string {
+	switch {
+	case hasStepBound:
+		return fmt.Sprintf(" within %d steps", stepBound)
+	case duration > 0:
+		return fmt.Sprintf(" within %s", duration)
+	default:
+		return ""
+	}
+}