summaryrefslogtreecommitdiffstats
path: root/theories/example.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/example.v')
-rw-r--r--theories/example.v723
1 files changed, 723 insertions, 0 deletions
diff --git a/theories/example.v b/theories/example.v
new file mode 100644
index 0000000..7857118
--- /dev/null
+++ b/theories/example.v
@@ -0,0 +1,723 @@
1From iris.program_logic Require Import atomic.
2From iris.heap_lang Require Import notation proofmode adequacy.
3From iris.algebra Require Import list gmultiset.
4From iris.algebra.lib Require Import excl_auth.
5From iris.base_logic.lib Require Import invariants mono_list.
6From iris_named_props Require Import custom_syntax.
7From iris.heap_lang.lib Require Import assert par.
8
9From lmpmc Require lmpmc_queue_spec lmpmc_queue_proof fin_queue_proof lmpmc_blocking_dequeue.
10From lmpmc Require Import upstream.
11
12Definition somes {A} (xs : list (option A)) : list A := xs ≫= option_list.
13Definition option_le {A} (mx my : option A) := option_relation (=) (const False) (const True) mx my.
14Definition option_nat (x : nat) : option nat := guard (x ≠ 0);; Some x.
15Definition vals_of_nats : list nat → list val := fmap (LitV ∘ LitInt ∘ Z.of_nat).
16
17Lemma option_le_None {A} (x : A) : option_le None (Some x).
18Proof. done. Qed.
19Lemma option_le_Some {A} (x : A) : option_le (Some x) (Some x).
20Proof. done. Qed.
21Lemma option_le_inv {A} (mx my : option A) : option_le mx my → mx = None ∨ mx = my.
22Proof. induction mx, my; intros ?; simplify_eq/=; done || (by right) || by left. Qed.
23
24#[global] Instance timeless_if_bool {PROP : bi} {b : bool} {Q R : PROP} : Timeless Q → Timeless R → Timeless (if b then Q else R).
25Proof. by destruct b. Qed.
26
27Section hl.
28 Context (lq : lmpmc_queue_spec.lmpmc_queue_hl).
29 Import lmpmc_blocking_dequeue lmpmc_queue_spec.
30
31 Notation "'let2:' x1 , x2 := e1 'in' e2" :=
32 (Lam (BNamed x2) (Lam (BNamed x1) (Lam (BNamed x2) e2 (Snd (Var x2))) (Fst (Var x2))) e1)%E
33 (at level 200, x1, x2 at level 1, e1, e2 at level 200,
34 format "'[' 'let2:' x1 ',' x2 := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
35
36 Definition simple_example_2_1 : expr :=
37 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
38 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
39 lq.(enqueue) "ℓ_enq1" #10;;
40 lq.(link) "ℓ_enq1" "ℓ_deq2";;
41 lq.(enqueue) "ℓ_enq2" #20;;
42 let: "x" := dequeue lq "ℓ_deq1" in
43 let: "y" := dequeue lq "ℓ_deq1" in
44 ("x", "y").
45
46 Definition simple_example_2_2 : expr :=
47 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
48 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
49 (( lq.(enqueue) "ℓ_enq1" #10;;
50 lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *)
51 ||| lq.(enqueue) "ℓ_enq2" #20 (* thread B *)
52 );;
53 let: "x" := dequeue lq "ℓ_deq1" in
54 let: "y" := dequeue lq "ℓ_deq1" in
55 ("x", "y").
56
57 Definition mt_example_1 : expr :=
58 let: "ℓ_sum" := Alloc #0 in
59 let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in
60 let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in
61 (( lq.(enqueue) "ℓ_enq1" #1;;
62 lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *)
63 ||| lq.(enqueue) "ℓ_enq2" #2 (* thread B *)
64 ||| lq.(enqueue) "ℓ_enq2" #3 (* thread C *)
65 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread D *)
66 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread E *)
67 ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread F *)
68 );;
69 ! "ℓ_sum".
70
71End hl.
72
73Section proofs.
74 Context `{!heapGS Σ, !spawnG Σ,
75 !mono_listG natO Σ,
76 !inG Σ (excl_authR (gmultisetO nat)),
77 !inG Σ (excl_authR natO),
78 !inG Σ (excl_authR boolO),
79 !inG Σ (excl_authR (listO natO)),
80 !inG Σ (excl_authR (optionO natO)),
81 !inG Σ (exclR (listO natO))}.
82 Context {lq : lmpmc_queue_spec.lmpmc_queue_hl}
83 {lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq}.
84 Import lmpmc_blocking_dequeue lmpmc_queue_spec.
85
86 Lemma simple_example_2_1_safe :
87 ⊢ WP simple_example_2_1 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
88 Proof.
89 iUnfold simple_example_2_1.
90 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
91 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
92 awp_apply lqp.(enqueue_spec lq). iAaccIntro with "Hq1"; iIntros "Hq1"; first by iFrame.
93 simpl. iModIntro. wp_pures.
94 awp_apply lqp.(link_spec lq).
95 rewrite /atomic_acc /=.
96 iExists true. iFrame.
97 iApply fupd_mask_intro; first done.
98 iIntros "Hupd". iSplit. { iIntros "[? ?]". iFrame. }
99 iIntros "Hq". simpl. iMod "Hupd" as "_". iModIntro.
100 wp_pures. awp_apply lqp.(enqueue_spec lq).
101 iAaccIntro with "Hq"; iIntros "Hq"; first by iFrame.
102 simpl.
103
104 iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
105 iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
106 iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.
107 iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp).
108 iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame.
109 iIntros (? ?) "[%Hvs Hq]". iSimplifyEq.
110
111 iModIntro. by wp_pures.
112 Qed.
113
114 Record smp_gstate :=
115 SmpGstate
116 { γ1_linked : gname; (* (●E) whether Q1 and Q2 have been linked already *)
117 γ1_contA : gname; (* (●E) (list nat) contribution of thread A *)
118 γ1_contB : gname; (* (●E) (list nat) contribution of thread B *)
119 }.
120
121 Definition smp_inv γs (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
122 ∃ (linked : bool) (contA contB : list nat),
123 ("Hlinked●" ∷ own γs.(γ1_linked) (●E linked)) ∗
124 ("HcontA●" ∷ own γs.(γ1_contA) (●E contA)) ∗
125 ("HcontB●" ∷ own γs.(γ1_contB) (●E contB)) ∗
126 ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats (if linked then contA ++ contB else contA))) ∗
127 ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats contB)).
128
129 Lemma simple_example_2_2_safe :
130 ⊢ WP simple_example_2_2 lq {{ v, ⌜v = (#10, #20)%V⌝ }}.
131 Proof.
132 iUnfold simple_example_2_2.
133 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
134 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
135
136 iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
137 iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contA') "[HcontA● HcontA◯]"; first apply excl_auth_valid.
138 iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contB') "[HcontB● HcontB◯]"; first apply excl_auth_valid.
139
140 pose γs := SmpGstate γ1_linked' γ1_contA' γ1_contB'.
141 replace γ1_linked' with γs.(γ1_linked) by done.
142 replace γ1_contA' with γs.(γ1_contA) by done.
143 replace γ1_contB' with γs.(γ1_contB) by done.
144 clearbody γs. clear γ1_linked' γ1_contA' γ1_contB'.
145 iAssert (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "[$]" as "Hinv".
146 iMod (inv_alloc nroot _ (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".
147
148 wp_smart_apply (wp_par (λ _, own γs.(γ1_linked) (◯E true) ∗ own γs.(γ1_contA) (◯E [10]))%I
149 (λ _, own γs.(γ1_contB) (◯E [20]))
150 with "[Hlinked◯ HcontA◯] [HcontB◯]").
151 { awp_apply lqp.(enqueue_spec lq).
152 iInv "Hinv" as (linked contA contB) ">H".
153 iNamedSuffix "H" "_1".
154 iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
155 iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
156 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
157 iIntros "Hq1_1".
158 iCombine "HcontA●_1 HcontA◯" as "HcontA".
159 iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
160 { apply (excl_auth_update _ _ [10]). }
161 iIntros "!>".
162 iSimplifyEq. replace ([ #10 ] : list val) with (vals_of_nats [10]) by done.
163 iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". wp_pures. clear contB.
164
165 awp_apply lqp.(link_spec lq).
166 iInv "Hinv" as (linked contA contB) ">H".
167 iNamedSuffix "H" "_2".
168 iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
169 iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
170 rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
171 iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
172 { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. do 2 iFrame. }
173 iIntros "Hq1". iMod "Hclose" as "_".
174 iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
175 iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
176 { apply (excl_auth_update _ _ true). }
177 iFrame "Hlinked●_2 HcontA●_2 HcontB●_2 Hq1". by iFrame. }
178 { awp_apply lqp.(enqueue_spec lq).
179 iInv "Hinv" as (linked contA contB) ">H".
180 iNamedSuffix "H" "_1".
181 iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
182 destruct linked eqn:Hlinked.
183 { iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
184 iIntros "Hq1_1".
185 iCombine "HcontB◯ HcontB●_1" as "HcontB".
186 iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
187 { apply (excl_auth_update _ _ [20]). }
188 iIntros "!>".
189 iSimplifyEq.
190 replace [ #20 ] with (vals_of_nats [20]) by done.
191 iEval (rewrite app_nil_r /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1_1".
192 by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1". }
193 { iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". by iFrame. }
194 iIntros "Hq2_1".
195 iCombine "HcontB◯ HcontB●_1" as "HcontB".
196 iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]".
197 { apply (excl_auth_update _ _ [20]). }
198 iIntros "!>".
199 iSimplifyEq.
200 replace [ #20 ] with (vals_of_nats [20]) by done.
201 by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". } }
202 { iIntros (v1 v2) "[[Hlinked◯ HcontA◯] HcontB◯]".
203 iModIntro. wp_pures. clear v1 v2.
204 awp_apply (dequeue_spec lq lqp).
205 iInv "Hinv" as (linked contA contB) ">H".
206 iNamedSuffix "H" "_1".
207 iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L.
208 iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L.
209 iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L.
210 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
211 iIntros (v0 vs) "[%Hvs Hq1]".
212 simpl in Hvs. injection Hvs as <- <-.
213 replace [ #20%nat ] with (vals_of_nats [20]) by done.
214 iCombine "HcontA●_1 HcontA◯" as "HcontA".
215 iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]".
216 { apply (excl_auth_update _ _ []). }
217 iIntros "!>".
218 iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1". wp_pures.
219
220 awp_apply (dequeue_spec lq lqp).
221 iInv "Hinv" as (linked contA contB) ">H".
222 iNamedSuffix "H" "_2".
223 iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L.
224 iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L.
225 iCombine "HcontB◯ HcontB●_2" gives %->%excl_auth_agree_L.
226 iAaccIntro with "Hq1_2". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. }
227 iIntros (v0 vs) "[%Hvs Hq1]".
228 simpl in Hvs. injection Hvs as <- <-.
229 replace [ #20%nat ] with (vals_of_nats [20]) by done.
230 iCombine "HcontB●_2 HcontB◯" as "HcontB".
231 iMod (own_update with "HcontB") as "[HcontB●_2 HcontB◯]".
232 { apply (excl_auth_update _ _ []). }
233 iIntros "!>".
234 iFrame "Hlinked●_2 HcontB●_2 HcontA●_2 Hq1". wp_pures.
235 done. }
236 Qed.
237
238 Record mt_gstate :=
239 Gstate
240 { γ2_hist1 : gname; (* (●ML) (list nat) succesfully enqueued items (Q1) *)
241 γ2_hist2 : gname; (* (●E ) (list nat) sucessfully enqueued items (Q2) *)
242 γ2_linked : gname; (* (●E ) (bool) whether Q1 and Q2 have been linked *)
243 γ2_venqA : gname; (* (●E ) (gmultiset nat) of items enqueued by thread A *)
244 γ2_venqB : gname; (* (●E ) (gmultiset nat) of items enqueued by thread B *)
245 γ2_venqC : gname; (* (●E ) (gmultiset nat) of items enqueued by thread C *)
246 γ2_vdeqD : gname; (* (●E ) (option nat) poised contribution of first dequeueing thread *)
247 γ2_vdeqE : gname; (* (●E ) (option nat) poised contribution of second dequeueing thread *)
248 γ2_vdeqF : gname; (* (●E ) (option nat) poised contribution of third dequeueing thread *)
249 γ2_contD : gname; (* (●E ) (nat) as-is contribution of first dequeueing thread *)
250 γ2_contE : gname; (* (●E ) (nat) as-is contribution of second dequeueing thread *)
251 γ2_contF : gname; (* (●E ) (nat) as-is contribution of third dequeueing thread *)
252 }.
253
254 Definition mt_inv γs ℓ_sum (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ :=
255 ∃ (hist1 hist2 : list nat) (ndeq : nat) (linked : bool) (ecsA ecsB ecsC : gmultiset nat) (npD npE npF : option nat) (nD nE nF : nat) (vs1 : list nat),
256 ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats vs1)) ∗
257 ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats hist2)) ∗
258 ("Hhist1●" ∷ γs.(γ2_hist1) ↪●ML hist1) ∗
259 ("Hhist2E" ∷ own γs.(γ2_hist2) (Excl hist2)) ∗
260 ("Hlinked●" ∷ own γs.(γ2_linked) (●E linked)) ∗
261 ("HvenqA●" ∷ own γs.(γ2_venqA) (●E ecsA)) ∗
262 ("HvenqB●" ∷ own γs.(γ2_venqB) (●E ecsB)) ∗
263 ("HvenqC●" ∷ own γs.(γ2_venqC) (●E ecsC)) ∗
264 ("HvdeqD●" ∷ own γs.(γ2_vdeqD) (●E npD)) ∗
265 ("HvdeqE●" ∷ own γs.(γ2_vdeqE) (●E npE)) ∗
266 ("HvdeqF●" ∷ own γs.(γ2_vdeqF) (●E npF)) ∗
267 ("HcontD●" ∷ own γs.(γ2_contD) (●E nD)) ∗
268 ("HcontE●" ∷ own γs.(γ2_contE) (●E nE)) ∗
269 ("HcontF●" ∷ own γs.(γ2_contF) (●E nF)) ∗
270 ("Hsum" ∷ ℓ_sum ↦ #(nD + nE + nF)) ∗
271 ("%Hhist1" ∷ ⌜list_to_set_disj hist1 ⊆ if linked then ecsA ⊎ ecsB ⊎ ecsC else ecsA⌝) ∗
272 ("%Hhist2" ∷ ⌜list_to_set_disj hist2 ⊆ ecsB ⊎ ecsC⌝) ∗
273 ("%Hhist1n0" ∷ ⌜Forall (.≠ 0) hist1⌝) ∗
274 ("%Hhist2n0" ∷ ⌜Forall (.≠ 0) hist2⌝) ∗
275 ("%HnDEF" ∷ ⌜somes [npD; npE; npF] ⊆+ take ndeq hist1⌝) ∗
276 ("%HD" ∷ ⌜option_le (option_nat nD) npD⌝) ∗
277 ("%HE" ∷ ⌜option_le (option_nat nE) npE⌝) ∗
278 ("%HF" ∷ ⌜option_le (option_nat nF) npF⌝) ∗
279 ("%Hndeq" ∷ ⌜ndeq ≤ length hist1⌝) ∗
280 ("%Hhistvs" ∷ ⌜drop ndeq hist1 = vs1⌝).
281
282 (* Post, we expect:
283 linked = true
284 nD, nE, nF ≠ 0 (hence npD, npE, npF ≠ None and all are unique, adding up to 6) *)
285
286 Lemma mt_example_1_safe :
287 ⊢ WP mt_example_1 lq {{ v, ⌜v = #6⌝ }}.
288 Proof.
289 iUnfold mt_example_1.
290 wp_alloc ℓ_sum as "Hsum". wp_pures.
291 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures.
292 wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures.
293 iEval (replace [] with (vals_of_nats [])) in "Hq1 Hq2".
294 iMod (mono_list_own_alloc []) as "[%γ2_hist1 [Hhist1● _]]".
295 iMod (own_alloc (Excl [])) as "[%γ2_hist2 Hhist2E]"; first done.
296 iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid.
297 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqA') "[HvenqA● HvenqA◯]"; first apply excl_auth_valid.
298 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqB') "[HvenqB● HvenqB◯]"; first apply excl_auth_valid.
299 iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqC') "[HvenqC● HvenqC◯]"; first apply excl_auth_valid.
300 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqD' [HvdeqD● HvdeqD◯]]"; first apply excl_auth_valid.
301 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqE' [HvdeqE● HvdeqE◯]]"; first apply excl_auth_valid.
302 iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqF' [HvdeqF● HvdeqF◯]]"; first apply excl_auth_valid.
303 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contD') "[HcontD● HcontD◯]"; first apply excl_auth_valid.
304 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contE') "[HcontE● HcontE◯]"; first apply excl_auth_valid.
305 iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contF') "[HcontF● HcontF◯]"; first apply excl_auth_valid.
306 pose γs := Gstate γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'.
307 replace γ2_linked' with γs.(γ2_linked) by done.
308 replace γ2_venqA' with γs.(γ2_venqA) by done.
309 replace γ2_venqB' with γs.(γ2_venqB) by done.
310 replace γ2_venqC' with γs.(γ2_venqC) by done.
311 replace γ2_vdeqD' with γs.(γ2_vdeqD) by done.
312 replace γ2_vdeqE' with γs.(γ2_vdeqE) by done.
313 replace γ2_vdeqF' with γs.(γ2_vdeqF) by done.
314 replace γ2_contD' with γs.(γ2_contD) by done.
315 replace γ2_contE' with γs.(γ2_contE) by done.
316 replace γ2_contF' with γs.(γ2_contF) by done.
317 iAssert (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2)
318 with "[$Hhist1● $Hhist2E $Hlinked● $HvenqA● $HvenqB● $HvenqC● $HvdeqD● $HvdeqE● $HvdeqF● $HcontD● $HcontE● $HcontF● $Hq1 $Hq2 $Hsum]"
319 as "Hinv".
320 { iPureIntro. exists 0. split; try done. }
321 clearbody γs.
322 clear γ2_hist1 γ2_hist2 γ2_linked' γ2_venqA' γ2_venqB' γ2_venqC' γ2_vdeqD' γ2_vdeqE' γ2_vdeqF' γ2_contD' γ2_contE' γ2_contF'.
323 iMod (inv_alloc nroot _ (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv".
324
325 pose (P1 := (own (γ2_venqA γs) (◯E {[+ 1 +]}) ∗ own (γ2_linked γs) (◯E true))%I).
326 pose (P2 := own (γ2_venqB γs) (◯E {[+ 2 +]})).
327 pose (P3 := own (γ2_venqC γs) (◯E {[+ 3 +]})).
328 pose (P4 := (∃ nD : nat, own γs.(γ2_contD) (◯E nD) ∗ ⌜nD ≠ 0⌝)%I).
329 pose (P5 := (∃ nE : nat, own γs.(γ2_contE) (◯E nE) ∗ ⌜nE ≠ 0⌝)%I).
330 pose (P6 := (∃ nF : nat, own γs.(γ2_contF) (◯E nF) ∗ ⌜nF ≠ 0⌝)%I).
331
332 wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4 ∗ P5)%I (λ _, P6)%I with "[- HcontF◯ HvdeqF◯] [HcontF◯ HvdeqF◯]").
333 { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4)%I (λ _, P5)%I with "[- HcontE◯ HvdeqE◯] [HcontE◯ HvdeqE◯]").
334 { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3)%I (λ _, P4)%I with "[- HcontD◯ HvdeqD◯] [HcontD◯ HvdeqD◯]").
335 { wp_smart_apply (wp_par (λ _, P1 ∗ P2)%I (λ _, P3)%I with "[- HvenqC◯] [HvenqC◯]").
336 { wp_smart_apply (wp_par (λ _, P1) (λ _, P2) with "[- HvenqB◯] [HvenqB◯]").
337 { awp_apply lqp.(enqueue_spec lq).
338 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
339 iNamedSuffix "H" "_1". iCombine "HvenqA◯ HvenqA●_1" gives %->%excl_auth_agree_L.
340 iCombine "Hlinked●_1 Hlinked◯" gives %->%excl_auth_agree_L.
341 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
342 iIntros "Hq1".
343
344 iMod (mono_list_auth_own_update (hist1 ++ [1]) with "Hhist1●_1") as "[Hhist1●_1 _]".
345 { by apply prefix_app_r. }
346 iCombine "HvenqA●_1 HvenqA◯" as "HvenqA".
347 iMod (own_update with "HvenqA") as "[HvenqA●_1 HvenqA◯]".
348 { apply (excl_auth_update _ _ {[+ 1 +]}). }
349 replace (vals_of_nats vs1 ++ [ #1 ]) with (vals_of_nats (vs1 ++ [1]))
350 by rewrite /vals_of_nats fmap_app //.
351 iModIntro. iFrame "HvenqA◯". iFrame. iFrame "Hq1". iSplit.
352 { iPureIntro. exists ndeq. repeat split; try done.
353 + rewrite list_to_set_disj_app.
354 multiset_solver.
355 + apply Forall_app. by split; last apply Forall_singleton.
356 + etrans; first apply HnDEF_1.
357 apply prefix_submseteq, take_app_prefix.
358 + rewrite ->!length_app in *. lia.
359 + by rewrite drop_app_le // Hhistvs_1. }
360 wp_pures.
361 clear.
362
363 awp_apply lqp.(link_spec lq).
364 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
365 iNamedSuffix "H" "_2".
366 iCombine "Hlinked●_2 Hlinked◯" gives %->%excl_auth_agree_L.
367 rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
368 iExists true. iFrame "Hq1_2 Hq2_2". iSplit.
369 { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro.
370 iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
371 iIntros "Hq1". iMod "Hclose" as "_".
372
373 iCombine "Hlinked●_2 Hlinked◯" as "Hlinked".
374 iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]".
375 { apply (excl_auth_update _ _ true). }
376 iEval (rewrite /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1".
377 iMod (mono_list_auth_own_update (hist1 ++ hist2) with "Hhist1●_2") as "[Hhist1●_2 _]"; first by apply prefix_app_r.
378 iFrame. iModIntro. iModIntro. iPureIntro. exists ndeq. repeat split; try done.
379 - rewrite list_to_set_disj_app. multiset_solver.
380 - by rewrite Forall_app.
381 - etrans; first apply HnDEF_2.
382 apply prefix_submseteq, take_app_prefix.
383 - rewrite length_app. lia.
384 - by rewrite drop_app_le // Hhistvs_2.
385 }
386 { awp_apply lqp.(enqueue_spec lq).
387 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
388 iNamedSuffix "H" "_1". iCombine "HvenqB◯ HvenqB●_1" gives %->%excl_auth_agree_L.
389
390 destruct linked eqn:Hlinked.
391 - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
392 iIntros "Hq1".
393 iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
394 iMod (mono_list_auth_own_update (hist1 ++ [2]) with "Hhist1●_1") as "[Hhist1●_1 _]".
395 { by apply prefix_app_r. }
396 iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
397 { apply (excl_auth_update _ _ {[+ 2 +]}). }
398 replace (vals_of_nats vs1 ++ [ #2 ]) with (vals_of_nats (vs1 ++ [2]))
399 by rewrite /vals_of_nats fmap_app //.
400 iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [2]). iFrame.
401 iPureIntro. repeat split; try done.
402 + rewrite list_to_set_disj_app.
403 multiset_solver
404 + apply Forall_app.
405 + multiset_solver.
406 + apply Forall_app. by split; last apply Forall_singleton.
407 + etrans; first apply HnDEF_1.
408 apply prefix_submseteq, take_app_prefix.
409 + rewrite length_app. lia.
410 + by rewrite drop_app_le // Hhistvs_1.
411 - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
412 iIntros "Hq1".
413 iCombine "HvenqB●_1 HvenqB◯" as "HvenqB".
414 iMod (own_update _ _ (Excl (hist2 ++ [2])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
415 iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]".
416 { apply (excl_auth_update _ _ {[+ 2 +]}). }
417 replace (vals_of_nats hist2 ++ [ #2 ]) with (vals_of_nats (hist2 ++ [2]))
418 by rewrite /vals_of_nats fmap_app //.
419 iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iFrame.
420 iPureIntro. exists ndeq. repeat split; try done.
421 + rewrite list_to_set_disj_app.
422 multiset_solver.
423 + apply Forall_app. split; first done.
424 by apply Forall_singleton.
425 }
426 { by iIntros (_ _) "H !>". }
427 }
428 { awp_apply lqp.(enqueue_spec lq).
429 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
430 iNamedSuffix "H" "_1". iCombine "HvenqC◯ HvenqC●_1" gives %->%excl_auth_agree_L.
431
432 destruct linked eqn:Hlinked.
433 - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. }
434 iIntros "Hq1".
435 iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
436 iMod (mono_list_auth_own_update (hist1 ++ [3]) with "Hhist1●_1") as "[Hhist1●_1 _]".
437 { by apply prefix_app_r. }
438 iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
439 { apply (excl_auth_update _ _ {[+ 3 +]}). }
440 replace (vals_of_nats vs1 ++ [ #3 ]) with (vals_of_nats (vs1 ++ [3]))
441 by rewrite /vals_of_nats fmap_app //.
442 iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [3]). iFrame.
443 iPureIntro. repeat split; try done.
444 + rewrite list_to_set_disj_app.
445 multiset_solver.
446 + multiset_solver.
447 + apply Forall_app. by split; last apply Forall_singleton.
448 + etrans; first apply HnDEF_1.
449 apply prefix_submseteq, take_app_prefix.
450 + rewrite length_app. lia.
451 + by rewrite drop_app_le // Hhistvs_1.
452 - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. }
453 iIntros "Hq1".
454 iCombine "HvenqC●_1 HvenqC◯" as "HvenqC".
455 iMod (own_update _ _ (Excl (hist2 ++ [3])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|].
456 iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]".
457 { apply (excl_auth_update _ _ {[+ 3 +]}). }
458 replace (vals_of_nats hist2 ++ [ #3 ]) with (vals_of_nats (hist2 ++ [3]))
459 by rewrite /vals_of_nats fmap_app //.
460 iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iFrame.
461 iPureIntro. exists ndeq. repeat split; try done.
462 + rewrite list_to_set_disj_app.
463 multiset_solver.
464 + apply Forall_app. split; first done.
465 by apply Forall_singleton.
466 }
467 { iIntros (_ _) "[H1 H2] !>". iFrame. }
468 }
469 { awp_apply (dequeue_spec lq lqp).
470 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
471 iNamedSuffix "H" "_1".
472 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
473 iIntros (v0 vs') "[%Hvs Hq1]".
474 destruct vs1; simplify_eq/=.
475 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
476 iCombine "HcontD◯ HcontD●_1" gives %->%excl_auth_agree_L.
477
478 iCombine "HvdeqD●_1 HvdeqD◯" as "HvdeqD" gives %->%excl_auth_agree_L.
479 iMod (own_update with "HvdeqD") as "[HvdeqD●_1 HvdeqD◯]".
480 { apply (excl_auth_update _ _ (Some n)). }
481
482 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
483 iModIntro. iFrame. iFrameNamed. iSplit.
484 { iPureIntro. exists (S ndeq). repeat split; try done.
485 - etrans; first done.
486 simplify_eq/=. rewrite ->app_nil_r in *.
487 etrans. { apply Permutation_submseteq, Permutation_cons_append. }
488 rewrite (take_S_r _ _ n) //.
489 by apply submseteq_skips_r.
490 - by apply lookup_lt_Some in Hhistndeq_1. }
491
492 clear - Hhistndeq_1 Hhistvs_1.
493 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
494 iNamedSuffix "H" "_2".
495 wp_faa.
496
497 iCombine "HcontD●_2 HcontD◯" as "HcontD" gives %->%excl_auth_agree_L.
498 iMod (own_update with "HcontD") as "[HcontD●_2 HcontD◯]".
499 { apply (excl_auth_update _ _ n). }
500
501 iEval (rewrite Z.add_0_l Z.add_comm Z.add_assoc) in "Hsum_2".
502
503 iCombine "HvdeqD●_2 HvdeqD◯" gives %->%excl_auth_agree_L.
504
505 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
506 assert (Hn : n ≠ 0).
507 { eapply (Forall_lookup (.≠ 0)); last done.
508 by eapply Forall_prefix. }
509
510 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
511 iPureIntro. exists ndeq'. repeat split; try done.
512 by rewrite /option_nat option_guard_True.
513 }
514 { iIntros (_ _) "[H1 H2] !>". iFrame. }
515 }
516 { awp_apply (dequeue_spec lq lqp).
517 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
518 iNamedSuffix "H" "_1".
519 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
520 iIntros (v0 vs') "[%Hvs Hq1]".
521 destruct vs1; simplify_eq/=.
522 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
523 iCombine "HcontE◯ HcontE●_1" gives %->%excl_auth_agree_L.
524
525 iCombine "HvdeqE●_1 HvdeqE◯" as "HvdeqE" gives %->%excl_auth_agree_L.
526 iMod (own_update with "HvdeqE") as "[HvdeqE●_1 HvdeqE◯]".
527 { apply (excl_auth_update _ _ (Some n)). }
528
529 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
530 iModIntro. iFrame. iFrameNamed. iSplit.
531 { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
532 - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
533 rewrite app_nil_r.
534 etrans. { apply submseteq_skips_l, Permutation_submseteq, Permutation_cons_append. }
535 rewrite (take_S_r _ _ n) // app_assoc.
536 by apply submseteq_skips_r.
537 - by apply lookup_lt_Some in Hhistndeq_1. }
538
539 clear - Hhistndeq_1 Hhistvs_1.
540 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
541 iNamedSuffix "H" "_2".
542 wp_faa.
543
544 iCombine "HcontE●_2 HcontE◯" as "HcontE" gives %->%excl_auth_agree_L.
545 iMod (own_update with "HcontE") as "[HcontE●_2 HcontE◯]".
546 { apply (excl_auth_update _ _ n). }
547
548 iEval (rewrite Z.add_0_r -Z.add_assoc [(nF + n)%Z]Z.add_comm Z.add_assoc) in "Hsum_2".
549
550 iCombine "HvdeqE●_2 HvdeqE◯" gives %->%excl_auth_agree_L.
551
552 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
553 assert (Hn : n ≠ 0).
554 { eapply (Forall_lookup (.≠ 0)); last done.
555 by eapply Forall_prefix. }
556
557 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
558 iPureIntro. exists ndeq'. repeat split; try done.
559 by rewrite /option_nat option_guard_True.
560 }
561 { iIntros (_ _) "[H1 H2] !>". iFrame. }
562 }
563 { awp_apply (dequeue_spec lq lqp).
564 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H".
565 iNamedSuffix "H" "_1".
566 iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. }
567 iIntros (v0 vs') "[%Hvs Hq1]".
568 destruct vs1; simplify_eq/=.
569 iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1".
570 iCombine "HcontF◯ HcontF●_1" gives %->%excl_auth_agree_L.
571
572 iCombine "HvdeqF●_1 HvdeqF◯" as "HvdeqF" gives %->%excl_auth_agree_L.
573 iMod (own_update with "HvdeqF") as "[HvdeqF●_1 HvdeqF◯]".
574 { apply (excl_auth_update _ _ (Some n)). }
575
576 apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1].
577 iModIntro. iFrame. iFrameNamed. iSplit.
578 { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done.
579 - simplify_eq/=. rewrite app_nil_r in HnDEF_1.
580 rewrite (take_S_r _ _ n) // app_assoc.
581 by apply submseteq_skips_r.
582 - by apply lookup_lt_Some in Hhistndeq_1. }
583
584 clear - Hhistndeq_1 Hhistvs_1.
585 iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H".
586 iNamedSuffix "H" "_2".
587 wp_faa.
588
589 iCombine "HcontF●_2 HcontF◯" as "HcontF" gives %->%excl_auth_agree_L.
590 iMod (own_update with "HcontF") as "[HcontF●_2 HcontF◯]".
591 { apply (excl_auth_update _ _ n). }
592
593 iEval (rewrite Z.add_0_r) in "Hsum_2".
594
595 iCombine "HvdeqF●_2 HvdeqF◯" gives %->%excl_auth_agree_L.
596
597 iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre].
598 assert (Hn : n ≠ 0).
599 { eapply (Forall_lookup (.≠ 0)); last done.
600 by eapply Forall_prefix. }
601
602 iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro.
603 iPureIntro. exists ndeq'. repeat split; try done.
604 by rewrite /option_nat option_guard_True.
605 }
606
607 iIntros (v1 v2) "[(H1 & HvenqB◯ & HvenqC◯ & H4 & H5) H6]".
608 unfold P1, P2, P3, P4, P5, P6. clear P1 P2 P3 P4 P5 P6.
609 iDestruct "H1" as "[HvenqA◯ Hlinked◯]".
610 iDestruct "H4" as "(%nD' & HnD'◯ & %HcontD)".
611 iDestruct "H5" as "(%nE' & HnE'◯ & %HcontE)".
612 iDestruct "H6" as "(%nF' & HnF'◯ & %HcontF)".
613 iModIntro. wp_pures.
614
615 iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">@".
616 wp_load. iModIntro. iSplit; [by iFrame; iExists ndeq|].
617 iCombine "HnD'◯ HcontD●" gives %<-%excl_auth_agree_L. iClear "HnD'◯ HcontD●".
618 iCombine "HnE'◯ HcontE●" gives %<-%excl_auth_agree_L. iClear "HnE'◯ HcontE●".
619 iCombine "HnF'◯ HcontF●" gives %<-%excl_auth_agree_L. iClear "HnF'◯ HcontF●".
620
621 rewrite /option_nat !option_guard_True // in HD HE HF.
622 apply option_le_inv in HD as [HD|<-]; first done.
623 apply option_le_inv in HE as [HE|<-]; first done.
624 apply option_le_inv in HF as [HF|<-]; first done.
625 simplify_eq/=.
626
627 iCombine "Hlinked● Hlinked◯" gives %->%excl_auth_agree_L.
628 iClear "Hq2 Hlinked● Hlinked◯".
629
630 iCombine "HvenqA● HvenqA◯" gives %->%excl_auth_agree_L. iClear "HvenqA◯ HvenqA●".
631 iCombine "HvenqB● HvenqB◯" gives %->%excl_auth_agree_L. iClear "HvenqB◯ HvenqB●".
632 iCombine "HvenqC● HvenqC◯" gives %->%excl_auth_agree_L. iClear "HvenqC◯ HvenqC●".
633 iPureIntro. enough (nD + nE + nF = 6). { do 2 f_equal. lia. }
634
635 assert (ndeq ≥ 3 ∧ length hist1 ≥ 3) as [Hndeq' Hhist1'].
636 { apply submseteq_length in HnDEF as Hndeq'.
637 rewrite /= length_take in Hndeq'. lia. }
638 apply gmultiset_subseteq_size in Hhist1 as Hhist1''.
639 rewrite list_to_set_disj_size !gmultiset_size_disj_union !gmultiset_size_singleton /= in Hhist1''.
640 have {Hhist1''}Hhist1' : length hist1 = 3 by lia.
641 apply gmultiset_subseteq_size_eq in Hhist1; last first.
642 { rewrite !gmultiset_size_disj_union !gmultiset_size_singleton /= list_to_set_disj_size. lia. }
643
644 assert (HnDEF' : [nD; nE; nF] ≡ₚ hist1).
645 { apply submseteq_length_Permutation; last (simpl; lia).
646 etrans; [apply HnDEF | apply submseteq_take]. }
647
648 assert (Hhist1'' : hist1 ≡ₚ elements ({[+ 1; 2; 3 +]} : gmultiset nat)).
649 { erewrite elements_list_to_set_disj_perm.
650 by rewrite Hhist1. }
651
652 assert (H123 : elements ({[+ 1; 2; 3 +]} : gmultiset nat) ≡ₚ [1; 2; 3]).
653 { by rewrite !gmultiset_elements_disj_union !gmultiset_elements_singleton /=. }
654
655 trans (foldr Nat.add 0 [nD; nE; nF]). { simpl. lia. }
656 by rewrite HnDEF' Hhist1'' H123.
657 Qed.
658
659End proofs.
660
661Definition fq := fin_queue_proof.fin_queue_hl.
662Definition lq := lmpmc_queue_proof.lmpmc_queue_hl fq.
663
664(** First example *)
665
666Definition simple_clientΣ : gFunctors := #[ heapΣ; fin_queue_proof.fin_queueΣ ].
667Lemma simple_client_adequate σ : adequate NotStuck (simple_example_2_1 lq) σ (λ v _, v = (#10, #20)%V).
668Proof.
669 eapply (heap_adequacy simple_clientΣ). iIntros (?) "_". iApply simple_example_2_1_safe.
670 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
671Qed.
672
673(** Second example *)
674
675Definition simple_mt_clientΣ : gFunctors :=
676 #[ heapΣ; spawnΣ;
677 fin_queue_proof.fin_queueΣ;
678 GFunctor (excl_authRF boolO);
679 GFunctor (excl_authRF (listO natO)) ].
680
681Instance smc_inG_excl_auth_bool Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR boolO).
682Proof. solve_inG. Qed.
683Instance smc_inG_excl_auth_nat_list Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR (listO natO)).
684Proof. solve_inG. Qed.
685
686Lemma simple_mt_client_adequate σ : adequate NotStuck (simple_example_2_2 lq) σ (λ v _, v = (#10, #20)%V).
687Proof.
688 eapply (heap_adequacy simple_mt_clientΣ). iIntros (?) "_". iApply simple_example_2_2_safe.
689 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
690Qed.
691
692(** Third example *)
693
694Definition mt_example_1Σ : gFunctors :=
695 #[ heapΣ; spawnΣ;
696 fin_queue_proof.fin_queueΣ;
697 mono_listΣ natO;
698 GFunctor (excl_authRF (gmultisetO nat));
699 GFunctor (excl_authRF natO);
700 GFunctor (excl_authRF boolO);
701 GFunctor (excl_authRF (optionO natO));
702 GFunctor (exclR (listO natO)) ].
703
704Instance me_inG_excl_auth_multiset Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (gmultisetO nat)).
705Proof. solve_inG. Qed.
706Instance me_inG_excl_auth_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR natO).
707Proof. solve_inG. Qed.
708Instance me_inG_excl_auth_bool Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR boolO).
709Proof. solve_inG. Qed.
710Instance me_inG_excl_auth_option_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (optionO natO)).
711Proof. solve_inG. Qed.
712Instance me_inG_excl_list_nat Σ : subG mt_example_1Σ Σ → inG Σ (exclR (listO natO)).
713Proof. solve_inG. Qed.
714
715Lemma mt_example_1_adequate σ : adequate NotStuck (mt_example_1 lq) σ (λ v _, v = #6%V).
716Proof.
717 eapply (heap_adequacy mt_example_1Σ). iIntros (?) "_". iApply mt_example_1_safe.
718 Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris.
719Qed.
720
721Print Assumptions simple_client_adequate.
722Print Assumptions simple_mt_client_adequate.
723Print Assumptions mt_example_1_adequate.
generated by cgit v1.3 (git 2.53.0) at 2026-06-25 21:01:51 +0000