diff options
Diffstat (limited to 'src/Spec')
-rw-r--r-- | src/Spec/Ed25519.v | 110 | ||||
-rw-r--r-- | src/Spec/EdDSA.v | 10 | ||||
-rw-r--r-- | src/Spec/Encoding.v | 60 |
3 files changed, 124 insertions, 56 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index c4547860a..e5796b8f2 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.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 }. - 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/Encoding.v b/src/Spec/Encoding.v new file mode 100644 index 000000000..95ac85c97 --- /dev/null +++ b/src/Spec/Encoding.v @@ -0,0 +1,60 @@ +Require Import ZArith.ZArith Zpower ZArith. +Require Import NPeano. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. +Require Import Bedrock.Word. +Require Import VerdiTactics. +Require Import Crypto.Util.NatUtil. + +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). + +Local Open Scope nat_scope. + +Section ModularWordEncoding. + Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + + Definition Fm_enc (x : F m) : word sz := natToWord sz (Z.to_nat (FieldToZ x)). + + Definition Fm_dec (x_ : word sz) : option (F m) := + let z := Z.of_nat (wordToNat (x_)) in + if Z_lt_dec z m + then Some (ZToField z) + else None + . + + Lemma bound_check_N : forall x : F m, (N.of_nat (Z.to_nat x) < Npow2 sz)%N. + Proof. + intro. + pose proof (FieldToZ_range x m_pos) as x_range. + rewrite <- Nnat.N2Nat.id. + rewrite Npow2_nat. + apply (Nat2N_inj_lt (Z.to_nat x) (pow2 sz)). + rewrite ZUtil.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. + replace (Z.to_nat 2) with 2%nat by auto. + omega. + Qed. + + Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. + Proof. + unfold Fm_dec, Fm_enc; intros. + pose proof (FieldToZ_range x m_pos). + rewrite wordToNat_natToWord_idempotent by apply bound_check_N. + rewrite Z2Nat.id by omega. + rewrite ZToField_idempotent. + break_if; auto; omega. + Qed. + + Instance modular_word_encoding : encoding of F m as word sz := { + enc := Fm_enc; + dec := Fm_dec; + encoding_valid := Fm_encoding_valid + }. + +End ModularWordEncoding. |