From 579e484941e1dcd24afa98887104c9021436d4ec Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 00:23:18 +0200 Subject: [PATCH] =?UTF-8?q?docs(rivet):=20VCR-DEC-003=20=E2=80=94=20resolv?= =?UTF-8?q?e=20witness=20provenance=20offset-domain=20(#396)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- artifacts/verified-codegen-roadmap.yaml | 30 ++++++++++++++++--------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 8bbb12c..c7a5283 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/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: