From 338adc7d0aede27fab045a8f94e5076d03ca351b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 May 2020 14:41:38 +0200
Subject: [PATCH] Functional correctness spec of double example.

---
 theories/logrel/examples/double.v | 140 ++++++++++++++++++------------
 1 file changed, 84 insertions(+), 56 deletions(-)

diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 28980c4..333e5b6 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import frac.
+From iris.algebra Require Import frac auth excl updates.
 From iris.heap_lang.lib Require Export par spin_lock.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_typing_judgment session_types.
@@ -19,69 +19,96 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{heapG Σ, chanG Σ, inG Σ fracR, spawnG Σ}.
+  Context `{!heapG Σ, !chanG Σ, !spawnG Σ}.
+  Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
-  Definition prog_prot : iProto Σ :=
-    (<? (x : Z)> MSG #x; <? (y : Z)> MSG #y; END)%proto.
+  Definition prog_prot (P : val → val → iProp Σ) : iProto Σ :=
+    (<? (v1 : val)> MSG v1; <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END)%proto.
 
-  Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
-    (c ↣ prog_prot ∨
-     (own γ (1/2)%Qp ∗ c ↣ <? (x : Z)> MSG #x; END) ∨
-     (own γ 1%Qp ∗ c ↣ END))%I.
+  Definition chan_inv (γ γ1 γ2 : gname) (P : val → val → iProp Σ) (c : val) : iProp Σ :=
+    (own γ (Excl ()) ∗ c ↣ prog_prot P ∨
+     (∃ b v1,
+       own (if b : bool then γ1 else γ2) (3/4, to_agree (Some v1))%Qp ∗
+       c ↣ <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END) ∨
+     (∃ v1 v2,
+       own γ1 (1/4, to_agree (Some v1))%Qp ∗
+       own γ2 (1/4, to_agree (Some v2))%Qp))%I.
 
-  Lemma wp_prog c :
-    {{{ ▷ c ↣ prog_prot }}}
+  Lemma wp_prog P c :
+    {{{ ▷ c ↣ prog_prot P }}}
       prog c
-    {{{ (k1 k2 : Z), RET (#k1, #k2); True }}}.
+    {{{ v1 v2, RET (v1, v2); P v1 v2 ∨ P v2 v1 }}}.
   Proof.
-    iIntros (Φ) "Hc HΦ".
-    rewrite /prog.
-    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]"; [done|].
+    iIntros (Φ) "Hc HΦ". rewrite /prog.
+    iMod (own_alloc (Excl ())) as (γ) "Hγ"; [done|].
+    iMod (own_alloc (1, to_agree None)%Qp) as (γ1) "Hγ1"; [done|].
+    iMod (own_alloc (1, to_agree None)%Qp) as (γ2) "Hγ2"; [done|].
     (* Create lock *)
-    wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
-    { iLeft. iFrame "Hc". }
-    iIntros (lk γlk) "#Hlock".
-    wp_pures.
+    wp_apply (newlock_spec (chan_inv γ γ1 γ2 P c) with "[Hγ Hc]").
+    { iLeft. by iFrame. }
+    iIntros (lk γlk) "#Hlock". wp_pures.
     (* Fork into two threads *)
-    wp_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
-                with "[Hcredit1] [Hcredit2]").
+    wp_apply (wp_par
+      (λ v1, own γ1 (1/4, to_agree (Some v1))%Qp ∗ own γ (Excl ()) ∨
+        (∃ v2, own γ1 (3/4, to_agree (Some v1))%Qp ∗
+               own γ2 (1/2, to_agree (Some v2))%Qp ∗ P v2 v1))%I
+      (λ v2, own γ2 (1/4, to_agree (Some v2))%Qp ∗ own γ (Excl ()) ∨
+        (∃ v1, own γ2 (3/4, to_agree (Some v2))%Qp ∗
+               own γ1 (1/2, to_agree (Some v1))%Qp ∗ P v1 v2))%I with "[Hγ1] [Hγ2]").
     - (* Acquire lock *)
       wp_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
-      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
-      + wp_recv (x1) as "_". wp_pures.
-        wp_apply (release_spec with "[Hlocked Hcredit1 Hc]").
-        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit1 Hc". }
-        iIntros "_". wp_pures.
-        eauto.
-      + iDestruct "Hc" as "[Hcredit2 Hc]".
-        wp_recv (x1) as "_". wp_pures.
-        iCombine "Hcredit1 Hcredit2" as "Hcredit".
-        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
-        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
-        iIntros "_". wp_pures.
-        eauto.
-      + iDestruct "Hc" as "[Hcredit2 Hc]".
-        by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
+      iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
+      + wp_recv (v) as "_". wp_pures.
+        iMod (own_update _ _ ((3/4 ⋅ 1/4), to_agree (Some v))%Qp with "Hγ1")
+          as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
+        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hc]").
+        { iRight. iLeft. iExists true, v. iFrame. }
+        iIntros "_". wp_pures. iLeft. iFrame.
+      + iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
+        { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
+        wp_recv (v') as "HP". wp_pures.
+        iMod (own_update _ _ ((1/4 ⋅ 3/4), to_agree (Some v'))%Qp with "Hγ1")
+          as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
+        rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
+        iDestruct "Hγ2" as "[Hγ2a Hγ2b]".
+        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
+        { do 2 iRight. iExists v', v. iFrame. }
+        iIntros "_". wp_pures. iRight. iExists v. iFrame.
+      + iDestruct "Hc" as (v v') "[Hγ1' _]".
+        by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
     - (* Acquire lock *)
       wp_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
-      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
-      + wp_recv (x1) as "_". wp_pures.
-        wp_apply (release_spec with "[Hlocked Hcredit2 Hc]").
-        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit2 Hc". }
-        iIntros "_". wp_pures.
-        eauto.
-      + iDestruct "Hc" as "[Hcredit1 Hc]".
-        wp_recv (x1) as "Hx1". wp_pures.
-        iCombine "Hcredit1 Hcredit2" as "Hcredit".
-        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
-        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
-        iIntros "_". wp_pures.
-        eauto.
-      + iDestruct "Hc" as "[Hcredit1 Hc]".
-        by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
-    - iIntros (?? [[x1 ->] [x2 ->]]) "!>". wp_pures. by iApply "HΦ".
+      iDestruct "Hc" as "[[Hγ Hc]|[Hc|Hc]]".
+      + wp_recv (v) as "_". wp_pures.
+        iMod (own_update _ _ ((3/4 ⋅ 1/4), to_agree (Some v))%Qp with "Hγ2")
+          as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
+        wp_apply (release_spec with "[$Hlock $Hlocked Hγ2a Hc]").
+        { iRight. iLeft. iExists false, v. iFrame. }
+        iIntros "_". wp_pures. iLeft. iFrame.
+      + iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
+        { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
+        wp_recv (v') as "HP". wp_pures.
+        iMod (own_update _ _ ((1/4 ⋅ 3/4), to_agree (Some v'))%Qp with "Hγ2")
+          as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
+        rewrite {1}(_ : 3/4 = 1/4 + 1/2)%Qp; last (by apply: bool_decide_unpack).
+        iDestruct "Hγ1" as "[Hγ1a Hγ1b]".
+        wp_apply (release_spec with "[$Hlock $Hlocked Hγ1a Hγ2a Hc]").
+        { do 2 iRight. iExists v, v'. iFrame. }
+        iIntros "_". wp_pures. iRight. iExists v. iFrame.
+      + iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
+        by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[].
+    - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
+      + by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
+      + iDestruct "H2" as (v2') "(_&H1'&HP)".
+        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%agree_op_invL'].
+        iApply "HΦ"; auto.
+      + iDestruct "H1" as (v1') "(_&H2'&HP)".
+        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%agree_op_invL'].
+        iApply "HΦ"; auto.
+      + iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
+        by iDestruct (own_valid_2 with "H1 H2") as %[].
   Qed.
 
   Lemma prog_typed :
@@ -91,11 +118,12 @@ Section double.
     iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.
     iIntros (c) "Hc".
-    iApply (wp_prog with "[Hc]").
+    iApply (wp_prog (λ v1 v2, ltty_car lty_int v1 ∗ ltty_car lty_int v2)%I with "[Hc]").
     { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
-      iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists x1.
-      iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists x2. auto. }
-    iIntros "!>" (k1 k2 _).
-    iExists _, _. iSplit; first done. eauto.
+      iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists #x1.
+      iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists #x2. iSplitL; last done.
+      rewrite /ltty_car /=. auto. }
+    iIntros "!>" (v1 v2 [[[k1 ->] [k2 ->]]|[[k1 ->] [k2 ->]]]);
+      iExists _, _; iSplit; by eauto.
   Qed.
 End double.
-- 
GitLab