Delete Lean modules that nothing uses - #590
Merged
Merged
Conversation
Remove proofs, and the code they alone verified, that no registration
file, generic file, variant or test reaches:
* Proof/Poly1305/AArch64/{Update,Finalize}: the radix-26 update and
finalize proofs, superseded by Radix64 (the artifact registers only
Radix64's), with their code literals in Proof/Poly1305/AArch64/Lit.
* Proof/X448/AArch64/{Verified,Lit}: the non-Weak x448 artifact proof;
only Weak is registered.
* Proof/ChaCha20/AArch64/Neon/{Block,Quarter,RoundSpec,Rounds} and
Impl/ChaCha20/AArch64/Neon: the single-block NEON implementation,
never registered. Neon/Lanes stays (Neon4 uses its lemmas) and no
longer imports the deleted code.
* Proof/MlKem/X86_64/PairOut: unused loop lemmas.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016m94ApXKUeS9mmGwopxjrB
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
2 participants
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
Deletes proofs and code that nothing reaches: no registration file, generic file, variant or test imports them, directly or indirectly.
lake buildstill checks them today, because the library's glob builds every module underVerifiedGarbage.*, so they cost CI time without verifying anything that ships.These were found while reviewing the repo for duplication that points to missing abstractions; the dead copies were a by-product of that review.
Removed: 12 files, 1,677 lines deleted, 0 added
Proof/Poly1305/AArch64/{Update,Finalize}.lean(about 1,150 lines): radix-26update/finalizeproofs. The AArch64 artifact registers only theRadix64code and proofs. Theirmaterialize_codeliterals inProof/Poly1305/AArch64/Lit.leango too, since only they used them.Proof/X448/AArch64/{Verified,Lit}.lean: the non-Weakx448artifact proof.Artifacts/X448/AArch64.leanregisters onlyWeak.Proof/ChaCha20/AArch64/Neon/{Block,Quarter,RoundSpec,Rounds}.leanandImpl/ChaCha20/AArch64/Neon.lean: a single-block NEON implementation and its proof, never registered.Neon/Lanes.leanstays, becauseNeon4/Rounds.leanuses its lemmas.Lanesno longer imports the deleted code, which it never used.Proof/MlKem/X86_64/PairOut.lean: unused loop lemmas.How the dead modules were found: a script built the import graph from every root and listed the modules no root reaches. The roots are
Artifacts/,Generic/,Variants/,TCB/,VerifiedGarbageTest/and the top-levelEmit.lean,CheckEd25519.leanandVerifiedGarbage.lean.Deliberately kept, though no root imports them:
Spec/MlKem/Expanded.lean: a spec awaiting its implementation.Follow-ups (not in this PR): some dead theorems sit inside modules that are still live.
Proof/X448/AArch64/Main.lean'scorrectproves the superseded non-Weakx448. It is the only reasonMainimportsLadder,FinalSwapandInv.Proof/Poly1305/AArch64/Blocks.leanproves the radix-26blocks. TheRadix64proofs import it for shared lemmas only.Cutting these needs the shared parts split out first; it is left for a separate change.
No changes to
Spec/orTCB/. The generatedsrc/asm/is unchanged, since none of the deleted code was registered.Validation
lake buildof every registration file that imports an edited module, plus what they import: 1,399 modules, all passing.Artifacts/{Poly1305,X448,ChaCha20}/AArch64Artifacts/MlKem/X86_64Generic/ChaCha20Xor/AArch64/ChaCha20Poly1305python3 ci/check_lean_imports.pyandpython3 ci/check_lean_speed.pypass.lake buildandEmit.lean --check. CI runs both.🤖 Generated with Claude Code
https://claude.ai/code/session_016m94ApXKUeS9mmGwopxjrB
Generated by Claude Code