diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-03-20 20:06:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-03-20 20:06:28 -0400 |
| commit | 0f77ed606c8687e5cdcd72c85eefde609c5e0de1 (patch) | |
| tree | 8e53488998c34d2fc413364352201688c38c4341 /src/Specific | |
| parent | a189e7a6b7d0b462f128ab7eba1612f373c8ee6f (diff) | |
state top-level derivation for Ed25519.verify
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v new file mode 100644 index 000000000..33c8398f7 --- /dev/null +++ b/src/Specific/Ed25519.v @@ -0,0 +1,30 @@ +Require Import Crypto.Spec.Ed25519. +Require Import Crypto.Tactics.VerdiTactics. +Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. +Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.ExtendedCoordinates. + +Local Infix "++" := Word.combine. +Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). +Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). + +Lemma sharper_verify : { verify | forall pk l msg sig, verify pk l msg sig = ed25519_verify pk l msg sig}. +Proof. + eexists; intros. + cbv [ed25519_verify EdDSA.verify Encoding.dec EdDSA.PointEncoding PointEncoding + PointEncoding.point_encoding EdDSA.FlEncoding FlEncoding + Encoding.modular_word_encoding ed25519params]. + break_match. + break_match. + break_match. + repeat match goal with + | |- context [(?n * ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + erewrite <-scalarMultM1_rep + | |- context [(?P + unExtendedPoint _)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + erewrite unifiedAddM1_rep + end. + rewrite !Znat.Z_nat_N, <-!Word.wordToN_nat. + + (* unfold scalarMultM1 at 1. *) +Admitted.
\ No newline at end of file |