(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) Set Implicit Arguments. Require Import vgtac. Require Import VocabA. Require Import Monad Global UserInputType UserInput. Require Import DItv Vali SemProof. Require Import Morphisms. Load VeqCommon. Lemma mem_lookup_access_same : forall x m, veq (RunOnly.SemPrune.SemEval.SemMem.mem_lookup x m) (RunAccess.SemPrune.SemEval.SemMem.mem_lookup x m). Proof. i. unfold RunOnly.SemPrune.SemEval.SemMem.mem_lookup , RunAccess.SemPrune.SemEval.SemMem.mem_lookup. apply PowLoc.fold2_3; [|by apply PowLoc.eq_refl|by dest_veq]. i; dest_veq; [by auto|]. i; dest_veq; [|i; by dest_veq]. unfold DomMem.IdMem.mem_find, AccMem.mem_find, veq; s. by apply DomMem.Mem.find_mor2. Qed. Lemma can_strong_update_same : forall g l, RunOnly.SemMem.can_strong_update Strong g l = RunAccess.SemMem.can_strong_update Strong g l. Proof. i; unfold RunOnly.SemMem.can_strong_update, RunAccess.SemMem.can_strong_update. reflexivity. Qed. Lemma mem_update_access_same : forall g l v m, veq (RunOnly.mem_update Strong g l v m) (RunAccess.mem_update Strong g l v m). Proof. i; unfold RunOnly.mem_update, RunAccess.mem_update , RunOnly.SemMem.mem_update, RunAccess.SemMem.mem_update. rewrite can_strong_update_same. destruct (RunAccess.SemMem.can_strong_update Strong g l). - i; unfold RunOnly.SemMem.add, RunAccess.SemMem.add; s. by unfold DomMem.IdMem.mem_add, AccMem.mem_add, veq; s. - i; unfold RunOnly.SemMem.weak_add, RunAccess.SemMem.weak_add; s. by unfold DomMem.IdMem.mem_weak_add, AccMem.mem_weak_add, veq; s. Qed. Lemma mem_wupdate_access_same : forall l v m, veq (RunOnly.mem_wupdate Strong l v m) (RunAccess.mem_wupdate Strong l v m). Proof. i; unfold RunOnly.mem_wupdate, RunAccess.mem_wupdate , RunOnly.SemMem.mem_wupdate, RunAccess.SemMem.mem_wupdate. apply PowLoc.fold2_4; [|by dest_veq]. i; dest_veq; [by auto|]. i; unfold RunOnly.SemMem.weak_add, RunAccess.SemMem.weak_add; s. by unfold DomMem.IdMem.mem_weak_add, AccMem.mem_weak_add, veq; s. Qed. Section Env. Variables (g : G.t) (cn : InterNode.t) (cmd : Syn.cmd). Lemma pow_proc_fold_access_same T : forall s f1 f2 (Hf : forall e1 e2 (He : Proc.eq e1 e2) t1 t2 (Ht : veq t1 t2), veq (f1 e1 t1) (f2 e2 t2)) (a1 : MId.m T) (a2 : Acc.MAcc.m T) (Ha : veq a1 a2), veq (PowProc.fold f1 s a1) (PowProc.fold f2 s a2). Proof. i. by eapply PowProc.fold2_3. Qed. Lemma weak_big_join_access_same : forall ls f1 f2 (Hf : forall e1 e2 (He : Proc.eq e1 e2) t1 t2 (Ht : t1 = t2), veq (f1 e1 t1) (f2 e2 t2)) a1 a2 (Ha : veq a1 a2), veq (RunOnly.BJProcMem.weak_big_join f1 ls a1) (RunAccess.BJProcMem.weak_big_join f2 ls a2). Proof. unfold RunOnly.BJProcMem.weak_big_join, RunAccess.BJProcMem.weak_big_join. i; apply pow_proc_fold_access_same; [|by auto]. i; dest_veq; [by auto|i; by apply Hf]. Qed. Lemma eval_access_same : forall e m, veq (RunOnly.eval Strong cn e m) (RunAccess.eval Strong cn e m) with eval_lv_access_same : forall lv m, veq (RunOnly.SemPrune.SemEval.eval_lv Strong cn lv m) (RunAccess.SemPrune.SemEval.eval_lv Strong cn lv m) with resolve_offset_access_same : forall o x m, veq (RunOnly.SemPrune.SemEval.resolve_offset Strong cn x o m) (RunAccess.SemPrune.SemEval.resolve_offset Strong cn x o m). Proof. { induction e; s; i. - by dest_veq. - dest_veq; [by apply eval_lv_access_same|i; by apply mem_lookup_access_same]. - by dest_veq. - by dest_veq. - by dest_veq. - by dest_veq. - by dest_veq. - dest_veq; [by apply eval_access_same|i; by dest_veq]. - dest_veq; [by apply eval_access_same|]. i; dest_veq; [by apply eval_access_same|i; by dest_veq]. - dest_veq; [by apply eval_access_same|]. i; dest_if_dec. dest_if_dec. dest_if_dec. dest_veq; [by apply eval_access_same|]. i; dest_veq; [by apply eval_access_same|]. i; by dest_veq. - destruct i; [|by apply eval_access_same]. dest_veq; [by apply eval_access_same|]. i; by dest_veq. - dest_veq; [by apply eval_lv_access_same|]. i; by dest_veq. - dest_veq; [by apply eval_lv_access_same|]. i; by dest_veq. } { induction lv; s; i. dest_veq; [|i; by apply resolve_offset_access_same]. destruct lh; [|by apply eval_access_same]. by dest_veq. } { induction o; s; i. - i; by dest_veq. - i; by apply IHo. - i; dest_veq; [by apply eval_access_same|]. i; dest_veq; [by apply mem_lookup_access_same|]. i; by apply IHo. } Qed. Lemma prune_access_same : forall e m, veq (RunOnly.SemPrune.prune g Strong cn e m) (RunAccess.SemPrune.prune g Strong cn e m). Proof. destruct e; i ; unfold RunOnly.SemPrune.prune, RunAccess.SemPrune.prune ; try by dest_veq. destruct e1; try dest_veq. destruct lv; try dest_veq. destruct lh; try dest_veq. destruct o; try dest_veq. - by apply mem_lookup_access_same. - i; dest_veq; [by apply eval_access_same|]. i; by apply mem_update_access_same. Qed. Lemma eval_list_access_same : forall args m, veq (RunOnly.SemPrune.SemEval.eval_list Strong cn args m) (RunAccess.SemPrune.SemEval.eval_list Strong cn args m). Proof. induction args; s; i. - by dest_veq. - dest_veq; [by apply eval_access_same|]. i; dest_veq; [by apply IHargs|]. i; by dest_veq. Qed. Lemma list_fold2_access_same T U V : forall f1 f2 (Hf : forall a u i, veq (f1 a u i) (f2 a u i)) (l : list T) (x : list U) (i : V), veq (RunOnly.SemMem.list_fold2_m f1 l x i) (RunAccess.SemMem.list_fold2_m f2 l x i). Proof. induction l; destruct x; s; i. - by dest_veq. - by dest_veq. - by dest_veq. - dest_veq; [by auto|by apply IHl]. Qed. Lemma bind_args_access_same : forall x e1 e2 (He : Proc.eq e1 e2) (t1 t2 : DomMem.Mem.t) (Ht : t1 = t2), veq (RunOnly.SemMem.bind_args Strong g x e1 t1) (RunAccess.SemMem.bind_args Strong g x e2 t2). Proof. i; unfold RunOnly.SemMem.bind_args, RunAccess.SemMem.bind_args. inversion He; subst. destruct (InterCfg.get_args (G.icfg g) e2); [|by dest_veq]. by apply list_fold2_access_same. Qed. Lemma eval_alloc_access_same : forall m a, veq (RunOnly.SemPrune.SemEval.eval_alloc Strong cn a m) (RunAccess.SemPrune.SemEval.eval_alloc Strong cn a m). Proof. unfold RunOnly.SemPrune.SemEval.eval_alloc, RunAccess.SemPrune.SemEval.eval_alloc. destruct a. dest_veq; [by apply eval_access_same|]. i; dest_veq. Qed. Lemma run_only_access_same : forall m, veq (run_only Strong g cn cmd m) (run_access Strong g cn cmd m). Proof. unfold run_only, run_access, RunOnly.run, RunAccess.run. destruct cmd; i. - destruct lv, lh, o ; try (i; dest_veq; [by apply eval_access_same|] ; i; by apply mem_update_access_same) ; try (dest_veq; [by apply eval_lv_access_same|] ; i; dest_veq; [by apply eval_access_same|] ; i; by apply mem_wupdate_access_same). - i; unfold RunOnly.set_ext_allocsite, RunAccess.set_ext_allocsite. dest_veq; [by apply eval_lv_access_same|]. i; dest_veq; [by apply mem_wupdate_access_same|]. i; by apply mem_wupdate_access_same. - dest_veq; [by apply eval_lv_access_same|]. i; dest_veq. + by apply eval_alloc_access_same. + i; by apply mem_wupdate_access_same. - dest_veq; [by apply eval_lv_access_same|]. i; dest_veq; [by apply mem_wupdate_access_same|]. i; by apply mem_wupdate_access_same. - dest_veq; [by apply eval_lv_access_same|]. i; by apply mem_wupdate_access_same. - by apply prune_access_same. - dest_veq; [by apply eval_list_access_same|]. i; destruct (G.is_undef_e f g). + unfold RunOnly.run_undef_funcs, RunAccess.run_undef_funcs. destruct ret_opt; [|by dest_veq]. dest_if_dec; [|dest_if_dec]. * destruct x; [s; by dest_veq|]. destruct x; [s; by dest_veq|]. s; dest_veq; [by apply eval_lv_access_same|]. i; by apply mem_wupdate_access_same. * unfold RunOnly.run_strlen, RunAccess.run_strlen. dest_veq; [by apply eval_lv_access_same|]. i; by apply mem_wupdate_access_same. * unfold RunOnly.set_ext_allocsite, RunAccess.set_ext_allocsite. dest_veq; [by apply eval_lv_access_same|]. i; dest_veq; [by apply mem_wupdate_access_same|]. i; by apply mem_wupdate_access_same. + dest_veq; [by apply eval_access_same|]. i; dest_veq. * unfold RunOnly.update_rets, RunAccess.update_rets. dest_veq; [|i; by apply mem_wupdate_access_same]. destruct ret_opt; [by apply eval_lv_access_same|by dest_veq]. * i; apply weak_big_join_access_same; [|by dest_veq]. i; by apply bind_args_access_same. - i; destruct ret_opt; [|by dest_veq]. dest_veq; [by apply eval_access_same|]. i; dest_veq; [by apply mem_lookup_access_same|]. i; by apply mem_wupdate_access_same. - by dest_veq. - by dest_veq. Qed. (* Morphisms *) Lemma add_mor : Proper (Loc.eq ==> Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) RunAccess.SemMem.add. Proof. intros l1 l2 Hl v1 v2 Hv m1 m2 Hm. split. - by apply DomMem.Mem.add_mor. - split; s. + apply PowLoc.add_mor; [by auto|by apply PowLoc.eq_refl]. + by apply PowLoc.eq_refl. Qed. Lemma weak_add_mor : Proper (Loc.eq ==> Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.SemMem.weak_add Strong). Proof. intros l1 l2 Hl v1 v2 Hv m1 m2 Hm. split. - by apply DomMem.Mem.weak_add_mor. - split; s. + apply PowLoc.add_mor; [by auto|by apply PowLoc.eq_refl]. + apply PowLoc.add_mor; [by auto|by apply PowLoc.eq_refl]. Qed. Lemma mem_update_mor : Proper (Loc.eq ==> Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.mem_update Strong g). Proof. intros l1 l2 Hl v1 v2 Hv m1 m2 Hm ; unfold RunAccess.mem_update, RunAccess.SemMem.mem_update. remember (RunAccess.SemMem.can_strong_update Strong g l1) as s1. remember (RunAccess.SemMem.can_strong_update Strong g l2) as s2. assert (s1 = s2) as Hs ; [ rewrite Heqs1, Heqs2; by apply RunAccess.SemMem.can_strong_update_mor | rewrite Hs ]. destruct s2; [by apply add_mor|by apply weak_add_mor]. Qed. Lemma mem_wupdate_mor : Proper (PowLoc.eq ==> Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.mem_wupdate Strong). Proof. intros l1 l2 Hl v1 v2 Hv m1 m2 Hm ; unfold RunAccess.mem_wupdate, RunAccess.SemMem.mem_wupdate. apply PowLoc.fold_mor. + by apply Acc.MAcc.eq_equiv. + i; apply bind_mor with (Hteq:=Mem.zb_eq) ; [by auto|intros ? ? ?; by apply weak_add_mor]. + by auto. + by apply ret_mor. Qed. Lemma acc_add_mor : forall m, Proper (Loc.eq ==> DomMem.Acc.eq ==> DomMem.Acc.eq) (DomMem.Acc.add m). Proof. intros m l1 l2 Hl a1 a2 Ha; destruct m; split; s. - apply PowLoc.add_mor; [by apply Hl|by apply Ha]. - by apply Ha. - by apply Ha. - apply PowLoc.add_mor; [by apply Hl|by apply Ha]. - apply PowLoc.add_mor; [by apply Hl|by apply Ha]. - apply PowLoc.add_mor; [by apply Hl|by apply Ha]. Qed. Lemma mem_find_mor : Proper (Loc.eq ==> Mem.eq ==> Acc.MAcc.eq Val.zb_eq) DomMem.AccMem.mem_find. Proof. intros l1 l2 Hl m1 m2 Hm; unfold DomMem.AccMem.mem_find. split; [by apply DomMem.Mem.find_mor|by apply acc_add_mor]. Qed. Lemma mem_lookup_mor : Proper (PowLoc.eq ==> Mem.eq ==> Acc.MAcc.eq Val.zb_eq) RunAccess.mem_lookup. Proof. intros l1 l2 Hl m1 m2 Hm ; unfold RunAccess.mem_lookup, RunAccess.SemMem.mem_lookup. apply PowLoc.fold_mor. + by apply Acc.MAcc.eq_equiv. + i; apply bind_mor with (Hteq:=Val.zb_eq); [by auto|]. intros v1 v2 Hv. apply bind_mor with (Hteq:=Val.zb_eq); [by apply mem_find_mor|]. intros ? ? ?; apply ret_mor; by apply Val.join_eq. + by auto. + by apply Acc.MAcc.eq_equiv. Qed. Lemma eval_mor : forall e, Proper (Mem.eq ==> Acc.MAcc.eq Val.zb_eq) (RunAccess.eval Strong cn e) with eval_lv_mor : forall l, Proper (Mem.eq ==> Acc.MAcc.eq PowLoc.zb_eq) (RunAccess.SemPrune.SemEval.eval_lv Strong cn l) with resolve_offset_mor : forall o, Proper (Val.eq ==> Mem.eq ==> Acc.MAcc.eq PowLoc.zb_eq) (fun v m => RunAccess.SemPrune.SemEval.resolve_offset Strong cn v o m). Proof. { induction e; simpl RunAccess.eval. - intros ? ? ?; by apply Acc.MAcc.eq_equiv. - intros ? ? ?; apply bind_mor with (Hteq:=PowLoc.zb_eq) ; [by apply eval_lv_mor|]. intros ? ? ?; by apply mem_lookup_mor. - intros ? ? ?. by apply Acc.MAcc.eq_equiv. - intros ? ? ?. by apply Acc.MAcc.eq_equiv. - intros ? ? ?. by apply Acc.MAcc.eq_equiv. - intros ? ? ?. by apply Acc.MAcc.eq_equiv. - intros ? ? ?. by apply Acc.MAcc.eq_equiv. - intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe|]. intros ? ? ?. apply ret_mor. by apply SemEval.eval_uop_mor. - intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe1|]. intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe2|]. intros ? ? ?. apply ret_mor. by apply SemEval.eval_bop_mor. - intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe1|]. intros v1 v2 Hv. apply if_dec_mor ; [ intro HP; eapply Itv.eq_trans ; [|by apply HP]; by apply Itv.eq_sym, DomAbs.itv_of_val_mor | intro HP; eapply Itv.eq_trans; [|by apply HP] ; by apply DomAbs.itv_of_val_mor | by apply Acc.MAcc.eq_equiv |]. apply if_dec_mor ; [ intro HP; eapply Itv.eq_trans ; [|by apply HP]; by apply Itv.eq_sym, DomAbs.itv_of_val_mor | intro HP; eapply Itv.eq_trans; [|by apply HP] ; by apply DomAbs.itv_of_val_mor | by apply IHe3 |]. apply if_dec_not_mor ; [ intro HP; eapply Itv.le_trans; [by apply HP|] ; by apply Itv.le_refl, DomAbs.itv_of_val_mor | intro HP; eapply Itv.le_trans; [by apply HP|] ; by apply Itv.le_refl, Itv.eq_sym, DomAbs.itv_of_val_mor | by apply IHe2 |]. apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe2|]. intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe3|]. intros ? ? ?; by apply ret_mor, Val.join_eq. - intros m1 m2 Hm. destruct i; [|by apply IHe]. apply bind_mor with (Hteq:=Val.zb_eq); [by apply IHe|]. intros ? ? ?; apply ret_mor, DomAbs.modify_array_mor; [by auto|]. by apply DomArrayBlk.ArrayBlk.cast_array_int_mor, DomAbs.array_of_val_mor. - intros ? ? ?; apply bind_mor with (Hteq:=PowLoc.zb_eq) ; [by apply eval_lv_mor|]. intros ? ? ?; by apply ret_mor, DomAbs.val_of_pow_loc_mor. - intros ? ? ?; apply bind_mor with (Hteq:=PowLoc.zb_eq) ; [by apply eval_lv_mor|]. intros ? ? ?; by apply ret_mor, DomAbs.val_of_pow_loc_mor. } { induction l; simpl RunAccess.SemPrune.SemEval.eval_lv. intros ? ? ?; eapply bind_mor with (Hteq:=Val.zb_eq). - destruct lh; [|by apply eval_mor]. by apply Acc.MAcc.eq_equiv. - intros ? ? ?; by apply resolve_offset_mor. } { induction o; simpl RunAccess.SemPrune.SemEval.resolve_offset. - intros ? ? ? ? ? ?; by apply ret_mor, SemEval.deref_of_val_mor. - intros ? ? ? ? ? ?. apply IHo; [|by auto]. apply DomAbs.val_of_pow_loc_mor, PowLoc.join_eq. + apply pow_loc_append_field_mor ; [by apply DomAbs.pow_loc_of_val_mor|by apply Field.eq_refl]. + apply DomArrayBlk.ArrayBlk.pow_loc_of_struct_w_field_mor ; [by apply DomAbs.array_of_val_mor|by apply Field.eq_refl]. - intros ? ? ? ? ? ?. apply bind_mor with (Hteq:=Val.zb_eq); [by apply eval_mor|]. intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq) ; [apply mem_lookup_mor; [by apply SemEval.deref_of_val_mor|by auto]|]. intros ? ? ?; apply IHo; [|by auto]. apply DomAbs.modify_array_mor; [by auto|]. apply DomArrayBlk.ArrayBlk.plus_offset_mor. + by apply DomAbs.array_of_val_mor. + by apply DomAbs.itv_of_val_mor. } Qed. Lemma eval_alloc'_mor : Proper (Val.eq ==> Val.eq) (RunAccess.SemPrune.SemEval.eval_alloc' cn). Proof. intros v1 v2 Hv. unfold RunAccess.SemPrune.SemEval.eval_alloc'. apply Val.join_eq; [by apply Val.eq_refl|]. apply DomAbs.val_of_array_mor. unfold DomArrayBlk.ArrayBlk.make. apply DomArrayBlk.ArrayBlk.add_mor ; [by apply Allocsite.eq_refl| |by apply DomArrayBlk.ArrayBlk.eq_refl]. unfold DomArrayBlk.ArrInfo.make. constructor; s; [|by apply Itv.eq_refl]. constructor; s; [by apply Itv.eq_refl|]. by apply DomAbs.itv_of_val_mor. Qed. Lemma eval_alloc_mor : forall a, Proper (Mem.eq ==> Acc.MAcc.eq Val.zb_eq) (RunAccess.SemPrune.SemEval.eval_alloc Strong cn a). Proof. destruct a. intros m1 m2 Hm. simpl RunAccess.SemPrune.SemEval.eval_alloc. apply bind_mor with (Hteq:=Val.zb_eq); [by apply eval_mor|]. intros ? ? ?. apply ret_mor. by apply eval_alloc'_mor. Qed. Lemma run_realloc_mor : forall l, Proper (SetoidList.eqlistA Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.run_realloc Strong cn l). Proof. intros l v1 v2 Hv m1 m2 Hm; unfold RunAccess.run_realloc. inversion Hv; subst; [by apply ret_mor|]. inversion H0; subst; [by apply ret_mor|]. apply bind_mor with (Hteq:=PowLoc.zb_eq); [by apply eval_lv_mor|]. intros ? ? ?. apply mem_wupdate_mor; [by auto|by apply eval_alloc'_mor|by auto]. Qed. Lemma run_strlen_mor : forall l, Proper (Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.run_strlen Strong cn l). Proof. intros ? m1 m2 Hm; unfold RunAccess.run_strlen. apply bind_mor with (Hteq:=PowLoc.zb_eq); [by apply eval_lv_mor|]. intros ? ? ?. apply mem_wupdate_mor; [by auto|by apply Val.eq_refl|by auto]. Qed. Lemma set_ext_allocsite_mor : forall l a, Proper (Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.set_ext_allocsite Strong cn l a). Proof. intros ? ? m1 m2 Hm; unfold RunAccess.set_ext_allocsite. apply bind_mor with (Hteq:=PowLoc.zb_eq); [by apply eval_lv_mor|]. intros ? ? ?. apply bind_mor with (Hteq:=Mem.zb_eq). - apply mem_wupdate_mor; [by auto|by apply Val.eq_refl|by auto]. - intros ? ? ?. apply mem_wupdate_mor; [by auto|by apply Val.eq_refl|by auto]. Qed. Lemma run_undef_funcs_mor : forall ret_opt p, Proper (SetoidList.eqlistA Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.run_undef_funcs Strong cn ret_opt p). Proof. i. intros vs1 vs2 Hvs m1 m2 Hm. unfold RunAccess.run_undef_funcs. destruct ret_opt; [|by apply ret_mor]. apply if_dec_mor; [by auto|by auto|by apply run_realloc_mor|]. apply if_dec_mor; [by auto|by auto|by apply run_strlen_mor|]. by apply set_ext_allocsite_mor. Qed. Lemma list_fold2_m_mor T U V : forall (teq : T -> T -> Prop) (ueq : U -> U -> Prop) (veq : V -> V -> Prop) (v_zb_eq : DLat.zb_equiv veq), Proper ((teq ==> ueq ==> veq ==> Acc.MAcc.eq v_zb_eq) ==> SetoidList.eqlistA teq ==> SetoidList.eqlistA ueq ==> veq ==> Acc.MAcc.eq v_zb_eq) RunAccess.SemMem.list_fold2_m. Proof. intros ? ? ? ? f1 f2 Hf ts1 ts2 Hts. induction Hts. - intros us1 us2 Hus v1 v2 Hv; s. inversion Hus; [by apply ret_mor|by apply ret_mor]. - intros us1 us2 Hus v1 v2 Hv; s. inversion Hus; [by apply ret_mor|]. apply bind_mor with (Hteq:=v_zb_eq); [by apply Hf|by apply IHHts]. Qed. Lemma bind_arg_mor : forall f x, Proper (Val.eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.SemMem.bind_arg Strong f x). Proof. intros f x v1 v2 Hv m1 m2 Hm. unfold RunAccess.SemMem.bind_arg. apply mem_wupdate_mor; [by apply PowLoc.eq_refl|by auto|by auto]. Qed. Lemma bind_args_mor : Proper (SetoidList.eqlistA Val.eq ==> eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.SemMem.bind_args Strong g). Proof. intros vs1 vs2 Hvs v1 v2 Hv m1 m2 Hm; subst. unfold RunAccess.SemMem.bind_args; destruct (InterCfg.get_args (G.icfg g) v2) ; [|by apply ret_mor]. apply list_fold2_m_mor with (teq:=eq) (ueq:=Val.eq) ; [|by apply eqlistA_eq_refl|by auto|by auto]. intros ? ? ? ? ? ? ? ? ?; subst. by apply bind_arg_mor. Qed. Lemma weak_big_join_mor : Proper ((eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) ==> PowProc.eq ==> Acc.MAcc.eq Mem.zb_eq ==> Acc.MAcc.eq Mem.zb_eq) RunAccess.BJProcMem.weak_big_join. Proof. intros f1 f2 Hf l1 l2 Hl m1 m2 Hm. unfold RunAccess.BJProcMem.weak_big_join. apply PowProc.fold_mor; [by apply Acc.MAcc.eq_equiv| |by auto|by auto]. intros; subst. eapply bind_mor; [by apply Hacc|]. intros m1' m2' Hm'. by apply Hf. Qed. Lemma SMProcLoc_map_mor : Proper ((eq ==> Loc.eq) ==> PowProc.eq ==> PowLoc.eq) SMProcLoc.map. Proof. intros f1 f2 Hf p1 p2 Hp. unfold SMProcLoc.map. apply PowProc.fold_mor ; [by apply PowLoc.zb_eq| |by auto|by apply PowLoc.eq_refl]. intros; subst. apply PowLoc.add_mor; [by apply Hf|by auto]. Qed. Lemma update_rets_mor : Proper (PowProc.eq ==> eq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.update_rets Strong cn). Proof. intros l1 l2 Hl lv1 lv2 Hlv m1 m2 Hm; subst. unfold RunAccess.update_rets. apply bind_mor with (Hteq:=PowLoc.zb_eq). - destruct lv2; [by apply eval_lv_mor|by apply ret_mor]. - intros ret_loc1 ret_loc2 Hret_loc. apply mem_wupdate_mor; [|by apply DomAbs.val_of_pow_loc_mor|by auto]. apply SMProcLoc_map_mor; [|by auto]. intros ? ? ?; subst. by apply loc_of_proc_mor. Qed. Lemma prune_mor : forall e, Proper (Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (RunAccess.SemPrune.prune g Strong cn e). Proof. destruct e; intros ? ? ?; unfold RunAccess.SemPrune.prune ; try by apply ret_mor. destruct e1; try by apply ret_mor. destruct lv; try by apply ret_mor. destruct lh; try by apply ret_mor. destruct o; try by apply ret_mor. apply bind_mor with (Hteq:=Val.zb_eq) ; [apply mem_lookup_mor; [by apply PowLoc.eq_refl|by auto]|]. intros ? ? ?; apply bind_mor with (Hteq:=Val.zb_eq); [by apply eval_mor|]. intros ? ? ?; apply mem_update_mor ; [ by apply Loc.eq_refl | apply DomAbs.modify_itv_mor ; [by auto|apply SemPrune.itv_prune_mor; by apply itv_of_val_mor] | by auto ]. Qed. Lemma eval_list_mor : forall args, Proper (Mem.eq ==> Acc.MAcc.eq list_val_zb_eq) (RunAccess.SemPrune.SemEval.eval_list Strong cn args). Proof. induction args; intros ? ? ?. - split; [by constructor|by apply Acc.eq_refl]. - s. apply bind_mor with (Hteq:=Val.zb_eq). + by apply eval_mor. + intros ? ? ?. apply bind_mor with (Hteq:=list_val_zb_eq). * by apply IHargs. * intros ? ? ?. apply ret_mor. by constructor. Qed. Ltac mor := repeat match goal with | |- Val.eq ?x ?x => by apply Val.eq_refl | |- Itv.eq ?x ?x => by apply Itv.eq_refl | |- Mem.eq ?x ?x => by apply Mem.eq_refl | |- Allocsite.eq ?x ?x => by apply Allocsite.eq_refl | H : ?eq ?x ?y |- ?eq ?x ?y => by apply H | |- Acc.MAcc.eq _ ?x ?x => by apply (DLat.zb_equiv_refl (Acc.MAcc.eq_equiv _)) | |- Proper _ _ => intros ? ? ? | |- (_ ==> _)%signature _ _ => intros ? ? ? | H : Val.eq ?y ?x |- Val.eq ?x ?y => apply Val.eq_sym | |- Acc.MAcc.eq _ (if _ then _ else _) (if _ then _ else _) => apply if_dec_mor | |- Itv.eq ?x1 ?y1 -> Itv.eq ?x2 ?y2 => let Heq := fresh "Heq" in intro Heq; apply Itv.eq_trans with x1 ; [ apply Itv.eq_sym | apply Itv.eq_trans with y1; [by apply Heq|] ] | |- Itv.eq (DomAbs.itv_of_val _) (DomAbs.itv_of_val _) => apply DomAbs.itv_of_val_mor | |- Acc.MAcc.eq Val.zb_eq (RunAccess.SemPrune.SemEval.eval _ _ _ _) (RunAccess.SemPrune.SemEval.eval _ _ _ _) => apply eval_mor | |- Acc.MAcc.eq Val.zb_eq (RunAccess.eval _ _ _ _) (RunAccess.eval _ _ _ _) => apply eval_mor | |- Acc.MAcc.eq _ (if Sumbool.sumbool_not ?A (?A -> False) ?HA then _ else _) (if Sumbool.sumbool_not ?B (?B -> False) ?HB then _ else _) => let Heq := fresh "Heq" in let Ha := fresh "Ha" in let Hb := fresh "Hb" in assert (A <-> B) as Heq ; [| destruct (Sumbool.sumbool_not A (~ A) HA) as [Ha | Ha] , (Sumbool.sumbool_not B (~ B) HB) as [Hb | Hb] ; [|elim Ha; by apply Heq, Hb|elim Hb; by apply Heq, Ha|] ; clear Heq ] | |- _ <-> _ => split | |- Itv.le _ _ -> Itv.le _ _ => let Htemp := fresh "Htemp" in intro Htemp; eapply Itv.le_trans; [eapply Itv.le_trans; [|apply Htemp]|] | |- Itv.le _ _ => apply Itv.le_refl | |- Acc.MAcc.eq _ (Acc.MAcc.bind _ _) (Acc.MAcc.bind _ _) => first [ apply bind_mor with (Hteq:=Val.zb_eq) | apply bind_mor with (Hteq:=PowLoc.zb_eq) | apply bind_mor with (Hteq:=Mem.zb_eq) | apply bind_mor with (Hteq:=list_val_zb_eq) ] | |- Acc.MAcc.eq _ (Acc.MAcc.ret _) (Acc.MAcc.ret _) => apply ret_mor | |- Val.eq (SemEval.eval_uop _ _) (SemEval.eval_uop _ _) => apply SemEval.eval_uop_mor | |- Acc.MAcc.eq Val.zb_eq (RunAccess.SemPrune.SemEval.SemMem.mem_lookup _ _) (RunAccess.SemPrune.SemEval.SemMem.mem_lookup _ _) => apply mem_lookup_mor | |- Val.eq (SemEval.eval_bop _ _ _) (SemEval.eval_bop _ _ _) => apply SemEval.eval_bop_mor | |- Val.eq (DomAbs.modify_array _ _) (DomAbs.modify_array _ _) => apply modify_array_mor | |- DomArrayBlk.ArrayBlk.eq (DomArrayBlk.ArrayBlk.cast_array_int _ _) (DomArrayBlk.ArrayBlk.cast_array_int _ _) => apply DomArrayBlk.ArrayBlk.cast_array_int_mor | |- DomArrayBlk.ArrayBlk.eq (DomAbs.array_of_val _) (DomAbs.array_of_val _) => apply DomAbs.array_of_val_mor | |- Val.eq (DomAbs.val_of_pow_loc _) (DomAbs.val_of_pow_loc _) => apply DomAbs.val_of_pow_loc_mor | |- Acc.MAcc.eq PowLoc.zb_eq (RunAccess.SemPrune.SemEval.resolve_offset _ _ _ _ _) (RunAccess.SemPrune.SemEval.resolve_offset _ _ _ _ _) => apply resolve_offset_mor | |- PowLoc.eq (SemEval.deref_of_val _) (SemEval.deref_of_val _) => apply SemEval.deref_of_val_mor | |- DomArrayBlk.ArrayBlk.eq (DomArrayBlk.ArrayBlk.plus_offset _ _) (DomArrayBlk.ArrayBlk.plus_offset _ _) => apply DomArrayBlk.ArrayBlk.plus_offset_mor | |- Acc.MAcc.eq Mem.zb_eq (RunAccess.mem_update _ _ _ _ _) (RunAccess.mem_update _ _ _ _ _) => apply mem_update_mor | |- Acc.MAcc.eq Mem.zb_eq (RunAccess.mem_wupdate _ _ _ _) (RunAccess.mem_wupdate _ _ _ _) => apply mem_wupdate_mor | |- PowLoc.eq (PowLoc.singleton _) (PowLoc.singleton _) => apply PowLoc.singleton_mor | |- context[Loc.eq'] => replace Loc.eq' with Loc.eq by auto | |- Loc.eq (DomBasic.loc_of_allocsite _) (DomBasic.loc_of_allocsite _) => apply loc_of_allocsite_mor | |- Val.eq (RunAccess.SemPrune.SemEval.eval_alloc' _ _) (RunAccess.SemPrune.SemEval.eval_alloc' _ _) => apply eval_alloc'_mor | |- Acc.MAcc.eq Val.zb_eq (RunAccess.SemPrune.SemMem.mem_lookup _ _) (RunAccess.SemPrune.SemMem.mem_lookup _ _) => apply mem_lookup_mor | |- Acc.MAcc.eq Mem.zb_eq (RunAccess.SemPrune.SemMem.mem_update _ _ _ _ _) (RunAccess.SemPrune.SemMem.mem_update _ _ _ _ _) => apply mem_update_mor | |- Val.eq (DomAbs.modify_itv _ _) (DomAbs.modify_itv _ _) => apply DomAbs.modify_itv_mor | |- Itv.eq (SemPrune.itv_prune _ _ _) (SemPrune.itv_prune _ _ _) => apply SemPrune.itv_prune_mor | |- Acc.MAcc.eq list_val_zb_eq (RunAccess.SemPrune.SemEval.eval_list _ _ _ _) (RunAccess.SemPrune.SemEval.eval_list _ _ _ _) => apply eval_list_mor | |- Val.eq (Val.join _ _) (Val.join _ _) => apply Val.join_eq | |- Mem.eq (Mem.join _ _) (Mem.join _ _) => apply Mem.join_eq | |- Itv.eq (Itv.meet _ _) (Itv.meet _ _) => apply Itv.meet_eq | |- Itv.eq (Itv.join _ _) (Itv.join _ _) => apply Itv.join_eq | |- SetoidList.eqlistA Val.eq _ _ => constructor | H : SetoidList.eqlistA _ ?x ?y |- SetoidList.eqlistA _ ?x ?y => by apply H end. (* Soundness *) Lemma add_access_sound : forall e v, aeqm1 (RunAccess.SemMem.add e v). Proof. unfold RunAccess.SemMem.add, DomMem.AccMem.mem_add; s; i. unfold aeqm1; s; i. split; [|by apply Acc.eq_refl]. intro k; destruct (Loc.eq_dec k e). - eapply Val.eq_trans; [apply Mem.add_same; by apply e0|]. eapply Val.eq_trans; [|by apply Val.eq_sym, Mem.join_find]. eapply Val.eq_trans; [by apply Val.join_bot|]. apply Val.join_eq; [by apply Val.eq_sym, Mem.add_same|]. apply Val.eq_sym, Hm'. by apply Acc.mem_accessof_left, PowLoc.mem_add_1. - eapply Val.eq_trans; [rewrite Mem.add_diff; [by apply Val.eq_refl|by auto]|]. eapply Val.eq_trans; [|by apply Val.eq_sym, Mem.join_find]. eapply Val.eq_trans; [by apply Mem.join_find|]. apply Val.join_eq; [|by apply Val.eq_refl]. rewrite Mem.add_diff; [|by auto]. by apply Val.eq_refl. Qed. Lemma weak_add_access_sound : forall e v, aeqm1 (RunAccess.SemMem.weak_add Strong e v). Proof. unfold RunAccess.SemMem.weak_add, DomMem.AccMem.mem_weak_add; s; i. unfold aeqm1; s; i. split; [|by apply Acc.eq_refl]. intro k; destruct (Loc.eq_dec k e). - eapply Val.eq_trans; [apply Val.eq_sym, Mem.weak_add_prop; by auto|]. eapply Val.eq_trans; [|by apply Val.eq_sym, Mem.join_find]. eapply Val.eq_trans ; [apply Val.join_eq; [by apply Val.eq_refl|by apply Mem.join_find]|]. eapply Val.eq_trans; [by apply Val.join_assoc|]. apply Val.join_eq; [|apply Mem.find_mor; [by auto|by apply Mem.eq_refl]]. by apply Mem.weak_add_prop. - eapply Val.eq_trans ; [rewrite Mem.weak_add_diff; [by apply Val.eq_refl|by auto]|]. eapply Val.eq_trans; [|by apply Val.eq_sym, Mem.join_find]. eapply Val.eq_trans; [by apply Mem.join_find|]. apply Val.join_eq; [|by apply Val.eq_refl]. rewrite Mem.weak_add_diff; [|by auto]. by apply Val.eq_refl. Qed. Lemma mem_update_access_sound : forall k v, aeqm1 (RunAccess.mem_update Strong g k v). Proof. unfold RunAccess.mem_update, RunAccess.SemMem.mem_update; i. destruct (RunAccess.SemMem.can_strong_update Strong g k). - by apply add_access_sound. - by apply weak_add_access_sound. Qed. Lemma mem_wupdate_access_sound : forall k v, aeqm1 (RunAccess.mem_wupdate Strong k v). Proof. unfold RunAccess.mem_wupdate, RunAccess.SemMem.mem_wupdate; i. - remember (fun (lv : Loc.t) m_a => DomMem.Acc.MAcc.bind m_a (RunAccess.SemMem.weak_add Strong lv v)) as f. apply ret_mem2, fold_access_sound. + subst; i; destruct m; s. by apply Acc.join_left. + subst; i. apply bind_mmem. by apply weak_add_access_sound. + intros e m1 m2 Hm. subst. eapply bind_mor; [by apply Hm|]. intros m1' m2' Hm'. apply weak_add_mor; [by apply Loc.eq_refl|by apply Val.eq_refl|by auto]. Qed. Lemma mem_find_access_sound : forall e, aeqv Val.zb_eq (DomMem.AccMem.mem_find e). Proof. unfold aeqv, DomMem.AccMem.mem_find; s; i. split; [|by apply Acc.eq_refl]. eapply Val.eq_trans; [by apply Mem.join_find|]. eapply Val.eq_trans; [|by apply Val.eq_sym, Val.join_bot]. apply Val.join_eq; [by apply Val.eq_refl|]. apply Hm'. by apply Acc.mem_accessof_right, PowLoc.mem_add_1, Loc.eq_refl. Qed. Lemma mem_lookup_access_sound : forall l, aeqv Val.zb_eq (RunAccess.mem_lookup l). Proof. unfold RunAccess.mem_lookup, RunAccess.SemMem.mem_lookup; i. match goal with | |- aeqv _ (fun m => ?e _) => apply aeqmv_1 with (f:= fun m => e) end. apply fold_access_sound'. - i. destruct v. s. by apply Acc.join_left. - i. apply bind_mval. i. apply aeqv_1 with (Hteq:=Val.zb_eq). + intros v1 v2 Hv. apply ret_mor, Val.join_eq; [by apply Val.eq_refl|by auto]. + by apply mem_find_access_sound. - i. intros ? ? ?. apply bind_mor with (Hteq:=Val.zb_eq); [by auto|]. intros ? ? ?. apply bind_mor with (Hteq:=Val.zb_eq). + apply mem_find_mor; [by apply Loc.eq_refl|by apply Mem.eq_refl]. + intros ? ? ?. apply ret_mor. by apply Val.join_eq. Qed. Lemma eval_access_sound : forall e, aeqv Val.zb_eq (RunAccess.eval Strong cn e) with eval_lv_access_sound : forall lv, aeqv PowLoc.zb_eq (RunAccess.SemPrune.SemEval.eval_lv Strong cn lv) with resolve_offset_sound : forall o x, aeqv PowLoc.zb_eq (RunAccess.SemPrune.SemEval.resolve_offset Strong cn x o). Proof. induction e; simpl RunAccess.eval. { by apply aeqv_3. } { apply aeqv_2 with (Hteq:=PowLoc.zb_eq) ; [by apply mem_lookup_access_sound|by mor|]. by apply eval_lv_access_sound. } { by apply aeqv_3. } { by apply aeqv_3. } { by apply aeqv_3. } { by apply aeqv_3. } { by apply aeqv_3. } { apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe]. by apply aeqv_3. } { apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe1]. apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe2]. by apply aeqv_3. } { apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe1]. dest_if_dec; [by apply aeqv_3|]. dest_if_dec. dest_if_dec. apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe2]. apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe3]. by apply aeqv_3. } { destruct i. - apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply IHe]. by apply aeqv_3. - by apply IHe. } { apply aeqv_1 with (Hteq:=PowLoc.zb_eq); [by mor|]. by apply eval_lv_access_sound. } { apply aeqv_1 with (Hteq:=PowLoc.zb_eq); [by mor|]. by apply eval_lv_access_sound. } destruct lv; simpl RunAccess.SemPrune.SemEval.eval_lv. { apply aeqv_2 with (Hteq:=Val.zb_eq); [|by mor|]. - by apply resolve_offset_sound. - destruct lh. + by apply aeqv_3. + by apply eval_access_sound. } induction o; simpl RunAccess.SemPrune.SemEval.resolve_offset; i. { by apply aeqv_3. } { by apply IHo. } { apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply eval_access_sound]. apply aeqv_2 with (Hteq:=Val.zb_eq) ; [i|by mor|by apply mem_lookup_access_sound]. by apply IHo. } Qed. Lemma set_ext_allocsite_access_sound : forall lv a, aeqm1 (RunAccess.set_ext_allocsite Strong cn lv (allocsite_of_ext a)). Proof. i; unfold RunAccess.set_ext_allocsite. apply bind_val1 with (Ht:=PowLoc.zb_eq) ; [i|by mor|by apply eval_lv_access_sound]. apply bind_mem1; [|by mor|by apply mem_wupdate_access_sound]. by apply mem_wupdate_access_sound. Qed. Lemma eval_alloc_access_sound : forall a, aeqv Val.zb_eq (RunAccess.SemPrune.SemEval.eval_alloc Strong cn a). Proof. destruct a; unfold RunAccess.SemPrune.SemEval.eval_alloc. apply aeqv_1 with (Hteq:=Val.zb_eq); [by mor|by apply eval_access_sound]. Qed. Lemma prune_access_sound : forall e, aeqm1 (RunAccess.SemPrune.prune g Strong cn e). Proof. destruct e; unfold RunAccess.SemPrune.prune ; try (apply ret_mem1; i; by mor). destruct e1; try (apply ret_mem1; i; by mor). destruct lv; try (apply ret_mem1; i; by mor). destruct lh; try (apply ret_mem1; i; by mor). destruct o; try (apply ret_mem1; i; by mor). apply bind_val1 with (Ht:=Val.zb_eq) ; [i|by mor|by apply mem_lookup_access_sound]. apply bind_val1 with (Ht:=Val.zb_eq) ; [i|by mor|by apply eval_access_sound]. by apply mem_update_access_sound. Qed. Lemma eval_list_access_sound : forall args, aeqv list_val_zb_eq (RunAccess.SemPrune.SemEval.eval_list Strong cn args). Proof. induction args. - s. apply aeqv_3. - s. apply aeqv_2 with (Hteq:=Val.zb_eq); [i|by mor|by apply eval_access_sound]. apply aeqv_1 with (Hteq:=list_val_zb_eq); [by mor|by apply IHargs]. Qed. Lemma run_realloc_access_sound : forall l v, aeqm1 (RunAccess.run_realloc Strong cn l v). Proof. i; unfold RunAccess.run_realloc. destruct v; [apply ret_mem1; i; by apply Mem.eq_refl|]. destruct v; [apply ret_mem1; i; by apply Mem.eq_refl|]. apply bind_val1 with (Ht:=PowLoc.zb_eq) ; [i|by mor|by apply eval_lv_access_sound]. by apply mem_wupdate_access_sound. Qed. Lemma run_strlen_access_sound : forall l, aeqm1 (RunAccess.run_strlen Strong cn l). Proof. unfold RunAccess.run_strlen; i. apply bind_val1 with (Ht:=PowLoc.zb_eq) ; [i|by mor|by apply eval_lv_access_sound]. by apply mem_wupdate_access_sound. Qed. Lemma run_undef_funcs_access_sound : forall ret_opt p v, aeqm1 (RunAccess.run_undef_funcs Strong cn ret_opt p v). Proof. unfold RunAccess.run_undef_funcs; i. destruct ret_opt. - destruct (Proc.eq_dec p str_realloc); [by apply run_realloc_access_sound|]. destruct (Proc.eq_dec p str_strlen); [by apply run_strlen_access_sound|]. apply set_ext_allocsite_access_sound. - apply ret_mem1; i; by apply Mem.eq_refl. Qed. Lemma list_fold2_access_sound T U (ueq : U -> U -> Prop) (Hueq : DLat.zb_equiv ueq) : forall (l : list T) (vs : list U) f (Hf : forall t u, aeqm1 (f t u)) (Hf_mor : forall t, Proper (ueq ==> Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (f t)), aeqm1 (RunAccess.SemMem.list_fold2_m f l vs). Proof. induction l; destruct vs. - s; i. apply ret_mem1; i; by apply Mem.eq_refl. - s; i. apply ret_mem1; i; by apply Mem.eq_refl. - s; i. apply ret_mem1; i; by apply Mem.eq_refl. - s; i. apply bind_mem1; [by apply IHl|mor|by apply Hf]. apply list_fold2_m_mor with (teq:=eq) (ueq:=ueq) ; [ intros ? ? ?; subst; by apply Hf_mor | by apply eqlistA_eq_refl | by apply (DLat.zb_equiv_refl (list_zb_eq Hueq)) | by auto ]. Qed. Lemma bind_arg_access_sound : forall f x v, aeqm1 (RunAccess.SemMem.bind_arg Strong f x v). Proof. unfold RunAccess.SemMem.bind_arg; i. by apply mem_wupdate_access_sound. Qed. Lemma bind_args_access_sound : forall vs e, aeqm1 (RunAccess.SemMem.bind_args Strong g vs e). Proof. unfold RunAccess.SemMem.bind_args; i. destruct (InterCfg.get_args (G.icfg g) e) ; [|apply ret_mem1; i; by apply Mem.eq_refl]. apply list_fold2_access_sound with (ueq:=Val.eq). - by apply Val.zb_eq. - by apply bind_arg_access_sound. - by apply bind_arg_mor. Qed. Lemma weak_big_join_access_sound : forall f (Hf_access_sound : forall e, aeqm1 (f e)) (Hf_mor : forall e, Proper (Mem.eq ==> Acc.MAcc.eq Mem.zb_eq) (f e)) l, aeqm1 (fun m => RunAccess.BJProcMem.weak_big_join f l (Acc.MAcc.ret m)). Proof. { unfold RunAccess.BJProcMem.weak_big_join. i; unfold aeqm1, Acc.MAcc.bind, Acc.MAcc.ret. intros m m'. remember (fun (s : TStr.string_t) (acc : Acc.MAcc.m DomMem.Mem.t) => let (x, a1) := acc in let (y, a2) := f s x in (y, Acc.join a1 a2)) as f'. apply PowProc.fold2_4 with (P := fun t q => forall (Hdis : Vali.disjoint m' (Acc.get_acc q)), Acc.MAcc.eq Mem.zb_eq t (mem_join q m')). - subst; i. destruct t1 as [x1 a1], t2 as [x2 a2]. remember (f e x1) as _m. destruct _m as [x1' a1']. remember (f e x2) as _m. destruct _m as [x2' a2']. remember (f e (Mem.join x2 m')) as _m. destruct _m as [x3 a3]. destruct Ht as [Ht1 Ht2] ; [eapply disjoint_left; by apply Hdis|simpl in Ht1, Ht2]. assert (Acc.MAcc.eq Mem.zb_eq (x3, a3) (mem_join (x2', a2') m')) as eq1. { rewrite Heq_m1, Heq_m0. apply Hf_access_sound. rewrite <- Heq_m0. eapply disjoint_right; by apply Hdis. } destruct eq1 as [eq11 eq12]; simpl in eq11, eq12. assert (Acc.MAcc.eq Mem.zb_eq (x1', a1') (x3, a3)) as eq2. { rewrite Heq_m, Heq_m1. apply Hf_mor. by auto. } destruct eq2 as [eq21 eq22]; simpl in eq21, eq22. split; s. + by apply Mem.eq_trans with x3. + apply Acc.join_eq; [by auto|by apply Acc.eq_trans with a3]. - split; s; [by apply Mem.eq_refl|by apply Acc.eq_refl]. } Qed. Lemma update_rets_access_sound : forall v ret_opt, aeqm1 (RunAccess.update_rets Strong cn (DomAbs.powProc_of_val v) ret_opt). Proof. unfold RunAccess.update_rets; i. apply bind_val1 with (Ht:=PowLoc.zb_eq). - i. by apply mem_wupdate_access_sound. - mor. apply SMProcLoc_map_mor. + intros ? ? ?; subst. by apply Loc.eq_refl. + by apply PowProc.eq_refl. - destruct ret_opt. + by apply eval_lv_access_sound. + by apply aeqv_3. Qed. Lemma run_access_sound : aeqm1 (run_access Strong g cn cmd). Proof. unfold run_access, RunAccess.run. destruct cmd. - destruct lv, lh, o ; try (apply bind_val1 with (Ht:=PowLoc.zb_eq) ; [|by mor|by apply eval_lv_access_sound] ; i; apply bind_val1 with (Ht:=Val.zb_eq) ; [ by apply mem_wupdate_access_sound | by mor | by apply eval_access_sound ]). apply bind_val1 with (Ht:=Val.zb_eq). * by apply mem_update_access_sound. * by apply mem_update_mor. * by apply eval_access_sound. - by apply set_ext_allocsite_access_sound. - apply bind_val1 with (Ht:=PowLoc.zb_eq). + i; apply bind_val1 with (Ht:=Val.zb_eq). * i; by apply mem_wupdate_access_sound. * by apply mem_wupdate_mor. * by apply eval_alloc_access_sound. + intros k1 k2 Hk m1 m2 Hm; apply bind_mor with (Hteq:=Val.zb_eq). * by apply eval_alloc_mor. * intros v1 v2 Hv; by apply mem_wupdate_mor. + by apply eval_lv_access_sound. - apply bind_val1 with (Ht:=PowLoc.zb_eq). + i; apply bind_mem1. * by apply mem_wupdate_access_sound. * apply mem_wupdate_mor; [by apply PowLoc.eq_refl|by apply Val.eq_refl]. * by apply mem_wupdate_access_sound. + intros l1 l2 Hl m1 m2 Hm. apply bind_mor with (Hteq:=Mem.zb_eq). * apply mem_wupdate_mor ; [by apply PowLoc.eq_refl|by apply Val.eq_refl|by auto]. * intros m1' m2' Hm'. apply mem_wupdate_mor; [by auto|by apply Val.eq_refl|by auto]. + by apply eval_lv_access_sound. - apply bind_val1 with (Ht:=PowLoc.zb_eq). + i; by apply mem_wupdate_access_sound. + intros l1 l2 Hl m1 m2 Hm. apply mem_wupdate_mor; [by auto|by apply Val.eq_refl|by auto]. + by apply eval_lv_access_sound. - by apply prune_access_sound. - apply bind_val1 with (Ht:=list_val_zb_eq). + destruct (G.is_undef_e f g). * i. by apply run_undef_funcs_access_sound. * i. apply bind_val1 with (Ht:=Val.zb_eq). { i; apply bind_mem1. { apply weak_big_join_access_sound ; [ i; by apply bind_args_access_sound | i; apply bind_args_mor ; [by apply (DLat.zb_equiv_refl list_val_zb_eq)|by auto] ]. } { intros ? ? ?; apply weak_big_join_mor ; [ by apply bind_args_mor, (DLat.zb_equiv_refl list_val_zb_eq) | by apply PowProc.eq_refl | by apply ret_mor ]. } { by apply update_rets_access_sound. } } { intros v1 v2 Hv m1 m2 Hm. apply bind_mor with (Hteq:=Mem.zb_eq). { apply update_rets_mor ; [by apply pow_proc_of_val_mor|by auto|by auto]. } { intros ? ? ?; apply weak_big_join_mor ; [ by apply bind_args_mor, (DLat.zb_equiv_refl list_val_zb_eq) | by apply pow_proc_of_val_mor | by apply ret_mor ]. } } { by apply eval_access_sound. } + intros v1 v2 Hv m1 m2 Hm. destruct (G.is_undef_e f g). * by apply run_undef_funcs_mor. * apply bind_mor with (Hteq:=Val.zb_eq). { by apply eval_mor. } { intros v1' v2' Hv'. eapply bind_mor with (Hteq:=Mem.zb_eq). { apply update_rets_mor ; [by apply pow_proc_of_val_mor|by auto|by auto]. } { intros m1' m2' Hm'. apply weak_big_join_mor ; [ by apply bind_args_mor | by apply pow_proc_of_val_mor | by apply ret_mor ]. } } + by apply eval_list_access_sound. - destruct ret_opt. + apply bind_val1 with (Ht:=Val.zb_eq). { i. apply bind_val1 with (Ht:=Val.zb_eq). { i. by apply mem_wupdate_access_sound. } { intros v1 v2 Hv m1 m2 Hm. apply mem_wupdate_mor ; [by apply SemEval.deref_of_val_mor|by apply Val.eq_refl|by auto]. } { by apply mem_lookup_access_sound. } } { intros v1 v2 Hv m1 m2 Hm. apply bind_mor with (Hteq:= Val.zb_eq). { by apply mem_lookup_mor. } { intros v1' v2' Hv'; apply mem_wupdate_mor ; [by apply SemEval.deref_of_val_mor|by auto|by auto]. } } { by apply eval_access_sound. } + apply ret_mem1; i; by apply Mem.eq_refl. - apply ret_mem1. i; by apply Mem.eq_refl. - apply ret_mem1. i; by apply Mem.eq_refl. Qed. End Env.