diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-01 17:32:06 -0400 |
|---|---|---|
| committer |  jadep <jade.philipoom@gmail.com> | 2016-11-02 15:23:46 -0400 |
| commit | be02e665fe86ef81a30c18577d82ff58c8bc0441 (patch) | |
| tree | a11e58529add4cc238af497e77ed2c05836ce952 /src | |
| parent | f670e48c3b74fbb3a9f21d6c9351b08593af311f (diff) | |
Fix [sqrtW_sig]
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 49e800396..64c6151c3 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -176,14 +176,14 @@ Definition sqrt_m1W : fe25519W := Eval vm_compute in fe25519ZToW sqrt_m1. Definition GF25519sqrt x : GF25519.fe25519 := - dlet powx := powW (fe25519ZToW x) (chain GF25519.sqrt_ec) in - GF25519.sqrt (fe25519WToZ powx) (fe25519WToZ (mulW powx powx)) x. + dlet powx := GF25519.pow x (chain GF25519.sqrt_ec) in + GF25519.sqrt powx (GF25519.mul powx powx) x. Definition sqrtW_sig : { sqrtW | iunop_correct_and_bounded sqrtW GF25519sqrt }. Proof. eexists. - unfold GF25519.sqrt. + unfold GF25519sqrt, GF25519.sqrt. intros; set_evars; rewrite <- (fun pf => proj1 (powW_correct_and_bounded _ _ pf)) by assumption; subst_evars. match goal with | [ |- context G[dlet x := fe25519WToZ ?v in @?f x] ] @@ -196,6 +196,10 @@ Proof. Focus 2. { apply Proper_Let_In_nd_changebody_eq; intros. set_evars. + match goal with (* unfold the first dlet ... in, but only if it's binding a var *) + | [ |- ?x = dlet y := fe25519WToZ ?z in ?f ] + => is_var z; change (x = match fe25519WToZ z with y => f end) + end. change sqrt_m1 with (fe25519WToZ sqrt_m1W). rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded a a X Y)), <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ) @@ -229,7 +233,7 @@ Definition sqrtW (f : fe25519W) : fe25519W := Eval cbv [proj1_sig sqrtW_sig app_fe25519W] in app_fe25519W f (proj1_sig sqrtW_sig). -Lemma sqrtW_correct_and_bounded : iunop_correct_and_bounded sqrtW GF25519.sqrt. +Lemma sqrtW_correct_and_bounded : iunop_correct_and_bounded sqrtW GF25519sqrt. Proof. intro f. set (f' := f). @@ -303,7 +307,7 @@ Lemma pow_correct (f : fe25519) chain : proj1_fe25519 (pow f chain) = GF25519.po Proof. op_correct_t pow (powW_correct_and_bounded chain). Qed. Lemma inv_correct (f : fe25519) : proj1_fe25519 (inv f) = GF25519.inv (proj1_fe25519 f). Proof. op_correct_t inv invW_correct_and_bounded. Qed. -Lemma sqrt_correct (f : fe25519) : proj1_fe25519 (sqrt f) = GF25519.sqrt (proj1_fe25519 f). +Lemma sqrt_correct (f : fe25519) : proj1_fe25519 (sqrt f) = GF25519sqrt (proj1_fe25519 f). Proof. op_correct_t sqrt sqrtW_correct_and_bounded. Qed. Import Morphisms. |