Skip to content
Snippets Groups Projects
Commit 4f918d4a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak tests/one_shot.

parent 898bc304
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
tests/one_shot.v
+ 2
− 2
View file @ 4f918d4a
...@@ -52,11 +52,11 @@ Proof. ...@@ -52,11 +52,11 @@ Proof.
iPvsIntro. iApply "Hf"; iSplit. iPvsIntro. iApply "Hf"; iSplit.
- iIntros {n} "!". wp_let. - iIntros {n} "!". wp_let.
iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]". iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
+ iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft]. + wp_cas_suc. iSplitL; [|by iLeft].
iPvs (own_update with "Hγ") as "Hγ". iPvs (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). } { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
iPvsIntro; iRight; iExists n; by iSplitL "Hl". iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+ wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight. + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ". - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ Pending) ∨ iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ Pending) ∨
∃ n : Z, v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv". ∃ n : Z, v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
......
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