diff options
51 files changed, 625 insertions, 225 deletions
diff --git a/_CoqProject b/_CoqProject index cae81fdae..1d65a7564 100644 --- a/_CoqProject +++ b/_CoqProject @@ -26,6 +26,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/PointEncoding.v +src/Specific/Ed25519.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v diff --git a/coqprime/Coqprime/Cyclic.v b/coqprime/Coqprime/Cyclic.v index c25f683ca..e2daa4d67 100644 --- a/coqprime/Coqprime/Cyclic.v +++ b/coqprime/Coqprime/Cyclic.v @@ -11,13 +11,13 @@ Proof that an abelien ring is cyclic ************************************************************************) -Require Import ZCAux. -Require Import List. -Require Import Root. -Require Import UList. -Require Import IGroup. -Require Import EGroup. -Require Import FGroup. +Require Import Coqprime.ZCAux. +Require Import Coq.Lists.List. +Require Import Coqprime.Root. +Require Import Coqprime.UList. +Require Import Coqprime.IGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v index fd543fe04..553cb746c 100644 --- a/coqprime/Coqprime/EGroup.v +++ b/coqprime/Coqprime/EGroup.v @@ -11,15 +11,15 @@ Given an element a, create the group {e, a, a^2, ..., a^n} **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import List. -Require Import ZCAux. -Require Import ZArith Znumtheory. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import Lagrange. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Lists.List. +Require Import Coqprime.ZCAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.Lagrange. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v index 06d92ce57..e571d8e3c 100644 --- a/coqprime/Coqprime/Euler.v +++ b/coqprime/Coqprime/Euler.v @@ -11,10 +11,10 @@ Definition of the Euler Totient function *************************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Export ZSum. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Export Coqprime.ZSum. Open Scope Z_scope. diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v index a55710e7c..0bcc9ebf1 100644 --- a/coqprime/Coqprime/FGroup.v +++ b/coqprime/Coqprime/FGroup.v @@ -13,10 +13,10 @@ Definition: FGroup **********************************************************************) -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v index 11a73d414..04219be5a 100644 --- a/coqprime/Coqprime/IGroup.v +++ b/coqprime/Coqprime/IGroup.v @@ -13,12 +13,12 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import ListAux. -Require Import FGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v index 96d3e5655..e84687cd4 100644 --- a/coqprime/Coqprime/Iterator.v +++ b/coqprime/Coqprime/Iterator.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export List. -Require Export Permutation. -Require Import Arith. +Require Export Coq.Lists.List. +Require Export Coqprime.Permutation. +Require Import Coq.Arith.Arith. Section Iterator. Variables A B : Set. diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v index b35460bad..b890c5621 100644 --- a/coqprime/Coqprime/Lagrange.v +++ b/coqprime/Coqprime/Lagrange.v @@ -14,12 +14,12 @@ Definition: lagrange **********************************************************************) -Require Import List. -Require Import UList. -Require Import ListAux. -Require Import ZArith Znumtheory. -Require Import NatAux. -Require Import FGroup. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coqprime.NatAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v index c3c9602bd..4ed154685 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export List. -Require Export Arith. -Require Export Tactic. -Require Import Inverse_Image. -Require Import Wf_nat. +Require Export Coq.Lists.List. +Require Export Coq.Arith.Arith. +Require Export Coqprime.Tactic. +Require Import Coq.Wellfounded.Inverse_Image. +Require Import Coq.Arith.Wf_nat. (************************************** Some properties on list operators: app, map,... diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v index c3c255036..c459195a8 100644 --- a/coqprime/Coqprime/LucasLehmer.v +++ b/coqprime/Coqprime/LucasLehmer.v @@ -13,17 +13,17 @@ Definition: LucasLehmer **********************************************************************) -Require Import ZArith. -Require Import ZCAux. -Require Import Tactic. -Require Import Wf_nat. -Require Import NatAux. -Require Import UList. -Require Import ListAux. -Require Import FGroup. -Require Import EGroup. -Require Import PGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.NatAux. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.PGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/NatAux.v b/coqprime/Coqprime/NatAux.v index eab09150c..6df511eed 100644 --- a/coqprime/Coqprime/NatAux.v +++ b/coqprime/Coqprime/NatAux.v @@ -11,7 +11,7 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Arith. +Require Export Coq.Arith.Arith. (************************************** Some properties of minus diff --git a/coqprime/Coqprime/PGroup.v b/coqprime/Coqprime/PGroup.v index e9c1b2f47..19eff5850 100644 --- a/coqprime/Coqprime/PGroup.v +++ b/coqprime/Coqprime/PGroup.v @@ -14,15 +14,15 @@ Definition: PGroup **********************************************************************) -Require Import ZArith. -Require Import Znumtheory. -Require Import Tactic. -Require Import Wf_nat. -Require Import ListAux. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.ListAux. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v index a06693f89..7cb6f629d 100644 --- a/coqprime/Coqprime/Permutation.v +++ b/coqprime/Coqprime/Permutation.v @@ -11,8 +11,8 @@ Defintion and properties of permutations **********************************************************************) -Require Export List. -Require Export ListAux. +Require Export Coq.Lists.List. +Require Export Coqprime.ListAux. Section permutation. Variable A : Set. diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v index f64af48e3..45961896e 100644 --- a/coqprime/Coqprime/Pmod.v +++ b/coqprime/Coqprime/Pmod.v @@ -6,8 +6,8 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. -Require Export ZCmisc. +Require Export Coq.ZArith.ZArith. +Require Export Coqprime.ZCmisc. Open Local Scope positive_scope. @@ -392,7 +392,7 @@ Lemma gcd_log2_mod0 : Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. -Require Import Zwf. +Require Import Coq.ZArith.Zwf. Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). Proof. @@ -510,8 +510,8 @@ Proof. destruct (gcd_log2 b r r);intros;trivial. Qed. -Require Import ZArith. -Require Import Znumtheory. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v index 9871cd3e6..79e7dc616 100644 --- a/coqprime/Coqprime/Pocklington.v +++ b/coqprime/Coqprime/Pocklington.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Import ZCAux. -Require Import Zp. -Require Import FGroup. -Require Import EGroup. -Require Import Euler. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Zp. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.Euler. Open Scope Z_scope. diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v index ed75ca281..fccea30b6 100644 --- a/coqprime/Coqprime/PocklingtonCertificat.v +++ b/coqprime/Coqprime/PocklingtonCertificat.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import List. -Require Import ZArith. -Require Import Zorder. -Require Import ZCAux. -Require Import LucasLehmer. -Require Import Pocklington. -Require Import ZCmisc. -Require Import Pmod. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Zorder. +Require Import Coqprime.ZCAux. +Require Import Coqprime.LucasLehmer. +Require Import Coqprime.Pocklington. +Require Import Coqprime.ZCmisc. +Require Import Coqprime.Pmod. Definition dec_prime := list (positive * positive). diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v index 321865ba1..4e74a4d2f 100644 --- a/coqprime/Coqprime/Root.v +++ b/coqprime/Coqprime/Root.v @@ -11,11 +11,11 @@ Proof that a polynomial has at most n roots ************************************************************************) -Require Import ZArith. -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import Permutation. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coqprime.Permutation. Open Scope Z_scope. diff --git a/coqprime/Coqprime/ZCAux.v b/coqprime/Coqprime/ZCAux.v index de03a2fe2..aa47fb655 100644 --- a/coqprime/Coqprime/ZCAux.v +++ b/coqprime/Coqprime/ZCAux.v @@ -12,10 +12,10 @@ Auxillary functions & Theorems **********************************************************************) -Require Import ArithRing. -Require Export ZArith Zpow_facts. -Require Export Znumtheory. -Require Export Tactic. +Require Import Coq.setoid_ring.ArithRing. +Require Export Coq.ZArith.ZArith Coq.ZArith.Zpow_facts. +Require Export Coq.ZArith.Znumtheory. +Require Export Coqprime.Tactic. Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x. intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith. diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v index c1bdacc63..e2ec66ba1 100644 --- a/coqprime/Coqprime/ZCmisc.v +++ b/coqprime/Coqprime/ZCmisc.v @@ -6,7 +6,7 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. +Require Export Coq.ZArith.ZArith. Open Local Scope Z_scope. Coercion Zpos : positive >-> Z. diff --git a/coqprime/Coqprime/ZProgression.v b/coqprime/Coqprime/ZProgression.v index 51ce91cdc..4cf30d692 100644 --- a/coqprime/Coqprime/ZProgression.v +++ b/coqprime/Coqprime/ZProgression.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Iterator. -Require Import ZArith. -Require Export UList. +Require Export Coqprime.Iterator. +Require Import Coq.ZArith.ZArith. +Require Export Coqprime.UList. Open Scope Z_scope. Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m. diff --git a/coqprime/Coqprime/ZSum.v b/coqprime/Coqprime/ZSum.v index 3a7f14065..907720f7c 100644 --- a/coqprime/Coqprime/ZSum.v +++ b/coqprime/Coqprime/ZSum.v @@ -9,12 +9,12 @@ (*********************************************************************** Summation.v from Z to Z *********************************************************************) -Require Import Arith. -Require Import ArithRing. -Require Import ListAux. -Require Import ZArith. -Require Import Iterator. -Require Import ZProgression. +Require Import Coq.Arith.Arith. +Require Import Coq.setoid_ring.ArithRing. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Iterator. +Require Import Coqprime.ZProgression. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Zp.v b/coqprime/Coqprime/Zp.v index 9b99bef1d..2f7d28d69 100644 --- a/coqprime/Coqprime/Zp.v +++ b/coqprime/Coqprime/Zp.v @@ -14,16 +14,16 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith Znumtheory Zpow_facts. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. Require Import Coqprime.Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. -Require Import Cyclic. -Require Import Euler. -Require Import ZProgression. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. +Require Import Coqprime.Cyclic. +Require Import Coqprime.Euler. +Require Import Coqprime.ZProgression. Open Scope Z_scope. diff --git a/src/BaseSystem.v b/src/BaseSystem.v index 627550440..e6ad55f18 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Local Open Scope Z. diff --git a/src/BoundedIterOp.v b/src/BoundedIterOp.v index fbdc823ad..bd4f7d66e 100644 --- a/src/BoundedIterOp.v +++ b/src/BoundedIterOp.v @@ -1,5 +1,5 @@ Require Import Crypto.Tactics.VerdiTactics. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Definition testbit_rev p i bound := Pos.testbit_nat p (bound - i). diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 01b3584c0..3740f5a29 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -4,7 +4,7 @@ Require Import Crypto.ModularArithmetic.FField. Require Import Crypto.ModularArithmetic.FNsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Eqdep_dec. +Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Section CompleteEdwardsCurveTheorems. @@ -18,10 +18,10 @@ Section CompleteEdwardsCurveTheorems. postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], constants [Fconstant], div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + power_tac (@Fpower_theory q) [Fexp_tac]). Add Field Ffield_notConstant : (OpaqueFieldTheory q) - (constants [notConstant]). + (constants [notConstant]). Ltac clear_prm := generalize dependent a; intro a; intros; @@ -34,7 +34,7 @@ Section CompleteEdwardsCurveTheorems. mkPoint p1 pf1 = mkPoint p2 pf2. Proof. destruct p1, p2; 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. *) + 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. @@ -55,11 +55,11 @@ Section CompleteEdwardsCurveTheorems. Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E. Proof. - (* The Ltac takes ~15s, the Qed takes longer than I have had patience for *) + (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *) Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz); repeat split; match goal with [ |- _ = 0%F -> False ] => admit end; fail "unreachable". - Admitted. + Qed. Lemma zeroIsIdentity : forall P, (P + zero = P)%E. Proof. diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index 7c1e173ee..84c1289f6 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -1,7 +1,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 226600428..e918ac128 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -3,6 +3,9 @@ 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. @@ -80,10 +83,43 @@ Section ExtendedCoordinates. solveExtended. Qed. + Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ onCurve (extendedToTwisted P) }. + + Program Definition mkExtendedPoint : point -> extendedPoint := twistedToExtended. + Next Obligation. + destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. + Qed. + + Program Definition unExtendedPoint : extendedPoint -> 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 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. + 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 := + 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 @@ -101,8 +137,8 @@ Section ExtendedCoordinates. (X3, Y3, Z3, T3). Local Hint Unfold unifiedAdd. - Lemma unifiedAdd_repM1: forall P Q rP rQ, onCurve rP -> onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAddM1 P Q) ~= (unifiedAdd' rP rQ). + Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ). Proof. intros P Q rP rQ HoP HoQ HrP HrQ. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). @@ -136,5 +172,63 @@ Section ExtendedCoordinates. - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. Qed. + + Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q). + Proof. + intros; pose proof (proj2_sig (unifiedAdd (mkPoint _ H) (mkPoint _ 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, unifiedAdd (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). + Proof. + destruct P, Q; unfold unExtendedPoint, unifiedAdd, unifiedAddM1; eapply 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 point_eq; congruence. + Qed. + + Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint zero) === P. + unfold equiv, extendedPoint_eq; intros. + rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + Qed. + + Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint zero) P === P. + unfold equiv, extendedPoint_eq; intros. + rewrite <-!unifiedAddM1_rep, twistedAddComm, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + Qed. + + Lemma unifiedAddM1_assoc : forall a b c, unifiedAddM1 a (unifiedAddM1 b c) === unifiedAddM1 (unifiedAddM1 a b) c. + Proof. + unfold equiv, extendedPoint_eq; intros. + rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto. + Qed. + + Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero). + Definition scalarMultM1_spec := iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l. + Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P) = scalarMult n (unExtendedPoint P). + intros; rewrite scalarMultM1_spec, Nat2N.id. + induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]. + unfold scalarMult; fold scalarMult. + rewrite <-IHn, unifiedAddM1_rep; auto. + Qed. + End TwistMinus1. + End ExtendedCoordinates.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index e4dc140e1..fea4a99b3 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,4 +1,4 @@ -Require Import BinInt Znumtheory VerdiTactics. +Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v index 7357284e1..83467bf6d 100644 --- a/src/EdDSAProofs.v +++ b/src/EdDSAProofs.v @@ -1,11 +1,11 @@ Require Import Crypto.Spec.EdDSA Crypto.Spec.Encoding. -Require Import NPeano. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Bedrock.Word. -Require Import Znumtheory BinInt ZArith. +Require Import Coq.ZArith.Znumtheory Coq.ZArith.BinInt Coq.ZArith.ZArith. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import VerdiTactics. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope nat_scope. Section EdDSAProofs. diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v index cd293056f..4f2b623e0 100644 --- a/src/ModularArithmetic/FField.v +++ b/src/ModularArithmetic/FField.v @@ -1,5 +1,5 @@ Require Export Crypto.Spec.ModularArithmetic. -Require Export Field. +Require Export Coq.setoid_ring.Field. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. @@ -14,6 +14,10 @@ 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. @@ -26,7 +30,7 @@ Ltac FIELD_SIMPL_idtac FLD lH rl := get_FldPost FLD (). Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G. -Ltac F_to_Opaque := +Ltac F_to_Opaque := change F with OpaqueF in *; change BinInt.Z.modulo with OpaqueZmodulo in *; change @add with @Opaqueadd in *; @@ -41,13 +45,10 @@ 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 @Opaqueadd with @add in *; - change @Opaquemul with @mul in *; - change @Opaquesub with @sub in *; - change @Opaquediv with @div in *; change @Opaqueopp with @opp in *; change @Opaqueinv with @inv in *; - change @OpaqueZToField with @ZToField 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) _ _ => @@ -59,4 +60,4 @@ Ltac F_field_simplify_eq := Ltac F_field := F_field_simplify_eq; [ring|..]. -Ltac notConstant t := constr:NotConstant.
\ No newline at end of file +Ltac notConstant t := constr:NotConstant. diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v index a0f34073d..221b8d799 100644 --- a/src/ModularArithmetic/FNsatz.v +++ b/src/ModularArithmetic/FNsatz.v @@ -1,6 +1,6 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Export Crypto.ModularArithmetic.FField. -Require Import Nsatz. +Require Import Coq.nsatz.Nsatz. Ltac FqAsIntegralDomain := lazymatch goal with [H:Znumtheory.prime ?q |- _ ] => diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index f39cc4176..ddb689547 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -1,11 +1,11 @@ Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.Pre. -Require Import Eqdep_dec. -Require Import Tactics.VerdiTactics. -Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *) -Require Import Coq.Classes.Morphisms Setoid. -Require Export Ring_theory Field_theory Field_tac. +Require Import Coq.Logic.Eqdep_dec. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. Section ModularArithmeticPreliminaries. Context {m:Z}. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 2bfcdcf0b..f63bfbb1c 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,8 +1,12 @@ -Require Import Zpower ZArith. -Require Import List. -Require Import Crypto.Util.ListUtil. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.BaseSystem Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z_scope. Section PseudoMersenneBase. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 3432488c4..2978fdd42 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -1,6 +1,6 @@ -Require Import BinInt BinNat BinNums Zdiv Znumtheory. -Require Import Eqdep_dec. -Require Import EqdepFacts. +Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArith.Zdiv Coq.ZArith.Znumtheory. +Require Import Coq.Logic.Eqdep_dec. +Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 40af15dac..77d84c455 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -1,13 +1,13 @@ -Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems. -Require Export Ring_theory Field_theory Field_tac. +Require Export Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.ModularArithmeticTheorems. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Import Nsatz. +Require Import Coq.nsatz.Nsatz. Require Import Crypto.ModularArithmetic.Pre. -Require Import Util.NumTheoryUtil. -Require Import Tactics.VerdiTactics. -Require Import Coq.Classes.Morphisms Setoid. -Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *) -Require Import Eqdep_dec. +Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. +Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) +Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Existing Class prime. @@ -294,7 +294,7 @@ Section VariousModPrime. } Qed. - Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q), if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1)) then (isSquare a) else (forall b, b ^ 2 <> a). Proof. @@ -309,6 +309,16 @@ Section VariousModPrime. apply euler_criterion_F in a_square; auto. Qed. + Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1) + then (isSquare a) else (forall b, b ^ 2 <> a). + Proof. + intros. + pose proof (euler_criterion_if' a q_odd) as H. + unfold F_eqb in *; simpl in *. + rewrite !Zmod_small, !@FieldToZ_pow_efficient in H by omega; eauto. + Qed. + Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. intros ? ? squares_eq. diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index 425816f9e..d6c7fa4b8 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -1,5 +1,5 @@ -Require Import BinInt Zpower ZArith Znumtheory. -Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems. +Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems. (* Example for modular arithmetic with a concrete modulus in a section *) diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 23e201405..b7d2c0d8e 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -1,4 +1,4 @@ -Require BinInt Znumtheory. +Require Coq.ZArith.BinInt Coq.ZArith.Znumtheory. Require Crypto.CompleteEdwardsCurve.Pre. @@ -46,8 +46,11 @@ Section TwistedEdwardsCurves. | O => zero | S n' => unifiedAdd P (scalarMult n' P) end. + + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. End TwistedEdwardsCurves. Delimit Scope E_scope with E. Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope.
\ No newline at end of file +Infix "*" := scalarMult : E_scope. +Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index e16cc73f6..6ab47e8e5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -1,14 +1,14 @@ -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import NPeano NArith. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. -Require Import VerdiTactics. -Require Import Decidable. -Require Import Omega. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Logic.Decidable. +Require Import Coq.omega.Omega. Local Open Scope nat_scope. Definition q : Z := (2 ^ 255 - 19)%Z. @@ -43,13 +43,28 @@ Proof. rewrite Z.mod_small; q_bound. Qed. -(* TODO *) -(* d = .*) -Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F. -Lemma nonsquare_d : forall x, (x^2 <> d)%F. Admitted. -(* Definition nonsquare_d : (forall x, x^2 <> d) := euler_criterion_if d. <-- currently not computable in reasonable time *) +Hint Rewrite + @FieldToZ_add + @FieldToZ_mul + @FieldToZ_opp + @FieldToZ_inv_efficient + @FieldToZ_pow_efficient + @FieldToZ_ZToField + @Zmod_mod + : ZToField. -Instance TEParams : TwistedEdwardsParams := { +Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F. +Lemma nonsquare_d : forall x, (x^2 <> d)%F. + pose proof @euler_criterion_if q prime_q d two_lt_q. + match goal with + [H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H] + end. + unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..]. + vm_compute. (* 10s *) + exact eq_refl. +Qed. (* 10s *) + +Instance curve25519params : TwistedEdwardsParams := { q := q; prime_q := prime_q; two_lt_q := two_lt_q; @@ -117,13 +132,6 @@ Definition FlEncoding : encoding of F (Z.of_nat l) as word b := Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. -Hint Rewrite - @FieldToZ_pow_efficient - @FieldToZ_ZToField - @FieldToZ_opp - @FieldToZ_ZToField : ZToField - . - Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. Proof. apply F_eq. @@ -132,15 +140,15 @@ Proof. reflexivity. Qed. -Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. +Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) Definition B_nonzero : B <> zero. Admitted. Definition l_order_B : scalarMult l B = zero. Admitted. -Instance x : EdDSAParams := { - E := TEParams; +Local Instance ed25519params : EdDSAParams := { + E := curve25519params; b := b; H := H; c := c; @@ -160,3 +168,7 @@ Instance x : EdDSAParams := { l_odd := l_odd; l_order_B := l_order_B }. + +Definition ed25519_verify + : forall (pubkey:word b) (len:nat) (msg:word len) (sig:word (b+b)), bool + := @verify ed25519params.
\ No newline at end of file diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 45950f6a1..3decae6a7 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -4,8 +4,8 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Util.WordUtil. Require Bedrock.Word. -Require Znumtheory BinInt. -Require NPeano. +Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. +Require Coq.Numbers.Natural.Peano.NPeano. Coercion Word.wordToNat : Word.word >-> nat. @@ -14,6 +14,7 @@ Infix "mod" := NPeano.modulo. Infix "++" := Word.combine. Section EdDSAParams. + Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) E : TwistedEdwardsParams; (* underlying elliptic curve *) @@ -70,14 +71,12 @@ Section EdDSA. (r + H (enc R ++ public sk ++ M) * s)) in enc R ++ enc S. - Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. - Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. 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 point with None => false | Some A => match dec R_ : option point with None => false | Some R => - match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A then true else false end diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v index 7bef9295b..14cf9d9d9 100644 --- a/src/Spec/Encoding.v +++ b/src/Spec/Encoding.v @@ -1,8 +1,8 @@ -Require Import ZArith.ZArith Zpower ZArith. -Require Import NPeano. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.WordUtil. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index da6a62ada..76efe3d79 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -1,4 +1,4 @@ -Require Znumtheory BinNums. +Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums. Require Crypto.ModularArithmetic.Pre. diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 2fec05863..e1d3744fb 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -1,11 +1,11 @@ -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import NPeano NArith. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. Require Import Crypto.Spec.Encoding Crypto.Encoding.EncodingTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope F_scope. @@ -57,6 +57,18 @@ Section PointEncoding. Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N. Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in WS (sign_bit x) (enc y). +Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) := + match dec (wtl w) with + | None => None + | Some y => let x2 := solve_for_x2 y in + let x := sqrt_mod_q x2 in + if F_eq_dec (x ^ 2) x2 + then if Bool.eqb (whd w) (sign_bit x) + then Some (x, y) + else Some (opp x, y) + else None + end. + Definition point_dec (w : word (S sz)) : option point := match dec (wtl w) with | None => None @@ -70,6 +82,15 @@ Definition point_dec (w : word (S sz)) : option point := end end. +Lemma point_dec_coordinates_correct w + : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w. +Proof. + unfold point_dec, point_dec_coordinates. + edestruct dec; [ | reflexivity ]. + edestruct @F_eq_dec; [ | reflexivity ]. + edestruct @Bool.eqb; reflexivity. +Qed. + Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)). Proof. intros. diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v new file mode 100644 index 000000000..32de3dc13 --- /dev/null +++ b/src/Specific/Ed25519.v @@ -0,0 +1,255 @@ +Require Import Bedrock.Word. +Require Import Crypto.Spec.Ed25519. +Require Import Crypto.Tactics.VerdiTactics. +Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. +Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.Util.IterAssocOp. + +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'} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z + (op_proj : forall a b, proj (op a b) = op' (proj a) (proj b)) + : proj (iter_op op x y z) = iter_op op' (proj x) y (proj z). +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. + +Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool. +Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false. + +Axiom Bc : F q * F q. +Axiom B_proj : proj1_sig B = Bc. + +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 "==?" := point_eqb (at level 70) : E_scope. + +Axiom negate : point -> point. +Definition point_sub P Q := (P + negate Q)%E. +Infix "-" := point_sub : E_scope. +Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. + +Axiom negateExtendedc : extended -> extended. +Definition negateExtended : extendedPoint -> extendedPoint. +Proof. + intro x. + exists (negateExtendedc (proj1_sig x)). + admit. +Defined. +Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). + +Local Existing Instance PointEncoding. +Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. + +Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option point => bool) + (fun S : 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 (S (b - 1)). +Proof. + intro x. + let enc' := (eval hnf in (@enc (@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 (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) + := eq_refl. + +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 + | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] + => etransitivity; + [ + | refine (_ : option_rect (fun _ => T) _ N a = _); + let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in + refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) + (fun x => _) _ a); intros; simpl @option_rect ]; + [ reflexivity | .. ] + end. + set_evars. + rewrite<- point_eqb_correct. + rename x0 into R. rename x1 into S. rename x into A. + rewrite solve_for_R. + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in + repeat match goal with + | |- context [(_ * ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite <-p1 + | |- context [(?P + unExtendedPoint _)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + 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. + + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + unfold point_sub. rewrite negateExtended_correct. + let p := constr:(unifiedAddM1_rep eq_refl) in rewrite p. + reflexivity. + } Unfocus. + + rewrite enc'_correct. + cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. + unfold proj1_sig at 1 2 5 6. + 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 ?x ?y ?z)] ] + => erewrite (@iter_op_proj T A (@proj1_sig _ _)) by reflexivity + end. + subst_evars. + reflexivity. } + Unfocus. + + cbv [mkExtendedPoint zero mkPoint]. + unfold proj1_sig at 1 2 3 5 6 7. + 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 zeta delta [test_and_op]. + Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *) + + Axiom rep : forall {m}, list Z -> F m -> Prop. + Axiom decode_point_limbs : word (S (b-1)) -> option (list Z * list Z). + Axiom point_dec_rep : forall P_ P lx ly, dec P_ = Some P -> decode_point_limbs P_ = Some (lx, ly) -> rep lx (fst (proj1_sig P)) /\ rep ly (fst (proj1_sig P)).*) +Admitted. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 795c360ed..14a7332e7 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,12 +1,12 @@ -Require Import ModularArithmetic.PrimeFieldTheorems. -Require Import ModularArithmetic.PseudoMersenneBaseRep. -Require Import ModularArithmetic.PseudoMersenneBaseParams. -Require Import BaseSystem ModularBaseSystem. -Require Import List Util.ListUtil. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Coq.Lists.List Crypto.Util.ListUtil. Import ListNotations. -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import QArith.QArith QArith.Qround. -Require Import VerdiTactics. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.QArith.QArith Coq.QArith.Qround. +Require Import Crypto.Tactics.VerdiTactics. Close Scope Q. Local Open Scope Z. diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v index 35f207ffc..af04a1e49 100644 --- a/src/Util/CaseUtil.v +++ b/src/Util/CaseUtil.v @@ -1,4 +1,4 @@ -Require Import Arith. +Require Import Coq.Arith.Arith. Ltac case_max := match goal with [ |- context[max ?x ?y] ] => diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index fc21b997b..5e23bb987 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,5 +1,5 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Require Import NArith BinPosDef. +Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. Local Open Scope equiv_scope. Generalizable All Variables. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 783e3f527..1f9a62457 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Omega. -Require Import Arith.Peano_dec. -Require Import VerdiTactics. +Require Import Coq.Lists.List. +Require Import Coq.omega.Omega. +Require Import Coq.Arith.Peano_dec. +Require Import Crypto.Tactics.VerdiTactics. Ltac boring := simpl; intuition; diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 4ba6d0808..6a62d6c22 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,4 @@ -Require Import NPeano Omega. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Local Open Scope nat_scope. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 5acef8b75..10ce148b0 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -1,8 +1,8 @@ -Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. Require Import Coqprime.Zp. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z. (* TODO: move somewhere else for lemmas about Coqprime? *) diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 49de971ef..17d04c60a 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,5 @@ -Require Import NPeano. -Require Import ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.ZArith.ZArith. Require Import Bedrock.Word. Local Open Scope nat_scope. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 2cfab2e90..db3d84b2d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,5 @@ -Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Local Open Scope Z. |