Commit ef76090d by Dan Frumin

### Add `a_pre_bin_op`

parent 54668a87
 ... ... @@ -34,6 +34,10 @@ Definition a_un_op (op : un_op) : val := λ: "x", "v" ←ᶜ "x" ;;ᶜ a_ret (UnOp op "v"). (*Definition a_pre_un_op (op : un_op) : val := λ: "x", "l" ←ᶜ "x" ;;ᶜ a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*) Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2", "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ a_ret (BinOp op (Fst "vv") (Snd "vv")). ... ... @@ -46,6 +50,16 @@ Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope. Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope. Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y", "lv" ←ᶜ ("x" |||ᶜ "y");;ᶜ a_atomic (λ: <>, "ov" ←ᶜ (∗ᶜ (a_ret (Fst "lv")));;ᶜ a_store (a_ret (Fst "lv")) (a_bin_op op (a_ret "ov") (a_ret (Snd "lv")));;ᶜ a_ret "ov"). Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. (* M () *) (* The eta expansion is used to turn it into a value *) Definition a_seq : val := λ: <>, ... ... @@ -223,7 +237,7 @@ Section proofs. Lemma a_un_op_spec R Φ e op: AWP e @ R {{ v, ∃ w : val, ⌜un_op_eval op v = Some w⌝ ∧ Φ w }} -∗ AWP (a_un_op op) e @ R {{ Φ }}. AWP a_un_op op e @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam. ... ... @@ -233,11 +247,39 @@ Section proofs. iApply awp_ret. by wp_op. Qed. (* Lemma a_pre_un_op_spec R Φ e op : AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝ ∗ ⌜un_op_eval op v = Some w⌝ ∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗ AWP a_pre_un_op op e @ R {{ Φ }}. Proof. iIntros "He". rewrite /a_pre_un_op. awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam. iApply awp_bind. iApply (awp_wand with "HΦ"). iIntros (vl) "H". awp_lam. iApply awp_atomic. iNext. iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)". simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I (λ v', ⌜v' = w⌝ ∗ l ↦C v)%I with "[] [Hl] [-]"). - iApply awp_ret. by wp_value_head. - iApply a_un_op_spec. iApply a_load_spec. iApply awp_ret. wp_value_head. iExists _,_; iFrame. iSplit; eauto. - iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=. iExists _,_; iFrame. iSplit; eauto. iIntros "? _". by iApply "HΦ". Qed. *) Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) : AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗ AWP (a_bin_op op e1 e2) @ R {{ Φ }}. AWP a_bin_op op e1 e2 @ R {{ Φ }}. Proof. iIntros "H1 H2 HΦ". awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam. ... ... @@ -250,6 +292,39 @@ Section proofs. iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. Qed. Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op : AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R -∗ ∃ l v w, l ↦C v ∗ ⌜v1 = #l⌝ ∗ ⌜bin_op_eval op v v2 = Some w⌝ ∗ (l ↦C[LLvl] w -∗ R ∗ Φ v)) -∗ AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. Proof. iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op. awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam. awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam. iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext. iIntros (v1 v2) "Hv1 Hv2". iNext. awp_let. iApply awp_atomic. iNext. iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (l v w) "(Hl & % & % & HΦ)". simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head. iExists l, v; iFrame. iSplit; eauto. iIntros "Hl". awp_let. iApply awp_bind. iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]"). - awp_proj. iApply awp_ret; by wp_value_head. - iApply (a_bin_op_spec _ _ (λ v', ⌜v' = v⌝)%I (λ v', ⌜v' = v2⌝)%I); try (try awp_proj; iApply awp_ret; by wp_value_head). iNext. iIntros (? ? -> ->). eauto. - iNext. iIntros (? ? -> ->). iExists _,_; iFrame. iSplit; eauto. iIntros "?". awp_seq. iApply awp_ret; wp_value_head. iIntros "_". by iApply "HΦ". Qed. Lemma a_seq_spec R Φ : U (Φ #()) -∗ AWP (a_seq #()) @ R {{ Φ }}. ... ...
 ... ... @@ -136,4 +136,15 @@ Section test. - iIntros (? ? -> ->). iExists #(z1+z2). iSplit; eauto. Qed. Lemma inc_test1 (l : loc) (z0 : Z) R: l ↦C #z0 -∗ AWP ♯l +=ᶜ ♯1 @ R {{ v, ⌜v = #z0⌝ ∧ l ↦C[LLvl] #(z0+1) }}. Proof. iIntros "Hl". iApply (a_pre_bin_op_spec _ _ (λ v, ⌜v = #l⌝)%I (λ v, ⌜v = #1⌝)%I); try (iApply awp_ret; by wp_value_head). iNext. iIntros (? ? -> ->) "HR". iExists _,_,#(z0+1); iFrame. repeat iSplit; eauto. Qed. End test.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment