From 844b223ff137574d94e34bed2e3d57ccba44ddae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 15 Aug 2023 19:08:50 -0400 Subject: [PATCH] Avoid bottomify-ing higher order functions Reworked value type to more closely match the possible spec. Deduplicated `interp_ident` / `abstract_interp_ident` overlapped state. The specification of `reify` and `reflect` has been simplified to more closely match the intuition: `reify`'s spec no longer talks about output bounds, only interpretation, and a companion lemma `abstraction_relation_of_related_bounded_value'` shows that the spec of `reflect` is effectively one direction of an isomorphism between interpreted-values bounded by abstract state, and `value`s which are in relationship with the given interpreted-value. Not really sure how best to describe this in words yet, probably needs some digesting work. There's some interesting lemmas where we have an equivalency between two ways of representing things only for up-to-second-order types, and an implication for up-to-third-order types, which is currently all the identifiers. But this means that if we add fourth-order identifiers, we'll have to deal with two different sorts of `Proper` abstraction relations (one used by `Assembly/Symbolic` and one used by bounds analysis, though it's possible the `Assembly/Symbolic` one can be adapted). --- .../AbstractInterpretation.v | 300 ++--- src/AbstractInterpretation/Proofs.v | 1098 +++++++++-------- src/AbstractInterpretation/Wf.v | 517 +++++--- src/AbstractInterpretation/ZRangeProofs.v | 40 +- src/BoundsPipeline.v | 2 +- 5 files changed, 1128 insertions(+), 829 deletions(-) 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;