docs(#945): correct a false claim we wrote, and stop a gate passing on nothing

.github/workflows/ci.yml

@@ -505,7 +505,31 @@ 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.
+        # `|| 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
+          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."
+          elif [ "$rc" -ne 0 ]; then
+            exit "$rc"
+          fi
         timeout-minutes: 10
 
   cmp-select-oracle:

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:

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<Vec<u8>> {
         let dm_num = vfp_dreg_to_num(dm)?;
         if dm_num > 7 {

crates/synth-cli/src/main.rs

@@ -461,18 +461,35 @@ enum Commands {
         #[arg(long, value_name = "FILE")]
         wcet_hints: Option<PathBuf>,
 
-        /// #543 (Phase 1): mark a linear-memory segment as VOLATILE — the DMA
-        /// transfer window. Format `<base>:<len>`; 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 `<base>:<len>`; 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<buffer>` 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<buffer>` 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<String>,