diff options
Diffstat (limited to 'src/Compilers/Z/Bounds')
| -rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 289 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 214 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v | 192 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v | 197 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijn.v | 24 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | 48 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v | 42 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 56 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 285 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Glue.v | 550 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/OutputType.v | 52 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 362 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Relax.v | 135 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/RoundUpLemmas.v | 34 |
14 files changed, 0 insertions, 2480 deletions
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v deleted file mode 100644 index e37b64a09..000000000 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ /dev/null @@ -1,289 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.Tactics.DestructHead. -Export Compilers.Syntax.Notations. - -Local Notation eta x := (fst x, snd x). -Local Notation eta3 x := (eta (fst x), snd x). -Local Notation eta4 x := (eta3 (fst x), snd x). - -Notation bounds := zrange. -Delimit Scope bounds_scope with bounds. -Local Open Scope Z_scope. - -Module Import Bounds. - Definition t := bounds. - Bind Scope bounds_scope with t. - Local Coercion Z.of_nat : nat >-> Z. - Definition interp_base_type (ty : base_type) : Set := t. - - Section ops. - (** Generic helper definitions *) - Definition t_map1 (f : Z -> Z) : t -> t - := fun x => ZRange.two_corners f x. - Definition t_map2 (f : Z -> Z -> Z) : t -> t -> t - := fun x y => ZRange.four_corners f x y. - Definition t_map3 (f : Z -> Z -> Z -> Z) : t -> t -> t -> t - := fun x y z => ZRange.eight_corners f x y z. - (** Definitions of the actual bounds propogation *) - (** Rules for adding new operations: - - - Use [t_mapn] to if the underlying operation on [Z] is - monotonic in all [n] of its arguments ([t_mapn] handles both - monotonic non-increasing and monotonic non-decreasing) *) - - Definition add : t -> t -> t := t_map2 Z.add. - Definition sub : t -> t -> t := t_map2 Z.sub. - Definition mul : t -> t -> t := t_map2 Z.mul. - Definition shl : t -> t -> t := t_map2 Z.shiftl. - Definition shr : t -> t -> t := t_map2 Z.shiftr. - Definition max_abs_bound (x : t) : Z - := upper (ZRange.abs x). - Definition upper_lor_and_bounds (x y : Z) : Z - := 2^(1 + Z.log2_up (Z.max x y)). - Definition extreme_lor_land_bounds (x y : t) : t - := let mx := max_abs_bound x in - let my := max_abs_bound y in - {| lower := -upper_lor_and_bounds mx my ; upper := upper_lor_and_bounds mx my |}. - Definition extremization_bounds (f : t -> t -> t) (x y : t) : t - := let (lx, ux) := x in - let (ly, uy) := y in - if ((lx <? 0) || (ly <? 0))%Z%bool - then extreme_lor_land_bounds x y - else f x y. - Definition land : t -> t -> t - := extremization_bounds - (fun x y - => let (lx, ux) := x in - let (ly, uy) := y in - {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}). - Definition lor : t -> t -> t - := extremization_bounds - (fun x y - => let (lx, ux) := x in - let (ly, uy) := y in - {| lower := Z.max lx ly; - upper := 2^(Z.max (Z.log2_up (ux+1)) (Z.log2_up (uy+1))) - 1 |}). - Definition opp : t -> t := t_map1 Z.opp. - Definition zselect' (r1 r2 : t) : t - := let (lr1, ur1) := r1 in - let (lr2, ur2) := r2 in - {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}. - Definition zselect (c r1 r2 : t) : t - := zselect' r1 r2. - Definition add_with_carry : t -> t -> t -> t - := t_map3 Z.add_with_carry. - Definition sub_with_borrow : t -> t -> t -> t - := t_map3 Z.sub_with_borrow. - Definition modulo_pow2_constant : Z -> t -> t - := fun e x - => let d := 2^e in - let (l, u) := (lower x, upper x) in - {| lower := if l / d =? u / d then Z.min (l mod d) (u mod d) else Z.min 0 (d + 1); - upper := if l / d =? u / d then Z.max (l mod d) (u mod d) else Z.max 0 (d - 1) |}. - Definition div_pow2_constant : Z -> t -> t - := fun e x - => let d := 2^e in - let (l, u) := (lower x, upper x) in - {| lower := l / d ; upper := u / d |}. - Definition opp_div_pow2_constant : Z -> t -> t - := fun e x - => let d := 2^e in - let (l, u) := (lower x, upper x) in - {| lower := -(u / d) ; upper := -(l / d) |}. - Definition neg (int_width : Z) : t -> t - := fun v - => let (lb, ub) := v in - let might_be_one := ((lb <=? 1) && (1 <=? ub))%Z%bool in - let must_be_one := ((lb =? 1) && (ub =? 1))%Z%bool in - if must_be_one - then {| lower := Z.ones int_width ; upper := Z.ones int_width |} - else if might_be_one - then {| lower := Z.min 0 (Z.ones int_width) ; upper := Z.max 0 (Z.ones int_width) |} - else {| lower := 0 ; upper := 0 |}. - Definition cmovne' (r1 r2 : t) : t - := let (lr1, ur1) := r1 in - let (lr2, ur2) := r2 in - {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}. - Definition cmovne (x y r1 r2 : t) : t - := cmovne' r1 r2. - Definition cmovle' (r1 r2 : t) : t - := let (lr1, ur1) := r1 in - let (lr2, ur2) := r2 in - {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}. - Definition cmovle (x y r1 r2 : t) : t - := cmovle' r1 r2. - - Definition id_with_alt {T1 T2 Tout} (x : interp_base_type T1) (y : interp_base_type T2) - : interp_base_type Tout - := match T1, T2, Tout with - | TZ, TZ, TZ => y - | _, _, _ => x - end. - End ops. - Section ops_with_carry. - Context (carry_boundary_bit_width : Z). - Definition get_carry : t -> t * t - := fun v => - (modulo_pow2_constant carry_boundary_bit_width v, - div_pow2_constant carry_boundary_bit_width v). - Definition get_borrow : t -> t * t - := fun v => - (modulo_pow2_constant carry_boundary_bit_width v, - opp_div_pow2_constant carry_boundary_bit_width v). - Definition add_with_get_carry : t -> t -> t -> t * t - := fun c x y - => get_carry (add_with_carry c x y). - Definition sub_with_get_borrow : t -> t -> t -> t * t - := fun c x y - => get_borrow (sub_with_borrow c x y). - Definition mul_split : t -> t -> t * t - := fun x y => get_carry (mul x y). - End ops_with_carry. - - Module Export Notations. - Export Util.ZRange.Notations. - Infix "+" := add : bounds_scope. - Infix "-" := sub : bounds_scope. - Infix "*" := mul : bounds_scope. - Infix "<<" := shl : bounds_scope. - Infix ">>" := shr : bounds_scope. - Infix "&'" := land : bounds_scope. - Notation "- x" := (opp x) : bounds_scope. - End Notations. - - Definition log_bit_width_of_base_type ty : option nat - := match ty with - | TZ => None - | TWord logsz => Some logsz - end. - - Definition bit_width_of_base_type ty : option Z - := option_map (fun logsz => 2^Z.of_nat logsz)%Z (log_bit_width_of_base_type ty). - - Definition truncation_bounds' bit_width (b : t) - := match bit_width with - | Some bit_width => if ((0 <=? lower b) && (upper b <? 2^bit_width))%bool - then b - else {| lower := 0 ; upper := 2^bit_width - 1 |} - | None => b - end. - Definition truncation_bounds ty : interp_base_type ty -> interp_base_type ty - := truncation_bounds' (bit_width_of_base_type ty). - - Definition interp_op {src dst} (f : op src dst) - (x : interp_flat_type interp_base_type src) - : interp_flat_type interp_base_type dst - := SmartVarfMap - truncation_bounds - (match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst T v => fun _ => {| lower := v ; upper := v |} - | Add _ _ T => fun xy => add (fst xy) (snd xy) - | Sub _ _ T => fun xy => sub (fst xy) (snd xy) - | Mul _ _ T => fun xy => mul (fst xy) (snd xy) - | Shl _ _ T => fun xy => shl (fst xy) (snd xy) - | Shr _ _ T => fun xy => shr (fst xy) (snd xy) - | Land _ _ T => fun xy => land (fst xy) (snd xy) - | Lor _ _ T => fun xy => lor (fst xy) (snd xy) - | Opp _ T => fun x => opp x - | IdWithAlt _ _ T => fun xy => id_with_alt (fst xy) (snd xy) - | Zselect _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in zselect c x y - | MulSplit carry_boundary_bit_width _ _ T1 T2 - => fun xy => mul_split carry_boundary_bit_width (fst xy) (snd xy) - | AddWithCarry _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in add_with_carry c x y - | AddWithGetCarry carry_boundary_bit_width _ _ _ T1 T2 - => fun cxy => let '(c, x, y) := eta3 cxy in - add_with_get_carry carry_boundary_bit_width c x y - | SubWithBorrow _ _ _ T => fun cxy => let '(c, x, y) := eta3 cxy in sub_with_borrow c x y - | SubWithGetBorrow carry_boundary_bit_width _ _ _ T1 T2 - => fun cxy => let '(c, x, y) := eta3 cxy in - sub_with_get_borrow carry_boundary_bit_width c x y - end%bounds x). - - Definition of_Z (z : Z) : t := ZToZRange z. - - Definition of_interp t (z : Syntax.interp_base_type t) : interp_base_type t - := ZToZRange (interpToZ z). - - Definition smallest_logsz - (round_up : nat -> option nat) - (b : t) - : option nat - := if (0 <=? lower b)%Z - then Some (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) - else None. - Definition actual_logsz - (round_up : nat -> option nat) - (b : t) - : option nat - := if (0 <=? lower b)%Z - then let smallest_lgsz := (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) in - let lgsz := round_up smallest_lgsz in - match lgsz with - | Some lgsz - => if Nat.leb smallest_lgsz lgsz - then Some lgsz - else None - | None => None - end - else None. - Definition bounds_to_base_type - {round_up : nat -> option nat} - (T : base_type) - (b : interp_base_type T) - : base_type - := match T with - | TZ => match actual_logsz round_up b with - | Some lgsz => TWord lgsz - | None => TZ - end - | TWord _ - => match smallest_logsz round_up b with - | Some lgsz => TWord lgsz - | None => TZ - end - end. - - Definition option_min (a : nat) (b : option nat) - := match b with - | Some b => Nat.min a b - | None => a - end. - - Definition round_up_to_in_list (allowable_lgsz : list nat) - (lgsz : nat) - : option nat - := let good_lgsz := List.filter (Nat.leb lgsz) allowable_lgsz in - List.fold_right (fun a b => Some (option_min a b)) None good_lgsz. - - Definition ComputeBounds {t} (e : Expr t) - (input_bounds : interp_flat_type interp_base_type (domain t)) - : interp_flat_type interp_base_type (codomain t) - := Compilers.Syntax.Interp (@interp_op) e input_bounds. - - Definition is_tighter_thanb' {T} : interp_base_type T -> interp_base_type T -> bool - := is_tighter_than_bool. - - Definition is_bounded_by' {T} : interp_base_type T -> Syntax.interp_base_type T -> Prop - := fun bounds val => is_bounded_by' (bit_width_of_base_type T) bounds (interpToZ val). - - Definition is_tighter_thanb {T} : interp_flat_type interp_base_type T -> interp_flat_type interp_base_type T -> bool - := interp_flat_type_relb_pointwise (@is_tighter_thanb'). - - Definition is_bounded_by {T} : interp_flat_type interp_base_type T -> interp_flat_type Syntax.interp_base_type T -> Prop - := interp_flat_type_rel_pointwise (@is_bounded_by'). - - Local Arguments interp_base_type !_ / . - Global Instance dec_eq_interp_flat_type : forall {T}, DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. - Proof. - induction T; destruct_head base_type; simpl; exact _. - Defined. -End Bounds. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v deleted file mode 100644 index b23e0ff1b..000000000 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ /dev/null @@ -1,214 +0,0 @@ -Require Import Coq.Classes.Morphisms. -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Psatz. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.ZRange.CornersMonotoneBounds. -Require Import Crypto.Util.ZUtil.Stabilization. -Require Import Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Modulo. -Require Import Crypto.Util.ZUtil.LandLorShiftBounds. -Require Import Crypto.Util.ZUtil.Morphisms. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.FixedWordSizesEquality. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. - -Local Open Scope Z_scope. - -Local Arguments Bounds.is_bounded_by' !_ _ _ / . - -Lemma is_bounded_by_truncation_bounds' Tout bs v - (H : Bounds.is_bounded_by (T:=Tbase TZ) bs v) - : Bounds.is_bounded_by (T:=Tbase Tout) - (Bounds.truncation_bounds' (Bounds.bit_width_of_base_type Tout) bs) - (ZToInterp v). -Proof. - destruct bs as [l u]; cbv [Bounds.truncation_bounds' Bounds.is_bounded_by Bounds.is_bounded_by' Bounds.bit_width_of_base_type Bounds.log_bit_width_of_base_type option_map ZRange.is_bounded_by'] in *; simpl in *. - repeat first [ break_t_step - | fin_t - | progress simpl in * - | Zarith_t_step - | rewriter_t - | word_arith_t ]. -Qed. - -Lemma is_bounded_by_compose T1 T2 f_v bs v f_bs fv - (H : Bounds.is_bounded_by (T:=Tbase T1) bs v) - (Hf : forall bs v, Bounds.is_bounded_by (T:=Tbase T1) bs v -> Bounds.is_bounded_by (T:=Tbase T2) (f_bs bs) (f_v v)) - (Hfv : f_v v = fv) - : Bounds.is_bounded_by (T:=Tbase T2) (f_bs bs) fv. -Proof. - subst; eauto. -Qed. - -Local Existing Instances Z.log2_up_le_Proper Z.add_le_Proper Z.sub_with_borrow_le_Proper. -Lemma land_upper_lor_land_bounds a b - : Z.abs (Z.land a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b). -Proof. - unfold Bounds.upper_lor_and_bounds. - apply stabilizes_bounded; auto with zarith. - rewrite <- !Z.max_mono by exact _. - apply land_stabilizes; apply stabilization_time_weaker. -Qed. - -Lemma lor_upper_lor_land_bounds a b - : Z.abs (Z.lor a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b). -Proof. - unfold Bounds.upper_lor_and_bounds. - apply stabilizes_bounded; auto with zarith. - rewrite <- !Z.max_mono by exact _. - apply lor_stabilizes; apply stabilization_time_weaker. -Qed. - -Lemma upper_lor_and_bounds_Proper - : Proper (Z.le ==> Z.le ==> Z.le) Bounds.upper_lor_and_bounds. -Proof. - intros ??? ???. - unfold Bounds.upper_lor_and_bounds. - auto with zarith. -Qed. - -Local Arguments Z.pow !_ !_. -Local Arguments Z.log2_up !_. -Local Arguments Z.add !_ !_. -Lemma land_bounds_extreme xb yb x y - (Hx : ZRange.is_bounded_by' None xb x) - (Hy : ZRange.is_bounded_by' None yb y) - : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.land x y). -Proof. - apply ZRange.monotonify2; auto; - unfold Bounds.extreme_lor_land_bounds; - [ apply land_upper_lor_land_bounds - | apply upper_lor_and_bounds_Proper ]. -Qed. -Lemma lor_bounds_extreme xb yb x y - (Hx : ZRange.is_bounded_by' None xb x) - (Hy : ZRange.is_bounded_by' None yb y) - : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.lor x y). -Proof. - apply ZRange.monotonify2; auto; - unfold Bounds.extreme_lor_land_bounds; - [ apply lor_upper_lor_land_bounds - | apply upper_lor_and_bounds_Proper ]. -Qed. - -Local Arguments N.ldiff : simpl never. -Local Arguments Z.pow : simpl never. -Local Arguments Z.add !_ !_. -Local Existing Instances Z.add_le_Proper Z.sub_le_flip_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper Z.add_with_carry_le_Proper. -Local Hint Extern 1 => progress cbv beta iota : typeclass_instances. -Local Ltac ibbio_prefin := - [ > | intros | simpl; reflexivity ]. -Local Ltac apply_is_bounded_by_truncation_bounds := - cbv [id - Bounds.interp_op interp_op Bounds.is_bounded_by Relations.interp_flat_type_rel_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop SmartVarfMap smart_interp_flat_map lift_op SmartFlatTypeMapUnInterp cast_const Zinterp_op SmartFlatTypeMapInterp2 - Z.add_with_get_carry Bounds.add_with_get_carry Bounds.sub_with_get_borrow Bounds.get_carry Bounds.get_borrow Z.get_carry Bounds.mul_split]; - cbn [interpToZ fst snd]; - repeat match goal with - | [ |- _ /\ _ ] => split - end; - lazymatch goal with - | [ |- Bounds.is_bounded_by' (Bounds.truncation_bounds _ _) (ZToInterp _) ] - => apply is_bounded_by_truncation_bounds' - end. -Local Ltac handle_mul := - apply (ZRange.monotone_four_corners_genb Z.mul); try (split; auto); - unfold Basics.flip; - let x := fresh "x" in - intro x; - exists (0 <=? x); - break_match; Z.ltb_to_lt; - intros ???; nia. -Lemma is_bounded_by_interp_op t tR (opc : op t tR) - (bs : interp_flat_type Bounds.interp_base_type _) - (v : interp_flat_type interp_base_type _) - (H : Bounds.is_bounded_by bs v) - (H_side : to_prop (interped_op_side_conditions opc v)) - : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v). -Proof. - destruct opc; apply_is_bounded_by_truncation_bounds; - [ .. - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _); - [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_mod ]; - ibbio_prefin - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _)) (v:=ZToInterp _); - [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_div ]; - ibbio_prefin - | - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _); - ibbio_prefin - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _)) (v:=ZToInterp _); - ibbio_prefin - | - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _); - ibbio_prefin - | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (-(v / _))) (v:=ZToInterp _); - ibbio_prefin ]; - repeat first [ progress simpl in * - | progress cbv [Bounds.interp_base_type Bounds.is_bounded_by' ZRange.is_bounded_by'] in * - | progress destruct_head'_prod - | progress destruct_head'_and - | omega - | match goal with - | [ |- context[interpToZ ?x] ] - => generalize dependent (interpToZ x); clear x; intros - | [ |- _ /\ True ] => split; [ | tauto ] - end ]. - { apply (@ZRange.monotone_four_corners true true Z.add _); split; auto. } - { apply (@ZRange.monotone_four_corners true false Z.sub _); split; auto. } - { handle_mul. } - { apply (ZRange.monotone_four_corners_genb Z.shiftl); try (split; auto); - [ eexists; apply Z.shiftl_le_Proper1 - | exists true; apply Z.shiftl_le_Proper2 ]. } - { apply (ZRange.monotone_four_corners_genb Z.shiftr); try (split; auto); - [ eexists; apply Z.shiftr_le_Proper1 - | exists true; apply Z.shiftr_le_Proper2 ]. } - { cbv [Bounds.land Bounds.extremization_bounds]; break_innermost_match; - [ apply land_bounds_extreme; split; auto | .. ]; - repeat first [ progress simpl in * - | Zarith_t_step - | rewriter_t - | progress saturate_land_lor_facts - | split_min_max; omega ]. } - { cbv [Bounds.lor Bounds.extremization_bounds]; break_innermost_match; - [ apply lor_bounds_extreme; split; auto | .. ]; - repeat first [ progress simpl in * - | Zarith_t_step - | rewriter_t - | progress Zarith_land_lor_t_step - | solve [ split_min_max; try omega; try Zarith_land_lor_t_step ] ]. } - { repeat first [ progress destruct_head Bounds.t - | progress simpl in * - | progress split_min_max - | omega ]. } - { cbv [Bounds.id_with_alt]; - break_innermost_match; simpl in *; Z.ltb_to_lt; subst; - split; assumption. } - { destruct_head Bounds.t; cbv [Bounds.zselect' Z.zselect]. - break_innermost_match; split_min_max; omega. } - { handle_mul. } - { apply Z.mod_bound_min_max; auto. } - { handle_mul. } - { auto with zarith. } - { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. } - { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. } - { apply Z.mod_bound_min_max; auto. } - { apply (@ZRange.monotone_eight_corners true true true Z.add_with_carry _ _); split; auto. } - { auto with zarith. } - { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. } - { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. } - { apply Z.mod_bound_min_max; auto. } - { apply (@ZRange.monotone_eight_corners false true false Z.sub_with_borrow _ _); split; auto. } - { auto with zarith. } -Qed. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v deleted file mode 100644 index 7ffe0beb1..000000000 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v +++ /dev/null @@ -1,192 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Psatz. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Syntax.Equality. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.ZUtil.Morphisms. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Pow2. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.FixedWordSizesEquality. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.UniquePose. - -Local Open Scope Z_scope. - -Local Arguments lift_op : simpl never. -Local Arguments cast_back_flat_const : simpl never. -Local Arguments unzify_op : simpl never. -Local Arguments Z.pow : simpl never. -Local Arguments Z.add !_ !_. -Local Existing Instances Z.pow_Zpos_le_Proper Z.log2_up_le_Proper. - -Section with_round_up. - Context (is_bounded_by_interp_op - : forall t tR (opc : op t tR) - (bs : interp_flat_type Bounds.interp_base_type _) - (v : interp_flat_type interp_base_type _) - (H : Bounds.is_bounded_by bs v) - (Hside : to_prop (interped_op_side_conditions opc v)), - Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v)). - Context {round_up : nat -> option nat}. - - Local Notation pick_typeb := (@Bounds.bounds_to_base_type round_up) (only parsing). - Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). - - Local Ltac t_small := - repeat first [ progress cbv [Bounds.bounds_to_base_type Bounds.smallest_logsz Bounds.actual_logsz] in * - | progress simpl in * - | progress autorewrite with push_Zof_nat zsimplify_const - | solve [ trivial ] - | progress change (@interpToZ) with (fun t1 => cast_const (t1:=t1) (t2:=TZ)) in * - | progress change (@cast_const TZ TZ) with (fun x : Z => x) in * - | progress Z.ltb_to_lt - | rewrite Z2Nat.id in * by auto with zarith - | rewrite <- Z.log2_up_le_pow2_full in * by auto with zarith - | break_innermost_match_step - | apply conj - | omega - | rewrite <- Z.log2_up_le_full - | match goal with - | [ |- ?x < ?y ] => cut (x + 1 <= y); [ omega | ] - | [ H : (_ <=? _)%nat = true |- _ ] => apply Nat.leb_le in H - | [ H : (_ <= _)%nat |- _ ] => apply inj_le in H - end ]. - - Local Arguments cast_const : simpl never. - Lemma interpToZ_cast_const_small T0 (bs : Bounds.interp_base_type T0) - (v : interp_base_type (@Bounds.bounds_to_base_type round_up T0 bs)) - (H : match Bounds.bit_width_of_base_type T0 with - | Some sz => 0 <= ZRange.lower bs /\ ZRange.upper bs < 2 ^ sz - | None => True - end) - (Hv : ZRange.lower bs <= interpToZ (cast_const (t2:=T0) v) <= ZRange.upper bs) - : interpToZ (cast_const (t2:=T0) v) = interpToZ v. - Proof. - destruct_head base_type; simpl in *; try reflexivity. - unfold Bounds.smallest_logsz, Bounds.interp_base_type, cast_const in *. - break_innermost_match_hyps; Z.ltb_to_lt; simpl in *; - [ pose proof (wordToZ_range v) | omega ]. - rewrite wordToZ_ZToWord_mod_full. - rewrite wordToZ_ZToWord_mod_full in Hv. - revert Hv; apply Z.max_case_strong; Z.rewrite_mod_small; intros; try omega; []. - rewrite Z.mod_small; [ reflexivity | split; auto with zarith ]. - autorewrite with push_Zof_nat zsimplify_const in *. - rewrite Z2Nat.id in * by auto with zarith. - destruct_head' and. - eapply Z.lt_le_trans; [ eassumption | ]. - repeat first [ progress Z.peel_le - | rewrite <- Z.log2_up_pow2 by auto with zarith; progress Z.peel_le - | omega ]. - Qed. - - Local Existing Instances Z.pow_Zpos_le_Proper Z.pow_Zpos_le_Proper_flip Z.lt_le_flip_Proper_flip_impl. - Lemma ZToInterp_cast_const_small T (bs : Bounds.interp_base_type T) - v - (H : match Bounds.bit_width_of_base_type T with - | Some sz => 0 <= ZRange.lower bs /\ ZRange.upper bs < 2 ^ sz - | None => True - end) - (Hb : ZRange.lower bs <= interpToZ (@ZToInterp T v) <= ZRange.upper bs) - : @cast_const (@Bounds.bounds_to_base_type round_up T bs) T (ZToInterp v) = ZToInterp v. - Proof. - apply ZToInterp_eq_inj. - rewrite ?interpToZ_ZToInterp_mod. - rewrite interpToZ_ZToInterp_mod in Hb. - destruct T; simpl in *. - { unfold Bounds.actual_logsz. - break_innermost_match; Z.ltb_to_lt; try reflexivity; []. - t_small. - apply Z.max_case_strong; intros; Z.rewrite_mod_small; omega. } - { unfold Bounds.smallest_logsz. - break_innermost_match_step; Z.ltb_to_lt; try omega; []. - revert Hb; apply (Z.max_case_strong 0 v); intros; Z.rewrite_mod_small; try reflexivity. - rewrite Z.max_r by auto with zarith. - autorewrite with push_Zof_nat zsimplify_const in *. - rewrite Z2Nat.id by auto with zarith. - rewrite Z.mod_mod_small; try apply conj; auto with zarith; - repeat first [ rewrite <- Z.log2_up_le_pow2_full in * by auto with zarith - | rewrite <- Z.log2_up_le_full - | omega - | apply conj - | progress Z.peel_le - | rewrite <- Z.log2_up_pow2 by auto with zarith; progress Z.peel_le - | match goal with - | [ |- 2^?x mod 2^?y = 0 ] - => destruct (Z.pow2_lt_or_divides x y); - [ solve [ auto with zarith ] - | exfalso; assert (2^y <= 2^x) - | assumption ] - end ]. } - Qed. - - Lemma pull_cast_genericize_op - t tR (opc : op t tR) - (bs : interp_flat_type Bounds.interp_base_type t) - (v : interp_flat_type interp_base_type (pick_type bs)) - (H : Bounds.is_bounded_by bs - (SmartFlatTypeMapUnInterp - (fun (t1 : base_type) (b0 : Bounds.interp_base_type t1) => cast_const) v)) - (Hside : to_prop (interped_op_side_conditions opc (cast_back_flat_const v))) - : interp_op t tR opc (cast_back_flat_const v) - = cast_back_flat_const (interp_op (pick_type bs) (pick_type (Bounds.interp_op opc bs)) (genericize_op opc) v). - Proof. - pose proof (is_bounded_by_interp_op t tR opc bs). - unfold interp_op in *. - rewrite Zinterp_op_genericize_op. - generalize dependent (Zinterp_op t tR opc). - generalize dependent (Bounds.interp_op opc bs); simpl; intros. - repeat (destruct_one_head flat_type; try solve [ inversion opc ]); - repeat first [ progress simpl in * - | progress destruct_head unit - | progress destruct_head True - | progress cbv [unzify_op cast_back_flat_const lift_op Bounds.is_bounded_by' ZRange.is_bounded_by'] in * - | progress change (@interpToZ TZ) with (fun x : Z => x) in * - | progress specialize_by auto - | progress specialize_by constructor - | match goal with - | [ H : forall v, _ <= ?f v <= _ /\ _ -> _ |- context[?f ?v'] ] - => specialize (H v') - | _ => progress specialize_by_assumption - | _ => progress specialize_by auto - | [ H : forall v : unit, _ |- _ ] => specialize (H tt) - | [ H : forall v : _ * _, _ /\ _ -> _ |- _ ] - => specialize (fun v1 v2 p1 p2 => H (v1, v2) (conj p1 p2)); - cbn [fst snd] in H; - specialize (fun v1 p1 v2 p2 => H v1 v2 p1 p2) - end - | progress destruct_head'_and ]; - [ - | rewrite cast_const_idempotent_small by t_small; reflexivity - | .. ]; - repeat match goal with - | _ => progress change (@cast_const TZ) with @ZToInterp in * - | [ |- context[@cast_const ?x TZ] ] - => progress change (@cast_const x TZ) with (@interpToZ x) in * - | [ H : context[@cast_const ?x TZ] |- _ ] - => progress change (@cast_const x TZ) with (@interpToZ x) in * - end; - repeat match goal with - | _ => reflexivity - | _ => progress rewrite ?interpToZ_cast_const_small, ?ZToInterp_cast_const_small by auto - | [ H : context[ZToInterp (?f (interpToZ (cast_const ?v)))] |- _ ] - => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto - | [ H : context[(interpToZ (cast_const ?v), _)] |- _ ] - => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto - | [ H : context[(_, interpToZ (cast_const ?v))] |- _ ] - => rewrite (@interpToZ_cast_const_small _ _ v) in H by auto - end. - Qed. -End with_round_up. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v deleted file mode 100644 index 6486b2e00..000000000 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v +++ /dev/null @@ -1,197 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Psatz. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Util.ZUtil.Hints. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.ZSimplify.Core. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Shift. -Require Import Crypto.Util.ZUtil.LandLorShiftBounds. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZRange.Operations. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.FixedWordSizesEquality. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. - -Local Open Scope Z_scope. - -Ltac break_t_step := - first [ progress destruct_head'_and - | progress destruct_head'_or - | progress destruct_head'_prod - | progress split_andb - | break_innermost_match_step ]. - -Ltac fin_t := - first [ reflexivity - | assumption - | match goal with - | [ |- and _ _ ] - => first [ split; [ | solve [ fin_t ] ] - | split; [ solve [ fin_t ] | ] ]; - try solve [ fin_t ] - end - | omega ]. - -Ltac specializer_t_step := - first [ progress specialize_by_assumption - | progress specialize_by fin_t ]. - -Ltac Zarith_t_step := - first [ match goal with - | [ H : (?x <= ?y)%Z, H' : (?y <= ?x)%Z |- _ ] - => assert (x = y) by omega; clear H H' - end - | progress Z.ltb_to_lt_in_context ]. -Ltac Zarith_land_lor_t_step := - match goal with - | [ |- _ <= Z.lor _ _ <= _ ] - => split; etransitivity; [ | apply Z.lor_bounds; omega | apply Z.lor_bounds; omega | ] - | [ |- 2^Z.log2_up (?x + 1) - 1 <= 2^Z.log2_up (?y + 1) - 1 ] - => let H := fresh in assert (H : x <= y) by omega; rewrite H; reflexivity - end. -Ltac word_arith_t := - match goal with - | [ |- (0 <= FixedWordSizes.wordToZ ?w <= 2^2^Z.of_nat ?logsz - 1)%Z ] - => clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega - end. - -Ltac case_Zvar_nonneg_on x := - is_var x; - lazymatch type of x with - | Z => lazymatch goal with - | [ H : (0 <= x)%Z |- _ ] => fail - | [ H : (x < 0)%Z |- _ ] => fail - | _ => destruct (Z_lt_le_dec x 0); try omega - end - end. -Ltac case_Zvar_nonneg_step := - match goal with - | [ |- context[?x] ] - => case_Zvar_nonneg_on x - end. -Ltac case_Zvar_nonneg := repeat case_Zvar_nonneg_step. - -Ltac remove_binary_operation_le_hyps_step := - match goal with - | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ] - => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia); - clear H - | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ] - => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia); - clear H - | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ] - => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia); - clear H - | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ] - => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia); - clear H - | [ H : ?T, H' : ?T |- _ ] => clear H' - | [ H : ?A \/ (~?A /\ ?B), H' : ?A \/ (~?A /\ ?C) |- _ ] - => assert (A \/ (~A /\ (B /\ C))) by (clear -H H'; tauto); clear H H' - | _ => progress destruct_head' or; destruct_head' and; subst; try omega - | [ |- (_ <= _ <= _)%Z ] => split - | _ => case_Zvar_nonneg_step - end. - -Ltac saturate_with_shift_facts := - repeat match goal with - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x << ?x'] ] - => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y << ?y'] ] - => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?y'] ] - => unique assert (x >> y' <= y >> x') by (Z.shiftr_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?x'] ] - => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega) - end. -Ltac saturate_with_all_shift_facts := - repeat match goal with - | _ => progress saturate_with_shift_facts - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftl _ _] ] - => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftr _ _] ] - => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega) - end. -Ltac preprocess_shift_min_max := - repeat first [ rewrite (Z.min_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) - | rewrite (Z.min_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) - | rewrite (Z.max_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) - | rewrite (Z.max_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) - | rewrite (Z.min_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) - | rewrite (Z.min_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) - | rewrite (Z.max_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) - | rewrite (Z.max_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) ]. -Ltac saturate_land_lor_facts := - repeat match goal with - | [ |- context[Z.land ?x ?y] ] - => let H := fresh in - let H' := fresh in - assert (H : 0 <= x) by omega; - assert (H' : 0 <= y) by omega; - unique pose proof (Z.land_upper_bound_r x y H H'); - unique pose proof (Z.land_upper_bound_l x y H H') - | [ |- context[Z.land ?x ?y] ] - => unique assert (0 <= Z.land x y) by (apply Z.land_nonneg; omega) - | [ |- context[Z.land ?x ?y] ] - => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y - | [ |- context[Z.lor ?x ?y] ] - => let H := fresh in - let H' := fresh in - assert (H : 0 <= x) by omega; - assert (H' : 0 <= y) by omega; - unique pose proof (proj1 (Z.lor_bounds x y H H')); - unique pose proof (proj2 (Z.lor_bounds x y H H')) - | [ |- context[Z.lor ?x ?y] ] - => unique assert (0 <= Z.lor x y) by (apply Z.lor_nonneg; omega) - | [ |- context[Z.lor ?x ?y] ] - => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y - end. -Ltac handle_shift_neg := - repeat first [ rewrite !Z.shiftr_opp_r - | rewrite !Z.shiftl_opp_r - | rewrite !Z.shiftr_opp_l - | rewrite !Z.shiftl_opp_l ]. - -Ltac handle_four_corners_step_fast := - first [ progress destruct_head Bounds.t - | progress cbv [ZRange.four_corners] in * - | progress subst - | Zarith_t_step - | progress split_min_max - | omega - | nia ]. -Ltac handle_four_corners_step := - first [ handle_four_corners_step_fast - | remove_binary_operation_le_hyps_step ]. -Ltac handle_four_corners := - lazymatch goal with - | [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ] - => idtac - end; - repeat handle_four_corners_step. - -Ltac rewriter_t := - first [ rewrite !Bool.andb_true_iff - | rewrite !Bool.andb_false_iff - | rewrite !Bool.orb_true_iff - | rewrite !Bool.orb_false_iff - | rewrite !Z.abs_opp - | rewrite !Z.max_log2_up - | rewrite !Z.add_max_distr_r - | rewrite !Z.add_max_distr_l - | rewrite wordToZ_ZToWord by (autorewrite with push_Zof_nat zsimplify_const; omega) - | match goal with - | [ H : _ |- _ ] - => first [ rewrite !Bool.andb_true_iff in H - | rewrite !Bool.andb_false_iff in H - | rewrite !Bool.orb_true_iff in H - | rewrite !Bool.orb_false_iff in H ] - end ]. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v deleted file mode 100644 index c08ae1298..000000000 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.MapCastByDeBruijn. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. - -Section language. - Context (round_up : nat -> option nat) - {t : type base_type}. - - Definition MapCastCompile := @MapCastCompile t. - Definition MapCastDoCast - := @MapCastDoCast - (@Bounds.interp_base_type) (@Bounds.interp_op) - (@Bounds.bounds_to_base_type round_up) - (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) - t. - Definition MapCastDoInterp - := @MapCastDoInterp - (@Bounds.interp_base_type) (@Bounds.bounds_to_base_type round_up) - t. - Definition MapCast e input_bounds - := MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)). -End language. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v deleted file mode 100644 index 1217cd721..000000000 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v +++ /dev/null @@ -1,48 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.InterpSideConditions. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. -Require Import Crypto.Util.PointedProp. - -Lemma MapCastCorrect - {round_up} - {t} (e : Expr t) - (Hwf : Wf e) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) - v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e v)), - Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b - /\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v) - /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v). -Proof. - apply MapCastCorrect; auto. - { apply is_bounded_by_interp_op. } - { apply pull_cast_genericize_op, is_bounded_by_interp_op. } -Qed. - -Lemma MapCastCorrect_eq - {round_up} - {t} (e : Expr t) - {evb ev} - (Hwf : Wf e) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) - v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e v)) - (Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds) - (Hev : ev = Compilers.Syntax.Interp interp_op e v), - evb = b - /\ Bounds.is_bounded_by b ev - /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev. -Proof. - intros; subst; apply MapCastCorrect; auto. -Qed. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v deleted file mode 100644 index fabb8b2b8..000000000 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Z.MapCastByDeBruijnWf. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. - -Definition Wf_MapCast - {round_up} - {t} (e : Expr t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e')) - (Hwf : Wf e) - : Wf e' - := @Wf_MapCast - (@Bounds.interp_base_type) (@Bounds.interp_op) - (@Bounds.bounds_to_base_type round_up) - (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) - t e input_bounds b e' He' Hwf. - -Definition Wf_MapCast_arrow - {round_up} - {s d} (e : Expr (Arrow s d)) - (input_bounds : interp_flat_type Bounds.interp_base_type s) - {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e')) - (Hwf : Wf e) - : Wf e' - := @Wf_MapCast_arrow - (@Bounds.interp_base_type) (@Bounds.interp_op) - (@Bounds.bounds_to_base_type round_up) - (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) - s d e input_bounds b e' He' Hwf. - -Hint Extern 1 (Wf ?e') -=> match goal with - | [ He : MapCast _ _ _ = Some (existT _ _ e') |- _ ] - => first [ refine (@Wf_MapCast _ _ _ _ _ _ He _) - | refine (@Wf_MapCast_arrow _ _ _ _ _ _ _ He _) ] - end : wf. diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v deleted file mode 100644 index c7060ea44..000000000 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ /dev/null @@ -1,56 +0,0 @@ -(** * Reflective Pipeline *) -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics. -Import ListNotations. -Local Open Scope nat_scope. -Local Open Scope list_scope. -(** This file combines the various PHOAS modules in tactics, - culminating in a tactic [refine_reflectively], which solves a goal of the form -<< -cast_back_flat_const (?x args) = f (cast_back_flat_const args) - /\ Bounds.is_bounded_by ?bounds (?x args) ->> -while instantiating [?x] and [?bounds] with nicely-reduced constants. - *) - -Module Export Exports. - Export Glue.Exports. - Export ReflectiveTactics.Exports. - Existing Instance DefaultedTypes.by_default. -End Exports. - -Ltac refine_reflectively_gen allowable_bit_widths opts := - refine_to_reflective_glue allowable_bit_widths; - do_reflective_pipeline opts. - -Ltac refine_reflectively128_with opts := refine_reflectively_gen [128; 256] opts. -Ltac refine_reflectively64_with opts := refine_reflectively_gen [64; 128] opts. -Ltac refine_reflectively32_with opts := refine_reflectively_gen [32; 64] opts. -Ltac refine_reflectively128_with_bool_with opts := refine_reflectively_gen [1; 128; 256] opts. -Ltac refine_reflectively64_with_bool_with opts := refine_reflectively_gen [1; 64; 128] opts. -Ltac refine_reflectively32_with_bool_with opts := refine_reflectively_gen [1; 32; 64] opts. -Ltac refine_reflectively128_with_uint8_with opts := refine_reflectively_gen [8; 128; 256] opts. -Ltac refine_reflectively64_with_uint8_with opts := refine_reflectively_gen [8; 64; 128] opts. -Ltac refine_reflectively32_with_uint8_with opts := refine_reflectively_gen [8; 32; 64] opts. -Ltac refine_reflectively128 := refine_reflectively128_with default_PipelineOptions. -Ltac refine_reflectively64 := refine_reflectively64_with default_PipelineOptions. -Ltac refine_reflectively32 := refine_reflectively32_with default_PipelineOptions. -Ltac refine_reflectively128_with_bool := refine_reflectively128_with_bool_with default_PipelineOptions. -Ltac refine_reflectively64_with_bool := refine_reflectively64_with_bool_with default_PipelineOptions. -Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with default_PipelineOptions. -Ltac refine_reflectively128_with_uint8 := refine_reflectively128_with_uint8_with default_PipelineOptions. -Ltac refine_reflectively64_with_uint8 := refine_reflectively64_with_uint8_with default_PipelineOptions. -Ltac refine_reflectively32_with_uint8 := refine_reflectively32_with_uint8_with default_PipelineOptions. - -(** Convenience notations for options *) -Definition anf := {| Pipeline.Definition.anf := true |}. -Definition anf_without_adc_fusion := {| Pipeline.Definition.anf := true ; Pipeline.Definition.adc_fusion := false |}. -Definition adc_fusion := {| Pipeline.Definition.adc_fusion := true |}. -Definition default := default_PipelineOptions. - -(** The default *) -Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts. -Ltac refine_reflectively_with_uint8_with opts := refine_reflectively64_with_uint8_with opts. -Ltac refine_reflectively_with opts := refine_reflectively64_with opts. -Ltac refine_reflectively := refine_reflectively_with default. diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v deleted file mode 100644 index 435ec793e..000000000 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ /dev/null @@ -1,285 +0,0 @@ -(** * Reflective Pipeline: Main Pipeline Definition *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.OutputType. -(** This file contains the definitions of the assembling of the - various transformations that are used in the pipeline. There are - two stages to the reflective pipeline, with different - requirements. - - The pre-Wf stage is intended to consist of transformations that - make the term smaller, and, importantly, should only consist of - transformations whose interpretation-correctness proofs do not - require well-founded hypotheses. Generally this is the case for - transformations whose input and output [var] types match. The - correctness condition for this stage is that the interpretation of - the transformed term must equal the interpretation of the original - term, with no side-conditions. - - The post-Wf stage is the rest of the pipeline; its correctness - condition must have the shape of the correctness condition for - word-size selection. We define a record to hold the transformed - term, so that we can get bounds and similar out of it, without - running into issues with slowness of conversion. *) - -(** ** Pre-Wf Stage *) -(** *** Pre-Wf Pipeline Imports *) -Require Import Crypto.Compilers.Eta. -Require Import Crypto.Compilers.EtaInterp. -Require Import Crypto.Compilers.Linearize. -Require Import Crypto.Compilers.LinearizeInterp. -Require Import Crypto.Compilers.Z.ArithmeticSimplifier. -Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp. - -(** *** Definition of the Pre-Wf Pipeline *) -(** Do not change the name or the type of this definition *) -Definition PreWfPipeline {t} (e : Expr t) : Expr _ - := ExprEta (SimplifyArith false (Linearize e)). - -(** *** Correctness proof of the Pre-Wf Pipeline *) -(** Do not change the statement of this lemma. You shouldn't need to - change it's proof, either; all of the relevant lemmas should be in - the [reflective_interp] rewrite database. If they're not, you - should find the file where they are defined and add them. *) -Lemma InterpPreWfPipeline {t} (e : Expr t) - : forall x, Interp (PreWfPipeline e) x = Interp e x. -Proof. - unfold PreWfPipeline; intro. - repeat autorewrite with reflective_interp. - reflexivity. -Qed. - - - -(** ** Post-Wf Stage *) -(** *** Post-Wf Pipeline Imports *) -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.EtaWf. -Require Import Crypto.Compilers.Z.Inline. -Require Import Crypto.Compilers.Z.InlineInterp. -Require Import Crypto.Compilers.Z.InlineWf. -Require Import Crypto.Compilers.Linearize. -Require Import Crypto.Compilers.LinearizeInterp. -Require Import Crypto.Compilers.LinearizeWf. -(*Require Import Crypto.Compilers.Z.CommonSubexpressionElimination. -Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationInterp. -Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationWf.*) -Require Import Crypto.Compilers.Z.ArithmeticSimplifierWf. -Require Import Crypto.Compilers.Z.RewriteAddToAdc. -Require Import Crypto.Compilers.Z.RewriteAddToAdcWf. -Require Import Crypto.Compilers.Z.RewriteAddToAdcInterp. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf. -Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Util.DefaultedTypes. - -(** *** Definition of the Post-Wf Pipeline *) -(** We define the record that holds various options to customize the - pipeline. *) -Record PipelineOptions := - { - anf : with_default bool false; - adc_fusion : with_default bool true; - }. -Definition default_PipelineOptions := {| anf := _ |}. - -(** Do not change the name or the type of these two definitions *) -(** The definition [PostWfPreBoundsPipeline] is for the part of the - pipeline that comes before [MapCast]; it must preserve the type of - the expression. *) -Definition PostWfPreBoundsPipeline - (opts : PipelineOptions) - {t} (e : Expr t) - : Expr t - := let e := InlineConst e in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := InlineConst (Linearize (SimplifyArith false e)) in - let e := if opts.(anf) then InlineConst (ANormal e) else e in - let e := if opts.(adc_fusion) then RewriteAdc e else e in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - (*let e := CSE false e in*) - e. -(** The definition [PostWfBoundsPipeline] is for the part of the - pipeline that begins with [MapCast]. *) -Definition PostWfBoundsPipeline - round_up - (opts : PipelineOptions) - {t} (e0 : Expr t) - (e : Expr t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : option (@ProcessedReflectivePackage round_up) - := Build_ProcessedReflectivePackage_from_option_sigma - e0 input_bounds - (let e := MapCast _ e input_bounds in - option_map - (projT2_map - (fun b e' - => let e' := InlineConst e' in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := InlineConst (Linearize (SimplifyArith false e')) in - let e' := if opts.(anf) then InlineConst (ANormal e') else e' in - let e' := ExprEta e' in - e')) - e). - -(** *** Correctness proof of the Post-Wf Pipeline *) -(** Do not change the statement of this lemma. *) -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Equality. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.InterpSideConditions. -Require Import Crypto.Compilers.InterpRewriting. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.PointedProp. - -Section with_round_up_list. - Context {allowable_lgsz : list nat}. - - Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing). - Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). - Local Opaque to_prop InterpSideConditions. - - Definition PostWfPreBoundsPipelineCorrect - opts - {t} - (e : Expr t) - (Hwf : Wf e) - (e' := PostWfPreBoundsPipeline opts e) - : (forall v, Interp e' v = Interp e v) /\ Wf e'. - Proof using Type. - (** These first two lines probably shouldn't change much *) - unfold PostWfPreBoundsPipeline in *; subst e'. - break_match_hyps. - (** Now handle all the transformations that come before the word-size selection *) - rewrite_reflective_interp_cached. - split; intros; finish_rewrite_reflective_interp_cached; auto. - Qed. - - Definition PostWfBoundsPipelineCorrect - opts - {t} - (e0 : Expr t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - (e : Expr t) - (Hwf : Wf e) - {b e'} (He' : PostWfBoundsPipeline _ opts e0 e input_bounds - = Some {| input_expr := e0 ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |}) - (v : interp_flat_type Syntax.interp_base_type (domain t)) - (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds)) - (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e v)) - : Bounds.is_bounded_by b (Interp e v) - /\ cast_back_flat_const (Interp e' v') = Interp e v. - Proof using Type. - (** These first two lines probably shouldn't change much *) - unfold PostWfBoundsPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *. - repeat (break_match_hyps || inversion_option || inversion_ProcessedReflectivePackage - || inversion_sigma || eliminate_hprop_eq || inversion_prod - || simpl in * || subst). - (** Now handle all the transformations that come after the word-size selection *) - all:rewrite_reflective_interp_cached. - (** Now handle word-size selection *) - all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | assumption | .. ]; - [ solve_wf_side_condition | reflexivity | ]). - all:reflexivity. - Qed. - - Definition PostWfPipelineCorrect - opts - {t} - (e : Expr t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - (Hwf : Wf e) - (e' := PostWfPreBoundsPipeline opts e) - {b e''} (He' : PostWfBoundsPipeline _ opts e e' input_bounds - = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e'' |}) - (v : interp_flat_type Syntax.interp_base_type (domain t)) - (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds)) - (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e' v)) - : Bounds.is_bounded_by b (Interp e v) - /\ cast_back_flat_const (Interp e'' v') = Interp e v. - Proof. - rewrite <- (proj1 (PostWfPreBoundsPipelineCorrect opts e Hwf)) by assumption. - eapply PostWfBoundsPipelineCorrect; eauto. - apply PostWfPreBoundsPipelineCorrect; assumption. - Qed. -End with_round_up_list. - -(** ** Constant Simplification and Unfolding *) -(** The reflective pipeline may introduce constants that you want to - unfold before instantiating the refined term; you can control that - here. A number of reflection-specific constants are always - unfolded (in ReflectiveTactics.v). Currently, we also reduce - expressions of the form [wordToZ (ZToWord Z_literal)], as - specified here. *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.FixedWordSizes. -Require Import bbv.WordScope. - -Module Export Exports. (* export unfolding strategy *) - (* iota is probably (hopefully?) the cheapest reduction. - Unfortunately, we can't say no-op here. This is meant to be - extended. *) - Declare Reduction extra_interp_red := cbv iota. - - (** Overload this to change reduction behavior of constants of the - form [wordToZ (ZToWord Z_literal)]. You might want to set this - to false if your term is very large, to speed things up. *) - Ltac do_constant_simplification := constr:(true). - - Global Arguments ZToWord !_ !_ / . - Global Arguments wordToZ !_ !_ / . - Global Arguments word_case_dep _ !_ _ _ _ _ / . - Global Arguments ZToWord32 !_ / . - Global Arguments ZToWord64 !_ / . - Global Arguments ZToWord128 !_ / . - Global Arguments ZToWord_gen !_ !_ / . - Global Arguments word32ToZ !_ / . - Global Arguments word64ToZ !_ / . - Global Arguments word128ToZ !_ / . - Global Arguments wordToZ_gen !_ !_ / . - Global Arguments Z.to_N !_ / . - Global Arguments Z.of_N !_ / . - Global Arguments Word.NToWord !_ !_ / . - Global Arguments Word.wordToN !_ !_ / . - Global Arguments Word.posToWord !_ !_ / . - Global Arguments N.succ_double !_ / . - Global Arguments Word.wzero' !_ / . - Global Arguments N.double !_ . - Global Arguments Nat.pow !_ !_ / . - Global Arguments Nat.mul !_ !_ / . - Global Arguments Nat.add !_ !_ / . - - Declare Reduction constant_simplification := cbn [FixedWordSizes.wordToZ FixedWordSizes.ZToWord word_case_dep ZToWord32 ZToWord64 ZToWord128 ZToWord_gen word32ToZ word64ToZ word128ToZ wordToZ_gen Word.NToWord Word.wordToN Word.posToWord Word.wzero' Z.to_N Z.of_N N.succ_double N.double Nat.pow Nat.mul Nat.add]. -End Exports. diff --git a/src/Compilers/Z/Bounds/Pipeline/Glue.v b/src/Compilers/Z/Bounds/Pipeline/Glue.v deleted file mode 100644 index ed9abf9a6..000000000 --- a/src/Compilers/Z/Bounds/Pipeline/Glue.v +++ /dev/null @@ -1,550 +0,0 @@ -(** * Reflective Pipeline: Glue Code *) -(** This file defines the tactics that transform a non-reflective goal - into a goal the that the reflective machinery can handle. *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Reify. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Reify. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Curry. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Sigma.Associativity. -Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Util.Logic.ImplAnd. -Require Import Crypto.Util.Tactics.EvarExists. -Require Import Crypto.Util.Tactics.GetGoal. -Require Import Crypto.Util.Tactics.PrintContext. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.ClearAll. -Require Import Crypto.Util.Tactics.ClearbodyAll. - -Module Export Exports. - Export Crypto.Compilers.Z.Reify. (* export for the tactic redefinitions *) -End Exports. - -(** ** [reassoc_sig_and_eexists] *) -(** The [reassoc_sig_and_eexists] tactic operates on a goal convertible with -<< -{ f : { a | is_bounded_by bounds a } -| BoundedWordToZ f = rexprZ (BoundedWordToZ a) ... (BoundedWordToZ z) } ->> - and leaves a goal of the form -<< -is_bounded_by bounds (map wordToZ ?f) - /\ map wordToZ ?f = rexprZ (map wordToZ (proj1_sig a)) ... (map wordToZ (proj1_sig z)) ->> - where [?f] is a context variable set to a new evar. This tactic - relies on the exact definition of [BoundedWordToZ]. *) - - -(** The tactic [unfold_paired_tuple_map] unfolds any [Tuple.map]s - applied to [pair]s. *) -Ltac unfold_paired_tuple_map := - repeat match goal with - | [ |- context[Tuple.map (n:=S ?N) _ (pair _ _)] ] - => progress change (@Tuple.map (S N)) with (fun A B f => @Tuple.map' A B f N); cbv beta iota delta [Tuple.map'] - end. -(** The tactic [change_to_reified_type f] reifies the type of a - context variable [f] and changes [f] to the interpretation of that - type. *) -Ltac change_to_reified_type f := - let T := type of f in - let cT := (eval compute in T) in - let rT := reify_type cT in - change (interp_type Syntax.interp_base_type rT) in (type of f). - -(** The tactic [goal_dlet_to_context_curried] moves to the - context any [dlet x := y in ...] in the goal, curries each such - moved definition, and then reifies the type of each such context - variable. *) -Ltac goal_dlet_to_context_curried := - lazymatch goal with - | [ |- context[@Let_In ?A ?B ?x _] ] - => let f := fresh in - goal_dlet_to_context_step f; - change_with_curried f; - change_to_reified_type f; - goal_dlet_to_context_curried - | _ => idtac - end. -(** The tactic [preunfold_and_dlet_to_context] will unfold - [BoundedWordToZ] and [Tuple.map]s applied to [pair]s, and then - look for a [dlet x := y in ...] in the RHS of a goal of shape [{a - | LHS = RHS }] and replace it with a context variable. *) -Ltac preunfold_and_dlet_to_context _ := - unfold_paired_tuple_map; - cbv [BoundedWordToZ]; cbn [fst snd proj1_sig]; - goal_dlet_to_context_curried. -(** The tactic [pattern_proj1_sig_in_lhs_of_sig] takes a goal of the form -<< -{ a : A | P } ->> - where [A] is a sigma type, and leaves a goal of the form -<< -{ a : A | dlet p := P' in p (proj1_sig a) ->> - where all occurrences of [proj1_sig a] have been abstracted out of - [P] to make [P']. *) -Ltac pattern_proj1_sig_in_sig := - eapply proj2_sig_map; - [ let a := fresh in - let H := fresh in - intros a H; - lazymatch goal with - | [ |- context[@proj1_sig ?A ?P a] ] - => pattern (@proj1_sig A P a) - end; - lazymatch goal with - | [ |- ?P ?p1a ] - => cut (dlet p := P in p p1a); - [ repeat (clear_all; clearbody_all); - abstract (cbv [Let_In]; exact (fun x => x)) | ] - end; - exact H - | cbv beta ]. -(** The tactic [pattern_sig_sig_assoc] takes a goal of the form -<< -{ a : { a' : A | P } | Q } ->> - where [Q] mentions [proj1_sig a] but not [proj2_sig a], and leaves - a goal of the form -<< -{ a : A | P /\ Q } ->> - *) -Ltac pattern_sig_sig_assoc := - pattern_proj1_sig_in_sig; - let f := fresh in - goal_dlet_to_context_step f; - apply sig_sig_assoc; - subst f; cbv beta. -(** The tactic [reassoc_sig_and_eexists] will take a goal either of the form -<< -{ a : { a' : A | P a' } | Q (proj1_sig a) } ->> - where [Q] mentions [proj1_sig a] but not [proj2_sig a], and leave - a goal of the form -<< -P ?a /\ Q ?a ->> - - The tactic [maybe_reassoc_sig_and_eexists] also supports goals that - don't need to be reassociated. - *) -Ltac reassoc_sig_and_eexists := - pattern_sig_sig_assoc; - evar_exists. -Ltac maybe_reassoc_sig_and_eexists _ := - lazymatch goal with - | [ |- { a : ?T | _ } ] - => lazymatch (eval hnf in T) with - | { a' | _ } - => reassoc_sig_and_eexists - | _ => evar_exists - end - end. - -(** ** [intros_under_and] *) -(** The [intros_under_and] tactic takes a goal of the form -<< -(A -> B -> ... -> Y -> Z) /\ (A -> B -> ... -> Y -> Z') ->> - and turns it into a goal of the form -<< -Z /\ Z' ->> - where [A], [B], ..., [Y] have been introduced into the context. *) -Ltac intros_under_and _ := - repeat (apply (proj1 impl_and_iff); intro); intros. - -(** ** [do_curry_rhs] *) -(** The [do_curry_rhs] tactic takes a goal of the form -<< -_ /\ _ = F A B ... Z ->> - and turns it into a goal of the form -<< -_ /\ _ = F' (A, B, ..., Z) ->> - *) -Ltac do_curry_rhs _ := - lazymatch goal with - | [ |- _ /\ _ = ?f_Z ] - => let f_Z := head f_Z in - change_with_curried f_Z - end. - -(** ** [split_BoundedWordToZ] *) -(** The [split_BoundedWordToZ] tactic takes a goal of the form -<< -_ /\ (map wordToZ (proj1_sig f1), ... map wordToZ (proj1_sig fn)) = F ARGS ->> - and splits [f1] ... [fn] and any arguments in ARGS into two - parts, one part about the computational behavior, and another part - about the boundedness. - - This pipeline relies on the specific definition of - [BoundedWordToZ], and requires [f] to be a context variable which - is set to a single evar. *) -(** First we ensure the goal has the right shape, and give helpful - error messages if it does not *) -Ltac check_fW_type descr top_fW fW := - lazymatch fW with - | fst ?fW => check_fW_type descr top_fW fW - | snd ?fW => check_fW_type descr top_fW fW - | _ => let G := get_goal in - let shape := uconstr:(Tuple.map wordToZ ?fW) in - let efW := uconstr:(?fW) in - first [ is_var fW - | fail 1 "In the goal" G - descr shape - "where" efW "must be a repeated application of fst and snd" - "to a single context variable which is defined to be an evar." - "The term" top_fW "is based on" fW "which is not a variable" ]; - match goal with - | [ fW' := ?e |- _ ] - => constr_eq fW' fW; - first [ is_evar e - | fail 2 "In the goal" G - descr shape - "where" efW "must be a repeated application of fst and snd" - "to a single context variable which is defined to be an evar." - "The term" top_fW "is based on" fW' "which is a context variable" - "with body" e "which is not a bare evar" ] - | [ fW' : _ |- _ ] - => constr_eq fW fW'; - fail 1 "In the goal" G - descr shape - "where" efW "must be a repeated application of fst and snd" - "to a single context variable which is defined to be an evar." - "The term" top_fW "is based on" fW' "which is a context variable without a body" - | _ => fail 1 "In the goal" G - descr shape - "where" efW "must be a repeated application of fst and snd" - "to a single context variable which is defined to be an evar." - "The term" top_fW "is based on" fW "which is not a context variable" - end - end. -Tactic Notation "check_fW_type" string(descr) constr(fW) - := check_fW_type descr fW fW. -Ltac check_is_map_wordToZ lvl descr top_subterm subterm := - lazymatch subterm with - | wordToZ => idtac - | Tuple.map ?f => check_is_map_wordToZ lvl descr top_subterm f - | _ => let map_shape := uconstr:(Tuple.map) in - let wordToZ_shape := uconstr:(wordToZ) in - fail lvl descr - "which are a repeated application of" map_shape "to" wordToZ_shape - "but in the subterm" top_subterm "the function" subterm - "was found, which is not of this form" - end. -Tactic Notation "check_is_map_wordToZ" int_or_var(lvl) string(descr) constr(term) - := check_is_map_wordToZ lvl descr term term. - -Ltac check_is_bounded_by_shape subterm_type := - lazymatch subterm_type with - | ZRange.is_bounded_by None ?bounds (Tuple.map wordToZ ?fW) - => check_fW_type "The ℤ argument to is_bounded_by must have the shape" fW - | ?A /\ ?B - => check_is_bounded_by_shape A; - check_is_bounded_by_shape B - | _ => let G := get_goal in - let shape := uconstr:(ZRange.is_bounded_by None ?bounds (Tuple.map wordToZ ?fW)) in - fail "In the goal" G - "The first conjunct of the goal is expected to be a conjunction of things of the shape" shape - "but a subterm not matching this shape was found:" subterm_type - end. -Ltac check_LHS_Z_shape subterm := - lazymatch subterm with - | Tuple.map ?f ?fW - => check_is_map_wordToZ 0 "The left-hand side of the second conjunct of the goal must be a tuple of terms" f; - check_fW_type "The left-hand side of the second conjunct of the goal must be a tuple of terms with shape" fW - | (?A, ?B) - => check_LHS_Z_shape A; - check_LHS_Z_shape B - | _ => let G := get_goal in - let shape := uconstr:(Tuple.map wordToZ ?fW) in - let ef := uconstr:(?f) in - let shape' := uconstr:(Tuple.map ?f ?fW) in - let map_shape := uconstr:(Tuple.map) in - let wordToZ_shape := uconstr:(wordToZ) in - fail "In the goal" G - "The second conjunct of the goal is expected to be a equality whose" - "left-hand side is a tuple of terms of the shape" shape - "or" shape' "where" ef "is a repeated application of" map_shape "to" wordToZ_shape - "but a subterm not matching this shape was found:" subterm - end. -Ltac check_RHS_Z_shape_rec subterm := - lazymatch subterm with - | Tuple.map ?f ?fW - => check_is_map_wordToZ - 0 - "The second conjunct of the goal is expected to be a equality whose right-hand side is the application of a function to a tuple of terms" f - | (?A, ?B) - => check_RHS_Z_shape_rec A; - check_RHS_Z_shape_rec B - | _ => let G := get_goal in - let shape := uconstr:(Tuple.map wordToZ ?fW) in - let ef := uconstr:(?f) in - let shape' := uconstr:(Tuple.map ?f ?fW) in - let map_shape := uconstr:(Tuple.map) in - let wordToZ_shape := uconstr:(wordToZ) in - fail "In the goal" G - "The second conjunct of the goal is expected to be a equality whose" - "right-hand side is the application of a function to a tuple of terms of the shape" shape - "or" shape' "where" ef "is a repeated application of" map_shape "to" wordToZ_shape - "but a subterm not matching this shape was found:" subterm - end. -Ltac check_RHS_Z_shape RHS := - lazymatch RHS with - | ?f ?args - => let G := get_goal in - first [ is_var f - | fail 1 "In the goal" G - "The second conjunct of the goal is expected to be a equality whose" - "right-hand side is the application of a single context-variable to a tuple" - "but the right-hand side is" RHS - "which is an application of something which is not a context variable:" f ]; - check_RHS_Z_shape_rec args - | _ => let G := get_goal in - let shape := uconstr:(Tuple.map wordToZ ?fW) in - let ef := uconstr:(?f) in - let shape' := uconstr:(Tuple.map ?f ?fW) in - let map_shape := uconstr:(Tuple.map) in - let wordToZ_shape := uconstr:(wordToZ) in - fail "In the goal" G - "The second conjunct of the goal is expected to be a equality whose" - "right-hand side is the application of a function to a tuple of terms of the shape" shape - "or" shape' "where" ef "is a repeated application of" map_shape "to" wordToZ_shape - "but the right-hand side is not a function application:" RHS - end. -Ltac check_precondition _ := - lazymatch goal with - | [ |- ?is_bounded_by /\ ?LHS = ?RHS ] - => check_is_bounded_by_shape is_bounded_by; - check_LHS_Z_shape LHS; - check_RHS_Z_shape RHS - | [ |- ?G ] - => let shape := uconstr:(?is_bounded /\ ?LHS = ?RHS) in - fail "The goal has the wrong shape for reflective gluing; expected" shape "but found" G - end. -Ltac split_BoundedWordToZ _ := - (** first revert the context definition which is an evar named [f] - in the docs above, so that it becomes evar 1 (for - [instantiate]), and so that [make_evar_for_first_projection] - works. It's not the most robust way to find the right term; - maybe we should modify some of the checks above to assert that - the evar found is a particular one? *) - check_precondition (); - lazymatch goal with - | [ |- _ /\ ?LHS = _ ] - => match goal with - | [ f := ?e |- _ ] - => is_evar e; match LHS with context[f] => idtac end; - revert f - end - end; - let destruct_sig x := - is_var x; - first [ clearbody x; fail 1 - | (** we want to keep the same context variable in the - evar that we reverted above, and in the current - goal; hence the instantiate trick *) - instantiate (1:=ltac:(destruct x)); destruct x ] in - let destruct_pair x := - is_var x; - first [ clearbody x; fail 1 - | (** we want to keep the same context variable in the - evar that we reverted above, and in the current - goal; hence the instantiate trick *) - change (fst x) with (let (a, b) := x in a) in *; - change (snd x) with (let (a, b) := x in b) in *; - instantiate (1:=ltac:(destruct x)); destruct x ]; - (cbv beta iota) in - let destruct_sig_or_pair v := - match v with - | context[proj1_sig ?x] => destruct_sig x - | context[fst ?x] => destruct_pair x - | context[snd ?x] => destruct_pair x - end in - repeat match goal with - | [ |- context[Tuple.map ?f ?v] ] - => check_is_map_wordToZ 0 "DEBUG" f; destruct_sig_or_pair v - | [ H := context[Tuple.map ?f ?v] |- _ ] - => check_is_map_wordToZ 0 "DEBUG" f; destruct_sig_or_pair v - | [ H : context[Tuple.map ?f ?v] |- _ ] - => check_is_map_wordToZ 0 "DEBUG" f; destruct_sig_or_pair v - | [ H : _ /\ _ |- _ ] - => destruct H - end; - cbv beta iota in *; intro; (* put [f] back in the context so that [cbn] doesn't remove this let-in *) - cbn [proj1_sig] in *. - -(** ** [zrange_to_reflective] *) -(** The [zrange_to_reflective] tactic takes a goal of the form -<< -(is_bounded_by _ bounds (map wordToZ (?fW args)) /\ ...) - /\ (map wordToZ (?fW args), ...) = fZ argsZ ->> - and uses [cut] and a small lemma to turn it into a goal that the - reflective machinery can handle. The goal left by this tactic - should be fully solvable by the reflective pipeline. *) - -Lemma adjust_goal_for_reflective {T P} (LHS RHS : T) - : P RHS /\ LHS = RHS -> P LHS /\ LHS = RHS. -Proof. intros [? ?]; subst; tauto. Qed. -Ltac adjust_goal_for_reflective := apply adjust_goal_for_reflective. -Ltac unmap_wordToZ_tuple term := - lazymatch term with - | (?x, ?y) => let x' := unmap_wordToZ_tuple x in - let y' := unmap_wordToZ_tuple y in - constr:((x', y')) - | Tuple.map ?f ?x - => let dummy := match goal with - | _ => check_is_map_wordToZ 1 "In unmap_wordToZ_tuple, expected terms" f - end in - x - end. -Ltac bounds_from_is_bounded_by T := - lazymatch T with - | ?A /\ ?B => let a := bounds_from_is_bounded_by A in - let b := bounds_from_is_bounded_by B in - constr:((a, b)) - | ZRange.is_bounded_by _ ?bounds _ - => bounds - end. -Ltac pose_proof_bounded_from_Zargs_hyps Zargs H := - lazymatch Zargs with - | (?a, ?b) - => let Ha := fresh in - let Hb := fresh in - pose_proof_bounded_from_Zargs_hyps a Ha; - pose_proof_bounded_from_Zargs_hyps b Hb; - let pf := constr:(conj Ha Hb) in - lazymatch type of pf with - | @Bounds.is_bounded_by ?A ?boundsA (@cast_back_flat_const ?var ?tA ?f ?VA ?argsA) - /\ @Bounds.is_bounded_by ?B ?boundsB (@cast_back_flat_const ?var ?tB ?f ?VB ?argsB) - => pose proof - ((pf : @Bounds.is_bounded_by - (Prod A B) (boundsA, boundsB) - (@cast_back_flat_const var (Prod tA tB) f (VA, VB) (argsA, argsB)))) - as H; - clear Ha Hb - | ?pfT - => let shape - := uconstr:(@Bounds.is_bounded_by ?A ?boundsA (@cast_back_flat_const ?var ?tA ?f ?VA ?argsA) - /\ @Bounds.is_bounded_by ?B ?boundsB (@cast_back_flat_const ?var ?tB ?f ?VB ?argsB)) in - fail 1 "Returned value from recursive call of bounded_from_Zargs_hyps has the wrong type" - "Cannot match type" pfT - "with shape" shape - end - | Tuple.map ?f ?arg - => first [ check_is_map_wordToZ 0 "DEBUG" f - | let G := get_goal in - idtac "In the context:"; print_context (); - idtac "In the goal:" G; - idtac "When looking for bounds for" Zargs; - check_is_map_wordToZ 1 "Expected a map of a function" f ]; - pose_proof_bounded_from_Zargs_hyps arg H - | ?arg => - lazymatch goal with - | [ H' : Bounds.is_bounded_by ?bounds (cast_back_flat_const arg) |- _ ] - => rename H' into H - | _ => let shape := uconstr:(Bounds.is_bounded_by _ (cast_back_flat_const arg)) in - idtac "In the context:"; print_context (); - fail 1 "Could not find bounds in the context for" arg - "when looking for a hypothesis of shape" shape - end - end. -Ltac find_reified_f_evar LHS := - lazymatch LHS with - | fst ?x => find_reified_f_evar x - | snd ?x => find_reified_f_evar x - | (?x, _) => find_reified_f_evar x - | map ?f ?x - => let dummy := match goal with - | _ => check_is_map_wordToZ 1 "In find_reified_f_evar, expected terms" f - end in - find_reified_f_evar x - | _ => LHS - end. -Ltac zrange_to_reflective_hyps_step_gen then_tac round_up := - lazymatch goal with - | [ H : @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (Tuple.map wordToZ ?arg) |- _ ] - => let rT := constr:(Syntax.tuple (Tbase TZ) count) in - let is_bounded_by' := constr:(@Bounds.is_bounded_by rT) in - let map' := constr:(@cast_back_flat_const (@Bounds.interp_base_type) rT (@Bounds.bounds_to_base_type round_up) bounds) in - (* we use [assert] and [abstract] rather than [change] to catch - inefficiencies in conversion early, rather than allowing - [Defined] to take forever *) - let H' := fresh H in - rename H into H'; - assert (H : is_bounded_by' bounds (map' arg)) by (clear -H'; abstract exact H'); - clear H'; move H at top; - then_tac () - | _ => idtac - end. -Ltac zrange_to_reflective_hyps_step := zrange_to_reflective_hyps_step_gen ltac:(fun _ => idtac). -Ltac zrange_to_reflective_hyps round_up := zrange_to_reflective_hyps_step_gen ltac:(fun _ => zrange_to_reflective_hyps round_up) round_up. -Ltac zrange_to_reflective_goal round_up Hbounded := - lazymatch goal with - | [ |- ?is_bounded_by_T /\ ?LHS = ?f ?Zargs ] - => let T := type of f in - let f_domain := lazymatch (eval hnf in T) with ?A -> ?B => A end in - let T := (eval compute in T) in - let rT := reify_type T in - let is_bounded_by' := constr:(@Bounds.is_bounded_by (codomain rT)) in - let output_bounds := bounds_from_is_bounded_by is_bounded_by_T in - pose_proof_bounded_from_Zargs_hyps Zargs Hbounded; - let input_bounds := lazymatch type of Hbounded with Bounds.is_bounded_by ?bounds _ => bounds end in - let map_t := constr:(fun t bs => @cast_back_flat_const (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) bs) in - let map_output := constr:(map_t (codomain rT) output_bounds) in - let map_input := constr:(map_t (domain rT) input_bounds) in - let args := unmap_wordToZ_tuple Zargs in - let reified_f_evar := find_reified_f_evar LHS in - let mapped_output := constr:(map_output reified_f_evar) in - let conjunct1 := constr:(is_bounded_by' output_bounds mapped_output) in - let conjunct2_rhs := constr:(f (map_input args)) in - let conjunct2 := constr:(mapped_output = conjunct2_rhs) in - (* we use [cut] and [abstract] rather than [change] to catch - inefficiencies in conversion early, rather than allowing - [Defined] to take forever *) - cut (conjunct1 /\ conjunct2); - [ generalize reified_f_evar; clear; clearbody f; clear; let x := fresh in intros ? x; abstract exact x - | ]; - cbv beta - end; - adjust_goal_for_reflective. -Ltac zrange_to_reflective round_up Hbounded := - zrange_to_reflective_hyps round_up; zrange_to_reflective_goal round_up Hbounded. - - -(** ** [round_up_from_allowable_bit_widths] *) -(** Construct a valid [round_up] function from allowable bit-widths *) -Ltac round_up_from_allowable_bit_widths allowable_bit_widths := - let allowable_lgsz := (eval compute in (List.map Nat.log2 allowable_bit_widths)) in - constr:(Bounds.round_up_to_in_list allowable_lgsz). - -(** ** [refine_to_reflective_glue] *) -(** The tactic [refine_to_reflective_glue] is the public-facing one; - it takes a goal of the form -<< -BoundedWordToZ ?f = F (BoundedWordToZ A) (BoundedWordToZ B) ... (BoundedWordToZ Z) ->> - where [?f] is an evar, and turns it into a goal the that - reflective automation pipeline can handle. *) -Ltac refine_to_reflective_glue' allowable_bit_widths Hbounded := - let round_up := round_up_from_allowable_bit_widths allowable_bit_widths in - preunfold_and_dlet_to_context (); - maybe_reassoc_sig_and_eexists (); - intros_under_and (); - do_curry_rhs (); - split_BoundedWordToZ (); - zrange_to_reflective round_up Hbounded. -Ltac refine_to_reflective_glue allowable_bit_widths := - let Hbounded := fresh "Hbounded" in - refine_to_reflective_glue' allowable_bit_widths Hbounded. diff --git a/src/Compilers/Z/Bounds/Pipeline/OutputType.v b/src/Compilers/Z/Bounds/Pipeline/OutputType.v deleted file mode 100644 index 028dd23a9..000000000 --- a/src/Compilers/Z/Bounds/Pipeline/OutputType.v +++ /dev/null @@ -1,52 +0,0 @@ -(** * Definition of the output type of the post-Wf pipeline *) -(** Do not change these definitions unless you're hacking on the - entire reflective pipeline tactic automation. *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. - -Section with_round_up_list. - Context {allowable_lgsz : list nat}. - - Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing). - Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). - - Record ProcessedReflectivePackage - := { InputType : _; - input_expr : Expr InputType; - input_bounds : interp_flat_type Bounds.interp_base_type (domain InputType); - output_bounds :> interp_flat_type Bounds.interp_base_type (codomain InputType); - output_expr :> Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) }. - - Definition Build_ProcessedReflectivePackage_from_option_sigma - {t} (e : Expr t) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - (result : option { output_bounds : interp_flat_type Bounds.interp_base_type (codomain t) - & Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) }) - : option ProcessedReflectivePackage - := option_map - (fun be - => let 'existT b e' := be in - {| InputType := t ; input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |}) - result. - - Definition ProcessedReflectivePackage_to_sigT (x : ProcessedReflectivePackage) - : { InputType : _ - & Expr InputType - * { bounds : interp_flat_type Bounds.interp_base_type (domain InputType) - * interp_flat_type Bounds.interp_base_type (codomain InputType) - & Expr (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type - := let (a, b, c, d, e) := x in - existT _ a (b, (existT _ (c, d) e)). -End with_round_up_list. - -Ltac inversion_ProcessedReflectivePackage := - repeat match goal with - | [ H : _ = _ :> ProcessedReflectivePackage |- _ ] - => apply (f_equal ProcessedReflectivePackage_to_sigT) in H; - cbv [ProcessedReflectivePackage_to_sigT] in H - end; - inversion_sigma; inversion_prod. diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v deleted file mode 100644 index 9193ea17f..000000000 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ /dev/null @@ -1,362 +0,0 @@ -(** * Reflective Pipeline: Tactics that execute the pipeline *) -(** N.B. This file should not need to be changed in normal - modifications of the reflective transformations; to modify the - transformations performed in the reflective pipeline; see - Pipeline/Definition.v. If the input format of the pre-reflective - goal changes, prefer adding complexity to Pipeline/Glue.v to - transform the goal and hypotheses into a uniform syntax to - modifying this file. This file will need to be modified if you - perform heavy changes in the shape of the generic or ℤ-specific - reflective machinery itself, or if you find bugs or slowness. *) -(** ** Preamble *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Intros. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.WfReflective. -Require Import Crypto.Compilers.RenameBinders. -Require Import Crypto.Compilers.Eta. -Require Import Crypto.Compilers.EtaInterp. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.Relax. -Require Import Crypto.Compilers.Reify. -Require Import Crypto.Compilers.Z.Reify. -Require Import Crypto.Compilers.InterpSideConditions. -Require Import Crypto.Compilers.Z.InterpSideConditions. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.SubstLet. -Require Import Crypto.Util.Tactics.UnfoldArg. -Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Util.Option. -Require Import bbv.WordScope. - -(** The final tactic in this file, [do_reflective_pipeline], takes a - goal of the form -<< -@Bounds.is_bounded_by (codomain T) bounds (fZ (cast_back_flat_const v)) - /\ cast_back_flat_const fW = fZ (cast_back_flat_const v) ->> - - where [fW] must be a context definition which is a single evar, - and all other terms must be evar-free. It fully solves the goal, - instantiating [fW] with an appropriately-unfolded - (reflection-definition-free) version of [fZ (cast_back_flat_const - v)] which has been transformed by the reflective pipeline. *) - -Module Export Exports. - Export Crypto.Compilers.Reify. (* export for the instances for recursing under binders *) - Export Crypto.Compilers.Z.Reify. (* export for the tactic redefinitions *) - Export Crypto.Compilers.Z.Bounds.Pipeline.Definition.Exports. -End Exports. - -(** ** Reification *) -(** The [do_reify] tactic handles goals of the form -<< -forall x, Interp _ ?e x = F ->> - by reifying [F]. *) -Ltac do_reify := - unfold_second_arg Tuple.tuple; - unfold_second_arg Tuple.tuple'; - cbv beta iota delta [Tuple.tuple Tuple.tuple'] in *; - cbv beta iota delta [Syntax.interp_flat_type Syntax.interp_base_type]; - reify_context_variables; - Reify_rhs; reflexivity. -(** ** Input Boundedness Side-Conditions *) -(** The tactic [handle_bounds_from_hyps] handles goals of the form -<< -Bounds.is_bounded_by (_, _, ..., _) _ ->> - by splitting them apart and looking in the context for hypotheses - that prove the bounds. *) -Ltac handle_bounds_from_hyps := - repeat match goal with - | _ => assumption - | [ |- cast_back_flat_const _ = cast_back_flat_const _ ] => reflexivity - | [ |- _ /\ _ ] => split - | [ |- Bounds.is_bounded_by (_, _) _ ] => split - end. -(** ** Unfolding [Interp] *) -(** The reduction strategies [interp_red], [extra_interp_red], and - [constant_simplification] (the latter two defined in - Pipeline/Definition.v) define the constants that get unfolded - before instantiating the original evar with [Interp _ - vm_computed_reified_expression arguments]. *) -Declare Reduction interp_red - := cbv [fst snd - Interp (*InterpEta interp_op*) interp interp_eta interpf interpf_step - interp_flat_type_eta interp_flat_type_eta_gen interp_flat_type - interp_base_type interp_op - SmartMap.SmartFlatTypeMap SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2 - SmartMap.smart_interp_flat_map - codomain domain - lift_op Zinterp_op cast_const - ZToInterp interpToZ - ]. - -(** ** Solving Side-Conditions of Equality *) -(** This section defines a number of different ways to solve goals of - the form [LHS = RHS] where [LHS] may contain evars and [RHS] must - not contain evars. Most tactics use [abstract] to reduce the load - on [Defined] and to catch looping behavior early. *) - -(** The tactic [unify_abstract_cbv_interp_rhs_reflexivity] runs the interpretation - reduction strategies in [RHS] and unifies the result with [LHS], - and does not use the vm (and hence does not fully reduce things, - which is important for efficiency). *) -Ltac unify_abstract_cbv_interp_rhs_reflexivity := - intros; clear; - lazymatch goal with - | [ |- ?LHS = ?RHS ] - => let RHS' := (eval interp_red in RHS) in - let RHS' := (eval extra_interp_red in RHS') in - let RHS' := lazymatch do_constant_simplification with - | true => (eval constant_simplification in RHS') - | _ => RHS' - end in - unify LHS RHS'; abstract exact_no_check (eq_refl RHS') - end. - -(** *** Boundedness Lemma Side Conditions *) -(** The tactic [handle_boundedness_side_condition] unfolds relevant - identifiers in the side-condition of the boundedness lemma. It - then calls [boundedness_side_condition_solver], which can be - overridden. *) -(** The tactic [boundedness_side_condition_solver] attempts to solve - the algebraic side conditions of the boundedness lemma; it leaves - them over if it cannot solve them. *) -Ltac boundedness_side_condition_solver := - repeat match goal with - | [ |- _ /\ _ ] => apply conj - | [ |- ?x = ?x ] => reflexivity - end; - try abstract ring. -Ltac handle_boundedness_side_condition := - post_intro_interp_flat_type_intros; - cbv [id - fst snd - InterpSideConditions Compilers.InterpSideConditions.InterpSideConditions interp_side_conditions interpf_side_conditions interpf_side_conditions_gen - Z.Syntax.Util.interped_op_side_conditions - ExprInversion.invert_Abs - Syntax.interp_op Syntax.lift_op - Syntax.Zinterp_op - SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartValf SmartMap.SmartFlatTypeMapInterp2 - Syntax.cast_const Syntax.ZToInterp Syntax.interpToZ]; - cbv [PointedProp.and_pointed_Prop PointedProp.to_prop]; - try match goal with - | [ |- True ] => exact I - end; - boundedness_side_condition_solver. - -(** ** Assemble the parts of Pipeline.Definition, in Gallina *) -(** In this section, we assemble [PreWfPipeline] and [PostWfPipeline], - and add extra equality hypotheses to minimize the work we have to - do in Ltac. *) -(** *** Gallina assembly imports *) -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.WfReflectiveGen. -Require Import Crypto.Compilers.WfReflective. -Require Import Crypto.Compilers.Eta. -Require Import Crypto.Compilers.EtaWf. -Require Import Crypto.Compilers.EtaInterp. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.OutputType. -Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Equality. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.Relax. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.PartiallyReifiedProp. -Require Import Crypto.Util.Equality. - -(** *** Gallina assembly *) -Section with_round_up_list. - Context {allowable_lgsz : list nat}. - - Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing). - Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). - - Context (opts : PipelineOptions) - {t : type base_type} - {input_bounds : interp_flat_type Bounds.interp_base_type (domain t)} - {given_output_bounds : interp_flat_type Bounds.interp_base_type (codomain t)} - {v' : interp_flat_type interp_base_type (pick_type input_bounds)} - {fZ : interp_flat_type interp_base_type (domain t) - -> interp_flat_type interp_base_type (codomain t)} - {final_e_evar : interp_flat_type interp_base_type (pick_type given_output_bounds)}. - - Class PipelineEvars := - { - b : interp_flat_type Bounds.interp_base_type (codomain t); - e' : Expr (pick_type input_bounds -> pick_type b); - e_final_newtype : Expr (pick_type input_bounds -> pick_type given_output_bounds); - e : Expr (domain t -> codomain t); - e_pre_pkg : Expr (domain t -> codomain t); - e_pkg : option (@ProcessedReflectivePackage allowable_lgsz) - }. - - Context (evars : PipelineEvars) - - (** ** reification *) - (rexpr_sig : { rexpr : Expr t | forall x, Interp rexpr x = fZ x }). - - Record PipelineSideConditions := - { - (** ** pre-wf pipeline *) - He : e = PreWfPipeline (proj1_sig rexpr_sig); - (** ** proving wf *) - He_unnatize_for_wf : forall var, unnatize_expr 0 (ExprEta' e (fun t => (nat * var t)%type)) = ExprEta' e _; - Hwf : forall var1 var2, - let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (ExprEta' e _) (ExprEta' e _)) in - trueify P = P; - (** ** post-wf-pre-bounds-pipeline *) - Hpost_wf_pre_bounds : e_pre_pkg = PostWfPreBoundsPipeline opts e; - (** ** post-wf-pipeline *) - Hpost : e_pkg = PostWfBoundsPipeline _ opts e e_pre_pkg input_bounds; - Hpost_correct : Some {| OutputType.input_expr := e ; OutputType.input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg; - (** ** bounds relaxation *) - Hbounds_relax : Bounds.is_tighter_thanb b given_output_bounds = true; - Hbounds_sane : pick_type given_output_bounds = pick_type b; - Hbounds_sane_refl - : e_final_newtype - = eq_rect _ (fun t => Expr (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane); - (** ** instantiation of original evar *) - Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v'; - (** ** side conditions (boundedness) *) - Hv1 : Bounds.is_bounded_by input_bounds (cast_back_flat_const v'); - Hv2 : intros_interp_flat_type_Prop (fun v => PointedProp.to_prop (InterpSideConditions e_pre_pkg v)); - }. - - Definition PipelineCorrect - (side_conditions : PipelineSideConditions) - : Bounds.is_bounded_by given_output_bounds (fZ (cast_back_flat_const v')) - /\ cast_back_flat_const final_e_evar = fZ (cast_back_flat_const v'). - Proof using All. - destruct side_conditions - as [He He_unnatize_for_wf Hwf Hpost_wf_pre_bounds Hpost Hpost_correct Hbounds_relax Hbounds_sane Hbounds_sane_refl Hevar Hv1 Hv2]. - cbv [b e' e_final_newtype e e_pre_pkg e_pkg] in *. - destruct evars as [b e' e_final_newtype e e_pre_pkg e_pkg]; - clear evars. - destruct rexpr_sig as [? Hrexpr]; clear rexpr_sig. - assert (Hwf' : Wf e) - by (apply (proj1 (@Wf_ExprEta'_iff _ _ _ e)); - eapply reflect_Wf; - [ .. | intros; split; [ eapply He_unnatize_for_wf | rewrite <- Hwf; apply trueify_true ] ]; - auto using base_type_eq_semidec_is_dec, op_beq_bl). - clear Hwf He_unnatize_for_wf. - symmetry in Hpost_correct. - subst; cbv [proj1_sig] in *. - rewrite eq_InterpEta, <- Hrexpr. - pose proof (introsP_interp_flat_type Hv2) as Hv2'. - eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ]. - rewrite !@InterpPreWfPipeline in Hpost_correct. - unshelve eapply relax_output_bounds; try eassumption; []. - match goal with - | [ |- context[Interp (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ] - => rewrite (@ap_transport A P _ x y pf (fun t e => Interp e v) k) - end. - rewrite <- transport_pp, concat_Vp; simpl. - apply Hpost_correct. - Qed. -End with_round_up_list. - -(** ** Assembling the Pipeline, in Ltac *) -(** The tactic [refine_with_pipeline_correct] uses the - [PipelineCorrect] lemma to create side-conditions. It assumes the - goal is in exactly the form given in the conclusion of the - [PipelineCorrect] lemma. *) -(** The [refine_PipelineSideConditions_constructor] subtactic splits - up the [PipelineSideConditions] record goal into multiple - subgoals, to be discharged by automation lower in this file - ([solve_post_reified_side_conditions]). *) -Ltac refine_PipelineSideConditions_constructor := - lazymatch goal with - | [ |- PipelineSideConditions ?opts ?evars _ ] - => simple refine {| Hevar := _ |}; - cbv [b e' e_final_newtype e e_pre_pkg e_pkg proj1_sig] - end. -Ltac refine_with_pipeline_correct opts := - lazymatch goal with - | [ |- _ /\ ?castback ?fW = ?fZ ?arg ] - => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ {| e_pkg := _ |}) in - simple refine (lem _ _); - subst fW fZ - end; - [ eexists - | refine_PipelineSideConditions_constructor ]. - -(** The tactic [solve_side_conditions] uses the above - reduction-and-proving-equality tactics to prove the - side-conditions of [PipelineCorrect]. The order must match with - [PipelineCorrect]. Which tactic to use was chosen in the - following way: - - - The default is [unify_abstract_vm_compute_rhs_reflexivity] - - - If the [RHS] is already in [vm_compute]d form, use - [unify_abstract_rhs_reflexivity] (saves a needless [vm_compute] which would be a - costly no-op) - - - If the proof needs to be transparent and there are no evars and - you want the user to see the fully [vm_compute]d term on error, - use [vm_compute; reflexivity] - - - If the user should see an unreduced term and you're proving [_ = - true], use [abstract vm_cast_no_check (eq_refl true)] - - - If you want to preserve binder names, use [unify_abstract_cbv_rhs_reflexivity] - - The other choices are tactics that are specialized to the specific - side-condition for which they are used (reification, boundedness - of input, reduction of [Interp], renaming). *) -Ltac solve_post_reified_side_conditions := - [> - (** ** pre-wf pipeline *) - unify_abstract_vm_compute_rhs_reflexivity | - (** ** reflective wf side-condition 1 *) - unify_abstract_vm_compute_rhs_reflexivity | - (** ** reflective wf side-condition 2 *) - unify_abstract_vm_compute_rhs_reflexivity | - (** ** post-wf-pre-bounds-pipeline *) - unify_abstract_vm_compute_rhs_reflexivity | - (** ** post-wf pipeline *) - unify_abstract_vm_compute_rhs_reflexivity | - (** ** post-wf pipeline gives [Some _] *) - unify_abstract_rhs_reflexivity | - (** ** computed output bounds are not looser than the given output bounds *) - (** we do subst and we don't [vm_compute] first because we want to - get an error message that displays the bounds *) - subst_let; clear; abstract vm_cast_no_check (eq_refl true) | - (** ** types computed from given output bounds are the same as types computed from computed output bounds *) - (** N.B. the proof must be exactly [eq_refl] because it's used in a - later goal and needs to reduce *) - subst_let; clear; vm_compute; reflexivity | - (** ** removal of a cast across the equality proof above *) - unify_abstract_compute_rhs_reflexivity | - (** ** unfolding of [interp] constants *) - unify_abstract_cbv_interp_rhs_reflexivity | - (** ** boundedness of inputs *) - abstract handle_bounds_from_hyps | - (** ** boundedness side-condition *) - handle_boundedness_side_condition ]. -Ltac solve_side_conditions := - [> - (** ** reification *) - do_reify | - .. ]; - solve_post_reified_side_conditions. - -(** ** The Entire Pipeline *) -(** The [do_reflective_pipeline] tactic solves a goal of the form that - is described at the top of this file, and is the public interface - of this file. *) -Ltac do_reflective_pipeline opts := - refine_with_pipeline_correct opts; solve_side_conditions. -Notation default_PipelineOptions := default_PipelineOptions. diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v deleted file mode 100644 index 8178592ed..000000000 --- a/src/Compilers/Z/Bounds/Relax.v +++ /dev/null @@ -1,135 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Arith.Arith. -Require Import Coq.Classes.Morphisms. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Equality. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.RoundUpLemmas. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.Bool. - -Local Lemma helper logsz v - : (v < 2 ^ 2 ^ Z.of_nat logsz)%Z <-> (Z.to_nat (Z.log2_up (Z.log2_up (1 + v))) <= logsz)%nat. -Proof. - rewrite Nat2Z.inj_le, Z2Nat.id by auto with zarith. - transitivity (1 + v <= 2^2^Z.of_nat logsz)%Z; [ omega | ]. - rewrite !Z.log2_up_le_pow2_full by auto with zarith. - reflexivity. -Qed. - -Local Arguments Z.pow : simpl never. -Local Arguments Z.sub !_ !_. -Local Arguments Z.add !_ !_. -Local Arguments Z.mul !_ !_. -Lemma relax_output_bounds' - round_up - t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t) - (Hv : SmartFlatTypeMap (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds - = SmartFlatTypeMap (@Bounds.bounds_to_base_type round_up) tight_output_bounds) - v k - (v' := eq_rect _ (interp_flat_type _) v _ Hv) - (Htighter : @Bounds.is_bounded_by - t tight_output_bounds - (@cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) tight_output_bounds - v') - /\ @cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) tight_output_bounds - v' - = k) - (Hrelax : Bounds.is_tighter_thanb tight_output_bounds relaxed_output_bounds = true) - : @Bounds.is_bounded_by - t relaxed_output_bounds - (@cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds - v) - /\ @cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds - v - = k. -Proof. - destruct Htighter as [H0 H1]; subst v' k. - cbv [Bounds.is_bounded_by cast_back_flat_const Bounds.is_tighter_thanb] in *. - apply interp_flat_type_rel_pointwise_iff_relb in Hrelax. - induction t; unfold SmartFlatTypeMap in *; simpl @smart_interp_flat_map in *; inversion_flat_type. - { cbv [Bounds.is_tighter_thanb' Bounds.bounds_to_base_type ZRange.is_tighter_than_bool is_true SmartFlatTypeMap ZRange.is_bounded_by' Bounds.smallest_logsz ZRange.is_bounded_by Bounds.is_bounded_by' Bounds.bit_width_of_base_type] in *; simpl in *; - repeat first [ progress inversion_flat_type - | progress inversion_base_type_constr - | progress subst - | progress destruct_head bounds - | progress destruct_head base_type - | progress split_andb - | progress Z.ltb_to_lt - | progress break_match_hyps - | progress destruct_head'_and - | progress simpl in * - | rewrite helper in * - | omega - | tauto - | congruence - | progress destruct_head @eq; (reflexivity || omega) - | progress break_innermost_match_step - | apply conj ]. } - { compute in *; tauto. } - { simpl in *. - specialize (fun Hv => IHt1 (fst tight_output_bounds) (fst relaxed_output_bounds) Hv (fst v)). - specialize (fun Hv => IHt2 (snd tight_output_bounds) (snd relaxed_output_bounds) Hv (snd v)). - do 2 match goal with - | [ H : _ = _, H' : forall x, _ |- _ ] => specialize (H' H) - end. - simpl in *. - split_and. - repeat apply conj; - [ match goal with H : _ |- _ => apply H end.. - | apply (f_equal2 (@pair _ _)); (etransitivity; [ match goal with H : _ |- _ => apply H end | ]) ]; - repeat first [ progress destruct_head prod - | progress simpl in * - | reflexivity - | assumption - | match goal with - | [ |- ?P (eq_rect _ _ _ _ _) = ?P _ ] - => apply f_equal; clear - | [ H : interp_flat_type_rel_pointwise (@Bounds.is_bounded_by') ?x ?y |- interp_flat_type_rel_pointwise (@Bounds.is_bounded_by') ?x ?y' ] - => clear -H; - match goal with |- ?R _ _ => generalize dependent R; intros end - | [ H : ?x = ?y |- _ ] - => first [ generalize dependent x | generalize dependent y ]; - let k := fresh in intro k; intros; subst k - end ]. } -Qed. - -Lemma relax_output_bounds - round_up - t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t) - (Hv : SmartFlatTypeMap (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds - = SmartFlatTypeMap (@Bounds.bounds_to_base_type round_up) tight_output_bounds) - v k - (v' := eq_rect _ (interp_flat_type _) v _ Hv) - (Htighter : @Bounds.is_bounded_by t tight_output_bounds k - /\ @cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) tight_output_bounds - v' - = k) - (Hrelax : Bounds.is_tighter_thanb tight_output_bounds relaxed_output_bounds = true) - : @Bounds.is_bounded_by t relaxed_output_bounds k - /\ @cast_back_flat_const - (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds - v - = k. -Proof. - pose proof (fun pf => @relax_output_bounds' round_up t tight_output_bounds relaxed_output_bounds Hv v k (conj pf (proj2 Htighter)) Hrelax) as H. - destruct H as [H1 H2]; [ | rewrite <- H2; tauto ]. - subst v'. - destruct Htighter; subst k; assumption. -Qed. diff --git a/src/Compilers/Z/Bounds/RoundUpLemmas.v b/src/Compilers/Z/Bounds/RoundUpLemmas.v deleted file mode 100644 index ce4ea9373..000000000 --- a/src/Compilers/Z/Bounds/RoundUpLemmas.v +++ /dev/null @@ -1,34 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.NatUtil. - -Notation round_up_monotone_T round_up - := (forall x y, - (x <= y)%nat - -> match round_up x, round_up y with - | Some x', Some y' => (x' <= y')%nat - | None, None => True - | Some _, None => True - | None, Some _ => False - end) - (only parsing). - -Lemma round_up_to_in_list_monotone (allowable_lgsz : list nat) - : round_up_monotone_T (Bounds.round_up_to_in_list allowable_lgsz). -Proof. - intros x y H. - induction allowable_lgsz as [|s ss]. - { constructor. } - { unfold Bounds.round_up_to_in_list in *. - repeat match goal with - | _ => solve [ trivial ] - | _ => progress simpl in * - | _ => progress break_innermost_match_step - | _ => progress break_innermost_match_hyps_step - | [ H : ?leb _ _ = true |- _ ] => apply NPeano.Nat.leb_le in H - | [ H : ?leb _ _ = false |- _ ] => apply NPeano.Nat.leb_gt in H - | _ => omega * - end. } -Qed. |