feat(verifier): label evaluator observations with the runner step index

internal/runner/runner.go

@@ -185,6 +185,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 {

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 {

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