diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-15 15:21:29 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-15 15:21:49 -0500 |
| commit | c711c52d057024c4b40a86f6f77f2e96ae2208ef (patch) | |
| tree | e032092b0313157fe0d3848370616855c30bd845 /src | |
| parent | 0b5115da9d2b1d9a32bdb11eb9f81ceec9999c1d (diff) | |
Finish seperating our specs: remove old non-specified code
Diffstat (limited to 'src')
| -rw-r--r-- | src/BaseSystem.v (renamed from src/Galois/BaseSystem.v) | 0 | ||||
| -rw-r--r-- | src/Curves/PointFormats.v | 774 | ||||
| -rw-r--r-- | src/Curves/ScalarMult.v | 48 | ||||
| -rw-r--r-- | src/Galois/EdDSA.v | 267 | ||||
| -rw-r--r-- | src/Galois/Galois.v | 163 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v | 243 | ||||
| -rw-r--r-- | src/Galois/GaloisRep.v | 6 | ||||
| -rw-r--r-- | src/Galois/GaloisTheory.v | 424 | ||||
| -rw-r--r-- | src/Galois/GaloisTutorial.v | 106 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v (renamed from src/Galois/ModularBaseSystem.v) | 2 | ||||
| -rw-r--r-- | src/Rep/ECRep.v | 16 | ||||
| -rw-r--r-- | src/Rep/GaloisRep.v | 26 | ||||
| -rw-r--r-- | src/Spec/Ed25519.v (renamed from src/Spec/EdDSA25519.v) | 0 | ||||
| -rw-r--r-- | src/Specific/EdDSA25519.v | 636 |
14 files changed, 1 insertions, 2710 deletions
diff --git a/src/Galois/BaseSystem.v b/src/BaseSystem.v index f0e0db077..f0e0db077 100644 --- a/src/Galois/BaseSystem.v +++ b/src/BaseSystem.v diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v deleted file mode 100644 index 2ea04cde5..000000000 --- a/src/Curves/PointFormats.v +++ /dev/null @@ -1,774 +0,0 @@ -Require Import Crypto.Galois.GaloisTheory Crypto.Galois.GaloisField. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Logic Logic.Eqdep_dec. -Require Import BinNums NArith Nnat ZArith. - -Module Type TwistedEdwardsParams (M : Modulus). - Module Export GFDefs := GaloisField M. - Axiom modulus_odd : (primeToZ M.modulus > 2)%Z. - Local Open Scope GF_scope. - Parameter a : GF. - Axiom a_nonzero : a <> 0. - Axiom a_square : exists sqrt_a, sqrt_a^2 = a. - Parameter d : GF. - Axiom d_nonsquare : forall x, x * x <> d. -End TwistedEdwardsParams. - -Definition testbit_rev p i b := Pos.testbit_nat p (b - i). - -(* TODO: decide if this should go here or somewhere else (util?) *) -(* implements Pos.iter_op only using testbit, not destructing the positive *) -Definition iter_op {A} (op : A -> A -> A) (zero : A) (bound : nat) := - fix iter (p : positive) (i : nat) (a : A) : A := - match i with - | O => zero - | S i' => if testbit_rev p i bound - then op a (iter p i' (op a a)) - else iter p i' (op a a) - end. - -Lemma testbit_rev_xI : forall p i b, (i < S b) -> - testbit_rev p~1 i (S b) = testbit_rev p i b. -Proof. - unfold testbit_rev; intros. - replace (S b - i) with (S (b - i)) by omega. - case_eq (b - S i); intros; simpl; auto. -Qed. - -Lemma testbit_rev_xO : forall p i b, (i < S b) -> - testbit_rev p~0 i (S b) = testbit_rev p i b. -Proof. - unfold testbit_rev; intros. - replace (S b - i) with (S (b - i)) by omega. - case_eq (b - S i); intros; simpl; auto. -Qed. - -Lemma testbit_rev_1 : forall i b, (i < S b) -> - testbit_rev 1%positive i (S b) = false. -Proof. - unfold testbit_rev; intros. - replace (S b - i) with (S (b - i)) by omega. - case_eq (b - S i); intros; simpl; auto. -Qed. - -Lemma iter_op_step_xI : forall {A} p i op z b (a : A), (i < S b) -> - iter_op op z (S b) p~1 i a = iter_op op z b p i a. -Proof. - induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. - simpl; rewrite testbit_rev_xI by omega. - case_eq i; intros; auto. - rewrite <- H0; simpl. - rewrite IHi by omega; auto. -Qed. - -Lemma iter_op_step_xO : forall {A} p i op z b (a : A), (i < S b) -> - iter_op op z (S b) p~0 i a = iter_op op z b p i a. -Proof. - induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. - simpl; rewrite testbit_rev_xO by omega. - case_eq i; intros; auto. - rewrite <- H0; simpl. - rewrite IHi by omega; auto. -Qed. - -Lemma iter_op_step_1 : forall {A} i op z b (a : A), (i < S b) -> - iter_op op z (S b) 1%positive i a = z. -Proof. - induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. - simpl; rewrite testbit_rev_1 by omega. - case_eq i; intros; auto. - rewrite <- H0; simpl. - rewrite IHi by omega; auto. -Qed. - -Lemma pos_size_gt0 : forall p, 0 < Pos.size_nat p. -Proof. - intros; case_eq p; intros; simpl; auto; try apply Lt.lt_0_Sn. -Qed. -Hint Resolve pos_size_gt0. - -Ltac iter_op_step := match goal with -| [ |- context[iter_op ?op ?z ?b ?p~1 ?i ?a] ] => rewrite iter_op_step_xI -| [ |- context[iter_op ?op ?z ?b ?p~0 ?i ?a] ] => rewrite iter_op_step_xO -| [ |- context[iter_op ?op ?z ?b 1%positive ?i ?a] ] => rewrite iter_op_step_1 -end; auto. - -Lemma iter_op_spec : forall b p {A} op z (a : A) (zero_id : forall x : A, op x z = x), (Pos.size_nat p <= b) -> - iter_op op z b p b a = Pos.iter_op op p a. -Proof. - induction b; intros; [pose proof (pos_size_gt0 p); omega |]. - simpl; unfold testbit_rev; rewrite Minus.minus_diag. - case_eq p; intros; simpl; iter_op_step; simpl; - rewrite IHb; rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto. -Qed. - -Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M). - Local Open Scope GF_scope. - (** Twisted Edwards curves with complete addition laws. References: - * <https://eprint.iacr.org/2008/013.pdf> - * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> - * <https://eprint.iacr.org/2015/677.pdf> - *) - Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. - Definition point := { P | onCurve P}. - Definition mkPoint := exist onCurve. - - Lemma GFdecidable_neq : forall x y : GF, Zbool.Zeq_bool x y = false -> x <> y. - Proof. - intros. intro. rewrite GFcomplete in H; intuition. - Qed. - - Ltac case_eq_GF a b := - case_eq (Zbool.Zeq_bool a b); intro Hx; - match type of Hx with - | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = true => - pose proof (GFdecidable a b Hx) - | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = false => - pose proof (GFdecidable_neq a b Hx) - end; clear Hx. - - Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. - Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. - - (* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *) - (* c=1 and an extra a in front of x^2 *) - - (* NOTE: these should serve as an example for using field *) - - - - Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. Admitted. - Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. Admitted. - - Lemma char_gt_2 : inject 2 <> 0. - intro H; inversion H; clear H. - pose proof modulus_odd. - rewrite Zmod_small in H1; intuition; auto; omega. - Qed. - - Ltac whatsNotZero := - repeat match goal with - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (lhs <> 0) by (rewrite H; auto) - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (rhs <> 0) by (rewrite H; auto) - | [H: (?a^?p)%GF <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - let Y:=fresh in let Z:=fresh in try ( - assert (p <> 0%N) as Z by (intro Y; inversion Y); - assert (a <> 0) by (eapply root_nonzero; eauto); - clear Z) - | [H: (?a*?b)%GF <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (a <> 0) by (eapply mul_nonzero_l; eauto) - | [H: (?a*?b)%GF <> 0 |- _ ] => - match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (b <> 0) by (eapply mul_nonzero_r; eauto) - end. - - Lemma edwardsAddComplete' x1 y1 x2 y2 : - onCurve (x1,y1) -> - onCurve (x2, y2) -> - (d*x1*x2*y1*y2)^2 <> 1. - Proof. - unfold onCurve; intuition; whatsNotZero. - - pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. - destruct a_square as [sqrt_a a_square]. - rewrite <-a_square in *. - - (* Furthermore... *) - pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. - rewrite H0 in Heqt at 2. - replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) - with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. - rewrite H1 in Heqt. - replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. - rewrite <-H in Heqt. - - (* main equation for both potentially nonzero denominators *) - case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0; - try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => - assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = - f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) - (d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1)) as Heqw1 by field; - rewrite H1 in *; - replace (1 * y1^2) with (y1^2) in * by field; - rewrite <- Heqt in *; - assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / - (x1 * y1 * (f (sqrt_a * x2) y2))^2) - by (rewriteAny; field; auto); - match goal with [H: d = (?n^2)/(?l^2) |- _ ] => - destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) - end - end. - - assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - - replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field. - - (* contradiction: product of nonzero things is zero *) - destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. - destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. - apply Ha_nonzero; field. - Qed. - Lemma edwardsAddCompletePlus x1 y1 x2 y2 : - onCurve (x1,y1) -> - onCurve (x2, y2) -> - (1 + d*x1*x2*y1*y2) <> 0. - Proof. - unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field. - intro; rewrite H2 in H1; intuition. - Qed. - - Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : - onCurve (x1,y1) -> - onCurve (x2, y2) -> - (1 - d*x1*x2*y1*y2) <> 0. - Proof. - unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field. - intro; rewrite H2 in H1; apply H1; field. - Qed. - Hint Resolve edwardsAddCompletePlus edwardsAddCompleteMinus. - - Definition projX (P:point) := fst (proj1_sig P). - Definition projY (P:point) := snd (proj1_sig P). - - Definition checkOnCurve (x y: GF) : if Zbool.Zeq_bool (a*x^2 + y^2)%GF (1 + d*x^2*y^2)%GF then point else True. - break_if; trivial. exists (x, y). apply GFdecidable. exact Heqb. - Defined. - Local Hint Unfold onCurve mkPoint. - - Definition zero : point. refine (mkPoint (0, 1) _). - abstract (unfold onCurve; field). - Defined. - - Definition unifiedAdd' (P1' P2' : (GF*GF)) := - let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - - Lemma unifiedAdd'_onCurve x1 y1 x2 y2 x3 y3 - (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : - onCurve (x1,y1) -> onCurve (x2, y2) -> onCurve (x3, y3). - Proof. - (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; - * c=1 and an extra a in front of x^2 *) - - unfold unifiedAdd', onCurve in *; injection H; clear H; intros. - - Ltac t x1 y1 x2 y2 := - assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 - = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); - assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 - = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). - t x1 y1 x2 y2; t x2 y2 x1 y1. - - remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - - (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. - assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). - assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( - (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * - y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). - replace 1 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. - - match goal with [ |- ?x = 1 ] => replace x with - ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + - ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto. - - rewrite <-HT1, <-HT2; field; rewrite HT1. - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; simpl; auto. - - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; auto. - Qed. - - Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 -> - onCurve (unifiedAdd' P1 P2). - Proof. - intros; destruct P1, P2. - remember (unifiedAdd' (g, g0) (g1, g2)) as p; destruct p. - eapply unifiedAdd'_onCurve; eauto. - Qed. - - Definition unifiedAdd (P1 P2 : point) : point := - let 'exist P1' pf1 := P1 in - let 'exist P2' pf2 := P2 in - mkPoint (unifiedAdd' P1' P2') (unifiedAdd'_onCurve' _ _ pf1 pf2). - Local Infix "+" := unifiedAdd. - - Fixpoint scalarMult (n:nat) (P : point) : point := - match n with - | O => zero - | S n' => P + scalarMult n' P - end - . - - Definition doubleAndAdd (b n : nat) (P : point) : point := - match N.of_nat n with - | 0%N => zero - | N.pos p => iter_op unifiedAdd zero b p b P - end. - - Hint Resolve char_gt_2. -End CompleteTwistedEdwardsCurve. - - -Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M). - Local Open Scope GF_scope. - Module Curve := CompleteTwistedEdwardsCurve M P. - Parameter point : Type. - Parameter encode : (GF*GF) -> point. - Parameter decode : point -> (GF*GF). - Parameter unifiedAdd : point -> point -> point. - - Parameter rep : point -> (GF*GF) -> Prop. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Axiom encode_rep: forall P, encode P ~= P. - Axiom decode_rep : forall P rP, P ~= rP -> decode P = rP. - Axiom unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). -End CompleteTwistedEdwardsPointFormat. - -Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). - Local Open Scope GF_scope. - Module Import Curve := CompleteTwistedEdwardsCurve M P. - - Lemma point_eq : forall x1 x2 y1 y2, - x1 = x2 -> y1 = y2 -> - forall p1 p2, - mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. - Proof. - intros; subst; f_equal. - apply (UIP_dec). (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) - apply GF_eq_dec. - Qed. - Hint Resolve point_eq. - - Local Hint Unfold unifiedAdd onCurve mkPoint. - Ltac twisted := autounfold; intros; - repeat (match goal with - | [ x : point |- _ ] => destruct x; unfold onCurve in * - | [ x : (GF*GF)%type |- _ ] => destruct x - | [ |- exist _ _ _ = exist _ _ _ ] => eapply point_eq - end; simpl; repeat (ring || f_equal)). - Local Infix "+" := unifiedAdd. - Lemma twistedAddComm : forall A B, (A+B = B+A). - Proof. - twisted. - Qed. - - Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. - Proof. - (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) - Admitted. - - Lemma zeroIsIdentity' : forall P, unifiedAdd' P (proj1_sig zero) = P. - unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field; auto. - Qed. - - Lemma zeroIsIdentity : forall P, P + zero = P. - Proof. - unfold zero, unifiedAdd. - destruct P as [[x y] pf]. - simpl. - apply point_eq; field; auto. - Qed. - Hint Resolve zeroIsIdentity. - - Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P). - Proof. - intros. - replace (n + n)%nat with (n * 2)%nat by omega. - induction n; simpl; auto. - rewrite twistedAddAssoc. - f_equal; auto. - Qed. - - Lemma iter_op_double : forall p P, - Pos.iter_op unifiedAdd (p + p) P = Pos.iter_op unifiedAdd p (P + P). - Proof. - intros. - rewrite Pos.add_diag. - unfold Pos.iter_op; simpl. - auto. - Qed. - - Lemma xO_neq1 : forall p, (1 < p~0)%positive. - Proof. - induction p; simpl; auto. - replace 2%positive with (Pos.succ 1) by auto. - apply Pos.lt_succ_diag_r. - Qed. - - Lemma xI_neq1 : forall p, (1 < p~1)%positive. - Proof. - induction p; simpl; auto. - replace 3%positive with (Pos.succ (Pos.succ 1)) by auto. - pose proof (Pos.lt_succ_diag_r (Pos.succ 1)). - pose proof (Pos.lt_succ_diag_r 1). - apply (Pos.lt_trans _ _ _ H0 H). - Qed. - - Lemma xI_is_succ : forall n p - (H : Pos.of_succ_nat n = p~1%positive), - (Pos.to_nat (2 * p))%nat = n. - Proof. - induction n; intros; simpl in *; auto. { - pose proof (xI_neq1 p). - rewrite H in H0. - pose proof (Pos.lt_irrefl p~1). - intuition. - } { - rewrite Pos.xI_succ_xO in H. - pose proof (Pos.succ_inj _ _ H); clear H. - rewrite Pos.of_nat_succ in H0. - rewrite <- Pnat.Pos2Nat.inj_iff in H0. - rewrite Pnat.Pos2Nat.inj_xO in H0. - rewrite Pnat.Nat2Pos.id in H0 by apply NPeano.Nat.neq_succ_0. - rewrite H0. - apply Pnat.Pos2Nat.inj_xO. - } - Qed. - - Lemma xO_is_succ : forall n p - (H : Pos.of_succ_nat n = p~0%positive), - Pos.to_nat (Pos.pred_double p) = n. - Proof. - induction n; intros; simpl; auto. { - pose proof (xO_neq1 p). - simpl in H; rewrite H in H0. - pose proof (Pos.lt_irrefl p~0). - intuition. - } { - rewrite Pos.pred_double_spec. - rewrite <- Pnat.Pos2Nat.inj_iff in H. - rewrite Pnat.Pos2Nat.inj_xO in H. - rewrite Pnat.SuccNat2Pos.id_succ in H. - rewrite Pnat.Pos2Nat.inj_pred by apply xO_neq1. - rewrite <- NPeano.Nat.succ_inj_wd. - rewrite Pnat.Pos2Nat.inj_xO. - rewrite <- H. - auto. - } - Qed. - - Lemma size_of_succ : forall n, - Pos.size_nat (Pos.of_nat n) <= Pos.size_nat (Pos.of_nat (S n)). - Proof. - intros; induction n; [simpl; auto|]. - apply Pos.size_nat_monotone. - apply Pos.lt_succ_diag_r. - Qed. - - Lemma doubleAndAdd_spec : forall n b P, (Pos.size_nat (Pos.of_nat n) <= b) -> - scalarMult n P = doubleAndAdd b n P. - Proof. - induction n; auto; intros. - unfold doubleAndAdd; simpl. - rewrite Pos.of_nat_succ. - rewrite iter_op_spec by auto. - case_eq (Pos.of_nat (S n)); intros. { - simpl; f_equal. - rewrite (IHn b) by (pose proof (size_of_succ n); omega). - unfold doubleAndAdd. - rewrite H0 in H. - rewrite <- Pos.of_nat_succ in H0. - rewrite <- (xI_is_succ n p) by apply H0. - rewrite Znat.positive_nat_N; simpl. - rewrite iter_op_spec; auto. - } { - simpl; f_equal. - rewrite (IHn b) by (pose proof (size_of_succ n); omega). - unfold doubleAndAdd. - rewrite <- (xO_is_succ n p) by (rewrite Pos.of_nat_succ; auto). - rewrite Znat.positive_nat_N; simpl. - rewrite <- Pos.succ_pred_double in H0. - rewrite H0 in H. - rewrite iter_op_spec by - (try (pose proof (Pos.lt_succ_diag_r (Pos.pred_double p)); - apply Pos.size_nat_monotone in H1; omega); auto). - rewrite <- iter_op_double. - rewrite Pos.add_diag. - rewrite <- Pos.succ_pred_double. - rewrite Pos.iter_op_succ by apply twistedAddAssoc; auto. - } { - rewrite <- Pnat.Pos2Nat.inj_iff in H0. - rewrite Pnat.Nat2Pos.id in H0 by auto. - rewrite Pnat.Pos2Nat.inj_1 in H0. - assert (n = 0)%nat by omega; subst. - auto. - } - Qed. - -End CompleteTwistedEdwardsFacts. - -Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export GFDefs := GaloisField M. - Axiom modulus_odd : (primeToZ M.modulus > 2)%Z. - Local Open Scope GF_scope. - Axiom char_gt_2 : inject 2 <> 0. - Definition a := inject (- 1). - Axiom a_nonzero : a <> 0. - Axiom a_square : exists sqrt_a, sqrt_a^2 = a. - Parameter d : GF. - Axiom d_nonsquare : forall x, x * x <> d. -End Minus1Params. - -Module ExtendedM1 (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P. - Local Hint Unfold a. - Local Open Scope GF_scope. - Module Import Facts := CompleteTwistedEdwardsFacts M P. - Module Import Curve := Facts.Curve. - - (* TODO: move to wherever GF theorems are *) - Lemma GFdiv_1 : forall x, x/1 = x. - Proof. - intros; field; auto. - Qed. - Hint Resolve GFdiv_1. - - (** [extended] represents a point on an elliptic curve using extended projective - * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) - Record extended := mkExtended {extendedX : GF; - extendedY : GF; - extendedZ : GF; - extendedT : GF}. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). - Definition point := extended. - - Definition encode (P : (GF*GF)) : point := - let '(x, y) := P in (x, y, 1, x*y). - Definition decode (P : point) : GF * GF := - let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)). - Definition rep (P:point) (rP:(GF*GF)) : Prop := - let '(X, Y, Z, T) := P in - decode P = rP /\ - Z <> 0 /\ - T = X*Y/Z. - Local Hint Unfold encode decode rep. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Ltac extended_tac := - repeat progress (autounfold; intros); - repeat match goal with - | [ p : (GF*GF)%type |- _ ] => - let x := fresh "x" in - let y := fresh "y" in - destruct p as [x y] - | [ p : point |- _ ] => - let X := fresh "X" in - let Y := fresh "Y" in - let Z := fresh "Z" in - let T := fresh "T" in - destruct p as [X Y Z T] - | [ H: _ /\ _ |- _ ] => destruct H - | [ |- _ /\ _ ] => split - | [ H: @eq (GF * GF)%type _ _ |- _ ] => invcs H - | [ H: @eq GF ?x _ |- _ ] => isVar x; rewrite H; clear H - | [ |- @eq (GF * GF)%type _ _] => apply f_equal2 - | [ |- @eq GF _ _] => field - | [ |- _ ] => progress eauto - end. - - Lemma encode_rep : forall P, encode P ~= P. - Proof. - extended_tac. - Qed. - - Lemma decode_rep : forall P rP, P ~= rP -> decode P = rP. - Proof. - extended_tac. - Qed. - - Local Notation "2" := (inject 2). - (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) - Definition unifiedAdd (P1 P2 : point) : point := - let '(X1, Y1, Z1, T1) := P1 in - let '(X2, Y2, Z2, T2) := P2 in - let A := (Y1-X1)*(Y2-X2) in - let B := (Y1+X1)*(Y2+X2) in - let C := T1*2*d*T2 in - let D := Z1*2 *Z2 in - let E := B-A in - let F := D-C in - let G := D+C in - let H := B+A in - let X3 := E*F in - let Y3 := G*H in - let T3 := E*H in - let Z3 := F*G in - (X3, Y3, Z3, T3). - Local Hint Unfold unifiedAdd. - - Delimit Scope extendedM1_scope with extendedM1. - Infix "+" := unifiedAdd : extendedM1_scope. - - Local Hint Unfold unifiedAdd'. - Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). - Proof. - extended_tac; - pose proof (edwardsAddCompletePlus _ _ _ _ H0 H) as Hp; - pose proof (edwardsAddCompleteMinus _ _ _ _ H0 H) as Hm. - - (* If we we had reasoning modulo associativity and commutativity, - * the following tactic would probably solve all 10 goals here: - repeat match goal with [H1: @eq GF _ _, H2: @eq GF _ _ |- _ ] => - let H := fresh "H" in ( - pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H; - match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end - ) || ( - pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H; - match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end - ); repeat apply mul_nonzero_nonzero; auto 10 - end. - *) - - - replace (Z0 * Z * Z0 * Z + d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto). - repeat apply mul_nonzero_nonzero. - + replace (Z0 * 2 * Z - X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - + replace (Z0 * 2 * Z + X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. - Qed. -End ExtendedM1. - - -(* -(** [precomputed] represents a point on an elliptic curve using "precomputed" -* Edwards coordinates, as used for fixed-base scalar multiplication -* (see <http://ed25519.cr.yp.to/ed25519-20110926.pdf> section 4: addition). *) -Record precomputed := mkPrecomputed {precomputedSum : GF; - precomputedDifference : GF; - precomputed2dxy : GF}. -Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed := -let x := twistedX P in -let y := twistedY P in -mkPrecomputed (y+x) (y-x) (2*d*x*y). -*) - -Module WeirstrassMontgomery (Import M : Modulus). - Module Import GT := GaloisTheory M. - Local Open Scope GF_scope. - Local Notation "2" := (1+1). - Local Notation "3" := (1+1+1). - Local Notation "4" := (1+1+1+1). - Local Notation "27" := (3*3*3). - (** [weierstrass] represents a point on an elliptic curve using Weierstrass - * coordinates (<http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf>) definition 13.1*) - Record weierstrass := mkWeierstrass {weierstrassX : GF; weierstrassY : GF}. - Definition weierstrassOnCurve (a1 a2 a3 a4 a5 a6:GF) (P : weierstrass) : Prop := - let x := weierstrassX P in - let y := weierstrassY P in - y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6. - - (** [montgomery] represents a point on an elliptic curve using Montgomery - * coordinates (see <https://en.wikipedia.org/wiki/Montgomery_curve>) *) - Record montgomery := mkMontgomery {montgomeryX : GF; montgomeryY : GF}. - Definition montgomeryOnCurve (B A:GF) (P : montgomery) : Prop := - let x := montgomeryX P in - let y := montgomeryY P in - B*y^2 = x^3 + A*x^2 + x. - - (** see <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> section 13.2.3.c and <https://en.wikipedia.org/wiki/Montgomery_curve#Equivalence_with_Weierstrass_curves> *) - Definition montgomeryToWeierstrass (B A:GF) (P : montgomery) : weierstrass := - let x := montgomeryX P in - let y := montgomeryY P in - mkWeierstrass (x/B + A/(3*B)) (y/B). - - Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery), - let a4 := 1/B^2 - A^2/(3*B^2) in - let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in - let P' := montgomeryToWeierstrass B A P in - montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'. - Proof. - intros. - unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *. - remember (weierstrassY P') as y in *. - remember (weierstrassX P') as x in *. - remember (montgomeryX P) as u in *. - remember (montgomeryY P) as v in *. - clear Hequ Heqv Heqy Heqx P'. - (* This is not currently important and makes field run out of memory. Maybe - * because I transcribed it incorrectly... *) - Abort. - - - (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom.html> *) - Definition montgomeryAddDistinct (B A:GF) (P1 P2:montgomery) : montgomery := - let x1 := montgomeryX P1 in - let y1 := montgomeryY P1 in - let x2 := montgomeryX P2 in - let y2 := montgomeryY P2 in - mkMontgomery - (B*(y2-y1)^2/(x2-x1)^2-A-x1-x2) - ((2*x1+x2+A)*(y2-y1)/(x2-x1)-B*(y2-y1)^3/(x2-x1)^3-y1). - Definition montgomeryDouble (B A:GF) (P1:montgomery) : montgomery := - let x1 := montgomeryX P1 in - let y1 := montgomeryY P1 in - mkMontgomery - (B*(3*x1^2+2*A*x1+1)^2/(2*B*y1)^2-A-x1-x1) - ((2*x1+x1+A)*(3*x1^2+2*A*x1+1)/(2*B*y1)-B*(3*x1^2+2*A*x1+1)^3/(2*B*y1)^3-y1). - Definition montgomeryNegate P := mkMontgomery (montgomeryX P) (0-montgomeryY P). - - (** [montgomeryXFrac] represents a point on an elliptic curve using Montgomery x - * coordinate stored as fraction as in - * <http://cr.yp.to/ecdh/curve25519-20060209.pdf> appendix B. *) - Record montgomeryXFrac := mkMontgomeryXFrac {montgomeryXFracX : GF; montgomeryXFracZ : GF}. - Definition montgomeryToMontgomeryXFrac P := mkMontgomeryXFrac (montgomeryX P) 1. - Definition montgomeryXFracToMontgomeryX P : GF := (montgomeryXFracX P) / (montgomeryXFracZ P). - - (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom-xz.html#ladder-mladd-1987-m>, - * also appears in <https://tools.ietf.org/html/draft-josefsson-tls-curve25519-06#appendix-A.1.3> *) - Definition montgomeryDifferentialDoubleAndAdd (a : GF) - (X1 : GF) (P2 P3 : montgomeryXFrac) : (montgomeryXFrac * montgomeryXFrac) := - let X2 := montgomeryXFracX P2 in - let Z2 := montgomeryXFracZ P2 in - let X3 := montgomeryXFracX P3 in - let Z3 := montgomeryXFracZ P3 in - let A := X2 + Z2 in - let AA := A^2 in - let B := X2 - Z2 in - let BB := B^2 in - let E := AA - BB in - let C := X3 + Z3 in - let D := X3 - Z3 in - let DA := D * A in - let CB := C * B in - let X5 := (DA + CB)^2 in - let Z5 := X1 * (DA - CB)^2 in - let X4 := AA * BB in - let Z4 := E * (BB + (a-2)/4 * E) in - (mkMontgomeryXFrac X4 Z4, mkMontgomeryXFrac X5 Z5). - - (* - (* <https://eprint.iacr.org/2008/013.pdf> Theorem 3.2. *) - (* TODO: exceptional points *) - Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery := - let x := twistedX P in - let y := twistedY P in - mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)). - Definition montgomeryToTwisted (B A:GF) (P : montgomery) : twisted := - let X := montgomeryX P in - let Y := montgomeryY P in - mkTwisted (X/Y) ((X-1)/(X+1)). - *) - -End WeirstrassMontgomery. diff --git a/src/Curves/ScalarMult.v b/src/Curves/ScalarMult.v deleted file mode 100644 index d71550413..000000000 --- a/src/Curves/ScalarMult.v +++ /dev/null @@ -1,48 +0,0 @@ -Require Import ZArith.BinInt. -Require Import List Util.ListUtil. - - -Section ScalarMult. - Variable G : Type. - Variable neutral : G. - Variable add : G -> G -> G. - Local Infix "+" := add. - - Fixpoint scalarMultSpec (n:nat) (g:G) : G := - match n with - | O => neutral - | S n' => g + scalarMultSpec n' g - end - . - - (* ng = - * (n/2)(g+g) + g if n odd - * (n/2)(g+g) if n even - * g if n == 1 - *) - Fixpoint scalarMultPos (n:positive) (g:G) : G := - match n with - | xI n' => scalarMultPos n' (g + g) + g - | xO n' => scalarMultPos n' (g + g) - | xH => g - end - . - - Definition scalarMultNat (n:nat) (g:G) : G := - match n with - | O => neutral - | S n' => scalarMultPos (Pos.of_succ_nat n') g - end - . - - Definition sel {T} (b:bool) (x y:T) := if b then y else x. - Definition scalarMultStaticZ (bitLengthN:nat) (n:Z) (g:G): G := - fst (fold_right - (fun (i : nat) (s : G * G) => let (Q, P) := s in - let Q' := sel (Z.testbit (Z.of_nat i) n) Q (Q + P) in - let P' := P+P in - (Q', P + P)) - (neutral, g) (* initial state *) - (seq 0 bitLengthN)) (* range of i *) - . -End ScalarMult. diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v deleted file mode 100644 index c0699f316..000000000 --- a/src/Galois/EdDSA.v +++ /dev/null @@ -1,267 +0,0 @@ -Require Import ZArith NPeano. -Require Import Bedrock.Word. -Require Import Crypto.Curves.PointFormats. -Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisField. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import VerdiTactics. - -Local Open Scope nat_scope. -Local Coercion Z.to_nat : Z >-> nat. - -(* 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 - | eq_refl => w - end)); abstract omega. -Defined. - -Class Encoding (T B:Type) := { - enc : T -> B ; - dec : B -> option T ; - encoding_valid : forall x, dec (enc x) = Some x -}. -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 : Prime. - Axiom q_odd : (q > 2)%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 <: Modulus. - Definition modulus := q. - 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 GFDefs := GaloisField Modulus_q. - Local Open Scope GF_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 : GF. - Axiom a_nonzero : a <> 0%GF. - 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 : GF. - 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. *) - - Module CurveParameters <: TwistedEdwardsParams Modulus_q. - Module GFDefs := GFDefs. - Definition modulus_odd : (Modulus_q.modulus > 2)%Z := q_odd. - Definition a : GF := a. - Definition a_nonzero := a_nonzero. - Definition a_square := a_square. - Definition d := d. - Definition d_nonsquare := d_nonsquare. - End CurveParameters. - Module Export Facts := CompleteTwistedEdwardsFacts Modulus_q CurveParameters. - Module Export Curve := Facts.Curve. - Parameter B : point. (* 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 : Prime. - 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 GF as word (b-1). - Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b. - Parameter PointEncoding : encoding of point as word b. - -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. - - 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 = Curve.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. diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v deleted file mode 100644 index 86ce7f05e..000000000 --- a/src/Galois/Galois.v +++ /dev/null @@ -1,163 +0,0 @@ - -Require Import BinInt BinNat ZArith Znumtheory. -Require Import Eqdep_dec. -Require Import Tactics.VerdiTactics. - -(* This file is for the high-level type definitions of - * GF, Primes, Moduli, etc. and their notations and essential - * operations. - * - * The lemmas required for the ring and field theories are - * in GaloisTheory.v and the actual tactic implementations - * for the field are in GaloisField.v. An introduction to the - * use of our implementation of the Galois field is in - * GaloisTutorial.v - *) - -Section GaloisPreliminaries. - (* The core prime modulus type, relying on Znumtheory's prime *) - Definition Prime := {x: Z | prime x}. - - (* Automagically coerce primes to Z *) - Definition primeToZ(x: Prime) := proj1_sig x. - Coercion primeToZ: Prime >-> Z. -End GaloisPreliminaries. - -(* A module to hold the field's modulus, which will be an argument to - * all of our Galois modules. - *) -Module Type Modulus. - Parameter modulus: Prime. -End Modulus. - -(* The core Galois Field model *) -Module Galois (M: Modulus). - Import M. - - (* The sigma definition of an element of the field: we have - * an element corresponding to the values in Z which can be - * produced by a 'mod' operation. - *) - Definition GF := {x: Z | x = x mod modulus}. - - Delimit Scope GF_scope with GF. - Local Open Scope GF_scope. - - (* Automagically convert GF to Z when needed *) - Definition GFToZ(x: GF) := proj1_sig x. - Coercion GFToZ: GF >-> Z. - - (* Automagically convert Z to GF when needed *) - Definition inject(x: Z): GF. - exists (x mod modulus). - abstract (rewrite Zmod_mod; trivial). - Defined. - - Coercion inject : Z >-> GF. - - (* Convert Z to GF without a mod operation, for when the modulus is opaque *) - Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True. - break_if; [|trivial]. - exists x. - destruct (Bool.andb_true_eq _ _ (eq_sym Heqb)); clear Heqb. - erewrite Zmod_small; [trivial|]. - intuition. - - rewrite <- Z.leb_le; auto. - - rewrite <- Z.ltb_lt; auto. - Defined. - - (* Core lemma: equality in GF implies equality in Z *) - Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. - Proof. - destruct x, y; intuition; simpl in *; try congruence. - subst x. - f_equal. - apply UIP_dec. - apply Z.eq_dec. - Qed. - - (* Core values: One and Zero *) - Definition GFzero: GF. - exists 0. - abstract trivial. - Defined. - - Definition GFone: GF. - exists 1. - abstract( symmetry; apply Zmod_small; intuition; - destruct modulus; simpl; - apply prime_ge_2 in p; intuition). - Defined. - - Lemma GFone_nonzero : GFone <> GFzero. - Proof. - unfold GFone, GFzero. - intuition; solve_by_inversion. - Qed. - Hint Resolve GFone_nonzero. - - (* Elementary operations: +, -, * *) - Definition GFplus(x y: GF): GF. - exists ((x + y) mod modulus); - abstract (rewrite Zmod_mod; trivial). - Defined. - - Definition GFminus(x y: GF): GF. - exists ((x - y) mod modulus). - abstract (rewrite Zmod_mod; trivial). - Defined. - - Definition GFmult(x y: GF): GF. - exists ((x * y) mod modulus). - abstract (rewrite Zmod_mod; trivial). - Defined. - - Definition GFopp(x: GF): GF := GFminus GFzero x. - - (* Modular exponentiation *) - Fixpoint GFexp' (x: GF) (power: positive) := - match power with - | xH => x - | xO power' => GFexp' (GFmult x x) power' - | xI power' => GFmult x (GFexp' (GFmult x x) power') - end. - - Definition GFexp (x: GF) (power: N): GF := - match power with - | N0 => GFone - | Npos power' => GFexp' x power' - end. - - (* Preliminaries to inversion in a prime field *) - Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero -> - GFexp g e = GFone. - - Definition Totient := {e: N | isTotient e}. - - (* Get a totient via Fermat's little theorem *) - Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)). - Admitted. - - Definition totient : Totient. - exists (N.pred (Z.to_N modulus)). - exact fermat_little_theorem. - Defined. - - Definition totientToN(x: Totient) := proj1_sig x. - Coercion totientToN: Totient >-> N. - - (* Define inversion and division *) - Definition GFinv(x: GF): GF := GFexp x (N.pred totient). - - Definition GFdiv(x y: GF): GF := GFmult x (GFinv y). - - (* Notations for all of the operations we just made *) - Notation "1" := GFone : GF_scope. - Notation "0" := GFzero : GF_scope. - Infix "+" := GFplus : GF_scope. - Infix "-" := GFminus : GF_scope. - Infix "*" := GFmult : GF_scope. - Infix "/" := GFdiv : GF_scope. - Infix "^" := GFexp : GF_scope. - -End Galois. diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v deleted file mode 100644 index f3c769e67..000000000 --- a/src/Galois/GaloisField.v +++ /dev/null @@ -1,243 +0,0 @@ -Require Import BinInt BinNat ZArith Znumtheory. -Require Import BoolEq Field_theory. -Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Tactics.VerdiTactics. - -(* This file is for the actual field tactics and some specialized - * morphisms that help field operate. - * - * When you want a Galois Field, this is the /only module/ you - * should import, because it automatically pulls in everything - * from Galois and the Modulus. - *) -Module GaloisField (M: Modulus). - Module G := Galois M. - Module T := GaloisTheory M. - Export M G T. - - (* Define a "ring morphism" between GF and Z, i.e. an equivalence - * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. - * - * Doing this allows us to do our coefficient manipulations in Z - * rather than GF, because we know it's equivalent to inject the - * result afterward. - *) - Lemma GFring_morph: - ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq - 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - inject. - Proof. - constructor; intros; try galois; - try (apply gf_eq; simpl; intuition). - - apply Zmod_small; destruct modulus; simpl; - apply prime_ge_2 in p; intuition. - - replace (- (x mod modulus)) with (0 - (x mod modulus)); - try rewrite Zminus_mod_idemp_r; trivial. - - replace x with y; intuition. - symmetry; apply Zeq_bool_eq; trivial. - Qed. - - (* Redefine our division theory under the ring morphism *) - Lemma GFmorph_div_theory: - div_theory eq Zplus Zmult inject Z.quotrem. - Proof. - constructor; intros; intuition. - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - eq_remove_proofs; demod; - rewrite <- (Z.quot_rem' a b); - destruct a; simpl; trivial. - Qed. - - (* Some simple utility lemmas *) - Lemma injectZeroIsGFZero : - GFzero = inject 0. - Proof. - apply gf_eq; simpl; trivial. - Qed. - - Lemma injectOneIsGFOne : - GFone = inject 1. - Proof. - apply gf_eq; simpl; intuition. - symmetry; apply Zmod_small; destruct modulus; simpl; - apply prime_ge_2 in p; intuition. - Qed. - - Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py. - Proof. - intuition; solve_by_inversion. - Qed. - - (* Change all GFones to (inject 1) and GFzeros to (inject 0) so that - * we can use our ring morphism to simplify them - *) - Ltac GFpreprocess := - repeat rewrite injectZeroIsGFZero; - repeat rewrite injectOneIsGFOne. - - (* Split up the equation (because field likes /\, then - * change back all of our GFones and GFzeros. - * - * TODO (adamc): what causes it to generate these subproofs? - *) - Ltac GFpostprocess := - repeat split; - repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] => - replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity - end; - repeat rewrite <- injectZeroIsGFZero; - repeat rewrite <- injectOneIsGFOne. - - (* Tactic to passively convert from GF to Z in special circumstances *) - Ltac GFconstant t := - match t with - | inject ?x => x - | _ => NotConstant - end. - - (* Add our ring with all the fixin's *) - Add Ring GFring_Z : GFring_theory - (morphism GFring_morph, - constants [GFconstant], - div GFmorph_div_theory, - power_tac GFpower_theory [GFexp_tac]). - - (* Add our field with all the fixin's *) - Add Field GFfield_Z : GFfield_theory - (morphism GFring_morph, - preprocess [GFpreprocess], - postprocess [GFpostprocess], - constants [GFconstant], - div GFmorph_div_theory, - power_tac GFpower_theory [GFexp_tac]). - - Local Open Scope GF_scope. - - Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y. - Proof. - intros ? ? ? z_nonzero mul_z_eq. - replace x with (x * 1) by field. - rewrite <- (GF_multiplicative_inverse z_nonzero). - replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring. - rewrite mul_z_eq. - replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring. - rewrite GF_multiplicative_inverse; auto; field. - Qed. - - Lemma GF_mul_0_l : forall x, 0 * x = 0. - Proof. - intros; field. - Qed. - - Lemma GF_mul_0_r : forall x, x * 0 = 0. - Proof. - intros; field. - Qed. - - Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}. - intros. - assert (H := Z.eq_dec (inject x) (inject y)). - - destruct H. - - - left; galois; intuition. - - - right; intuition. - rewrite H in n. - assert (y = y); intuition. - Qed. - - Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0. - intros; intuition; subst. - assert (0 * b = 0) by field; intuition. - Qed. - - Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0. - intros; intuition; subst. - assert (a * 0 = 0) by field; intuition. - Qed. - - Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0. - intros. - assert (Z := GF_eq_dec a 0); destruct Z. - - - left; intuition. - - - assert (a * b / a = 0) by - ( rewrite H; field; intuition ). - - field_simplify in H0. - replace (b/1) with b in H0 by (field; intuition). - right; intuition. - apply n in H0; intuition. - Qed. - - Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0. - intros; intuition; subst. - apply mul_zero_why in H1. - destruct H1; subst; intuition. - Qed. - Hint Resolve mul_nonzero_nonzero. - - Lemma GFexp_distr_mul : forall x y z, (0 <= z)%N -> - (x ^ z) * (y ^ z) = (x * y) ^ z. - Proof. - intros. - replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id. - apply natlike_ind with (x := Z.of_N z); simpl; [ field | | - replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto]. - intros z' z'_nonneg IHz'. - rewrite Z2N.inj_succ by auto. - rewrite (GFexp_pred x) by apply N.neq_succ_0. - rewrite (GFexp_pred y) by apply N.neq_succ_0. - rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0. - rewrite N.pred_succ. - rewrite <- IHz'. - field. - Qed. - - Lemma GF_square_mul : forall x y z, (y <> 0) -> - x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z. - Proof. - intros ? ? ? y_nonzero A. - exists (x / y). - assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div. { - unfold GFdiv, GFexp, GFexp'. - replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring. - unfold GFinv. - destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ]; - [ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field. - simpl. - do 2 rewrite <- Z2N.inj_pred. - replace 0%N with (Z.to_N 0%Z) by auto. - apply Z2N.inj_le; modulus_bound. - } - assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto). - rewrite (GF_mul_eq _ z (y ^ 2)); auto. - unfold GFdiv. - rewrite <- A. - field; auto. - Qed. - - Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x. - Proof. - intros. - (* TODO(jadep) *) - Admitted. - - Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y. - Proof. - split; intro; subst; field. - Qed. - - Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x. - Proof. - intros; field. - Qed. - -End GaloisField. diff --git a/src/Galois/GaloisRep.v b/src/Galois/GaloisRep.v deleted file mode 100644 index 4f4dce486..000000000 --- a/src/Galois/GaloisRep.v +++ /dev/null @@ -1,6 +0,0 @@ - - -Module Type GaloisRep . - -End GaloisRep. - diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v deleted file mode 100644 index feb37007a..000000000 --- a/src/Galois/GaloisTheory.v +++ /dev/null @@ -1,424 +0,0 @@ - -Require Import BinInt BinNat ZArith Znumtheory NArith. -Require Import Eqdep_dec. -Require Export Coq.Classes.Morphisms Setoid. -Require Export Ring_theory Field_theory Field_tac. -Require Export Crypto.Galois.Galois. - -Set Implicit Arguments. -Unset Strict Implicits. - -(* This file is for all the lemmas we need to construct a ring, - * field, power, and division theory on a Galois Field. - *) -Module GaloisTheory (M: Modulus). - Module G := Galois M. - Export M G. - - (***** Preliminary Tactics *****) - - (* Fails iff the input term does some arithmetic with mod'd values. *) - Ltac notFancy E := - match E with - | - (_ mod _) => idtac - | context[_ mod _] => fail 1 - | _ => idtac - end. - - Lemma Zplus_neg : forall n m, n + -m = n - m. - Proof. - auto. - Qed. - - Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n. - Proof. - intros; rewrite H; trivial. - Qed. - - (* Remove redundant [mod] operations from the conclusion. *) - Ltac demod := - repeat match goal with - | [ |- context[(?x mod _ + _) mod _] ] => - notFancy x; rewrite (Zplus_mod_idemp_l x) - | [ |- context[(_ + ?y mod _) mod _] ] => - notFancy y; rewrite (Zplus_mod_idemp_r y) - | [ |- context[(?x mod _ - _) mod _] ] => - notFancy x; rewrite (Zminus_mod_idemp_l x) - | [ |- context[(_ - ?y mod _) mod _] ] => - notFancy y; rewrite (Zminus_mod_idemp_r _ y) - | [ |- context[(?x mod _ * _) mod _] ] => - notFancy x; rewrite (Zmult_mod_idemp_l x) - | [ |- context[(_ * (?y mod _)) mod _] ] => - notFancy y; rewrite (Zmult_mod_idemp_r y) - | [ |- context[(?x mod _) mod _] ] => - notFancy x; rewrite (Zmod_mod x) - | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in * - end. - - (* Remove exists under equals: we do this a lot *) - Ltac eq_remove_proofs := match goal with - | [ |- ?a = ?b ] => - assert (Q := gf_eq a b); - simpl in *; apply Q; clear Q - end. - - (* General big hammer for proving Galois arithmetic facts *) - Ltac galois := intros; apply gf_eq; simpl; - repeat match goal with - | [ x : GF |- _ ] => destruct x - end; simpl in *; autorewrite with core; - intuition; demod; try solve [ f_equal; intuition ]. - - (* Automatically unfold the definition of Z *) - Lemma modmatch_eta : forall n, - match n with - | 0 => 0 - | Z.pos y' => Z.pos y' - | Z.neg y' => Z.neg y' - end = n. - Proof. - destruct n; auto. - Qed. - - Hint Rewrite Zmod_mod modmatch_eta. - - (* Substitution to prove all Compats *) - Ltac compat := repeat intro; subst; trivial. - - (***** Ring Theory *****) - - Instance GFplus_compat : Proper (eq==>eq==>eq) GFplus. - Proof. - compat. - Qed. - - Instance GFminus_compat : Proper (eq==>eq==>eq) GFminus. - Proof. - compat. - Qed. - - Instance GFmult_compat : Proper (eq==>eq==>eq) GFmult. - Proof. - compat. - Qed. - - Instance GFopp_compat : Proper (eq==>eq) GFopp. - Proof. - compat. - Qed. - - Definition GFring_theory : ring_theory GFzero GFone GFplus GFmult GFminus GFopp eq. - Proof. - constructor; galois. - Qed. - - (***** Power theory *****) - - Local Open Scope GF_scope. - - (* Separate two of the same base *) - Lemma GFexp'_doubling : forall q r0, GFexp' (r0 * r0) q = GFexp' r0 q * GFexp' r0 q. - Proof. - induction q; simpl; intuition. - rewrite (IHq (r0 * r0)); generalize (GFexp' (r0 * r0) q); intro. - galois. - apply Zmod_eq; ring. - Qed. - - (* Equivalence with pow_pos for subroutine of GFexp *) - Lemma GFexp'_correct : forall r p, GFexp' r p = pow_pos GFmult r p. - Proof. - induction p; simpl; intuition; - rewrite GFexp'_doubling; congruence. - Qed. - - Hint Immediate GFexp'_correct. - - (* Equivalence with pow_pos for GFexp *) - Lemma GFexp_correct : forall r n, - r^n = pow_N 1 GFmult r n. - Proof. - induction n; simpl; intuition. - Qed. - - (* Equivalence with pow_pos for GFexp with identity (a utility lemma) *) - Lemma GFexp_correct' : forall r n, - r^id n = pow_N 1 GFmult r n. - Proof. - apply GFexp_correct. - Qed. - - Hint Immediate GFexp_correct'. - - Lemma GFpower_theory : power_theory GFone GFmult eq id GFexp. - Proof. - constructor; auto. - Qed. - - (***** Additional tricks for Ring *****) - - Ltac GFexp_tac t := Ncst t. - - (* Decideability *) - Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. - Proof. - intros; galois. - apply Zeq_is_eq_bool. - trivial. - Qed. - - (* Completeness *) - Lemma GFcomplete : forall (x y: GF), x = y -> Zeq_bool x y = true. - Proof. - intros. - apply Zeq_is_eq_bool. - galois. - Qed. - - (***** Division Theory *****) - - (* Compatibility between inject and addition *) - Lemma inject_distr_add : forall (m n : Z), - inject (m + n) = inject m + inject n. - Proof. - galois. - Qed. - - (* Compatibility between inject and subtraction *) - Lemma inject_distr_sub : forall (m n : Z), - inject (m - n) = inject m - inject n. - Proof. - galois. - Qed. - - (* Compatibility between inject and multiplication *) - Lemma inject_distr_mul : forall (m n : Z), - inject (m * n) = inject m * inject n. - Proof. - galois. - Qed. - - (* Compatibility between inject and GFtoZ *) - Lemma inject_eq : forall (x : GF), inject x = x. - Proof. - galois. - Qed. - - (* Compatibility between inject and mod *) - Lemma inject_mod_eq : forall x, inject x = inject (x mod modulus). - Proof. - galois. - Qed. - - (* The main division theory: - * equivalence between division and quotrem (euclidean division) - *) - - Definition GFquotrem(a b: GF): GF * GF := - match (Z.quotrem a b) with - | (q, r) => (inject q, inject r) - end. - - Lemma GFdiv_theory : div_theory eq GFplus GFmult (@id _) GFquotrem. - Proof. - constructor; intros; unfold GFquotrem. - - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - eq_remove_proofs; demod; - rewrite <- (Z.quot_rem' a b); - destruct a; simpl; trivial. - Qed. - - (***** Field Theory *****) - - (* First, add the modifiers to our ring *) - Add Ring GFring0 : GFring_theory - (power_tac GFpower_theory [GFexp_tac]). - - (* Utility lemmas for multiplicative inverses *) - Lemma GFexp'_pred' : forall x p, - GFexp' p (Pos.succ x) = GFexp' p x * p. - Proof. - induction x; simpl; intuition; try ring. - rewrite IHx; ring. - Qed. - - Lemma GFexp'_pred : forall x p, - x <> 1%positive - -> GFexp' p x = GFexp' p (Pos.pred x) * p. - Proof. - intros; rewrite <- (Pos.succ_pred x) at 1; auto using GFexp'_pred'. - Qed. - - Lemma GFexp_pred : forall x p, - x <> 0%N - -> p^x = p^N.pred x * p. - Proof. - destruct x; simpl; intuition. - destruct (Pos.eq_dec p 1); subst; simpl; try ring. - rewrite GFexp'_pred by auto. - destruct p; intuition. - Qed. - - (* Show that GFinv actually defines multiplicative inverses *) - Lemma GF_multiplicative_inverse : forall p, - p <> 0 - -> GFinv p * p = 1. - Proof. - unfold GFinv; destruct totient as [ ? [ ] ]; simpl. - intros. - rewrite <- GFexp_pred; auto using N.gt_lt, N.lt_neq. - intro; subst. - eapply N.lt_irrefl; eauto using N.gt_lt. - Qed. - - (* Compatibility of inverses and equality *) - Instance GFinv_compat : Proper (eq==>eq) GFinv. - Proof. - compat. - Qed. - - (* Compatibility of division and equality *) - Instance GFdiv_compat : Proper (eq==>eq==>eq) GFdiv. - Proof. - compat. - Qed. - - Hint Immediate GF_multiplicative_inverse GFring_theory. - - Local Hint Extern 1 False => discriminate. - - (* Add an abstract field (without modifiers) *) - Definition GFfield_theory : field_theory GFzero GFone GFplus GFmult GFminus GFopp GFdiv GFinv eq. - Proof. - constructor; auto. - Qed. - - Ltac modulus_bound := - pose proof (prime_ge_2 (primeToZ modulus) (proj2_sig modulus)); omega. - - Lemma GFToZ_inject : forall x, GFToZ (inject x) = (x mod primeToZ modulus)%Z. - Proof. - intros; unfold GFToZ, proj1_sig, inject; reflexivity. - Qed. - - Lemma GFexp_Zpow : forall (a : GF) - (k : Z) (k_nonneg : (0 <= k)%Z), - a ^ (Z.to_N k) = ((GFToZ a) ^ k)%Z. - Proof. - intro a. - apply natlike_ind; [ galois; symmetry; apply Z.mod_small; modulus_bound | ]. - intros k k_nonneg IHk. - rewrite Z2N.inj_succ by auto. - rewrite GFexp_pred by (auto; apply N.neq_succ_0). - rewrite N.pred_succ. - rewrite IHk. - rewrite Z.pow_succ_r by auto. - galois. - Qed. - - Lemma GF_Zmod : forall x, ((GFToZ x) mod primeToZ modulus = GFToZ x)%Z. - Proof. - intros. - pose proof (inject_eq x) as inject_eq_x. - apply gf_eq in inject_eq_x. - rewrite <- inject_eq_x. - rewrite inject_mod_eq. - rewrite GFToZ_inject. - apply Z.mod_mod. - modulus_bound. - Qed. - - Lemma square_Zmod_GF : forall (a : GF) (a_nonzero : a <> 0), - (exists b : Z, ((b * b) mod modulus)%Z = (a mod modulus)%Z) <-> (exists b, b * b = a). - Proof. - split; intros A; destruct A as [b b_id]. { - exists (inject b). - galois. - } { - exists (GFToZ b). - rewrite GF_Zmod. - rewrite <- b_id. - rewrite <- (inject_eq b) at 3 4. - rewrite <- inject_distr_mul. - rewrite GFToZ_inject. - auto. - } - Qed. - - Lemma inject_Zmod : forall x y, inject x = inject y <-> (x mod primeToZ modulus = y mod primeToZ modulus)%Z. - Proof. - split; intros A. - + apply gf_eq in A. - do 2 rewrite GFToZ_inject in A; auto. - + rewrite (inject_mod_eq x). - rewrite (inject_mod_eq y). - rewrite A; auto. - Qed. - - Lemma GFexp_0 : forall e : N, (0 < e)%N -> 0 ^ e = 0. - Proof. - intros. - replace e with (Z.to_N (Z.of_N e)) by apply N2Z.id. - replace e with (N.succ (N.pred e)) by (apply N.succ_pred_pos; auto). - rewrite N2Z.inj_succ. - apply natlike_ind with (x := Z.of_N (N.pred e)); try reflexivity. - + intros x x_pos IHx. - rewrite Z2N.inj_succ by omega. - rewrite GFexp_pred by apply N.neq_succ_0. - rewrite N.pred_succ. - rewrite IHx; ring. - + replace 0%Z with (Z.of_N 0%N) by auto. - rewrite <- N2Z.inj_le. - apply N.lt_le_pred; auto. - Qed. - - Lemma nonzero_Zmod_GF : forall a, - (inject a <> 0) <-> (a mod primeToZ modulus <> 0)%Z. - Proof. - split; intros A B; unfold not in A. { - rewrite inject_mod_eq in A. - rewrite B in A. - apply A. - apply gf_eq. - rewrite GFToZ_inject. - rewrite Z.mod_0_l by modulus_bound. - auto. - } { - apply A. - apply gf_eq in B. - rewrite GFToZ_inject in B. - auto. - } - Qed. - - Lemma nonzero_range : forall (a : GF), (a <> 0) -> (1 <= a <= primeToZ modulus - 1)%Z. - Proof. - intros a a_nonzero. - assert (a mod primeToZ modulus <> 0)%Z by (apply nonzero_Zmod_GF; rewrite inject_eq; auto). - replace (GFToZ a) with (a mod primeToZ modulus)%Z by (symmetry; apply (proj2_sig a)). - assert (0 < primeToZ modulus)%Z as modulus_pos by - (pose proof (prime_ge_2 (primeToZ modulus) (proj2_sig modulus)); omega). - pose proof (Z.mod_pos_bound a (primeToZ modulus) modulus_pos). - omega. - Qed. - - Lemma GF_mod_bound : forall (x : GF), (0 <= x < modulus)%Z. - Proof. - intros. - assert (0 < modulus)%Z as gt_0_modulus by modulus_bound. - pose proof (Z.mod_pos_bound x modulus gt_0_modulus). - rewrite <- (inject_eq x). - unfold GFToZ, inject in *. - auto. - Qed. - - Lemma GF_minus_plus : forall x y z, x + y = z <-> x = z - y. - Proof. - split; intros A; [ symmetry in A | ]; rewrite A; ring. - Qed. - - -End GaloisTheory.
\ No newline at end of file diff --git a/src/Galois/GaloisTutorial.v b/src/Galois/GaloisTutorial.v deleted file mode 100644 index 5ef0e4cf5..000000000 --- a/src/Galois/GaloisTutorial.v +++ /dev/null @@ -1,106 +0,0 @@ - -Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.GaloisField. - -(* First, we define our prime in Z*) -Definition two_5_1 := (two_p 5) - 1. -Definition two_127_1 := (two_p 127) - 1. - -(* Then proofs of their primality *) -Lemma two_5_1_prime : prime two_5_1. -Admitted. - -Lemma two_127_1_prime : prime two_127_1. -Admitted. - -(* And use those to make modulus modules *) -Module Modulus31 <: Modulus. - Definition modulus := exist _ two_5_1 two_5_1_prime. -End Modulus31. - -Module Modulus127_1 <: Modulus. - Definition modulus := exist _ two_127_1 two_127_1_prime. -End Modulus127_1. - -Module Example31. - (* Then we can construct a field with that modulus *) - Module Field := GaloisField Modulus31. - Import Field. - - (* And pull in the appropriate notations *) - Local Open Scope GF_scope. - - (* First, let's solve a ring example*) - Lemma ring_example: forall x: GF, x * 2 = x + x. - Proof. - intros. - ring. - Qed. - - (* Then a field example (we have to know we can't divide by zero!) *) - Lemma field_example: forall x y z: GF, z <> 0 -> - x * (y / z) / z = x * y / (z ^ 2). - Proof. - intros; simpl. - field; trivial. - Qed. - - (* Then an example with exponentiation *) - Lemma exp_example: forall x: GF, x ^ 2 + 2 * x + 1 = (x + 1) ^ 2. - Proof. - intros; simpl. - field; trivial. - Qed. - - (* In general, the rule I've been using is: - - - If our goal looks like x = y: - - + If we need to use assumptions to prove the goal, then before - we apply field, - - * Perform all relevant substitutions (especially subst) - - * If we have something more complex, we're probably going - to have to performe some sequence of "replace X with Y" - and solve out the subgoals manually before we can use - field. - - + Else, just use field directly - - - If we just want to simplify terms and put them into a canonical - form, then field_simplify or ring_simplify should do the trick. - Note, however, that the canonical form has lots of annoying "/1"s - - - Otherwise, do a "replace X with Y" to generate an equality - so that we can use field in the above case - - *) - -End Example31. - -(* Notice that the field tactics work whether we know what the modulus is *) -Module TimesZeroTransparentTestModule. - Module Theory := GaloisField Modulus127_1. - Import Theory. - Local Open Scope GF_scope. - - Lemma timesZero : forall a, a*0 = 0. - intros. - field. - Qed. -End TimesZeroTransparentTestModule. - -(* Or if we don't (i.e. it's opaque) *) -Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := GaloisField M. - Import Theory. - Local Open Scope GF_scope. - - Lemma timesZero : forall a, a*0 = 0. - intros. - field. - Qed. -End TimesZeroParametricTestModule. - diff --git a/src/Galois/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 86585b894..8c22a8091 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -2,7 +2,7 @@ Require Import Zpower ZArith. Require Import List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Galois.BaseSystem. +Require Import Crypto.BaseSystem. Require Import VerdiTactics. Local Open Scope Z_scope. diff --git a/src/Rep/ECRep.v b/src/Rep/ECRep.v deleted file mode 100644 index 60481fe72..000000000 --- a/src/Rep/ECRep.v +++ /dev/null @@ -1,16 +0,0 @@ - -Require Export Crypto.Galois.GaloisField. - -Module ECRep (M: Modulus). - Module F := GaloisField M. - Import F. - Local Open Scope GF_scope. - - (* Definition ECSig : ADTSig := - ADTsignature { - Constructor "FromTwistedXY" - : GF x GF -> rep, - Method "Add" - : rep x rep -> rep, - }.*) -End ECRep. diff --git a/src/Rep/GaloisRep.v b/src/Rep/GaloisRep.v deleted file mode 100644 index bfd09acfd..000000000 --- a/src/Rep/GaloisRep.v +++ /dev/null @@ -1,26 +0,0 @@ - -Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.GaloisField. - -Module GaloisRep (M: Modulus). - Module G := Galois M. - Module F := GaloisField M. - Import M G F. - Local Open Scope GF_scope. - - (* Definition GFSig : ADTSig := - ADTsignature { - Constructor "FromGF" - : GF -> rep, - Method "ToGF" - : rep -> GF, - Method "Add" - : rep x rep -> rep, - Method "Mult" - : rep x rep -> rep, - Method "Sub" - : rep x rep -> rep, - Method "Div" - : rep x rep -> rep - }. *) -End GaloisRep. diff --git a/src/Spec/EdDSA25519.v b/src/Spec/Ed25519.v index c4547860a..c4547860a 100644 --- a/src/Spec/EdDSA25519.v +++ b/src/Spec/Ed25519.v diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v deleted file mode 100644 index 242661bc5..000000000 --- a/src/Specific/EdDSA25519.v +++ /dev/null @@ -1,636 +0,0 @@ -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import NPeano NArith. -Require Import Crypto.Galois.EdDSA Crypto.Galois.GaloisField. -Require Import Crypto.Curves.PointFormats. -Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. -Require Import Bedrock.Word. -Require Import VerdiTactics. -Require Import Decidable. -Require Import Omega. - -Module Modulus25519 <: Modulus. - Definition two_255_19 := two_p 255 - 19. - Lemma two_255_19_prime : prime two_255_19. Admitted. - Definition prime25519 := exist _ two_255_19 two_255_19_prime. - Definition modulus := prime25519. -End Modulus25519. - -Lemma prime_l : prime (252 + 27742317777372353535851937790883648493). Admitted. - -Local Open Scope nat_scope. - -Module EdDSA25519_Params <: EdDSAParams. - Definition q : Prime := Modulus25519.modulus. - Ltac prime_bound := pose proof (prime_ge_2 q (proj2_sig q)); try omega. - - Lemma q_odd : (primeToZ q > 2)%Z. - Proof. - cbv; congruence. - Qed. - - Module Modulus_q := Modulus25519. - - Definition b := 256. - Lemma b_valid : (2 ^ (Z.of_nat b - 1) > q)%Z. - Proof. - remember 19%Z as y. - replace (Z.of_nat b - 1)%Z with 255%Z by auto. - assert (y > 0)%Z by (rewrite Heqy; cbv; auto). - remember (2 ^ 255)%Z as x. - simpl. unfold Modulus25519.two_255_19. - rewrite two_p_equiv. - rewrite <- Heqy. - rewrite <- Heqx. - omega. - Qed. - - (* TODO *) - Parameter H : forall {n}, word n -> word (b + b). - - Definition c := 3. - Lemma c_valid : c = 2 \/ c = 3. - Proof. - right; auto. - Qed. - - Definition n := b - 2. - Lemma n_ge_c : n >= c. - Proof. - unfold n, c, b; omega. - Qed. - Lemma n_le_b : n <= b. - Proof. - unfold n, b; omega. - Qed. - - Module GFDefs := GaloisField Modulus_q. - Import GFDefs. - Local Open Scope GF_scope. - - Lemma gt_div2_q_zero : (q / 2 > 0)%Z. - Proof. - replace (GFToZ 0) with 0%Z by auto. - assert (0 < 2 <= primeToZ q)%Z by (pose proof q_odd; omega). - pose proof (Z.div_str_pos (primeToZ q) 2 H0). - omega. - Qed. - - Definition isSquare x := exists sqrt_x, sqrt_x ^ 2 = x. - - Lemma euler_criterion_GF : forall (a : GF) (a_nonzero : a <> 0), - (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a. - Proof. - assert (prime q) by apply Modulus25519.two_255_19_prime. - assert (primeToZ q <> 2)%Z by (pose proof q_odd; omega). - assert (primeToZ q <> 0)%Z by (pose proof q_odd; omega). - split; intros A. { - apply square_Zmod_GF; auto. - eapply euler_criterion. - + auto. - + pose proof q_odd; unfold q in *; omega. - + apply div2_p_1mod4; auto. - + rewrite GF_Zmod. - apply nonzero_range; auto. - + rewrite GFexp_Zpow in A by (auto || apply Z_div_pos; prime_bound). - rewrite inject_mod_eq in A. - apply gf_eq in A. - replace (GFToZ 1) with 1%Z in A by auto. - rewrite GFToZ_inject in A. - rewrite Z.mod_mod in A by auto. - rewrite GF_Zmod. - exact A. - } { - rewrite GFexp_Zpow by first [apply Z.div_pos; pose proof q_odd; omega | auto]. - apply gf_eq. - replace (GFToZ 1) with 1%Z by auto. - rewrite GFToZ_inject. - apply euler_criterion; auto. - + apply nonzero_range; auto. - + rewrite <- GF_Zmod. - apply square_Zmod_GF; auto. - } - Qed. - - Lemma euler_criterion_if : forall (a : GF), - if (orb (Zeq_bool (a ^ (Z.to_N (q / 2)))%GF 1) (Zeq_bool a 0)) - then (isSquare a) else (forall b, b * b <> a). - Proof. - intros. - unfold orb. do 2 break_if; try congruence. { - assert (a <> 0). { - intro eq_a_0. - replace 1%Z with (GFToZ 1) in Heqb1 by auto. - apply GFdecidable in Heqb1; auto. - rewrite eq_a_0 in Heqb1. - rewrite GFexp_0 in Heqb1; auto. - replace 0%N with (Z.to_N 0%Z) by auto. - rewrite <- (Z2N.inj_lt 0 (q / 2)); (omega || pose proof gt_div2_q_zero; omega). - } - apply euler_criterion_GF; auto. - apply GFdecidable; auto. - } { - exists 0. - replace (0 * 0)%GF with 0%GF by field. - replace 0%Z with (GFToZ 0) in Heqb0 by auto. - apply GFdecidable in Heqb0; auto. - subst; field. - } { - intros b b_id. - assert (a <> 0). { - intro eq_a_0. - replace 0%Z with (GFToZ 0) in Heqb0 by auto. - apply GFcomplete in eq_a_0. - congruence. - } - assert (Zeq_bool (GFToZ (a ^ Z.to_N (q / 2))) 1 = true); try congruence. { - replace 1%Z with (GFToZ 1) by auto; apply GFcomplete. - apply euler_criterion_GF; unfold isSquare; eauto. - } - } - Qed. - - Definition a := GFopp 1%GF. - Lemma a_nonzero : a <> 0%GF. - Proof. - unfold a, GFopp; simpl. - intuition. - assert (proj1_sig 0%GF = proj1_sig (0 - 1)%GF) by (rewrite H0; reflexivity). - assert (proj1_sig 0%GF = 0%Z) by auto. - assert (proj1_sig (0 - 1)%GF <> 0%Z). { - simpl; intuition. - apply Z.rem_mod_eq_0 in H3; [|unfold two_255_19; cbv; omega]. - unfold Z.rem in H3; simpl in H3. - congruence. - } - omega. - Qed. - - Lemma q_1mod4 : (q mod 4 = 1)%Z. - Proof. - simpl. - unfold Modulus25519.two_255_19. - rewrite Zminus_mod. - simpl. - auto. - Qed. - - Lemma a_square : exists sqrt_a, (sqrt_a^2 = a)%GF. - Proof. - intros. - pose proof (minus1_square_1mod4 q (proj2_sig q) q_1mod4). - destruct H0. - apply square_Zmod_GF; try apply a_nonzero. - exists (inject x). - rewrite GFToZ_inject. - rewrite <- Zmult_mod. - rewrite GF_Zmod. - unfold a. - replace (GFopp 1) with (inject (q - 1)) by galois. - auto. - Qed. - - (* TODO *) - (* d = ((-121665)%Z / 121666%Z)%GF.*) - Definition d : GF := 37095705934669439343138083508754565189542113879843219016388785533085940283555%Z. - Axiom d_nonsquare : forall x, x^2 <> d. - (* Definition d_nonsquare : (forall x, x^2 <> d) := euler_criterion_if d. <-- currently not computable in reasonable time *) - - Module CurveParameters <: TwistedEdwardsParams Modulus_q. - Module GFDefs := GFDefs. - Definition modulus_odd : (primeToZ Modulus_q.modulus > 2)%Z := q_odd. - Definition a : GF := a. - Definition a_nonzero := a_nonzero. - Definition a_square := a_square. - Definition d := d. - Definition d_nonsquare := d_nonsquare. - End CurveParameters. - Module Facts := CompleteTwistedEdwardsFacts Modulus_q CurveParameters. - Module Import Curve := Facts.Curve. - - (* TODO: B = decodePoint (y=4/5, x="positive") *) - Parameter B : point. - Axiom B_not_identity : B <> zero. - - Definition l : Prime := exist _ (252 + 27742317777372353535851937790883648493)%Z prime_l. - Lemma l_odd : (Z.to_nat l > 2)%nat. - Proof. - unfold l, primeToZ, proj1_sig. - rewrite Z2Nat.inj_add; try omega. - apply lt_plus_trans. - compute; omega. - Qed. - Axiom l_order_B : (scalarMult (Z.to_nat l) B) = zero. - - (* H' is the identity function. *) - Definition H'_out_len (n : nat) := n. - Definition H' {n} (w : word n) := w. - - Lemma l_bound : Z.to_nat l < pow2 b. - Proof. - rewrite Zpow_pow2. - rewrite <- Z2Nat.inj_lt by first [unfold l, primeToZ, proj1_sig; omega | compute; congruence]. - reflexivity. - Qed. - - Definition Fq_enc (x : GF) : word (b - 1) := natToWord (b - 1) (Z.to_nat x). - Definition Fq_dec (x_ : word (b - 1)) : option GF := - Some (inject (Z.of_nat (wordToNat x_))). - Lemma Fq_encoding_valid : forall x : GF, Fq_dec (Fq_enc x) = Some x. - Proof. - unfold Fq_dec, Fq_enc; intros. - f_equal. - rewrite wordToNat_natToWord_idempotent. { - rewrite Z2Nat.id by apply GF_mod_bound. - apply inject_eq. - } { - rewrite <- Nnat.N2Nat.id. - rewrite Npow2_nat. - apply (Nat2N_inj_lt (Z.to_nat x) (pow2 (b - 1))). - replace (pow2 (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat b - 1))%Z) by (rewrite Zpow_pow2; auto). - pose proof (GF_mod_bound x). - pose proof b_valid. - pose proof q_odd. - replace modulus with q in * by reflexivity. - apply Z2Nat.inj_lt; try omega. - } - Qed. - Definition FqEncoding : encoding of GF as word (b-1) := - Build_Encoding GF (word (b-1)) Fq_enc Fq_dec Fq_encoding_valid. - - Definition Fl_enc (x : {s : nat | s mod (Z.to_nat l) = s}) : word b := - natToWord b (proj1_sig x). - Definition Fl_dec (x_ : word b) : option {s:nat | s mod (Z.to_nat l) = s} := - match (lt_dec (wordToNat x_) (Z.to_nat l)) with - | left A => Some (exist _ _ (Nat.mod_small _ (Z.to_nat l) A)) - | _ => None - end. - Lemma Fl_encoding_valid : forall x, Fl_dec (Fl_enc x) = Some x. - Proof. - Opaque l. - unfold Fl_enc, Fl_dec; intros. - assert (proj1_sig x < (Z.to_nat l)). { - destruct x; simpl. - apply Nat.mod_small_iff in e; auto. - pose proof l_odd; omega. - } - rewrite wordToNat_natToWord_idempotent by - (pose proof l_bound; apply Nomega.Nlt_in; rewrite Nnat.Nat2N.id; rewrite Npow2_nat; omega). - case_eq (lt_dec (proj1_sig x) (Z.to_nat l)); intros; try omega. - destruct x. - do 2 (simpl in *; f_equal). - apply Eqdep_dec.UIP_dec. - apply eq_nat_dec. - Transparent l. - Qed. - - Definition FlEncoding := - Build_Encoding {s:nat | s mod (Z.to_nat l) = s} (word b) Fl_enc Fl_dec Fl_encoding_valid. - - Lemma q_5mod8 : (q mod 8 = 5)%Z. - Proof. - simpl. - unfold two_255_19. - rewrite Zminus_mod. - auto. - Qed. - - (* TODO : move to ZUtil *) - Lemma mod2_one_or_zero : forall x, (x mod 2 = 1)%Z \/ (x mod 2 = 0)%Z. - Proof. - intros. - pose proof (Zmod_even x) as mod_even. - case_eq (Z.even x); intro x_even; rewrite x_even in mod_even; auto. - Qed. - - (* TODO: move to GaloisField *) - Lemma GFexp_add : forall x k j, x ^ j * x ^ k = x ^ (j + k). - Proof. - intros. - apply N.peano_ind with (n := j); simpl; try field. - intros j' IHj. - rewrite N.add_succ_l. - rewrite GFexp_pred by apply N.neq_succ_0. - assert (N.succ (j' + k) <> 0)%N as neq_exp_0 by apply N.neq_succ_0. - rewrite (GFexp_pred _ neq_exp_0). - do 2 rewrite N.pred_succ. - rewrite <- IHj. - field. - Qed. - - Lemma GFexp_compose : forall k x j, (x ^ j) ^ k = x ^ (k * j). - Proof. - intros k. - apply N.peano_ind with (n := k); auto. - intros k' IHk x j. - rewrite Nmult_Sn_m. - rewrite <- GFexp_add. - rewrite <- IHk. - rewrite GFexp_pred by apply N.neq_succ_0. - rewrite N.pred_succ. - field. - Qed. - - Lemma sqrt_one : forall x, x ^ 2 = 1 -> x = 1 \/ x = GFopp 1. - Proof. - intros x x_squared. - apply sqrt_solutions. - rewrite x_squared; field. - Qed. - - Definition sqrt_minus1 := inject 2 ^ Z.to_N (q / 4). - (* straightforward computation once GF computations get fast *) - Axiom sqrt_minus1_valid : sqrt_minus1 ^ 2 = GFopp 1. - - (* square root mod q relies on the fact that q is 5 mod 8 *) - Definition sqrt_mod_q (a : GF) := - let b := a ^ Z.to_N (q / 8 + 1) in - (match (GF_eq_dec (b ^ 2) a) with - | left A => b - | right A => sqrt_minus1 * b - end). - - Lemma eq_b4_a2 : forall x, isSquare x -> - ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2. - Proof. - intros. - destruct (GF_eq_dec x 0). { - admit. - } { - rewrite GFexp_compose. - replace (2 * 2)%N with 4%N by auto. - rewrite GFexp_compose. - replace (4 * Z.to_N (q / 8 + 1))%N with (Z.to_N (q / 2 + 2))%N by (cbv; auto). - pose proof gt_div2_q_zero. - rewrite Z2N.inj_add by omega. - rewrite <- GFexp_add by omega. - replace (x ^ Z.to_N (q / 2)) with 1 - by (symmetry; apply euler_criterion_GF; auto). - replace (Z.to_N 2) with 2%N by auto. - field. - } - Qed. - - Lemma sqrt_mod_q_valid : forall x, isSquare x -> - (sqrt_mod_q x) ^ 2 = x. - Proof. - intros x x_square. - destruct (sqrt_solutions x _ (eq_b4_a2 x x_square)) as [? | eq_b2_oppx]; - unfold sqrt_mod_q; break_if; intuition. - rewrite <- GFexp_distr_mul by apply N.le_0_2. - rewrite sqrt_minus1_valid. - rewrite eq_b2_oppx. - field. - Qed. - - Definition solve_for_x (y : GF) := sqrt_mod_q ( (y ^ 2 - 1) / (d * (y ^ 2) - a)). - - Lemma d_y2_a_nonzero : forall y, d * y ^ 2 - a <> 0. - intros ? eq_zero. - symmetry in eq_zero. - apply GF_minus_plus in eq_zero. - replace (0 + a) with a in eq_zero by field. - destruct a_square as [sqrt_a a_square]. - rewrite <- a_square in eq_zero. - destruct (GF_eq_dec y 0). { - subst. - rewrite a_square in eq_zero. - replace (d * 0 ^ 2) with 0 in eq_zero by field. - pose proof a_nonzero; auto. - } { - apply GF_square_mul in eq_zero; auto. - destruct eq_zero as [sqrt_d d_square]. - pose proof (d_nonsquare sqrt_d). - auto. - } - Qed. - - Lemma a_d_y2_nonzero : forall y, a - d * y ^ 2 <> 0. - Proof. - intros y eq_zero. - symmetry in eq_zero. - apply GF_minus_plus in eq_zero. - replace (0 + d * y ^ 2) with (d * y ^ 2) in eq_zero by field. - replace a with (0 + a) in eq_zero by field. - symmetry in eq_zero. - apply GF_minus_plus in eq_zero. - pose proof (d_y2_a_nonzero y). - auto. - Qed. - - Lemma onCurve_solve_x2 : forall x y, onCurve (x, y) -> - x ^ 2 = (y ^ 2 - 1) / (d * (y ^ 2) - a). - Proof. - intros ? ? onCurve_x_y. - unfold onCurve, CurveParameters.d, CurveParameters.a in onCurve_x_y. - apply GF_minus_plus in onCurve_x_y. - symmetry in onCurve_x_y. - replace (1 + d * x ^ 2 * y ^ 2 - y ^ 2) with (1 - y ^ 2 + d * x ^ 2 * y ^ 2) - in onCurve_x_y by ring. - apply GF_minus_plus in onCurve_x_y. - replace (a * x ^ 2 - d * x ^ 2 * y ^ 2) with (x ^ 2 * (a - d * y ^ 2)) in onCurve_x_y by ring. - replace ((y ^ 2 - 1) / (d * y ^ 2 - a)) with ((1 - y ^ 2) / (a - d * y ^ 2)) - by (field; [ apply d_y2_a_nonzero | apply a_d_y2_nonzero ]). - rewrite onCurve_x_y. - unfold GFdiv. - field. - apply a_d_y2_nonzero. - Qed. - - Lemma solve_for_x_onCurve (x y : GF): onCurve (x, y) -> - onCurve (solve_for_x y, y). - Proof. - intros. - unfold onCurve, solve_for_x, CurveParameters.d, CurveParameters.a. - rewrite sqrt_mod_q_valid by (erewrite <- onCurve_solve_x2; unfold isSquare; eauto). - field; apply d_y2_a_nonzero. - Qed. - - Lemma solve_for_x_onCurve_GFopp (x y : GF) : onCurve (x, y) -> - onCurve (GFopp (solve_for_x y), y). - Proof. - pose proof (solve_for_x_onCurve x y) as x_onCurve. - unfold onCurve, CurveParameters.d, CurveParameters.a in *. - replace ((solve_for_x y) ^ 2) with ((GFopp (solve_for_x y)) ^ 2) in x_onCurve by field. - auto. - Qed. - - (* - * Admitting these looser version of solve_for_x_onCurve and - * solve_for_x_onCurve_GFopp for now; need to figure out how - * to deal with the onCurve precondition when inside point_dec. - *) - Lemma solve_for_x_onCurve_loose : forall y, onCurve (solve_for_x y, y). - Admitted. - - Lemma solve_for_x_onCurve_GFopp_loose : - forall y, onCurve (GFopp (solve_for_x y), y). - Admitted. - - Lemma point_onCurve : forall p, onCurve (projX p, projY p). - Proof. - intro. - replace (projX p, projY p) with (proj1_sig p) - by (unfold projX, projY; apply surjective_pairing). - apply (proj2_sig p). - Qed. - - Lemma GFopp_x_point : forall p p', projY p = projY p' -> - projX p = projX p' \/ projX p = GFopp (projX p'). - Proof. - intros ? ? projY_eq. - pose proof (point_onCurve p) as onCurve_p. - pose proof (point_onCurve p') as onCurve_p'. - apply sqrt_solutions. - rewrite projY_eq in *. - unfold solve_for_x, onCurve, CurveParameters.a, CurveParameters.d in *. - apply onCurve_solve_x2 in onCurve_p. - apply onCurve_solve_x2 in onCurve_p'. - rewrite <- onCurve_p in onCurve_p'; auto. - Qed. - - Lemma GFopp_solve_for_x : forall p, - solve_for_x (projY p) = projX p \/ solve_for_x (projY p) = GFopp (projX p). - Proof. - intros. - pose proof (point_onCurve p). - remember (mkPoint (solve_for_x (projY p), projY p) (solve_for_x_onCurve (projX p) (projY p) (point_onCurve p))) as q1. - replace (solve_for_x (projY p)) with (projX q1) by (rewrite Heqq1; auto). - apply GFopp_x_point. - rewrite Heqq1; auto. - Qed. - - Definition sign_bit (x : GF) := (wordToN (Fq_enc (GFopp x)) <? wordToN (Fq_enc x))%N. - Definition point_enc (p : point) : word b := WS (sign_bit (projX p)) (Fq_enc (projY p)). - Definition point_dec (w : word (S (b - 1))) : option point := - match (Fq_dec (wtl w)) with - | None => None - | Some y => match (Bool.eqb (whd w) (sign_bit (solve_for_x y))) with - | true => value (mkPoint (solve_for_x y, y) (solve_for_x_onCurve_loose y )) - | false => value (mkPoint (GFopp (solve_for_x y), y) (solve_for_x_onCurve_GFopp_loose y)) - end - end. - - - Definition value_or_default {T} (opt : option T) d := match opt with - | Some x => x - | None => d - end. - - Lemma value_or_default_inj : forall {T} (x y d : T), - value_or_default (Some x) d = value_or_default (Some y) d -> x = y. - Proof. - unfold value_or_default; auto. - Qed. - - Lemma Fq_enc_inj : forall x y, Fq_enc x = Fq_enc y -> x = y. - Proof. - intros ? ? enc_eq. - pose proof (Fq_encoding_valid x) as enc_valid_x. - rewrite enc_eq in enc_valid_x. - pose proof (Fq_encoding_valid y) as enc_valid_y. - rewrite enc_valid_x in enc_valid_y. - apply value_or_default_inj with (d := 0). - rewrite enc_valid_y; auto. - Qed. - - Lemma sign_bit_GFopp_negb : forall x, sign_bit x = negb (sign_bit (GFopp x)) \/ x = GFopp x. - Proof. - intros. - destruct (GF_eq_dec x (GFopp x)); auto. - left. - unfold sign_bit. - rewrite GFopp_involutive. - rewrite N.ltb_antisym. - case_eq (wordToN (Fq_enc x) <=? wordToN (Fq_enc (GFopp x)))%N; intro A. - + apply N.leb_le in A. - apply N.lt_eq_cases in A. - destruct A as [A | A]. - - apply N.ltb_lt in A. - rewrite A; auto. - - apply wordToN_inj in A. - apply Fq_enc_inj in A. - congruence. - + apply N.leb_gt in A. - rewrite N.ltb_antisym. - apply N.lt_le_incl in A. - apply N.leb_le in A. - rewrite A. - auto. - Qed. - - Lemma point_mkPoint : forall p, p = mkPoint (proj1_sig p) (proj2_sig p). - Proof. - intros; destruct p; auto. - Qed. - - Lemma onCurve_proof_eq : forall x y (P : onCurve x) (Q : onCurve y) (xyeq: x = y), - match xyeq in (_ = y') return onCurve y' with - | eq_refl => P - end = Q. - Proof. - intros; subst. - intros; unfold onCurve in *. - break_let. - apply Eqdep_dec.UIP_dec. - exact GF_eq_dec. - Qed. - - Lemma two_arg_eq : forall {A B} C (f : forall a: A, B a -> C) x1 y1 x2 y2 (xeq: x1 = x2), - match xeq in (_ = x) return (B x) with - | eq_refl => y1 - end = y2 -> f x1 y1 = f x2 y2. - Proof. - intros; subst; reflexivity. - Qed. - - Lemma point_destruct : forall p P, mkPoint (projX p, projY p) P = p. - Proof. - intros; rewrite point_mkPoint. - assert ((projX p, projY p) = proj1_sig p) by - (unfold projX, projY; simpl; symmetry; apply surjective_pairing). - apply two_arg_eq with (xeq := H0). - apply onCurve_proof_eq. - Qed. - - (* There are currently two copies of mkPoint in scope. I would like to use Facts.point_eq - here, but it is proven for Facts.Curve.mkPoint, not mkPoint. These are equivalent, but - I have so far not managed to unify them. *) - Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 -> - forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. - apply Facts.point_eq. - Qed. - - Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. - Proof. - intros. - unfold point_dec, point_enc, wtl, whd. - rewrite Fq_encoding_valid. - break_if; unfold value; f_equal. { - remember (mkPoint (solve_for_x (projY p), projY p) (solve_for_x_onCurve (projX p) (projY p) (point_onCurve p))). - rewrite <- (point_destruct _ (point_onCurve p)). - subst. - apply point_eq_copy; auto. - destruct (GFopp_solve_for_x p) as [? | A]; auto. - rewrite A in Heqb0. - pose proof (sign_bit_GFopp_negb (projX p)) as sign_bit_opp. - destruct sign_bit_opp as [sign_bit_opp | opp_eq ]; [ | rewrite opp_eq; auto ]. - rewrite Bool.eqb_true_iff in Heqb0. - rewrite Heqb0 in sign_bit_opp. - symmetry in sign_bit_opp. - apply Bool.no_fixpoint_negb in sign_bit_opp. - contradiction. - } { - remember (mkPoint (GFopp (solve_for_x (projY p)), projY p) (solve_for_x_onCurve_GFopp (projX p) (projY p) (point_onCurve p))). - rewrite <- (point_destruct _ (point_onCurve p)). - subst. - apply point_eq_copy; auto. - destruct (GFopp_solve_for_x p) as [A | A]; try apply GFopp_swap; auto; - rewrite A in Heqb0; apply Bool.eqb_false_iff in Heqb0; congruence. - } - Qed. - - Definition PointEncoding := Build_Encoding point (word b) point_enc point_dec point_encoding_valid. - - Print Assumptions PointEncoding. - -End EdDSA25519_Params. |