Recovered original double manual proof

theories/logrel/examples/double.v

@@ -30,14 +30,79 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{!heapG Σ, !chanG Σ, !spawnG Σ}.
+  Context `{heapG Σ, chanG Σ, spawnG Σ}.
+  Context `{!inG Σ fracR}.
   Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
-  Definition prog_prot (P : val → val → iProp Σ) : iProto Σ :=
+  Definition prog_prot : iProto Σ :=
+    (<? (x : Z)> MSG #x; <? (y : Z)> MSG #y; 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.
+
+  Lemma wp_prog c :
+    {{{ ▷ c ↣ prog_prot }}}
+      prog c
+    {{{ (k1 k2 : Z), RET (#k1, #k2); True }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    rewrite /prog.
+    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]"; [done|].
+    (* Create lock *)
+    wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
+    { iLeft. iFrame "Hc". }
+    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]").
+    - (* 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 %[].
+    - (* 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Φ".
+  Qed.
+
+  Definition prog_prot_fp (P : val → val → iProp Σ) : iProto Σ :=
     (<? (v1 : val)> MSG v1; <? (v2 : val)> MSG v2 {{ P v1 v2 }}; END)%proto.
 
-  Definition chan_inv (γ γ1 γ2 : gname) (P : val → val → iProp Σ) (c : val) : iProp Σ :=
-    (own γ (Excl ()) ∗ c ↣ prog_prot P ∨
+  Definition chan_inv_fp (γ γ1 γ2 : gname) (P : val → val → iProp Σ) (c : val) :
+    iProp Σ :=
+    (own γ (Excl ()) ∗ c ↣ prog_prot_fp 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) ∨
@@ -45,8 +110,8 @@ Section double.
        own γ1 (1/4, to_agree (Some v1))%Qp ∗
        own γ2 (1/4, to_agree (Some v2))%Qp))%I.
 
-  Lemma wp_prog P c :
-    {{{ ▷ c ↣ prog_prot P }}}
+  Lemma wp_prog_fp P c :
+    {{{ ▷ c ↣ prog_prot_fp P }}}
       prog c
     {{{ v1 v2, RET (v1, v2); P v1 v2 ∨ P v2 v1 }}}.
   Proof.
@@ -55,7 +120,7 @@ Section double.
     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 γ γ1 γ2 P c) with "[Hγ Hc]").
+    wp_apply (newlock_spec (chan_inv_fp γ γ1 γ2 P c) with "[Hγ Hc]").
     { iLeft. by iFrame. }
     iIntros (lk γlk) "#Hlock". wp_pures.
     (* Fork into two threads *)
@@ -128,7 +193,7 @@ Section double.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value. iSplitL; last by iApply env_ltyped_nil.
     iIntros (c) "Hc".
-    iApply (wp_prog (λ v1 v2, ltty_car lty_int v1 ∗ ltty_car lty_int v2)%I with "[Hc]").
+    iApply (wp_prog_fp (λ 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). iDestruct 1 as %[x1 ->]. iExists #x1.
       iIntros "!>" (v2). iDestruct 1 as %[x2 ->]. iExists #x2. iSplitL; last done.