diff options
| -rw-r--r-- | _CoqProject | 8 | ||||
| -rw-r--r-- | src/Algebra.v | 594 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 376 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 431 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 256 | ||||
| -rw-r--r-- | src/EdDSAProofs.v | 30 | ||||
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v | 376 | ||||
| -rw-r--r-- | src/Experiments/GenericFieldPow.v | 336 | ||||
| -rw-r--r-- | src/ModularArithmetic/FField.v | 63 | ||||
| -rw-r--r-- | src/ModularArithmetic/FNsatz.v | 40 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 9 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 9 | ||||
| -rw-r--r-- | src/Nsatz.v | 120 | ||||
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 69 | ||||
| -rw-r--r-- | src/Spec/EdDSA.v | 107 | ||||
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 2 | ||||
| -rw-r--r-- | src/Spec/PointEncoding.v | 14 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 581 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 11 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 80 |
20 files changed, 2112 insertions, 1400 deletions
diff --git a/_CoqProject b/_CoqProject index 4b36c103b..ffb532390 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,11 +2,15 @@ -R Bedrock Bedrock Bedrock/Nomega.v Bedrock/Word.v +src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v src/EdDSAProofs.v +src/Field.v +src/Nsatz.v src/Rep.v src/Testbit.v +src/UnfinishedDerivations.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -17,8 +21,6 @@ src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v src/Encoding/PointEncodingTheorems.v src/ModularArithmetic/ExtendedBaseVector.v -src/ModularArithmetic/FField.v -src/ModularArithmetic/FNsatz.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v @@ -36,7 +38,6 @@ src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Spec/PointEncoding.v -src/Specific/Ed25519.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v @@ -46,5 +47,6 @@ src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v src/Util/Tactics.v +src/Util/Tuple.v src/Util/WordUtil.v src/Util/ZUtil.v diff --git a/src/Algebra.v b/src/Algebra.v new file mode 100644 index 000000000..27c0d2e59 --- /dev/null +++ b/src/Algebra.v @@ -0,0 +1,594 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +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}. + 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; + + 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 }. + 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_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_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. + + +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, 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, 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. + +Section ZeroNeqOne. + Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}. + + Lemma one_neq_zero : not (eq one zero). + Proof. + intro HH; symmetry in HH. auto using zero_neq_one. + Qed. +End ZeroNeqOne. + +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. + 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. + + Lemma inv_unique x ix : ix * x = id -> ix = inv x. + Proof. + intro Hix. + cut (ix*x*inv x = inv x). + - rewrite <-associative, right_inverse, right_identity; trivial. + - rewrite Hix, left_identity; reflexivity. + Qed. + + Lemma inv_id : inv id = id. + Proof. symmetry. eapply inv_unique, left_identity. Qed. + + Lemma inv_nonzero_nonzero : forall x, x <> id -> inv x <> id. + Proof. + intros ? Hx Ho. + assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity). + rewrite Ho, right_identity in Hxo. intuition. + Qed. + + Section ZeroNeqOne. + Context {one} `{is_zero_neq_one T eq id one}. + Lemma opp_one_neq_zero : inv one <> id. + Proof. apply inv_nonzero_nonzero, one_neq_zero. Qed. + Lemma zero_neq_opp_one : id <> inv one. + Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed. + End ZeroNeqOne. + End BasicProperties. + + Section Homomorphism. + Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}. + Context {H eq op id inv} {groupH:@group H eq op id inv}. + Context {phi:G->H}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + + Class is_homomorphism := + { + homomorphism : forall a b, phi (OP a b) = op (phi a) (phi b); + + is_homomorphism_phi_proper : Proper (respectful EQ eq) phi + }. + Global Existing Instance is_homomorphism_phi_proper. + Context `{is_homomorphism}. + + Lemma homomorphism_id : phi ID = id. + Proof. + assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by + (rewrite <- homomorphism, left_identity, right_identity; reflexivity). + rewrite cancel_left in Hii; exact Hii. + Qed. + + Lemma homomorphism_inv : forall x, phi (INV x) = inv (phi x). + Proof. + Admitted. + End Homomorphism. +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, 0 * x = 0. + Proof. + intros. + 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. + + 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. + + 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. + + Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero. + + 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. + 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. + - intros; eapply right_distributive. + - intros; eapply left_distributive. + Qed. + End Ring. + + Section Homomorphism. + Context {R EQ ZERO ONE OPP ADD SUB MUL} `{@ring R EQ ZERO ONE OPP ADD SUB MUL}. + Context {S eq zero one opp add sub mul} `{@ring S eq zero one opp add sub mul}. + Context {phi:R->S}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + + Class is_homomorphism := + { + homomorphism_is_homomorphism : Group.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq); + homomorphism_mul : forall x y, phi (MUL x y) = mul (phi x) (phi y); + homomorphism_one : phi ONE = one + }. + Global Existing Instance homomorphism_is_homomorphism. + + Context `{is_homomorphism}. + + Definition homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y) := + Group.homomorphism. + + Definition homomorphism_opp : forall x, phi (OPP x) = opp (phi x) := + (Group.homomorphism_inv (INV:=OPP) (inv:=opp)). + + Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y). + Proof. + intros. + rewrite !ring_sub_definition, Group.homomorphism, homomorphism_opp. reflexivity. + Qed. + + End Homomorphism. + + 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. + + Lemma ring_theory_for_stdlib_tactic : Ring_theory.ring_theory zero one add mul sub opp eq. + Proof. + constructor; intros. (* TODO(automation): make [auto] do this? *) + - apply left_identity. + - apply commutative. + - apply associative. + - apply left_identity. + - apply commutative. + - apply associative. + - apply right_distributive. + - apply ring_sub_definition. + - apply right_inverse. + Qed. + End TacticSupportCommutative. +End Ring. + +Module IntegralDomain. + Section IntegralDomain. + 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 IntegralDomain. +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. (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. + 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. + { apply Ring.ring_theory_for_stdlib_tactic. } + { intro H01. symmetry in H01. auto using zero_neq_one. } + { apply field_div_definition. } + { apply left_multiplicative_inverse. } + Qed. + + End Field. + + Section Homomorphism. + Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. + Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}. + Context {phi:F->K}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}. + + Lemma homomorphism_multiplicative_inverse : forall x, phi (INV x) = inv (phi x). Admitted. + + Lemma homomorphism_div : forall x y, phi (DIV x y) = div (phi x) (phi y). + Proof. + intros. rewrite !field_div_definition. + rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse. reflexivity. + Qed. + End Homomorphism. +End Field. + +(*** Tactics for manipulating field equations *) +Require Import Coq.setoid_ring.Field_tac. + +Ltac guess_field := + match goal with + | |- ?eq _ _ => constr:(_:field (eq:=eq)) + | |- not (?eq _ _) => constr:(_:field (eq:=eq)) + | [H: ?eq _ _ |- _ ] => constr:(_:field (eq:=eq)) + | [H: not (?eq _ _) |- _] => constr:(_:field (eq:=eq)) + end. + +Ltac common_denominator := + let fld := guess_field in + lazymatch type of fld with + field (div:=?div) => + lazymatch goal with + | |- appcontext[div] => field_simplify_eq + | |- _ => idtac + end + end. + +Ltac common_denominator_in H := + let fld := guess_field in + lazymatch type of fld with + field (div:=?div) => + lazymatch type of H with + | appcontext[div] => field_simplify_eq in H + | _ => idtac + end + end. + +Ltac common_denominator_all := + common_denominator; + repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end. + +Inductive field_simplify_done {T} : T -> Type := + Field_simplify_done : forall H, field_simplify_done H. + +Ltac field_simplify_eq_hyps := + 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_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. + + +(*** Polynomial equations over fields *) + +Ltac neq01 := + try solve + [apply zero_neq_one + |apply Group.zero_neq_opp_one + |apply one_neq_zero + |apply Group.opp_one_neq_zero]. + +Ltac field_algebra := + intros; + common_denominator_all; + try (nsatz; dropRingSyntax); + repeat (apply conj); + try solve + [neq01 + |trivial + |apply Ring.opp_nonzero_nonzero;trivial]. + +Section Example. + Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. + Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "0" := zero. Local Notation "1" := one. + + Add Field _ExampleField : (Field.field_theory_for_stdlib_tactic (T:=F)). + + Example _example_nsatz x y : 1+1 <> 0 -> x + y = 0 -> x - y = 0 -> x = 0. + Proof. field_algebra. Qed. + + Example _example_field_nsatz x y z : y <> 0 -> x/y = z -> z*y + y = x + y. + Proof. field_algebra. Qed. + + Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0). + Proof. intros. intro. nsatz_contradict. Qed. +End Example. + +Section Z. + Require Import ZArith. + Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed. + + Global Instance commutative_ring_Z : @commutative_ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. eauto using @commutative_ring, @is_commutative, ring_Z with zarith. Qed. + + Global Instance integral_domain_Z : @integral_domain Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. + split. + { apply commutative_ring_Z. } + { constructor. intros. apply Z.neq_mul_0; auto. } + { constructor. discriminate. } + Qed. + + Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0). + Proof. intros. intro. nsatz_contradict. Qed. +End Z.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index f70479c3a..f9a866acb 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,47 +1,33 @@ 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. +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Crypto.Util.Tuple. 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) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q). + Infix "=" := eq : E_scope. + (* TODO: decide whether we still want something like this, then port Local Ltac t := unfold point_eqb; repeat match goal with @@ -94,207 +80,149 @@ 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. - Proof. - induction n; intros; auto. - rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity. - Qed. + Ltac bash := + repeat match goal with + | |- _ => progress intros + | [H: _ /\ _ |- _ ] => destruct H + | |- _ => progress destruct_points + | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in * + | |- _ => split + | |- Feq _ _ => field_algebra + | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto] + | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances + end. - 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. - Proof. - split. - + intro onCurve_x_y. - pose proof prime_q. - unfold E.onCurve in onCurve_x_y. - eapply F_div_mul; auto using (d_y2_a_nonzero y). - replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring. - rewrite F_sub_add_swap. - replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring. - rewrite onCurve_x_y. - ring. - + intro x2_eq. - unfold E.onCurve, solve_for_x2 in *. - rewrite x2_eq. - field. - auto using d_y2_a_nonzero. - Qed. - - - Program Definition opp (P:E.point) : E.point := let '(x, y) := proj1_sig P in (opp x, y). - Next Obligation. Proof. - pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. - rewrite F_square_opp; trivial. - Qed. - - Definition sub P Q := (P + opp Q)%E. - - Lemma opp_zero : opp E.zero = E.zero. - Proof. - pose proof @F_opp_0. - unfold opp, E.zero; eapply point_eq; congruence. - Qed. - - Lemma add_opp_r : forall P, (P + opp P = E.zero)%E. - Proof. - unfold opp; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]); - rewrite <-?@F_pow_2_r in *; - pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); - pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); - field_nonzero idtac. - Qed. - - Lemma add_opp_l : forall P, (opp P + P = E.zero)%E. - Proof. - intros. rewrite add_comm. eapply add_opp_r. - Qed. - - Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E. - Proof. - intros. - assert ((B + A) + opp A = (C + A) + opp A)%E as Hc by congruence. - rewrite <-!add_assoc, !add_opp_r, !add_0_r in Hc; exact Hc. - Qed. - - Lemma add_cancel_l : forall A B C, (A+B = A+C -> B = C)%E. - Proof. - intros. - rewrite (add_comm A C) in H. - rewrite (add_comm A B) in H. - eauto using add_cancel_r. - Qed. - - Lemma shuffle_eq_add_opp : forall P Q R, (P + Q = R <-> Q = opp P + R)%E. + 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). 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. } + bash. + (* 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 opp_opp : forall P, opp (opp P) = P. + + (* 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. - 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. + induction n; intros; + rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. Qed. - - Lemma opp_add : forall P Q, opp (P + Q)%E = (opp P + opp Q)%E. + Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%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. + induction n; intros; [reflexivity|]. + rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity. Qed. + 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. + Admitted. + + 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; simpl; intros; 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 + + Section Homomorphism. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} + {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} + {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. + 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 := (@point F Feq Fone Fadd Fmul Fa Fd). + Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd). + + Create HintDb field_homomorphism discriminated. + Hint Rewrite <- + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + Ha + Hd + : field_homomorphism. + + Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( + let (x, y) := coordinates P in (phi x, phi y)) _. + Next Obligation. + destruct P as [[? ?] ?]; simpl. + rewrite_strat bottomup hints field_homomorphism. + eauto using is_homomorphism_phi_proper; assumption. + Qed. + + Context {point_phi:Fpoint->Kpoint} + {point_phi_Proper:Proper (eq==>eq) point_phi} + {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. + + Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi. + Proof. + repeat match goal with + | |- Group.is_homomorphism => split + | |- _ => intro + | |- _ /\ _ => split + | [H: _ /\ _ |- _ ] => destruct H + | [p: point |- _ ] => destruct p as [[??]?] + | |- 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. + Qed. + End Homomorphism. +End E.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index e91bc084b..fe0e732a8 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,194 +1,154 @@ -Require Import Crypto.CompleteEdwardsCurve.Pre. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.FField. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Util.IterAssocOp BinNat NArith. -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Local Open Scope equiv_scope. -Local Open Scope F_scope. - -Section ExtendedCoordinates. - 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]). - - (** [extended] represents a point on an elliptic curve using extended projective - * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) - Record extended := mkExtended {extendedX : F q; - extendedY : F q; - extendedZ : F q; - extendedT : F q}. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). - - Definition twistedToExtended (P : (F q*F q)) : extended := - let '(x, y) := P in (x, y, 1, x*y). - Definition extendedToTwisted (P : extended) : F q * F q := - let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)). - Definition rep (P:extended) (rP:(F q*F q)) : Prop := - let '(X, Y, Z, T) := P in - extendedToTwisted P = rP /\ - Z <> 0 /\ - T = X*Y/Z. - Local Hint Unfold twistedToExtended extendedToTwisted rep. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Ltac unfoldExtended := - repeat progress (autounfold; unfold E.onCurve, E.add, E.add', rep in *; intros); - repeat match goal with - | [ p : (F q*F q)%type |- _ ] => - let x := fresh "x" p in - let y := fresh "y" p in - destruct p as [x y] - | [ p : extended |- _ ] => - let X := fresh "X" p in - let Y := fresh "Y" p in - let Z := fresh "Z" p in - let T := fresh "T" p in - destruct p as [X Y Z T] - | [ H: _ /\ _ |- _ ] => destruct H - | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H - | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H - end. - - Ltac solveExtended := unfoldExtended; - repeat match goal with - | [ |- _ /\ _ ] => split - | [ |- @eq (F q * F q)%type _ _] => apply f_equal2 - | _ => progress 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 - | _ => solve [eapply @Fq_1_neq_0; eauto with typeclass_instances] - | _ => solve [eauto with typeclass_instances] - | [ H: a = _ |- _ ] => rewrite H - end. - - Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P. - Proof. - solveExtended. - Qed. - - Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP. - Proof. - solveExtended. - Qed. - - Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }. - - Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended. - Next Obligation. - destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. - Qed. - - Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted. - Next Obligation. - destruct x; simpl; intuition. - Qed. - - Definition extendedPoint_eq P Q := unExtendedPoint P = unExtendedPoint Q. - Global Instance Equivalence_extendedPoint_eq : Equivalence extendedPoint_eq. - Proof. - repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. - Qed. - - Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P. - Proof. - destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. - Qed. - - Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint. - Proof. - repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. - Qed. - - Global Instance Proper_unExtendedPoint : Proper (equiv==>eq) unExtendedPoint. - Proof. - repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. - Qed. - - Definition twice_d := d + d. - - Section TwistMinus1. - Context (a_eq_minus1 : a = opp 1). - (** 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> *) - Definition unifiedAddM1' (P1 P2 : extended) : extended := - let '(X1, Y1, Z1, T1) := P1 in - let '(X2, Y2, Z2, T2) := P2 in - 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). - Local Hint Unfold E.add. - - Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). - - Lemma F_mul_2_l : forall x : F q, ZToField 2 * x = x + x. - intros. ring. - Qed. - - Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ). - Proof. - intros P Q rP rQ HoP HoQ HrP HrQ. - pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). - pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). - unfoldExtended; unfold twice_d; rewrite a_eq_minus1 in *; simpl in *. repeat rewrite <-F_mul_2_l. - repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto; - 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; - field_nonzero tnz. - Qed. - - Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q). - Proof. - intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto. - Qed. - - Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'. - Next Obligation. - destruct x, x0; simpl; intuition. - - erewrite extendedToTwisted_rep; eauto using unifiedAddM1'_rep. - - erewrite extendedToTwisted_rep. - (* It would be nice if I could use eauto here, but it gets evars wrong :( *) - 2: eapply unifiedAddM1'_rep. 5:apply H1. 4:apply H. 3:auto. 2:auto. - eauto using unifiedAdd'_onCurve. - Qed. - - Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). - Proof. - destruct P, Q; unfold unExtendedPoint, E.add, unifiedAddM1; eapply E.point_eq; simpl in *; intuition. - pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0)); - destruct (unifiedAddM1' x x0); - unfold rep in *; intuition. - Qed. - - Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1. - Proof. - repeat (econstructor || intro). - repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq. - rewrite <-!unifiedAddM1_rep. - destruct x, y, x0, y0; simpl in *; eapply E.point_eq; congruence. - Qed. +Require Export Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Algebra Crypto.Nsatz. +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 Relation_Definitions. +Require Import Crypto.Util.Tuple. + +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}. + 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 Epoint := (@E.point F Feq Fone Fadd Fmul a d). + Local Notation onCurve := (@Pre.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 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 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] + | _ => solve [etransitivity; eauto] + | |- Feq _ _ => field_algebra + | |- _ <> 0 => apply mul_nonzero_nonzero + | [ H : _ <> 0 |- _ <> 0 ] => + intro; apply H; + field_algebra; + solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2 + | apply E.char_gt_2] + end. + + 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 ((X/Z), (Y/Z))) _. + + Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). + + Local Hint Unfold from_twisted to_twisted eq : bash. + + Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; bash. Qed. + Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. bash. Qed. + Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. bash. Qed. + Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. Proof. bash. Qed. + + 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> *) + Definition add_coordinates P1 P2 : F*F*F*F := + let '(X1, Y1, Z1, T1) := P1 in + let '(X2, Y2, Z2, T2) := P2 in + 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). + + 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. + bash. + Qed. + + Obligation Tactic := idtac. + Program Definition add (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q). + Next Obligation. + intros. + pose proof (add_coordinates_correct P Q) as Hrep. + pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon. + 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 as Hnz1. + 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 as Hnz2. + autounfold with bash in *; simpl in *. + destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. + bash. + Qed. + Local Hint Unfold add : bash. + + Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)). + Proof. + pose proof (add_coordinates_correct P Q) as Hrep. + destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + autounfold with bash in *; simpl in *. + destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. + split; reflexivity. + Qed. + + 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 : @Group.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 : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted. + Proof. split; trivial using Proper_from_twisted, add_from_twisted. 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. @@ -210,30 +170,75 @@ Section ExtendedCoordinates. trivial. Qed. - Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint E.zero) N.testbit_nat. - Definition scalarMultM1_spec := - iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint E.zero) unifiedAddM1_0_l - N.testbit_nat (fun x => x) testbit_conversion_identity. - Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = E.mul n (unExtendedPoint P). - intros; rewrite scalarMultM1_spec, Nat2N.id; auto. - induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]. + 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. + + Section Homomorphism. + Import Group Ring Field. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} + {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Fprm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} + {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. + Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul phi}. + Context {phi_nonzero : forall x, ~ Feq x Fzero -> ~ Keq (phi x) Kzero}. + Context {HFa: Feq Fa (Fopp Fone)} {HKa:Keq Ka (Kopp Kone)}. + Context {Hd:Keq (phi Fd) Kd} {Kdd Fdd} {HKdd:Keq Kdd (Kadd Kd Kd)} {HFdd:Feq Fdd (Fadd Fd Fd)}. + Local Notation Fpoint := (@point F Feq Fzero Fone Fadd Fmul Fdiv Fa Fd). + Local Notation Kpoint := (@point K Keq Kzero Kone Kadd Kmul Kdiv Ka Kd). + + Lemma Ha : Keq (phi Fa) Ka. + Proof. rewrite HFa, HKa, <-homomorphism_one. eapply homomorphism_opp. Qed. + + Lemma Hdd : Keq (phi Fdd) Kdd. + Proof. rewrite HFdd, HKdd. rewrite homomorphism_add. repeat f_equiv; auto. Qed. + + Create HintDb field_homomorphism discriminated. + Hint Rewrite <- + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + Ha + Hd + Hdd + : field_homomorphism. + + Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( + let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _. + Next Obligation. + destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl. + rewrite_strat bottomup hints field_homomorphism. + eauto 10 using is_homomorphism_phi_proper, phi_nonzero. + Qed. + + Context {point_phi:Fpoint->Kpoint} + {point_phi_Proper:Proper (eq==>eq) point_phi} + {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. - End TwistMinus1. - - Definition negateExtended' P := let '(X, Y, Z, T) := P in (opp X, Y, Z, opp T). - Program Definition negateExtended (P:extendedPoint) : extendedPoint := negateExtended' (proj1_sig P). - Next Obligation. - Proof. - unfold negateExtended', rep; destruct P as [[X Y Z T] H]; simpl. destruct H as [[[] []] ?]; subst. - repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; repeat split; trivial. - Qed. - - Lemma negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P). - Proof. - unfold E.opp, unExtendedPoint, negateExtended; destruct P as [[]]; simpl; intros. - eapply E.point_eq; repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial. - Qed. -End ExtendedCoordinates. + Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi. + Proof. + repeat match goal with + | |- Group.is_homomorphism => split + | |- _ => intro + | |- _ /\ _ => split + | [H: _ /\ _ |- _ ] => destruct H + | [p: point |- _ ] => destruct p as [[[[] ?] ?] [? [? ?]]] + | |- context[point_phi] => setoid_rewrite point_phi_correct + | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates 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. + Qed. + End Homomorphism. +End Extended.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index f10e587d6..4744afe6b 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,188 +1,100 @@ -Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. -Require Import Coq.omega.Omega. - -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Local Open Scope Z_scope. -Local Open Scope F_scope. +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra Crypto.Nsatz. +Generalizable All Variables. Section Pre. - Context {q : BinInt.Z}. - Context {a : F q}. - Context {d : F q}. - Context {prime_q : Znumtheory.prime q}. - Context {two_lt_q : 2 < q}. - Context {a_nonzero : a <> 0}. - Context {a_square : exists sqrt_a, sqrt_a^2 = a}. - Context {d_nonsquare : forall x, x^2 <> d}. - - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - + 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)). + + 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}. + (* the canonical definitions are in Spec *) - Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). - Local Notation 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))) - ). - - Lemma char_gt_2 : ZToField 2 <> (0: F q). - intro; find_injection. - pose proof two_lt_q. - rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. - Qed. - - Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. - Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. - - Ltac whatsNotZero := - repeat match goal with - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: (?a^?p)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - let Y:=fresh in let Z:=fresh in try ( - assert (p <> 0%N) as Z by (intro Y; inversion Y); - assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0); - clear Z) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) - end. + 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))). + + Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. 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. - intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero. - - 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 - 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. + unfold onCurve, not; use_sqrt_a; intros. + 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) |- _ ] + => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) + /(f (sqrt_a * x2) y2 * x1 * y1 )) + | _ => apply a_nonzero + end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 + d*x1*x2*y1*y2) <> 0. - Proof. - intros Hc1 Hc2; simpl in Hc1, Hc2. - intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field. - intro Hz; rewrite Hz in H; intuition. - Qed. - + onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 - d*x1*x2*y1*y2) <> 0. + onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. + + Lemma unifiedAdd'_onCurve : forall P1 P2, + onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. - intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field. - intro Hz; rewrite Hz in H; apply H; field. - Qed. - - Definition zeroOnCurve : onCurve (0, 1). - simpl. field. - Qed. - - Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 - (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : - onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). - Proof. - (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; - * c=1 and an extra a in front of x^2 *) - - injection H; cbv beta iota; clear H; intros. - - Ltac t x1 y1 x2 y2 := - assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 - = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); - assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 - = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). - t x1 y1 x2 y2; t x2 y2 x1 y1. - - remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - - (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. - assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). - assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( - (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * - y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). - replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. - - match goal with [ |- ?x = 1 ] => replace x with - ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + - ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end. - - rewrite <-HT1, <-HT2; field; rewrite HT1. - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field. - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. - - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. + unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. + field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. Qed. +End Pre. - Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> - onCurve (unifiedAdd' P1 P2). +Import Group Ring Field. + +(* TODO: move -- this does not need to be defined before [point] *) +Section RespectsFieldHomomorphism. + Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. + Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Context {phi:F->K} `{@is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}. + Context {A D:F} {a d:K} {a_ok:phi A=a} {d_ok:phi D=d}. + + Let phip := fun (P':F*F) => let (x, y) := P' in (phi x, phi y). + + Let eqp := fun (P1' P2':K*K) => + let (x1, y1) := P1' in + let (x2, y2) := P2' in + and (eq x1 x2) (eq y1 y2). + + Create HintDb field_homomorphism discriminated. + Hint Rewrite + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + a_ok + d_ok + : field_homomorphism. + + Lemma morphism_unidiedAdd' : forall P Q:F*F, + eqp + (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q)) + (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)). Proof. - intros; destruct P1, P2. - remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. - eapply unifiedAdd'_onCurve'; eauto. + intros [x1 y1] [x2 y2]. + cbv [unifiedAdd' phip eqp]; + apply conj; + (rewrite_strat topdown hints field_homomorphism); reflexivity. Qed. -End Pre. +End RespectsFieldHomomorphism.
\ No newline at end of file diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v index dba71b49c..2e45bcad5 100644 --- a/src/EdDSAProofs.v +++ b/src/EdDSAProofs.v @@ -75,4 +75,34 @@ Section EdDSAProofs. Proof. unfold verify, sign, public; arith; try break_if; intuition. Qed. + + (* This is just an experiment, talk to andreser if you think this is a good idea *) + Inductive valid {n:nat} : word b -> Word.word n -> word (b+b) -> Prop := + Valid : forall (A:E.point) (M:Word.word n) (S:nat) (R:E.point), + (S * B = R + (H (enc R ++ enc A ++ M)) * A)%E + -> valid (enc A) M (enc R ++ enc (ZToField (BinInt.Z.of_nat S))). + Goal forall A_ {n} (M:Word.word n) sig, verify A_ M sig = true <-> valid A_ M sig. + split; unfold verify. + Focus 2. { + intros. + inversion H. subst. + rewrite !Word.split2_combine, !Word.split1_combine, !encoding_valid. + rewrite FieldToZ_ZToField. + rewrite <-Zdiv.mod_Zmod by admit. + rewrite Znat.Nat2Z.id. + rewrite <-H0. + assert ((S mod l) * B = S * B)%E as Hl by admit; rewrite Hl. + destruct (E.point_eq_dec (S * B)%E); congruence. + } Unfocus. { + repeat match goal with |- context [match ?x with _ => _ end] => case_eq x; intro end; try congruence. + intros. clear H. + repeat match goal with [H: _ |- _ ] => apply encoding_canonical in H end; subst. + rewrite <-(Word.combine_split b b sig). + rewrite <-H0 in *; clear H0. rewrite <-H2 in *; clear H2. + assert (f = (ZToField (BinInt.Z.of_nat (BinInt.Z.to_nat (FieldToZ f))))) as H1. { + rewrite Znat.Z2Nat.id by admit. rewrite ZToField_FieldToZ; reflexivity. } + rewrite H1; clear H1. + econstructor; trivial. + } + Qed. End EdDSAProofs. diff --git a/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v b/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v new file mode 100644 index 000000000..146059ca4 --- /dev/null +++ b/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v @@ -0,0 +1,376 @@ +Require Import Bedrock.Word. +Require Import Crypto.Spec.EdDSA. +Require Import Crypto.Tactics.VerdiTactics. +Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. +Require Import ModularArithmetic.ModularArithmeticTheorems. +Require Import ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. +Require Import Zdiv. +Require Import Crypto.Util.Tuple. +Local Open Scope equiv_scope. + +Generalizable All Variables. + + +Local Ltac set_evars := + repeat match goal with + | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) + end. + +Local Ltac subst_evars := + repeat match goal with + | [ e := ?E |- _ ] => is_evar E; subst e + end. + +Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)} + {HP:Proper (RA==>Basics.impl) P} + (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py)) + (x : @sig A P) (y0:A) (pf : RA (proj1_sig x) y0) +: Rsig x (exist _ y0 (HP _ _ pf (proj2_sig x))). +Proof. destruct x. eapply H. assumption. Defined. + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. +Global Instance Let_In_Proper_changebody {A P R} {Reflexive_R:@Reflexive P R} + : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). +Proof. + lazy; intros; try congruence. + subst; auto. +Qed. + +Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f} + : Proper (RA ==> RB) (fun x => Let_In x f). +Proof. intuition. Qed. + +Ltac fold_identity_lambdas := + repeat match goal with + | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in * + | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in * + end. + +Local Ltac replace_let_in_with_Let_In := + match goal with + | [ |- context G[let x := ?y in @?z x] ] + => let G' := context G[Let_In y z] in change G' + end. + +Local Ltac Let_In_app fn := + match goal with + | [ |- appcontext G[Let_In (fn ?x) ?f] ] + => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn y))); cbv beta + end. + +Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). +Proof. + destruct b; trivial. +Qed. + +Lemma pull_Let_In {B C} (f : B -> C) A (v : A) (b : A -> B) + : Let_In v (fun v' => f (b v')) = f (Let_In v b). +Proof. + reflexivity. +Qed. + +Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : + @Let_In _ (fun _ => T) (g x) f = + @Let_In _ (fun _ => T) x (fun p => f (g x)). +Proof. reflexivity. Qed. + +Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R} + (g : A -> B) (f : B -> T) (x : A) + f' (f'_ok: forall z, f' z === f (g z)), + Let_In (g x) f === Let_In x f'. +Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed. +Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl. + +Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) : + @Let_In _ (fun _ => T) (g1 x, g2 y) f = + @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))). +Proof. reflexivity. Qed. + +Lemma funexp_proj {T T'} `{@Equivalence T' RT'} + (proj : T -> T') + (f : T -> T) + (f' : T' -> T') {Proper_f':Proper (RT'==>RT') f'} + (f_proj : forall a, proj (f a) === f' (proj a)) + x n + : proj (funexp f x n) === funexp f' (proj x) n. +Proof. + revert x; induction n as [|n IHn]; simpl; intros. + - reflexivity. + - rewrite f_proj. rewrite IHn. reflexivity. +Qed. + +Global Instance pair_Equivalence {A B} `{@Equivalence A RA} `{@Equivalence B RB} : @Equivalence (A*B) (fun x y => fst x = fst y /\ snd x === snd y). +Proof. + constructor; repeat intro; intuition; try congruence. + match goal with [H : _ |- _ ] => solve [rewrite H; auto] end. +Qed. + +Global Instance Proper_test_and_op {T scalar} `{Requiv:@Equivalence T RT} + {op:T->T->T} {Proper_op:Proper (RT==>RT==>RT) op} + {testbit:scalar->nat->bool} {s:scalar} {zero:T} : + let R := fun x y => fst x = fst y /\ snd x === snd y in + Proper (R==>R) (test_and_op op testbit s zero). +Proof. + unfold test_and_op; simpl; repeat intro; intuition; + repeat match goal with + | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:?; simpl in *; subst; try discriminate; auto + | [ H: _ |- _ ] => setoid_rewrite H; reflexivity + end. +Qed. + +Lemma iter_op_proj {T T' S} `{T'Equiv:@Equivalence T' RT'} + (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') {Proper_op':Proper (RT' ==> RT' ==> RT') op'} x y z + (testbit : S -> nat -> bool) (bound : nat) + (op_proj : forall a b, proj (op a b) === op' (proj a) (proj b)) + : proj (iter_op op x testbit y z bound) === iter_op op' (proj x) testbit y (proj z) bound. +Proof. + unfold iter_op. + lazymatch goal with + | [ |- ?proj (snd (funexp ?f ?x ?n)) === snd (funexp ?f' _ ?n) ] + => pose proof (fun pf x0 x1 => @funexp_proj _ _ _ _ (fun x => (fst x, proj (snd x))) f f' (Proper_test_and_op (Requiv:=T'Equiv)) pf (x0, x1)) as H'; + lazymatch type of H' with + | ?H'' -> _ => assert (H'') as pf; [clear H'|edestruct (H' pf); simpl in *; solve [eauto]] + end + end. + + intros [??]; simpl. + repeat match goal with + | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:? + | _ => progress (unfold equiv; simpl) + | _ => progress (subst; intuition) + | _ => reflexivity + | _ => rewrite op_proj + end. +Qed. + +Global Instance option_rect_Proper_nd {A T} + : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)). +Proof. + intros ?? H ??? [|]??; subst; simpl; congruence. +Qed. + +Global Instance option_rect_Proper_nd' {A T} + : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)). +Proof. + intros ?? H ??? [|]; subst; simpl; congruence. +Qed. + +Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances. + +Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v, + option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v). +Proof. + destruct v; reflexivity. +Qed. + +Lemma option_rect_function {A B C S' N' v} f + : f (option_rect (fun _ : option A => option B) S' N' v) + = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v. +Proof. destruct v; reflexivity. Qed. +Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *) + idtac; + lazymatch goal with + | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ] + => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *) + cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta; + [ set_evars; + let H := fresh in + intro H; + rewrite H; + clear; + abstract (cbv [Let_In]; reflexivity) + | ] + end. + +(** TODO: possibly move me, remove local *) +Local Ltac replace_option_match_with_option_rect := + idtac; + lazymatch goal with + | [ |- _ = ?RHS :> ?T ] + => lazymatch RHS with + | match ?a with None => ?N | Some x => @?S x end + => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity) + end + end. +Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *) + repeat match goal with + | [ |- context[option_rect ?P ?S ?N None] ] + => change (option_rect P S N None) with N + | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] + => change (option_rect P S N (Some x)) with (S x); cbv beta + end. + +Definition COMPILETIME {T} (x:T) : T := x. + +Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat. +Proof. + intros. + pose proof (Nomega.Nlt_out a (N.succ b)). + rewrite N2Nat.inj_succ, N.lt_succ_r, <-NPeano.Nat.lt_succ_r in *; auto. +Qed. +Lemma N_size_nat_le_mono : forall a b, (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. +Proof. + intros. + destruct (N.eq_dec a 0), (N.eq_dec b 0); try abstract (subst;rewrite ?N.le_0_r in *;subst;simpl;omega). + rewrite !Nsize_nat_equiv, !N.size_log2 by assumption. + edestruct N.succ_le_mono; eauto using N_to_nat_le_mono, N.log2_le_mono. +Qed. + +Lemma Z_to_N_Z_of_nat : forall n, Z.to_N (Z.of_nat n) = N.of_nat n. +Proof. induction n; auto. Qed. + +Lemma Z_of_nat_nonzero : forall m, m <> 0 -> (0 < Z.of_nat m)%Z. +Proof. intros. destruct m; [congruence|reflexivity]. Qed. + +Local Infix "mod" := NPeano.modulo : nat_scope. +Lemma N_of_nat_modulo : forall n m, m <> 0 -> N.of_nat (n mod m)%nat = (N.of_nat n mod N.of_nat m)%N. +Proof. + intros. + apply Znat.N2Z.inj_iff. + rewrite !Znat.nat_N_Z. + rewrite Zdiv.mod_Zmod by auto. + apply Znat.Z2N.inj_iff. + { apply Z.mod_pos_bound. apply Z_of_nat_nonzero. assumption. } + { apply Znat.N2Z.is_nonneg. } + rewrite Znat.Z2N.inj_mod by (auto using Znat.Nat2Z.is_nonneg, Z_of_nat_nonzero). + rewrite !Z_to_N_Z_of_nat, !Znat.N2Z.id; reflexivity. +Qed. + +Lemma encoding_canonical' {T} {B} {encoding:canonical encoding of T as B} : + forall a b, enc a = enc b -> a = b. +Proof. + intros. + pose proof (f_equal dec H). + pose proof encoding_valid. + pose proof encoding_canonical. + congruence. +Qed. + +Lemma compare_encodings {T} {B} {encoding:canonical encoding of T as B} + (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b) + : forall a b : T, (a = b) <-> (B_eqb (enc a) (enc b) = true). +Proof. + intros. + split; intro H. + { rewrite B_eqb_iff; congruence. } + { apply B_eqb_iff in H; eauto using encoding_canonical'. } +Qed. + +Lemma eqb_eq_dec' {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b, if eqb a b then a = b else a <> b. +Proof. + intros. + case_eq (eqb a b); intros. + { eapply eqb_iff; trivial. } + { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition. } +Qed. + +Definition eqb_eq_dec {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b : T, {a=b}+{a<>b}. +Proof. + intros. + pose proof (eqb_eq_dec' eqb eqb_iff a b). + destruct (eqb a b); eauto. +Qed. + +Definition eqb_eq_dec_and_output {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b : T, {a = b /\ eqb a b = true}+{a<>b /\ eqb a b = false}. +Proof. + intros. + pose proof (eqb_eq_dec' eqb eqb_iff a b). + destruct (eqb a b); eauto. +Qed. + +Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B} + (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b) + (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b) + : forall a b : T, T_eqb a b = B_eqb (enc a) (enc b). +Proof. + intros; + destruct (eqb_eq_dec_and_output T_eqb T_eqb_iff a b); + destruct (eqb_eq_dec_and_output B_eqb B_eqb_iff (enc a) (enc b)); + intuition; + try find_copy_apply_lem_hyp B_eqb_iff; + try find_copy_apply_lem_hyp T_eqb_iff; + try congruence. + apply (compare_encodings B_eqb B_eqb_iff) in H2; congruence. +Qed. + +Lemma decode_failed_neq_encoding {T B} (encoding_T_B:canonical encoding of T as B) (X:B) + (dec_failed:dec X = None) (a:T) : X <> enc a. +Proof. pose proof encoding_valid. congruence. Qed. +Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B) + (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b) + (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b) + (P_:B) (Q:T) : + option_rect (fun _ : option T => bool) + (fun P : T => T_eqb P Q) + false + (dec P_) + = B_eqb P_ (enc Q). +Proof. + destruct (dec P_) eqn:Hdec; simpl option_rect. + { apply encoding_canonical in Hdec; subst; auto using eqb_compare_encodings. } + { pose proof encoding_canonical. + pose proof encoding_valid. + pose proof eqb_compare_encodings. + eapply decode_failed_neq_encoding in Hdec. + destruct (B_eqb P_ (enc Q)) eqn:Heq; [rewrite B_eqb_iff in Heq; eauto | trivial]. } +Qed. + +Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + +Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x). +Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed. + +Definition natToField {m} x : F m := ZToField (Z.of_nat x). +Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x). +Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x). + unfold natToField, FieldToNat; intros. + rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial. +Qed. + +Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. +Proof. + split; eauto using F_eqb_eq, F_eqb_complete. +Qed. + +Section FSRepOperations. + Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. + Context {l:Z} {two_lt_l:(2 < l)%Z}. + Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}. + Context `(rcF:RepConversions (F q) FRep) (rcFOK:RepConversionsOK rcF). + Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul). + Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul). + Axiom SRep_testbit : SRep -> nat -> bool. + Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i. + + Definition FSRepPow width x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x width. + Lemma FSRepPow_correct : forall width x n, (N.size_nat (FieldToN (unRep n)) <= width)%nat -> (unRep x ^ FieldToN (unRep n))%F = unRep (FSRepPow width x n). + Proof. (* this proof derives the required formula, which I copy-pasted above to be able to reference it without the length precondition *) + unfold FSRepPow; intros. + erewrite <-pow_nat_iter_op_correct by auto. + erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ _ SRep_testbit_correct n x width) by auto. + rewrite <-(rcFOK 1%F) at 1. + erewrite <-iter_op_proj; + [apply eq_refl + |eauto with typeclass_instances + |symmetry; eapply FRepMul_correct]. + Qed. + + Context (q_minus_2_lt_l:(q - 2 < l)%Z). + Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (ZToField (q - 2)))). + Lemma FRepInv_correct : forall x, inv (unRep x)%F = unRep (FRepInv x). + unfold FRepInv, COMPILETIME; intros. + rewrite <-FSRepPow_correct; rewrite FieldToN_correct, rcSOK, FieldToZ_ZToField, Zmod_small by omega; trivial. + pose proof @Fq_inv_fermat_correct as Hf; unfold inv_fermat in Hf; rewrite Hf by + auto using prime_q, two_lt_q. + reflexivity. + Qed. +End FSRepOperations.
\ No newline at end of file diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v new file mode 100644 index 000000000..884a9fe5c --- /dev/null +++ b/src/Experiments/GenericFieldPow.v @@ -0,0 +1,336 @@ +Require Import Coq.setoid_ring.Cring. +Generalizable All Variables. + + +(*TODO: move *) +Lemma Z_pos_pred_0 p : Z.pos p - 1 = 0 -> p=1%positive. +Proof. destruct p; simpl in *; try discriminate; auto. Qed. + +Lemma Z_neg_succ_neg : forall a b, (Z.neg a + 1)%Z = Z.neg b -> a = Pos.succ b. +Admitted. + +Lemma Z_pos_pred_pos : forall a b, (Z.pos a - 1)%Z = Z.pos b -> a = Pos.succ b. +Admitted. + +Lemma Z_pred_neg p : (Z.neg p - 1)%Z = Z.neg (Pos.succ p). +Admitted. + +(* teach nsatz to deal with the definition of power we are use *) +Instance reify_pow_pos (R:Type) `{Ring R} +e1 lvar t1 n +`{Ring (T:=R)} +{_:reify e1 lvar t1} +: reify (PEpow e1 (N.pos n)) lvar (pow_pos t1 n)|1. + +Class Field_ops (F:Type) + `{Ring_ops F} + {inv:F->F} := {}. + +Class Division (A B C:Type) := division : A -> B -> C. + +Local Notation "_/_" := division. +Local Notation "n / d" := (division n d). + +Module F. + + Definition div `{Field_ops F} n d := n * (inv d). + Global Instance div_notation `{Field_ops F} : @Division F F F := div. + + Class Field {F inv} `{FieldCring:Cring (R:=F)} {Fo:Field_ops F (inv:=inv)} := + { + field_inv_comp : Proper (_==_ ==> _==_) inv; + field_inv_def : forall x, (x == 0 -> False) -> inv x * x == 1; + field_one_neq_zero : not (1 == 0) + }. + Global Existing Instance field_inv_comp. + + Definition powZ `{Field_ops F} (x:F) (n:Z) := + match n with + | Z0 => 1 + | Zpos p => pow_pos x p + | Zneg p => inv (pow_pos x p) + end. + Global Instance power_field `{Field_ops F} : Power | 5 := { power := powZ }. + + Section FieldProofs. + Context `{Field F}. + + Definition unfold_div (x y:F) : x/y = x * inv y := eq_refl. + + Global Instance Proper_div : + Proper (_==_ ==> _==_ ==> _==_) div. + Proof. + unfold div; repeat intro. + repeat match goal with + | [H: _ == _ |- _ ] => rewrite H; clear H + end; reflexivity. + Qed. + + Global Instance Proper_pow_pos : Proper (_==_==>eq==>_==_) pow_pos. + Proof. + cut (forall n (y x : F), x == y -> pow_pos x n == pow_pos y n); + [repeat intro; subst; eauto|]. + induction n; simpl; intros; trivial; + repeat eapply ring_mult_comp; eauto. + Qed. + + Global Instance Propper_powZ : Proper (_==_==>eq==>_==_) powZ. + Proof. + repeat intro; subst; unfold powZ. + match goal with |- context[match ?x with _ => _ end] => destruct x end; + repeat (eapply Proper_pow_pos || f_equiv; trivial). + Qed. + + Require Import Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. + Lemma field_theory_for_tactic : field_theory 0 1 _+_ _*_ _-_ -_ _/_ inv _==_. + Proof. + split; repeat constructor; repeat intro; gen_rewrite; try cring; + eauto using field_one_neq_zero, field_inv_def. Qed. + + Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.NArithRing. + Lemma power_theory_for_tactic : power_theory 1 _*_ _==_ NtoZ power. + Proof. constructor; destruct n; reflexivity. Qed. + + Create HintDb field_nonzero discriminated. + Hint Resolve field_one_neq_zero : field_nonzero. + Ltac field_nonzero := repeat split; auto 3 with field_nonzero. + Ltac field_power_isconst t := Ncst t. + Add Field FieldProofsAddField : field_theory_for_tactic + (postprocess [field_nonzero], + power_tac power_theory_for_tactic [field_power_isconst]). + + Lemma div_mul_idemp_l : forall a b, (a==0 -> False) -> a*b/a == b. + Proof. intros. field. Qed. + + Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}. + Lemma mul_zero_why : forall a b, a*b == 0 -> a == 0 \/ b == 0. + intros; destruct (eq_dec a 0); intuition. + assert (a * b / a == 0) by + (match goal with [H: _ == _ |- _ ] => rewrite H; field end). + rewrite div_mul_idemp_l in *; auto. + Qed. + + Require Import Coq.nsatz.Nsatz. + Global Instance Integral_domain_Field : Integral_domain (R:=F). + Proof. + constructor; intros; eauto using mul_zero_why, field_one_neq_zero. + Qed. + + Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := + let t := type of H in + generalize H; + field_lookup (PackField FIELD_SIMPL_EQ) [] t; + try (exact I); + try (idtac; []; clear H;intro H). + + Require Import Util.Tactics. + Inductive field_simplify_done {x y:F} : (x==y) -> Type := + Field_simplify_done : forall (H:x==y), field_simplify_done H. + Ltac field_nsatz := + repeat match goal with + [ H: (_:F) == _ |- _ ] => + 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; + try field_simplify_eq; + try nsatz. + + Create HintDb field discriminated. + Hint Extern 5 (_ == _) => field_nsatz : field. + Hint Extern 5 (_ <-> _) => split. + + Lemma mul_inv_l : forall x, not (x == 0) -> inv x * x == 1. Proof. auto with field. Qed. + + Lemma mul_inv_r : forall x, not (x == 0) -> x * inv x == 1. Proof. auto with field. Qed. + + Lemma mul_cancel_r' (x y z:F) : not (z == 0) -> x * z == y * z -> x == y. + Proof. + intros. + assert (x * z * inv z == y * z * inv z) by + (match goal with [H: _ == _ |- _ ] => rewrite H; auto with field end). + assert (x * z * inv z == x * (z * inv z)) by auto with field. + assert (y * z * inv z == y * (z * inv z)) by auto with field. + rewrite mul_inv_r, @ring_mul_1_r in *; auto with field. + Qed. + + Lemma mul_cancel_r (x y z:F) : not (z == 0) -> (x * z == y * z <-> x == y). + Proof. intros;split;intros Heq; try eapply mul_cancel_r' in Heq; eauto with field. Qed. + + Lemma mul_cancel_l (x y z:F) : not (z == 0) -> (z * x == z * y <-> x == y). + Proof. intros;split;intros; try eapply mul_cancel_r; eauto with field. Qed. + + Lemma mul_cancel_r_eq : forall x z:F, not(z==0) -> (x*z == z <-> x == 1). + Proof. + intros;split;intros Heq; [|nsatz]. + pose proof ring_mul_1_l z as Hz; rewrite <- Hz in Heq at 2; rewrite mul_cancel_r in Heq; eauto. + Qed. + + Lemma mul_cancel_l_eq : forall x z:F, not(z==0) -> (z*x == z <-> x == 1). + Proof. intros;split;intros Heq; try eapply mul_cancel_r_eq; eauto with field. Qed. + + Lemma inv_unique (a:F) : forall x y, x * a == 1 -> y * a == 1 -> x == y. Proof. auto with field. Qed. + + Lemma mul_nonzero_nonzero (a b:F) : not (a == 0) -> not (b == 0) -> not (a*b == 0). + Proof. intros; intro Hab. destruct (mul_zero_why _ _ Hab); auto. Qed. + Hint Resolve mul_nonzero_nonzero : field_nonzero. + + Lemma inv_nonzero (x:F) : not(x == 0) -> not(inv x==0). + Proof. + intros Hx Hi. + assert (Hc:not (inv x*x==0)) by (rewrite field_inv_def; auto with field_nonzero); contradict Hc. + ring [Hi]. + Qed. + Hint Resolve inv_nonzero : field_nonzero. + + Lemma div_nonzero (x y:F) : not(x==0) -> not(y==0) -> not(x/y==0). + Proof. + unfold division, div_notation, div; auto with field_nonzero. + Qed. + Hint Resolve div_nonzero : field_nonzero. + + Lemma pow_pos_nonzero (x:F) p : not(x==0) -> not(Ncring.pow_pos x p == 0). + Proof. + intros; induction p using Pos.peano_ind; try assumption; []. + rewrite Ncring.pow_pos_succ; eauto using mul_nonzero_nonzero. + Qed. + Hint Resolve pow_pos_nonzero : field_nonzero. + + Lemma sub_diag_iff (x y:F) : x - y == 0 <-> x == y. Proof. auto with field. Qed. + + Lemma mul_same (x:F) : x*x == x^2%Z. Proof. auto with field. Qed. + + Lemma inv_mul (x y:F) : not(x==0) -> not (y==0) -> inv (x*y) == inv x * inv y. + Proof. intros;field;intuition. Qed. + + Lemma pow_0_r (x:F) : x^0 == 1. Proof. auto with field. Qed. + Lemma pow_1_r : forall x:F, x^1%Z == x. Proof. auto with field. Qed. + Lemma pow_2_r : forall x:F, x^2%Z == x*x. Proof. auto with field. Qed. + Lemma pow_3_r : forall x:F, x^3%Z == x*x*x. Proof. auto with field. Qed. + + Lemma pow_succ_r (x:F) (n:Z) : not (x==0)\/(n>=0)%Z -> x^(n+1) == x * x^n. + Proof. + intros Hnz; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. + - simpl; ring. + - setoid_rewrite <-Pos2Z.inj_succ; rewrite Ncring.pow_pos_succ; ring. + - destruct (Z.succ (Z.neg p)) eqn:Hn. + + assert (p=1%positive) by (destruct p; simpl in *; try discriminate; auto). + subst; simpl in *; field. destruct Hnz; auto with field_nonzero. + + destruct p, p0; discriminate. + + setoid_rewrite Hn. + apply Z_neg_succ_neg in Hn; subst. + rewrite Ncring.pow_pos_succ; field; + destruct Hnz; auto with field_nonzero. + Qed. + + Lemma pow_pred_r (x:F) (n:Z) : not (x==0) -> x^(n-1) == x^n/x. + Proof. + intros; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. + - simpl. rewrite unfold_div; field. + - destruct (Z.pos p - 1) eqn:Hn. + + apply Z_pos_pred_0 in Hn; subst; simpl; field. + + apply Z_pos_pred_pos in Hn; subst. + rewrite Ncring.pow_pos_succ; field; auto with field_nonzero. + + destruct p; discriminate. + - rewrite Z_pred_neg, Ncring.pow_pos_succ; field; auto with field_nonzero. + Qed. + + Local Ltac pow_peano := + repeat (setoid_rewrite pow_0_r + || setoid_rewrite pow_succ_r + || setoid_rewrite pow_pred_r). + + Lemma pow_mul (x y:F) : forall (n:Z), not(x==0)/\not(y==0)\/(n>=0)%Z -> (x * y)^n == x^n * y^n. + Proof. + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. + { repeat intro. subst. reflexivity. } + - intros; cbv [power power_field powZ]; ring. + - intros n Hn IH Hxy. + repeat setoid_rewrite pow_succ_r; try rewrite IH; try ring; (right; omega). + - intros n Hn IH Hxy. destruct Hxy as [[]|?]; try omega; []. + repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; auto with field_nonzero. + Qed. + + Lemma pow_nonzero (x:F) : forall (n:Z), not(x==0) -> not(x^n==0). + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; pow_peano; + auto with field_nonzero. + { repeat intro. subst. reflexivity. } + Qed. + Hint Resolve pow_nonzero : field_nonzero. + + Lemma pow_inv (x:F) : forall (n:Z), not(x==0) -> inv x^n == inv (x^n). + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. + { repeat intro. subst. reflexivity. } + - intros; cbv [power power_field powZ]. field. + - intros n Hn IH Hx. + repeat setoid_rewrite pow_succ_r; try rewrite IH; try field; auto with field_nonzero. + - intros n Hn IH Hx. + repeat setoid_rewrite pow_pred_r; try rewrite IH; try field; auto 3 with field_nonzero. + Qed. + + Lemma pow_0_l : forall n, (n>0)%Z -> (0:F)^n==0. + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; try omega. + { repeat intro. subst. reflexivity. } + setoid_rewrite pow_succ_r; [auto with field|right;omega]. + Qed. + + Lemma pow_div (x y:F) (n:Z) : not (y==0) -> not(x==0)\/(n >= 0)%Z -> (x/y)^n == x^n/y^n. + Proof. + intros Hy Hxn. unfold division, div_notation, div. + rewrite pow_mul, pow_inv; try field; destruct Hxn; auto with field_nonzero. + Qed. + + Hint Extern 3 (_ >= _)%Z => omega : field_nonzero. + Lemma issquare_mul (x y z:F) : not (y == 0) -> x^2%Z == z * y^2%Z -> (x/y)^2%Z == z. + Proof. intros. rewrite pow_div by (auto with field_nonzero); auto with field. Qed. + + Lemma issquare_mul_sub (x y z:F) : 0 == z*y^2%Z - x^2%Z -> (x/y)^2%Z == z \/ x == 0. + Proof. destruct (eq_dec y 0); [right|left]; auto using issquare_mul with field. Qed. + + Lemma div_mul : forall x y z : F, not(y==0) -> (z == (x / y) <-> z * y == x). + Proof. auto with field. Qed. + + Lemma div_1_r : forall x : F, x/1 == x. + Proof. auto with field. Qed. + + Lemma div_1_l : forall x : F, not(x==0) -> 1/x == inv x. + Proof. auto with field. Qed. + + Lemma div_opp_l : forall x y, not (y==0) -> (-_ x) / y == -_ (x / y). + Proof. auto with field. Qed. + + Lemma div_opp_r : forall x y, not (y==0) -> x / (-_ y) == -_ (x / y). + Proof. auto with field. Qed. + + Lemma eq_opp_zero : forall x : F, (~ 1 + 1 == (0:F)) -> (x == -_ x <-> x == 0). + Proof. auto with field. Qed. + + Lemma add_cancel_l : forall x y z:F, z+x == z+y <-> x == y. + Proof. auto with field. Qed. + + Lemma add_cancel_r : forall x y z:F, x+z == y+z <-> x == y. + Proof. auto with field. Qed. + + Lemma add_cancel_r_eq : forall x z:F, x+z == z <-> x == 0. + Proof. auto with field. Qed. + + Lemma add_cancel_l_eq : forall x z:F, z+x == z <-> x == 0. + Proof. auto with field. Qed. + + Lemma sqrt_solutions : forall x y:F, y ^ 2%Z == x ^ 2%Z -> y == x \/ y == -_ x. + Proof. + intros ? ? squares_eq. + remember (y - x) as z eqn:Heqz. + assert (y == x + z) as Heqy by (subst; ring); rewrite Heqy in *; clear Heqy Heqz. + assert (Hw:(x + z)^2%Z == z * (x + (x + z)) + x^2%Z) + by (auto with field); rewrite Hw in squares_eq; clear Hw. + rewrite add_cancel_r_eq in squares_eq. + apply mul_zero_why in squares_eq; destruct squares_eq; auto with field. + Qed. + + End FieldProofs. +End F.
\ No newline at end of file diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v deleted file mode 100644 index 4f2b623e0..000000000 --- a/src/ModularArithmetic/FField.v +++ /dev/null @@ -1,63 +0,0 @@ -Require Export Crypto.Spec.ModularArithmetic. -Require Export Coq.setoid_ring.Field. - -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. - -Local Open Scope F_scope. - -Definition OpaqueF := F. -Definition OpaqueZmodulo := BinInt.Z.modulo. -Definition Opaqueadd {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @add p. -Definition Opaquemul {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @mul p. -Definition Opaquesub {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @sub p. -Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p. -Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p. -Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p. -Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p. -Definition Opaqueadd_correct {p} : @Opaqueadd p = @add p := eq_refl. -Definition Opaquesub_correct {p} : @Opaquesub p = @sub p := eq_refl. -Definition Opaquemul_correct {p} : @Opaquemul p = @mul p := eq_refl. -Definition Opaquediv_correct {p} : @Opaquediv p = @div p := eq_refl. -Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField. - -Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p. - -Ltac FIELD_SIMPL_idtac FLD lH rl := - let Simpl := idtac (* (protect_fv "field") *) in - let lemma := get_SimplifyEqLemma FLD in - get_FldPre FLD (); - Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH; - get_FldPost FLD (). -Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G. - -Ltac F_to_Opaque := - change F with OpaqueF in *; - change BinInt.Z.modulo with OpaqueZmodulo in *; - change @add with @Opaqueadd in *; - change @mul with @Opaquemul in *; - change @sub with @Opaquesub in *; - change @div with @Opaquediv in *; - change @opp with @Opaqueopp in *; - change @inv with @Opaqueinv in *; - change @ZToField with @OpaqueZToField in *. - -Ltac F_from_Opaque p := - change OpaqueF with F in *; - change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *; - change OpaqueZmodulo with BinInt.Z.modulo in *; - change @Opaqueopp with @opp in *; - change @Opaqueinv with @inv in *; - change @OpaqueZToField with @ZToField in *; - rewrite ?@Opaqueadd_correct, ?@Opaquesub_correct, ?@Opaquemul_correct, ?@Opaquediv_correct in *. - -Ltac F_field_simplify_eq := - lazymatch goal with |- @eq (F ?p) _ _ => - F_to_Opaque; - field_simplify_eq_idtac; - compute; - F_from_Opaque p - end. - -Ltac F_field := F_field_simplify_eq; [ring|..]. - -Ltac notConstant t := constr:NotConstant. diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v deleted file mode 100644 index 221b8d799..000000000 --- a/src/ModularArithmetic/FNsatz.v +++ /dev/null @@ -1,40 +0,0 @@ -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Export Crypto.ModularArithmetic.FField. -Require Import Coq.nsatz.Nsatz. - -Ltac FqAsIntegralDomain := - lazymatch goal with [H:Znumtheory.prime ?q |- _ ] => - pose proof (_:@Integral_domain.Integral_domain (F q) _ _ _ _ _ _ _ _ _ _) as FqIntegralDomain; - lazymatch type of FqIntegralDomain with @Integral_domain.Integral_domain _ _ _ _ _ _ _ _ ?ringOps ?ringOk ?ringComm => - generalize dependent ringComm; intro Cring; - generalize dependent ringOk; intro Ring; - generalize dependent ringOps; intro RingOps; - lazymatch type of RingOps with @Ncring.Ring_ops ?t ?z ?o ?a ?m ?s ?p ?e => - generalize dependent e; intro equiv; - generalize dependent p; intro opp; - generalize dependent s; intro sub; - generalize dependent m; intro mul; - generalize dependent a; intro add; - generalize dependent o; intro one; - generalize dependent z; intro zero; - generalize dependent t; intro R - end - end; intros; - clear q H - end. - -Ltac fixed_equality_to_goal H x y := generalize (psos_r1 x y H); clear H. -Ltac fixed_equalities_to_goal := - match goal with - | H:?x == ?y |- _ => fixed_equality_to_goal H x y - | H:_ ?x ?y |- _ => fixed_equality_to_goal H x y - | H:_ _ ?x ?y |- _ => fixed_equality_to_goal H x y - | H:_ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y - | H:_ _ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y - end. -Ltac fixed_nsatz := - intros; try apply psos_r1b; - lazymatch goal with - | |- @equality ?T _ _ _ => repeat fixed_equalities_to_goal; nsatz_generic 6%N 1%Z (@nil T) (@nil T) - end. -Ltac F_nsatz := abstract (FqAsIntegralDomain; fixed_nsatz). diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 6168f88bd..8e526745c 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -150,6 +150,15 @@ Section FandZ. intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition. Qed. + Require Crypto.Algebra. + Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul. + Proof. + repeat split; Fdefn; try apply F_eq_dec. + { 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. } + { rewrite Z.mul_1_r. auto. } + Qed. + Lemma ZToField_0 : @ZToField m 0 = 0. Proof. Fdefn. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 70a2c4a87..2021e8514 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -10,6 +10,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Crypto.Algebra. Existing Class prime. @@ -51,6 +52,14 @@ Section FieldModuloPre. Proof. constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l. Qed. + + Global Instance field_modulo : @Algebra.field (F q) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul inv div. + Proof. + constructor; try solve_proper. + - apply commutative_ring_modulo. + - split. auto using F_mul_inv_l. + - split. auto using Fq_1_neq_0. + Qed. End FieldModuloPre. Module Type PrimeModulus. diff --git a/src/Nsatz.v b/src/Nsatz.v new file mode 100644 index 000000000..469ba4c29 --- /dev/null +++ b/src/Nsatz.v @@ -0,0 +1,120 @@ +(*** Tactics for manipulating polynomial equations *) +Require Coq.nsatz.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 := + unfold not; + 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 2ad3877ac..5df36e295 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -1,47 +1,44 @@ -Require Coq.ZArith.BinInt Coq.ZArith.Znumtheory. - Require Crypto.CompleteEdwardsCurve.Pre. -Require Import Crypto.Spec.ModularArithmetic. -Local Open Scope F_scope. - -Global Set Asymmetric Patterns. - -Class TwistedEdwardsParams := { - q : BinInt.Z; - a : F q; - d : F q; - prime_q : Znumtheory.prime q; - two_lt_q : BinInt.Z.lt 2 q; - nonzero_a : a <> 0; - square_a : exists sqrt_a, sqrt_a^2 = a; - nonsquare_d : forall x, x^2 <> d -}. - Module E. Section TwistedEdwardsCurves. - Context {prm:TwistedEdwardsParams}. - (* Twisted Edwards curves with complete addition laws. References: * <https://eprint.iacr.org/2008/013.pdf> * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> * <https://eprint.iacr.org/2015/677.pdf> *) - Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. - Definition point := { P | onCurve P}. - - Definition zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). - Definition add' P1' P2' := - let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - - Definition add (P1 P2 : point) : point := - let 'exist P1' pf1 := P1 in - let 'exist P2' pf2 := P2 in - exist _ (add' P1' P2') - (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). + 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 "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "x ^2" := (x*x) (at level 30). + + Context {a d: F}. + Class twisted_edwards_params := + { + char_gt_2 : 1 + 1 <> 0; + nonzero_a : a <> 0; + square_a : exists sqrt_a, sqrt_a^2 = a; + nonsquare_d : forall x, x^2 <> d + }. + Context `{twisted_edwards_params}. + + 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. + + Program Definition zero : point := (0, 1). + + Program Definition add (P1 P2:point) : point := exist _ ( + let (x1, y1) := coordinates P1 in + let (x2, y2) := coordinates P2 in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))) _. + + (** The described points are indeed on the curve -- see [CompleteEdwardsCurve.Pre] for proof *) + Solve All Obligations using intros; exact Pre.zeroOnCurve + || exact (Pre.unifiedAdd'_onCurve (char_gt_2:=char_gt_2) (d_nonsquare:=nonsquare_d) + (a_nonzero:=nonzero_a) (a_square:=square_a) _ _ (proj2_sig _) (proj2_sig _)). Fixpoint mul (n:nat) (P : point) : point := match n with @@ -50,7 +47,7 @@ Module E. end. End TwistedEdwardsCurves. End E. - + Delimit Scope E_scope with E. Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope. +Infix "*" := E.mul : E_scope.
\ No newline at end of file diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 99f0766e0..bd8a095dd 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,6 +1,4 @@ Require Import Crypto.Spec.Encoding. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Util.WordUtil. Require Bedrock.Word. @@ -8,80 +6,77 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Coercion Word.wordToNat : Word.word >-> nat. +Local Infix "^" := NPeano.pow. +Local Infix "mod" := NPeano.modulo (at level 40, no associativity). +Local Infix "++" := Word.combine. -Infix "^" := NPeano.pow. -Infix "mod" := NPeano.modulo. -Infix "++" := Word.combine. +Generalizable All Variables. +Section EdDSA. + Class EdDSA (* <https://eprint.iacr.org/2015/677.pdf> *) + {E Eeq Eadd Ezero Eopp} {EscalarMult} (* the underllying elliptic curve operations *) -Section EdDSAParams. + {b : nat} (* public keys are k bits, signatures are 2*k bits *) + {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) + {c : nat} (* cofactor E = 2^c *) + {n : nat} (* secret keys are (n+1) bits *) + {l : nat} (* order of the subgroup of E generated by B *) - Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) - E : TwistedEdwardsParams; (* underlying elliptic curve *) + {B : E} (* base point *) - b : nat; (* public keys are k bits, signatures are 2*k bits *) - b_valid : 2^(b - 1) > BinInt.Z.to_nat q; - FqEncoding : canonical encoding of F q as Word.word (b-1); - PointEncoding : canonical encoding of E.point as Word.word b; + {PointEncoding : canonical encoding of E as Word.word b} (* wire format *) + {FlEncoding : canonical encoding of { n | n < l } as Word.word b} + := + { + EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; - H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) + EdDSA_c_valid : c = 2 \/ c = 3; - c : nat; (* cofactor E = 2^c *) - c_valid : c = 2 \/ c = 3; + EdDSA_n_ge_c : n >= c; + EdDSA_n_le_b : n <= b; - n : nat; (* secret keys are (n+1) bits *) - n_ge_c : n >= c; - n_le_b : n <= b; + EdDSA_B_not_identity : B <> Ezero; - B : E.point; - B_not_identity : B <> E.zero; + EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l); + EdDSA_l_odd : l > 2; + EdDSA_l_order_B : EscalarMult l B = Ezero + }. + Global Existing Instance EdDSA_group. - l : nat; (* order of the subgroup of E generated by B *) - l_prime : Znumtheory.prime (BinInt.Z.of_nat l); - l_odd : l > 2; - l_order_B : (l*B)%E = E.zero; - FlEncoding : canonical encoding of F (BinInt.Z.of_nat l) as Word.word b - }. -End EdDSAParams. + Context `{prm:EdDSA}. + + Local Infix "=" := Eeq. + Local Coercion Word.wordToNat : Word.word >-> nat. + Local Notation secretkey := (Word.word b) (only parsing). + Local Notation publickey := (Word.word b) (only parsing). + Local Notation signature := (Word.word (b + b)) (only parsing). -Section EdDSA. - Context {prm:EdDSAParams}. - Existing Instance E. - Existing Instance PointEncoding. - Existing Instance FlEncoding. - Existing Class le. - Existing Instance n_le_b. - - Notation secretkey := (Word.word b) (only parsing). - Notation publickey := (Word.word b) (only parsing). - Notation signature := (Word.word (b + b)) (only parsing). - Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope . + + Existing Class le. Local Existing Instance EdDSA_n_le_b. + Local Arguments H {n} _. (* TODO: proofread curveKey and definition of n *) Definition curveKey (sk:secretkey) : nat := let x := wfirstn n sk in (* first half of the secret key is a scalar *) let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) x + 2^n. (* and the high bit is always set *) + + Local Infix "+" := Eadd. + Local Infix "*" := EscalarMult. + Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). - Definition public (sk:secretkey) : publickey := enc (curveKey sk * B)%E. + Definition public (sk:secretkey) : publickey := enc (curveKey sk*B). - Definition sign (A_:publickey) sk {n} (M : Word.word n) := + Program Definition sign (A_:publickey) sk {n} (M : Word.word n) := let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : E.point := (r * B)%E in (* commitment to nonce *) + let R : E := r * B in (* commitment to nonce *) let s : nat := curveKey sk in (* secret scalar *) - let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat - (r + H (enc R ++ public sk ++ M) * s)) in + let S : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in enc R ++ enc S. + Admit Obligations. - Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := - let R_ := Word.split1 b b sig in - let S_ := Word.split2 b b sig in - match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => - match dec A_ : option E.point with None => false | Some A => - match dec R_ : option E.point with None => false | Some R => - if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A - then true else false - end - end - end%E. + (* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *) + Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop := + ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat) S_lt_l, + S * B = R + (H (enc R ++ enc A ++ message) mod l) * A + -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)). End EdDSA.
\ No newline at end of file diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index d6f6bcb3c..acd2bedbd 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -28,7 +28,7 @@ Section ModularWordEncoding. | Word.WS b _ w' => b end. - Instance modular_word_encoding : canonical encoding of F m as word sz := { + Global Instance modular_word_encoding : canonical encoding of F m as word sz := { enc := Fm_enc; dec := Fm_dec; encoding_valid := diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index f4634f52f..29e359baa 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -20,7 +20,6 @@ Section PointEncoding. {FqEncoding : canonical encoding of (F q) as (Word.word sz)} {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. - Existing Instance prime_q. Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in Word.WS (sign_bit x) (enc y). @@ -29,19 +28,12 @@ Section PointEncoding. {point_dec : Word.word (S sz) -> option E.point | forall w x, point_dec w = Some x -> (point_enc x = w) } := @PointEncodingPre.point_dec _ _ _ sign_bit. - Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). - Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p := - @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp. - - Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc := - PointEncodingPre.point_encoding_canonical. - - Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := { + Global Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := { enc := point_enc; dec := point_dec; - encoding_valid := point_encoding_valid; - encoding_canonical := point_encoding_canonical + encoding_valid := @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp; + encoding_canonical := PointEncodingPre.point_encoding_canonical }. End PointEncoding.
\ No newline at end of file diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v deleted file mode 100644 index 377fb9592..000000000 --- a/src/Specific/Ed25519.v +++ /dev/null @@ -1,581 +0,0 @@ -Require Import Bedrock.Word. -Require Import Crypto.Spec.Ed25519. -Require Import Crypto.Tactics.VerdiTactics. -Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. -Require Import ModularArithmetic.ModularArithmeticTheorems. -Require Import ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Encoding.PointEncodingPre. -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. -Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. - -Local Infix "++" := Word.combine. -Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). -Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). -Local Arguments H {_} _. -Local Arguments scalarMultM1 {_} {_} _ _ _. -Local Arguments unifiedAddM1 {_} {_} _ _. - -Local Ltac set_evars := - repeat match goal with - | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) - end. -Local Ltac subst_evars := - repeat match goal with - | [ e := ?E |- _ ] => is_evar E; subst e - end. - -Lemma funexp_proj {T T'} (proj : T -> T') (f : T -> T) (f' : T' -> T') x n - (f_proj : forall a, proj (f a) = f' (proj a)) - : proj (funexp f x n) = funexp f' (proj x) n. -Proof. - revert x; induction n as [|n IHn]; simpl; congruence. -Qed. - -Lemma iter_op_proj {T T' S} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z - (testbit : S -> nat -> bool) (bound : nat) - (op_proj : forall a b, proj (op a b) = op' (proj a) (proj b)) - : proj (iter_op op x testbit y z bound) = iter_op op' (proj x) testbit y (proj z) bound. -Proof. - unfold iter_op. - simpl. - lazymatch goal with - | [ |- ?proj (snd (funexp ?f ?x ?n)) = snd (funexp ?f' _ ?n) ] - => pose proof (fun x0 x1 => funexp_proj (fun x => (fst x, proj (snd x))) f f' (x0, x1)) as H' - end. - simpl in H'. - rewrite <- H'. - { reflexivity. } - { intros [??]; simpl. - repeat match goal with - | [ |- context[match ?n with _ => _ end] ] - => destruct n eqn:? - | _ => progress simpl - | _ => progress subst - | _ => reflexivity - | _ => rewrite op_proj - end. } -Qed. - -Lemma B_proj : proj1_sig B = (fst(proj1_sig B), snd(proj1_sig B)). destruct B as [[]]; reflexivity. Qed. - -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. -Global Instance option_rect_Proper_nd {A T} - : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)). -Proof. - intros ?? H ??? [|]??; subst; simpl; congruence. -Qed. - -Global Instance option_rect_Proper_nd' {A T} - : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)). -Proof. - intros ?? H ??? [|]; subst; simpl; congruence. -Qed. - -Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances. - -Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v, - option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v). -Proof. - destruct v; reflexivity. -Qed. - -Axiom decode_scalar : word b -> option N. -Local Existing Instance Ed25519.FlEncoding. -Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x). - -Local Infix "==?" := E.point_eqb (at level 70) : E_scope. -Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. - -Lemma solve_for_R_eq : forall A B C, (A = B + C <-> B = A - C)%E. -Proof. - intros; split; intros; subst; unfold E.sub; - rewrite <-E.add_assoc, ?E.add_opp_r, ?E.add_opp_l, E.add_0_r; reflexivity. -Qed. - -Lemma solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. -Proof. - intros. - repeat match goal with |- context [(?P ==? ?Q)%E] => - let H := fresh "H" in - destruct (E.point_eq_dec P Q) as [H|H]; - (rewrite (E.point_eqb_complete _ _ H) || rewrite (E.point_eqb_neq_complete _ _ H)) - end; rewrite solve_for_R_eq in H; congruence. -Qed. - -Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). -Local Notation "2" := (ZToField 2) : F_scope. - -Local Existing Instance PointEncoding. -Lemma decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), - dec P_ = Some P -> - dec Q_ = Some Q -> - weqb P_ Q_ = (P ==? Q)%E. -Proof. - intros. - replace P_ with (enc P) in * by (auto using encoding_canonical). - replace Q_ with (enc Q) in * by (auto using encoding_canonical). - rewrite E.point_eqb_correct. - edestruct E.point_eq_dec; (apply weqb_true_iff || apply weqb_false_iff); congruence. -Qed. - -Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool) - (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). -Proof. - intros. - destruct (dec S_) eqn:H. - { symmetry; eauto using decode_point_eq, encoding_valid. } - { simpl @option_rect. - destruct (weqb S_ (enc X)) eqn:Heqb; trivial. - apply weqb_true_iff in Heqb. subst. rewrite encoding_valid in H; discriminate. } -Qed. - -Definition enc' : F q * F q -> word b. -Proof. - intro x. - let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in - match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with - | (fun _ => ?enc') => exact enc' - end. -Defined. - -Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) - := eq_refl. - -Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. -Global Instance Let_In_Proper_nd {A P} - : Proper (eq ==> pointwise_relation _ eq ==> eq) (@Let_In A (fun _ => P)). -Proof. - lazy; intros; congruence. -Qed. -Lemma option_rect_function {A B C S' N' v} f - : f (option_rect (fun _ : option A => option B) S' N' v) - = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v. -Proof. destruct v; reflexivity. Qed. -Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *) - idtac; - lazymatch goal with - | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ] - => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *) - cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta; - [ set_evars; - let H := fresh in - intro H; - rewrite H; - clear; - abstract (cbv [Let_In]; reflexivity) - | ] - end. -Local Ltac replace_let_in_with_Let_In := - repeat match goal with - | [ |- context G[let x := ?y in @?z x] ] - => let G' := context G[Let_In y z] in change G' - | [ |- _ = Let_In _ _ ] - => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] - end. -Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *) - repeat match goal with - | [ |- context[option_rect ?P ?S ?N None] ] - => change (option_rect P S N None) with N - | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] - => change (option_rect P S N (Some x)) with (S x); cbv beta - end. - -Section Ed25519Frep. - Generalizable All Variables. - Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). - Context `(rcF:RepConversions (F (Ed25519.q)) FRep) (rcFOK:RepConversionsOK rcF). - Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul). - Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul). - Local Notation rep2F := (unRep : FRep -> F (Ed25519.q)). - Local Notation F2Rep := (toRep : F (Ed25519.q) -> FRep). - Local Notation rep2S := (unRep : SRep -> N). - Local Notation S2Rep := (toRep : N -> SRep). - - Axiom FRepOpp : FRep -> FRep. - Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x). - - Axiom wltu : forall {b}, word b -> word b -> bool. - Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x <? wordToN y)%N. - - Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y). - - Axiom wire2FRep : word (b-1) -> option FRep. - Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x). - - Axiom FRep2wire : FRep -> word (b-1). - Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (rep2F x). - - Axiom SRep_testbit : SRep -> nat -> bool. - Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (unRep x0) i. - - Definition FSRepPow x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x 255. - Lemma FSRepPow_correct : forall x n, (N.size_nat (unRep n) <= 255)%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow x n). - Proof. (* this proof derives the required formula, which I copy-pasted above to be able to reference it without the length precondition *) - unfold FSRepPow; intros. - erewrite <-pow_nat_iter_op_correct by auto. - erewrite <-(fun x => iter_op_spec (scalar := SRep) (mul (m:=Ed25519.q)) F_mul_assoc _ F_mul_1_l _ unRep SRep_testbit_correct n x 255%nat) by auto. - rewrite <-(rcFOK 1%F) at 1. - erewrite <-iter_op_proj by auto. - reflexivity. - Qed. - - Definition FRepInv x : FRep := FSRepPow x (S2Rep (Z.to_N (Ed25519.q - 2))). - Lemma FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x). - unfold FRepInv; intros. - rewrite <-FSRepPow_correct; rewrite rcSOK; try reflexivity. - pose proof @Fq_inv_fermat_correct as H; unfold inv_fermat in H; rewrite H by - auto using Ed25519.prime_q, Ed25519.two_lt_q. - reflexivity. - Qed. - - Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. - - Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := - match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end. - - Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). - Proof. - destruct b; trivial. - Qed. - - Local Ltac Let_In_unRep := - match goal with - | [ |- appcontext G[Let_In (unRep ?x) ?f] ] - => let G' := context G[Let_In x (fun y => f (unRep y))] in change G'; cbv beta - end. - - - (** TODO: Move me *) - Lemma pull_Let_In {B C} (f : B -> C) A (v : A) (b : A -> B) - : Let_In v (fun v' => f (b v')) = f (Let_In v b). - Proof. - reflexivity. - Qed. - - Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : - @Let_In _ (fun _ => T) (g x) f = - @Let_In _ (fun _ => T) x (fun p => f (g x)). - Proof. reflexivity. Qed. - - Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) : - @Let_In _ (fun _ => T) (g1 x, g2 y) f = - @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))). - Proof. reflexivity. Qed. - - Create HintDb FRepOperations discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - - Create HintDb EdDSA_opts discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. - - Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. - Proof. - destruct a as [[[]]]; destruct b as [[[]]]. - eexists. - lazymatch goal with |- ?LHS = ?RHS :> ?T => - evar (e:T); replace LHS with e; [subst e|] - end. - unfold rep2E. cbv beta delta [unifiedAddM1']. - pose proof (rcFOK twice_d) as H; rewrite <-H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) - - { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. - repeat ( - autorewrite with FRepOperations; - Let_In_unRep; - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). - lazymatch goal with |- ?LHS = (unRep ?x, unRep ?y, unRep ?z, unRep ?t) => - change (LHS = (rep2E (((x, y), z), t))) - end. - reflexivity. } - - subst e. - Local Opaque Let_In. - repeat setoid_rewrite (pull_Let_In rep2E). - Local Transparent Let_In. - reflexivity. - Defined. - - Definition unifiedAddM1Rep (a b:FRep * FRep * FRep * FRep) : FRep * FRep * FRep * FRep := Eval hnf in proj1_sig (unifiedAddM1Rep_sig a b). - Definition unifiedAddM1Rep_correct a b : rep2E (unifiedAddM1Rep a b) = unifiedAddM1' (rep2E a) (rep2E b) := Eval hnf in proj2_sig (unifiedAddM1Rep_sig a b). - - Definition rep2T (P:FRep * FRep) := (rep2F (fst P), rep2F (snd P)). - Definition erep2trep (P:FRep * FRep * FRep * FRep) := Let_In P (fun P => Let_In (FRepInv (snd (fst P))) (fun iZ => (FRepMul (fst (fst (fst P))) iZ, FRepMul (snd (fst (fst P))) iZ))). - Lemma erep2trep_correct : forall P, rep2T (erep2trep P) = extendedToTwisted (rep2E P). - Proof. - unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. - rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. - Qed. - - (** TODO: possibly move me, remove local *) - Local Ltac replace_option_match_with_option_rect := - idtac; - lazymatch goal with - | [ |- _ = ?RHS :> ?T ] - => lazymatch RHS with - | match ?a with None => ?N | Some x => @?S x end - => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity) - end - end. - - (** TODO: Move me, remove Local *) - Definition proj1_sig_unmatched {A P} := @proj1_sig A P. - Definition proj1_sig_nounfold {A P} := @proj1_sig A P. - Definition proj1_sig_unfold {A P} := Eval cbv [proj1_sig] in @proj1_sig A P. - Local Ltac unfold_proj1_sig_exist := - (** Change the first [proj1_sig] into [proj1_sig_unmatched]; if it's applied to [exist], mark it as unfoldable, otherwise mark it as not unfoldable. Then repeat. Finally, unfold. *) - repeat (change @proj1_sig with @proj1_sig_unmatched at 1; - match goal with - | [ |- context[proj1_sig_unmatched (exist _ _ _)] ] - => change @proj1_sig_unmatched with @proj1_sig_unfold - | _ => change @proj1_sig_unmatched with @proj1_sig_nounfold - end); - (* [proj1_sig_nounfold] is a thin wrapper around [proj1_sig]; unfolding it restores [proj1_sig]. Unfolding [proj1_sig_nounfold] exposes the pattern match, which is reduced by ι. *) - cbv [proj1_sig_nounfold proj1_sig_unfold]. - - (** TODO: possibly move me, remove Local *) - Local Ltac reflexivity_when_unification_is_stupid_about_evars - := repeat first [ reflexivity - | apply f_equal ]. - - - Local Existing Instance eq_Reflexive. (* To get some of the [setoid_rewrite]s below to work, we need to infer [Reflexive eq] before [Reflexive Equivalence.equiv] *) - - (* TODO: move me *) - Lemma fold_rep2E x y z t - : (rep2F x, rep2F y, rep2F z, rep2F t) = rep2E (((x, y), z), t). - Proof. reflexivity. Qed. - Lemma commute_negateExtended'_rep2E x y z t - : negateExtended' (rep2E (((x, y), z), t)) - = rep2E (((FRepOpp x, y), z), FRepOpp t). - Proof. simpl; autorewrite with FRepOperations; reflexivity. Qed. - Lemma fold_rep2E_ffff x y z t - : (x, y, z, t) = rep2E (((toRep x, toRep y), toRep z), toRep t). - Proof. simpl; rewrite !rcFOK; reflexivity. Qed. - Lemma fold_rep2E_rrfr x y z t - : (rep2F x, rep2F y, z, rep2F t) = rep2E (((x, y), toRep z), t). - Proof. simpl; rewrite !rcFOK; reflexivity. Qed. - Lemma fold_rep2E_0fff y z t - : (0%F, y, z, t) = rep2E (((toRep 0%F, toRep y), toRep z), toRep t). - Proof. apply fold_rep2E_ffff. Qed. - Lemma fold_rep2E_ff1f x y t - : (x, y, 1%F, t) = rep2E (((toRep x, toRep y), toRep 1%F), toRep t). - Proof. apply fold_rep2E_ffff. Qed. - Lemma commute_negateExtended'_rep2E_rrfr x y z t - : negateExtended' (unRep x, unRep y, z, unRep t) - = rep2E (((FRepOpp x, y), toRep z), FRepOpp t). - Proof. rewrite <- commute_negateExtended'_rep2E; simpl; rewrite !rcFOK; reflexivity. Qed. - - Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) @if_F_eq_dec_if_F_eqb compare_enc (if_map unRep) (fun T => Let_app2_In (T := T) unRep unRep) @F_pow_2_r @unfoldDiv : EdDSA_opts. - Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) FRep2wire_correct: EdDSA_opts. - - Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. - Proof. - eexists; intros. - cbv [ed25519_verify EdDSA.verify - ed25519params curve25519params - EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H - EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. - - etransitivity. - Focus 2. - { repeat match goal with - | [ |- ?x = ?x ] => reflexivity - | _ => replace_option_match_with_option_rect - | [ |- _ = option_rect _ _ _ _ ] - => eapply option_rect_Proper_nd; [ intro | reflexivity.. ] - end. - set_evars. - rewrite<- E.point_eqb_correct. - rewrite solve_for_R; unfold E.sub. - rewrite E.opp_mul. - let p1 := constr:(scalarMultM1_rep eq_refl) in - let p2 := constr:(unifiedAddM1_rep eq_refl) in - repeat match goal with - | |- context [(_ * E.opp ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite negateExtended_correct; - rewrite <-p1 - | |- context [(_ * ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite <-p1 - | _ => rewrite p2 - end; - rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; - subst_evars; - reflexivity. - } Unfocus. - - etransitivity. - Focus 2. - { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. - match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' - end. - reflexivity. - } Unfocus. - rewrite <-decode_scalar_correct. - - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - symmetry; apply decode_test_encode_test. - } Unfocus. - - rewrite enc'_correct. - cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. - unfold_proj1_sig_exist. - - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - set_evars. - repeat match goal with - | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] - => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity - end. - subst_evars. - reflexivity. } - Unfocus. - - cbv [mkExtendedPoint E.zero]. - unfold_proj1_sig_exist. - rewrite B_proj. - - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - set_evars. - lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. - match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' - end. - reflexivity. - } Unfocus. - - cbv [dec PointEncoding point_encoding]. - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - etransitivity. - Focus 2. - { apply f_equal. - symmetry. - apply point_dec_coordinates_correct. } - Unfocus. - reflexivity. } - Unfocus. - - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. - etransitivity. - Focus 2. - { apply f_equal. - lazymatch goal with - | [ |- _ = ?term :> ?T ] - => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) - => let term' := constr:((option_rect (fun _ => T) S N) a) in - replace term with term' by reflexivity - end - end. - reflexivity. } Unfocus. reflexivity. } Unfocus. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - do 1 (eapply option_rect_Proper_nd; [ intro; reflexivity | reflexivity | ]). - eapply option_rect_Proper_nd; [ cbv beta delta [pointwise_relation]; intro | reflexivity.. ]. - replace_let_in_with_Let_In. - reflexivity. - } Unfocus. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - set_evars. - rewrite option_rect_function. (* turn the two option_rects into one *) - subst_evars. - simpl_option_rect. - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - (* push the [option_rect] inside until it hits a [Some] or a [None] *) - repeat match goal with - | _ => commute_option_rect_Let_In - | [ |- _ = Let_In _ _ ] - => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] - | [ |- ?LHS = option_rect ?P ?S ?N (if ?b then ?t else ?f) ] - => transitivity (if b then option_rect P S N t else option_rect P S N f); - [ - | destruct b; reflexivity ] - | [ |- _ = if ?b then ?t else ?f ] - => apply (f_equal2 (fun x y => if b then x else y)) - | [ |- _ = false ] => reflexivity - | _ => progress simpl_option_rect - end. - reflexivity. - } Unfocus. - - cbv iota beta delta [q d a]. - - rewrite wire2FRep_correct. - - etransitivity. - Focus 2. { - eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. - rewrite <-!(option_rect_option_map rep2F). - eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. - autorewrite with EdDSA_opts. - rewrite <-(rcFOK 1%F). - pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1. - pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1. - rewrite <- (rcSOK (Z.to_N (Ed25519.q / 8 + 1))). - autorewrite with EdDSA_opts. - (Let_In_unRep). - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. - etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. { - rewrite FSRepPow_correct by (rewrite rcSOK; cbv; omega). - (Let_In_unRep). - etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { - set_evars. - rewrite <-(rcFOK sqrt_minus1). - autorewrite with EdDSA_opts. - subst_evars. - reflexivity. } Unfocus. - rewrite pull_Let_In. - reflexivity. } Unfocus. - set_evars. - (Let_In_unRep). - - subst_evars. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. - - autorewrite with EdDSA_opts. - - subst_evars. - lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. - set_evars. - - unfold twistedToExtended. - autorewrite with EdDSA_opts. - progress cbv beta delta [erep2trep]. - - subst_evars. - reflexivity. } Unfocus. - reflexivity. - Defined. -End Ed25519Frep. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 8ee9b25d8..7e0e815e5 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -59,6 +59,17 @@ Proof. exact Hfg. Time Defined. +Local Transparent Let_In. +Infix "<<" := Z.shiftr (at level 50). +Infix "&" := Z.land (at level 50). +Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in + fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => proj1_sig ( + GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9). +Local Opaque Let_In. + + Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. (* It's easy enough to use extraction to get the proper nice-looking formula. * More Ltac acrobatics will be needed to get out that formula for further use in Coq. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v new file mode 100644 index 000000000..de1af2a95 --- /dev/null +++ b/src/Util/Tuple.v @@ -0,0 +1,80 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. + +Fixpoint tuple' T n : Type := + match n with + | O => T + | S n' => (tuple' T n' * T)%type + end. + +Definition tuple T n : Type := + match n with + | O => unit + | S n' => tuple' T n' + end. + +Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := + match n with + | 0 => fun x => (x::nil)%list + | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list + end. + +Definition to_list {T} (n:nat) : tuple T n -> list T := + match n with + | 0 => fun _ => nil + | S n' => fun xs : tuple T (S n') => to_list' n' xs + end. + +Fixpoint from_list' {T} (x:T) (xs:list T) : tuple' T (length xs) := + match xs with + | nil => x + | (y :: xs')%list => (from_list' y xs', x) + end. + +Definition from_list {T} (xs:list T) : tuple T (length xs) := + match xs as l return (tuple T (length l)) with + | nil => tt + | (t :: xs')%list => from_list' t xs' + end. + +Lemma to_list_from_list : forall {T} (xs:list T), to_list (length xs) (from_list xs) = xs. +Proof. + destruct xs; auto; simpl. + generalize dependent t. + induction xs; auto; simpl; intros; f_equal; auto. +Qed. + +Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n. +Proof. + destruct n; auto; intros; simpl in *. + induction n; auto; intros; simpl in *. + destruct xs; simpl in *; eauto. +Qed. + +Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop. + destruct n; simpl @tuple' in *. + { exact (R a b). } + { exact (R (snd a) (snd b) /\ fieldwise' _ _ n R (fst a) (fst b)). } +Defined. + +Definition fieldwise {A B} (n:nat) (R:A->B->Prop) (a:tuple A n) (b:tuple B n) : Prop. + destruct n; simpl @tuple in *. + { exact True. } + { exact (fieldwise' _ R a b). } +Defined. + +Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: + Equivalence (fieldwise' n R). +Proof. + induction n; [solve [auto]|]. + simpl; constructor; repeat intro; intuition eauto. +Qed. + +Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: + Equivalence (fieldwise n R). +Proof. + destruct n; (repeat constructor || apply Equivalence_fieldwise'). +Qed. + +Arguments fieldwise' {A B n} _ _ _. +Arguments fieldwise {A B n} _ _ _.
\ No newline at end of file |