The gap
witness measures MC/DC by instrumenting the wasm branches. synth lowers wasm → ARM/RISC-V and changes the branch set during lowering, so the MC/DC witness certifies at the wasm level does not 1:1 represent the object code's structural coverage. For DO-178C Level A / ISO 26262 ASIL D this is the source-to-object structural-coverage traceability obligation (DO-178C 6.4.4.2: account for object structure not directly traceable to source, whether compiler-added or removed).
Three ways synth's lowering moves the decision set (all present today):
1. Fold to predication — a wasm decision becomes branchless. select → conditional move; the #390 pass-4 compare-feeds-br_if fusion → predicated it/movCC; if-conversion. The decision still EXISTS (the condition flag is computed and gates the result), but there's no PC branch for an object-level branch-counter to see. → SAFE direction: the wasm-level MC/DC is the authoritative measurement; the object code just realizes the same decision without a branch. No untraceable object branch.
2. Eliminate a provably-constant branch — a wasm decision disappears. A const-condition (folded by loom upstream or synth) has one side unreachable, so MC/DC for it is infeasible by construction. → Needs JUSTIFICATION, not coverage. This is exactly where scry helps: its constant-condition / reachability analysis is the sound evidence that the branch is dead, so its uncoverable side is justified deactivated/dead code, not a coverage hole.
3. Split into multiple object branches — synth ADDS branches. i64 compare → cmp hi; bne; cmp lo; ...; br_table → comparison ladder / jump table. These object branches are compiler-introduced. → Needs either object-level MC/DC on them OR a faithful-implementation argument that exercising the single wasm decision's MC/DC vectors covers all the split branches. This is the direction that genuinely adds obligations.
How to deal with it — the same provenance spine as #394 (DWARF)
synth should emit a decision-provenance map: for each wasm decision (br_if / select / if / br_table), record how it lowered — {1:1 branch | folded-to-predication | eliminated-constant (+scry evidence) | split-into-N-object-branches}. This is the same source-to-object correspondence the DWARF work (#394) needs (source_line threading is already the spine); one mechanism, two consumers (debugger + coverage reconciler).
A small reconciler (in witness or alongside it) then:
- keeps wasm-level MC/DC authoritative for folded/predicated decisions (case 1);
- marks scry-proven-dead branches as justified-infeasible (case 2) — not coverage gaps;
- flags split decisions (case 3) for object-level coverage or a faithful-implementation argument.
That closes the traceability gap synth's folding currently leaves open, and makes the witness truth table defensible against the object code, not just the wasm.
Coordination
Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001.
The gap
witness measures MC/DC by instrumenting the wasm branches. synth lowers wasm → ARM/RISC-V and changes the branch set during lowering, so the MC/DC witness certifies at the wasm level does not 1:1 represent the object code's structural coverage. For DO-178C Level A / ISO 26262 ASIL D this is the source-to-object structural-coverage traceability obligation (DO-178C 6.4.4.2: account for object structure not directly traceable to source, whether compiler-added or removed).
Three ways synth's lowering moves the decision set (all present today):
1. Fold to predication — a wasm decision becomes branchless.
select→ conditional move; the #390 pass-4 compare-feeds-br_iffusion → predicatedit/movCC; if-conversion. The decision still EXISTS (the condition flag is computed and gates the result), but there's no PC branch for an object-level branch-counter to see. → SAFE direction: the wasm-level MC/DC is the authoritative measurement; the object code just realizes the same decision without a branch. No untraceable object branch.2. Eliminate a provably-constant branch — a wasm decision disappears. A const-condition (folded by loom upstream or synth) has one side unreachable, so MC/DC for it is infeasible by construction. → Needs JUSTIFICATION, not coverage. This is exactly where scry helps: its constant-condition / reachability analysis is the sound evidence that the branch is dead, so its uncoverable side is justified deactivated/dead code, not a coverage hole.
3. Split into multiple object branches — synth ADDS branches. i64 compare →
cmp hi; bne; cmp lo; ...;br_table→ comparison ladder / jump table. These object branches are compiler-introduced. → Needs either object-level MC/DC on them OR a faithful-implementation argument that exercising the single wasm decision's MC/DC vectors covers all the split branches. This is the direction that genuinely adds obligations.How to deal with it — the same provenance spine as #394 (DWARF)
synth should emit a decision-provenance map: for each wasm decision (
br_if/select/if/br_table), record how it lowered —{1:1 branch | folded-to-predication | eliminated-constant (+scry evidence) | split-into-N-object-branches}. This is the same source-to-object correspondence the DWARF work (#394) needs (source_linethreading is already the spine); one mechanism, two consumers (debugger + coverage reconciler).A small reconciler (in witness or alongside it) then:
That closes the traceability gap synth's folding currently leaves open, and makes the witness truth table defensible against the object code, not just the wasm.
Coordination
Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001.