Commit 011eb020 by Ralf Jung

add lemmas for combining CAS and Resolve

parent b97c5886
 ... ... @@ -8,34 +8,6 @@ Section tests. Implicit Types P Q : iProp Σ. Implicit Types Φ : val → iProp Σ. Definition CAS_resolve e1 e2 e3 p v := Resolve (CAS e1 e2 e3) p v. Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) : vals_cas_compare_safe v1 v1 → {{{ proph p vs ∗ ▷ l ↦ v1 }}} CAS_resolve #l v1 v2 #p v @ s; E {{{ RET v1 ; ∃ vs', ⌜vs = (v1, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}. Proof. iIntros (Hcmp Φ) "[Hp Hl] HΦ". wp_apply (wp_resolve with "Hp"); first done. assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp. wp_cas_suc. iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame. Qed. Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) : val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 → {{{ proph p vs ∗ ▷ l ↦ v' }}} CAS_resolve #l v1 v2 #p v @ s; E {{{ RET v' ; ∃ vs', ⌜vs = (v', v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}. Proof. iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ". wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail. iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame. Qed. Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) : l ↦ #n -∗ proph p vs -∗ ... ...
 ... ... @@ -495,6 +495,7 @@ Proof. iMod "HΦ". iModIntro. by iApply "HΦ". Qed. (** Lemmas for some particular expression inside the [Resolve]. *) Lemma wp_resolve_proph s E p vs v : {{{ proph p vs }}} ResolveProph (Val \$ LitV \$ LitProphecy p) (Val v) @ s; E ... ... @@ -505,4 +506,29 @@ Proof. iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame. Qed. Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) : vals_cas_compare_safe v1 v1 → {{{ proph p vs ∗ ▷ l ↦ v1 }}} Resolve (CAS #l v1 v2) #p v @ s; E {{{ RET v1 ; ∃ vs', ⌜vs = (v1, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}. Proof. iIntros (Hcmp Φ) "[Hp Hl] HΦ". iApply (wp_resolve with "Hp"); first done. assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp. iApply (wp_cas_suc with "Hl"); [done..|]. iIntros "!> Hl". iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame. Qed. Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) q (v' v1 v2 v : val) : val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 → {{{ proph p vs ∗ ▷ l ↦{q} v' }}} Resolve (CAS #l v1 v2) #p v @ s; E {{{ RET v' ; ∃ vs', ⌜vs = (v', v)::vs'⌝ ∗ proph p vs' ∗ l ↦{q} v' }}}. Proof. iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ". iApply (wp_resolve with "Hp"); first done. iApply (wp_cas_fail with "Hl"); [done..|]. iIntros "!> Hl". iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame. Qed. End lifting.
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