diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5566735a..cf1cc6d0 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 diff --git a/CHANGELOG.md b/CHANGELOG.md index f2a3ddd3..626e0b48 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,8 +7,81 @@ 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. + +- **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 + (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. + - **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and attested (VCR-MEM-004, #901).** `synth compile --proven-safe safe-accesses.json` consumes scry's `scry/safe-accesses/v1` verdict list @@ -86,6 +159,28 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 turns it RED with a real `UC_ERR_READ_UNMAPPED`. Opt-in; frozen anchors 10/10 (the mark vector defaults empty). +### 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. `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 + 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 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 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 | diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index b2940ddf..05d8f9a7 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 @@ -696,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) diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 1aa0cf09..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 @@ -533,3 +551,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 2eb15e41..0d50a238 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,42 @@ 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, + `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 + 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 +641,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) @@ -1458,6 +1503,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)" @@ -2080,8 +2255,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 +2314,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" @@ -2272,14 +2514,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: @@ -3598,76 +3846,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) # --------------------------------------------------------------------------- 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)] { &[ (