Changes to sqrt for easier bounds proofs; currently blocked on broken proof in GF25519Bounded

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 }.