From iris_c.c_translation Require Export translation. From iris.algebra Require Import frac. From iris_c.vcgen Require Import denv. Section vcg. Context `{amonadG Σ}. (** `mapsto_wand_list E [l1:=v1,l2:=v2,...ln:=vn] Φ` = `l1 ↦C v1 -∗ l2 ↦C v2 -∗ ... -∗ ln ↦C vn -∗ Φ` *) Fixpoint mapsto_wand_list_aux (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ := match m with | [] => Φ | None :: m' => mapsto_wand_list_aux E m' Φ (S i) | Some (DenvItem x q dv) :: m' => dloc_interp E (dLoc i 0) ↦C[x]{q} dval_interp E dv -∗ mapsto_wand_list_aux E m' Φ (S i) end%I. Definition mapsto_wand_list (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ := mapsto_wand_list_aux E m Φ O. Global Arguments mapsto_wand_list _ !_ /. Definition popstack (ms : list denv) : option (list denv * denv) := match ms with | [] => None | m :: ms => Some (ms, m) end. Global Arguments popstack !_ /. (** Evaluation of simple expressions *) Fixpoint vcg_eval_dexpr (de : dexpr) : option dval := match de with | dEVal dv => Some dv | dEVar x => None | dEPair de1 de2 => dv1 ← vcg_eval_dexpr de1; dv2 ← vcg_eval_dexpr de2; Some (dPairV dv1 dv2) | dEFst de => dv ← vcg_eval_dexpr de; match dv with | dPairV dv1 _ => Some dv1 | _ => None end | dESnd de => dv ← vcg_eval_dexpr de; match dv with | dPairV _ dv2 => Some dv2 | _ => None end | dEUnknown _ => None end. (** Computes the framing for the resources, necessary for the safety of the expression, and simulatenously computes the strongest postcondition based on that. See `vcg_sp_correct` and `vcg_sp'_correct`. *) Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr) (n: nat) { struct n }: option (list denv * denv * dval) := match de, n with | dCRet de, _ => dv ← vcg_eval_dexpr de; Some (ms, [], dv) | dCBind x de1 de2, S p => ''(ms1, mNew1, dv1) ← vcg_sp E ms de1 p; ''(ms2, mNew2, dv2) ← vcg_sp E (mNew1 :: ms1) (dce_subst E x dv1 de2) p; ''(ms3, mNew3) ← popstack ms2; Some (ms3, denv_merge mNew2 mNew3, dv2) | dCLoad de1, S p => ''(ms1, mNew, dl) ← vcg_sp E ms de1 p; i ← is_dloc E dl; ''(ms2, mNew2, q, dv) ← denv_delete_frac_2 i ms1 mNew; Some (ms2, denv_insert i ULvl q dv mNew2, dv) | dCStore de1 de2, S p => ''(ms1, mNew1, dl) ← vcg_sp E ms de1 p; i ← is_dloc E dl; ''(ms2, mNew2, dv) ← vcg_sp E ms1 de2 p; ''(ms3, mNew3, _) ← denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2); Some (ms3, denv_insert i LLvl 1 dv mNew3, dv) | dCBinOp op de1 de2, S p => ''(ms1, mNew1, dv1) ← vcg_sp E ms de1 p; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2 p; dv ← dcbin_op_eval E op dv1 dv2; Some (ms2, denv_merge mNew1 mNew2, dv) | dCPreBinOp op de1 de2, S p => ''(ms1, mNew1, dl) ← vcg_sp E ms de1 p; i ← is_dloc E dl; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2 p; ''(ms3, mNew3, dv) ← denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2); dv3 ← dcbin_op_eval E op dv dv2; Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv) | dCUnOp op de, S p => ''(ms1, mNew1, dv) ← vcg_sp E ms de p ; dv' ← dun_op_eval E op dv; Some (ms1, mNew1, dv') | dCSeq de1 de2, S p => ''(ms1, mNew1, _) ← vcg_sp E ms de1 p; ''(ms2, mNew2, dv2) ← vcg_sp E (denv_unlock mNew1 :: ms1) de2 p; ''(ms3, mNew3) ← popstack ms2; Some (ms3, denv_merge mNew2 mNew3, dv2) | dCPar de1 de2, S p => ''(ms1, mNew1, dv1) ← vcg_sp E ms de1 p; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2 p; Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2)) | dCAlloc _ _, _ | dCUnknown _, _ | dCInvoke _ _, _ => None | _, O => None end. Definition vcg_sp' (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) := ''(ms,mNew,dv) ← vcg_sp E [m] de 1024 (*TODO: add some better measure than a constant :) *); ''(_, m') ← popstack ms; Some (m', mNew, dv). Global Arguments vcg_sp' _ _ !_ /. Definition vcg_wp_continuation (E: known_locs) (Φ : known_locs → denv → dval → iProp Σ) : val → iProp Σ := λ v, (∃ E' dv m', ⌜ v = dval_interp E' dv ⌝ ∧ ⌜ E `prefix_of` E' ⌝ ∧ ⌜ denv_wf E' m'⌝ ∧ ⌜ dval_wf E' dv ⌝ ∧ denv_interp E' m' ∗ Φ E' m' dv)%I. Definition vcg_wp_awp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)). Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dval_to_nat dv1 with | Some n => mapsto_wand_list E m ( ∀ l, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l))%I | None => mapsto_wand_list E m (∃ n : nat, ⌜ dval_interp E dv1 = #n ⌝ ∧ ∀ l, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l))%I end. Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match is_dloc E dv with | Some i => match denv_lookup i m with | Some (_, dw) => Φ E m dw | None => mapsto_wand_list E m (∃ q v, dloc_interp E (dLoc i 0) ↦C{q} v ∗ (dloc_interp E (dLoc i 0) ↦C[ULvl]{q} dval_interp E (dValUnknown v) -∗ vcg_wp_continuation E Φ v)) end | None => mapsto_wand_list E m (∃ (cl : cloc) q v, ⌜dval_interp E dv = cloc_to_val cl⌝ ∧ cl ↦C{q} v ∗ (cl ↦C{q} v -∗ vcg_wp_continuation E Φ v))%I end%I. Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match is_dloc E dv1 with | Some i => match denv_delete_full i m with | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2 | None => mapsto_wand_list E m (∃ v : val, dloc_interp E (dLoc i 0) ↦C v ∗ (dloc_interp E (dLoc i 0) ↦C[LLvl] dval_interp E dv2 -∗ vcg_wp_continuation E Φ (dval_interp E dv2))) end | None => mapsto_wand_list E m (∃ (cl : cloc) (v : val), ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∧ cl ↦C v ∗ (cl ↦C[LLvl] dval_interp E dv2 -∗ vcg_wp_continuation E Φ (dval_interp E dv2)))%I end%I. (* DF: the handling of pointer operations is uniform wrt other binary operations, but it doesnt work very well because of the deep embedding of cbin_op_eval *) Definition vcg_wp_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dcbin_op_eval E op dv1 dv2 with | Some dw => Φ E m dw | None => mapsto_wand_list E m (∃ v, ⌜ cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some v ⌝ ∧ vcg_wp_continuation E Φ v) end%I. Definition vcg_wp_un_op (E : known_locs) (op : un_op) (dv : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dun_op_eval E op dv with | Some dw => Φ E m dw | None => mapsto_wand_list E m (∃ w, ⌜un_op_eval op (dval_interp E dv) = Some w⌝ ∧ vcg_wp_continuation E Φ w) end%I. Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match is_dloc E dv1 with | Some i => match denv_delete_full i m with | Some (m', dw) => match dcbin_op_eval E op dw dv2 with | Some dw' => Φ E (denv_insert i LLvl 1 dw' m') dw | None => mapsto_wand_list E m' \$ ∃ w', ⌜ cbin_op_eval op (dval_interp E dw) (dval_interp E dv2) = Some w'⌝ ∧ (dloc_interp E (dLoc i 0) ↦C[LLvl] w' -∗ vcg_wp_continuation E Φ (dval_interp E dw)) end | None => mapsto_wand_list E m (∃ v w : val, dloc_interp E (dLoc i 0) ↦C v ∗ ⌜ cbin_op_eval op v (dval_interp E dv2) = Some w ⌝ ∗ (dloc_interp E (dLoc i 0) ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v)) end | None => mapsto_wand_list E m (∃ (cl : cloc) (v w : val), ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∗ cl ↦C v ∗ ⌜cbin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ (cl ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v)) end%I. Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr) (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) (n: nat) {struct n}: iProp Σ := match de, n with | dCRet de', _ => match vcg_eval_dexpr de' with | Some dv => Φ E m dv | None => vcg_wp_awp_continuation R E de m Φ end | dCBind x de1 de2, S p => vcg_wp E m de1 R (λ E m' dv1, vcg_wp E m' (dce_subst E x dv1 de2) R Φ p) p | dCAlloc de1 de2, S p => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => vcg_wp E m' de2 R (λ E m'' dv2, vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p | None => match vcg_sp' E m de2 with | Some (m', mNew, dv2) => vcg_wp E m' de1 R (λ E m'' dv1, vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p | None => vcg_wp_awp_continuation R E de m Φ end end | dCLoad de1, S p => vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ) p | dCStore de1 de2, S p => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => vcg_wp E m' de2 R (λ E m'' dv2, vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p | None => match vcg_sp' E m de2 with | Some (m', mNew, dv2) => vcg_wp E m' de1 R (λ E m'' dv1, vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p | None => vcg_wp_awp_continuation R E de m Φ end end | dCBinOp op de1 de2, S p => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => vcg_wp E m' de2 R (λ E m'' dv2, vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p | None => match vcg_sp' E m de2 with | Some (m', mNew, dv2) => vcg_wp E m' de1 R (λ E m'' dv1, vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p | None => vcg_wp_awp_continuation R E de m Φ end end | dCPreBinOp op de1 de2, S p => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => vcg_wp E m' de2 R (λ E m'' dv2, vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p | None => match vcg_sp' E m de2 with | Some (m', mNew, dv2) => vcg_wp E m' de1 R (λ E m'' dv1, vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p | None => vcg_wp_awp_continuation R E de m Φ end end | dCUnOp op de, S p => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ) p | dCSeq de1 de2, S p => vcg_wp E m de1 R (λ E m _, U (vcg_wp E (denv_unlock m) de2 R Φ p)) p | dCPar de1 de2, S p => match vcg_sp' E m de1 with | Some (m', mNew, dv1) => vcg_wp E m' de2 R (λ E m'' dv2, (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p | None => match vcg_sp' E m de2 with | Some (m', mNew, dv2) => vcg_wp E m' de1 R (λ E m'' dv1, (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p | None => vcg_wp_awp_continuation R E de m Φ end end | dCInvoke ef de1, S p => vcg_wp E m de1 R (λ E m dv, vcg_wp_awp_continuation R E (dCUnknown (W.ClosedExpr (ef (dval_interp E dv)))) m Φ) p | _, S p => vcg_wp_awp_continuation R E de m Φ | _, O => ⌜False⌝ end%I. End vcg. Section vcg_spec. Context `{amonadG Σ}. Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) : mapsto_wand_list_aux E m Φ k -∗ ([∗ list] n↦dio ∈ m, from_option (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |}, dloc_interp E (dLoc (k + n) 0) ↦C[lv]{q} dval_interp E dv) True dio) -∗ Φ. Proof. iIntros "H". iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto. - iIntros "[H1 H2]". rewrite -plus_n_O. iSpecialize ("H" with "H1"). iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2"). iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega. - iIntros "[_ H2]". iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2"). iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega. Qed. Lemma mapsto_wand_list_spec E m Φ : mapsto_wand_list E m Φ -∗ denv_interp E m -∗ Φ. Proof. unfold mapsto_wand_list, denv_interp. iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2"). Qed. Lemma vcg_sp_length E de ms ms' mNew dv n: vcg_sp E ms de n = Some (ms', mNew, dv) → length ms = length ms'. Proof. revert ms ms' mNew dv de. induction n. (*Base case*) - intros ms ms' mNew dv de Hsp. destruct de; by simplify_option_eq. (*Induction case*) - intros ms ms' mNew dv de Hsp; destruct (vcg_sp E ms de (S n)) as [[[ms1 mNew1] dv1]|] eqn:Hout. destruct de; simplify_eq /=; try by simplify_option_eq. + (*bind case*) destruct (vcg_sp E ms de1 n) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. destruct ms2; simplify_eq/=. transitivity (length ms1). * by eapply IHn. * apply IHn in Hde2; by simplify_eq/=. + destruct (vcg_sp E ms de n) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=. transitivity (length ms1). * by eapply IHn. * by eapply denv_delete_frac_2_length. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. transitivity (length ms1). * by eapply IHn. * transitivity (length ms2). by eapply IHn. by eapply denv_delete_full_2_length. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. transitivity (length ms1); eauto. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. transitivity (length ms1); eauto. transitivity (length ms2); eauto using denv_delete_full_2_length. + destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=. destruct (dun_op_eval E u dv1); simplify_eq/=. by eapply IHn. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. destruct ms2; simplify_eq/=. transitivity (length ms1). * by eapply IHn. * apply IHn in Hde2; by simplify_eq/=. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. transitivity (length ms1); eauto. + done. Qed. Lemma vcg_eval_dexpr_wf E de dv : vcg_eval_dexpr de = Some dv → dexpr_wf [] E de → dval_wf E dv. Proof. generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=; eauto. - simplify_option_eq. naive_solver. - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=. destruct dv'; simplify_eq/=. intros Hwfde. specialize (IHde (dPairV dv dv'2) eq_refl Hwfde). (* THIS IS UGLY AF ^ *) simpl in IHde. destruct_and!. auto. - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=. destruct dv'; simplify_eq/=. intros Hwfde. specialize (IHde (dPairV dv'1 dv) eq_refl Hwfde). (* THIS IS UGLY AF ^ *) simpl in IHde. destruct_and!. auto. Qed. Lemma vcg_sp_wf' E de ms ms' mNew dv n: Forall (denv_wf E) ms → dcexpr_wf [] E de → vcg_sp E ms de n = Some (ms', mNew, dv) → Forall (denv_wf E) ms' ∧ denv_wf E mNew ∧ dval_wf E dv . Proof. revert de ms ms' mNew dv. induction n as [|n IH]; intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto. { destruct de; simplify_option_eq. repeat split_and; eauto. by eapply vcg_eval_dexpr_wf. } destruct de; simplify_eq /=. - simplify_option_eq. repeat split_and; eauto. by eapply vcg_eval_dexpr_wf. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2)) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. destruct ms2 as [|t ms2]; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). assert (Forall (denv_wf E) (mNew1 :: ms1)) as Hwfms2. { apply Forall_cons. split; eauto. } assert (dcexpr_wf [] E (dce_subst E s dv1 de2)) as Hwfsubst. by apply dce_subst_dcexpr_wf. destruct (IH (dce_subst E s dv1 de2) _ _ _ _ Hwfms2 Hwfsubst Hsp2) as (Hall&?&?). apply Forall_cons in Hall. destruct Hall. repeat split; eauto using denv_wf_merge. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=. destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?). eapply denv_wf_delete_frac_2 in Hout1; eauto. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). eapply denv_wf_delete_full_2 in Hout1; try eassumption. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert. eauto using denv_wf_merge. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). repeat split; eauto. apply denv_wf_merge; eauto. eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). eapply denv_wf_delete_full_2 in Hout1; try eassumption. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert, denv_wf_merge. eapply denv_wf_insert; eauto. eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto. by eapply denv_wf_merge. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=. repeat split; eauto. eapply dun_op_eval_Some_wf; eauto. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. destruct ms2 as [|t ms2]; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2. { apply Forall_cons. split; eauto. by apply denv_wf_unlock. } destruct (IH de2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?). apply Forall_cons in Hall. destruct Hall. repeat split; eauto using denv_wf_merge. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). repeat split; eauto. apply denv_wf_merge; eauto. Qed. Lemma vcg_sp'_wf E de m m' mNew dv : denv_wf E m → dcexpr_wf [] E de → vcg_sp' E m de = Some (m', mNew, dv) → denv_wf E m' ∧ denv_wf E mNew ∧ dval_wf E dv. Proof. rewrite /vcg_sp'. intros Hm Hde Hsp'. assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto). destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq. destruct ms as [|?m' ms]; simplify_eq. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen). simpl in Hsp'. inversion Hsp'. subst. destruct (vcg_sp_wf' E de [m] [m'] mNew _ _ Hms Hde Hsp) as (Hm'&?&?). repeat split; eauto. by inversion Hm'. Qed. Lemma vcg_eval_dexpr_correct E de dv : vcg_eval_dexpr de = Some dv → WP dexpr_interp E de {{ v, ⌜v = dval_interp E dv⌝ }}%I. Proof. generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=. - by iApply wp_value. - simplify_option_eq. wp_bind (dexpr_interp E de2). iApply wp_wand; first by iApply IHde2. iIntros (? ->). wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1. iIntros (? ->). by iApply wp_value. - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=. destruct dv'; simplify_eq/=. wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde. iIntros (? ->). simpl. by wp_proj. - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=. destruct dv'; simplify_eq/=. wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde. iIntros (? ->). simpl. by wp_proj. Qed. Lemma vcg_sp_correct' E de ms ms' mNew dv R n : vcg_sp E ms de n = Some (ms', mNew, dv) → Forall (denv_wf E) ms → dcexpr_wf [] E de → (denv_stack_interp ms ms' E (awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew)))%I. Proof. revert de ms ms' mNew dv. induction n as [|n IH]. (* Base Case *) { iIntros (de ms ms' mNew dv Hsp Hwfms Hwf); simplify_eq/=. destruct de; simplify_option_eq. iApply denv_stack_interp_intro. iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct. iIntros (? ->). iSplit; eauto. rewrite /denv_interp //. } { iIntros (de ms ms' mNew dv Hsp Hwfms Hwf). destruct de; simplify_option_eq. - iApply denv_stack_interp_intro; iApply awp_ret; iApply wp_wand; first by iApply vcg_eval_dexpr_correct. iIntros (? ->). iSplit; eauto. rewrite /denv_interp //. - destruct (vcg_sp E ms de1 n) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=. unfold popstack in Hsp. destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=. apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. iPoseProof (IH de1 ms) as "Hawp1"; eauto. assert (Forall (denv_wf E) ms1 ∧ denv_wf E mNew1 ∧ dval_wf E dv1). { eapply vcg_sp_wf'; eauto. } destruct_and!. assert (Forall (denv_wf E) (mNew1 :: ms1)). { econstructor; eauto. } assert (Forall (denv_wf E) (t :: ms') ∧ denv_wf E mNew2 ∧ dval_wf E dv). { eapply (vcg_sp_wf' _ (dce_subst E s dv1 de2)); eauto. apply dce_subst_dcexpr_wf; eauto. } iPoseProof (IH (dce_subst E s dv1 de2) (mNew1 :: ms1)) as "Hawp2"; eauto. { apply dce_subst_dcexpr_wf; eauto. } iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp". iClear "Hawp1 Hawp2". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]". assert (Closed ( [s]) (dcexpr_interp E de2)). { apply dcexpr_closed. apply Hwf2. } iApply awp_bind. * exists (λ: s, dcexpr_interp E de2)%V. by unlock. * iApply (awp_wand with "Hawp1"). iIntros (v) "[% HmNew1]". simplify_eq/=. iClear "Hawp". iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]". awp_let. rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto. rewrite- denv_merge_interp. iFrame. - destruct (vcg_sp E ms de n) as [[[ms1 mNew1] dv1]|] eqn:Hsp'; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=. specialize (IH de ms). iPoseProof IH as "Hawp"; eauto. iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption. iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'". iClear "Hawp Hm". iApply (denv_stack_interp_mono with "Hawp'"). iIntros "[Hawp Hm]". iApply a_load_spec. iApply (awp_wand with "Hawp"). iIntros (?) "[% HmNew1]". simplify_eq/=. iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmNew1") as "[HmNew2 \$]". iIntros "Hl". iSplit; eauto. rewrite -denv_insert_interp. by iFrame. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv3] |] eqn:Hfar; simplify_eq/=. iPoseProof (IH de1) as "Hawp1"; destruct_and!; eauto. iPoseProof (IH de2) as "Hawp2"; eauto. { eapply (vcg_sp_wf' _ de1); eauto. } iPoseProof denv_delete_full_2_interp as "Hl"; first done. iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'". iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp". iClear "Hawp1 Hawp2 Hl Hawp'". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[[Hawp1 Hawp2] Hl]". iApply (a_store_spec with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=. iExists _, _; iSplit; eauto. iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp -denv_insert_interp. iDestruct ("Hl" with "HmNew") as "[HmNew3 \$]". iIntros "Hl". by iFrame. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=; destruct_and!. iPoseProof (IH de1 ms) as "Hawp1"; eauto. iPoseProof (IH de2 ms1) as "Hawp2"; eauto. { eapply (vcg_sp_wf' _ de1); eauto. } iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp". iClear "Hawp1 Hawp2". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]". iApply (a_bin_op_spec with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=. iExists (dval_interp E dv). repeat iSplit; eauto. + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe. + rewrite -denv_merge_interp. iFrame. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=. destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=; destruct_and!. iPoseProof (IH de1 ms) as "Hawp1"; try done. iPoseProof (IH de2 ms1) as "Hawp2"; eauto. { eapply (vcg_sp_wf' _ de1); eauto. } iPoseProof denv_delete_full_2_interp as "Hl"; first done. iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'". iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp". iClear "Hawp1 Hawp2 Hawp' Hl". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[[Hawp1 Hawp2] Hl]". iApply (a_pre_bin_op_spec with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] HR"; simplify_eq/=. iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp. iExists (dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d). iDestruct ("Hl" with "HmNew") as "[HmNew \$]". repeat iSplit; eauto. + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe. + iIntros "Hl". iFrame. iSplit; first done. rewrite -denv_insert_interp. by iFrame. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=. iPoseProof (IH de ms) as "Hawp"; try done. iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp". iIntros "Hawp". iApply a_un_op_spec. iApply (awp_wand with "Hawp"). iIntros (v) "[% H]". simplify_eq/=. iExists (dval_interp E dv). repeat iSplit; eauto. iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (vcg_sp E _ de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=; destruct_and!. iPoseProof (IH de1 ms) as "Hawp1"; eauto. iPoseProof (IH de2 (denv_unlock mNew1 :: ms1)) as "Hawp2"; eauto. { econstructor; [eapply denv_wf_unlock |]; eapply (vcg_sp_wf' _ de1); eauto. } unfold popstack in Hsp. destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=. iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp". iClear "Hawp1 Hawp2". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]". iApply a_sequence_spec'. { by apply dcexpr_closed. } iApply (awp_wand with "Hawp1"). iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp". rewrite (denv_unlock_interp E mNew1). iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]". iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]". rewrite -denv_merge_interp. iSplit; eauto with iFrame. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=; destruct_and!. iPoseProof (IH de1) as "Hawp1"; try done. iPoseProof (IH de2) as "Hawp2"; eauto. { eapply (vcg_sp_wf' _ de1); eauto. } iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp". iClear "Hawp1 Hawp2". iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]". iApply (awp_par with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>"; simplify_eq/=; iSplit; eauto. rewrite -denv_merge_interp. iFrame. } Qed. Lemma vcg_sp_correct E de m ms mNew dv R n: vcg_sp E [m] de n = Some (ms, mNew, dv) → denv_wf E m → dcexpr_wf [] E de → denv_interp E m -∗ denv_interp E (denv_stack_merge ms) ∗ awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew). Proof. iIntros (Hsp Hwfm Hwf) "Hm". iPoseProof vcg_sp_correct' as "Hawp"; eauto. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen; assert (∃ m', ms = [m']) as [m' ->]=>/=. { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. } rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[\$ \$]". Qed. Lemma vcg_sp'_correct E de m m' mNew dv R : vcg_sp' E m de = Some (m', mNew, dv) → denv_wf E m → dcexpr_wf [] E de → denv_interp E m -∗ denv_interp E m' ∗ awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew). Proof. rewrite /vcg_sp'. iIntros (Hsp' Hwfm Hwf) "Hm". destruct (vcg_sp E [m] de 1024) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq. destruct ms as [|?m' ms]; simplify_eq. pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen. assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen); simplify_eq. rewrite vcg_sp_correct; eauto. simpl. rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=. by iFrame. Qed. Lemma vcg_wp_awp_continuation_correct R E m de Φ : denv_wf E m → denv_interp E m -∗ vcg_wp_awp_continuation R E de m Φ -∗ awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ). Proof. rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm"). iApply (awp_wand with "Hwp"). iIntros (v) "H". iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)". iExists E', dv, m'. repeat (iSplit; first done); iFrame. Qed. Lemma vcg_wp_load_correct E m dv Φ : denv_wf E m → denv_interp E m -∗ vcg_wp_load E dv m Φ -∗ ∃ (cl : cloc) q w, ⌜dval_interp E dv = cloc_to_val cl⌝ ∧ cl ↦C{q} w ∗ (cl ↦C{q} w -∗ vcg_wp_continuation E Φ w). Proof. rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc. - destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=. + destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption. rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_Some in Hdloc. simplify_eq/=. iExists (dloc_interp E (dLoc i 0)), q, (dval_interp E dv'); iSplit; first done. iFrame. iIntros "Hl". iExists E, dv', m; repeat (iSplit; first done). iFrame. rewrite Hm0. eapply denv_lookup_wf in Hlkp; eauto with iFrame. + rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm"). simpl. iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_Some in Hdloc. subst. iExists (dloc_interp E (dLoc i 0)), q, v'; iSplit; first done. iFrame. - rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm"); simpl. iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]". iExists l, q, v'. iSplit; first done. iFrame. Qed. Lemma vcg_wp_un_op_correct E m dv b Φ : dval_wf E dv → denv_wf E m → denv_interp E m -∗ vcg_wp_un_op E b dv m Φ -∗ ∃ w : val, ⌜un_op_eval b (dval_interp E dv) = Some w⌝ ∧ vcg_wp_continuation E Φ w. Proof. iIntros (Hwf Hwf2) "Hm Hwp". rewrite /vcg_wp_un_op. destruct (dun_op_eval E b dv) as [dw|] eqn:Hbin. - iExists (dval_interp E dw); iSplit. { iPureIntro. apply dun_op_eval_correct. by rewrite Hbin. } iExists E, dw, m. apply dun_op_eval_Some_wf in Hbin; try done. eauto with iFrame. - rewrite mapsto_wand_list_spec. iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto. Qed. Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ : E0 `prefix_of` E → dval_wf E dv1 → dval_wf E dv2 → denv_wf E (denv_merge mOut m) → denv_interp E m -∗ vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -∗ denv_interp E mOut -∗ ∃ w : val, ⌜cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w⌝ ∧ vcg_wp_continuation E Φ w. Proof. iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op. destruct (dcbin_op_eval E b dv1 dv2) as [dw|] eqn:Hbin. - iExists (dval_interp E dw); iSplit. { iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. } iExists E, dw, (denv_merge mOut m). apply dcbin_op_eval_Some_wf in Hbin; try done. rewrite -denv_merge_interp //. eauto with iFrame. - iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp. rewrite mapsto_wand_list_spec. iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto. Qed. Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ : denv_wf E m → dval_wf E dv2 → denv_interp E m -∗ vcg_wp_pre_bin_op E op dv1 dv2 m Φ -∗ ∃ l v w, l ↦C v ∗ ⌜dval_interp E dv1 = cloc_to_val l⌝ ∗ ⌜cbin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ (l ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v). Proof. iIntros (? ?) "Hm Hwp". rewrite /vcg_wp_pre_bin_op. destruct (is_dloc E dv1) as [i|] eqn:Hloc; last first. { rewrite mapsto_wand_list_spec. iDestruct ("Hwp" with "Hm") as (l v w) "(%&Hl&%&Hwp)". iExists l,v,w. iFrame. eauto. } apply is_dloc_Some in Hloc. simplify_eq/=. destruct (denv_delete_full i m) as [[m' dw] | ] eqn:Hdel; last first. - rewrite mapsto_wand_list_spec. iDestruct ("Hwp" with "Hm") as (v w) "(Hl&%&Hwp)". iExists (dloc_interp E (dLoc i 0)),v,w. iFrame. eauto. - iDestruct (denv_delete_full_interp E with "Hm") as "[Hm' Hl]"; first eassumption. destruct (dcbin_op_eval E op dw dv2) as [dw'|] eqn:Hop. { iExists (dloc_interp E (dLoc i 0)), (dval_interp E dw), (dval_interp E dw'). iFrame "Hl". repeat iSplit; eauto; try iPureIntro. - apply dcbin_op_eval_correct. by rewrite Hop. - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp. rewrite /vcg_wp_continuation. iExists E,dw,_. iFrame. eapply denv_wf_delete_full in Hdel; eauto. destruct_and!. apply dcbin_op_eval_Some_wf in Hop; eauto. repeat iSplit; eauto. iPureIntro. eapply denv_wf_insert; eauto. } rewrite mapsto_wand_list_spec. iDestruct ("Hwp" with "Hm'") as (w' ?) "Hwp". iExists (dloc_interp E (dLoc i 0)), (dval_interp E dw), w'. iFrame; eauto. Qed. Lemma vcg_wp_alloc_correct E m dv1 dv2 Φ : denv_interp E m -∗ vcg_wp_alloc E dv1 dv2 m Φ -∗ ∃ n : nat, ⌜dval_interp E dv1 = #n⌝ ∧ (∀ l : cloc, l ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val l)). Proof. iIntros "Hm Hwp". rewrite /vcg_wp_alloc. destruct (dval_to_nat dv1) as [n|] eqn:Hdv1. - iExists n. iSplit. iPureIntro; by apply dval_to_nat_correct. rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). - rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). Qed. Lemma vcg_wp_store_correct E m dv1 dv2 Φ : denv_wf E m → dval_wf E dv2 → denv_interp E m -∗ vcg_wp_store E dv1 dv2 m Φ -∗ ∃ (cl : cloc) (w : val), ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] dval_interp E dv2 -∗ vcg_wp_continuation E Φ (dval_interp E dv2)). Proof. iIntros (Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp. destruct (is_dloc E dv1) as [i|] eqn:Hdloc. - apply is_dloc_Some in Hdloc; rewrite Hdloc. destruct (denv_delete_full i m) as [[m' dv_old]|] eqn:Hdel. + iExists (dloc_interp E (dLoc i 0)), (dval_interp E dv_old); iSplit; first done. iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption. iSpecialize ("Hdel" with "Hm"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame. iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done). iSplit. iPureIntro. apply denv_wf_insert; eauto; apply (denv_wf_delete_full E dv_old i m m' Hwf Hdel). rewrite -denv_insert_interp. eauto with iFrame. + rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[Hm]"); iFrame. iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; iExists (dloc_interp E (dLoc i 0)), dv_old; iSplit; first done. iFrame. - rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[Hm]"); iFrame. Qed. Lemma vcg_wp_continuation_mono E E' Φ w: E `prefix_of` E' → vcg_wp_continuation E' Φ w -∗ vcg_wp_continuation E Φ w. Proof. iIntros (Hpre) "Hp". iDestruct "Hp" as (E1 dv m' ? Hpre1 ?) "(% & Hm' & H)"; simplify_eq /=. iExists E1, dv, m'; repeat (iSplit; first done). iSplit. iPureIntro. by trans E'. eauto with iFrame. Qed. Lemma vcg_wp_correct R E m de Φ n: dcexpr_wf [] E de → denv_wf E m → denv_interp E m -∗ vcg_wp E m de R Φ n -∗ awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ). Proof. revert de Φ E m. induction n as [|n IH]; intros de Φ E m Hwf; iIntros (Hmwf) "Hm Hwp". { simpl; case_match; eauto with iFrame. simpl. case_match. + iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct. iIntros (? ->). iExists E,_,m. repeat iSplit; eauto with iFrame. iPureIntro. by eapply vcg_eval_dexpr_wf. + by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } destruct de; eauto with iFrame. - simpl. case_match. + iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct. iIntros (? ->). iExists E,_,m. repeat iSplit; eauto with iFrame. iPureIntro. by eapply vcg_eval_dexpr_wf. + by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. assert (Closed [s] (dcexpr_interp E de2)). { by apply dcexpr_closed. } iApply (awp_bind with "[Hm]"); fold dcexpr_interp. { exists (λ: s, dcexpr_interp E de2)%V. by unlock. } iApply (awp_wand with "Hm"). iIntros (v) "Hex". awp_let. iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". assert (dcexpr_wf [] Enew (dce_subst Enew s dv de2)) as Hwfs. { apply dce_subst_dcexpr_wf; first done. by eapply dcexpr_wf_mono. } rewrite (IH (dce_subst Enew s dv de2)) //. iSpecialize ("Hm" with "Hwp"). rewrite (dcexpr_interp_mono _ E Enew _ Hwf2 Hpre'). rewrite Hpre -dce_subst_subst_comm. iApply (awp_wand with "Hm"). iIntros (v1) "Hex". iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl. iExists Ef, dvf, mf; iSplit; first done. iSplit. iPureIntro. trans Enew ; done. iSplit; first done. iFrame. iPureIntro; done. - simpl in *. apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first. { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?). iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done. clear Heqsp2 Heqsp. iDestruct (IH de1 with "Hm' Hwp") as "Hde1"; try done. iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iDestruct 1 as (E' dw m'' -> Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". rewrite (dval_interp_mono E E') //. iCombine "HmNew Hm'" as "Hm'". rewrite (denv_interp_mono E E') // denv_merge_interp. iDestruct (vcg_wp_alloc_correct with "Hm' H") as (n' ->) "Hcont"; eauto. iExists n'; iSplit; eauto. iIntros (l) "Hl". iSpecialize ("Hcont" with "Hl"). by iApply (vcg_wp_continuation_mono with "Hcont"). + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; try done. clear Heqsp. iDestruct (IH de2 with "Hm' Hwp") as "Hde2"; try done. iApply (a_alloc_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 -> ???) "[Hm' H]". rewrite (dval_interp_mono E E') //. iCombine "HmNew Hm'" as "Hm'". rewrite (denv_interp_mono E E') // denv_merge_interp. iDestruct (vcg_wp_alloc_correct with "Hm' H") as (n' ->) "Hcont"; eauto. iExists n'; iSplit; eauto. iIntros (l) "Hl". iSpecialize ("Hcont" with "Hl"). by iApply (vcg_wp_continuation_mono with "Hcont"). - rewrite (IH de) //. iRename "Hm" into "Hawp". iSpecialize ("Hawp" with "Hwp"); simpl. iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp"). iIntros (v) "H". iDestruct "H" as (E' dv m' Heq Hwf0 Hm'wf Hwf2) "(Hm & Hwp)". iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done. iDestruct "Hload" as (l q w) "(% & Hl & Hwp)". rewrite Heq. iExists l, q, w. iSplit; first done. iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl"). iDestruct "Hwp" as (Ef dvf mf Hpre' Hwf5 Hwf3 Hwf4) "(Hmf & Hwp)". iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro. iSplit. iPureIntro. trans E'; done. done. - rewrite{1} /vcg_wp; fold vcg_wp. simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first. { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?). iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; try done. clear Heqsp2 Heqsp. iDestruct (IH de1 with "Hm' Hwp") as "Hde1"; try done. iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iDestruct 1 as (E' dw m'' ? Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]". rewrite (dval_interp_mono E E') //. subst v1. iDestruct (vcg_wp_store_correct with "[-H] H") as (l w ?) "[Hl H]"; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. { rewrite -!denv_merge_interp. iFrame "Hm'". rewrite -!(denv_interp_mono E E'); eauto. } iExists l, w. iSplit; first done. iIntros "{\$Hl} Hl". iApply vcg_wp_continuation_mono; last by iApply "H". done. + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; try done. clear Heqsp. iDestruct (IH de2 with "Hm' Hwp") as "Hde2"; try done. iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2). iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? ? ?) "(% & Hm' & H)". rewrite (dval_interp_mono E E') //. subst v2. iDestruct (vcg_wp_store_correct with "[-H] H") as (l w ?) "[Hl H]"; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. { rewrite -!denv_merge_interp. iFrame "Hm'". rewrite -!(denv_interp_mono E E'); eauto. } iExists l, w. iSplit; first done. iIntros "{\$Hl} Hl". iApply vcg_wp_continuation_mono; last by iApply "H". done. - rewrite{1} /vcg_wp; fold vcg_wp. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2]. destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first. { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]". iClear "Hsp"; clear Heqsp2 Heqsp. rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iApply (a_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "Hex (-> & HmNew)". iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. rewrite (dval_interp_mono E E' dv2); eauto. iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H"; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. { iApply (denv_interp_mono with "HmNew"); eauto. } iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono. + iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp. rewrite (IH de2); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iRename "Hm'" into "Hde2". iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "(-> & HmNew) Hex". iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H"; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. { iApply (denv_interp_mono with "HmNew"); eauto. } iExists w. rewrite (dval_interp_mono E E') //. iSplit; first done. by iApply vcg_wp_continuation_mono. - rewrite{1} /vcg_wp; fold vcg_wp. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2]. destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first. { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]". iClear "Hsp"; clear Heqsp2 Heqsp. rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iApply (a_pre_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "Hex (-> & HmNew) \$". iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. iDestruct (denv_interp_mono with "HmNew") as "HmNew"; eauto. iCombine ("HmNew Hm'") as "Hm". rewrite denv_merge_interp. iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp") as (l v w) "(Hl & % & % & Hwp)". { apply denv_wf_merge; eauto using denv_wf_mono. } { eapply dval_wf_mono; eauto. } iExists l, v, w. iFrame. repeat iSplit; eauto. * iPureIntro. rewrite (dval_interp_mono E E'); auto. * rewrite (vcg_wp_continuation_mono E E'); auto. + iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp. rewrite (IH de2); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iRename "Hm'" into "Hde2". iApply (a_pre_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "(-> & HmNew) Hex \$". iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. iDestruct (denv_interp_mono with "HmNew") as "HmNew"; eauto. iCombine ("HmNew Hm'") as "Hm". rewrite denv_merge_interp. iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp") as (l v w) "(Hl & % & % & Hwp)". { apply denv_wf_merge; eauto using denv_wf_mono. } { eapply dval_wf_mono; eauto. } iExists l, v, w. iFrame. repeat iSplit; eauto. * iPureIntro. rewrite (dval_interp_mono E E'); auto. * rewrite (vcg_wp_continuation_mono E E'); auto. - rewrite (IH de) //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp"). iApply (awp_wand with "Hm"). iIntros (v) "Hex". iDestruct "Hex" as (E' dv m' -> Hpre' Hm'wf) "(% & Hm & Hwp)". iDestruct (vcg_wp_un_op_correct with "Hm Hwp") as (w ?) "Hcont"; auto. iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono. - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2]. rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. by apply dcexpr_closed. iApply (awp_wand with "Hm"). iIntros (v) "Hex". iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl. rewrite denv_unlock_interp. iModIntro. rewrite (IH de2) //. iSpecialize ("Hm" with "Hwp"). specialize (dcexpr_interp_mono [] E Enew de2 Hwf2 Hpre'). intro Heq; rewrite Heq. iApply (awp_wand with "Hm"). iIntros (v1) "Hex". iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl. iExists Ef, dvf, mf; iSplit; first done. iSplit. iPureIntro. trans Enew ; done. iSplit; first done. iFrame. iPureIntro; done. eapply dcexpr_wf_mono in Hwf2. done. done. by apply denv_wf_unlock. - rewrite{1} /vcg_wp; fold vcg_wp. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2]. destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first. + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first. { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). } iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]". iClear "Hsp"; clear Heqsp2 Heqsp. rewrite (IH de1); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iApply (awp_par with "Hm' Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "Hex (-> & HmNew)". iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. rewrite (dval_interp_mono E E' dv2); eauto. iNext. iApply vcg_wp_continuation_mono; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. iExists E', (dPairV dv1 dv2), (denv_merge mNew m''); repeat (iSplit; try iPureIntro; simpl; eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge). iFrame. rewrite (denv_interp_mono E) //. iApply denv_merge_interp. iFrame. + iPoseProof (vcg_sp'_correct) as "Hsp"; eauto. specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?). iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp. rewrite (IH de2); [| done | done]. iSpecialize ("Hm'" with "Hwp"). iRename "Hm'" into "Hde2". iApply (awp_par with "Hde1 Hde2"); fold dcexpr_interp. iNext. iIntros (v1 v2) "(-> & HmNew) Hex !>". iDestruct "Hex" as (E' dv2 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=. rewrite (dval_interp_mono E E' dv1); eauto. iApply vcg_wp_continuation_mono; eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono. iExists E', (dPairV dv1 dv2), (denv_merge mNew m''); repeat (iSplit; try iPureIntro; simpl; eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge). iFrame. rewrite (denv_interp_mono E) //. iApply denv_merge_interp. iFrame. - simpl. rewrite (IH de) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp. iApply (a_invoke_spec with "Hm"). iIntros (arg) "Hf !> HR". iDestruct "Hf" as (E' dv1 m' Heq Hpre Hm'wf) "(% & Hm' & Hwp)". unfold vcg_wp_awp_continuation. rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm'"). simplify_eq /=. iExists R. iFrame. iApply (awp_wand with "Hwp"). iIntros (v) "Hc Hr". rewrite (vcg_wp_continuation_mono E) //. iFrame. - by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). Qed. End vcg_spec. Arguments vcg_wp_awp_continuation _ _ _ _ _ _ _ /. Arguments vcg_wp_alloc _ _ _ _ _ _ _ /. Arguments vcg_wp_load _ _ _ _ _ _ /. Arguments vcg_wp_store _ _ _ _ _ _ _ /. Arguments vcg_wp_bin_op _ _ _ _ _ _ _ _ /. Arguments vcg_wp_un_op _ _ _ _ _ _ _ /. Arguments vcg_wp_pre_bin_op _ _ _ _ _ _ _ _ /.