From 30ef733d1a5820456d5e5aac774270b51a9c9dde Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 21 Apr 2016 18:48:02 -0400 Subject: finished last cases of nonzero proofs for associativity --- .../CompleteEdwardsCurveTheorems.v | 33 +++++++++++----------- to_gallina.md | 1 - 2 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 6ea5ec283..d39f864da 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -53,6 +53,21 @@ Section CompleteEdwardsCurveTheorems. Edefn; apply (f_equal2 div); ring. Qed. + Ltac unifiedAdd_nonzero := match goal with + | [ |- (?op 1 (d * _ * _ * _ * _ * + inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F] + => let Hadd := fresh "Hadd" in + pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd; + simpl in Hadd; + match goal with + | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] => + replace other with + (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) + * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring); + auto + end + end. + Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E. Proof. (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *) @@ -60,23 +75,7 @@ Section CompleteEdwardsCurveTheorems. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); cbv beta iota in *; - repeat split. - { field_nonzero idtac. } - { field_nonzero idtac. } - 2: field_nonzero idtac. - 2: field_nonzero idtac. - 3: field_nonzero idtac. - 3: field_nonzero idtac. - 4: field_nonzero idtac. - 4: field_nonzero idtac. - 4:field_nonzero idtac. - 3:field_nonzero idtac. - 2:field_nonzero idtac. - 1:field_nonzero idtac. - admit. - admit. - admit. - admit. + repeat split; field_nonzero idtac; unifiedAdd_nonzero. Qed. Lemma zeroIsIdentity : forall P, (P + zero = P)%E. diff --git a/to_gallina.md b/to_gallina.md index bf5ab8270..812d9fd88 100644 --- a/to_gallina.md +++ b/to_gallina.md @@ -6,6 +6,5 @@ Remaining work needed for Gallina verification code + make EdDSA point addition use ModularBaseSystem + represent scalars (Fl) in ModularBaseSystem (large c) + elliptic curve decidable equality -+ associativity nonseroes + negation of elliptic curve points + canonical representations of field elements -- cgit v1.2.3