diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 59 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas.v | 263 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijn.v | 7 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | 3 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v | 16 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 10 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 71 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Glue.v | 31 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/OutputType.v | 61 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 124 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Relax.v | 61 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/RoundUpLemmas.v | 34 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestDisplayCommon.v | 3 |
14 files changed, 435 insertions, 309 deletions
diff --git a/_CoqProject b/_CoqProject index 85b20d005..07a1305b8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -137,6 +137,7 @@ src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v src/Compilers/Z/Bounds/Pipeline.v src/Compilers/Z/Bounds/Relax.v +src/Compilers/Z/Bounds/RoundUpLemmas.v src/Compilers/Z/Bounds/Pipeline/Definition.v src/Compilers/Z/Bounds/Pipeline/Glue.v src/Compilers/Z/Bounds/Pipeline/OutputType.v diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index b9880f097..80f2dd9da 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -123,12 +123,15 @@ Module Import Bounds. Definition interp_base_type (ty : base_type) : Set := t. - Definition bit_width_of_base_type ty : option Z + Definition log_bit_width_of_base_type ty : option nat := match ty with | TZ => None - | TWord logsz => Some (2^Z.of_nat logsz)%Z + | 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 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 @@ -147,10 +150,56 @@ Module Import Bounds. 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 + 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 TWord (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) - else TZ. + 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 base_type op t) (input_bounds : interp_flat_type interp_base_type (domain t)) diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas.v b/src/Compilers/Z/Bounds/InterpretationLemmas.v index 7a1c2bc73..3f7aad17e 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas.v @@ -15,9 +15,6 @@ 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 := @@ -232,7 +229,7 @@ Lemma is_bounded_by_truncation_bounds Tout bs v (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 *. + 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 * @@ -304,130 +301,136 @@ 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. +Section with_round_up. + 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). + + 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. + + Admitted. +End with_round_up. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v index 45b084566..c08ae1298 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v @@ -5,18 +5,19 @@ Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Section language. - Context {t : type base_type}. + Context (round_up : nat -> option nat) + {t : type base_type}. Definition MapCastCompile := @MapCastCompile t. Definition MapCastDoCast := @MapCastDoCast (@Bounds.interp_base_type) (@Bounds.interp_op) - (fun _ => @Bounds.bounds_to_base_type) + (@Bounds.bounds_to_base_type round_up) (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) t. Definition MapCastDoInterp := @MapCastDoInterp - (@Bounds.interp_base_type) (fun _ => @Bounds.bounds_to_base_type) + (@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)). diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v index 46f472311..da8f91ef4 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v @@ -10,10 +10,11 @@ Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. Lemma MapCastCorrect + {round_up} {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')) + : 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), Interp (@Bounds.interp_op) e input_bounds = b /\ Bounds.is_bounded_by b (Interp interp_op e v) diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v index 04d1f964e..154a3d29e 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v @@ -10,32 +10,34 @@ Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. Definition Wf_MapCast + {round_up} {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')) + {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) - (fun _ => @Bounds.bounds_to_base_type) + (@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 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')) + {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) - (fun _ => @Bounds.bounds_to_base_type) + (@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 _) ] + | [ 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 index 6c9cda840..f58ece206 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -15,6 +15,12 @@ Module Export Exports. Export ReflectiveTactics.Exports. End Exports. -Ltac refine_reflectively := - refine_to_reflective_glue; +Ltac refine_reflectively_gen allowable_bit_widths := + refine_to_reflective_glue allowable_bit_widths; do_reflective_pipeline. + +Ltac refine_reflectively64 := refine_reflectively_gen (64::128::nil)%nat%list. +Ltac refine_reflectively32 := refine_reflectively_gen (32::64::nil)%nat%list. + +(** The default *) +Ltac refine_reflectively := refine_reflectively64. diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index ae3401b78..d7f289c70 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -67,14 +67,15 @@ 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 + round_up {t} (e : Expr base_type op t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : option ProcessedReflectivePackage + : option (@ProcessedReflectivePackage round_up) := 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 + let e := MapCast _ e input_bounds in option_map (projT2_map (fun b e' @@ -96,37 +97,41 @@ 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. - +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). + + 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. +End with_round_up_list. (** ** Constant Simplification and Unfolding *) (** The reflective pipeline may introduce constants that you want to diff --git a/src/Compilers/Z/Bounds/Pipeline/Glue.v b/src/Compilers/Z/Bounds/Pipeline/Glue.v index 675d1d358..87a5ef321 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Glue.v +++ b/src/Compilers/Z/Bounds/Pipeline/Glue.v @@ -388,12 +388,12 @@ Ltac find_reified_f_evar LHS := | map wordToZ ?x => find_reified_f_evar x | _ => LHS end. -Ltac zrange_to_reflective_hyps_step_gen then_tac := +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 (fun _ => Bounds.bounds_to_base_type) bounds) 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 *) @@ -405,19 +405,19 @@ Ltac zrange_to_reflective_hyps_step_gen then_tac := | _ => idtac end. Ltac zrange_to_reflective_hyps_step := zrange_to_reflective_hyps_step_gen ltac:(fun _ => idtac). -Ltac zrange_to_reflective_hyps := zrange_to_reflective_hyps_step_gen ltac:(fun _ => zrange_to_reflective_hyps). -Ltac zrange_to_reflective_goal Hbounded := +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 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_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 @@ -431,7 +431,15 @@ Ltac zrange_to_reflective_goal Hbounded := cbv beta end; adjust_goal_for_reflective. -Ltac zrange_to_reflective Hbounded := zrange_to_reflective_hyps; zrange_to_reflective_goal Hbounded. +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; @@ -441,11 +449,12 @@ BoundedWordToZ ?f = F (BoundedWordToZ A) (BoundedWordToZ B) ... (BoundedWordToZ >> where [?f] is an evar, and turns it into a goal the that reflective automation pipeline can handle. *) -Ltac refine_to_reflective_glue' Hbounded := +Ltac refine_to_reflective_glue' allowable_bit_widths Hbounded := + let round_up := round_up_from_allowable_bit_widths allowable_bit_widths in reassoc_sig_and_eexists; do_curry_rhs; split_BoundedWordToZ; - zrange_to_reflective Hbounded. -Ltac refine_to_reflective_glue := + zrange_to_reflective round_up Hbounded. +Ltac refine_to_reflective_glue allowable_bit_widths := let Hbounded := fresh "Hbounded" in - refine_to_reflective_glue' Hbounded. + 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 index 8205ef70c..88e38fbf6 100644 --- a/src/Compilers/Z/Bounds/Pipeline/OutputType.v +++ b/src/Compilers/Z/Bounds/Pipeline/OutputType.v @@ -7,40 +7,41 @@ 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)) }. +Section with_round_up_list. + Context {allowable_lgsz : list nat}. -Notation OutputType pkg - := (Arrow (pick_type (@input_bounds pkg)) (pick_type (@output_bounds pkg))) - (only parsing). + 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). -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. + 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)) }. -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)). + 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)). +End with_round_up_list. Ltac inversion_ProcessedReflectivePackage := repeat match goal with diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 147db3e54..9876c568c 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -148,66 +148,70 @@ 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_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 base_type op (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 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 eq_InterpEta, <- 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. +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). + 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_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 base_type op (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 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 eq_InterpEta, <- 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. +End with_round_up_list. (** ** Assembling the Pipeline, in Ltac *) (** The tactic [refine_with_pipeline_correct] uses the @@ -217,7 +221,7 @@ Qed. Ltac refine_with_pipeline_correct := lazymatch goal with | [ |- _ /\ ?castback ?fW = ?fZ ?arg ] - => let lem := open_constr:(@PipelineCorrect _ _ _ _ _ _ _ _ _ _ _ _) in + => let lem := open_constr:(@PipelineCorrect _ _ _ _ _ _ _ _ _ _ _ _ _) in simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _); subst fW fZ end; diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v index 40b678071..328ea5f48 100644 --- a/src/Compilers/Z/Bounds/Relax.v +++ b/src/Compilers/Z/Bounds/Relax.v @@ -1,4 +1,5 @@ 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. @@ -8,10 +9,12 @@ 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. Require Import Crypto.Util.Bool. @@ -29,28 +32,29 @@ 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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds - = SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) tight_output_bounds) + (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 (fun _ => Bounds.bounds_to_base_type) tight_output_bounds + (@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 (fun _ => Bounds.bounds_to_base_type) tight_output_bounds + (@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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + (@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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + (@Bounds.interp_base_type) t (@Bounds.bounds_to_base_type round_up) relaxed_output_bounds v = k. Proof. @@ -58,22 +62,24 @@ Proof. 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 ]. } + { 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)). @@ -103,24 +109,25 @@ Proof. Qed. Lemma relax_output_bounds + round_up 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) + (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 (fun _ => Bounds.bounds_to_base_type) tight_output_bounds + (@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 (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds + (@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' t tight_output_bounds relaxed_output_bounds Hv v k (conj pf (proj2 Htighter)) Hrelax) as H. + 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. diff --git a/src/Compilers/Z/Bounds/RoundUpLemmas.v b/src/Compilers/Z/Bounds/RoundUpLemmas.v new file mode 100644 index 000000000..ce4ea9373 --- /dev/null +++ b/src/Compilers/Z/Bounds/RoundUpLemmas.v @@ -0,0 +1,34 @@ +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. diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v index 960b65db0..8ef0f58dd 100644 --- a/src/Specific/IntegrationTestDisplayCommon.v +++ b/src/Specific/IntegrationTestDisplayCommon.v @@ -44,6 +44,9 @@ Tactic Notation "display" open_constr(f) := adjust_tuple2_tuple2_sig Tuple.tuple Tuple.tuple' FixedWordSizes.wordT FixedWordSizes.word_case FixedWordSizes.ZToWord FixedWordSizes.word_case_dep + Bounds.actual_logsz Bounds.round_up_to_in_list Bounds.option_min + List.map List.filter List.fold_right List.fold_left + Nat.leb Nat.min PeanoNat.Nat.log2 PeanoNat.Nat.log2_iter PeanoNat.Nat.pred Bounds.bounds_to_base_type interp_flat_type |