From 9958b0ddc8361580a1e1d9186833c855e2451781 Mon Sep 17 00:00:00 2001 From: pjay Date: Fri, 5 Jun 2026 23:46:36 +0530 Subject: [PATCH] Attribute violations to the causing step and render witness evidence (#59) * feat(ltl): attribute violations to the obligation origin step * feat(verifier): label evaluator observations with the runner step index * feat(trace): carry the causing step in violation witnesses and summary * feat(replay): move the violation marker to the causing step * feat(replay-ui): render witness evidence in the violations panel * feat(replay-ui): wire witnesses and step jump into violation panels * fix(ltl): treat next obligations as vacuous at run end * fix(runner): give the finalize trace record its own step index --- internal/ltl/evaluator.go | 126 ++++++++++------ internal/ltl/finalize_test.go | 42 ++++-- internal/ltl/witness_test.go | 77 ++++++++++ internal/replay/runs_cache.go | 9 +- internal/replay/runs_decode.go | 56 ++++++- internal/replay/runs_test.go | 60 ++++++++ internal/runner/runner.go | 50 +++++-- internal/runner/runner_test.go | 180 +++++++++++++++++++++++ internal/trace/writer.go | 9 +- internal/verifier/verifier_test.go | 40 +++++ internal/verifier/worker.go | 13 +- replay-ui/src/panels/ViolationsPanel.css | 51 +++++++ replay-ui/src/panels/ViolationsPanel.tsx | 70 ++++++++- replay-ui/src/routes/RunDetail.tsx | 10 ++ replay-ui/src/types.ts | 11 ++ 15 files changed, 719 insertions(+), 85 deletions(-) diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go index 3f8fa07..e242aaf 100644 --- a/internal/ltl/evaluator.go +++ b/internal/ltl/evaluator.go @@ -33,17 +33,27 @@ func (v Verdict) String() string { // violates, the overall verdict latches to Violated. type Evaluator struct { root Formula - pending []Formula + pending []obligation violated bool steps int violation *Violation } +// obligation pairs a residual formula with the step that spawned it, so a +// deferred check (a next, a pending eventually) that fails on a later step can +// be attributed to the step that created the obligation. +type obligation struct { + formula Formula + origin int +} + // Violation is the witness for a latched verdict: the failing sub-formula, a -// human-readable reason, and the observation step it fired at. A thrown -// predicate carries the goja error text as its reason and sets IsError; a plain -// false carries "predicate false"; Finalize fills it for liveness obligations -// that never discharged. +// human-readable reason, and the step the failed obligation originated at. For +// an immediate predicate failure that is the observation step itself; for a +// deferred obligation (next, eventually) it is the earlier step that spawned +// it, the one that caused the violation. A thrown predicate carries the goja +// error text as its reason and sets IsError; a plain false carries "predicate +// false"; Finalize fills it for liveness obligations that never discharged. type Violation struct { Formula Formula Reason string @@ -62,19 +72,29 @@ func (e *Evaluator) Observe() Verdict { return e.ObserveAt(time.Now()) } -// ObserveAt is like Observe but takes the current step time explicitly. +// ObserveAt is like Observe but takes the current step time explicitly. Steps +// are numbered by an internal counter starting at 1; callers whose step +// numbering can skip observations should use ObserveAtStep instead. func (e *Evaluator) ObserveAt(now time.Time) Verdict { + return e.ObserveAtStep(now, e.steps+1) +} + +// ObserveAtStep is like ObserveAt but labels the observation with the caller's +// step index, so violation witnesses carry the caller's numbering even when +// some steps were never observed (for example transitional steps the verifier +// skips). +func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict { if e.violated { return VerdictViolated } - e.steps++ + e.steps = step - fresh := rootObligation(e.root) + fresh := obligation{formula: rootObligation(e.root), origin: step} obligations := append(e.pending, fresh) e.pending = e.pending[:0] - for _, obligation := range obligations { - result := reduce(obligation, now) + for _, entry := range obligations { + result := reduce(entry.formula, now) switch result.status { case statusHolds: // drop @@ -83,11 +103,11 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict { e.pending = nil e.violation = result.witness if e.violation != nil { - e.violation.Step = e.steps + e.violation.Step = entry.origin } return VerdictViolated case statusPending: - e.pending = append(e.pending, result.formula) + e.pending = append(e.pending, obligation{formula: result.formula, origin: entry.origin}) } } @@ -100,41 +120,43 @@ func (e *Evaluator) ObserveAt(now time.Time) Verdict { } // collapse removes structurally-identical obligations, keeping the first -// occurrence in order. Distinct predicates never merge because ThunkFormula's -// name participates in its describe() key, so deduping cannot hide a violation. -func collapse(obligations []Formula) []Formula { +// occurrence in order so the surviving entry carries the earliest origin step. +// Distinct predicates never merge because ThunkFormula's name participates in +// its describe() key, so deduping cannot hide a violation. +func collapse(obligations []obligation) []obligation { if len(obligations) < 2 { return obligations } seen := make(map[string]struct{}, len(obligations)) result := obligations[:0] - for _, obligation := range obligations { - key := obligation.describe() + for _, entry := range obligations { + key := entry.formula.describe() if _, ok := seen[key]; ok { continue } seen[key] = struct{}{} - result = append(result, obligation) + result = append(result, entry) } return result } -// Finalize reports the terminal verdict for the run. Pending obligations that -// can never be discharged by a future step (an unbounded eventually that never -// fired, a strong next with no successor) resolve to Violated; safety -// obligations that were never breached resolve to Holds. +// Finalize reports the terminal verdict for the run. A liveness promise that +// never discharged (an eventually that never fired) resolves to Violated. A +// deferred state check (the residue of a next) has no successor state to +// evaluate against, so it is indefinite and resolves vacuously to Holds: the +// run ended before the obligation could be checked, which is not a failure. func (e *Evaluator) Finalize() Verdict { if e.violated { return VerdictViolated } - for _, obligation := range e.pending { - if finalize(obligation) == statusViolated { + for _, entry := range e.pending { + if finalize(entry.formula) == statusViolated { e.violated = true e.pending = nil e.violation = &Violation{ - Formula: obligation, - Reason: finalizeReason(obligation), - Step: e.steps, + Formula: entry.formula, + Reason: finalizeReason(entry.formula), + Step: entry.origin, } return VerdictViolated } @@ -156,17 +178,18 @@ func finalizeReason(formula Formula) string { switch formula.(type) { case EventuallyFormula: return "eventually never satisfied" - case NextFormula: - return "next obligation unmet at run end" - case ThunkFormula: - return "obligation unmet at run end" default: return "liveness obligation unmet at run end" } } // finalize collapses a pending obligation to its terminal status assuming no -// further steps will occur. +// further steps will occur. Three-valued: a pending thunk or next is the +// residue of a deferred state check with no state left to check, so it is +// indefinite (statusPending) rather than violated; only a liveness promise +// (an eventually that never fired) is a definite end-of-run violation. +// Connectives combine with Kleene semantics so an indefinite sub-formula +// never manufactures a definite verdict. func finalize(formula Formula) residualStatus { switch concrete := formula.(type) { case PureFormula: @@ -175,11 +198,11 @@ func finalize(formula Formula) residualStatus { } return statusViolated case ThunkFormula: - return statusViolated + return statusPending case EventuallyFormula: return statusViolated case NextFormula: - return statusViolated + return statusPending case AlwaysFormula: return statusHolds case NowFormula: @@ -188,24 +211,34 @@ func finalize(formula Formula) residualStatus { switch finalize(concrete.Inner) { case statusViolated: return statusHolds - default: + case statusHolds: return statusViolated + default: + return statusPending } case AndFormula: - if finalize(concrete.Left) == statusViolated || finalize(concrete.Right) == statusViolated { + left, right := finalize(concrete.Left), finalize(concrete.Right) + if left == statusViolated || right == statusViolated { return statusViolated } + if left == statusPending || right == statusPending { + return statusPending + } return statusHolds case OrFormula: - if finalize(concrete.Left) == statusHolds || finalize(concrete.Right) == statusHolds { + left, right := finalize(concrete.Left), finalize(concrete.Right) + if left == statusHolds || right == statusHolds { return statusHolds } + if left == statusPending || right == statusPending { + return statusPending + } return statusViolated case ImpliesFormula: - if finalize(concrete.Antecedent) == statusViolated { - return statusHolds - } - return finalize(concrete.Consequent) + return finalize(OrFormula{ + Left: NotFormula{Inner: concrete.Antecedent}, + Right: concrete.Consequent, + }) default: return statusHolds } @@ -224,9 +257,9 @@ func (e *Evaluator) Residual() Formula { if len(e.pending) == 0 { return PureFormula{Value: true} } - combined := e.pending[0] - for _, formula := range e.pending[1:] { - combined = AndFormula{Left: combined, Right: formula} + combined := e.pending[0].formula + for _, entry := range e.pending[1:] { + combined = AndFormula{Left: combined, Right: entry.formula} } return combined } @@ -258,11 +291,6 @@ type reduceResult struct { func holds() reduceResult { return reduceResult{status: statusHolds} } -// violated reports a violation without an attached witness. Used where the -// failing sub-formula is recovered from a child result whose own witness is -// carried up by violatedFrom. -func violated() reduceResult { return reduceResult{status: statusViolated} } - // violatedWith reports a violation that originates at the given sub-formula // with the given reason. The reason distinguishes a thrown predicate from a // plain false so callers (and the replay UI) can render the cause. diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go index d16a6b5..11dd577 100644 --- a/internal/ltl/finalize_test.go +++ b/internal/ltl/finalize_test.go @@ -18,13 +18,32 @@ func TestFinalize_UnboundedEventuallyUnmetIsViolated(t *testing.T) { } } -func TestFinalize_FinalStepNextIsViolated(t *testing.T) { +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 != VerdictViolated { - t.Errorf("Finalize = %v, want violated", 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) } } @@ -128,20 +147,23 @@ func TestViolationLatchIsMonotonic(t *testing.T) { } func TestCollapse_IdenticalObligationsMerge(t *testing.T) { - merged := collapse([]Formula{ - Next(Pure(true)), - Next(Pure(true)), - Next(Pure(true)), + 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([]Formula{ - Eventually(ThunkNamed("p3", func() (bool, error) { return false, nil })), - Eventually(ThunkNamed("p4", func() (bool, error) { return false, nil })), + 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)) diff --git a/internal/ltl/witness_test.go b/internal/ltl/witness_test.go index 6e4c580..ec253c5 100644 --- a/internal/ltl/witness_test.go +++ b/internal/ltl/witness_test.go @@ -71,6 +71,83 @@ func TestViolation_FinalizeFillsWitness(t *testing.T) { } } +func TestViolation_NextAttributesOriginStep(t *testing.T) { + // always(next(p)): the obligation spawned at step 2 is checked against + // step 3's state; the violation belongs to step 2, the step that caused it. + values := []bool{true, false} + step := 0 + evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { + current := values[step] + step++ + return current, nil + })))) + if got := evaluator.ObserveAt(time.Unix(0, 0)); got != VerdictPending { + t.Fatalf("step 1: got %v, want pending", got) + } + if got := evaluator.ObserveAt(time.Unix(1, 0)); got != VerdictPending { + t.Fatalf("step 2: got %v, want pending", got) + } + if got := evaluator.ObserveAt(time.Unix(2, 0)); got != VerdictViolated { + t.Fatalf("step 3: got %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil, want non-nil") + } + if witness.Step != 2 { + t.Errorf("Step = %d, want 2 (the step that spawned the next obligation)", witness.Step) + } +} + +func TestViolation_FinalizeAttributesOriginStep(t *testing.T) { + // An eventually that never fires is reported by Finalize at the step the + // obligation was first spawned (collapse keeps the earliest origin). + evaluator := NewEvaluator(Eventually(ThunkNamed("p", func() (bool, error) { + return false, nil + }))) + evaluator.ObserveAt(time.Unix(0, 0)) + evaluator.ObserveAt(time.Unix(1, 0)) + evaluator.ObserveAt(time.Unix(2, 0)) + if got := evaluator.Finalize(); got != VerdictViolated { + t.Fatalf("Finalize = %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil after Finalize, want non-nil") + } + if witness.Step != 1 { + t.Errorf("Step = %d, want 1 (the step the eventually obligation was spawned)", witness.Step) + } +} + +func TestViolation_ObserveAtStepUsesCallerNumbering(t *testing.T) { + // The caller skips step 5 (a transitional step the verifier never saw); the + // origin must carry the caller's labels, not a contiguous internal count. + values := []bool{true, false} + step := 0 + evaluator := NewEvaluator(Always(Next(ThunkNamed("p", func() (bool, error) { + current := values[step] + step++ + return current, nil + })))) + if got := evaluator.ObserveAtStep(time.Unix(0, 0), 3); got != VerdictPending { + t.Fatalf("step 3: got %v, want pending", got) + } + if got := evaluator.ObserveAtStep(time.Unix(1, 0), 4); got != VerdictPending { + t.Fatalf("step 4: got %v, want pending", got) + } + if got := evaluator.ObserveAtStep(time.Unix(2, 0), 6); got != VerdictViolated { + t.Fatalf("step 6: got %v, want violated", got) + } + witness := evaluator.Violation() + if witness == nil { + t.Fatal("Violation = nil, want non-nil") + } + if witness.Step != 4 { + t.Errorf("Step = %d, want 4 (caller-labeled origin, not detection step 6)", witness.Step) + } +} + func TestViolation_NilBeforeViolation(t *testing.T) { evaluator := NewEvaluator(Always(Pure(true))) evaluator.Observe() diff --git a/internal/replay/runs_cache.go b/internal/replay/runs_cache.go index 3cc87a5..0adf27a 100644 --- a/internal/replay/runs_cache.go +++ b/internal/replay/runs_cache.go @@ -91,7 +91,7 @@ func scanSteps(tracePath string) ([]StepSummary, []int64, int, time.Time, error) reader := bufio.NewReaderSize(file, 64*1024) steps := []StepSummary{} offsets := []int64{} - violationCount := 0 + attributions := []violationAttribution{} var offset int64 for { lineStart := offset @@ -102,19 +102,20 @@ func scanSteps(tracePath string) ([]StepSummary, []int64, int, time.Time, error) trimmed = trimmed[:len(trimmed)-1] } if len(trimmed) > 0 { - summary, partial, decodeErr := decodeStepSummary(trimmed) + summary, lineAttributions, decodeErr := decodeStepSummary(trimmed) if decodeErr != nil { return nil, nil, 0, time.Time{}, decodeErr } steps = append(steps, summary) offsets = append(offsets, lineStart) - violationCount += partial + attributions = append(attributions, lineAttributions...) } if err != nil { break } } - return steps, offsets, violationCount, info.ModTime(), nil + markViolations(steps, attributions) + return steps, offsets, len(attributions), info.ModTime(), nil } // Step decodes the full Step record at index n (1-based, matching trace.Step.Index). diff --git a/internal/replay/runs_decode.go b/internal/replay/runs_decode.go index 553cffb..5f5185f 100644 --- a/internal/replay/runs_decode.go +++ b/internal/replay/runs_decode.go @@ -56,7 +56,16 @@ func tallyTrace(tracePath string) (steps, violations int, err error) { return steps, violations, nil } -func decodeStepSummary(line []byte) (StepSummary, int, error) { +// violationAttribution maps one recorded violation to the step the marker +// belongs on: the causing step its witness names, falling back to the step +// whose trace line carries it (the detection step) for witnesses written +// before the step field existed. +type violationAttribution struct { + attributedStep int + detectedStep int +} + +func decodeStepSummary(line []byte) (StepSummary, []violationAttribution, error) { var partial struct { Index int `json:"step"` Timestamp time.Time `json:"timestamp"` @@ -76,15 +85,28 @@ func decodeStepSummary(line []byte) (StepSummary, int, error) { } `json:"next_action,omitempty"` Exceptions []json.RawMessage `json:"exceptions,omitempty"` Violations []string `json:"violations,omitempty"` + Witnesses map[string]struct { + Step int `json:"step"` + } `json:"witnesses,omitempty"` } if err := json.Unmarshal(line, &partial); err != nil { - return StepSummary{}, 0, fmt.Errorf("decode step: %w", err) + return StepSummary{}, nil, fmt.Errorf("decode step: %w", err) + } + var attributions []violationAttribution + for _, name := range partial.Violations { + attribution := violationAttribution{ + attributedStep: partial.Index, + detectedStep: partial.Index, + } + if witness, ok := partial.Witnesses[name]; ok && witness.Step > 0 { + attribution.attributedStep = witness.Step + } + attributions = append(attributions, attribution) } summary := StepSummary{ Index: partial.Index, Timestamp: partial.Timestamp, Screen: partial.Screen, - HasViolations: len(partial.Violations) > 0, HasExceptions: len(partial.Exceptions) > 0, } if partial.NextAction != nil { @@ -113,7 +135,33 @@ func decodeStepSummary(line []byte) (StepSummary, int, error) { } } } - return summary, len(partial.Violations), nil + return summary, attributions, nil +} + +// markViolations sets HasViolations on the step each attribution points at. +// The marker goes on the causing step; when that index is missing from the +// trace the detection step keeps it. Duplicate indices (a finalize line echoes +// the last step's index) resolve to the first occurrence, the real step. +func markViolations(steps []StepSummary, attributions []violationAttribution) { + if len(attributions) == 0 { + return + } + positionOf := make(map[int]int, len(steps)) + for position, step := range steps { + if _, ok := positionOf[step.Index]; !ok { + positionOf[step.Index] = position + } + } + for _, attribution := range attributions { + position, ok := positionOf[attribution.attributedStep] + if !ok { + position, ok = positionOf[attribution.detectedStep] + if !ok { + continue + } + } + steps[position].HasViolations = true + } } func swipeDirectionLabel(fromX, fromY, toX, toY int) string { diff --git a/internal/replay/runs_test.go b/internal/replay/runs_test.go index c0ce1aa..2d3b39a 100644 --- a/internal/replay/runs_test.go +++ b/internal/replay/runs_test.go @@ -138,6 +138,66 @@ func TestCacheStep_LazyDecodeReturnsFullStep(t *testing.T) { } } +func TestCacheOpen_ViolationMarkerMovesToCausingStep(t *testing.T) { + // The violation is detected at step 3 but its witness attributes it to + // step 2 (the step that spawned the next obligation). The action-list + // marker belongs on step 2; the full step 3 payload keeps the violation + // record itself. + root := t.TempDir() + startedAt := time.Now().UTC() + steps := []trace.Step{ + {Index: 1, Timestamp: startedAt}, + {Index: 2, Timestamp: startedAt.Add(time.Second)}, + { + Index: 3, + Timestamp: startedAt.Add(2 * time.Second), + Violations: []string{"prop1"}, + Witnesses: map[string]trace.Witness{"prop1": {Reason: "predicate false", Step: 2}}, + }, + } + writeRun(t, root, "r1", trace.Meta{StartedAt: startedAt, EndedAt: timePointer(startedAt.Add(3 * time.Second))}, steps) + + cache := NewCache(root) + run, err := cache.Open("r1") + if err != nil { + t.Fatalf("Open: %v", err) + } + if !run.Steps[1].HasViolations { + t.Error("step 2 (causing step) should carry the violation marker") + } + if run.Steps[2].HasViolations { + t.Error("step 3 (detection step) should not carry the marker") + } + full, err := cache.Step(run, 3) + if err != nil { + t.Fatalf("Step(3): %v", err) + } + if len(full.Violations) != 1 || full.Violations[0] != "prop1" { + t.Errorf("step 3 payload violations = %v, want [prop1]", full.Violations) + } +} + +func TestCacheOpen_ViolationWithoutWitnessStepKeepsDetectionStep(t *testing.T) { + // Traces written before witnesses carried a step field fall back to + // marking the detection step, the old behavior. + root := t.TempDir() + startedAt := time.Now().UTC() + steps := []trace.Step{ + {Index: 1, Timestamp: startedAt}, + {Index: 2, Timestamp: startedAt.Add(time.Second), Violations: []string{"prop1"}}, + } + writeRun(t, root, "r1", trace.Meta{StartedAt: startedAt, EndedAt: timePointer(startedAt.Add(2 * time.Second))}, steps) + + cache := NewCache(root) + run, err := cache.Open("r1") + if err != nil { + t.Fatalf("Open: %v", err) + } + if !run.Steps[1].HasViolations { + t.Error("step 2 should keep the marker when the witness has no step") + } +} + func TestDecodeStepSummary_ActionLabelPerKind(t *testing.T) { cases := []struct { line string diff --git a/internal/runner/runner.go b/internal/runner/runner.go index af070bf..a2d8237 100644 --- a/internal/runner/runner.go +++ b/internal/runner/runner.go @@ -8,6 +8,8 @@ import ( "fmt" "io" "log/slog" + "maps" + "slices" "strings" "time" @@ -185,6 +187,7 @@ func Run(ctx context.Context, options Options) (Summary, error) { Tree: tree, LastAction: lastAction, StepTime: stepStart, + StepIndex: stepIndex, RunStart: summary.StartTime, Logs: logs, }); err != nil { @@ -263,10 +266,7 @@ func Run(ctx context.Context, options Options) (Summary, error) { } summary.Steps = stepIndex if len(violations) > 0 { - summary.Violations = append(summary.Violations, ViolationRecord{ - StepIndex: stepIndex, - Properties: violations, - }) + summary.Violations = append(summary.Violations, violationRecords(violations, witnesses, stepIndex)...) } // Wait actions are themselves a settling: skip the idle poll. Actions // that mutate the UI fall through to WaitForIdle so the next step's @@ -284,17 +284,17 @@ func Run(ctx context.Context, options Options) (Summary, error) { } // Finalize each evaluator once the loop ends so liveness obligations that - // never discharged (an unbounded eventually that never fired, a strong - // next with no successor) are reported as violations rather than silently - // left pending. Properties already violated mid-run are not re-reported. + // never discharged (an eventually that never fired) are reported as + // violations rather than silently left pending. Properties already + // violated mid-run are not re-reported. The synthetic record gets its own + // step index so no two trace lines share one; witnesses still attribute + // the violation to the step that spawned the obligation. if ended := options.Verifier.Finalize(); len(ended) > 0 { - witnesses := collectWitnesses(options.Verifier, ended, logger, stepIndex) - summary.Violations = append(summary.Violations, ViolationRecord{ - StepIndex: stepIndex, - Properties: ended, - }) + finalIndex := stepIndex + 1 + witnesses := collectWitnesses(options.Verifier, ended, logger, finalIndex) + summary.Violations = append(summary.Violations, violationRecords(ended, witnesses, finalIndex)...) finalStep := trace.Step{ - Index: stepIndex, + Index: finalIndex, Timestamp: time.Now(), Violations: ended, Witnesses: witnesses, @@ -806,6 +806,26 @@ func captureMetrics(ctx context.Context, options Options, logger *slog.Logger, s } } +// violationRecords groups newly-violated properties by the step their witness +// attributes the violation to (the causing step), falling back to the +// detection step for properties without a witness. Records are ordered by +// step; properties keep the sorted order NewlyViolatedProperties produced. +func violationRecords(properties []string, witnesses map[string]trace.Witness, detectionStep int) []ViolationRecord { + byStep := map[int][]string{} + for _, name := range properties { + step := detectionStep + if witness, ok := witnesses[name]; ok && witness.Step > 0 { + step = witness.Step + } + byStep[step] = append(byStep[step], name) + } + records := make([]ViolationRecord, 0, len(byStep)) + for _, step := range slices.Sorted(maps.Keys(byStep)) { + records = append(records, ViolationRecord{StepIndex: step, Properties: byStep[step]}) + } + return records +} + // collectWitnesses gathers the violation witness for each newly-violated // property, logs its cause, and returns them keyed by property name for the // trace. Properties without a captured witness are skipped. @@ -820,10 +840,12 @@ func collectWitnesses(verifierInstance *verifier.Verifier, properties []string, continue } logger.Warn("property violated", - "step", stepIndex, "property", name, "reason", witness.Reason, "error", witness.IsError) + "step", witness.Step, "detected_step", stepIndex, + "property", name, "reason", witness.Reason, "error", witness.IsError) witnesses[name] = trace.Witness{ Reason: witness.Reason, IsError: witness.IsError, + Step: witness.Step, Extractors: witness.Extractors, } } diff --git a/internal/runner/runner_test.go b/internal/runner/runner_test.go index 1fe2394..1ee7eb6 100644 --- a/internal/runner/runner_test.go +++ b/internal/runner/runner_test.go @@ -253,6 +253,186 @@ func TestRunner_ViolationSurfacesOnlyOnOnsetStep(t *testing.T) { } } +func TestRunner_NextViolationAttributedToCausingStep(t *testing.T) { + // always(next(p)): the obligation spawned at step 2 fails against step 3's + // state. The summary record and the trace witness must attribute the + // violation to step 2 (the causing step); the trace line that carries it is + // still step 3, where the failure was detected. + const nextViolationSpec = ` +import { actions, always, next, extract } from "@sanderling/spec"; +let observed = 0; +const tick = extract(() => ++observed); +globalThis.properties = { + nextHolds: always(next(() => tick.current < 3)), +}; +globalThis.actions = actions(() => []); +` + state := newHarnessWithSpec(t, nextViolationSpec) + + ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second) + defer cancel() + summary, err := Run(ctx, Options{ + Duration: time.Hour, + IdleTimeout: 20 * time.Millisecond, + MaxSteps: 5, + Driver: state.mock, + Verifier: state.verifier, + TraceWriter: state.writer, + }) + if err != nil { + t.Fatalf("Run: %v", err) + } + if len(summary.Violations) != 1 { + t.Fatalf("expected exactly one ViolationRecord, got %d: %v", + len(summary.Violations), summary.Violations) + } + if summary.Violations[0].StepIndex != 2 { + t.Errorf("summary step: got %d, want 2 (the step that spawned the next obligation)", + summary.Violations[0].StepIndex) + } + if !slices.Equal(summary.Violations[0].Properties, []string{"nextHolds"}) { + t.Errorf("properties: got %v, want [nextHolds]", summary.Violations[0].Properties) + } + + file, err := os.Open(filepath.Join(state.writer.Directory(), "trace.jsonl")) + if err != nil { + t.Fatal(err) + } + defer file.Close() + + type traceLine struct { + Step int `json:"step"` + Violations []string `json:"violations"` + Witnesses map[string]trace.Witness `json:"witnesses"` + } + found := false + scanner := bufio.NewScanner(file) + scanner.Buffer(make([]byte, 0, 64*1024), 8*1024*1024) + for scanner.Scan() { + var line traceLine + if err := json.Unmarshal(scanner.Bytes(), &line); err != nil { + t.Fatalf("trace line decode: %v", err) + } + if len(line.Violations) == 0 { + continue + } + found = true + if line.Step != 3 { + t.Errorf("violation detected on step %d, want 3", line.Step) + } + witness, ok := line.Witnesses["nextHolds"] + if !ok { + t.Fatalf("step %d carries no witness for nextHolds", line.Step) + } + if witness.Step != 2 { + t.Errorf("witness step: got %d, want 2 (causing step)", witness.Step) + } + } + if err := scanner.Err(); err != nil { + t.Fatalf("scan trace: %v", err) + } + if !found { + t.Error("no trace line carried the violation") + } +} + +func TestRunner_AlwaysNextLeavesNoEndOfRunViolation(t *testing.T) { + // always(next(p)) ends every run with a pending deferred check. That + // residue is vacuous (no successor state to check), so neither the + // summary nor the trace may report an end-of-run violation. + const spec = ` +import { actions, always, next } from "@sanderling/spec"; +globalThis.properties = { + nextHolds: always(next(() => true)), +}; +globalThis.actions = actions(() => []); +` + state := newHarnessWithSpec(t, spec) + + ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second) + defer cancel() + summary, err := Run(ctx, Options{ + Duration: time.Hour, + IdleTimeout: 20 * time.Millisecond, + MaxSteps: 3, + Driver: state.mock, + Verifier: state.verifier, + TraceWriter: state.writer, + }) + if err != nil { + t.Fatalf("Run: %v", err) + } + if len(summary.Violations) != 0 { + t.Errorf("expected no violations, got %v", summary.Violations) + } +} + +func TestRunner_FinalizeRecordUsesDistinctStepIndex(t *testing.T) { + // An eventually that never fires is reported at run end through a + // synthetic trace record. That record must carry its own step index so no + // two trace lines share one (duplicate indices made the replay UI select + // two rows at once). + const spec = ` +import { actions, eventually } from "@sanderling/spec"; +globalThis.properties = { + neverFires: eventually(() => false), +}; +globalThis.actions = actions(() => []); +` + state := newHarnessWithSpec(t, spec) + + ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second) + defer cancel() + summary, err := Run(ctx, Options{ + Duration: time.Hour, + IdleTimeout: 20 * time.Millisecond, + MaxSteps: 3, + Driver: state.mock, + Verifier: state.verifier, + TraceWriter: state.writer, + }) + if err != nil { + t.Fatalf("Run: %v", err) + } + if !containsProperty(summary.Violations, "neverFires") { + t.Fatalf("expected neverFires in violations: %v", summary.Violations) + } + + file, err := os.Open(filepath.Join(state.writer.Directory(), "trace.jsonl")) + if err != nil { + t.Fatal(err) + } + defer file.Close() + + type traceLine struct { + Step int `json:"step"` + Violations []string `json:"violations"` + } + seen := map[int]bool{} + finalizeStep := 0 + scanner := bufio.NewScanner(file) + scanner.Buffer(make([]byte, 0, 64*1024), 8*1024*1024) + for scanner.Scan() { + var line traceLine + if err := json.Unmarshal(scanner.Bytes(), &line); err != nil { + t.Fatalf("trace line decode: %v", err) + } + if seen[line.Step] { + t.Errorf("duplicate step index %d in trace", line.Step) + } + seen[line.Step] = true + if slices.Contains(line.Violations, "neverFires") { + finalizeStep = line.Step + } + } + if err := scanner.Err(); err != nil { + t.Fatalf("scan trace: %v", err) + } + if finalizeStep != summary.Steps+1 { + t.Errorf("finalize record step = %d, want %d (steps+1)", finalizeStep, summary.Steps+1) + } +} + func TestRunner_ThrowingPredicateIsLoggedNotPanic(t *testing.T) { const throwingSpec = ` import { actions, always, Tap } from "@sanderling/spec"; diff --git a/internal/trace/writer.go b/internal/trace/writer.go index 384a446..7e29a53 100644 --- a/internal/trace/writer.go +++ b/internal/trace/writer.go @@ -43,8 +43,13 @@ type Step struct { // Witness is the trace-side record of a property violation: why it fired and a // snapshot of every extractor's value at the violating step. type Witness struct { - Reason string `json:"reason,omitempty"` - IsError bool `json:"is_error,omitempty"` + Reason string `json:"reason,omitempty"` + IsError bool `json:"is_error,omitempty"` + // Step is the step the failed obligation originated at: the step that + // caused the violation. For a deferred obligation (a next, an eventually) + // this is earlier than the step whose record carries the witness, which is + // where the failure was detected. + Step int `json:"step,omitempty"` Extractors map[string]json.RawMessage `json:"extractors,omitempty"` } diff --git a/internal/verifier/verifier_test.go b/internal/verifier/verifier_test.go index 2923ea0..8defe5a 100644 --- a/internal/verifier/verifier_test.go +++ b/internal/verifier/verifier_test.go @@ -782,6 +782,46 @@ globalThis.properties = { } } +// A next obligation spawned at step k and checked against step k+1's state is +// attributed to step k, the step that caused it. StepIndex from SnapshotInput +// labels the evaluator observations so the witness carries runner step numbers. +func TestEvaluateProperties_NextViolationCarriesOriginStepIndex(t *testing.T) { + const spec = ` +globalThis.flag = __sanderling__.extract(state => state.snapshots["flag"] ?? false, "flag"); +globalThis.properties = { + flagStaysTrue: __sanderling__.always(__sanderling__.next(() => flag.current === true)), +}; +` + verifier := newVerifier(t) + mustLoad(t, verifier, spec) + + push := func(stepIndex int, flag string) map[string]ltl.Verdict { + t.Helper() + if err := verifier.PushSnapshot(SnapshotInput{ + Snapshots: Snapshots{"flag": json.RawMessage(flag)}, + StepIndex: stepIndex, + }); err != nil { + t.Fatal(err) + } + return verifier.EvaluateProperties() + } + + push(7, `true`) + push(8, `true`) + verdicts := push(9, `false`) + if got := verdicts["flagStaysTrue"]; got != ltl.VerdictViolated { + t.Fatalf("step 9: verdict = %v, want violated", got) + } + + witness := verifier.Witness("flagStaysTrue") + if witness == nil { + t.Fatal("Witness = nil, want non-nil") + } + if witness.Step != 8 { + t.Errorf("Witness.Step = %d, want 8 (the step that spawned the next obligation)", witness.Step) + } +} + func TestLoad_AcceptsSpecWithoutPropertiesOrActions(t *testing.T) { verifier := newVerifier(t) if err := verifier.Load(`const noop = 1;`); err != nil { diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go index 24bfebd..29fd8d9 100644 --- a/internal/verifier/worker.go +++ b/internal/verifier/worker.go @@ -39,6 +39,7 @@ type Verifier struct { lastLogs []LogEntry lastExceptions []Exception stepTime time.Time + stepIndex int runStart time.Time appPackage string @@ -259,6 +260,7 @@ func (v *Verifier) PushSnapshot(input SnapshotInput) error { v.lastLogs = input.Logs v.lastExceptions = input.Exceptions v.stepTime = input.StepTime + v.stepIndex = input.StepIndex if v.runStart.IsZero() { v.runStart = input.RunStart } @@ -385,6 +387,11 @@ type SnapshotInput struct { Tree *hierarchy.Tree LastAction *Action StepTime time.Time + // StepIndex is the runner's step number for this snapshot. Evaluators label + // observations with it so violation witnesses carry runner step numbers even + // when transitional steps were skipped. Zero means unlabeled; evaluators + // then fall back to their internal counter. + StepIndex int RunStart time.Time Logs []LogEntry Exceptions []Exception @@ -404,7 +411,11 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict { stepTime = time.Now() } for name, evaluator := range v.evaluators { - verdicts[name] = evaluator.ObserveAt(stepTime) + if v.stepIndex > 0 { + verdicts[name] = evaluator.ObserveAtStep(stepTime, v.stepIndex) + } else { + verdicts[name] = evaluator.ObserveAt(stepTime) + } } var onset []string diff --git a/replay-ui/src/panels/ViolationsPanel.css b/replay-ui/src/panels/ViolationsPanel.css index 0b3c731..3ab7935 100644 --- a/replay-ui/src/panels/ViolationsPanel.css +++ b/replay-ui/src/panels/ViolationsPanel.css @@ -97,6 +97,57 @@ font-size: 13px; } +.violations-panel-witness { + margin-top: 6px; + display: flex; + flex-direction: column; + gap: 4px; + font-size: 12px; +} + +.violations-panel-witness-line { + display: flex; + align-items: baseline; + gap: 8px; + margin: 0; +} + +.violations-panel-witness-key { + flex-shrink: 0; + min-width: 96px; + color: var(--text-muted); + font-size: 11px; + text-transform: lowercase; +} + +.violations-panel-witness-value { + word-break: break-all; + white-space: pre-wrap; + margin: 0; +} + +.violations-panel-witness-step { + font-family: var(--font-mono); + font-size: 11px; + padding: 1px 6px; + background: var(--surface); + color: var(--text-primary); + border: 1px solid var(--border); + border-radius: 3px; + cursor: pointer; +} + +.violations-panel-witness-step:hover { + border-color: var(--border-strong); +} + +.violations-panel-witness-evidence { + display: flex; + flex-direction: column; + gap: 3px; + margin: 0; +} + .violations-panel-residual { margin-top: 6px; font-size: 12px; diff --git a/replay-ui/src/panels/ViolationsPanel.tsx b/replay-ui/src/panels/ViolationsPanel.tsx index b2d457c..8266ffc 100644 --- a/replay-ui/src/panels/ViolationsPanel.tsx +++ b/replay-ui/src/panels/ViolationsPanel.tsx @@ -1,5 +1,5 @@ import { useMemo } from "react"; -import type { ResidualNode } from "../types"; +import type { ResidualNode, Witness } from "../types"; import ResidualNodeView from "../components/ResidualNode"; import "./ViolationsPanel.css"; @@ -7,8 +7,10 @@ export interface ViolationsPanelProps { propertyNames: string[]; violations: string[]; residuals?: Record; + witnesses?: Record; onJumpToFirstViolation: () => void; hasFirstViolation: boolean; + onJumpToStep?: (step: number) => void; /** When true, only render violated rows and hide the header button row. */ violationsOnly?: boolean; } @@ -36,12 +38,74 @@ function statusFor( return "pending"; } +function formatValue(value: unknown): string { + const encoded = JSON.stringify(value); + return encoded === undefined ? String(value) : encoded; +} + +function WitnessView({ + witness, + onJumpToStep, + open, +}: { + witness: Witness; + onJumpToStep?: (step: number) => void; + open: boolean; +}) { + const evidence = Object.entries(witness.extractors ?? {}) + .filter(([, value]) => value !== null && value !== undefined) + .sort(([a], [b]) => a.localeCompare(b)); + return ( +
+ {witness.reason ? ( +
+ + {witness.is_error ? "error" : "reason"} + + {witness.reason} +
+ ) : null} + {witness.step ? ( +
+ caused at + {onJumpToStep ? ( + + ) : ( + step {witness.step} + )} +
+ ) : null} + {evidence.length > 0 ? ( +
+ witness +
+ {evidence.map(([name, value]) => ( +
+
{name}
+
{formatValue(value)}
+
+ ))} +
+
+ ) : null} +
+ ); +} + export default function ViolationsPanel({ propertyNames, violations, residuals, + witnesses, onJumpToFirstViolation, hasFirstViolation, + onJumpToStep, violationsOnly = false, }: ViolationsPanelProps) { const violationSet = useMemo(() => new Set(violations), [violations]); @@ -84,6 +148,7 @@ export default function ViolationsPanel({
    {rows.map(({ name, status }) => { const residual = residuals?.[name]; + const witness = status === "violated" ? witnesses?.[name] : undefined; return (
  • @@ -96,6 +161,9 @@ export default function ViolationsPanel({ {name}
    + {witness ? ( + + ) : null} {residual ? (
    residual diff --git a/replay-ui/src/routes/RunDetail.tsx b/replay-ui/src/routes/RunDetail.tsx index 8063816..eab5ca9 100644 --- a/replay-ui/src/routes/RunDetail.tsx +++ b/replay-ui/src/routes/RunDetail.tsx @@ -126,6 +126,8 @@ export default function RunDetail() { const violationsAfter = nextStep?.violations ?? violationsBefore; const residualsBefore = currentStep?.residuals; const residualsAfter = nextStep?.residuals ?? residualsBefore; + const witnessesBefore = currentStep?.witnesses; + const witnessesAfter = nextStep?.witnesses ?? witnessesBefore; const exceptionsForStep = currentStep?.exceptions; const beforeTabs: TabDefinition[] = [ @@ -157,8 +159,10 @@ export default function RunDetail() { propertyNames={history?.names ?? []} violations={violationsBefore} residuals={residualsBefore} + witnesses={witnessesBefore} onJumpToFirstViolation={jumpToFirstViolation} hasFirstViolation={history?.firstViolationStep !== undefined} + onJumpToStep={goTo} /> ), }, @@ -176,8 +180,10 @@ export default function RunDetail() { propertyNames={history?.names ?? []} violations={violationsBefore} residuals={residualsBefore} + witnesses={witnessesBefore} onJumpToFirstViolation={jumpToFirstViolation} hasFirstViolation={history?.firstViolationStep !== undefined} + onJumpToStep={goTo} violationsOnly /> ), @@ -213,8 +219,10 @@ export default function RunDetail() { propertyNames={history?.names ?? []} violations={violationsAfter} residuals={residualsAfter} + witnesses={witnessesAfter} onJumpToFirstViolation={jumpToFirstViolation} hasFirstViolation={history?.firstViolationStep !== undefined} + onJumpToStep={goTo} /> ), }, @@ -232,8 +240,10 @@ export default function RunDetail() { propertyNames={history?.names ?? []} violations={violationsAfter} residuals={residualsAfter} + witnesses={witnessesAfter} onJumpToFirstViolation={jumpToFirstViolation} hasFirstViolation={history?.firstViolationStep !== undefined} + onJumpToStep={goTo} violationsOnly /> ), diff --git a/replay-ui/src/types.ts b/replay-ui/src/types.ts index 773d18b..dfa8708 100644 --- a/replay-ui/src/types.ts +++ b/replay-ui/src/types.ts @@ -121,6 +121,16 @@ export interface ExtractorChange { curr: unknown; } +export interface Witness { + reason?: string; + is_error?: boolean; + // step is the step the failed obligation originated at: the causing step, + // which for deferred obligations (next, eventually) is earlier than the + // step whose record carries the witness. + step?: number; + extractors?: Record; +} + export interface Step { step: number; timestamp: string; @@ -134,4 +144,5 @@ export interface Step { residuals?: Record; metrics?: Metrics; extractor_changes?: Record; + witnesses?: Record; }