From 39ec94341fa3a30d97d4462e9c9d481ada2c8d3d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 17 Jun 2016 13:33:17 -0400 Subject: move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems --- src/Algebra.v | 267 +++++++----------- .../CompleteEdwardsCurveTheorems.v | 314 ++++++--------------- src/ModularArithmetic/ModularArithmeticTheorems.v | 3 +- src/Nsatz.v | 119 ++++++++ src/Spec/CompleteEdwardsCurve.v | 8 +- 5 files changed, 317 insertions(+), 394 deletions(-) create mode 100644 src/Nsatz.v (limited to 'src') diff --git a/src/Algebra.v b/src/Algebra.v index b5eb4a7f5..f6b2fa330 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1,6 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Util.Tactics. -Close Scope nat_scope. Close Scope type_scope. Close Scope core_scope. +Require Import Crypto.Util.Tactics Crypto.Nsatz. +Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. Section Algebra. Context {T:Type} {eq:T->T->Prop}. @@ -22,11 +22,18 @@ Section Algebra. { monoid_is_associative : is_associative; monoid_is_left_identity : is_left_identity; - monoid_is_right_identity : is_right_identity + monoid_is_right_identity : is_right_identity; + + monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op; + monoid_Equivalence : Equivalence eq; + monoid_is_eq_dec : is_eq_dec }. Global Existing Instance monoid_is_associative. Global Existing Instance monoid_is_left_identity. Global Existing Instance monoid_is_right_identity. + Global Existing Instance monoid_Equivalence. + Global Existing Instance monoid_is_eq_dec. + Global Existing Instance monoid_op_Proper. Context {inv:T->T}. Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }. @@ -38,17 +45,11 @@ Section Algebra. group_is_left_inverse : is_left_inverse; group_is_right_inverse : is_right_inverse; - group_Equivalence : Equivalence eq; - group_is_eq_dec : is_eq_dec; - group_op_Proper: Proper (respectful eq (respectful eq eq)) op; group_inv_Proper: Proper (respectful eq eq) inv }. Global Existing Instance group_monoid. Global Existing Instance group_is_left_inverse. Global Existing Instance group_is_right_inverse. - Global Existing Instance group_Equivalence. - Global Existing Instance group_is_eq_dec. - Global Existing Instance group_op_Proper. Global Existing Instance group_inv_Proper. Class is_commutative := { commutative : forall x y, op x y = op y x }. @@ -137,45 +138,63 @@ Section Algebra. End Algebra. -Section GenericCancellation. - Context {T:Type} {eq:T->T->Prop} {Equivalence_eq : Equivalence eq}. - Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Context {op:T->T->T} {Proper_op : Proper(respectful eq (respectful eq eq)) op}. - Context {id:T}. - - Context {Hassoc: is_associative (op:=op) (eq:=eq)}. - Context {Hrid: is_right_identity (op:=op) (eq:=eq) (id := id)}. - Context {Hlid: is_left_identity (op:=op) (eq:=eq) (id:=id) }. +Module Monoid. + Section Monoid. + Context {T eq op id} {monoid:@monoid T eq op id}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "*" := op. - Lemma cancel_right z iz (Hinv:op z iz = id) : - forall x y, op x z = op y z <-> x = y. - Proof. - split; intros. - { assert (op (op x z) iz = op (op y z) iz) as Hcut by (f_equiv; assumption). - rewrite <-associative in Hcut. - rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. } - { f_equiv; assumption. } - Qed. + Lemma cancel_right z iz (Hinv:op z iz = id) : + forall x y, x * z = y * z <-> x = y. + Proof. + split; intros. + { assert (op (op x z) iz = op (op y z) iz) as Hcut by (f_equiv; assumption). + rewrite <-associative in Hcut. + rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. } + { f_equiv; assumption. } + Qed. - Lemma cancel_left z iz (Hinv:op iz z = id) : - forall x y, op z x = op z y <-> x = y. - Proof. - split; intros. - { assert (op iz (op z x) = op iz (op z y)) as Hcut by (f_equiv; assumption). - rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } - { f_equiv; assumption. } - Qed. -End GenericCancellation. + Lemma cancel_left z iz (Hinv:op iz z = id) : + forall x y, z * x = z * y <-> x = y. + Proof. + split; intros. + { assert (op iz (op z x) = op iz (op z y)) as Hcut by (f_equiv; assumption). + rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } + { f_equiv; assumption. } + Qed. + + Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x. + Proof. + intros Hi Hii. + assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity). + rewrite associative, Hii, left_identity, right_identity in H; exact H. + Qed. + + Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id. + Proof. + intros Hx Hy. + cut (iy * (ix*x) * y = id); try intro H. + { rewrite <-!associative; rewrite <-!associative in H; exact H. } + rewrite Hx, right_identity, Hy. reflexivity. + Qed. + + End Monoid. +End Monoid. Module Group. Section BasicProperties. Context {T eq op id inv} `{@group T eq op id inv}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - - Lemma cancel_left : forall z x y, op z x = op z y <-> x = y. - Proof. eauto using cancel_left, left_inverse. Qed. - Lemma cancel_right : forall z x y, op x z = op y z <-> x = y. - Proof. eauto using cancel_right, right_inverse. Qed. + Local Infix "*" := op. + + Lemma cancel_left : forall z x y, z*x = z*y <-> x = y. + Proof. eauto using Monoid.cancel_left, left_inverse. Qed. + Lemma cancel_right : forall z x y, x*z = y*z <-> x = y. + Proof. eauto using Monoid.cancel_right, right_inverse. Qed. + Lemma inv_inv x : inv(inv(x)) = x. + Proof. eauto using Monoid.inv_inv, left_inverse. Qed. + Lemma inv_op x y : (inv y*inv x)*(x*y) =id. + Proof. eauto using Monoid.inv_op, left_inverse. Qed. End BasicProperties. Section Homomorphism. @@ -240,12 +259,12 @@ Module Ring. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. - Lemma mul_0_r : forall x, x * 0 = 0. + Lemma mul_0_r : forall x, 0 * x = 0. Proof. intros. - assert (x*0 = x*0) as Hx by reflexivity. - rewrite <-(left_identity 0), left_distributive in Hx at 1. - assert (x*0 + x*0 - x*0 = x*0 - x*0) as Hxx by (f_equiv; exact Hx). + assert (0*x = 0*x) as Hx by reflexivity. + rewrite <-(right_identity 0), right_distributive in Hx at 1. + assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (f_equiv; exact Hx). rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx. Qed. @@ -258,6 +277,37 @@ Module Ring. rewrite associative, left_inverse, left_identity in Hxx; exact Hxx. Qed. + Lemma sub_0_l x : 0 - x = opp x. + Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed. + + Lemma mul_opp_r x y : x * opp y = opp (x * y). + Proof. + assert (Ho:x*(opp y) + x*y = 0) + by (rewrite <-left_distributive, left_inverse, mul_0_l; reflexivity). + rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. + rewrite <-!associative, right_inverse, right_identity; reflexivity. + Qed. + + Lemma mul_opp_l x y : opp x * y = opp (x * y). + Proof. + assert (Ho:opp x*y + x*y = 0) + by (rewrite <-right_distributive, left_inverse, mul_0_r; reflexivity). + rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. + rewrite <-!associative, right_inverse, right_identity; reflexivity. + Qed. + + Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul). + Proof. + split; intros. rewrite !ring_sub_definition, left_distributive. + eapply Group.cancel_left, mul_opp_r. + Qed. + + Global Instance is_right_distributive_sub : is_right_distributive (eq:=eq)(add:=sub)(mul:=mul). + Proof. + split; intros. rewrite !ring_sub_definition, right_distributive. + eapply Group.cancel_left, mul_opp_l. + Qed. + Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq. Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops. Proof. @@ -266,6 +316,8 @@ Module Ring. eapply @left_identity; eauto with typeclass_instances. - eapply @right_identity; eauto with typeclass_instances. - eapply associative. + - intros; eapply right_distributive. + - intros; eapply left_distributive. Qed. Lemma opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0. @@ -361,7 +413,7 @@ Module Field. Global Instance is_mul_nonzero_nonzero : @is_mul_nonzero_nonzero T eq 0 mul. Proof. constructor. intros x y Hx Hy Hxy. - assert (0 = (inv y * (inv x * x)) * y) as H00 by (rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity). + assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_l; reflexivity). rewrite left_multiplicative_inverse in H00 by assumption. rewrite right_identity in H00. rewrite left_multiplicative_inverse in H00 by assumption. @@ -456,128 +508,6 @@ Ltac field_simplify_eq_hyps := Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. -(*** Tactics for manipulating polynomial equations *) -Require Nsatz. -Require Import List. -Open Scope core_scope. - -Generalizable All Variables. -Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)} - : forall x y, eq (sub x y) zero <-> eq x y. -Proof. - split;intros Hx. - { eapply Nsatz.psos_r1b. eapply Hx. } - { eapply Nsatz.psos_r1. eapply Hx. } -Qed. - -Ltac get_goal := lazymatch goal with |- ?g => g end. - -Ltac nsatz_equation_implications_to_list eq zero g := - lazymatch g with - | eq ?p zero => constr:(p::nil) - | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l) - end. - -Ltac nsatz_reify_equations eq zero := - let g := get_goal in - let lb := nsatz_equation_implications_to_list eq zero g in - lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with - (?variables, ?le) => - lazymatch (eval compute in (List.rev le)) with - | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal) - end - end. - -Ltac nsatz_get_free_variables reified_package := - lazymatch reified_package with (?fv, _, _) => fv end. - -Ltac nsatz_get_reified_givens reified_package := - lazymatch reified_package with (_, ?givens, _) => givens end. - -Ltac nsatz_get_reified_goal reified_package := - lazymatch reified_package with (_, _, ?goal) => goal end. - -Require Import Coq.setoid_ring.Ring_polynom. -Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := - nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). - -Ltac nsatz_compute_get_leading_coefficient := - lazymatch goal with - |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a - end. - -Ltac nsatz_compute_get_certificate := - lazymatch goal with - |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b) - end. - -Ltac nsatz_rewrite_and_revert domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => - lazymatch goal with - | |- eq _ zero => idtac - | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring)) - end; - repeat match goal with - | [H : eq _ zero |- _ ] => revert H - | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H - end - end. - -Ltac nsatz_nonzero := - try solve [apply Integral_domain.integral_domain_one_zero - |apply Integral_domain.integral_domain_minus_one_zero - |trivial - |apply Ring.opp_nonzero_nonzero;trivial]. - -Ltac nsatz_domain_sugar_power domain sugar power := - let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) - lazymatch type of domain with - | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => - nsatz_rewrite_and_revert domain; - let reified_package := nsatz_reify_equations eq zero in - let fv := nsatz_get_free_variables reified_package in - let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in - let reified_givens := nsatz_get_reified_givens reified_package in - let reified_goal := nsatz_get_reified_goal reified_package in - nsatz_compute_to_goal sugar nparams reified_goal power reified_givens; - let a := nsatz_compute_get_leading_coefficient in - let crt := nsatz_compute_get_certificate in - intros _ (* discard [nsatz_compute] output *); intros; - apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); - [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] - | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *) - | solve [repeat (split; [assumption|]); exact I] ] - end. - -Ltac nsatz_guess_domain := - match goal with - | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | |- not (?eq _ _) => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | [H: ?eq _ _ |- _ ] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | [H: not (?eq _ _) |- _] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - end. - -Ltac nsatz_sugar_power sugar power := - let domain := nsatz_guess_domain in - nsatz_domain_sugar_power domain sugar power. - -Tactic Notation "nsatz" constr(n) := - let nn := (eval compute in (BinNat.N.of_nat n)) in - nsatz_sugar_power BinInt.Z0 nn. - -Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat. - -Ltac nsatz_contradict := - intros; - let domain := nsatz_guess_domain in - lazymatch type of domain with - | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => - assert (eq one zero) as Hbad; - [nsatz; nsatz_nonzero - |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] - end. - (*** Polynomial equations over fields *) Ltac field_algebra := @@ -587,6 +517,7 @@ Ltac field_algebra := repeat (apply conj); try solve [nsatz_nonzero + |apply Ring.opp_nonzero_nonzero;trivial |unfold not; intro; nsatz_contradict]. Section Example. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 88ae9578c..4ad76856e 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,47 +1,32 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.ModularArithmetic.FField. -Require Import Crypto.ModularArithmetic.FNsatz. +Require Import Crypto.Algebra Crypto.Nsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Module E. + Import Group Ring Field CompleteEdwardsCurve.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. + 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}. + 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) (at level 30). + Local Notation point := (@point F Feq Fone Fadd Fmul a d). + Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). + + Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)). - 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))). + Definition eq (P Q:point) := + let Feq2 (ab xy:F*F) := fst ab = fst xy /\ snd ab = snd xy in + Feq2 (coordinates P) (coordinates Q). + Infix "=" := eq : E_scope. + (* TODO:port Local Ltac t := unfold point_eqb; repeat match goal with @@ -94,207 +79,94 @@ Module E. 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. + *) - Lemma add_0_l : forall P, (E.zero + P)%E = P. - Proof. - intros; rewrite add_comm. apply add_0_r. - Qed. + (* TODO: move to util *) + Lemma decide_and : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}. + Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed. - Lemma mul_0_l : forall P, (0 * P = E.zero)%E. - Proof. - auto. - Qed. + 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. - Lemma mul_S_l : forall n P, (S n * P)%E = (P + n * P)%E. - Proof. - auto. - Qed. + Ltac expand_opp := + rewrite ?mul_opp_r, ?mul_opp_l, ?ring_sub_definition, ?inv_inv, <-?ring_sub_definition. - 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. + Local Hint Resolve char_gt_2. + Local Hint Resolve nonzero_a. + Local Hint Resolve square_a. + Local Hint Resolve nonsquare_d. + Local Hint Resolve @edwardsAddCompletePlus. + Local Hint Resolve @edwardsAddCompleteMinus. + + Program Definition opp (P:point) : point := + exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. + Solve All Obligations using intros; destruct_points; simpl; field_algebra. - Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. + Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp). Proof. - induction n; intros; auto. - rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity. + repeat match goal with + | |- _ => progress intros + | [H: _ /\ _ |- _ ] => destruct H + | |- _ => progress destruct_points + | |- _ => progress cbv [fst snd coordinates proj1_sig eq add zero opp] in * + | |- _ => split + | |- Feq _ _ => common_denominator_all; try nsatz + | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto] + | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances + end. + (* TODO: port denominator-nonzero proofs for associativity *) + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. Qed. - 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. - 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. + (* TODO: move to [Group] and [AbelianGroup] as appropriate *) + Lemma mul_0_l : forall P, (0 * P = zero)%E. + Proof. intros; reflexivity. Qed. + Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E. + Proof. intros; reflexivity. Qed. + Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E. 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. + induction n; intros; + rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. Qed. - - - Definition opp' (xy:(F q*F q)) : (F q * F q) := let '(x, y) := xy in (opp x, y). - Definition opp (P:E.point) : E.point. exists (opp' (proj1_sig P)). - Proof. - destruct P as [[]]; simpl; rewrite F_square_opp; trivial. - Defined. - - Definition sub P Q := (P + opp Q)%E. - - Lemma opp_zero : opp E.zero = E.zero. - Proof. - pose proof @F_opp_0. - unfold opp, opp', E.zero; simpl; eapply point_eq; congruence. - Qed. - - Lemma add_opp_r : forall P, (P + opp P = E.zero)%E. - Proof. - unfold opp, 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. + Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. Proof. - intros. rewrite add_comm. eapply add_opp_r. + induction n; intros; [reflexivity|]. + rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity. Qed. - - Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E. + Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. + Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed. + (* + Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%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. + induction n. intros. simpl. admit. 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. + + Section PointCompression. + Local Notation "x ^2" := (x*x). + Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). - 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; trivial; intros; rewrite !mul_S_l, opp_add; congruence. - Qed. + Lemma a_d_y2_nonzero : forall 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 (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra. + Qed. + + Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). + Proof. + unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero. + Qed. + End PointCompression. End CompleteEdwardsCurveTheorems. -End E. -Infix "-" := E.sub : E_scope. \ No newline at end of file +End E. \ No newline at end of file diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index fe7600784..4e0ba461e 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -154,9 +154,10 @@ Section FandZ. Proof. repeat split; Fdefn. { rewrite Z.add_0_r. auto. } - { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. } { apply F_eq_dec. } + { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. } { rewrite Z.mul_1_r. auto. } + { apply F_eq_dec. } Qed. Lemma ZToField_0 : @ZToField m 0 = 0. diff --git a/src/Nsatz.v b/src/Nsatz.v new file mode 100644 index 000000000..c8a648626 --- /dev/null +++ b/src/Nsatz.v @@ -0,0 +1,119 @@ +(*** Tactics for manipulating polynomial equations *) +Require Nsatz. +Require Import List. + +Generalizable All Variables. +Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)} + : forall x y, eq (sub x y) zero <-> eq x y. +Proof. + split;intros Hx. + { eapply Nsatz.psos_r1b. eapply Hx. } + { eapply Nsatz.psos_r1. eapply Hx. } +Qed. + +Ltac get_goal := lazymatch goal with |- ?g => g end. + +Ltac nsatz_equation_implications_to_list eq zero g := + lazymatch g with + | eq ?p zero => constr:(p::nil) + | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l) + end. + +Ltac nsatz_reify_equations eq zero := + let g := get_goal in + let lb := nsatz_equation_implications_to_list eq zero g in + lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with + (?variables, ?le) => + lazymatch (eval compute in (List.rev le)) with + | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal) + end + end. + +Ltac nsatz_get_free_variables reified_package := + lazymatch reified_package with (?fv, _, _) => fv end. + +Ltac nsatz_get_reified_givens reified_package := + lazymatch reified_package with (_, ?givens, _) => givens end. + +Ltac nsatz_get_reified_goal reified_package := + lazymatch reified_package with (_, _, ?goal) => goal end. + +Require Import Coq.setoid_ring.Ring_polynom. +Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := + nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). + +Ltac nsatz_compute_get_leading_coefficient := + lazymatch goal with + |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a + end. + +Ltac nsatz_compute_get_certificate := + lazymatch goal with + |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b) + end. + +Ltac nsatz_rewrite_and_revert domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => + lazymatch goal with + | |- eq _ zero => idtac + | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring)) + end; + repeat match goal with + | [H : eq _ zero |- _ ] => revert H + | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H + end + end. + +Ltac nsatz_nonzero := + try solve [apply Integral_domain.integral_domain_one_zero + |apply Integral_domain.integral_domain_minus_one_zero + |trivial]. + +Ltac nsatz_domain_sugar_power domain sugar power := + let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) + lazymatch type of domain with + | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => + nsatz_rewrite_and_revert domain; + let reified_package := nsatz_reify_equations eq zero in + let fv := nsatz_get_free_variables reified_package in + let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in + let reified_givens := nsatz_get_reified_givens reified_package in + let reified_goal := nsatz_get_reified_goal reified_package in + nsatz_compute_to_goal sugar nparams reified_goal power reified_givens; + let a := nsatz_compute_get_leading_coefficient in + let crt := nsatz_compute_get_certificate in + intros _ (* discard [nsatz_compute] output *); intros; + apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); + [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] + | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *) + | solve [repeat (split; [assumption|]); exact I] ] + end. + +Ltac nsatz_guess_domain := + match goal with + | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | |- not (?eq _ _) => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | [H: ?eq _ _ |- _ ] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | [H: not (?eq _ _) |- _] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + end. + +Ltac nsatz_sugar_power sugar power := + let domain := nsatz_guess_domain in + nsatz_domain_sugar_power domain sugar power. + +Tactic Notation "nsatz" constr(n) := + let nn := (eval compute in (BinNat.N.of_nat n)) in + nsatz_sugar_power BinInt.Z0 nn. + +Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat. + +Ltac nsatz_contradict := + intros; + let domain := nsatz_guess_domain in + lazymatch type of domain with + | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => + assert (eq one zero) as Hbad; + [nsatz; nsatz_nonzero + |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] + end. \ No newline at end of file diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 518d3d551..5df36e295 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -8,11 +8,11 @@ Module E. * *) - Context {F eq Fzero one opp Fadd sub Fmul inv div} `{Algebra.field F eq Fzero one opp Fadd sub Fmul inv div}. - Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Notation "0" := Fzero. Local Notation "1" := one. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. + 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 "-" := sub. Local Infix "/" := div. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^2" := (x*x) (at level 30). Context {a d: F}. -- cgit v1.2.3