docs(rivet): VCR-DEC-003 — resolve witness provenance offset-domain (#396) (#521)

The one open item on the synth-provenance-v1 contract (#396) is resolved from
synth's side, verified from code: synth's op_offsets are ABSOLUTE byte offsets
into the original .wasm binary (wasm_decoder.rs feeds the whole module via
Parser::new(0).parse_all + reads per-op offsets via into_iter_with_offsets),
the same origin as walrus InstrLocId — so the join is direct, no normalization.
Replaces the normalization caveat with the real invariant (both tools key off
the same input .wasm bytes). Pending only witness's confirmation of the walrus
side. Behavior-frozen: docs/traceability only.

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: avrabe

artifacts/verified-codegen-roadmap.yaml

@@ -1286,17 +1286,25 @@ artifacts:
       branch object sequence (I64SetCond / I64Shl / I64DivU / …); preserved =
       every 1:1 `br_if`.
 
-      ONE OPEN ITEM TO SETTLE BEFORE IMPLEMENTING (raised on #396): the offset
-      NORMALIZATION domain — synth's `op_offsets` are module-relative WASM byte
-      offsets (into the code section); witness's `InstrLocId` byte_offset must be
-      confirmed module-relative vs function-body-relative so the join is exact, not
-      off-by-a-function-header. Once witness confirms, the emitter is the
-      implementation milestone: thread a per-branch transformation label through
-      BOTH lowering paths (optimized `ir_to_arm` currently sets `source_line: None`
-      — provenance is dropped there today; the direct selector carries it) and
-      serialize `synth-provenance-v1` behind a CLI flag (frozen-safe: additive
-      output file, no `.text` change). NOT in scope for the contract-settling step;
-      tracked as the VCR-DBG/witness follow-up.
+      OFFSET-NORMALIZATION DOMAIN — RESOLVED on synth's side (#396, 2026-06-27):
+      synth's `op_offsets` are ABSOLUTE byte offsets into the original `.wasm`
+      binary, verified from code — `wasm_decoder.rs` feeds the whole module to
+      wasmparser (`Parser::new(0).parse_all(wasm_bytes)`, base 0) and reads per-op
+      offsets via `into_iter_with_offsets()` (whole-buffer positions, NOT
+      function-body-relative). walrus `InstrLocId` is the same origin (offset in
+      the original Wasm buffer), so the join is DIRECT — no per-function header
+      subtraction, no normalization. Pending only witness's confirmation of the
+      walrus side. The replacement invariant to carry in the contract: both tools
+      must key off the SAME input `.wasm` bytes (witness measures the module before
+      synth lowers it; if witness re-serializes via walrus, the `InstrLocId`s must
+      refer to the bytes synth then compiles).
+
+      Remaining = the EMITTER milestone (purely synth-internal): thread a per-branch
+      transformation label through BOTH lowering paths (optimized `ir_to_arm`
+      currently sets `source_line: None` — provenance is dropped there today; the
+      direct selector carries it) and serialize `synth-provenance-v1` behind a CLI
+      flag (frozen-safe: additive output file, no `.text` change). NOT in scope for
+      the contract-settling step; tracked as the VCR-DBG/witness follow-up.
     status: proposed
     tags: [witness, mcdc, traceability, provenance, vcr-dbg, decision, integration]
     links: