blob: 5051c6a6b854e50286da4f011346cd59761d7eec (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.
From lmpmc Require Import lmpmc_queue_spec util.
Section lmpmc_blocking.
Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).
(* https://types.pl/@pigworker/115629120124299549 *)
Definition dequeue : val := rec: "go" "ℓ_deq" :=
match: lq.(try_dequeue) "ℓ_deq" with
NONE => "go" "ℓ_deq"
| SOME "v" => "v"
end.
Section proofs.
Context `{heapGS Σ} (lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq).
Lemma dequeue_spec (ℓ_deq : loc) :
⊢ <<{ ∀∀ ℓ_enq cvs, lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs }>>
dequeue #ℓ_deq @ ∅
<<{ ∃∃ cv cvs', ⌜cvs = cv :: cvs'⌝ ∗ lqp.(queue_repr lq) ℓ_deq ℓ_enq cvs' | RET cv }>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_rec.
awp_apply lqp.(try_dequeue_spec lq).
rewrite /atomic_acc /=.
iMod "AU" as "(%ℓ_enq & %cvs & Hcvs & Hclose)".
iFrame. iModIntro. iSplit; iIntros "Hrepr".
- by iMod ("Hclose" with "Hrepr") as "AU".
- destruct cvs as [|cv cvs']; simplify_list_eq.
+ iMod ("Hclose" with "Hrepr") as "AU". iModIntro.
wp_pures. by iApply "IH".
+ iDestruct "Hclose" as "[_ Hclose]".
iMod ("Hclose" $! cv cvs' with "[$Hrepr //]") as "HΦ".
iModIntro. by wp_pures.
Qed.
End proofs.
End lmpmc_blocking.
|
