From 6df43f9f6b631e600d66ffc0b284856cc7e931c4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 26 Jun 2026 23:32:37 +0200 Subject: [PATCH] =?UTF-8?q?docs(rivet):=20VCR-DEC-003=20=E2=80=94=20settle?= =?UTF-8?q?=20synth-provenance-v1=20contract=20for=20witness=20MC/DC=20rec?= =?UTF-8?q?onciliation=20(#396)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit witness (#396, PR witness#130) landed its reconciler + `witness object-disposition` CLI and defined the `synth-provenance-v1` schema synth must emit so MC/DC coverage measured on the WASM reconciles against the object code synth's branch folding/splitting produces. Records the synth-side acceptance of the contract as a rivet decision: - Join key CONFIRMED available — synth's `op_offsets` side-table (VCR-DBG-001 step 1) is the per-function WASM byte offset witness joins on; no decode/manifest change either side. - The 4-kind taxonomy (preserved / folded-predication / eliminated-constant / split-into-object-branches) maps 1:1 onto real synth transforms (cmp→select fuse, guard elision + scry#51 evidence, br_table/i64 multi-branch expansion). - ONE open item raised on #396 before implementing: the offset-normalization domain (module-relative vs function-body-relative) so the join is exact. - Emitter scoped as the follow-up milestone (label branches through both lowering paths — optimized `ir_to_arm` drops provenance today — + serialize behind a CLI flag, frozen-safe/additive). Behavior-frozen: docs/traceability artifact only, no code or `.text` change. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 71 +++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 4d35383..0341b09 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1238,6 +1238,77 @@ artifacts: criterion: t_lock << 887, handoff < 1661). All frozen fixtures stay bit-identical at every step. + - id: VCR-DEC-003 + type: sw-req + title: "Decision: emit `synth-provenance-v1` branch-transformation map for witness MC/DC source-to-object reconciliation (#396, witness#130)" + description: > + witness (#396, PR witness#130 — reconciler + `witness object-disposition` + CLI landed AHEAD of synth) defines the 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. Schema + `synth-provenance-v1`: a list of entries + `{ func_index, instruction_offset, kind, count?, scry_evidence? }` where + `kind ∈ preserved | folded-predication | eliminated-constant | + split-into-object-branches`. witness's reconciler maps each to an + object-verdict: preserved/folded-predication → obligation-stands (WASM MC/DC + authoritative); eliminated-constant → justified-infeasible (carries optional + scry#51 evidence); split-into-object-branches → needs-object-coverage (N new + object obligations); an object branch witness never instrumented → + only-in-synth divergence (surfaced, not hidden). Output extends the + rivet-evidence schema as `witness-object-disposition-v1`. + + FEASIBILITY — the join key ALREADY EXISTS in synth. witness keys by the WASM + `(func_index, byte_offset)` (from walrus `InstrLocId`); synth's decoder + records exactly this as the `op_offsets` side-table (VCR-DBG-001 step 1, + SWVER-016 — per-op WASM byte offset, parallel to ops, per function). No + decoder/manifest change is needed on either side; an if/else's two arms share + one WASM op offset (one `if` instruction), matching witness's intentionally + many-to-one join (emit one entry per WASM instruction, not per witness + branch-arm). + + TAXONOMY maps cleanly onto synth's real transformations: folded-predication = + the cmp→select→IT fuse (VCR-SEL-004, SYNTH_CMP_SELECT_FUSE, default-on); + eliminated-constant = constant-condition guard elision (Opt-1a) carrying + scry#51 reachability evidence; split-into-object-branches = `br_table` + lowering (#508) and the i64 ops that expand one WASM branch into a multi-cmp/ + 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. + status: proposed + tags: [witness, mcdc, traceability, provenance, vcr-dbg, decision, integration] + links: + - type: derives-from + target: VCR-001 + - type: refines + target: VCR-DBG-001 + - type: traces-to + target: synth:396 + - type: traces-to + target: witness:130 + fields: + req-type: constraint + priority: should + verification-criteria: > + Contract-settling step (this artifact): the `synth-provenance-v1` schema + + kind-taxonomy + join-key (op_offsets) are agreed with witness on #396, and + the offset-normalization domain is resolved. Implementation milestone + (separate): `witness object-disposition --manifest m.witness.json + --provenance synth-map.json` composes end-to-end on a shared fixture, with + each kind producing its specified object-verdict; the emitter is frozen-safe + (no frozen `.text` byte changes — control_step 0x00210A55, flight_algo + 0x07FDF307). + - id: VCR-PERF-001 type: sw-req title: "Silicon-quantified gust hot-path size gap: 3.9× vs LLVM, per-pass attribution (gale #390)"