WP rule for `par`

theories/examples/par.v

 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl.
 From iris_logrel Require Export logrel.
 
 Definition par : val := λ: "e1" "e2",
   let: "x1" := ref InjL #() in
   Fork ("x1" <- InjR ("e1" #()));;
   let: "x2" := "e2" #() in
-  let: "f" := rec: "f" <> := 
+  let: "f" := rec: "f" <> :=
     match: !"x1" with
       InjL <>  => "f" #()
     | InjR "v" => "v"
@@ -35,4 +36,63 @@ Section compatibility.
     iApply binary_fundamental_masked; eauto with typeable.
   Qed.
 
+  Context `{!inG Σ (exclR unitR)}.
+  Definition parinv (x1 : loc) (Ψ : val -> iProp Σ) (γ : gname) :=
+    (x1 ↦ᵢ InjLV #() ∨ ∃ v, x1 ↦ᵢ InjRV v ∗ (Ψ v ∨ (own γ (Excl ()))))%I.
+  Definition parN := logrelN.@"parN".
+  Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 (f1 f2 : val) (Φ : val → iProp Σ)
+        `{Hef1 : !IntoVal e1 f1} `{Hef2 : !IntoVal e2 f2}:
+    WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
+    (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
+    WP par e1 e2 {{ Φ }}.
+  Proof.
+    apply of_to_val in Hef1 as <-.
+    apply of_to_val in Hef2 as <-.
+    iIntros "Hf1 Hf2 HΦ".
+    unlock par; simpl. repeat wp_let.
+    wp_alloc x1 as "Hx1". wp_let.
+    iMod (own_alloc (Excl ())) as (γ) "Ht"; first done.
+    iMod (inv_alloc parN _ (parinv x1 Ψ1 γ) with "[Hx1]") as "#Hinv".
+    { iNext. by iLeft. }
+    wp_bind (Fork _).
+    iApply wp_fork.
+    iSplitR "Hf1"; last first.
+    { iNext.
+      wp_bind (f1 #()). iApply (wp_wand with "Hf1").
+      iIntros (v) "HΨ1".
+      iInv (logrelN.@"parN") as "Hx1" "Hcl".
+      iAssert (|={⊤ ∖ ↑logrelN.@"parN"}=> ∃ z, x1 ↦ᵢ z)%I with "[Hx1]" as "Hx1".
+      { iDestruct "Hx1" as "[>Hx1 | Hx1]".
+        + iModIntro. iExists _. iFrame.
+        + iDestruct "Hx1" as (?) "[>Hx1 ?]".
+          iModIntro. iExists _. iFrame. }
+      iMod "Hx1" as (?) "Hx1".
+      wp_store.
+      iApply "Hcl".
+      iNext. iRight. iExists _; iFrame.
+      iLeft. iFrame. }
+    { iNext.
+      iModIntro. wp_let.
+      wp_bind (f2 #()). iApply (wp_wand with "Hf2").
+      iIntros (v2) "HΨ2". wp_let. wp_let.
+      wp_bind (App _ #()).
+      iLöb as "IH". wp_rec.
+      wp_bind (! #x1)%E.
+      iInv (logrelN.@"parN") as "[>Hx1 | Hx1]" "Hcl".
+      - wp_load.
+        iMod ("Hcl" with "[Hx1]") as "_". { by iLeft. }
+        iModIntro. wp_case. wp_let.
+        iApply ("IH" with "HΦ Ht HΨ2").
+      - iDestruct "Hx1" as (v1) "[>Hx1 HΨ1]".
+        wp_load.
+        iDestruct "HΨ1" as "[HΨ1 | Ht']"; last first.
+        { iDestruct (own_valid_2 with "Ht Ht'") as %[]. }
+        iMod ("Hcl" with "[Hx1 Ht]") as "_".
+        { iNext. iRight. iExists _; iFrame.
+          iRight. iFrame. }
+        iModIntro. simpl. (* TODO: simpl is required here *) wp_case.
+        iSpecialize ("HΦ" with "[$HΨ1 $HΨ2]").
+        wp_let. by wp_value. }
+  Qed.
+
 End compatibility.