From bc2c535af4288e06f285658ef2844aa45da9b302 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 18 May 2023 23:22:32 +0100 Subject: Add new proofs about semantic identity --- src/hls/GiblePargenproofForward.v | 522 +------------------------------------- 1 file changed, 1 insertion(+), 521 deletions(-) (limited to 'src/hls/GiblePargenproofForward.v') 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 -- cgit