diff options
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | _CoqProject | 5 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 4 | ||||
-rw-r--r-- | src/Spec/EdDSA.v | 19 | ||||
-rw-r--r-- | src/Spec/Encoding.v | 3 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 6 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 27 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 15 |
8 files changed, 45 insertions, 38 deletions
@@ -4,8 +4,10 @@ SRC_DIR := src .PHONY: coq clean install coqprime update-_CoqProject .DEFAULT_GOAL := coq +SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' + update-_CoqProject:: - (echo '-R $(SRC_DIR) $(MOD_NAME)'; git ls-files src/*.v) > _CoqProject + (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files "src/*.v" | $(SORT_COQPROJECT))) > _CoqProject coq: coqprime Makefile.coq $(MAKE) -f Makefile.coq diff --git a/_CoqProject b/_CoqProject index 984606959..61f0fdd3d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,11 +1,11 @@ -R src Crypto src/BaseSystem.v src/BoundedIterOp.v +src/EdDSAProofs.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v -src/EdDSAProofs.v src/Encoding/EncodingTheorems.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v @@ -13,8 +13,8 @@ src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v -src/Spec/EdDSA.v src/Spec/Ed25519.v +src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/PointEncoding.v @@ -24,4 +24,5 @@ src/Util/CaseUtil.v src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v +src/Util/WordUtil.v src/Util/ZUtil.v diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index adc40dae6..e16cc73f6 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -4,7 +4,7 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. +Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. Require Import VerdiTactics. Require Import Decidable. @@ -150,7 +150,7 @@ Instance x : EdDSAParams := { FqEncoding := FqEncoding; FlEncoding := FlEncoding; PointEncoding := PointEncoding; - + b_valid := b_valid; c_valid := c_valid; n_ge_c := n_ge_c; diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index a7b8fe987..45950f6a1 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -2,16 +2,11 @@ Require Import Crypto.Spec.Encoding. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Util.WordUtil. Require Bedrock.Word. Require Znumtheory BinInt. Require NPeano. -(* TODO : where should this be? *) -Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. - refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with - | eq_refl => w - end)); abstract omega. Defined. - Coercion Word.wordToNat : Word.word >-> nat. Infix "^" := NPeano.pow. @@ -21,21 +16,21 @@ Infix "++" := Word.combine. Section EdDSAParams. Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) E : TwistedEdwardsParams; (* underlying elliptic curve *) - + b : nat; (* public keys are k bits, signatures are 2*k bits *) b_valid : 2^(b - 1) > BinInt.Z.to_nat q; FqEncoding : encoding of F q as Word.word (b-1); PointEncoding : encoding of point as Word.word b; - + H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) - + c : nat; (* cofactor E = 2^c *) c_valid : c = 2 \/ c = 3; - + n : nat; (* secret keys are (n+1) bits *) n_ge_c : n >= c; n_le_b : n <= b; - + B : point; B_not_identity : B <> zero; @@ -74,7 +69,7 @@ Section EdDSA. let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat (r + H (enc R ++ public sk ++ M) * s)) in enc R ++ enc S. - + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v index 95ac85c97..7bef9295b 100644 --- a/src/Spec/Encoding.v +++ b/src/Spec/Encoding.v @@ -4,6 +4,7 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithme Require Import Bedrock.Word. Require Import VerdiTactics. Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.WordUtil. Class Encoding (T B:Type) := { enc : T -> B ; @@ -33,7 +34,7 @@ Section ModularWordEncoding. rewrite <- Nnat.N2Nat.id. rewrite Npow2_nat. apply (Nat2N_inj_lt (Z.to_nat x) (pow2 sz)). - rewrite ZUtil.Zpow_pow2. + rewrite Zpow_pow2. destruct x_range as [x_low x_high]. apply Z2Nat.inj_lt in x_high; try omega. rewrite <- ZUtil.pow_Z2N_Zpow by omega. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 256654df7..4ba6d0808 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,5 +1,4 @@ Require Import NPeano Omega. -Require Import Bedrock.Word. Local Open Scope nat_scope. @@ -57,8 +56,3 @@ Proof. rewrite <- nat_compare_lt; auto. } Qed. - -Lemma pow2_id : forall n, pow2 n = 2 ^ n. -Proof. - induction n; intros; simpl; auto. -Qed. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v new file mode 100644 index 000000000..49de971ef --- /dev/null +++ b/src/Util/WordUtil.v @@ -0,0 +1,27 @@ +Require Import NPeano. +Require Import ZArith.ZArith. +Require Import Bedrock.Word. + +Local Open Scope nat_scope. + +Lemma pow2_id : forall n, pow2 n = 2 ^ n. +Proof. + induction n; intros; simpl; auto. +Qed. + +Lemma Zpow_pow2 : forall n, pow2 n = 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. + +Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. + refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with + | eq_refl => w + end)); abstract omega. Defined. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index ac1c47152..2cfab2e90 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,7 +1,6 @@ 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. @@ -38,7 +37,7 @@ Proof. rewrite Zmod_mod; auto. Qed. -Lemma pos_pow_nat_pos : forall x n, +Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. do 2 (intros; induction n; subst; simpl in *; auto with zarith). rewrite <- Pos.add_1_r, Zpower_pos_is_exp. @@ -53,18 +52,6 @@ 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. - Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. Proof. |