diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/common/NonEmpty.v | 70 | ||||
-rw-r--r-- | src/hls/AbstrSemIdent.v | 665 | ||||
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 152 | ||||
-rw-r--r-- | src/hls/GiblePargenproofEvaluable.v | 128 | ||||
-rw-r--r-- | src/hls/GiblePargenproofForward.v | 522 |
5 files changed, 937 insertions, 600 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index f15bb82..3aff11d 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -24,6 +24,8 @@ Require Export Coq.Classes.SetoidClass. Require Export Coq.Classes.SetoidDec. Require Import Coq.Logic.Decidable. +Require Import Vericertlib. + Inductive non_empty (A: Type) := | singleton : A -> non_empty A | cons : A -> non_empty A -> non_empty A @@ -214,7 +216,7 @@ Inductive norepet {A : Type} : non_empty A -> Prop := | list_norepet_cons hd tl : ~ In hd tl -> norepet tl -> norepet (hd ::| tl). -Lemma NEin_NEapp5 : +Lemma in_NEapp5 : forall A (a: A) x y, In a (app x y) -> In a x \/ In a y. @@ -224,3 +226,69 @@ Proof. - inv H. inv H1. left. constructor; tauto. apply IHx in H. inv H; intuition (constructor; auto). Qed. + +Lemma app_NEmap : + forall A B (f: A -> B) a b, + map f (app a b) = app (map f a) (map f b). +Proof. induction a; auto; intros; cbn in *; now rewrite IHa. Qed. + +Lemma of_list_some : + forall A a a' (e: A), + of_list a = Some a' -> + of_list (e :: a) = Some (cons e a'). +Proof. + induction a; [crush|]. + intros. + cbn in H. destruct a0. inv H. auto. + destruct_match; [|discriminate]. + inv H. specialize (IHa n a ltac:(trivial)). + cbn. destruct_match. unfold of_list in IHa. + fold (@of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. auto. + unfold of_list in IHa. fold (@of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. +Qed. + +Lemma of_list_contra : + forall A b (a: A), + ~ of_list (a :: b) = None. +Proof. + induction b; try solve [crush]. + intros. + specialize (IHb a). + enough (X: exists x, of_list (a :: b) = Some x). + inversion_clear X as [x X']. + erewrite of_list_some; eauto; discriminate. + destruct (of_list (a :: b)) eqn:?; [eauto|contradiction]. +Qed. + +Lemma of_list_exists : + forall A b (a: A), + exists x, of_list (a :: b) = Some x. +Proof. + intros. pose proof (of_list_contra _ b a). + destruct (of_list (a :: b)); try contradiction. + eauto. +Qed. + +Lemma of_list_exists2 : + forall A b (a c: A), + exists x, + of_list (c :: a :: b) = Some (cons c x) + /\ of_list (a :: b) = Some x. +Proof. + intros. pose proof (of_list_exists _ b a). + inversion_clear H as [x B]. + econstructor; split; eauto. + eapply of_list_some; eauto. +Qed. + +Lemma of_list_to_list : + forall A (x: list A) y, + of_list x = Some y -> + to_list y = x. +Proof. + induction x; [crush|]. + intros. destruct x; [crush|]. + pose proof (of_list_exists2 _ x a0 a). + inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H. + cbn. f_equal. eauto. +Qed. diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v new file mode 100644 index 0000000..0cc8e9d --- /dev/null +++ b/src/hls/AbstrSemIdent.v @@ -0,0 +1,665 @@ +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Linking. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePargenproofEquiv. +Require Import vericert.hls.GiblePargen. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.Abstr. +Require Import vericert.common.Monad. + +Module Import OptionExtra := MonadExtra(Option). + +#[local] Open Scope positive. +#[local] Open Scope forest. +#[local] Open Scope pred_op. + +#[local] Opaque simplify. +#[local] Opaque deep_simplify. + +#[local] Ltac destr := destruct_match; try discriminate; []. + +Inductive sem_ident {B A: Type} (c: @Abstr.ctx B) (a: A): A -> Prop := +| sem_ident_intro : sem_ident c a a. + +Section PROOF. + +Context (A B G: Type). +Context (ctx: @Abstr.ctx G). +Context (a_sem: @Abstr.ctx G -> A -> B -> Prop). + +Lemma eval_predf_negate : + forall ps p, + eval_predf ps (negate p) = negb (eval_predf ps p). +Proof. + unfold eval_predf; intros. rewrite negate_correct. auto. +Qed. + +Lemma is_truthy_negate : + forall ps p pred, + truthy ps p -> + falsy ps (combine_pred (Some (negate (Option.default T p))) pred). +Proof. + inversion 1; subst; simplify. + - destruct pred; constructor; auto. + - destruct pred; constructor. + rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto. + rewrite eval_predf_negate. rewrite H0. auto. +Qed. + +Lemma sem_pred_expr_NEapp : + forall f_p a b v, + sem_pred_expr f_p a_sem ctx a v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - inv H. constructor; auto. + - inv H. constructor; eauto. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_app_predicated_false : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx y v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = false -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v. +Proof. +Admitted. + +Lemma sem_pred_expr_prune_predicated : + forall f_p y x v, + sem_pred_expr f_p a_sem ctx x v -> + prune_predicated x = Some y -> + sem_pred_expr f_p a_sem ctx y v. +Proof. + intros * SEM PRUNE. unfold prune_predicated in *. +Admitted. + +Lemma sem_pred_expr_prune_predicated2 : + forall f_p y x v, + sem_pred_expr f_p a_sem ctx y v -> + prune_predicated x = Some y -> + sem_pred_expr f_p a_sem ctx x v. +Proof. + intros * SEM PRUNE. unfold prune_predicated in *. + Admitted. + +Lemma sem_pred_expr_app_predicated_false2 : + forall f_p y x v p ps, + sem_pred_expr f_p sem ctx (app_predicated p y x) v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = false -> + sem_pred_expr f_p sem ctx y v. +Admitted. + +Lemma sem_pred_expr_pred_ret : + forall (i: A) ps, + sem_pred_expr ps sem_ident ctx (pred_ret i) i. +Proof. intros; constructor; constructor. Qed. + +Lemma sem_pred_expr_ident_det : + forall A ps x (v v2: A), + sem_pred_expr ps sem_ident ctx x v -> + sem_pred_expr ps sem_ident ctx x v2 -> + v = v2. +Proof. + intros. + exploit (@sem_pred_expr_det G G). + apply similar_refl. + 2: { instantiate (4 := (fun x => @sem_ident x A0)). + cbn. eauto. } + intros. inv H1. inv H2. auto. + apply H. auto. +Qed. + +Lemma sem_pred_expr_NEapp2 : + forall f_p a b v ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + (forall x, NE.In x a -> eval_predf ps (fst x) = false) -> + sem_pred_expr f_p a_sem ctx b v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H0 _ IN). destruct a. + eapply sem_pred_expr_cons_false; eauto. cbn [fst] in *. + eapply sem_pexpr_eval; eauto. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H0 in H2. + destruct a. cbn [fst] in *. + eapply sem_pred_expr_cons_false. + eapply sem_pexpr_eval; eauto. eapply IHa; eauto. + intros. eapply H0. constructor; tauto. +Qed. + +Lemma sem_pred_expr_NEapp3 : + forall f_p ctx a b v, + (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> + sem_pred_expr f_p a_sem ctx b v -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H _ IN). destruct a. + eapply sem_pred_expr_cons_false; eauto. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H in H1. + destruct a. cbn [fst] in *. + eapply sem_pred_expr_cons_false; auto. + eapply IHa; eauto. + intros. eapply H. constructor; tauto. +Qed. + +Lemma sem_pred_expr_NEapp4 : + forall f_p ctx a b v, + (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v -> + sem_pred_expr f_p a_sem ctx b v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H _ IN). inv H0; auto. + eapply sem_pexpr_det in H; eauto; now try apply similar_refl. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H in H1. inv H0. + eapply sem_pexpr_det in H1; eauto; now try apply similar_refl. + eapply IHa; eauto. intros. eapply H. apply NE.In_cons; auto. +Qed. + +Lemma sem_pred_expr_NEapp5 : + forall f_p ctx a b v, + (exists x, NE.In x a /\ sem_pexpr ctx (from_pred_op f_p (fst x)) true) -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v -> + sem_pred_expr f_p a_sem ctx a v. +Proof. + induction a; crush. + - inv H. inv H0. constructor; eauto. + eapply sem_pexpr_det in H2; eauto; now try apply similar_refl. + - inv H. inv H3. inv H0. constructor; auto. + eapply sem_pexpr_det in H2; eauto; now try apply similar_refl. inv H0. + constructor; auto. apply sem_pred_expr_cons_false; auto. eauto. +Qed. + +Lemma In_pexpr_eval : + forall A f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + forall (a: predicated A), + (exists x, NE.In x a /\ sem_pexpr ctx (from_pred_op f_p (fst x)) true) + \/ (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false). +Proof. + induction a; cbn in *. + - pose proof (sem_pexpr_evaluable _ _ _ _ H (fst a)); simplify. + destruct x. + + left. exists a. split; auto. constructor. + + right; intros. inv H0; auto. + - inv IHa; simplify. + + left. exists x. split; auto. apply NE.In_cons; auto. + + pose proof (sem_pexpr_evaluable _ _ _ _ H (fst a)); simplify. + destruct x. + * left. exists a; split; auto. constructor; auto. + * right; intros. inv H1. inv H4; auto. +Qed. + +Lemma sem_pred_expr_map_not : + forall A p ps y x0, + eval_predf ps p = false -> + NE.In x0 (NE.map (fun x => (p ∧ fst x, snd x)) y) -> + eval_predf ps (@fst _ A x0) = false. +Proof. + induction y; crush. + - inv H0. simplify. rewrite eval_predf_Pand. rewrite H. auto. + - inv H0. inv H2. cbn -[eval_predf]. rewrite eval_predf_Pand. + rewrite H. auto. eauto. +Qed. + +Lemma sem_pred_expr_map_Pand : + forall f_p ps x v p, + (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx x v -> + sem_pred_expr f_p a_sem ctx + (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v. +Proof. + induction x; crush. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + eapply sem_pred_expr_cons_false. cbn. + replace false with (true && false) by auto. apply sem_pexpr_Pand; auto. + eapply sem_pexpr_eval; eauto. eauto. +Qed. + +Lemma sem_pred_expr_app_predicated : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx x v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v. +Proof. + intros * SEM PS EVAL. unfold app_predicated. + eapply sem_pred_expr_NEapp2; eauto. + intros. eapply sem_pred_expr_map_not; eauto. + rewrite eval_predf_negate. rewrite EVAL. auto. + eapply sem_pred_expr_map_Pand; eauto. +Qed. + +Lemma sem_pred_expr_app_predicated2 : + forall f_p y x v p ps, + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v -> + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx x v. +Proof. Admitted. + +Lemma sem_pred_expr_ident : + forall ps l l_, + sem_pred_expr ps sem_ident ctx l l_ -> + forall (v: B), + a_sem ctx l_ v -> + sem_pred_expr ps a_sem ctx l v. +Proof. + induction 1. + - intros. constructor; auto. inv H0. auto. + - intros. apply sem_pred_expr_cons_false; auto. + - intros. inv H0. constructor; auto. +Qed. + +Lemma sem_pred_expr_ident2 : + forall ps l v, + sem_pred_expr ps a_sem ctx l v -> + exists l_, sem_pred_expr ps sem_ident ctx l l_ /\ a_sem ctx l_ v. +Proof. + induction 1. + - exists e; split; auto. constructor; auto. constructor. + - inversion_clear IHsem_pred_expr as [x IH]. + inversion_clear IH as [SEM EVALS]. + exists x; split; auto. apply sem_pred_expr_cons_false; auto. + - exists e; split; auto; constructor; auto; constructor. +Qed. + +Fixpoint of_elist (e: expression_list): list expression := + match e with + | Econs a b => a :: of_elist b + | Enil => nil + end. + +Fixpoint to_elist (e: list expression): expression_list := + match e with + | a :: b => Econs a (to_elist b) + | nil => Enil + end. + +Lemma sem_val_list_elist : + forall l j, + sem_val_list ctx (to_elist l) j -> + Forall2 (sem_value ctx) l j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist2 : + forall l j, + Forall2 (sem_value ctx) l j -> + sem_val_list ctx (to_elist l) j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist3 : + forall l j, + sem_val_list ctx l j -> + Forall2 (sem_value ctx) (of_elist l) j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_val_list_elist4 : + forall l j, + Forall2 (sem_value ctx) (of_elist l) j -> + sem_val_list ctx l j. +Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. + +Lemma sem_pred_expr_predicated_map : + forall pr (f: A -> B) pred pred', + sem_pred_expr pr sem_ident ctx pred pred' -> + sem_pred_expr pr sem_ident ctx (predicated_map f pred) (f pred'). +Proof. + induction pred; unfold predicated_map; intros. + - inv H. inv H3. constructor; eauto. constructor. + - inv H. inv H5. constructor; eauto. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_predicated_map2 : + forall pr (f: A -> B) pred x, + sem_pred_expr pr sem_ident ctx (predicated_map f pred) x -> + exists pred', sem_pred_expr pr sem_ident ctx pred pred' /\ x = f pred'. +Proof. + induction pred; unfold predicated_map; intros. + - cbn in *. inv H. inv H5. destruct a. exists a. + split; auto. constructor; auto. constructor. + - cbn in *. inv H. destruct a. inv H6. cbn [fst snd] in *. + exists a; repeat constructor; auto. + exploit IHpred; eauto; simplify. + exists x0; split; auto. + destruct a. apply sem_pred_expr_cons_false; auto. +Qed. + +End PROOF. + +Section PROOF. + +Context (G: Type). +Context (ctx: @Abstr.ctx G). + +Lemma sem_pred_expr_predicated_prod : + forall A B pr (a: predicated A) (b: predicated B) a' b', + sem_pred_expr pr sem_ident ctx a a' -> + sem_pred_expr pr sem_ident ctx b b' -> + sem_pred_expr pr sem_ident ctx (predicated_prod a b) (a', b'). +Proof. + induction a; intros. + - inv H. inv H4. unfold predicated_prod. + generalize dependent b. induction b; intros. + + cbn. destruct_match. inv Heqp. inv H0. inv H6. + constructor. simplify. replace true with (true && true) by auto. + eapply sem_pexpr_Pand; eauto. constructor. + + inv H0. inv H6. cbn. constructor; cbn. + replace true with (true && true) by auto. + constructor; auto. constructor. + eapply sem_pred_expr_cons_false; eauto. cbn. + replace false with (true && false) by auto. + apply sem_pexpr_Pand; auto. + - unfold predicated_prod. simplify. + rewrite NE.app_NEmap. + inv H. eapply sem_pred_expr_NEapp. + { induction b; crush. + destruct a. inv H0. constructor. + replace true with (true && true) by auto. + eapply sem_pexpr_Pand; auto. inv H6. inv H7. + constructor. + + destruct a. inv H0. constructor. + replace true with (true && true) by auto. + constructor; auto. inv H8. inv H6. constructor. + + specialize (IHb H8). eapply sem_pred_expr_cons_false; auto. + replace false with (true && false) by auto. + apply sem_pexpr_Pand; auto. + } + { exploit IHa. eauto. eauto. intros. + unfold predicated_prod in *. + eapply sem_pred_expr_NEapp3; eauto; []. + clear H. clear H0. + induction b. + { intros. inv H. destruct a. simpl. + constructor; tauto. } + { intros. inv H. inv H1. destruct a. simpl. + constructor; tauto. eauto. } } +Qed. + +Lemma sem_pred_expr_predicated_prod2 : + forall A B f ps (a: predicated A) (b: predicated B) x, + (forall x, sem_pexpr ctx (get_forest_p' x f) (ps !! x)) -> + sem_pred_expr f sem_ident ctx (predicated_prod a b) x -> + sem_pred_expr f sem_ident ctx a (fst x) + /\ sem_pred_expr f sem_ident ctx b (snd x). +Proof. + induction a; intros. + - generalize dependent x. generalize dependent b. induction b; intros. + + cbn in *; repeat destr; destruct a, a0. inv Heqp. inv Heqp0. + inv H0. inv H6; split. + * constructor. inv H4. tauto. constructor. + * cbn in *. inv H4. constructor. tauto. constructor. + + destruct x; cbn in *. repeat destr. inv Heqp0. inv H0. + * inv H6. inv H7. repeat (constructor; auto). + * exploit IHb; eauto; intros. inv H0. cbn in *. inv H6. + inv H3. inv H1. eapply sem_pexpr_det in H0; try eassumption. discriminate. + apply similar_refl. split; auto. + apply sem_pred_expr_cons_false; auto. + - destruct x in *; cbn in *. + rewrite NE.app_NEmap in H0. + generalize dependent b; induction b; intros. + + cbn in *; repeat destr. inv Heqp0. inv H0. + * inv H6. inv H7. solve [repeat constructor; auto]. + * inv H6. inv H1. + -- exploit IHa; eauto; intros. inv H1. split; auto. + apply sem_pred_expr_cons_false; eauto. + -- exploit IHa; eauto; intros. inv H1. inv H3. + eapply sem_pexpr_det in H0; try eassumption. discriminate. + apply similar_refl. + + Admitted. + +Lemma sem_pred_expr_seq_app : + forall A B (f: predicated (A -> B)) ps l f_ l_, + sem_pred_expr ps sem_ident ctx l l_ -> + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (seq_app f l) (f_ l_). +Proof. + unfold seq_app; intros. + remember (fun x : (A -> B) * A => fst x (snd x)) as app. + replace (f_ l_) with (app (f_, l_)) by (rewrite Heqapp; auto). + eapply sem_pred_expr_predicated_map. eapply sem_pred_expr_predicated_prod; auto. +Qed. + +Lemma sem_pred_expr_seq_app2 : + forall A B (f: predicated (A -> B)) ps pr l x_, + (forall x, sem_pexpr ctx (get_forest_p' x ps) (pr !! x)) -> + sem_pred_expr ps sem_ident ctx (seq_app f l) x_ -> + exists l_ f_, + x_ = f_ l_ + /\ sem_pred_expr ps sem_ident ctx l l_ + /\ sem_pred_expr ps sem_ident ctx f f_. +Proof. + unfold seq_app; intros. + remember (fun x : (A -> B) * A => fst x (snd x)) as app. + exploit sem_pred_expr_predicated_map2; eauto; simplify. + exploit sem_pred_expr_predicated_prod2; eauto; simplify. + eauto. +Qed. + +Lemma sem_pred_expr_map : + forall A B ps (f: A -> B) y v, + sem_pred_expr ps sem_ident ctx y v -> + sem_pred_expr ps sem_ident ctx (NE.map (fun x => (fst x, f (snd x))) y) (f v). +Proof. + induction y; crush. inv H. constructor; crush. inv H3. constructor. + inv H. inv H5. constructor; eauto. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_flap : + forall A B C (f: predicated (A -> B -> C)) ps l f_, + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (flap f l) (f_ l). +Proof. + induction f. unfold flap2; intros. inv H. inv H3. + constructor; eauto. constructor. + intros. inv H. cbn. + constructor; eauto. inv H5. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_flap2 : + forall A B C (f: predicated (A -> B -> C)) ps l1 l2 f_, + sem_pred_expr ps sem_ident ctx f f_ -> + sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) (f_ l1 l2). +Proof. + induction f. unfold flap2; intros. inv H. inv H3. + constructor; eauto. constructor. + intros. inv H. cbn. + constructor; eauto. inv H5. constructor. + eapply sem_pred_expr_cons_false; eauto. +Qed. + +Lemma sem_pred_expr_seq_app_val : + forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) + (f: predicated (A -> B)) + ps l v f_ l_, + sem_pred_expr ps sem_ident ctx l l_ -> + sem_pred_expr ps sem_ident ctx f f_ -> + s ctx (f_ l_) v -> + sem_pred_expr ps s ctx (seq_app f l) v. +Proof. + intros. eapply sem_pred_expr_ident; [|eassumption]. + eapply sem_pred_expr_seq_app; eauto. +Qed. + +Lemma sem_pred_expr_seq_app_val2 : + forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) + (f: predicated (A -> B)) ps pr l v, + (forall x, sem_pexpr ctx (get_forest_p' x ps) (pr !! x)) -> + sem_pred_expr ps s ctx (seq_app f l) v -> + exists f_ l_, + sem_pred_expr ps sem_ident ctx l l_ + /\ sem_pred_expr ps sem_ident ctx f f_ + /\ s ctx (f_ l_) v. +Proof. + intros; exploit sem_pred_expr_ident2; eauto; simplify. + exploit sem_pred_expr_seq_app2; eauto; simplify. + eauto. +Qed. + +Fixpoint Eapp a b := + match a with + | Enil => b + | Econs ax axs => Econs ax (Eapp axs b) + end. + +Lemma Eapp_right_nil : + forall a, Eapp a Enil = a. +Proof. induction a; cbn; try rewrite IHa; auto. Qed. + +Lemma Eapp_left_nil : + forall a, Eapp Enil a = a. +Proof. auto. Qed. + +Lemma sem_pred_expr_cons_pred_expr : + forall pr s s' a e, + sem_pred_expr pr sem_ident ctx s s' -> + sem_pred_expr pr sem_ident ctx a e -> + sem_pred_expr pr sem_ident ctx (cons_pred_expr a s) (Econs e s'). +Proof. + intros. unfold cons_pred_expr. + replace (Econs e s') with ((uncurry Econs) (e, s')) by auto. + eapply sem_pred_expr_predicated_map. + eapply sem_pred_expr_predicated_prod; eauto. +Qed. + +Lemma sem_pred_expr_fold_right : + forall pr s a a' s', + sem_pred_expr pr sem_ident ctx s s' -> + Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a') -> + sem_pred_expr pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s'). +Proof. + induction a; crush. inv H0. inv H5. destruct a'; crush. destruct a'; crush. + inv H3. eapply sem_pred_expr_cons_pred_expr; eauto. + inv H0. destruct a'; crush. inv H3. + eapply sem_pred_expr_cons_pred_expr; eauto. +Qed. + +Lemma sem_pred_expr_fold_right2 : + forall A pr ctx s a a' s', + sem_pred_expr pr sem_ident ctx s s' -> + @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') -> + Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a'). +Proof. + induction a. Admitted. + +Lemma sem_pred_expr_merge : + forall G (ctx: @Abstr.ctx G) ps l args, + Forall2 (sem_pred_expr ps sem_ident ctx) args l -> + sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). +Proof. + induction l; intros. + - inv H. cbn; repeat constructor. + - inv H. cbn. unfold merge. Admitted. + +Lemma sem_pred_expr_merge2 : + forall pr l l', + sem_pred_expr pr sem_ident ctx (merge l) l' -> + Forall2 (sem_pred_expr pr sem_ident ctx) l (of_elist l'). +Proof. + induction l; crush. + - unfold merge in *; cbn in *. + inv H. inv H5. constructor. + - unfold merge in H. + pose proof (NE.of_list_exists _ l a) as Y. + inversion_clear Y as [x HNE]. rewrite HNE in H. + erewrite <- (NE.of_list_to_list _ (a :: l)) by eassumption. + apply sem_pred_expr_fold_right2 with (s := (NE.singleton (T, Enil))) (s' := Enil). + repeat constructor. + rewrite Eapp_right_nil. auto. +Qed. + +Lemma sem_merge_list : (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) + forall f rs ps m args, + sem ctx f ((mk_instr_state rs ps m), None) -> + sem_pred_expr (forest_preds f) sem_val_list ctx + (merge (list_translation args f)) (rs ## args). +Proof. + induction args; crush. cbn. constructor; constructor. + unfold merge. specialize (IHargs H). + eapply sem_pred_expr_ident2 in IHargs. + inversion_clear IHargs as [l_ [HSEM HVAL]]. + destruct_match; [|exfalso; eapply NE.of_list_contra; eauto]. + destruct args; cbn -[NE.of_list] in *. + - unfold merge in *. simplify. + inv H. inv H6. specialize (H a). + eapply sem_pred_expr_ident2 in H. + inversion_clear H as [l_2 [HSEM2 HVAL2]]. + unfold cons_pred_expr. + eapply sem_pred_expr_ident. + eapply sem_pred_expr_predicated_map. + eapply sem_pred_expr_predicated_prod; [eassumption|repeat constructor]. + repeat constructor; auto. + - pose proof (NE.of_list_exists2 _ (list_translation args f) (f #r (Reg r)) (f #r (Reg a))) as Y. + inversion_clear Y as [x [Y1 Y2]]. rewrite Heqo in Y1. inv Y1. + inversion_clear H as [? ? ? ? ? ? REG PRED MEM EXIT]. + inversion_clear REG as [? ? ? REG']. + inversion_clear PRED as [? ? ? PRED']. + pose proof (REG' a) as REGa. pose proof (REG' r) as REGr. + exploit sem_pred_expr_ident2; [exact REGa|]. + intro REGI'; inversion_clear REGI' as [a' [SEMa SEMa']]. + exploit sem_pred_expr_ident2; [exact REGr|]. + intro REGI'; inversion_clear REGI' as [r' [SEMr SEMr']]. + apply sem_pred_expr_ident with (l_ := Econs a' l_); [|constructor; auto]. + replace (Econs a' l_) with (Eapp (Econs a' l_) Enil) by (now apply Eapp_right_nil). + apply sem_pred_expr_fold_right; eauto. + repeat constructor. + constructor; eauto. + erewrite NE.of_list_to_list; eauto. + eapply sem_pred_expr_merge2; auto. +Qed. + +Lemma sem_pred_expr_list_translation : + forall args f i, + sem ctx f (i, None) -> + exists l, + Forall2 (sem_pred_expr (forest_preds f) sem_ident ctx) (list_translation args f) l + /\ sem_val_list ctx (to_elist l) ((is_rs i)##args). +Proof. + induction args; intros. + - exists nil; cbn; split; auto; constructor. + - exploit IHargs; try eassumption; intro EX. + inversion_clear EX as [l [FOR SEM]]. + destruct i as [rs' m' ps']. + inversion_clear H as [? ? ? ? ? ? REGSET PREDSET MEM EXIT]. + inversion_clear REGSET as [? ? ? REG]. + pose proof (REG a). + exploit sem_pred_expr_ident2; eauto; intro IDENT. + inversion_clear IDENT as [l_ [SEMP SV]]. + exists (l_ :: l). split. constructor; auto. + cbn; constructor; auto. +Qed. + +End PROOF. diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 7b68475..718eb66 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -33,6 +33,7 @@ Require Import vericert.hls.GiblePargenproofEquiv. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. +Require Import vericert.hls.AbstrSemIdent. Require Import vericert.common.Monad. Require Import Optionmonad. @@ -49,6 +50,8 @@ Module Import OptionExtra := MonadExtra(Option). Definition state_lessdef := GiblePargenproofEquiv.match_states. +(* Set Nested Proofs Allowed. *) + (*| =================================== GiblePar to Abstr Translation Proof @@ -113,17 +116,46 @@ Definition evaluable_pred_list {G} ctx pr l := In p l -> @evaluable_pred_expr G ctx pr p. +(* Lemma evaluable_pred_expr_exists : *) +(* forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst, *) +(* update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> *) +(* sem (mk_ctx i0 sp ge) f (i, cf) -> *) +(* evaluable_pred_expr (mk_ctx i0 sp ge) pr (f' #r (Reg dst)) -> *) +(* state_lessdef i ti -> *) +(* exists i', sem (mk_ctx i0 sp ge) f' (i', cf). *) +(* Proof. *) +(* intros. cbn in H. unfold Option.bind in H. destr. inv H. *) +(* destruct ti. econstructor. econstructor. *) +(* unfold evaluable_pred_expr in H1. Admitted. *) + Lemma evaluable_pred_expr_exists : - forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst, + forall sp pr f i0 exit_p exit_p' f' i ti p op args dst, + (forall x, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x f'.(forest_preds)) (pr !! x)) -> + eval_predf pr exit_p = true -> update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> - sem (mk_ctx i0 sp ge) f (i, cf) -> - evaluable_pred_expr (mk_ctx i0 sp ge) pr (f' #r (Reg dst)) -> + sem (mk_ctx i0 sp ge) f (i, None) -> + evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r (Reg dst)) -> state_lessdef i ti -> exists ti', step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti'). Proof. - intros. cbn in H. unfold Option.bind in H. destr. inv H. - destruct ti. econstructor. econstructor. - unfold evaluable_pred_expr in H1. Admitted. + intros * HPRED HEVAL **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + destruct ti. + unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval). + rewrite forest_reg_gss in Heval. + exploit sem_pred_expr_prune_predicated2; eauto; intros. + assert (eval_predf pr (dfltp p ∧ exit_p') = true) by admit. + exploit sem_pred_expr_app_predicated2; eauto; intros. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + unfold pred_ret in *. inv H4. inv H12. + destruct i. exploit sem_merge_list; eauto; intros. + instantiate (1 := args) in H4. + eapply sem_pred_expr_ident2 in H4. simplify. + exploit sem_pred_expr_ident_det. eapply H5. eapply H4. + intros. subst. exploit sem_pred_expr_ident. eapply H5. eapply H8. + intros. + + econstructor. econstructor. + Admitted. Lemma remember_expr_in : forall x l f a, @@ -148,6 +180,100 @@ Proof. auto using remember_expr_in. Qed. +Lemma not_remembered_in_forest : + forall a p f p_mid f_mid l x, + update (p, f) a = Some (p_mid, f_mid) -> + ~ In f #r (Reg x) (remember_expr f l a) -> + f #r (Reg x) = f_mid #r (Reg x). +Proof. + intros; destruct a; cbn in *; + unfold Option.bind in H; repeat destr; inv H; try easy. + - assert (~ (f #r (Reg r) = f #r (Reg x)) /\ ~ (In f #r (Reg x) l)) by tauto. + inv H. destruct (resource_eq (Reg r) (Reg x)); + try (rewrite e in *; contradiction). + now rewrite forest_reg_gso by auto. + - assert (~ (f #r (Reg r) = f #r (Reg x)) /\ ~ (In f #r (Reg x) l)) by tauto. + inv H. destruct (resource_eq (Reg r) (Reg x)); + try (rewrite e in *; contradiction). + now rewrite forest_reg_gso by auto. + - destruct (resource_eq Mem (Reg x)); try discriminate. + now rewrite forest_reg_gso by auto. +Qed. + +Lemma in_forest_or_remembered : + forall instrs p f l p' f' l', + mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall x, In (f #r (Reg x)) l' \/ f #r (Reg x) = f' #r (Reg x). +Proof. + induction instrs; try solve [crush]; []; intros. + cbn -[update] in H. + pose proof H as YX. + apply OptionExtra.mfold_left_Some in YX. inv YX. + rewrite H0 in H. + destruct x0 as ((p_mid & f_mid) & l_mid). + pose proof (IHinstrs _ _ _ _ _ _ H). + unfold Option.bind2, Option.ret in H0; cbn -[update] in H0; repeat destr. + inv H0. specialize (H1 x). + pose proof H as Y. + destruct (in_dec pred_expr_eqb (f #r (Reg x)) (remember_expr f l a)); + eauto using in_mfold_left_abstr. + inv H1; eapply not_remembered_in_forest with (f_mid := f_mid) in n; eauto; + rewrite n in *; tauto. +Qed. + +Lemma in_forest_evaluable : + forall G sp ge i' cf instrs p f l p' f' l' x i0, + mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + sem (mk_ctx i0 sp ge) f' (i', cf) -> + @evaluable_pred_list G (mk_ctx i0 sp ge) f'.(forest_preds) l' -> + evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f #r (Reg x)). +Proof. + intros. + pose proof H as Y. apply in_forest_or_remembered with (x := x) in Y. + inv Y; eauto. + inv H0. inv H5. rewrite H2. + unfold evaluable_pred_expr. eauto. +Qed. + +Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) := + match i with + | RBop (Some p) _ _ _ + | RBload (Some p) _ _ _ _ + | RBstore (Some p) _ _ _ _ + | RBexit (Some p) _ => + Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p)) + | RBsetpred p' c args p => + let preds' := match p' with + | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'') + | None => preds + end + in + match preds' ! p with + | Some _ => None + | None => Some preds' + end + | _ => Some preds + end. + +Lemma abstr_seq_revers_correct_fold_sem_pexpr : + forall instrs p f l p' f' l' preds preds', + mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + forall pred, preds ! pred = Some tt -> + f #p pred = f' #p pred. +Proof. Admitted. + +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval : + forall G instrs p f l p' f' l' i0 sp ge ps preds preds' ps', + mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + forall pred, preds ! pred = Some tt -> + sem_predset (mk_ctx i0 sp ge) f ps -> + sem_predset (@mk_ctx G i0 sp ge) f' ps' -> + ps !! pred = ps' !! pred. +Proof. Admitted. + +(* [[id:5e6486bb-fda2-4558-aed8-243a9698de85]] *) Lemma abstr_seq_reverse_correct_fold : forall sp instrs i0 i i' ti cf f' l p p' l' f, sem (mk_ctx i0 sp ge) f (i, None) -> @@ -178,15 +304,13 @@ Proof. by admit; destruct H as (pred & op & args & dst & EQ); subst a. exploit evaluable_pred_expr_exists; eauto. - unfold evaluable_pred_list in Y0. - instantiate (1 := forest_preds f'). - apply Y0 in YI. auto. - (* provable using evaluability in list *) intros [t step]. - - assert (exists ti_mid, sem {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} - f_mid (ti_mid, None)) by admit. + (* I have the pred already from sem. *) + admit. admit. admit. intros [t step]. + (* unfold evaluable_pred_list in Y0. *) + (* instantiate (1 := forest_preds f'). *) + (* eapply in_forest_evaluable; eauto. *) + (* (* provable using evaluability in list *) intros [t step]. *) - destruct H as (ti_mid & Hsem2). exploit IHinstrs. 2: { eapply Y. } eauto. auto. eauto. reflexivity. intros (ti_mid' & Hseq & Hstate). assert (state_lessdef ti_mid t) by admit. diff --git a/src/hls/GiblePargenproofEvaluable.v b/src/hls/GiblePargenproofEvaluable.v index 9013cd5..84e7200 100644 --- a/src/hls/GiblePargenproofEvaluable.v +++ b/src/hls/GiblePargenproofEvaluable.v @@ -269,7 +269,7 @@ Lemma all_evaluable_non_empty_prod : Proof. induction a; intros. - cbn in *. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply H; constructor. - - cbn in *. eapply NE.NEin_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto. + - cbn in *. eapply NE.in_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply all_evaluable_cons2; eauto. eapply all_evaluable_cons in H. eauto. Qed. @@ -326,70 +326,70 @@ Qed. eapply H. eauto. Qed. - Lemma evaluable_impl : - forall A (ctx: @ctx A) a b, - p_evaluable ctx a -> - p_evaluable ctx b -> - p_evaluable ctx (a → b). - Proof. - unfold evaluable. - inversion_clear 1 as [b1 SEM1]. - inversion_clear 1 as [b2 SEM2]. - unfold Pimplies. - econstructor. apply sem_pexpr_Por; - eauto using sem_pexpr_negate. - Qed. +Lemma evaluable_impl : + forall A (ctx: @ctx A) a b, + p_evaluable ctx a -> + p_evaluable ctx b -> + p_evaluable ctx (a → b). +Proof. + unfold evaluable. + inversion_clear 1 as [b1 SEM1]. + inversion_clear 1 as [b2 SEM2]. + unfold Pimplies. + econstructor. apply sem_pexpr_Por; + eauto using sem_pexpr_negate. +Qed. - Lemma parts_evaluable : - forall A (ctx: @ctx A) b p0, - evaluable sem_pred ctx p0 -> - evaluable sem_pexpr ctx (Plit (b, p0)). - Proof. - intros. unfold evaluable in *. inv H. - destruct b. do 2 econstructor. eauto. - exists (negb x). constructor. rewrite negb_involutive. auto. - Qed. +Lemma parts_evaluable : + forall A (ctx: @ctx A) b p0, + evaluable sem_pred ctx p0 -> + evaluable sem_pexpr ctx (Plit (b, p0)). +Proof. + intros. unfold evaluable in *. inv H. + destruct b. do 2 econstructor. eauto. + exists (negb x). constructor. rewrite negb_involutive. auto. +Qed. - Lemma p_evaluable_Pand : - forall A (ctx: @ctx A) a b, - p_evaluable ctx a -> - p_evaluable ctx b -> - p_evaluable ctx (a ∧ b). - Proof. - intros. inv H. inv H0. - econstructor. apply sem_pexpr_Pand; eauto. - Qed. +Lemma p_evaluable_Pand : + forall A (ctx: @ctx A) a b, + p_evaluable ctx a -> + p_evaluable ctx b -> + p_evaluable ctx (a ∧ b). +Proof. + intros. inv H. inv H0. + econstructor. apply sem_pexpr_Pand; eauto. +Qed. - Lemma from_predicated_evaluable : - forall A (ctx: @ctx A) f b a, - pred_forest_evaluable ctx f -> - all_evaluable2 ctx sem_pred a -> - p_evaluable ctx (from_predicated b f a). - Proof. - induction a. - cbn. destruct_match; intros. - eapply evaluable_impl. - eauto using predicated_evaluable. - unfold all_evaluable2 in H0. unfold p_evaluable. - eapply parts_evaluable. eapply H0. econstructor. - - intros. cbn. destruct_match. - eapply p_evaluable_Pand. - eapply all_evaluable2_cons2 in H0. - eapply evaluable_impl. - eauto using predicated_evaluable. - unfold all_evaluable2 in H0. unfold p_evaluable. - eapply parts_evaluable. eapply H0. - eapply all_evaluable2_cons in H0. eauto. - Qed. +Lemma from_predicated_evaluable : + forall A (ctx: @ctx A) f b a, + pred_forest_evaluable ctx f -> + all_evaluable2 ctx sem_pred a -> + p_evaluable ctx (from_predicated b f a). +Proof. + induction a. + cbn. destruct_match; intros. + eapply evaluable_impl. + eauto using predicated_evaluable. + unfold all_evaluable2 in H0. unfold p_evaluable. + eapply parts_evaluable. eapply H0. econstructor. + + intros. cbn. destruct_match. + eapply p_evaluable_Pand. + eapply all_evaluable2_cons2 in H0. + eapply evaluable_impl. + eauto using predicated_evaluable. + unfold all_evaluable2 in H0. unfold p_evaluable. + eapply parts_evaluable. eapply H0. + eapply all_evaluable2_cons in H0. eauto. +Qed. - Lemma p_evaluable_imp : - forall A (ctx: @ctx A) a b, - sem_pexpr ctx a false -> - p_evaluable ctx (a → b). - Proof. - intros. unfold "→". - unfold p_evaluable, evaluable. exists true. - constructor. replace true with (negb false) by trivial. left. - now apply sem_pexpr_negate. - Qed. +Lemma p_evaluable_imp : + forall A (ctx: @ctx A) a b, + sem_pexpr ctx a false -> + p_evaluable ctx (a → b). +Proof. + intros. unfold "→". + unfold p_evaluable, evaluable. exists true. + constructor. replace true with (negb false) by trivial. left. + now apply sem_pexpr_negate. +Qed. diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 8222513..1d59216 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -33,6 +33,7 @@ Require Import vericert.hls.GiblePargenproofEquiv. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. +Require Import vericert.hls.AbstrSemIdent. Require Import vericert.common.Monad. Module Import OptionExtra := MonadExtra(Option). @@ -102,527 +103,6 @@ Section CORRECTNESS. Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. - Lemma eval_predf_negate : - forall ps p, - eval_predf ps (negate p) = negb (eval_predf ps p). - Proof. - unfold eval_predf; intros. rewrite negate_correct. auto. - Qed. - - Lemma is_truthy_negate : - forall ps p pred, - truthy ps p -> - falsy ps (combine_pred (Some (negate (Option.default T p))) pred). - Proof. - inversion 1; subst; simplify. - - destruct pred; constructor; auto. - - destruct pred; constructor. - rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto. - rewrite eval_predf_negate. rewrite H0. auto. - Qed. - - Lemma sem_pred_expr_NEapp : - forall A B C sem f_p ctx a b v, - sem_pred_expr f_p sem ctx a v -> - @sem_pred_expr A B C f_p sem ctx (NE.app a b) v. - Proof. - induction a; crush. - - inv H. constructor; auto. - - inv H. constructor; eauto. - eapply sem_pred_expr_cons_false; eauto. - Qed. - - Lemma sem_pred_expr_NEapp2 : - forall A B C sem f_p ctx a b v ps, - (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> - (forall x, NE.In x a -> eval_predf ps (fst x) = false) -> - sem_pred_expr f_p sem ctx b v -> - @sem_pred_expr A B C f_p sem ctx (NE.app a b) v. - Proof. - induction a; crush. - - assert (IN: NE.In a (NE.singleton a)) by constructor. - specialize (H0 _ IN). destruct a. - eapply sem_pred_expr_cons_false; eauto. cbn [fst] in *. - eapply sem_pexpr_eval; eauto. - - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). - apply H0 in H2. - destruct a. cbn [fst] in *. - eapply sem_pred_expr_cons_false. - eapply sem_pexpr_eval; eauto. eapply IHa; eauto. - intros. eapply H0. constructor; tauto. - Qed. - - Lemma sem_pred_expr_NEapp3 : - forall A B C sem f_p ctx (a b: predicated B) v, - (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> - sem_pred_expr f_p sem ctx b v -> - @sem_pred_expr A B C f_p sem ctx (NE.app a b) v. - Proof. - induction a; crush. - - assert (IN: NE.In a (NE.singleton a)) by constructor. - specialize (H _ IN). destruct a. - eapply sem_pred_expr_cons_false; eauto. - - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). - apply H in H1. - destruct a. cbn [fst] in *. - eapply sem_pred_expr_cons_false; auto. - eapply IHa; eauto. - intros. eapply H. constructor; tauto. - Qed. - - Lemma sem_pred_expr_map_not : - forall A p ps y x0, - eval_predf ps p = false -> - NE.In x0 (NE.map (fun x => (p ∧ fst x, snd x)) y) -> - eval_predf ps (@fst _ A x0) = false. - Proof. - induction y; crush. - - inv H0. simplify. rewrite eval_predf_Pand. rewrite H. auto. - - inv H0. inv H2. cbn -[eval_predf]. rewrite eval_predf_Pand. - rewrite H. auto. eauto. - Qed. - - Lemma sem_pred_expr_map_Pand : - forall A B C sem ctx f_p ps x v p, - (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> - eval_predf ps p = true -> - sem_pred_expr f_p sem ctx x v -> - @sem_pred_expr A B C f_p sem ctx - (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v. - Proof. - induction x; crush. - inv H1. simplify. constructor; eauto. - simplify. replace true with (true && true) by auto. - constructor; auto. - eapply sem_pexpr_eval; eauto. - inv H1. simplify. constructor; eauto. - simplify. replace true with (true && true) by auto. - constructor; auto. - eapply sem_pexpr_eval; eauto. - eapply sem_pred_expr_cons_false. cbn. - replace false with (true && false) by auto. apply sem_pexpr_Pand; auto. - eapply sem_pexpr_eval; eauto. eauto. - Qed. - - Lemma sem_pred_expr_app_predicated : - forall A B C sem ctx f_p y x v p ps, - sem_pred_expr f_p sem ctx x v -> - (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> - eval_predf ps p = true -> - @sem_pred_expr A B C f_p sem ctx (app_predicated p y x) v. - Proof. - intros * SEM PS EVAL. unfold app_predicated. - eapply sem_pred_expr_NEapp2; eauto. - intros. eapply sem_pred_expr_map_not; eauto. - rewrite eval_predf_negate. rewrite EVAL. auto. - eapply sem_pred_expr_map_Pand; eauto. - Qed. - - Lemma sem_pred_expr_app_predicated_false : - forall A B C sem ctx f_p y x v p ps, - sem_pred_expr f_p sem ctx y v -> - (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> - eval_predf ps p = false -> - @sem_pred_expr A B C f_p sem ctx (app_predicated p y x) v. - Admitted. - - Lemma sem_pred_expr_prune_predicated : - forall A B C sem ctx f_p y x v, - sem_pred_expr f_p sem ctx x v -> - prune_predicated x = Some y -> - @sem_pred_expr A B C f_p sem ctx y v. - Proof. - intros * SEM PRUNE. unfold prune_predicated in *. - Admitted. - - Inductive sem_ident {B A: Type} (c: @ctx B) (a: A): A -> Prop := - | sem_ident_intro : sem_ident c a a. - - Lemma sem_pred_expr_pred_ret : - forall G A (ctx: @Abstr.ctx G) (i: A) ps, - sem_pred_expr ps sem_ident ctx (pred_ret i) i. - Proof. intros; constructor; constructor. Qed. - - Lemma sem_pred_expr_ident : - forall G A B ps (ctx: @Abstr.ctx G) (l: predicated A) (s: @Abstr.ctx G -> A -> B -> Prop) l_, - sem_pred_expr ps sem_ident ctx l l_ -> - forall (v: B), - s ctx l_ v -> - sem_pred_expr ps s ctx l v. - Proof. - induction 1. - - intros. constructor; auto. inv H0. auto. - - intros. apply sem_pred_expr_cons_false; auto. - - intros. inv H0. constructor; auto. - Qed. - - Lemma sem_pred_expr_ident2 : - forall G A B ps (ctx: @Abstr.ctx G) (l: predicated A) (s: @Abstr.ctx G -> A -> B -> Prop) (v: B), - sem_pred_expr ps s ctx l v -> - exists l_, sem_pred_expr ps sem_ident ctx l l_ /\ s ctx l_ v. - Proof. - induction 1. - - exists e; split; auto. constructor; auto. constructor. - - inversion_clear IHsem_pred_expr as [x IH]. - inversion_clear IH as [SEM EVALS]. - exists x; split; auto. apply sem_pred_expr_cons_false; auto. - - exists e; split; auto; constructor; auto; constructor. - Qed. - - Fixpoint of_elist (e: expression_list): list expression := - match e with - | Econs a b => a :: of_elist b - | Enil => nil - end. - - Fixpoint to_elist (e: list expression): expression_list := - match e with - | a :: b => Econs a (to_elist b) - | nil => Enil - end. - - Lemma sem_val_list_elist : - forall G (ctx: @Abstr.ctx G) l j, - sem_val_list ctx (to_elist l) j -> - Forall2 (sem_value ctx) l j. - Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. - - Lemma sem_val_list_elist2 : - forall G (ctx: @Abstr.ctx G) l j, - Forall2 (sem_value ctx) l j -> - sem_val_list ctx (to_elist l) j. - Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. - - Lemma sem_val_list_elist3 : - forall G (ctx: @Abstr.ctx G) l j, - sem_val_list ctx l j -> - Forall2 (sem_value ctx) (of_elist l) j. - Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. - - Lemma sem_val_list_elist4 : - forall G (ctx: @Abstr.ctx G) l j, - Forall2 (sem_value ctx) (of_elist l) j -> - sem_val_list ctx l j. - Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed. - - Lemma sem_pred_expr_predicated_map : - forall A B C pr (f: C -> B) ctx (pred: predicated C) (pred': C), - sem_pred_expr pr sem_ident ctx pred pred' -> - @sem_pred_expr A _ _ pr sem_ident ctx (predicated_map f pred) (f pred'). - Proof. - induction pred; unfold predicated_map; intros. - - inv H. inv H3. constructor; eauto. constructor. - - inv H. inv H5. constructor; eauto. constructor. - eapply sem_pred_expr_cons_false; eauto. - Qed. - - Lemma NEapp_NEmap : - forall A B (f: A -> B) a b, - NE.map f (NE.app a b) = NE.app (NE.map f a) (NE.map f b). - Proof. induction a; crush. Qed. - - Lemma sem_pred_expr_predicated_prod : - forall A B C pr ctx (a: predicated C) (b: predicated B) a' b', - sem_pred_expr pr sem_ident ctx a a' -> - sem_pred_expr pr sem_ident ctx b b' -> - @sem_pred_expr A _ _ pr sem_ident ctx (predicated_prod a b) (a', b'). - Proof. - induction a; intros. - - inv H. inv H4. unfold predicated_prod. - generalize dependent b. induction b; intros. - + cbn. destruct_match. inv Heqp. inv H0. inv H6. - constructor. simplify. replace true with (true && true) by auto. - eapply sem_pexpr_Pand; eauto. constructor. - + inv H0. inv H6. cbn. constructor; cbn. - replace true with (true && true) by auto. - constructor; auto. constructor. - eapply sem_pred_expr_cons_false; eauto. cbn. - replace false with (true && false) by auto. - apply sem_pexpr_Pand; auto. - - unfold predicated_prod. simplify. - rewrite NEapp_NEmap. - inv H. eapply sem_pred_expr_NEapp. - { induction b; crush. - destruct a. inv H0. constructor. - replace true with (true && true) by auto. - eapply sem_pexpr_Pand; auto. inv H6. inv H7. - constructor. - - destruct a. inv H0. constructor. - replace true with (true && true) by auto. - constructor; auto. inv H8. inv H6. constructor. - - specialize (IHb H8). eapply sem_pred_expr_cons_false; auto. - replace false with (true && false) by auto. - apply sem_pexpr_Pand; auto. - } - { exploit IHa. eauto. eauto. intros. - unfold predicated_prod in *. - eapply sem_pred_expr_NEapp3; eauto; []. - clear H. clear H0. - induction b. - { intros. inv H. destruct a. simpl. - constructor; tauto. } - { intros. inv H. inv H1. destruct a. simpl. - constructor; tauto. eauto. } } - Qed. - - Lemma sem_pred_expr_seq_app : - forall G A B (f: predicated (A -> B)) - ps (ctx: @ctx G) l f_ l_, - sem_pred_expr ps sem_ident ctx l l_ -> - sem_pred_expr ps sem_ident ctx f f_ -> - sem_pred_expr ps sem_ident ctx (seq_app f l) (f_ l_). - Proof. - unfold seq_app; intros. - remember (fun x : (A -> B) * A => fst x (snd x)) as app. - replace (f_ l_) with (app (f_, l_)) by (rewrite Heqapp; auto). - eapply sem_pred_expr_predicated_map. eapply sem_pred_expr_predicated_prod; auto. - Qed. - - Lemma sem_pred_expr_map : - forall A B C (ctx: @ctx A) ps (f: B -> C) y v, - sem_pred_expr ps sem_ident ctx y v -> - sem_pred_expr ps sem_ident ctx (NE.map (fun x => (fst x, f (snd x))) y) (f v). - Proof. - induction y; crush. inv H. constructor; crush. inv H3. constructor. - inv H. inv H5. constructor; eauto. constructor. - eapply sem_pred_expr_cons_false; eauto. - Qed. - - Lemma sem_pred_expr_flap : - forall G A B C (f: predicated (A -> B -> C)) - ps (ctx: @ctx G) l f_, - sem_pred_expr ps sem_ident ctx f f_ -> - sem_pred_expr ps sem_ident ctx (flap f l) (f_ l). - Proof. - induction f. unfold flap2; intros. inv H. inv H3. - constructor; eauto. constructor. - intros. inv H. cbn. - constructor; eauto. inv H5. constructor. - eapply sem_pred_expr_cons_false; eauto. - Qed. - - Lemma sem_pred_expr_flap2 : - forall G A B C (f: predicated (A -> B -> C)) - ps (ctx: @ctx G) l1 l2 f_, - sem_pred_expr ps sem_ident ctx f f_ -> - sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) (f_ l1 l2). - Proof. - induction f. unfold flap2; intros. inv H. inv H3. - constructor; eauto. constructor. - intros. inv H. cbn. - constructor; eauto. inv H5. constructor. - eapply sem_pred_expr_cons_false; eauto. - Qed. - - Lemma sem_pred_expr_seq_app_val : - forall G A B V (s: @Abstr.ctx G -> B -> V -> Prop) - (f: predicated (A -> B)) - ps ctx l v f_ l_, - sem_pred_expr ps sem_ident ctx l l_ -> - sem_pred_expr ps sem_ident ctx f f_ -> - s ctx (f_ l_) v -> - sem_pred_expr ps s ctx (seq_app f l) v. - Proof. - intros. eapply sem_pred_expr_ident; [|eassumption]. - eapply sem_pred_expr_seq_app; eauto. - Qed. - - Fixpoint Eapp a b := - match a with - | Enil => b - | Econs ax axs => Econs ax (Eapp axs b) - end. - - Lemma Eapp_right_nil : - forall a, Eapp a Enil = a. - Proof. induction a; cbn; try rewrite IHa; auto. Qed. - - Lemma Eapp_left_nil : - forall a, Eapp Enil a = a. - Proof. auto. Qed. - - Lemma sem_pred_expr_cons_pred_expr : - forall A (ctx: @ctx A) pr s s' a e, - sem_pred_expr pr sem_ident ctx s s' -> - sem_pred_expr pr sem_ident ctx a e -> - sem_pred_expr pr sem_ident ctx (cons_pred_expr a s) (Econs e s'). - Proof. - intros. unfold cons_pred_expr. - replace (Econs e s') with ((uncurry Econs) (e, s')) by auto. - eapply sem_pred_expr_predicated_map. - eapply sem_pred_expr_predicated_prod; eauto. - Qed. - - Lemma sem_pred_expr_fold_right : - forall A pr ctx s a a' s', - sem_pred_expr pr sem_ident ctx s s' -> - Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a') -> - @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s'). - Proof. - induction a; crush. inv H0. inv H5. destruct a'; crush. destruct a'; crush. - inv H3. eapply sem_pred_expr_cons_pred_expr; eauto. - inv H0. destruct a'; crush. inv H3. - eapply sem_pred_expr_cons_pred_expr; eauto. - Qed. - - Lemma sem_pred_expr_fold_right2 : - forall A pr ctx s a a' s', - sem_pred_expr pr sem_ident ctx s s' -> - @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') -> - Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a'). - Proof. - induction a. Admitted. - - Lemma NEof_list_some : - forall A a a' (e: A), - NE.of_list a = Some a' -> - NE.of_list (e :: a) = Some (NE.cons e a'). - Proof. - induction a; [crush|]. - intros. - cbn in H. destruct a0. inv H. auto. - destruct_match; [|discriminate]. - inv H. specialize (IHa n a ltac:(trivial)). - cbn. destruct_match. unfold NE.of_list in IHa. - fold (@NE.of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. auto. - unfold NE.of_list in IHa. fold (@NE.of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. - Qed. - - Lemma NEof_list_contra : - forall A b (a: A), - ~ NE.of_list (a :: b) = None. - Proof. - induction b; try solve [crush]. - intros. - specialize (IHb a). - enough (X: exists x, NE.of_list (a :: b) = Some x). - inversion_clear X as [x X']. - erewrite NEof_list_some; eauto; discriminate. - destruct (NE.of_list (a :: b)) eqn:?; [eauto|contradiction]. - Qed. - - Lemma NEof_list_exists : - forall A b (a: A), - exists x, NE.of_list (a :: b) = Some x. - Proof. - intros. pose proof (NEof_list_contra _ b a). - destruct (NE.of_list (a :: b)); try contradiction. - eauto. - Qed. - - Lemma NEof_list_exists2 : - forall A b (a c: A), - exists x, - NE.of_list (c :: a :: b) = Some (NE.cons c x) - /\ NE.of_list (a :: b) = Some x. - Proof. - intros. pose proof (NEof_list_exists _ b a). - inversion_clear H as [x B]. - econstructor; split; eauto. - eapply NEof_list_some; eauto. - Qed. - - Lemma NEof_list_to_list : - forall A (x: list A) y, - NE.of_list x = Some y -> - NE.to_list y = x. - Proof. - induction x; [crush|]. - intros. destruct x; [crush|]. - pose proof (NEof_list_exists2 _ x a0 a). - inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H. - cbn. f_equal. eauto. - Qed. - - Lemma sem_pred_expr_merge : - forall G (ctx: @Abstr.ctx G) ps l args, - Forall2 (sem_pred_expr ps sem_ident ctx) args l -> - sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). - Proof. - induction l; intros. - - inv H. cbn; repeat constructor. - - inv H. cbn. unfold merge. Admitted. - - Lemma sem_pred_expr_merge2 : - forall A (ctx: @ctx A) pr l l', - sem_pred_expr pr sem_ident ctx (merge l) l' -> - Forall2 (sem_pred_expr pr sem_ident ctx) l (of_elist l'). - Proof. - induction l; crush. - - unfold merge in *; cbn in *. - inv H. inv H5. constructor. - - unfold merge in H. - pose proof (NEof_list_exists _ l a) as Y. - inversion_clear Y as [x HNE]. rewrite HNE in H. - erewrite <- (NEof_list_to_list _ (a :: l)) by eassumption. - apply sem_pred_expr_fold_right2 with (s := (NE.singleton (T, Enil))) (s' := Enil). - repeat constructor. - rewrite Eapp_right_nil. auto. - Qed. - - Lemma sem_merge_list : - forall A ctx f rs ps m args, - sem ctx f ((mk_instr_state rs ps m), None) -> - @sem_pred_expr A _ _ (forest_preds f) sem_val_list ctx - (merge (list_translation args f)) (rs ## args). - Proof. - induction args; crush. cbn. constructor; constructor. - unfold merge. specialize (IHargs H). - eapply sem_pred_expr_ident2 in IHargs. - inversion_clear IHargs as [l_ [HSEM HVAL]]. - destruct_match; [|exfalso; eapply NEof_list_contra; eauto]. - destruct args; cbn -[NE.of_list] in *. - - unfold merge in *. simplify. - inv H. inv H6. specialize (H a). - eapply sem_pred_expr_ident2 in H. - inversion_clear H as [l_2 [HSEM2 HVAL2]]. - unfold cons_pred_expr. - eapply sem_pred_expr_ident. - eapply sem_pred_expr_predicated_map. - eapply sem_pred_expr_predicated_prod; [eassumption|repeat constructor]. - repeat constructor; auto. - - pose proof (NEof_list_exists2 _ (list_translation args f) (f #r (Reg r)) (f #r (Reg a))) as Y. - inversion_clear Y as [x [Y1 Y2]]. rewrite Heqo in Y1. inv Y1. - inversion_clear H as [? ? ? ? ? ? REG PRED MEM EXIT]. - inversion_clear REG as [? ? ? REG']. - inversion_clear PRED as [? ? ? PRED']. - pose proof (REG' a) as REGa. pose proof (REG' r) as REGr. - exploit sem_pred_expr_ident2; [exact REGa|]. - intro REGI'; inversion_clear REGI' as [a' [SEMa SEMa']]. - exploit sem_pred_expr_ident2; [exact REGr|]. - intro REGI'; inversion_clear REGI' as [r' [SEMr SEMr']]. - apply sem_pred_expr_ident with (l_ := Econs a' l_); [|constructor; auto]. - replace (Econs a' l_) with (Eapp (Econs a' l_) Enil) by (now apply Eapp_right_nil). - apply sem_pred_expr_fold_right; eauto. - repeat constructor. - constructor; eauto. - erewrite NEof_list_to_list; eauto. - eapply sem_pred_expr_merge2; auto. - Qed. - - Lemma sem_pred_expr_list_translation : - forall G ctx args f i, - @sem G ctx f (i, None) -> - exists l, - Forall2 (sem_pred_expr (forest_preds f) sem_ident ctx) (list_translation args f) l - /\ sem_val_list ctx (to_elist l) ((is_rs i)##args). - Proof. - induction args; intros. - - exists nil; cbn; split; auto; constructor. - - exploit IHargs; try eassumption; intro EX. - inversion_clear EX as [l [FOR SEM]]. - destruct i as [rs' m' ps']. - inversion_clear H as [? ? ? ? ? ? REGSET PREDSET MEM EXIT]. - inversion_clear REGSET as [? ? ? REG]. - pose proof (REG a). - exploit sem_pred_expr_ident2; eauto; intro IDENT. - inversion_clear IDENT as [l_ [SEMP SV]]. - exists (l_ :: l). split. constructor; auto. - cbn; constructor; auto. - Qed. - (*| Here we can finally assume that everything in the forest is evaluable, which will allow us to prove that translating the list of register accesses will also |