Commit 6f3dc0a9 authored by Dan Frumin's avatar Dan Frumin

Full circle for the "awkward" example

parent 7546cf67
......@@ -140,6 +140,51 @@ Section refinement.
rel_vals; eauto.
Qed.
Lemma refinement25 `{oneshotG Σ} Γ :
Γ
(λ: "f", "f" #();; #1)
log
(let: "x" := ref #0 in
(λ: "f", "x" <- #1;; "f" #();; !"x"))
: ((Unit Unit) TNat).
Proof.
iIntros (Δ).
rel_alloc_r as x "Hx".
rel_let_r.
iMod new_pending as (γ) "Ht".
iMod (inv_alloc shootN _ ((x ↦ₛ #0 pending γ x ↦ₛ #1 shot γ))%I with "[Hx Ht]") as "#Hinv".
{ iNext. iLeft. iFrame. }
iApply bin_log_related_arrow; auto.
iIntros "!#" (f1 f2) "#Hf".
rel_let_l. rel_let_r.
iInv shootN as ">[[Hx Hp] | [Hx #Hs]]" "Hcl";
rel_store_r; rel_seq_r.
- iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
rel_finish.
+ iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
rel_load_r.
{ iExFalso. iApply (shot_not_pending with "Hs Hp"). }
iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
rel_finish.
- iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
rel_finish.
+ iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
rel_load_r.
{ iExFalso. iApply (shot_not_pending with "Hs Hp"). }
iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
rel_finish.
Qed.
(* Also known as "callback with lock" *)
Definition i3 x x' b b' : iProp Σ :=
(( (n : nat), x ↦ᵢ #n x' ↦ₛ #n
......
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