diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 22:22:36 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:03 -0400 |
| commit | 67004987959e1c9e46e879f06da00d567547482e (patch) | |
| tree | 05c6cd8d60f73b135248ae013768c8b718b567b5 /src/CompleteEdwardsCurve | |
| parent | 1f21c2be76a6f84fa90669876e425ee006978899 (diff) | |
workaround field with typeclass modulus
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v index 37bc8cca5..8d24f2cd2 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -4,22 +4,19 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Section ExtendedCoordinates. Local Open Scope F_scope. - (* - Context {prm:TwistedEdwardsParams}. (* DOESN'T WORK *) - *) - Context {q:BinInt.Z} {prime_q:Znumtheory.prime q}. (* WORKS OKAY-ish *) - - Check q : BinInt.Z. - Check prime_q : Znumtheory.prime q. - Existing Instance prime_q. + Context {prm:TwistedEdwardsParams}. + Context {p:BinInt.Z} {p_eq_q:p = q}. + Lemma prime_p : Znumtheory.prime p. + rewrite p_eq_q; exact prime_q. + Qed. - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), + Add Field Ffield_Z : (@Ffield_theory p prime_p) + (morphism (@Fring_morph p), preprocess [Fpreprocess], postprocess [Fpostprocess], constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + div (@Fmorph_div_theory p), + power_tac (@Fpower_theory p) [Fexp_tac]). Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, ZQ <> 0 -> @@ -34,7 +31,8 @@ Section ExtendedCoordinates. (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). Proof. + rewrite <-p_eq_q. intros. - field; assumption. + abstract (field; assumption). Qed. End ExtendedCoordinates.
\ No newline at end of file |