diff options
| -rw-r--r-- | _CoqProject | 4 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 1 | ||||
| -rw-r--r-- | src/Curves/PointFormats.v | 42 | ||||
| -rw-r--r-- | src/Galois/EdDSA.v | 21 | ||||
| -rw-r--r-- | src/Specific/EdDSA25519.v | 213 | ||||
| -rw-r--r-- | src/Util/NatUtil.v | 56 | ||||
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 81 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 14 |
8 files changed, 396 insertions, 36 deletions
diff --git a/_CoqProject b/_CoqProject index b862cf7ac..a99d9a3f7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,7 +4,9 @@ src/Tactics/VerdiTactics.v src/Util/CaseUtil.v src/Util/ListUtil.v +src/Util/NatUtil.v src/Util/ZUtil.v +src/Util/NumTheoryUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v src/Galois/ZGaloisField.v @@ -14,7 +16,7 @@ src/Galois/ComputationalGaloisField.v src/Galois/BaseSystem.v src/Galois/ModularBaseSystem.v src/Curves/PointFormats.v +src/Galois/EdDSA.v src/Assembly/WordBounds.v src/Curves/Curve25519.v src/Specific/GF25519.v -src/Galois/EdDSA.v diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index edcf6a24c..8bb2148db 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -10,6 +10,7 @@ End Modulus25519. Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. Module Import GFDefs := GaloisDefs Modulus25519. + Local Open Scope GF_scope. Coercion inject : Z >-> GF. Definition a : GF := -1. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 2cf5d3665..1e8df9337 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -5,11 +5,11 @@ Require Import BinNums NArith. Module GaloisDefs (M : Modulus). Module Export GT := GaloisTheory M. - Open Scope GF_scope. End GaloisDefs. Module Type TwistedEdwardsParams (M : Modulus). Module Export GFDefs := GaloisDefs M. + Local Open Scope GF_scope. Parameter a : GF. Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -54,7 +54,7 @@ Proof. case_eq (b - S i); intros; simpl; auto. Qed. -Lemma iter_op_xI : forall {A} p i op z b (a : A), (i < S b) -> +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 | ]. @@ -64,7 +64,7 @@ Proof. rewrite IHi by omega; auto. Qed. -Lemma iter_op_xO : forall {A} p i op z b (a : A), (i < S b) -> +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 | ]. @@ -74,7 +74,7 @@ Proof. rewrite IHi by omega; auto. Qed. -Lemma iter_op_1 : forall {A} i op z b (a : A), (i < S b) -> +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 | ]. @@ -90,36 +90,23 @@ Proof. Qed. Hint Resolve pos_size_gt0. -Lemma test_low_bit_xI : forall p b, testbit_rev p~1 b b = true. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Lemma test_low_bit_xO : forall p b, testbit_rev p~0 b b = false. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Lemma test_low_bit_1 : forall b, testbit_rev 1%positive b b = true. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Ltac low_bit := match goal with -| [ |- context[testbit_rev ?p~1 ?b ?b] ] => rewrite test_low_bit_xI; f_equal; rewrite iter_op_xI -| [ |- context[testbit_rev ?p~0 ?b ?b] ] => rewrite test_low_bit_xO; rewrite iter_op_xO -| [ |- context[testbit_rev 1%positive ?b ?b] ] => rewrite test_low_bit_1; rewrite iter_op_1 +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 |]. - case_eq p; intros; simpl; low_bit; apply IHb; - rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto. + 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 Ewdwards curves with complete addition laws. References: * <https://eprint.iacr.org/2008/013.pdf> * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> @@ -173,6 +160,7 @@ 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. @@ -189,6 +177,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). + Local Open Scope GF_scope. Module Import Curve := CompleteTwistedEdwardsCurve M P. Lemma twistedAddCompletePlus : forall (P1 P2:point), let '(x1, y1) := proj1_sig P1 in @@ -365,7 +354,7 @@ End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. Module Export GFDefs := GaloisDefs M. - Open Scope GF_scope. + Local Open Scope GF_scope. Definition a := inject (- 1). Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -374,6 +363,7 @@ Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. End Minus1Params. Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P. + Local Open Scope GF_scope. Module Import Facts := CompleteTwistedEdwardsFacts M P. Module Import Curve := Facts.Curve. (** [projective] represents a point on an elliptic curve using projective diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index a2df23076..af4f892ca 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -5,8 +5,7 @@ Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. -Open Scope nat_scope. - +Local Open Scope nat_scope. Local Coercion Z.to_nat : Z >-> nat. (* TODO : where should this be? *) @@ -27,6 +26,7 @@ Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). Module Type EdDSAParams. Parameter q : Prime. Axiom q_odd : q > 2. + (* Choosing q sufficiently large is important for security, since the size of * q constrains the size of l below. *) @@ -34,10 +34,9 @@ Module Type EdDSAParams. Module Modulus_q <: Modulus. Definition modulus := q. End Modulus_q. - Module Export GFDefs := GaloisDefs Modulus_q. Parameter b : nat. - Axiom b_valid : 2^(b - 1) > q. + 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). @@ -54,6 +53,10 @@ Module Type EdDSAParams. Parameter n : nat. Axiom n_ge_c : n >= c. Axiom n_le_b : n <= b. + + Module Import GFDefs := GaloisDefs 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: @@ -64,7 +67,7 @@ Module Type EdDSAParams. Parameter a : GF. Axiom a_nonzero : a <> 0%GF. - Axiom a_square : exists x, x^2 = a. + Axiom a_square : exists x, x * x = 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: @@ -100,7 +103,7 @@ Module Type EdDSAParams. * EdDSA secret key from an EdDSA public key. *) Parameter l : Prime. - Axiom l_odd : l > 2. + Axiom l_odd : (l > 2)%nat. Axiom l_order_B : scalarMult l B = zero. (* TODO: (2^c)l = #E *) @@ -116,7 +119,7 @@ Module Type EdDSAParams. 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 = s mod l} as word b. + Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b. Parameter PointEncoding : encoding of point as word b. End EdDSAParams. @@ -130,7 +133,7 @@ Ltac arith := arith'; | [ H : _ |- _ ] => rewrite H; arith' end. -Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s = s mod l}. +Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s mod l = s}. exists (n mod l); abstract arith. Defined. @@ -163,7 +166,7 @@ Module Type EdDSA (Import P : EdDSAParams). let S_ := split2 b b sig in exists A, dec A_ = Some A /\ exists R, dec R_ = Some R /\ - exists S : {s:nat | s = s mod l}, dec S_ = Some S /\ + 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. diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v new file mode 100644 index 000000000..26c45a713 --- /dev/null +++ b/src/Specific/EdDSA25519.v @@ -0,0 +1,213 @@ +Require Import ZArith.ZArith Zpower ZArith Znumtheory. +Require Import NPeano. +Require Import Galois.EdDSA Galois GaloisTheory. +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. + Local Open Scope Z_scope. + 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. + +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 : Z.to_nat q > 2. + Proof. + assert (q >= 0)%Z by (cbv; congruence). + assert (q > 2)%Z by (simpl; cbv; auto). + rewrite Nat2Z.inj_gt. + rewrite Z2Nat.id by omega; auto. + 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 Import GFDefs := GaloisDefs Modulus_q. + Local Open Scope GF_scope. + + 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 square_mod_GF : forall (a x : Z), + (0 <= x < q /\ x * x mod q = a)%Z -> + (inject x * inject x = inject a)%GF. + Proof. + intros. + destruct H0. + rewrite <- inject_distr_mul. + rewrite inject_mod_eq. + replace modulus with q by auto. + rewrite H1; reflexivity. + Qed. + + Lemma a_square : exists x, (x * x = a)%GF. + Proof. + intros. + pose proof (minus1_square_1mod4 q (proj2_sig q) q_1mod4). + destruct H0. + pose proof (square_mod_GF (q - 1)%Z x H0). + exists (inject x). + unfold a. + replace (GFopp 1) with (inject (q - 1)) by galois. + auto. + Qed. + + (* TODO *) + Parameter d : GF. + Axiom d_nonsquare : forall x, x^2 <> d. + + Module CurveParameters <: TwistedEdwardsParams Modulus_q. + Module GFDefs := GFDefs. + 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 *) + Parameter B : point. + Axiom B_not_identity : B <> zero. + + (* TODO *) + Parameter l : Prime. + Axiom l_odd : (Z.to_nat l > 2)%nat. + 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. (* TODO *) + Admitted. + + Lemma GF_mod_bound : forall (x : GF), (0 <= x < q)%Z. + Proof. + intros. + assert (0 < q)%Z by (prime_bound; omega). + pose proof (Z.mod_pos_bound x q H0). + rewrite <- (inject_eq x). + replace q with modulus in * by auto. + unfold GFToZ, inject in *. + auto. + 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. + 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. + 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. + Qed. + Definition FlEncoding := + Build_Encoding {s:nat | s mod (Z.to_nat l) = s} (word b) Fl_enc Fl_dec Fl_encoding_valid. + + (* TODO *) + Parameter PointEncoding : encoding of point as word b. +End EdDSA25519_Params. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v new file mode 100644 index 000000000..afed2a231 --- /dev/null +++ b/src/Util/NatUtil.v @@ -0,0 +1,56 @@ +Require Import NPeano Omega. + +Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1. +Proof. + intros. + assert (b = 1 * b) by omega. + rewrite H0 at 1. + rewrite <- Nat.div_add by auto. + reflexivity. +Qed. + +Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2). +Proof. + assert (4 <> 0) as ne40 by omega. + induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. { + rewrite H0 in H1. + simpl in H1. + rewrite H1. + exists 0; auto. + } { + rewrite mult_succ_r in H1. + assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; omega). + rewrite <- Nat.add_1_r in H. + replace x with ((x - 4) + 4) in H by omega. + rewrite div_minus in H by auto. + apply Nat.add_cancel_r in H. + replace x with ((x - 4) + (1 * 4)) in H0 by omega. + rewrite Nat.mod_add in H0 by auto. + pose proof (IHc _ H H0). + destruct H2. + exists (x0 + 1). + rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto. + replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega. + apply Nat.add_cancel_r in H1. + replace (2 * (x0 + 1)) with (2 * x0 + 2) + by (rewrite Nat.mul_add_distr_l; auto). + rewrite H2. + rewrite <- Nat.div_add by omega. + f_equal. + simpl. + apply Nat.sub_add; auto. + } +Qed. + +Lemma Nat2N_inj_lt : forall n m, (N.of_nat n < N.of_nat m)%N <-> n < m. +Proof. + split; intros. { + rewrite nat_compare_lt. + rewrite Nnat.Nat2N.inj_compare. + rewrite N.compare_lt_iff; auto. + } { + rewrite <- N.compare_lt_iff. + rewrite <- Nnat.Nat2N.inj_compare. + rewrite <- nat_compare_lt; auto. + } +Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v new file mode 100644 index 000000000..4a54e5437 --- /dev/null +++ b/src/Util/NumTheoryUtil.v @@ -0,0 +1,81 @@ +Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. +Require Import Omega NPeano Arith. +Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. +Local Open Scope Z. + +Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p), + (x * 2 + 1 = p)%Z -> (a ^ x mod p = 1)%Z -> + exists b : Z, (0 <= b < p /\ b * b mod p = a)%Z. +Admitted. + +Lemma divide2_1mod4 : forall x, x mod 4 = 1 -> 0 <= x -> (2 | x / 2). +Proof. + intros. + assert (Z.to_nat x mod 4 = 1)%nat. { + replace 1%Z with (Z.of_nat 1) in H by auto. + replace (x mod 4)%Z with (Z.of_nat (Z.to_nat x mod 4)) in H + by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto). + apply Nat2Z.inj in H; auto. + } + remember (Z.to_nat x / 4)%nat as c. + pose proof (divide2_1mod4_nat c (Z.to_nat x) Heqc H1). + destruct H2. + replace 2%nat with (Z.to_nat 2) in H2 by auto. + apply inj_eq in H2. + rewrite div_Zdiv in H2 by (replace (Z.to_nat 2) with 2%nat by auto; omega). + rewrite Nat2Z.inj_mul in H2. + do 2 rewrite Z2Nat.id in H2 by (auto || omega). + rewrite Z.mul_comm in H2. + symmetry in H2. + apply Zdivide_intro in H2; auto. +Qed. + +Lemma minus1_even_pow : forall x y, (2 | y) -> (1 < x) -> (0 <= y) -> ((x - 1) ^ y mod x = 1). +Proof. + intros. + apply Zdivide_Zdiv_eq in H; try omega. + rewrite H. + rewrite Z.pow_mul_r by omega. + assert ((x - 1)^2 mod x = 1). { + replace ((x - 1)^2) with (x ^ 2 - 2 * x + 1) + by (do 2 rewrite Z.pow_2_r; rewrite Z.mul_sub_distr_l; do 2 rewrite Z.mul_sub_distr_r; omega). + rewrite Zplus_mod. + rewrite Z.pow_2_r. + rewrite <- Z.mul_sub_distr_r. + rewrite Z_mod_mult. + do 2 rewrite Zmod_1_l by auto; auto. + } + rewrite <- (Z2Nat.id (y / 2)) by omega. + induction (Z.to_nat (y / 2)); try apply Zmod_1_l; auto. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite Zmult_mod. + rewrite IHn. + rewrite H2. + simpl. + apply Zmod_1_l; auto. +Qed. + +Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p), + (p mod 4 = 1)%Z -> exists b : Z, (0 <= b < p /\ b * b mod p = p - 1)%Z. +Proof. + intros. + assert (4 <> 0)%Z by omega. + pose proof (Z.div_mod p 4 H0). + pose proof (prime_ge_2 p (prime_p)). + assert (2 | p / 2)%Z by (apply divide2_1mod4; (auto || omega)). + apply (euler_criterion (p - 1) (p / 2) p prime_p); + [ | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega]. + rewrite <- H. + rewrite H1 at 3. + f_equal. + replace 4%Z with (2 * 2)%Z by auto. + rewrite <- Z.div_div by omega. + rewrite <- Zdivide_Zdiv_eq_2 by (auto || omega). + replace (2 * 2 * (p / 2) / 2)%Z with (2 * (2 * (p / 2)) / 2)%Z + by (f_equal; apply Z.mul_assoc). + rewrite ZUtil.Z_div_mul' by omega. + rewrite Z.mul_comm. + auto. +Qed. + diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5950f57ad..1a48abfd6 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,7 @@ Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. Require Import Omega NPeano Arith. +Require Import Crypto.Util.NatUtil. +Require Import Bedrock.Word. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -50,3 +52,15 @@ Qed. Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. intuition. Qed. + +Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)). +Proof. + induction n; intros; auto. + simpl pow2. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite untimes2. + rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega). + rewrite <- IHn. + auto. +Qed. |