diff options
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index a39755eee..16ce7a545 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -584,23 +584,23 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe25519) : - { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ one_ sqrt_m1 f}. +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. eexists. cbv [sqrt_5mod8_opt int_width]. - rewrite <- pow_correct. apply Proper_Let_In_nd_changebody; [reflexivity|intro]. set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. reflexivity. Defined. -Definition sqrt (f : fe25519) : fe25519 - := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). +Definition sqrt (powf powf_squared f : fe25519) : fe25519 + := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powf powf_squared f). -Definition sqrt_correct (f : fe25519) - : sqrt f = sqrt_5mod8_opt k_ c_ one_ sqrt_m1 f - := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). +Definition sqrt_correct (powf powf_squared f : fe25519) + : sqrt powf powf_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powf powf_squared f + := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powf powf_squared f). Definition pack_simpl_sig (f : fe25519) : { f' | f' = pack_opt params25519 wire_widths_nonneg bits_eq f }. |