diff options
| -rw-r--r-- | src/Algebra.v | 6 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 185 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 147 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 230 | ||||
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 17 |
5 files changed, 372 insertions, 213 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index c9e535dd5..5a32989e0 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -773,7 +773,7 @@ Module Field. intros. rewrite commutative. auto using left_multiplicative_inverse. Qed. - Lemma inv_unique x ix : ix * x = one -> ix = inv x. + Lemma left_inv_unique x ix : ix * x = one -> ix = inv x. Proof. intro Hix. assert (ix*x*inv x = inv x). @@ -782,6 +782,10 @@ Module Field. intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix. apply zero_neq_one. assumption. Qed. + Definition inv_unique := left_inv_unique. + + Lemma right_inv_unique x ix : x * ix = one -> ix = inv x. + Proof. rewrite commutative. apply left_inv_unique. Qed. Lemma div_one x : div x one = x. Proof. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index c8986cee9..468255f5d 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -11,10 +11,33 @@ Require Export Crypto.Util.FixCoqMistakes. Module E. Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. + + Notation onCurve_zero := Pre.onCurve_zero. + Notation denominator_nonzero := Pre.denominator_nonzero. + Notation denominator_nonzero_x := denominator_nonzero_x. + Notation denominator_nonzero_y := Pre.denominator_nonzero_y. + Notation onCurve_add := Pre.onCurve_add. + + (* used in Theorems and Homomorphism *) + Ltac _gather_nonzeros := + match goal with + |- context[?t] => + match type of t with + ?T => + match type of T with + Prop => + let T := (eval simpl in T) in + match T with + not (_ _ _) => unique pose proof (t:T) + end + end + end + end. + Section CompleteEdwardsCurveTheorems. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {prm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d} + {prm:@twisted_edwards_params F Feq Fzero Fmul a d} {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. @@ -22,126 +45,94 @@ Module E. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). Local Notation point := (@point F Feq Fone Fadd Fmul a d). - Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2). - - Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)). - - Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q). - Infix "=" := eq : E_scope. - - Ltac destruct_points := - 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] - end. + Definition onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2). + (* TODO: remove uses of this defnition, then make it a local notation *) + Definition eq := @E.eq F Feq Fone Fadd Fmul a d. - Local Obligation Tactic := intros; destruct_points; simpl; super_nsatz. - Program Definition opp (P:point) : point := - exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. - - (* all nonzero-denominator goals here require proofs that are not - trivially implied by field axioms. Posing all such proofs at once - and then solving the nonzero-denominator goal using [super_nsatz] - is too slow because the context contains many assumed nonzero - expressions and the product of all of them is a very large - polynomial. However, we never need to use more than one - nonzero-ness assumption for a given nonzero-denominator goal, so - we can try them separately one-by-one. *) - - Ltac apply_field_nonzero H := - match goal with |- not (Feq _ 0) => idtac | _ => fail "not a nonzero goal" end; - try solve [exact H]; - let Hx := fresh "H" in - intro Hx; - apply H; - try common_denominator; - [rewrite <-Hx; ring | ..]. - - Ltac bash_step := - let addCompletePlus := constr:(edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in - let addCompleteMinus := constr:(edwardsAddCompleteMinus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in - let addOnCurve := constr:(unifiedAdd'_onCurve(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in + Ltac t_step := match goal with - | |- _ => progress intros - | [H: _ /\ _ |- _ ] => destruct H - | [H: ?a = ?b |- _ ] => is_var a; is_var b; repeat rewrite <-H in *; clear H b (* fast path *) - | |- _ => progress destruct_points - | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in * - | |- _ => split - | [H:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0] - => apply_field_nonzero (addCompletePlus _ _ _ _ H H) || - apply_field_nonzero (addCompleteMinus _ _ _ _ H H) - | [A:Feq (a*_^2+_^2) (1 + d*_^2*_^2), - B:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0] - => apply_field_nonzero (addCompletePlus _ _ _ _ A B) || - apply_field_nonzero (addCompleteMinus _ _ _ _ A B) - | [A:Feq (a*_^2+_^2) (1 + d*_^2*_^2), - B:Feq (a*_^2+_^2) (1 + d*_^2*_^2), - C:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0] - => apply_field_nonzero (addCompleteMinus _ _ _ _ A (addOnCurve (_, _) (_, _) B C)) || - apply_field_nonzero (addCompletePlus _ _ _ _ A (addOnCurve (_, _) (_, _) B C)) - | |- ?x <> 0 => let H := fresh "H" in assert (x = 1) as H by ring; rewrite H; exact one_neq_zero - | |- Feq _ _ => progress common_denominator - | |- Feq _ _ => nsatz - | |- _ => exact _ (* typeclass instances *) + | _ => exact _ + | _ => intro + | |- Equivalence _ => split + | |- abelian_group => split | |- group => split | |- monoid => split + | |- is_associative => split | |- is_commutative => split + | |- is_left_inverse => split | |- is_right_inverse => split + | |- is_left_identity => split | |- is_right_identity => split + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' prod + | _ => progress destruct_head' and + | _ => progress cbv [onCurve eq E.eq E.add E.coordinates proj1_sig] in * + (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *) + | _ => _gather_nonzeros + | _ => progress simpl in * + | |- _ /\ _ => split | |- _ <-> _ => split + | _ => solve [fsatz] end. + Ltac t := repeat t_step. - Ltac bash := repeat bash_step. + Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)). + Next Obligation. t. Qed. - Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed. - Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed. - Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. bash. Qed. - Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp). + Global Instance associative_add : is_associative(eq:=E.eq)(op:=add). Proof. - bash. + do 17 t_step. + (* + Ltac debuglevel ::= constr:(1%nat). + all: goal_to_field_equality field. + all: inequalities_to_inverses field. + all: divisions_to_inverses field. + nsatz. (* runs out of 6GB of stack space *) + *) + Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + all:repeat common_denominator_equality_inequality_all; try nsatz. + { revert H5; intro. fsatz. } + { revert H1; intro. fsatz. } + { revert H6; intro. fsatz. } + { revert H2; intro. fsatz. } Qed. + Global Instance edwards_curve_abelian_group : abelian_group (eq:=E.eq)(op:=add)(id:=zero)(inv:=opp). + Proof. t. Qed. + + Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. t. Qed. + Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul. Proof. intros n n'; repeat intro; subst n'. - induction n; (reflexivity || eapply Proper_add; eauto). + induction n; (reflexivity || eapply (_:Proper (eq==>eq==>eq) add); eauto). Qed. Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. - Proof. unfold mul; split; intros; (reflexivity || exact _). Qed. + Proof. split; intros; (reflexivity || exact _). Qed. Section PointCompression. Local Notation "x ^ 2" := (x*x). Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). - Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. + Lemma a_d_y2_nonzero y : d * y^2 - a <> 0. Proof. - intros ? eq_zero. - destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero. - destruct (dec (y=0)); [apply nonzero_a | apply nonsquare_d with (sqrt_a/y)]; super_nsatz. + destruct square_a as [sqrt_a], (dec (y=0)); + pose proof nonzero_a; pose proof (nonsquare_d (sqrt_a/y)); fsatz. Qed. Lemma solve_correct : forall x y, onCurve x y <-> (x^2 = solve_for_x2 y). - Proof. - unfold solve_for_x2; simpl; split; intros; - (common_denominator_all; [nsatz | auto using a_d_y2_nonzero]). - Qed. + Proof. pose proof a_d_y2_nonzero; cbv [solve_for_x2]; t. Qed. End PointCompression. End CompleteEdwardsCurveTheorems. Section Homomorphism. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd} + {Fprm:@twisted_edwards_params F Feq Fzero Fmul Fa Fd} {Feq_dec:DecidableRel Feq}. Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} - {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd} + {Kprm:@twisted_edwards_params K Keq Kzero Kmul Ka Kd} {Keq_dec:DecidableRel Keq}. Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul K Keq Kone Kadd Kmul phi}. Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}. Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd). Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd). - Local Notation FonCurve := (@onCurve F Feq Fone Fadd Fmul Fa Fd). - Local Notation KonCurve := (@onCurve K Keq Kone Kadd Kmul Ka Kd). Create HintDb field_homomorphism discriminated. Hint Rewrite <- @@ -170,21 +161,21 @@ Module E. Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq add Kpoint eq add point_phi. Proof. repeat match goal with - | |- Monoid.is_homomorphism => split | |- _ => intro - | |- _ /\ _ => split - | [H: _ /\ _ |- _ ] => destruct H - | [p: point |- _ ] => destruct p as [ [??]?] + | |- Monoid.is_homomorphism => split + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' prod + | _ => progress destruct_head' and | |- context[point_phi] => setoid_rewrite point_phi_correct - | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in * - | |- Keq ?x ?x => reflexivity - | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism - | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] - end; - assert (FonCurve (f1,f2)) as FonCurve1 by assumption; - assert (FonCurve (f,f0)) as FonCurve2 by assumption; - [ eapply (@edwardsAddCompleteMinus F) with (x1 := f1); destruct Fprm; eauto - | eapply (@edwardsAddCompletePlus F) with (x1 := f1); destruct Fprm; eauto]. + | _ => progress cbv [ref_phi eq E.eq CompleteEdwardsCurve.E.eq E.add E.coordinates proj1_sig] in * + (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *) + | _ => _gather_nonzeros + | _ => progress simpl in * + | |- _ ?x ?x => reflexivity + | |- _ ?x ?y => rewrite_strat bottomup hints field_homomorphism + | |- _ /\ _ => split + | _ => solve [fsatz | repeat (f_equiv; auto) ] + end. Qed. End Homomorphism. End E. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index eef1eb371..08eaa6387 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -9,13 +9,14 @@ 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. Module Extended. Section ExtendedCoordinates. Import Group Ring Field. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {prm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d} + {prm:@E.twisted_edwards_params F Feq Fzero Fmul a d} {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. @@ -23,47 +24,42 @@ Module Extended. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). - Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d). + Local Notation onCurve := (@E.onCurve F Feq Fone Fadd Fmul a d). Add Field _edwards_curve_extended_field : (field_theory_for_stdlib_tactic (H:=field)). (** [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 }. + Definition point := { P | let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y }. Definition coordinates (P:point) : F*F*F*F := proj1_sig P. - Create HintDb bash discriminated. - Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash. - Ltac safe_bash := - repeat match goal with - | |- Proper _ _ => intro - | _ => progress intros - | [ H: _ /\ _ |- _ ] => destruct H - | [ p:E.point |- _ ] => destruct p as [ [??] ? ] - | [ p:point |- _ ] => destruct p as [ [ [ [??] ? ] ? ] ? ] - | _ => progress autounfold with bash in * - | |- _ /\ _ => split - | _ => solve [neq01] - | _ => solve [eauto] - | _ => solve [intuition eauto] - | _ => solve [etransitivity; eauto] - | |- _ => rewrite <-!(field_div_definition(field:=field)) in * - | |- _*_ <> 0 => apply Ring.zero_product_iff_zero_factor - | [H: _ |- _ ] => solve [intro; apply H; super_nsatz] - | |- Feq _ _ => super_nsatz - end. - (** Using [pose proof E.char_gt_2] causes [E.char_gt_2] to get - picked up in the proof term when we don't want it to. *) - Ltac unsafe_bash := pose proof E.char_gt_2; safe_bash. - Ltac bash := safe_bash; unsafe_bash. - - Obligation Tactic := bash. - - Program Definition from_twisted (P:Epoint) : point := exist _ - (let (x,y) := E.coordinates P in (x, y, 1, x*y)) _. - - Program Definition to_twisted (P:point) : Epoint := exist _ - (let '(X,Y,Z,T) := coordinates P in let iZ := Finv Z in ((X*iZ), (Y*iZ))) _. + Ltac t_step := + match goal with + | |- Proper _ _ => intro + | _ => progress intros + | _ => progress destruct_head' prod + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' point + | _ => progress destruct_head' and + | _ => E._gather_nonzeros + | _ => progress cbv [CompleteEdwardsCurve.E.eq E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig E.onCurve] in * + | |- _ /\ _ => split | |- _ <-> _ => split + | _ => rewrite <-!(field_div_definition(field:=field)) + | _ => solve [fsatz] + end. + Ltac t := repeat t_step. + + 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. + + Program Definition to_twisted (P:point) : Epoint := + let XYZT := coordinates P in let T := snd XYZT in + let XYZ := fst XYZT in let Z := snd XYZ in + let XY := fst XYZ in let Y := snd XY in + let X := fst XY in + let iZ := Finv Z in ((X*iZ), (Y*iZ)). + Next Obligation. t. Qed. Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). @@ -72,10 +68,8 @@ Module Extended. let '(X2, Y2, Z2, _) := coordinates P2 in Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2. - Local Hint Unfold from_twisted to_twisted eq eq_noinv : bash. - Lemma eq_noinv_eq P Q : eq P Q <-> eq_noinv P Q. - Proof. safe_bash; repeat split; safe_bash. Qed. + Proof. cbv [eq_noinv eq to_twisted from_twisted]; t. Qed. Global Instance DecidableRel_eq_noinv : Decidable.DecidableRel eq_noinv. Proof. intros P Q. @@ -87,45 +81,31 @@ Module Extended. eapply @Decidable_iff_to_flip_impl; [eapply eq_noinv_eq | exact _]. Defined. - Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; safe_bash. Qed. - Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. unsafe_bash. Qed. - Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. safe_bash. Qed. - Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. Proof. unsafe_bash. Qed. + 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. 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. - repeat match goal with - | _ => progress simpl in * - | [ H : prod _ _ |- _ ] => destruct H - | [ H : and _ _ |- _ ] => destruct H - | _ => reflexivity - | [ H : ?x = ?y |- _ ] => is_var x; rewrite H; clear x H - end. - Qed. + (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. + (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. + (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. + Section generic. (* TODO(jgross) what is this section? *) Context (F4 : Type) (pair4 : F -> F -> F -> F -> F4) (let_in : F -> (F -> F4) -> F4). @@ -155,23 +135,20 @@ Module Extended. (fun x f => let y := x in f y) P1 P2. - Local Hint Unfold E.add E.coordinates add_coordinates : bash. - 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. - destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. - pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. - pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. - unsafe_bash. + cbv [E.add add_coordinates to_twisted] in *. destruct prm. t. + (* TODO: change [prove_nsatz_nonzero] to use typeclass resolution to look up field characteristic instead of context matching. then we won't need to destruct prm *) 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)}. + (* TODO(jgross): what are these definitions? *) Obligation Tactic := idtac. Program Definition add_unopt (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q). Next Obligation. @@ -264,36 +241,6 @@ Module Extended. - unfold opp; intros; rewrite to_twisted_from_twisted; reflexivity. - unfold zero; intros; rewrite to_twisted_from_twisted; reflexivity. Qed. - - (* TODO: decide whether we still need those, then port *) - (* - Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P. - unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. - Qed. - - Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint E.zero) P === P. - unfold equiv, extendedPoint_eq; intros. - 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, 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. - Proof. - trivial. - Qed. - - Lemma scalarMultM1_rep : forall n P, unExtendedPoint (nat_iter_op unifiedAddM1 (mkExtendedPoint E.zero) n P) = E.mul n (unExtendedPoint P). - induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]; intros. - unfold E.mul; fold E.mul. - rewrite <-IHn, unifiedAddM1_rep; auto. - Qed. - *) End TwistMinus1. End ExtendedCoordinates. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index aa10fbd5f..7fa95101e 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -2,11 +2,217 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.Util.Notations Crypto.Util.Decidable Crypto.Util.Tactics. -Section Pre. +(* TODO: move *) +Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed. + +Global Instance Symmetric_not {T:Type} (R:T->T->Prop) + {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)). +Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed. + +Section ReflectiveNsatzSideConditionProver. + 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}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. + + Import BinInt BinNat BinPos. + Axiom ZtoR : Z -> R. + Inductive coef := + | Coef_one + | Coef_opp (_:coef) + | Coef_add (_ _:coef) + | Coef_mul (_ _:coef). + Fixpoint denote (c:coef) : R := + match c with + | Coef_one => one + | Coef_opp c => opp (denote c) + | Coef_add c1 c2 => add (denote c1) (denote c2) + | Coef_mul c1 c2 => mul (denote c1) (denote c2) + end. + Fixpoint CtoZ (c:coef) : Z := + match c with + | Coef_one => Z.one + | Coef_opp c => Z.opp (CtoZ c) + | Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2) + | Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2) + end. + Lemma CtoZ_correct c : ZtoR (CtoZ c) = denote c. + Proof. + Admitted. + + Section WithChar. + Context C (char_gt_C:forall p, Pos.le p C -> ZtoR (Zpos p) <> zero). + Fixpoint is_nonzero (c:coef) : bool := + match c with + | Coef_opp c => is_nonzero c + | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2) + | _ => + match CtoZ c with + | Z0 => false + | Zpos p => Pos.leb p C + | Zneg p => Pos.leb p C + end + end. + Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. + Proof. + induction c; + repeat match goal with + | _ => progress (unfold is_nonzero in *; fold is_nonzero in *) + | _ => progress change (denote Coef_one) with one in * + | _ => progress change (denote (Coef_opp c)) with (opp (denote c)) in * + | _ => progress change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * + | _ => rewrite Pos.leb_le in * + | _ => rewrite <-Pos2Z.opp_pos in * + | H: Logic.eq match ?x with _ => _ end true |- _ => destruct x eqn:? + | H: _ |- _ => unique pose proof (C_lt_char _ H) + | H:_ |- _ => unique pose proof (proj1 (Bool.andb_true_iff _ _) H) + | H:_/\_|- _ => unique pose proof (proj1 H) + | H:_/\_|- _ => unique pose proof (proj2 H) + | H: _ |- _ => unique pose proof (z_nonzero_correct _ H) + | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor + | |- opp _ <> zero => eapply Ring.opp_nonzero_nonzero + | |- _ => solve [eauto | discriminate] + end. + { admit. } + { rewrite <-CtoZ_correct, Heqz. auto. } + { rewrite <-CtoZ_correct, Heqz. admit. } + Admitted. + End WithChar. +End ReflectiveNsatzSideConditionProver. + +Ltac debuglevel := constr:(1%nat). + +Ltac assert_as_by_debugfail G n tac := + ( + assert G as n by tac + ) || + let dbg := debuglevel in + match dbg with + | O => idtac + | _ => idtac "couldn't prove" G + end. + +Ltac solve_debugfail tac := + match goal with + |- ?G => let H := fresh "H" in + assert_as_by_debugfail G H tac; exact H + end. + +Ltac _reify one opp add mul x := + match x with + | one => constr:(Coef_one) + | opp ?a => + let a := _reify one opp add mul a in + constr:(Coef_opp a) + | add ?a ?b => + let a := _reify one opp add mul a in + let b := _reify one opp add mul b in + constr:(Coef_add a b) + | mul ?a ?b => + let a := _reify one opp add mul a in + let b := _reify one opp add mul b in + constr:(Coef_mul a b) + end. + +Ltac solve_nsatz_nonzero := + match goal with (* TODO: change this match to a typeclass resolution *) + |H:forall p:BinPos.positive, BinPos.Pos.le p ?C -> not (?eq (?ZtoR (BinInt.Z.pos p)) ?zero) |- not (?eq ?x ?zero) => + let refl_ok' := fresh "refl_ok" in + pose (is_nonzero_correct(eq:=eq)(zero:=zero)(*TODO:ZtoR*) _ H) as refl_ok'; + let refl_ok := (eval cbv delta [refl_ok'] in refl_ok') in + clear refl_ok'; + match refl_ok with + is_nonzero_correct(R:=?R)(one:=?one)(opp:=?opp)(add:=?add)(mul:=?mul)(ring:=?rn)(zpzf:=?zpzf) _ _ => + solve_debugfail ltac:( + let x' := _reify one opp add mul x in + let x' := constr:(@denote R one opp add mul x') in + change (not (eq x' zero)); apply refl_ok; vm_decide + ) + end + end. + +Ltac goal_to_field_equality fld := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + match goal with + | [ |- eq _ _] => idtac + | [ |- not (eq ?x ?y) ] => apply not_exfalso; intro; goal_to_field_equality fld + | _ => exfalso; + match goal with + | H: not (eq _ _) |- _ => apply not_exfalso in H; apply H + | _ => apply (field_is_zero_neq_one(field:=fld)) + end + end. + +Ltac _introduce_inverse fld d d_nz := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in + let one := match type of fld with Algebra.field(one:=?one) => one end in + let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in + match goal with [H: eq (mul d _) one |- _ ] => fail 1 | _ => idtac end; + let d_i := fresh "i" in + unique pose proof (Field.right_multiplicative_inverse(H:=fld) _ d_nz); + set (inv d) as d_i in *; + clearbody d_i. + +Ltac inequalities_to_inverses fld := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let div := match type of fld with Algebra.field(div:=?div) => div end in + let sub := match type of fld with Algebra.field(sub:=?sub) => sub end in + repeat match goal with + | [H: not (eq _ _) |- _ ] => + lazymatch type of H with + | not (eq ?d zero) => _introduce_inverse fld d H + | not (eq zero ?d) => _introduce_inverse fld d (symmetry(R:=fun a b => not (eq a b)) H) + | not (eq ?x ?y) => _introduce_inverse fld (sub x y) (Ring.neq_sub_neq_zero _ _ H) + end + end. + +Ltac _division_to_inverse_by fld n d tac := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let one := match type of fld with Algebra.field(one:=?one) => one end in + let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in + let div := match type of fld with Algebra.field(div:=?div) => div end in + let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in + let d_nz := fresh "nz" in + assert_as_by_debugfail constr:(not (eq d zero)) d_nz tac; + rewrite (field_div_definition(field:=fld) n d) in *; + lazymatch goal with + | H: eq (mul ?di d) one |- _ => rewrite <-!(Field.left_inv_unique(H:=fld) _ _ H) in * + | H: eq (mul d ?di) one |- _ => rewrite <-!(Field.right_inv_unique(H:=fld) _ _ H) in * + | _ => _introduce_inverse constr:(fld) constr:(d) d_nz + end; + clear d_nz. + +Ltac _nonzero_tac fld := + solve [trivial | goal_to_field_equality fld; nsatz; solve_nsatz_nonzero]. + +Ltac divisions_to_inverses_step fld := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let div := match type of fld with Algebra.field(div:=?div) => div end in + match goal with + | [H: context[div ?n ?d] |- _ ] => _division_to_inverse_by fld n d ltac:(_nonzero_tac fld) + | |- context[div ?n ?d] => _division_to_inverse_by fld n d ltac:(_nonzero_tac fld) + end. + +Ltac divisions_to_inverses fld := + repeat divisions_to_inverses_step fld. + +Ltac fsatz := + let fld := Algebra.guess_field in + goal_to_field_equality fld; + inequalities_to_inverses fld; + divisions_to_inverses fld; + nsatz; solve_nsatz_nonzero. + +Section Edwards. Context {F eq zero one opp add sub mul inv div} {field:@Algebra.field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}. - Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. @@ -17,10 +223,10 @@ Section Pre. Context (a:F) (a_nonzero : a<>0) (a_square : exists sqrt_a, sqrt_a^2 = a). Context (d:F) (d_nonsquare : forall sqrt_d, sqrt_d^2 <> d). - Context (char_gt_2 : 1+1 <> 0). + Context (char_gt_2:forall p, BinPos.Pos.le p 2 -> ZtoR (BinInt.Zpos p) <> zero). - Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2). - Lemma zeroOnCurve : onCurve 0 1. nsatz. Qed. + Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). + Lemma onCurve_zero : onCurve 0 1. nsatz. Qed. Section Addition. Context (x1 y1:F) (P1onCurve: onCurve x1 y1). @@ -29,12 +235,16 @@ Section Pre. Proof. destruct a_square as [sqrt_a], (dec(sqrt_a*x2+y2 = 0)), (dec(sqrt_a*x2-y2 = 0)); try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] - => specialize (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) + => pose proof (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) /(f (sqrt_a * x2) y2 * x1 * y1 ))) - end; field_nsatz. + end; fsatz. Qed. - Lemma add_onCurve : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). - Proof. pose proof denominator_nonzero; field_nsatz. Qed. + Lemma denominator_nonzero_x : 1 + d*x1*x2*y1*y2 <> 0. + Proof. pose proof denominator_nonzero. fsatz. Qed. + Lemma denominator_nonzero_y : 1 - d*x1*x2*y1*y2 <> 0. + Proof. pose proof denominator_nonzero. fsatz. Qed. + Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). + Proof. pose proof denominator_nonzero. fsatz. Qed. End Addition. -End Pre.
\ No newline at end of file +End Edwards.
\ No newline at end of file diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index e081ded1e..d475f78c2 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -13,13 +13,14 @@ Module E. 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 Infix "-" := Fsub. Local Notation "x ^ 2" := (x*x) (at level 30). + Local Notation "n / d" := (fst (Fdiv n d, (_:(d <> 0)))). (* force nonzero d *) Context {a d: F}. Class twisted_edwards_params := { - char_gt_2 : 1 + 1 <> 0; + char_gt_2 : forall p : BinNums.positive, BinPos.Pos.le p 2 -> Pre.ZtoR (BinNums.Zpos p) <> 0; nonzero_a : a <> 0; square_a : exists sqrt_a, sqrt_a^2 = a; nonsquare_d : forall x, x^2 <> d @@ -28,15 +29,20 @@ Module E. Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }. Definition coordinates (P:point) : (F*F) := proj1_sig P. + Definition eq (P Q:point) := + fst (coordinates P) = fst (coordinates Q) /\ + snd (coordinates P) = snd (coordinates Q). Program Definition zero : point := (0, 1). - Next Obligation. auto using Pre.zeroOnCurve. Defined. + Next Obligation. eauto using Pre.onCurve_zero. Qed. Program Definition add (P1 P2:point) : point := let x1y1 := coordinates P1 in let x1 := fst x1y1 in let y1 := snd x1y1 in let x2y2 := coordinates P2 in let x2 := fst x2y2 in let y2 := snd x2y2 in (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; auto using Pre.add_onCurve. Defined. + Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H. eauto using Pre.denominator_nonzero_x. Qed. + Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.denominator_nonzero_y. Qed. + Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.onCurve_add. Qed. Fixpoint mul (n:nat) (P : point) : point := match n with @@ -47,5 +53,6 @@ Module E. End E. Delimit Scope E_scope with E. +Infix "=" := E.eq : E_scope. Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope. +Infix "*" := E.mul : E_scope.
\ No newline at end of file |