diff --git a/src/AbstractInterpretation/AbstractInterpretation.v b/src/AbstractInterpretation/AbstractInterpretation.v index c43ead4fc9..5345c0e3c3 100644 --- a/src/AbstractInterpretation/AbstractInterpretation.v +++ b/src/AbstractInterpretation/AbstractInterpretation.v @@ -34,7 +34,8 @@ Module Compilers. {var : type -> Type}. Local Notation expr := (@expr base_type ident). Local Notation UnderLets := (@UnderLets base_type ident var). - Context (abstract_domain' : base_type -> Type) + Context {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + (abstract_domain' : base_type -> Type) (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> UnderLets (@expr var t)) (bottom' : forall A, abstract_domain' A) (skip_annotations_under : forall t, ident t -> bool). @@ -42,18 +43,25 @@ Module Compilers. Definition abstract_domain (t : type) := type.interp abstract_domain' t. - Fixpoint value (t : type) + Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *) + + (** A value should carry both an abstract state and a way of turning value's into expressions *) + Fixpoint value' (t : type) := match t return Type (* COQBUG(https://github.com/coq/coq/issues/7727) *) with | type.base t - => abstract_domain t * @expr var t + => @expr var t | type.arrow s d - => value s -> UnderLets (value d) + => abstract_domain s * value' s -> UnderLets (value' d) end%type. - Definition value_with_lets (t : type) - := UnderLets (value t). + Definition value (t : type) : Type + := abstract_domain t * UnderLets (value' t). + + Context (ident_extract : forall t, ident t -> abstract_domain t). + Context (interp_ident' : bool (* annotate with state? *) -> forall t, ident t -> UnderLets (value' t)). - Context (interp_ident : bool (* annotate with state? *) -> forall t, ident t -> value_with_lets t). + Definition interp_ident (annotate_with_state : bool) {t} (idc : ident t) : value t + := (ident_extract _ idc, interp_ident' annotate_with_state _ idc). Fixpoint bottom {t} : abstract_domain t := match t with @@ -67,54 +75,50 @@ Module Compilers. | type.arrow s d => (bottom, @bottom_for_each_lhs_of_arrow d) end. - Definition state_of_value {t} : value t -> abstract_domain t - := match t return value t -> abstract_domain t with - | type.base t => fun '(st, v) => st - | type.arrow s d => fun _ => bottom - end. + Definition state_of_value {t} : value t -> abstract_domain t := fst. + Definition project_value' {t} : value t -> UnderLets (value' t) := snd. + Definition Base_value' {t} : abstract_domain t * value' t -> value t + := fun x => (fst x, Base (snd x)). + Definition apply_value {s d} (f : value (s -> d)) (x : value s) : value d + := let '(x1, x2) := (state_of_value x, project_value' x) in + let '(f1, f2) := (state_of_value f, project_value' f) in + (f1 x1, (f2 <-- f2; x2 <-- x2; f2 (x1, x2))%under_lets). - (** We need to make sure that we ignore the state of - higher-order arrows *everywhere*, or else the proofs don't go - through. So we sometimes need to replace the state of - arrow-typed values with [⊥]. *) - Fixpoint bottomify {t} : value t -> value_with_lets t - := match t return value t -> value_with_lets t with - | type.base t => fun '(st, v) => Base (bottom' t, v) - | type.arrow s d => fun f => Base (fun x => fx <-- f x; @bottomify d fx) - end%under_lets. - - (** We drop the state of higher-order arrows *) Fixpoint reify (annotate_with_state : bool) (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with | type.base t => fun '(st, v) 'tt - => if annotate_with_state - then annotate is_let_bound t st v - else if is_let_bound - then UnderLets.UnderLet v (fun v' => UnderLets.Base ($$v')) - else UnderLets.Base v + => (v <-- v; + if annotate_with_state + then annotate is_let_bound t st v + else if is_let_bound + then UnderLets.UnderLet v (fun v' => UnderLets.Base ($$v')) + else UnderLets.Base v) | type.arrow s d => fun f_e '(sv, dv) - => let sv := match s with - | type.base _ => sv - | type.arrow _ _ => bottom - end in - Base - (λ x , (UnderLets.to_expr - (fx <-- f_e (@reflect annotate_with_state _ (expr.Var x) sv); - @reify annotate_with_state false _ fx dv))) - end%core%expr + => (let f := state_of_value f_e in + f_e <-- project_value' f_e; + Base + (λ x , UnderLets.to_expr + (let sv := @reflect annotate_with_state _ (expr.Var x) sv in + let sx := state_of_value sv in + x <-- project_value' sv; + fx <-- f_e (sx, x)%core; + @reify annotate_with_state false _ (f sx, Base fx)%core dv))) + end%core%expr%under_lets with reflect (annotate_with_state : bool) {t} : @expr var t -> abstract_domain t -> value t := match t return @expr var t -> abstract_domain t -> value t with | type.base t - => fun e st => (st, e) + => fun e st => Base_value' (st, e) | type.arrow s d => fun e absf - => (fun v - => let stv := state_of_value v in - (rv <-- (@reify annotate_with_state false s v bottom_for_each_lhs_of_arrow); - Base (@reflect annotate_with_state d (e @ rv) (absf stv))%expr)) - end%under_lets. + => Base_value' + (absf, + (fun v + => rv <-- @reify annotate_with_state false s (Base_value' v) bottom_for_each_lhs_of_arrow; + (* TODO: Should we be feeding in [fst v], or should we bottom out the arguments to [fst v]? *) + project_value' (@reflect annotate_with_state d (e @ rv) (absf (fst v)))%expr)) + end%under_lets%core. Definition skip_annotations_for_App {var'} {t} (e : @expr var' t) : bool := match invert_AppIdent_curried e with @@ -122,64 +126,74 @@ Module Compilers. | None => false end. - Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value_with_lets t) : value_with_lets t + Definition invert_default {A B} (t : type) (x : option { t : type & @expr abstract_domain (A t) * @expr abstract_domain (B t) }%type) : @expr abstract_domain (A t) * @expr abstract_domain (B t) + := Option.value + (type.try_transport + _ _ t + (projT2 + (Option.value x (existT _ t (DefaultValue.type.base.defaultv, DefaultValue.type.base.defaultv))))) + (DefaultValue.type.base.defaultv, DefaultValue.type.base.defaultv). + + Definition invert_default' {A B C} (t : type) (x : option { t : type & @expr abstract_domain (A t) * (abstract_domain (B t) -> @expr abstract_domain (C t)) }%type) : @expr abstract_domain (A t) * (abstract_domain (B t) -> @expr abstract_domain (C t)) + := Option.value + (type.try_transport + _ _ t + (projT2 + (Option.value x (existT _ t (DefaultValue.type.base.defaultv, fun _ => DefaultValue.type.base.defaultv))))) + (DefaultValue.type.base.defaultv, fun _ => DefaultValue.type.base.defaultv). + + Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value t) : @expr abstract_domain t -> value t := let annotate_with_state := annotate_with_state && negb (skip_annotations_for_App e) in - match e in expr.expr t return value_with_lets t with - | expr.Ident t idc => interp_ident annotate_with_state _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*) - | expr.Var t v => v - | expr.Abs s d f => Base (fun x => @interp annotate_with_state d (f (Base x))) - | expr.App (type.base s) d f x - => (x' <-- @interp annotate_with_state _ x; - f' <-- @interp annotate_with_state (_ -> d)%etype f; - f' x') - | expr.App (type.arrow s' d') d f x - => (x' <-- @interp annotate_with_state (s' -> d')%etype x; - x'' <-- bottomify x'; - f' <-- @interp annotate_with_state (_ -> d)%etype f; - f' x'') - | expr.LetIn (type.arrow _ _) B x f - => (x' <-- @interp annotate_with_state _ x; - @interp annotate_with_state _ (f (Base x'))) - | expr.LetIn (type.base A) B x f - => (x' <-- @interp annotate_with_state _ x; - x'' <-- reify annotate_with_state true (* this forces a let-binder here *) x' tt; - @interp annotate_with_state _ (f (Base (reflect annotate_with_state x'' (state_of_value x'))))) + let expr_interp {t} := expr.interp (@ident_extract) (t:=t) in + match e in expr.expr t return @expr abstract_domain t -> value t with + | expr.Ident t idc => fun _ => @interp_ident annotate_with_state _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*) + | expr.Var t v => fun _ => v + | expr.Abs s d f + => fun fe_st + => let f_st := expr_interp fe_st in + let fe_st := Option.value (invert_Abs fe_st) ((* should never happen *)fun _ => DefaultValue.type.base.defaultv) in + Base_value' + (f_st, + (fun x + => project_value' (@interp annotate_with_state d (f (Base_value' x)) (fe_st (fst x))))) + | expr.App s d f x + => fun fx_st + => (let '(f_st, x_st) := invert_default s (invert_App fx_st) in + let x := @interp annotate_with_state s x x_st in + let f := @interp annotate_with_state (s -> d)%etype f f_st in + apply_value f x) + | expr.LetIn (type.base A' as A) B x f + => fun st + => let '(x_st, f_st) := invert_default' A (invert_LetIn st) in + let x := @interp annotate_with_state _ x x_st in + let x_st := state_of_value x in + let fx_st := f_st x_st in + (expr_interp fx_st, + x <-- reify annotate_with_state true (* this forces a let-binder here *) x tt; + project_value' (@interp annotate_with_state _ (f (reflect annotate_with_state x x_st)) fx_st)) + | expr.LetIn (type.arrow _ _ as A) B x f + => fun st + => let '(x_st, f_st) := invert_default' A (invert_LetIn st) in + let x := @interp annotate_with_state _ x x_st in + @interp annotate_with_state _ (f x) (f_st (state_of_value x)) end%under_lets. - Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value_with_lets t) + Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value t) (e_st : @expr abstract_domain t) (st : type.for_each_lhs_of_arrow abstract_domain t) : expr t - := UnderLets.to_expr (e' <-- interp annotate_with_state e; reify annotate_with_state false e' st). + := UnderLets.to_expr (reify annotate_with_state false (interp annotate_with_state e e_st) st). - Definition eval' {t} (e : @expr value_with_lets t) : expr t - := eval_with_bound' false e bottom_for_each_lhs_of_arrow. + Definition eval' {t} (e : @expr value t) (e_st : @expr abstract_domain t) : expr t + := eval_with_bound' false e e_st bottom_for_each_lhs_of_arrow. Definition eta_expand_with_bound' {t} (e : @expr var t) (st : type.for_each_lhs_of_arrow abstract_domain t) : expr t := UnderLets.to_expr (reify true false (reflect true e bottom) st). - Section extract. - Context (ident_extract : forall t, ident t -> abstract_domain t). - - (** like [expr.interp (@ident_extract) e], except we replace - all higher-order state with bottom *) - Fixpoint extract' {t} (e : @expr abstract_domain t) : abstract_domain t - := match e in expr.expr t return abstract_domain t with - | expr.Ident t idc => ident_extract t idc - | expr.Var t v => v - | expr.Abs s d f => fun v : abstract_domain s => @extract' _ (f v) - | expr.App (type.base s) d f x - => @extract' _ f (@extract' _ x) - | expr.App (type.arrow s' d') d f x - => @extract' _ f (@bottom (type.arrow s' d')) - | expr.LetIn A B x f => dlet y := @extract' _ x in @extract' _ (f y) - end. - - Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t) - : abstract_domain' (type.final_codomain t) - := type.app_curried (extract' e) bound. - End extract. + Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t) + : abstract_domain' (type.final_codomain t) + := type.app_curried (expr.interp (@ident_extract) e) bound. End with_var. Module ident. @@ -194,8 +208,8 @@ Module Compilers. Local Notation UnderLets := (@UnderLets base.type ident var). Context (abstract_domain' : base.type -> Type). Local Notation abstract_domain := (@abstract_domain base.type abstract_domain'). - Local Notation value_with_lets := (@value_with_lets base.type ident var abstract_domain'). Local Notation value := (@value base.type ident var abstract_domain'). + Local Notation value' := (@value' base.type ident var abstract_domain'). Context (annotate_expr : forall t, abstract_domain' t -> option (@expr var (t -> t))) (bottom' : forall A, abstract_domain' A) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) @@ -204,7 +218,7 @@ Module Compilers. (is_annotated_for : forall t t', @expr var t -> abstract_domain' t' -> bool) (annotation_to_cast : forall s d, @expr var (s -> d) -> option (@expr var s -> @expr var d)) (skip_annotations_under : forall t, ident t -> bool) - (strip_annotation : forall t, ident t -> option (value t)). + (strip_annotation : forall t, ident t -> option (value' t)). (** TODO: Is it okay to commute annotations? *) Definition update_annotation {t} (st : abstract_domain' t) (e : @expr var t) : @expr var t @@ -286,34 +300,35 @@ Module Compilers. Local Notation reify := (@reify base.type ident var abstract_domain' annotate bottom'). Local Notation reflect := (@reflect base.type ident var abstract_domain' annotate bottom'). + Local Notation apply_value := (@apply_value base.type ident var abstract_domain'). + Local Notation Base_value' := (@Base_value' base.type ident var abstract_domain'). (** We manually rewrite with the rule for [nth_default], as the eliminator for eta-expanding lists in the input *) - Definition interp_ident (annotate_with_state : bool) {t} (idc : ident t) : value_with_lets t - := match idc in ident t return value_with_lets t with + Definition interp_ident' (annotate_with_state : bool) {t} (idc : ident t) : UnderLets (value' t) + := match idc in ident t return UnderLets (value' t) with | ident.List_nth_default T as idc - => let default := reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) in - Base - (fun default_arg - => default <-- default default_arg; - Base - (fun ls_arg - => default <-- default ls_arg; - Base - (fun n_arg - => default <-- default n_arg; - ls' <-- @reify annotate_with_state false (base.type.list T) ls_arg tt; - Base - (fst default, - match reflect_list ls', invert_Literal (snd n_arg) with - | Some ls, Some n - => nth_default (snd default_arg) ls n - | _, _ => snd default - end)))) - | idc => Base - match strip_annotation _ idc with - | Some v => v - | None => reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) - end + => let '(default_st, default) := reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) in + (default <-- default; + Base + (fun default_arg + => default <-- default default_arg; + Base + (fun ls_arg + => default <-- default ls_arg; + Base + (fun n_arg + => default <-- default n_arg; + ls' <-- @reify annotate_with_state false (base.type.list T) (Base_value' ls_arg) tt; + Base + match reflect_list ls', invert_Literal (snd n_arg) with + | Some ls, Some n + => nth_default (snd default_arg) ls n + | _, _ => default + end)))) + | idc => match strip_annotation _ idc with + | Some v => Base v + | None => project_value' _ (reflect annotate_with_state (###idc) (abstract_interp_ident _ idc)) + end end%core%under_lets%expr. Fixpoint strip_all_annotations' (should_strip : bool) {t} (e : @expr var t) : @expr var t @@ -343,13 +358,13 @@ Module Compilers. Definition strip_all_annotations {t} (e : @expr var t) : @expr var t := @strip_all_annotations' false t e. - Definition eval_with_bound (skip_annotations_under : forall t, ident t -> bool) (annotate_with_state : bool) {t} (e : @expr value_with_lets t) + Definition eval_with_bound (skip_annotations_under : forall t, ident t -> bool) (annotate_with_state : bool) {t} (e : @expr value t) (e_st : @expr abstract_domain t) (st : type.for_each_lhs_of_arrow abstract_domain t) : @expr var t - := @eval_with_bound' base.type ident var abstract_domain' annotate bottom' skip_annotations_under interp_ident annotate_with_state t e st. + := @eval_with_bound' base.type ident var _ abstract_domain' annotate bottom' skip_annotations_under _ abstract_interp_ident interp_ident' annotate_with_state t e e_st st. - Definition eval {t} (e : @expr value_with_lets t) : @expr var t - := @eval' base.type ident var abstract_domain' annotate bottom' (fun _ _ => false) interp_ident t e. + Definition eval {t} (e : @expr value t) (e_st : @expr abstract_domain t) : @expr var t + := @eval' base.type ident var _ abstract_domain' annotate bottom' (fun _ _ => false) _ abstract_interp_ident interp_ident' t e e_st. Definition eta_expand_with_bound {t} (e : @expr var t) (st : type.for_each_lhs_of_arrow abstract_domain t) @@ -357,7 +372,7 @@ Module Compilers. := @eta_expand_with_bound' base.type ident var abstract_domain' annotate bottom' t e st. Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @extract_gen base.type ident abstract_domain' bottom' abstract_interp_ident t e bound. + := @extract_gen base.type ident abstract_domain' abstract_interp_ident t e bound. End with_var. End ident. @@ -366,8 +381,8 @@ Module Compilers. Section specialized. Local Notation abstract_domain' := ZRange.type.base.option.interp. Local Notation abstract_domain := (@partial.abstract_domain base.type abstract_domain'). - Local Notation value_with_lets var := (@value_with_lets base.type ident var abstract_domain'). Local Notation value var := (@value base.type ident var abstract_domain'). + Local Notation value' var := (@value' base.type ident var abstract_domain'). Notation expr := (@expr base.type ident). Notation Expr := (@expr.Expr base.type ident). Local Notation type := (type base.type). @@ -412,8 +427,8 @@ Module Compilers. Definition abstract_interp_ident {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) t (idc : ident t) : type.interp abstract_domain' t := ZRange.ident.option.interp assume_cast_truncates idc. - Definition always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} t (idc : ident t) : option (value var t) - := match idc in ident t return option (value var t) with + Definition always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} t (idc : ident t) : option (value' var t) + := match idc in ident t return option (value' var t) with | ident.Z_cast as idc | ident.Z_cast2 as idc => let tZ_type := (fun t (idc : ident (type.base _ -> type.base t -> type.base t)) => t) _ idc in (* we want Coq to pick up the Z type for bounds tightness, not the zrange type (where "tighter" means "equal") *) @@ -422,8 +437,7 @@ Module Compilers. => Base (fun '(r_known, e) => Base - ((abstract_interp_ident assume_cast_truncates _ idc r_orig r_known, - let do_strip + (let do_strip := match ZRange.type.base.option.lift_Some r_known, ZRange.type.base.option.lift_Some r_orig with | Some r_known, Some r_orig => ZRange.type.base.is_tighter_than @@ -433,11 +447,11 @@ Module Compilers. end in if do_strip then e - else (###idc @ re @ e)%expr)))) + else (###idc @ re @ e)%expr))) | _ => None end. - Definition strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var} : forall t, ident t -> option (value var t) + Definition strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var} : forall t, ident t -> option (value' var t) := if strip_annotations then always_strip_annotation assume_cast_truncates else fun _ _ => None. @@ -485,10 +499,10 @@ Module Compilers. Definition strip_all_annotations strip_annotations_under {var} {t} (e : @expr var t) : @expr var t := @ident.strip_all_annotations var (@annotation_to_cast _) strip_annotations_under t e. - Definition eval_with_bound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t + Definition eval_with_bound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e e_st : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t := let annotate_with_state := true in (@partial.ident.eval_with_bound) - var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e bound. + var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e e_st bound. Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t := let assume_cast_truncates := false in @@ -499,35 +513,39 @@ Module Compilers. Definition StripAllAnnotations strip_annotations_under {t} (e : Expr t) : Expr t := fun var => strip_all_annotations strip_annotations_under (e _). - Definition EvalWithBound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t - := fun var => eval_with_bound assume_cast_truncates skip_annotations_under strip_preexisting_annotations (e _) bound. + Definition EvalWithBound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (E : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t + := dlet_nd e := GeneralizeVar.ToFlat E in + let E := GeneralizeVar.FromFlat e in + fun var => eval_with_bound assume_cast_truncates skip_annotations_under strip_preexisting_annotations (E _) (E _) bound. Definition EtaExpandWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t := fun var => eta_expand_with_bound (e _) bound. End with_relax. - Definition strip_annotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t + Definition strip_annotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} {t} (e e_st : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t := let strip_preexisting_annotations := true in let annotate_with_state := false in let skip_annotations_under := fun _ _ => false in (@partial.ident.eval_with_bound) - var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e bound. + var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e e_st bound. Definition StripAnnotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t - := fun var => strip_annotations assume_cast_truncates (e _) bound. + := fun var => strip_annotations assume_cast_truncates (e _) (e _) bound. - Definition eval {opts : AbstractInterpretation.Options} {var} {t} (e : @expr _ t) : expr t + Definition eval {opts : AbstractInterpretation.Options} {var} {t} (e e_st : @expr _ t) : expr t := let assume_cast_truncates := false in let strip_preexisting_annotations := false in (@partial.ident.eval) - var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) t e. - Definition Eval {opts : AbstractInterpretation.Options} {t} (e : Expr t) : Expr t - := fun var => eval (e _). + var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) t e e_st. + Definition Eval {opts : AbstractInterpretation.Options} {t} (E : Expr t) : Expr t + := dlet_nd e := GeneralizeVar.ToFlat E in + let E := GeneralizeVar.FromFlat e in + fun var => eval (E _) (E _). Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t := EtaExpandWithBound default_relax_zrange e (type.map_for_each_lhs_of_arrow (@ZRange.type.option.strip_ranges) bound). Definition extract {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @partial.ident.extract abstract_domain' bottom' (abstract_interp_ident assume_cast_truncates) t e bound. + := @partial.ident.extract abstract_domain' (abstract_interp_ident assume_cast_truncates) t e bound. Definition Extract {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @partial.ident.extract abstract_domain' bottom' (abstract_interp_ident assume_cast_truncates) t (e _) bound. + := @partial.ident.extract abstract_domain' (abstract_interp_ident assume_cast_truncates) t (e _) bound. End specialized. End partial. Import API. diff --git a/src/AbstractInterpretation/Proofs.v b/src/AbstractInterpretation/Proofs.v index 22a96f8bff..2deca7fd74 100644 --- a/src/AbstractInterpretation/Proofs.v +++ b/src/AbstractInterpretation/Proofs.v @@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.Classes.Morphisms. Require Import Coq.Classes.RelationPairs. Require Import Coq.Relations.Relations. +Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.BasicLemmas. @@ -100,80 +101,133 @@ Module Compilers. (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v) (skip_annotations_under : forall t, ident t -> bool) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) - (ident_interp_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (ident_interp t idc)) + (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop). + Local Notation abstract_domain := (@abstract_domain base_type abstract_domain'). + Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R). + (* we only care about inputs that are extensional, so we restrict this here *) + (* skip_base:=true because abstract_domain'_R refl and eqv refl follows from abstraction_relation' *) + Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop + := type.related_hetero_and_Proper (skip_base:=true) (@abstract_domain'_R) (fun _ => eq) (@abstraction_relation'). + (*Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop + := type.related_hetero (@abstraction_relation').*) + Context (ident_interp_Proper : forall t (idc : ident t), abstraction_relation (abstract_interp_ident t idc) (ident_interp t idc)) (ident_interp_Proper' : forall t, Proper (eq ==> type.eqv) (ident_interp t)) - (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop) (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t)) {abstract_domain'_R_transitive : forall t, Transitive (@abstract_domain'_R t)} {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)} {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} + (base_type_beq : base_type -> base_type -> bool) + {reflect_base_type_beq : reflect_rel eq base_type_beq} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type} (abstract_domain'_R_of_related : forall t st v, @abstraction_relation' t st v -> @abstract_domain'_R t st st). - Local Notation abstract_domain := (@abstract_domain base_type abstract_domain'). - Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop - := type.related_hetero (@abstraction_relation'). Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')). Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')). - Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R). Local Notation var := (type.interp base_interp). Local Notation expr := (@expr.expr base_type ident). Local Notation UnderLets := (@UnderLets base_type ident). + Local Notation value' := (@value' base_type ident var abstract_domain'). Local Notation value := (@value base_type ident var abstract_domain'). - Local Notation value_with_lets := (@value_with_lets base_type ident var abstract_domain'). - Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain' bottom'). + Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain'). + Local Notation project_value' := (@project_value' base_type ident var abstract_domain'). + Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' abstract_interp_ident). + Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *) Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> @UnderLets var (@expr var t)) - (interp_ident : bool -> forall t, ident t -> value_with_lets t) - (ident_extract : forall t, ident t -> abstract_domain t) + (interp_ident' : bool -> forall t, ident t -> @UnderLets var (value' t)) (interp_annotate : forall is_let_bound t st e (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e)), expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate is_let_bound t st e)) = expr.interp (@ident_interp) e) - (ident_extract_Proper : forall t, Proper (eq ==> abstract_domain_R) (ident_extract t)). + (abstract_interp_ident_Proper : forall t, Proper (eq ==> abstract_domain_R) (abstract_interp_ident t)). Local Notation eta_expand_with_bound' := (@eta_expand_with_bound' base_type ident _ abstract_domain' annotate bottom'). - Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ abstract_domain' annotate bottom' skip_annotations_under interp_ident). - Local Notation extract' := (@extract' base_type ident abstract_domain' bottom' ident_extract). - Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' bottom' ident_extract). + Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ try_make_transport_base_type_cps abstract_domain' annotate bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'). Local Notation reify := (@reify base_type ident _ abstract_domain' annotate bottom'). Local Notation reflect := (@reflect base_type ident _ abstract_domain' annotate bottom'). - Local Notation interp := (@interp base_type ident var abstract_domain' annotate bottom' skip_annotations_under interp_ident). - Local Notation bottomify := (@bottomify base_type ident _ abstract_domain' bottom'). - - Lemma bottom_related t v : @abstraction_relation t bottom v. - Proof using bottom'_related. cbv [abstraction_relation]; induction t; cbn; cbv [respectful_hetero]; eauto. Qed. - - Local Hint Resolve bottom_related : core typeclass_instances. + Local Notation interp := (@interp base_type ident var try_make_transport_base_type_cps abstract_domain' annotate bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'). + Local Notation invert_default := (@invert_default base_type ident try_make_transport_base_type_cps abstract_domain' default_expr). + Local Notation invert_default' := (@invert_default' base_type ident try_make_transport_base_type_cps abstract_domain' default_expr). + Local Notation interp_ident := (@interp_ident base_type ident var abstract_domain' abstract_interp_ident interp_ident'). + + Lemma abstract_domain_R_refl_of_abstraction_relation {t st v} + : @abstraction_relation t st v -> Proper abstract_domain_R st. + Proof using abstract_domain'_R_of_related. apply type.related_hetero_and_Proper_proj1, abstract_domain'_R_of_related. Qed. + Local Hint Immediate abstract_domain_R_refl_of_abstraction_relation : core typeclass_instances. + Lemma eqv_refl_of_abstraction_relation {t st v} + : @abstraction_relation t st v -> v == v. + Proof using Type. apply type.related_hetero_and_Proper_proj2; repeat intro; hnf; auto. Qed. + Local Hint Immediate eqv_refl_of_abstraction_relation : core typeclass_instances. + + Lemma eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow {t st v} + : type.and_for_each_lhs_of_arrow (t:=t) (@abstraction_relation) st v -> type.and_for_each_lhs_of_arrow (t:=t) (@type.eqv) v v. + Proof using Type. + apply type.and_for_each_lhs_of_arrow_Proper_impl_hetero2, @eqv_refl_of_abstraction_relation. + Qed. + Local Hint Immediate eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow : core typeclass_instances. - Lemma bottom_for_each_lhs_of_arrow_related t v : type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v. - Proof using bottom'_related. induction t; cbn; eauto using bottom_related. Qed. + Lemma abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow {t st v} + : type.and_for_each_lhs_of_arrow (t:=t) (@abstraction_relation) st v -> type.and_for_each_lhs_of_arrow (t:=t) (@abstract_domain_R) st st. + Proof using abstract_domain'_R_of_related. + apply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1, @abstract_domain_R_refl_of_abstraction_relation. + Qed. + Local Hint Immediate abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow : core typeclass_instances. + + Lemma abstraction_relation_iff_app_curried {t st v} + : @abstraction_relation t st v + <-> (Proper (@abstract_domain_R t) st + /\ v == v + /\ forall x y, + type.and_for_each_lhs_of_arrow (@abstraction_relation) x y + -> abstraction_relation' _ (type.app_curried st x) (type.app_curried v y)). + Proof using abstract_domain'_R_of_related. + apply type.related_hetero_and_Proper_iff_app_curried; eauto; repeat intro; hnf; eauto. + Qed. Local Notation bottom_Proper := (@bottom_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper). Local Notation bottom_for_each_lhs_of_arrow_Proper := (@bottom_for_each_lhs_of_arrow_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper). Local Hint Resolve (@bottom_Proper) (@bottom_for_each_lhs_of_arrow_Proper) : core typeclass_instances. - Fixpoint related_bounded_value {t} : abstract_domain t -> value t -> type.interp base_interp t -> Prop - := match t return abstract_domain t -> value t -> type.interp base_interp t -> Prop with + Lemma bottom_related t v : v == v -> @abstraction_relation t bottom v. + Proof using bottom'_Proper bottom'_related. + induction t; cbv [abstraction_relation]; cbn [type.related_hetero_and_Proper]; cbv [respectful_hetero]; repeat split; eauto. + repeat intro; cbn. + repeat first [ do_with_exactly_one_hyp ltac:(fun H => apply H) + | eassumption + | eapply eqv_refl_of_abstraction_relation ]. + Qed. + + Local Hint Immediate bottom_related : core typeclass_instances. + + Lemma related_bottom_for_each_lhs_of_arrow t v : type.and_for_each_lhs_of_arrow (@type.eqv) v v -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v. + Proof using bottom'_Proper bottom'_related. induction t; cbn; split; split_and; eauto using bottom_related. Qed. + Local Hint Immediate related_bottom_for_each_lhs_of_arrow : core. + + Lemma related_bottom_for_each_lhs_of_arrow_hetero_eqv_l t v v' : type.and_for_each_lhs_of_arrow (@type.eqv) v v' -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v. + Proof using bottom'_Proper bottom'_related. intro; apply related_bottom_for_each_lhs_of_arrow; etransitivity; (idtac + symmetry); eassumption. Qed. + Lemma related_bottom_for_each_lhs_of_arrow_hetero_eqv_r t v v' : type.and_for_each_lhs_of_arrow (@type.eqv) v' v -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v. + Proof using bottom'_Proper bottom'_related. intro; apply related_bottom_for_each_lhs_of_arrow; etransitivity; (idtac + symmetry); eassumption. Qed. + Local Hint Immediate related_bottom_for_each_lhs_of_arrow_hetero_eqv_l related_bottom_for_each_lhs_of_arrow_hetero_eqv_r : core. + + Fixpoint related_bounded_value' {t} : abstract_domain t -> value' t -> type.interp base_interp t -> Prop + := match t return abstract_domain t -> value' t -> type.interp base_interp t -> Prop with | type.base t - => fun st '(e_st, e) v - => abstract_domain'_R t st e_st - /\ expr.interp ident_interp e = v + => fun st e v + => expr.interp ident_interp e = v /\ abstraction_relation' t st v | type.arrow s d => fun st e v => Proper type.eqv v - /\ forall st_s e_s v_s, - let st_s := match s with - | type.base _ => st_s - | type.arrow _ _ => bottom - end in - @related_bounded_value s st_s e_s v_s - -> @related_bounded_value d (st st_s) (UnderLets.interp ident_interp (e e_s)) (v v_s) + /\ Proper abstract_domain_R st + /\ forall st_s e_s v_s, + @related_bounded_value' s st_s e_s v_s + -> @related_bounded_value' d (st st_s) (UnderLets.interp ident_interp (e (st_s, e_s))) (v v_s) end. - Definition related_bounded_value_with_lets {t} : abstract_domain t -> value_with_lets t -> type.interp base_interp t -> Prop - := fun st e v => related_bounded_value st (UnderLets.interp ident_interp e) v. + Definition related_bounded_value {t} : value t -> type.interp base_interp t -> Prop + := fun st_e v => related_bounded_value' (state_of_value st_e) (UnderLets.interp ident_interp (project_value' st_e)) v. - Definition related_of_related_bounded_value {t} st e v - : @related_bounded_value t st e v -> v == v. + Definition related_of_related_bounded_value' {t} st e v + : @related_bounded_value' t st e v -> v == v. Proof using Type. destruct t; [ reflexivity | intros [? ?]; assumption ]. Qed. Lemma abstract_domain'_R_refl_of_rel_l t x y (H : @abstract_domain'_R t x y) @@ -199,43 +253,35 @@ Module Compilers. Local Hint Immediate abstract_domain_R_refl_of_rel_l abstract_domain_R_refl_of_rel_r : core. - Lemma related_bottom_for_each_lhs_of_arrow {t} v - : type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v. - Proof using bottom'_related. induction t; cbn; eauto. Qed. - - Local Hint Immediate related_bottom_for_each_lhs_of_arrow : core. - - Fixpoint fill_in_bottom_for_arrows {t} : abstract_domain t -> abstract_domain t - := match t with - | type.base t => fun x => x - | type.arrow s d - => fun f x => let x := match s with - | type.base _ => x - | type.arrow _ _ => bottom - end in - @fill_in_bottom_for_arrows d (f x) - end. - - Lemma abstract_domain_R_bottom_fill_arrows {t} - : abstract_domain_R (@bottom t) (fill_in_bottom_for_arrows (@bottom t)). - Proof using bottom'_Proper. - cbv [abstract_domain_R]; induction t as [t|s IHs d IHd]; cbn [fill_in_bottom_for_arrows bottom type.related]; - cbv [respectful Proper] in *; auto. + Definition abstract_domain_R_of_related_bounded_value' {t} st e v + : @related_bounded_value' t st e v -> abstract_domain_R st st. + Proof using abstract_domain'_R_of_related. + destruct t; [ cbn; intros [? ?]; subst; eapply abstract_domain'_R_of_related; eassumption | intros [? ?]; destruct_head'_and; assumption ]. Qed. - Lemma fill_in_bottom_for_arrows_bottom_related {t} v - : abstraction_relation (fill_in_bottom_for_arrows (@bottom t)) v. - Proof using bottom'_related. - cbv [abstraction_relation]; induction t; cbn; cbv [respectful_hetero]; eauto. + Lemma abstraction_relation_Proper_iff {t} : Proper (abstract_domain_R ==> type.eqv ==> iff) (@abstraction_relation t). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper. + apply @type.related_hetero_and_Proper_Proper_iff; try exact _. + all: try now repeat intro; split; subst; eapply abstraction_relation'_Proper; (idtac + symmetry); auto; eassumption. + all: try now apply abstract_domain'_R_of_related. Qed. - Hint Resolve fill_in_bottom_for_arrows_bottom_related : core. + Lemma abstraction_relation_Proper_iff_abstract_domain_R {t} : Proper (abstract_domain_R ==> eq ==> iff) (@abstraction_relation t). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper. + repeat intro; subst. + match goal with |- ?A <-> ?B => cut (A \/ B -> (A <-> B)); [ tauto | ] end. + intro H'. + apply abstraction_relation_Proper_iff; try assumption. + destruct_head'_or; eapply eqv_refl_of_abstraction_relation; eassumption. + Qed. - Local Instance fill_in_bottom_for_arrows_Proper {t} : Proper (abstract_domain_R ==> abstract_domain_R) (@fill_in_bottom_for_arrows t). - Proof using bottom'_Proper. - pose proof (@bottom_Proper). - cbv [Proper respectful abstract_domain_R] in *; induction t; cbn in *; cbv [respectful] in *; - intros; break_innermost_match; eauto. + Lemma abstraction_relation_Proper_iff_eqv {t} : Proper (eq ==> type.eqv ==> iff) (@abstraction_relation t). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper. + repeat intro; subst. + match goal with |- ?A <-> ?B => cut (A \/ B -> (A <-> B)); [ tauto | ] end. + intro H'. + apply abstraction_relation_Proper_iff; try assumption. + destruct_head'_or; eapply abstract_domain_R_refl_of_abstraction_relation; eassumption. Qed. Local Instance bottom_eqv_Proper_refl {t} : Proper type.eqv (@bottom t). @@ -245,179 +291,133 @@ Module Compilers. Proof using Type. apply bottom_eqv_Proper_refl. Qed. Local Hint Resolve bottom_eqv_refl : core. - Local Instance fill_in_bottom_for_arrows_Proper_eqv {t} : Proper (type.eqv ==> type.eqv) (@fill_in_bottom_for_arrows t). - Proof using Type. - cbv [Proper respectful] in *; induction t; cbn in *; cbv [respectful] in *; - intros; break_innermost_match; cbn in *; cbv [respectful] in *; eauto. - Qed. - - Lemma state_of_value_related_fill {t} v (HP : Proper abstract_domain_R (@state_of_value t v)) - : abstract_domain_R (@state_of_value t v) (fill_in_bottom_for_arrows (@state_of_value t v)). - Proof using bottom'_Proper. destruct t; [ assumption | apply abstract_domain_R_bottom_fill_arrows ]. Qed. - - Lemma eqv_bottom_fill_bottom {t} - : @bottom t == fill_in_bottom_for_arrows bottom. - Proof using Type. induction t; cbn; [ reflexivity | ]; cbv [respectful]; auto. Qed. - - Lemma eqv_fill_bottom_idempotent {t} v1 v2 - : v1 == v2 -> fill_in_bottom_for_arrows (fill_in_bottom_for_arrows v1) == @fill_in_bottom_for_arrows t v2. - Proof using Type. induction t; cbn; cbv [respectful]; break_innermost_match; auto. Qed. - - Lemma abstract_domain_R_fill_bottom_idempotent {t} v1 v2 - : abstract_domain_R v1 v2 - -> abstract_domain_R (fill_in_bottom_for_arrows (fill_in_bottom_for_arrows v1)) - (@fill_in_bottom_for_arrows t v2). - Proof using bottom'_Proper. - pose proof (@bottom_Proper) as Hb. - induction t as [|s IHs d IHd]; cbn; cbv [respectful Proper abstract_domain_R] in *; break_innermost_match; auto. + Lemma related_refl_of_related_bounded_value' {t} st e v + : @related_bounded_value' t st e v -> abstract_domain_R st st. + Proof using abstract_domain'_R_of_related. + destruct t; cbn; break_innermost_match; intros; destruct_head'_and; try assumption. + eapply abstract_domain'_R_of_related; eassumption. Qed. - Lemma app_curried_state_of_value_fill {t} v x y - (H : type.and_for_each_lhs_of_arrow (@type.eqv) x y) - : type.app_curried (@state_of_value t v) x = type.app_curried (fill_in_bottom_for_arrows (@state_of_value t v)) y. - Proof using Type. - destruct t; [ reflexivity | cbv [state_of_value] ]. - apply type.app_curried_Proper; [ apply eqv_bottom_fill_bottom | assumption ]. - Qed. - - Lemma first_order_app_curried_fill_in_bottom_for_arrows_eq {t} f xs - (Ht : type.is_not_higher_order t = true) - : type.app_curried (t:=t) f xs = type.app_curried (fill_in_bottom_for_arrows f) xs. - Proof using Type. - clear -Ht. - induction t as [| [|s' d'] IHs d IHd]; cbn in *; try discriminate; auto. - Qed. - - Lemma first_order_abstraction_relation_fill_in_bottom_for_arrows_iff - {t} f v - (Ht : type.is_not_higher_order t = true) - : @abstraction_relation t f v - <-> @abstraction_relation t (fill_in_bottom_for_arrows f) v. - Proof using Type. - clear -Ht; cbv [abstraction_relation]. - split; induction t as [| [|s' d'] IHs d IHd]; - cbn in *; cbv [respectful_hetero]; try discriminate; auto. - Qed. - - Lemma related_state_of_value_of_related_bounded_value {t} st e v - : @related_bounded_value t st e v -> abstract_domain_R match t with - | type.base _ => st - | type.arrow _ _ => bottom - end (state_of_value e). - Proof using bottom'_Proper. intro H; destruct t; cbn in *; [ destruct e; apply H | repeat intro; refine bottom_Proper ]. Qed. - - Lemma related_state_of_value_of_related_bounded_value2 {t} st e v (st' := match t with - | type.base _ => st - | type.arrow _ _ => bottom - end) - : @related_bounded_value t st' e v -> abstract_domain_R st' (state_of_value e). - Proof using bottom'_Proper. intro H; destruct t; cbn in *; [ destruct e; apply H | repeat intro; refine bottom_Proper ]. Qed. - - Lemma related_bounded_value_Proper {t} st1 st2 (Hst : abstract_domain_R (fill_in_bottom_for_arrows st1) (fill_in_bottom_for_arrows st2)) + Lemma related_bounded_value'_Proper {t} st1 st2 (Hst : abstract_domain_R st1 st2) a a1 a2 (Ha' : type.eqv a1 a2) - : @related_bounded_value t st1 a a1 -> @related_bounded_value t st2 a a2. - Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper. - induction t as [t|s IHs d IHd]; cbn [related_bounded_value type.related] in *; cbv [respectful abstract_domain_R] in *. - all: cbn [type.andb_each_lhs_of_arrow] in *. - all: rewrite ?Bool.andb_true_iff in *. - all: destruct_head'_and. - { intros; break_innermost_match; subst; - destruct_head'_and; repeat apply conj; auto. - { etransitivity; (idtac + symmetry); eassumption. } - { eapply abstraction_relation'_Proper; (eassumption + reflexivity). } } + : @related_bounded_value' t st1 a a1 -> @related_bounded_value' t st2 a a2. + Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric abstract_domain'_R_of_related. + induction t as [t|s IHs d IHd]; cbn [related_bounded_value' type.related] in *; cbv [respectful abstract_domain_R] in *. + all: subst. + { intros; destruct_head'_and; subst; repeat apply conj; try reflexivity. + eapply abstraction_relation'_Proper; (eassumption + reflexivity). } { intros [? Hrel]. - split; [ repeat intro; etransitivity; (idtac + symmetry); eapply Ha'; (eassumption + (etransitivity; (idtac + symmetry); eassumption)) | ]. - pose proof (@bottom_Proper s) as Hsbot. - intros ?? v_s; destruct s; intros Hx; cbn [type.related] in *; - cbn [fill_in_bottom_for_arrows] in *; cbv [respectful] in *. - { specialize_by_assumption; cbn in *. - eapply IHd; [ cbn in Hst |- *; eapply Hst | apply Ha'; reflexivity | eapply Hrel, Hx ]; cbv [respectful]. - cbn [related_bounded_value] in *. - break_innermost_match_hyps; destruct_head'_and. - eauto. } - { eapply IHd; [ eapply Hst | apply Ha' | eapply Hrel, Hx ]; - [ eexact Hsbot | refine (@related_of_related_bounded_value _ _ _ v_s _); eassumption | refine bottom ]. } } + split; [ | split ]; + [ repeat intro; etransitivity; (idtac + symmetry); (eapply Ha' + eapply Hst); (eassumption + (etransitivity; (idtac + symmetry); eassumption)) .. + | ]. + { intros ?? v_s Hx; cbn [type.related] in *; cbv [respectful] in *. + eapply IHd; [ cbn in Hst |- *; eapply Hst | apply Ha' | eapply Hrel, Hx ]. + all: try now eapply related_refl_of_related_bounded_value'; eassumption. + all: try now eapply related_of_related_bounded_value'; eassumption. } } Qed. - Lemma related_bounded_value_fill_bottom_iff {t} st1 st2 (Hst : abstract_domain_R st1 st2) - a a1 a2 - (Ha' : type.eqv a1 a2) - : @related_bounded_value t st1 a a1 <-> @related_bounded_value t (fill_in_bottom_for_arrows st2) a a2. - Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper. - split; eapply related_bounded_value_Proper; try solve [ (idtac + symmetry); assumption ]. - all: (idtac + symmetry); apply abstract_domain_R_fill_bottom_idempotent. - all: (idtac + symmetry); assumption. + Lemma related_bounded_value'_Proper1 {t} + : Proper (abstract_domain_R ==> eq ==> eq ==> Basics.impl) (@related_bounded_value' t). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper. + repeat intro; subst; eapply related_bounded_value'_Proper; try eassumption. + eapply related_of_related_bounded_value'; eassumption. Qed. - Lemma related_bounded_value_Proper1 {t} - : Proper (abstract_domain_R ==> eq ==> eq ==> Basics.impl) (@related_bounded_value t). - Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper. - repeat intro; subst; eapply related_bounded_value_Proper. - { eapply fill_in_bottom_for_arrows_Proper; eassumption. } - { eapply related_of_related_bounded_value; eassumption. } - { assumption. } + Lemma related_bounded_value'_Proper3 {t} + : Proper (eq ==> eq ==> type.eqv ==> Basics.impl) (@related_bounded_value' t). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper. + repeat intro; subst; eapply related_bounded_value'_Proper; try eassumption. + eapply abstract_domain_R_of_related_bounded_value'; eassumption. Qed. - Lemma related_bounded_value_Proper_eq {t} - : Proper (eq ==> eq ==> eq ==> Basics.impl) (@related_bounded_value t). + Lemma related_bounded_value'_Proper_eq {t} + : Proper (eq ==> eq ==> eq ==> Basics.impl) (@related_bounded_value' t). Proof using Type. repeat intro; subst; assumption. Qed. - Lemma related_bounded_value_Proper_interp_eq_base {t} - : Proper (eq ==> RelProd eq (fun x y => expr.interp ident_interp x = expr.interp ident_interp y) ==> eq ==> Basics.impl) (@related_bounded_value (type.base t)). + Lemma related_bounded_value'_Proper_interp_eq_base {t} + : Proper (eq ==> (fun x y => expr.interp ident_interp x = expr.interp ident_interp y) ==> eq ==> Basics.impl) (@related_bounded_value' (type.base t)). Proof using Type. repeat intro; subst. - cbv [value RelProd relation_conjunction predicate_intersection pointwise_extension RelCompFun] in *. - destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *; subst. - cbv [related_bounded_value] in *; destruct_head'_and; repeat apply conj; subst; (idtac + symmetry); assumption. + cbv [related_bounded_value'] in *; destruct_head'_and; repeat apply conj; subst; (idtac + symmetry); assumption. + Qed. + + Lemma state_of_value_reflect is_let_bound {t} e st + : state_of_value (@reflect is_let_bound t e st) = st. + Proof using Type. destruct t; reflexivity. Qed. + + Lemma related_bounded_value'_of_abstraction_relation_of_reflect + {t} {annotate_with_state} + (interp_reflect + : forall st e v + (H_val : expr.interp ident_interp e == v) + (Hst1 : abstraction_relation st (expr.interp ident_interp e)), + related_bounded_value + (@reflect annotate_with_state t e st) + v) + st v + (H : abstraction_relation st v) + : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect annotate_with_state t (expr.Var v) st))) v. + Proof using Type. + specialize (interp_reflect st (expr.Var v) v). + cbv [related_bounded_value] in interp_reflect. + rewrite state_of_value_reflect in interp_reflect. + apply interp_reflect; try assumption. + eapply eqv_refl_of_abstraction_relation; eassumption. Qed. Fixpoint interp_reify - annotate_with_state is_let_bound {t} st e v b_in - (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in) - (H : related_bounded_value st e v) {struct t} - : (forall arg1 arg2 - (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) - (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1), - type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1 - = type.app_curried v arg2) - /\ (forall arg1 - (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1) - (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1), - abstraction_relation' - _ - (type.app_curried (fill_in_bottom_for_arrows st) b_in) - (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1)) + annotate_with_state is_let_bound {t} e v b_in + (H : related_bounded_value e v) + {struct t} + : forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) + (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1), + type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1 + = type.app_curried v arg2 with interp_reflect annotate_with_state {t} st e v - (Hst_Proper : Proper abstract_domain_R st) + (*(Hst_Proper : Proper abstract_domain_R st)*) (* follows from abstraction relation *) (H_val : expr.interp ident_interp e == v) - (Hst1 : abstraction_relation (fill_in_bottom_for_arrows st) (expr.interp ident_interp e)) + (Hst1 : abstraction_relation st (expr.interp ident_interp e)) {struct t} : related_bounded_value - st (@reflect annotate_with_state t e st) - v. - Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric. + v + with abstraction_relation_of_related_bounded_value' + {t} st e v + {struct t} + : @related_bounded_value' t st e v + -> abstraction_relation st v. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate. all: destruct t as [t|s d]; - [ clear interp_reify interp_reflect - | pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound s) as interp_reify_s; - pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound d) as interp_reify_d; - pose proof (interp_reflect annotate_with_state s) as interp_reflect_s; - pose proof (interp_reflect annotate_with_state d) as interp_reflect_d; - clear interp_reify interp_reflect; - pose proof (@abstract_domain_R_bottom_fill_arrows s); - pose proof (@abstract_domain_R_bottom_fill_arrows d) ]. + [ clear interp_reify interp_reflect abstraction_relation_of_related_bounded_value' + | pose proof (fun annotate_with_state is_let_bound => interp_reify annotate_with_state is_let_bound s) as interp_reify_s; + pose proof (fun annotate_with_state is_let_bound => interp_reify annotate_with_state is_let_bound d) as interp_reify_d; + pose proof (fun annotate_with_state => interp_reflect annotate_with_state s) as interp_reflect_s; + pose proof (fun annotate_with_state => interp_reflect annotate_with_state d) as interp_reflect_d; + pose proof (abstraction_relation_of_related_bounded_value' s) as abstraction_relation_of_related_bounded_value'_s; + pose proof (abstraction_relation_of_related_bounded_value' d) as abstraction_relation_of_related_bounded_value'_d; + pose proof (@related_bounded_value'_of_abstraction_relation_of_reflect s false (interp_reflect_s false)) as related_bounded_value'_of_abstraction_relation_s; + pose proof (@related_bounded_value'_of_abstraction_relation_of_reflect d false (interp_reflect_d false)) as related_bounded_value'_of_abstraction_relation_d; + try specialize (interp_reify_s annotate_with_state); + try specialize (interp_reify_d annotate_with_state); + try specialize (interp_reflect_s annotate_with_state); + try specialize (interp_reflect_d annotate_with_state); + clear interp_reify interp_reflect abstraction_relation_of_related_bounded_value' ]. + all: cbv [abstraction_relation] in *; cbn [type.related_hetero_and_Proper] in *; cbv [respectful_hetero] in *. all: cbn [reify reflect] in *; fold (@reify) (@reflect) in *. - all: cbn [related_bounded_value type.related type.app_curried] in *. - all: cbn [UnderLets.interp expr.interp type.final_codomain type.andb_each_lhs_of_arrow type.is_base fst snd fill_in_bottom_for_arrows type.map_for_each_lhs_of_arrow type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow partial.bottom_for_each_lhs_of_arrow partial.bottom] in *. - all: destruct annotate_with_state; try destruct is_let_bound. + all: cbn [related_bounded_value' type.related type.app_curried] in *. + all: cbn [UnderLets.interp expr.interp type.final_codomain type.andb_each_lhs_of_arrow type.is_base fst snd type.map_for_each_lhs_of_arrow type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow partial.bottom_for_each_lhs_of_arrow partial.bottom] in *. + all: try destruct annotate_with_state; try destruct is_let_bound. + all: change (type.related_hetero_and_Proper abstract_domain'_R (fun t : base_type => eq) abstraction_relation' (t:=?t)) with (@abstraction_relation t) in *. all: repeat first [ reflexivity + | assumption | progress eta_expand - | progress cbv [type.is_not_higher_order] in * | progress cbn [UnderLets.interp expr.interp type.final_codomain fst snd] in * + | progress cbn [state_of_value project_value' fst snd Base_value' UnderLets.interp] in * | progress subst | progress destruct_head'_and | progress destruct_head'_prod @@ -437,84 +437,102 @@ Module Compilers. | match goal with | [ H : fst ?x = _ |- _ ] => is_var x; destruct x | [ H : Proper _ ?st |- ?R (?st _) (?st _) ] => apply H - | [ |- ?R (state_of_value _) (state_of_value _) ] => cbv [state_of_value] in * + | [ |- type.related _ ?x ?x ] + => eapply related_refl_of_related_bounded_value'; eassumption + end + | match goal with + | [ H' : ?R ?i, H : forall a b, ?R a /\ @?A b -> @?B b |- _ ] + => specialize (fun b H'' => H i b (conj H' H'')) + | [ H' : ?R ?i, H : forall a b, @?A a /\ ?R b -> @?B a |- _ ] + => specialize (fun a H'' => H a i (conj H'' H')) end | solve [ repeat intro; apply bottom_Proper - | auto; cbv [Proper respectful Basics.impl] in *; eauto ] + | auto; cbv [Proper respectful Basics.impl] in *; eauto + | eapply related_refl_of_related_bounded_value'; eassumption + | eapply related_bottom_for_each_lhs_of_arrow, eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow; eassumption + | eapply abstract_domain_R_refl_of_abstraction_relation; eassumption ] | progress (repeat apply conj; intros * ) | progress intros | progress destruct_head'_or - | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H); - try assumption; auto; [] | match goal with | [ |- Proper ?R _ ] => (eapply PER_valid_l + eapply PER_valid_r); eassumption - | [ |- @related_bounded_value ?t ?st1 (reflect _ _ ?st2) _ ] - => (tryif first [ constr_eq st1 st2 | has_evar st1 | has_evar st2 ] - then fail - else (eapply (@related_bounded_value_Proper1 t st2 st1); - try reflexivity)) | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry; assumption end - | break_innermost_match_step - | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H); - try assumption; auto | match goal with - | [ |- abstraction_relation (fill_in_bottom_for_arrows (?f (state_of_value ?e))) _ ] - => replace (state_of_value e) with (match s with - | type.base _ => state_of_value e - | type.arrow _ _ => bottom - end) by (destruct s; reflexivity) + | [ H : related_bounded_value' ?st ?e ?v |- related_bounded_value' ?st ?e' ?v' ] + => is_evar e'; unify e e'; + eapply related_bounded_value'_Proper3; [ reflexivity .. | symmetry | exact H ] + | [ H' : abstraction_relation ?stv ?vv, H : forall annotate_with_state st e v, _ == v -> abstraction_relation st (expr.interp _ e) -> related_bounded_value (reflect annotate_with_state e st) v |- related_bounded_value' ?stv ?ee ?vv ] + => is_evar ee; + specialize (H false stv (expr.Var vv) vv); + cbv [related_bounded_value] in H; + rewrite state_of_value_reflect in H; eapply H; clear H end - | progress fold (@reify) (@reflect) (@type.interp) (@type.related) (@type.related_hetero) in * + | break_innermost_match_step + | progress fold (@reify) (@reflect) (@type.interp) (@type.related) (@type.related_hetero) (@related_bounded_value') (@abstraction_relation) in * | match goal with + | [ H : forall a b c d e (f : bool), _ |- _ ] + => unique pose proof (fun a b c d e => H a b c d e true); + unique pose proof (fun a b c d e => H a b c d e false); + clear H | [ |- type.related _ (expr.interp _ (UnderLets.interp _ (reify _ _ _ _))) _ ] => rewrite type.related_iff_app_curried - | [ |- type.related_hetero _ (@state_of_value ?t _) _ ] - => is_var t; destruct t; cbv [state_of_value]; [ cbn | apply bottom_related ] - end ]. + | [ interp_reflect_d : context[_ -> related_bounded_value (reflect _ _ _) _] |- related_bounded_value' ?st (UnderLets.interp _ (project_value' (reflect _ ?e ?st))) ?v ] + => specialize (interp_reflect_d st e v); + cbv [related_bounded_value] in interp_reflect_d; + rewrite state_of_value_reflect in interp_reflect_d + | [ H : context[_ -> type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b _ _ _))) _ = _] |- type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b ?is_let_bound ?e ?b_in))) ?arg = _ ] + => apply H; clear H + | [ H : context[_ -> abstraction_relation' _ (type.app_curried _ _) (type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b _ _ _))) _)] + |- abstraction_relation' _ (type.app_curried _ ?x) (type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b ?is_let_bound ?e ?b_in))) ?arg) ] + => specialize (H is_let_bound e); cbn [state_of_value Base_value' fst] in H; + eapply H; clear H + | [ |- related_bounded_value (_, Base _) _ ] => hnf; cbn [state_of_value project_value' Base_value' UnderLets.interp fst snd] + | [ H : forall st e v, _ -> related_bounded_value' _ (UnderLets.interp _ (?u _)) _ |- related_bounded_value' _ (UnderLets.interp _ (?u _)) _ ] + => apply H; clear H + | [ H : context[_ -> related_bounded_value' _ _ _ -> abstraction_relation _ _] |- abstraction_relation _ _ ] + => eapply H; clear H + end + | match goal with + | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b)) + end + | rewrite state_of_value_reflect + | rewrite type.related_hetero_iff_app_curried + | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) ]. Qed. - Lemma interp_reify_first_order - annotate_with_state is_let_bound {t} st e v b_in - (Ht : type.is_not_higher_order t = true) - (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in) - (H : related_bounded_value st e v) - : (forall arg1 arg2 - (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) - (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1), - type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1 - = type.app_curried v arg2) - /\ (forall arg1 - (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1) - (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1), - abstraction_relation' - _ - (type.app_curried st b_in) - (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1)). - Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric. - rewrite first_order_app_curried_fill_in_bottom_for_arrows_eq by assumption. - apply interp_reify; assumption. + Lemma related_bounded_value'_of_abstraction_relation_annotate_with_state + {t} {annotate_with_state} st v + (H : abstraction_relation st v) + : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect annotate_with_state t (expr.Var v) st))) v. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate. + apply related_bounded_value'_of_abstraction_relation_of_reflect; try assumption. + apply @interp_reflect. Qed. - Lemma interp_reflect_first_order - annotate_with_state {t} st e v - (Ht : type.is_not_higher_order t = true) - (Hst_Proper : Proper abstract_domain_R st) - (H_val : expr.interp ident_interp e == v) - (Hst : abstraction_relation st (expr.interp ident_interp e)) - : related_bounded_value - st - (@reflect annotate_with_state t e st) - v. - Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric. - rewrite first_order_abstraction_relation_fill_in_bottom_for_arrows_iff in Hst by assumption. - apply interp_reflect; assumption. + Lemma related_bounded_value'_of_abstraction_relation + {t} st v + (H : abstraction_relation st v) + : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect false t (expr.Var v) st))) v. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate. + apply related_bounded_value'_of_abstraction_relation_annotate_with_state; assumption. + Qed. + + Lemma abstraction_relation_of_related_bounded_value'_app_curried + {t} st e v b_in arg + (H : @related_bounded_value' t st e v) + (Harg : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg) + : abstraction_relation' _ (type.app_curried st b_in) (type.app_curried v arg). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate. + pose proof (@abstraction_relation_of_related_bounded_value' t st e v H) as H'. + rewrite abstraction_relation_iff_app_curried in H'. + apply H'; assumption. Qed. Lemma related_bounded_value_annotate_base {t} v_st st v - : @related_bounded_value (type.base t) v_st st v - -> @related_bounded_value (type.base t) v_st (fst st, UnderLets.interp ident_interp (annotate true t (fst st) (snd st))) v. + : @related_bounded_value' (type.base t) v_st st v + -> @related_bounded_value' (type.base t) v_st (UnderLets.interp ident_interp (annotate true t v_st st)) v. Proof using interp_annotate abstraction_relation'_Proper. clear -interp_annotate abstraction_relation'_Proper. cbv [Proper respectful Basics.impl] in *. @@ -523,136 +541,157 @@ Module Compilers. rewrite interp_annotate by eauto; reflexivity. Qed. - Lemma related_bounded_value_bottomify {t} v_st st v - : @related_bounded_value t v_st st v - -> @related_bounded_value t bottom (UnderLets.interp ident_interp (bottomify st)) v. - Proof using bottom'_Proper bottom'_related. - induction t; cbn in *; - repeat first [ progress subst - | progress cbv [respectful] in * - | progress cbn [UnderLets.interp] in * - | progress destruct_head'_and - | break_innermost_match_step - | progress intros - | apply conj - | reflexivity - | apply bottom'_Proper - | apply bottom'_related - | solve [ eauto ] - | rewrite UnderLets.interp_splice ]. + Lemma interp_extract_gen_from_wf_gen G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> abstract_domain_R v1 v2) + {t} (e1 e2 : expr t) b_in1 b_in2 + (Hwf : expr.wf G e1 e2) + (Hb_in : type.and_for_each_lhs_of_arrow (@abstract_domain_R) b_in1 b_in2) + : abstract_domain'_R _ (extract_gen e1 b_in1) (extract_gen e2 b_in2). + Proof using abstract_interp_ident_Proper. + cbv [extract_gen]. + eapply type.related_iff_app_curried; try assumption. + unshelve eapply expr.wf_interp_Proper_gen1; try eassumption. + + Qed. + + Lemma interp_extract_gen_from_wf + {t} (e1 e2 : expr t) b_in1 b_in2 + (Hwf : expr.wf nil e1 e2) + (Hb_in : type.and_for_each_lhs_of_arrow (@abstract_domain_R) b_in1 b_in2) + : abstract_domain'_R _ (extract_gen e1 b_in1) (extract_gen e2 b_in2). + Proof using abstract_interp_ident_Proper. + eapply interp_extract_gen_from_wf_gen; try eassumption; wf_t. Qed. Context (interp_ident_Proper : forall annotate_with_state t idc, - related_bounded_value (ident_extract t idc) (UnderLets.interp ident_interp (interp_ident annotate_with_state t idc)) (ident_interp t idc)). + related_bounded_value (interp_ident annotate_with_state idc) (ident_interp t idc)). Lemma interp_interp - annotate_with_state G G' {t} (e_st e1 e2 e3 : expr t) - (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G - -> related_bounded_value_with_lets v1 v2 v3) - (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> v1 == v2) - (Hwf : expr.wf3 G e_st e1 e2) - (Hwf' : expr.wf G' e2 e3) - : related_bounded_value_with_lets - (extract' e_st) - (interp annotate_with_state e1) - (expr.interp (@ident_interp) e2). - Proof using interp_ident_Proper interp_annotate abstraction_relation'_Proper ident_interp_Proper' abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related. - clear -ident_interp_Proper' interp_ident_Proper interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related HG HG' Hwf Hwf'. - cbv [related_bounded_value_with_lets] in *; - revert dependent annotate_with_state; revert dependent G'; induction Hwf; intros; - cbn [extract' interp expr.interp UnderLets.interp List.In related_bounded_value reify reflect] in *; cbv [Let_In] in *. + annotate_with_state G G' G'' G''' {t} (e e_st e_v : expr t) + (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G + -> related_bounded_value v2 v3 + /\ abstract_domain_R v1 (state_of_value v2)) + (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> abstract_domain_R (state_of_value v1) v2) + (HG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G'' -> v1 == v2) + (HG''' : forall t v1 v2, List.In (existT _ t (v1, v2)) G''' -> abstract_domain_R v1 v2) + (Hwf : expr.wf3 G e_st e e_v) + (Hwf' : expr.wf G' e e_st) + (Hwf'' : expr.wf G'' e_v e_v) + (Hwf''' : expr.wf G''' e_st e_st) + : related_bounded_value + (interp annotate_with_state e e_st) + (expr.interp (@ident_interp) e_v) + /\ abstract_domain_R (expr.interp (@abstract_interp_ident) e_st) (state_of_value (interp annotate_with_state e e_st)). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct. + clear -abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct HG HG' HG'' HG''' Hwf Hwf' Hwf'' Hwf'''. + cbv [related_bounded_value] in *; + revert dependent annotate_with_state; revert dependent G'; revert dependent G''; revert dependent G'''; induction Hwf; intros. all: destruct annotate_with_state eqn:?. + all: cbn [interp expr.interp UnderLets.interp List.In related_bounded_value' reify reflect abstract_domain_R type.related] in *; cbv [Let_In Proper respectful] in *; cbn [state_of_value Base_value' fst snd] in *. + all: repeat apply conj; intros. all: repeat first [ progress intros | progress subst | progress inversion_sigma - | progress inversion_prod - | progress destruct_head'_and - | progress destruct_head'_or + | progress inversion_pair | progress destruct_head'_sig - | progress destruct_head'_sigT - | progress destruct_head'_prod + | progress destruct_head'_and | progress eta_expand - | exfalso; assumption - | progress cbn [UnderLets.interp List.In eq_rect fst snd projT1 projT2] in * + | progress cbv [interp_ident] in * + | progress cbn [eq_rect UnderLets.interp project_value' state_of_value fst snd Base_value' List.In apply_value] in * + | progress eliminate_hprop_eq + | apply related_bounded_value_annotate_base + | eapply abstract_domain_R_of_related_bounded_value'; eassumption + | eapply related_of_related_bounded_value'; eassumption + | solve [ cbv [abstract_domain_R] in *; (idtac + symmetry); eauto ] + | progress split_and + | erewrite invert_default_Some by first [ eassumption | reflexivity ] + | erewrite invert_default'_Some by first [ eassumption | reflexivity ] | rewrite UnderLets.interp_splice - | rewrite interp_annotate - | solve [ cbv [Proper respectful Basics.impl] in *; unshelve eauto using related_of_related_bounded_value, related_bounded_value_bottomify ] - | progress specialize_by_assumption - | progress cbv [Let_In] in * - | progress cbn [state_of_value extract'] in * - | progress expr.invert_subst - | match goal with - | [ |- abstract_domain ?t ] => exact (@bottom t) - | [ H : expr.wf _ _ _ |- Proper type.eqv _ ] - => apply expr.wf_interp_Proper_gen1 in H; - [ cbv [Proper]; etransitivity; (idtac + symmetry); exact H | auto ] - | [ H : _ |- _ ] - => (tryif first [ constr_eq H HG | constr_eq H HG' ] - then fail - else (apply H; clear H)) - | [ |- related_bounded_value _ (fst _, UnderLets.interp _ (annotate _ _ _ _)) _ ] - => apply related_bounded_value_annotate_base - | [ H : context[match ?v with None => _ | _ => _ end] |- _ ] => destruct v eqn:? - | [ H : context[@related_bounded_value (type.base ?t) ?x _ ?y] - |- @related_bounded_value (type.base ?t) ?x _ ?y ] - => eapply related_bounded_value_Proper_interp_eq_base; [ reflexivity | split; hnf | reflexivity | eapply H ]; - cbn [fst snd expr.interp]; - [ reflexivity | reflexivity | .. ] - end - | apply conj + | progress destruct_head'_or + | eapply expr.wf_interp_Proper_gen1; [ | now eauto ] | match goal with - | [ H : _ = _ |- _ ] => rewrite H + | [ |- _ /\ _ ] => split end - | break_innermost_match_step - | progress expr.inversion_wf_one_constr + | progress expr.inversion_wf_constr + | do_with_hyp' ltac:(fun H => now apply H; first [ eapply related_of_related_bounded_value' | eapply related_refl_of_related_bounded_value' ]; eauto) | match goal with - | [ H : _ |- _ ] - => (tryif first [ constr_eq H HG | constr_eq H HG' ] - then fail - else (eapply H; clear H; - [ lazymatch goal with - | [ |- expr.wf _ _ _ ] - => solve [ eassumption - | match goal with - | [ H : forall v1 v2, expr.wf _ _ _ |- expr.wf _ (?f ?x) _ ] - => apply (H x x) - end ] - | [ |- bool ] (* unused [annotate_with_state] argument to a [Proper ... /\ ...] lemma which is used for its [Proper] part *) - => constructor - | _ => idtac - end .. ]; - match goal with - [ |- ?G ] => assert_fails has_evar G - end)) + | [ H : context[related_bounded_value' _ (UnderLets.interp _ (project_value' (interp _ (?f2 _) (?f1 _)))) (expr.interp _ (?f3 _))] + |- related_bounded_value' _ (UnderLets.interp _ (project_value' (interp _ (?f2 _) (?f1 _)))) (expr.interp _ (?f3 _)) ] + => first [ eapply H + | eapply related_bounded_value'_Proper1; [ | reflexivity .. | eapply H ] ]; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => solve [ eauto ] + | _ => idtac + end; + clear H + | [ H : context[related_bounded_value' _ (UnderLets.interp _ (UnderLets.interp _ (project_value' (interp _ ?f2 ?f1)) _)) (expr.interp _ ?f3 _)] + |- related_bounded_value' _ (UnderLets.interp _ (UnderLets.interp _ (project_value' (interp _ ?f2 ?f1)) _)) (expr.interp _ ?f3 _) ] + => first [ eapply H + | eapply related_bounded_value'_Proper1; [ | reflexivity .. | eapply H ] ]; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => solve [ eauto ] + | _ => idtac + end; + clear H + | [ H : context[abstract_domain_R (expr.interp _ (?f1 _)) (state_of_value (interp _ (?f2 _) (?f1 _)))] + |- abstract_domain_R (expr.interp _ (?f1 _)) (state_of_value (interp _ (?f2 _) (?f1 _))) ] + => first [ eapply H; clear H + | etransitivity; [ | eapply H; clear H ] ]; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => solve [ eauto ] + | _ => idtac + end + | [ H : context[type.related abstract_domain'_R (expr.interp _ ?f1 _) (state_of_value (interp _ ?f2 ?f1) _)] + |- abstract_domain_R (expr.interp _ ?f1 _) (state_of_value (interp _ ?f2 ?f1) _) ] + => eapply H; clear H; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => solve [ eauto ] + | _ => idtac + end + | [ H : context[_ -> abstract_domain_R _ (state_of_value (interp _ ?f _))] + |- abstract_domain_R (state_of_value (interp _ ?f ?x)) (state_of_value (interp _ ?f ?x)) ] + => etransitivity; [ symmetry | ]; eapply H; clear H; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => solve [ eauto ] + | _ => idtac + end + | [ |- abstract_domain_R (state_of_value _) (expr.interp _ _) ] => symmetry end - | reflexivity ]. + | progress repeat first [ progress eta_expand | break_innermost_match_step ] ]. Qed. Lemma interp_eval_with_bound' - annotate_with_state {t} (e_st e1 e2 : expr t) - (Hwf : expr.wf3 nil e_st e1 e2) - (Hwf' : expr.wf nil e2 e2) - (Ht : type.is_not_higher_order t = true) + annotate_with_state {t} (e e_st e_v : expr t) + (Hwf : expr.wf3 nil e_st e e_v) + (Hwf' : expr.wf nil e e_st) + (Hwf'' : expr.wf nil e_v e_v) + (Hwf''' : expr.wf nil e_st e_st) (st : type.for_each_lhs_of_arrow abstract_domain t) - (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st) : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1), - type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1 - = type.app_curried (expr.interp ident_interp e2) arg2) + type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e e_st st)) arg1 + = type.app_curried (expr.interp ident_interp e_v) arg2) /\ (forall arg1 (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1) (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1), abstraction_relation' _ (extract_gen e_st st) - (type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1)). - Proof using interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_related interp_ident_Proper bottom'_Proper ident_interp_Proper'. - cbv [extract_gen extract' eval_with_bound']. - split; intros; rewrite UnderLets.interp_to_expr, UnderLets.interp_splice. - all: eapply interp_reify_first_order; eauto. - all: eapply interp_interp; eauto; wf_t. + (type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e e_st st)) arg1)). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper bottom'_Proper bottom'_related ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct. + cbv [extract_gen eval_with_bound']. + split; intros; rewrite UnderLets.interp_to_expr. + { apply interp_reify; eauto; []. + eapply interp_interp; eauto; wf_t. } + { erewrite interp_reify; try eassumption. + { eapply abstraction_relation_of_related_bounded_value'_app_curried; try assumption; []. + eapply related_bounded_value'_Proper1; [ .. | eapply interp_interp ]; try reflexivity; try eassumption; eauto; wf_t; []. + symmetry; eapply interp_interp; try eassumption; wf_t. } + { now eapply interp_interp; eauto; wf_t. } } + Unshelve. + all: exact true. Qed. Lemma interp_eta_expand_with_bound' @@ -664,38 +703,12 @@ Module Compilers. (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1), type.app_curried (expr.interp ident_interp (eta_expand_with_bound' e1 b_in)) arg1 = type.app_curried (expr.interp ident_interp e2) arg2. - Proof using interp_annotate ident_interp_Proper' bottom'_related abstraction_relation'_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related ident_interp_Proper' interp_annotate. cbv [eta_expand_with_bound']. intros; rewrite UnderLets.interp_to_expr. eapply interp_reify; eauto. - eapply interp_reflect; eauto using bottom_related. - eapply @expr.wf_interp_Proper_gen; auto using Hwf. - Qed. - - Lemma interp_extract'_from_wf_gen G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> abstract_domain_R v1 v2) - {t} (e1 e2 : expr t) - (Hwf : expr.wf G e1 e2) - : abstract_domain_R (extract' e1) (extract' e2). - Proof using ident_extract_Proper bottom'_Proper. - cbv [abstract_domain_R] in *; induction Hwf; cbn [extract']; break_innermost_match. - all: repeat first [ progress subst - | progress inversion_sigma - | progress inversion_prod - | solve [ cbv [Proper respectful] in *; eauto ] - | progress cbv [respectful Let_In] in * - | progress cbn [type.related List.In eq_rect partial.bottom] in * - | progress intros - | progress destruct_head'_or - | apply bottom_Proper - | match goal with H : _ |- type.related _ _ _ => apply H; clear H end ]. - Qed. - - Lemma interp_extract'_from_wf {t} (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : abstract_domain_R (extract' e1) (extract' e2). - Proof using ident_extract_Proper bottom'_Proper. - eapply interp_extract'_from_wf_gen; revgoals; wf_t. + eapply interp_reflect; try (apply bottom_related; etransitivity; [ | symmetry ]). + all: eapply @expr.wf_interp_Proper_gen; [ | exact Hwf ]; auto. Qed. End with_type. @@ -714,19 +727,20 @@ Module Compilers. (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A))) (is_annotated_for : forall t t', @expr var t -> abstract_domain' t' -> bool) (skip_annotations_under : forall t, ident t -> bool) - (strip_annotation : forall t, ident t -> option (@value base.type ident var abstract_domain' t)) + (strip_annotation : forall t, ident t -> option (@value' base.type ident var abstract_domain' t)) (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop) (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop) (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t)) (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v) {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} {abstract_domain'_R_transitive : forall t, Transitive (@abstract_domain'_R t)} - {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)}. - Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation'). + {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)} + (abstract_domain'_R_of_related : forall t st v, @abstraction_relation' t st v -> @abstract_domain'_R t st st). + Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation' abstract_domain'_R). Local Notation ident_interp := ident.interp (only parsing). Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R). - Local Notation fill_in_bottom_for_arrows := (@fill_in_bottom_for_arrows base.type abstract_domain' bottom'). - Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' bottom' abstract_domain'_R). + Local Notation related_bounded_value' := (@related_bounded_value' base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' abstract_domain'_R). + Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' abstract_domain'_R). Context {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)} (interp_annotate_expr : forall t st idc, @@ -734,7 +748,7 @@ Module Compilers. -> forall v, abstraction_relation' _ st v -> expr.interp (@ident_interp) idc v = v) (abstract_interp_ident_Proper' - : forall t idc, type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc)) + : forall t idc, abstraction_relation (abstract_interp_ident t idc) (ident_interp idc)) (extract_list_state_related : forall t st ls v st' v', extract_list_state t st = Some ls @@ -754,7 +768,7 @@ Module Compilers. (strip_annotation_related : forall t idc v, strip_annotation t idc = Some v - -> related_bounded_value (abstract_interp_ident t idc) v (ident_interp idc)). + -> related_bounded_value' (abstract_interp_ident t idc) v (ident_interp idc)). Local Notation update_annotation := (@ident.update_annotation _ abstract_domain' annotate_expr is_annotated_for). Local Notation annotate_with_expr := (@ident.annotate_with_expr _ abstract_domain' annotate_expr is_annotated_for). @@ -763,18 +777,6 @@ Module Compilers. Local Notation reify := (@reify base.type ident _ abstract_domain' annotate bottom'). Local Notation reflect := (@reflect base.type ident _ abstract_domain' annotate bottom'). - Lemma abstract_interp_ident_Proper'' t idc - : type.related_hetero (@abstraction_relation') (fill_in_bottom_for_arrows (abstract_interp_ident t idc)) (ident_interp idc). - Proof using abstract_interp_ident_Proper' bottom'_related. - generalize (abstract_interp_ident_Proper' t idc); clear -bottom'_related. - generalize (ident_interp idc), (abstract_interp_ident t idc); clear idc. - intros v st H. - induction t as [| [|s' d'] IHs d IHd]; cbn in *; cbv [respectful_hetero] in *; - auto. - intros; apply IHd, H; clear IHd H. - intros; apply bottom_related; assumption. - Qed. - Lemma interp_update_annotation t st e (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e)) : expr.interp (@ident_interp) (@update_annotation t st e) @@ -827,7 +829,7 @@ Module Compilers. | progress break_innermost_match | progress break_innermost_match_hyps | progress expr.invert_subst - | progress cbn [fst snd UnderLets.interp expr.interp ident_interp Nat.add] in * + | progress cbn [fst snd UnderLets.interp expr.interp ident.interp Nat.add] in * | progress cbv [ident.literal] in * | match goal with | [ H : context[ident_interp (ident.ident_Literal _)] |- _ ] => rewrite ident.interp_ident_Literal in H @@ -846,9 +848,13 @@ Module Compilers. | match goal with | [ H : context[expr.interp _ (reify_list _)] |- _ ] => rewrite expr.interp_reify_list in H | [ H : abstraction_relation' (_ * _) _ (_, _) |- _ ] - => pose proof (abstract_interp_ident_Proper'' _ ident.fst _ _ H); - pose proof (abstract_interp_ident_Proper'' _ ident.snd _ _ H); - clear H + => let H' := fresh in + let H'' := fresh in + pose proof H as H'; + pose proof H as H''; + apply (abstract_interp_ident_Proper' _ ident.fst) in H'; + apply (abstract_interp_ident_Proper' _ ident.snd) in H''; + clear H | [ H : context[_ = _] |- _ = _ ] => rewrite H by assumption | [ |- List.map ?f (List.combine ?l1 ?l2) = List.map ?g ?l2 ] => transitivity (List.map g (List.map (@snd _ _) (List.combine l1 l2))); @@ -905,38 +911,43 @@ Module Compilers. end ]. Qed. - Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation). + Local Notation interp_ident' := (@ident.interp_ident' _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation). Lemma interp_ident_Proper_not_nth_default_nostrip annotate_with_state t idc - : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc). - Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric. - cbn [UnderLets.interp]. + : related_bounded_value (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)) (@ident_interp t idc). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr. eapply interp_reflect; try first [ apply ident.interp_Proper - | apply abstract_interp_ident_Proper'' | eapply abstract_interp_ident_Proper; reflexivity | apply interp_annotate ]; eauto. Qed. Lemma interp_ident_Proper_not_nth_default annotate_with_state t idc - : related_bounded_value + : related_bounded_value' (abstract_interp_ident t idc) - ((UnderLets.interp (@ident_interp)) - (Base match strip_annotation _ idc with - | Some v => v - | None => reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc) - end)) + (UnderLets.interp + (@ident.interp) + match strip_annotation _ idc with + | Some v => Base v + | None => project_value' _ (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)) + end) (ident_interp idc). - Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric strip_annotation_related. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. pose proof (strip_annotation_related t idc) as H. + cbv [related_bounded_value]. break_innermost_match; eauto using eq_refl, interp_ident_Proper_not_nth_default_nostrip. + eapply related_bounded_value'_Proper1; [ try exact eq_refl; try exact _ .. | eapply interp_reflect; eauto using interp_annotate ]. + all: eauto. + all: rewrite ?state_of_value_reflect. + all: try now apply abstract_interp_ident_Proper. + all: try now apply Compilers.eqv_Reflexive_Proper. Qed. Lemma interp_ident_Proper_nth_default annotate_with_state T (idc:=@ident.List_nth_default T) - : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc). - Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr bottom'_related. - subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value abstract_domain value]. + : related_bounded_value' (abstract_interp_ident _ idc) (UnderLets.interp (@ident.interp) (interp_ident' annotate_with_state idc)) (ident_interp idc). + Proof using abstract_domain'_R_of_related abstract_interp_ident_Proper abstract_interp_ident_Proper' bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr. + subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value' abstract_domain value]. cbv [abstract_domain]; cbn [type.interp bottom_for_each_lhs_of_arrow state_of_value fst snd]. repeat first [ progress intros | progress cbn [UnderLets.interp fst snd expr.interp ident_interp] in * @@ -952,7 +963,7 @@ Module Compilers. | solve [ cbv [Proper respectful Basics.impl] in *; eauto ] | split; [ apply (@abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl) | ] | split; [ reflexivity | ] - | apply (@abstract_interp_ident_Proper'' _ (@ident.List_nth_default T)) + | apply (@abstract_interp_ident_Proper' _ (@ident.List_nth_default T)) | apply conj | rewrite map_nth_default_always | rewrite expr.interp_reify_list @@ -964,53 +975,58 @@ Module Compilers. | [ H : _ = reify_list _ |- _ ] => apply (f_equal (expr.interp (@ident_interp))) in H | [ H : expr.interp _ ?x = _ |- context[expr.interp _ ?x] ] => rewrite H | [ |- Proper _ _ ] => cbv [Proper type.related respectful] - end ]. + end + | progress cbn [interp_ident' reify snd fst Base_value' reflect project_value']; eta_expand ]. Qed. Lemma interp_ident_Proper annotate_with_state t idc - : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc). - Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. + : related_bounded_value' (abstract_interp_ident _ idc) (UnderLets.interp (@ident.interp) (@interp_ident' t annotate_with_state idc)) (ident_interp idc). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. pose idc as idc'. - destruct idc; first [ refine (@interp_ident_Proper_not_nth_default _ _ idc') - | refine (@interp_ident_Proper_nth_default _ _) ]. + destruct idc; + first [ refine (@interp_ident_Proper_not_nth_default _ _ idc') + | refine (@interp_ident_Proper_nth_default _ _) ]. Qed. Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation). Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for). - Local Notation extract := (@ident.extract abstract_domain' bottom' abstract_interp_ident). + Local Notation extract := (@ident.extract abstract_domain' abstract_interp_ident). Lemma interp_eval_with_bound - annotate_with_state {t} (e_st e1 e2 : expr t) - (Hwf : expr.wf3 nil e_st e1 e2) - (Hwf' : expr.wf nil e2 e2) - (Ht : type.is_not_higher_order t = true) - (st : type.for_each_lhs_of_arrow abstract_domain t) - (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st) + annotate_with_state {t} (e e_st e_v : expr t) + (Hwf : expr.wf3 nil e_st e e_v) + (Hwf' : expr.wf nil e e_st) + (Hwf'' : expr.wf nil e_v e_v) + (Hwf''' : expr.wf nil e_st e_st) + (st : type.for_each_lhs_of_arrow abstract_domain t) : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1), - type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e1 st)) arg1 - = type.app_curried (expr.interp (@ident_interp) e2) arg2) + type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e e_st st)) arg1 + = type.app_curried (expr.interp (@ident_interp) e_v) arg2) /\ (forall arg1 (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1) (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1), abstraction_relation' _ (extract e_st st) - (type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e1 st)) arg1)). - Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. cbv [extract eval_with_bound]; apply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper, ident.interp_Proper. Qed. + (type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e e_st st)) arg1)). + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. + cbv [extract eval_with_bound]; eapply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper, ident.interp_Proper; try exact _; intros; apply interp_ident_Proper. + Qed. Lemma interp_eta_expand_with_bound {t} (e1 e2 : expr t) (Hwf : expr.wf nil e1 e2) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow abstract_domain t) (Hb_in : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1), type.app_curried (expr.interp (@ident_interp) (eta_expand_with_bound e1 b_in)) arg1 = type.app_curried (expr.interp (@ident_interp) e2) arg2. - Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using interp_annotate, ident.interp_Proper. Qed. + Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr. + cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using (@interp_ident), interp_annotate, ident.interp_Proper; try typeclasses eauto. + Qed. End with_type. End ident. @@ -1028,11 +1044,12 @@ Module Compilers. Local Notation abstract_domain := (@partial.abstract_domain base.type abstract_domain'). Local Notation abstract_domain'_R t := (@eq (abstract_domain' t)) (only parsing). Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' (fun t => abstract_domain'_R t)). - Local Notation fill_in_bottom_for_arrows := (@fill_in_bottom_for_arrows base.type abstract_domain' bottom'). Definition abstraction_relation' {t} : abstract_domain' t -> base.interp t -> Prop := fun st v => @ZRange.type.base.option.is_bounded_by t st v = true. + Local Notation abstraction_relation := (@abstraction_relation _ abstract_domain' _ (@abstraction_relation') (fun t => abstract_domain'_R t)). + Lemma bottom'_bottom {t} : forall v, abstraction_relation' (bottom' t) v. Proof using Type. cbv [abstraction_relation' bottom']; induction t; cbn; intros; break_innermost_match; cbn; try reflexivity. @@ -1040,8 +1057,8 @@ Module Compilers. Qed. Lemma abstract_interp_ident_related {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (idc : ident t) - : type.related_hetero (@abstraction_relation') (abstract_interp_ident assume_cast_truncates t idc) (ident.interp idc). - Proof using Type. apply ZRange.ident.option.interp_related. Qed. + : abstraction_relation (abstract_interp_ident assume_cast_truncates t idc) (ident.interp idc). + Proof using Type. apply ZRange.ident.option.interp_related_and_Proper. Qed. Local Ltac zrange_interp_idempotent_t := repeat first [ progress destruct_head'_ex @@ -1082,22 +1099,24 @@ Module Compilers. : ZRange.type.base.option.is_bounded_by (t:=base.type.Z*base.type.Z) (ZRange.ident.option.interp assume_cast_truncates ident.Z_cast2 r1 r2) v = true. Proof using Type. destruct r1, r2, assume_cast_truncates; zrange_interp_idempotent_t. Qed. - Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident.interp) (@abstraction_relation') bottom' (fun t => abstract_domain'_R t)). + Local Notation related_bounded_value' := (@related_bounded_value' base.type ident abstract_domain' base.interp (@ident.interp) (@abstraction_relation') (fun t => abstract_domain'_R t)). Lemma always_strip_annotation_related {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (idc : ident t) v (Hv : always_strip_annotation assume_cast_truncates t idc = Some v) - : related_bounded_value (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc). + : related_bounded_value' (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc). Proof using Type. pose proof (@abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast). - pose proof (fun x1 x2 y1 y2 H x01 x02 y01 y02 H' => @abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast2 (x1, x2) (y1, y2) H (x01, x02) (y01, y02) H'). + pose proof (fun x1 x2 y1 y2 H x01 x02 y01 y02 H' => proj2 (proj2 (proj2 (proj2 (@abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast2)) (x1, x2) (y1, y2) H)) (x01, x02) (y01, y02) H'). + cbn [abstraction_relation] in *. cbv [always_strip_annotation] in *; break_innermost_match_hyps; inversion_option; subst. all: repeat first [ reflexivity - | progress cbn [related_bounded_value UnderLets.interp fst snd type.related_hetero] in * + | progress cbn [related_bounded_value' UnderLets.interp fst snd type.related_hetero] in * | progress cbv [respectful_hetero] in * | progress intros | progress destruct_head'_and | progress subst | progress inversion_prod | progress inversion_option + | progress destruct_head_hnf' prod | match goal with | [ |- Proper _ _ ] => exact _ | [ |- _ /\ _ ] => split @@ -1117,7 +1136,7 @@ Module Compilers. | progress break_innermost_match_hyps | progress Reflect.reflect_beq_to_eq zrange_beq | progress cbv [abstraction_relation' ZRange.type.base.option.lift_Some] in * - | cbn [Compilers.ident_interp]; progress cbv [ident.cast2] + | cbn [ident.interp]; progress cbv [ident.cast2] | rewrite ident.cast_in_bounds by assumption | now destruct assume_cast_truncates | rewrite zrange_interp_idempotent_Z_cast by (cbn; eexists; eassumption) @@ -1141,7 +1160,7 @@ Module Compilers. Lemma strip_annotation_related {opts : AbstractInterpretation.Options} {assume_cast_truncates strip_annotations : bool} {t} (idc : ident t) v (Hv : strip_annotation assume_cast_truncates strip_annotations t idc = Some v) - : related_bounded_value (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc). + : related_bounded_value' (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc). Proof using Type. destruct strip_annotations; cbv [strip_annotation] in *; try congruence; now apply always_strip_annotation_related. @@ -1179,8 +1198,8 @@ Module Compilers. cbv [partial.Extract partial.ident.extract partial.extract_gen]. revert b_in1 b_in2 Hb. rewrite <- (@type.related_iff_app_curried base.type ZRange.type.base.option.interp (fun _ => eq)). - apply interp_extract'_from_wf; auto with wf typeclass_instances. - apply GeneralizeVar.wf_from_flat_to_flat, Hwf. + eapply expr.wf_interp_Proper_gen1; [ | apply GeneralizeVar.wf_from_flat_to_flat, Hwf ]. + wf_t. Qed. Lemma Extract_FromFlat_ToFlat {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (e : Expr t) (Hwf : Wf e) b_in @@ -1244,35 +1263,35 @@ Module Compilers. {assume_cast_truncates : bool} {skip_annotations_under : forall t, ident t -> bool} {strip_preexisting_annotations : bool} - {t} (e_st e1 e2 : expr t) - (Hwf : expr.wf3 nil e_st e1 e2) - (Hwf' : expr.wf nil e2 e2) - (Ht : type.is_not_higher_order t = true) + {t} (e_st e e_v : expr t) + (Hwf : expr.wf3 nil e_st e e_v) + (Hwf' : expr.wf nil e e_st) + (Hwf'' : expr.wf nil e_v e_v) + (Hwf''' : expr.wf nil e_st e_st) (st : type.for_each_lhs_of_arrow abstract_domain t) : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true), - type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1 - = type.app_curried (expr.interp (@ident.interp) e2) arg2) + type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e e_st st)) arg1 + = type.app_curried (expr.interp (@ident.interp) e_v) arg2) /\ (forall arg1 (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true), abstraction_relation' (extract assume_cast_truncates e_st st) - (type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1)). + (type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e e_st st)) arg1)). Proof using Hrelax. cbv [eval_with_bound]; split; [ intros arg1 arg2 Harg12 Harg1 | intros arg1 Harg11 Harg1 ]. - all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ]. + all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply @ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper with (skip_base:=true) ]. all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr with typeclass_instances. - all: intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption. + all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption). Qed. Lemma interp_eta_expand_with_bound {t} (e1 e2 : expr t) (Hwf : expr.wf nil e1 e2) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow abstract_domain t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1282,8 +1301,9 @@ Module Compilers. cbv [partial.eta_expand_with_bound]; intros arg1 arg2 Harg12 Harg1. eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1. { apply ident.interp_eta_expand_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr with typeclass_instances. - all: intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption. } - { apply ZRange.type.option.is_bounded_by_impl_related_hetero. } + all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption). + all: try (cbv [Proper]; eapply abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow; try eassumption; reflexivity). } + { apply ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper. } Qed. Lemma Interp_EvalWithBound @@ -1293,9 +1313,7 @@ Module Compilers. {strip_preexisting_annotations : bool} {t} (e : Expr t) (Hwf : expr.Wf e) - (Ht : type.is_not_higher_order t = true) (st : type.for_each_lhs_of_arrow abstract_domain t) - (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st) : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true), @@ -1307,12 +1325,37 @@ Module Compilers. abstraction_relation' (Extract assume_cast_truncates e st) (type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e st)) arg1)). - Proof using Hrelax. cbv [Extract EvalWithBound]; apply interp_eval_with_bound; try apply expr.Wf3_of_Wf; auto. Qed. + Proof using Hrelax. + cbv [EvalWithBound Let_In]. + epose proof (interp_eval_with_bound + (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _) + (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _) + (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _)) as H. + edestruct H as [H0 H1]; [ shelve .. | ]. + split; intros. + { cbv [expr.Interp]; erewrite H0 by eassumption. + eapply (@type.related_iff_app_curried _ _ (fun _ => eq) t). + { apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat; eauto. } + { etransitivity; (idtac + symmetry); eassumption. } } + { lazymatch goal with + | [ H : context[abstraction_relation' ?e _] |- abstraction_relation' ?e' _ ] + => replace e' with e; [ now eapply H | ] + end. + apply Extract_FromFlat_ToFlat'; eauto; []. + eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1; + [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ]; + [ | refine (fun t x y H => H) ]; + cbv beta. + intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. } + Unshelve. + all: try apply expr.Wf3_of_Wf. + all: apply GeneralizeVar.Wf_FromFlat_to_flat. + all: apply Hwf. + Qed. Lemma Interp_EtaExpandWithBound {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow abstract_domain t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1367,29 +1410,30 @@ Module Compilers. Lemma interp_strip_annotations {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} - {t} (e_st e1 e2 : expr t) - (Hwf : expr.wf3 nil e_st e1 e2) - (Hwf' : expr.wf nil e2 e2) - (Ht : type.is_not_higher_order t = true) + {t} (e_st e e_v : expr t) + (Hwf : expr.wf3 nil e_st e e_v) + (Hwf' : expr.wf nil e e_st) + (Hwf'' : expr.wf nil e_v e_v) + (Hwf''' : expr.wf nil e_st e_st) (st : type.for_each_lhs_of_arrow abstract_domain t) : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true), - type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1 - = type.app_curried (expr.interp (@ident.interp) e2) arg2) + type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e e_st st)) arg1 + = type.app_curried (expr.interp (@ident.interp) e_v) arg2) /\ (forall arg1 (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true), abstraction_relation' (extract assume_cast_truncates e_st st) - (type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1)). + (type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e e_st st)) arg1)). Proof using Type. cbv [strip_annotations]; split; [ intros arg1 arg2 Harg12 Harg1 | intros arg1 Harg11 Harg1 ]. - all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ]. + all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply @ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper with (skip_base:=true) ]. all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr, default_relax_zrange_good, abstract_interp_ident_related with typeclass_instances. - all: intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption. + all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption). Qed. Lemma Interp_StripAnnotations @@ -1397,7 +1441,6 @@ Module Compilers. {assume_cast_truncates : bool} {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1413,7 +1456,6 @@ Module Compilers. {assume_cast_truncates : bool} {t} (E : Expr t) (Hwf : expr.Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1) @@ -1429,7 +1471,6 @@ Module Compilers. Lemma Interp_EtaExpandWithListInfoFromBound {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow abstract_domain t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1453,7 +1494,6 @@ Module Compilers. -> is_tighter_than_bool z r' = true) {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1479,7 +1519,6 @@ Module Compilers. -> is_tighter_than_bool z r' = true) {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1) @@ -1491,15 +1530,20 @@ Module Compilers. Proof. cbv [PartialEvaluateWithBounds]. intros arg1 Harg11 Harg1. - rewrite <- Extract_GeneralizeVar by auto with wf typeclass_instances. - eapply @Interp_EvalWithBound; eauto with wf typeclass_instances. + rewrite <- Extract_GeneralizeVar; auto with wf typeclass_instances. + { eapply @Interp_EvalWithBound; eauto with wf typeclass_instances. } + { cbv [Proper] in *. + eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1; + [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ]; + [ | refine (fun t x y H => H) ]; + cbv beta. + intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. } Qed. Lemma Interp_PartialEvaluateWithListInfoFromBounds {opts : AbstractInterpretation.Options} {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) @@ -1526,10 +1570,10 @@ Module Compilers. -> is_tighter_than_bool z r' = true) {t} (E : Expr t) (Hwf : Wf E) - (Ht : type.is_not_higher_order t = true) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (b_out : ZRange.type.base.option.interp (type.final_codomain t)) rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv) + {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R base.type ZRange.type.base.option.interp (fun t0 : base.type => eq))) b_in} : (forall arg1 arg2 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), @@ -1543,17 +1587,49 @@ Module Compilers. [ intros arg1 arg2 Harg12 Harg1; assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1) by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]); + (*assert (b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related _ _ (fun _ => eq))) b_in) + by (cbv [Proper] in *; + eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1; + [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ]; + [ | refine (fun t x y H => H) ]; + cbv beta; + intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl);*) split; - repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances - | rewrite <- Extract_FromFlat_ToFlat by auto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto - | rewrite Extract_FromFlat_ToFlat by auto with wf typeclass_instances - | progress intros - | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ] - | solve [ eauto with wf typeclass_instances ] - | erewrite !Interp_PartialEvaluateWithBounds - | apply type.app_curried_Proper - | apply expr.Wf_Interp_Proper_gen - | progress intros ] - | eauto with wf typeclass_instances ]. + repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances + | rewrite <- Extract_FromFlat_ToFlat by eauto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto + | rewrite Extract_FromFlat_ToFlat by eauto with wf typeclass_instances + | progress intros + | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ] + | solve [ eauto with wf typeclass_instances ] + | erewrite !Interp_PartialEvaluateWithBounds + | apply type.app_curried_Proper + | apply expr.Wf_Interp_Proper_gen + | progress intros ] + | eauto with wf typeclass_instances ]. + Qed. + + Theorem CheckedPartialEvaluateWithBounds_Correct_first_order + {opts : AbstractInterpretation.Options} + (relax_zrange : zrange -> option zrange) + (assume_cast_truncates : bool) + (skip_annotations_under : forall t, ident t -> bool) + (strip_preexisting_annotations : bool) + (Hrelax : forall r r' z, is_tighter_than_bool z r = true + -> relax_zrange r = Some r' + -> is_tighter_than_bool z r' = true) + {t} (E : Expr t) + (Hwf : Wf E) + (Ht : type.is_not_higher_order t = true) + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + (b_out : ZRange.type.base.option.interp (type.final_codomain t)) + rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv) + : (forall arg1 arg2 + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), + ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg1) = true + /\ type.app_curried (Interp rv) arg1 = type.app_curried (Interp E) arg2) + /\ Wf rv. + Proof. + eapply CheckedPartialEvaluateWithBounds_Correct; eauto with core typeclass_instances. Qed. End Compilers. diff --git a/src/AbstractInterpretation/Wf.v b/src/AbstractInterpretation/Wf.v index fb1c30b3b4..21ac4df51d 100644 --- a/src/AbstractInterpretation/Wf.v +++ b/src/AbstractInterpretation/Wf.v @@ -15,11 +15,13 @@ Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DoWithHyp. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.HProp. Require Import Rewriter.Language.Language. Require Import Rewriter.Language.Inversion. Require Import Crypto.Language.InversionExtra. @@ -58,25 +60,33 @@ Module Compilers. (bottom' : forall A, abstract_domain' A) (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop) - {abstract_interp_ident_Proper : forall t, Proper (eq ==> abstract_domain'_R t) (abstract_interp_ident t)} - {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}. - Local Notation value var := (@value base_type ident var abstract_domain'). + {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)} + (base_type_beq : base_type -> base_type -> bool) + {reflect_base_type_beq : reflect_rel eq base_type_beq} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + + Local Notation value' var := (@value' base_type ident var abstract_domain'). Local Notation abstract_domain := (@abstract_domain base_type abstract_domain'). Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')). Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')). + Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *) + + (*Context {base_type_eq_Decidable : DecidableRel (@eq base_type)}.*) + Section with_var2. Context {var1 var2 : type -> Type}. Local Notation UnderLets1 := (@UnderLets.UnderLets base_type ident var1). Local Notation UnderLets2 := (@UnderLets.UnderLets base_type ident var2). Local Notation expr1 := (@expr.expr base_type ident var1). Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation value1 := (@value var1). - Local Notation value2 := (@value var2). - Local Notation value_with_lets1 := (@value_with_lets base_type ident var1 abstract_domain'). - Local Notation value_with_lets2 := (@value_with_lets base_type ident var2 abstract_domain'). - Local Notation state_of_value1 := (@state_of_value base_type ident var1 abstract_domain' bottom'). - Local Notation state_of_value2 := (@state_of_value base_type ident var2 abstract_domain' bottom'). + Local Notation value'1 := (@value' var1). + Local Notation value'2 := (@value' var2). + Local Notation value1 := (@value base_type ident var1 abstract_domain'). + Local Notation value2 := (@value base_type ident var2 abstract_domain'). + Local Notation state_of_value1 := (@state_of_value base_type ident var1 abstract_domain'). + Local Notation state_of_value2 := (@state_of_value base_type ident var2 abstract_domain'). Context (annotate1 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr1 t -> UnderLets1 (@expr1 t)) (annotate2 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr2 t -> UnderLets2 (@expr2 t)) (annotate_Proper @@ -84,57 +94,58 @@ Module Compilers. v1 v2 (Hv : abstract_domain'_R t v1 v2) e1 e2 (He : expr.wf G e1 e2), UnderLets.wf (fun G' => expr.wf G') G (annotate1 is_let_bound t v1 e1) (annotate2 is_let_bound t v2 e2)) - (interp_ident1 : bool -> forall t, ident t -> value_with_lets1 t) - (interp_ident2 : bool -> forall t, ident t -> value_with_lets2 t) + (interp_ident'1 : bool -> forall t, ident t -> UnderLets1 (value'1 t)) + (interp_ident'2 : bool -> forall t, ident t -> UnderLets2 (value'2 t)) (skip_annotations_under : forall t, ident t -> bool). Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom'). Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom'). Local Notation reflect1 := (@reflect base_type ident var1 abstract_domain' annotate1 bottom'). Local Notation reflect2 := (@reflect base_type ident var2 abstract_domain' annotate2 bottom'). - Local Notation bottomify1 := (@bottomify base_type ident var1 abstract_domain' bottom'). - Local Notation bottomify2 := (@bottomify base_type ident var2 abstract_domain' bottom'). - Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1). - Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2). - Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1). - Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2). - Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1). - Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2). + Local Notation interp1 := (@interp base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1). + Local Notation interp2 := (@interp base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2). + Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1). + Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2). + Local Notation eval'1 := (@eval' base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1). + Local Notation eval'2 := (@eval' base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2). Local Notation eta_expand_with_bound'1 := (@eta_expand_with_bound' base_type ident var1 abstract_domain' annotate1 bottom'). Local Notation eta_expand_with_bound'2 := (@eta_expand_with_bound' base_type ident var2 abstract_domain' annotate2 bottom'). + Local Notation invert_default := (@invert_default base_type ident try_make_transport_base_type_cps abstract_domain' default_expr). + Local Notation invert_default' := (@invert_default' base_type ident try_make_transport_base_type_cps abstract_domain' default_expr). Definition abstract_domain_R {t} : relation (abstract_domain t) := type.related abstract_domain'_R. + Context {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}. + (** This one is tricky. Because we need to be stable under weakening and reordering of the context, we permit any context for well-formedness of the input in the arrow case, and simply tack on that context at the beginning of the output. This is sort-of wasteful on the output context, but it's sufficient to prove - [wf_value_Proper_list] below, which is what we really + [wf_value'_Proper_list] below, which is what we really need. *) - Fixpoint wf_value G {t} : value1 t -> value2 t -> Prop - := match t return value1 t -> value2 t -> Prop with - | type.base t - => fun v1 v2 - => abstract_domain_R (fst v1) (fst v2) - /\ expr.wf G (snd v1) (snd v2) + Fixpoint wf_value' G {t} : value'1 t -> value'2 t -> Prop + := match t return value'1 t -> value'2 t -> Prop with + | type.base t => expr.wf G | type.arrow s d => fun v1 v2 => forall seg G' sv1 sv2, G' = (seg ++ G)%list - -> @wf_value seg s sv1 sv2 + -> abstract_domain_R (fst sv1) (fst sv2) + /\ @wf_value' seg s (snd sv1) (snd sv2) -> UnderLets.wf - (fun G' => @wf_value G' d) G' + (fun G' => @wf_value' G' d) G' (v1 sv1) (v2 sv2) end. - Definition wf_value_with_lets G {t} : value_with_lets1 t -> value_with_lets2 t -> Prop - := UnderLets.wf (fun G' => wf_value G') G. + Definition wf_value G {t} : value1 t -> value2 t -> Prop + := fun v1 v2 => abstract_domain_R (fst v1) (fst v2) + /\ UnderLets.wf (fun G' => wf_value' G') G (snd v1) (snd v2). Context (interp_ident_Proper : forall G t idc1 idc2 (Hidc : idc1 = idc2) annotate_with_state, - wf_value_with_lets G (interp_ident1 annotate_with_state t idc1) (interp_ident2 annotate_with_state t idc2)). + UnderLets.wf (fun G' => wf_value' G') G (interp_ident'1 annotate_with_state t idc1) (interp_ident'2 annotate_with_state t idc2)). Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10. Proof using bottom'_Proper. @@ -152,20 +163,17 @@ Module Compilers. Lemma state_of_value_Proper G {t} v1 v2 (Hv : @wf_value G t v1 v2) : abstract_domain_R (state_of_value1 v1) (state_of_value2 v2). - Proof using bottom'_Proper. - clear -Hv type_base bottom'_Proper. - destruct t; [ destruct v1, v2, Hv | ]; cbn in *; cbv [respectful]; eauto; intros; apply bottom_Proper. - Qed. + Proof using Type. apply Hv. Qed. Local Hint Resolve (fun A (P : list A -> Prop) => ex_intro P nil) (fun A (x : A) (P : list A -> Prop) => ex_intro P (cons x nil)) : core. Local Hint Constructors expr.wf ex : core. Local Hint Unfold List.In : core. - Lemma wf_value_Proper_list G1 G2 + Lemma wf_value'_Proper_list G1 G2 (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) t e1 e2 - (Hwf : @wf_value G1 t e1 e2) - : @wf_value G2 t e1 e2. + (Hwf : @wf_value' G1 t e1 e2) + : @wf_value' G2 t e1 e2. Proof using Type. clear -type_base HG1G2 Hwf. revert dependent G1; revert dependent G2; induction t; intros; @@ -182,6 +190,49 @@ Module Compilers. | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ]. Qed. + Lemma wf_value_Proper_list G1 G2 + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + t e1 e2 + (Hwf : @wf_value G1 t e1 e2) + : @wf_value G2 t e1 e2. + Proof using Type. + split; try apply Hwf. + eapply UnderLets.wf_Proper_list, Hwf; eauto using wf_value'_Proper_list. + Qed. + + Local Ltac wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d + := first [ progress cbn [fst snd] in * + | progress fold (@wf_value') in * + | match goal with + | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d + | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ] + => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ] + | [ |- UnderLets.wf _ _ (reify1 _ _ _ _) (reify2 _ _ _ _) ] + => apply wf_reify_s || apply wf_reify_d + | [ |- abstract_domain_R (state_of_value1 ?v1 ?x1) (state_of_value2 ?v2 ?x2) ] + => eapply (state_of_value_Proper _ v1 v2); [ | change (abstract_domain_R x1 x2) ] + end + | progress cbn [wf_value'] in * + | progress intros + | progress subst + | progress destruct_head'_and + | progress destruct_head'_ex + | progress cbv [respectful wf_value] in * + | match goal with + | [ |- ?x ++ ?y::?z ++ ?w = ?seg ++ ?z ++ ?w ] => unify seg (x ++ y::nil); cbn [List.app]; rewrite <- !app_assoc + end + | solve [ eauto | wf_t ] + | apply annotate_Proper + | apply UnderLets.wf_to_expr + | break_innermost_match_step + | eapply wf_value'_Proper_list; [ | eassumption ] + | match goal with + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ |- expr.wf _ _ _ ] => constructor + | [ |- _ /\ _ ] => split + | [ |- abstract_domain_R (state_of_value1 _) (state_of_value2 _) ] + => eapply state_of_value_Proper + end ]. Fixpoint wf_reify (annotate_with_state : bool) (is_let_bound : bool) G {t} : forall v1 v2 (Hv : @wf_value G t v1 v2) s1 s2 (Hs : type.and_for_each_lhs_of_arrow (@abstract_domain_R) s1 s2), @@ -204,53 +255,49 @@ Module Compilers. all: cbn [reify reflect] in *. all: fold (@reify2) (@reflect2) (@reify1) (@reflect1). all: cbn in *. - all: repeat first [ progress cbn [fst snd] in * - | progress cbv [respectful] in * - | progress intros - | progress subst - | progress destruct_head'_and - | progress destruct_head'_ex - | solve [ eauto | wf_t ] - | apply annotate_Proper - | apply UnderLets.wf_to_expr - | break_innermost_match_step - | match goal with - | [ |- UnderLets.wf _ _ _ _ ] => constructor - | [ |- expr.wf _ _ _ ] => constructor - | [ He : forall seg G' sv1 sv2, G' = (seg ++ ?G)%list -> _ |- UnderLets.wf _ (?v :: ?G) (UnderLets.splice _ _) (UnderLets.splice _ _) ] - => eapply UnderLets.wf_splice; [ apply (He (cons v nil)) | ] - | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ] - => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ] - | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d - | [ H : wf_value _ ?x ?y |- wf_value _ ?x ?y ] - => eapply wf_value_Proper_list; [ | eassumption ] - | [ H : forall x y, ?R x y -> ?R' (?f x) (?g y) |- ?R' (?f _) (?g _) ] - => apply H - | [ |- ?R (state_of_value1 _) (state_of_value2 _) ] => eapply state_of_value_Proper - end ]. + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]). + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]). + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]). + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: try (apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d). + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: [ > ]. + eapply UnderLets.wf_splice. + 1: match goal with + | [ H : wf_value' ?G ?x ?y |- UnderLets.wf ?P ?G (?f (_, ?x)) (?g (_, ?y)) ] + => eapply UnderLets.wf_Proper_list_impl with (P1:=P) (P2:=P); revgoals + end; + [ exactly_once multimatch goal with H : _ |- _ => eapply H end | .. ]. + all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d. + all: instantiate (1:=_::nil); left; reflexivity. Qed. - Lemma wf_bottomify {t} G v1 v2 - (Hwf : @wf_value G t v1 v2) - : wf_value_with_lets G (bottomify1 v1) (bottomify2 v2). - Proof using bottom'_Proper. - cbv [wf_value_with_lets] in *. - revert dependent G; induction t as [|s IHs d IHd]; intros; - cbn [bottomify wf_value]; fold (@value1) (@value2) in *; break_innermost_match; - constructor. - all: repeat first [ progress cbn [fst snd wf_value] in * - | progress destruct_head'_and - | assumption - | apply bottom'_Proper - | apply conj - | progress intros - | progress subst - | solve [ eapply UnderLets.wf_splice; eauto ] ]. + #[local] Existing Instance type.reflect_type_beq. + + Lemma invert_default_Some {A B o t v} + : o = Some (existT _ t v) -> @invert_default A B t o = v. + Proof using try_make_transport_base_type_cps_correct. + intro; subst; cbv [invert_default Option.sequence_return projT1 projT2]. + rewrite_type_transport_correct. + break_innermost_match; try now exfalso; reflect_hyps; congruence. + rewrite Reflect.eq_reflect_to_dec_true_refl; reflexivity. + Qed. + + Lemma invert_default'_Some {A B C o t v} + : o = Some (existT _ t v) -> @invert_default' A B C t o = v. + Proof using try_make_transport_base_type_cps_correct. + intro; subst; cbv [invert_default' Option.sequence_return projT1 projT2]. + rewrite_type_transport_correct. + break_innermost_match; try now exfalso; reflect_hyps; congruence. + rewrite Reflect.eq_reflect_to_dec_true_refl; reflexivity. Qed. Local Ltac wf_interp_t := - repeat first [ progress cbv [wf_value_with_lets abstract_domain_R respectful] in * - | progress cbn [wf_value fst snd partial.bottom type.related eq_rect List.In] in * + repeat first [ progress cbv [wf_value abstract_domain_R respectful Base_value' project_value' Option.sequence_return] in * + | progress cbn [wf_value' fst snd partial.bottom type.related eq_rect List.In] in * | wf_safe_t_step | exact I | apply wf_reify @@ -258,17 +305,21 @@ Module Compilers. | progress destruct_head'_ex | progress destruct_head'_or | eapply UnderLets.wf_splice + | erewrite invert_default_Some by reflexivity + | erewrite invert_default'_Some by reflexivity | match goal with - | [ |- UnderLets.wf _ _ (bottomify1 _) (bottomify2 _) ] => apply wf_bottomify | [ |- UnderLets.wf _ _ _ _ ] => constructor | [ |- and _ _ ] => apply conj + | [ H : _ = snd ?x |- _ ] => is_var x; destruct x + | [ H : _ = fst ?x |- _ ] => is_var x; destruct x end - | eapply wf_value_Proper_list; [ | solve [ eauto ] ] - | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] + | eapply wf_value'_Proper_list; [ | solve [ eauto | split_and; eauto ] ] + | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto | split_and; eauto ] ] | match goal with | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ] end - | break_innermost_match_step ]. + | break_innermost_match_step + | progress eliminate_hprop_eq ]. Local Notation skip_annotations_for_App := (@skip_annotations_for_App base_type ident skip_annotations_under). @@ -299,12 +350,39 @@ Module Compilers. end ]. Qed. - Lemma wf_interp (annotate_with_state : bool) G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t) - (Hwf : expr.wf G e1 e2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : wf_value_with_lets G' (interp1 annotate_with_state e1) (interp2 annotate_with_state e2). - Proof using annotate_Proper bottom'_Proper interp_ident_Proper. - revert dependent G'; revert annotate_with_state; induction Hwf; intros; cbn [interp]; + Lemma wf_interp (annotate_with_state : bool) (G : list { t : _ & value1 t * value2 t * abstract_domain t * abstract_domain t }%type) G12 G34 G' {t} (e1 : @expr (@value1) t) (est1 : @expr abstract_domain t) (e2 : @expr (@value2) t) (est2 : @expr abstract_domain t) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf : expr.wf4 G e1 e2 est1 est2) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : wf_value G' (interp1 annotate_with_state e1 est1) (interp2 annotate_with_state e2 est2). + Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct. + revert dependent G12; revert dependent G34; revert dependent G'; revert annotate_with_state; induction Hwf; intros; cbn [interp]; + repeat match goal with + | [ H : List.In (existT _ ?t (?v1, ?v2, ?v3, ?v4)) ?G, H' : List.map _ ?G = ?G12 |- _ ] + => unique assert (List.In (existT _ t (v1, v2)) G12) + by (rewrite <- H'; revert H; rewrite in_map_iff; eexists; split; try eassumption; reflexivity) + | [ H : List.In (existT _ ?t (?v1, ?v2, ?v3, ?v4)) ?G, H' : List.map _ ?G = ?G34 |- _ ] + => unique assert (List.In (existT _ t (v3, v4)) G34) + by (rewrite <- H'; revert H; rewrite in_map_iff; eexists; split; try eassumption; reflexivity) + | [ HG : List.map ?f ?G = ?G12, H : forall v1 v2 v3 v4, expr.wf4 (@?v v1 v2 v3 v4 :: ?G) (@?e1 v1 v2) (@?e2 v1 v2) _ _ |- _ ] + => let v' := (eval cbn in (fun v1 v2 => f (v v1 v2 bottom bottom))) in + let lem := (eval cbv beta in (forall v1 v2, expr.wf (v' v1 v2 :: G12) (e1 v1 v2) (e2 v1 v2))) in + unique assert lem + by (intros v1 v2; specialize (H v1 v2 bottom bottom); + apply expr.wf_of_wf4_default in H; subst G12; cbn [List.map] in H; + apply H; split; apply bottom) + | [ HG : List.map ?f ?G = ?G12, H : expr.wf4 ?G ?e1 ?e2 _ _ |- _ ] + => unique assert (expr.wf G12 e1 e2) + by (apply expr.wf_of_wf4_default in H; subst G12; cbn [List.map] in H; + apply H; split; apply bottom) + | [ HG : List.map ?f ?G = ?G34, H : expr.wf4 ?G _ _ ?e3 ?e4 |- _ ] + => unique assert (expr.wf G34 e3 e4) + by (apply expr.wf_of_wf4_default in H; subst G34; cbn [List.map] in H; + apply H; split; apply bottom) + end; try solve [ apply interp_ident_Proper; auto | eauto ]; match goal with @@ -312,27 +390,97 @@ Module Compilers. => match goal with | [ |- context[skip_annotations_for_App ?e2v] ] => epose proof (wf_skip_annotations_for_App (e1:=e1v) (e2:=e2v) (G:=G') ltac:(solve [ wf_t ])); - generalize dependent (skip_annotations_for_App e1v); - generalize dependent (skip_annotations_for_App e2v); intros; - subst + generalize dependent (skip_annotations_for_App e1v); + generalize dependent (skip_annotations_for_App e2v); intros; + subst end end; wf_interp_t. + all: lazymatch goal with + | [ H : type.related ?R ?x ?y |- type.related ?R (expr.interp ?ii1 ?f1 ?x) (expr.interp ?ii2 ?f2 ?y) ] + => is_var x; is_var y; + revert x y H; + change (type.related R (expr.interp ii1 f1) (expr.interp ii2 f2)); + eapply expr.wf_interp_Proper_gen2; eauto + | _ => idtac + end. + all: repeat match goal with + | [ H : invert_Abs (expr.Abs _) = _ |- _ ] + => cbv in H; inversion_option; subst + end. + all: expr.inversion_wf_constr; wf_interp_t. + all: try now + ( + do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H); + lazymatch goal with + | [ |- expr.wf _ _ _ ] => now eauto + | _ => idtac + end; + try reflexivity; + [ > wf_interp_t .. ]; + cbn [List.In List.map] in *; + wf_interp_t + ). + all: try now + ( + eapply UnderLets.wf_Proper_list_impl; + [ .. | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H) ]; + try reflexivity; + [ .. | wf_interp_t ]; + wf_interp_t + ). + all: try now + ( + eapply expr.wf_interp_Proper_gen2; + lazymatch goal with + | [ |- expr.wf _ _ _ ] => now eauto + | _ => idtac + end; + cbn [List.map List.In]; + wf_interp_t + ). + all: try now + ( + do_with_hyp' ltac:(fun H => eapply H; clear H); + try reflexivity; + cbn [List.In List.map] in *; + wf_interp_t + ). + all: try do_with_hyp' + ltac:(fun H + => now + ( + eapply H; + try reflexivity; + wf_interp_t; + cbn [List.In List.map] in *; + wf_interp_t + ) + ). + Unshelve. + all: assumption. Qed. - Lemma wf_eval_with_bound' (annotate_with_state : bool) G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (@eval_with_bound'1 annotate_with_state t e1 st1) (@eval_with_bound'2 annotate_with_state t e2 st2). - Proof using annotate_Proper bottom'_Proper interp_ident_Proper. - eapply UnderLets.wf_to_expr, UnderLets.wf_splice. - { eapply wf_interp; solve [ eauto ]. } - { intros; destruct_head'_ex; subst; eapply wf_reify; eauto. } + Lemma wf_eval_with_bound' (annotate_with_state : bool) G G12 G34 G' {t} e1 e2 est1 est2 (He : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (@eval_with_bound'1 annotate_with_state t e1 est1 st1) (@eval_with_bound'2 annotate_with_state t e2 est2 st2). + Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct. + eapply UnderLets.wf_to_expr, wf_reify; eauto; []. + eapply wf_interp; try eassumption. Qed. - Lemma wf_eval' G G' {t} e1 e2 (He : expr.wf G e1 e2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (@eval'1 t e1) (@eval'2 t e2). - Proof using annotate_Proper bottom'_Proper interp_ident_Proper. + Lemma wf_eval' G G12 G34 G' {t} e1 e2 est1 est2 (He : expr.wf4 G e1 e2 est1 est2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (@eval'1 t e1 est1) (@eval'2 t e2 est2). + Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct. eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper. Qed. @@ -389,14 +537,14 @@ Module Compilers. Section with_var2. Context {var1 var2 : type -> Type}. - Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' abstract_domain'_R var1 var2). Local Notation wf_value := (@wf_value base.type ident abstract_domain' abstract_domain'_R var1 var2). + Local Notation wf_value' := (@wf_value' base.type ident abstract_domain' abstract_domain'_R var1 var2). Context (annotate_expr1 : forall t, abstract_domain' t -> option (@expr var1 (t -> t))) (annotate_expr2 : forall t, abstract_domain' t -> option (@expr var2 (t -> t))) (is_annotated_for1 : forall t t', @expr var1 t -> abstract_domain' t' -> bool) (is_annotated_for2 : forall t t', @expr var2 t -> abstract_domain' t' -> bool) - (strip_annotation1 : forall t, ident t -> option (value _ t)) - (strip_annotation2 : forall t, ident t -> option (value _ t)) + (strip_annotation1 : forall t, ident t -> option (value' _ t)) + (strip_annotation2 : forall t, ident t -> option (value' _ t)) (annotation_to_cast1 : forall s d, @expr var1 (s -> d) -> option (@expr var1 s -> @expr var1 d)) (annotation_to_cast2 : forall s d, @expr var2 (s -> d) -> option (@expr var2 s -> @expr var2 d)) (skip_annotations_under : forall t, ident t -> bool) @@ -416,7 +564,7 @@ Module Compilers. (@is_annotated_for2 t t' e2)} {wf_strip_annotation : forall G t idc, - option_eq (wf_value G) + option_eq (wf_value' G) (@strip_annotation1 t idc) (@strip_annotation2 t idc)}. @@ -428,8 +576,8 @@ Module Compilers. Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_expr2 is_annotated_for2). Local Notation annotate_with_expr1 := (@ident.annotate_with_expr var1 abstract_domain' annotate_expr1 is_annotated_for1). Local Notation annotate_with_expr2 := (@ident.annotate_with_expr var2 abstract_domain' annotate_expr2 is_annotated_for2). - Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1). - Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2). + Local Notation interp_ident'1 := (@ident.interp_ident' var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1). + Local Notation interp_ident'2 := (@ident.interp_ident' var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2). Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom'). Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom'). @@ -608,23 +756,30 @@ Module Compilers. | progress cbn [type.decode f_equal eq_rect fst snd] in * | solve [ wf_t ] ] ]. Qed. - Local Ltac type_of_value v := + Local Ltac type_of_value' v := lazymatch v with | (abstract_domain ?t * _)%type => t + | expr ?t => t | (?a -> UnderLets _ ?b) - => let a' := type_of_value a in - let b' := type_of_value b in + => let a' := type_of_value' a in + let b' := type_of_value' b in constr:(type.arrow a' b') + | ?v => fail 0 "type_of_value': unrecognized:" v end. Local Opaque ident.ident_Literal. Lemma wf_interp_ident_nth_default (annotate_with_state : bool) G T - : wf_value_with_lets G (@interp_ident1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident2 annotate_with_state _ (@ident.List_nth_default T)). + : UnderLets.wf (fun G' => wf_value' G') G (@interp_ident'1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident'2 annotate_with_state _ (@ident.List_nth_default T)). Proof using abstract_interp_ident_Proper annotate_expr_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. - cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain]. - { intros; subst. - destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. + cbv [wf_value wf_value' ident.interp_ident']; constructor; cbn -[abstract_domain_R abstract_domain]. + all: intros; subst. + all: destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. + all: repeat first [ progress subst | lazymatch goal with + | [ H : wf_value' _ (reify_list _) _ |- _ ] + => progress cbn [wf_value'] in H + | [ H : wf_value' _ _ (reify_list _) |- _ ] + => progress cbn [wf_value'] in H | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ] => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ] @@ -655,8 +810,8 @@ Module Compilers. | [ |- expr _ -> _ -> _ ] => refine (expr.wf G) | [ |- ?T -> _ -> _ ] - => let t := type_of_value T in - refine (@wf_value G t) + => let t := type_of_value' T in + refine (@wf_value' G t) end | | ] | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ] @@ -666,8 +821,8 @@ Module Compilers. | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H | [ H : List.nth_error _ _ = None |- _ ] => apply List.nth_error_None in H | [ H : List.nth_error _ _ = Some _ |- _ ] - => unique pose proof (@ListUtil.nth_error_value_length _ _ _ _ H); - unique pose proof (@ListUtil.nth_error_value_In _ _ _ _ H) + => unique pose proof (@nth_error_value_length _ _ _ _ H); + unique pose proof (@nth_error_value_In _ _ _ _ H) | [ H : context[List.In _ (List.map _ _)] |- _ ] => rewrite List.in_map_iff in H | [ H : (?x <= ?y)%nat, H' : (?y < ?x)%nat |- _ ] => exfalso; clear -H H'; lia | [ H : (?x <= ?y)%nat, H' : (?y < ?x')%nat, H'' : ?x' = ?x |- _ ] => exfalso; clear -H H' H''; lia @@ -686,7 +841,7 @@ Module Compilers. end | progress inversion_option | progress intros - | progress cbn [fst snd value] in * + | progress cbn [fst snd value'] in * | progress destruct_head'_prod | progress destruct_head'_ex | progress destruct_head'_and @@ -698,10 +853,9 @@ Module Compilers. | progress expr.inversion_expr | handle_Forall2_step | wf_safe_t_step - | progress destruct_head' (@partial.wf_value) | solve [ eapply wf_annotate; wf_t; try apply DefaultValue.expr.base.wf_default | eapply wf_annotate_base; wf_t - | eapply (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl); assumption + | eapply (abstract_interp_ident_Proper _ (@ident.List_nth_default _) _ eq_refl); assumption | eapply wf_update_annotation; wf_t | wf_t | match goal with @@ -723,14 +877,14 @@ Module Compilers. | progress expr.inversion_wf_one_constr | progress expr.invert_match | match goal with - | [ |- wf_value _ _ _ ] => progress hnf - end ]. } + | [ |- wf_value' _ _ _ ] => progress hnf + end ]. Qed. Lemma wf_interp_ident_not_nth_default_nostrip (annotate_with_state : bool) G {t} (idc : ident t) - : wf_value_with_lets G (Base (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))). + : wf_value G (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)) (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)). Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper. - constructor; eapply wf_reflect; + constructor; unshelve eapply wf_reflect; solve [ apply bottom'_Proper | apply wf_annotate | repeat constructor @@ -738,30 +892,31 @@ Module Compilers. Qed. Lemma wf_interp_ident_not_nth_default (annotate_with_state : bool) G {t} (idc : ident t) - : (wf_value_with_lets G) - (Base match strip_annotation1 _ idc with - | Some v => v - | None => reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc) - end) - (Base match strip_annotation2 _ idc with - | Some v => v - | None => reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc) - end). + : (UnderLets.wf (fun G' => wf_value' G') G) + (match strip_annotation1 _ idc with + | Some v => Base v + | None => project_value' _ (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)) + end) + (match strip_annotation2 _ idc with + | Some v => Base v + | None => project_value' _ (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)) + end). Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation. pose proof (wf_strip_annotation G _ idc). break_innermost_match; cbn [option_eq] in *; solve [ exfalso; assumption | congruence | apply wf_interp_ident_not_nth_default_nostrip - | constructor; assumption ]. + | constructor; assumption + | split; [ now apply abstract_interp_ident_Proper | constructor; assumption ] ]. Qed. Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2) (annotate_with_state : bool) - : wf_value_with_lets G (@interp_ident1 annotate_with_state t idc1) (@interp_ident2 annotate_with_state t idc2). + : UnderLets.wf (fun G' => wf_value' G') G (@interp_ident'1 annotate_with_state t idc1) (@interp_ident'2 annotate_with_state t idc2). Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation. - cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1; - first [ apply wf_interp_ident_nth_default - | apply wf_interp_ident_not_nth_default ]. + subst idc2; destruct idc1; + first [ apply wf_interp_ident_not_nth_default + | apply wf_interp_ident_nth_default ]. Qed. Local Notation strip_all_annotations'1 := (@partial.ident.strip_all_annotations' var1 annotation_to_cast1 skip_annotations_under). @@ -795,26 +950,38 @@ Module Compilers. Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1 skip_annotations_under). Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2 skip_annotations_under). - Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 st1) (@eval_with_bound2 annotate_with_state t e2 st2). + + Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 est1 st1) (@eval_with_bound2 annotate_with_state t e2 est2 st2). Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation. eapply wf_eval_with_bound'; solve [ eassumption | eapply wf_annotate - | eapply wf_interp_ident ]. + | eapply wf_interp_ident + | typeclasses eauto ]. Qed. Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1). Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2). - Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (@eval1 t e1) (@eval2 t e2). + + Lemma wf_eval {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (@eval1 t e1 est1) (@eval2 t e2 est2). Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation. eapply wf_eval'; solve [ eassumption | eapply wf_annotate - | eapply wf_interp_ident ]. + | eapply wf_interp_ident + | typeclasses eauto ]. Qed. Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1). @@ -837,7 +1004,7 @@ Module Compilers. Local Notation abstract_domain := (@partial.abstract_domain base.type abstract_domain'). Local Notation abstract_domain'_R t := (@eq (abstract_domain' t)) (only parsing). Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' (fun t => abstract_domain'_R t)). - Local Notation wf_value := (@wf_value base.type ident abstract_domain' (fun t => abstract_domain'_R t)). + Local Notation wf_value' := (@wf_value' base.type ident abstract_domain' (fun t => abstract_domain'_R t)). Lemma annotate_expr_Proper {relax_zrange var1 var2} {t} s1 s2 : abstract_domain'_R t s1 s2 @@ -877,12 +1044,12 @@ Module Compilers. (#(@ident.Literal base.type.zrange r1%zrange), #(@ident.Literal base.type.zrange r2%zrange))%expr_pat). Lemma wf_always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var1 var2} G {t} idc - : option_eq (wf_value G) + : option_eq (wf_value' G) (always_strip_annotation assume_cast_truncates (var:=var1) t idc) (always_strip_annotation assume_cast_truncates (var:=var2) t idc). Proof using Type. cbv [always_strip_annotation]; break_innermost_match; try reflexivity; - cbn [option_eq wf_value]. + cbn [option_eq wf_value']. all: repeat first [ progress intros | assumption | progress subst @@ -899,7 +1066,7 @@ Module Compilers. Qed. Lemma wf_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var1 var2} G {t} idc - : option_eq (wf_value G) + : option_eq (wf_value' G) (strip_annotation assume_cast_truncates strip_annotations (var:=var1) t idc) (strip_annotation assume_cast_truncates strip_annotations (var:=var2) t idc). Proof using Type. @@ -1041,11 +1208,15 @@ Module Compilers. Section with_var2. Context {var1 var2 : type -> Type}. - Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2). - - Lemma wf_eval {opts : AbstractInterpretation.Options} {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (t:=t) (eval (var:=var1) e1) (eval (var:=var2) e2). + Local Notation wf_value := (@wf_value base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2). + + Lemma wf_eval {opts : AbstractInterpretation.Options} {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (t:=t) (eval (var:=var1) e1 est1) (eval (var:=var2) e2 est2). Proof using Type. eapply ident.wf_eval; solve [ eassumption @@ -1062,11 +1233,15 @@ Module Compilers. : expr.wf G (@strip_all_annotations strip_annotations_under var1 t e1) (@strip_all_annotations strip_annotations_under var2 t e2). Proof using Type. revert Hwf; apply ident.wf_strip_all_annotations, @wf_annotation_to_cast. Qed. - Lemma wf_eval_with_bound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) + Lemma wf_eval_with_bound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) : expr.wf G' (var1:=var1) (var2:=var2) (t:=t) - (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st1) - (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e2 st2). + (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 est1 st1) + (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e2 est2 st2). Proof using Type. eapply ident.wf_eval_with_bound; solve [ eassumption @@ -1079,9 +1254,13 @@ Module Compilers. | apply is_annotated_for_Proper ]. Qed. - Lemma wf_strip_annotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2) - : expr.wf G' (t:=t) (strip_annotations assume_cast_truncates (var:=var1) e1 st1) (strip_annotations assume_cast_truncates (var:=var2) e2 st2). + Lemma wf_strip_annotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12) + (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34) + (Hwf' : expr.wf G34 est1 est2) + (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2) + (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2) + : expr.wf G' (t:=t) (strip_annotations assume_cast_truncates (var:=var1) e1 est1 st1) (strip_annotations assume_cast_truncates (var:=var2) e2 est2 st2). Proof using Type. eapply ident.wf_eval_with_bound; solve [ eassumption @@ -1115,19 +1294,19 @@ Module Compilers. Lemma Wf_Eval {opts : AbstractInterpretation.Options} {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e). Proof using Type. - intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + intros ??; cbv [Eval Let_In]; eapply wf_eval with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; tauto. Qed. Lemma Wf_EvalWithBound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) : Wf (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound). Proof using Type. - intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + intros ??; cbv [EvalWithBound Let_In]; eapply wf_eval_with_bound with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; tauto. Qed. Lemma Wf_StripAnnotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) : Wf (StripAnnotations assume_cast_truncates e bound). Proof using Type. - intros ??; eapply wf_strip_annotations with (G:=nil); cbn [List.In]; try tauto; apply Hwf. + intros ??; cbv [StripAnnotations]; eapply wf_strip_annotations with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply Hwf; tauto. Qed. Lemma Wf_EtaExpandWithBound {relax_zrange t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v index 5f04e08a17..f09333f70a 100644 --- a/src/AbstractInterpretation/ZRangeProofs.v +++ b/src/AbstractInterpretation/ZRangeProofs.v @@ -44,9 +44,12 @@ Require Import Crypto.Util.Tactics.PrintGoal. Require Import Crypto.Language.PreExtra. Require Import Crypto.CastLemmas. Require Import Crypto.AbstractInterpretation.ZRange. +Require Import Crypto.AbstractInterpretation.ZRangeCommonProofs. Module Compilers. Import AbstractInterpretation.ZRange.Compilers. + Import AbstractInterpretation.ZRangeCommonProofs.Compilers. + Import Rewriter.Language.Wf.Compilers. (* for properties about type.related_hetero *) Export ZRange.Settings. Module ZRange. @@ -113,6 +116,14 @@ Module Compilers. (fun t st v => ZRange.type.base.option.is_bounded_by st v = true) (ZRange.ident.option.interp assume_cast_truncates idc) (ident.interp idc)). + Local Notation interp_is_related_and_Proper idc + := (type.related_hetero_and_Proper + (skip_base:=true) + (fun t => eq) + (fun t => eq) + (fun t st v => ZRange.type.base.option.is_bounded_by st v = true) + (ZRange.ident.option.interp assume_cast_truncates idc) + (ident.interp idc)). Local Ltac z_cast_t := cbn [type.related_hetero ZRange.ident.option.interp ident.interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some]; @@ -621,9 +632,13 @@ Module Compilers. break_innermost_match; apply Bool.andb_true_iff; split; apply Z.leb_le; try apply Z.le_sub_1_iff; auto with zarith. } Qed. - Lemma interp_related {t} (idc : ident t) : interp_is_related idc. + (** In abstract interpretation, we only need this version of the lemma for less-than-third-order types, but in Assembly/Symbolic, we use it for all identifiers *) + Lemma interp_related {t} (idc : ident t) (*H : type.is_not_higher_order_than 3 t = true*) : interp_is_related idc. Proof using Type. destruct idc. + (* + (** clear out higher-than-third-order types *) + all: cbn in H; try congruence.*) all: lazymatch goal with | [ |- context[ident.Z_cast] ] => apply interp_related_Z_cast | [ |- context[ident.Z_cast2] ] => apply interp_related_Z_cast2 @@ -735,13 +750,24 @@ Module Compilers. => Z.div_mod_to_quot_rem; nia end | intros; mul_by_halves_t ]. + all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ]. (** For command-line debugging, we display goals that should not remain *) - all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. | | ]. - { intros. - rewrite Z.le_sub_1_iff. - break_innermost_match; Z.ltb_to_lt; - auto with zarith. } - { non_arith_t; Z.ltb_to_lt; reflexivity. } + all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ]. + Qed. + + Lemma interp_related_and_Proper {t} (idc : ident t) : interp_is_related_and_Proper idc. + Proof using Type. + destruct (type.is_not_higher_order_than 3 t) eqn:Hho. + { apply type.related_hetero_impl_related_hetero_and_Proper_eqv_not_higher_order_than_3. + all: try apply interp_related. + all: try apply ident.interp_Proper. + all: try apply ZRange.ident.option.interp_Proper. + all: try assumption. + all: try reflexivity. } + { destruct idc. + all: try (apply Bool.diff_true_false in Hho; exfalso; exact Hho). + (** For command-line debugging, we display goals that should not remain *) + all: [ > idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal () .. ]. } Qed. End interp_related. End option. diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 5df6d6a5e7..4d21680e4e 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -1375,7 +1375,7 @@ Module Pipeline. let e' := fresh "e" in destruct v as [e'|e'] eqn:H; cbv beta iota in Hrv; - [ apply CheckedPartialEvaluateWithBounds_Correct in H; + [ apply CheckedPartialEvaluateWithBounds_Correct_first_order in H; [ let Hwf' := fresh "Hwf" in rewrite (correct_of_final_iff_correct_of_initial Hinterp) in H by assumption; destruct H as [? Hwf']; split_and;