Finished sqrt in GF25519

2 files changed, 58 insertions, 7 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 878b62abe..2d4bb525f 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -991,8 +991,6 @@ Section SquareRoots.
     etransitivity.
     Focus 2. {
       apply if_equiv. {
-        etransitivity.
-        Focus 2. {
         apply eqb_Proper; [ | reflexivity ].
         transitivity (carry_mul_opt k_ c_ (pow_opt k_ c_ one_ us chain) (pow_opt k_ c_ one_ us chain)); [ reflexivity | ].
         cbv [eq].
@@ -1000,11 +998,6 @@ Section SquareRoots.
         rewrite carry_mul_rep by reflexivity.
         rewrite mul_rep by reflexivity.
         f_equal; apply pow_opt_correct; auto.
-        } Unfocus.
-        cbv [ModularBaseSystem.eqb freeze].
-        rewrite <-!from_list_default_eq with (d := 0).
-        erewrite <-!freeze_opt_correct by eauto using length_to_list.
-        reflexivity.
       } {
         apply pow_opt_correct; auto.
       } {
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index bf7811b86..2816a07cc 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -394,6 +394,64 @@ Proof.
   assumption.
 Defined.
 
+Definition fieldwiseb_sig (f g : fe25519) :
+  { b | b = @fieldwiseb Z Z 10 Z.eqb f g }.
+Proof.
+  cbv [fe25519] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv.
+  reflexivity.
+Defined.
+
+Definition fieldwiseb (f g : fe25519) : bool
+  := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in proj1_sig (fieldwiseb_sig f g).
+
+Definition fieldwiseb_correct (f g : fe25519)
+  : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g
+  := Eval cbv beta iota delta [proj2_sig fieldwiseb_sig] in proj2_sig (fieldwiseb_sig f g).
+
+Definition eqb_sig (f g : fe25519) :
+  { b | b = eqb f g }.
+Proof.
+  cbv [eqb].
+  cbv [fe25519] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv [ModularBaseSystem.freeze].
+  rewrite <-!from_list_default_eq with (d := 0).
+  rewrite <-!(freeze_opt_correct c_) by auto using length_to_list.
+  rewrite <-!freeze_correct.
+  rewrite <-fieldwiseb_correct.
+  reflexivity.
+Defined.
+
+Definition eqb (f g : fe25519) : bool
+  := Eval cbv beta iota delta [proj1_sig eqb_sig] in proj1_sig (eqb_sig f g).
+
+Definition eqb_correct (f g : fe25519)
+  : eqb f g = ModularBaseSystem.eqb f g
+  := Eval cbv beta iota delta [proj2_sig eqb_sig] in proj2_sig (eqb_sig f g).
+
+Definition sqrt_sig (f : fe25519) :
+  { f' : fe25519 | f' = sqrt_5mod8_opt k_ c_ one_ sqrt_m1 f}.
+Proof.
+  eexists.
+  cbv [sqrt_5mod8_opt].
+  apply Let_In_ext.
+  intros.
+  do 2 rewrite <-mul_correct.
+  rewrite <-eqb_correct.
+  reflexivity.
+Defined.
+
+Definition sqrt (f : fe25519) : fe25519
+  := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig 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 pack_simpl_sig (f : fe25519) :
   { f' | f' = pack_opt params25519 wire_widths_nonneg bits_eq f }.
 Proof.