diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-14 20:41:22 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-14 20:41:22 -0500 |
commit | b68e0ebe9c9064fa90ff47dc794674310d86a8d7 (patch) | |
tree | 3dfdce965f73599c29a8aeb8b1b72711950a177b /src/SpecificGen/GFtemplate3mod4 | |
parent | e2cac8ba391a9f173d32a79ce612a88ee36f94cb (diff) |
Fix some sqrt things
Diffstat (limited to 'src/SpecificGen/GFtemplate3mod4')
-rw-r--r-- | src/SpecificGen/GFtemplate3mod4 | 17 |
1 files changed, 17 insertions, 0 deletions
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. |