Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v

1 files changed, 85 insertions, 249 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index bc81dce01..c7314486e 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,19 +1,17 @@
-Require Import ZArith NPeano Znumtheory.
-Require Import Bedrock.Word.
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
-Require Import VerdiTactics.
+Require Import Crypto.Spec.ModularArithmetic.
+Require Import Crypto.Spec.CompleteEdwardsCurve.
 
-Local Open Scope nat_scope.
-Local Coercion Z.to_nat : Z >-> nat.
+Require Bedrock.Word.
+Require Znumtheory BinInt.
+Require NPeano.
 
 (* TODO : where should this be? *)
-Definition wfirstn {m} {n} (w : word m) (H : n <= m) : word n.
-  refine (split1 n (m - n) (match _ in _ = N return word N with
+Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
+  refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w
-                            end)); abstract omega.
-Defined.
+                            end)); abstract omega. Defined.
+
+Coercion Word.wordToNat : Word.word >-> nat.
 
 Class Encoding (T B:Type) := {
   enc : T -> B ;
@@ -22,243 +20,81 @@ Class Encoding (T B:Type) := {
 }.
 Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
 
-(* Spec from <https://eprint.iacr.org/2015/677.pdf> *)
-Module Type EdDSAParams.
-  Parameter q : Z.
-  Axiom q_prime : prime q.
-  Axiom q_odd : (2 < q)%Z.
-
-  (* Choosing q sufficiently large is important for security, since the size of
-   * q constrains the size of l below. *)
-
-  (* GF is the finite field of integers modulo q *)
-  Module Modulus_q <: PrimeModulus.
-    Definition modulus := q.
-    Definition prime_modulus := q_prime.
-  End Modulus_q.
-
-  Parameter b : nat.
-  Axiom b_valid : (2^(Z.of_nat b - 1) > q)%Z.
-  Notation secretkey := (word b) (only parsing).
-  Notation publickey := (word b) (only parsing).
-  Notation signature := (word (b + b)) (only parsing).
-
-  Parameter H : forall {n}, word n -> word (b + b).
-  (* A cryptographic hash function. Conservative hash functions are recommended
-   * and do not have much impact on the total cost of EdDSA. *)
-
-  Parameter c : nat.
-  Axiom c_valid : c = 2 \/ c = 3.
-  (* Secret EdDSA scalars are multiples of 2^c. The original specification of
-   * EdDSA did not include this parameter: it implicitly took c = 3. *)
-
-  Parameter n : nat.
-  Axiom n_ge_c : n >= c.
-  Axiom n_le_b : n <= b.
-
-  Module Import Field := FieldModulo Modulus_q.
-  Definition Fq := F q.
-  Local Open Scope F_scope.
-
-  (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit
-   *   (the 2n position) always set and the bottom c bits always cleared.
-   * The original specification of EdDSA did not include this parameter:
-   *   it implicitly took n = b−2.
-   * Choosing n sufficiently large is important for security:
-   *   standard “kangaroo” attacks use approximately 1.36\sqrt(2n−c) additions
-   *   on average to determine an EdDSA secret key from an EdDSA public key *)
-
-  Parameter a : Fq.
-  Axiom a_nonzero : a <> 0%F.
-  Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
-  (* The usual recommendation for best performance is a = −1 if q mod 4 = 1,
-   *   and a = 1 if q mod 4 = 3.
-   * The original specification of EdDSA did not include this parameter:
-   *   it implicitly took a = −1 (and required q mod 4 = 1). *)
-
-  Parameter d : Fq.
-  Axiom d_nonsquare : forall x, x^2 <> d.
-  (* The exact choice of d (together with a and q) is important for security,
-   *   and is the main topic considered in “curve selection”. *)
-
-  (* E = {(x, y) \in Fq x Fq : ax^2 + y^2 = 1 + dx^2y^2}.
-   * This set forms a group with neutral element 0 = (0, 1) under the
-   *   twisted Edwards addition law. *)
-  Definition CurveParameters : TwistedEdwardsParams :=
-    Build_TwistedEdwardsParams q a d q_prime q_odd a_nonzero a_square d_nonsquare.
-
-  Definition pt := @point CurveParameters.
-  Parameter B : pt. (* element of E *)
-  Axiom B_not_identity : B <> zero.
-
-  (*
-   * An odd prime l such that lB = 0 and (2^c)l = #E.
-   * The number #E is part of the standard data provided for an elliptic
-   *   curve E.
-   * Choosing l sufficiently large is important for security: standard “rho”
-   *   attacks use approximately 0.886√l additions on average to determine an
-   *   EdDSA secret key from an EdDSA public key.
-   *)
-  Parameter l : Z.
-  Axiom l_prime : prime l.
-  Axiom l_odd : (l > 2)%nat.
-  Axiom l_order_B : scalarMult l B = zero.
-  (* TODO: (2^c)l = #E *)
-
-  (*
-   * A “prehash” function H'.
-   * PureEdDSA means EdDSA where H' is the identity function, i.e. H'(M) = M.
-   * HashEdDSA means EdDSA where H' generates a short output, no matter how
-   *   long the message is; for example, H'(M) = SHA-512(M).
-   * The original specification of EdDSA did not include this parameter:
-   *   it implicitly took H0 as the identity function.
-   *)
-  Parameter H'_out_len : nat -> nat.
-  Parameter H' : forall {n}, word n -> word (H'_out_len n).
-
-  Parameter FqEncoding : encoding of Fq as word (b-1).
-  Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b.
-  Parameter PointEncoding : encoding of pt as word b.
+Infix "^" := NPeano.pow.
+Infix "mod" := NPeano.modulo.
+Infix "++" := Word.combine.
+
+Section EdDSAParams.
+  Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *)
+    E : TwistedEdwardsParams; (* underlying elliptic curve *)
+                        
+    b : nat;
+    b_valid : 2^(b - 1) > BinInt.Z.to_nat q;
+    FqEncoding : encoding of F q as Word.word (b-1);
+    PointEncoding : encoding of point as Word.word b;
+  
+    H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *)
+  
+    c : nat; (* cofactor E = 2^c *)
+    c_valid : c = 2 \/ c = 3;
   
+    n : nat;
+    n_ge_c : n >= c;
+    n_le_b : n <= b;
+  
+    B : point;
+    B_not_identity : B <> zero;
+
+    l : nat; (* order of the subgroup of E generated by B *)
+    l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
+    l_odd : l > 2;
+    l_order_B : scalarMult l B = zero;
+    FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b;
+
+    H'_out_len : nat -> nat;
+    H' : forall {n}, Word.word n -> Word.word (H'_out_len n) (* prehash function *)
+  }.
 End EdDSAParams.
 
-Hint Rewrite Nat.mod_mod using omega.
-
-Ltac arith' := intros; autorewrite with core; try (omega || congruence).
-
-Ltac arith := arith';
-             repeat match goal with
-                    | [ H : _ |- _ ] => rewrite H; arith'
-                    end.
-
-Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s mod l = s}.
-  exists (n mod l); abstract arith.
-Defined.
-
-Module Type EdDSA (Import P : EdDSAParams).
-  Infix "++" := combine.
-  Infix "*" := scalarMult.
-  Infix "+" := unifiedAdd.
-  Coercion wordToNat : word >-> nat.
-
-  Definition curveKey sk := let N := wfirstn sk n_le_b in
-    (N - (N mod pow2 c) + pow2 n)%nat.
-  Definition randKey (sk:secretkey) := split2 b b (H sk).
-  Definition modL := modularNat l l_odd.
-
-  Parameter public : secretkey -> publickey.
-  Axiom public_spec : forall sk, public sk = enc (curveKey sk * B).
-
-  (* TODO: use GF for both GF(q) and GF(l) *)
-  Parameter sign : publickey -> secretkey -> forall {n}, word n -> signature.
-  Axiom sign_spec : forall A_ sk {n} (M : word n), sign A_ sk M = 
-    let r := H (randKey sk ++ M) in
-    let R := r * B in
-    let s := curveKey sk in
-    let S := (r + H (enc R ++ public sk ++ M) * s)%nat in
-    enc R ++ enc (modL S).
-
-  Parameter verify : publickey -> forall {n}, word n -> signature -> bool.
-  Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ M sig  = true <-> (
-    let R_ := split1 b b sig in
-    let S_ := split2 b b sig in
-    exists A, dec A_ = Some A /\
-    exists R, dec R_ = Some R /\
-    exists S : {s:nat | s mod l = s}, dec S_ = Some S /\
-    proj1_sig S * B = R + wordToNat (H (R_ ++ A_ ++ M)) * A).
-End EdDSA.
-
-Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P).
-  Hint Rewrite sign_spec split1_combine split2_combine.
-
-  (* for signature (R_, S_), R_ = encode_point (r * B) *) 
-  Lemma decode_sign_split1 : forall A_ sk {n} (M : word n),
-    split1 b b (sign A_ sk M) = enc (wordToNat (H (randKey sk ++ M)) * B).
-  Proof.
-    arith.
-  Qed.
-  Hint Rewrite decode_sign_split1.
-
-  (* for signature (R_, S_), S_ = encode_scalar (r + H(R_, A_, M)s) *) 
-  Lemma decode_sign_split2 : forall sk {n} (M : word n),
-    split2 b b (sign (public sk) sk M) =
-    let r := H (randKey sk ++ M) in
-    let R := r * B in
-    let s := curveKey sk in
-    let S := (r + (H ((enc R) ++ (public sk) ++ M) * s))%nat in
-    enc (modL S).
-  Proof.
-    arith.
-  Qed.
-  Hint Rewrite decode_sign_split2.
-
-  Existing Instance CurveParameters.
-  Lemma zero_times : forall n, 0 * n = zero.
-  Proof.
-    auto.
-  Qed.
-
-  Lemma zero_plus : forall n, zero + n = n.
-  Proof.
-    intros; rewrite twistedAddComm; apply zeroIsIdentity.
-  Qed.
-
-  Lemma times_S : forall n m, S n * m = m + n * m.
-  Proof.
-    auto.
-  Qed.
-
-  Lemma times_S_nat : forall n m, (S n * m = m + n * m)%nat.
-  Proof.
-    auto.
-  Qed.
-
-  Hint Rewrite plus_O_n plus_Sn_m times_S times_S_nat.
-  Hint Rewrite zeroIsIdentity zero_times zero_plus twistedAddAssoc.
-
-  Lemma scalarMult_distr : forall n0 m, (n0 + m) * B = unifiedAdd (n0 * B) (m * B).
-  Proof.
-    induction n0; arith.
-  Qed.
-  Hint Rewrite scalarMult_distr.
-
-  Lemma scalarMult_assoc : forall (n0 m : nat), n0 * (m * B) = (n0 * m) * B.
-  Proof.
-    induction n0; arith.
-  Qed.
-  Hint Rewrite scalarMult_assoc.
-
-  Lemma scalarMult_zero : forall m, m * zero = zero.
-  Proof.
-    induction m; arith.
-  Qed.
-  Hint Rewrite scalarMult_zero.
-  Hint Rewrite l_order_B.
-
-  Lemma l_order_B' : forall x, l * x * B = zero.
-  Proof.
-    intros; rewrite mult_comm; rewrite <- scalarMult_assoc; arith.
-  Qed.
-
-  Hint Rewrite l_order_B'.
-
-  Lemma scalarMult_mod_l : forall n0, n0 mod l * B = n0 * B.
-  Proof.
-    intros.
-    rewrite (div_mod n0 l) at 2 by (generalize l_odd; omega).
-    arith.
-  Qed.
-  Hint Rewrite scalarMult_mod_l.
-
-  Hint Rewrite verify_spec public_spec.
-
-  Hint Resolve @encoding_valid.
-
-  Lemma verify_valid_passes : forall sk {n} (M : word n),
-    verify (public sk) M (sign (public sk) sk M) = true.
-  Proof.
-    arith; simpl.
-    repeat eexists; eauto; simpl; arith.
-  Qed.
-
-End EdDSAFacts.
+Section EdDSA.
+  Context {prm:EdDSAParams}.
+  Existing Instance E.
+  Existing Instance PointEncoding.
+  Existing Instance FlEncoding.
+  Existing Class le.
+  Existing Instance n_le_b.
+
+  Notation secretkey := (Word.word b) (only parsing).
+  Notation publickey := (Word.word b) (only parsing).
+  Notation signature := (Word.word (b + b)) (only parsing).
+
+  (* TODO: proofread curveKey and definition of n *)
+  Definition curveKey (sk:secretkey) : nat :=
+    let x := wfirstn n sk in (* first half of the secret key is a scalar *)
+    let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *)
+             x + 2^n. (* and the high bit is always set *)
+  Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk).
+  Definition public (sk:secretkey) : publickey := enc (curveKey sk * B)%E.
+
+  Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
+    let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
+    let R : point := (r * B)%E in (* commitment to nonce *)
+    let s : nat := curveKey sk in (* secret scalar *)
+    let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat
+                              (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
+    match dec A_ : option point with None => false | Some A =>
+    match dec R_ : option point with None => false | Some R =>
+    match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' =>
+    if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A
+    then true else false
+    end
+    end
+    end%E.
+End EdDSA.
\ No newline at end of file