Skip to content

v0.37.1 — i32 register shifts obey WASM mod-32 semantics (#682)

Choose a tag to compare

View all tags
@avrabe avrabe released this 10 Jul 10:57
· 502 commits to main since this release
v0.37.1
7a9222d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

i32.shl/shr_s/shr_u with amounts >= 32 silently compiled to 0/sign on both direct selectors — a latent hand-written bug the verified-selector DSL had faithfully mirrored, with a Rocq proof that was vacuous against real hardware (exactly the model divergence the Sail/ASL bridge documented as gaps 6–7).

Fixed

  • #682 (PR #683): AND R12, rm, #31 before every register-controlled i32 shift on both direct selectors (the optimized bridge always masked — never affected); DSL rules re-proved with the mask + rs != rn side condition; Compilation.v aligned; ROR exempt (cyclic) and pinned. Red→green: 8 mismatches → 0; new CI oracle. Deliberate byte change with the full refreeze ritual (23 differentials green before 13 re-pins; constant shift amounts imm-fold and are unaffected). The honest ArmSemantics Rm[7:0] fix rides the flat-executor follow-up.
  • rust-1.97 clippy drift (PR #684).

Platform binaries attach ~10 min after the tag.

🤖 Generated with Claude Code

Assets 13
Loading