From c5bd36711a3bed0c71a61b74eaee1de7a0cdbc85 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 22 Jun 2026 06:23:16 +0200 Subject: [PATCH] docs(rivet): keep the DWARF verification artifact current with steps 1-4 (VCR-DBG-001, #242) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SWVER-016 was written when only DWARF steps 1-2 (decoder op_offsets + .debug_line read) were implemented. Steps 3 (compose, #414) and 4-emit-logic (#415) have since landed with their own passing tests, leaving the verification artifact stale. Updates SWVER-016 to verify the full frozen-safe read→compose→emit LOGIC (steps 1-4) and reference all the tests that discharge it: wasm_decoder op_offsets, dwarf_line_read_spike, dwarf_coherent_fixture, dwarf_compose_step3 + dwarf_line:: unit tests, dwarf_emit_roundtrip_step4. The GATED step-4 ELF wiring (production gimli dep + ELF builder + host-link, v0.12.0) stays explicitly open. Keeps the requirement→test mapping accurate as the feature grew (the gap reported in pulseengine.eu#93) — no coverage-count change (VCR-DBG-001 already covered), just an honest, current trace. Frozen-safe: rivet artifact only, zero codegen, frozen fixtures bit-identical, rivet non-xref 0; all referenced tests verified passing. Trace: skip Co-Authored-By: Claude Opus 4.8 --- artifacts/sw-verification.yaml | 37 +++++++++++++++++++++++----------- 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 4cf92d7f..fa393299 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -350,27 +350,40 @@ artifacts: - id: SWVER-016 type: sw-verification - title: DWARF Tier-1 source-provenance read path (steps 1-2) + title: DWARF Tier-1 source-provenance read→compose→emit logic (steps 1-4, frozen-safe) description: > - Verifies the implemented portion of VCR-DBG-001: step 1 — the decoder - records the per-op wasm code BYTE OFFSET (op_offsets side-table); step 2 — - the input wasm's `.debug_line` parses into (wasm-byte-offset to file:line) - rows via gimli (DEV-dep). Together these are the read side of the - source-to-object provenance bridge. The COMPOSE (step 3) and EMIT (step 4) - remain open (see the VCR-DBG-001 PROGRESS notes), so this verifies the - read path only, not the full Tier-1 feature. + Verifies the frozen-safe portion of VCR-DBG-001 — the full read→compose→emit + LOGIC, all proven in-tree without a production gimli dep or any output-ELF + change (the gated step-4 ELF wiring + host-link is the v0.12.0 release step, + verified separately when it lands): + step 1 — the decoder records the per-op wasm code BYTE OFFSET + (op_offsets side-table); + step 2 — the input wasm's `.debug_line` parses into (wasm-byte-offset → + file:line) rows via gimli (DEV-dep); + step 3 — synth_core::dwarf_line::op_offsets_to_source joins op-index → + source line, normalizing module-relative op_offsets into the + code-relative DWARF address space (single code-base subtraction); + step 4 (logic) — synth's composed table emits as a `.debug_line` via + gimli::write and reads back faithfully (every address → the same + source line). + A coherence-checked fixture (scripts/repro/dwarf_coherent.wasm) underpins + steps 2-4 (its `.debug_line` describes its OWN source, unlike the dissolved + fixtures). The gated EMIT wiring (production gimli dep + ELF builder + real + ARM offsets) remains open — see the VCR-DBG-001 PROGRESS notes. status: implemented - tags: [dwarf, debuggability, vcr-dbg, partial-steps-1-2] + tags: [dwarf, debuggability, vcr-dbg, steps-1-4-frozen-safe] links: - type: verifies target: VCR-DBG-001 fields: method: automated-test steps: - run: "cargo test -p synth-core --test dwarf_line_read_spike && cargo test -p synth-core dbg001" + run: "cargo test -p synth-core dwarf_ dbg001 && cargo test -p synth-core --lib dwarf_line::" coverage: > - crates/synth-core/src/wasm_decoder.rs op_offsets test (step 1) + - crates/synth-core/tests/dwarf_line_read_spike.rs (.debug_line to file:line, step 2) + wasm_decoder.rs op_offsets test (step 1) + dwarf_line_read_spike.rs + (step 2) + dwarf_coherent_fixture.rs (coherent fixture) + + dwarf_compose_step3.rs & dwarf_line:: unit tests (step 3 compose) + + dwarf_emit_roundtrip_step4.rs (step-4 emit logic round-trip) - id: SWVER-017 type: sw-verification