Skip to content

Commit f87554e

Browse files
avrabeclaude
andauthored
docs(rivet): keep the DWARF verification artifact current with steps 1-4 (VCR-DBG-001, #242) (#416)
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 <noreply@anthropic.com>
1 parent 20d4855 commit f87554e

1 file changed

Lines changed: 25 additions & 12 deletions

File tree

artifacts/sw-verification.yaml

Lines changed: 25 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -350,27 +350,40 @@ artifacts:
350350
351351
- id: SWVER-016
352352
type: sw-verification
353-
title: DWARF Tier-1 source-provenance read path (steps 1-2)
353+
title: DWARF Tier-1 source-provenance read→compose→emit logic (steps 1-4, frozen-safe)
354354
description: >
355-
Verifies the implemented portion of VCR-DBG-001: step 1 — the decoder
356-
records the per-op wasm code BYTE OFFSET (op_offsets side-table); step 2 —
357-
the input wasm's `.debug_line` parses into (wasm-byte-offset to file:line)
358-
rows via gimli (DEV-dep). Together these are the read side of the
359-
source-to-object provenance bridge. The COMPOSE (step 3) and EMIT (step 4)
360-
remain open (see the VCR-DBG-001 PROGRESS notes), so this verifies the
361-
read path only, not the full Tier-1 feature.
355+
Verifies the frozen-safe portion of VCR-DBG-001 — the full read→compose→emit
356+
LOGIC, all proven in-tree without a production gimli dep or any output-ELF
357+
change (the gated step-4 ELF wiring + host-link is the v0.12.0 release step,
358+
verified separately when it lands):
359+
step 1 — the decoder records the per-op wasm code BYTE OFFSET
360+
(op_offsets side-table);
361+
step 2 — the input wasm's `.debug_line` parses into (wasm-byte-offset →
362+
file:line) rows via gimli (DEV-dep);
363+
step 3 — synth_core::dwarf_line::op_offsets_to_source joins op-index →
364+
source line, normalizing module-relative op_offsets into the
365+
code-relative DWARF address space (single code-base subtraction);
366+
step 4 (logic) — synth's composed table emits as a `.debug_line` via
367+
gimli::write and reads back faithfully (every address → the same
368+
source line).
369+
A coherence-checked fixture (scripts/repro/dwarf_coherent.wasm) underpins
370+
steps 2-4 (its `.debug_line` describes its OWN source, unlike the dissolved
371+
fixtures). The gated EMIT wiring (production gimli dep + ELF builder + real
372+
ARM offsets) remains open — see the VCR-DBG-001 PROGRESS notes.
362373
status: implemented
363-
tags: [dwarf, debuggability, vcr-dbg, partial-steps-1-2]
374+
tags: [dwarf, debuggability, vcr-dbg, steps-1-4-frozen-safe]
364375
links:
365376
- type: verifies
366377
target: VCR-DBG-001
367378
fields:
368379
method: automated-test
369380
steps:
370-
run: "cargo test -p synth-core --test dwarf_line_read_spike && cargo test -p synth-core dbg001"
381+
run: "cargo test -p synth-core dwarf_ dbg001 && cargo test -p synth-core --lib dwarf_line::"
371382
coverage: >
372-
crates/synth-core/src/wasm_decoder.rs op_offsets test (step 1) +
373-
crates/synth-core/tests/dwarf_line_read_spike.rs (.debug_line to file:line, step 2)
383+
wasm_decoder.rs op_offsets test (step 1) + dwarf_line_read_spike.rs
384+
(step 2) + dwarf_coherent_fixture.rs (coherent fixture) +
385+
dwarf_compose_step3.rs & dwarf_line:: unit tests (step 3 compose) +
386+
dwarf_emit_roundtrip_step4.rs (step-4 emit logic round-trip)
374387
375388
- id: SWVER-017
376389
type: sw-verification

0 commit comments

Comments
 (0)