diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-11-03 14:23:41 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-11-03 14:24:03 -0400 |
| commit | e094a3f049444dd4db93b0862b2b9ff847677aa8 (patch) | |
| tree | edf6e5660bd393bdbd0d1cc760b87422f84f4cec /src/Specific/GF25519.v | |
| parent | 690d35a9f418fd3cf03ec7c746e201ebaa2fc1a0 (diff) | |
Make [freeze] proofs consider machine integer width and hard input bounds separately
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 16ce7a545..0a487b1e2 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -22,7 +22,8 @@ Local Open Scope Z. Definition modulus : Z := Eval compute in 2^255 - 19. Lemma prime_modulus : prime modulus. Admitted. -Definition int_width := 32%Z. +Definition int_width := 64%Z. +Definition freeze_input_bound := 32%Z. Instance params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. @@ -46,7 +47,7 @@ Instance carryChain : CarryChain limb_widths. contradiction H. Defined. -Definition freezePreconditions25519 : freezePreconditions params25519 int_width. +Definition freezePreconditions25519 : FreezePreconditions freeze_input_bound int_width. Proof. constructor; compute_preconditions. Defined. @@ -584,7 +585,6 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Print sqrt_5mod8_opt. Definition sqrt_sig (powf powf_squared f : fe25519) : { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powf powf_squared f}. Proof. |