From 3cca0fa62b1b78ca0df38b539d88704b26b21645 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 27 May 2023 18:55:10 +0100 Subject: Finish proofs in GiblePargenproofBackward.v --- src/hls/GiblePargenproofBackward.v | 127 +++++++++++++++++++++++++++++-------- 1 file changed, 101 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 28ca830..5a18efe 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -164,18 +164,6 @@ Definition evaluable_pred_list_m {G} ctx pr l := In p l -> @evaluable_pred_expr_m 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_RBop : forall sp f i0 exit_p exit_p' f' i ti p op args dst, eval_predf (is_ps i) exit_p = true -> @@ -1487,12 +1475,76 @@ Qed. Definition PMapmap {A} (f: positive -> A -> A) (m: PMap.t A): PMap.t A := (fst m, PTree.map f (snd m)). -Definition mask_pred_map (preds: PTree.t unit) (initial_map after_map: PMap.t bool): PMap.t bool := - PMapmap (fun i a => +Definition mask_pred_map' (preds: PTree.t unit) (initial_map after_map: PMap.t bool): PMap.t bool := + (fst after_map, PTree.map (fun i a => match preds ! i with - | Some _ => a + | Some _ => after_map !! i | None => initial_map !! i - end) after_map. + end) (PTree.combine + (fun i a => + match a with + | Some x => Some x + | None => i + end) (snd initial_map) (snd after_map))). + +Definition mask_pred_map (preds: PTree.t unit) (initial_map after_map: PMap.t bool): PMap.t bool := + (fst initial_map, + PTree.combine + (fun l r => + match r with + | Some _ => r + | None => l + end) + (snd initial_map) (PTree.map (fun i a => after_map !! i) preds)). + +(* Lemma mask_pred_map_in_pred : *) +(* forall preds initial_map after_map x, *) +(* preds ! x = Some tt -> *) +(* (mask_pred_map preds initial_map after_map) !! x = after_map !! x. *) +(* Proof. *) +(* intros. unfold mask_pred_map, PMapmap. *) +(* destruct ((snd after_map) ! x) eqn:?. *) +(* - unfold "!!"; cbn. rewrite PTree.gmap. rewrite PTree.gcombine by auto. *) +(* rewrite Heqo. now rewrite H. *) +(* - unfold "!!"; cbn. rewrite PTree.gmap. rewrite PTree.gcombine by auto. *) +(* rewrite Heqo. rewrite H. now destruct ((snd initial_map) ! x). *) +(* Qed. *) + +(* Lemma mask_pred_map_not_in_pred : *) +(* forall preds initial_map after_map x, *) +(* preds ! x = None -> *) +(* fst initial_map = fst after_map -> *) +(* (mask_pred_map preds initial_map after_map) !! x = initial_map !! x. *) +(* Proof. *) +(* intros. unfold mask_pred_map, PMapmap. *) +(* destruct ((snd after_map) ! x) eqn:?. *) +(* - unfold "!!"; cbn. rewrite PTree.gmap. rewrite PTree.gcombine by auto. *) +(* rewrite Heqo. now rewrite H. *) +(* - unfold "!!"; cbn. rewrite PTree.gmap. rewrite PTree.gcombine by auto. *) +(* rewrite Heqo. rewrite H. now destruct ((snd initial_map) ! x). *) +(* Qed. *) + +Lemma mask_pred_map_in_pred : + forall preds initial_map after_map x, + preds ! x = Some tt -> + (mask_pred_map preds initial_map after_map) !! x = after_map !! x. +Proof. + intros. unfold mask_pred_map, PMapmap, "!!"; cbn. + rewrite PTree.gcombine by auto. + rewrite PTree.gmap. + rewrite H; auto. +Qed. + +Lemma mask_pred_map_not_in_pred : + forall preds initial_map after_map x, + preds ! x = None -> + (mask_pred_map preds initial_map after_map) !! x = initial_map !! x. +Proof. + intros. unfold mask_pred_map, PMapmap, "!!"; cbn. + rewrite PTree.gcombine by auto. + rewrite PTree.gmap. + rewrite H; auto. +Qed. Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval : forall G instrs p f l p' f' l' i0 sp ge preds preds' ps' lm lm', @@ -1508,8 +1560,8 @@ Proof. 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. 2: { eauto. } 2: { eauto. } eapply update_rev_gather_constant; eauto. - eauto. + exploit IHinstrs. 3: { eauto. } 3: { eauto. } eapply update_rev_gather_constant; 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. *) @@ -1533,8 +1585,12 @@ Proof. exists (mask_pred_map preds (is_ps i0) ps_mid). econstructor; intros. destruct (peq x p0); subst. - * admit. + * 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 u1. 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. @@ -1545,6 +1601,7 @@ Qed. 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', (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 -> @@ -1560,7 +1617,7 @@ Lemma abstr_seq_reverse_correct_fold : SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - induction instrs; intros * YPREDSIN YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2. + induction instrs; intros * YPREDSIN YPREDNONE YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2. - 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 |}) @@ -1596,7 +1653,9 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. + 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. @@ -1620,7 +1679,9 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. + 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. @@ -1644,7 +1705,9 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. + 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. @@ -1654,7 +1717,13 @@ Proof. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. - + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval; eauto. admit. intros [ps_mid HPRED2]. + + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval. + 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]. @@ -1665,7 +1734,9 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. + 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. @@ -1698,7 +1769,9 @@ Proof. 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. 5: { eauto. } eapply gather_predicates_update_constant; eauto. + 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. @@ -1709,6 +1782,7 @@ Proof. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. + Unshelve. all: exact nil. Qed. Lemma sem_empty : @@ -1747,6 +1821,7 @@ Proof. eapply abstr_seq_reverse_correct_fold; try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. inversion 1. + intros; repeat constructor. Qed. (*| -- cgit