From 3febea4ed8fdb255c634acbeb3705c88baa89303 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 03:50:08 -0400 Subject: Remove anything incompatible with new algebraic hierarcy - PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway --- src/Experiments/SpecEd25519.v | 165 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 src/Experiments/SpecEd25519.v (limited to 'src/Experiments') diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v new file mode 100644 index 000000000..4e30313d9 --- /dev/null +++ b/src/Experiments/SpecEd25519.v @@ -0,0 +1,165 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. +Require Import Crypto.Spec.ModularWordEncoding. +Require Import Crypto.Encoding.ModularWordEncodingTheorems. +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.WordUtil Crypto.Util.NumTheoryUtil. +Require Import Bedrock.Word. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Logic.Decidable. +Require Import Coq.omega.Omega. + +Local Open Scope nat_scope. +Definition q : Z := (2 ^ 255 - 19)%Z. +Global Instance prime_q : prime q. Admitted. +Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed. + +Definition a : F q := opp 1%F. + +(* TODO (jadep) : make the proofs about a and d more general *) +Lemma nonzero_a : a <> 0%F. +Proof. + unfold a. + intro eq_opp1_0. + apply (@Fq_1_neq_0 q prime_q). + rewrite <- (F_opp_spec 1%F). + rewrite eq_opp1_0. + symmetry; apply F_add_0_r. +Qed. + +Ltac q_bound := pose proof two_lt_q; omega. +Lemma square_a : isSquare a. +Proof. + Lemma q_1mod4 : (q mod 4 = 1)%Z. reflexivity. Qed. + intros. + pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square. + destruct minus1_square as [b b_id]. + apply square_Zmod_F. + exists b; rewrite b_id. + unfold a. + rewrite opp_ZToField. + rewrite FieldToZ_ZToField. + rewrite Z.mod_small; q_bound. +Qed. + +Hint Rewrite + @FieldToZ_add + @FieldToZ_mul + @FieldToZ_opp + @FieldToZ_inv_efficient + @FieldToZ_pow_efficient + @FieldToZ_ZToField + @Zmod_mod + : ZToField. + +Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F. +Lemma nonsquare_d : forall x, (x^2 <> d)%F. + pose proof @euler_criterion_if q prime_q d two_lt_q. + match goal with + [H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H] + end. + unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..]. + vm_compute. (* 10s *) + exact eq_refl. +Qed. (* 10s *) + +Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d := + { + nonzero_a := nonzero_a + (* TODO:port + char_gt_2 : ~ Feq (Fadd Fone Fone) Fzero; + nonzero_a : ~ Feq a Fzero; + nonsquare_d : forall x : F, ~ Feq (Fmul x x) d } + *) + }. +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 q)%nat. +Proof. + 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 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. + +Require Import Crypto.Spec.Encoding. + +Lemma q_pos : (0 < q)%Z. q_bound. Qed. +Definition FqEncoding : canonical encoding of (F q) as word (b-1) := + @modular_word_encoding q (b - 1) q_pos b_valid. + +Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed. +Lemma l_bound : Z.to_nat (Z.of_nat l) < 2 ^ b. +Proof. + rewrite Nat2Z.id. + rewrite <- pow2_id. + rewrite Zpow_pow2. + unfold l. + apply Z2Nat.inj_lt; compute; congruence. +Qed. +Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b := + @modular_word_encoding (Z.of_nat l) b l_pos l_bound. + +Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. + +Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. +Proof. + apply F_eq. + autorewrite with ZToField. + vm_compute. + reflexivity. +Qed. + +Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d). +Local Notation zero := (E.zero(H:=field_modulo)). +Local Notation add := (E.add(H0:=curve25519params)). +Local Infix "*" := (E.mul(H0:=curve25519params)). +Axiom H : forall n : nat, word n -> word (b + b). +Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *) +Axiom B_nonzero : B <> zero. +Axiom l_order_B : l * B = zero. +Axiom point_encoding : canonical encoding of point as word b. +Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b. + +Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding := + { + EdDSA_c_valid := c_valid; + EdDSA_n_ge_c := n_ge_c; + EdDSA_n_le_b := n_le_b; + EdDSA_B_not_identity := B_nonzero; + EdDSA_l_prime := prime_l; + EdDSA_l_odd := l_odd; + EdDSA_l_order_B := l_order_B + }. \ No newline at end of file -- cgit v1.2.3