diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 30 |
2 files changed, 31 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index d7c71f7cb..6d2b3a880 100644 --- a/_CoqProject +++ b/_CoqProject @@ -20,6 +20,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/PointEncoding.v +src/Specific/Ed25519.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v 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 |