diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-03-20 19:13:03 -0400 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:42:17 -0400 |
| commit | c353e1d89fb65bfaa7b79dec693ccb1e7f251d27 (patch) | |
| tree | af8180ece896b3ef55a6bfa139dd65cadf7eb864 | |
| parent | ac694189f4b45eb7278d08a919c4a7e118ed503e (diff) | |
instantiate ed25519 sign in spec
| -rw-r--r-- | src/Spec/Ed25519.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index d6d02b93f..6ab47e8e5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -64,7 +64,7 @@ Lemma nonsquare_d : forall x, (x^2 <> d)%F. exact eq_refl. Qed. (* 10s *) -Instance TEParams : TwistedEdwardsParams := { +Instance curve25519params : TwistedEdwardsParams := { q := q; prime_q := prime_q; two_lt_q := two_lt_q; @@ -140,15 +140,15 @@ Proof. reflexivity. Qed. -Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. +Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) Definition B_nonzero : B <> zero. Admitted. Definition l_order_B : scalarMult l B = zero. Admitted. -Instance x : EdDSAParams := { - E := TEParams; +Local Instance ed25519params : EdDSAParams := { + E := curve25519params; b := b; H := H; c := c; @@ -168,3 +168,7 @@ Instance x : EdDSAParams := { l_odd := l_odd; l_order_B := l_order_B }. + +Definition ed25519_verify + : forall (pubkey:word b) (len:nat) (msg:word len) (sig:word (b+b)), bool + := @verify ed25519params.
\ No newline at end of file |