From ce4dba4f81fdeb1c1220b8dabf9d8acb00fce901 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 15 Feb 2016 18:54:23 -0500 Subject: instantiated FqEncoding and FlEncoding (also fixed indentation, which is why the commit looks huge) --- src/Spec/EdDSA.v | 10 +---- src/Spec/EdDSA25519.v | 110 ++++++++++++++++++++++++++++---------------------- 2 files changed, 64 insertions(+), 56 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 35fc1d543..a7b8fe987 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,3 +1,4 @@ +Require Import Crypto.Spec.Encoding. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Spec.CompleteEdwardsCurve. @@ -13,13 +14,6 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. Coercion Word.wordToNat : Word.word >-> nat. -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). - Infix "^" := NPeano.pow. Infix "mod" := NPeano.modulo. Infix "++" := Word.combine. @@ -94,4 +88,4 @@ Section EdDSA. end end end%E. -End EdDSA. \ No newline at end of file +End EdDSA. diff --git a/src/Spec/EdDSA25519.v b/src/Spec/EdDSA25519.v index c4547860a..e5796b8f2 100644 --- a/src/Spec/EdDSA25519.v +++ b/src/Spec/EdDSA25519.v @@ -1,5 +1,6 @@ Require Import ZArith.ZArith Zpower ZArith Znumtheory. Require Import NPeano NArith. +Require Import Crypto.Spec.Encoding. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. @@ -60,58 +61,72 @@ Instance TEParams : TwistedEdwardsParams := { nonsquare_d := nonsquare_d }. - Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n. - Admitted. +Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n. +Admitted. - Definition b := 256. - Lemma b_valid : (2 ^ (b - 1) > Z.to_nat CompleteEdwardsCurve.q)%nat. - Proof. - replace (CompleteEdwardsCurve.q) with q by reflexivity. - unfold q, gt. - replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1)))) - by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat). - rewrite <- Z2Nat.inj_lt; compute; congruence. - Qed. +Definition b := 256. +Lemma b_valid : (2 ^ (b - 1) > Z.to_nat CompleteEdwardsCurve.q)%nat. +Proof. + replace (CompleteEdwardsCurve.q) with q by reflexivity. + unfold q, gt. + replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1)))) + by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat). + rewrite <- Z2Nat.inj_lt; compute; congruence. +Qed. - Definition c := 3. - Lemma c_valid : c = 2 \/ c = 3. - Proof. - right; auto. - Qed. +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. +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. - Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z. - Lemma prime_l : prime (Z.of_nat l). Admitted. - Lemma l_odd : l > 2. - Proof. - unfold l, proj1_sig. - rewrite Z2Nat.inj_add; try omega. - apply lt_plus_trans. - compute; omega. - Qed. - Lemma l_bound : l < pow2 b. - Proof. - rewrite Zpow_pow2. - unfold l. - rewrite <- Z2Nat.inj_lt; compute; congruence. - Qed. +Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z. +Lemma prime_l : prime (Z.of_nat l). Admitted. +Lemma l_odd : l > 2. +Proof. + unfold l, proj1_sig. + rewrite Z2Nat.inj_add; try omega. + apply lt_plus_trans. + compute; omega. +Qed. +Lemma l_bound : l < pow2 b. +Proof. + rewrite Zpow_pow2. + unfold l. + rewrite <- Z2Nat.inj_lt; compute; congruence. +Qed. + +Lemma q_pos : (0 < q)%Z. q_bound. Qed. +Definition FqEncoding : encoding of (F q) as word (b-1) := + @modular_word_encoding q (b - 1) q_pos b_valid. - Definition H : forall n : nat, word n -> word (b + b). Admitted. - Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) - Definition B_nonzero : B <> zero. Admitted. - Definition l_order_B : scalarMult l B = zero. Admitted. - Definition FqEncoding : encoding of F q as word (b - 1). Admitted. - Definition FlEncoding : encoding of F (Z.of_nat l) as word b. Admitted. - Definition PointEncoding : encoding of point as word b. Admitted. +Check @modular_word_encoding. +Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed. +(* form of l_bound needed for FlEncoding *) +Lemma l_bound_encoding : Z.to_nat (Z.of_nat l) < 2 ^ b. +Proof. + rewrite Nat2Z.id. + rewrite <- pow2_id. + exact l_bound. +Qed. +Definition FlEncoding : encoding of F (Z.of_nat l) as word b := + @modular_word_encoding (Z.of_nat l) b l_pos l_bound_encoding. + +Definition H : forall n : nat, word n -> word (b + b). Admitted. +Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) +Definition B_nonzero : B <> zero. Admitted. +Definition l_order_B : scalarMult l B = zero. Admitted. +Definition PointEncoding : encoding of point as word b. Admitted. Instance x : EdDSAParams := { E := TEParams; @@ -134,4 +149,3 @@ Instance x : EdDSAParams := { l_odd := l_odd; l_order_B := l_order_B }. - -- cgit v1.2.3