docs(#945): correct a false claim we wrote, and stop a gate passing on nothing - #945
Merged
Conversation
… passing on nothing
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
…irst
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
force-pushed
the
fix/doc-truth-corrections-945
branch
from
August 11, 2026 20:33
b04425b to
4325dea
Compare
… false one
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
`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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Contributor
Author
|
Note for review: the |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
From a doc-vs-source sweep (~430 claims examined mechanically, 10 genuine disagreements). This PR carries the two that are ours and consequential; the rest are filed as #945.
1. We called the official testsuite "absent". It is present, runnable, and unrun.
RQ-56-CONFsaid the official WebAssembly testsuite was absent — written by this project three days ago, and false.tests/spec-testsuiteis a checked-out submodule at3453673with 257.wastfiles, andtests/spec/BUILD.bazelhas targets consuming it.The true statement is worse. Three states coexist in the tree:
README.md:122,FEATURE_MATRIX:122spec-testsuitezero times2. That CI step passed while selecting nothing
Bazel exit 4 = NO TESTS MATCHED. The
||swallowed it, so the step reported success having run nothing — the exact vacuity class this release is named for, sitting inside the gate list.An empty Renode matrix is still tolerated (the emulator isn't always available), but it now emits a
::warning::and states it is TOLERATED-EMPTY rather than passing silently.3. Scope statuses advanced
RQ-56-CITEandRQ-56-PSAFEmoveproposed→implemented; both deliverables are ancestors oforigin/main(#927, #934).The sweep caught the release-scope artifact not being advanced as items land — the same drift as
status: implementedon unimplemented work, inverted. It would have made the readiness query lie in the safe-looking direction, which is the harder one to notice.claim 43/43 · citations 0 false claims · rivet ours-errors 0.