diff options
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 690 |
1 files changed, 689 insertions, 1 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 43e97a6..659a683 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -76,16 +76,42 @@ Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pr | RBexit p c => lst end. +Definition remember_expr_inc (fop : pred_op * forest) (lst: list pred_expr) (i : instr): list pred_expr := + let (pred, f) := fop in + match i with + | RBnop => lst + | RBop p op rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( + (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))))) :: lst + | RBload p chunk addr rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( + (seq_app + (seq_app (pred_ret (Eload chunk addr)) + (merge (list_translation rl f))) + (f #r Mem)))) :: lst + | RBstore p chunk addr rl r => lst + | RBsetpred p' c args p => lst + | RBexit p c => lst + end. + Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) := let '(p, f, l, lm) := s in Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i). +Definition update'_inc (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) := + let '(p, f, l, lm) := s in + Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr_inc (p, f) l i, remember_expr_m_inc (p, f) lm i)) (update (p, f) i). + Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) := Option.bind (fun x => Option.bind (fun _ => Some x) (mfold_left gather_predicates b (Some (PTree.empty _)))) (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm)) (mfold_left update' b (Some (Ptrue, empty, nil, nil)))). +Definition abstract_sequence'_inc (b : list instr) : option (forest * list pred_expr * list pred_expr) := + Option.bind (fun x => Option.bind (fun _ => Some x) + (mfold_left gather_predicates b (Some (PTree.empty _)))) + (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm)) + (mfold_left update'_inc b (Some (Ptrue, empty, nil, nil)))). + Section CORRECTNESS. Context (prog: GibleSeq.program) (tprog : GiblePar.program). @@ -106,6 +132,19 @@ Proof. eapply IHi; eauto. Qed. +Lemma equiv_update_inc: + forall i p f l lm p' f' l' lm', + mfold_left update'_inc i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left update i (Some (p, f)) = Some (p', f'). +Proof. + induction i; cbn -[update] in *; intros. + - inv H; auto. + - exploit OptionExtra.mfold_left_Some; eauto; + intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. + unfold Option.bind2, Option.ret in HB; repeat destr. inv Heqp1. + eapply IHi; eauto. +Qed. + Lemma equiv_update1: forall i p f l lm p' f' l' lm', update' (p, f, l, lm) i = Some (p', f', l', lm') -> @@ -115,6 +154,15 @@ Proof. now inv H. Qed. +Lemma equiv_update1_inc: + forall i p f l lm p' f' l' lm', + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + update (p, f) i = Some (p', f'). +Proof. + intros. unfold update'_inc, Option.bind2, Option.ret in *. repeat destr. + now inv H. +Qed. + Lemma equiv_update1'': forall i p f l lm p' f' l' lm' lp lp', update'' (p, f, l, lm, lp) i = Some (p', f', l', lm', lp') -> @@ -148,6 +196,18 @@ Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p := Definition evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr p := exists r, sem_pred_expr pr sem_mem ctx p r. +Definition cond_evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr ps cond p := + eval_predf ps cond = true -> + exists r, sem_pred_expr pr sem_value ctx p r. + +Definition cond_evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr ps cond p := + eval_predf ps cond = true -> + exists r, sem_pred_expr pr sem_mem ctx p r. + +Definition evaluable_forest {G} (ctx: @Abstr.ctx G) pr f := + (forall x, evaluable_pred_expr ctx pr (f #r (Reg x))) + /\ evaluable_pred_expr_m ctx pr (f #r Mem). + Definition evaluable_pred_list {G} ctx pr l := forall p, In p l -> @@ -472,11 +532,25 @@ Proof. unfold remember_expr; destruct a; eauto using in_cons. Qed. +Lemma remember_expr_in_inc : + forall x l f a, + In x l -> In x (remember_expr_inc f l a). +Proof. + unfold remember_expr_inc; destruct a; repeat destruct_match; eauto using in_cons. +Qed. + Lemma remember_expr_in_m : forall x l f a, In x l -> In x (remember_expr_m f l a). Proof. - unfold remember_expr; destruct a; eauto using in_cons. + unfold remember_expr_m; destruct a; eauto using in_cons. +Qed. + +Lemma remember_expr_in_m_inc : + forall x l f a, + In x l -> In x (remember_expr_m_inc f l a). +Proof. + unfold remember_expr_m_inc; destruct a; repeat destruct_match; eauto using in_cons. Qed. Lemma in_mfold_left_abstr : @@ -495,6 +569,22 @@ Proof. auto using remember_expr_in. Qed. +Lemma in_mfold_left_abstr_inc : + forall instrs p f l p' f' l' x lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + In x l -> In x l'. +Proof. + induction instrs; intros. + - cbn in *; now inv H. + - cbn -[update] in *. + pose proof H as Y. + apply OptionExtra.mfold_left_Some in Y. inv Y. + rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int). + exploit IHinstrs; eauto. + unfold Option.bind2, Option.ret in H1; repeat destr. inv H1. + destruct a; auto; apply in_cons; auto. +Qed. + Lemma in_mfold_left_abstr_m : forall instrs p f l p' f' l' x lm lm', mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -511,6 +601,22 @@ Proof. auto using remember_expr_in_m. Qed. +Lemma in_mfold_left_abstr_m_inc: + forall instrs p f l p' f' l' x lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + In x lm -> In x lm'. +Proof. + induction instrs; intros. + - cbn in *; now inv H. + - cbn -[update remember_expr_inc remember_expr_m_inc] in *. + pose proof H as Y. + apply OptionExtra.mfold_left_Some in Y. inv Y. + rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int). + exploit IHinstrs; eauto. + unfold Option.bind, Option.bind2, Option.ret in *; repeat destr. inv H1. + destruct a; auto. apply in_cons; auto. +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) -> @@ -615,6 +721,34 @@ Proof. unfold evaluable_pred_expr_m. eauto. Qed. +(* Lemma in_forest_evaluable_inc : *) +(* forall G sp ge i' cf instrs p f l p' f' l' x i0 lm lm', *) +(* mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> *) +(* 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. *) + +(* Lemma in_forest_evaluable_m_inc : *) +(* forall G sp ge i' cf instrs p f l p' f' l' i0 lm lm', *) +(* mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> *) +(* sem (mk_ctx i0 sp ge) f' (i', cf) -> *) +(* @evaluable_pred_list_m G (mk_ctx i0 sp ge) f'.(forest_preds) lm' -> *) +(* evaluable_pred_expr_m (mk_ctx i0 sp ge) f'.(forest_preds) (f #r Mem). *) +(* Proof. *) +(* intros. *) +(* pose proof H as Y. apply in_forest_or_remembered_m in Y. *) +(* inv Y; eauto. *) +(* inv H0. inv H5. rewrite H2. *) +(* unfold evaluable_pred_expr_m. eauto. *) +(* Qed. *) + Definition pe_preds_in {A} (x: predicated A) preds := NE.Forall (fun x => forall pred, PredIn pred (fst x) -> PTree.get pred preds = Some tt) x. @@ -1346,6 +1480,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc : + forall A B G a_sem instrs p f p' f' i0 sp ge preds preds' pe pe_val l l' lm lm', + update'_inc (p, f, l, lm) instrs = Some (p', f', l', lm') -> + gather_predicates preds instrs = Some preds' -> + @sem_pred_expr G A B f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val -> + NE.Forall (fun x => forall pred, PredIn pred (fst x) -> preds ! pred = Some tt) pe -> + sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. +Proof. + intros. + unfold update'_inc, Option.bind2, Option.ret in H; repeat destr. + inversion H; subst. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto. +Qed. + Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3 : forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val lm lm', mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -1369,6 +1517,29 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc : + forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + @sem_pred_expr G A B f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val -> + NE.Forall (fun x => forall pred, PredIn pred (fst x) -> preds ! pred = Some tt) pe -> + sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. +Proof. + induction instrs; [crush|]. + intros. cbn -[update remember_expr_inc remember_expr_m_inc] in H,H0. + exploit OptionExtra.mfold_left_Some. eapply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBind]. + rewrite HBind in H. + exploit OptionExtra.mfold_left_Some. eapply H0. intros [preds_mid HGATHER]. + rewrite HGATHER in H0. + exploit IHinstrs; eauto. + apply NE.Forall_forall. intros [p_op aval] YIN ypred YPREDIN. + apply NE.Forall_forall with (x:=(p_op, aval)) in H2; auto. cbn [fst snd] in *. + specialize (H2 ypred YPREDIN). + eapply gather_predicates_in; eassumption. + intros HSEM. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc; eauto. +Qed. + Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2 : forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -1383,6 +1554,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + @evaluable_pred_expr G (mk_ctx i0 sp ge) f'.(forest_preds) pe -> + NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) pe -> + evaluable_pred_expr (mk_ctx i0 sp ge) f.(forest_preds) pe. +Proof. + unfold evaluable_pred_expr in *. + intros. inv H1. exists x. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc; eauto. +Qed. + Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4 : forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -1397,6 +1582,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + @evaluable_pred_expr_m G (mk_ctx i0 sp ge) f'.(forest_preds) pe -> + NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) pe -> + evaluable_pred_expr_m (mk_ctx i0 sp ge) f.(forest_preds) pe. +Proof. + unfold evaluable_pred_expr in *. + intros. inv H1. exists x. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc; eauto. +Qed. + Lemma state_lessdef_state_equiv : forall x y, state_lessdef x y <-> state_equiv x y. Proof. split; intros; inv H; constructor; auto. Qed. @@ -1419,6 +1618,24 @@ Proof. unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_inc : + forall instrs p f l p' f' l' preds preds' lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + forall pred, preds ! pred = Some tt -> + f #p pred = f' #p pred. +Proof. + induction instrs; try solve [crush]. + intros. cbn -[update] in *. + exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND]. + exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER]. + rewrite HBIND in H. rewrite HGATHER in H0. + exploit IHinstrs; eauto. eapply gather_predicates_in; eauto. + intros. rewrite <- H2. + unfold "#p". unfold get_forest_p'. erewrite abstr_seq_revers_correct_fold_sem_pexpr_sem2; eauto. + unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto. +Qed. + (*| This lemma states that predicates are always evaluable, given that the output forest is also evaluable. This is true because gather_predicates ensures that @@ -1482,6 +1699,60 @@ Proof. eauto. inv H1; eauto. Qed. +Lemma update_rev_gather_constant_inc: + forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps, + (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) (ps !! p)) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + gather_predicates preds i = Some preds' -> + (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) (ps !! p)). +Proof. + unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr. + - inv H0. inv H1. inv Heqo. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4. + destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate. + rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto. + destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. +Qed. + +Lemma update_rev_gather_constant2_inc: + forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps, + (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) ps) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + gather_predicates preds i = Some preds' -> + (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) ps). +Proof. + unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr. + - inv H0. inv H1. inv Heqo. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4. + destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate. + rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto. + destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. +Qed. + Definition PMapmap {A} (f: positive -> A -> A) (m: PMap.t A): PMap.t A := (fst m, PTree.map f (snd m)). @@ -1607,6 +1878,57 @@ Proof. econstructor. constructor; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' ps' lm lm', + (forall p, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f #p p) ((is_ps i0) !! p)) -> + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + sem_predset (@mk_ctx G i0 sp ge) f' ps' -> + exists ps, sem_predset (mk_ctx i0 sp ge) f ps. +Proof. + induction instrs. + - intros * YH **. cbn in *. inv H. inv H0. eauto. + - intros * YH **. cbn -[update remember_expr_inc remember_expr_m_inc] in *. + exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND]. + exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER]. + rewrite HBIND in H. rewrite HGATHER in H0. + exploit IHinstrs. 3: { eauto. } 3: { eauto. } eapply update_rev_gather_constant_inc; eauto. + eauto. eauto. + intros [ps_mid HSEM_MID]. + (* destruct (preds ! p0) eqn:?. destruct u. eapply gather_predicates_in in HGATHER; eauto. *) + (* rewrite HGATHER in H2. discriminate. *) + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HBIND. + destruct a; cbn in *. + + inv Heqo. inv HGATHER. eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HGATHER. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + exists (mask_pred_map preds (is_ps i0) ps_mid). + econstructor; intros. + destruct (peq x p0); subst. + * destruct o; [assert (YX: preds ! p0 = None) by (eapply gather_predicates_fold3; eauto)|]; + rewrite mask_pred_map_not_in_pred; auto. + * inv HSEM_MID. specialize (H2 x). rewrite forest_pred_gso in H2 by auto. + destruct (preds ! x) eqn:HDESTR. + -- destruct u3. now rewrite mask_pred_map_in_pred. + -- rewrite mask_pred_map_not_in_pred; auto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. +Qed. + (* [[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 preds preds' lm lm' ps', @@ -1795,6 +2117,346 @@ Proof. Unshelve. all: exact nil. Qed. +Lemma eval_app_predicated : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + evaluable_pred_expr ctx f_p (app_predicated p c a) -> + evaluable_pred_expr ctx f_p b -> + evaluable_pred_expr ctx f_p (app_predicated p b a). +Proof. + intros * HPred HEvalR HEvalL. + inv HEvalR. inv HEvalL. + case_eq (eval_predf ps p); intros. + - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto. + eapply sem_pred_expr_app_predicated2; eauto. + - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto. +Qed. + +Lemma eval_prune_predicated : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + prune_predicated a = Some b -> + evaluable_pred_expr ctx f_p a -> + evaluable_pred_expr ctx f_p b. +Proof. + intros * HPred Hprune HEval. inv HEval. + exists x. eapply sem_pred_expr_prune_predicated; eauto. +Qed. + +Lemma eval_app_predicated_m : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + evaluable_pred_expr_m ctx f_p (app_predicated p c a) -> + evaluable_pred_expr_m ctx f_p b -> + evaluable_pred_expr_m ctx f_p (app_predicated p b a). +Proof. + intros * HPred HEvalR HEvalL. + inv HEvalR. inv HEvalL. + case_eq (eval_predf ps p); intros. + - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto. + eapply sem_pred_expr_app_predicated2; eauto. + - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto. +Qed. + +Lemma eval_prune_predicated_m : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + prune_predicated a = Some b -> + evaluable_pred_expr_m ctx f_p a -> + evaluable_pred_expr_m ctx f_p b. +Proof. + intros * HPred Hprune HEval. inv HEval. + exists x. eapply sem_pred_expr_prune_predicated; eauto. +Qed. + +Lemma eval_forest_update_inc : + forall sp i i0 p p' f f' l l' lm lm' f_p ps, + (forall x0 : positive, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x0 f_p) ps !! x0) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + evaluable_pred_list (mk_ctx i0 sp ge) f_p l' -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f_p lm' -> + evaluable_forest (mk_ctx i0 sp ge) f_p f -> + evaluable_forest (mk_ctx i0 sp ge) f_p f'. +Proof. + destruct i; intros * Hpred **; cbn -[app_predicated seq_app] in *; unfold Option.ret, Option.bind2, Option.bind in *; repeat (destruct_match; try easy; []). + - inv H; auto. + - inv H. inv Heqo1. inv H2. + constructor. + 2: { + inv H3. exists x. rewrite forest_reg_gso by discriminate. auto. + } + intro x. destruct (peq x r); subst. + 2: { + rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction. + } + rewrite forest_reg_gss. + unfold evaluable_pred_list in *. + exploit eval_app_predicated. eauto. eapply H0. constructor. eauto. + eapply H. instantiate (1:=r). intros. + eapply eval_prune_predicated; eauto. + - inv H. inv Heqo0. inv H2. + constructor. + 2: { + inv H3. exists x. rewrite forest_reg_gso by discriminate. auto. + } + intro x. destruct (peq x r); subst. + 2: { + rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction. + } + rewrite forest_reg_gss. + unfold evaluable_pred_list in *. + exploit eval_app_predicated. eauto. eapply H0. constructor. eauto. + eapply H. instantiate (1:=r). intros. + eapply eval_prune_predicated; eauto. + - inv Heqo0. inv H. inv H2. + constructor; intros. + rewrite forest_reg_gso by discriminate. auto. + rewrite forest_reg_gss. + exploit eval_app_predicated_m. eauto. apply H1. constructor. eauto. + apply H3. + intros. eapply eval_prune_predicated_m; eauto. + - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_pred_reg; eauto. + - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_exit_regs; auto. +Qed. + +Lemma abstr_seq_reverse_correct_fold_inc : + forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps', + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + (forall p : positive, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) f #p p (is_ps i0) !! p) -> + valid_mem (is_mem i0) (is_mem i) -> + all_preds_in f preds -> + eval_predf (is_ps i) p = true -> + sem (mk_ctx i0 sp ge) f (i, None) -> + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) l' -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) lm' -> + sem_predset (mk_ctx i0 sp ge) f' ps' -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + state_lessdef i ti -> + evaluable_forest (mk_ctx i0 sp ge) f'.(forest_preds) f -> + exists ti', + SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) + /\ state_lessdef i' ti'. +Proof. + induction instrs; intros * YPREDSIN YPREDNONE YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2 HEval. + - cbn in *. inv Y. + assert (X: similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} + {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}) + by reflexivity. + now eapply sem_det in X; [| exact Y1 | exact Y3 ]. + - cbn -[update'_inc] in Y. + pose proof Y as YX. + apply OptionExtra.mfold_left_Some in YX. inv YX. + cbn in YGATHER. + pose proof YGATHER as YX. + apply OptionExtra.mfold_left_Some in YX. inv YX. rewrite H0 in YGATHER. + pose proof H0 as YGATHER_SINGLE. clear H0. + rewrite H in Y. + destruct x as ((p_mid & f_mid) & l_mid). + pose proof H as Hupdate'_inc. + unfold update'_inc, Option.bind2, Option.ret in H. repeat destr. + inv H. + + destruct a. + + cbn in Heqo. inv Heqo. cbn in YGATHER_SINGLE. inv YGATHER_SINGLE. + exploit IHinstrs; eauto; simplify. + exists x; split; auto. econstructor. constructor. auto. + + exploit evaluable_pred_expr_exists_RBop; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc; eauto. + (* unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. *) + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit evaluable_pred_expr_exists_RBload; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc; eauto. + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit evaluable_pred_expr_exists_RBstore; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval4_inc; eauto. + + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval_inc. + 2: { eauto. } + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + eauto. + eauto. + intros [ps_mid HPRED2]. + exploit evaluable_pred_expr_exists_RBsetpred; eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + case_eq (eval_predf (is_ps i) (dfltp o)); intros. + * exploit evaluable_pred_expr_exists_RBexit2; eauto; intros HSTEP. + instantiate (1:=c) in HSTEP. + instantiate (1:=sp) in HSTEP. + exploit evaluable_pred_expr_exists_RBexit3. eauto. eauto. intros. + pose proof (state_lessdef_state_equiv i ti). inv H1. + specialize (H2 Y2). + pose proof (step_exists_Iterm ge sp ti _ i _ HSTEP + ltac:(symmetry; assumption)). + exploit sem_update_instr_term; eauto; intros. inv H4. + exploit abstr_fold_falsy; auto. eauto. eapply equiv_update_inc; eauto. cbn. auto. + intros. eapply sem_det in Y1; eauto. inv Y1. inv H7. + eexists. split. constructor. eauto. transitivity i. + symmetry; auto. auto. reflexivity. + * exploit evaluable_pred_expr_exists_RBexit; eauto; intros HSTEP. + instantiate (1:=c) in HSTEP. instantiate (1:=sp) in HSTEP. + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H2. + exploit sem_update_instr. auto. eauto. eauto. eauto. eapply Heqo. eauto. auto. intros. + exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + cbn. inv H4. + reflexivity. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + Unshelve. all: exact nil. +Qed. + Lemma sem_empty : forall G (ctx: @Abstr.ctx G), sem ctx empty (ctx_is ctx, None). @@ -1834,6 +2496,32 @@ Proof. intros; repeat constructor. Qed. +Lemma abstr_seq_reverse_correct_inc: + forall sp x i i' ti cf x' l lm, + abstract_sequence'_inc x = Some (x', l, lm) -> + evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l -> + evaluable_pred_list_m (mk_ctx i sp ge) x'.(forest_preds) lm -> + sem (mk_ctx i sp ge) x' (i', (Some cf)) -> + state_lessdef i ti -> + exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) + /\ state_lessdef i' ti'. +Proof. + intros. unfold abstract_sequence'_inc in H. + unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo. + pose proof H2 as X. inv X. + eapply abstr_seq_reverse_correct_fold_inc; + try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. + inversion 1. + intros; repeat constructor. + unfold evaluable_forest; split. + - intros. unfold "#r". cbn. rewrite RTree.gempty. + unfold evaluable_pred_expr. eexists. constructor. constructor. + constructor. + - intros. unfold "#r". cbn. rewrite RTree.gempty. + unfold evaluable_pred_expr_m. eexists. constructor. constructor. + constructor. +Qed. + (*| Proof Sketch: |