diff options
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 | ||||
-rw-r--r-- | src/Spec/EdDSA.v | 3 | ||||
-rw-r--r-- | src/Specific/Ed25519.v | 39 |
3 files changed, 34 insertions, 13 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 8dbfdf7b9..b7d2c0d8e 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -46,8 +46,11 @@ Section TwistedEdwardsCurves. | O => zero | S n' => unifiedAdd P (scalarMult n' P) end. + + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. End TwistedEdwardsCurves. Delimit Scope E_scope with E. Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope.
\ No newline at end of file +Infix "*" := scalarMult : E_scope. +Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 6f57d7bec..c9660bd98 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -14,6 +14,7 @@ Infix "mod" := NPeano.modulo. Infix "++" := Word.combine. Section EdDSAParams. + Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) E : TwistedEdwardsParams; (* underlying elliptic curve *) @@ -70,8 +71,6 @@ Section EdDSA. (r + H (enc R ++ public sk ++ M) * s)) in enc R ++ enc S. - Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. - Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := let R_ := Word.split1 b b sig in let S_ := Word.split2 b b sig in diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 33c8398f7..efee4e7af 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -1,30 +1,49 @@ +Require Import Bedrock.Word. 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. +Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.Util.IterAssocOp. 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). +Local Arguments H {_} _. +Local Arguments scalarMultM1 {_} {_} _ _. +Local Arguments unifiedAddM1 {_} {_} _ _. 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. + cbv [ed25519_verify EdDSA.verify + ed25519params curve25519params + EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H + EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + + (* zoom in to the interesting case *) + repeat match goal with |- context[match ?a with Some x => _ | _ => _ end] => + let n := fresh x in + let H := fresh "Heq" x in + destruct a as [x|] + end. + + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with | |- context [(?n * ?P)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite <-scalarMultM1_rep + erewrite <-p1 | |- context [(?P + unExtendedPoint _)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite unifiedAddM1_rep + erewrite p2 end. rewrite !Znat.Z_nat_N, <-!Word.wordToN_nat. - (* unfold scalarMultM1 at 1. *) + cbv [scalarMultM1 iter_op]. + Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *) + cbv iota zeta delta [test_and_op]. + + Admitted.
\ No newline at end of file |