Commit 5fa04408 authored by Ralf Jung's avatar Ralf Jung

update one_shot_once

parent ffccb508
...@@ -35,5 +35,9 @@ ...@@ -35,5 +35,9 @@
"Hγ" : own γ (Shot m') "Hγ" : own γ (Shot m')
--------------------------------------∗ --------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP InjRV #m = InjRV #m' {{ v, ⌜v = #true⌝ ∧ ▷ True }} ∗ WP let: "y'" := InjRV #m' in
match: InjRV #m with
InjL <> => #()
| InjR <> => assert: InjRV #m = "y'"
end {{ _, True }}
...@@ -15,10 +15,11 @@ Definition one_shot_example : val := λ: <>, ...@@ -15,10 +15,11 @@ Definition one_shot_example : val := λ: <>,
assert: CAS "x" NONE (SOME "n")), assert: CAS "x" NONE (SOME "n")),
(* check *) (λ: <>, (* check *) (λ: <>,
let: "y" := !"x" in λ: <>, let: "y" := !"x" in λ: <>,
match: "y" with let: "y'" := !"x" in
NONE => #() match: "y" with
| SOME <> => assert: "y" = !"x" NONE => #()
end)). | SOME <> => assert: "y" = "y'"
end)).
Definition one_shotR := csumR fracR (agreeR ZO). Definition one_shotR := csumR fracR (agreeR ZO).
Definition Pending (q : Qp) : one_shotR := Cinl q. Definition Pending (q : Qp) : one_shotR := Cinl q.
...@@ -37,6 +38,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ := ...@@ -37,6 +38,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
(l NONEV own γ (Pending (1/2)%Qp) (l NONEV own γ (Pending (1/2)%Qp)
n : Z, l SOMEV #n own γ (Shot n))%I. n : Z, l SOMEV #n own γ (Shot n))%I.
Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) => unfold one_shot_inv.
Lemma pending_split γ q : Lemma pending_split γ q :
own γ (Pending q) own γ (Pending (q/2)) own γ (Pending (q/2)). own γ (Pending q) own γ (Pending (q/2)) own γ (Pending (q/2)).
Proof. Proof.
...@@ -86,17 +89,18 @@ Proof. ...@@ -86,17 +89,18 @@ Proof.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto. + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. } + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto. iSplitL "Hinv"; first by eauto.
iModIntro. wp_pures. iIntros "!#". wp_lam. iModIntro. wp_pures. iIntros "!#". wp_lam. wp_bind (! _)%E.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; iInv N as "Hinv".
subst; wp_match; [done|]. iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
wp_pures. iApply wp_assert. wp_bind (! _)%E. + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]". wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
{ by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. } wp_pures; done.
wp_load. Show. + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst. { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
iModIntro. iSplitL "Hl". wp_load. Show.
{ iNext; iRight; by eauto. } iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
wp_pures. by case_bool_decide. iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
Qed. Qed.
Lemma ht_one_shot (Φ : val iProp Σ) : Lemma ht_one_shot (Φ : val iProp Σ) :
......
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