Fix some sqrt things

1 files changed, 17 insertions, 0 deletions

diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 03590bf8c..c766d7ddf 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -365,6 +365,23 @@ Proof.
   intros; subst; apply mul_correct.
 Qed.
 
+(* Now that we have [pow], we can compute sqrt of -1 for use
+   in sqrt function (this is not needed unless the prime is
+   5 mod 8) *)
+Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb.
+
+Definition sqrt_m1 := Eval vm_compute in (pow (encode (F.of_Z _ 2)) (pow2_chain (Z.to_pos ((modulus - 1) / 4)))).
+
+Lemma sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F).
+Proof.
+  cbv [rep].
+  apply F.eq_to_Z_iff.
+  vm_compute.
+  reflexivity.
+Qed.
+
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb.
+
 Definition inv_sig (f : fe41417_32) :
   { g : fe41417_32 | g = inv_opt k_ c_ one_ f }.
 Proof.