diff options
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 11 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 9 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 69 | ||||
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 86 |
4 files changed, 51 insertions, 124 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 410cb8dfe..56a7051af 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -21,8 +21,15 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sum. Require Import Crypto.Util.Bool. Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Opp. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Le. Require Import Crypto.Util.ZUtil.Hints.PullPush. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -37,7 +44,7 @@ Require Import Crypto.Util.ZUtil.Sorting. Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. Require Import Crypto.Util.ZUtil.Hints.PullPush. Require Import Crypto.Util.ZUtil.EquivModulo. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 869abea8e..01018c3e2 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -30,10 +30,17 @@ Require Import Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Log2. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.CC. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ZUtil.ModInv. diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index e35e14616..ffb6b0215 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Util.Tactics.DestructHead. @@ -29,10 +30,14 @@ Require Import Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.CC. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ErrorT. @@ -2087,24 +2092,13 @@ Module ProdEquiv. let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx. Proof. reflexivity. Qed. - (* TODO : move *) - Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) : - (forall x : A, f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - rewrite IHn by assumption. - rewrite H; reflexivity. - Qed. - Lemma interp_state_equiv e : forall cc ctx cc' ctx', cc = cc' -> (forall r, ctx r = ctx' r) -> interp256 e cc ctx = interp256 e cc' ctx'. Proof. induction e; intros; subst; cbn; [solve[auto]|]. - apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto; + apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto; [reflexivity|]. intros; break_match; auto. Qed. @@ -2116,17 +2110,6 @@ Module ProdEquiv. reflexivity. Qed. - Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) : - (forall x, In x (to_list n t) -> f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - destruct t. - rewrite IHn by auto using in_cons. - rewrite H; auto using in_eq. - Qed. - Definition value_unused r e : Prop := forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r'). @@ -2141,7 +2124,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -2155,7 +2138,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -2649,19 +2632,6 @@ Module Barrett256. => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x n : - 0 <= n -> - - (2 ^ n) <= x < 2 ^ n -> - Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. - Proof. - intros. break_match; Z.ltb_to_lt. - { autorewrite with zsimplify. reflexivity. } - { autorewrite with zsimplify. - rewrite Z.bits_above_pow2 by omega. - reflexivity. } - Qed. - Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -2755,7 +2725,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context. { reflexivity. } @@ -2763,7 +2733,7 @@ Module Barrett256. rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega). match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). reflexivity. } step start_context. { rewrite Z.bit0_eqb. @@ -2782,7 +2752,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. @@ -3169,19 +3139,6 @@ Module Montgomery256. => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x y n : - 0 <= n -> - 0 <= x < 2 ^ n -> - 0 <= y < 2 ^ n -> - Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2. - Proof. - intros. rewrite Z.sub_pos_bound_div_eq by omega. - break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ]. - rewrite Z.testbit_eqb, Z.div_between_0_if by omega. - break_innermost_match; Z.ltb_to_lt; try lia; reflexivity. - Qed. - Local Ltac break_ifs := repeat (break_innermost_match_step; Z.ltb_to_lt; try (exfalso; omega); []). @@ -3228,7 +3185,7 @@ Module Montgomery256. { let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity. rewrite !Z.shiftl_0_r, !Z.mod_mod by omega. - apply testbit_neg_eq_if; + apply Z.testbit_neg_eq_if; let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity; auto using Z.mod_pos_bound with omega. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 3745e59ff..c0c8dbdeb 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -23,13 +23,21 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.Sum. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.PullPush. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Shift. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SubstEvars. @@ -41,7 +49,7 @@ Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. Require Import Crypto.Util.ZUtil.Hints.PullPush. Require Import Crypto.Util.ZUtil.EquivModulo. @@ -1245,13 +1253,6 @@ Module Rows. rewrite Columns.length_from_associational in *; auto. Qed. - (* TODO : move *) - Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat). - Proof. - destruct a, b; try tauto. - rewrite <-Nat.succ_max_distr. - split; [ | destruct 1]; congruence. - Qed. Lemma max_column_size_zero_iff x : max_column_size x = 0%nat <-> (forall c, In c x -> c = nil). Proof. @@ -10402,24 +10403,13 @@ Module ProdEquiv. let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx. Proof. reflexivity. Qed. - (* TODO : move *) - Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) : - (forall x : A, f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - rewrite IHn by assumption. - rewrite H; reflexivity. - Qed. - Lemma interp_state_equiv e : forall cc ctx cc' ctx', cc = cc' -> (forall r, ctx r = ctx' r) -> interp256 e cc ctx = interp256 e cc' ctx'. Proof. induction e; intros; subst; cbn; [solve[auto]|]. - apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto; + apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto; [reflexivity|]. intros; break_match; auto. Qed. @@ -10431,17 +10421,6 @@ Module ProdEquiv. reflexivity. Qed. - Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) : - (forall x, In x (to_list n t) -> f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - destruct t. - rewrite IHn by auto using in_cons. - rewrite H; auto using in_eq. - Qed. - Definition value_unused r e : Prop := forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r'). @@ -10456,7 +10435,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -10470,7 +10449,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -11525,19 +11504,6 @@ Module Barrett256. | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x n : - 0 <= n -> - - (2 ^ n) <= x < 2 ^ n -> - Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. - Proof. - intros. break_match; Z.ltb_to_lt. - { autorewrite with zsimplify. reflexivity. } - { autorewrite with zsimplify. - rewrite Z.bits_above_pow2 by omega. - reflexivity. } - Qed. - Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -11631,7 +11597,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context. { reflexivity. } @@ -11639,7 +11605,7 @@ Module Barrett256. rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega). match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). reflexivity. } step start_context. { rewrite Z.bit0_eqb. @@ -11658,7 +11624,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. @@ -12567,19 +12533,6 @@ Module Montgomery256. | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x y n : - 0 <= n -> - 0 <= x < 2 ^ n -> - 0 <= y < 2 ^ n -> - Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2. - Proof. - intros. rewrite Z.sub_pos_bound_div_eq by omega. - break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ]. - rewrite Z.testbit_eqb, Z.div_between_0_if by omega. - break_innermost_match; Z.ltb_to_lt; try lia; reflexivity. - Qed. - Lemma prod_montred256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags can be anything *) (start_context : register -> Z) (* starting register values *) @@ -12622,9 +12575,12 @@ Module Montgomery256. { let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity. rewrite !Z.shiftl_0_r, !Z.mod_mod by omega. - apply testbit_neg_eq_if; + repeat match goal with + | |- context [?a mod ?b] => unique pose proof (Z.mod_pos_bound a b ltac:(omega)) + end. + apply Z.testbit_neg_eq_if; let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity; - auto using Z.mod_pos_bound with omega. } + omega. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. Qed. |