diff options
Diffstat (limited to 'src/Compilers/Z/Bounds')
| -rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 177 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas.v | 433 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijn.v | 23 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | 25 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v | 41 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 20 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 177 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Glue.v | 456 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/OutputType.v | 51 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 288 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Relax.v | 127 |
11 files changed, 1818 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v new file mode 100644 index 000000000..b9880f097 --- /dev/null +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -0,0 +1,177 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Relations. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZRange. +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. + Section with_bitwidth. + Context (bit_width : option Z). + Definition four_corners (f : Z -> Z -> Z) : t -> t -> t + := fun x y + => let (lx, ux) := x in + let (ly, uy) := y in + {| lower := Z.min (f lx ly) (Z.min (f lx uy) (Z.min (f ux ly) (f ux uy))); + upper := Z.max (f lx ly) (Z.max (f lx uy) (Z.max (f ux ly) (f ux uy))) |}. + Definition two_corners (f : Z -> Z) : t -> t + := fun x + => let (lx, ux) := x in + {| lower := Z.min (f lx) (f ux); + upper := Z.max (f lx) (f ux) |}. + Definition truncation_bounds (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 BuildTruncated_bounds (l u : Z) : t + := truncation_bounds {| lower := l ; upper := u |}. + Definition t_map1 (f : Z -> Z) (x : t) + := truncation_bounds (two_corners f x). + Definition t_map2 (f : Z -> Z -> Z) : t -> t -> t + := fun x y => truncation_bounds (four_corners f x y). + Definition t_map4 (f : bounds -> bounds -> bounds -> bounds -> bounds) (x y z w : t) + := truncation_bounds (f x y z w). + 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 extreme_lor_land_bounds (x y : t) : t + := let (lx, ux) := x in + let (ly, uy) := y in + let lx := Z.abs lx in + let ly := Z.abs ly in + let ux := Z.abs ux in + let uy := Z.abs uy in + let max := Z.max (Z.max lx ly) (Z.max ux uy) in + {| lower := -2^(1 + Z.log2_up max) ; upper := 2^(1 + Z.log2_up max) |}. + Definition extermization_bounds (f : t -> t -> t) (x y : t) : t + := truncation_bounds + (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 + := extermization_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 + := extermization_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 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 neg (int_width : Z) : t -> t + := fun v + => truncation_bounds (neg' int_width v). + 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 + := truncation_bounds (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 + := truncation_bounds (cmovle' r1 r2). + End with_bitwidth. + + 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 interp_base_type (ty : base_type) : Set := t. + + Definition bit_width_of_base_type ty : option Z + := match ty with + | TZ => None + | TWord logsz => Some (2^Z.of_nat logsz)%Z + end. + + Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst + := 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 _ => BuildTruncated_bounds (bit_width_of_base_type T) v v + | Add _ _ T => fun xy => add (bit_width_of_base_type T) (fst xy) (snd xy) + | Sub _ _ T => fun xy => sub (bit_width_of_base_type T) (fst xy) (snd xy) + | Mul _ _ T => fun xy => mul (bit_width_of_base_type T) (fst xy) (snd xy) + | Shl _ _ T => fun xy => shl (bit_width_of_base_type T) (fst xy) (snd xy) + | Shr _ _ T => fun xy => shr (bit_width_of_base_type T) (fst xy) (snd xy) + | Land _ _ T => fun xy => land (bit_width_of_base_type T) (fst xy) (snd xy) + | Lor _ _ T => fun xy => lor (bit_width_of_base_type T) (fst xy) (snd xy) + | Opp _ T => fun x => opp (bit_width_of_base_type T) x + end%bounds. + + 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 bounds_to_base_type (b : t) : base_type + := if (0 <=? lower b)%Z + then TWord (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) + else TZ. + + Definition ComputeBounds {t} (e : Expr base_type op t) + (input_bounds : interp_flat_type interp_base_type (domain t)) + : interp_flat_type interp_base_type (codomain t) + := 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 {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.v b/src/Compilers/Z/Bounds/InterpretationLemmas.v new file mode 100644 index 000000000..7a1c2bc73 --- /dev/null +++ b/src/Compilers/Z/Bounds/InterpretationLemmas.v @@ -0,0 +1,433 @@ +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.SmartMap. +Require Import Crypto.Util.ZUtil. +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. + +Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing). +Local Notation pick_type v := (SmartFlatTypeMap (fun _ => pick_typeb) v). + +Local Open Scope Z_scope. + +Local Ltac break_t_step := + first [ progress destruct_head'_and + | progress destruct_head'_or + | progress destruct_head'_prod + | progress split_andb + | break_innermost_match_step ]. + +Local 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 ]. + +Local Ltac specializer_t_step := + first [ progress specialize_by_assumption + | progress specialize_by fin_t ]. + +Local 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 ]. +Local 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. +Local 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. + +Local Ltac revert_min_max := + repeat match goal with + | [ H : context[Z.min _ _] |- _ ] => revert H + | [ H : context[Z.max _ _] |- _ ] => revert H + end. +Local Ltac split_min_max := + repeat match goal with + | [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ] + => rewrite (Z.max_r a b) by omega + | [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ] + => rewrite (Z.max_l a b) by omega + | [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ] + => rewrite (Z.min_l a b) by omega + | [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ] + => rewrite (Z.min_r a b) by omega + | [ |- context[Z.max ?a ?b] ] + => first [ rewrite (Z.max_l a b) by omega + | rewrite (Z.max_r a b) by omega ] + | [ |- context[Z.min ?a ?b] ] + => first [ rewrite (Z.min_l a b) by omega + | rewrite (Z.min_r a b) by omega ] + | _ => revert_min_max; progress repeat apply Z.min_case_strong; intros + | _ => revert_min_max; progress repeat apply Z.max_case_strong; intros + end. + +Local 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. +Local Ltac case_Zvar_nonneg_step := + match goal with + | [ |- context[?x] ] + => case_Zvar_nonneg_on x + end. +Local Ltac case_Zvar_nonneg := repeat case_Zvar_nonneg_step. + +Local 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. + +Local 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 >> ?x'] ] + => unique assert (x >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) + | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?y'] ] + => unique assert (x >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) + end. +Local 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 >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) + end. +Local 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. +Local Ltac clean_neg := + repeat match goal with + | [ H : (-?x) < 0 |- _ ] => assert (0 <= x) by omega; assert (x <> 0) by omega; clear H + | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H + | [ |- -?x <= -?y ] => apply Z.opp_le_mono + | _ => progress rewrite <- Z.opp_le_mono in * + end. +Local Ltac replace_with_neg x := + assert (x = -(-x)) by omega; generalize dependent (-x); + let x' := fresh in + rename x into x'; intro x; intros; subst x'; + clean_neg. +Local Ltac replace_all_neg_with_pos := + repeat match goal with + | [ H : ?x < 0 |- _ ] => replace_with_neg x + end. +Local Ltac handle_shift_neg := + repeat first [ rewrite !Z.shiftr_opp_r + | rewrite !Z.shiftl_opp_r ]. + +Local Ltac handle_four_corners_step_fast := + first [ progress destruct_head Bounds.t + | progress cbv [Bounds.four_corners] in * + | progress subst + | Zarith_t_step + | progress split_min_max + | omega + | nia ]. +Local Ltac handle_four_corners_step := + first [ handle_four_corners_step_fast + | remove_binary_operation_le_hyps_step ]. +Local Ltac handle_four_corners := + lazymatch goal with + | [ |- (ZRange.lower (Bounds.four_corners _ _ _) <= _ <= _)%Z ] + => idtac + end; + repeat handle_four_corners_step. + +Local 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 ]. + +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 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. + +Local Arguments Z.pow : simpl never. +Local Arguments Z.add !_ !_. +Local Existing Instances Z.add_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper. +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) + : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v). +Proof. + destruct opc; apply is_bounded_by_truncation_bounds; + repeat first [ progress simpl in * + | progress cbv [interp_op lift_op cast_const 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 ]. + { handle_four_corners. } + { handle_four_corners. } + { handle_four_corners. } + { destruct_head Bounds.t. + case_Zvar_nonneg; replace_all_neg_with_pos; handle_shift_neg; + autorewrite with Zshift_to_pow; + rewrite ?Z.div_opp_l_complete by auto with zarith; + autorewrite with Zpow_to_shift. + 16:split_min_max; saturate_with_shift_facts; omega. + all:admit. } + { destruct_head Bounds.t. + case_Zvar_nonneg; replace_all_neg_with_pos; handle_shift_neg; admit. } + { repeat first [ progress destruct_head Bounds.t + | progress simpl in * + | break_t_step + | Zarith_t_step + | rewriter_t + | progress replace_all_neg_with_pos + | progress saturate_land_lor_facts + | split_min_max; omega ]; + admit. } + { repeat first [ progress destruct_head Bounds.t + | progress simpl in * + | break_t_step + | Zarith_t_step + | rewriter_t + | progress replace_all_neg_with_pos + | progress saturate_land_lor_facts + | progress Zarith_land_lor_t_step + | solve [ split_min_max; try omega; try Zarith_land_lor_t_step ] ]; + admit. } + { repeat first [ progress destruct_head Bounds.t + | progress simpl in * + | progress split_min_max + | omega ]. } +Admitted. + +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 Instance Z.pow_Zpos_le_Proper. +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)) + : 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); clear opc; simpl; intros. + revert dependent t; induction tR as [tR| |]; intros; + [ + | repeat first [ match goal with + | [ |- ?x = ?y ] + => transitivity tt; destruct x, y; reflexivity + end + | reflexivity + | progress simpl @Bounds.is_bounded_by in * + | rewrite !lift_op_prod_dst + | rewrite !cast_back_flat_const_prod + | progress split_and + | match goal with + | [ H : _ |- _ ] => first [ setoid_rewrite lift_op_prod_dst in H + | setoid_rewrite cast_back_flat_const_prod in H ] + end + | setoid_rewrite lift_op_prod_dst + | match goal with + | [ H : _ |- _ ] => erewrite H by eassumption + end ].. ]. + revert dependent tR; induction t as [t| |]; intros; + [ + | repeat first [ match goal with + | [ |- ?x = ?y ] + => transitivity tt; destruct x, y; reflexivity + end + | reflexivity + | progress simpl @Bounds.is_bounded_by in * + | rewrite !lift_op_prod_dst + | rewrite !cast_back_flat_const_prod + | progress split_and + | match goal with + | [ H : _ |- _ ] => first [ setoid_rewrite lift_op_prod_dst in H + | setoid_rewrite cast_back_flat_const_prod in H ] + end + | setoid_rewrite lift_op_prod_dst + | match goal with + | [ H : _ |- _ ] => erewrite H by eassumption + end ].. ]. + { simpl in *; unfold unzify_op, cast_back_flat_const, SmartFlatTypeMap, Bounds.interp_base_type, cast_const, Bounds.is_bounded_by', lift_op, SmartFlatTypeMapUnInterp, SmartFlatTypeMapInterp2, cast_const in *; simpl in *. + unfold Bounds.is_bounded_by', cast_const, ZToInterp, interpToZ, Bounds.bounds_to_base_type, ZRange.is_bounded_by' in *; simpl in *. + destruct_head base_type; break_innermost_match; Z.ltb_to_lt; destruct_head Bounds.t; + repeat match goal with + | _ => progress destruct_head'_and + | _ => reflexivity + | [ H : forall v, _ /\ True -> _ |- _ ] => specialize (fun v pf => H v (conj pf I)) + | [ H : forall v, _ -> _ /\ True |- _ ] => pose proof (fun v pf => proj1 (H v pf)); clear H + | [ H : True |- _ ] => clear H + | [ H : ?T, H' : ?T |- _ ] => clear H + | [ H : forall v, _ -> _ <= ?f v <= _ |- ?f ?v' = _ ] + => specialize (H v') + | [ H : forall v, _ -> _ <= ?f (?g v) <= _ |- ?f (?g ?v') = _ ] + => specialize (H v') + | [ H : forall v, _ -> _ <= ?f (?g (?h v)) <= _ /\ _ /\ _ |- context[?h ?v'] ] + => specialize (H v') + | [ H : forall v, _ -> _ <= ?f (?g (?h (?i v))) <= _ /\ _ /\ _ |- context[?h (?i ?v')] ] + => specialize (H v') + | _ => progress specialize_by omega + | _ => rewrite wordToZ_ZToWord + by repeat match goal with + | [ |- and _ _ ] => split + | [ |- ?x < ?y ] => cut (1 + x <= y); [ omega | ] + | _ => omega + | _ => progress autorewrite with push_Zof_nat zsimplify_const + | _ => rewrite Z2Nat.id by auto with zarith + | _ => rewrite <- !Z.log2_up_le_full + end + | _ => rewrite wordToZ_ZToWord in * + by repeat match goal with + | [ |- and _ _ ] => split + | [ |- ?x < ?y ] => cut (1 + x <= y); [ omega | ] + | _ => omega + | _ => progress autorewrite with push_Zof_nat zsimplify_const + | _ => rewrite Z2Nat.id by auto with zarith + | _ => rewrite <- !Z.log2_up_le_full + end + | _ => rewrite wordToZ_ZToWord_wordToZ + by (rewrite Nat2Z.inj_le, Z2Nat.id, <- !Z.log2_up_le_pow2_full by auto with zarith; omega) + | _ => rewrite wordToZ_ZToWord_wordToZ in * + by (rewrite Nat2Z.inj_le, Z2Nat.id, <- !Z.log2_up_le_pow2_full by auto with zarith; omega) + end. + all:admit. } + { simpl in *. + specialize (H0 tt I). + simpl in *. + hnf in H0. + unfold cast_back_flat_const, lift_op, unzify_op in *; simpl in *. + unfold interpToZ in *. + unfold Bounds.bounds_to_base_type in *. + destruct_head base_type; simpl in *. + split_andb. + Z.ltb_to_lt. + all:destruct_head' and. + all:simpl in *. + all:break_innermost_match; break_match_hyps; split_andb; Z.ltb_to_lt; try reflexivity. + all:try (simpl in *; + rewrite wordToZ_ZToWord + by (autorewrite with push_Zof_nat zsimplify_const; + rewrite Z2Nat.id by auto with zarith; + split; try omega; + match goal with + | [ |- (?x < ?y)%Z ] + => apply (Z.lt_le_trans x (x + 1) y); [ omega | ] + end; + rewrite <- !Z.log2_up_le_full; + omega)). + all:try reflexivity. + unfold interpToZ, cast_const. + simpl. + rewrite ZToWord_wordToZ_ZToWord; [ reflexivity | ]. + apply Nat2Z.inj_le. + rewrite Z2Nat.id by auto with zarith. + +Admitted. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v new file mode 100644 index 000000000..45b084566 --- /dev/null +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v @@ -0,0 +1,23 @@ +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 {t : type base_type}. + + Definition MapCastCompile := @MapCastCompile t. + Definition MapCastDoCast + := @MapCastDoCast + (@Bounds.interp_base_type) (@Bounds.interp_op) + (fun _ => @Bounds.bounds_to_base_type) + (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) + t. + Definition MapCastDoInterp + := @MapCastDoInterp + (@Bounds.interp_base_type) (fun _ => @Bounds.bounds_to_base_type) + 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 new file mode 100644 index 000000000..46f472311 --- /dev/null +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v @@ -0,0 +1,25 @@ +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.Bounds.Interpretation. +Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas. +Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. + +Lemma MapCastCorrect + {t} (e : Expr base_type op t) + (Hwf : Wf e) + (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) + : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')) + v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v), + Interp (@Bounds.interp_op) e input_bounds = b + /\ Bounds.is_bounded_by b (Interp interp_op e v) + /\ cast_back_flat_const (Interp interp_op e' v') = (Interp interp_op e v). +Proof. + apply MapCastCorrect; auto. + { apply is_bounded_by_interp_op. } + { apply pull_cast_genericize_op. } +Qed. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v new file mode 100644 index 000000000..04d1f964e --- /dev/null +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v @@ -0,0 +1,41 @@ +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.InterpretationLemmas. +Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. + +Definition Wf_MapCast + {t} (e : Expr base_type op t) + (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) + {b} e' (He' : MapCast e input_bounds = Some (existT _ b e')) + (Hwf : Wf e) + : Wf e' + := @Wf_MapCast + (@Bounds.interp_base_type) (@Bounds.interp_op) + (fun _ => @Bounds.bounds_to_base_type) + (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) + t e input_bounds b e' He' Hwf. + +Definition Wf_MapCast_arrow + {s d} (e : Expr base_type op (Arrow s d)) + (input_bounds : interp_flat_type Bounds.interp_base_type s) + {b} e' (He' : MapCast e input_bounds = Some (existT _ b e')) + (Hwf : Wf e) + : Wf e' + := @Wf_MapCast_arrow + (@Bounds.interp_base_type) (@Bounds.interp_op) + (fun _ => @Bounds.bounds_to_base_type) + (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 new file mode 100644 index 000000000..6c9cda840 --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -0,0 +1,20 @@ +(** * Reflective Pipeline *) +Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue. +Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics. +(** 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. +End Exports. + +Ltac refine_reflectively := + refine_to_reflective_glue; + do_reflective_pipeline. diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v new file mode 100644 index 000000000..ae3401b78 --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -0,0 +1,177 @@ +(** * 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.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 base_type op t) : Expr base_type op _ + := ExprEta (SimplifyArith 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 base_type op t) + : forall x, Interp interp_op (PreWfPipeline e) x = Interp interp_op 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.Bounds.MapCastByDeBruijn. +Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp. +Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf. +Require Import Crypto.Util.Sigma.MapProjections. + +(** *** Definition of the Post-Wf Pipeline *) +(** Do not change the name or the type of this definition *) +Definition PostWfPipeline + {t} (e : Expr base_type op t) + (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) + : option ProcessedReflectivePackage + := Build_ProcessedReflectivePackage_from_option_sigma + e input_bounds + (let e := Linearize e in + let e := InlineConst e in + let e := MapCast e input_bounds in + option_map + (projT2_map + (fun b e' + => let e' := InlineConst e' in + let e' := ExprEta e' in + e')) + e). + +(** *** Correctness proof of the Pre-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.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. + +Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing). +Local Notation pick_type v := (SmartFlatTypeMap (fun _ => pick_typeb) v). +Definition PostWfPipelineCorrect + {t} + (e : Expr base_type op t) + (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) + (Hwf : Wf e) + {b e'} (He : PostWfPipeline 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) + : Interp (@Bounds.interp_op) e input_bounds = b + /\ Bounds.is_bounded_by b (Interp interp_op e v) + /\ cast_back_flat_const (Interp interp_op e' v') = Interp interp_op e v. +Proof. + (** These first two lines probably shouldn't change much *) + unfold PostWfPipeline, 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 *) + rewrite InterpExprEta_arrow, InterpInlineConst + by eauto with wf. + (** Now handle all the transformations that come before the word-size selection *) + rewrite <- !InterpLinearize with (e:=e), <- !(@InterpInlineConst _ _ _ (Linearize e)) + by eauto with wf. + (** Now handle word-size selection itself *) + eapply MapCastCorrect; eauto with wf. +Qed. + + +(** ** 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 Bedrock.Word. + +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 new file mode 100644 index 000000000..5aa22e106 --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline/Glue.v @@ -0,0 +1,456 @@ +(** * 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.Tactics.EvarExists. +Require Import Crypto.Util.Tactics.GetGoal. +Require Import Crypto.Util.Tactics.PrintContext. +Require Import Crypto.Util.Tactics.MoveLetIn. + +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 [sig_dlet_in_rhs_to_context_curried] moves to the + context any [dlet x := y in ...] on the rhs of a goal of the form + [{ a | lhs = rhs }], curries each such moved definition, and then + reifies the type of each such context variable. *) +Ltac sig_dlet_in_rhs_to_context_curried := + lazymatch goal with + | [ |- { a | _ = @Let_In ?A ?B ?x _ } ] + => let f := fresh in + sig_dlet_in_rhs_to_context_step f; + change_with_curried f; + change_to_reified_type f; + sig_dlet_in_rhs_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]; + sig_dlet_in_rhs_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; pattern (proj1_sig a); + lazymatch goal with + | [ |- ?P ?p1a ] + => cut (dlet p := P in p p1a); + [ clear; 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 unfold [BoundedWordToZ] + and move any [dlet x := ... in ...] to context variables, and then + take a goal 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 +>> + *) +Ltac reassoc_sig_and_eexists := + preunfold_and_dlet_to_context; + pattern_sig_sig_assoc; + evar_exists. + + +(** ** [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:(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_bounded_by_shape subterm_type := + lazymatch subterm_type with + | ZRange.is_bounded_by None ?bounds (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 (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 + | map wordToZ ?fW + => 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:(map wordToZ ?fW) 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 + "but a subterm not matching this shape was found:" subterm + end. +Ltac check_RHS_Z_shape_rec subterm := + lazymatch subterm with + | map wordToZ ?fW + => idtac + | (?A, ?B) + => check_RHS_Z_shape_rec A; + check_RHS_Z_shape_rec B + | _ => let G := get_goal in + let shape := uconstr:(map wordToZ ?fW) 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 + "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:(map wordToZ ?fW) 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 + "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; + repeat match goal with + | [ |- context[map wordToZ (proj1_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 ] + | [ H := context[map wordToZ (proj1_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 ] + | [ |- context[fst ?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); + change (snd x) with (let (a, b) := x in b); + instantiate (1:=ltac:(destruct x)); destruct x ]; + cbv beta iota + 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')) + | map wordToZ ?x => 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 wordToZ ?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 wordToZ ?x => find_reified_f_evar x + | _ => LHS + end. +Ltac zrange_to_reflective_hyps_step := + match 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 (fun _ => Bounds.bounds_to_base_type) 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 + | [ H := context Hv[@Tuple.map ?a ?b ?c (@wordToZ ?d) ?x], Hbounded : Bounds.is_bounded_by ?bounds (cast_back_flat_const ?x) |- _ ] + => let T := type of (@Tuple.map a b c (@wordToZ d) x) in + let T := (eval compute in T) in + let rT := reify_flat_type T in + let map_t := constr:(fun t bs => @cast_back_flat_const (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) bs) in + let map' := constr:(map_t rT bounds) in + let Hv' := context Hv[map' x] in + progress change Hv' in (value of H); cbv beta in H + end. +Ltac zrange_to_reflective_hyps := repeat zrange_to_reflective_hyps_step. +Ltac zrange_to_reflective_goal 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 (fun _ => Bounds.bounds_to_base_type) 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 + (* we use [cut] and [abstract] rather than [change] to catch + inefficiencies in conversion early, rather than allowing + [Defined] to take forever *) + cut (is_bounded_by' output_bounds (map_output reified_f_evar) /\ map_output reified_f_evar = f (map_input args)); + [ 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 Hbounded := zrange_to_reflective_hyps; zrange_to_reflective_goal Hbounded. + +(** ** [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' Hbounded := + reassoc_sig_and_eexists; + do_curry_rhs; + split_BoundedWordToZ; + zrange_to_reflective Hbounded. +Ltac refine_to_reflective_glue := + let Hbounded := fresh "Hbounded" in + refine_to_reflective_glue' Hbounded. diff --git a/src/Compilers/Z/Bounds/Pipeline/OutputType.v b/src/Compilers/Z/Bounds/Pipeline/OutputType.v new file mode 100644 index 000000000..8205ef70c --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline/OutputType.v @@ -0,0 +1,51 @@ +(** * 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. +Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing). +Local Notation pick_type v := (SmartFlatTypeMap (fun _ => pick_typeb) v). + +Record ProcessedReflectivePackage + := { InputType : _; + input_expr : Expr base_type op 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 base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }. + +Notation OutputType pkg + := (Arrow (pick_type (@input_bounds pkg)) (pick_type (@output_bounds pkg))) + (only parsing). + +Definition Build_ProcessedReflectivePackage_from_option_sigma + {t} (e : Expr base_type op 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 base_type op (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 base_type op InputType + * { bounds : interp_flat_type Bounds.interp_base_type (domain InputType) + * interp_flat_type Bounds.interp_base_type (codomain InputType) + & Expr base_type op (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)). + +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 new file mode 100644 index 000000000..3586cc78d --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -0,0 +1,288 @@ +(** * 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.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.Z.Bounds.Pipeline.Definition. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SubstLet. +Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. +Require Import Crypto.Util.FixedWordSizes. +Require Import Crypto.Util.Option. +Require Import Bedrock.Word. + +(** 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 := + 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_renamify_rhs_reflexivity] calls [renamify] on [RHS] and unifies + that with [LHS]; and then costs one [vm_compute] to prove the + equality. *) +Ltac unify_abstract_renamify_rhs_reflexivity := + unify_transformed_rhs_abstract_tac + ltac:(renamify) + unify_tac + vm_cast_no_check. +(** 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. + + +(** ** 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.PartiallyReifiedProp. +Require Import Crypto.Util.Equality. + +(** *** Gallina assembly *) +Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing). +Local Notation pick_type v := (SmartFlatTypeMap (fun _ => pick_typeb) v). +Definition PipelineCorrect + {t} + {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 Syntax.interp_base_type (pick_type input_bounds)} + {b e' e_final e_final_newtype} + {fZ} + {final_e_evar : interp_flat_type Syntax.interp_base_type (pick_type given_output_bounds)} + {e} + {e_pkg} + (** ** reification *) + (rexpr_sig : { rexpr : Expr base_type op t | forall x, Interp Syntax.interp_op rexpr x = fZ x }) + (** ** 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-pipeline *) + (Hpost : e_pkg = PostWfPipeline e input_bounds) + (Hpost_correct : Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg) + (** ** renaming *) + (Hrenaming : e_final = e') + (** ** bounds relaxation *) + (Hbounds_sane : pick_type given_output_bounds = pick_type b) + (Hbounds_relax : Bounds.is_tighter_thanb b given_output_bounds = true) + (Hbounds_sane_refl + : e_final_newtype + = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane)) + (** ** instantiation of original evar *) + (Hevar : final_e_evar = Interp (t:=Arrow _ _) Syntax.interp_op e_final_newtype v') + (** ** side condition *) + (Hv : Bounds.is_bounded_by input_bounds (cast_back_flat_const v')) + : 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. + destruct rexpr_sig as [? Hrexpr]. + 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 <- Hrexpr. + 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 interp_op e v) k) + end. + rewrite <- transport_pp, concat_Vp; simpl. + apply Hpost_correct. +Qed. + + +(** ** 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. *) +Ltac refine_with_pipeline_correct := + lazymatch goal with + | [ |- _ /\ ?castback ?fW = ?fZ ?arg ] + => let lem := open_constr:(@PipelineCorrect _ _ _ _ _ _ _ _ _ _ _ _) in + simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _); + subst fW fZ + end; + [ eexists + | cbv [proj1_sig].. ]. + +(** 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_side_conditions := + [> + (** ** reification *) + do_reify | + (** ** 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 pipeline *) + unify_abstract_vm_compute_rhs_reflexivity | + (** ** post-wf pipeline gives [Some _] *) + unify_abstract_rhs_reflexivity | + (** ** renaming binders *) + unify_abstract_renamify_rhs_reflexivity | + (** ** 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 | + (** ** 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) | + (** ** 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 ]. + + +(** ** 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 := + refine_with_pipeline_correct; solve_side_conditions. diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v new file mode 100644 index 000000000..40b678071 --- /dev/null +++ b/src/Compilers/Z/Bounds/Relax.v @@ -0,0 +1,127 @@ +Require Import Coq.ZArith.ZArith. +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.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.ZUtil. +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' + t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t) + (Hv : SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + = SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) 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 (fun _ => Bounds.bounds_to_base_type) tight_output_bounds + v') + /\ @cast_back_flat_const + (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) 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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + v) + /\ @cast_back_flat_const + (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) 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' ZRange.is_tighter_than_bool is_true SmartFlatTypeMap Bounds.bounds_to_base_type ZRange.is_bounded_by' 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 + | progress destruct_head bounds + | 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 + t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t) + (Hv : SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + = SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) 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 (fun _ => Bounds.bounds_to_base_type) 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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + v + = k. +Proof. + pose proof (fun pf => @relax_output_bounds' 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. |