diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-21 18:48:02 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-21 18:48:02 -0400 |
| commit | 30ef733d1a5820456d5e5aac774270b51a9c9dde (patch) | |
| tree | 7e3dbf3a317d5367bd36d43b797caa3c2428de6c | |
| parent | e4f24c70af9044a9f2e8279d98ed9842eb858858 (diff) | |
finished last cases of nonzero proofs for associativity
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 33 | ||||
| -rw-r--r-- | 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 |