99 verify mul #845
Open
99 verify mul #845
Conversation
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
Claude eliminated the assume from lemma_carry_propagation_is_division no cleaning done yet, it is possible that there are redundancies, unused lemmas/asserts Claude proposes a refactoring for lemma_carry_propagation_is_division rm redundancies part 1 rm redundancies part 2 mv unused lemmas simplify lemma_small_div no more assumes in telescoping div rm redundant lemma_u64_shr_is_div simplify lemma_div_converse mv div lemmas to common_verus no assumes in lemma_to_bytes_reduction, cleaning comes next
<!-- Please ensure that your PR includes the following, as needed --> - [ ] Source code modifications **highlighted and justified** - [ ] Proof cheats (`assume(false)`, `sorry`, etc.) **highlighted and justified** Removes 2 unused lemmas and creates backend_u64_core. Closes #205.
For the "Counts Over Time" chart: - improved visibility of latest commits: the jump to a new plateau was not clearly visible - excluded external body specs from green line <!-- Please ensure that your PR includes the following, as needed --> - [ n/a] Source code modifications **highlighted and justified** - [ n/a] Proof cheats (`assume(false)`, `sorry`, etc.) **highlighted and justified**
<!-- Please ensure that your PR includes the following, as needed --> - [ ] Source code modifications **highlighted and justified** - [ ] Proof cheats (`assume(false)`, `sorry`, etc.) **highlighted and justified** Cascades a few proofs in tolevel `scalar.rs`. closes #183
Initial commit for solving the mul(a: &Scalar52, b: &Scalar52)
I had some issues using that limbs_bound lemma, claude suggested that work-around.
Replaced assume(false) with actual proofs in three functions: - mul(a, b): Scalar multiplication via two-step Montgomery reduction - square(self): Scalar squaring using same Montgomery pattern - as_montgomery(self): Convert to Montgomery form Verification approach: - Treats montgomery_reduce specification as axiom - Uses lemma_mul_montgomery_chain to prove ((a×b)/R × R²)/R = a×b mod L - Proves algorithm structure correct via modular arithmetic Introduces 3 axioms in scalar_lemmas.rs (tested necessary): 1. lemma_modular_cancellation_power_of_2: Number theory basic result 2. lemma_r_value: R = 2^260 mod L (Verus by(compute_only) failed) 3. lemma_rr_equals_r_squared: RR = R² mod L (Verus by(compute_only) failed) Plus lemma_rr_limbs_bounded (Verus visibility workaround) Adds vstd::arithmetic::mul import in scalar.rs for proven modular arithmetic lemmas.
|
Whoops, I think this PR should be opened against https://github.com/Beneficial-AI-Foundation/dalek-lite instead |
2 tasks
|
I've opened Beneficial-AI-Foundation#242 Anyone with the permissions to close this PR (i.e. #845), feel free to do so |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 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.
Replaced assume(false) with actual proofs in three functions (scalar.rs):
Verification approach:
Introduces 3 axioms in scalar_lemmas.rs (tested necessary):
Plus lemma_rr_limbs_bounded (Verus visibility workaround)
Adds vstd::arithmetic::mul import in scalar.rs for proven modular arithmetic lemmas.