Wave 1: Consolidate Foundations#14
Merged
Merged
Conversation
Prove highdigits_top, lowdigits_lowdigits, bigdigitsum_works, bigdigit_add_left, bigdigit_succ, and bigdigit_lowdigits. Zero sorry remaining in Common/Basic. Closes #1 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Prove the sorry placeholder for the decoder correctness lemma. Zero sorry remaining in Arm/Machine. Closes #2 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add Loader.lean with: - readBinaryFile: reads raw binary bytes from objcopy output - compareBytes/assertBytesFromFile: verify bytes match expected list - #load_bytes: elaboration-time command to display file bytes - Program.fromFile/fromFileVerified: create Programs from binary files - formatBytesAsLeanDef, hexDump: formatting utilities The loader is outside the TCB — byte lists in proof source are the ground truth (per June Lee's design rationale). Closes #6 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add decoder entries for: - MOVZ (Move Wide with Zero, 64-bit): supports hw shift positions - MUL (alias for MADD with Ra=XZR): 64-bit multiply Both instructions are needed for the sequence.ml tutorial (Phase 1). Closes #3 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Prove all 6 sorry placeholders in Sequence.lean: - 4 decode lemmas (ADD, ADD, MOVZ, MUL) - 2 chunk proofs (chunk1: two ADDs, chunk2: MOV+MUL) - Compositional verification via ensures_sequence Also add MOVZ and MUL decoder branches and restore arm_decode_of_bytes_loaded proof. Zero sorry remaining in entire project. Closes #4 Closes #5 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Remove addWithCarry, adcWithCarry, subWithBorrow, sbcWithBorrow from Word.lean (unused, Nat carry type was unsound) - Add @[simp] to bigdigit_zero, highdigits_zero, lowdigits_zero, lowdigits_trivial, highdigits_trivial, bigdigit_bound, lowdigits_bound - Add DecidableEq to Instruction deriving clause Closes #9, closes #10, closes #11 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Extract `advance_pc s s'` helper to eliminate 16 duplicated `.write_reg Reg.PC (s.read_reg Reg.PC + 4)` calls. Marked @[reducible] for proof transparency. Branch instructions (RET) set PC directly without advance_pc. Closes #12 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace all Word64.ofNat occurrences with BitVec.ofNat 64 across the codebase. Since Word64 is just an abbrev for BitVec 64, the wrapper added indirection without benefit. Also removes unused carry/borrow helper functions from Word.lean. Resolves #8. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The @[simp] annotation commit (9fa7847) accidentally regressed 6 proven theorems back to sorry. Restore proofs for highdigits_top, lowdigits_lowdigits, bigdigitsum_works, bigdigit_add_left, bigdigit_succ, and bigdigit_lowdigits. Zero sorry in codebase. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR continues the “Consolidate Foundations” work by simplifying the 64-bit word layer to use BitVec primitives directly, filling in previously sorry-based foundational bignum lemmas, and extending the ARM machine/tutorial infrastructure (decoder + loader + proof scripts).
Changes:
- Remove
Word64.val/Word64.ofNatwrappers and update downstream code to useBitVec.ofNat 64/.toNatdirectly. - Replace multiple
sorrys inBignum/Common/Basic/Lemmas.leanwith proof attempts and add[simp]attributes to core lemmas. - Extend ARM support: add MOVZ/MUL decoding, refactor PC advancement, add a binary
.textloader utility, and update tutorial proofs accordingly.
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| Bignum/Common/Word.lean | Drops Word64 conversion helpers; keeps Word64 := BitVec 64 and foundational toNat theorems. |
| Bignum/Common/Memory.lean | Migrates address arithmetic and word/byte conversions from Word64.ofNat/.val to BitVec.ofNat/.toNat. |
| Bignum/Common/Basic/Defs.lean | Marks several basic theorems as [simp] to improve proof automation. |
| Bignum/Common/Basic/Lemmas.lean | Replaces sorry with proof code for several bignum lemmas and rewrites the digit-sum lemma to use List.range sums. |
| Bignum/Arm/Tutorial/Simple.lean | Updates word constructions to BitVec.ofNat 64 and adjusts proof scripts. |
| Bignum/Arm/Tutorial/Sequence.lean | Updates word constructions and fills in decode lemmas + chunk correctness proofs. |
| Bignum/Arm/Machine/Loader.lean | Adds a raw-binary loader + byte verification tooling and an elaboration-time #load_bytes command. |
| Bignum/Arm/Machine/Instruction.lean | Adds advance_pc helper, derives DecidableEq for Instruction, and refactors step to use advance_pc. |
| Bignum/Arm/Machine/Decode.lean | Adds decoding support for MOVZ and MUL; updates examples and fills arm_decode_of_bytes_loaded. |
| Bignum/Arm/Machine.lean | Re-exports the new loader module. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Bump lean-toolchain from v4.28.0-rc1 to v4.30.0-rc2 and update all dependency revisions in lake-manifest.json. Replace `push_neg` with `push Not` (API rename in new toolchain) in Simple.lean, Sequence.lean, and Lemmas.lean. Fix `arm_decode_of_bytes_loaded` proof in Decode.lean to use `bv_omega` rewrites and `simp only`. Rewrite Loader.lean to parse Mach-O and ELF object files directly (no `objcopy`), adding `#load_obj` elaboration command and removing outdated tests/comments. Add BignumTests as a separate `lean_lib` target in lakefile.toml.
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
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.
No description provided.