From c8b7eca3c747f09cf5b3d495c4ec44c86d8b4edb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 May 2023 11:35:05 +0100 Subject: Work on smaller evaluability proof --- src/hls/GiblePargenproofBackward.v | 137 ++++++++++++++++++++++++------------- 1 file changed, 88 insertions(+), 49 deletions(-) diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index b4b4145..21a5a38 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -73,22 +73,6 @@ Context (prog: GibleSeq.program) (tprog : GiblePar.program). Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. -(*Lemma sem_equiv_execution : - forall sp x i i' ti cf x' ti', - abstract_sequence x = Some x' -> - sem (mk_ctx i sp ge) x' (i', (Some cf)) -> - SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) -> - state_lessdef i ti -> - state_lessdef i' ti'. -Proof. Admitted. - -Lemma sem_exists_execution : - forall sp x i i' ti cf x', - abstract_sequence x = Some x' -> - sem (mk_ctx i sp ge) x' (i', (Some cf)) -> - exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf). -Proof. Admitted. *) - Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := match i with | RBnop => lst @@ -663,26 +647,96 @@ Lemma gather_predicates_in_forest : all_preds_in f' preds'. Proof. Admitted. +Lemma gather_predicates_fold: + forall l preds x, + preds ! x = Some tt -> + (fold_right (fun x0 : positive => PTree.set x0 tt) preds l) ! x = Some tt. +Proof. + induction l; crush. + destruct (peq x a); subst. + { rewrite PTree.gss; auto. } + rewrite PTree.gso; eauto. +Qed. + +Lemma gather_predicates_in : + forall i preds preds' x, + gather_predicates preds i = Some preds' -> + preds ! x = Some tt -> + preds' ! x = Some tt. +Proof. + destruct i; crush; try (destruct_match; inv H; auto); + try (apply gather_predicates_fold; auto). + destruct o; auto. + apply gather_predicates_fold; auto. +Qed. + +(* Lemma update_pred_constant: *) +(* forall A p f a p_mid f_mid preds preds_mid x i0 sp ge0 b, *) +(* update (p, f) a = Some (p_mid, f_mid) -> *) +(* gather_predicates preds a = Some preds_mid -> *) +(* preds ! x = Some tt -> *) +(* @sem_pexpr A {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge0 |} f #p x b -> *) +(* sem_pexpr {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge0 |} f_mid #p x b. *) +(* Proof. *) +(* intros. Admitted. *) + +(* 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') -> *) +(* (forall x b, preds ! x = Some tt -> sem_pexpr (mk_ctx i0 sp ge) (f' #p x) b -> *) +(* sem_pexpr (mk_ctx i0 sp ge) (f #p x) b) -> *) +(* 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; try solve [crush]; intros * ? YHFORALL **. *) +(* cbn -[update] in *. *) +(* 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. eassumption. instantiate (7:=preds_mid). *) +(* intros. eapply YHFORALL in H4. unfold Option.bind2, Option.ret in *. repeat destr. *) +(* inv Heqp1. inv HBind. eapply update_pred_constant; eauto. *) +(* eassumption. eassumption. *) +(* { apply NE.Forall_forall. intros. apply NE.Forall_forall with (x:=x) in H2; auto. *) +(* eapply gather_predicates_in; eauto. } *) +(* intros. *) +(* unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBind. *) + +Lemma update_pred_constant: + forall A p f a p_mid f_mid preds preds_mid x i0 sp ge0 b, + update (p, f) a = Some (p_mid, f_mid) -> + gather_predicates preds a = Some preds_mid -> + preds ! x = Some tt -> + @sem_pexpr A {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge0 |} f #p x b <-> + sem_pexpr {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge0 |} f_mid #p x b. +Proof. + intros. Admitted. + 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', + forall A instrs p f l p' f' l' i0 sp ge preds preds' pe_val lm lm' r, + all_preds_in f preds -> mfold_left update' 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) - -> PTree.get pred preds = Some tt) pe -> - sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. + @sem_pred_expr A _ _ f'.(forest_preds) sem_value (mk_ctx i0 sp ge) (f' #r (Reg r)) pe_val -> + sem_pred_expr f.(forest_preds) sem_value (mk_ctx i0 sp ge) (f #r (Reg r)) pe_val. Proof. - induction instrs; try solve [crush]; intros. - cbn -[update] in *. - 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. eassumption. eassumption. eassumption. admit. - intros. - Admitted. -(* exploit exists_sem_pred. exact H1. *) -(* intros [[p_val e_val] [HIN HSEM]]. *) + induction instrs. + - intros. cbn in *. inv H1. inv H0. auto. + - intros. cbn -[update] in *. + exploit OptionExtra.mfold_left_Some. eapply H0. intros [[[[p_mid f_mid] l_mid] lm_mid] HBind]. + rewrite HBind in H0. + exploit OptionExtra.mfold_left_Some. eapply H1. intros [preds_mid HGATHER]. + rewrite HGATHER in H1. + unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBind. + exploit IHinstrs. + { eapply gather_predicates_in_forest; eauto. } + { eassumption. } + { eassumption. } + { eassumption. } + intros HSEM_PRED. 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', @@ -716,16 +770,6 @@ Lemma state_lessdef_state_equiv : forall x y, state_lessdef x y <-> state_equiv x y. Proof. split; intros; inv H; constructor; auto. Qed. -Lemma abstr_seq_reverse_correct_fold_false : - forall sp instrs i0 i ti cf f' l p p' l' f lm lm', - eval_predf (is_ps i) p = false -> - sem (mk_ctx i0 sp ge) f (i, Some cf) -> - mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> - sem (mk_ctx i0 sp ge) f' (i, Some cf) -> - state_lessdef i ti -> - SeqBB.step ge sp (Iexec ti) instrs (Iterm ti cf). -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 preds preds' lm lm' ps', @@ -871,13 +915,8 @@ Proof. exploit sem_update_instr_term; eauto; intros. inv H4. exploit abstr_fold_falsy; auto. eauto. eapply equiv_update; eauto. cbn. auto. intros. eapply sem_det in Y1; eauto. inv Y1. inv H7. - exploit abstr_seq_reverse_correct_fold_false. - eapply H6. eapply H5. eauto. eauto. eauto. intros. - 2: { reflexivity. } - exploit GibleSeq.step_exists. eapply H7. transitivity i. symmetry. - eapply state_lessdef_state_equiv; auto. eauto. simplify. - exists ti; split; auto. constructor. auto. transitivity i. symmetry; auto. - auto. + 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. -- cgit