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

@@ -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)

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(),
+		runtime:       goja.New(),
-		properties: map[string]int{},
+		properties:    map[string]int{},
-		evaluators: map[string]*ltl.Evaluator{},
+		evaluators:    map[string]*ltl.Evaluator{},
-		rng:        rand.New(rand.NewPCG(0, 0)),
+		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