docs(rivet): VCR-DEC-003 — settle synth-provenance-v1 contract for witness MC/DC reconciliation (#396)

[avrabe]

What

witness (#396, PR witness#130 — reconciler + witness object-disposition CLI) landed
its consumer and defined the synth-provenance-v1 contract synth must emit so MC/DC
coverage measured on the WASM can be reconciled against the object code synth's branch
folding/splitting actually produces. This lands the synth-side contract acceptance
as a rivet decision (no code yet — witness explicitly asked to settle the schema before
implementing).

Findings recorded in VCR-DEC-003

• Join key already exists on synth. witness keys by WASM (func_index, byte_offset)
  (walrus InstrLocId); synth's decoder records exactly this as the op_offsets
  side-table (VCR-DBG-001 step 1, wasm_decoder.rs). No decode/manifest change either
  side; the if/else "two arms → one byte_offset" many-to-one join matches.
• Taxonomy maps 1:1 onto real synth transforms: folded-predication = cmp→select→IT
  fuse (default-on v0.13.0); eliminated-constant = guard elision + scry#51 evidence;
  split-into-object-branches = br_table + i64 multi-branch expansion; preserved =
  1:1 br_if.
• One open item raised on MC/DC source-to-object traceability: synth's branch folding/splitting changes the decision set witness measures on wasm #396 before the emitter: the offset-normalization domain
  (module-relative vs function-body-relative).
• Emitter scoped as a follow-up — threads a per-branch kind label through both
  lowering paths (the optimized ir_to_arm path sets source_line: None, so it drops
  provenance today and needs wiring) + serializes behind a CLI flag, frozen-safe.

Gate

Behavior-frozen — docs/traceability artifact only, no code or .text change. rivet
validate: VCR-DEC-003 introduces zero non-xref errors (its synth:396/witness:130
cross-refs are the gate-filtered kind, matching the gale:209 precedent).

Settling reply posted on #396 (issuecomment-4813581111).

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!