Commit 39e98fa6 by Dan Frumin

### Update the translation for c_pre_bin_op

parent 9105d328
 ... ... @@ -225,9 +225,10 @@ Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val := Definition c_pre_bin_op (op : cbin_op) : val := λ: "x" "y", (* all binds should be non-sequenced *) "lv" ←ᶜ ("x" |||ᶜ "y");;ᶜ c_atomic (λ: <>, "ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;ᶜ c_ret (Fst "lv") =ᶜ c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;ᶜ c_ret "ov". c_ret "ov"). Notation "e1 +=ᶜ e2" := (c_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope. Notation "e1 +∗=ᶜ e2" := (c_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope. ... ... @@ -647,11 +648,11 @@ Section proofs. Lemma cwp_pre_bin_op R Φ Ψ1 Ψ2 e1 e2 op : CWP e1 @ R {{ Ψ1 }} -∗ CWP e2 @ R {{ Ψ2 }} -∗ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R ={⊤}=∗ ∃ cl v w, ⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C v ∗ ⌜ cbin_op_eval op v v2 = Some w ⌝ ∗ (cl ↦C[LLvl] w -∗ Φ v)) -∗ (cl ↦C[LLvl] w ={⊤}=∗ R ∗ Φ v)) -∗ CWP c_pre_bin_op op e1 e2 @ R {{ Φ }}. Proof. iIntros "He1 He2 HΦ". ... ... @@ -659,7 +660,9 @@ Section proofs. cwp_apply (cwp_wp with "He1"); iIntros (a1) "Ha1". cwp_lam; cwp_pures. iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2"). iNext. iIntros (v1 v2) "Hv1 Hv2 !>". cwp_pures. iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)". iApply cwp_atomic. iIntros "HR !>". iExists True%I. iSplitR; first done. cwp_lam. cwp_pures. iMod ("HΦ" with "Hv1 Hv2 HR") as (cl v w ->) "(Hl & % & HΦ)". iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value. iIntros "HR !>". iExists cl, v; iFrame. iSplit; first done. iIntros "Hl !>". cwp_pures. iApply cwp_bind. ... ... @@ -671,7 +674,8 @@ Section proofs. iIntros (? ? -> ->); eauto. - iIntros (? ? -> ->). iIntros "HR !>". iExists _, _; iFrame. iSplit; first done. iIntros "? !>". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ". iIntros "Hcl !>". cwp_seq. iMod ("HΦ" with "Hcl") as "[\$ HΦ]". iApply cwp_ret; iApply wp_value. eauto. Qed. End proofs. ... ...
 ... ... @@ -272,11 +272,11 @@ Section forward_spec. { iApply denv_delete_full_2_interp; eauto. } iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]". iApply (cwp_pre_bin_op with "H1 H2"). iIntros (v1 v2) "[-> Hm1] [-> Hm2]". iIntros (v1 v2) "[-> Hm1] [-> Hm2] \$ !>". iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]". { iApply denv_merge_interp; eauto with iFrame. } iExists _, _, _. iFrame "Hi". repeat (iSplit; first by eauto). iIntros "Hi"; iSplit; first done. iIntros "Hi !>"; iSplit; first done. iApply denv_insert_interp; eauto 10 with iFrame. - (* un op *) destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=. ... ...
 ... ... @@ -579,8 +579,9 @@ Section vcg_spec. { 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. iIntros "\$ !>". iExists _, _, _. iFrame "Hi". repeat (iSplit; first done). iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H". 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. } ... ... @@ -590,8 +591,9 @@ Section vcg_spec. { 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. iIntros "\$ !>". iExists _, _, _. iFrame "Hi". repeat (iSplit; first done). iIntros "Hi". by iApply vcg_continuation_mono; last by iApply "H". 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. } ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!