par.v 3.38 KB
Newer Older
1
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.algebra Require Import excl.
3
From iris_logrel Require Export logrel.
4 5

Definition par : val := λ: "e1" "e2",
6 7 8
  let: "x1" := ref InjL #() in
  Fork ("x1" <- InjR ("e1" #()));;
  let: "x2" := "e2" #() in
Dan Frumin's avatar
Dan Frumin committed
9
  let: "f" := rec: "f" <> :=
Dan Frumin's avatar
Dan Frumin committed
10
    match: !"x1" with
11
      InjL <>  => "f" #()
Dan Frumin's avatar
Dan Frumin committed
12 13
    | InjR "v" => "v"
    end
14
  in ("f" #(), "x2").
15 16 17 18 19

Lemma par_type Γ τ1 τ2 :
  typed Γ par
        (TArrow (TArrow TUnit τ1) (TArrow (TArrow TUnit τ2)
            (TProd τ1 τ2))).
Dan Frumin's avatar
Dan Frumin committed
20
Proof. solve_typed. Qed.
21 22 23 24

Hint Resolve par_type : typeable.

Section compatibility.
25
  Context `{logrelG Σ}.
26

27
  Lemma bin_log_related_par Δ Γ E e1 e2 e1' e2' τ1 τ2 :
28
    logrelN  E 
29 30 31
    {E;Δ;Γ}  e1 log e1' : TArrow TUnit τ1 -
    {E;Δ;Γ}  e2 log e2' : TArrow TUnit τ2 -
    {E;Δ;Γ}  par e1 e2 log par e1' e2' : TProd τ1 τ2.
32
  Proof.
33
    iIntros (?) "He1 He2".
34 35 36 37
    iApply (bin_log_related_app with "[He1] He2").
    iApply (bin_log_related_app with "[] He1").
    iApply binary_fundamental_masked; eauto with typeable.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
38

Dan Frumin's avatar
Dan Frumin committed
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  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.

98
End compatibility.