From 4b519c8ee979451567a8b55d653777f3b3bfa65e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 11 Aug 2026 21:57:08 +0200 Subject: [PATCH 1/4] docs(#945): correct a false claim this project wrote, and stop a gate passing on nothing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit From a doc-vs-source sweep (~430 claims examined, 10 genuine disagreements). These are the two that are ours and consequential; the rest are filed. 1. RQ-56-CONF said the official WebAssembly testsuite was 'absent'. FALSE, and written by us three days ago. `tests/spec-testsuite` is a checked-out submodule at 3453673 with 257 .wast files, and `tests/spec/BUILD.bazel` has targets consuming it. The true statement is WORSE: present, runnable, unrun. Three states coexist in the tree — * README.md:122 + FEATURE_MATRIX:122 advertise a 'CI-tracked compile rate' over it; * the only wast CI step references spec-testsuite ZERO times; * our own requirement called it missing. 2. That step was `bazel test //tests/renode/... --test_tag_filters=wast || [ $? -eq 4 ]`. Exit 4 is Bazel's NO TESTS MATCHED, so it passed while selecting nothing — the exact vacuity class this release is named for, sitting in the gate list. An empty Renode matrix is still tolerated (the emulator is not always present) but now prints a ::warning:: and says it is TOLERATED-EMPTY rather than reporting a silent pass. Also advances RQ-56-CITE and RQ-56-PSAFE from `proposed` to `implemented`: both deliverables are ancestors of origin/main (#927, #934). The sweep caught the release-scope artifact not being advanced as items land — the same drift as `status: implemented` on unimplemented work, inverted, and it would have made the readiness query lie in the safe-looking direction. claim 43/43, citations 0 false claims, rivet ours-errors 0. Refs #945 --- .github/workflows/ci.yml | 22 +++++++++++++++++++++- artifacts/release-v0.56.yaml | 22 ++++++++++++++++++---- 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 28ef33b8..1c5d7fbc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -505,7 +505,27 @@ jobs: - name: Verify Rocq proofs run: bazel test //coq:verify_proofs - name: Run Renode emulation tests - run: bazel test //tests/renode/... --test_tag_filters=wast || [ $? -eq 4 ] + # #945: `|| [ $? -eq 4 ]` swallows Bazel exit 4 = NO TESTS MATCHED, so + # this step passed while selecting nothing. Keep tolerating a genuinely + # empty Renode matrix (the emulator is not always available), but SAY so + # rather than reporting a silent pass — an unreachable gate that prints + # nothing is the class this release exists to remove. + # + # NOTE, recorded not fixed here: this target tree references + # `tests/spec-testsuite` ZERO times, so it is NOT the "CI-tracked compile + # rate" over the official suite that README.md:122 and + # FEATURE_MATRIX:122 advertise. That 257-file suite is checked out and + # entirely unrun. Wiring it is RQ-56-CONF's continuation. + run: | + set -uo pipefail + bazel test //tests/renode/... --test_tag_filters=wast + rc=$? + if [ "$rc" -eq 4 ]; then + echo "::warning::renode wast matrix selected ZERO tests (bazel exit 4)" + echo " This step is TOLERATED-EMPTY, not passing on evidence." + elif [ "$rc" -ne 0 ]; then + exit "$rc" + fi timeout-minutes: 10 cmp-select-oracle: diff --git a/artifacts/release-v0.56.yaml b/artifacts/release-v0.56.yaml index ea3e623b..c80f1353 100644 --- a/artifacts/release-v0.56.yaml +++ b/artifacts/release-v0.56.yaml @@ -55,7 +55,7 @@ artifacts: shape for repro scripts; the artifacts surface simply never got one. Red-first is mandatory: the new check must be seen to FAIL on the two current citations before they are fixed. - status: proposed + status: implemented release: v0.56 tags: [instrument-quality, traceability, vacuity, spar-ported] links: @@ -258,8 +258,22 @@ artifacts: conformance gate; synth (the compiler, whose output actually runs on target) has none. `crates/synth-test/` already PARSES and COMPARES assertions — the infrastructure exists and is simply not wired. - Also absent: the official WebAssembly testsuite, so the compiler has never - been graded against the standard at all. + CORRECTED 2026-08-11 (doc-vs-source sweep): an earlier draft of this + requirement said the official WebAssembly testsuite was "absent". That was + FALSE and written by this project, not inherited — `tests/spec-testsuite` + is a checked-out submodule at 3453673 carrying 257 `.wast` files, with + `tests/spec/BUILD.bazel` targets that consume it. + The true statement is worse, not better: the suite is PRESENT, RUNNABLE and + UNRUN. No workflow invokes those targets — the only wast step in CI is + `bazel test //tests/renode/... --test_tag_filters=wast`, whose target tree + references `spec-testsuite` ZERO times, and whose `|| [ $? -eq 4 ]` suffix + swallows Bazel's "no tests matched" exit so the step passes while selecting + nothing. Meanwhile README.md:122 and FEATURE_MATRIX:122 both advertise a + "CI-tracked compile rate" over it. + So there are three states in the tree: a doc claiming CI tracks it, a CI + step that cannot reach it and cannot fail, and a requirement that called it + missing. Wiring the 257-file official suite is the natural continuation of + this requirement once the in-tree assertions execute. Non-negotiable on delivery: the wired gate must report an EXECUTED ASSERTION COUNT and fail on zero, or it recreates the defect it closes. status: proposed @@ -302,7 +316,7 @@ artifacts: blind spot; only execution catches it"). Fix must include the imported-memory shape in the differential, and a module whose floor cannot be established must REFUSE, never derive 0. - status: proposed + status: implemented release: v0.56 tags: [security, soundness, proven-safe, regression, critical] links: From 4325deafe98d9caf1df9c7c032050b6c802926eb Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 11 Aug 2026 22:33:55 +0200 Subject: [PATCH 2/4] =?UTF-8?q?fix(#945):=20capture=20bazel's=20exit=20wit?= =?UTF-8?q?h=20`||=20rc=3D$=3F`=20=E2=80=94=20`bash=20-e`=20aborted=20firs?= =?UTF-8?q?t?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first version of this step read bazel test //tests/renode/... --test_tag_filters=wast rc=$? GitHub runs `run:` blocks under `bash -e`, so the non-zero `bazel test` aborted the step BEFORE `rc=$?` ever executed. The step failed with exactly the exit 4 it was written to REPORT: ERROR: No test targets were found, yet testing was requested ##[error]Process completed with exit code 4 `|| rc=$?` suppresses `-e` for that command, which is the whole point of the idiom. Verified locally under `bash -e` on all three legs, including the negative control that matters most — the fix must not turn into a new swallow: exit 4 (empty matrix) -> step exit 0, prints TOLERATED-EMPTY exit 1 (real failure) -> step exit 1, propagates old form, exit 4 -> step exit 4, prints NOTHING (the bug) The finding this step was added to surface still stands, and CI has now confirmed it on a real runner: the Renode wast matrix selects ZERO tests. The `|| [ $? -eq 4 ]` it replaced had been reporting that as a silent pass. Refs #945 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1c5d7fbc..0e59a65c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -516,10 +516,14 @@ jobs: # rate" over the official suite that README.md:122 and # FEATURE_MATRIX:122 advertise. That 257-file suite is checked out and # entirely unrun. Wiring it is RQ-56-CONF's continuation. + # `|| rc=$?`, NOT a bare `rc=$?` on the next line: GitHub runs `run:` + # under `bash -e`, so a non-zero `bazel test` aborts the step BEFORE the + # capture — which is exactly how the first attempt at this fix failed, + # with the very exit 4 it was written to report. run: | set -uo pipefail - bazel test //tests/renode/... --test_tag_filters=wast - rc=$? + rc=0 + bazel test //tests/renode/... --test_tag_filters=wast || rc=$? if [ "$rc" -eq 4 ]; then echo "::warning::renode wast matrix selected ZERO tests (bazel exit 4)" echo " This step is TOLERATED-EMPTY, not passing on evidence." From 96eaaecb95c277a016e37c195bc4d765825d4944 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 12 Aug 2026 00:33:34 +0200 Subject: [PATCH 3/4] docs(#946 A+B): name the guarantor of the VCVT precondition, drop the false one MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two Tier-1 items from the doc-vs-source sweep, both landing on `encode_thumb_i32_trunc_f64`. Investigated by compiling and reading the emitted instructions. **Neither is a live miscompile**, and neither resolves the way the scan hypothesized — which is the point of the "report the disagreement, don't rule on it" framing. ## A — "the SELECTOR guarantees `dm` is a dead temp" TRUE, of the selector the compiler actually uses. `select_with_stack` emits the copy; visible in the shipped output for a single-f64-param function: vmov r1, r2, d0 ; param's AAPCS-VFP home vmov d1, r1, r2 ; -> fresh D-temp vcvt.s32.f64 s2, d1 ; converts from the TEMP `select_default` genuinely does not implement it (`alloc_vfp_dreg` is a bare `(n + 1) % 16`). But the scan's reachability premise was that "`--relocatable` forces `select_default` (per #197)", and that is wrong: #197 forces the DIRECT selector, and the direct selector IS `select_with_stack` (`arm_backend.rs:566`). "Direct" and "default" are different things. `InstructionSelector::select` is not reachable from `synth compile` at all — its only non-test caller in the tree is `examples/compile_add.rs`. So the exposure is a `pub` API without the guarantee, not a compiled miscompile. Now stated where someone reaching for that API would see it. ## B — "never S0" FALSE as written, and measurable in three lines of wat: (func (result i32) (i32.trunc_f64_s (f64.const 3.7))) -> vcvt.s32.f64 s0, d0 The claim was also unnecessary. S0 is dangerous only as an *unrelated* scratch; `S(2m)` is always the low half of `dm`, which the dead-temp precondition already covers. Removed rather than "corrected" — a guard the code does not have and does not need is worse than no sentence, because it reads as load-bearing. This is the category the sweep is weakest at finding: not a doc contradicting its source, but a soundness argument that is locally true and cites the wrong reason. Both halves read correct; only writing a new consumer exposes it. Noted on #946 as a class to hunt deliberately. Refs #946 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- Cargo.lock | 21 ----------- crates/synth-backend/src/arm_encoder.rs | 50 +++++++++++++++++++++---- 2 files changed, 42 insertions(+), 29 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 8ceead90..d07ce5c3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1533,16 +1533,6 @@ dependencies = [ "unicode-ident", ] -[[package]] -name = "wasm-encoder" -version = "0.254.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09480d646178e5fdd12bb06e812d0af9a3a191dbc9cd697fdc86687beade7393" -dependencies = [ - "leb128fmt", - "wasmparser 0.254.0", -] - [[package]] name = "wasm-encoder" version = "0.255.0" @@ -1584,17 +1574,6 @@ dependencies = [ "bitflags", ] -[[package]] -name = "wasmparser" -version = "0.254.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d5769a29f799fbab136aaf65b4fe5384cd7d93fe6fc9ba0dcb6c8382a1f16e27" -dependencies = [ - "bitflags", - "indexmap", - "semver", -] - [[package]] name = "wasmparser" version = "0.255.0" diff --git a/crates/synth-backend/src/arm_encoder.rs b/crates/synth-backend/src/arm_encoder.rs index 323370ae..42ba465a 100644 --- a/crates/synth-backend/src/arm_encoder.rs +++ b/crates/synth-backend/src/arm_encoder.rs @@ -7277,14 +7277,48 @@ impl ArmEncoder { Ok(vfp_to_thumb_bytes(vcvt)) } - /// Encode f64 → i32 truncation as Thumb-2 (round-toward-zero VCVT). The - /// 32-bit result stages through the SOURCE's own low S-alias (`S(2m)`, - /// clobbering half of an operand the selector has already popped) — never - /// S0, which may hold an unrelated live value (the #615 class). The - /// overlapping write is well-defined: VCVT reads its source operand - /// before writing (compilers emit `vcvt.f32.f64 s0, d0` routinely). - /// The SELECTOR guarantees `dm` is a dead temp, never a pinned param/ - /// local home (it copies a home into a fresh D-temp first). + /// Encode f64 → i32 truncation as Thumb-2 (round-toward-zero VCVT). + /// + /// The 32-bit result stages through the SOURCE's own low S-alias, `S(2m)`, + /// clobbering half of an operand the selector has already popped. The + /// overlapping write is well-defined: VCVT reads its source operand before + /// writing (compilers emit `vcvt.f32.f64 s0, d0` routinely). + /// + /// # The one precondition, and who actually provides it + /// + /// `dm` must be a DEAD TEMP — never a pinned param/local home. That is the + /// whole safety argument, and it is worth naming the guarantor precisely + /// (#946): **`select_with_stack`** provides it, by copying a home into a + /// fresh D-temp first. Visible in the shipped output for + /// `(func (param f64) (result i32) (i32.trunc_f64_s (local.get 0)))`: + /// + /// ```text + /// vmov r1, r2, d0 ; read the param out of its AAPCS-VFP home D0 + /// vmov d1, r1, r2 ; ...into a fresh D-temp + /// vcvt.s32.f64 s2, d1 ; convert from the TEMP, staging into its own S2 + /// ``` + /// + /// `InstructionSelector::select` / `select_default` do NOT provide it — + /// `alloc_vfp_dreg` is a bare round-robin `(n + 1) % 16` with no liveness + /// or home test. That path is not reachable from `synth compile` + /// (`arm_backend.rs` calls `select_with_stack` exclusively; the only + /// non-test caller of `select` is `examples/compile_add.rs`), so this is + /// not a live miscompile — but a caller reaching that `pub` API directly + /// gets no such guarantee. + /// + /// # What this deliberately does NOT claim + /// + /// An earlier version of this comment said the staging register is "never + /// S0, which may hold an unrelated live value (the #615 class)". **That is + /// false**, and measurably so: for + /// `(func (result i32) (i32.trunc_f64_s (f64.const 3.7)))` the shipped + /// compiler emits `vcvt.s32.f64 s0, d0`. + /// + /// It is also unnecessary. S0 is only dangerous as an *unrelated* scratch; + /// here it is always the low half of `dm` itself, which the precondition + /// above already makes dead. Naming a guard the code does not have — and + /// does not need — invites a future reader to lean on it. The dead-temp + /// precondition is the only thing holding this up. fn encode_thumb_i32_trunc_f64(&self, rd: &Reg, dm: &VfpReg, signed: bool) -> Result> { let dm_num = vfp_dreg_to_num(dm)?; if dm_num > 7 { From 9945d175a62b917f444a331aafb963d08dc1f72d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 12 Aug 2026 00:37:19 +0200 Subject: [PATCH 4/4] =?UTF-8?q?docs(#946=20C):=20--volatile-segment=20is?= =?UTF-8?q?=20not=20free=20=E2=80=94=20it=20doubles=20code=20size?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `main.rs` told users the flag is inert: > PHASE 1 = plumbing only: the ranges are parsed and threaded to codegen but > NOT yet consumed — the emitted bytes are unchanged whether or not the flag > is passed. Phase 2 shipped and this sentence did not move. Measured on `scripts/repro/volatile_segment_543.wat`, `--cortex-m` on `cortex-m4`, with a scrubbed env so no ambient `SYNTH_*` leaks in: levers flag-off flag-on CSE default 36 B 74 B <- differs both CSE off 98 B 98 B <- same The second row is what makes the first one interpretable: with the CSE levers already off the flag changes nothing, so the +38 B is EXACTLY the aliasing back-off and not some other effect. **Code is right; only the doc was wrong.** Backing off const-CSE and base-CSE inside a volatile window is the whole point of the feature — sharing a materialized constant across accesses an external agent rewrites out-of-band is precisely what must not happen. It is also properly gated, by three tests in `volatile_segment_phase2_543.rs`. What made this worth fixing is the direction of the error. Most stale docs understate what ships and cost nothing; this one told a user that a flag which DOUBLES code size was free, so the safe-looking move (mark generously, it is only plumbing) is the expensive one. On a Cortex-M part that is the wrong way round. Refs #946, #543 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 39 ++++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index f3d94f34..f6aae872 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -461,18 +461,35 @@ enum Commands { #[arg(long, value_name = "FILE")] wcet_hints: Option, - /// #543 (Phase 1): mark a linear-memory segment as VOLATILE — the DMA - /// transfer window. Format `:`; both accept hex (`0x…`) or - /// decimal, e.g. `--volatile-segment 0x20001000:4096`. Repeatable to mark - /// more than one range. Names a region `[base, base+len)` of the fused + /// #543: mark a linear-memory segment as VOLATILE — the DMA transfer + /// window. Format `:`; both accept hex (`0x…`) or decimal, + /// e.g. `--volatile-segment 0x20001000:4096`. Repeatable to mark more + /// than one range. Names a region `[base, base+len)` of the fused /// linear memory that an external agent (the DMA engine, gale's - /// `own` handoff / decision DD-DMA-REGION-001) rewrites out-of-band, - /// so loads/stores inside it must eventually not be cached or reordered - /// across the transfer boundary. PHASE 1 = plumbing only: the ranges are - /// parsed and threaded to codegen but NOT yet consumed — the emitted bytes - /// are unchanged whether or not the flag is passed. The codegen back-off - /// (const-CSE + #468 base-CSE decline inside these ranges) is the gated - /// Phase 2. See rivet VCR-DMA-001. + /// `own` handoff / decision DD-DMA-REGION-001) rewrites + /// out-of-band, so loads/stores inside it must not be cached or + /// reordered across the transfer boundary. + /// + /// PASSING THIS FLAG COSTS CODE SIZE. Phase 2 has shipped: marking any + /// range makes the aliasing rewrites back off (const-CSE wholesale, + /// #468 base-CSE inside the window), so each constant is + /// re-materialized at every use rather than shared. Measured on + /// `scripts/repro/volatile_segment_543.wat`, `--cortex-m` on + /// `cortex-m4`: **36 B without the flag, 74 B with + /// `--volatile-segment 0x100:16`**. With both CSE levers already off + /// the flag changes nothing (98 B either way), which is what pins the + /// delta as exactly the back-off and not some other effect. + /// + /// So mark only the ranges an external agent really writes — this is + /// not a free annotation. Gated by `volatile_segment_phase2_543.rs` + /// (base-CSE window honoured, const-CSE declines wholesale, and the + /// gates are the identity when no range is marked). See rivet + /// VCR-DMA-001. + /// + /// #946: this text used to read "PHASE 1 = plumbing only … the emitted + /// bytes are unchanged whether or not the flag is passed", which + /// survived the Phase 2 landing and told users the opposite of the + /// truth about a flag that doubles code size. #[arg(long, value_name = "BASE:LEN")] volatile_segment: Vec,