diff options
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 461 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 14 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 44 | ||||
-rw-r--r-- | src/EdDSAProofs.v | 57 | ||||
-rw-r--r-- | src/Encoding/PointEncodingPre.v | 46 | ||||
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 67 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 6 | ||||
-rw-r--r-- | src/Spec/EdDSA.v | 17 | ||||
-rw-r--r-- | src/Spec/PointEncoding.v | 9 | ||||
-rw-r--r-- | src/Specific/Ed25519.v | 54 |
10 files changed, 408 insertions, 367 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 2fdaff4a5..f70479c3a 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -7,187 +7,294 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. -Section CompleteEdwardsCurveTheorems. - Context {prm:TwistedEdwardsParams}. - Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *) - Existing Instance prime_q. +Module E. + Section CompleteEdwardsCurveTheorems. + Context {prm:TwistedEdwardsParams}. + Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *) + Existing Instance prime_q. + + Add Field Ffield_p' : (@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]). + + Add Field Ffield_notConstant : (OpaqueFieldTheory q) + (constants [notConstant]). + + Ltac clear_prm := + generalize dependent a; intro a; intros; + generalize dependent d; intro d; intros; + generalize dependent prime_q; intro prime_q; intros; + generalize dependent q; intro q; intros; + clear prm. + + Lemma point_eq : forall xy1 xy2 pf1 pf2, + xy1 = xy2 -> exist E.onCurve xy1 pf1 = exist E.onCurve xy2 pf2. + Proof. + destruct xy1, xy2; intros; find_injection; intros; subst. apply f_equal. + apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) + Qed. Hint Resolve point_eq. + + Definition point_eqb (p1 p2:E.point) : bool := andb + (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2))) + (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))). + + Local Ltac t := + unfold point_eqb; + repeat match goal with + | _ => progress intros + | _ => progress simpl in * + | _ => progress subst + | [P:E.point |- _ ] => destruct P + | [x: (F q * F q)%type |- _ ] => destruct x + | [H: _ /\ _ |- _ ] => destruct H + | [H: _ |- _ ] => rewrite Bool.andb_true_iff in H + | [H: _ |- _ ] => apply F_eqb_eq in H + | _ => rewrite F_eqb_refl + end; eauto. + + Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2. + Proof. + t. + Qed. + + Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true. + Proof. + t. + Qed. + + Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2. + Proof. + intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. + apply point_eqb_complete in H0; congruence. + Qed. + + Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false. + Proof. + intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. + apply point_eqb_sound in Hneq. congruence. + Qed. + + Lemma point_eqb_refl : forall p, point_eqb p p = true. + Proof. + t. + Qed. + + Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}. + destruct (point_eqb p1 p2) eqn:H; match goal with + | [ H: _ |- _ ] => apply point_eqb_sound in H + | [ H: _ |- _ ] => apply point_eqb_neq in H + end; eauto. + Qed. + + Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false. + Proof. + intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete. + Qed. + + Ltac Edefn := unfold E.add, E.add', E.zero; intros; + repeat match goal with + | [ p : E.point |- _ ] => + let x := fresh "x" p in + let y := fresh "y" p in + let pf := fresh "pf" p in + destruct p as [[x y] pf]; unfold E.onCurve in pf + | _ => eapply point_eq, (f_equal2 pair) + | _ => eapply point_eq + end. + Lemma add_comm : forall A B, (A+B = B+A)%E. + Proof. + Edefn; apply (f_equal2 div); ring. + Qed. + + Ltac unifiedAdd_nonzero := match goal with + | [ |- (?op 1 (d * _ * _ * _ * _ * + inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F] + => let Hadd := fresh "Hadd" in + pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd; + simpl in Hadd; + match goal with + | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] => + replace other with + (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) + * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring); + auto + end + end. + + Lemma add_assoc : forall A B C, (A+(B+C) = (A+B)+C)%E. + Proof. + Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz); + pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); + pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); + cbv beta iota in *; + repeat split; field_nonzero idtac; unifiedAdd_nonzero. + Qed. + + Lemma add_0_r : forall P, (P + E.zero = P)%E. + Proof. + Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, + ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl. + Qed. - Add Field Ffield_p' : (@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]). + Lemma add_0_l : forall P, (E.zero + P)%E = P. + Proof. + intros; rewrite add_comm. apply add_0_r. + Qed. - Add Field Ffield_notConstant : (OpaqueFieldTheory q) - (constants [notConstant]). + Lemma mul_0_l : forall P, (0 * P = E.zero)%E. + Proof. + auto. + Qed. - Ltac clear_prm := - generalize dependent a; intro a; intros; - generalize dependent d; intro d; intros; - generalize dependent prime_q; intro prime_q; intros; - generalize dependent q; intro q; intros; - clear prm. + Lemma mul_S_l : forall n P, (S n * P)%E = (P + n * P)%E. + Proof. + auto. + Qed. - Lemma point_eq' : forall xy1 xy2 pf1 pf2, - xy1 = xy2 -> exist onCurve xy1 pf1 = exist onCurve xy2 pf2. - Proof. - destruct xy1, xy2; intros; find_injection; intros; subst. apply f_equal. - apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) - Qed. + Lemma mul_add_l : forall a b P, ((a + b)%nat * P)%E = E.add (a * P)%E (b * P)%E. + Proof. + induction a; intros; rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?mul_0_l, ?add_0_l, ?mul_S_, ?IHa, ?add_assoc; auto. + Qed. - Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2, - mkPoint p1 pf1 = mkPoint p2 pf2. - Proof. - eauto using point_eq'. - Qed. - Hint Resolve point_eq' point_eq. + Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. + Proof. + induction n; intros; auto. + rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity. + Qed. - Definition point_eqb (p1 p2:point) : bool := andb - (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2))) - (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))). - - Local Ltac t := - unfold point_eqb; - repeat match goal with - | _ => progress intros - | _ => progress simpl in * - | _ => progress subst - | [P:point |- _ ] => destruct P - | [x: (F q * F q)%type |- _ ] => destruct x - | [H: _ /\ _ |- _ ] => destruct H - | [H: _ |- _ ] => rewrite Bool.andb_true_iff in H - | [H: _ |- _ ] => apply F_eqb_eq in H - | _ => rewrite F_eqb_refl - end; eauto. - - Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2. - Proof. - t. - Qed. - - Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true. - Proof. - t. - Qed. - - Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2. - Proof. - intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. - apply point_eqb_complete in H0; congruence. - Qed. - - Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false. - Proof. - intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. - apply point_eqb_sound in Hneq. congruence. - Qed. - - Lemma point_eqb_refl : forall p, point_eqb p p = true. - Proof. - t. - Qed. - - Definition point_eq_dec (p1 p2:point) : {p1 = p2} + {p1 <> p2}. - destruct (point_eqb p1 p2) eqn:H; match goal with - | [ H: _ |- _ ] => apply point_eqb_sound in H - | [ H: _ |- _ ] => apply point_eqb_neq in H - end; eauto. - Qed. - - Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false. - Proof. - intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete. - Qed. - - Ltac Edefn := unfold unifiedAdd, unifiedAdd', zero; intros; - repeat match goal with - | [ p : point |- _ ] => - let x := fresh "x" p in - let y := fresh "y" p in - let pf := fresh "pf" p in - destruct p as [[x y] pf]; unfold onCurve in pf - | _ => eapply point_eq, (f_equal2 pair) - | _ => eapply point_eq - end. - Lemma twistedAddComm : forall A B, (A+B = B+A)%E. - Proof. - Edefn; apply (f_equal2 div); ring. - Qed. - - Ltac unifiedAdd_nonzero := match goal with - | [ |- (?op 1 (d * _ * _ * _ * _ * - inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F] - => let Hadd := fresh "Hadd" in - pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd; - simpl in Hadd; - match goal with - | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] => - replace other with - (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) - * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring); - auto - end - end. - - Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E. - Proof. - (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *) - Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz); - pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); - pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); - cbv beta iota in *; - repeat split; field_nonzero idtac; unifiedAdd_nonzero. - Qed. - - Lemma zeroIsIdentity : forall P, (P + zero = P)%E. - Proof. - Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, - ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl. - Qed. - - (* solve for x ^ 2 *) - Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F. - - Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F. - intros ? eq_zero. - pose proof prime_q. - destruct square_a as [sqrt_a sqrt_a_id]. - rewrite <- sqrt_a_id in eq_zero. - destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero]. - + pose proof (nonsquare_d sqrt_d); auto. - + subst. - rewrite Fq_pow_zero in sqrt_a_id by congruence. - auto using nonzero_a. - Qed. - - Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F. - Proof. - intros y eq_zero. - pose proof prime_q. - eapply F_minus_swap in eq_zero. - eauto using (d_y2_a_nonzero y). - Qed. - - Lemma solve_correct : forall x y, onCurve (x, y) <-> - (x ^ 2 = solve_for_x2 y)%F. - Proof. - split. - + intro onCurve_x_y. + Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. + Proof. + induction m; rewrite ?mul_S_l, ?add_0_l; auto. + Qed. + + (* solve for x ^ 2 *) + Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F. + + Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F. + intros ? eq_zero. pose proof prime_q. - unfold onCurve in onCurve_x_y. - eapply F_div_mul; auto using (d_y2_a_nonzero y). - replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring. - rewrite F_sub_add_swap. - replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring. - rewrite onCurve_x_y. - ring. - + intro x2_eq. - unfold onCurve, solve_for_x2 in *. - rewrite x2_eq. - field. - auto using d_y2_a_nonzero. - Qed. - -End CompleteEdwardsCurveTheorems. + destruct square_a as [sqrt_a sqrt_a_id]. + rewrite <- sqrt_a_id in eq_zero. + destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero]. + + pose proof (nonsquare_d sqrt_d); auto. + + subst. + rewrite Fq_pow_zero in sqrt_a_id by congruence. + auto using nonzero_a. + Qed. + + Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F. + Proof. + intros y eq_zero. + pose proof prime_q. + eapply F_minus_swap in eq_zero. + eauto using (d_y2_a_nonzero y). + Qed. + + Lemma solve_correct : forall x y, E.onCurve (x, y) <-> + (x ^ 2 = solve_for_x2 y)%F. + Proof. + split. + + intro onCurve_x_y. + pose proof prime_q. + unfold E.onCurve in onCurve_x_y. + eapply F_div_mul; auto using (d_y2_a_nonzero y). + replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring. + rewrite F_sub_add_swap. + replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring. + rewrite onCurve_x_y. + ring. + + intro x2_eq. + unfold E.onCurve, solve_for_x2 in *. + rewrite x2_eq. + field. + auto using d_y2_a_nonzero. + Qed. + + + Program Definition opp (P:E.point) : E.point := let '(x, y) := proj1_sig P in (opp x, y). + Next Obligation. Proof. + pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. + rewrite F_square_opp; trivial. + Qed. + + Definition sub P Q := (P + opp Q)%E. + + Lemma opp_zero : opp E.zero = E.zero. + Proof. + pose proof @F_opp_0. + unfold opp, E.zero; eapply point_eq; congruence. + Qed. + + Lemma add_opp_r : forall P, (P + opp P = E.zero)%E. + Proof. + unfold opp; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]); + rewrite <-?@F_pow_2_r in *; + pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); + pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); + field_nonzero idtac. + Qed. + + Lemma add_opp_l : forall P, (opp P + P = E.zero)%E. + Proof. + intros. rewrite add_comm. eapply add_opp_r. + Qed. + + Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E. + Proof. + intros. + assert ((B + A) + opp A = (C + A) + opp A)%E as Hc by congruence. + rewrite <-!add_assoc, !add_opp_r, !add_0_r in Hc; exact Hc. + Qed. + + Lemma add_cancel_l : forall A B C, (A+B = A+C -> B = C)%E. + Proof. + intros. + rewrite (add_comm A C) in H. + rewrite (add_comm A B) in H. + eauto using add_cancel_r. + Qed. + + Lemma shuffle_eq_add_opp : forall P Q R, (P + Q = R <-> Q = opp P + R)%E. + Proof. + split; intros. + { assert (opp P + (P + Q) = opp P + R)%E as Hc by congruence. + rewrite add_assoc, add_opp_l, add_comm, add_0_r in Hc; exact Hc. } + { subst. rewrite add_assoc, add_opp_r, add_comm, add_0_r; reflexivity. } + Qed. + + Lemma opp_opp : forall P, opp (opp P) = P. + Proof. + intros. + pose proof (add_opp_r P%E) as H. + rewrite add_comm in H. + rewrite shuffle_eq_add_opp in H. + rewrite add_0_r in H. + congruence. + Qed. + + Lemma opp_add : forall P Q, opp (P + Q)%E = (opp P + opp Q)%E. + Proof. + intros. + pose proof (add_opp_r (P+Q)%E) as H. + rewrite <-!add_assoc in H. + rewrite add_comm in H. + rewrite <-!add_assoc in H. + rewrite shuffle_eq_add_opp in H. + rewrite add_comm in H. + rewrite shuffle_eq_add_opp in H. + rewrite add_0_r in H. + assumption. + Qed. + + Lemma opp_mul : forall n P, opp (E.mul n P) = E.mul n (opp P). + Proof. + pose proof opp_add; pose proof opp_zero. + induction n; simpl; intros; congruence. + Qed. + End CompleteEdwardsCurveTheorems. +End E. +Infix "-" := E.sub : E_scope.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index d58a06c55..50027349d 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -5,26 +5,26 @@ Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. - Definition doubleAndAdd (bound n : nat) (P : point) : point := - iter_op unifiedAdd zero N.testbit_nat (N.of_nat n) P bound. + 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, scalarMult (n + n) P = scalarMult n (P + P)%E. + 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 twistedAddAssoc. + rewrite E.add_assoc. f_equal; auto. Qed. Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound -> - scalarMult n P = doubleAndAdd bound n P. + 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 twistedAddAssoc - || rewrite twistedAddComm; apply zeroIsIdentity). + 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/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index a9fbf5e40..5e4fe0b0b 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -45,7 +45,7 @@ Section ExtendedCoordinates. Local Notation "P '~=' rP" := (rep P rP) (at level 70). Ltac unfoldExtended := - repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros); + repeat progress (autounfold; unfold E.onCurve, E.add, E.add', rep in *; intros); repeat match goal with | [ p : (F q*F q)%type |- _ ] => let x := fresh "x" p in @@ -83,14 +83,14 @@ Section ExtendedCoordinates. solveExtended. Qed. - Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ onCurve (extendedToTwisted P) }. + Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }. - Program Definition mkExtendedPoint : point -> extendedPoint := twistedToExtended. + Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended. Next Obligation. destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. Qed. - Program Definition unExtendedPoint : extendedPoint -> point := extendedToTwisted. + Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted. Next Obligation. destruct x; simpl; intuition. Qed. @@ -103,7 +103,7 @@ Section ExtendedCoordinates. Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P. Proof. - destruct P; eapply point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. + destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. Qed. Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint. @@ -135,12 +135,12 @@ Section ExtendedCoordinates. let T3 := E*H in let Z3 := F*G in (X3, Y3, Z3, T3). - Local Hint Unfold unifiedAdd. + Local Hint Unfold E.add. Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). - Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ). + Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ). Proof. intros P Q rP rQ HoP HoQ HrP HrQ. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). @@ -152,9 +152,9 @@ Section ExtendedCoordinates. field_nonzero tnz. Qed. - Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q). + Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q). Proof. - intros; pose proof (proj2_sig (unifiedAdd (mkPoint _ H) (mkPoint _ H0))); eauto. + intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto. Qed. Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'. @@ -167,9 +167,9 @@ Section ExtendedCoordinates. eauto using unifiedAdd'_onCurve. Qed. - Lemma unifiedAddM1_rep : forall P Q, unifiedAdd (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). + Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). Proof. - destruct P, Q; unfold unExtendedPoint, unifiedAdd, unifiedAddM1; eapply point_eq; simpl in *; intuition. + destruct P, Q; unfold unExtendedPoint, E.add, unifiedAddM1; eapply E.point_eq; simpl in *; intuition. pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0)); destruct (unifiedAddM1' x x0); unfold rep in *; intuition. @@ -180,23 +180,23 @@ Section ExtendedCoordinates. repeat (econstructor || intro). repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq. rewrite <-!unifiedAddM1_rep. - destruct x, y, x0, y0; simpl in *; eapply point_eq; congruence. + destruct x, y, x0, y0; simpl in *; eapply E.point_eq; congruence. Qed. - Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint zero) === P. + Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. Qed. - Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint zero) P === P. + Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint E.zero) P === P. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, twistedAddComm, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + rewrite <-!unifiedAddM1_rep, E.add_comm, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. Qed. Lemma unifiedAddM1_assoc : forall a b c, unifiedAddM1 a (unifiedAddM1 b c) === unifiedAddM1 (unifiedAddM1 a b) c. Proof. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto. + rewrite <-!unifiedAddM1_rep, E.add_assoc; auto. Qed. Lemma testbit_conversion_identity : forall x i, N.testbit_nat x i = N.testbit_nat ((fun a => a) x) i. @@ -204,14 +204,14 @@ Section ExtendedCoordinates. trivial. Qed. - Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero) N.testbit_nat. + Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint E.zero) N.testbit_nat. Definition scalarMultM1_spec := - iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l + iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint E.zero) unifiedAddM1_0_l N.testbit_nat (fun x => x) testbit_conversion_identity. - Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = scalarMult n (unExtendedPoint P). + Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = E.mul n (unExtendedPoint P). intros; rewrite scalarMultM1_spec, Nat2N.id; auto. induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]. - unfold scalarMult; fold scalarMult. + unfold E.mul; fold E.mul. rewrite <-IHn, unifiedAddM1_rep; auto. Qed. diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v index 83467bf6d..dba71b49c 100644 --- a/src/EdDSAProofs.v +++ b/src/EdDSAProofs.v @@ -37,7 +37,7 @@ Section EdDSAProofs. 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 : point := (r * B)%E in (* commitment to 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. @@ -46,62 +46,21 @@ Section EdDSAProofs. Qed. Hint Rewrite decode_sign_split2. - Lemma zero_times : forall P, (0 * P = zero)%E. - Proof. - auto. - Qed. - - Lemma zero_plus : forall P, (zero + P = P)%E. - Proof. - intros; rewrite twistedAddComm; apply zeroIsIdentity. - Qed. - - Lemma times_S : forall n m, S n * m = m + n * m. - Proof. - auto. - Qed. - - Lemma times_S_nat : forall n m, (S n * m = m + n * m)%nat. - Proof. - auto. - Qed. - - Hint Rewrite plus_O_n plus_Sn_m times_S times_S_nat. - Hint Rewrite zeroIsIdentity zero_times zero_plus twistedAddAssoc. - - Lemma scalarMult_distr : forall n0 m, ((n0 + m)%nat * B)%E = unifiedAdd (n0 * B)%E (m * B)%E. - Proof. - unfold scalarMult; induction n0; arith. - Qed. - Hint Rewrite scalarMult_distr. - - Lemma scalarMult_assoc : forall (n0 m : nat), (n0 * (m * B) = (n0 * m)%nat * B)%E. - Proof. - induction n0; arith; simpl; arith. - Qed. - Hint Rewrite scalarMult_assoc. - - Lemma scalarMult_zero : forall m, (m * zero = zero)%E. - Proof. - unfold scalarMult; induction m; arith. - Qed. - Hint Rewrite scalarMult_zero. + 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 = zero)%E. + Lemma l_order_B' : forall x, (l * x * B = E.zero)%E. Proof. - intros; rewrite Mult.mult_comm. rewrite <- scalarMult_assoc. arith. - Qed. - - Hint Rewrite l_order_B'. + 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. + Qed. Hint Rewrite scalarMult_mod_l. Hint Rewrite @encoding_valid. Hint Rewrite @FieldToZ_ZToField. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 9eb5118bd..b7e907e10 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -27,12 +27,12 @@ Section PointEncoding. Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - Lemma solve_sqrt_valid : forall p, onCurve p -> - sqrt_valid (solve_for_x2 (snd p)). + 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 (solve_correct x y) in onCurve_xy. + rewrite (E.solve_correct x y) in onCurve_xy. rewrite <- onCurve_xy. unfold sqrt_valid. eapply sqrt_mod_q_valid; eauto. @@ -40,20 +40,20 @@ Section PointEncoding. Grab Existential Variables. eauto. Qed. - Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (sqrt_mod_q (solve_for_x2 y), y). + 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 solve_correct; auto. + apply E.solve_correct; auto. Qed. - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). + 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 solve_correct. + apply E.solve_correct. rewrite <- sqrt_valid_x2 at 2. ring. Qed. @@ -67,13 +67,13 @@ Section PointEncoding. 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 : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in + 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 := solve_for_x2 y in + | 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 @@ -86,7 +86,7 @@ Section PointEncoding. 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 -> onCurve p. + 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]. @@ -108,13 +108,13 @@ Section PointEncoding. Admitted. - Definition point_dec' w p : option point := + Definition point_dec' w p : option E.point := match (option_eq_dec (point_dec_coordinates sign_bit w) (Some p)) with - | left EQ => Some (mkPoint p (point_dec_coordinates_onCurve w p EQ)) + | 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 point := + 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 @@ -192,7 +192,7 @@ Section PointEncoding. 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 (solve_for_x2 f1)) 0%F) as [sqrt_0 | ?]. + + 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_0 in sqrt_0. rewrite sqrt_0 in *. @@ -268,12 +268,12 @@ Proof. congruence. Qed. -Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) -> +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 solve_correct in onCurve_x. - apply solve_correct in onCurve_x'. + 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. @@ -287,7 +287,7 @@ Qed. Lemma blah : forall x y, (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0 && sign_bit x)%bool = true. *) -Lemma point_encoding_coordinates_valid : forall p, onCurve p -> +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. @@ -297,9 +297,9 @@ Proof. unfold sqrt_valid in *. destruct p as [x y]. simpl in *. - destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition. + destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition. break_if; f_equal. - + case_eq (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0); intros eqb_0. + + case_eq (F_eqb (sqrt_mod_q (E.solve_for_x2 y)) 0); intros eqb_0. (* SearchAbout F_eqb. @@ -333,7 +333,7 @@ Proof. break_match. + f_equal. destruct p. - apply point_eq. + apply E.point_eq. reflexivity. + rewrite point_encoding_coordinates_valid in n by apply (proj2_sig p). congruence. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 8dbfdf7b9..3348be1d9 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -16,38 +16,39 @@ Class TwistedEdwardsParams := { nonsquare_d : forall x, x^2 <> d }. -Section TwistedEdwardsCurves. - Context {prm:TwistedEdwardsParams}. - - (* Twisted Edwards curves with complete addition laws. References: - * <https://eprint.iacr.org/2008/013.pdf> - * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> - * <https://eprint.iacr.org/2015/677.pdf> - *) - Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. - Definition point := { P | onCurve P}. - Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf. - - Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). +Module E. + Section TwistedEdwardsCurves. + Context {prm:TwistedEdwardsParams}. + + (* Twisted Edwards curves with complete addition laws. References: + * <https://eprint.iacr.org/2008/013.pdf> + * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> + * <https://eprint.iacr.org/2015/677.pdf> + *) + Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition point := { P | onCurve P}. + + Definition zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). + + Definition add' P1' P2' := + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). + + Definition add (P1 P2 : point) : point := + let 'exist P1' pf1 := P1 in + let 'exist P2' pf2 := P2 in + exist _ (add' P1' P2') + (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). + + Fixpoint mul (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => add P (mul n' P) + end. + End TwistedEdwardsCurves. +End E. - Definition unifiedAdd' P1' P2' := - let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - - Definition unifiedAdd (P1 P2 : point) : point := - let 'exist P1' pf1 := P1 in - let 'exist P2' pf2 := P2 in - mkPoint (unifiedAdd' P1' P2') - (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). - - Fixpoint scalarMult (n:nat) (P : point) : point := - match n with - | O => zero - | S n' => unifiedAdd P (scalarMult n' P) - end. -End TwistedEdwardsCurves. - Delimit Scope E_scope with E. -Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope.
\ No newline at end of file +Infix "+" := E.add : E_scope. +Infix "*" := E.mul : E_scope.
\ No newline at end of file diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 30892c006..6543823cb 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -145,9 +145,9 @@ Qed. Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding. 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 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; diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 8a48f4dea..80aed4a20 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -22,7 +22,7 @@ Section EdDSAParams. 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; + PointEncoding : encoding of E.point as Word.word b; H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) @@ -33,13 +33,13 @@ Section EdDSAParams. n_ge_c : n >= c; n_le_b : n <= b; - B : point; - B_not_identity : B <> zero; + B : E.point; + B_not_identity : B <> E.zero; l : nat; (* order of the subgroup of E generated by B *) l_prime : Znumtheory.prime (BinInt.Z.of_nat l); l_odd : l > 2; - l_order_B : (l*B)%E = zero; + l_order_B : (l*B)%E = E.zero; FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b }. End EdDSAParams. @@ -55,8 +55,7 @@ Section EdDSA. Notation secretkey := (Word.word b) (only parsing). Notation publickey := (Word.word b) (only parsing). Notation signature := (Word.word (b + b)) (only parsing). - Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec. - Local Infix "==" := point_eq_dec (at level 70) : E_scope . + Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope . (* TODO: proofread curveKey and definition of n *) Definition curveKey (sk:secretkey) : nat := @@ -68,7 +67,7 @@ Section EdDSA. Definition sign (A_:publickey) sk {n} (M : Word.word n) := let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : point := (r * B)%E in (* commitment to nonce *) + let R : E.point := (r * B)%E in (* commitment to nonce *) let s : nat := curveKey sk in (* secret scalar *) let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat (r + H (enc R ++ public sk ++ M) * s)) in @@ -78,8 +77,8 @@ Section EdDSA. let R_ := Word.split1 b b sig in let S_ := Word.split2 b b sig in match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => - match dec A_ : option point with None => false | Some A => - match dec R_ : option point with None => false | Some R => + match dec A_ : option E.point with None => false | Some A => + match dec R_ : option E.point with None => false | Some R => if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A then true else false end diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 38b4b4224..1d79a018d 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -23,20 +23,19 @@ Section PointEncoding. | Word.WS b _ w' => b end. - Definition point_enc (p : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in + 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 CompleteEdwardsCurve.point + {point_dec : Word.word (S sz) -> option E.point | forall w x, point_dec w = Some x -> (point_enc x = w) } := PointEncodingPre.point_dec. Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). - Instance point_encoding : encoding of CompleteEdwardsCurve.point as (Word.word (S sz)) := { + Instance point_encoding : encoding of E.point as (Word.word (S sz)) := { enc := point_enc; dec := point_dec; encoding_valid := PointEncodingPre.point_encoding_valid }. - -End PointEncoding. +End PointEncoding.
\ No newline at end of file diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index f02c24ffb..f8fb5aad7 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -87,33 +87,9 @@ Axiom decode_scalar : word b -> option N. Local Existing Instance Ed25519.FlEncoding. Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x). -Local Infix "==?" := point_eqb (at level 70) : E_scope. +Local Infix "==?" := E.point_eqb (at level 70) : E_scope. Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. -Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y). -Next Obligation. -Proof. - pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. - rewrite F_square_opp; trivial. -Qed. - -Definition point_sub P Q := (P + negate Q)%E. -Infix "-" := point_sub : E_scope. - -Lemma negate_zero : negate zero = zero. -Proof. - pose proof @F_opp_0. - unfold negate, zero; eapply point_eq'; congruence. -Qed. - -Lemma negate_add : forall P Q, negate (P + Q)%E = (negate P + negate Q)%E. Admitted. - -Lemma negate_scalarMult : forall n P, negate (scalarMult n P) = scalarMult n (negate P). -Proof. - pose proof negate_add; pose proof negate_zero. - induction n; simpl; intros; congruence. -Qed. - Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). @@ -127,13 +103,13 @@ Proof. repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial. Admitted. -Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). +Axiom negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P). Local Existing Instance PointEncoding. -Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. +Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. -Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option point => bool) - (fun S : point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). +Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool) + (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). Proof. intros. destruct (dec S_) eqn:H. @@ -146,13 +122,13 @@ Qed. Definition enc' : F q * F q -> word (S (b - 1)). Proof. intro x. - let enc' := (eval hnf in (@enc (@point curve25519params) _ _)) in + let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with | (fun _ => ?enc') => exact enc' end. Defined. -Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) +Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) := eq_refl. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. @@ -276,13 +252,13 @@ Proof. [ reflexivity | .. ] end. set_evars. - rewrite<- point_eqb_correct. - rewrite solve_for_R; unfold point_sub. - rewrite negate_scalarMult. + rewrite<- E.point_eqb_correct. + rewrite solve_for_R; unfold E.sub. + rewrite E.opp_mul. let p1 := constr:(scalarMultM1_rep eq_refl) in let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with - | |- context [(_ * negate ?P)%E] => + | |- context [(_ * E.opp ?P)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); rewrite negateExtended_correct; rewrite <-p1 @@ -336,7 +312,7 @@ Proof. reflexivity. } Unfocus. - cbv [mkExtendedPoint zero mkPoint]. + cbv [mkExtendedPoint E.zero]. unfold proj1_sig at 1 2 3 5 6 7 8. rewrite B_proj. @@ -369,7 +345,7 @@ Proof. reflexivity. } Unfocus. - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding CompleteEdwardsCurveTheorems.solve_for_x2 sqrt_mod_q]. + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. etransitivity. Focus 2. { @@ -484,8 +460,8 @@ Proof. unfold curve25519params, q. (* TODO: do we really wanna do it here? *) rewrite (rep2F_F2rep 0%F). rewrite (rep2F_F2rep 1%F). - match goal with |- context [?x] => match x with (fst (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. - match goal with |- context [?x] => match x with (snd (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. + match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. + match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. rewrite !FRepMul_correct. repeat match goal with |- appcontext [ ?E ] => match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => |