EdDSA: mostly-complete spec and preliminary structure.

3 files changed, 204 insertions, 70 deletions

diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 430a48c82..4c5572ea7 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -2,23 +2,18 @@
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Tactics.VerdiTactics.
 
-Module TwistedEdwardsDefs (Import M : Modulus).
+Module TwistedEdwardsDefs (M : Modulus).
   Module Export GT := GaloisTheory M.
   Open Scope GF_scope.
-  Definition isSquareAndNonzero (a : GF) :=  a <> 0 /\ exists sqrt_a, sqrt_a^2 = a.
-  Definition isNonSquare (d : GF) :=  forall not_sqrt_d, not_sqrt_d^2 <> d.
-  Definition twistedA := { a : GF | isSquareAndNonzero a }.
-  Definition twistedD := { d : GF | isNonSquare d }.
-  Definition twistedAToGF (a : twistedA) := proj1_sig a.
-  Coercion twistedAToGF : twistedA >-> GF.
-  Definition twistedDToGF (d : twistedD) := proj1_sig d.
-  Coercion twistedDToGF : twistedD >-> GF.
 End TwistedEdwardsDefs.
 
 Module Type TwistedEdwardsParams (M : Modulus).
-  Module Export D := TwistedEdwardsDefs M.
-  Parameter a : twistedA.
-  Parameter d : twistedD.
+  Module Export Defs := TwistedEdwardsDefs M.
+  Parameter a : GF.
+  Axiom a_nonzero : a <> 0.
+  Axiom a_square : exists x, x * x = a.
+  Parameter d : GF.
+  Axiom d_nonsquare : forall x, x * x <> d.
 End TwistedEdwardsParams.
 
 Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M).
@@ -28,7 +23,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   * <https://eprint.iacr.org/2015/677.pdf>
   *)
   Record point := mkPoint {projX : GF; projY : GF}.
-
+  Notation "'(' x ',' y ')'" := (mkPoint x y). 
+  Definition zero := (0, 1).
   Definition unifiedAdd (P1 P2 : point) : point :=
     let x1 := projX P1 in
     let y1 := projY P1 in
@@ -43,6 +39,20 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     let x := projX P in
     let y := projY P in
     a*x^2 + y^2 = 1 + d*x^2*y^2.
+  
+  Local Infix "+" := unifiedAdd.
+
+  (* Naive implementation *)
+  Fixpoint scalarMultSpec (n:nat) (P : point) : point :=
+    match n with 
+    | O => zero
+    | S n' => P + scalarMultSpec n' P
+    end
+  .
+
+  (* TODO: non-naive *)
+  Definition scalarMult := scalarMultSpec.
+  
 End CompleteTwistedEdwardsCurve.
 
 Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M).
@@ -63,7 +73,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE
 End CompleteTwistedEdwardsPointFormat.
 
 Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M).
-  Module Export Curve := CompleteTwistedEdwardsCurve M P.
+  Module Import Curve := CompleteTwistedEdwardsCurve M P.
   Lemma twistedAddCompletePlus : forall (P1 P2:point)
     (oc1:onCurve P1) (oc2:onCurve P2),
     let x1 := projX P1 in
@@ -101,8 +111,6 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
     (* uh... I don't actually know where this is proven... *)
   Admitted.
 
-  Local Notation "'(' x ',' y ')'" := (mkPoint x y).
-  Definition zero := (0, 1).
   Lemma zeroOnCurve : onCurve (0, 1).
   Proof.
     twisted.
@@ -111,21 +119,24 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
   Proof.
     admit.
   Qed.
-End CompleteTwistedEdwardsFacts.
-
-Module Minus1Twisted (Import M : Modulus).
-  Module Minus1Params <: TwistedEdwardsParams M.
-    Module Export D := TwistedEdwardsDefs M.
-    Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1).
-    Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero.
-    Parameter d : twistedD.
-  End Minus1Params.
-  Import Minus1Params.
 
-  Module Import Curve := CompleteTwistedEdwardsCurve M Minus1Params.
+End CompleteTwistedEdwardsFacts.
 
-  Module Minus1Format <: CompleteTwistedEdwardsPointFormat M Minus1Params.
-    Module Import Facts := CompleteTwistedEdwardsFacts M Minus1Params.
+Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
+  Module Export Defs := TwistedEdwardsDefs M.
+  Open Scope GF_scope.
+  Definition a := 0 - 1.
+  Axiom a_nonzero : a <> 0.
+  Axiom a_square : exists x, x * x = a.
+  Parameter d : GF.
+  Axiom d_nonsquare : forall x, x * x <> d.
+End Minus1Params.
+
+Module Minus1Twisted (M : Modulus) (Import P : Minus1Params M).
+  Module Import Curve := CompleteTwistedEdwardsCurve M P.
+
+  Module Minus1Format <: CompleteTwistedEdwardsPointFormat M P.
+    Module Import Facts := CompleteTwistedEdwardsFacts M P.
     (** [projective] represents a point on an elliptic curve using projective
     * Edwards coordinates for twisted edwards curves with a=-1 (see
     * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html>
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index 8197bed8d..28ae37233 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -39,7 +39,7 @@ Module BaseSystem (Import B:BaseCoefs).
 
   Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us).
   Proof.
-    unfold decode, decode'; intros; f_equal; apply combine_truncate_l.
+    unfold decode'; intros; f_equal; apply combine_truncate_l.
   Qed.
   
   Fixpoint add (us vs:digits) : digits :=
diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v
index bb256248d..1f0792acb 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -1,5 +1,4 @@
 Require Import ZArith.
-Require Import List.
 Require Import Bedrock.Word.
 Require Import Crypto.Curves.PointFormats.
 Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
@@ -17,32 +16,39 @@ Module Type EdDSAParams.
   * There are additional security concerns when q is not chosen to be prime.
   *)
   Parameter q : Prime.
-  Axiom q_odd : Z.odd q = true.
+  Axiom q_odd : q > 2.
 
   Module Modulus_q <: Modulus.
     Definition modulus := q.
   End Modulus_q.
-  Module Import Defs := TwistedEdwardsDefs Modulus_q.
+  Module Export CurveDefs := TwistedEdwardsDefs Modulus_q.
 
   (*
   * An integer b with 2^(b − 1) > q.
   * EdDSA public keys have exactly b bits,
   *   and EdDSA signatures have exactly 2b bits.
   *)
+  (* Note: the parameter pred_b is (b - 1) to make proofs about the (b-1)-bit
+  * encoding easier *)
   Parameter b : nat.
-  Axiom b_valid : 2^((Z.of_nat b) - 1) > q.
+  Coercion Z.of_nat : nat >-> Z.
+  Axiom b_valid : 2^(b - 1) > q.
+  Definition secretkey : Type := word b.
+  Definition publickey : Type := word b.
+  Definition signature : Type := word (b + b).
 
   (* A (b − 1)-bit encoding of elements of the finite field Fq. *)
-  Parameter decode : word (b - 1) -> GF.
-  Parameter encode : GF -> word (b - 1).
-  Axiom consistent : forall x, decode( encode x) = x.
+  Parameter decode_scalar : word (b - 1) -> GF.
+  Parameter encode_scalar : GF -> word (b - 1).
+  Axiom decode_encode_scalar_consistent : forall x, decode_scalar (encode_scalar x) = x.
+  Axiom encode_decode_scalar_consistent : forall x, encode_scalar (decode_scalar x) = x.
 
   (*
   * A cryptographic hash function H producing 2b-bit output.
   * Conservative hash functions are recommended and do not have much
   *   impact on the total cost of EdDSA.
   *)
-  Parameter H : forall n, word n -> word (b + b).
+  Parameter H : forall {n}, word n -> word (b + b).
 
   (*
   * An integer c \in {2, 3}. Secret EdDSA scalars are multiples of 2c.
@@ -63,8 +69,8 @@ Module Type EdDSAParams.
   *   on average to determine an EdDSA secret key from an EdDSA public key.
   *)
   Parameter n : nat.
-  Axiom n_gte_c : (n >= c)%nat.
-  Axiom n_lte_b : (n <= b)%nat.
+  Axiom n_ge_c : n >= c.
+  Axiom n_le_b : (n <= b)%nat.
 
   (*
   * A nonzero square element a of Fq.
@@ -73,22 +79,28 @@ Module Type EdDSAParams.
   * The original specification of EdDSA did not include this parameter:
   *   it implicitly took a = −1 (and required q mod 4 = 1).
   *)
-  Parameter a : twistedA.
+  Parameter a : GF.
+  Axiom a_nonzero : a <> 0%GF.
+  Axiom a_square : exists x, x * x = a.
 
   (*
   * A non-square element d of Fq.
   * The exact choice of d (together with a and q) is important for security,
   *   and is the main topic considered in “curve selection”.
   *)
-  Parameter d : twistedD.
+  Parameter d : GF.
+  Axiom d_nonsquare : forall x, x * x <> d.
 
   Module Parameters <: TwistedEdwardsParams Modulus_q.
-    Definition a := a.
+    Module Defs := CurveDefs.
+    Definition a : GF := a.
+    Definition a_nonzero := a_nonzero.
+    Definition a_square := a_square.
     Definition d := d.
-    Module D := Defs.
+    Definition d_nonsquare := d_nonsquare.
   End Parameters.
 
-  Module Export Facts := CompleteTwistedEdwardsFacts Modulus_q Parameters.
+  Module Export Curve := CompleteTwistedEdwardsCurve Modulus_q Parameters.
 
   (*
   *  An element B \neq (0, 1) of the set
@@ -97,8 +109,9 @@ Module Type EdDSAParams.
   *    twisted Edwards addition law.
   *)
   Parameter B : point.
+  Axiom B_not_identity : B <> zero.
   Axiom B_valid : onCurve B.
-  Axiom B_not_identity : B = zero -> False.
+  Hint Resolve B_valid.
 
   (*
   * An odd prime l such that lB = 0 and (2^c)l = #E.
@@ -109,7 +122,8 @@ Module Type EdDSAParams.
   *   EdDSA secret key from an EdDSA public key.
   *)
   Parameter l : Prime.
-  Axiom l_odd : Z.odd l = true.
+  Axiom l_odd : l > 2.
+  (* TODO: (2^c)l = #E *)
 
   (*
   * A “prehash” function H'.
@@ -120,36 +134,145 @@ Module Type EdDSAParams.
   *   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 H' : forall {n}, word n -> word (H'_out_len n).
 
 End EdDSAParams.
 
+(* TODO : where should this be? *)
+Definition wfirstn {m} {n} (w : word m) (H : (n <= m)%nat) : word n.
+  replace m with (n + (m - n))%nat in * by (symmetry; apply le_plus_minus; apply H)
+.
+  exact (split1 n (m - n) w).
+Defined.
+
+Lemma wtl_WS : forall b {n} (w : word n), wtl (WS b w) = w.
+Proof.
+  auto.
+Qed.
+
 Module Type EdDSA (Import P : EdDSAParams).
+  Local Infix "++" := combine.
+  Local Infix "*" := scalarMult.
+  Local Infix "+" := unifiedAdd.
+
+  (* From [https://eprint.iacr.org/2015/677.pdf]: x is negative if the 
+  * (b − 1)-bit encoding of x is lexicographically larger than the 
+  * (b − 1)-bit encoding of −x *)
+  Definition sign_bit x : word 1 := 
+    match (wordToNat (encode_scalar x) ?= wordToNat (encode_scalar (GFopp x)))%nat with
+    | Gt => wone 1
+    | _ => wzero 1
+    end.
+
+  (* TODO: move eventually *)
+  Lemma b_gt_0 : b > 0.
+  Proof.
+    pose proof b_valid.
+    pose proof q_odd.
+    destruct b; boring.
+  Qed.
+  
   Parameter encode_point : point -> word b.
-  Parameter decode_point : word b -> point.
-  Parameter secret : Type.
-  Parameter public : secret -> word b.
-  Parameter signature : secret -> forall n, word n -> word (b + b).
-End EdDSA.
+  Definition encode_point_ref (P : point) : word b.
+    replace b with (b - 1 + 1)%nat by abstract (pose proof b_gt_0; omega).
+    apply (combine (encode_scalar (projY P)) (sign_bit (projX P))).
+  Defined.
+  Axiom encode_point_spec : forall P, encode_point P = encode_point_ref P.
+  Parameter decode_point : word b -> option point.
+  Axiom decode_point_spec : forall P, onCurve P ->
+    decode_point (encode_point P) = Some P.
+
+  Definition s (sk : secretkey) :=
+    let N := wordToNat (wfirstn sk n_le_b) in
+    ((N - (NPeano.modulo N (pow2 c))) * pow2 c)%nat.
+  Parameter public : secretkey -> publickey.
+  Axiom public_spec : forall sk, public sk = encode_point ((s sk) * B).
 
-Module EdDSAImpl (Import P : EdDSAParams) <: EdDSA P.
-  Definition encode_point (p : point) := wzero b. (* TODO *)
-  Definition decode_point (w : word b) := zero.  (* TODO *)
+  Parameter sign : secretkey -> forall {n}, word n -> signature.
+  Axiom sign_spec : forall sk {n} (M : word n), sign sk M = 
+    let r := wordToNat (H ((split2 b b (H sk)) ++ M)) in
+    let R := r * B in
+    let S := NPeano.modulo (r + ((s sk) * wordToNat (H ((encode_point R) ++ (public sk) ++ M))))%nat (Z.to_nat l) in
+    (encode_point R) ++ (natToWord b S).
 
-  Definition leading_ones n := natToWord b (wordToNat (wone n)).
-  Definition c_to_n_window := wxor (leading_ones c) (leading_ones n).
-  (* Precompute s and the high half of H(k) *)
-  Record secret := mkSecret{
-    key : word b;
-    s : Z;
-    hash_high : word b;
-    s_def : s =  wordToZ (wand c_to_n_window key);
-    hash_high_def : hash_high = split2 b b (H b key)
-  }.
+  Parameter verify : publickey -> signature -> forall {n}, word n -> bool.
+  Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ sig M = true <->
+    let R_ := split1 b b sig in
+    let S_ := split2 b b sig in
+    let S := wordToNat S_ in
+    match (decode_point A_) with
+    | None => False
+    | Some A => match (decode_point R_) with
+                | None => False
+                | Some R => S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A)
+                end
+    end.
 
-  (* Needs scalar multiplication:
-  * Definition public (sk : secret) := H b (encode_point (scalar_mul (inject (s sk)) B)). *)
+  (* for signature (R_, S_), R_ = encode_point (r * B) *) 
+  Lemma decode_sign_split1 : forall (sk : secretkey) {n} (M : word n),
+    split1 b b (sign sk M) = encode_point ((wordToNat (H ((split2 b b (H sk)) ++ M))) * B).
+  Proof.
+    intros. pose proof (sign_spec sk M).
+    simpl in H0. rewrite H0; clear H0.
+    apply split1_combine.
+  Qed.
+  
+  (* for signature (R_, S_), S_ = encode_scalar (r + H(R_, A_, M)s) *) 
+  Lemma decode_sign_split2 : forall (sk : secretkey) {n} (M : word n),
+    split2 b b (sign sk M) =
+    let r := wordToNat (H ((split2 b b (H sk)) ++ M)) in
+    natToWord b (NPeano.modulo (r + ((s sk) * wordToNat (H ((encode_point (r * B)) ++ (public sk) ++ M)))) (Z.to_nat l)).
+  Proof.
+    intros. rewrite sign_spec; simpl.
+    rewrite split2_combine.
+    f_equal.
+  Qed.
 
-  Definition signature (sk : secret) n (w : word n) := wzero (b + b).
+  Lemma verification_principle : forall n,
+    NPeano.modulo n (Z.to_nat l) * B = n * B.
+  Admitted.
 
-End EdDSAImpl.
+  Lemma l_bound : (Z.to_nat l < pow2 b)%nat.
+  Admitted.
+
+  Lemma l_gt_zero : (Z.to_nat l <> 0)%nat.
+  Admitted.
+
+  (* TODO : move to TwistedEdwardsFacts *)
+  Lemma scalarMultOnCurve : forall n P, onCurve P -> onCurve (n * P).
+  Proof.
+    intros; induction n0; boring.
+  Admitted.
+  Hint Resolve scalarMultOnCurve.
+
+  (* TODO : move somewhere else (EdDSAFacts?) *)
+  Lemma verify_valid_passes : forall sk {n} (M : word n),
+    verify (public sk) (sign sk M) M = true.
+  Proof.
+    intros; rewrite verify_spec.
+    intros; subst R_.
+    rewrite decode_sign_split1.
+    rewrite public_spec.
+    rewrite decode_point_spec by auto.
+    rewrite decode_point_spec by auto.
+    subst S S_.
+    rewrite decode_sign_split2; simpl.
+    remember (wordToNat (H (split2 b b (H sk) ++ M))) as r.
+    rewrite public_spec.
+    remember (wordToNat
+      (H (encode_point (r * B) ++ encode_point (s sk * B) ++ M))).
+    assert (N.of_nat (NPeano.modulo (r + s sk * n1) (Z.to_nat l)) < Npow2 b)%N. {
+      remember (r + s sk * n1)%nat.
+      pose proof (NPeano.Nat.mod_upper_bound n2 (Z.to_nat l) l_gt_zero).
+      pose proof l_bound.
+      pose proof (lt_trans _ (Z.to_nat l) (pow2 b) H0 H1).
+      clear H0 H1.
+      apply Nomega.Nlt_in.
+      rewrite Nnat.Nat2N.id, Npow2_nat; auto.
+    }
+    rewrite (wordToNat_natToWord_idempotent b 
+      (NPeano.modulo (r + s sk * n1) (Z.to_nat l)) H0); clear H0.
+    rewrite verification_principle.
+  Admitted. (* relies on group properties, e.g. distributivity, exp *)
+
+End EdDSA.