Why (North Star)
The static-data addressing / multi-segment relocation path is the clearest live counter-example to the North Star ("correctness from construction, not an ever-growing pile of locally-correct patches"). #739 → #746 → #757 → #758 are four consecutive patches to the same hand-written offset-arithmetic in main.rs (the #354 mixed-split retargeting, main.rs:3944-3976) + the selector's static-source lowering. Each fixed a locally-observed case; none foundationally verified the whole address computation.
#757 proves coverage-based validation is insufficient here. It's a real silent miscompile (gale's fused loom.wasm, confirmed byte-identical across 0.43.0/0.43.1/0.44.0/0.45.0) that survived four releases because the differential oracles only check shapes we thought to test — and 7 faithful synthetic reconstructions were all green. The bug lives in a coverage hole by construction.
The gap
- VCR-VER-002 translation-validates traps on every compilation (caught 6 latent bugs by construction).
- VCR-ISA-001 proves the 50 selector ops (generate-not-mirror Rocq).
- Neither covers the ELF relocation / segment-layout / static-address computation — still hand-written arithmetic guarded by a hand-argued (not mechanical) "SAFE-BY-CONSTRUCTION" comment.
Proposal
A per-compilation validator (ordeal/QF-BV, the VCR-VER-002 pattern) that proves: for every static memory access, the emitted relocation (symbol, addend) across N data segments correctly realizes that op's WASM linear-memory address. A wrong segment base then fails validation at compile time on the offending module itself — no need to have tested that shape. Makes the #739/#746/#757/#758 class unrepresentable.
Relation to qualification
This is the answer to "is synth qualifiable as a safety compiler despite recurring silent miscompiles": the qualification argument must be every compilation is validated against the linmem semantics (construction), not we tested many shapes (coverage — which #757 proves is holey). We have this for traps; this lane extends it to addressing.
Blocks-closure-of / regression-anchor: #757 (the immediate fix ships as v0.45.1 + gale's real loom.wasm as a permanent fixture; this lane prevents the next one).
Filed from the #757 root-cause session; North Star track B/validation. Epic #242.
Why (North Star)
The static-data addressing / multi-segment relocation path is the clearest live counter-example to the North Star ("correctness from construction, not an ever-growing pile of locally-correct patches"). #739 → #746 → #757 → #758 are four consecutive patches to the same hand-written offset-arithmetic in
main.rs(the#354mixed-split retargeting,main.rs:3944-3976) + the selector's static-source lowering. Each fixed a locally-observed case; none foundationally verified the whole address computation.#757 proves coverage-based validation is insufficient here. It's a real silent miscompile (gale's fused
loom.wasm, confirmed byte-identical across 0.43.0/0.43.1/0.44.0/0.45.0) that survived four releases because the differential oracles only check shapes we thought to test — and 7 faithful synthetic reconstructions were all green. The bug lives in a coverage hole by construction.The gap
Proposal
A per-compilation validator (ordeal/QF-BV, the VCR-VER-002 pattern) that proves: for every static memory access, the emitted relocation
(symbol, addend)across N data segments correctly realizes that op's WASM linear-memory address. A wrong segment base then fails validation at compile time on the offending module itself — no need to have tested that shape. Makes the#739/#746/#757/#758class unrepresentable.Relation to qualification
This is the answer to "is synth qualifiable as a safety compiler despite recurring silent miscompiles": the qualification argument must be every compilation is validated against the linmem semantics (construction), not we tested many shapes (coverage — which #757 proves is holey). We have this for traps; this lane extends it to addressing.
Blocks-closure-of / regression-anchor: #757 (the immediate fix ships as v0.45.1 + gale's real loom.wasm as a permanent fixture; this lane prevents the next one).
Filed from the #757 root-cause session; North Star track B/validation. Epic #242.