chore(release): v0.8.0 — honest i64 verification foundation#151
Merged
Conversation
Bumps workspace version 0.7.0 → 0.8.0 and promotes the [Unreleased] section to [0.8.0] with the re-framed theme and falsification statement. Sweeps the 23 intra-workspace path-dep version pins to 0.8.0 (per the lesson from v0.7.0's release-tail) and bumps MODULE.bazel module version. Theme: aligned Compilation.v model + i64 proof tooling, not the originally-scoped T1 parity. Re-framed honestly because the falsification clause from the umbrella (#147) explicitly forbade shipping T1 proofs against a simplified model that "proves a different operation than the compiler emits" — which is what PR #149's clean-room check surfaced. v0.9.0 picks up the actual T2→T1 promotions against the now-aligned model. PRs included: #148 docs(v0.8.0): defer F64↔I64 conversions — ARMv7-M FPv5 has no 64-bit VCVT #150 feat(coq): align Compilation.v i64 ops with real Rust codegen #149 feat(coq): i64 tactics + flag-correspondence lemmas (foundation)
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.8.0] - 2026-05-26with re-framed theme + falsification statementWhy the theme changed mid-release
The originally-scoped theme ("i64 T1 parity", umbrella #147) was caught by its own falsification clause. A clean-room check of PR #149 (the foundation PR) surfaced that
coq/Synth/Synth/Compilation.vmodeled i64 ops as single 32-bit ARM instructions while the real Rust compiler emits properADDS R0,R0,R2; ADC R1,R1,R3register-pair sequences. Per the umbrella's falsification clause, T1 proofs against the simplified model "prove a different operation than the compiler emits" — disqualifying.Rather than overclaim, v0.8.0 ships the aligned model + proof tooling layer that makes the actual T1 lifts honest. v0.9.0 picks up the T2→T1 promotions against the now-correct model.
PRs included
Net verification delta
Falsification statement
v0.8.0 is wrong if:
Compilation.vclauses don't match what the Rust compiler emits (cross-check againstdocs/analysis/I64_CODEGEN_SURVEY.md)bazel test //coq:verify_proofsgoes red on a clean v0.8.0 checkoutTest plan
v0.8.0, release.yml ships the 10-asset GitHub Release (4 binary tarballs + SHA256SUMS + 3 cosign artifacts + build-env.txt + toolchain SBOM)publish-to-crates-io.ymlrepublishes the workspace at 0.8.0 viaCARGO_REGISTRY_TOKEN