From b9fa41553fa78dbc3bc6b65f541dbbf4523adb21 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 30 May 2026 16:30:37 +0530 Subject: [PATCH] feat(verifier): track newly-violated property set per step Sticky `always(P)` violations re-surfaced on every step after onset, flooding traces and summaries with duplicate records. EvaluateProperties now diffs against the prior verdict map and records the onset set; a new NewlyViolatedProperties accessor exposes it so callers can emit each violation exactly once at its onset step. The verdict-map return is preserved for residual / current-verdict consumers. --- internal/verifier/verifier_test.go | 111 +++++++++++++++++++++++++++++ internal/verifier/worker.go | 47 ++++++++++-- 2 files changed, 154 insertions(+), 4 deletions(-) diff --git a/internal/verifier/verifier_test.go b/internal/verifier/verifier_test.go index 32f8ffa..681cc60 100644 --- a/internal/verifier/verifier_test.go +++ b/internal/verifier/verifier_test.go @@ -119,6 +119,117 @@ func TestEvaluateProperties_HoldsThenViolates(t *testing.T) { } } +func TestNewlyViolatedProperties_OnsetOnly(t *testing.T) { + verifier := newVerifier(t) + mustLoad(t, verifier, helloSpec) + + // Balance trajectory: holds, holds, violates, stays violated, stays violated. + // Onset must appear only on step 3 even though the residual stays false + // through steps 4 and 5 (LTL `always` sticky semantics). + balances := []int{1500, 1500, -1, 500, 500} + for index, balance := range balances { + raw, _ := json.Marshal(balance) + if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{"ledger.balance": raw}}); err != nil { + t.Fatal(err) + } + _ = verifier.EvaluateProperties() + got := verifier.NewlyViolatedProperties() + step := index + 1 + if step == 3 { + want := []string{"balanceNonNegative"} + if !slices.Equal(got, want) { + t.Errorf("step %d (onset): got %v, want %v", step, got, want) + } + } else if len(got) != 0 { + t.Errorf("step %d: expected empty onset set, got %v", step, got) + } + } +} + +func TestNewlyViolatedProperties_FirstStepViolation(t *testing.T) { + const spec = ` +globalThis.properties = { + alwaysFalse: __sanderling__.always(() => false), +}; +` + verifier := newVerifier(t) + mustLoad(t, verifier, spec) + + for step := 1; step <= 3; step++ { + if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}}); err != nil { + t.Fatal(err) + } + _ = verifier.EvaluateProperties() + got := verifier.NewlyViolatedProperties() + if step == 1 { + want := []string{"alwaysFalse"} + if !slices.Equal(got, want) { + t.Errorf("step 1 (onset): got %v, want %v", got, want) + } + } else if len(got) != 0 { + t.Errorf("step %d: expected empty onset set after first-step violation, got %v", step, got) + } + } +} + +func TestNewlyViolatedProperties_MultipleProperties(t *testing.T) { + const spec = ` +const a = __sanderling__.extract(state => state.snapshots["a"] ?? 0); +const b = __sanderling__.extract(state => state.snapshots["b"] ?? 0); +globalThis.properties = { + propA: __sanderling__.always(() => a.current >= 0), + propB: __sanderling__.always(() => b.current >= 0), +}; +` + verifier := newVerifier(t) + mustLoad(t, verifier, spec) + + // propA violates at step 2, propB violates at step 4. Each must surface + // only on its own onset step. + aValues := []int{1, -1, -1, -1} + bValues := []int{1, 1, 1, -1} + expectOnset := map[int][]string{ + 2: {"propA"}, + 4: {"propB"}, + } + for index := range aValues { + aRaw, _ := json.Marshal(aValues[index]) + bRaw, _ := json.Marshal(bValues[index]) + if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{"a": aRaw, "b": bRaw}}); err != nil { + t.Fatal(err) + } + _ = verifier.EvaluateProperties() + got := verifier.NewlyViolatedProperties() + step := index + 1 + want := expectOnset[step] + if !slices.Equal(got, want) { + t.Errorf("step %d: got %v, want %v", step, got, want) + } + } +} + +func TestNewlyViolatedProperties_DeterministicOrder(t *testing.T) { + const spec = ` +globalThis.properties = { + zebra: __sanderling__.always(() => false), + apple: __sanderling__.always(() => false), + mango: __sanderling__.always(() => false), +}; +` + verifier := newVerifier(t) + mustLoad(t, verifier, spec) + + if err := verifier.PushSnapshot(SnapshotInput{Snapshots: Snapshots{}}); err != nil { + t.Fatal(err) + } + _ = verifier.EvaluateProperties() + got := verifier.NewlyViolatedProperties() + want := []string{"apple", "mango", "zebra"} + if !slices.Equal(got, want) { + t.Errorf("onset order: got %v, want %v (sorted lexicographically)", got, want) + } +} + func TestNextAction_FromActionsGenerator(t *testing.T) { verifier := newVerifier(t) mustLoad(t, verifier, helloSpec) diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go index 5616b72..53555c8 100644 --- a/internal/verifier/worker.go +++ b/internal/verifier/worker.go @@ -5,6 +5,7 @@ import ( "errors" "fmt" "math/rand/v2" + "sort" "strings" "time" @@ -26,6 +27,9 @@ type Verifier struct { evaluators map[string]*ltl.Evaluator + priorVerdicts map[string]ltl.Verdict + newlyViolated []string + lastTree *hierarchy.Tree lastAction *Action lastLogs []LogEntry @@ -44,10 +48,11 @@ func WithRand(rng *rand.Rand) Option { func New(options ...Option) (*Verifier, error) { verifier := &Verifier{ - runtime: goja.New(), - properties: map[string]int{}, - evaluators: map[string]*ltl.Evaluator{}, - rng: rand.New(rand.NewPCG(0, 0)), + runtime: goja.New(), + properties: map[string]int{}, + evaluators: map[string]*ltl.Evaluator{}, + priorVerdicts: map[string]ltl.Verdict{}, + rng: rand.New(rand.NewPCG(0, 0)), } for _, option := range options { option(verifier) @@ -288,6 +293,9 @@ type SnapshotInput struct { // after the most recent PushSnapshot. The step time passed in PushSnapshot is // forwarded to each evaluator so deadline-bound operators see the snapshot's // wall clock rather than time.Now(). +// +// As a side effect, the set of properties that newly transitioned to violated +// on this call is recorded; see NewlyViolatedProperties. func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict { verdicts := map[string]ltl.Verdict{} stepTime := v.stepTime @@ -298,9 +306,40 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict { 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) + } + } + sort.Strings(onset) + v.newlyViolated = onset + + next := make(map[string]ltl.Verdict, len(verdicts)) + for name, verdict := range verdicts { + next[name] = verdict + } + v.priorVerdicts = next + return verdicts } +// 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 +// transition occurred or EvaluateProperties has not been called. +// +// This is the onset set: each property name appears at most once across a +// run's traces, at the step where the violation first fired. Subsequent +// steps where the property remains violated (LTL `always` sticky semantics) +// will not list it. Use this for trace emission and summary reporting so the +// onset is the only step that surfaces the violation event; use +// EvaluateProperties for residual / current-verdict needs. +func (v *Verifier) NewlyViolatedProperties() []string { + return append([]string(nil), v.newlyViolated...) +} + // 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