From 6f85147630b3ff4d34265e344d1fe82e3e387ac5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:02:50 +0200 Subject: [PATCH 01/13] fix(rivet): VCR-DEC-003 traces-to an ARTIFACT, not a GitHub issue number MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `traces-to: synth:396` was the one genuinely-ours rivet broken-link error: `synth:396` reads as "artifact 396 in repo synth", and no such artifact exists — an issue number used where an artifact id belongs. The traceability intent is preserved rather than deleted: synth#396's own body says "Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001", and VCR-COV-001's title carries "(synth #396)". So the link retargets to VCR-COV-001 (in-repo `traces-to` targets are already idiomatic in this file — VCR-SEL-001, VCR-RA-001, VCR-MEM-001, …), and `synth-396` joins the tags so the issue number stays discoverable as a reference instead of a resolvable target. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index b26214df..a7e016f8 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -2272,14 +2272,20 @@ artifacts: AArch64 carry no `branch_map`; the eliminated-constant fixture; witness#130 `object-disposition` end-to-end compose. status: implemented - tags: [witness, mcdc, traceability, provenance, vcr-dbg, decision, integration] + tags: [witness, mcdc, traceability, provenance, vcr-dbg, decision, integration, synth-396] links: - type: derives-from target: VCR-001 - type: refines target: VCR-DBG-001 + # synth#396 (the MC/DC source-to-object obligation this decision settles the + # contract for) is tracked in rivet as VCR-COV-001 — the issue body says so + # verbatim ("Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001") and + # VCR-COV-001's title carries "(synth #396)". A GitHub ISSUE NUMBER is not an + # artifact id; the link belongs on the artifact, and the issue number stays in + # the title/tags where it is a reference rather than a resolvable target. - type: traces-to - target: synth:396 + target: VCR-COV-001 - type: traces-to target: witness:130 fields: From dc9e7dde28d438979c5a6a81b666d4af02629ef8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:05:36 +0200 Subject: [PATCH 02/13] =?UTF-8?q?fix(rivet):=20GI-FPU-002=20was=20declared?= =?UTF-8?q?=20TWICE=20=E2=80=94=20the=20`proposed`=20copy=20silently=20won?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The second genuinely-ours rivet error, which the lane brief did not know about because the local grep for it (`^ ERROR:`) misses filename-prefixed diagnostics: gale-integration.yaml: ERROR: [GI-FPU-002] artifact id 'GI-FPU-002' is declared more than once: ./artifacts/verified-codegen-roadmap.yaml and ./artifacts/gale-integration.yaml — the second definition silently overwrites the first This is the #893 class one level worse than a stale description: the requirement was declared in gale-integration.yaml (`status: proposed`, the original #369 ask) and AGAIN in verified-codegen-roadmap.yaml (`status: implemented`, the phase-1 delivery record added by PR #705). rivet loaded the `proposed` copy over the `implemented` one, so the traceability graph reported GI-FPU-002 as NOT STARTED while README/CHANGELOG report #369 CLOSED, f32 complete v0.41, f64 complete v0.43, and VFP register-file spilling shipped v0.53. Resolved by MERGING, not deleting — the two copies carried disjoint edges and disjoint evidence: * Survivor: gale-integration.yaml. That is the id's namespace home (GI-002 -> GI-FPU-001 -> GI-FPU-002 -> GI-FPU-VER-001 are one chain in that file; GI-FPU-002 was the ONLY GI-* artifact in the roadmap). It also already carried `derives-from GI-002`, `traces-to gale:369`, and the jess REQ-PIX-001 / AFD-024 Pixhawk linkage — all of which a straight delete of that side would have dropped. README names the roadmap the single source of truth for the VCR-* program's roadmap status, which GI-* is not. * Folded in: the roadmap copy's six-point phase-1 DELIVERED list and its full verification-criteria (the f32_vfp_619_differential RED->GREEN evidence, the m3 honest-reject direction, the f32_hardfloat_619.rs unit lock, and the recorded unicorn VMRS FPSCR->APSR emulator gap). * De-staled, since the merge had to pick one status anyway: `proposed` -> `implemented`, with the post-phase-1 evidence the roadmap copy predated — f64 complete v0.43 (#369 closed), v0.52 #869 inline i64<->float, v0.53 #881 VFP spilling (109 rows bit-identical to wasmtime) — and the two residuals stated as loud declines rather than implied away (`f32.{ceil,floor,trunc,nearest}` pending a real VRINT.F32 after v0.54 removed the unsound saturating-VCVT pseudo-op, and `i64.trunc_sat_f32_*` on single-precision FPUs). * Where the duplicate was, the roadmap now carries a pointer comment explaining why the id is not defined there. rivet: 52 -> 50 errors; NON-EXTERNAL errors 2 -> 0. Warning/info diagnostic sets are byte-identical before/after (no new class introduced). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/gale-integration.yaml | 114 ++++++++++++++++++------ artifacts/verified-codegen-roadmap.yaml | 81 +++-------------- 2 files changed, 101 insertions(+), 94 deletions(-) diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index b2940ddf..6af0bbc5 100644 --- a/artifacts/gale-integration.yaml +++ b/artifacts/gale-integration.yaml @@ -632,29 +632,77 @@ artifacts: native_pointer_bss) stay byte-identical. A unit test asserts the FP op yields Err, not a stub. + # SINGLE DEFINITION of GI-FPU-002. Until v0.55 this id was declared TWICE — here + # (status: proposed, the original requirement) and again in + # artifacts/verified-codegen-roadmap.yaml (status: implemented, the phase-1 + # delivery record added by PR #705). rivet loaded the second over the first, so + # the graph reported GI-FPU-002 as `proposed` while README/CHANGELOG reported + # #369 CLOSED — one id meaning two things depending on which file you read. + # Resolved by merging the delivery record INTO the requirement's namespace home + # (GI-002 → GI-FPU-001 → GI-FPU-002 → GI-FPU-VER-001 all live in this file; the + # roadmap carries VCR-* program items) and leaving a pointer where the duplicate + # was. - id: GI-FPU-002 type: sw-req title: Hardware-FPU (VFP) lowering for f32/f64 on Cortex-M FPU targets (#369, REQ-PIX-001) description: > - The VFP lowering that exists (`F32Add if self.fpu.is_some() => - ArmOp::F32Add{sd,sn,sm}`, instruction_selector.rs:2769) lives in the - LEGACY `select()` function (line 1726) which NO production compile path - calls — a dead prototype. synth shall implement real hardware-FPU - lowering wired into the production `select_with_stack`: `vmov`/`vldr`/ - `vstr` to move floats between GPR/memory and VFP s/d registers, the VFP - arithmetic/compare/convert ops (`vadd/vsub/vmul/vdiv/vcvt/vcmp/vabs/ - vneg/vsqrt/...`) on s registers (f32) and d registers (f64), full op - coverage for gale's falcon mix (2044 f32 + 480 f64), correct value - semantics, and the EABI build attributes (`Tag_FP_arch`, - `Tag_ABI_VFP_args`) so the FP mode is verifiable from the artifact. - Target FPU mapping: cortex-m4f → fpv4-sp, cortex-m7 → fpv5-sp, - cortex-m7dp → fpv5-d16; soft path retained for no-FPU targets - (cortex-m3, rv32i). Multi-pass feature; behavior frozen and oracle-gated - every increment. Blocks jess REQ-PIX-001 / AFD-024 (Pixhawk 6X-RT M7 - hard-float). Supersedes the GI-FPU-001 loud-skip degradation per op as - coverage lands. - status: proposed - tags: [gale, fpu, vfp, hard-float, float, performance, pixhawk, feature, multi-pass] + ORIGINAL GAP (2026, #369): the VFP lowering that existed (`F32Add if + self.fpu.is_some() => ArmOp::F32Add{sd,sn,sm}`) lived in the LEGACY + `select()` function which NO production compile path calls — a dead + prototype. synth shall implement real hardware-FPU lowering wired into the + production `select_with_stack`: `vmov`/`vldr`/`vstr` to move floats between + GPR/memory and VFP s/d registers, the VFP arithmetic/compare/convert ops + (`vadd/vsub/vmul/vdiv/vcvt/vcmp/vabs/vneg/vsqrt/...`) on s registers (f32) + and d registers (f64), full op coverage for gale's falcon mix (2044 f32 + + 480 f64), correct value semantics, and the EABI build attributes + (`Tag_FP_arch`, `Tag_ABI_VFP_args`) so the FP mode is verifiable from the + artifact. Target FPU mapping: cortex-m4f → fpv4-sp, cortex-m7 → fpv5-sp, + cortex-m7dp → fpv5-d16; soft path retained for no-FPU targets (cortex-m3, + rv32i). Multi-pass feature; behavior frozen and oracle-gated every + increment. Blocks jess REQ-PIX-001 / AFD-024 (Pixhawk 6X-RT M7 hard-float). + Supersedes the GI-FPU-001 loud-skip degradation per op as coverage lands. + + DELIVERED — phase 1, f32 on thumb-2 (v0.41, synth #619, PR #705): + (1) Decoder un-drops the in-scope scalar f32 ops (add/sub/mul/div, the six + comparisons, i32.trunc_f32_s/u, f32.convert_i32_s/u, f32.const). + (2) A real VFP value stack in `select_with_stack`: `StackVal::Float`, an + S0..S15 allocator, and f32 arms that pop/push S-register operands. + Integer modules never construct a Float entry, so the frozen integer + path is byte-identical. + (3) AAPCS-VFP calling convention: f32 params homed in S0..S15 (threaded + `params_f32`, decoder → CompileConfig → selector), f32 result in S0. + (4) FPU gate: only FPU targets (cortex-m4f/m7/m7dp) lower f32; m0/m3/r5 + keep the honest reject with a clear GI-FPU-002 message. + (5) `.ARM.attributes`: Tag_FP_arch=VFPv4-D16 + Tag_ABI_VFP_args=VFP on FPU + targets (non-FPU byte-identical), and the reset handler enables + CP10/CP11 in SCB->CPACR (the M4F FPU is off at reset). + (6) Encoder bugs fixed: the signed/unsigned VCVT constants in + encode_{arm,thumb}_f32_convert_i32 were SWAPPED (0xEEB80A40 is U32), + silently making convert_i32_s unsigned; and the CPACR ORR mask + encoded #0x07800000 instead of #0x00F00000. + + DELIVERED SINCE — the requirement is now MET, not merely started: + * f32 complete v0.41, **f64 complete v0.43 — #369 CLOSED** (the D-register + arithmetic/compare/convert surface plus f32 load/store, local.set/tee, + and non-param float locals; the phase-1 "HELD" list below is history). + * v0.52 (#869): the eight ARM i64↔float conversions lower INLINE rather + than calling `__aeabi_*`, execution-verified over 96k checks. + * v0.53 (#881, VCR-RA-004): **VFP register-file spilling** — the falcon + v1.128 `--relocatable cortex-m7dp` exhaustion wall (`S0..S15 all live` / + `caller-saved VFP D-register file exhausted`) is gone; both files spill + and reload through the cycle-safe parallel-move resolver, and VCR-RA-003 + was extended to SEE the VFP file. 7 spilled-VFP shapes, 109 rows + bit-identical to wasmtime, NaN-aware per WASM §4.3.3. + + RESIDUALS (loud declines, never silent): `f32.{ceil,floor,trunc,nearest}` + decline on every ARM target pending a real `VRINT.F32` lowering — the legacy + pseudo-op was removed in v0.54 as unsound (it rounded via a saturating + `VCVT`); and `i64.trunc_sat_f32_*` declines on single-precision FPUs, which + needs the f64 promote. Float/SIMD cross-backend parity is separately tracked + (VCR-SEL-005 classifies it StructurallyExcluded with a written reason, + because ARM float lowering is TARGET-parameterized). + status: implemented + tags: [gale, fpu, vfp, hard-float, float, performance, pixhawk, feature, multi-pass, synth-369, synth-619, synth-881, release-v0.43, release-v0.53] links: - type: derives-from target: GI-002 @@ -664,13 +712,27 @@ artifacts: req-type: functional priority: must verification-criteria: > - falcon-v1.56.fused.wasm compiled for cortex-m7dp emits VFP - instructions (vadd/vmul/vcvt on d registers) and the ELF carries - Tag_FP_arch=fpv5-d16 / Tag_ABI_VFP_args; a numeric differential of FP - results against wasmtime matches bit-for-bit on gale's G474RE/RT1176 - re-test; cortex-m7 (sp) and cortex-m7dp (dp) outputs DIFFER (FPU mode - consulted); all frozen fixtures stay byte-identical (no float content, - unaffected); soft-float retained and unchanged for cortex-m3. + MET. Execution differential `scripts/repro/f32_vfp_619_differential.py`: + compiles f32.add/sub/mul/div + i32.trunc_f32_s + f32.convert_i32_s/u for + cortex-m4f, reads each symbol from the ELF SYMTAB (#489), runs it under + unicorn (ARM/Thumb, FPU enabled via CPACR CP10/CP11 + FPEXC.EN) with f32 + args in S0/S1 (hard-float), and asserts the result is bit-exact + (`to_bits`) vs wasmtime on boundary values (0.0, 1.5, -2.25, large, + subnormal) — RED on the pre-#705 tree (compile REJECTS → exit 1), GREEN + after (48/48 → exit 0). The same harness asserts cortex-m3 REJECTS f32 + (honest-reject direction). `crates/synth-backend/tests/f32_hardfloat_619.rs` + locks the AAPCS-VFP S0/S1 homing, the honest reject, and the + convert-signedness fix without unicorn. The ELF carries + Tag_FP_arch/Tag_ABI_VFP_args, and cortex-m7 (sp) vs cortex-m7dp (dp) + outputs DIFFER (FPU mode consulted). v0.53's spilled-VFP differential + (7 shapes, 109 rows bit-identical to wasmtime on `-t cortex-m7dp + --relocatable`, internal `bl` resolved by a REAL link so an unresolved + relocation cannot be silently skipped) closes the falcon exhaustion + criterion. Frozen anchors 10/10 and the #511 estimator oracle pass + untouched; soft-float retained and unchanged for cortex-m3. NOT + execution-differentiated: the f32 comparisons are byte-pinned in + f32_vfp_encoding_test.rs but unicorn does not model the VMRS FPSCR→APSR + flag transfer (an emulator gap, recorded not hidden). - id: GI-FPU-VER-001 type: sw-verification diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index a7e016f8..63ab68c3 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -3479,76 +3479,21 @@ artifacts: (frozen anchors pass untouched). # --------------------------------------------------------------------------- - # Scalar f32 hard-float reachability (GI-FPU-002, #619/#369) + # Scalar f32 hard-float (GI-FPU-002) — NOT DEFINED HERE. + # + # PR #705 recorded the phase-1 f32 delivery by declaring a SECOND `GI-FPU-002` + # artifact at this point in the file. The id was already defined in + # artifacts/gale-integration.yaml (its namespace home — GI-002 -> GI-FPU-001 -> + # GI-FPU-002 -> GI-FPU-VER-001 form one chain there), so rivet loaded one over + # the other and reported `status: proposed` for a requirement the README and + # CHANGELOG both report as met (#369 closed, f32 v0.41 / f64 v0.43, VFP + # spilling v0.53). This file is the single source of truth for the VCR-* + # program's roadmap status, not for the GI-* gale-integration requirements. + # + # The delivery evidence was merged into the single GI-FPU-002 in + # artifacts/gale-integration.yaml, which now carries `status: implemented`. # --------------------------------------------------------------------------- - - id: GI-FPU-002 - type: sw-req - title: "Scalar f32 hard-float (VFP) reachable on the thumb-2 CLI path — phase 1 (synth #619/#369)" - description: > - synth had a working VFP encoder (f32_vfp_encoding_test.rs) and selector - VFP arms, but the decoder DROPPED every scalar float op - (wasm_decoder.rs `_ => None`), so `synth compile -t cortex-m4f` - HONEST-REJECTED f32 on every CLI path (GI-FPU-001 loud-skip). Worse, the - "existing" selector VFP lowering was a NON-FUNCTIONAL prototype: the - direct `select_with_stack` fell through to `select_default`, whose - `alloc_vfp_reg` is a blind `%16` round-robin with no operand-stack - integration, so `f32.const;f32.const;f32.add` emitted `VADD S2,S3,S4` over - garbage. Phase 1 builds the real bridge. - - DELIVERED (phase 1, implemented): - (1) Decoder un-drops the in-scope scalar f32 ops (add/sub/mul/div, the - six comparisons, i32.trunc_f32_s/u, f32.convert_i32_s/u, f32.const); - f64 and the rest of the f32 surface (abs/neg/sqrt/min/max, load/store, - local.set/tee) stay dropped → phase 1b/2. - (2) A real VFP value stack in `select_with_stack`: `StackVal::Float`, - an S0..S15 allocator (no VFP spilling — loud-bail on exhaustion), - and f32 arms that pop/push S-register operands. Integer modules never - construct a Float entry, so the frozen integer path is byte-identical. - (3) AAPCS-VFP calling convention: f32 params homed in S0..S15 (threaded - `params_f32`, decoder → CompileConfig → selector), f32 result in S0. - (4) FPU gate: only FPU targets (cortex-m4f/m7/m7dp) lower f32; m0/m3/r5 - keep the honest reject with a clear GI-FPU-002 message. - (5) `.ARM.attributes`: Tag_FP_arch=VFPv4-D16 + Tag_ABI_VFP_args=VFP - registers on FPU targets (non-FPU byte-identical), and the reset - handler enables CP10/CP11 in SCB->CPACR (the M4F FPU is off at reset). - (6) Encoder bug fixed: the signed/unsigned VCVT constants in - encode_{arm,thumb}_f32_convert_i32 were SWAPPED (0xEEB80A40 is U32), - silently making convert_i32_s an unsigned conversion; and the CPACR - ORR mask (main.rs / cortex_m.rs) encoded #0x07800000 instead of - #0x00F00000. Both corrected. - - HELD (honest-subset boundary, chosen not missed): f64 (phase 2 — M7DP - D-registers), f32 load/store (VLDR/VSTR address materialization — 1b), - f32 local.set/tee and non-param f32 locals (VFP home write-back — 1b), - mixed f32/integer parameter lists and f32-in-functions-with-calls (both - loud-decline: AAPCS-VFP independent register pools / S0..S15 caller-saved). - status: implemented - tags: [codegen, f32, vfp, hard-float, aapcs-vfp, cortex-m4f, decoder, selector, synth-619, synth-369, gi-fpu-002] - links: - - type: derives-from - target: VCR-001 - fields: - req-type: functional - priority: should - verification-criteria: > - Tracks GitHub issues #619 / #369. RED→GREEN execution differential - (scripts/repro/f32_vfp_619_differential.py): compiles f32.add/sub/mul/div - + i32.trunc_f32_s + f32.convert_i32_s/u for cortex-m4f, reads each symbol - from the ELF SYMTAB (#489), runs it under unicorn (ARM/Thumb, FPU enabled - via CPACR CP10/CP11 + FPEXC.EN) with f32 args in S0/S1 (hard-float), and - asserts the result is bit-exact (`to_bits`) vs wasmtime on boundary - values (0.0, 1.5, -2.25, large, subnormal). RED on origin/main (compile - REJECTS → exit 1); GREEN after (48/48 bit-exact → exit 0). Honest-reject: - the same harness asserts cortex-m3 REJECTS f32. CI-gateable Rust test - crates/synth-backend/tests/f32_hardfloat_619.rs locks the AAPCS-VFP S0/S1 - homing, the honest reject, and the convert-signedness fix without - unicorn. Frozen anchors 10/10 and the #511 estimator oracle pass - untouched (float declines the optimized path → the estimator never sees - VFP ops). The f32 comparisons compile + are byte-pinned in - f32_vfp_encoding_test.rs but are not execution-differentiated (unicorn - does not model the VMRS FPSCR→APSR flag transfer — an emulator gap). - # --------------------------------------------------------------------------- # Track D — schedulability: sound static WCET bound (#778) # --------------------------------------------------------------------------- From 911ded9b621195ffab2bc93e95bb38ebd555acff Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:08:22 +0200 Subject: [PATCH 03/13] fix(#893): VCR-RA-004 was `proposed` for a resolver that shipped in v0.11.38 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Half of #893: v0.53's VFP-spilling lane tagged its work `VCR-RA-004`, while artifacts/verified-codegen-roadmap.yaml still carried that id as `status: proposed`. The brief offered two resolutions — mint a new id for the v0.53 work, or flip VCR-RA-004 to implemented. The evidence decides it, and it is neither of the two things the ID-collision framing suggested: the resolver VCR-RA-004 describes shipped in **v0.11.38**, three years of releases before the lane that got blamed for overloading the id. `synth_synthesis::parallel_move` is verbatim what the artifact asks for — a pure, testable component that sequentializes a parallel move set with cycle detection, scratch selection from dead registers, and a guaranteed-progress fallback. The artifact's own tags already said `release-v0.11.38`; the CHANGELOG names it twice (v0.11.38 "Cycle-safe parallel-move resolver (`synth_synthesis::parallel_move`, VCR-RA-004)" and v0.11.39 "#327 — VCR-RA-004's resolver (v0.11.38) breaks cycles via a stack-scratch cell"). Only the status field was never flipped. Minting a second id would have created the collision the issue was trying to remove. So: `proposed` -> `implemented`, with the evidence written down instead of left in changelog prose — * the algorithm and its progress discipline (the size bound and the strictly-shrinking pending set are `assert!`s in the resolver, so an unbounded path aborts rather than emitting); * both consumers, each of which removed a real defect rather than only adding a component: v0.11.39 #327 arg-move marshalling (the old cycle-breaker demanded a callee-saved register AND miscompiled genuine 2-swaps by duplicating a value), and v0.53 #881 VFP register-file spilling (the falcon `S0..S15 all live` wall) — which is precisely the work the v0.53 notes tagged VCR-RA-004; * SWVER-022, a new sw-verification artifact linking `verifies` -> VCR-RA-004, so the right side of the V is closed by a typed link rather than by a paragraph. It records the run recipe and what each of the three criteria clauses is actually met by. `implemented`, NOT `verified`, deliberately. The property test the criteria demand does exist and does exactly what they specify — 2000 iterations over R0..R8 alternating full random permutations with partial move sets, each re-checked at scratch-set sizes 0/1/2 (6000 sequentializations) against a reference parallel semantics, plus 12 directed shape tests — verified locally, `cargo test -p synth-synthesis parallel_move` 13/13, real exit 0. But the second pitfall the artifact names, split points landing inside hot loops, is still bounded by ASSUMPTION (synth's straight-line segment scope) rather than by a check that fails when segments widen. That residual is now stated in both the requirement and SWVER-022 rather than implied away. rivet: non-external errors still 0; warnings 104 -> 103 (VCR-RA-004's "should be verified by at least one verification measure" WARN closed, no new warning introduced). claim_check 37/37. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/sw-verification.yaml | 48 +++++++++++++++++ artifacts/verified-codegen-roadmap.yaml | 71 ++++++++++++++++++++++++- 2 files changed, 117 insertions(+), 2 deletions(-) diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 1aa0cf09..2fa882a5 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -533,3 +533,51 @@ artifacts: via pop2_i64 / VI64) + coq/Synth/WASM/WasmCertBridge.v (six i64_*_exec_refines_wasmcert theorems, +6 Qed → 591 total); frozen 10/10 confirms the semantics-model change does not alter compiled bytes + + # --------------------------------------------------------------------------- + # Track A right-side closure (#893): VCR-RA-004 shipped in v0.11.38 and was + # extended to the VFP file in v0.53, but nothing linked `verifies` to it, so + # the requirement's evidence lived only in changelog prose. + # --------------------------------------------------------------------------- + + - id: SWVER-022 + type: sw-verification + title: Cycle-safe parallel-move resolver — property test + over-pressure differentials (VCR-RA-004) + description: > + Verifies VCR-RA-004's three criteria clauses. (1) PROPERTY: + `property_random_move_sets_match_parallel_semantics` sequentializes 2000 + deterministic move sets over R0..R8 — alternating full random permutations + (guaranteeing cycles and self-moves) with partial sets (chains, fan-out, + self-moves, cycles) — each re-checked with scratch sets of size 0, 1 and 2, + i.e. 6000 sequentializations, every one compared against a reference + PARALLEL semantics (all sources read in the old state) and against the + `moves.len() + 2 * cycle_count` size bound. Twelve directed tests pin the + named shapes (two_swap, three_cycle, two_disjoint_cycles, chain_into_cycle, + scratch-collision filtering, the no-scratch stack-scratch pair, and the + rejected duplicate-destination caller bug). (2) EXECUTION: the resolver's + two consumers are differentiated against wasmtime — `high_pressure_i32.wat` + (hard `Err` before v0.11.38, 6/6 after) for the integer arg-move path, and + the v0.53 #881 spilled-VFP differential (7 shapes on `-t cortex-m7dp + --relocatable`, 109 rows bit-identical, NaN-aware per WASM §4.3.3, internal + `bl` resolved by a real link) for the VFP file. (3) PROGRESS: the size bound + and the strictly-shrinking pending set are `assert!`s inside + `sequentialize`, so an unbounded path aborts rather than emitting — checked + by construction, not by sampling. HONEST BOUND: the "split points inside hot + loops" pitfall named in VCR-RA-004 is bounded by synth's straight-line + segment scope and has NO check of its own; widening segments must add one. + status: implemented + tags: [register-allocation, parallel-move, spilling, property-test, differential, vcr-ra, epic-242, synth-893] + links: + - type: verifies + target: VCR-RA-004 + fields: + method: automated-test + steps: + run: "cargo test -p synth-synthesis parallel_move" + coverage: > + crates/synth-synthesis/src/parallel_move.rs (the property test + 12 + directed cases) and its consumers + `InstructionSelector::emit_arg_moves` (#327) and the v0.53 VFP + spill/reload insertion (#881); execution evidence via + scripts/repro/high_pressure_i32.wat and the #881 spilled-VFP + differential diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 63ab68c3..21026c50 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -2080,8 +2080,49 @@ artifacts: named pitfall — split points landing inside hot loops — is bounded at this stage by synth's straight-line segment scope (no interior loops), and re-checked when segments widen. - status: proposed - tags: [codegen, register-allocation, parallel-move, spilling, track-a, release-v0.11.38] + + DELIVERED v0.11.38 — `synth_synthesis::parallel_move` (`sequentialize`), + a pure module with no compiler state: destinations must be pairwise + distinct (anything else is a caller bug and is REJECTED, not guessed at); + self-moves are dropped; phase 1 emits chain moves leaf-first from a + worklist until what remains is exactly a set of disjoint cycles; phase 2 + breaks each cycle through a scratch register filtered against the move set, + or — when no scratch survives the filter — through ONE self-bracketing + stack-scratch pair (`MoveStep::SpillScratch` / `ReloadScratch`, lowered by + the consumer to `str`/`ldr [sp, #resolver_slot]`). That stack fallback is + the "guaranteed-progress" clause: there is no fixpoint-and-hope loop — + phase 1 removes exactly one pending move per pop, the phase-2 walk removes + one per step against the disjoint-cycle invariant, the outer loop ASSERTS + the pending set strictly shrank, and the emitted sequence is asserted + bounded by `moves.len() + 2 * cycle_count` before returning. + + CONSUMED, twice, and each time it removed a real defect rather than only + adding a component: + * v0.11.39 (#327, gale #326): `emit_arg_moves` call-marshalling. The old + cycle-breaker DEMANDED a callee-saved register, so the dissolved + k_mutex_unlock hard-failed under saturation; it also MISCOMPILED + genuine 2-swaps (duplicated a value). Phase 1 emits the + lowest-destination ready move first — exactly the order the legacy + `emit_parallel_move` produced for ascending-destination arg lists — so + wiring the resolver in was byte-invisible for everything that already + compiled. + * v0.53 (#881, GI-FPU-002): VFP register-file spilling. `VCR-RA-001` + gave the INTEGER file Belady spilling in v0.24 but the VFP file never + got it, so five falcon v1.128 entry points died on `S0..S15 all live` + / `caller-saved VFP D-register file exhausted`. Both files now spill + and reload, and the swap/cycle cases go through THIS resolver. This is + the delivery the v0.53 notes tagged `VCR-RA-004`; the status field is + what had not been flipped (#893). + + STATUS IS `implemented`, NOT `verified`, deliberately. All three + verification-criteria clauses have evidence (below), but no `sw-verification` + artifact linked `verifies` to this requirement until v0.55 (#893), and the + second named pitfall — split points landing inside hot loops — is still + bounded by assumption (synth's straight-line segment scope, no interior + loops) rather than by a check that fails when segments widen. That + re-check remains open and is stated here rather than implied away. + status: implemented + tags: [codegen, register-allocation, parallel-move, spilling, track-a, release-v0.11.38, release-v0.53, synth-327, synth-881, synth-893] links: - type: derives-from target: VCR-001 @@ -2098,6 +2139,32 @@ artifacts: result-identical to wasmtime; no resolver path can emit an unbounded-progress sequence. + MET, clause by clause — the linked verification artifact carries the run + recipe and the honest bound: + (1) `property_random_move_sets_match_parallel_semantics` + (crates/synth-synthesis/src/parallel_move.rs) runs 2000 deterministic + iterations over R0..R8 — alternating a FULL random permutation + (guaranteeing cycles and self-moves) with a partial move set (chains, + fan-out, self-moves, cycles) — and re-runs each against scratch sets of + size 0, 1 and 2, i.e. 6000 sequentializations, each checked against a + reference parallel semantics and against the size bound. Twelve directed + cases cover the named shapes explicitly (two_swap, three_cycle, + two_disjoint_cycles, chain_into_cycle, the scratch-collision filter, and + the no-scratch stack pair). + (2) `scripts/repro/high_pressure_i32.wat` + its unicorn-vs-wasmtime + differential: hard `Err` on v0.11.37, 6/6 on v0.11.38. v0.53 (#881) adds + the spilled-VFP differential — 7 shapes on `-t cortex-m7dp + --relocatable`, 109 rows bit-identical to wasmtime, NaN-aware per WASM + §4.3.3, with the internal `bl` resolved by a REAL link so an unresolved + relocation cannot be silently skipped. + (3) Unbounded progress is excluded structurally, not empirically: the + `moves.len() + 2 * cycle_count` bound and the strictly-shrinking pending + set are `assert!`s in the resolver itself, so a violating path aborts + rather than emitting. + OPEN: the "split points inside hot loops" pitfall is still bounded by + synth's straight-line segment scope, and the re-check owed when segments + widen does not exist yet. + - id: VCR-DEC-001 type: sw-req title: "Decision: Chaitin/Briggs colouring over backtracking-bundle allocation — rationale + revisit trigger" From 9bab337d4248e6514e544f678ab5458a7fedb959 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:11:49 +0200 Subject: [PATCH 04/13] fix(#893): VCR-SEL-005 spans THREE backends, and both ledger counts had drifted MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second half of #893. VCR-SEL-005's description still said the gate lowers probes on "BOTH the ARM (Thumb-2) and RISC-V (RV32IMAC) selectors" — it has covered a third, aarch64, since v0.53 (#883). SWVER-017, the verification artifact that is supposed to be the right-side evidence for exactly this requirement, carried the same claim in its title ("ARM vs RISC-V") and described a two-selector ledger. While correcting the backend count I checked the numbers the same documents assert, and both were stale in the same direction — they described gaps that have since CLOSED, which is the flattering direction and therefore the one worth checking: * The roadmap said "the KNOWN_DIVERGENCES ledger is now 5 Zbb + 16 new = 21 entries". The array holds 18: `memory.size`/`memory.grow` closed in v0.50 and `br_table` in v0.53 (#882). * `known_divergences`'s own doc comment said 19 (it had accounted for v0.50 but not #882). * `aarch64_known_divergences`'s doc comment said "leaving the SEVEN below" over an array of 5 — v0.54 (#899) closed `global.get`/`global.set` and removed the entries without updating the prose above them. All four now state what the arrays hold, with the counts' derivation written out so the next drift is visible, and a note at each site that the count must move with the array. The stale-entry check already forces a CLOSED gap to retire its ledger line; nothing forced the PROSE ABOUT the ledger to move with it, which is the #893 defect one layer up. Also recorded, because it is the part of the third-backend leg that is not just "one more backend": aarch64 gets a probed FLOAT/SIMD surface (`a64_extended_surface`, floor `probed >= 100`) that ARM and RV32 structurally cannot have — float is `StructurallyExcluded` from their leg because ARM float lowering is TARGET-parameterized (f32.add declines at fpu=None, lowers at Single/Double) and RV32 has no FPU, whereas the aarch64 backend has one fixed host profile, so both directions are assertable and a stale gap-claim is caught the same way a stale divergence is. Changes are prose and doc-comment only — no test logic touched. `cargo test -p synth-backend-riscv --test cross_backend_op_parity` 8/8, real exit 0. rivet non-external errors still 0; claim_check 37/37. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/sw-verification.yaml | 32 ++++++-- artifacts/verified-codegen-roadmap.yaml | 77 +++++++++++++++---- .../tests/cross_backend_op_parity.rs | 20 +++-- 3 files changed, 100 insertions(+), 29 deletions(-) diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 2fa882a5..6a21dd6a 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -387,15 +387,29 @@ artifacts: - id: SWVER-017 type: sw-verification - title: Cross-backend op-parity oracle (ARM vs RISC-V) + title: Cross-backend op-parity oracle (ARM vs RISC-V vs AArch64) description: > Verifies the VCR-SEL-005 op-parity oracle: the ledger of which WasmOps - each selector (ARM select_default, RISC-V selector) lowers, asserting the - tracked parity so a "selector missed an op" regression (the #223/#232 - class) is caught mechanically rather than on silicon. Both selectors fail - honestly on an unlowered op; this oracle tracks the gap explicitly. + each selector lowers, asserting the tracked parity so a "selector missed + an op" regression (the #223/#232 class) is caught mechanically rather than + on silicon. Every selector fails honestly on an unlowered op; this oracle + tracks the gap explicitly, in both directions (a NEW unledgered gap + reddens, and so does a ledgered gap that has CLOSED). + + THREE selectors, not two — the title said "ARM vs RISC-V" until v0.55 + (#893), but aarch64 joined the same no-wildcard universe enumeration in + v0.53 (#883). The gate is now eight tests: the RV32 parity leg + (cross_backend_integer_op_parity_242), the aarch64 parity leg + (aarch64_integer_op_parity_851), the aarch64 float/SIMD extended surface + (aarch64_extended_surface_851 — probe-able there because the backend has + one fixed host profile, whereas ARM float lowering is TARGET-parameterized + and RV32 has no FPU), the #882 br_table sub-shape asymmetry check, a + ledger-liveness test per leg, and a red-first non-vacuity companion per leg + that removes a REAL ledger entry (i32.rotl / an aarch64 gap) and asserts + the gate goes red on the real backends — no synthetic op, no shipping-code + change. status: implemented - tags: [instruction-selection, cross-backend, vcr-sel, op-parity] + tags: [instruction-selection, cross-backend, aarch64, vcr-sel, op-parity, synth-883, synth-893] links: - type: verifies target: VCR-SEL-005 @@ -405,7 +419,11 @@ artifacts: run: "cargo test -p synth-backend-riscv --test cross_backend_op_parity" coverage: > crates/synth-backend-riscv/tests/cross_backend_op_parity.rs — the - ARM/RISC-V op-lowering parity ledger + ARM/RISC-V and ARM/AArch64 op-lowering parity ledgers (18 and 5 entries + respectively as of 2026-08) plus the aarch64 extended float/SIMD + surface; non-vacuity floors at_parity >= 65 (RV32), >= 60 (aarch64), + probed >= 100 (aarch64 extended). CI job + vcr-sel-005-cross-backend-op-parity-gate # Native-pointer ABI verification cluster (#237/#354/#359/#383): completes the # right side of the V for the native-pointer linear-memory family alongside diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 21026c50..287af417 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -505,14 +505,18 @@ artifacts: - id: VCR-SEL-005 type: sw-req - title: Cross-backend op-parity oracle + title: Cross-backend op-parity oracle (ARM / RISC-V / AArch64) description: > - A test-time gate (crates/synth-backend-riscv/tests/cross_backend_op_parity.rs, - cross_backend_integer_op_parity_242) that lowers a curated set of - self-contained, minimally-valid WasmOp sequences on BOTH the ARM (Thumb-2) - and RISC-V (RV32IMAC) selectors and asserts integer-core PARITY: an op the - ARM selector lowers must be lowered-or-explicitly-ledgered by the RV32 - selector. This is the concrete near-term increment of VCR-SEL-001: the + A test-time gate (crates/synth-backend-riscv/tests/cross_backend_op_parity.rs) + that lowers self-contained, minimally-valid WasmOp sequences on ALL THREE + shipping selectors — ARM (Thumb-2), RISC-V (RV32IMAC) and AArch64 (A64) — + and asserts integer-core PARITY against ARM as the reference: an op the ARM + selector lowers must be lowered-or-explicitly-ledgered by the RV32 selector + (`cross_backend_integer_op_parity_242`) and by the aarch64 selector + (`aarch64_integer_op_parity_851`). NOTE the backend count: this description + said "BOTH the ARM and RISC-V selectors" until v0.55 (#893) — it has spanned + three backends since v0.53 (#883). This is the concrete near-term increment + of VCR-SEL-001: the VCR-SEL-001 pilot measurement (2026-06-20) established that "selector missed an op" is no longer a silent miscompile (ARM select_default is an exhaustive WasmOp match; RV32 ends dispatch with a typed Unsupported Err), so the @@ -592,8 +596,40 @@ artifacts: also covers globals, the memory intrinsics (size/grow/copy/fill), br_table, and the sub-word i64 memory variants — each landing retires its ledger line via the stale-entry check. + + THIRD BACKEND (v0.53, #883/#851): aarch64 joined the same no-wildcard + enumeration. Before that its only breadth check was 25 hand-written probes, + so "what does aarch64 not lower?" had no mechanical answer and gap-picking + was guesswork. The aarch64 leg (`aarch64_integer_op_parity_851`, ledger + `aarch64_known_divergences`) enumerated TWENTY ARM-lowers/aarch64-declines + integer-core gaps on first run; each decline names the missing selector arm + AND the A64 instruction that would implement it, so the ledger reads as a + work plan rather than an absence. Thirteen closed in the same release + (`select` via CSEL/FCSEL, `drop`/`nop`, `i32.wrap_i64`, + `i64.extend_i32_{s,u}`, the five `extend8/16/32_s` forms, fixed-memory + `memory.size`/`memory.grow` — selector 148 -> 161 ops, gale's matrix 35 -> + 45); v0.54 closed `global.get`/`global.set`. aarch64 also gets what ARM and + RV32 structurally cannot have: a probed FLOAT/SIMD surface + (`a64_extended_surface`, floor `probed >= 100`). Float is + `StructurallyExcluded` from the ARM/RV32 leg because ARM float lowering is + TARGET-parameterized (f32.add DECLINES at fpu=None, LOWERS at + Single/Double) and RV32 has no FPU — but the aarch64 backend has ONE fixed + host profile, so both directions are assertable there, and a stale "gap" + claim is caught the same way a stale divergence is. + + LEDGER STATE (2026-08, keep in step with the arrays — a drifting count is + the #893 class this oracle exists to prevent): ARM<->RV32 18 entries + (5 Zbb + 16 universe-completeness − `memory.size`/`memory.grow` closed + v0.50 − `br_table` closed v0.53 #882); ARM<->aarch64 5 entries (br_table, + writing a PARAM local via local.set/local.tee in a leaf function, + memory.copy, memory.fill). Non-vacuity floors: `at_parity >= 65` (RV32), + `at_parity >= 60` (aarch64), `probed >= 100` (aarch64 extended surface). + Both legs carry their own red-first companion + (`red_first_unledgered_one_sided_gap_is_caught` drops the real i32.rotl + entry; `red_first_unledgered_aarch64_gap_is_caught` does the same on the + aarch64 leg) and their own ledger-liveness test. status: implemented - tags: [codegen, selector, riscv, parity, oracle, track-a, release-v0.11.51] + tags: [codegen, selector, riscv, aarch64, parity, oracle, track-a, release-v0.11.51, release-v0.53, synth-883, synth-893] links: - type: derives-from target: VCR-001 @@ -603,15 +639,22 @@ artifacts: req-type: functional priority: should verification-criteria: > - cross_backend_integer_op_parity_242 is green: every WasmOp variant is - classified by a no-wildcard match (universe-complete by construction), and - every integer-core probe is at ARM/RV32 parity OR carries a reasoned - KNOWN_DIVERGENCES entry, with the at-parity floor (>=65 common-core ops) - guarding against a construction regression that would let "everything - errors" masquerade as parity. The red-first companion - (red_first_unledgered_one_sided_gap_is_caught) proves non-vacuity by - surfacing the real i32.rotl gap once its ledger entry is removed, and the - gate is CI-wired as vcr-sel-005-cross-backend-op-parity-gate. + All EIGHT tests in cross_backend_op_parity.rs are green: every WasmOp + variant is classified by a no-wildcard match (universe-complete by + construction — a new variant fails to COMPILE until classified, the #615 + tripwire), and every integer-core probe is at parity with ARM on BOTH the + RV32 and the aarch64 leg OR carries a reasoned ledger entry. The + at-parity floors (>=65 RV32, >=60 aarch64 common-core ops; >=100 probed + on the aarch64 extended float/SIMD surface) guard against a construction + regression that would let "everything errors" masquerade as parity. Each + leg carries its own red-first companion proving non-vacuity on the REAL + backends — red_first_unledgered_one_sided_gap_is_caught surfaces the real + i32.rotl gap once its ledger entry is removed, and + red_first_unledgered_aarch64_gap_is_caught does the same for aarch64 — and + a ledger-liveness test per leg guards drift. Stale entries fail too, in + both directions: a divergence that has CLOSED reddens the gate until its + line is deleted, so a parity claim cannot outlive the gap it documents. + CI-wired as vcr-sel-005-cross-backend-op-parity-gate. # --------------------------------------------------------------------------- # Track B — authoritative semantics (independent; parallel with Track A) diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index 30b79449..3be37ec3 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -777,8 +777,16 @@ fn all_wasm_op_representatives() -> Vec { /// CLOSED v0.50 (#242): `memory.size` + `memory.grow` now lower on RV32 /// (fixed-memory page-count constant + fixed-memory `-1` grow, shared /// `rewrite_memory_grow_zero` fold; execution differential -/// `rv32_mem_size_grow_242_differential.py`). Ledger total: 5 Zbb + 16 − -/// 2 closed = 19 entries. +/// `rv32_mem_size_grow_242_differential.py`). +/// +/// CLOSED v0.53 (#882): `br_table` now lowers on RV32 (comparison ladder, +/// execution-verified under unicorn vs wasmtime across every table entry and +/// the out-of-range / unsigned-edge indices; oversized and value-carrying +/// tables LOUD-DECLINE by name rather than miscompiling). +/// +/// Ledger total: 5 Zbb + 16 − 3 closed = **18 entries** — the number below. +/// Keep this line in step with the array: a count that drifts from the array is +/// exactly the stale-claim class this ledger exists to prevent (#893). fn known_divergences() -> &'static [(&'static str, &'static str)] { &[ // ---- Zbb bit-manipulation class (measured 2026-06-20) ---- @@ -915,9 +923,11 @@ fn known_divergences() -> &'static [(&'static str, &'static str)] { /// Thirteen were closed in the same change (v0.53 #851: `select` via /// CSEL/FCSEL, `drop`, `nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, the five /// `extend8/16/32_s` forms, fixed-memory `memory.size`/`memory.grow`), leaving -/// the SEVEN below. This ledger — the COMPLEMENT of what aarch64 lowers — is -/// the mechanically-derived answer to "what is missing on armv8?" (#851); the -/// float-surface complement lives in [`a64_extended_surface`]. +/// seven. v0.54 (#851 lane L3) closed two more — `global.get`/`global.set` — +/// leaving the **FIVE** below. This ledger — the COMPLEMENT of what aarch64 +/// lowers — is the mechanically-derived answer to "what is missing on armv8?" +/// (#851); the float-surface complement lives in [`a64_extended_surface`]. +/// Keep this count in step with the array (#893). fn aarch64_known_divergences() -> &'static [(&'static str, &'static str)] { &[ ( From 7579bf5d205aff87788e1cce1963ca972a4f82de Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:14:48 +0200 Subject: [PATCH 05/13] =?UTF-8?q?docs(roadmap):=20file=20VCR-VER-004=20?= =?UTF-8?q?=E2=80=94=20a=20shipped=20North-Star=20component=20had=20NO=20r?= =?UTF-8?q?oadmap=20entry?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit README calls artifacts/verified-codegen-roadmap.yaml "the single source of truth for roadmap status". VCR-VER-004 shipped in v0.54 and appeared in the CHANGELOG, the FEATURE_MATRIX template and the CI job list — but the roadmap had no entry for it at all, so the one document the README points at for "what is the state of the VCR-* program" was missing the release's headline validator. The entry records what it is and, more importantly, why it exists: v0.53 showed by mutation that emptying `cfg_exit_observable` makes the compiler leave a return value in the WRONG REGISTER and that BOTH per-compilation validators accept it (`validate_cfg_rewrite` -> Ok, VCR-RA-003 -> Consistent). Only execution caught it. `abi_contract::validate_abi_contract` is not a third file on the same axis — it differs on four axes (an obligation that cannot be emptied because it is `RETURN_CONTRACT_REGS = [R0, R1]` hard-named in its own source; forward rather than backward, so there is no seed whose empty set is a vacuous fixpoint; evidence that is a VALUE compared by greatest-fixpoint bisimulation rather than a name-pair; and a `(orig, rewritten)` signature that takes nothing from the pass). Its honest limit is in the entry, not implied away — all three residuals: (a) it GATES only the flag-off colouring allocator; on the default path it is a report-only audit held to a `Violated 0` CI floor, because gating a user's compile on a checker whose false-positive rate is measured rather than proven is a flip we have deliberately not taken; (b) memory is NOT in its obligation (complementary to `validate_cfg_rewrite`, not redundant with it); (c) THE OP MODEL IS STILL SHARED — def/use extraction runs through `liveness::reg_effect`, so a mismodeled op is a blind spot common to all three instruments. VCR-VER-004 closes the shared-CONTRACT hole, not the shared-OP-MODEL hole, and until `synth-verify`'s `ArmSemantics::encode_op` is pinned against it (VCR-ISA-001's Sail-derived semantics being the eventual anchor, now a typed `traces-to` link rather than a prose aside) "three independent validators" WOULD BE AN OVERCLAIM. Shaped to match its two siblings VCR-VER-003 / VCR-VER-761 exactly: `sys-verification`, `verifies -> VCR-001`, `method: translation-validation`, `preconditions`/`steps`/`pass-criteria`. That inherits two diagnostics those siblings already carry (the schema's `method` allowed-values does not list `translation-validation`, and `pass-criteria` is not a declared sys-verification field) — kept deliberately, because the fix for those is a rivet schema decision about the whole family, not a divergent shape for one member. rivet: 50 errors, non-external 0 (unchanged). Warnings 103 -> 105; the delta is exactly the three new-artifact diagnostics above, and the diagnostic-class diff against the lane's baseline shows no new KIND. claim_check 37/37. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 130 ++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 287af417..a7c69b62 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1501,6 +1501,136 @@ artifacts: full-boot oracle green); AArch64 is documented N/A (no linear-memory ops in the subset). + - id: VCR-VER-004 + type: sys-verification + title: "ABI observable-contract validator: a per-compilation check that fails DIFFERENTLY from the two dataflow validators that shared a blind spot (#242)" + description: > + SHIPPED v0.54. Filed into this roadmap in v0.55 (#893) — it was absent + entirely, which README calls out as a real gap because this file is + "the single source of truth for roadmap status" and VCR-VER-004 is a + shipped North-Star component. + + THE MEASUREMENT THAT MOTIVATES IT (v0.53). Emptying `cfg_exit_observable` + — the exit contract the join-aware graph allocator and its OWN CFG + validator SHARE — makes the compiler emit code that leaves the return + value in the WRONG REGISTER, and BOTH per-compilation validators accept + it: `validate_cfg_rewrite` returns `Ok` and VCR-RA-003's + `validate_final_allocation` returns `Consistent`. Only EXECUTION caught + it. Two independent-LOOKING instruments, one shared blind spot — #872's + lesson one level up, and a direct counterexample to the claim that + per-compilation validation is an independent check on the code generator. + + THE RESPONSE IS NOT A THIRD FILE ON THE SAME AXIS. Independence is not + obtained by writing a second checker, only by checking a different WAY. + `synth_synthesis::abi_contract::validate_abi_contract` differs on four + axes that matter: + (1) ITS OBLIGATION CANNOT BE EMPTIED. The exit obligation is + `RETURN_CONTRACT_REGS = [R0, R1]`, a constant of the AAPCS hard-named + in the module's own source. Deleting `cfg_exit_observable` outright + would not change one line of it. + (2) IT IS FORWARD, and a forward value analysis is structurally + incapable of the fail-open mode that bit v0.53. + `validate_cfg_rewrite` is a BACKWARD MUST-analysis whose obligation + set is a VARIABLE — and the empty set is a fixpoint, so an empty + seed means zero obligations means vacuous green. A forward + evaluation always produces EXACTLY ONE value for `R0` at each + return. There is no seed to shrink. + (3) ITS EVIDENCE IS A VALUE, NOT A NAME-PAIR. Per side independently it + builds a value graph (`Init(r)` / `Def(i,k)` / `Phi(b,n)`) and + compares by GREATEST-FIXPOINT BISIMULATION; on a deterministic term + graph that is equality of the infinite unfoldings, so loops and back + edges are handled coinductively rather than by unrolling. `Init(r)` + is one node SHARED by both sides — the AAPCS PARAMETER half of the + anchor — so reading an argument out of the wrong register is a value + change too. + (4) IT TAKES NOTHING FROM THE PASS. The signature is + `(orig, rewritten)`; the CFG is re-derived from both streams' + label-form branch structure and the two must agree. The v0.50 join + attempt failed precisely by letting the pass hand the checker its own + seed. + + CALLS ARE MODELLED, NOT EXEMPTED. Each clobbered register + `{R0-R3, R12, LR}` is rebound to a FRESH node whose operands are the + PRE-CALL argument values, while `R4-R11`/`SP` flow through — so a call + result is an opaque value equal across the sides exactly when the same + callee got the same arguments. The AAPCS call effect reuses + `liveness::call_effect`, the ONE definition the pass and + `validate_cfg_rewrite` already share, because two divergent call models + would be a fresh instance of the very blind-spot class this module + attacks. + + HONEST LIMITS — three, stated because the point of this artifact is that a + validator which quietly shares its pass's blind spot is worse than no + validator: + (a) IT IS A GATE ONLY ON THE FLAG-OFF graph-colouring allocator. On the + DEFAULT path it is a report-only audit held to a CI floor. Making it + gate the default path means hard-erroring a user's compile on a + checker whose false-positive rate is MEASURED, not proven; that flip + is deliberately not taken. + (b) MEMORY IS NOT IN ITS OBLIGATION. A mis-renamed store address that a + later load reads back is a false negative for this instrument (it is + covered by `validate_cfg_rewrite`'s use-equations when that seed is + intact — the two are COMPLEMENTARY, which is what independence looks + like, not redundancy). + (c) THE OP MODEL IS STILL SHARED. Def/use extraction runs through + `liveness::reg_effect`, so a MISMODELED OP remains a blind spot + common to ALL THREE instruments. VCR-VER-004 closes the shared- + CONTRACT hole, not the shared-OP-MODEL hole. `synth-verify`'s + `ArmSemantics::encode_op` is a genuinely second model of the same + operations; PINNING THE TWO AGAINST EACH OTHER IS THE NEXT RUNG (the + VCR-ISA-001 Sail-derived semantics are the eventual anchor), and + until it is done "three independent validators" WOULD BE AN + OVERCLAIM. This is the named follow-up. + status: implemented + tags: [validation, abi, aapcs, translation-validation, independence, register-allocation, track-c, epic-242, release-v0.54, synth-893] + links: + # Same shape as its two siblings VCR-VER-003 / VCR-VER-761: a + # sys-verification measure must `verifies` a system requirement. + - type: verifies + target: VCR-001 + - type: traces-to + target: VCR-RA-003 + - type: traces-to + target: VCR-DEC-001 + # The shared-op-model residual (c) below names VCR-ISA-001's Sail-derived + # semantics as the eventual anchor for pinning `liveness::reg_effect` + # against a genuinely second model. + - type: traces-to + target: VCR-ISA-001 + fields: + method: translation-validation + preconditions: + - "v0.53 #872: the shared-blind-spot class demonstrated by mutation on validate_segment_rewrite" + - "VCR-DEC-001 increment 3 (#896): the graph-colouring allocator colours across calls, so the gate must model the AAPCS call effect rather than decline it" + steps: + - "synth_synthesis::abi_contract: forward value-graph construction + greatest-fixpoint bisimulation over RETURN_CONTRACT_REGS" + - "graph_alloc::abi_gate wires it as the accept/reject gate on the flag-off colouring allocator (NotAttempted is a DECLINE, not an accept)" + - "Re-run v0.53's EXACT mutation from the committed patch (scripts/repro/mutations/v053_shared_exit_contract.patch), not a reconstruction" + - "Report-only audit of the SHIPPING allocator over the repro corpus, held to a CI floor" + - "CI: instrument-independence-oracle asserts the BASELINE direction first, then the mutation, then that the tree was restored" + pass-criteria: > + On the mutated compiler and ONE compilation: `validate_cfg_rewrite` + returns Ok and VCR-RA-003 returns Consistent (both still green — the + shared blind spot is real and unpatched by this change) while + `validate_abi_contract` REJECTS with a concrete violation naming the ABI + result register — `Violated { sink: 81, reg: R0 }` on + `brif_outer_740::poll`, the function that returned 0x1111 instead of its + parameter — and the miscompile is NOT emitted. Proven RED-FIRST: make + `abi_gate` treat `Violated` as an accept and the mutated compiler goes + back to emitting the miscompile. COSTS NOTHING on the gated path — + composed with VCR-DEC-001 increment 3 over the ARM repro corpus, 617 + functions, 307 applied, 40822 -> 40722 bytes (−100 B relocatable, + −120 B self-contained): increment 3's result TO THE BYTE, with the check + conservative enough to demand both R0 and R1 for every function and to + decline whenever it cannot analyze. On the DEFAULT (shipping) path the + audit measured `Holds 431 / NotAttempted 202 / Violated 0` over 633 + corpus functions — ~68 % of the shipping path proven, `bl`/`blx` calls + included — with the corpus GROWING as lanes add fixtures, so the pinned + invariant is `Violated 0`, not the absolute counts. Both CI steps assert + machine-readable counts (`ASSERTIONS=4/4`, five `OK` lines, + `VIOLATED=0`) rather than trusting exit 0, and the job fails if the + mutation was left in the tree. + - id: VCR-VER-761 type: sys-verification title: "Self-contained --cortex-m linmem<->globals disjointness geometry gate catches the R9-overlap alias (#761)" From 613b72e23be3305a53b1f26ceb3cbf28aaceb762 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:15:25 +0200 Subject: [PATCH 06/13] docs(README): the aarch64 crate row still said "integer subset" MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `synth-backend-aarch64` has not been an integer subset since v0.54. The row now names what actually ships and points at the generated feature matrix for the exact surface rather than restating it (a second copy of that list is how v0.54's cold review found a doc-honesty defect): * the complete scalar f32/f64 surface (v0.54 #898 — rounding, FP memory, i64 converts, guarded i64 truncations); * bounds-checked linear memory (default `--safety-bounds software`, #865); * WASM globals and `call_indirect` with all three §4.4.8 trap guards (v0.54 #899); * direct calls and full control flow. The row is the LAST place in README that described the backend by what it could not do; the intro paragraph and the feature matrix were already current. Note for whoever picks this up next: CLAUDE.md carries a byte-identical stale copy of this row. It is deliberately NOT touched here — that file is agent configuration and is not mine to edit on a lane brief. claim_check 37/37 (the aarch64 rows in the generated matrix are template- driven and unaffected — no generated doc was hand-edited). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 695b46a3..a267f472 100644 --- a/README.md +++ b/README.md @@ -295,7 +295,7 @@ Honest open items: the RV32 local-promotion flip is held on a failed no-grow gat | `synth-frontend` | WASM Component Model parser and validator | | `synth-backend` | ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU | | `synth-backend-riscv` | RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 | -| `synth-backend-aarch64` | AArch64 (A64) host-native backend — integer subset, `-b aarch64` | +| `synth-backend-aarch64` | AArch64 (A64) host-native backend, `-b aarch64` — i32/i64 integer core, the **complete scalar f32/f64 surface** (v0.54), bounds-checked linear memory, globals, `call_indirect` with all three §4.4.8 trap guards, direct calls, and full control flow. See the [feature matrix](docs/status/FEATURE_MATRIX.md) for the exact op surface and the mechanically-enumerated declines | | `synth-backend-awsm` | aWsm backend integration (WASM-to-native via aWsm) | | `synth-backend-wasker` | Wasker backend integration (WASM-to-Rust transpiler) | | `synth-synthesis` | WASM-to-ARM instruction selection, peephole optimizer, pattern matcher | From 0b288e86c2d91d705c33ea4f62ff04e6018635dc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:17:37 +0200 Subject: [PATCH 07/13] ci(#893): the Rivet Validation gate could not see either error this lane fixed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both defects this lane repaired were sitting in a tree with `Rivet Validation` green. That is not a coincidence — the job's filter had two holes, and each one swallowed exactly one of them. (1) `grep "^ ERROR:"` anchored on two-space-indented lines. rivet prefixes SOME diagnostics with the source file instead (`gale-integration.yaml: ERROR: …`), so that entire class was invisible to the gate — including "artifact id X is declared more than once … the second definition silently overwrites the first". That is how GI-FPU-002 could be `implemented` in one file and `proposed` in another, with rivet resolving it to `proposed`, and nothing complained. (2) The cross-repo exemption `targets '.*:.*' which does not exist` exempted any target containing a COLON. `synth:396` contains a colon. So a broken link in our OWN graph — an issue number written where an artifact id belongs — was classified as an unresolvable link into an un-rivet'd sibling repo and waved through. Fixed structurally rather than by allowlist: every line containing `ERROR:` is now considered, and the exemption is "a target carrying a FOREIGN prefix", with our own `synth:` prefix explicitly added back to the ours-count. A new sibling repo therefore needs no edit here, and our own prefix can never slip back into the exempt set. Failures now PRINT the offending lines instead of only a count, so the next one is self-diagnosing. RED-FIRST, end to end, by replaying this exact step (extracted from the YAML, not paraphrased) against both trees: * pre-fix artifacts (65417c0): exit 1, "Found 2 rivet validation errors that are OURS (not cross-repo)", both named; * fixed artifacts (this branch): exit 0, with the expected cross-repo warning still emitted. CAVEAT, stated rather than assumed: this was verified against local rivet 0.28.0, while the job pins 0.23.0. The duplicate-id diagnostic may not exist in 0.23.0 at all, in which case hole (1)'s fix is latent protection rather than an active check today; hole (2)'s fix is version-independent. If 0.23.0 emits some other filename-prefixed error we cannot see locally, this job is where it will surface — and surfacing it is the point. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 47 ++++++++++++++++++++++++++++++++-------- 1 file changed, 38 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b6069e16..152e4aff 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -355,18 +355,47 @@ jobs: cargo install --force --git https://github.com/pulseengine/rivet --tag v0.23.0 rivet-cli fi - name: Validate artifacts + # THIS GATE HAD TWO HOLES, and v0.55 (#893) found them by finding two + # OURS-not-theirs errors sitting in a green tree. Both are fixed below; + # both fixes are red-first — replay this step's logic against the + # pre-fix artifacts and it reports 2, against the fixed ones 0. + # + # (1) `^ ERROR:` anchored on two-space-indented lines. rivet prefixes + # SOME diagnostics with the source file instead + # (`gale-integration.yaml: ERROR: …`), so that whole class was + # invisible here — including "artifact id X is declared more than + # once … the second definition silently overwrites the first", + # which is how GI-FPU-002 could be `implemented` in one file and + # `proposed` in another with this job green. Now every line + # containing `ERROR:` is considered. + # (2) The exemption `targets '.*:.*' which does not exist` exempted ANY + # target containing a colon — including `synth:396`, i.e. OUR OWN + # repo prefix. A `synth:`-prefixed target that does not resolve is + # not a cross-repo link into an un-rivet'd sibling; it is a broken + # link in our own graph (there, an issue NUMBER written where an + # artifact id belongs). Exemption is now "any prefix EXCEPT ours". + # + # Deliberately still exempt: kiln/gale/sigil/scry/jess/witness/loom/meld + # targets, because those repos have no rivet project at the configured + # path and the errors are unresolvable from this repo. Not an allowlist — + # the rule is structural ("a foreign prefix"), so a new sibling repo does + # not need this file edited, and our own prefix can never slip back in. run: | sed -i '/^externals:/,$d' rivet.yaml - # Allow cross-repo link errors (kiln/gale/sigil haven't set up rivet yet) - # but fail on any non-cross-repo errors (schema, missing fields, broken local refs) rivet validate 2>&1 | tee /tmp/rivet-output.txt - # Check if all errors are cross-repo links (contain ':' in target) - if grep -q "^ ERROR:" /tmp/rivet-output.txt; then - NON_XREF=$(grep "^ ERROR:" /tmp/rivet-output.txt | grep -v "targets '.*:.*' which does not exist" | grep -cv "missing '.*' link to" || true) - if [ "$NON_XREF" -gt 0 ]; then - echo "::error::Found $NON_XREF non-cross-repo validation errors" - exit 1 - fi + grep -E "ERROR:" /tmp/rivet-output.txt > /tmp/rivet-errors.txt || true + # Everything that is NOT a foreign-prefix broken link, ... + grep -vE "targets '[A-Za-z0-9_.-]+:[^']*' which does not exist" /tmp/rivet-errors.txt \ + | grep -v "missing '.*' link to" > /tmp/rivet-ours.txt || true + # ... plus foreign-looking links that actually carry OUR prefix. + grep -E "targets 'synth:[^']*' which does not exist" /tmp/rivet-errors.txt >> /tmp/rivet-ours.txt || true + NON_XREF=$(grep -c . /tmp/rivet-ours.txt || true) + if [ "${NON_XREF:-0}" -gt 0 ]; then + echo "::error::Found $NON_XREF rivet validation errors that are OURS (not cross-repo):" + cat /tmp/rivet-ours.txt + exit 1 + fi + if [ -s /tmp/rivet-errors.txt ]; then echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)" fi - name: Check coverage From f810b1a4ff3f54ac7f2efe9f0b9573da9cb357bf Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:22:54 +0200 Subject: [PATCH 08/13] =?UTF-8?q?docs(CHANGELOG):=20v0.55=20L7=20=E2=80=94?= =?UTF-8?q?=20traceability=20repair=20+=20the=20honest-N/A=20backlog?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c77dba86..01c6a83b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,85 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Fixed + +- **The traceability graph disagreed with itself in four places, and the gate + that should have said so could not see two of them (#893, #396).** No code + behaviour changes here; what changes is whether the project's evidence + artifacts can be trusted to mean one thing. + + - **`VCR-DEC-003` pointed at an issue NUMBER where an artifact id belongs.** + `traces-to: synth:396` reads as "artifact 396 in repo synth" and no such + artifact exists. The link is not deleted: synth#396's own body says + *"Tracked in rivet as VCR-COV-001"*, and `VCR-COV-001`'s title carries + "(synth #396)", so the link now targets the artifact and the issue number + moves to the tags, where it is a reference rather than a resolvable target. + - **`GI-FPU-002` was declared TWICE, and the stale copy won.** The id existed + in `gale-integration.yaml` (`proposed`, the original #369 ask) and again in + `verified-codegen-roadmap.yaml` (`implemented`, PR #705's phase-1 delivery + record). rivet loaded the second over the first, so the graph reported the + requirement as NOT STARTED while README and CHANGELOG report #369 closed, + f32 complete v0.41, f64 complete v0.43, VFP spilling v0.53. Merged — not + deleted, because each copy carried edges and evidence the other lacked — + into the id's namespace home, and de-staled to `implemented` with the two + remaining float declines named rather than implied away. + - **`VCR-RA-004` was `proposed` for a resolver that shipped in v0.11.38.** + v0.53's VFP-spilling lane tagged its work with that id and the issue read it + as one id meaning two things. The evidence says otherwise: + `synth_synthesis::parallel_move` is verbatim what the artifact specifies, + the artifact's own tags already said `release-v0.11.38`, and v0.53 *extended* + it to the VFP file rather than reusing its name. Only the status field had + never been flipped — minting a second id would have created the collision + the issue was trying to remove. Now `implemented`, with `SWVER-022` closing + the right side of the V by a typed `verifies` link instead of a paragraph. + Deliberately **not** `verified`: the property test the criteria demand does + exist and does exactly what they specify (6000 sequentializations against a + reference parallel semantics), but the second pitfall the artifact names — + split points inside hot loops — is still bounded by assumption, and that + residual is now written down. + - **`VCR-SEL-005` said "BOTH the ARM and RISC-V selectors"** for a gate that + has spanned three backends since v0.53 (#883). Correcting the count exposed + that every ledger *size* asserted around it had also drifted — and all in the + flattering direction, describing gaps that have since closed: the roadmap + said 21 entries for an array of 18, `known_divergences`'s doc comment said + 19, and `aarch64_known_divergences`'s said "the SEVEN below" over an array of + 5. The stale-entry check already forces a closed gap to retire its ledger + line; nothing forced the prose *about* the ledger to move with it. + +- **The `Rivet Validation` job had two blind spots — one per defect above.** + Both errors sat in a green tree, which is not a coincidence: the filter + anchored on `^ ERROR:` and so never saw rivet's filename-prefixed diagnostics + (the duplicate-id class), and its cross-repo exemption waved through any target + containing a colon — including `synth:`, our own prefix. Fixed structurally + rather than by allowlist, and proven red-first by replaying the exact step + against both trees: exit 1 naming both errors on the pre-fix artifacts, exit 0 + after. + +### Added + +- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared + in the CHANGELOG, the feature matrix and CI — but not in the file README calls + "the single source of truth for roadmap status". The entry records the four + axes on which it fails *differently* from the two validators that shared a + blind spot, and all three of its limits, including the one that bounds the + whole claim: **the op model is still shared.** Def/use extraction for all three + instruments runs through `liveness::reg_effect`, so a mismodeled op remains a + common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the + shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is + pinned against it, "three independent validators" would be an overclaim. + +### Documentation + +- README's `synth-backend-aarch64` row still said "integer subset". It has not + been one since v0.54 — the scalar float surface, globals, `call_indirect` and + bounds-checked memory all ship. +- Filed #912: the feature loop's step 5 (witness MC/DC) has been marked N/A four + releases running, past the skill's own three-feature threshold. synth compiles + Wasm rather than emitting components, so witness may have no artifact to + instrument — but `VCR-COV-001` is the standing argument that the DO-178C + 6.4.4.2 source-to-object obligation does not go away just because the + measurement point does. Recorded for a decision rather than re-skipped. + ## [0.54.0] - 2026-08-05 **"Close what we measured."** v0.53 built the instruments; this release acts on From 5802785712d5f735f48f53219916fed74e51f230 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:30:46 +0200 Subject: [PATCH 09/13] =?UTF-8?q?fix(#893):=20GI-FPU-VER-002=20=E2=80=94?= =?UTF-8?q?=20close=20the=20gap=20the=20GI-FPU-002=20status=20flip=20revea?= =?UTF-8?q?led?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flipping GI-FPU-002 from `proposed` to `implemented` made rivet START checking its lifecycle coverage, which correctly reported that the requirement had NO verification artifact at all. The gap was not created by the flip — the wrong status was HIDING it, which is the same failure mode as the duplicate id itself, one rule further down. The evidence already existed and was already named in the requirement's own criteria; it simply had no typed `verifies` link. GI-FPU-VER-002 is that link, and it records what the verification actually is rather than asserting that some exists: * the f32 execution differential (48/48 bit-exact vs wasmtime on cortex-m4f, symbols read from the ELF SYMTAB per #489 rather than from host-dependent `synth disasm` text, FPU genuinely enabled via CPACR + FPEXC.EN); * the HONEST-REJECT direction in the same harness (cortex-m3 must still refuse) — a one-directional differential would pass equally well on a compiler that had quietly widened the FPU gate; * the unit-level pins that need no emulator (AAPCS-VFP S0/S1 homing, the swapped-VCVT signedness fix); * the v0.53 #881 spilled-VFP differential (109 rows, NaN-aware per WASM §4.3.3, internal `bl` resolved by a REAL link so an unresolved relocation cannot be silently skipped as a pass); * and the one part of the surface whose evidence is encoding-level ONLY — the f32 comparisons, because unicorn does not model the VMRS FPSCR→APSR flag transfer. Recorded, not omitted. Deliberately shaped `method: automated-test` + `steps.run`/`steps.coverage` rather than mirroring GI-FPU-VER-001's `method: test` + `pass-criteria`, which produce a WARN and an INFO against the schema. This adds ZERO new diagnostics. MEASURED, prompted by review asking whether `rivet coverage` — the SECOND step of the same CI job, which I had not exercised — moved: rivet coverage, real exit 0 both sides swe1-has-verification (sw-req) 31/60 (51.7%) -> 33/60 (55.0%) swe6-verifies-swe1 32/32 -> 34/34 sys5-verifies-sys2 49/49 -> 50/50 Overall (weighted) 90.3% -> 90.7% VCR-RA-004 and GI-FPU-002 both drop off the "lacking verification" list. Full diagnostic diff for the whole branch vs main is now exactly: −2 ERROR (both ours: synth:396, the duplicate id) −2 WARN (GI-FPU-002 and VCR-RA-004 "should be verified by", both closed) +2 WARN, +1 INFO (all three VCR-VER-004's, all of kinds its sibling sys-verification artifacts already carry) So: errors 52 -> 50 with ours 2 -> 0, and warnings net UNCHANGED at 104. Lifecycle coverage gaps 54 -> 56 — honest, not a regression: GI-FPU-002 and VCR-RA-004 are newly CHECKED because they are no longer `proposed`. Both were absent from the baseline list only because a wrong status exempted them. cargo fmt 0 / clippy 0 / test --workspace 0 (2675 passed) / claim_check 37/37. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/gale-integration.yaml | 59 +++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index 6af0bbc5..05d8f9a7 100644 --- a/artifacts/gale-integration.yaml +++ b/artifacts/gale-integration.yaml @@ -758,6 +758,65 @@ artifacts: cargo test test_369 green; f32 module emits no fadd/dmul symbol; control_step / flight_seam / div_const differentials byte-identical. + # Right-side closure for GI-FPU-002 (#893). Flipping that requirement from + # `proposed` to `implemented` made rivet START checking its lifecycle coverage, + # which correctly reported it had NO verification artifact — a gap the wrong + # status had been hiding, not one the flip created. The evidence already + # existed and was named in the requirement's criteria; it just had no typed + # `verifies` link. This artifact is that link. + - id: GI-FPU-VER-002 + type: sw-verification + title: "Hardware-FPU (VFP) lowering (#369) — execution differentials + honest-reject + spilled-VFP" + description: > + Verifies GI-FPU-002 across its whole arc, by EXECUTION rather than by + inspection: + + (1) f32 reachability (v0.41, #619/#705) — + `scripts/repro/f32_vfp_619_differential.py` compiles f32 add/sub/mul/div, + i32.trunc_f32_s and f32.convert_i32_s/u for cortex-m4f, reads each symbol + from the ELF SYMTAB (#489 — never from `synth disasm` text, which is + host-dependent), runs it under unicorn with the FPU actually enabled + (CPACR CP10/CP11 + FPEXC.EN) and f32 args in S0/S1 per AAPCS-VFP, and + asserts bit-exactness (`to_bits`) against wasmtime on boundary values + including a subnormal. RED before the fix (compile REJECTS, exit 1), GREEN + after (48/48). + + (2) The HONEST-REJECT direction, in the same harness: cortex-m3 must still + REFUSE f32 rather than silently emitting something. A one-directional + differential would pass just as well on a compiler that had quietly + widened the FPU gate. + + (3) Unit-level pinning without an emulator — + `crates/synth-backend/tests/f32_hardfloat_619.rs` locks the AAPCS-VFP + S0/S1 homing, the honest reject, and the swapped-VCVT signedness fix. + + (4) Exhaustion (v0.53, #881) — the spilled-VFP differential: 7 shapes on + `-t cortex-m7dp --relocatable`, 109 rows bit-identical to wasmtime, + NaN-aware per WASM §4.3.3, with the internal `bl` resolved by a REAL link + so an unresolved relocation cannot be silently skipped as a pass. + + HONEST BOUND, recorded not hidden: the f32 COMPARISONS are byte-pinned in + `f32_vfp_encoding_test.rs` but are NOT execution-differentiated — unicorn + does not model the VMRS FPSCR→APSR flag transfer. That is an emulator gap, + and it is the one part of the surface whose evidence is encoding-level + only. + status: implemented + tags: [gale, fpu, vfp, verification, differential, unicorn, symtab, release-v0.41, release-v0.53, synth-893] + links: + - type: verifies + target: GI-FPU-002 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend --test f32_hardfloat_619 && python3 scripts/repro/f32_vfp_619_differential.py" + coverage: > + scripts/repro/f32_vfp_619_differential.py (48/48 bit-exact vs wasmtime + on cortex-m4f + the cortex-m3 honest-reject leg), + crates/synth-backend/tests/f32_hardfloat_619.rs (AAPCS-VFP homing, + reject, VCVT signedness), the #881 spilled-VFP differential (109 rows), + and crates/synth-backend/tests/f32_vfp_encoding_test.rs for the + comparison encodings unicorn cannot execute + - id: GI-MEM-001 type: sw-req title: Full-width i64.load/i64.store lower correctly (#372) From 3e99332e64f2a7d013c155dcb17b40de6c82bd55 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:31:06 +0200 Subject: [PATCH 10/13] docs(CHANGELOG): record the two verification artifacts + the rivet coverage delta Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 01c6a83b..a849d5e3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,6 +52,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 5. The stale-entry check already forces a closed gap to retire its ledger line; nothing forced the prose *about* the ledger to move with it. +- **Two verification artifacts were added to close gaps the status fixes + revealed** (`SWVER-022` for VCR-RA-004, `GI-FPU-VER-002` for GI-FPU-002). + Neither gap was created by this work — a `proposed` artifact is not + lifecycle-checked, so the wrong statuses had been *hiding* them. The evidence + existed and was already named in both requirements' criteria; it just had no + typed `verifies` link. Measured on `rivet coverage` (the job's second step): + sw-req V-closure **31/60 → 33/60**, weighted overall **90.3 % → 90.7 %**. + - **The `Rivet Validation` job had two blind spots — one per defect above.** Both errors sat in a green tree, which is not a coincidence: the filter anchored on `^ ERROR:` and so never saw rivet's filename-prefixed diagnostics From 9df092d4b42114af44a64b6c3eab67d66e1cb63e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:32:14 +0200 Subject: [PATCH 11/13] docs(roadmap): disambiguate the aarch64 ledger count (5 entries, not 4 named) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The prose grouped `local.set`+get and `local.tee` on a param local as one phrase over two separate ledger entries, so the sentence read as four items beside the count 5 — a small instance of exactly the prose-vs-array drift this paragraph exists to prevent. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index a7c69b62..d1eb4349 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -620,9 +620,11 @@ artifacts: LEDGER STATE (2026-08, keep in step with the arrays — a drifting count is the #893 class this oracle exists to prevent): ARM<->RV32 18 entries (5 Zbb + 16 universe-completeness − `memory.size`/`memory.grow` closed - v0.50 − `br_table` closed v0.53 #882); ARM<->aarch64 5 entries (br_table, - writing a PARAM local via local.set/local.tee in a leaf function, - memory.copy, memory.fill). Non-vacuity floors: `at_parity >= 65` (RV32), + v0.50 − `br_table` closed v0.53 #882); ARM<->aarch64 5 entries — br_table, + `local.set`+get on a PARAM local, `local.tee` on a PARAM local (two + separate entries, both the leaf-function param-homing prerequisite), + memory.copy, memory.fill — after v0.54 closed `global.get`/`global.set`. + Non-vacuity floors: `at_parity >= 65` (RV32), `at_parity >= 60` (aarch64), `probed >= 100` (aarch64 extended surface). Both legs carry their own red-first companion (`red_first_unledgered_one_sided_gap_is_caught` drops the real i32.rotl From 0f0c232fb9fbd14a61205a1a1d0a7ba2b2746374 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:36:50 +0200 Subject: [PATCH 12/13] docs(CLAUDE.md): de-stale the three aarch64 claims MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit L7 correctly declined to touch this on a lane brief (agent configuration, not lane scope) and flagged it instead. Coordinator picking it up. CLAUDE.md carried a byte-identical copy of the stale README row the v0.54 cold review found, plus a third instance nobody had spotted: 1. header: "AArch64 (host-native, integer subset)" — the scalar float surface is complete as of v0.54. 2. crate map: "integer subset" — now i32/i64 core, complete scalar f32/f64, globals, call_indirect, bounds-checked linear memory. 3. VCR-VER-003 note: "AArch64 is N/A (no linear-memory ops in the integer subset)". The VERDICT is still right, the REASON is false — aarch64 has had bounds-checked linear-memory load/store since v0.52 (#865). It is N/A because it emits no data section and REFUSES data-carrying modules loudly (v0.53), so there is no served-vs-runtime image to compare. A correct conclusion resting on a false premise is the harder version of this defect: the sentence reads fine and the reasoning has rotted. Fourth copy of a list this project keeps duplicating (oracle, matrix row, CHANGELOG, CLAUDE.md). Generating the prose from the executable decline list is the standing fix; #911 is the nearest tracked version of it. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CLAUDE.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 0aebbee1..7b9b76ec 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -2,7 +2,7 @@ ## What This Is -Synth is a WebAssembly-to-ARM Cortex-M (Thumb-2), Cortex-R5 (A32), RISC-V (RV32IMAC), and AArch64 (host-native, integer subset) compiler with mechanized correctness proofs in Rocq (formerly Coq). It produces bare-metal ELF binaries for embedded targets. +Synth is a WebAssembly-to-ARM Cortex-M (Thumb-2), Cortex-R5 (A32), RISC-V (RV32IMAC), and AArch64 (host-native) compiler with mechanized correctness proofs in Rocq (formerly Coq). It produces bare-metal ELF binaries for embedded targets. Part of [PulseEngine](https://github.com/pulseengine): synth (compiler) + [loom](https://github.com/pulseengine/loom) (WASM optimizer) + [meld](https://github.com/pulseengine/meld) (platform). @@ -29,7 +29,7 @@ bazel test //tests/... # Renode ARM Cortex-M4 emulation tests | `synth-frontend` | WASM Component Model parser and validator | | `synth-backend` | ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU | | `synth-backend-riscv` | RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 | -| `synth-backend-aarch64` | AArch64 (A64) host-native backend — integer subset, `-b aarch64` | +| `synth-backend-aarch64` | AArch64 (A64) host-native backend — i32/i64 core, complete scalar f32/f64, globals, `call_indirect`, bounds-checked linear memory; `-b aarch64` | | `synth-backend-awsm` | aWsm backend integration (WASM→native via aWsm) | | `synth-backend-wasker` | Wasker backend integration (WASM→Rust transpiler) | | `synth-synthesis` | WASM→ARM instruction selection, peephole optimizer, pattern matcher | @@ -172,8 +172,11 @@ frozen and oracle-gated every step: generated startup at reset — the emitted blob is READ BACK and validate_served_image hard-errors the compile on any served/runtime disagreement (the v0.47 warning is gone; the de-vacuated control_step - differential + a full-boot unicorn oracle gate it); AArch64 is N/A (no - linear-memory ops in the integer subset). + differential + a full-boot unicorn oracle gate it); AArch64 is N/A, but for a + DIFFERENT reason than when this was written — it HAS bounds-checked + linear-memory load/store (v0.52 #865), and is N/A because it emits no data + section at all and REFUSES a module carrying active data segments loudly + (v0.53), so there is no served-vs-runtime image to compare. - **Track D (schedulability, #778):** `--emit-wcet` emits a SOUND static per-function worst-case cycle bound (`synth-wcet-v1` sidecar) as gale spar's T3/T4 `C_i` input — a bound, not a DWT observation. Loop-free functions get an From f43f5796decd782bbccb439ae51d2a7c50ff3221 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:39:27 +0200 Subject: [PATCH 13/13] docs(CHANGELOG): record the CLAUDE.md aarch64 de-staling, incl. the rotted premise MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 0f0c232 landed the CLAUDE.md half of the aarch64 doc fix but no release note. Adding one — and specifically calling out its third finding, which is the only one of the four that is not a plain stale string: VCR-VER-003's aarch64 N/A note gave a FALSE REASON for a TRUE verdict ("no linear-memory ops in the integer subset" — aarch64 has had bounds-checked linear-memory load/store since v0.52 #865). It is N/A because it emits no data section and refuses data-carrying modules loudly, so there is no served-vs-runtime image to compare. That failure mode deserves the note more than the two string copies do: a stale "integer subset" reads wrong and invites a check, whereas a correct conclusion resting on a rotted premise still reads fine, so nothing prompts one. Both underlying facts re-verified against the generated feature matrix before writing this. claim_check 37/37 (CLAUDE.md is pinned by three ledger entries; unaffected). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a849d5e3..95fc3cbe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -86,7 +86,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - README's `synth-backend-aarch64` row still said "integer subset". It has not been one since v0.54 — the scalar float surface, globals, `call_indirect` and - bounds-checked memory all ship. + bounds-checked memory all ship. `CLAUDE.md` carried a byte-identical copy plus + a **third** instance worth naming on its own: its Track-C note said aarch64 is + N/A for VCR-VER-003 *"(no linear-memory ops in the integer subset)"*. The + **verdict is still correct and the reason is false** — aarch64 has had + bounds-checked linear-memory load/store since v0.52 (#865); it is N/A because it + emits no data section and refuses data-carrying modules loudly (v0.53), so there + is no served-vs-runtime image to compare. A right conclusion resting on a rotted + premise is the harder version of this defect: the sentence still reads fine, so + nothing prompts a re-check. That was the **fourth** copy of a list this project + keeps duplicating (parity oracle, matrix row, CHANGELOG, CLAUDE.md); generating + the prose from the executable decline list is the standing fix (#911). - Filed #912: the feature loop's step 5 (witness MC/DC) has been marked N/A four releases running, past the skill's own three-feature threshold. synth compiles Wasm rather than emitting components, so witness may have no artifact to