From 4780b03680319a0e1bedff72b00eca6218f21bb9 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 20 Jun 2026 17:11:09 +0200 Subject: [PATCH 1/2] =?UTF-8?q?docs(roadmap):=20VCR-DBG-001=20=E2=80=94=20?= =?UTF-8?q?emit=20DWARF=20in=20the=20ELF=20(synth=20#394);=20Tier-2=20gate?= =?UTF-8?q?d=20on=20VCR-RA=20value=E2=86=92location=20map?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit synth drops all DWARF (zero .debug_* in output) → bare-metal images aren't source-debuggable. The input wasm carries it and meld already remaps it through fusion (meld-core/src/dwarf.rs); synth is the only stage that drops it. Tractable: synth's source_line threading (~220 sites) is the (machine-addr → wasm-offset) half — compose with the wasm DWARF for (machine-addr → source). Two tiers: Tier 1 .debug_line (machine-addr → source line; raw material ready; regalloc-independent) → breakpoints/backtraces; Tier 2 .debug_info variable locations gated on the VCR-RA value→location mapping (the same (pc,local)→ARM-vreg map surfaced in VCR-RA-010). DWARF is additive non-loadable sections ⇒ frozen fixtures bit-identical. Coordinate encodings with meld end-to-end. Docs only — no code, frozen-fixture-safe. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 54 +++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index aa266777..e01b30a2 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1046,3 +1046,57 @@ artifacts: LAYER (2), next: acyclic + direct-only + canonical-frame modules derive B automatically (output "proven"); call_indirect / recursion / non-canonical frame ⇒ refuse → fall back to (1). LAYER (3): scry#51 proves the tail. + + # --------------------------------------------------------------------------- + # Toolchain completeness — debuggability (not a VCR correctness item, but + # Tier-2 depends on the VCR-RA value→location mapping) + # --------------------------------------------------------------------------- + + - id: VCR-DBG-001 + type: sw-req + title: "Emit DWARF in the ARM/RISC-V ELF — synth drops debug info (synth #394)" + description: > + synth #394: synth lowers WASM → bare-metal ELF but emits ZERO DWARF + (confirmed: no `.debug_*` in any output), so a synth-compiled image is not + source-debuggable (no source line at a PC, no variable locations, no named + backtraces). The input carries it and the upstream preserves it: real + Rust/clang→wasm modules ship DWARF in custom sections (e.g. + msgq_put_359.wasm: `.debug_*` across 8 custom sections), and MELD already + REMAPS that wasm DWARF through fusion (meld-core/src/dwarf.rs + + dwarf_remap_witness/dwarf_passthrough tests). synth is the ONLY stage that + drops it — like meld adjusts wasm-DWARF through its transform, synth must + EMIT ARM/RISC-V-ELF DWARF through its WASM→machine lowering. + TRACTABLE — synth already has the spine: every ArmInstruction carries + `source_line` (the wasm op index, ~220 threading sites) = the + (machine-addr → wasm-offset) half; compose with the wasm DWARF + (wasm-offset → source) for (machine-addr → source). + TWO TIERS: + - Tier 1 `.debug_line` (near-term, raw material ready): machine-addr → + source line ⇒ breakpoints/single-step land on source, file:line + backtraces. Independent of regalloc. + - Tier 2 `.debug_info` variable locations (DWARF location lists): + source var → ARM reg/stack-slot range. Needs the value→physical-location + mapping the register allocator produces — the SAME (pc, local) → + ARM-vreg mapping surfaced in VCR-RA-010 — so it is GATED on the VCR-RA + allocator wiring. + DWARF is additive non-loadable sections ⇒ `.text` and the frozen fixtures + stay bit-identical. Coordinate the line/var encodings with meld so + source → meld → synth → on-target debugger composes end-to-end. + status: proposed + tags: [toolchain, dwarf, debuggability, elf, meld-coordination, gale-adjacent, synth-394] + links: + - type: derives-from + target: VCR-001 + - type: constrained-by + target: VCR-RA-001 + fields: + req-type: functional + priority: should + verification-criteria: > + Tier 1: a synth-compiled ELF from a DWARF-carrying wasm, loaded in + gdb/lldb (or Renode) against the target, stops at the correct SOURCE line + on a PC breakpoint and shows a file:line backtrace; `.text` byte-identical + to the no-DWARF build (DWARF additive, non-loadable) ⇒ all frozen fixtures + unchanged. Tier 2: a local variable resolves to its register/stack + location at a breakpoint, validated once the VCR-RA value→location map + exists. From 5d582e3ac3b7c55198ea18455600151b89388b92 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 20 Jun 2026 17:20:56 +0200 Subject: [PATCH 2/2] =?UTF-8?q?docs(roadmap):=20VCR-COV-001=20=E2=80=94=20?= =?UTF-8?q?MC/DC=20source-to-object=20traceability=20(synth=20#396);=20sha?= =?UTF-8?q?res=20the=20DWARF=20provenance=20spine?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit witness measures MC/DC on wasm branches; synth's wasm→ARM lowering changes the branch set (fold→predication / eliminate-constant / split), so wasm-level MC/DC doesn't 1:1 represent the object code (DO-178C 6.4.4.2). Three directions: fold (safe — wasm MC/DC authoritative), eliminate (justified by scry's constant-condition evidence), split (the one that adds object obligations). Fix = the SAME decision-provenance map as VCR-DBG-001 (#394): one mechanism (the source_line threading already present), two consumers — debugger (DWARF) + coverage reconciler (witness). Bundled with the DWARF artifact because they share the source-to-object provenance spine. Coordinate with witness + scry. Docs only — frozen-fixture-safe. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 52 +++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index e01b30a2..16a31553 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1100,3 +1100,55 @@ artifacts: unchanged. Tier 2: a local variable resolves to its register/stack location at a breakpoint, validated once the VCR-RA value→location map exists. + + - id: VCR-COV-001 + type: sw-req + title: "MC/DC source-to-object traceability: synth's branch folding changes witness's decision set (synth #396)" + description: > + synth #396: witness measures MC/DC by instrumenting WASM branches, but + synth's WASM→ARM lowering CHANGES the branch set, so the WASM-level MC/DC + does not 1:1 represent the OBJECT code's structural coverage (DO-178C + 6.4.4.2 / ISO 26262 ASIL D source-to-object obligation). Three directions, + all present in synth today (select→cmov, the #390 pass-4 compare→br_if + fusion, i64-compare, br_table): + (1) FOLD to predication — a WASM decision becomes branchless (no PC + branch). SAFE: WASM-level MC/DC stays authoritative; the object code + realizes the same decision via a flag, no untraceable branch. + (2) ELIMINATE a provably-constant branch — one side unreachable ⇒ MC/DC + infeasible by construction. Needs JUSTIFICATION, and scry's + constant-condition/reachability analysis is the sound evidence that + the dead side is justified-deactivated, not a coverage hole. + (3) SPLIT into N object branches (i64 cmp → cmp/bne/cmp; br_table → + ladder) — compiler-INTRODUCED branches. Needs object-level MC/DC OR a + faithful-implementation argument that the source decision's vectors + cover them. The one direction that genuinely ADDS obligations. + FIX = the SAME provenance spine as VCR-DBG-001 (#394): synth emits a + decision-provenance map per WASM decision (br_if/select/if/br_table) → + {1:1 branch | folded-predication | eliminated-constant(+scry evidence) | + split-into-N}. One mechanism (the source_line threading already present), + two consumers — the debugger (DWARF) and a coverage reconciler (witness). + The reconciler keeps WASM MC/DC authoritative for (1), marks scry-proven + dead branches justified for (2), flags (3) for object coverage. + Coordinate with witness (consume the map) + scry (dead-branch evidence, + ties to VCR-RA-010 / scry#51). + status: proposed + tags: [toolchain, mcdc, structural-coverage, do-178c, witness-coordination, scry, traceability, synth-396] + links: + - type: derives-from + target: VCR-001 + - type: refines + target: VCR-DBG-001 + - type: constrained-by + target: VCR-RA-010 + fields: + req-type: functional + priority: should + verification-criteria: > + A synth-compiled module's witness MC/DC truth table reconciles against + the ARM object code via the decision-provenance map: every WASM decision + is classified (folded / eliminated / split / 1:1); folded decisions keep + their WASM-level obligation; scry-proven-dead branches are marked + justified-infeasible (not gaps); split decisions either get object-level + MC/DC or a recorded faithful-implementation argument. No object branch is + untraceable to a source decision. Frozen fixtures bit-identical (the map + is emitted metadata, not a codegen change).