Skip to content

v0.35.0 — North-Star wave: verified i64 pair rules, Sail/ASL bridge, falsification gate

Choose a tag to compare

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

The verified selector DSL enters the i64 pair family (27 rules / 27 Qed — ~40% of integer-compute ops DSL-served); Track B unblocks with Sail/ASL bridge lemmas proving our NZCV flag semantics equal to ARM's own spec; the VCR-VER-001 falsification gate is demonstrated.

Added

  • VCR-SEL-001 increment 3 (#661): i64 add/sub/and/or/xor + eqz as verified rules — pair-result T1 theorems, the #632 clobber class encoded as aliasing hypotheses AND runtime Err. Anchors green even with SYNTH_SEL_DSL=1.
  • VCR-ISA-001 spike (#660): GO on transcribe-and-bridge — SailArmBridge.v (23 Qed) proves ADD/ADDS/CMP + all four flag computations equal to hand-transcribed sail-arm (ASL-derived) semantics with file:line provenance. Import of the generated 42 MB Coq model: NO-GO. ~0.5–1 day per remaining op class.
  • VCR-VER-001 demonstrated (#659): the #209 cost-gate reversal recorded as the passing instance; the #496 reversal is correctness-complete but cycle-regressive on i32 shapes — missing capability named: post-exhaustion code quality.

Fixed

  • RV32 bounds/mask soundness (#655, PR #658): offset-before-mask (the #651 twin) + audit finding: i64 loads/stores had NO guard in either mode — both now guard the full 8-byte access.

Platform binaries attach ~10 min after the tag.

🤖 Generated with Claude Code

Assets 13
Loading