example_joining_existentials.v 4.37 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
Set Default Proof Using "Type".

Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
Ralf Jung's avatar
Ralf Jung committed
11
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Robbert Krebbers's avatar
Robbert Krebbers committed
12
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
Ralf Jung's avatar
Ralf Jung committed
13 14 15 16 17 18 19 20 21
  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

Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Local Notation X := (F (iProp Σ) _).
Ralf Jung's avatar
Ralf Jung committed
32 33 34 35

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.