diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 156 | ||||
| -rw-r--r-- | src/SaneField.v | 307 |
3 files changed, 394 insertions, 70 deletions
diff --git a/_CoqProject b/_CoqProject index de22ff9d4..4ad320808 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,6 +4,7 @@ src/BaseSystemProofs.v src/EdDSAProofs.v src/Field.v src/Rep.v +src/SaneField.v src/Testbit.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index f0754f7a0..4d9085a21 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,40 +1,88 @@ -Require Import Crypto.Field. Import Crypto.Field.F. +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Close Scope nat_scope. Close Scope type_scope. Close Scope core_scope. +Require Import Crypto.SaneField. + +Module NsatzExportGuarantine. + Require Import Coq.nsatz.Nsatz. + Ltac sane_nsatz := + let H := fresh "HRingOps" in + let carrierType := lazymatch goal with |- ?R ?x _ => type of x end in + let inst := constr:(_:Ncring.Ring (T:=carrierType)) in + lazymatch type of inst with + | @Ncring.Ring _ _ _ _ _ _ _ _ ?ops => + lazymatch type of ops with + @Ncring.Ring_ops ?F ?zero ?one ?add ?mul ?sub ?opp ?eq + => + pose ops as H; + (* (* apparently [nsatz] matches the goal to look for equalitites, so [eq] will need to become + [Algebra_syntax.equality]. However, reification is done using typeclasses so definitional + equality is enough (and faster) *) + change zero with (@Algebra_syntax.zero F (@Ncring.zero_notation F zero one add mul sub opp eq ops)) in *; + change one with (@Algebra_syntax.one F (@Ncring.one_notation F zero one add mul sub opp eq ops)) in *; + change add with (@Algebra_syntax.addition F (@Ncring.add_notation F zero one add mul sub opp eq ops)) in *; + change mul with (@Algebra_syntax.multiplication F F (@Ncring.mul_notation F zero one add mul sub opp eq ops)) in *; + change opp with (@Algebra_syntax.opposite F (@Ncring.opp_notation F zero one add mul sub opp eq ops)) in *; + change eq with (@Algebra_syntax.equality F (@Ncring.eq_notation F zero one add mul sub opp eq ops)) in *; + *) + move H at top (* [nsatz] requires equalities to be continuously at the bottom of the hypothesis list *) + end + end; + nsatz; + clear H. +End NsatzExportGuarantine. +Import NsatzExportGuarantine. +Ltac nsatz := sane_nsatz. + +Require Import Util.Tactics. +Inductive field_simplify_done {T} : T -> Type := + Field_simplify_done : forall H, field_simplify_done H. + +Require Import Coq.setoid_ring.Field_tac. +Ltac field_simplify_eq_all := + repeat match goal with + [ H: _ |- _ ] => + match goal with + | [ Ha : field_simplify_done H |- _ ] => fail + | _ => idtac + end; + field_simplify_eq in H; + unique pose proof (Field_simplify_done H) + end; + repeat match goal with [ H: field_simplify_done _ |- _] => clear H end. +Ltac field_nsatz := + field_simplify_eq_all; + try field_simplify_eq; + try nsatz. Generalizable All Variables. Section Pre. - Context `{Field}. - Local Notation "0" := ring0. - Local Notation "1" := ring1. - Local Notation "a = b" := (ring_eq a b). - Local Notation "a <> b" := (not (ring_eq a b)). - Local Notation "a = b" := (ring_eq a b) : type_scope. - Local Notation "a <> b" := (not (ring_eq a b)) : type_scope. - Local Infix "+" := add. - Local Infix "*" := mul. - Local Infix "-" := sub. - Local Infix "/" := div. - Local Infix "^" := powZ. + Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. + 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 Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "x '^' 2" := (x*x) (at level 30). + + Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + + Goal forall x y z, y <> 0 -> x/y = z -> z*y + y = x + y. intros; field_nsatz; auto. Qed. - Context {a:F} {a_nonzero : not(a<>0)} {a_square : exists sqrt_a, sqrt_a^2 = a}. + Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}. Context {d:F} {d_nonsquare : forall x, x^2 <> d}. Context {char_gt_2 : 1+1 <> 0}. - - (*CRUFT - Require Import Coq.setoid_ring.Field_tac. - Add Field EdwardsCurveField : (Field_theory_for_tactic F). - *) (* the canonical definitions are in Spec *) - Definition onCurve P := let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. - Definition unifiedAdd' P1' P2' := - let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). + Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition unifiedAdd' (P1' P2':F*F) : F*F := + let (x1, y1) := P1' in + let (x2, y2) := P2' in + pair (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - (*CRUFT Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. + (*CRUFT Ltac whatsNotZero := repeat match goal with | [H: ?lhs = ?rhs |- _ ] => @@ -58,55 +106,23 @@ Section Pre. end. *) + Ltac admit_nonzero := abstract (repeat split; match goal with |- not (eq _ 0) => admit end). + Lemma edwardsAddComplete' x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> + onCurve (pair x1 y1) -> + onCurve (pair x2 y2) -> (d*x1*x2*y1*y2)^2 <> 1. Proof. - unfold onCurve; intros Hc1 Hc2. - simpl in Hc1, Hc2. - Fail idtac. - Set Printing All. - Locate "*". - - pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. - destruct a_square as [sqrt_a a_square']. - rewrite <-a_square' in *. - - (* Furthermore... *) - pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. - rewrite Hc2 in Heqt at 2. - replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) - with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. - rewrite Hcontra in Heqt. - replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. - rewrite <-Hc1 in Heqt. - - (* main equation for both potentially nonzero denominators *) - destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0); - try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => - assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = - f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) - (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field; - rewrite Hcontra in Heqw1; - replace (1 * y1^2) with (y1^2) in * by field; - rewrite <- Heqt in *; - assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / - (x1 * y1 * (f (sqrt_a * x2) y2))^2) - by (rewriteAny; field; auto); - match goal with [H: d = (?n^2)/(?l^2) |- _ ] => - destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) - end + unfold onCurve; intros Hc1 Hc2 Hcontra. + assert (d * x1 ^2 * y1 ^2 * (a * x2 ^2 + y2 ^2) = a * x1 ^2 + y1 ^2) as Heqt by nsatz. + destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. + destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0); + lazymatch goal with + | [H: not (eq (?f (sqrt_a * x2) y2) 0) |- _ ] + => eapply (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) / (x1 * y1 * (f (sqrt_a * x2) y2)) )); + field_nsatz; admit_nonzero + | _ => apply a_nonzero; nsatz end. - - assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - - replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field. - - (* contradiction: product of nonzero things is zero *) - destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. - destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. - apply Ha_nonzero; field. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : diff --git a/src/SaneField.v b/src/SaneField.v new file mode 100644 index 000000000..91c1ef9b8 --- /dev/null +++ b/src/SaneField.v @@ -0,0 +1,307 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Close Scope nat_scope. Close Scope type_scope. Close Scope core_scope. + +Section Algebra. + Context {T:Type} {eq:T->T->Prop}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + + Class is_eq_dec := { eq_dec : forall x y : T, {x=y} + {x<>y} }. + + Section SingleOperation. + Context {op:T->T->T}. + + Class is_associative := { associative : forall x y z, op x (op y z) = op (op x y) z }. + + Context {id:T}. + + Class is_left_identity := { left_identity : forall x, op id x = x }. + Class is_right_identity := { right_identity : forall x, op x id = x }. + + Class monoid := + { + monoid_is_associative : is_associative; + monoid_is_left_identity : is_left_identity; + monoid_is_right_identity : is_right_identity + }. + Global Existing Instance monoid_is_associative. + Global Existing Instance monoid_is_left_identity. + Global Existing Instance monoid_is_right_identity. + + Context {inv:T->T}. + Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }. + Class is_right_inverse := { right_inverse : forall x, op x (inv x) = id }. + + Class group := + { + group_monoid : monoid; + 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 }. + + Record abelian_group := + { + abelian_group_group : group; + abelian_group_is_commutative : is_commutative + }. + Existing Class abelian_group. + Global Existing Instance abelian_group_group. + Global Existing Instance abelian_group_is_commutative. + End SingleOperation. + + Section AddMul. + Context {zero one:T}. Local Notation "0" := zero. Local Notation "1" := one. + Context {opp:T->T}. Local Notation "- x" := (opp x). + Context {add:T->T->T} {sub:T->T->T} {mul:T->T->T}. + Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. + + Class is_left_distributive := { left_distributive : forall a b c, a * (b + c) = a * b + a * c }. + Class is_right_distributive := { right_distributive : forall a b c, (b + c) * a = b * a + c * a }. + + + Class ring := + { + ring_abelian_group_add : abelian_group (op:=add) (id:=zero) (inv:=opp); + ring_monoid_mul : monoid (op:=mul) (id:=one); + ring_is_left_distributive : is_left_distributive; + ring_is_right_distributive : is_right_distributive; + + ring_sub_definition : forall x y, x - y = x + opp y; + + ring_mul_Proper : Proper (respectful eq (respectful eq eq)) mul; + ring_sub_Proper : Proper(respectful eq (respectful eq eq)) sub + }. + Global Existing Instance ring_abelian_group_add. + Global Existing Instance ring_monoid_mul. + Global Existing Instance ring_is_left_distributive. + Global Existing Instance ring_is_right_distributive. + Global Existing Instance ring_mul_Proper. + Global Existing Instance ring_sub_Proper. + + Class commutative_ring := + { + commutative_ring_ring : ring; + commutative_ring_is_commutative : is_commutative (op:=mul) + }. + Global Existing Instance commutative_ring_ring. + Global Existing Instance commutative_ring_is_commutative. + + Class is_mul_nonzero_nonzero := { mul_nonzero_nonzero : forall x y, x<>0 -> y<>0 -> x*y<>0 }. + + Class is_zero_neq_one := { zero_neq_one : zero <> one }. + + Class integral_domain := + { + integral_domain_commutative_ring : commutative_ring; + integral_domain_is_mul_nonzero_nonzero : is_mul_nonzero_nonzero; + integral_domain_is_zero_neq_one : is_zero_neq_one + }. + Global Existing Instance integral_domain_commutative_ring. + Global Existing Instance integral_domain_is_mul_nonzero_nonzero. + Global Existing Instance integral_domain_is_zero_neq_one. + + Context {inv:T->T} {div:T->T->T}. + Class is_left_multiplicative_inverse := { left_multiplicative_inverse : forall x, x<>0 -> (inv x) * x = 1 }. + + Class field := + { + field_commutative_ring : commutative_ring; + field_is_left_multiplicative_inverse : is_left_multiplicative_inverse; + field_domain_is_zero_neq_one : is_zero_neq_one; + + field_div_definition : forall x y , div x y = x * inv y; + + field_inv_Proper : Proper (respectful eq eq) inv; + field_div_Proper : Proper (respectful eq (respectful eq eq)) div + }. + Global Existing Instance field_commutative_ring. + Global Existing Instance field_is_left_multiplicative_inverse. + Global Existing Instance field_domain_is_zero_neq_one. + Global Existing Instance field_inv_Proper. + Global Existing Instance field_div_Proper. + End AddMul. +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) }. + + 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_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. + +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. + End BasicProperties. +End Group. + +Require Coq.nsatz.Nsatz. + +Ltac dropAlgebraSyntax := + cbv beta delta [ + Algebra_syntax.zero + Algebra_syntax.one + Algebra_syntax.addition + Algebra_syntax.multiplication + Algebra_syntax.subtraction + Algebra_syntax.opposite + Algebra_syntax.equality + Algebra_syntax.bracket + Algebra_syntax.power + ] in *. + +Ltac dropRingSyntax := + dropAlgebraSyntax; + cbv beta delta [ + Ncring.zero_notation + Ncring.one_notation + Ncring.add_notation + Ncring.mul_notation + Ncring.sub_notation + Ncring.opp_notation + Ncring.eq_notation + ] in *. + +Module Ring. + Section Ring. + Context {T eq zero one opp add sub mul} `{@ring T eq zero one opp add sub mul}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + 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. + 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). + rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx. + Qed. + + Lemma mul_0_l : forall x, x * 0 = 0. + Proof. + intros. + assert (x*0 = x*0) as Hx by reflexivity. + rewrite <-(left_identity 0), left_distributive in Hx at 1. + assert (opp (x*0) + (x*0 + x*0) = opp (x*0) + x*0) as Hxx by (f_equiv; exact Hx). + rewrite associative, left_inverse, left_identity in Hxx; exact Hxx. + 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. + split; dropRingSyntax; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances. + - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *) + eapply @left_identity; eauto with typeclass_instances. + - eapply @right_identity; eauto with typeclass_instances. + - eapply associative. + Qed. + End Ring. + + Section TacticSupportCommutative. + Context {T eq zero one opp add sub mul} `{@commutative_ring T eq zero one opp add sub mul}. + + Global Instance Cring_Cring_commutative_ring : + @Cring.Cring T zero one add mul sub opp eq Ring.Ncring_Ring_ops Ring.Ncring_Ring. + Proof. unfold Cring.Cring; intros; dropRingSyntax. eapply commutative. Qed. + End TacticSupportCommutative. +End Ring. + +Module IntegralDomain. + Section CommutativeRing. + Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}. + + Lemma mul_nonzero_nonzero_cases (x y : T) + : eq (mul x y) zero -> eq x zero \/ eq y zero. + Proof. + pose proof mul_nonzero_nonzero x y. + destruct (eq_dec x zero); destruct (eq_dec y zero); intuition. + Qed. + + Global Instance Integral_domain : + @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops + Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring. + Proof. + split; dropRingSyntax. + - auto using mul_nonzero_nonzero_cases. + - intro bad; symmetry in bad; auto using zero_neq_one. + Qed. + End CommutativeRing. +End IntegralDomain. + +Module Field. + Section Field. + Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + + 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). + rewrite left_multiplicative_inverse in H00 by assumption. + rewrite right_identity in H00. + rewrite left_multiplicative_inverse in H00 by assumption. + auto using zero_neq_one. + Qed. + + Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul. + Proof. + split; auto using field_commutative_ring, field_domain_is_zero_neq_one, is_mul_nonzero_nonzero. + Qed. + + Require Coq.setoid_ring.Field_theory. + Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq. + Proof. + constructor. + admit. + { intro H01. symmetry in H01. auto using zero_neq_one. } + { apply field_div_definition. } + { apply left_multiplicative_inverse. } + Qed. + End Field. +End Field.
\ No newline at end of file |