diff options
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 946 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationWf.v | 825 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 3 |
4 files changed, 909 insertions, 866 deletions
diff --git a/_CoqProject b/_CoqProject index afb75162c..84e328de7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -244,6 +244,7 @@ src/Experiments/PartialEvaluationWithLetIn.v src/Experiments/SimplyTypedArithmetic.v src/Experiments/NewPipeline/AbstractInterpretation.v src/Experiments/NewPipeline/AbstractInterpretationProofs.v +src/Experiments/NewPipeline/AbstractInterpretationWf.v src/Experiments/NewPipeline/Arithmetic.v src/Experiments/NewPipeline/CLI.v src/Experiments/NewPipeline/CStringification.v diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index 8a5905d92..1b985bda2 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -23,6 +23,7 @@ Require Import Crypto.Experiments.NewPipeline.LanguageInversion. Require Import Crypto.Experiments.NewPipeline.LanguageWf. Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. +Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationWf. Module Compilers. Import Language.Compilers. @@ -31,6 +32,8 @@ Module Compilers. Import LanguageInversion.Compilers. Import LanguageWf.Compilers. Import UnderLetsProofs.Compilers. + Import AbstractInterpretationWf.Compilers. + Import AbstractInterpretationWf.Compilers.partial. Import invert_expr. Module Import partial. @@ -54,362 +57,31 @@ Module Compilers. 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')). - - 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 base_type ident var1 abstract_domain'). - Local Notation value2 := (@value base_type ident var2 abstract_domain'). - 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'). - 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 - : forall is_let_bound t G - 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 : forall t, ident t -> value_with_lets1 t) - (interp_ident2 : forall t, ident t -> value_with_lets2 t). - 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 interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). - Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). - Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). - Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). - Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). - Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). - 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'). - - Definition abstract_domain_R {t} : relation (abstract_domain t) - := type.related abstract_domain'_R. - - (** 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 - 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) - | type.arrow s d - => fun v1 v2 - => abstract_domain_R (fst v1) (fst v2) - /\ (forall seg G' sv1 sv2, - G' = (seg ++ G)%list - -> @wf_value seg s sv1 sv2 - -> UnderLets.wf - (fun G' => @wf_value G' d) G' - (snd v1 sv1) (snd 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. - - Context (interp_ident_Proper - : forall G t idc1 idc2 (Hidc : idc1 = idc2), - wf_value_with_lets G (interp_ident1 t idc1) (interp_ident2 t idc2)). - - Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10. - Proof using bottom'_Proper. - clear -bottom'_Proper type_base. - cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto. - Qed. - - Global Instance bottom_for_each_lhs_of_arrow_Proper {t} - : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) (@bottom_for_each_lhs_of_arrow t) | 10. - Proof using bottom'_Proper. - clear -bottom'_Proper type_base. - pose proof (@bottom_Proper). - cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto. + Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R). + + Section extract. + Context (ident_extract : forall t, ident t -> abstract_domain t) + {ident_extract_Proper : forall {t}, Proper (eq ==> abstract_domain_R) (ident_extract t)}. + + Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract). + Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract). + + Lemma extract'_Proper G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2) + {t} + : Proper (expr.wf G ==> abstract_domain_R) (@extract' t). + Proof using ident_extract_Proper. apply expr.wf_interp_Proper_gen1, HG. Qed. + + Lemma extract_gen_Proper G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2) + {t} + : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract_gen t). + Proof using ident_extract_Proper. + intros ?? Hwf; cbv [extract_gen respectful abstract_domain_R]. + rewrite <- type.related_iff_app_curried. + eapply extract'_Proper; eassumption. Qed. - - 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 Type. - clear -Hv type_base. - destruct t, v1, v2, Hv; cbn in *; cbv [respectful]; eauto. - Qed. - - Local Hint Resolve (ex_intro _ nil) (ex_intro _ (cons _ nil)). - Local Hint Constructors expr.wf ex. - Local Hint Unfold List.In. - - 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. - clear -type_base HG1G2 Hwf. - revert dependent G1; revert dependent G2; induction t; intros; - repeat first [ progress cbn in * - | progress intros - | solve [ eauto ] - | progress subst - | progress destruct_head'_and - | progress destruct_head'_or - | apply conj - | rewrite List.in_app_iff in * - | match goal with H : _ |- _ => apply H; clear H end - | wf_unsafe_t_step - | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ]. - Qed. - - Fixpoint wf_reify (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), - UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2) - with wf_reflect G {t} - : forall e1 e2 (He : expr.wf G e1 e2) - s1 s2 (Hs : abstract_domain_R s1 s2), - @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2). - Proof using annotate_Proper bottom'_Proper. - all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper. - all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper] in *. - { destruct t as [t|s d]; - [ clear wf_reify wf_reflect - | specialize (fun G => wf_reflect G s); - specialize (fun G => wf_reify false G d) ]. - { cbn; intros [? ?] [? ?] [Hv0 Hv1] [] [] []; - cbn [fst snd] in *. - apply annotate_Proper; assumption. } - { cbn; cbv [respectful]; intros [? ?] [? ?] [He0 He1] [? ?] [? ?] [Hs0 Hs1]; - cbn [fst snd] in *. - do 2 constructor; intros v1 v2. - eapply UnderLets.wf_to_expr, UnderLets.wf_splice. - { eapply He1 with (seg:=cons _ nil); eauto using eq_refl. } - { intros; apply wf_reify; destruct_head'_ex; subst; auto. } } } - { destruct t as [t|s d]; - [ clear wf_reify wf_reflect - | specialize (fun G => wf_reflect G d); - specialize (fun G => wf_reify false G s) ]. - { cbn; auto. } - { cbn; cbv [respectful]; intros e1 e2 He s1 s2 Hs; - split; [ solve [ auto ] | ]; - intros G' seg sv1 sv2 HG1G2 Hsv; subst. - eapply UnderLets.wf_splice. - { apply wf_reify; auto; eapply wf_value_Proper_list; [ .. | solve [ eauto ] ]; - wf_safe_t. } - { intros G'' a1 a2 [seg' ?] Ha; subst G''. - constructor. - apply wf_reflect. - { constructor; auto; wf_unsafe_t_step; []. - destruct_head'_ex; subst. - intros *. - rewrite !List.in_app_iff; auto. } - { eapply Hs, state_of_value_Proper; eassumption. } } } } - 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 * - | wf_safe_t_step - | exact I - | apply wf_reify - | apply bottom_Proper - | progress destruct_head'_ex - | progress destruct_head'_or - | eapply UnderLets.wf_splice - | match goal with - | [ |- UnderLets.wf _ _ _ _ ] => constructor - | [ |- and _ _ ] => apply conj - end - | eapply wf_value_Proper_list; [ | solve [ eauto ] ] - | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] - | match goal with - | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ] - end - | break_innermost_match_step ]. - - Lemma wf_interp 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 e1) (interp2 e2). - Proof using annotate_Proper bottom'_Proper interp_ident_Proper. - revert dependent G'; induction Hwf; intros; cbn [interp]; - try solve [ apply interp_ident_Proper; auto - | eauto ]; - wf_interp_t. - Qed. - - Lemma wf_eval_with_bound' 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 t e1 st1) (@eval_with_bound'2 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. } - 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. - eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper. - Qed. - - Lemma wf_eta_expand_with_bound' 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) - : expr.wf G (@eta_expand_with_bound'1 t e1 st1) (@eta_expand_with_bound'2 t e2 st2). - Proof using annotate_Proper bottom'_Proper. - eapply UnderLets.wf_to_expr, wf_reify; [ eapply wf_reflect | ]; eauto; apply bottom_Proper. - Qed. - - (* - Lemma related_force {t} x y - : @lazy_abstract_domain_R t x y <-> @abstract_domain_R t (force_abstract_domain x) (force_abstract_domain y). - Proof. - induction t as [t|s IHs d IHd]; [ reflexivity | ]. - cbv [lazy_abstract_domain_R abstract_domain_R] in *; cbn [type.related] in *; cbv [respectful] in *. - setoid_rewrite IHs; setoid_rewrite IHd. - progress change (@force_abstract_domain (s -> d)) with (fun f x => @force_abstract_domain d (f (@thunk_abstract_domain s x))). - cbv beta iota. - (*progress change (@thunk_abstract_domain (s -> d)) with (fun f x => @thunk_abstract_domain d (f (@force_abstract_domain s x))).*) - intuition. - { match goal with - | [ H : _ |- _ ] => apply H; rewrite !force_thunk_abstract_domain_ext; assumption - end. } - { match goal with - | [ |- ?R (force_abstract_domain (?f ?x)) (force_abstract_domain (?g ?y)) ] - => rewrite <- (force_thunk_abstract_domain_ext x), <- (force_thunk_abstract_domain_ext y) - end. - eauto. - intuition (rewrite ?force_thunk_abstract_domain_ext; eauto). - apply H. - *) - (* - Section extract. - Context (ident_extract : forall t, ident t -> lazy_abstract_domain t) - {ident_extract_Proper : forall {t}, Proper (eq ==> lazy_abstract_domain_R) (ident_extract t)}. - - Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract). - Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract). - - Lemma extract'_Proper G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @lazy_abstract_domain_R t v1 v2) - {t} - : Proper (expr.wf G ==> lazy_abstract_domain_R) (@extract' t). - Proof using ident_extract_Proper. - clear -ident_extract_Proper HG type_base; cbv [lazy_abstract_domain_R]. - intros ? ? Hwf. - induction Hwf; red_thunk_force; cbn -[thunk_abstract_domain force_abstract_domain] in *; red_thunk_force; - cbv [respectful] in *; try apply ident_extract_Proper; intros; eauto; - try solve [ repeat first [ progress intros - | progress cbn [List.In fst snd] in * - | progress cbv [lazy_abstract_domain_R] in * - | rewrite force_thunk_abstract_domain_ext - | progress wf_safe_t - | match goal with - | [ H : _ |- _ ] => eapply H; clear H - end ] ]. - repeat first [ progress intros - | progress cbn [List.In fst snd] in * - | progress cbv [lazy_abstract_domain_R] in * - | rewrite force_thunk_abstract_domain_ext - | progress wf_safe_t ]. - eapply IHHwf1. - match goal with - | [ H : _ |- _ ] => eapply H; clear H - end. - { repeat first [ progress intros - | progress cbn [List.In fst snd] in * - | progress cbv [lazy_abstract_domain_R] in * - | rewrite force_thunk_abstract_domain_ext - | progress wf_safe_t ]. - . - - Qed. - - Local Lemma pull_prod_forall A A' B B' (Q : A * A' -> B * B' -> Prop) - : (forall x y, Q x y) <-> (forall x0 y0 x1 y1, Q (x0, x1) (y0, y1)). - Proof. intuition. Qed. - - Lemma abstract_domain_R_app_curried_iff t F G - : (@abstract_domain_R t F G) - <-> (forall x y, type.and_for_each_lhs_of_arrow (@abstract_domain_R) x y -> abstract_domain'_R (type.final_codomain t) (type.app_curried F x) (type.app_curried G y)). - Proof using Type. - clear -type_base. - induction t as [t|s IHs d IHd]; cbn; [ tauto | ]. - cbv [respectful]. - rewrite pull_prod_forall. - lazymatch goal with - | [ |- (forall x y, @?P x y) <-> (forall z w, @?Q z w) ] - => cut (forall x y, (P x y <-> Q x y)); [ intro H'; setoid_rewrite H'; reflexivity | intros ??; cbn [fst snd] ] - end. - lazymatch goal with - | [ |- (?P -> ?Q) <-> (forall z w, ?P' /\ @?R z w -> @?S z w) ] - => unify P P'; cut (P' -> (Q <-> (forall z w, R z w -> S z w))); [ change P with P'; solve [ intuition ] | intro; cbn [fst snd] ] - end. - eauto. - Qed. - - Lemma lazy_abstract_domain_R_app_curried_iff t F G - : (@lazy_abstract_domain_R t F G) - <-> (forall x y, type.and_for_each_lhs_of_arrow (@abstract_domain_R) x y -> abstract_domain'_R (type.final_codomain t) (type.app_curried F (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) x) tt) (type.app_curried G (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) y) tt)). - Proof using Type. - clear -type_base. - induction t as [t|s IHs d IHd]; cbn; [ tauto | ]. - cbv [respectful]. - rewrite pull_prod_forall; cbn. - lazymatch goal with - | [ |- (forall x y, @?P x y) <-> (forall z w, @?Q z w) ] - => cut (forall x y, (P x y <-> Q (force_abstract_domain x) (force_abstract_domain y))); [ intro H'; setoid_rewrite H' | intros ??; cbn [fst snd] ] - end. - { cbn; intuition. - match goal with - | [ H : _ |- ?R (type.app_curried (?F ?x) _ _) (type.app_curried (?G ?y) _ _) ] - => specialize (H x y); rewrite !force_thunk_abstract_domain_ext in H; apply H; auto - end. } - lazymatch goal with - | [ |- (?P -> ?Q) <-> (forall z w, ?P' /\ @?R z w -> @?S z w) ] - => unify P P'; cut (P' -> (Q <-> (forall z w, R z w -> S z w))); [ change P with P'; solve [ intuition ] | intro; cbn [fst snd] ] - end. - eauto. - Qed. - - Lemma extract_gen_Proper G - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @lazy_abstract_domain_R t v1 v2) - {t} - : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract_gen t). - Proof. - intros ?? Hwf ?? Hv; cbv [extract_gen]. - generalize (@extract'_Proper G HG t _ _ Hwf). - generalize (extract' x) (extract' y); clear x y G HG Hwf; intros x y Hwf. - generalize (conj Hv Hwf). - clear Hv Hwf. - - setoid_rewrite abstract_domain_R_app_curried_iff. - lazymatch goal with - | [ |- ?X -> ?Y ] => cut (X <-> Y); [ tauto | ] - end. - induction t; [ solve [ intuition eauto; constructor ] | ]; - cbn [type.final_codomain type.app_curried type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow type.map_for_each_lhs_of_arrow fst snd] in *. - destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. - rewrite <- IHt2. - rewrite !and_assoc, !(and_comm (type.and_for_each_lhs_of_arrow _ _ _)), <- !and_assoc. - lazymatch goal with - | [ |- (?A /\ ?B) <-> (?C /\ ?B) ] => cut (A <-> C); [ tauto | ] - end. - Definition extract_gen {t} (e : @expr lazy_abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t) - : abstract_domain' (type.final_codomain t) - := type.app_curried (extract' e) (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) bound) tt. - End extract.*) - - End with_var2. + End extract. End with_type. Module ident. @@ -433,338 +105,17 @@ Module Compilers. (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2)) (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2). - Local Instance abstract_interp_ident_Proper_arrow s d - : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d)) - := abstract_interp_ident_Proper (type.arrow s d). - - Section with_var2. - Context {var1 var2 : type -> Type}. - - Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation). - Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation). - Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation). - Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation). - Print ident.annotate_with_ident. - Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation). - Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation). - Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom'). - Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom'). - - Lemma wf_update_annotation G {t} st1 st2 (Hst : abstract_domain'_R t st1 st2) e1 e2 (He : expr.wf G e1 e2) - : expr.wf G (@update_annotation1 t st1 e1) (@update_annotation2 t st2 e2). - Proof. - cbv [ident.update_annotation]; - repeat first [ progress subst - | progress expr.invert_subst - | progress cbn [fst snd projT1 projT2 eq_rect] in * - | progress cbn [invert_AppIdent Option.bind invert_App invert_Ident] in * - | progress destruct_head'_sig - | progress destruct_head'_sigT - | progress destruct_head'_and - | progress destruct_head'_prod - | progress destruct_head' False - | progress inversion_option - | progress expr.inversion_wf_constr - | progress expr.inversion_wf_one_constr - | break_innermost_match_hyps_step - | expr.invert_match_step - | progress expr.inversion_expr - | progress rewrite_type_transport_correct - | progress type_beq_to_eq - | progress type.inversion_type - | progress base.type.inversion_type - | match goal with - | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H; clear dependent x - end - | progress wf_safe_t - | break_innermost_match_step ]. - Qed. - - Lemma wf_annotate_with_ident - is_let_bound t G - 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 (@annotate_with_ident1 is_let_bound t v1 e1) (@annotate_with_ident2 is_let_bound t v2 e2). - Proof. - cbv [ident.annotate_with_ident]; break_innermost_match; repeat constructor; apply wf_update_annotation; assumption. - Qed. - - Lemma wf_annotate_base - is_let_bound (t : base.type.base) G - 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 (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2). - Proof. - cbv [ident.annotate_base]; - repeat first [ apply wf_annotate_with_ident - | break_innermost_match_step - | progress subst - | progress cbv [type_base ident.smart_Literal] in * - | progress cbn [invert_Literal ident.invert_Literal] in * - | discriminate - | progress destruct_head' False - | progress expr.invert_subst - | progress expr.inversion_wf - | wf_safe_t_step - | break_innermost_match_hyps_step - | match goal with - | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H - | [ |- UnderLets.wf _ _ _ _ ] => constructor - | [ H : abstract_domain'_R _ _ _ |- _ ] => rewrite !H - end - | progress expr.invert_match_step - | progress expr.inversion_expr ]. - Qed. - - Lemma wf_annotate - is_let_bound t G - 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). - Proof. - revert dependent G; induction t; intros; - cbn [ident.annotate]; try apply wf_annotate_base; trivial. - all: repeat first [ lazymatch goal with - | [ 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 |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H - | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list - | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ] - => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length - | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence - | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain'_R _ ?v1 ?v2 |- _ ] - => let Hl := fresh in - let Hl' := fresh in - pose proof (extract_list_state_length _ v1 v2 Hv) as Hl; - pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl'; - rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H' - | [ H : ?x = ?x |- _ ] => clear H - | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' - end - | apply wf_annotate_with_ident - | apply DefaultValue.expr.base.wf_default - | apply DefaultValue.expr.wf_default - | progress expr.invert_subst - | progress cbn [ident.annotate ident.smart_Literal invert_Literal ident.invert_Literal invert_pair invert_AppIdent2 invert_App2 fst snd projT2 projT1 eq_rect Option.bind] in * - | progress destruct_head' False - | progress inversion_option - | progress destruct_head'_ex - | discriminate - | wf_safe_t_step - | progress expr.inversion_wf_constr - | progress expr.inversion_expr - | progress type_beq_to_eq - | progress type.inversion_type - | progress base.type.inversion_type - | match goal with - | [ |- expr.wf _ (update_annotation1 _ _) (update_annotation2 _ _) ] => apply wf_update_annotation - | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H - | [ |- UnderLets.wf _ _ _ _ ] => constructor - | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H - | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice - | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H - | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H - | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine - | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ] - => specialize (H _ _ eq_refl eq_refl) - | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n = Some ?a1, H'' : List.nth_error ?l2 ?n = Some ?a2 - |- ?R ?a1 ?a2 ] - => apply H - | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n') - end - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress expr.invert_match - | progress expr.inversion_wf_one_constr - | match goal with - | [ H : context[UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _)] - |- UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _) ] => eapply H - end - | apply abstract_interp_ident_Proper_arrow - | progress rewrite_type_transport_correct - | apply conj - | congruence - | solve [ wf_t ] ]. - Qed. - - 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). - - Lemma wf_interp_ident_nth_default G T - : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)). - Proof. - cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain]. - split. - { exact (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl). } - { intros; subst. - destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. - repeat first [ progress subst - | progress cbn [invert_Literal ident.invert_Literal] in * - | lazymatch goal with - | [ 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 |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H - | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list - | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ] - => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length - | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence - | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ] - => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence - | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain_R ?v1 ?v2 |- _ ] - => let Hl := fresh in - let Hl' := fresh in - pose proof (extract_list_state_length _ v1 v2 Hv) as Hl; - pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl'; - rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H' - | [ H : ?x = ?x |- _ ] => clear H - | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' - end - | match goal with - | [ |- UnderLets.wf ?Q ?G (UnderLets.splice ?x1 ?e1) (UnderLets.splice ?x2 ?e2) ] - => simple refine (@UnderLets.wf_splice _ _ _ _ _ _ _ _ _ Q G x1 x2 _ e1 e2 _); - [ let G := fresh "G" in - intro G; - lazymatch goal with - | [ |- (abstract_domain ?t * _) -> _ -> _ ] - => refine (@wf_value G t) - | [ |- expr _ -> _ -> _ ] - => refine (expr.wf G) - end - | | ] - | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ] - => constructor - | [ 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) - | [ 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 - | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H - | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H - | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H - | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine - | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ] - => specialize (H _ _ eq_refl eq_refl) - | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n' = Some ?a1, H'' : List.nth_error ?l2 ?n' = Some ?a2 - |- _ ] - => unique pose proof (H a1 a2 ltac:(apply nth_error_In with (n:=n'); rewrite nth_error_combine, H', H''; reflexivity)) - | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n') - | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H) - | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H - end - | progress inversion_option - | progress intros - | progress cbn [fst snd value] in * - | progress destruct_head'_prod - | progress destruct_head'_ex - | progress destruct_head'_and - | progress destruct_head' False - | progress specialize_by_assumption - | apply conj - | progress expr.invert_subst - | progress expr.inversion_wf_constr - | progress expr.inversion_expr - | 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 wf_update_annotation; wf_t - | wf_t - | match goal with - | [ H : context[UnderLets.wf _ _ _ _] |- UnderLets.wf _ _ _ _ ] => eapply H; solve [ repeat esplit; eauto ] - end - | eauto using List.nth_error_In - | eapply expr.wf_Proper_list; [ | eassumption ]; wf_safe_t; eauto 10 ] - | break_innermost_match_step - | match goal with - | [ H : context[List.In] |- expr.wf _ ?x ?y ] - => specialize (H x y); rewrite !List.nth_default_eq, <- List.combine_nth, <- !List.nth_default_eq in H; cbv [List.nth_default] in H |- * - | [ H : List.In _ _ -> ?P |- ?P ] => apply H - end - | break_innermost_match_hyps_step - | congruence - | rewrite List.combine_length in * - | rewrite NPeano.Nat.min_r in * by lia - | rewrite NPeano.Nat.min_l in * by lia - | progress expr.inversion_wf_one_constr - | progress expr.invert_match ]. } - Qed. - - Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t) - : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###idc)%expr (abstract_interp_ident _ idc))). - Proof. - constructor; eapply wf_reflect; - solve [ apply bottom'_Proper - | apply wf_annotate - | repeat constructor - | apply abstract_interp_ident_Proper; reflexivity ]. - Qed. - - Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2) - : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2). - Proof. - 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 ]. - Qed. - - Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Lemma wf_eval_with_bound {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 t e1 st1) (@eval_with_bound2 t e2 st2). - Proof. - eapply wf_eval_with_bound'; - solve [ eassumption - | eapply wf_annotate - | eapply wf_interp_ident ]. - Qed. - - Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - 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). - Proof. - eapply wf_eval'; - solve [ eassumption - | eapply wf_annotate - | eapply wf_interp_ident ]. - Qed. + Section extract. + Local Notation extract := (@ident.extract abstract_domain' abstract_interp_ident). - Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). - Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2). - Proof. - eapply wf_eta_expand_with_bound'; - solve [ eassumption - | eapply wf_annotate - | eapply wf_interp_ident ]. + Lemma extract_Proper G + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2) + {t} + : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract t). + Proof using abstract_interp_ident_Proper. + apply @extract_gen_Proper; eauto. Qed. - - Section extract. - (* - 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' (@ident_extract) t e bound. - *) - End extract. - End with_var2. + End extract. End with_type. End ident. @@ -778,12 +129,6 @@ Module Compilers. 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. - Global Instance annotate_ident_Proper {t} : Proper (abstract_domain'_R t ==> eq) (annotate_ident t). - Proof. - intros st st' ?; subst st'. - cbv [annotate_ident]; break_innermost_match; reflexivity. - Qed. - Lemma interp_annotate_ident {t} st idc (Hst : @annotate_ident t st = Some idc) : forall v, abstraction_relation' st v @@ -800,41 +145,12 @@ Module Compilers. : @annotate_ident t st1 = @annotate_ident t st2. Proof. congruence. Qed. - Global Instance bottom'_Proper {t} : Proper (abstract_domain'_R t) (bottom' t). - Proof. reflexivity. Qed. - Lemma bottom'_bottom {t} : forall v, abstraction_relation' (bottom' t) v. Proof. cbv [abstraction_relation' bottom']; induction t; cbn; intros; break_innermost_match; cbn; try reflexivity. rewrite Bool.andb_true_iff; split; auto. Qed. - Global Instance abstract_interp_ident_Proper {t} - : Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t). - Proof. - cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc; - repeat first [ reflexivity - | progress subst - | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Option.bind] in * - | progress cbv [Option.bind] - | intro - | progress destruct_head'_prod - | progress destruct_head'_bool - | progress destruct_head' option - | solve [ eauto ] - | apply NatUtil.nat_rect_Proper_nondep - | apply ListUtil.list_rect_Proper - | apply ListUtil.list_case_Proper - | apply ListUtil.pointwise_map - | apply ListUtil.fold_right_Proper - | apply ListUtil.update_nth_Proper - | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature) - | cbn; apply (f_equal (@Some _)) - | match goal with - | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity)) - end ]. - Qed. - Lemma abstract_interp_ident_related {t} (idc : ident t) : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (ident.interp idc). Proof. @@ -842,10 +158,6 @@ Module Compilers. all: cbv [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some]. Admitted. - Global Instance update_literal_with_state_Proper {t} - : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t). - Proof. repeat intro; congruence. Qed. - Lemma interp_update_literal_with_state {t : base.type.base} st v : @abstraction_relation' t st v -> @update_literal_with_state t st v = v. Proof. @@ -853,26 +165,6 @@ Module Compilers. break_innermost_match; try congruence; reflexivity. Qed. - Global Instance extract_list_state_Proper {t} - : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t))) - (extract_list_state t). - Proof. - intros st st' ?; subst st'; cbv [option_eq extract_list_state]; break_innermost_match; reflexivity. - Qed. - - Lemma extract_list_state_length - : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2). - Proof. - intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity. - Qed. - Lemma extract_list_state_rel - : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2. - Proof. - intros; cbv [extract_list_state] in *; subst; inversion_option; subst. - rewrite combine_same, List.in_map_iff in *. - destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity. - Qed. - Lemma extract_list_state_related {t} st v ls : @abstraction_relation' _ st v -> @extract_list_state t st = Some ls @@ -889,77 +181,22 @@ Module Compilers. intros; destruct_head'_and; destruct_head'_or; inversion_prod; subst; eauto. } Qed. - 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 {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' (@eval var1 t e1) (@eval var2 t e2). - Proof. - eapply ident.wf_eval; - solve [ eassumption - | exact _ - | apply extract_list_state_length - | apply extract_list_state_rel ]. - Qed. - - Lemma wf_eval_with_bound {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_bound var1 t e1 st1) (@eval_with_bound var2 t e2 st2). - Proof. - eapply ident.wf_eval_with_bound; - solve [ eassumption - | exact _ - | apply extract_list_state_length - | apply extract_list_state_rel ]. - Qed. - - - Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) - : expr.wf G (@eta_expand_with_bound var1 t e1 st1) (@eta_expand_with_bound var2 t e2 st2). - Proof. - eapply ident.wf_eta_expand_with_bound; - solve [ eassumption - | exact _ - | apply extract_list_state_length - | apply extract_list_state_rel ]. - Qed. - End with_var2. - - Lemma Wf_Eval {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e). - Proof. - intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto. - Qed. - - Lemma Wf_EvalWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) - : Wf (EvalWithBound e bound). + Lemma Extract_FromFlat_ToFlat' {t} (e : Expr t) (Hwf : Wf e) b_in1 b_in2 + (Hb : type.and_for_each_lhs_of_arrow (fun t => type.eqv) b_in1 b_in2) + : partial.Extract (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e)) b_in1 + = partial.Extract e b_in2. Proof. - intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + cbv [partial.Extract partial.ident.extract partial.extract_gen partial.extract']. + revert b_in1 b_in2 Hb. + rewrite <- (@type.related_iff_app_curried base.type ZRange.type.base.option.interp (fun _ => eq)). + apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat, Hwf. Qed. - Lemma Wf_EtaExpandWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) - : Wf (EtaExpandWithBound e bound). - Proof. - intros ??; eapply wf_eta_expand_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto. - Qed. - - Local Instance Proper_strip_ranges {t} - : Proper (@abstract_domain_R t ==> @abstract_domain_R t) (@ZRange.type.option.strip_ranges t). - Proof. - cbv [Proper abstract_domain_R respectful]. - induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; intros; subst; cbv [respectful] in *; - eauto. - Qed. - - Lemma Wf_EtaExpandWithListInfoFromBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) - : Wf (EtaExpandWithListInfoFromBound e bound). - Proof. - eapply Wf_EtaExpandWithBound; [ assumption | ]. - clear dependent e. - cbv [Proper] in *; induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; eauto. - split; auto; apply Proper_strip_ranges; auto. - Qed. + Lemma Extract_FromFlat_ToFlat {t} (e : Expr t) (Hwf : Wf e) b_in + (Hb : Proper (type.and_for_each_lhs_of_arrow (fun t => type.eqv)) b_in) + : partial.Extract (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e)) b_in + = partial.Extract e b_in. + Proof. apply Extract_FromFlat_ToFlat'; assumption. Qed. End specialized. End partial. Import defaults. @@ -1026,35 +263,6 @@ Module Compilers. (Hrelax : forall r r' z, is_tighter_than_bool z r = true -> relax_zrange r = Some r' -> is_tighter_than_bool z r' = true). - Section with_var2. - Context {var1 var2 : type -> Type}. - - Lemma wf_relax G {t} (e1 : @expr var1 t) (e2 : @expr var2 t) - (Hwf : expr.wf G e1 e2) - : expr.wf G (@RelaxZRange.expr.relax relax_zrange var1 t e1) (@RelaxZRange.expr.relax relax_zrange var2 t e2). - Proof using Type. - clear -Hwf. - induction Hwf; wf_safe_t. - cbn [RelaxZRange.expr.relax]; cbv [option_map] in *. - break_innermost_match; - repeat first [ progress wf_safe_t - | progress expr.invert_subst - | progress expr.inversion_wf_constr - | progress destruct_head' False - | progress inversion_option - | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in * - | match goal with - | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ] - => rewrite H' in H - | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ] - => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match - | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - end - | progress expr.inversion_wf_one_constr ]. - Qed. - End with_var2. - Lemma interp_relax {t} (e : expr t) v (Hinterp : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e) v @@ -1103,8 +311,6 @@ Module Compilers. end ]. Admitted. - Lemma Wf_Relax {t} (e : Expr t) (Hwf : Wf e) : Wf (@RelaxZRange.expr.Relax relax_zrange t e). - Proof. intros ??; eapply wf_relax, Hwf. Qed. Lemma Interp_Relax {t} (e : Expr t) v (Hinterp : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) v @@ -1120,23 +326,31 @@ Module Compilers. Axiom admit_pf : False. Local Notation admit := (match admit_pf with end). - Lemma Wf_PartialEvaluateWithListInfoFromBounds + Lemma Interp_PartialEvaluateWithBounds + cast_outside_of_range {t} (E : Expr t) - (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (Hwf : Wf E) - {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} - : Wf (PartialEvaluateWithListInfoFromBounds E b_in). - Proof. apply Wf_EtaExpandWithListInfoFromBound; assumption. Qed. - Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf. + (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) + (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), + type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1 + = type.app_curried (Interp E) arg2. + Proof. + Admitted. - Lemma Wf_PartialEvaluateWithBounds + Lemma Interp_PartialEvaluateWithBounds_bounded {t} (E : Expr t) - (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (Hwf : Wf E) - {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} - : Wf (PartialEvaluateWithBounds E b_in). - Proof. eapply partial.Wf_EvalWithBound; assumption. Qed. - Hint Resolve Wf_PartialEvaluateWithBounds : wf. + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + : forall arg1 + (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 + (partial.Extract (PartialEvaluateWithBounds E b_in) b_in) + (type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds E b_in)) arg1) + = true. + Proof. + Admitted. Lemma Interp_PartialEvaluateWithListInfoFromBounds {t} (E : Expr t) @@ -1149,8 +363,6 @@ Module Compilers. Proof. Admitted. - Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf. - Theorem CheckedPartialEvaluateWithBounds_Correct (relax_zrange : zrange -> option zrange) (Hrelax : forall r r' z, is_tighter_than_bool z r = true @@ -1174,16 +386,18 @@ Module Compilers. break_innermost_match_hyps; inversion_sum; subst. split. { 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 ]). split. - { eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]. - clear dependent arg2. - cbv [ident.interp]; rewrite RelaxZRange.expr.Interp_Relax; eauto. - all: revert Harg1. - all: exact admit. (* boundedness *) } - { intro cast_outside_of_range; revert cast_outside_of_range Harg12. - intros ? Harg; rewrite RelaxZRange.expr.Interp_Relax; eauto. - all: revert Harg. - all: exact admit. (* correctness of interp *) } } + all: repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances + | rewrite Extract_FromFlat_ToFlat by auto with wf + | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ] + | apply Interp_PartialEvaluateWithBounds_bounded; auto + | progress cbv [ident.interp] + | rewrite RelaxZRange.expr.Interp_Relax; eauto + | erewrite !Interp_PartialEvaluateWithBounds + | solve [ eauto ] + | progress intros ]. } { auto with wf. } Qed. End Compilers. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/Experiments/NewPipeline/AbstractInterpretationWf.v new file mode 100644 index 000000000..ecd52ddec --- /dev/null +++ b/src/Experiments/NewPipeline/AbstractInterpretationWf.v @@ -0,0 +1,825 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.Morphisms. +Require Import Coq.Classes.RelationPairs. +Require Import Coq.Relations.Relations. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.Sum. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.BreakMatch. +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.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. +Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. + +Module Compilers. + Import Language.Compilers. + Import UnderLets.Compilers. + Import AbstractInterpretation.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import UnderLetsProofs.Compilers. + Import invert_expr. + + Module Import partial. + Import AbstractInterpretation.Compilers.partial. + Import NewPipeline.UnderLets.Compilers.UnderLets. + Section with_type. + Context {base_type : Type}. + Local Notation type := (type base_type). + Let type_base (x : base_type) : type := type.base x. + Local Coercion type_base : base_type >-> type. + Context {ident : type -> Type}. + Local Notation expr := (@expr base_type ident). + Local Notation Expr := (@expr.Expr base_type ident). + Local Notation UnderLets := (@UnderLets base_type ident). + Context (abstract_domain' : base_type -> Type) + (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 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')). + + 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 base_type ident var1 abstract_domain'). + Local Notation value2 := (@value base_type ident var2 abstract_domain'). + 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'). + 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 + : forall is_let_bound t G + 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 : forall t, ident t -> value_with_lets1 t) + (interp_ident2 : forall t, ident t -> value_with_lets2 t). + 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 interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1). + Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2). + 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'). + + Definition abstract_domain_R {t} : relation (abstract_domain t) + := type.related abstract_domain'_R. + + (** 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 + 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) + | type.arrow s d + => fun v1 v2 + => abstract_domain_R (fst v1) (fst v2) + /\ (forall seg G' sv1 sv2, + G' = (seg ++ G)%list + -> @wf_value seg s sv1 sv2 + -> UnderLets.wf + (fun G' => @wf_value G' d) G' + (snd v1 sv1) (snd 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. + + Context (interp_ident_Proper + : forall G t idc1 idc2 (Hidc : idc1 = idc2), + wf_value_with_lets G (interp_ident1 t idc1) (interp_ident2 t idc2)). + + Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10. + Proof using bottom'_Proper. + clear -bottom'_Proper type_base. + cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto. + Qed. + + Global Instance bottom_for_each_lhs_of_arrow_Proper {t} + : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) (@bottom_for_each_lhs_of_arrow t) | 10. + Proof using bottom'_Proper. + clear -bottom'_Proper type_base. + pose proof (@bottom_Proper). + cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto. + Qed. + + 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 Type. + clear -Hv type_base. + destruct t, v1, v2, Hv; cbn in *; cbv [respectful]; eauto. + Qed. + + Local Hint Resolve (ex_intro _ nil) (ex_intro _ (cons _ nil)). + Local Hint Constructors expr.wf ex. + Local Hint Unfold List.In. + + 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. + clear -type_base HG1G2 Hwf. + revert dependent G1; revert dependent G2; induction t; intros; + repeat first [ progress cbn in * + | progress intros + | solve [ eauto ] + | progress subst + | progress destruct_head'_and + | progress destruct_head'_or + | apply conj + | rewrite List.in_app_iff in * + | match goal with H : _ |- _ => apply H; clear H end + | wf_unsafe_t_step + | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ]. + Qed. + + Fixpoint wf_reify (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), + UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2) + with wf_reflect G {t} + : forall e1 e2 (He : expr.wf G e1 e2) + s1 s2 (Hs : abstract_domain_R s1 s2), + @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2). + Proof using annotate_Proper bottom'_Proper. + all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper. + all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper] in *. + { destruct t as [t|s d]; + [ clear wf_reify wf_reflect + | specialize (fun G => wf_reflect G s); + specialize (fun G => wf_reify false G d) ]. + { cbn; intros [? ?] [? ?] [Hv0 Hv1] [] [] []; + cbn [fst snd] in *. + apply annotate_Proper; assumption. } + { cbn; cbv [respectful]; intros [? ?] [? ?] [He0 He1] [? ?] [? ?] [Hs0 Hs1]; + cbn [fst snd] in *. + do 2 constructor; intros v1 v2. + eapply UnderLets.wf_to_expr, UnderLets.wf_splice. + { eapply He1 with (seg:=cons _ nil); eauto using eq_refl. } + { intros; apply wf_reify; destruct_head'_ex; subst; auto. } } } + { destruct t as [t|s d]; + [ clear wf_reify wf_reflect + | specialize (fun G => wf_reflect G d); + specialize (fun G => wf_reify false G s) ]. + { cbn; auto. } + { cbn; cbv [respectful]; intros e1 e2 He s1 s2 Hs; + split; [ solve [ auto ] | ]; + intros G' seg sv1 sv2 HG1G2 Hsv; subst. + eapply UnderLets.wf_splice. + { apply wf_reify; auto; eapply wf_value_Proper_list; [ .. | solve [ eauto ] ]; + wf_safe_t. } + { intros G'' a1 a2 [seg' ?] Ha; subst G''. + constructor. + apply wf_reflect. + { constructor; auto; wf_unsafe_t_step; []. + destruct_head'_ex; subst. + intros *. + rewrite !List.in_app_iff; auto. } + { eapply Hs, state_of_value_Proper; eassumption. } } } } + 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 * + | wf_safe_t_step + | exact I + | apply wf_reify + | apply bottom_Proper + | progress destruct_head'_ex + | progress destruct_head'_or + | eapply UnderLets.wf_splice + | match goal with + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ |- and _ _ ] => apply conj + end + | eapply wf_value_Proper_list; [ | solve [ eauto ] ] + | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] + | match goal with + | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ] + end + | break_innermost_match_step ]. + + Lemma wf_interp 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 e1) (interp2 e2). + Proof using annotate_Proper bottom'_Proper interp_ident_Proper. + revert dependent G'; induction Hwf; intros; cbn [interp]; + try solve [ apply interp_ident_Proper; auto + | eauto ]; + wf_interp_t. + Qed. + + Lemma wf_eval_with_bound' 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 t e1 st1) (@eval_with_bound'2 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. } + 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. + eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper. + Qed. + + Lemma wf_eta_expand_with_bound' 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) + : expr.wf G (@eta_expand_with_bound'1 t e1 st1) (@eta_expand_with_bound'2 t e2 st2). + Proof using annotate_Proper bottom'_Proper. + eapply UnderLets.wf_to_expr, wf_reify; [ eapply wf_reflect | ]; eauto; apply bottom_Proper. + Qed. + End with_var2. + End with_type. + + Module ident. + Import defaults. + Local Notation UnderLets := (@UnderLets base.type ident). + Section with_type. + Context (abstract_domain' : base.type -> Type). + Local Notation abstract_domain := (@abstract_domain base.type abstract_domain'). + Context (annotate_ident : forall t, abstract_domain' t -> option (ident (t -> t))) + (bottom' : forall A, abstract_domain' A) + (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t) + (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A) + (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A))) + (is_annotation : forall t, ident t -> bool). + Context (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop). + Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R). + Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)} + {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)} + {update_literal_with_state_Proper : forall t, Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t)} + (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2)) + (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2). + + Local Instance abstract_interp_ident_Proper_arrow s d + : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d)) + := abstract_interp_ident_Proper (type.arrow s d). + + Section with_var2. + Context {var1 var2 : type -> Type}. + + Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation). + Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation). + Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation). + Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation). + Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation). + Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation). + Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom'). + Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom'). + + Lemma wf_update_annotation G {t} st1 st2 (Hst : abstract_domain'_R t st1 st2) e1 e2 (He : expr.wf G e1 e2) + : expr.wf G (@update_annotation1 t st1 e1) (@update_annotation2 t st2 e2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper. + cbv [ident.update_annotation]; + repeat first [ progress subst + | progress expr.invert_subst + | progress cbn [fst snd projT1 projT2 eq_rect] in * + | progress cbn [invert_AppIdent Option.bind invert_App invert_Ident] in * + | progress destruct_head'_sig + | progress destruct_head'_sigT + | progress destruct_head'_and + | progress destruct_head'_prod + | progress destruct_head' False + | progress inversion_option + | progress expr.inversion_wf_constr + | progress expr.inversion_wf_one_constr + | break_innermost_match_hyps_step + | expr.invert_match_step + | progress expr.inversion_expr + | progress rewrite_type_transport_correct + | progress type_beq_to_eq + | progress type.inversion_type + | progress base.type.inversion_type + | match goal with + | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H; clear dependent x + end + | progress wf_safe_t + | break_innermost_match_step ]. + Qed. + + Lemma wf_annotate_with_ident + is_let_bound t G + 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 (@annotate_with_ident1 is_let_bound t v1 e1) (@annotate_with_ident2 is_let_bound t v2 e2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper. + cbv [ident.annotate_with_ident]; break_innermost_match; repeat constructor; apply wf_update_annotation; assumption. + Qed. + + Lemma wf_annotate_base + is_let_bound (t : base.type.base) G + 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 (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper update_literal_with_state_Proper. + cbv [ident.annotate_base]; + repeat first [ apply wf_annotate_with_ident + | break_innermost_match_step + | progress subst + | progress cbv [type_base ident.smart_Literal] in * + | progress cbn [invert_Literal ident.invert_Literal] in * + | discriminate + | progress destruct_head' False + | progress expr.invert_subst + | progress expr.inversion_wf + | wf_safe_t_step + | break_innermost_match_hyps_step + | match goal with + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ H : abstract_domain'_R _ _ _ |- _ ] => rewrite !H + end + | progress expr.invert_match_step + | progress expr.inversion_expr ]. + Qed. + + Lemma wf_annotate + is_let_bound t G + 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). + Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + revert dependent G; induction t; intros; + cbn [ident.annotate]; try apply wf_annotate_base; trivial. + all: repeat first [ lazymatch goal with + | [ 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 |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H + | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list + | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ] + => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length + | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence + | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain'_R _ ?v1 ?v2 |- _ ] + => let Hl := fresh in + let Hl' := fresh in + pose proof (extract_list_state_length _ v1 v2 Hv) as Hl; + pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl'; + rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H' + | [ H : ?x = ?x |- _ ] => clear H + | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' + end + | apply wf_annotate_with_ident + | apply DefaultValue.expr.base.wf_default + | apply DefaultValue.expr.wf_default + | progress expr.invert_subst + | progress cbn [ident.annotate ident.smart_Literal invert_Literal ident.invert_Literal invert_pair invert_AppIdent2 invert_App2 fst snd projT2 projT1 eq_rect Option.bind] in * + | progress destruct_head' False + | progress inversion_option + | progress destruct_head'_ex + | discriminate + | wf_safe_t_step + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | progress type_beq_to_eq + | progress type.inversion_type + | progress base.type.inversion_type + | match goal with + | [ |- expr.wf _ (update_annotation1 _ _) (update_annotation2 _ _) ] => apply wf_update_annotation + | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H + | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice + | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H + | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H + | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine + | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ] + => specialize (H _ _ eq_refl eq_refl) + | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n = Some ?a1, H'' : List.nth_error ?l2 ?n = Some ?a2 + |- ?R ?a1 ?a2 ] + => apply H + | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n') + end + | break_innermost_match_step + | break_innermost_match_hyps_step + | progress expr.invert_match + | progress expr.inversion_wf_one_constr + | match goal with + | [ H : context[UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _)] + |- UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _) ] => eapply H + end + | apply abstract_interp_ident_Proper_arrow + | progress rewrite_type_transport_correct + | apply conj + | congruence + | solve [ wf_t ] ]. + Qed. + + 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). + + Lemma wf_interp_ident_nth_default G T + : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)). + Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain]. + split. + { exact (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl). } + { intros; subst. + destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *. + repeat first [ progress subst + | progress cbn [invert_Literal ident.invert_Literal] in * + | lazymatch goal with + | [ 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 |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H + | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list + | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ] + => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length + | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence + | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ] + => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence + | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain_R ?v1 ?v2 |- _ ] + => let Hl := fresh in + let Hl' := fresh in + pose proof (extract_list_state_length _ v1 v2 Hv) as Hl; + pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl'; + rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H' + | [ H : ?x = ?x |- _ ] => clear H + | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' + end + | match goal with + | [ |- UnderLets.wf ?Q ?G (UnderLets.splice ?x1 ?e1) (UnderLets.splice ?x2 ?e2) ] + => simple refine (@UnderLets.wf_splice _ _ _ _ _ _ _ _ _ Q G x1 x2 _ e1 e2 _); + [ let G := fresh "G" in + intro G; + lazymatch goal with + | [ |- (abstract_domain ?t * _) -> _ -> _ ] + => refine (@wf_value G t) + | [ |- expr _ -> _ -> _ ] + => refine (expr.wf G) + end + | | ] + | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ] + => constructor + | [ 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) + | [ 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 + | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H + | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H + | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H + | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine + | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ] + => specialize (H _ _ eq_refl eq_refl) + | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n' = Some ?a1, H'' : List.nth_error ?l2 ?n' = Some ?a2 + |- _ ] + => unique pose proof (H a1 a2 ltac:(apply nth_error_In with (n:=n'); rewrite nth_error_combine, H', H''; reflexivity)) + | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n') + | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H) + | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H + end + | progress inversion_option + | progress intros + | progress cbn [fst snd value] in * + | progress destruct_head'_prod + | progress destruct_head'_ex + | progress destruct_head'_and + | progress destruct_head' False + | progress specialize_by_assumption + | apply conj + | progress expr.invert_subst + | progress expr.inversion_wf_constr + | progress expr.inversion_expr + | 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 wf_update_annotation; wf_t + | wf_t + | match goal with + | [ H : context[UnderLets.wf _ _ _ _] |- UnderLets.wf _ _ _ _ ] => eapply H; solve [ repeat esplit; eauto ] + end + | eauto using List.nth_error_In + | eapply expr.wf_Proper_list; [ | eassumption ]; wf_safe_t; eauto 10 ] + | break_innermost_match_step + | match goal with + | [ H : context[List.In] |- expr.wf _ ?x ?y ] + => specialize (H x y); rewrite !List.nth_default_eq, <- List.combine_nth, <- !List.nth_default_eq in H; cbv [List.nth_default] in H |- * + | [ H : List.In _ _ -> ?P |- ?P ] => apply H + end + | break_innermost_match_hyps_step + | congruence + | rewrite List.combine_length in * + | rewrite NPeano.Nat.min_r in * by lia + | rewrite NPeano.Nat.min_l in * by lia + | progress expr.inversion_wf_one_constr + | progress expr.invert_match ]. } + Qed. + + Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t) + : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###idc)%expr (abstract_interp_ident _ idc))). + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + constructor; eapply wf_reflect; + solve [ apply bottom'_Proper + | apply wf_annotate + | repeat constructor + | apply abstract_interp_ident_Proper; reflexivity ]. + Qed. + + Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2) + : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + 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 ]. + Qed. + + Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Lemma wf_eval_with_bound {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 t e1 st1) (@eval_with_bound2 t e2 st2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + eapply wf_eval_with_bound'; + solve [ eassumption + | eapply wf_annotate + | eapply wf_interp_ident ]. + Qed. + + Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + 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). + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + eapply wf_eval'; + solve [ eassumption + | eapply wf_annotate + | eapply wf_interp_ident ]. + Qed. + + Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation). + Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2). + Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper. + eapply wf_eta_expand_with_bound'; + solve [ eassumption + | eapply wf_annotate + | eapply wf_interp_ident ]. + Qed. + End with_var2. + End with_type. + End ident. + + Section specialized. + Import defaults. + Local Notation abstract_domain' := ZRange.type.base.option.interp (only parsing). + 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)). + + Global Instance annotate_ident_Proper {t} : Proper (abstract_domain'_R t ==> eq) (annotate_ident t). + Proof. + intros st st' ?; subst st'. + cbv [annotate_ident]; break_innermost_match; reflexivity. + Qed. + + Global Instance bottom'_Proper {t} : Proper (abstract_domain'_R t) (bottom' t). + Proof. reflexivity. Qed. + + Global Instance abstract_interp_ident_Proper {t} + : Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t). + Proof. + cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc; + repeat first [ reflexivity + | progress subst + | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Option.bind] in * + | progress cbv [Option.bind] + | intro + | progress destruct_head'_prod + | progress destruct_head'_bool + | progress destruct_head' option + | solve [ eauto ] + | apply NatUtil.nat_rect_Proper_nondep + | apply ListUtil.list_rect_Proper + | apply ListUtil.list_case_Proper + | apply ListUtil.pointwise_map + | apply ListUtil.fold_right_Proper + | apply ListUtil.update_nth_Proper + | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature) + | cbn; apply (f_equal (@Some _)) + | match goal with + | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity)) + end ]. + Qed. + + Global Instance update_literal_with_state_Proper {t} + : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t). + Proof. repeat intro; congruence. Qed. + + Global Instance extract_list_state_Proper {t} + : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t))) + (extract_list_state t). + Proof. + intros st st' ?; subst st'; cbv [option_eq extract_list_state]; break_innermost_match; reflexivity. + Qed. + + Lemma extract_list_state_length + : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2). + Proof. + intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity. + Qed. + Lemma extract_list_state_rel + : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2. + Proof. + intros; cbv [extract_list_state] in *; subst; inversion_option; subst. + rewrite combine_same, List.in_map_iff in *. + destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity. + Qed. + + 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 {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' (@eval var1 t e1) (@eval var2 t e2). + Proof. + eapply ident.wf_eval; + solve [ eassumption + | exact _ + | apply extract_list_state_length + | apply extract_list_state_rel ]. + Qed. + + Lemma wf_eval_with_bound {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_bound var1 t e1 st1) (@eval_with_bound var2 t e2 st2). + Proof. + eapply ident.wf_eval_with_bound; + solve [ eassumption + | exact _ + | apply extract_list_state_length + | apply extract_list_state_rel ]. + Qed. + + + Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2) + : expr.wf G (@eta_expand_with_bound var1 t e1 st1) (@eta_expand_with_bound var2 t e2 st2). + Proof. + eapply ident.wf_eta_expand_with_bound; + solve [ eassumption + | exact _ + | apply extract_list_state_length + | apply extract_list_state_rel ]. + Qed. + End with_var2. + + Lemma Wf_Eval {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e). + Proof. + intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + Qed. + + Lemma Wf_EvalWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) + : Wf (EvalWithBound e bound). + Proof. + intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + Qed. + + Lemma Wf_EtaExpandWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) + : Wf (EtaExpandWithBound e bound). + Proof. + intros ??; eapply wf_eta_expand_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto. + Qed. + + Local Instance Proper_strip_ranges {t} + : Proper (@abstract_domain_R t ==> @abstract_domain_R t) (@ZRange.type.option.strip_ranges t). + Proof. + cbv [Proper abstract_domain_R respectful]. + induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; intros; subst; cbv [respectful] in *; + eauto. + Qed. + + Lemma Wf_EtaExpandWithListInfoFromBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound) + : Wf (EtaExpandWithListInfoFromBound e bound). + Proof. + eapply Wf_EtaExpandWithBound; [ assumption | ]. + clear dependent e. + cbv [Proper] in *; induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; eauto. + split; auto; apply Proper_strip_ranges; auto. + Qed. + End specialized. + End partial. + Import defaults. + + Module RelaxZRange. + Module expr. + Section relax. + Context (relax_zrange : zrange -> option zrange) + (Hrelax : forall r r' z, is_tighter_than_bool z r = true + -> relax_zrange r = Some r' + -> is_tighter_than_bool z r' = true). + Section with_var2. + Context {var1 var2 : type -> Type}. + + Lemma wf_relax G {t} (e1 : @expr var1 t) (e2 : @expr var2 t) + (Hwf : expr.wf G e1 e2) + : expr.wf G (@RelaxZRange.expr.relax relax_zrange var1 t e1) (@RelaxZRange.expr.relax relax_zrange var2 t e2). + Proof using Type. + clear -Hwf. + induction Hwf; wf_safe_t. + cbn [RelaxZRange.expr.relax]; cbv [option_map] in *. + break_innermost_match; + repeat first [ progress wf_safe_t + | progress expr.invert_subst + | progress expr.inversion_wf_constr + | progress destruct_head' False + | progress inversion_option + | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in * + | match goal with + | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ] + => rewrite H' in H + | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ] + => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match + | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' + end + | progress expr.inversion_wf_one_constr ]. + Qed. + End with_var2. + + Lemma Wf_Relax {t} (e : Expr t) (Hwf : Wf e) : Wf (@RelaxZRange.expr.Relax relax_zrange t e). + Proof. intros ??; eapply wf_relax, Hwf. Qed. + End relax. + End expr. + End RelaxZRange. + Hint Resolve RelaxZRange.expr.Wf_Relax : wf. + + Lemma Wf_PartialEvaluateWithListInfoFromBounds + {t} (E : Expr t) + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + (Hwf : Wf E) + {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} + : Wf (PartialEvaluateWithListInfoFromBounds E b_in). + Proof. apply Wf_EtaExpandWithListInfoFromBound; assumption. Qed. + Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf. + + Lemma Wf_PartialEvaluateWithBounds + {t} (E : Expr t) + (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) + (Hwf : Wf E) + {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} + : Wf (PartialEvaluateWithBounds E b_in). + Proof. eapply partial.Wf_EvalWithBound; assumption. Qed. + Hint Resolve Wf_PartialEvaluateWithBounds : wf. + + Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf. +End Compilers. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 437855405..3b8f81ac6 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -52,6 +52,7 @@ Require Crypto.Experiments.NewPipeline.LanguageWf. Require Crypto.Experiments.NewPipeline.UnderLetsProofs. Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs. Require Crypto.Experiments.NewPipeline.RewriterProofs. +Require Crypto.Experiments.NewPipeline.AbstractInterpretationWf. Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. @@ -499,6 +500,7 @@ Import Crypto.Experiments.NewPipeline.UnderLetsProofs Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs Crypto.Experiments.NewPipeline.RewriterProofs + Crypto.Experiments.NewPipeline.AbstractInterpretationWf Crypto.Experiments.NewPipeline.AbstractInterpretationProofs Crypto.Experiments.NewPipeline.Language Crypto.Experiments.NewPipeline.UnderLets @@ -512,6 +514,7 @@ Import UnderLetsProofs.Compilers MiscCompilerPassesProofs.Compilers RewriterProofs.Compilers + AbstractInterpretationWf.Compilers AbstractInterpretationProofs.Compilers Language.Compilers UnderLets.Compilers |