diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 20:47:58 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 20:47:58 -0500 |
| commit | e6c07d9cd3cf14ff28b3d3daa9942f9fe2fa90dd (patch) | |
| tree | 448b13272bab774e59b38207d582ae4e5bf9e7bb /src/SpecificGen | |
| parent | b68e0ebe9c9064fa90ff47dc794674310d86a8d7 (diff) | |
Update sqrtm1 for 3mod4
Diffstat (limited to 'src/SpecificGen')
| -rw-r--r-- | src/SpecificGen/GF2519_32.v | 8 | ||||
| -rw-r--r-- | src/SpecificGen/GF41417_32.v | 8 | ||||
| -rw-r--r-- | src/SpecificGen/GF5211_32.v | 8 | ||||
| -rw-r--r-- | src/SpecificGen/GFtemplate3mod4 | 8 |
4 files changed, 0 insertions, 32 deletions
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}}}) : |