From 16134f25845c4235c0699ce0b4075d531c7e078d Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Wed, 12 Aug 2026 16:47:25 +0530
Subject: [PATCH] fix(verifier): split a witness's origin step from its
 detection step

A deferred obligation spans two steps: the one that armed it and the one whose
reduction failed. They were conflated under one index, so the extractor snapshot
(which is the detecting step's state) was reported against the origin step.

Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
---
 internal/verifier/worker.go | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/internal/verifier/worker.go b/internal/verifier/worker.go
index bfab422..1eb9476 100644
--- a/internal/verifier/worker.go
+++ b/internal/verifier/worker.go
@@ -476,21 +476,27 @@ func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
 }
 
 // Witness is the verifier-level record of a property violation: the LTL reason
-// (a predicate's thrown-error text, "predicate false", or a liveness failure),
-// the step it fired at, and a snapshot of every extractor's current value at
-// that step. The snapshot lets a reader see the state that produced the
-// violation without replaying the run.
+// (a predicate's thrown-error text, "predicate false", or a liveness failure)
+// and the two step indices a deferred obligation spans.
+//
+// Step is the origin: the step whose observation armed the obligation that
+// failed. DetectedStep is the observation whose reduction produced the
+// violation, which for a next or an eventually is later. Extractors is that
+// observation's state, so it belongs to DetectedStep and not to Step; the two
+// were previously conflated under one index.
 type Witness struct {
-	Property   string
-	Reason     string
-	Step       int
-	IsError    bool
-	Extractors map[string]json.RawMessage
+	Property     string
+	Reason       string
+	Step         int
+	DetectedStep int
+	IsError      bool
+	Extractors   map[string]json.RawMessage
 }
 
 // captureWitness records the witness for a property that just transitioned to
 // violated, snapshotting the current extractor values so the cause is visible
-// after the run.
+// after the run. The snapshot is the state of the observation being reduced,
+// which the witness records as its detection step.
 func (v *Verifier) captureWitness(name string) {
 	evaluator, ok := v.evaluators[name]
 	if !ok {
@@ -501,11 +507,12 @@ func (v *Verifier) captureWitness(name string) {
 		return
 	}
 	v.witnesses[name] = Witness{
-		Property:   name,
-		Reason:     violation.Reason,
-		Step:       violation.Step,
-		IsError:    violation.IsError,
-		Extractors: v.extractorSnapshot(),
+		Property:     name,
+		Reason:       violation.Reason,
+		Step:         violation.Step,
+		DetectedStep: v.stepIndex,
+		IsError:      violation.IsError,
+		Extractors:   v.extractorSnapshot(),
 	}
 }