From f346864b2fd3b7b62f67281304647405ff79dbca Mon Sep 17 00:00:00 2001 From: PJ Date: Mon, 1 Jun 2026 13:56:11 +0530 Subject: [PATCH] refactor(verifier): replace predicate err side-channel with violation witness --- internal/verifier/bindings.go | 5 - internal/verifier/worker.go | 166 ++++++++++++++++++++-------------- 2 files changed, 97 insertions(+), 74 deletions(-) diff --git a/internal/verifier/bindings.go b/internal/verifier/bindings.go index eaae32a..4c63a87 100644 --- a/internal/verifier/bindings.go +++ b/internal/verifier/bindings.go @@ -20,11 +20,6 @@ type extractorState struct { type formulaState struct { predicate goja.Callable - // err holds the goja error from this thunk's most recent invocation, or - // nil if the latest call succeeded. The thunk returns false on error so - // the LTL evaluator marks the property violated; PredicateError surfaces - // the underlying cause for the current step. - err error } type specKind int diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go index 0d68f55..2252437 100644 --- a/internal/verifier/worker.go +++ b/internal/verifier/worker.go @@ -31,6 +31,7 @@ type Verifier struct { priorVerdicts map[string]ltl.Verdict newlyViolated []string + witnesses map[string]Witness lastTree *hierarchy.Tree lastAction *Action @@ -64,6 +65,7 @@ func New(options ...Option) (*Verifier, error) { properties: map[string]int{}, evaluators: map[string]*ltl.Evaluator{}, priorVerdicts: map[string]ltl.Verdict{}, + witnesses: map[string]Witness{}, rng: rand.New(rand.NewPCG(0, 0)), } for _, option := range options { @@ -139,7 +141,8 @@ func (v *Verifier) buildFormulaNode(index int) (ltl.Formula, error) { case specKindPure: return ltl.Pure(spec.pureValue), nil case specKindThunk: - return ltl.Thunk(v.formulaThunk(spec.predicateIndex)), nil + name := fmt.Sprintf("p%d", spec.predicateIndex) + return ltl.ThunkNamed(name, v.formulaThunk(spec.predicateIndex)), nil case specKindNow: child, err := v.buildFormulaNode(spec.childA) if err != nil { @@ -244,7 +247,6 @@ func (v *Verifier) PushSnapshot(input SnapshotInput) error { // Extractor previous/current advance exactly once per PushSnapshot. // Predicate thunks read these slots but never trigger advancement, so // invoking a thunk multiple times between snapshots is value-stable. - // refreshPredicateErrors relies on this to safely re-call predicates. for index, extractor := range v.extractors { previous := extractor.handle.Get("current") _ = extractor.handle.Set("previous", previous) @@ -362,12 +364,12 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict { for name, evaluator := range v.evaluators { verdicts[name] = evaluator.ObserveAt(stepTime) } - v.refreshPredicateErrors() var onset []string for name, verdict := range verdicts { if verdict == ltl.VerdictViolated && v.priorVerdicts[name] != ltl.VerdictViolated { onset = append(onset, name) + v.captureWitness(name) } } sort.Strings(onset) @@ -380,6 +382,89 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict { return verdicts } +// Witness is the verifier-level record of a property violation: the LTL reason +// (a predicate's thrown-error text, "predicate false", or a liveness failure), +// the step it fired at, and a snapshot of every extractor's current value at +// that step. The snapshot lets a reader see the state that produced the +// violation without replaying the run. +type Witness struct { + Property string + Reason string + Step int + IsError bool + Extractors map[string]json.RawMessage +} + +// captureWitness records the witness for a property that just transitioned to +// violated, snapshotting the current extractor values so the cause is visible +// after the run. +func (v *Verifier) captureWitness(name string) { + evaluator, ok := v.evaluators[name] + if !ok { + return + } + violation := evaluator.Violation() + if violation == nil { + return + } + v.witnesses[name] = Witness{ + Property: name, + Reason: violation.Reason, + Step: violation.Step, + IsError: violation.IsError, + Extractors: v.extractorSnapshot(), + } +} + +// extractorSnapshot encodes every named extractor's current value as JSON. A +// nil value (extractor never advanced or its value did not survive Export) +// is recorded as JSON null. +func (v *Verifier) extractorSnapshot() map[string]json.RawMessage { + if len(v.extractors) == 0 { + return nil + } + snapshot := make(map[string]json.RawMessage, len(v.extractors)) + for _, extractor := range v.extractors { + value := extractor.curr + if value == nil { + value = []byte("null") + } + snapshot[extractor.name] = append(json.RawMessage(nil), value...) + } + return snapshot +} + +// Witness returns the captured violation witness for a property, or nil if the +// property has not violated. Callers consult this after EvaluateProperties (or +// Finalize) reports a violation to surface the cause and the state at onset. +func (v *Verifier) Witness(name string) *Witness { + witness, ok := v.witnesses[name] + if !ok { + return nil + } + return &witness +} + +// Finalize drives each evaluator to its terminal verdict and returns the names +// of properties that violate only at run end (a liveness obligation that never +// discharged), capturing a witness for each. Properties already violated +// mid-run are not re-reported here. +func (v *Verifier) Finalize() []string { + var ended []string + for name, evaluator := range v.evaluators { + if v.priorVerdicts[name] == ltl.VerdictViolated { + continue + } + if evaluator.Finalize() == ltl.VerdictViolated { + ended = append(ended, name) + v.captureWitness(name) + v.priorVerdicts[name] = ltl.VerdictViolated + } + } + sort.Strings(ended) + return ended +} + // NewlyViolatedProperties returns the names of properties whose verdict // transitioned from non-Violated to Violated on the most recent // EvaluateProperties call, sorted lexicographically. Returns nil if no @@ -396,14 +481,14 @@ func (v *Verifier) NewlyViolatedProperties() []string { } // Residuals returns the residual formula for each registered property after -// the most recent EvaluateProperties call. Properties that errored during -// predicate evaluation surface as ErrorFormula so the inspect UI can render -// "predicate threw" inline. +// the most recent EvaluateProperties call. Properties whose violation was +// caused by a thrown predicate surface as ErrorFormula, sourced from the +// captured witness, so the inspect UI can render "predicate threw" inline. func (v *Verifier) Residuals() map[string]ltl.Formula { residuals := map[string]ltl.Formula{} for name, evaluator := range v.evaluators { - if predicateErr := v.PredicateError(name); predicateErr != nil { - residuals[name] = ltl.ErrorFormula{Message: predicateErr.Error()} + if witness, ok := v.witnesses[name]; ok && witness.IsError { + residuals[name] = ltl.ErrorFormula{Message: witness.Reason} continue } residuals[name] = evaluator.Residual() @@ -445,74 +530,17 @@ func (v *Verifier) NextAction() (Action, error) { var ErrNoAction = errors.New("verifier: no action available") -func (v *Verifier) formulaThunk(index int) func() bool { - return func() bool { +func (v *Verifier) formulaThunk(index int) func() (bool, error) { + return func() (bool, error) { formula := v.formulas[index] result, err := formula.predicate(goja.Undefined()) if err != nil { - formula.err = err - return false + return false, err } - formula.err = nil - return result.ToBoolean() + return result.ToBoolean(), nil } } -// refreshPredicateErrors re-invokes every registered predicate so that -// formula.err reflects the current step rather than a latched first-step -// throw. EvaluateProperties short-circuits once a property has latched to -// violated, so without this refresh the runner's per-step "predicate error" -// log freezes on whatever the predicate threw at step 1. The refreshed errors -// have no effect on verdicts. -// -// Invariant: predicates may be re-invoked here outside the LTL gate that -// would normally skip them (e.g. an `implies` consequent whose antecedent is -// false). They must therefore be side-effect-free reads of extractor state; -// any spec that asserts internal preconditions inside a predicate could -// surface a spurious error in the inspect UI without affecting verdicts. -func (v *Verifier) refreshPredicateErrors() { - for _, formula := range v.formulas { - result, err := formula.predicate(goja.Undefined()) - if err != nil { - formula.err = err - continue - } - _ = result - formula.err = nil - } -} - -// PredicateError returns the first goja error raised by any thunk in the -// named property's formula tree, or nil if none fired. Callers typically -// consult this after EvaluateProperties reports a violation to distinguish -// a genuine predicate-false verdict from a malformed spec. -func (v *Verifier) PredicateError(name string) error { - rootIndex, ok := v.properties[name] - if !ok { - return nil - } - return v.firstThunkError(rootIndex) -} - -func (v *Verifier) firstThunkError(index int) error { - if index < 0 || index >= len(v.formulaSpecs) { - return nil - } - spec := v.formulaSpecs[index] - switch spec.kind { - case specKindThunk: - return v.formulas[spec.predicateIndex].err - case specKindImplies, specKindOr, specKindAnd: - if err := v.firstThunkError(spec.childA); err != nil { - return err - } - return v.firstThunkError(spec.childB) - case specKindNow, specKindNext, specKindEventually, specKindNot, specKindAlways: - return v.firstThunkError(spec.childA) - } - return nil -} - func (v *Verifier) resolveGenerator(generator goja.Value) (Action, error) { object := generator.ToObject(v.runtime) if object == nil {