From 7854ab5071ae4ddb6d125187865f3340dfe9f184 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 3 Jul 2016 00:16:31 -0700 Subject: Implement and prove Barrett reduction on Z (#18) Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia). --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 904d716b8..beac11f07 100644 --- a/_CoqProject +++ b/_CoqProject @@ -43,6 +43,7 @@ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v +src/ModularArithmetic/BarrettReduction/Z.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v -- cgit v1.2.3 From 0cea3e2f80408a25954f820faebf5cd79d2e13ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 3 Jul 2016 00:22:13 -0700 Subject: Define the spec of Weierstrass curves (#6) Define the spec of Weierstrass curves This is the start of work on P256. --- _CoqProject | 2 ++ src/Spec/WeierstrassCurve.v | 84 +++++++++++++++++++++++++++++++++++++++++++++ src/WeierstrassCurve/Pre.v | 57 ++++++++++++++++++++++++++++++ 3 files changed, 143 insertions(+) create mode 100644 src/Spec/WeierstrassCurve.v create mode 100644 src/WeierstrassCurve/Pre.v (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index beac11f07..22af15eb5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -49,6 +49,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v +src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/Nsatz.v @@ -67,3 +68,4 @@ src/Util/Tuple.v src/Util/Unit.v src/Util/WordUtil.v src/Util/ZUtil.v +src/WeierstrassCurve/Pre.v diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v new file mode 100644 index 000000000..7ec5d99ec --- /dev/null +++ b/src/Spec/WeierstrassCurve.v @@ -0,0 +1,84 @@ +Require Crypto.WeierstrassCurve.Pre. + +Module E. + Section WeierstrassCurves. + (* Short Weierstrass curves with addition laws. References: + * + * + * See also: + * (page 79) + *) + + 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 Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3). + Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))). + Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))). + Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))). + + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F}. + + (** N.B. We may require more conditions to prove that points form + a group under addition (associativity, in particular. If + that's the case, more fields will be added to this class. *) + Class weierstrass_params := + { + char_gt_2 : 2 <> 0; + char_ne_3 : 3 <> 0; + nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0 + }. + Context `{weierstrass_params}. + + Definition point := { P | match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end }. + Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + + (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *) + Local Obligation Tactic := + try solve [ Program.Tactics.program_simpl + | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ]. + + Program Definition zero : point := ∞. + + Program Definition add (P1 P2:point) : point + := exist + _ + (match coordinates P1, coordinates P2 return _ with + | (x1, y1), (x2, y2) => + if x1 =? x2 then + if y2 =? -y1 then ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + end) + _. + + Fixpoint mul (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => add P (mul n' P) + end. + End WeierstrassCurves. +End E. + +Delimit Scope E_scope with E. +Infix "+" := E.add : E_scope. +Infix "*" := E.mul : E_scope. diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v new file mode 100644 index 000000000..060d2f479 --- /dev/null +++ b/src/WeierstrassCurve/Pre.v @@ -0,0 +1,57 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope core_scope. + +Generalizable All Variables. +Section Pre. + 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" := (opp x). + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "( x , y )" := (inl (pair x y)). + + Add Field WeierstrassCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + Add Ring WeierstrassCurveRing : (Ring.ring_theory_for_stdlib_tactic (T:=F)). + + Context {a:F}. + Context {b:F}. + + (* the canonical definitions are in Spec *) + Definition onCurve (P:F*F + ∞) := match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end. + Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ := + match P1', P2' with + | (x1, y1), (x2, y2) + => if x1 =? x2 then + if y2 =? -y1 then + ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else + ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => P2' + | _, ∞ => P1' + end. + + Lemma unifiedAdd'_onCurve : forall P1 P2, + onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). + Proof. + unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2; + break_match; trivial; setoid_subst_rel eq; only_two_square_roots; + field_algebra; nsatz_contradict. + Qed. +End Pre. -- cgit v1.2.3 From e4bbfc3ba802d6a8fc1eca47da5202b22b1decaf Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 6 Jul 2016 12:45:20 -0400 Subject: Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util. --- _CoqProject | 2 + src/ModularArithmetic/ModularBaseSystem.v | 20 +- src/ModularArithmetic/ModularBaseSystemOpt.v | 6 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 294 +++---------------- src/ModularArithmetic/Pow2Base.v | 43 +++ src/ModularArithmetic/Pow2BaseProofs.v | 320 +++++++++++++++++++++ .../PseudoMersenneBaseParamProofs.v | 197 ++----------- src/ModularArithmetic/PseudoMersenneBaseParams.v | 3 +- src/Util/ListUtil.v | 153 +++++++++- src/Util/ZUtil.v | 20 ++ 10 files changed, 599 insertions(+), 459 deletions(-) create mode 100644 src/ModularArithmetic/Pow2Base.v create mode 100644 src/ModularArithmetic/Pow2BaseProofs.v (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 904d716b8..55973017b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,6 +37,8 @@ src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v +src/ModularArithmetic/Pow2Base.v +src/ModularArithmetic/Pow2BaseProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index daad9443a..856cb1e81 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -8,6 +8,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Notations. +Require Import Crypto.ModularArithmetic.Pow2Base. Local Open Scope Z_scope. Section PseudoMersenneBase. @@ -19,16 +20,8 @@ Section PseudoMersenneBase. Local Notation "u ~= x" := (rep u x). Local Hint Unfold rep. - (* i is current index, counts down *) - Fixpoint encode' z i : digits := - match i with - | O => nil - | S i' => let lw := sum_firstn limb_widths in - encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil - end. - (* max must be greater than input; this is used to truncate last digit *) - Definition encode (x : F modulus) := encode' x (length base). + Definition encode (x : F modulus) := encodeZ limb_widths x. (* Converts from length of extended base to length of base by reduction modulo M.*) Definition reduce (us : digits) : digits := @@ -110,15 +103,6 @@ Section Canonicalization. (* compute at compile time *) Definition modulus_digits := modulus_digits' (length base - 1). - Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := - match la with - | nil => nil - | a :: la' => match lb with - | nil => nil - | b :: lb' => f a b :: map2 f la' lb' - end - end. - Definition and_term us := if isFull us then max_ones else 0. Definition freeze us := diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 4f918e147..bb9b1674e 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -45,10 +45,12 @@ Ltac opt_step := destruct e end. -Ltac brute_force_indices limb_widths := intros; unfold sum_firstn, limb_widths; simpl in *; +Ltac brute_force_indices limb_widths := + intros; unfold sum_firstn, limb_widths; cbv [length limb_widths] in *; repeat match goal with | _ => progress simpl in * - | _ => reflexivity + | [H : (0 + _ < _)%nat |- _ ] => simpl in H + | [H : (S _ + _ < S _)%nat |- _ ] => simpl in H | [H : (S _ < S _)%nat |- _ ] => apply lt_S_n in H | [H : (?x + _ < _)%nat |- _ ] => is_var x; destruct x | [H : (?x < _)%nat |- _ ] => is_var x; destruct x diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 544670f9b..75806f570 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -5,10 +5,15 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypt Require Import VerdiTactics. Require Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.Pow2BaseProofs. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. + Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. @@ -17,6 +22,7 @@ Section PseudoMersenneProofs. Local Notation "u .+ x" := (add u x). Local Notation "u .* x" := (ModularBaseSystem.mul u x). Local Hint Unfold rep. + Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. Lemma rep_decode : forall us x, us ~= x -> decode us = x. Proof. @@ -39,27 +45,18 @@ Section PseudoMersenneProofs. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. - (* TODO : move to ListUtil *) - Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d, - (forall x, In x l -> P x) -> P d -> P (nth_default d l n). - Proof. - intros; rewrite nth_default_eq. - destruct (nth_in_or_default n l d); auto. - congruence. - Qed. - - Lemma encode'_eq : forall (x : F modulus) i, (i <= length base)%nat -> - encode' x i = BaseSystem.encode' base x (2 ^ k) i. + Lemma encode'_eq : forall (x : F modulus) i, (i <= length limb_widths)%nat -> + encode' limb_widths x i = BaseSystem.encode' base x (2 ^ k) i. Proof. - induction i; intros. + rewrite <-base_length; induction i; intros. + rewrite encode'_zero. reflexivity. + rewrite encode'_succ, <-IHi by omega. simpl; do 2 f_equal. - rewrite Z.land_ones, Z.shiftr_div_pow2 by apply sum_firstn_limb_widths_nonneg. + rewrite Z.land_ones, Z.shiftr_div_pow2 by auto. match goal with H : (S _ <= length base)%nat |- _ => apply le_lt_or_eq in H; destruct H end. - - repeat f_equal; rewrite nth_default_base by omega; reflexivity. - - repeat f_equal; try solve [rewrite nth_default_base by omega; reflexivity]. + - repeat f_equal; unfold base in *; rewrite nth_default_base by (auto || omega); reflexivity. + - repeat f_equal; try solve [unfold base in *; rewrite nth_default_base by (auto || omega); reflexivity]. rewrite nth_default_out_of_bounds by omega. unfold k. rewrite <-base_length; congruence. @@ -69,7 +66,7 @@ Section PseudoMersenneProofs. encode x = BaseSystem.encode base x (2 ^ k). Proof. unfold encode, BaseSystem.encode; intros. - apply encode'_eq; omega. + rewrite base_length; apply encode'_eq; omega. Qed. Lemma encode_rep : forall x : F modulus, encode x ~= x. @@ -94,9 +91,9 @@ Section PseudoMersenneProofs. * rewrite !nth_default_eq. do 2 (erewrite nth_indep with (d := 2 ^ k) (d' := 0) by omega). rewrite <-!nth_default_eq. - apply base_succ; omega. + apply base_succ; auto; omega. - rewrite nth_default_out_of_bounds with (n := S i) by omega. - rewrite nth_default_base by omega. + unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). unfold k. match goal with H : S _ = length base |- _ => rewrite base_length in H; rewrite <-H end. @@ -349,160 +346,13 @@ Section PseudoMersenneProofs. apply Z.log2_lt_pow2; auto. Qed. - Fixpoint decode_bitwise' us i acc := - match i with - | O => acc - | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc (log_cap i'))) - end. - - Definition decode_bitwise us := decode_bitwise' us (length us) 0. - - - (* TODO : move to ZUtil *) - Lemma Z_lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> - Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). - Proof. - intros. - apply Z.bits_inj'; intros t ?. - rewrite Z.lor_spec, Z.shiftl_spec by assumption. - destruct (Z_lt_dec t n). - + rewrite Z_testbit_add_shiftl_low by omega. - rewrite Z.testbit_neg_r with (n := t - n) by omega. - apply Bool.orb_false_r. - + rewrite Z_testbit_add_shiftl_high by omega. - replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. - symmetry. - apply Z.testbit_false; try omega. - rewrite Z.div_small; try reflexivity. - split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. - apply Z.pow_le_mono_r; omega. - Qed. - - Lemma decode_bitwise'_succ : forall us i acc, carry_done us -> length us = length base -> - decode_bitwise' us (S i) acc = decode_bitwise' us i (acc * (2 ^ log_cap i) + nth_default 0 us i). - Proof. - intros. - simpl; f_equal. - rewrite Z_lor_shiftl by (auto; rewrite carry_done_bounds in H by assumption; - specialize (H i); assumption). - rewrite Z.shiftl_mul_pow2 by auto. - ring. - Qed. - - (* c is a counter, allows i to count up rather than down *) - Fixpoint partial_decode us i c := - match c with - | O => 0 - | S c' => (partial_decode us (S i) c' * 2 ^ log_cap i) + nth_default 0 us i - end. - - Lemma base_shift_log_cap : forall us, BaseSystem.decode' (skipn 1 base) us = - BaseSystem.decode' base us * 2 ^ log_cap 0. - Admitted. - - Lemma decode_cons_log_cap : forall us u0, - BaseSystem.decode' base (u0 :: us) = u0 + BaseSystem.decode' base us * 2 ^ log_cap 0. - Proof. - intros. - rewrite decode_cons by apply bv. - f_equal. - replace (0 :: us) with (BaseSystem.zeros 1%nat ++ us) by reflexivity. - rewrite decode'_splice, zeros_rep, length_zeros. - apply base_shift_log_cap. - Qed. - - Lemma partial_decode_counter_over : forall c us i, (c >= length us - i)%nat -> - partial_decode us i c = partial_decode us i (length us - i). - Proof. - induction c; intros. - + f_equal. omega. - + simpl. rewrite IHc by omega. - case_eq (length us - i)%nat; intros. - - rewrite nth_default_out_of_bounds by omega. - replace (length us - S i)%nat with 0%nat by omega. - reflexivity. - - simpl. repeat f_equal. omega. - Qed. - - Lemma partial_decode_counter_subst : forall c c' us i, - (c >= length us - i)%nat -> (c' >= length us - i)%nat -> - partial_decode us i c = partial_decode us i c'. - Proof. - intros. - rewrite partial_decode_counter_over by assumption. - symmetry. - auto using partial_decode_counter_over. - Qed. - - Lemma partial_decode_succ : forall c us i, (c >= length us - i)%nat -> - partial_decode us (S i) c * 2 ^ log_cap i + nth_default 0 us i = - partial_decode us i c. - Proof. - intros. - rewrite partial_decode_counter_subst with (i := i) (c' := S c) by omega. - reflexivity. - Qed. - - Lemma partial_decode_intermediate : forall c us i, length us = length base -> - (c >= length us - i)%nat -> - partial_decode us i c = BaseSystem.decode' (base_from_limb_widths (skipn i limb_widths)) (skipn i us). - Proof. - induction c; intros. - + simpl. rewrite skipn_all by (rewrite <-base_length; omega). - symmetry; apply decode_base_nil. - + simpl. - destruct (lt_dec i (length base)). - - rewrite IHc by omega. - do 2 (rewrite skipn_nth_default with (n := i) (d := 0) by (rewrite <-?base_length; omega)). - unfold base_from_limb_widths; fold base_from_limb_widths. - rewrite peel_decode. - fold (BaseSystem.mul_each (two_p (nth_default 0 limb_widths i))). - rewrite <-mul_each_base, mul_each_rep, two_p_correct. - ring_simplify. - f_equal; ring. - - rewrite <- IHc by omega. - apply partial_decode_succ; omega. - Qed. - - - Lemma decode_bitwise'_succ_partial_decode : forall us i c, - carry_done us -> length us = length base -> - decode_bitwise' us (S i) (partial_decode us (S i) c) = - decode_bitwise' us i (partial_decode us i (S c)). - Proof. - intros. - rewrite decode_bitwise'_succ by auto. - f_equal. - Qed. - - Lemma decode_bitwise'_spec : forall us i, (i <= length base)%nat -> - carry_done us -> length us = length base -> - decode_bitwise' us i (partial_decode us i (length us - i)) = - BaseSystem.decode base us. - Proof. - induction i; intros. - + rewrite partial_decode_intermediate by auto. - reflexivity. - + rewrite decode_bitwise'_succ_partial_decode by auto. - replace (S (length us - S i)) with (length us - i)%nat by omega. - apply IHi; auto; omega. - Qed. - - Lemma decode_bitwise_spec : forall us, carry_done us -> length us = length base -> - decode_bitwise us = BaseSystem.decode base us. - Proof. - unfold decode, decode_bitwise; intros. - replace 0 with (partial_decode us (length us) (length us - length us)) by - (rewrite Nat.sub_diag; reflexivity). - apply decode_bitwise'_spec; auto; omega. - Qed. - End PseudoMersenneProofs. Section CarryProofs. Context `{prm : PseudoMersenneBaseParams}. Local Notation "u ~= x" := (rep u x). Hint Unfold log_cap. + Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. Lemma base_length_lt_pred : (pred (length base) < length base)%nat. Proof. @@ -514,8 +364,8 @@ Section CarryProofs. nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i. Proof. intros. - repeat rewrite nth_default_base by omega. - rewrite <- Z.pow_add_r by (apply log_cap_nonneg || apply sum_firstn_limb_widths_nonneg). + unfold base; repeat rewrite nth_default_base by (unfold base in *; omega || auto). + rewrite <- Z.pow_add_r by auto using log_cap_nonneg. destruct (NPeano.Nat.eq_dec i 0). + subst; f_equal. unfold sum_firstn, log_cap. @@ -569,7 +419,7 @@ Section CarryProofs. unfold log_cap. subst; rewrite length_zero, limbs_length, nth_default_nil. reflexivity. - + rewrite nth_default_base by omega. + + unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). rewrite <- Z.add_opp_l, <- Z.opp_sub_distr. unfold pow2_mod. rewrite Z.land_ones by apply log_cap_nonneg. @@ -578,7 +428,7 @@ Section CarryProofs. rewrite Zopp_mult_distr_r. rewrite Z.mul_comm. rewrite Z.mul_assoc. - rewrite <- Z.pow_add_r by (apply log_cap_nonneg || apply sum_firstn_limb_widths_nonneg). + rewrite <- Z.pow_add_r by auto using log_cap_nonneg. unfold k. replace (length limb_widths) with (S (pred (length base))) by (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega). @@ -587,6 +437,7 @@ Section CarryProofs. rewrite <- Zopp_mult_distr_r. rewrite Z.mul_comm. rewrite (Z.add_comm (log_cap (pred (length base)))). + unfold base. ring. Qed. @@ -627,7 +478,6 @@ Section CarryProofs. induction is; boring. Qed. - (* TODO : move? *) Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. Proof. @@ -1492,63 +1342,6 @@ Section CanonicalizationProofs. Qed. Local Hint Resolve carry_full_3_length. - Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, - nth_default d (map2 f ls1 ls2) i = - if lt_dec i (min (length ls1) (length ls2)) - then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) - else d. - Proof. - induction ls1, ls2. - + cbv [map2 length min]. - intros. - break_if; try omega. - apply nth_default_nil. - + cbv [map2 length min]. - intros. - break_if; try omega. - apply nth_default_nil. - + cbv [map2 length min]. - intros. - break_if; try omega. - apply nth_default_nil. - + simpl. - destruct i. - - intros. rewrite !nth_default_cons. - break_if; auto; omega. - - intros. rewrite !nth_default_cons_S. - rewrite IHls1 with (d1 := d1) (d2 := d2). - repeat break_if; auto; omega. - Qed. - - Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b, - map2 f (a :: ls1) (b :: ls2) = f a b :: map2 f ls1 ls2. - Proof. - reflexivity. - Qed. - - Lemma map2_nil_l : forall A B C (f : A -> B -> C) ls2, - map2 f nil ls2 = nil. - Proof. - reflexivity. - Qed. - - Lemma map2_nil_r : forall A B C (f : A -> B -> C) ls1, - map2 f ls1 nil = nil. - Proof. - destruct ls1; reflexivity. - Qed. - Local Hint Resolve map2_nil_r map2_nil_l. - - Opaque map2. - - Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, - length (map2 f ls1 ls2) = min (length ls1) (length ls2). - Proof. - induction ls1, ls2; intros; try solve [cbv; auto]. - rewrite map2_cons, !length_cons, IHls1. - auto. - Qed. - Lemma modulus_digits'_length : forall i, length (modulus_digits' i) = S i. Proof. induction i; intros; [ cbv; congruence | ]. @@ -1598,15 +1391,6 @@ Section CanonicalizationProofs. Local Hint Resolve limb_widths_nonneg. Local Hint Resolve nth_error_value_In. - (* TODO : move *) - Lemma sum_firstn_all_succ : forall n l, (length l <= n)%nat -> - sum_firstn l (S n) = sum_firstn l n. - Proof. - unfold sum_firstn; intros. - rewrite !firstn_all_strong by omega. - congruence. - Qed. - Lemma decode_carry_done_upper_bound' : forall n us, carry_done us -> (length us = length base) -> BaseSystem.decode (firstn n base) (firstn n us) < 2 ^ (sum_firstn limb_widths n). @@ -1618,7 +1402,9 @@ Section CanonicalizationProofs. destruct (nth_error_length_exists_value _ _ n_lt_length). erewrite sum_firstn_succ; eauto. rewrite Z.pow_add_r; eauto. - rewrite nth_default_base by (rewrite base_length; assumption). + unfold base. + rewrite nth_default_base by + (unfold base in *; try rewrite base_from_limb_widths_length; omega || auto). rewrite Z.lt_add_lt_sub_r. eapply Z.lt_le_trans; eauto. rewrite Z.mul_comm at 1. @@ -1655,7 +1441,7 @@ Section CanonicalizationProofs. destruct (lt_dec n (length base)) as [ n_lt_length | ? ]. + rewrite decode_firstn_succ by auto. zero_bounds. - - rewrite nth_default_base by assumption. + - unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). apply Z.pow_nonneg; omega. - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. intuition. @@ -1714,7 +1500,6 @@ Section CanonicalizationProofs. Qed. Local Hint Resolve carry_done_modulus_digits. - (* TODO : move *) Lemma decode_mod : forall us vs x, (length us = length base) -> (length vs = length base) -> decode us = x -> BaseSystem.decode base us mod modulus = BaseSystem.decode base vs mod modulus -> @@ -1726,23 +1511,6 @@ Section CanonicalizationProofs. assumption. Qed. - Ltac simpl_list_lengths := repeat match goal with - | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H - | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H - | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) - | |- appcontext[length (_ :: _)] => rewrite length_cons - end. - - Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2', - (length ls1 = length ls2) -> - map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. - Proof. - induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; - simpl_list_lengths; try omega. - rewrite <-!app_comm_cons, !map2_cons. - rewrite IHls1; auto. - Qed. - Lemma decode_map2_sub : forall us vs, (length us = length vs) -> BaseSystem.decode' base (map2 (fun x y => x - y) us vs) @@ -1770,7 +1538,7 @@ Section CanonicalizationProofs. intros z ? base_eq. rewrite decode'_cons, decode_nil, Z.add_0_r. replace z with (nth_default 0 base 0) by (rewrite base_eq; auto). - rewrite nth_default_base by omega. + unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). replace (max_bound 0 - c + 1) with (Z.succ (max_bound 0) - c) by ring. rewrite max_bound_log_cap. rewrite sum_firstn_succ with (x := log_cap 0) by (rewrite log_cap_eq; @@ -1784,7 +1552,8 @@ Section CanonicalizationProofs. (rewrite log_cap_eq; apply nth_error_Some_nth_default; rewrite <-base_length; omega). rewrite Z.pow_add_r, <-max_bound_log_cap, set_higher by auto. - rewrite IHi, modulus_digits'_length, nth_default_base by omega. + rewrite IHi, modulus_digits'_length by omega. + unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). ring. - rewrite sum_firstn_all_succ by (rewrite <-base_length; omega). rewrite decode'_splice, modulus_digits'_length, firstn_all by auto. @@ -1962,7 +1731,8 @@ Section CanonicalizationProofs. + eapply Z.le_lt_trans. - eapply Z.add_le_mono with (q := nth_default 0 base n * -1); [ apply Z.le_refl | ]. apply Z.mul_le_mono_nonneg_l; try omega. - rewrite nth_default_base by omega; apply Z.pow_nonneg; omega. + unfold base; rewrite nth_default_base by (unfold base in *; omega || auto). + zero_bounds. - ring_simplify. apply Z.lt_sub_0. apply decode_lt_next_digit; auto. @@ -2302,4 +2072,4 @@ Section CanonicalizationProofs. eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs. +End CanonicalizationProofs. \ No newline at end of file diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v new file mode 100644 index 000000000..847967f52 --- /dev/null +++ b/src/ModularArithmetic/Pow2Base.v @@ -0,0 +1,43 @@ +Require Import Zpower ZArith. +Require Import Crypto.Util.ListUtil. +Require Import Coq.Lists.List. + +Local Open Scope Z_scope. + +Section Pow2Base. + Context (limb_widths : list Z). + Local Notation "w[ i ]" := (nth_default 0 limb_widths i). + + Fixpoint base_from_limb_widths limb_widths := + match limb_widths with + | nil => nil + | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw) + end. + + Local Notation "{base}" := (base_from_limb_widths limb_widths). + + + Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i]. + + Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)). + + Fixpoint decode_bitwise' us i acc := + match i with + | O => acc + | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc w[i'])) + end. + + Definition decode_bitwise us := decode_bitwise' us (length us) 0. + + (* i is current index, counts down *) + Fixpoint encode' z i := + match i with + | O => nil + | S i' => let lw := sum_firstn limb_widths in + encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil + end. + + (* max must be greater than input; this is used to truncate last digit *) + Definition encodeZ x:= encode' x (length limb_widths). + +End Pow2Base. \ No newline at end of file diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v new file mode 100644 index 000000000..23393d7ef --- /dev/null +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -0,0 +1,320 @@ +Require Import Zpower ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil. +Require Import Crypto.ModularArithmetic.Pow2Base Crypto.BaseSystemProofs. +Require Crypto.BaseSystem. +Local Open Scope Z_scope. + +Section Pow2BaseProofs. + Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). + Local Notation "{base}" := (base_from_limb_widths limb_widths). + + Lemma base_from_limb_widths_length : length {base} = length limb_widths. + Proof. + induction limb_widths; try reflexivity. + simpl; rewrite map_length. + simpl in limb_widths_nonneg. + rewrite IHl; auto. + Qed. + + Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. + Proof. + unfold sum_firstn; intros. + apply fold_right_invariant; try omega. + intros y In_y_lw ? ?. + apply Z.add_nonneg_nonneg; try assumption. + apply limb_widths_nonneg. + eapply In_firstn; eauto. + Qed. Hint Resolve sum_firstn_limb_widths_nonneg. + + Lemma base_from_limb_widths_step : forall i b w, (S i < length {base})%nat -> + nth_error {base} i = Some b -> + nth_error limb_widths i = Some w -> + nth_error {base} (S i) = Some (two_p w * b). + Proof. + induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; + unfold base_from_limb_widths in *; fold base_from_limb_widths in *; + [rewrite (@nil_length0 Z) in *; omega | ]. + simpl in *; rewrite map_length in *. + case_eq i; intros; subst. + + subst; apply nth_error_first in nth_err_w. + apply nth_error_first in nth_err_b; subst. + apply map_nth_error. + case_eq l; intros; subst; [simpl in *; omega | ]. + unfold base_from_limb_widths; fold base_from_limb_widths. + reflexivity. + + simpl in nth_err_w. + apply nth_error_map in nth_err_w. + destruct nth_err_w as [x [A B]]. + subst. + replace (two_p w * (two_p a * x)) with (two_p a * (two_p w * x)) by ring. + apply map_nth_error. + apply IHl; auto. omega. + Qed. + + + Lemma nth_error_base : forall i, (i < length {base})%nat -> + nth_error {base} i = Some (two_p (sum_firstn limb_widths i)). + Proof. + induction i; intros. + + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. + intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. + + assert (i < length {base})%nat as lt_i_length by omega. + specialize (IHi lt_i_length). + rewrite base_from_limb_widths_length in lt_i_length. + destruct (nth_error_length_exists_value _ _ lt_i_length) as [w nth_err_w]. + erewrite base_from_limb_widths_step; eauto. + f_equal. + simpl. + destruct (NPeano.Nat.eq_dec i 0). + - subst; unfold sum_firstn; simpl. + apply nth_error_exists_first in nth_err_w. + destruct nth_err_w as [l' lw_destruct]; subst. + simpl; ring_simplify. + f_equal; ring. + - erewrite sum_firstn_succ; eauto. + symmetry. + apply two_p_is_exp; auto using sum_firstn_limb_widths_nonneg. + apply limb_widths_nonneg. + eapply nth_error_value_In; eauto. + Qed. + + Lemma nth_default_base : forall d i, (i < length {base})%nat -> + nth_default d {base} i = 2 ^ (sum_firstn limb_widths i). + Proof. + intros ? ? i_lt_length. + destruct (nth_error_length_exists_value _ _ i_lt_length) as [x nth_err_x]. + unfold nth_default. + rewrite nth_err_x. + rewrite nth_error_base in nth_err_x by assumption. + rewrite two_p_correct in nth_err_x. + congruence. + Qed. + + Lemma base_succ : forall i, ((S i) < length {base})%nat -> + nth_default 0 {base} (S i) mod nth_default 0 {base} i = 0. + Proof. + intros. + repeat rewrite nth_default_base by omega. + apply mod_same_pow. + split; [apply sum_firstn_limb_widths_nonneg | ]. + destruct (NPeano.Nat.eq_dec i 0); subst. + + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. + apply Z.add_nonneg_nonneg; try omega. + apply limb_widths_nonneg. + rewrite lw_eq. + apply in_eq. + + assert (i < length {base})%nat as i_lt_length by omega. + rewrite base_from_limb_widths_length in *. + apply nth_error_length_exists_value in i_lt_length. + destruct i_lt_length as [x nth_err_x]. + erewrite sum_firstn_succ; eauto. + apply nth_error_value_In in nth_err_x. + apply limb_widths_nonneg in nth_err_x. + omega. + Qed. + + Lemma nth_error_subst : forall i b, nth_error {base} i = Some b -> + b = 2 ^ (sum_firstn limb_widths i). + Proof. + intros i b nth_err_b. + pose proof (nth_error_value_length _ _ _ _ nth_err_b). + rewrite nth_error_base in nth_err_b by assumption. + rewrite two_p_correct in nth_err_b. + congruence. + Qed. + +End Pow2BaseProofs. + +Section BitwiseDecodeEncode. + Context {limb_widths} (bv : BaseSystem.BaseVector (base_from_limb_widths limb_widths)) + (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). + Local Hint Resolve limb_widths_nonneg. + Local Notation "w[ i ]" := (nth_default 0 limb_widths i). + Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation "{max}" := (upper_bound limb_widths). + + Lemma encode'_spec : forall x i, (i <= length {base})%nat -> + encode' limb_widths x i = BaseSystem.encode' {base} x {max} i. + Proof. + induction i; intros. + + rewrite encode'_zero. reflexivity. + + rewrite encode'_succ, <-IHi by omega. + simpl; do 2 f_equal. + rewrite Z.land_ones, Z.shiftr_div_pow2 by auto using sum_firstn_limb_widths_nonneg. + match goal with H : (S _ <= length {base})%nat |- _ => + apply le_lt_or_eq in H; destruct H end. + - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity. + - repeat f_equal; try solve [rewrite nth_default_base by (omega || auto); reflexivity]. + rewrite nth_default_out_of_bounds by omega. + unfold upper_bound. + rewrite <-base_from_limb_widths_length by auto. + congruence. + Qed. + + Lemma nth_default_limb_widths_nonneg : forall i, 0 <= w[i]. + Proof. + intros; apply nth_default_preserves_properties; auto; omega. + Qed. Hint Resolve nth_default_limb_widths_nonneg. + + Lemma base_upper_bound_compatible : @base_max_succ_divide {base} {max}. + Proof. + unfold base_max_succ_divide; intros i lt_Si_length. + rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; + rewrite !nth_default_base by (omega || auto). + + erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); + rewrite <-base_from_limb_widths_length by auto; omega). + rewrite Z.pow_add_r; auto using sum_firstn_limb_widths_nonneg. + apply Z.divide_factor_r. + + rewrite nth_default_out_of_bounds by omega. + unfold upper_bound. + replace (length limb_widths) with (S (pred (length limb_widths))) by + (rewrite base_from_limb_widths_length in H by auto; omega). + replace i with (pred (length limb_widths)) by + (rewrite base_from_limb_widths_length in H by auto; omega). + erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); + rewrite <-base_from_limb_widths_length by auto; omega). + rewrite Z.pow_add_r; auto using sum_firstn_limb_widths_nonneg. + apply Z.divide_factor_r. + Qed. + Hint Resolve base_upper_bound_compatible. + + Lemma encodeZ_spec : forall x, + BaseSystem.decode {base} (encodeZ limb_widths x) = x mod {max}. + Proof. + intros. + assert (length {base} = length limb_widths) by auto using base_from_limb_widths_length. + unfold encodeZ; rewrite encode'_spec by omega. + rewrite BaseSystemProofs.encode'_spec; unfold upper_bound; try zero_bounds; + auto using sum_firstn_limb_widths_nonneg. + rewrite nth_default_out_of_bounds by omega. + reflexivity. + Qed. + + Lemma decode_bitwise'_succ : forall us i acc, bounded limb_widths us -> + decode_bitwise' limb_widths us (S i) acc = + decode_bitwise' limb_widths us i (acc * (2 ^ w[i]) + nth_default 0 us i). + Proof. + intros. + simpl; f_equal. + match goal with H : bounded _ _ |- _ => + rewrite Z_lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end. + rewrite Z.shiftl_mul_pow2 by auto. + ring. + Qed. + + (* c is a counter, allows i to count up rather than down *) + Fixpoint partial_decode us i c := + match c with + | O => 0 + | S c' => (partial_decode us (S i) c' * 2 ^ w[i]) + nth_default 0 us i + end. + + Lemma partial_decode_counter_over : forall c us i, (c >= length us - i)%nat -> + partial_decode us i c = partial_decode us i (length us - i). + Proof. + induction c; intros. + + f_equal. omega. + + simpl. rewrite IHc by omega. + case_eq (length us - i)%nat; intros. + - rewrite nth_default_out_of_bounds with (us0 := us) by omega. + replace (length us - S i)%nat with 0%nat by omega. + reflexivity. + - simpl. repeat f_equal. omega. + Qed. + + Lemma partial_decode_counter_subst : forall c c' us i, + (c >= length us - i)%nat -> (c' >= length us - i)%nat -> + partial_decode us i c = partial_decode us i c'. + Proof. + intros. + rewrite partial_decode_counter_over by assumption. + symmetry. + auto using partial_decode_counter_over. + Qed. + + Lemma partial_decode_succ : forall c us i, (c >= length us - i)%nat -> + partial_decode us (S i) c * 2 ^ w[i] + nth_default 0 us i = + partial_decode us i c. + Proof. + intros. + rewrite partial_decode_counter_subst with (i := i) (c' := S c) by omega. + reflexivity. + Qed. + + Lemma partial_decode_intermediate : forall c us i, length us = length limb_widths -> + (c >= length us - i)%nat -> + partial_decode us i c = BaseSystem.decode' (base_from_limb_widths (skipn i limb_widths)) (skipn i us). + Proof. + induction c; intros. + + simpl. rewrite skipn_all by omega. + symmetry; apply decode_base_nil. + + simpl. + destruct (lt_dec i (length limb_widths)). + - rewrite IHc by omega. + do 2 (rewrite skipn_nth_default with (n := i) (d := 0) by (rewrite <-?base_length; omega)). + unfold base_from_limb_widths; fold base_from_limb_widths. + rewrite peel_decode. + fold (BaseSystem.mul_each (two_p w[i])). + rewrite <-mul_each_base, mul_each_rep, two_p_correct. + ring_simplify. + f_equal; ring. + - rewrite <- IHc by omega. + apply partial_decode_succ; omega. + Qed. + + + Lemma decode_bitwise'_succ_partial_decode : forall us i c, + bounded limb_widths us -> length us = length limb_widths -> + decode_bitwise' limb_widths us (S i) (partial_decode us (S i) c) = + decode_bitwise' limb_widths us i (partial_decode us i (S c)). + Proof. + intros. + rewrite decode_bitwise'_succ by auto. + f_equal. + Qed. + + Lemma decode_bitwise'_spec : forall us i, (i <= length limb_widths)%nat -> + bounded limb_widths us -> length us = length limb_widths -> + decode_bitwise' limb_widths us i (partial_decode us i (length us - i)) = + BaseSystem.decode {base} us. + Proof. + induction i; intros. + + rewrite partial_decode_intermediate by auto. + reflexivity. + + rewrite decode_bitwise'_succ_partial_decode by auto. + replace (S (length us - S i)) with (length us - i)%nat by omega. + apply IHi; auto; omega. + Qed. + + Lemma decode_bitwise_spec : forall us, bounded limb_widths us -> + length us = length limb_widths -> + decode_bitwise limb_widths us = BaseSystem.decode {base} us. + Proof. + unfold decode_bitwise; intros. + replace 0 with (partial_decode us (length us) (length us - length us)) by + (rewrite Nat.sub_diag; reflexivity). + apply decode_bitwise'_spec; auto; omega. + Qed. + +End BitwiseDecodeEncode. + +Section Conversion. + Context {limb_widthsA} (limb_widthsA_nonneg : forall w, In w limb_widthsA -> 0 <= w) + {limb_widthsB} (limb_widthsB_nonneg : forall w, In w limb_widthsB -> 0 <= w). + Local Notation "{baseA}" := (base_from_limb_widths limb_widthsA). + Local Notation "{baseB}" := (base_from_limb_widths limb_widthsB). + Context (bvB : BaseSystem.BaseVector {baseB}). + + Definition convert xs := @encodeZ limb_widthsB (@decode_bitwise limb_widthsA xs). + + Lemma convert_spec : forall xs, @bounded limb_widthsA xs -> length xs = length limb_widthsA -> + BaseSystem.decode {baseA} xs mod (@upper_bound limb_widthsB) = BaseSystem.decode {baseB} (convert xs). + Proof. + unfold convert; intros. + rewrite encodeZ_spec, decode_bitwise_spec by auto. + reflexivity. + Qed. + +End Conversion. \ No newline at end of file diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 49b1875ce..50c1f3ea6 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -4,151 +4,30 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import VerdiTactics. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.Pow2Base Crypto.ModularArithmetic.Pow2BaseProofs. Require Crypto.BaseSystem. Local Open Scope Z_scope. Section PseudoMersenneBaseParamProofs. Context `{prm : PseudoMersenneBaseParams}. - Fixpoint base_from_limb_widths limb_widths := - match limb_widths with - | nil => nil - | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw) - end. - - Definition base := base_from_limb_widths limb_widths. - - Lemma base_length : length base = length limb_widths. - Proof. - unfold base. - induction limb_widths; try reflexivity. - simpl; rewrite map_length; auto. - Qed. - - Lemma nth_error_first : forall {T} (a b : T) l, nth_error (a :: l) 0 = Some b -> - a = b. - Proof. - intros; simpl in *. - unfold value in *. - congruence. - Qed. - - Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat -> - nth_error base i = Some b -> - nth_error limb_widths i = Some w -> - nth_error base (S i) = Some (two_p w * b). - Proof. - unfold base; induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; - unfold base_from_limb_widths in *; fold base_from_limb_widths in *; - [rewrite (@nil_length0 Z) in *; omega | ]. - simpl in *; rewrite map_length in *. - case_eq i; intros; subst. - + subst; apply nth_error_first in nth_err_w. - apply nth_error_first in nth_err_b; subst. - apply map_nth_error. - case_eq l; intros; subst; [simpl in *; omega | ]. - unfold base_from_limb_widths; fold base_from_limb_widths. - reflexivity. - + simpl in nth_err_w. - apply nth_error_map in nth_err_w. - destruct nth_err_w as [x [A B]]. - subst. - replace (two_p w * (two_p a * x)) with (two_p a * (two_p w * x)) by ring. - apply map_nth_error. - apply IHl; auto; omega. - Qed. - - Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x), - exists l', l = x :: l'. - Proof. - induction l; try discriminate; eexists. - apply nth_error_first in H. - subst; eauto. - Qed. - - Lemma sum_firstn_succ : forall l i x, - nth_error l i = Some x -> - sum_firstn l (S i) = x + sum_firstn l i. - Proof. - unfold sum_firstn; induction l; - [intros; rewrite (@nth_error_nil_error Z) in *; congruence | ]. - intros ? x nth_err_x; destruct (NPeano.Nat.eq_dec i 0). - + subst; simpl in *; unfold value in *. - congruence. - + rewrite <- (NPeano.Nat.succ_pred i) at 2 by auto. - rewrite <- (NPeano.Nat.succ_pred i) in nth_err_x by auto. - simpl. simpl in nth_err_x. - specialize (IHl (pred i) x). - rewrite NPeano.Nat.succ_pred in IHl by auto. - destruct (NPeano.Nat.eq_dec (pred i) 0). - - replace i with 1%nat in * by omega. - simpl. replace (pred 1) with 0%nat in * by auto. - apply nth_error_exists_first in nth_err_x. - destruct nth_err_x as [l' ?]. - subst; simpl; ring. - - rewrite IHl by auto; ring. - Qed. - Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof. intros. apply Z.lt_le_incl. auto using limb_widths_pos. - Qed. - - Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. - Proof. - unfold sum_firstn; intros. - apply fold_right_invariant; try omega. - intros y In_y_lw ? ?. - apply Z.add_nonneg_nonneg; try assumption. - apply limb_widths_nonneg. - eapply In_firstn; eauto. - Qed. + Qed. Hint Resolve limb_widths_nonneg. Lemma k_nonneg : 0 <= k. Proof. - apply sum_firstn_limb_widths_nonneg. - Qed. + apply sum_firstn_limb_widths_nonneg; auto. + Qed. Hint Resolve k_nonneg. - Lemma nth_error_base : forall i, (i < length base)%nat -> - nth_error base i = Some (two_p (sum_firstn limb_widths i)). - Proof. - induction i; intros. - + unfold base, sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. - intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. - + - assert (i < length base)%nat as lt_i_length by omega. - specialize (IHi lt_i_length). - rewrite base_length in lt_i_length. - destruct (nth_error_length_exists_value _ _ lt_i_length) as [w nth_err_w]. - erewrite base_from_limb_widths_step; eauto. - f_equal. - simpl. - destruct (NPeano.Nat.eq_dec i 0). - - subst; unfold sum_firstn; simpl. - apply nth_error_exists_first in nth_err_w. - destruct nth_err_w as [l' lw_destruct]; subst. - rewrite lw_destruct. - ring_simplify. - f_equal; simpl; ring. - - erewrite sum_firstn_succ; eauto. - symmetry. - apply two_p_is_exp; auto using sum_firstn_limb_widths_nonneg. - apply limb_widths_nonneg. - eapply nth_error_value_In; eauto. - Qed. + Definition base := base_from_limb_widths limb_widths. - Lemma nth_default_base : forall d i, (i < length base)%nat -> - nth_default d base i = 2 ^ (sum_firstn limb_widths i). + Lemma base_length : length base = length limb_widths. Proof. - intros ? ? i_lt_length. - destruct (nth_error_length_exists_value _ _ i_lt_length) as [x nth_err_x]. - unfold nth_default. - rewrite nth_err_x. - rewrite nth_error_base in nth_err_x by assumption. - rewrite two_p_correct in nth_err_x. - congruence. + unfold base; auto using base_from_limb_widths_length. Qed. Lemma base_matches_modulus: forall i j, @@ -164,62 +43,30 @@ Section PseudoMersenneBaseParamProofs. subst r. assert (i + j - length base < length base)%nat by omega. rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.mul_pos_pos; - [ | subst b; rewrite nth_default_base; try assumption ]; - apply Z.pow_pos_nonneg; omega || apply k_nonneg || apply sum_firstn_limb_widths_nonneg). + [ | subst b; unfold base; rewrite nth_default_base; try assumption ]; + zero_bounds; auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg). rewrite (Zminus_0_l_reverse (b i * b j)) at 1. f_equal. subst b. - repeat rewrite nth_default_base by assumption. - do 2 rewrite <- Z.pow_add_r by (apply sum_firstn_limb_widths_nonneg || apply k_nonneg). + unfold base; repeat rewrite nth_default_base by auto. + do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. symmetry. apply mod_same_pow. split. - + apply Z.add_nonneg_nonneg; apply sum_firstn_limb_widths_nonneg || apply k_nonneg. - + rewrite base_length in *; apply limb_widths_match_modulus; assumption. + + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. + + rewrite base_length, base_from_limb_widths_length in * by auto. + apply limb_widths_match_modulus; auto. Qed. - Lemma base_succ : forall i, ((S i) < length base)%nat -> - nth_default 0 base (S i) mod nth_default 0 base i = 0. - Proof. - intros. - repeat rewrite nth_default_base by omega. - apply mod_same_pow. - split; [apply sum_firstn_limb_widths_nonneg | ]. - destruct (NPeano.Nat.eq_dec i 0); subst. - + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. - apply Z.add_nonneg_nonneg; try omega. - apply limb_widths_nonneg. - rewrite lw_eq. - apply in_eq. - + assert (i < length base)%nat as i_lt_length by omega. - rewrite base_length in *. - apply nth_error_length_exists_value in i_lt_length. - destruct i_lt_length as [x nth_err_x]. - erewrite sum_firstn_succ; eauto. - apply nth_error_value_In in nth_err_x. - apply limb_widths_nonneg in nth_err_x. - omega. - Qed. - - Lemma nth_error_subst : forall i b, nth_error base i = Some b -> - b = 2 ^ (sum_firstn limb_widths i). - Proof. - intros i b nth_err_b. - pose proof (nth_error_value_length _ _ _ _ nth_err_b). - rewrite nth_error_base in nth_err_b by assumption. - rewrite two_p_correct in nth_err_b. - congruence. - Qed. - Lemma base_positive : forall b : Z, In b base -> b > 0. Proof. intros b In_b_base. apply In_nth_error_value in In_b_base. destruct In_b_base as [i nth_err_b]. - apply nth_error_subst in nth_err_b. + apply nth_error_subst in nth_err_b; [ | auto ]. rewrite nth_err_b. apply gt_lt_symmetry. - apply Z.pow_pos_nonneg; omega || apply sum_firstn_limb_widths_nonneg. + apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg. Qed. Lemma b0_1 : forall x : Z, nth_default x base 0 = 1. @@ -234,12 +81,14 @@ Section PseudoMersenneBaseParamProofs. b i * b j = r * b (i + j)%nat. Proof. intros; subst b r. - repeat rewrite nth_default_base by omega. + unfold base in *. + repeat rewrite nth_default_base by (omega || auto). rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.pow_pos_nonneg; omega || apply sum_firstn_limb_widths_nonneg). - rewrite <- Z.pow_add_r by apply sum_firstn_limb_widths_nonneg. + rewrite mul_div_eq by (apply gt_lt_symmetry; zero_bounds; + auto using sum_firstn_limb_widths_nonneg). + rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. rewrite mod_same_pow; try ring. - split; [ apply sum_firstn_limb_widths_nonneg | ]. + split; [ auto using sum_firstn_limb_widths_nonneg | ]. apply limb_widths_good. rewrite <- base_length; assumption. Qed. @@ -250,4 +99,4 @@ Section PseudoMersenneBaseParamProofs. base_good := base_good }. -End PseudoMersenneBaseParamProofs. +End PseudoMersenneBaseParamProofs. \ No newline at end of file diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index 02d409b68..1f9a0f2f6 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -1,10 +1,9 @@ Require Import ZArith. Require Import List. +Require Import Crypto.Util.ListUtil. Require Crypto.BaseSystem. Local Open Scope Z_scope. -Definition sum_firstn l n := fold_right Z.add 0 (firstn n l). - Class PseudoMersenneBaseParams (modulus : Z) := { limb_widths : list Z; limb_widths_pos : forall w, In w limb_widths -> 0 < w; diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 0426c0834..ed20cd15c 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -3,6 +3,17 @@ Require Import Coq.omega.Omega. Require Import Coq.Arith.Peano_dec. Require Import Crypto.Tactics.VerdiTactics. +Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l). + +Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := + match la with + | nil => nil + | a :: la' => match lb with + | nil => nil + | b :: lb' => f a b :: map2 f la' lb' + end + end. + Ltac boring := simpl; intuition; repeat match goal with @@ -624,4 +635,144 @@ Proof. induction n; (destruct l; [intros; simpl in *; omega | ]); simpl; destruct i; break_if; try omega; intros; try apply nth_default_cons; rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity. -Qed. \ No newline at end of file +Qed. + +Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d, + (forall x, In x l -> P x) -> P d -> P (nth_default d l n). +Proof. + intros; rewrite nth_default_eq. + destruct (nth_in_or_default n l d); auto. + congruence. +Qed. + +Lemma nth_error_first : forall {T} (a b : T) l, + nth_error (a :: l) 0 = Some b -> a = b. +Proof. + intros; simpl in *. + unfold value in *. + congruence. +Qed. + +Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x), + exists l', l = x :: l'. +Proof. + induction l; try discriminate; eexists. + apply nth_error_first in H. + subst; eauto. +Qed. + +Lemma list_elementwise_eq : forall {T} (l1 l2 : list T), + (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2. +Proof. + induction l1, l2; intros; try reflexivity; + pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst. + f_equal. + apply IHl1. + intros i; specialize (H (S i)). + boring. +Qed. + +Lemma sum_firstn_all_succ : forall n l, (length l <= n)%nat -> + sum_firstn l (S n) = sum_firstn l n. +Proof. + unfold sum_firstn; intros. + rewrite !firstn_all_strong by omega. + congruence. +Qed. + +Lemma sum_firstn_succ : forall l i x, + nth_error l i = Some x -> + sum_firstn l (S i) = (x + sum_firstn l i)%Z. +Proof. + unfold sum_firstn; induction l; + [intros; rewrite (@nth_error_nil_error Z) in *; congruence | ]. + intros ? x nth_err_x; destruct (NPeano.Nat.eq_dec i 0). + + subst; simpl in *; unfold value in *. + congruence. + + rewrite <- (NPeano.Nat.succ_pred i) at 2 by auto. + rewrite <- (NPeano.Nat.succ_pred i) in nth_err_x by auto. + simpl. simpl in nth_err_x. + specialize (IHl (pred i) x). + rewrite NPeano.Nat.succ_pred in IHl by auto. + destruct (NPeano.Nat.eq_dec (pred i) 0). + - replace i with 1%nat in * by omega. + simpl. replace (pred 1) with 0%nat in * by auto. + apply nth_error_exists_first in nth_err_x. + destruct nth_err_x as [l' ?]. + subst; simpl; omega. + - rewrite IHl by auto; omega. +Qed. + +Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, + nth_default d (map2 f ls1 ls2) i = + if lt_dec i (min (length ls1) (length ls2)) + then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) + else d. +Proof. + induction ls1, ls2. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + cbv [map2 length min]. + intros. + break_if; try omega. + apply nth_default_nil. + + simpl. + destruct i. + - intros. rewrite !nth_default_cons. + break_if; auto; omega. + - intros. rewrite !nth_default_cons_S. + rewrite IHls1 with (d1 := d1) (d2 := d2). + repeat break_if; auto; omega. +Qed. + +Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b, + map2 f (a :: ls1) (b :: ls2) = f a b :: map2 f ls1 ls2. +Proof. + reflexivity. +Qed. + +Lemma map2_nil_l : forall A B C (f : A -> B -> C) ls2, + map2 f nil ls2 = nil. +Proof. + reflexivity. +Qed. + +Lemma map2_nil_r : forall A B C (f : A -> B -> C) ls1, + map2 f ls1 nil = nil. +Proof. + destruct ls1; reflexivity. +Qed. +Local Hint Resolve map2_nil_r map2_nil_l. + +Opaque map2. + +Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, + length (map2 f ls1 ls2) = min (length ls1) (length ls2). +Proof. + induction ls1, ls2; intros; try solve [cbv; auto]. + rewrite map2_cons, !length_cons, IHls1. + auto. +Qed. + +Ltac simpl_list_lengths := repeat match goal with + | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H + | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H + | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) + | |- appcontext[length (_ :: _)] => rewrite length_cons + end. + +Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2', + (length ls1 = length ls2) -> + map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. +Proof. + induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; + simpl_list_lengths; try omega. + rewrite <-!app_comm_cons, !map2_cons. + rewrite IHls1; auto. +Qed. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1ebadeada..5ea174577 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -500,3 +500,23 @@ Proof. induction l; intros; try reflexivity. etransitivity; [ apply IHl | apply Z.le_max_r ]. Qed. + + (* TODO : move to ZUtil *) + Lemma Z_lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). + Proof. + intros. + apply Z.bits_inj'; intros t ?. + rewrite Z.lor_spec, Z.shiftl_spec by assumption. + destruct (Z_lt_dec t n). + + rewrite Z_testbit_add_shiftl_low by omega. + rewrite Z.testbit_neg_r with (n := t - n) by omega. + apply Bool.orb_false_r. + + rewrite Z_testbit_add_shiftl_high by omega. + replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. + symmetry. + apply Z.testbit_false; try omega. + rewrite Z.div_small; try reflexivity. + split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. + apply Z.pow_le_mono_r; omega. + Qed. -- cgit v1.2.3 From 71179e46a7c404e76bc58c2465d547ead6df3e26 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 7 Jul 2016 16:02:23 -0400 Subject: wrap nsatz in Algebra --- _CoqProject | 3 +- src/Algebra.v | 12 +- .../CompleteEdwardsCurveTheorems.v | 2 +- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 +- src/CompleteEdwardsCurve/Pre.v | 2 +- src/Tactics/Algebra_syntax/Nsatz.v | 159 +++++++++++++++++++++ src/Tactics/Nsatz.v | 156 -------------------- src/Util/Tactics.v | 3 + 8 files changed, 176 insertions(+), 163 deletions(-) create mode 100644 src/Tactics/Algebra_syntax/Nsatz.v delete mode 100644 src/Tactics/Nsatz.v (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index f3f07e840..f8aa1e966 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v +src/Encoding/PointEncodingPre.v src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v @@ -54,8 +55,8 @@ src/Spec/ModularWordEncoding.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v -src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v +src/Tactics/Algebra_syntax/Nsatz.v src/Util/CaseUtil.v src/Util/Decidable.v src/Util/IterAssocOp.v diff --git a/src/Algebra.v b/src/Algebra.v index f9dfbd519..9f53c0613 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1,9 +1,10 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Notations. Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. +Require Crypto.Tactics.Algebra_syntax.Nsatz. Module Import ModuloCoq8485. Import NPeano Nat. @@ -637,6 +638,11 @@ Module Field. End Homomorphism. End Field. +(** Tactics *) + +Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax. +Ltac nsatz_contradict := Algebra_syntax.Nsatz.nsatz_contradict; dropRingSyntax. + (*** Tactics for manipulating field equations *) Require Import Coq.setoid_ring.Field_tac. @@ -981,7 +987,7 @@ Ltac neq01 := Ltac conservative_field_algebra := intros; conservative_common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 @@ -991,7 +997,7 @@ Ltac conservative_field_algebra := Ltac field_algebra := intros; common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 65d899463..44bb80157 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 364d7f9ec..263582508 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index ed4511fc9..432e834aa 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.Util.Notations. Generalizable All Variables. diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v new file mode 100644 index 000000000..a5b04cfa2 --- /dev/null +++ b/src/Tactics/Algebra_syntax/Nsatz.v @@ -0,0 +1,159 @@ +(*** 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. +(* Kludge for 8.4/8.5 compatibility *) +Module Import mynsatz_compute. + Import Nsatz. + Global Ltac mynsatz_compute x := nsatz_compute x. +End mynsatz_compute. +Ltac nsatz_compute x := mynsatz_compute x. + +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. + +(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz] + cannot handle duplicate hypotheses. So we clear them. *) +Ltac nsatz_clear_duplicates_for_bug_4851 domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ => + repeat match goal with + | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H' + end + end. + +Ltac nsatz_nonzero := + try solve [apply Integral_domain.integral_domain_one_zero + |apply Integral_domain.integral_domain_minus_one_zero + |trivial + |assumption]. + +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_clear_duplicates_for_bug_4851 domain; + 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. + +Ltac nsatz_power power := + let power_N := (eval compute in (BinNat.N.of_nat power)) in + nsatz_sugar_power BinInt.Z0 power_N. + +Ltac nsatz := nsatz_power 1%nat || nsatz_power 2%nat || nsatz_power 3%nat || nsatz_power 4%nat || nsatz_power 5%nat. + +Tactic Notation "nsatz" := nsatz. +Tactic Notation "nsatz" constr(n) := nsatz_power n. + +(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] + contradicts any hypothesis of the form [?x' <> ?y'], we turn this + problem about inequalities into one about equalities and give it + to [nsatz]. *) +Ltac nsatz_contradict_single_hypothesis domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => + unfold not in *; + match goal with + | [ H : eq _ _ -> False |- eq _ _ -> False ] + => intro; apply H; nsatz + | [ H : eq _ _ -> False |- False ] + => apply H; nsatz + end + end. + +Ltac nsatz_contradict := + let domain := nsatz_guess_domain in + nsatz_contradict_single_hypothesis domain + || (unfold not; + intros; + 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). diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v deleted file mode 100644 index 04f35c200..000000000 --- a/src/Tactics/Nsatz.v +++ /dev/null @@ -1,156 +0,0 @@ -(*** 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. -(* Kludge for 8.4/8.5 compatibility *) -Module Import mynsatz_compute. - Import Nsatz. - Global Ltac mynsatz_compute x := nsatz_compute x. -End mynsatz_compute. -Ltac nsatz_compute x := mynsatz_compute x. - -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. - -(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz] - cannot handle duplicate hypotheses. So we clear them. *) -Ltac nsatz_clear_duplicates_for_bug_4851 domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ => - repeat match goal with - | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H' - end - end. - -Ltac nsatz_nonzero := - try solve [apply Integral_domain.integral_domain_one_zero - |apply Integral_domain.integral_domain_minus_one_zero - |trivial - |assumption]. - -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_clear_duplicates_for_bug_4851 domain; - 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. - -(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] - contradicts any hypothesis of the form [?x' <> ?y'], we turn this - problem about inequalities into one about equalities and give it - to [nsatz]. *) -Ltac nsatz_contradict_single_hypothesis domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => - unfold not in *; - match goal with - | [ H : eq _ _ -> False |- eq _ _ -> False ] - => intro; apply H; nsatz - | [ H : eq _ _ -> False |- False ] - => apply H; nsatz - end - end. - -Ltac nsatz_contradict := - let domain := nsatz_guess_domain in - nsatz_contradict_single_hypothesis domain - || (unfold not; - intros; - 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). diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 4630e4ab7..01d72def9 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -7,6 +7,9 @@ Tactic Notation "test" tactic3(tac) := (** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *) Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds"). +Ltac get_goal := + match goal with |- ?G => G end. + (** find the head of the given expression *) Ltac head expr := match expr with -- cgit v1.2.3