RQ-59-CRSWEEP (#242): 11 critical/high findings verified — 10 stale, 1 CONFIRMED REAL and executing (#1021) - #1031
Open
avrabe wants to merge 1 commit into
Open
RQ-59-CRSWEEP (#242): 11 critical/high findings verified — 10 stale, 1 CONFIRMED REAL and executing (#1021)#1031avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
…LL REAL (CR-H7 / #1021) Committed by the hub coordinator: the lane stalled with 8 hours of uncommitted work and zero commits. NOT REVIEWED by me beyond gate-checking. claim_check 49/49 and the YAML parses at this commit. THE HEADLINE IS THE ONE THAT DID NOT CLOSE. CR-H7 "Popcnt clobbers R11" is CONFIRMED STILL REAL at HEAD and it EXECUTES — a live memory-safety miscompile in shipped v0.58.0, filed as #1021: The Thumb-2 i32 Popcnt expansion takes R11 as a second scratch ("We need a second scratch register. Use R11.", six R11 writes); R11 is the WASM linear memory base. The A32 transcription (#615) deliberately mirrors the same register contract and inherits the defect. Execution differential (unicorn vs wasmtime), --cortex-m: f(0xFF) expected 1242, observed 0x20020008 — popcnt(0xFF)=8 plus the word at address 0 (the vector table's initial SP), because R11 ended as r5>>16 = 0. R11 also LEAKS to the caller (it is not in the pushed set), so every later [R11] access in the whole call chain is wrong too. i64.popcnt is unaffected (R3/R4/R5/R12, all pushed). Reachable from BOTH selector paths. ARCHITECTURAL NOTE worth carrying: the Rocq-proved `rule_i32_popcnt` emits the `ArmOp::Popcnt` PSEUDO-OP, and the defect is in that pseudo-op's ENCODER EXPANSION. The proof is stated at pseudo-op tier, ABOVE the expansion — so a genuine proof sits above a defective lowering and cannot see it. The other 10 findings verified as already fixed, with repro evidence per entry. Refs #242, #1021.
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.
All 11
proposedcritical/high findings incode-review-findings.yamlverified against the current binary, not by reading code or trusting the tracker.Result: 10 stale, 1 real
The board was advertising eleven open critical/high defects. Ten were records that had stopped being true — the same class the last six releases kept finding, one level up, and it matters because v0.58 made release readiness a query over rivet statuses.
But the sweep's value is the one that didn't close.
🔴 CR-H7 —
i32.popcntclobbers R11, and it executesFiled as #1021, scoped into v0.59 as
RQ-59-POPCNT(#1030).The Thumb-2
i32.popcntexpansion takes R11 as a second scratch — its own comment says "We need a second scratch register. Use R11.", six R11 writes — and R11 is the WASM linear memory base. The A32 transcription (#615) deliberately mirrors "the Thumb-2 arm's register contract (R11 + R12 as scratch)" and inherits it.Executed differential,
--cortex-m:12420x20020008popcnt(0xFF)=8plus the word at address 0 — the vector table's initial SP — because R11 ended asr5>>16 = 0. The expansion's last R11 write islsr.w r11, r5, #16; the followingldr.w r6, [r11]reads through it.R11 is not in the pushed set, so it leaks to the caller — every later
[R11]access in the whole call chain is wrong too. Reachable from both selector paths.i64.popcntis unaffected (R3/R4/R5/R12, all pushed).Why this is the argument for verifying rather than closing
The tempting disposition for eleven months-old
proposedentries is to close them as stale. Ten of them were. Doing that would have closed a live memory-safety miscompile along with them — and it had been sitting in an artifact nobody trusted precisely because it was surrounded by stale ones.Absence of a repro is not evidence of a fix. Each of the ten closures carries its repro command and observed result.
claim_check49/49. Rivet artifact only, no code.Refs #242, #1021.