From e6c07d9cd3cf14ff28b3d3daa9942f9fe2fa90dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Nov 2016 20:47:58 -0500 Subject: Update sqrtm1 for 3mod4 --- src/SpecificGen/GF2519_32.v | 8 -------- src/SpecificGen/GF41417_32.v | 8 -------- src/SpecificGen/GF5211_32.v | 8 -------- src/SpecificGen/GFtemplate3mod4 | 8 -------- 4 files changed, 32 deletions(-) (limited to 'src/SpecificGen') diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v index d1db7fd83..d64b24088 100644 --- a/src/SpecificGen/GF2519_32.v +++ b/src/SpecificGen/GF2519_32.v @@ -372,14 +372,6 @@ Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb 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) : diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v index c766d7ddf..61c13766b 100644 --- a/src/SpecificGen/GF41417_32.v +++ b/src/SpecificGen/GF41417_32.v @@ -372,14 +372,6 @@ Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb 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) : diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v index 0c28bf575..2a40a932d 100644 --- a/src/SpecificGen/GF5211_32.v +++ b/src/SpecificGen/GF5211_32.v @@ -372,14 +372,6 @@ Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb 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) : diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 index 09a0874bd..ccee86d1a 100644 --- a/src/SpecificGen/GFtemplate3mod4 +++ b/src/SpecificGen/GFtemplate3mod4 @@ -372,14 +372,6 @@ Local Transparent Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb 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}}}) : -- cgit v1.2.3