diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 16:47:41 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:03 -0400 |
| commit | 5a9f99ca5cdbc3ebff637b182959cbbfb86666ec (patch) | |
| tree | a22898e9567c5a7e66f608171bf73369bd3949d5 /src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v | |
| parent | 4c346d17e03f88a7ac5eb98cf2143563bae53bf4 (diff) | |
document field issue re-appearing
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v new file mode 100644 index 000000000..b9baf1498 --- /dev/null +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -0,0 +1,40 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.CompleteEdwardsCurve.Pre. + +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. + + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, + ZQ <> 0 -> + ZP <> 0 -> + ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + + ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * + (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) / + ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) * + (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. + intros. + field; assumption. + Qed. +End ExtendedCoordinates.
\ No newline at end of file |