Skip to content

v0.37.0 — the certifying validator reaches the shipped bytes

Choose a tag to compare

View all tags
@avrabe avrabe released this 08 Jul 22:32
· 505 commits to main since this release
v0.37.0
ebf06cb
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Expansion-level certifying validation (#667 move 2): the validator now checks the encoder's OWN emitted instruction sequences for 20 i64 pseudo-ops — encoder↔validator drift is unrepresentable by construction.

Added

  • expansion_validator (PR #674): Thumb-2 subset decoder (loud Err on unmodeled encodings) + guarded symbolic executor (forward-branch path conditions, IT predication, NZCV, scratch-stack model) + per-op UNSAT(wasm ≠ sequence) via ordeal with LRAT certificates, wired into synth verify. Certified: I64Mul, the I64SetCond family, Clz/Ctz/Popcnt, shifts, rotates (through the #610 fixed-ABI wrappers). Red on the literal #632 bug shape (counterexample). Held out loudly: div/rem loops — backward branches are a decode error; loop support is the named next increment.

Platform binaries attach ~10 min after the tag.

🤖 Generated with Claude Code

Assets 13
Loading