From cb9e18103c6fe0580fa6598380b6c6ec66d261a0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Mar 2017 16:48:08 -0400 Subject: Don't linearize and eta in MapCastByDeBruijn --- src/Reflection/MapCastByDeBruijn.v | 19 ++- src/Reflection/MapCastByDeBruijnInterp.v | 23 ++-- src/Reflection/MapCastByDeBruijnWf.v | 9 +- src/Reflection/Z/Bounds/Interpretation.v | 197 +++++++++++++++++++++++++++++++ src/Reflection/Z/BoundsInterpretations.v | 197 ------------------------------- 5 files changed, 215 insertions(+), 230 deletions(-) create mode 100644 src/Reflection/Z/Bounds/Interpretation.v delete mode 100644 src/Reflection/Z/BoundsInterpretations.v (limited to 'src/Reflection') diff --git a/src/Reflection/MapCastByDeBruijn.v b/src/Reflection/MapCastByDeBruijn.v index 7998b0a37..68eb06a54 100644 --- a/src/Reflection/MapCastByDeBruijn.v +++ b/src/Reflection/MapCastByDeBruijn.v @@ -5,10 +5,12 @@ Require Import Crypto.Reflection.Named.InterpretToPHOAS. Require Import Crypto.Reflection.Named.Compile. Require Import Crypto.Reflection.Named.PositiveContext. Require Import Crypto.Reflection.Named.PositiveContext.Defaults. -Require Import Crypto.Reflection.Linearize. -Require Import Crypto.Reflection.Eta. Require Import Crypto.Reflection.Syntax. +(** N.B. This procedure only works when there are no nested lets, + i.e., nothing like [let x := let y := z in w] in the PHOAS syntax + tree. This is a limitation of [compile]. *) + Section language. Context {base_type_code : Type} {op : flat_type base_type_code -> flat_type base_type_code -> Type} @@ -28,14 +30,11 @@ Section language. Context {t} (e : Expr base_type_code op t) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)). - Definition MapCastPreProcess - := ExprEta (Linearize e). - Definition MapCastCompile (e' : Expr base_type_code op (domain t -> codomain t)) - := compile (e' _) (DefaultNamesFor e'). - Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive (domain t -> codomain t))) + Definition MapCastCompile + := compile (e _) (DefaultNamesFor e). + Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive t)) := option_map (fun e'' => map_cast - (t:=Arrow (domain t) (codomain t)) interp_op_bounds pick_typeb cast_op (BoundsContext:=PContext _) empty @@ -51,12 +50,12 @@ Section language. & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) } := match e' with | Some (Some (existT output_bounds e'')) - => Some (existT _ output_bounds (Eta.ExprEta (InterpToPHOAS (Context:=fun var => PContext var) failb e''))) + => Some (existT _ output_bounds (InterpToPHOAS (Context:=fun var => PContext var) failb e'')) | Some None | None => None end. Definition MapCast : option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t) & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) } - := MapCastDoInterp (MapCastDoCast (MapCastCompile MapCastPreProcess)). + := MapCastDoInterp (MapCastDoCast MapCastCompile). End MapCast. End language. diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index 7fa043791..74622223e 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -11,10 +11,6 @@ Require Import Crypto.Reflection.Named.CompileWf. Require Import Crypto.Reflection.Named.PositiveContext. Require Import Crypto.Reflection.Named.PositiveContext.Defaults. Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties. -Require Import Crypto.Reflection.EtaInterp. -Require Import Crypto.Reflection.EtaWf. -Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.LinearizeWf. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.MapCastByDeBruijn. Require Import Crypto.Util.Decidable. @@ -83,7 +79,7 @@ Section language. /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). Proof. - unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'. + unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. break_innermost_match; try congruence; intros ? v v'. inversion_option; inversion_sigma; subst; simpl in *; intros. lazymatch goal with @@ -103,22 +99,17 @@ Section language. end | | change (interp interp_op (?e ?var) ?v') with (Interp interp_op e v'); - rewrite InterpExprEta; unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen; rewrite <- interp_interp_to_phoas; [ reflexivity | ] ]. - { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - cbv [Eta.ExprEta Linearize.Linearize]; - [ rewrite interp_expr_eta, interp_linearize | .. ]; - [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _); + [ reflexivity | auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } - { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - cbv [Eta.ExprEta Linearize.Linearize]; - [ rewrite interp_expr_eta, interp_linearize | .. ]; - [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _); + [ reflexivity | auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances. - { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - [ eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':= e _); + [ auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } } Qed. diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index 2cb7e2f40..7130c00ea 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -9,8 +9,6 @@ Require Import Crypto.Reflection.Named.CompileWf. Require Import Crypto.Reflection.Named.PositiveContext. Require Import Crypto.Reflection.Named.PositiveContext.Defaults. Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties. -Require Import Crypto.Reflection.LinearizeWf. -Require Import Crypto.Reflection.EtaWf. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.MapCastByDeBruijn. Require Import Crypto.Util.Decidable. @@ -76,12 +74,11 @@ Section language. : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')), Wf e'. Proof. - unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'. + unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. break_innermost_match; try congruence; intros ? v v'. inversion_option; inversion_sigma; subst; simpl in *; intros. unfold InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen. destruct t as [src dst]. - apply (proj2 (wf_expr_eta (t:=Arrow _ _))). eapply (@wf_interp_to_phoas base_type_code op FMapPositive.PositiveMap.key _ _ _ _ (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) @@ -90,9 +87,7 @@ Section language. (failb _) (failb _) _ e1); (eapply wf_map_cast with (fValues:=empty); eauto using PositiveContextOk with typeclass_instances); try (eapply (wf_compile (ContextOk:=PositiveContextOk)); - [ eapply (proj2 (wf_expr_eta (t:=Arrow _ _))); - [ eapply wf_linearize | .. ]; - eauto + [ eauto | .. | eassumption ]); try solve [ auto using name_list_unique_DefaultNamesFor diff --git a/src/Reflection/Z/Bounds/Interpretation.v b/src/Reflection/Z/Bounds/Interpretation.v new file mode 100644 index 000000000..8e90213b6 --- /dev/null +++ b/src/Reflection/Z/Bounds/Interpretation.v @@ -0,0 +1,197 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.Tactics.DestructHead. +Export Reflection.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. + +Module Import Bounds. + Definition t := option bounds. (* TODO?: Separate out the bounds computation from the overflow computation? e.g., have [safety := in_bounds | overflow] and [t := bounds * safety]? *) + Bind Scope bounds_scope with t. + Local Coercion Z.of_nat : nat >-> Z. + Section with_bitwidth. + Context (bit_width : option Z). + Definition SmartBuildBounds (l u : Z) + := if ((0 <=? l) && (match bit_width with Some bit_width => u true end))%Z%bool + then Some {| lower := l ; upper := u |} + else None. + Definition SmartRebuildBounds (b : t) : t + := match b with + | Some b => SmartBuildBounds (lower b) (upper b) + | None => None + end. + Definition t_map1 (f : bounds -> bounds) (x : t) + := match x with + | Some x + => match f x with + | {| lower := l ; upper := u |} + => SmartBuildBounds l u + end + | _ => None + end%Z. + Definition t_map2 (f : bounds -> bounds -> bounds) (x y : t) + := match x, y with + | Some x, Some y + => match f x y with + | {| lower := l ; upper := u |} + => SmartBuildBounds l u + end + | _, _ => None + end%Z. + Definition t_map4 (f : bounds -> bounds -> bounds -> bounds -> bounds) (x y z w : t) + := match x, y, z, w with + | Some x, Some y, Some z, Some w + => match f x y z w with + | {| lower := l ; upper := u |} + => SmartBuildBounds l u + end + | _, _, _, _ => None + end%Z. + Definition add' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx + ly ; upper := ux + uy |}. + Definition add : t -> t -> t := t_map2 add'. + Definition sub' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx - uy ; upper := ux - ly |}. + Definition sub : t -> t -> t := t_map2 sub'. + Definition mul' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx * ly ; upper := ux * uy |}. + Definition mul : t -> t -> t := t_map2 mul'. + Definition shl' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.shiftl lx ly ; upper := Z.shiftl ux uy |}. + Definition shl : t -> t -> t := t_map2 shl'. + Definition shr' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.shiftr lx uy ; upper := Z.shiftr ux ly |}. + Definition shr : t -> t -> t := t_map2 shr'. + Definition land' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := 0 ; upper := Z.min ux uy |}. + Definition land : t -> t -> t := t_map2 land'. + Definition lor' : bounds -> bounds -> 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 lor : t -> t -> t := t_map2 lor'. + Definition neg' (int_width : Z) : bounds -> bounds + := 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 := 0 ; upper := Z.ones int_width |} + else {| lower := 0 ; upper := 0 |}. + Definition neg (int_width : Z) : t -> t + := fun v + => if ((0 <=? int_width) (*&& (int_width <=? WordW.bit_width)*))%Z%bool + then t_map1 (neg' int_width) v + else None. + Definition cmovne' (r1 r2 : bounds) : bounds + := 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 := t_map4 (fun _ _ => cmovne') x y r1 r2. + Definition cmovle' (r1 r2 : bounds) : bounds + := 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 := t_map4 (fun _ _ => cmovle') x y 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. + 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 TZ v => fun _ => SmartBuildBounds None v v + | OpConst (TWord _ as T) v => fun _ => SmartBuildBounds (bit_width_of_base_type T) ((*FixedWordSizes.wordToZ*) v) ((*FixedWordSizes.wordToZ*) 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) + | Neg T int_width => fun x => neg (bit_width_of_base_type T) int_width x + | Cmovne T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne (bit_width_of_base_type T) x y z w + | Cmovle T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle (bit_width_of_base_type T) x y z w + | Cast _ T => fun x => SmartRebuildBounds (bit_width_of_base_type T) x + end%bounds. + + Definition of_Z (z : Z) : t := Some (ZToZRange z). + + Definition of_interp t (z : Syntax.interp_base_type t) : interp_base_type t + := Some (ZToZRange (match t return Syntax.interp_base_type t -> Z with + | TZ => fun z => z + | TWord logsz => fun z => z (*FixedWordSizes.wordToZ*) + end z)). + + Definition bounds_to_base_type' (b : bounds) : base_type + := if (0 <=? lower b)%Z + then TWord (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) + else TZ. + Definition bounds_to_base_type (b : t) : base_type + := match b with + | None => TZ + | Some b' => bounds_to_base_type' b' + end. + + 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 bound_is_goodb : forall t, interp_base_type t -> bool + := fun t bs + => match bs with + | Some bs + => (*let l := lower bs in + let u := upper bs in + let bit_width := bit_width_of_base_type t in + ((0 <=? l) && (match bit_width with Some bit_width => Z.log2 u true end))%Z%bool*) + true + | None => false + end. + Definition bound_is_good : forall t, interp_base_type t -> Prop + := fun t v => bound_is_goodb t v = true. + Definition bounds_are_good : forall {t}, interp_flat_type interp_base_type t -> Prop + := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). + + Definition is_bounded_by' {T} : Syntax.interp_base_type T -> interp_base_type T -> Prop + := fun val bound + => match bound with + | Some bounds' + => is_bounded_by' (bit_width_of_base_type T) bounds' val + | None => True + end. + + Definition is_bounded_by {T} : interp_flat_type Syntax.interp_base_type T -> interp_flat_type 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/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/BoundsInterpretations.v deleted file mode 100644 index 8e90213b6..000000000 --- a/src/Reflection/Z/BoundsInterpretations.v +++ /dev/null @@ -1,197 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Reflection.Z.Syntax. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Relations. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.Tactics.DestructHead. -Export Reflection.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. - -Module Import Bounds. - Definition t := option bounds. (* TODO?: Separate out the bounds computation from the overflow computation? e.g., have [safety := in_bounds | overflow] and [t := bounds * safety]? *) - Bind Scope bounds_scope with t. - Local Coercion Z.of_nat : nat >-> Z. - Section with_bitwidth. - Context (bit_width : option Z). - Definition SmartBuildBounds (l u : Z) - := if ((0 <=? l) && (match bit_width with Some bit_width => u true end))%Z%bool - then Some {| lower := l ; upper := u |} - else None. - Definition SmartRebuildBounds (b : t) : t - := match b with - | Some b => SmartBuildBounds (lower b) (upper b) - | None => None - end. - Definition t_map1 (f : bounds -> bounds) (x : t) - := match x with - | Some x - => match f x with - | {| lower := l ; upper := u |} - => SmartBuildBounds l u - end - | _ => None - end%Z. - Definition t_map2 (f : bounds -> bounds -> bounds) (x y : t) - := match x, y with - | Some x, Some y - => match f x y with - | {| lower := l ; upper := u |} - => SmartBuildBounds l u - end - | _, _ => None - end%Z. - Definition t_map4 (f : bounds -> bounds -> bounds -> bounds -> bounds) (x y z w : t) - := match x, y, z, w with - | Some x, Some y, Some z, Some w - => match f x y z w with - | {| lower := l ; upper := u |} - => SmartBuildBounds l u - end - | _, _, _, _ => None - end%Z. - Definition add' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx + ly ; upper := ux + uy |}. - Definition add : t -> t -> t := t_map2 add'. - Definition sub' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx - uy ; upper := ux - ly |}. - Definition sub : t -> t -> t := t_map2 sub'. - Definition mul' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx * ly ; upper := ux * uy |}. - Definition mul : t -> t -> t := t_map2 mul'. - Definition shl' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.shiftl lx ly ; upper := Z.shiftl ux uy |}. - Definition shl : t -> t -> t := t_map2 shl'. - Definition shr' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.shiftr lx uy ; upper := Z.shiftr ux ly |}. - Definition shr : t -> t -> t := t_map2 shr'. - Definition land' : bounds -> bounds -> bounds - := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := 0 ; upper := Z.min ux uy |}. - Definition land : t -> t -> t := t_map2 land'. - Definition lor' : bounds -> bounds -> 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 lor : t -> t -> t := t_map2 lor'. - Definition neg' (int_width : Z) : bounds -> bounds - := 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 := 0 ; upper := Z.ones int_width |} - else {| lower := 0 ; upper := 0 |}. - Definition neg (int_width : Z) : t -> t - := fun v - => if ((0 <=? int_width) (*&& (int_width <=? WordW.bit_width)*))%Z%bool - then t_map1 (neg' int_width) v - else None. - Definition cmovne' (r1 r2 : bounds) : bounds - := 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 := t_map4 (fun _ _ => cmovne') x y r1 r2. - Definition cmovle' (r1 r2 : bounds) : bounds - := 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 := t_map4 (fun _ _ => cmovle') x y 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. - 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 TZ v => fun _ => SmartBuildBounds None v v - | OpConst (TWord _ as T) v => fun _ => SmartBuildBounds (bit_width_of_base_type T) ((*FixedWordSizes.wordToZ*) v) ((*FixedWordSizes.wordToZ*) 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) - | Neg T int_width => fun x => neg (bit_width_of_base_type T) int_width x - | Cmovne T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne (bit_width_of_base_type T) x y z w - | Cmovle T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle (bit_width_of_base_type T) x y z w - | Cast _ T => fun x => SmartRebuildBounds (bit_width_of_base_type T) x - end%bounds. - - Definition of_Z (z : Z) : t := Some (ZToZRange z). - - Definition of_interp t (z : Syntax.interp_base_type t) : interp_base_type t - := Some (ZToZRange (match t return Syntax.interp_base_type t -> Z with - | TZ => fun z => z - | TWord logsz => fun z => z (*FixedWordSizes.wordToZ*) - end z)). - - Definition bounds_to_base_type' (b : bounds) : base_type - := if (0 <=? lower b)%Z - then TWord (Z.to_nat (Z.log2_up (Z.log2_up (1 + upper b)))) - else TZ. - Definition bounds_to_base_type (b : t) : base_type - := match b with - | None => TZ - | Some b' => bounds_to_base_type' b' - end. - - 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 bound_is_goodb : forall t, interp_base_type t -> bool - := fun t bs - => match bs with - | Some bs - => (*let l := lower bs in - let u := upper bs in - let bit_width := bit_width_of_base_type t in - ((0 <=? l) && (match bit_width with Some bit_width => Z.log2 u true end))%Z%bool*) - true - | None => false - end. - Definition bound_is_good : forall t, interp_base_type t -> Prop - := fun t v => bound_is_goodb t v = true. - Definition bounds_are_good : forall {t}, interp_flat_type interp_base_type t -> Prop - := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). - - Definition is_bounded_by' {T} : Syntax.interp_base_type T -> interp_base_type T -> Prop - := fun val bound - => match bound with - | Some bounds' - => is_bounded_by' (bit_width_of_base_type T) bounds' val - | None => True - end. - - Definition is_bounded_by {T} : interp_flat_type Syntax.interp_base_type T -> interp_flat_type 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. -- cgit v1.2.3