feat(#396): synth-provenance-v1 branch-transformation map + reconciliation gate (VCR-DEC-003)

[avrabe]

VCR-DEC-003 (#396, witness#130) — synth-provenance-v1 source-to-object branch-transformation map

synth's lowering changes the branch structure between the WASM source and the ARM object (cmp→select fusion → IT-block predication, br_table splitting, wide-branch expansion). witness measures MC/DC on the WASM component; to certify the OBJECT it must reconcile each object-level branch/condition back to its source condition. Without a provenance map that reconciliation is impossible — the #396 / witness#130 source-to-object traceability gap. This PR ships the emitter + the non-vacuous reconciliation gate.

Deliverable

1. Emitter (--emit-provenance) — writes a synth-provenance-v1 JSON sidecar (<output>.provenance.json). Frozen-safe: the ELF is byte-identical with and without the flag (verified on control_step.wasm). Derived post-hoc at the CLI from the compiled op stream + op_offsets + the ARM line_map + a new object-branch side-table BranchMap (crate::backend::BranchClass, captured at the ARM encode loop — the one datum post-hoc derivation couldn't recover: which emitted instruction IS a conditional branch vs a predicated move).

2. Reconciliation gate (provenance_reconciliation_396, CI job provenance-gate) — parses the sidecar as an independent consumer and asserts the two properties #396 exists to guarantee. Verified non-vacuous: mislabeling SelectMove as CondBranch turns the gate RED.

Schema synth-provenance-v1

{ schema, module, functions: [
  { func_index, name,
    entries: [ { instruction_offset,   // wasm byte offset — witness join key
                 wasm_op_index, op, kind, object_pcs, count?, scry_evidence? } ],
    object_cond_branches: [ { pc, wasm_op_index?, instruction_offset?, resolved, note? } ] } ] }

kind ∈ preserved | folded-predication | split-into-object-branches | eliminated-constant.

Fixture source→object correspondence (provenance_branches_396.wat)

source op (wasm off)	kind	object realization
br_if @47	preserved	cond branch @0x12
select @70	folded-predication	IT-block predicated move @0x32 (no branch)
br_table @81	split-into-object-branches (count 2)	cond @0x3c, cond @0x40, uncond @0x42
br @95	preserved	uncond branch @0x50

object_cond_branches: all 3 real object conditional branches (0x12, 0x3c, 0x40) reconcile back to their source condition — clause (a) satisfied non-vacuously. On a real fixture (msgq_put) an uncovered trap-guard branch is surfaced resolved:false with a note, never hidden.

Bounded v1 — named follow-ups

• optimized ir_to_arm on some op shapes drops source_line; such functions are loud-declined from the sidecar (warn + skip) rather than mislabeled.
• i64-expansion / div-mem trap-guard object branches are surfaced-unresolved, not reconciled.
• RISC-V / AArch64 carry no branch_map (ARM-Thumb only in v1).
• witness#130 object-disposition end-to-end compose.

Verification

• 3 emitter unit tests (synth-core::provenance) + reconciliation gate; full workspace green (2278 tests). ELF byte-identity confirmed. rivet validate non-xref error count unchanged (0). Roadmap VCR-DEC-003 → implemented.

Coordinates conceptually with witness#130 (referenced); the map + parse-assert gate live entirely in synth.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 83.83459% with 43 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	66.19%	24 Missing ⚠️
crates/synth-core/src/provenance.rs	88.75%	19 Missing ⚠️

📢 Thoughts on this report? Let us know!