diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-02-21 18:01:18 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | f5c6a57c1453249aac448a33ac3443e45a0d3222 (patch) | |
tree | 72919ee54472c746feab4b51898095ae5caad768 /src | |
parent | c1c764ead6291e25f6da3508f1ae2b46c1e574d4 (diff) |
rewrite ExtendedCoordinates, fix Ed25519
Diffstat (limited to 'src')
-rw-r--r-- | src/Algebra/Group.v | 7 | ||||
-rw-r--r-- | src/Algebra/IntegralDomain.v | 4 | ||||
-rw-r--r-- | src/Algebra/Ring.v | 47 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 52 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 310 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 11 |
6 files changed, 148 insertions, 283 deletions
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 7f580380f..c1c514171 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -115,10 +115,11 @@ Section Homomorphism_rev. {phi'_inv : forall a, phi' (inv a) = INV (phi' a)} {phi'_id : phi' id = ID}. - Local Instance group_from_redundant_representation - : @group H eq op id inv. + Lemma group_from_redundant_representation + : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'. Proof. repeat match goal with + | [ H : _/\_ |- _ ] => destruct H; try clear H | [ H : group |- _ ] => destruct H; try clear H | [ H : monoid |- _ ] => destruct H; try clear H | [ H : is_associative |- _ ] => destruct H; try clear H @@ -132,7 +133,7 @@ Section Homomorphism_rev. | [ H : eq _ _ |- _ ] => apply phi'_eq in H | [ |- eq _ _ ] => apply phi'_eq | [ H : EQ _ _ |- _ ] => rewrite H - | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id by reflexivity + | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity | _ => solve [ eauto ] end. diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 066886e83..8110ad5cd 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -19,7 +19,6 @@ Module IntegralDomain. Module _LargeCharacteristicReflective. Section ReflectiveNsatzSideConditionProver. Import BinInt BinNat BinPos. - Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted. Context {R eq zero one opp add sub mul} {ring:@Algebra.ring R eq zero one opp add sub mul} {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}. @@ -50,8 +49,9 @@ Module IntegralDomain. Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c. Proof. + Set Printing All. induction c; simpl CtoZ; simpl denote; - repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity. + repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity. Qed. (* TODO: move *) diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index b69e9b191..f39d730f2 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -135,15 +135,46 @@ Section Homomorphism. Qed. End Homomorphism. +(* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *) Ltac push_homomorphism phi := - let H := constr:(_:is_homomorphism(phi:=phi)) in - repeat rewrite - ?(homomorphism_zero( phi_homom:=H)), - ?(homomorphism_one(is_homomorphism:=H)), - ?(homomorphism_add( phi_homom:=H)), - ?(homomorphism_opp( phi_homom:=H)), - ?(homomorphism_sub( phi_homom:=H)), - ?(homomorphism_mul(is_homomorphism:=H)). + let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in + pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_0; + pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_1; + pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_p; + pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_o; + pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_s; + pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H) + as _push_homomrphism_m; + (rewrite_strat bottomup (terms _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m)); + clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m. + +Ltac pull_homomorphism phi := + let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in + pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_0; + pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_1; + pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_p; + pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_o; + pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_s; + pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H) + as _pull_homomrphism_m; + symmetry in _pull_homomrphism_0; + symmetry in _pull_homomrphism_1; + symmetry in _pull_homomrphism_p; + symmetry in _pull_homomrphism_o; + symmetry in _pull_homomrphism_s; + symmetry in _pull_homomrphism_m; + (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m)); + clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m. Lemma isomorphism_to_subring_ring {T EQ ZERO ONE OPP ADD SUB MUL} diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 42c394f07..32303a7bd 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -126,54 +126,11 @@ Module E. F Feq Fone Fadd Fmul KtoF}. Context {HisoF:forall x, Feq (KtoF (FtoK x)) x}. Context {Ka} {Ha:Keq (FtoK Fa) Ka} {Kd} {Hd:Keq (FtoK Fd) Kd}. - Print Field. - - (* for Ring *) - Ltac push_homomorphism phi := - let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in - pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_0; - pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_1; - pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_p; - pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_o; - pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_s; - pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H) - as _push_homomrphism_m; - (rewrite_strat bottomup (terms _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m)); - clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m. - - (* for Ring *) - Ltac pull_homomorphism phi := - let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in - pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_0; - pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_1; - pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_p; - pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_o; - pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_s; - pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H) - as _pull_homomrphism_m; - symmetry in _pull_homomrphism_0; - symmetry in _pull_homomrphism_1; - symmetry in _pull_homomrphism_p; - symmetry in _pull_homomrphism_o; - symmetry in _pull_homomrphism_s; - symmetry in _pull_homomrphism_m; - (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m)); - clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m. Lemma nonzero_Ka : ~ Keq Ka Kzero. Proof. rewrite <-Ha. - pull_homomorphism FtoK. + Ring.pull_homomorphism FtoK. intro X. eapply (Monoid.is_homomorphism_phi_proper(phi:=KtoF)) in X. rewrite 2HisoF in X. @@ -183,14 +140,14 @@ Module E. Lemma square_Ka : exists sqrt_a, Keq (Kmul sqrt_a sqrt_a) Ka. Proof. destruct square_a as [sqrt_a]. exists (FtoK sqrt_a). - pull_homomorphism FtoK. rewrite <-Ha. + Ring.pull_homomorphism FtoK. rewrite <-Ha. eapply Monoid.is_homomorphism_phi_proper; assumption. Qed. Lemma nonsquare_Kd : forall x, not (Keq (Kmul x x) Kd). Proof. intros x X. apply (nonsquare_d (KtoF x)). - pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF. + Ring.pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF. reflexivity. Qed. @@ -211,7 +168,6 @@ Module E. Local Notation KzeroP := (E.zero(nonzero_a:=nonzero_Ka)(d:=Kd)). Local Notation FaddP := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). Local Notation KaddP := (E.add(nonzero_a:=nonzero_Ka)(square_a:=square_Ka)(nonsquare_d:=nonsquare_Kd)). - Check KaddP. Obligation Tactic := idtac. Program Definition point_phi (P:Fpoint) : Kpoint := exist _ ( @@ -246,7 +202,7 @@ Module E. | _ => rewrite !(homomorphism_div(phi:=FtoK)) by assumption | _ => rewrite !Ha | _ => rewrite !Hd - | _ => push_homomorphism FtoK + | _ => Ring.push_homomorphism FtoK | |- _ ?x ?x => reflexivity | _ => eapply Monoid.is_homomorphism_phi_proper; assumption end. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 263884419..b2dbbc73d 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,35 +1,41 @@ -Require Export Crypto.Spec.CompleteEdwardsCurve. +Require Import Coq.Classes.Morphisms. + +Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Algebra Crypto.Algebra. -Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Coq.Classes.Morphisms. -Require Import Coq.Relations.Relation_Definitions. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Notations. -Require Export Crypto.Util.FixCoqMistakes. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings. +Require Export Crypto.Util.FixCoqMistakes Crypto.Util.Tactics. Module Extended. Section ExtendedCoordinates. - Import Group Ring Field. - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {prm:@E.twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul a d} + {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). + + Context {a d: F} + {nonzero_a : a <> 0} + {square_a : exists sqrt_a, sqrt_a^2 = a} + {nonsquare_d : forall x, x^2 <> d}. Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). - Local Notation onCurve := (@E.onCurve F Feq Fone Fadd Fmul a d) (only parsing). + Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). (** [Extended.point] represents a point on an elliptic curve using extended projective - * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) - Definition point := { P | let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y }. + * Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *) + Definition point := { P | let '(X,Y,Z,T) := P in + a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2 + /\ X * Y = Z * T + /\ Z <> 0 }. Definition coordinates (P:point) : F*F*F*F := proj1_sig P. + Definition eq (P1 P2:point) := + let '(X1, Y1, Z1, _) := coordinates P1 in + let '(X2, Y2, Z2, _) := coordinates P2 in + Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2. Ltac t_step := match goal with @@ -39,17 +45,21 @@ Module Extended. | _ => progress destruct_head' @E.point | _ => progress destruct_head' point | _ => progress destruct_head' and - | _ => E._gather_nonzeros - | _ => progress cbv [CompleteEdwardsCurve.E.eq E.onCurve E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig E.onCurve] in * + | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in * | |- _ /\ _ => split | |- _ <-> _ => split - | _ => rewrite <-!(field_div_definition(field:=field)) - | _ => solve [fsatz] end. - Ltac t := repeat t_step. + Ltac t := repeat t_step; Field.fsatz. + + Global Instance Equivalence_eq : Equivalence eq. + Proof. split; repeat intro; t. Qed. + Global Instance DecidableRel_eq : Decidable.DecidableRel eq. + Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined. Program Definition from_twisted (P:Epoint) : point := let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy). Next Obligation. t. Qed. + Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. + Proof. cbv [from_twisted]; t. Qed. Program Definition to_twisted (P:point) : Epoint := let XYZT := coordinates P in let T := snd XYZT in @@ -58,211 +68,71 @@ Module Extended. let X := fst XY in let iZ := Finv Z in ((X*iZ), (Y*iZ)). Next Obligation. t. Qed. + Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. + Proof. cbv [to_twisted]; t. Qed. - Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). - - Definition eq_noinv (P1 P2:point) := - let '(X1, Y1, Z1, _) := coordinates P1 in - let '(X2, Y2, Z2, _) := coordinates P2 in - Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2. - - Lemma eq_noinv_eq P Q : eq P Q <-> eq_noinv P Q. - Proof. cbv [eq_noinv eq to_twisted from_twisted]; t. Qed. - Global Instance DecidableRel_eq_noinv : Decidable.DecidableRel eq_noinv. - Proof. - intros P Q. - destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; simpl; exact _. - Defined. - Global Instance DecidableRel_eq : Decidable.DecidableRel eq. - Proof. - intros ? ?. - eapply @Decidable_iff_to_flip_impl; [eapply eq_noinv_eq | exact _]. - Defined. - - Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; cbv [eq] in *; t. Qed. - Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. cbv [eq]; t. Qed. - Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. cbv [eq to_twisted]; t. Qed. Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. Proof. cbv [to_twisted from_twisted]; t. Qed. + Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P. + Proof. cbv [to_twisted from_twisted]; t. Qed. - Section Proper. - Global Instance point_Proper : Proper (fieldwise (n:=4) Feq ==> iff) - (fun P => let '(X,Y,Z,T) := P in onCurve(X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y). - Proof. repeat intro; cbv [tuple tuple' fieldwise fieldwise'] in *; t. Qed. - Global Instance point_Proper_impl - : Proper (fieldwise (n:=4) Feq ==> Basics.impl) - (fun P => let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y). - Proof. intros A B H H'; apply (@point_Proper A B H); assumption. Qed. - Global Instance point_Proper_flip_impl - : Proper (fieldwise (n:=4) Feq ==> Basics.flip Basics.impl) - (fun P => let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y). - Proof. intros A B H H'; apply (@point_Proper A B H); assumption. Qed. - End Proper. - - Section TwistMinus1. - Context {a_eq_minus1 : a = Fopp 1}. - Context {twice_d:F} {Htwice_d:twice_d = d + d}. - (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) - Section generic. (* TODO(jgross) what is this section? *) - Context (F4 : Type) - (pair4 : F -> F -> F -> F -> F4) - (let_in : F -> (F -> F4) -> F4). - Local Notation "'slet' x := y 'in' z" := (let_in y (fun x => z)). - Definition add_coordinates_gen P1 P2 : F4 := - let '(X1, Y1, Z1, T1) := P1 in - let '(X2, Y2, Z2, T2) := P2 in - slet A := (Y1-X1)*(Y2-X2) in - slet B := (Y1+X1)*(Y2+X2) in - slet C := T1*twice_d*T2 in - slet D := Z1*(Z2+Z2) in - slet E := B-A in - slet F := D-C in - slet G := D+C in - slet H := B+A in - slet X3 := E*F in - slet Y3 := G*H in - slet T3 := E*H in - slet Z3 := F*G in - pair4 X3 Y3 Z3 T3. - End generic. - Definition add_coordinates P1 P2 : F*F*F*F := - Eval cbv beta delta [add_coordinates_gen] in - @add_coordinates_gen - (F*F*F*F) - (fun X3 Y3 Z3 T3 => (X3, Y3, Z3, T3)) - (fun x f => let y := x in f y) - P1 P2. - - Lemma add_coordinates_correct (P Q:point) : - let '(X,Y,Z,T) := add_coordinates (coordinates P) (coordinates Q) in - let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in - (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z). - Proof. cbv [E.add add_coordinates to_twisted] in *. t. Qed. - - Context {add_coordinates_opt} - {add_coordinates_opt_correct - : forall P1 P2, fieldwise (n:=4) Feq (add_coordinates_opt P1 P2) (add_coordinates P1 P2)}. + Program Definition zero : point := (0, 1, 1, 0). + Next Obligation. t. Qed. - Axiom admit : forall {T}, T. - Obligation Tactic := idtac. - Program Definition add_unopt (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q). - Next Obligation. - intros P Q. - pose proof (add_coordinates_correct P Q) as Hrep. - destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. - cbv; cbv in Hrep; destruct Hrep as [HA HB]; cbv in HP; cbv in HQ. - rewrite <-!HA, <-!HB; clear HA HB; repeat split; intros. - all: try ( - goal_to_field_equality field; - inequalities_to_inverse_equations field; - divisions_to_inverses field; - inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit)))); - IntegralDomain.nsatz). - (* TODO: in the onCurve proof for tw coordinate addition we get nonzero-denominator hypotheses from the definition itself. here the definition is not available, but we still need them... *) - exact admit. - Qed. + Program Definition opp P : point := + match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end. + Next Obligation. t. Qed. - Program Definition add (P Q:point) : point := add_coordinates_opt (coordinates P) (coordinates Q). + Section TwistMinusOne. + Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}. + Program Definition m1add + (P1 P2:point) : point := + match coordinates P1, coordinates P2 return F*F*F*F with + (X1, Y1, Z1, T1), (X2, Y2, Z2, T2) => + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) in + let C := T1*twice_d*T2 in + let D := Z1*(Z2+Z2) in + let E := B-A in + let F := D-C in + let G := D+C in + let H := B+A in + let X3 := E*F in + let Y3 := G*H in + let T3 := E*H in + let Z3 := F*G in + (X3, Y3, Z3, T3) + end. + Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed. + + Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : group /\ _ /\ _ := + @Group.group_from_redundant_representation + _ _ _ _ _ + ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a') + (nonsquare_d:=nonsquare_d')).(abelian_group_group)) + _ + eq + m1add + zero + opp + from_twisted + to_twisted + to_twisted_from_twisted + _ _ _ _. + Next Obligation. cbv [to_twisted]. t. Qed. Next Obligation. - intros; eapply point_Proper_flip_impl; - [ apply add_coordinates_opt_correct - | exact (proj2_sig (add_unopt P Q)) ]. - Qed. - Local Hint Unfold add : bash. - - Lemma to_twisted_add_unopt P Q : E.eq (to_twisted (add_unopt P Q)) (E.add (to_twisted P) (to_twisted Q)). - Proof. - clear add_coordinates_opt add_coordinates_opt_correct. - pose proof (add_coordinates_correct P Q) as Hrep. - destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. - cbv in *. - destruct Hrep as [HA HB]. - split; - goal_to_field_equality field; - inequalities_to_inverse_equations field; - divisions_to_inverses field; - (* and now we need the nonzeros here too *) - inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit)))); - IntegralDomain.nsatz. - Qed. - - Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)). - Proof. - rewrite <- to_twisted_add_unopt. - { pose proof (add_coordinates_opt_correct (coordinates P) (coordinates Q)). - cbv [add add_unopt]. - do 2 match goal with - | [ |- context[exist _ ?x ?p] ] - => first [ is_var p; fail 1 - | generalize p; cbv zeta; generalize dependent x ] - end. - clear add_coordinates_opt add_coordinates_opt_correct. - cbv [to_twisted coordinates proj1_sig E.eq E.coordinates fst snd] in *. - repeat match goal with - | _ => intro - | [ H : prod _ _ |- _ ] => destruct H - | [ H : and _ _ |- _ ] => destruct H - | _ => progress simpl in * - | [ |- and _ _ ] => split - | [ H : ?x = ?y |- context[?x] ] => is_var x; rewrite H - | _ => reflexivity - end. admit. } - Admitted. (* TODO: FIXME *) - - Global Instance Proper_add : Proper (eq==>eq==>eq) add. - Proof. - unfold eq. intros x y H x0 y0 H0. - transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity. - Qed. - - Lemma homomorphism_to_twisted : @Monoid.is_homomorphism point eq add Epoint E.eq E.add to_twisted. - Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed. - - Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)). - Proof. - pose proof (to_twisted_add (from_twisted P) (from_twisted Q)). - unfold eq; rewrite !to_twisted_from_twisted in *. - symmetry; assumption. - Qed. - - Lemma homomorphism_from_twisted : @Monoid.is_homomorphism Epoint E.eq E.add point eq add from_twisted. - Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed. - - Definition zero : point := from_twisted E.zero. - Definition opp P : point := from_twisted (E.opp (to_twisted P)). - Lemma extended_group : @group point eq add zero opp. - Proof. - eapply @isomorphism_to_subgroup_group; eauto with typeclass_instances core. - - apply DecidableRel_eq. - - unfold opp. repeat intro. match goal with [H:_|-_] => rewrite H; reflexivity end. - - intros. apply to_twisted_add. - - unfold opp; intros; rewrite to_twisted_from_twisted; reflexivity. - - unfold zero; intros; rewrite to_twisted_from_twisted; reflexivity. - Qed. - End TwistMinus1. + match goal with + | |- context[E.add ?P ?Q] => + unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)) + end. cbv [to_twisted m1add]. t. Qed. + Next Obligation. cbv [to_twisted opp]. t. Qed. + Next Obligation. cbv [to_twisted zero]. t. Qed. + Global Instance group x y z + : group := proj1 (_group_proof x y z). + Global Instance homomorphism_from_twisted x y z : + Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)). + Global Instance homomorphism_to_twisted x y z : + Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)). + End TwistMinusOne. End ExtendedCoordinates. - - Lemma add_coordinates_respectful_hetero - F Fadd Fsub Fmul twice_d P Q - F' Fadd' Fsub' Fmul' twice_d' P' Q' - (R : F -> F' -> Prop) - (Hadd : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fadd x y) (Fadd' x' y')) - (Hsub : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fsub x y) (Fsub' x' y')) - (Hmul : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fmul x y) (Fmul' x' y')) - (Htwice_d : R twice_d twice_d') - (HP : Tuple.fieldwise (n:=4) R P P') - (HQ : Tuple.fieldwise (n:=4) R Q Q') - : Tuple.fieldwise - (n:=4) R - (@add_coordinates F Fadd Fsub Fmul twice_d P Q) - (@add_coordinates F' Fadd' Fsub' Fmul' twice_d' P' Q'). - Proof. - repeat match goal with - | [ H : and _ _ |- _ ] => destruct H - | [ H : prod _ _ |- _ ] => destruct H - | _ => progress unfold add_coordinates, fieldwise, fieldwise', fst, snd, tuple, tuple' in * - | [ |- and _ _ ] => split - | _ => solve [ auto ] - end. - Qed. End Extended. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 45179a81e..02f59c9e5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -83,6 +83,13 @@ Section Ed25519. (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). Proof. split; try exact _. - timeout 1 match goal with H:?P |- ?P => idtac end. - Admitted. + (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) + (* timeout 1 match goal with H:?P |- ?P => idtac end. *) + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + Crypto.Util.Decidable.vm_decide. + exact l_order_B. + Qed. End Ed25519. |