diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 01:21:29 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 01:24:25 -0500 |
| commit | a408ad1ff2cd5ebc694ff8f5515922256b3beb2d (patch) | |
| tree | 85658d41df624297fe915f303fa104c35464c6c8 /src/Experiments | |
| parent | 3049b95b62e80cb15a203879a5a610aa720aae4a (diff) | |
Add mulW_noinline
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 5c107eb39..2cd70a3b4 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1382,6 +1382,10 @@ Local Ltac prove_bounded_by := => apply GF25519Bounded.mulW_correct_and_bounded | [ |- GF25519BoundedCommon.is_bounded (GF25519BoundedCommon.fe25519WToZ + (GF25519Bounded.mulW_noinline _ _)) = true ] + => apply GF25519Bounded.mulW_correct_and_bounded + | [ |- GF25519BoundedCommon.is_bounded + (GF25519BoundedCommon.fe25519WToZ (GF25519Bounded.powW _ _)) = true ] => apply GF25519Bounded.powW_correct_and_bounded | [ |- context[GF25519BoundedCommon.fe25519WToZ (GF25519BoundedCommon.fe25519ZToW _)] ] @@ -1410,7 +1414,7 @@ Proof. rewrite ModularBaseSystemProofs.encode_rep. symmetry. eapply @ModularBaseSystemProofs.sqrt_5mod8_correct; - eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519; [ reflexivity | + eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519; [ reflexivity | lazymatch goal with | |- appcontext[GF25519Bounded.powW ?a ?ch] => let A := fresh "H" in @@ -1420,8 +1424,9 @@ Proof. | rewrite A; rewrite GF25519.pow_correct, ModularBaseSystemOpt.pow_opt_correct by reflexivity] - end..]; + end..]; [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW by (eapply GF25519BoundedCommon.is_bounded_proj1_fe25519); reflexivity | ]. + unfold GF25519Bounded.mulW_noinline. match goal with | |- appcontext[GF25519Bounded.mulW ?a ?b] => let A := fresh "H" in @@ -1456,7 +1461,7 @@ Proof. intros. pose proof sqrt_correct' (GF25519BoundedCommon.encode x) as H. rewrite GF25519BoundedCommon.decode_encode in H; exact H. Qed. - + Local Instance Proper_sqrt : Proper (GF25519BoundedCommon.eq ==> GF25519BoundedCommon.eq) GF25519Bounded.sqrt. @@ -1620,4 +1625,4 @@ Print Assumptions three_correct. (* [B_order_l] is proven above in this file, just replace Admitted with Qed, start the build and wait for a couple of hours *) (* [prime_q] and [prime_l] have been proven in Coq exactly as stated here, see <https://github.com/andres-erbsen/safecurves-primes> for the (lengthy) proofs *) (* [SHA512] is outside the scope of this project, but its type is satisfied by [(fun n bits => Word.wzero 512)] *) -Definition __check_SHA512_type := [(fun n bits => Word.wzero 512); SHA512].
\ No newline at end of file +Definition __check_SHA512_type := [(fun n bits => Word.wzero 512); SHA512]. |