diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 28ef33b8..0e59a65c 100644 --- a/.github/workflows/ci.yml +++ b/.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: 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/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: 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 { 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,