diff options
| -rw-r--r-- | _CoqProject | 11 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 30 | ||||
| -rw-r--r-- | src/EdDSAProofs.v | 108 | ||||
| -rw-r--r-- | src/Encoding/PointEncodingPre.v | 275 | ||||
| -rw-r--r-- | src/Encoding/PointEncodingTheorems.v | 207 | ||||
| -rw-r--r-- | src/Experiments/SpecEd25519.v (renamed from src/Spec/Ed25519.v) | 82 | ||||
| -rw-r--r-- | src/Spec/PointEncoding.v | 39 |
7 files changed, 37 insertions, 715 deletions
diff --git a/_CoqProject b/_CoqProject index ffb532390..a3458ed1e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,21 +5,18 @@ Bedrock/Word.v src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v -src/EdDSAProofs.v -src/Field.v src/Nsatz.v src/Rep.v src/Testbit.v -src/UnfinishedDerivations.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v -src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v -src/Encoding/PointEncodingPre.v -src/Encoding/PointEncodingTheorems.v +src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v +src/Experiments/GenericFieldPow.v +src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v @@ -32,12 +29,10 @@ src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v -src/Spec/Ed25519.v src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v -src/Spec/PointEncoding.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v deleted file mode 100644 index 50027349d..000000000 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ /dev/null @@ -1,30 +0,0 @@ -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Util.IterAssocOp. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. - -Section EdwardsDoubleAndAdd. - Context {prm:TwistedEdwardsParams}. - Definition doubleAndAdd (bound n : nat) (P : E.point) : E.point := - iter_op E.add E.zero N.testbit_nat (N.of_nat n) P bound. - - Lemma scalarMult_double : forall n P, E.mul (n + n) P = E.mul n (P + P)%E. - Proof. - intros. - replace (n + n)%nat with (n * 2)%nat by omega. - induction n; simpl; auto. - rewrite E.add_assoc. - f_equal; auto. - Qed. - - Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound -> - E.mul n P = doubleAndAdd bound n P. - Proof. - induction n; auto; intros; unfold doubleAndAdd; - rewrite iter_op_spec with (scToN := fun x => x); ( - unfold Morphisms.Proper, Morphisms.respectful, Equivalence.equiv; - intros; subst; try rewrite Nat2N.id; - reflexivity || assumption || apply E.add_assoc - || rewrite E.add_comm; apply E.add_0_r). - Qed. -End EdwardsDoubleAndAdd.
\ No newline at end of file diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v deleted file mode 100644 index 2e45bcad5..000000000 --- a/src/EdDSAProofs.v +++ /dev/null @@ -1,108 +0,0 @@ -Require Import Crypto.Spec.EdDSA Crypto.Spec.Encoding. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Bedrock.Word. -Require Import Coq.ZArith.Znumtheory Coq.ZArith.BinInt Coq.ZArith.ZArith. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. -Require Import Crypto.Tactics.VerdiTactics. -Local Open Scope nat_scope. - -Section EdDSAProofs. - Context {prm:EdDSAParams}. - Existing Instance E. - Existing Instance PointEncoding. - Existing Instance FqEncoding. - Existing Instance FlEncoding. - Existing Instance n_le_b. - Hint Rewrite sign_spec split1_combine split2_combine. - Hint Rewrite Nat.mod_mod using omega. - - Ltac arith' := intros; autorewrite with core; try (omega || congruence). - - Ltac arith := arith'; - repeat match goal with - | [ H : _ |- _ ] => rewrite H; arith' - end. - - (* for signature (R_, S_), R_ = encode_point (r * B) *) - Lemma decode_sign_split1 : forall A_ sk {n} (M : word n), - split1 b b (sign A_ sk M) = enc (wordToNat (H (prngKey sk ++ M)) * B)%E. - Proof. - unfold sign; arith. - Qed. - Hint Rewrite decode_sign_split1. - - (* for signature (R_, S_), S_ = encode_scalar (r + H(R_, A_, M)s) *) - Lemma decode_sign_split2 : forall sk {n} (M : word n), - split2 b b (sign (public sk) sk M) = - let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : E.point := (r * B)%E in (* commitment to nonce *) - let s : nat := curveKey sk in (* secret scalar *) - let S : F (Z.of_nat l) := ZToField (Z.of_nat (r + H (enc R ++ public sk ++ M) * s)) in - enc S. - Proof. - unfold sign; arith. - Qed. - Hint Rewrite decode_sign_split2. - - Hint Rewrite E.add_0_r E.add_0_l E.add_assoc. - Hint Rewrite E.mul_assoc E.mul_add_l E.mul_0_l E.mul_zero_r. - Hint Rewrite plus_O_n plus_Sn_m mult_0_l mult_succ_l. - Hint Rewrite l_order_B. - Lemma l_order_B' : forall x, (l * x * B = E.zero)%E. - Proof. - intros; rewrite Mult.mult_comm. rewrite <- E.mul_assoc. arith. - Qed. Hint Rewrite l_order_B'. - - Lemma scalarMult_mod_l : forall n0, (n0 mod l * B = n0 * B)%E. - Proof. - intros. - rewrite (div_mod n0 l) at 2 by (generalize l_odd; omega). - arith. - Qed. Hint Rewrite scalarMult_mod_l. - - Hint Rewrite @encoding_valid. - Hint Rewrite @FieldToZ_ZToField. - Hint Rewrite <-mod_Zmod. - Hint Rewrite Nat2Z.id. - - Lemma l_nonzero : l <> O. pose l_odd; omega. Qed. - Hint Resolve l_nonzero. - - Lemma verify_valid_passes : forall sk {n} (M : word n), - verify (public sk) M (sign (public sk) sk M) = true. - Proof. - unfold verify, sign, public; arith; try break_if; intuition. - Qed. - - (* This is just an experiment, talk to andreser if you think this is a good idea *) - Inductive valid {n:nat} : word b -> Word.word n -> word (b+b) -> Prop := - Valid : forall (A:E.point) (M:Word.word n) (S:nat) (R:E.point), - (S * B = R + (H (enc R ++ enc A ++ M)) * A)%E - -> valid (enc A) M (enc R ++ enc (ZToField (BinInt.Z.of_nat S))). - Goal forall A_ {n} (M:Word.word n) sig, verify A_ M sig = true <-> valid A_ M sig. - split; unfold verify. - Focus 2. { - intros. - inversion H. subst. - rewrite !Word.split2_combine, !Word.split1_combine, !encoding_valid. - rewrite FieldToZ_ZToField. - rewrite <-Zdiv.mod_Zmod by admit. - rewrite Znat.Nat2Z.id. - rewrite <-H0. - assert ((S mod l) * B = S * B)%E as Hl by admit; rewrite Hl. - destruct (E.point_eq_dec (S * B)%E); congruence. - } Unfocus. { - repeat match goal with |- context [match ?x with _ => _ end] => case_eq x; intro end; try congruence. - intros. clear H. - repeat match goal with [H: _ |- _ ] => apply encoding_canonical in H end; subst. - rewrite <-(Word.combine_split b b sig). - rewrite <-H0 in *; clear H0. rewrite <-H2 in *; clear H2. - assert (f = (ZToField (BinInt.Z.of_nat (BinInt.Z.to_nat (FieldToZ f))))) as H1. { - rewrite Znat.Z2Nat.id by admit. rewrite ZToField_FieldToZ; reflexivity. } - rewrite H1; clear H1. - econstructor; trivial. - } - Qed. -End EdDSAProofs. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v deleted file mode 100644 index 73ced869b..000000000 --- a/src/Encoding/PointEncodingPre.v +++ /dev/null @@ -1,275 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Coq.Program.Equality. -Require Import Crypto.Encoding.EncodingTheorems. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Bedrock.Word. -Require Import Crypto.Encoding.ModularWordEncodingTheorems. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.ZUtil. - -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic. - -Local Open Scope F_scope. - -Section PointEncoding. - Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} - {bound_check : (Z.to_nat q < 2 ^ sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} - {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1} - {FqEncoding : canonical encoding of (F q) as (word sz)} - {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} - {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. - Existing Instance prime_q. - - Add Field Ffield : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - - Lemma solve_sqrt_valid : forall p, E.onCurve p -> - sqrt_valid (E.solve_for_x2 (snd p)). - Proof. - intros ? onCurve_xy. - destruct p as [x y]; simpl. - rewrite (E.solve_correct x y) in onCurve_xy. - rewrite <- onCurve_xy. - unfold sqrt_valid. - eapply sqrt_mod_q_valid; eauto. - unfold isSquare; eauto. - Grab Existential Variables. eauto. - Qed. - - Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y). - Proof. - intros. - unfold sqrt_valid in *. - apply E.solve_correct; auto. - Qed. - - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y). - Proof. - intros y sqrt_valid_x2. - unfold sqrt_valid in *. - apply E.solve_correct. - rewrite <- sqrt_valid_x2 at 2. - ring. - Qed. - - Definition point_enc_coordinates (p : (F q * F q)) : Word.word (S sz) := let '(x,y) := p in - Word.WS (sign_bit x) (enc y). - - Let point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in - Word.WS (sign_bit x) (enc y). - - Definition point_dec_coordinates (sign_bit : F q -> bool) (w : Word.word (S sz)) : option (F q * F q) := - match dec (Word.wtl w) with - | None => None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - if F_eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - if (andb (F_eqb x 0) (whd w)) - then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*) - else Some p - else None - end. - - Ltac inversion_Some_eq := match goal with [H: Some ?x = Some ?y |- _] => inversion H; subst end. - - Lemma point_dec_coordinates_onCurve : forall w p, point_dec_coordinates sign_bit w = Some p -> E.onCurve p. - Proof. - unfold point_dec_coordinates; intros. - edestruct dec; [ | congruence]. - break_if; [ | congruence]. - break_if; [ congruence | ]. - break_if; inversion_Some_eq; auto using solve_onCurve, solve_opp_onCurve. - Qed. - - Lemma prod_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}) - (x y : (A * A)), {x = y} + {x <> y}. - Proof. - decide equality. - Qed. - - Lemma option_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}) - (x y : option A), {x = y} + {x <> y}. - Proof. - decide equality. - Qed. - - Definition point_dec' w p : option E.point := - match (option_eq_dec (prod_eq_dec F_eq_dec) (point_dec_coordinates sign_bit w) (Some p)) with - | left EQ => Some (exist _ p (point_dec_coordinates_onCurve w p EQ)) - | right _ => None (* this case is never reached *) - end. - - Definition point_dec (w : word (S sz)) : option E.point := - match (point_dec_coordinates sign_bit w) with - | Some p => point_dec' w p - | None => None - end. - - Lemma point_coordinates_encoding_canonical : forall w p, - point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w. - Proof. - unfold point_dec_coordinates, point_enc_coordinates; intros ? ? coord_dec_Some. - case_eq (dec (wtl w)); [ intros ? dec_Some | intros dec_None; rewrite dec_None in *; congruence ]. - destruct p. - rewrite (shatter_word w). - f_equal; rewrite dec_Some in *; - do 2 (break_if; try congruence); inversion coord_dec_Some; subst. - + destruct (F_eq_dec (sqrt_mod_q (E.solve_for_x2 f1)) 0%F) as [sqrt_0 | ?]. - - rewrite sqrt_0 in *. - apply sqrt_mod_q_root_0 in sqrt_0; try assumption. - rewrite sqrt_0 in *. - break_if; [symmetry; auto using Bool.eqb_prop | ]. - rewrite sign_bit_zero in *. - simpl in Heqb; rewrite Heqb in *. - discriminate. - - break_if. - symmetry; auto using Bool.eqb_prop. - rewrite <- sign_bit_opp by assumption. - destruct (whd w); inversion Heqb0; break_if; auto. - + inversion coord_dec_Some; subst. - auto using encoding_canonical. -Qed. - - Lemma point_encoding_canonical : forall w x, point_dec w = Some x -> point_enc x = w. - Proof. - (* - unfold point_enc; intros. - unfold point_dec in *. - assert (point_dec_coordinates w = Some (proj1_sig x)). { - set (y := point_dec_coordinates w) in *. - revert H. - dependent destruction y. intros. - rewrite H0 in H. - *) - Admitted. - -Lemma point_dec_coordinates_correct w - : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates sign_bit w. -Proof. - unfold point_dec, option_map. - do 2 break_match; try congruence; unfold point_dec' in *; - break_match; try congruence. - inversion_Some_eq. - reflexivity. -Qed. - -Lemma y_decode : forall p, dec (wtl (point_enc_coordinates p)) = Some (snd p). -Proof. - intros. - destruct p as [x y]; simpl. - exact (encoding_valid y). -Qed. - -Lemma sign_bit_opp_eq_iff : forall x y, y <> 0 -> - (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). -Proof. - split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); - try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp in * by auto; - rewrite y_sign, x_sign in *; reflexivity || discriminate. -Qed. - -Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> - sign_bit x = sign_bit y -> x = y. -Proof. - intros ? ? y_nonzero squares_eq sign_match. - destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. - assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). - apply sign_bit_opp_eq_iff in sign_mismatch; auto. - congruence. -Qed. - -Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) -> - sign_bit x = sign_bit x' -> x = x'. -Proof. - intros ? ? ? onCurve_x onCurve_x' sign_match. - apply E.solve_correct in onCurve_x. - apply E.solve_correct in onCurve_x'. - destruct (F_eq_dec x' 0). - + subst. - rewrite Fq_pow_zero in onCurve_x' by congruence. - rewrite <- onCurve_x' in *. - eapply Fq_root_zero; eauto. - + apply sign_bit_squares; auto. - rewrite onCurve_x, onCurve_x'. - reflexivity. -Qed. - -Lemma point_encoding_coordinates_valid : forall p, E.onCurve p -> - point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p. -Proof. - intros p onCurve_p. - unfold point_dec_coordinates. - rewrite y_decode. - pose proof (solve_sqrt_valid p onCurve_p) as solve_sqrt_valid_p. - destruct p as [x y]. - unfold sqrt_valid in *. - simpl. - replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption). - case_eq (F_eqb x 0); intro eqb_x_0. - + apply F_eqb_eq in eqb_x_0; rewrite eqb_x_0 in *. - rewrite !Fq_pow_zero, sqrt_mod_q_of_0, Fq_pow_zero by congruence. - rewrite if_F_eq_dec_if_F_eqb, sign_bit_zero. - reflexivity. - + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_root_0 in false_eq; try assumption; - apply Fq_root_zero in false_eq; rewrite false_eq, F_eqb_refl in eqb_x_0; congruence). - replace (F_eqb (sqrt_mod_q (x ^ 2)) 0) with false by (symmetry; - apply F_eqb_neq_complete; assumption). - break_if. - - simpl. - f_equal. - break_if. - * rewrite Bool.eqb_true_iff in Heqb. - pose proof (solve_onCurve y solve_sqrt_valid_p). - f_equal. - apply (sign_bit_match _ _ y); auto. - apply E.solve_correct in onCurve_p; rewrite onCurve_p in *. - assumption. - * rewrite Bool.eqb_false_iff in Heqb. - pose proof (solve_opp_onCurve y solve_sqrt_valid_p). - f_equal. - apply sign_bit_opp_eq_iff in Heqb; try assumption. - apply (sign_bit_match _ _ y); auto. - apply E.solve_correct in onCurve_p. - rewrite onCurve_p; auto. - - simpl in solve_sqrt_valid_p. - replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption). - congruence. -Qed. - -Lemma point_dec'_valid : forall p, - point_dec' (point_enc_coordinates (proj1_sig p)) (proj1_sig p) = Some p. -Proof. - unfold point_dec'; intros. - break_match. - + f_equal. - destruct p. - apply E.point_eq. - reflexivity. - + rewrite point_encoding_coordinates_valid in n by apply (proj2_sig p). - congruence. -Qed. - -Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. -Proof. - intros. - unfold point_dec. - replace (point_enc p) with (point_enc_coordinates (proj1_sig p)) by reflexivity. - break_match; rewrite point_encoding_coordinates_valid in * by apply (proj2_sig p); try congruence. - inversion_Some_eq. - eapply point_dec'_valid. -Qed. - -End PointEncoding. diff --git a/src/Encoding/PointEncodingTheorems.v b/src/Encoding/PointEncodingTheorems.v deleted file mode 100644 index ccea1d81b..000000000 --- a/src/Encoding/PointEncodingTheorems.v +++ /dev/null @@ -1,207 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Coq.Program.Equality. -Require Import Crypto.Encoding.EncodingTheorems. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. - -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic Crypto.Spec.CompleteEdwardsCurve. - -Local Open Scope F_scope. - -Section PointEncoding. - Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} - {FqEncoding : canonical encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz} - {q_5mod8 : (CompleteEdwardsCurve.q mod 8 = 5)%Z} - {sqrt_minus1_valid : (@ZToField CompleteEdwardsCurve.q 2 ^ BinInt.Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1}. - Existing Instance CompleteEdwardsCurve.prime_q. - - Add Field Ffield : (@PrimeFieldTheorems.Ffield_theory CompleteEdwardsCurve.q _) - (morphism (@ModularArithmeticTheorems.Fring_morph CompleteEdwardsCurve.q), - preprocess [ModularArithmeticTheorems.Fpreprocess], - postprocess [ModularArithmeticTheorems.Fpostprocess; try exact PrimeFieldTheorems.Fq_1_neq_0; try assumption], - constants [ModularArithmeticTheorems.Fconstant], - div (@ModularArithmeticTheorems.Fmorph_div_theory CompleteEdwardsCurve.q), - power_tac (@ModularArithmeticTheorems.Fpower_theory CompleteEdwardsCurve.q) [ModularArithmeticTheorems.Fexp_tac]). - - Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - - Lemma solve_sqrt_valid : forall (p : E.point), - sqrt_valid (E.solve_for_x2 (snd (proj1_sig p))). - Proof. - intros. - destruct p as [[x y] onCurve_xy]; simpl. - rewrite (E.solve_correct x y) in onCurve_xy. - rewrite <- onCurve_xy. - unfold sqrt_valid. - eapply sqrt_mod_q_valid; eauto. - unfold isSquare; eauto. - Grab Existential Variables. eauto. - Qed. - - Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y). - Proof. - intros. - unfold sqrt_valid in *. - apply E.solve_correct; auto. - Qed. - - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y). - Proof. - intros y sqrt_valid_x2. - unfold sqrt_valid in *. - apply E.solve_correct. - rewrite <- sqrt_valid_x2 at 2. - ring. - Qed. - -Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N. -Definition point_enc (p : E.point) : word (S sz) := let '(x,y) := proj1_sig p in - WS (sign_bit x) (enc y). -Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) := - match dec (wtl w) with - | None => None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - if F_eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - Some p - else None - end. - -Definition point_dec (w : word (S sz)) : option E.point := - match dec (wtl w) with - | None => None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - match (F_eq_dec (x ^ 2) x2) with - | right _ => None - | left EQ => if Bool.eqb (whd w) (sign_bit x) - then Some (exist _ (x, y) (solve_onCurve y EQ)) - else Some (exist _ (opp x, y) (solve_opp_onCurve y EQ)) - end - end. - -Lemma point_dec_coordinates_correct w - : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w. -Proof. - unfold point_dec, point_dec_coordinates. - edestruct dec; [ | reflexivity ]. - edestruct @F_eq_dec; [ | reflexivity ]. - edestruct @Bool.eqb; reflexivity. -Qed. - -Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)). -Proof. - intros. - destruct p as [[x y] onCurve_p]; simpl. - exact (encoding_valid y). -Qed. - - -Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. -Proof. - intros x x_nonzero. - intro false_eq. - apply x_nonzero. - apply F_eq_opp_zero; try apply two_lt_q. - apply wordToN_inj in false_eq. - apply encoding_inj in false_eq. - auto. -Qed. - -Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x). -Proof. - intros x x_nonzero. - unfold sign_bit. - rewrite <- N.leb_antisym. - rewrite N.ltb_compare, N.leb_compare. - rewrite F_opp_involutive. - case_eq (wordToN (enc x) ?= wordToN (enc (opp x)))%N; auto. - intro wordToN_enc_eq. - pose proof (wordToN_enc_neq_opp x x_nonzero). - apply N.compare_eq_iff in wordToN_enc_eq. - congruence. -Qed. - -Lemma sign_bit_opp : forall x y, y <> 0 -> - (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). -Proof. - split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); - try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto; - rewrite y_sign, x_sign in *; reflexivity || discriminate. -Qed. - -Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> - sign_bit x = sign_bit y -> x = y. -Proof. - intros ? ? y_nonzero squares_eq sign_match. - destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. - assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). - apply sign_bit_opp in sign_mismatch; auto. - congruence. -Qed. - -Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) -> - sign_bit x = sign_bit x' -> x = x'. -Proof. - intros ? ? ? onCurve_x onCurve_x' sign_match. - apply E.solve_correct in onCurve_x. - apply E.solve_correct in onCurve_x'. - destruct (F_eq_dec x' 0). - + subst. - rewrite Fq_pow_zero in onCurve_x' by congruence. - rewrite <- onCurve_x' in *. - eapply Fq_root_zero; eauto. - + apply sign_bit_squares; auto. - rewrite onCurve_x, onCurve_x'. - reflexivity. -Qed. - -Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. -Proof. - intros. - unfold point_dec. - rewrite y_decode. - pose proof solve_sqrt_valid p as solve_sqrt_valid_p. - unfold sqrt_valid in *. - destruct p as [[x y] onCurve_p]. - simpl in *. - destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition. - break_if; f_equal; apply E.point_eq. - + rewrite Bool.eqb_true_iff in Heqb. - pose proof (solve_onCurve y solve_sqrt_valid_p). - f_equal. - apply (sign_bit_match _ _ y); auto. - + rewrite Bool.eqb_false_iff in Heqb. - pose proof (solve_opp_onCurve y solve_sqrt_valid_p). - f_equal. - apply sign_bit_opp in Heqb. - apply (sign_bit_match _ _ y); auto. - intro eq_zero. - apply E.solve_correct in onCurve_p. - rewrite eq_zero in *. - rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. - rewrite <- solve_sqrt_valid_p in onCurve_p. - apply Fq_root_zero in onCurve_p. - rewrite onCurve_p in Heqb; auto. -Qed. - -(* Waiting on canonicalization *) -Lemma point_encoding_canonical : forall (x_enc : word (S sz)) (x : E.point), -point_dec x_enc = Some x -> point_enc x = x_enc. -Admitted. - -Instance point_encoding : canonical encoding of E.point as (word (S sz)) := { - enc := point_enc; - dec := point_dec; - encoding_valid := point_encoding_valid; - encoding_canonical := point_encoding_canonical -}. - -End PointEncoding. diff --git a/src/Spec/Ed25519.v b/src/Experiments/SpecEd25519.v index 4876bb8d1..4e30313d9 100644 --- a/src/Spec/Ed25519.v +++ b/src/Experiments/SpecEd25519.v @@ -1,6 +1,6 @@ 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.PointEncoding Crypto.Spec.ModularWordEncoding. +Require Import Crypto.Spec.ModularWordEncoding. Require Import Crypto.Encoding.ModularWordEncodingTheorems. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. @@ -13,7 +13,7 @@ Require Import Coq.omega.Omega. Local Open Scope nat_scope. Definition q : Z := (2 ^ 255 - 19)%Z. -Lemma prime_q : prime q. Admitted. +Global Instance prime_q : prime q. Admitted. Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed. Definition a : F q := opp 1%F. @@ -65,24 +65,23 @@ Lemma nonsquare_d : forall x, (x^2 <> d)%F. exact eq_refl. Qed. (* 10s *) -Instance curve25519params : TwistedEdwardsParams := { - q := q; - prime_q := prime_q; - two_lt_q := two_lt_q; - a := a; - nonzero_a := nonzero_a; - square_a := square_a; - d := d; - nonsquare_d := nonsquare_d -}. +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 CompleteEdwardsCurve.q)%nat. +Lemma b_valid : (2 ^ (b - 1) > Z.to_nat 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). @@ -143,37 +142,24 @@ Proof. reflexivity. Qed. -Definition PointEncoding : canonical encoding of E.point as (word b) := - (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding sign_bit - (@sign_bit_zero _ prime_q two_lt_q _ b_valid) (@sign_bit_opp _ prime_q two_lt_q _ b_valid)). - -Definition H : forall n : nat, word n -> word (b + b). Admitted. -Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) -Definition B_nonzero : B <> E.zero. Admitted. -Definition l_order_B : (l * B)%E = E.zero. Admitted. - -Local Instance ed25519params : EdDSAParams := { - E := curve25519params; - b := b; - H := H; - c := c; - n := n; - B := B; - l := l; - FqEncoding := FqEncoding; - FlEncoding := FlEncoding; - PointEncoding := PointEncoding; - - b_valid := b_valid; - c_valid := c_valid; - n_ge_c := n_ge_c; - n_le_b := n_le_b; - B_not_identity := B_nonzero; - l_prime := prime_l; - l_odd := l_odd; - l_order_B := l_order_B -}. - -Definition ed25519_verify - : forall (pubkey:word b) (len:nat) (msg:word len) (sig:word (b+b)), bool - := @verify ed25519params.
\ No newline at end of file +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 diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v deleted file mode 100644 index 29e359baa..000000000 --- a/src/Spec/PointEncoding.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Coq.Numbers.Natural.Peano.NPeano. -Require Crypto.Encoding.EncodingTheorems. -Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Bedrock.Word. -Require Crypto.Tactics.VerdiTactics. -Require Crypto.Encoding.PointEncodingPre. -Obligation Tactic := eauto; exact PointEncodingPre.point_encoding_canonical. - -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Spec.ModularArithmetic. - -Local Open Scope F_scope. - -Section PointEncoding. - Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} - {bound_check : (BinInt.Z.to_nat q < NPeano.Nat.pow 2 sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} - {sqrt_minus1_valid : (@ZToField q 2 ^ BinInt.Z.to_N (q / 4)) ^ 2 = opp 1} - {FqEncoding : canonical encoding of (F q) as (Word.word sz)} - {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} - {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. - - Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in - Word.WS (sign_bit x) (enc y). - - Program Definition point_dec_with_spec : - {point_dec : Word.word (S sz) -> option E.point - | forall w x, point_dec w = Some x -> (point_enc x = w) - } := @PointEncodingPre.point_dec _ _ _ sign_bit. - Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). - - Global Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := { - enc := point_enc; - dec := point_dec; - encoding_valid := @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp; - encoding_canonical := PointEncodingPre.point_encoding_canonical - }. -End PointEncoding.
\ No newline at end of file |