Fix some sqrt things

11 files changed, 82 insertions, 14 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 055c5fa72..778c3b3ed 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe25519W :=
+Definition sqrt_m1W' : fe25519W :=
   Eval vm_compute in fe25519ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519W_word64ize sqrt_m1W'.
 
 Definition GF25519sqrt x : GF25519.fe25519 :=
   dlet powx := powW (fe25519ZToW x) (chain GF25519.sqrt_ec) in
diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index fd11aea5d..7aeb5fd45 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe2213_32W :=
+Definition sqrt_m1W' : fe2213_32W :=
   Eval vm_compute in fe2213_32ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe2213_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe2213_32W_word64ize sqrt_m1W'.
 
 Definition GF2213_32sqrt x : GF2213_32.fe2213_32 :=
   dlet powx := powW (fe2213_32ZToW x) (chain GF2213_32.sqrt_ec) in
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index 084e5ec57..d1db7fd83 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_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 : fe2519_32) :
   { g : fe2519_32 | g = inv_opt k_ c_ one_ f }.
 Proof.
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index eb18c7aa7..b49228967 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe2519_32W :=
+Definition sqrt_m1W' : fe2519_32W :=
   Eval vm_compute in fe2519_32ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe2519_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe2519_32W_word64ize sqrt_m1W'.
 
 Definition GF2519_32sqrt x : GF2519_32.fe2519_32 :=
   dlet powx := powW (fe2519_32ZToW x) (chain GF2519_32.sqrt_ec) in
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 4c015d25c..264d7c3d3 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe25519_32W :=
+Definition sqrt_m1W' : fe25519_32W :=
   Eval vm_compute in fe25519_32ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_32W_word64ize sqrt_m1W'.
 
 Definition GF25519_32sqrt x : GF25519_32.fe25519_32 :=
   dlet powx := powW (fe25519_32ZToW x) (chain GF25519_32.sqrt_ec) in
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index a103cf9ec..35ad2ee01 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe25519_64W :=
+Definition sqrt_m1W' : fe25519_64W :=
   Eval vm_compute in fe25519_64ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_64W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64W_word64ize sqrt_m1W'.
 
 Definition GF25519_64sqrt x : GF25519_64.fe25519_64 :=
   dlet powx := powW (fe25519_64ZToW x) (chain GF25519_64.sqrt_ec) in
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.
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index 7e4449912..53ee754f2 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe41417_32W :=
+Definition sqrt_m1W' : fe41417_32W :=
   Eval vm_compute in fe41417_32ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe41417_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe41417_32W_word64ize sqrt_m1W'.
 
 Definition GF41417_32sqrt x : GF41417_32.fe41417_32 :=
   dlet powx := powW (fe41417_32ZToW x) (chain GF41417_32.sqrt_ec) in
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index bca4d1050..0c28bf575 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_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 : fe5211_32) :
   { g : fe5211_32 | g = inv_opt k_ c_ one_ f }.
 Proof.
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index 0e5645ae1..74480a0d1 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -286,9 +286,9 @@ Proof.
   exact (proj2_sig (eqbW_sig f' g')).
 Qed.
 
-(* TODO(jgross): use NToWord or such for this constant too *)
-Definition sqrt_m1W : fe5211_32W :=
+Definition sqrt_m1W' : fe5211_32W :=
   Eval vm_compute in fe5211_32ZToW sqrt_m1.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe5211_32W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe5211_32W_word64ize sqrt_m1W'.
 
 Definition GF5211_32sqrt x : GF5211_32.fe5211_32 :=
   dlet powx := powW (fe5211_32ZToW x) (chain GF5211_32.sqrt_ec) in
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index 5c78316a1..09a0874bd 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -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 : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }.
 Proof.