From e2a94d48899bb436a57934d0f75b777d2c89995e Mon Sep 17 00:00:00 2001 From: PJ Date: Fri, 5 Jun 2026 22:34:07 +0530 Subject: [PATCH] feat(trace): carry the causing step in violation witnesses and summary --- internal/runner/runner.go | 36 +++++++++++---- internal/runner/runner_test.go | 83 ++++++++++++++++++++++++++++++++++ internal/trace/writer.go | 9 +++- 3 files changed, 117 insertions(+), 11 deletions(-) diff --git a/internal/runner/runner.go b/internal/runner/runner.go index 40d13e4..476d253 100644 --- a/internal/runner/runner.go +++ b/internal/runner/runner.go @@ -8,6 +8,8 @@ import ( "fmt" "io" "log/slog" + "maps" + "slices" "strings" "time" @@ -264,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 @@ -290,10 +289,7 @@ func Run(ctx context.Context, options Options) (Summary, error) { // left pending. Properties already violated mid-run are not re-reported. 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, - }) + summary.Violations = append(summary.Violations, violationRecords(ended, witnesses, stepIndex)...) finalStep := trace.Step{ Index: stepIndex, Timestamp: time.Now(), @@ -784,6 +780,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. @@ -798,10 +814,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 7c37521..5fc3885 100644 --- a/internal/runner/runner_test.go +++ b/internal/runner/runner_test.go @@ -253,6 +253,89 @@ 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_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"` }