From iris_c.c_translation Require Export translation. From iris_c.vcgen Require Export forward. From iris_c.lib Require Import Q. Section vcg. Context `{cmonadG Σ}. Definition vcg_continuation (E: known_locs) (Φ : known_locs → denv → dval → iProp Σ) (v : val) : iProp Σ := (∃ 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_cwp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := wand_denv_interp E m (CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}). Definition vcg_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match succ_nat_of_dval dv1 with | Some di => ∀ cl, let i := length E in block_info cl true (S (Z.to_nat (dint_interp di))) -∗ (cl +∗ 1) ↦C∗ replicate (Z.to_nat (dint_interp di)) (dval_interp E dv2) -∗ Φ (E ++ [cl]) (denv_insert i ULvl 1 dv2 m) (dLocV (dLoc i (dInt 0 None))) | _ => wand_denv_interp E m (∃ n : nat, ⌜ dval_interp E dv1 = #n ⌝ ∧ ⌜ n ≠ O ⌝ ∧ ∀ cl, block_info cl true n -∗ cl ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_continuation E Φ (cloc_to_val cl)) end%I. Definition vcg_load (E : known_locs) (dv : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dloc_var_of_dval dv with | Some i => match denv_lookup i m with | Some (_, dw) => Φ E m dw | None => wand_denv_interp E m (∃ q v, dloc_var_interp E i ↦C{q} v ∗ (dloc_var_interp E i ↦C[ULvl]{q} dval_interp E (dValUnknown v) -∗ vcg_continuation E Φ v)) end | None => wand_denv_interp E m (∃ (cl : cloc) q v, ⌜dval_interp E dv = cloc_to_val cl⌝ ∧ cl ↦C{q} v ∗ (cl ↦C{q} v -∗ vcg_continuation E Φ v))%I end%I. Definition vcg_store (E : known_locs) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dloc_var_of_dval dv1 with | Some i => match denv_delete_full i m with | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2 | None => wand_denv_interp E m (∃ v : val, dloc_var_interp E i ↦C v ∗ (dloc_var_interp E i ↦C[LLvl] dval_interp E dv2 -∗ vcg_continuation E Φ (dval_interp E dv2))) end | None => wand_denv_interp 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_continuation E Φ (dval_interp E dv2)))%I end%I. Definition vcg_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 => wand_denv_interp E m (∃ v, ⌜ cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some v ⌝ ∧ vcg_continuation E Φ v) end%I. Definition vcg_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 => wand_denv_interp E m (∃ w, ⌜un_op_eval op (dval_interp E dv) = Some w⌝ ∧ vcg_continuation E Φ w) end%I. Definition vcg_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match dloc_var_of_dval 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 => wand_denv_interp E m' \$ ∃ w', ⌜ cbin_op_eval op (dval_interp E dw) (dval_interp E dv2) = Some w'⌝ ∧ (dloc_var_interp E i ↦C[LLvl] w' -∗ vcg_continuation E Φ (dval_interp E dw)) end | None => wand_denv_interp E m (∃ v w : val, dloc_var_interp E i ↦C v ∗ ⌜ cbin_op_eval op v (dval_interp E dv2) = Some w ⌝ ∗ (dloc_var_interp E i ↦C[LLvl] w -∗ vcg_continuation E Φ v)) end | None => wand_denv_interp 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_continuation E Φ v)) end%I. Definition vcg_call (E : known_locs) (dv1 dv2 : dval) (m : denv) (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := (wand_denv_interp E m \$ U ( R -∗ ▷ CWP (dval_interp E dv1) (dval_interp E dv2) {{ v, R ∗ vcg_continuation E Φ v }}))%I. Fixpoint vcg (E : known_locs) (n : nat) (m : denv) (de : dcexpr) (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match de, n with | _, O => False | dCRet de', _ => match dexpr_eval de' with | Some dv => Φ E m dv | None => vcg_cwp_continuation R E de m Φ end | dCSeqBind mx de1 de2, S n => vcg E n m de1 R \$ λ E m dv1, let i := length E in vcg E n (denv_unlock m) (dce_subst' E mx dv1 de2) R Φ | dCMutBind mx de1 de2, S n => vcg E n m de1 R \$ λ E m dv1, ∀ cl, let i := length E in let dlv := dLocV (dLoc i (dInt 0 None)) in vcg (E ++ [cl]) n (denv_insert i ULvl 1 dv1 (denv_unlock m)) (dce_subst' (E ++ [cl]) mx dlv de2) R \$ λ E m dv2, match denv_delete_full i m with | Some (m', _) => Φ E m' dv2 | _ => wand_denv_interp E m (∃ v, cl ↦C v ∗ vcg_continuation E Φ (dval_interp E dv2)) end | dCAlloc de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, vcg_alloc E dv1 dv2 (denv_merge mNew m'') Φ | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, vcg_alloc E dv1 dv2 (denv_merge mNew m'') Φ | None => vcg_cwp_continuation R E de m Φ end end | dCLoad de1, S n => vcg E n m de1 R \$ λ E m' dv, vcg_load E dv m' Φ | dCStore de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, vcg_store E dv1 dv2 (denv_merge mNew m'') Φ | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, vcg_store E dv1 dv2 (denv_merge mNew m'') Φ | None => vcg_cwp_continuation R E de m Φ end end | dCBinOp op de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, vcg_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, vcg_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ | None => vcg_cwp_continuation R E de m Φ end end | dCPreBinOp op de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, vcg_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, vcg_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ | None => vcg_cwp_continuation R E de m Φ end end | dCUnOp op de, S n => vcg E n m de R \$ λ E m dv, vcg_un_op E op dv m Φ | dCPar de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)) | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)) | None => vcg_cwp_continuation R E de m Φ end end | dCWhile de1 de2, S n => vcg_cwp_continuation R E (dCWhileV de1 de2) m Φ | dCCall de1 de2, S n => match forward E n m de1 with | Some (m', mNew, dv1) => vcg E n m' de2 R \$ λ E m'' dv2, vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ | None => match forward E n m de2 with | Some (m', mNew, dv2) => vcg E n m' de1 R \$ λ E m'' dv1, vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ | None => vcg_cwp_continuation R E de m Φ end end | _, S p => vcg_cwp_continuation R E de m Φ end%I. Definition vcg_while (E : known_locs) (n : nat) (m : denv) (de : dcexpr) (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match de with | dCWhileV de1 de2 => ▷ (vcg E n m de1 R \$ λ E m dv1, match dknown_bool_of_dval dv1 with | Some true => U (vcg E n (denv_unlock m) de2 R \$ λ E m _, U (vcg E n (denv_unlock m) (dCWhileV de1 de2) R Φ)) | Some false => U (Φ E (denv_unlock m) (dLitV dLitUnit)) | _ => wand_denv_interp E m ( ⌜dval_interp E dv1 = #true⌝ ∧ (* FIXME, make sure that computation of vcg is blocked in the continuation. *) U (vcg_continuation E (λ E m dv, vcg E n m (dCSeqBind <> de2 (dCWhileV de1 de2)) R Φ) #()) ∨ ⌜dval_interp E dv1 = #false⌝ ∧ U (vcg_continuation E Φ #())) end) | _ => vcg E n m de R Φ end%I. End vcg. Section vcg_spec. Context `{cmonadG Σ}. Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|]. Hint Extern 0 (0 < 1)%Q => reflexivity. Hint Resolve dknown_bool_of_dval_correct. Hint Resolve dloc_var_of_dval_wf dloc_var_of_dval_correct. Hint Resolve denv_wf_1_stack_pop denv_wf_2_stack_pop. Hint Resolve dun_op_eval_Some_wf dun_op_eval_correct. Hint Resolve dcbin_op_eval_Some_wf dcbin_op_eval_correct. Hint Resolve dce_subst_wf'. Hint Resolve denv_wf_dval_wf_lookup. Hint Resolve denv_wf_insert denv_wf_merge denv_wf_unlock. Hint Resolve denv_wf_delete_full denv_wf_dval_wf_delete_full. Hint Resolve denv_wf_1_delete_frac_2 denv_wf_2_delete_frac_2. Hint Resolve denv_wf_frac_wf_delete_frac_2 denv_wf_dval_wf_delete_frac_2. Hint Resolve denv_wf_1_delete_full_2 denv_wf_2_delete_full_2. Hint Resolve denv_wf_dval_wf_delete_full_2. Hint Resolve dexpr_eval_wf. Hint Resolve denv_wf_1_forward denv_wf_2_forward denv_wf_dval_wf_forward. Lemma vcg_continuation_correct Φ E m dv : denv_wf E m → dval_wf E dv → Φ E m dv -∗ denv_interp E m -∗ vcg_continuation E Φ (dval_interp E dv). Proof. iIntros (??) "H Hm". iExists E, dv, m. eauto with iFrame. Qed. Lemma vcg_continuation_mono E E' Φ w : E `prefix_of` E' → vcg_continuation E' Φ w -∗ vcg_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_cwp_continuation_correct R E m de Φ : denv_wf E m → denv_interp E m -∗ vcg_cwp_continuation R E de m Φ -∗ CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}. Proof. rewrite /vcg_cwp_continuation. iIntros (?) "Hm Hwp". by iApply (wand_denv_interp_spec with "Hwp Hm"). Qed. Lemma vcg_alloc_correct E m dv1 dv2 Φ : denv_wf E m → dval_wf E dv1 → dval_wf E dv2 → denv_interp E m -∗ vcg_alloc E dv1 dv2 m Φ -∗ ∃ n : nat, ⌜dval_interp E dv1 = #n⌝ ∧ ⌜ n ≠ O%nat ⌝ ∧ (∀ cl, block_info cl true n -∗ cl ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_continuation E Φ (cloc_to_val cl)). Proof. iIntros (???) "Hm H". rewrite /vcg_alloc. destruct (succ_nat_of_dval dv1) as [di|] eqn:?; last first. { iApply (wand_denv_interp_spec with "H Hm"). } iExists (S (Z.to_nat (dint_interp di))); simpl. iSplit; first by eauto using succ_nat_of_dval_Some. iSplit; first done. iIntros (cl) "Hinfo [Hcl Hcls]". assert (dloc_var_interp (E ++ [cl]) (length E) = cl) as Hcl. { by rewrite /dloc_var_interp (list_lookup_middle _ []). } iExists (E ++ [cl]), (dLocV (dLoc (length E) (dInt 0 None))), (denv_insert (length E) ULvl 1 dv2 m); simpl. iSplit; first by rewrite Hcl. iSplit; first by eauto using prefix_app_r. iSplit; first by eauto using denv_wf_insert_extend. iSplit. { by rewrite /dloc_wf /= /dloc_var_wf (list_lookup_middle _ []). } iSplitL "Hcl Hm"; last by iApply ("H" with "Hinfo Hcls"). iApply denv_insert_interp; eauto using denv_wf_mono, prefix_app_r. iSplitL "Hm". { iApply (denv_interp_mono with "Hm"); eauto using prefix_app_r. } rewrite Hcl -(dval_interp_mono E (E ++ [cl])); eauto using prefix_app_r. Qed. Lemma vcg_load_correct E m dv Φ : denv_wf E m → denv_interp E m -∗ vcg_load E dv m Φ -∗ ∃ cl q w, ⌜dval_interp E dv = cloc_to_val cl⌝ ∧ cl ↦C{q} w ∗ (cl ↦C{q} w -∗ vcg_continuation E Φ w). Proof. iIntros (?) "Hm H". rewrite /vcg_load. destruct (dloc_var_of_dval dv) as [i|] eqn:?; last first. { iApply (wand_denv_interp_spec with "H Hm"). } destruct (denv_lookup i m) as [[q dv'] |] eqn:?; simplify_eq /=. - destruct (denv_lookup_interp E i q dv' m) as [mf Hmf]=> //. iDestruct (Hmf with "Hm") as "[Hmf Hi]". iExists _, _, _; iFrame "Hi"; iSplit; first by eauto. iIntros "Hi". iDestruct (Hmf with "[\$Hmf \$Hi]") as "Hm". iApply (vcg_continuation_correct with "H"); eauto 10. - iDestruct (wand_denv_interp_spec with "H Hm") as (q v) "[Hi H]". iExists _, _, _; iFrame; eauto. Qed. Lemma vcg_store_correct E m dv1 dv2 Φ : denv_wf E m → dval_wf E dv1 → dval_wf E dv2 → denv_interp E m -∗ vcg_store E dv1 dv2 m Φ -∗ ∃ cl w, ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] dval_interp E dv2 -∗ vcg_continuation E Φ (dval_interp E dv2)). Proof. iIntros (???) "Hm H". rewrite /vcg_store. destruct (dloc_var_of_dval dv1) as [i|] eqn:?; last first. { iApply (wand_denv_interp_spec with "H Hm"). } destruct (denv_delete_full i m) as [[m' dv_old]|] eqn:?; simplify_eq/=. - iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hi]"; eauto. iExists _, _; iFrame "Hi"; iSplit; first by eauto. iIntros "Hi". iApply (vcg_continuation_correct with "H"); eauto. iApply denv_insert_interp; eauto with iFrame. - iDestruct (wand_denv_interp_spec with "H Hm") as (w) "[Hi H]". iExists _, _; iFrame "Hi"; eauto. Qed. Lemma vcg_bin_op_correct E m dv1 dv2 op Φ : denv_wf E m → dval_wf E dv1 → dval_wf E dv2 → denv_interp E m -∗ vcg_bin_op E op dv1 dv2 m Φ -∗ ∃ w, ⌜cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some w⌝ ∧ vcg_continuation E Φ w. Proof. iIntros (???) "Hm H". rewrite /vcg_bin_op. destruct (dcbin_op_eval _ _ dv1 dv2) as [dw|] eqn:?; last first. { iApply (wand_denv_interp_spec with "H Hm"). } iExists _; iSplit; first by eauto. iApply (vcg_continuation_correct with "H"); eauto. Qed. Lemma vcg_pre_bin_op_correct E m op dv1 dv2 Φ : denv_wf E m → dval_wf E dv1 → dval_wf E dv2 → denv_interp E m -∗ vcg_pre_bin_op E op dv1 dv2 m Φ -∗ ∃ cl v w, ⌜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_continuation E Φ v). Proof. iIntros (???) "Hm H". rewrite /vcg_pre_bin_op. destruct (dloc_var_of_dval dv1) as [i|] eqn:?; last first. { iApply (wand_denv_interp_spec with "H Hm"). } destruct (denv_delete_full i m) as [[m' dv_old]|] eqn:?; simplify_eq/=. - iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hi]"; eauto. destruct (dcbin_op_eval _ _ dv_old dv2) as [dw|] eqn:?; last first. { iDestruct (wand_denv_interp_spec with "H Hm") as (w ?) "H". eauto 10 with iFrame. } iExists _, _, _; iFrame "Hi"; repeat (iSplit; first by eauto). iIntros "Hi". iApply (vcg_continuation_correct with "H"); eauto 10. iApply denv_insert_interp; eauto with iFrame. - iDestruct (wand_denv_interp_spec with "H Hm") as (w ?) "H". eauto 10 with iFrame. Qed. Lemma vcg_un_op_correct E m dv b Φ : dval_wf E dv → denv_wf E m → denv_interp E m -∗ vcg_un_op E b dv m Φ -∗ ∃ w, ⌜un_op_eval b (dval_interp E dv) = Some w⌝ ∧ vcg_continuation E Φ w. Proof. iIntros (Hwf Hwf2) "Hm H". rewrite /vcg_un_op. destruct (dun_op_eval E b dv) as [dw|] eqn:?. - iExists _; iSplit; first by eauto. iApply (vcg_continuation_correct with "H"); eauto. - by iApply (wand_denv_interp_spec with "H Hm"). Qed. Lemma vcg_correct R E m de Φ n : dcexpr_wf E de → denv_wf E m → denv_interp E m -∗ vcg E n m de R Φ -∗ CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}. Proof. iIntros (Hde Hm) "Hm H". iInduction n as [|n IH] "IH" forall (de Φ E m Hde Hm). { by destruct de. } destruct de; simplify_eq/=; destruct_and?. - (* return *) destruct (dexpr_eval _) as [dv1|] eqn:?; simplify_eq /=; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "\$". } iApply cwp_ret. iApply wp_wand; first by iApply dexpr_eval_correct. iIntros (v ->). iApply (vcg_continuation_correct with "H"); eauto. - (* bind *) iDestruct ("IH" with "[] [] Hm H") as "H"; eauto. iApply cwp_seq_bind. iApply (cwp_wand with "H"). iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]". iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. rewrite (dcexpr_interp_mono E E') // -dcexpr_interp_subst'. iDestruct ("IH" with "[] [] Hm H") as "H"; eauto using dcexpr_wf_mono. iApply (cwp_wand with "H"); iIntros (v) "H". by iApply (vcg_continuation_mono with "H"). - (* mut bind *) iDestruct ("IH" with "[] [] Hm H") as "H"; eauto. iApply cwp_mut_bind. iApply (cwp_wand with "H"). iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]". iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. iIntros (cl) "Hcl". iSpecialize ("H" \$! cl). assert (E' `prefix_of` E' ++ [cl]) by eauto using prefix_app_r. set (i := length E'). set (dlv := dLocV (dLoc i (dInt 0 None))). assert (dval_wf (E' ++ [cl]) dlv). { rewrite /dlv /= /dloc_wf /= /dloc_var_wf. by rewrite (list_lookup_middle _ []). } iDestruct ("IH" with "[%] [%] [Hm Hcl] H") as "H". { eauto using dcexpr_wf_mono. } { eauto using denv_wf_insert_extend. } { iApply denv_insert_interp; eauto using denv_wf_mono. rewrite /dloc_var_interp (list_lookup_middle _ []) //=. rewrite -(denv_interp_mono E'); eauto. rewrite -(dval_interp_mono E'); eauto. iFrame. } rewrite dcexpr_interp_subst' /= /dloc_var_interp (list_lookup_middle _ []) //=. rewrite -(dcexpr_interp_mono E); eauto. iApply (cwp_wand with "H"). iIntros (w) "H"; iDestruct "H" as (E'' dw m'' -> ???) "[Hm H]". destruct (denv_delete_full i m'') as [[m''' dw']|] eqn:?. + iDestruct (denv_delete_full_interp with "Hm") as "[Hm Hl]"; first done. rewrite -(dloc_var_interp_mono (E' ++ [cl])) /dloc_var_interp /=; eauto. rewrite (list_lookup_middle _ []) //=. iExists _; iFrame "Hl". iApply vcg_continuation_mono; [|iApply (vcg_continuation_correct with "H")]; eauto. + iDestruct (wand_denv_interp_spec with "H Hm") as (v) "[Hl H]". iExists _; iFrame "Hl". iApply (vcg_continuation_mono with "H"); eauto. - (* alloc *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_alloc with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_alloc_correct with "[HmNew Hm''] H") as (n' ??) "H"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl". rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono; last by iApply ("H" with "Hinfo"). + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_alloc with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_alloc_correct with "[HmNew Hm''] H") as (n' ??) "H"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl". by iApply vcg_continuation_mono; last by iApply ("H" with "Hinfo"). - (* load *) iApply cwp_load_exists_frac. iApply (cwp_wand with "[-]"). { iApply ("IH" with "[] [] Hm H"); eauto. } iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]". iDestruct (vcg_load_correct with "Hm H") as (cl q w ?) "[Hi H]"; eauto. iExists _, _, _; iSplit; first done. iIntros "{\$Hi} Hi". by iApply vcg_continuation_mono; last by iApply "H". - (* assign *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_store with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_store_correct with "[HmNew Hm''] H") as (cl w ?) "[Hi H]"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iExists _, _; iSplit; first done. iIntros "{\$Hi} Hi". rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono; last by iApply "H". + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_store with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_store_correct with "[HmNew Hm''] H") as (cl w ?) "[Hi H]"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _, _; iSplit; first done. iIntros "{\$Hi} Hi". by iApply vcg_continuation_mono; last by iApply "H". - (* bin op *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_bin_op with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_bin_op_correct with "[HmNew Hm''] H") as (w ?) "H"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _; iSplit; first done. by iApply vcg_continuation_mono. + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_bin_op with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_bin_op_correct with "[HmNew Hm''] H") as (w ?) "H"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _; iSplit; first done. by iApply vcg_continuation_mono. - (* pre bin op *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_pre_bin_op with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_pre_bin_op_correct with "[HmNew Hm''] H") as (cl w ??) "(Hi & % & H)"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _, _, _. iFrame "Hi". repeat (iSplit; first done). iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H". + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_pre_bin_op with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (v1 v2) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_pre_bin_op_correct with "[HmNew Hm''] H") as (cl w ??) "(Hi & % & H)"; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. iExists _, _, _. iFrame "Hi". repeat (iSplit; first done). iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H". - (* un op *) iApply cwp_un_op. iApply (cwp_wand with "[-]"). { iApply ("IH" with "[] [] Hm H"); eauto. } iIntros (v) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm H]". iDestruct (vcg_un_op_correct with "Hm H") as (w ?) "H"; eauto. iExists _; iSplit; first by eauto. by iApply vcg_continuation_mono. - (* par *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_par with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros "!>" (v1 v2) "H [-> HmNew] !>"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_continuation_correct with "H [Hm'' HmNew]") as "H"; simpl; split_and?; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono. + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_par with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros "!>" (v1 v2) "[-> HmNew] H !>"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (vcg_continuation_correct with "H [HmNew Hm'']") as "H"; simpl; split_and?; eauto using denv_wf_mono, dval_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } rewrite (dval_interp_mono E E'); eauto. by iApply vcg_continuation_mono. - (* while *) iApply cwp_while. iDestruct (vcg_cwp_continuation_correct with "Hm H") as "\$"; eauto. - (* whileV *) by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". - (* call *) destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first. + destruct (forward _ _ m de2) as [[[m' mNew] dv2]|] eqn:?; last first. { by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". } iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iApply (cwp_call with "[H Hm'] H2"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (f a) "H [-> HmNew]"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H". { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro. rewrite (dval_interp_mono E E'); eauto. iApply (cwp_wand with "H"); iIntros (w) "[\$ H]". by iApply vcg_continuation_mono. + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto. iApply (cwp_call with "H1 [H Hm']"). { iApply ("IH" with "[] [] Hm' H"); eauto. } iIntros (f a) "[-> HmNew] H"; iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H". { iApply denv_merge_interp; eauto using denv_wf_mono. iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro. rewrite (dval_interp_mono E E'); eauto. iApply (cwp_wand with "H"); iIntros (w) "[\$ H]". by iApply vcg_continuation_mono. - (* unknown *) by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "?". Qed. Lemma vcg_while_correct R E m de Φ n : dcexpr_wf E de → denv_wf E m → denv_interp E m -∗ vcg_while E n m de R Φ -∗ CWP dcexpr_interp E de @ R {{ vcg_continuation E Φ }}. Proof. destruct de; try apply vcg_correct; simpl. iIntros (??) "Hm H"; destruct_and?. iApply cwp_whileV; iNext. iDestruct (vcg_correct with "Hm H") as "H"; auto. iApply (cwp_wand with "H"); iIntros (v) "H". iDestruct "H" as (E' dv m' -> ???) "[Hm H]". destruct (dknown_bool_of_dval _) as [[]|] eqn:?; simplify_eq/=. - iLeft. iSplit; first by eauto. iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. rewrite (dcexpr_interp_mono E E') //. iDestruct (vcg_correct with "Hm H") as "H"; eauto using dcexpr_wf_mono. iApply (cwp_wand with "H"); iIntros (v) "H". iDestruct "H" as (E'' dw m'' -> ???) "[Hm H]". iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. iDestruct (vcg_correct with "Hm H") as "H"; simpl; split_and?; eauto using dcexpr_wf_mono. rewrite !(dcexpr_interp_mono _ E''); eauto using dcexpr_wf_mono. iApply (cwp_wand with "H"); iIntros (v) "H". iApply (vcg_continuation_mono with "H"); eauto. - iRight. iSplit; first by eauto. iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. iDestruct (vcg_continuation_correct with "H Hm") as "H"; eauto. iApply (vcg_continuation_mono with "H"); eauto. - iDestruct (wand_denv_interp_spec with "H Hm") as "[[% H]|[% H]]"; last first. { iRight. iSplit; first by eauto. iModIntro. iApply (vcg_continuation_mono with "H"); eauto. } iLeft. iSplit; first done. iModIntro. iDestruct "H" as (E'' dw m'' _ ???) "[Hm H]". destruct n as [|n]=> //=. iDestruct (vcg_correct with "Hm H") as "H"; eauto using dcexpr_wf_mono. rewrite (dcexpr_interp_mono E E''); eauto. iApply (cwp_wand with "H"); iIntros (v) "H". iDestruct "H" as (E''' dw' m''' _ ???) "[Hm H]". iDestruct (denv_unlock_interp with "Hm") as "Hm"; iModIntro. rewrite !(dcexpr_interp_mono _ E'''); eauto using dcexpr_wf_mono. iDestruct (vcg_correct with "Hm H") as "H"; simpl; split_and?; eauto using dcexpr_wf_mono. iApply (cwp_wand with "H"); iIntros (v') "H". iApply (vcg_continuation_mono with "H"); eauto. Qed. End vcg_spec. Arguments vcg_cwp_continuation _ _ _ _ _ _ _ /. Arguments vcg_alloc _ _ _ _ _ _ _ /. Arguments vcg_load _ _ _ _ _ _ /. Arguments vcg_store _ _ _ _ _ _ _ /. Arguments vcg_bin_op _ _ _ _ _ _ _ _ /. Arguments vcg_un_op _ _ _ _ _ _ _ /. Arguments vcg_pre_bin_op _ _ _ _ _ _ _ _ /. Arguments vcg_call _ _ _ _ _ _ _ _ /.