example_joining_existentials.v 4.36 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import notation par proofmode.
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
6
From iris_examples.barrier Require Import proof specification.
Ralf Jung's avatar
Ralf Jung committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
Set Default Proof Using "Type".

Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ)) : one_shotR Σ F :=
  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.

Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
  one_shot_inG :> inG Σ (one_shotR Σ F).
Definition oneShotΣ (F : cFunctor) : gFunctors :=
  #[ GFunctor (csumRF (exclRF unitC) (agreeRF ( F))) ].
Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ  oneShotG Σ F.
Proof. solve_inG. Qed.

22 23
Definition client : val :=
  λ: "fM" "fW1" "fW2",
Ralf Jung's avatar
Ralf Jung committed
24
  let: "b" := newbarrier #() in
25
  ("fM" #() ;; signal "b") ||| ((wait "b" ;; "fW1" #()) ||| (wait "b" ;; "fW2" #())).
Ralf Jung's avatar
Ralf Jung committed
26 27 28 29 30 31 32 33 34 35

Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace).
Local Notation X := (F (iProp Σ)).

Definition barrier_res γ (Φ : X  iProp Σ) : iProp Σ :=
  ( x, own γ (Shot x)  Φ x)%I.

36
Lemma worker_spec e γ l (Φ Ψ : X  iProp Σ) :
Ralf Jung's avatar
Ralf Jung committed
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
  recv N l (barrier_res γ Φ) - ( x, {{ Φ x }} e {{ _, Ψ x }}) -
  WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
  iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
  iDestruct 1 as (x) "[#Hγ Hx]".
  wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
  iIntros (v) "?"; iExists x; by iSplit.
Qed.

Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ).
Context {Φ_split :  x, Φ x - (Φ1 x  Φ2 x)}.
Context {Ψ_join  :  x, Ψ1 x - Ψ2 x - Ψ x}.

Lemma P_res_split γ : barrier_res γ Φ - barrier_res γ Φ1  barrier_res γ Φ2.
Proof.
  iDestruct 1 as (x) "[#Hγ Hx]".
  iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Qed.

Lemma Q_res_join γ : barrier_res γ Ψ1 - barrier_res γ Ψ2 -  barrier_res γ Ψ.
Proof.
  iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
  iAssert ( (x  x'))%I as "Hxx".
  { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
Ralf Jung's avatar
Ralf Jung committed
61
    rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
Ralf Jung's avatar
Ralf Jung committed
62
    rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
63 64 65 66
    assert (HF : cFunctor_map F (cid, cid)  cFunctor_map F (iProp_fold (Σ:=Σ)  iProp_unfold, iProp_fold (Σ:=Σ)  iProp_unfold)).
    { apply ne_proper; first by apply _.
      by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
    rewrite (HF x). rewrite (HF x').
Ralf Jung's avatar
Ralf Jung committed
67 68 69 70 71
    rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
  iNext. iRewrite -"Hxx" in "Hx'".
  iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Qed.

72
Lemma client_spec_new (fM fW1 fW2 : val) :
Ralf Jung's avatar
Ralf Jung committed
73
  P -
74 75 76 77
  {{ P }} fM #() {{ _,  x, Φ x }} -
  ( x, {{ Φ1 x }} fW1 #() {{ _, Ψ1 x }}) -
  ( x, {{ Φ2 x }} fW2 #() {{ _, Ψ2 x }}) -
  WP client fM fW1 fW2 {{ _,  γ, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
78
Proof using All.
79
  iIntros "/= HP #Hf #Hf1 #Hf2"; rewrite /client.
Ralf Jung's avatar
Ralf Jung committed
80
  iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
81
  wp_lam. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
Ralf Jung's avatar
Ralf Jung committed
82 83
  iIntros (l) "[Hr Hs]".
  set (workers_post (v : val) := (barrier_res γ Ψ1  barrier_res γ Ψ2)%I).
84 85 86
  wp_apply (par_spec  (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
  - wp_lam. wp_bind (fM #()). iApply (wp_wand with "[HP]"); [by iApply "Hf"|].
    iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_seq.
Ralf Jung's avatar
Ralf Jung committed
87 88 89 90 91 92
    iMod (own_update with "Hγ") as "Hx".
    { by apply (cmra_update_exclusive (Shot x)). }
    iApply (signal_spec with "[- $Hs]"); last auto.
    iExists x; auto.
  - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
    iMod (recv_split with "Hr") as "[H1 H2]"; first done.
93 94 95 96
    wp_apply (par_spec (λ _, barrier_res γ Ψ1)%I
                       (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
    + wp_apply (worker_spec with "H1"); auto.
    + wp_apply (worker_spec with "H2"); auto.
Ralf Jung's avatar
Ralf Jung committed
97 98 99 100
    + auto.
  - iIntros (_ v) "[_ [H1 H2]]". iDestruct (Q_res_join with "H1 H2") as "?". auto.
Qed.
End proof.