From e2681e43cc7849d66425d5bc93565e9e177d229a Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 24 Jun 2026 19:29:28 +0200 Subject: Initial commit --- theories/example.v | 723 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 723 insertions(+) create mode 100644 theories/example.v (limited to 'theories/example.v') 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 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode adequacy. +From iris.algebra Require Import list gmultiset. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants mono_list. +From iris_named_props Require Import custom_syntax. +From iris.heap_lang.lib Require Import assert par. + +From lmpmc Require lmpmc_queue_spec lmpmc_queue_proof fin_queue_proof lmpmc_blocking_dequeue. +From lmpmc Require Import upstream. + +Definition somes {A} (xs : list (option A)) : list A := xs ≫= option_list. +Definition option_le {A} (mx my : option A) := option_relation (=) (const False) (const True) mx my. +Definition option_nat (x : nat) : option nat := guard (x ≠ 0);; Some x. +Definition vals_of_nats : list nat → list val := fmap (LitV ∘ LitInt ∘ Z.of_nat). + +Lemma option_le_None {A} (x : A) : option_le None (Some x). +Proof. done. Qed. +Lemma option_le_Some {A} (x : A) : option_le (Some x) (Some x). +Proof. done. Qed. +Lemma option_le_inv {A} (mx my : option A) : option_le mx my → mx = None ∨ mx = my. +Proof. induction mx, my; intros ?; simplify_eq/=; done || (by right) || by left. Qed. + +#[global] Instance timeless_if_bool {PROP : bi} {b : bool} {Q R : PROP} : Timeless Q → Timeless R → Timeless (if b then Q else R). +Proof. by destruct b. Qed. + +Section hl. + Context (lq : lmpmc_queue_spec.lmpmc_queue_hl). + Import lmpmc_blocking_dequeue lmpmc_queue_spec. + + Notation "'let2:' x1 , x2 := e1 'in' e2" := + (Lam (BNamed x2) (Lam (BNamed x1) (Lam (BNamed x2) e2 (Snd (Var x2))) (Fst (Var x2))) e1)%E + (at level 200, x1, x2 at level 1, e1, e2 at level 200, + format "'[' 'let2:' x1 ',' x2 := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. + + Definition simple_example_2_1 : expr := + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + lq.(enqueue) "ℓ_enq1" #10;; + lq.(link) "ℓ_enq1" "ℓ_deq2";; + lq.(enqueue) "ℓ_enq2" #20;; + let: "x" := dequeue lq "ℓ_deq1" in + let: "y" := dequeue lq "ℓ_deq1" in + ("x", "y"). + + Definition simple_example_2_2 : expr := + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + (( lq.(enqueue) "ℓ_enq1" #10;; + lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *) + ||| lq.(enqueue) "ℓ_enq2" #20 (* thread B *) + );; + let: "x" := dequeue lq "ℓ_deq1" in + let: "y" := dequeue lq "ℓ_deq1" in + ("x", "y"). + + Definition mt_example_1 : expr := + let: "ℓ_sum" := Alloc #0 in + let2: "ℓ_deq1", "ℓ_enq1" := lq.(new) #() in + let2: "ℓ_deq2", "ℓ_enq2" := lq.(new) #() in + (( lq.(enqueue) "ℓ_enq1" #1;; + lq.(link) "ℓ_enq1" "ℓ_deq2") (* thread A *) + ||| lq.(enqueue) "ℓ_enq2" #2 (* thread B *) + ||| lq.(enqueue) "ℓ_enq2" #3 (* thread C *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread D *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread E *) + ||| FAA "ℓ_sum" (dequeue lq "ℓ_deq1") (* thread F *) + );; + ! "ℓ_sum". + +End hl. + +Section proofs. + Context `{!heapGS Σ, !spawnG Σ, + !mono_listG natO Σ, + !inG Σ (excl_authR (gmultisetO nat)), + !inG Σ (excl_authR natO), + !inG Σ (excl_authR boolO), + !inG Σ (excl_authR (listO natO)), + !inG Σ (excl_authR (optionO natO)), + !inG Σ (exclR (listO natO))}. + Context {lq : lmpmc_queue_spec.lmpmc_queue_hl} + {lqp : lmpmc_queue_spec.lmpmc_queue_iris Σ lq}. + Import lmpmc_blocking_dequeue lmpmc_queue_spec. + + Lemma simple_example_2_1_safe : + ⊢ WP simple_example_2_1 lq {{ v, ⌜v = (#10, #20)%V⌝ }}. + Proof. + iUnfold simple_example_2_1. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + awp_apply lqp.(enqueue_spec lq). iAaccIntro with "Hq1"; iIntros "Hq1"; first by iFrame. + simpl. iModIntro. wp_pures. + awp_apply lqp.(link_spec lq). + rewrite /atomic_acc /=. + iExists true. iFrame. + iApply fupd_mask_intro; first done. + iIntros "Hupd". iSplit. { iIntros "[? ?]". iFrame. } + iIntros "Hq". simpl. iMod "Hupd" as "_". iModIntro. + wp_pures. awp_apply lqp.(enqueue_spec lq). + iAaccIntro with "Hq"; iIntros "Hq"; first by iFrame. + simpl. + + iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp). + iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame. + iIntros (? ?) "[%Hvs Hq]". iSimplifyEq. + iModIntro. wp_pures. awp_apply (dequeue_spec lq lqp). + iAaccIntro with "Hq"; first by iIntros "Hq"; iFrame. + iIntros (? ?) "[%Hvs Hq]". iSimplifyEq. + + iModIntro. by wp_pures. + Qed. + + Record smp_gstate := + SmpGstate + { γ1_linked : gname; (* (●E) whether Q1 and Q2 have been linked already *) + γ1_contA : gname; (* (●E) (list nat) contribution of thread A *) + γ1_contB : gname; (* (●E) (list nat) contribution of thread B *) + }. + + Definition smp_inv γs (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ := + ∃ (linked : bool) (contA contB : list nat), + ("Hlinked●" ∷ own γs.(γ1_linked) (●E linked)) ∗ + ("HcontA●" ∷ own γs.(γ1_contA) (●E contA)) ∗ + ("HcontB●" ∷ own γs.(γ1_contB) (●E contB)) ∗ + ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats (if linked then contA ++ contB else contA))) ∗ + ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats contB)). + + Lemma simple_example_2_2_safe : + ⊢ WP simple_example_2_2 lq {{ v, ⌜v = (#10, #20)%V⌝ }}. + Proof. + iUnfold simple_example_2_2. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + + iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contA') "[HcontA● HcontA◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E [] ⋅ ◯E [])) as (γ1_contB') "[HcontB● HcontB◯]"; first apply excl_auth_valid. + + pose γs := SmpGstate γ1_linked' γ1_contA' γ1_contB'. + replace γ1_linked' with γs.(γ1_linked) by done. + replace γ1_contA' with γs.(γ1_contA) by done. + replace γ1_contB' with γs.(γ1_contB) by done. + clearbody γs. clear γ1_linked' γ1_contA' γ1_contB'. + iAssert (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "[$]" as "Hinv". + iMod (inv_alloc nroot _ (smp_inv γs ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv". + + wp_smart_apply (wp_par (λ _, own γs.(γ1_linked) (◯E true) ∗ own γs.(γ1_contA) (◯E [10]))%I + (λ _, own γs.(γ1_contB) (◯E [20])) + with "[Hlinked◯ HcontA◯] [HcontB◯]"). + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq1_1". + iCombine "HcontA●_1 HcontA◯" as "HcontA". + iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]". + { apply (excl_auth_update _ _ [10]). } + iIntros "!>". + iSimplifyEq. replace ([ #10 ] : list val) with (vals_of_nats [10]) by done. + iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". wp_pures. clear contB. + + awp_apply lqp.(link_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L. + rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose". + iExists true. iFrame "Hq1_2 Hq2_2". iSplit. + { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. do 2 iFrame. } + iIntros "Hq1". iMod "Hclose" as "_". + iCombine "Hlinked●_2 Hlinked◯" as "Hlinked". + iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]". + { apply (excl_auth_update _ _ true). } + iFrame "Hlinked●_2 HcontA●_2 HcontB●_2 Hq1". by iFrame. } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L. + destruct linked eqn:Hlinked. + { iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq1_1". + iCombine "HcontB◯ HcontB●_1" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]". + { apply (excl_auth_update _ _ [20]). } + iIntros "!>". + iSimplifyEq. + replace [ #20 ] with (vals_of_nats [20]) by done. + iEval (rewrite app_nil_r /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1_1". + by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1". } + { iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". by iFrame. } + iIntros "Hq2_1". + iCombine "HcontB◯ HcontB●_1" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_1 HcontB◯]". + { apply (excl_auth_update _ _ [20]). } + iIntros "!>". + iSimplifyEq. + replace [ #20 ] with (vals_of_nats [20]) by done. + by iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1_1 Hq2_1". } } + { iIntros (v1 v2) "[[Hlinked◯ HcontA◯] HcontB◯]". + iModIntro. wp_pures. clear v1 v2. + awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_1". + iCombine "Hlinked◯ Hlinked●_1" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_1" gives %->%excl_auth_agree_L. + iCombine "HcontB◯ HcontB●_1" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros (v0 vs) "[%Hvs Hq1]". + simpl in Hvs. injection Hvs as <- <-. + replace [ #20%nat ] with (vals_of_nats [20]) by done. + iCombine "HcontA●_1 HcontA◯" as "HcontA". + iMod (own_update with "HcontA") as "[HcontA●_1 HcontA◯]". + { apply (excl_auth_update _ _ []). } + iIntros "!>". + iFrame "Hlinked●_1 HcontB●_1 HcontA●_1 Hq1". wp_pures. + + awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (linked contA contB) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked◯ Hlinked●_2" gives %->%excl_auth_agree_L. + iCombine "HcontA◯ HcontA●_2" gives %->%excl_auth_agree_L. + iCombine "HcontB◯ HcontB●_2" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_2". { iIntros "Hq1 !>". iFrame. iIntros "!>". by iFrame. } + iIntros (v0 vs) "[%Hvs Hq1]". + simpl in Hvs. injection Hvs as <- <-. + replace [ #20%nat ] with (vals_of_nats [20]) by done. + iCombine "HcontB●_2 HcontB◯" as "HcontB". + iMod (own_update with "HcontB") as "[HcontB●_2 HcontB◯]". + { apply (excl_auth_update _ _ []). } + iIntros "!>". + iFrame "Hlinked●_2 HcontB●_2 HcontA●_2 Hq1". wp_pures. + done. } + Qed. + + Record mt_gstate := + Gstate + { γ2_hist1 : gname; (* (●ML) (list nat) succesfully enqueued items (Q1) *) + γ2_hist2 : gname; (* (●E ) (list nat) sucessfully enqueued items (Q2) *) + γ2_linked : gname; (* (●E ) (bool) whether Q1 and Q2 have been linked *) + γ2_venqA : gname; (* (●E ) (gmultiset nat) of items enqueued by thread A *) + γ2_venqB : gname; (* (●E ) (gmultiset nat) of items enqueued by thread B *) + γ2_venqC : gname; (* (●E ) (gmultiset nat) of items enqueued by thread C *) + γ2_vdeqD : gname; (* (●E ) (option nat) poised contribution of first dequeueing thread *) + γ2_vdeqE : gname; (* (●E ) (option nat) poised contribution of second dequeueing thread *) + γ2_vdeqF : gname; (* (●E ) (option nat) poised contribution of third dequeueing thread *) + γ2_contD : gname; (* (●E ) (nat) as-is contribution of first dequeueing thread *) + γ2_contE : gname; (* (●E ) (nat) as-is contribution of second dequeueing thread *) + γ2_contF : gname; (* (●E ) (nat) as-is contribution of third dequeueing thread *) + }. + + Definition mt_inv γs ℓ_sum (ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2 : loc) : iProp Σ := + ∃ (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), + ("Hq1" ∷ lqp.(queue_repr lq) ℓ_deq1 (if linked then ℓ_enq2 else ℓ_enq1) (vals_of_nats vs1)) ∗ + ("Hq2" ∷ if linked then True else lqp.(queue_repr lq) ℓ_deq2 ℓ_enq2 (vals_of_nats hist2)) ∗ + ("Hhist1●" ∷ γs.(γ2_hist1) ↪●ML hist1) ∗ + ("Hhist2E" ∷ own γs.(γ2_hist2) (Excl hist2)) ∗ + ("Hlinked●" ∷ own γs.(γ2_linked) (●E linked)) ∗ + ("HvenqA●" ∷ own γs.(γ2_venqA) (●E ecsA)) ∗ + ("HvenqB●" ∷ own γs.(γ2_venqB) (●E ecsB)) ∗ + ("HvenqC●" ∷ own γs.(γ2_venqC) (●E ecsC)) ∗ + ("HvdeqD●" ∷ own γs.(γ2_vdeqD) (●E npD)) ∗ + ("HvdeqE●" ∷ own γs.(γ2_vdeqE) (●E npE)) ∗ + ("HvdeqF●" ∷ own γs.(γ2_vdeqF) (●E npF)) ∗ + ("HcontD●" ∷ own γs.(γ2_contD) (●E nD)) ∗ + ("HcontE●" ∷ own γs.(γ2_contE) (●E nE)) ∗ + ("HcontF●" ∷ own γs.(γ2_contF) (●E nF)) ∗ + ("Hsum" ∷ ℓ_sum ↦ #(nD + nE + nF)) ∗ + ("%Hhist1" ∷ ⌜list_to_set_disj hist1 ⊆ if linked then ecsA ⊎ ecsB ⊎ ecsC else ecsA⌝) ∗ + ("%Hhist2" ∷ ⌜list_to_set_disj hist2 ⊆ ecsB ⊎ ecsC⌝) ∗ + ("%Hhist1n0" ∷ ⌜Forall (.≠ 0) hist1⌝) ∗ + ("%Hhist2n0" ∷ ⌜Forall (.≠ 0) hist2⌝) ∗ + ("%HnDEF" ∷ ⌜somes [npD; npE; npF] ⊆+ take ndeq hist1⌝) ∗ + ("%HD" ∷ ⌜option_le (option_nat nD) npD⌝) ∗ + ("%HE" ∷ ⌜option_le (option_nat nE) npE⌝) ∗ + ("%HF" ∷ ⌜option_le (option_nat nF) npF⌝) ∗ + ("%Hndeq" ∷ ⌜ndeq ≤ length hist1⌝) ∗ + ("%Hhistvs" ∷ ⌜drop ndeq hist1 = vs1⌝). + + (* Post, we expect: + linked = true + nD, nE, nF ≠ 0 (hence npD, npE, npF ≠ None and all are unique, adding up to 6) *) + + Lemma mt_example_1_safe : + ⊢ WP mt_example_1 lq {{ v, ⌜v = #6⌝ }}. + Proof. + iUnfold mt_example_1. + wp_alloc ℓ_sum as "Hsum". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq1 %ℓ_enq1 Hq1". wp_pures. + wp_apply (lqp.(new_spec lq) with "[//]") as "%ℓ_deq2 %ℓ_enq2 Hq2". wp_pures. + iEval (replace [] with (vals_of_nats [])) in "Hq1 Hq2". + iMod (mono_list_own_alloc []) as "[%γ2_hist1 [Hhist1● _]]". + iMod (own_alloc (Excl [])) as "[%γ2_hist2 Hhist2E]"; first done. + iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2_linked') "[Hlinked● Hlinked◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqA') "[HvenqA● HvenqA◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqB') "[HvenqB● HvenqB◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E ∅ ⋅ ◯E ∅)) as (γ2_venqC') "[HvenqC● HvenqC◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqD' [HvdeqD● HvdeqD◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqE' [HvdeqE● HvdeqE◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E None ⋅ ◯E None)) as "[%γ2_vdeqF' [HvdeqF● HvdeqF◯]]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contD') "[HcontD● HcontD◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contE') "[HcontE● HcontE◯]"; first apply excl_auth_valid. + iMod (own_alloc (●E 0 ⋅ ◯E 0)) as (γ2_contF') "[HcontF● HcontF◯]"; first apply excl_auth_valid. + 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'. + replace γ2_linked' with γs.(γ2_linked) by done. + replace γ2_venqA' with γs.(γ2_venqA) by done. + replace γ2_venqB' with γs.(γ2_venqB) by done. + replace γ2_venqC' with γs.(γ2_venqC) by done. + replace γ2_vdeqD' with γs.(γ2_vdeqD) by done. + replace γ2_vdeqE' with γs.(γ2_vdeqE) by done. + replace γ2_vdeqF' with γs.(γ2_vdeqF) by done. + replace γ2_contD' with γs.(γ2_contD) by done. + replace γ2_contE' with γs.(γ2_contE) by done. + replace γ2_contF' with γs.(γ2_contF) by done. + iAssert (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) + with "[$Hhist1● $Hhist2E $Hlinked● $HvenqA● $HvenqB● $HvenqC● $HvdeqD● $HvdeqE● $HvdeqF● $HcontD● $HcontE● $HcontF● $Hq1 $Hq2 $Hsum]" + as "Hinv". + { iPureIntro. exists 0. split; try done. } + clearbody γs. + 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'. + iMod (inv_alloc nroot _ (mt_inv γs ℓ_sum ℓ_deq1 ℓ_enq1 ℓ_deq2 ℓ_enq2) with "Hinv") as "#Hinv". + + pose (P1 := (own (γ2_venqA γs) (◯E {[+ 1 +]}) ∗ own (γ2_linked γs) (◯E true))%I). + pose (P2 := own (γ2_venqB γs) (◯E {[+ 2 +]})). + pose (P3 := own (γ2_venqC γs) (◯E {[+ 3 +]})). + pose (P4 := (∃ nD : nat, own γs.(γ2_contD) (◯E nD) ∗ ⌜nD ≠ 0⌝)%I). + pose (P5 := (∃ nE : nat, own γs.(γ2_contE) (◯E nE) ∗ ⌜nE ≠ 0⌝)%I). + pose (P6 := (∃ nF : nat, own γs.(γ2_contF) (◯E nF) ∗ ⌜nF ≠ 0⌝)%I). + + wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4 ∗ P5)%I (λ _, P6)%I with "[- HcontF◯ HvdeqF◯] [HcontF◯ HvdeqF◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3 ∗ P4)%I (λ _, P5)%I with "[- HcontE◯ HvdeqE◯] [HcontE◯ HvdeqE◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2 ∗ P3)%I (λ _, P4)%I with "[- HcontD◯ HvdeqD◯] [HcontD◯ HvdeqD◯]"). + { wp_smart_apply (wp_par (λ _, P1 ∗ P2)%I (λ _, P3)%I with "[- HvenqC◯] [HvenqC◯]"). + { wp_smart_apply (wp_par (λ _, P1) (λ _, P2) with "[- HvenqB◯] [HvenqB◯]"). + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqA◯ HvenqA●_1" gives %->%excl_auth_agree_L. + iCombine "Hlinked●_1 Hlinked◯" gives %->%excl_auth_agree_L. + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + + iMod (mono_list_auth_own_update (hist1 ++ [1]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iCombine "HvenqA●_1 HvenqA◯" as "HvenqA". + iMod (own_update with "HvenqA") as "[HvenqA●_1 HvenqA◯]". + { apply (excl_auth_update _ _ {[+ 1 +]}). } + replace (vals_of_nats vs1 ++ [ #1 ]) with (vals_of_nats (vs1 ++ [1])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqA◯". iFrame. iFrame "Hq1". iSplit. + { iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite ->!length_app in *. lia. + + by rewrite drop_app_le // Hhistvs_1. } + wp_pures. + clear. + + awp_apply lqp.(link_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_2". + iCombine "Hlinked●_2 Hlinked◯" gives %->%excl_auth_agree_L. + rewrite /atomic_acc /=. iApply fupd_mask_intro; first set_solver. iIntros "Hclose". + iExists true. iFrame "Hq1_2 Hq2_2". iSplit. + { iIntros "[Hq1 Hq2]". iMod "Hclose" as "_". iModIntro. + iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". iMod "Hclose" as "_". + + iCombine "Hlinked●_2 Hlinked◯" as "Hlinked". + iMod (own_update with "Hlinked") as "[Hlinked●_2 Hlinked◯]". + { apply (excl_auth_update _ _ true). } + iEval (rewrite /vals_of_nats -fmap_app -/vals_of_nats) in "Hq1". + iMod (mono_list_auth_own_update (hist1 ++ hist2) with "Hhist1●_2") as "[Hhist1●_2 _]"; first by apply prefix_app_r. + iFrame. iModIntro. iModIntro. iPureIntro. exists ndeq. repeat split; try done. + - rewrite list_to_set_disj_app. multiset_solver. + - by rewrite Forall_app. + - etrans; first apply HnDEF_2. + apply prefix_submseteq, take_app_prefix. + - rewrite length_app. lia. + - by rewrite drop_app_le // Hhistvs_2. + } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqB◯ HvenqB●_1" gives %->%excl_auth_agree_L. + + destruct linked eqn:Hlinked. + - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + iCombine "HvenqB●_1 HvenqB◯" as "HvenqB". + iMod (mono_list_auth_own_update (hist1 ++ [2]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]". + { apply (excl_auth_update _ _ {[+ 2 +]}). } + replace (vals_of_nats vs1 ++ [ #2 ]) with (vals_of_nats (vs1 ++ [2])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [2]). iFrame. + iPureIntro. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver + + apply Forall_app. + + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite length_app. lia. + + by rewrite drop_app_le // Hhistvs_1. + - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. } + iIntros "Hq1". + iCombine "HvenqB●_1 HvenqB◯" as "HvenqB". + iMod (own_update _ _ (Excl (hist2 ++ [2])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|]. + iMod (own_update with "HvenqB") as "[HvenqB●_1 HvenqB◯]". + { apply (excl_auth_update _ _ {[+ 2 +]}). } + replace (vals_of_nats hist2 ++ [ #2 ]) with (vals_of_nats (hist2 ++ [2])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqB◯". iModIntro. iFrame. iFrame. + iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. split; first done. + by apply Forall_singleton. + } + { by iIntros (_ _) "H !>". } + } + { awp_apply lqp.(enqueue_spec lq). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". iCombine "HvenqC◯ HvenqC●_1" gives %->%excl_auth_agree_L. + + destruct linked eqn:Hlinked. + - iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. iIntros "!>". iExists ndeq, vs1. by iFrame. } + iIntros "Hq1". + iCombine "HvenqC●_1 HvenqC◯" as "HvenqC". + iMod (mono_list_auth_own_update (hist1 ++ [3]) with "Hhist1●_1") as "[Hhist1●_1 _]". + { by apply prefix_app_r. } + iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]". + { apply (excl_auth_update _ _ {[+ 3 +]}). } + replace (vals_of_nats vs1 ++ [ #3 ]) with (vals_of_nats (vs1 ++ [3])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iExists ndeq, (vs1 ++ [3]). iFrame. + iPureIntro. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + multiset_solver. + + apply Forall_app. by split; last apply Forall_singleton. + + etrans; first apply HnDEF_1. + apply prefix_submseteq, take_app_prefix. + + rewrite length_app. lia. + + by rewrite drop_app_le // Hhistvs_1. + - iAaccIntro with "Hq2_1". { iIntros "Hq2 !>". iFrame. iIntros "!>". iExists ndeq. by iFrame. } + iIntros "Hq1". + iCombine "HvenqC●_1 HvenqC◯" as "HvenqC". + iMod (own_update _ _ (Excl (hist2 ++ [3])) with "Hhist2E_1") as "Hhist2E_1"; first by intros ? [[]|]. + iMod (own_update with "HvenqC") as "[HvenqC●_1 HvenqC◯]". + { apply (excl_auth_update _ _ {[+ 3 +]}). } + replace (vals_of_nats hist2 ++ [ #3 ]) with (vals_of_nats (hist2 ++ [3])) + by rewrite /vals_of_nats fmap_app //. + iModIntro. iFrame "HvenqC◯". iModIntro. iFrame. iFrame. + iPureIntro. exists ndeq. repeat split; try done. + + rewrite list_to_set_disj_app. + multiset_solver. + + apply Forall_app. split; first done. + by apply Forall_singleton. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontD◯ HcontD●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqD●_1 HvdeqD◯" as "HvdeqD" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqD") as "[HvdeqD●_1 HvdeqD◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. + - etrans; first done. + simplify_eq/=. rewrite ->app_nil_r in *. + etrans. { apply Permutation_submseteq, Permutation_cons_append. } + rewrite (take_S_r _ _ n) //. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontD●_2 HcontD◯" as "HcontD" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontD") as "[HcontD●_2 HcontD◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_l Z.add_comm Z.add_assoc) in "Hsum_2". + + iCombine "HvdeqD●_2 HvdeqD◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontE◯ HcontE●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqE●_1 HvdeqE◯" as "HvdeqE" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqE") as "[HvdeqE●_1 HvdeqE◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done. + - simplify_eq/=. rewrite app_nil_r in HnDEF_1. + rewrite app_nil_r. + etrans. { apply submseteq_skips_l, Permutation_submseteq, Permutation_cons_append. } + rewrite (take_S_r _ _ n) // app_assoc. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontE●_2 HcontE◯" as "HcontE" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontE") as "[HcontE●_2 HcontE◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_r -Z.add_assoc [(nF + n)%Z]Z.add_comm Z.add_assoc) in "Hsum_2". + + iCombine "HvdeqE●_2 HvdeqE◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + { iIntros (_ _) "[H1 H2] !>". iFrame. } + } + { awp_apply (dequeue_spec lq lqp). + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">H". + iNamedSuffix "H" "_1". + iAaccIntro with "Hq1_1". { iIntros "Hq1 !>". iFrame. by iExists ndeq. } + iIntros (v0 vs') "[%Hvs Hq1]". + destruct vs1; simplify_eq/=. + iPoseProof (mono_list_lb_own_get with "Hhist1●_1") as "#Hhist1◯_1". + iCombine "HcontF◯ HcontF●_1" gives %->%excl_auth_agree_L. + + iCombine "HvdeqF●_1 HvdeqF◯" as "HvdeqF" gives %->%excl_auth_agree_L. + iMod (own_update with "HvdeqF") as "[HvdeqF●_1 HvdeqF◯]". + { apply (excl_auth_update _ _ (Some n)). } + + apply drop_cons_inv in Hhistvs_1 as [Hhistndeq_1 Hhistvs_1]. + iModIntro. iFrame. iFrameNamed. iSplit. + { iPureIntro. exists (S ndeq). repeat split; try done. etrans; first done. + - simplify_eq/=. rewrite app_nil_r in HnDEF_1. + rewrite (take_S_r _ _ n) // app_assoc. + by apply submseteq_skips_r. + - by apply lookup_lt_Some in Hhistndeq_1. } + + clear - Hhistndeq_1 Hhistvs_1. + iInv "Hinv" as (hist1' hist2 ndeq' linked ecsA ecsB ecsC npD npE npF nD nE nF vs1') ">H". + iNamedSuffix "H" "_2". + wp_faa. + + iCombine "HcontF●_2 HcontF◯" as "HcontF" gives %->%excl_auth_agree_L. + iMod (own_update with "HcontF") as "[HcontF●_2 HcontF◯]". + { apply (excl_auth_update _ _ n). } + + iEval (rewrite Z.add_0_r) in "Hsum_2". + + iCombine "HvdeqF●_2 HvdeqF◯" gives %->%excl_auth_agree_L. + + iDestruct (mono_list_auth_lb_own_valid with "Hhist1●_2 Hhist1◯_1") as %[_ Hhistpre]. + assert (Hn : n ≠ 0). + { eapply (Forall_lookup (.≠ 0)); last done. + by eapply Forall_prefix. } + + iModIntro. iFrame. iFrameNamed. iSplit; last done. iModIntro. + iPureIntro. exists ndeq'. repeat split; try done. + by rewrite /option_nat option_guard_True. + } + + iIntros (v1 v2) "[(H1 & HvenqB◯ & HvenqC◯ & H4 & H5) H6]". + unfold P1, P2, P3, P4, P5, P6. clear P1 P2 P3 P4 P5 P6. + iDestruct "H1" as "[HvenqA◯ Hlinked◯]". + iDestruct "H4" as "(%nD' & HnD'◯ & %HcontD)". + iDestruct "H5" as "(%nE' & HnE'◯ & %HcontE)". + iDestruct "H6" as "(%nF' & HnF'◯ & %HcontF)". + iModIntro. wp_pures. + + iInv "Hinv" as (hist1 hist2 ndeq linked ecsA ecsB ecsC npD npE npF nD nE nF vs1) ">@". + wp_load. iModIntro. iSplit; [by iFrame; iExists ndeq|]. + iCombine "HnD'◯ HcontD●" gives %<-%excl_auth_agree_L. iClear "HnD'◯ HcontD●". + iCombine "HnE'◯ HcontE●" gives %<-%excl_auth_agree_L. iClear "HnE'◯ HcontE●". + iCombine "HnF'◯ HcontF●" gives %<-%excl_auth_agree_L. iClear "HnF'◯ HcontF●". + + rewrite /option_nat !option_guard_True // in HD HE HF. + apply option_le_inv in HD as [HD|<-]; first done. + apply option_le_inv in HE as [HE|<-]; first done. + apply option_le_inv in HF as [HF|<-]; first done. + simplify_eq/=. + + iCombine "Hlinked● Hlinked◯" gives %->%excl_auth_agree_L. + iClear "Hq2 Hlinked● Hlinked◯". + + iCombine "HvenqA● HvenqA◯" gives %->%excl_auth_agree_L. iClear "HvenqA◯ HvenqA●". + iCombine "HvenqB● HvenqB◯" gives %->%excl_auth_agree_L. iClear "HvenqB◯ HvenqB●". + iCombine "HvenqC● HvenqC◯" gives %->%excl_auth_agree_L. iClear "HvenqC◯ HvenqC●". + iPureIntro. enough (nD + nE + nF = 6). { do 2 f_equal. lia. } + + assert (ndeq ≥ 3 ∧ length hist1 ≥ 3) as [Hndeq' Hhist1']. + { apply submseteq_length in HnDEF as Hndeq'. + rewrite /= length_take in Hndeq'. lia. } + apply gmultiset_subseteq_size in Hhist1 as Hhist1''. + rewrite list_to_set_disj_size !gmultiset_size_disj_union !gmultiset_size_singleton /= in Hhist1''. + have {Hhist1''}Hhist1' : length hist1 = 3 by lia. + apply gmultiset_subseteq_size_eq in Hhist1; last first. + { rewrite !gmultiset_size_disj_union !gmultiset_size_singleton /= list_to_set_disj_size. lia. } + + assert (HnDEF' : [nD; nE; nF] ≡ₚ hist1). + { apply submseteq_length_Permutation; last (simpl; lia). + etrans; [apply HnDEF | apply submseteq_take]. } + + assert (Hhist1'' : hist1 ≡ₚ elements ({[+ 1; 2; 3 +]} : gmultiset nat)). + { erewrite elements_list_to_set_disj_perm. + by rewrite Hhist1. } + + assert (H123 : elements ({[+ 1; 2; 3 +]} : gmultiset nat) ≡ₚ [1; 2; 3]). + { by rewrite !gmultiset_elements_disj_union !gmultiset_elements_singleton /=. } + + trans (foldr Nat.add 0 [nD; nE; nF]). { simpl. lia. } + by rewrite HnDEF' Hhist1'' H123. + Qed. + +End proofs. + +Definition fq := fin_queue_proof.fin_queue_hl. +Definition lq := lmpmc_queue_proof.lmpmc_queue_hl fq. + +(** First example *) + +Definition simple_clientΣ : gFunctors := #[ heapΣ; fin_queue_proof.fin_queueΣ ]. +Lemma simple_client_adequate σ : adequate NotStuck (simple_example_2_1 lq) σ (λ v _, v = (#10, #20)%V). +Proof. + eapply (heap_adequacy simple_clientΣ). iIntros (?) "_". iApply simple_example_2_1_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +(** Second example *) + +Definition simple_mt_clientΣ : gFunctors := + #[ heapΣ; spawnΣ; + fin_queue_proof.fin_queueΣ; + GFunctor (excl_authRF boolO); + GFunctor (excl_authRF (listO natO)) ]. + +Instance smc_inG_excl_auth_bool Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR boolO). +Proof. solve_inG. Qed. +Instance smc_inG_excl_auth_nat_list Σ : subG simple_mt_clientΣ Σ → inG Σ (excl_authR (listO natO)). +Proof. solve_inG. Qed. + +Lemma simple_mt_client_adequate σ : adequate NotStuck (simple_example_2_2 lq) σ (λ v _, v = (#10, #20)%V). +Proof. + eapply (heap_adequacy simple_mt_clientΣ). iIntros (?) "_". iApply simple_example_2_2_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +(** Third example *) + +Definition mt_example_1Σ : gFunctors := + #[ heapΣ; spawnΣ; + fin_queue_proof.fin_queueΣ; + mono_listΣ natO; + GFunctor (excl_authRF (gmultisetO nat)); + GFunctor (excl_authRF natO); + GFunctor (excl_authRF boolO); + GFunctor (excl_authRF (optionO natO)); + GFunctor (exclR (listO natO)) ]. + +Instance me_inG_excl_auth_multiset Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (gmultisetO nat)). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR natO). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_bool Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR boolO). +Proof. solve_inG. Qed. +Instance me_inG_excl_auth_option_nat Σ : subG mt_example_1Σ Σ → inG Σ (excl_authR (optionO natO)). +Proof. solve_inG. Qed. +Instance me_inG_excl_list_nat Σ : subG mt_example_1Σ Σ → inG Σ (exclR (listO natO)). +Proof. solve_inG. Qed. + +Lemma mt_example_1_adequate σ : adequate NotStuck (mt_example_1 lq) σ (λ v _, v = #6%V). +Proof. + eapply (heap_adequacy mt_example_1Σ). iIntros (?) "_". iApply mt_example_1_safe. + Unshelve. apply lmpmc_queue_proof.lmpmc_queue_iris, fin_queue_proof.fin_queue_iris. +Qed. + +Print Assumptions simple_client_adequate. +Print Assumptions simple_mt_client_adequate. +Print Assumptions mt_example_1_adequate. -- cgit v1.3