fix(runner): record a witness's detection step in the trace

Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J

internal/runner/runner.go

@@ -1006,7 +1006,9 @@ func violationRecords(properties []string, witnesses map[string]trace.Witness, d
 
 // 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.
+// trace. Properties without a captured witness are skipped. stepIndex is the
+// trace line the witness lands on, and stands in as the detection step for a
+// verifier that observed no labeled step (a run-end finalize).
 func collectWitnesses(verifierInstance *verifier.Verifier, properties []string, logger *slog.Logger, stepIndex int) map[string]trace.Witness {
 	if len(properties) == 0 {
 		return nil
@@ -1017,14 +1019,19 @@ func collectWitnesses(verifierInstance *verifier.Verifier, properties []string,
 		if witness == nil {
 			continue
 		}
+		detectedStep := witness.DetectedStep
+		if detectedStep == 0 {
+			detectedStep = stepIndex
+		}
 		logger.Warn("property violated",
-			"step", witness.Step, "detected_step", stepIndex,
+			"step", witness.Step, "detected_step", detectedStep,
 			"property", name, "reason", witness.Reason, "error", witness.IsError)
 		witnesses[name] = trace.Witness{
-			Reason:     witness.Reason,
+			Reason:       witness.Reason,
-			IsError:    witness.IsError,
+			IsError:      witness.IsError,
-			Step:       witness.Step,
+			Step:         witness.Step,
-			Extractors: witness.Extractors,
+			DetectedStep: detectedStep,
+			Extractors:   witness.Extractors,
 		}
 	}
 	if len(witnesses) == 0 {

internal/runner/runner_test.go

@@ -363,6 +363,11 @@ globalThis.actions = actions(() => []);
 		if witness.Step != 2 {
 			t.Errorf("witness step: got %d, want 2 (causing step)", witness.Step)
 		}
+		// The two indices the witness spans are recorded separately: the
+		// extractor snapshot it carries is step 3's state, not step 2's.
+		if witness.DetectedStep != 3 {
+			t.Errorf("witness detected step: got %d, want 3", witness.DetectedStep)
+		}
 	}
 	if err := scanner.Err(); err != nil {
 		t.Fatalf("scan trace: %v", err)

internal/trace/writer.go

@@ -40,17 +40,19 @@ type Step struct {
 	Witnesses map[string]Witness `json:"witnesses,omitempty"`
 }
 
-// Witness is the trace-side record of a property violation: why it fired and a
+// Witness is the trace-side record of a property violation: why it fired, the
-// snapshot of every extractor's value at the violating step.
+// two steps a deferred obligation spans, and the extractor values behind it.
 type Witness struct {
 	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)
+	// armed it. For a deferred obligation (a next, an eventually) this is
-	// this is earlier than the step whose record carries the witness, which is
+	// earlier than the step at which the failure was detected.
-	// where the failure was detected.
+	Step int `json:"step,omitempty"`
-	Step       int                        `json:"step,omitempty"`
+	// DetectedStep is the observation whose evaluation produced the violation.
-	Extractors map[string]json.RawMessage `json:"extractors,omitempty"`
+	// Extractors is that step's state, not Step's.
+	DetectedStep int                        `json:"detected_step,omitempty"`
+	Extractors   map[string]json.RawMessage `json:"extractors,omitempty"`
 }
 
 // ExtractorChange records the prev/curr JSON values of an extractor whose