chore(release): v0.9.0 — i64 T1 result-correspondence lifts#158
Merged
Conversation
Bumps workspace version 0.8.0 → 0.9.0 and sweeps the intra-workspace path-dep version pins (per the saved v0.7.0 release-tail lesson) plus MODULE.bazel. Promotes the [Unreleased] section to [0.9.0] with theme re-framing and the v0.9.0 falsification statement. Theme: v0.9.0 picks up what v0.8.0's honest-foundation release set up. 26 new _spec axioms layered on the 26 type-only axioms from v0.8.0, then 30 T2 i64 theorems lifted to T1 + 5 v0.8.0 admits discharged. Net: 35 new i64 T1 Qeds; 5 honest Admitted carry-overs (Add/Sub on ADDS/ADC carry-prop; And/Or/Xor on Rocq 9 Z.mod_mod halves-distribute). PRs included: #153 feat(coq): i64 pseudo-op result-correspondence axioms + discharge 5 v0.8.0 admits #154 feat(coq): i64 arithmetic + bitwise T1 lifts #155 feat(coq): i64 comparison T1 lifts #156 feat(coq): i64 shifts + rotates T1 lifts #157 feat(coq): i64 bit-manip T1 lifts
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.
Summary
[Unreleased]→[0.9.0] - 2026-05-27Theme
i64 T1 result-correspondence parity (modulo five named follow-ups). v0.8.0 set the table with the aligned
Compilation.vand the type-only pseudo-op axioms. v0.9.0 lays the value-correspondence layer (26 new_specaxioms), lifts 30 T2 theorems to T1, and discharges the 5 admits v0.8.0 carried over.PRs merged
Z.mod_modhalves-distribute rework)Net verification delta
Falsification statement
v0.9.0 is wrong if:
bazel test //coq:verify_proofsgoes red on a clean v0.9.0 checkout_specaxiom claims a result the Rust codegen does not actually produce (cross-checked againstdocs/analysis/I64_CODEGEN_SURVEY.md)Test plan
v0.9.0, release.yml ships the 10-asset GitHub Releasepublish-to-crates-io.ymlrepublishes the workspace at 0.9.0