fix(verifier): record the extractor state the predicates actually read

On the web path extractor bodies are evaluated in V8 and injected here, but only
the goja value was replaced. The trace diff and the violation witness therefore
described a state no property ever saw.

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

internal/runner/web_extractor_trace_test.go

@@ -0,0 +1,118 @@
+package runner
+
+import (
+	"bufio"
+	"context"
+	"encoding/json"
+	"os"
+	"path/filepath"
+	"testing"
+	"time"
+
+	mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
+	"github.com/priyanshujain/sanderling/internal/trace"
+)
+
+// engineDisagreementSpec makes the two runtimes disagree on purpose: the
+// extractor body returns "goja" when it runs in-process, and the web driver
+// below reports "v8" for the same extractor. The property is true of one value
+// and false of the other, so the verdict names the engine the verdict used.
+const engineDisagreementSpec = `
+import { actions, always, extract } from "@sanderling/spec";
+const engine = extract("engine", () => "goja");
+globalThis.properties = {
+  ranInGoja: always(() => engine.current === "goja"),
+};
+globalThis.actions = actions(() => []);
+`
+
+// webMockDriver presents the mock device driver as a web target so the runner
+// takes the V8 path, where extractor values come from the page rather than
+// from goja.
+type webMockDriver struct {
+	*mockdriver.Driver
+	overrides map[int]json.RawMessage
+}
+
+func (d *webMockDriver) InstallBundle(context.Context, []byte) error { return nil }
+
+func (d *webMockDriver) EvaluateExtractors(context.Context) (map[int]json.RawMessage, error) {
+	return d.overrides, nil
+}
+
+func (d *webMockDriver) NextActionFromV8(context.Context) (json.RawMessage, error) {
+	return nil, nil
+}
+
+// TestRunner_TraceRecordsTheValueTheVerdictUsed fails if the trace and the
+// verdict disagree about an extractor. A witness is only an explanation of a
+// violation if it holds the state the violated property was evaluated against.
+func TestRunner_TraceRecordsTheValueTheVerdictUsed(t *testing.T) {
+	state := newHarnessWithSpec(t, engineDisagreementSpec)
+	const pageValue = `"v8"`
+	web := &webMockDriver{
+		Driver:    state.mock,
+		overrides: map[int]json.RawMessage{0: json.RawMessage(pageValue)},
+	}
+
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Second)
+	defer cancel()
+	summary, err := Run(ctx, Options{
+		Duration:    100 * time.Millisecond,
+		IdleTimeout: 20 * time.Millisecond,
+		Driver:      web,
+		Verifier:    state.verifier,
+		TraceWriter: state.writer,
+	})
+	if err != nil {
+		t.Fatalf("Run: %v", err)
+	}
+	if !containsProperty(summary.Violations, "ranInGoja") {
+		t.Fatalf("ranInGoja did not violate, so the page value never reached the verdict: %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"`
+		ExtractorChanges map[string]trace.ExtractorChange `json:"extractor_changes"`
+		Witnesses        map[string]trace.Witness         `json:"witnesses"`
+	}
+	changes, witnesses := 0, 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 change, ok := line.ExtractorChanges["engine"]; ok {
+			changes++
+			if got := string(change.Curr); got != pageValue {
+				t.Errorf("step %d: trace records engine=%s, verdict used %s",
+					line.Step, got, pageValue)
+			}
+		}
+		for name, witness := range line.Witnesses {
+			witnesses++
+			if got := string(witness.Extractors["engine"]); got != pageValue {
+				t.Errorf("step %d: %s witness records engine=%s, verdict used %s",
+					line.Step, name, got, pageValue)
+			}
+		}
+	}
+	if err := scanner.Err(); err != nil {
+		t.Fatalf("scan trace: %v", err)
+	}
+	if changes == 0 {
+		t.Error("no extractor change reached the trace; nothing was compared")
+	}
+	if witnesses == 0 {
+		t.Error("no witness reached the trace; nothing was compared")
+	}
+}

internal/verifier/verifier_test.go

@@ -1276,6 +1276,46 @@ func TestOverrideExtractorValues_PropagatesNestedObjectFields(t *testing.T) {
 	}
 }
 
+// TestOverrideExtractorValues_RecordedStateMatchesEvaluatedState pins the
+// reported state to the state predicates read. The web path evaluates
+// extractor bodies in V8 and injects the results here, so a diff or a witness
+// built from the goja value would describe a state no property ever saw.
+func TestOverrideExtractorValues_RecordedStateMatchesEvaluatedState(t *testing.T) {
+	verifier := newVerifier(t)
+	mustLoad(t, verifier, helloSpec)
+
+	if err := verifier.PushSnapshot(SnapshotInput{
+		Snapshots: Snapshots{"ledger.balance": json.RawMessage(`100`)},
+	}); err != nil {
+		t.Fatal(err)
+	}
+	if _, err := verifier.OverrideExtractorValues(map[int]json.RawMessage{
+		1: json.RawMessage(`-7`),
+	}); err != nil {
+		t.Fatal(err)
+	}
+	verifier.EvaluateProperties()
+
+	balance := verifier.runtime.GlobalObject().Get("balance").ToObject(verifier.runtime)
+	evaluated := balance.Get("current").String()
+	change, ok := verifier.ChangedExtractors()["extractor_1"]
+	if !ok {
+		t.Fatal("ChangedExtractors reported no change for the overridden extractor")
+	}
+	if string(change.Curr) != evaluated {
+		t.Errorf("ChangedExtractors curr = %s, want %s (the value predicates read)",
+			change.Curr, evaluated)
+	}
+	witness := verifier.Witness("balanceNonNegative")
+	if witness == nil {
+		t.Fatal("balanceNonNegative did not violate on the overridden value")
+	}
+	if got := string(witness.Extractors["extractor_1"]); got != evaluated {
+		t.Errorf("witness extractor = %s, want %s (the value predicates read)",
+			got, evaluated)
+	}
+}
+
 // TestUnsupportedVerbs_CollectedDedupedInOrder drives the real host binding the
 // shared picker invokes (__sanderlingHost__.reportUnsupported) and asserts the
 // verifier collects each verb once, in first-seen order, for the run report.

internal/verifier/worker.go

@@ -392,6 +392,12 @@ func (v *Verifier) ChangedExtractors() map[string]ExtractorChange {
 // call this unconditionally. The override must run *after* PushSnapshot
 // (which advanced `previous`) and *before* EvaluateProperties.
 //
+// The JSON snapshot `curr` is replaced alongside the value, so the diffs in
+// ChangedExtractors and the witness recorded by captureWitness describe the
+// state the verdict was computed from. Recording the goja value while a
+// predicate read the V8 one makes a witness explain a violation with a state
+// that never reached the property.
+//
 // Out-of-range indices are tolerated (skipped) rather than fatal: V8 and goja
 // register extractors from the same spec bundle so counts should always
 // match, but a stale or partial override map should not block valid overrides
@@ -411,6 +417,7 @@ func (v *Verifier) OverrideExtractorValues(overrides map[int]json.RawMessage) (s
 			return skipped, fmt.Errorf("extractor override %d: %w", index, conversionErr)
 		}
 		v.extractors[index].currentValue = value
+		v.extractors[index].curr = encodeExtractorValue(value)
 	}
 	return skipped, nil
 }