joining_existentials.v 4.15 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1 2
From iris.algebra Require Import csum.
From iris.program_logic Require Import hoare.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.heap_lang.lib.barrier Require Import proof specification.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
From iris.heap_lang Require Import notation par proofmode.
From iris.proofmode Require Import invariants.
Ralf Jung's avatar
Ralf Jung committed
6 7
Import uPred.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
8 9 10 11 12 13 14 15
Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
  one_shot_inG :>
    inG Λ Σ (csumR (exclR unitC) (agreeR $ laterC $ F (iPrePropG Λ Σ))).
Definition oneShotGF (F : cFunctor) : gFunctor :=
  GFunctor (csumRF (exclRF unitC) (agreeRF ( F))).
Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
Proof. apply: inGF_inG. Qed.

16
Definition client eM eW1 eW2 : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  let: "b" := newbarrier #() in
18
  (eM ;; signal "b") || ((wait "b" ;; eW1) || (wait "b" ;; eW2)).
19
Global Opaque client.
Ralf Jung's avatar
Ralf Jung committed
20 21 22 23 24 25 26 27

Section proof.
Context (G : cFunctor).
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation X := (G iProp).

Robbert Krebbers's avatar
Robbert Krebbers committed
28
Definition barrier_res γ (Φ : X  iProp) : iProp :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
29 30
  ( x, own γ (Cinr $ to_agree $
               Next (cFunctor_map G (iProp_fold, iProp_unfold) x))  Φ x)%I.
Ralf Jung's avatar
Ralf Jung committed
31

32
Lemma worker_spec e γ l (Φ Ψ : X  iProp) `{!Closed [] e} :
33
  recv heapN N l (barrier_res γ Φ)  ( x, {{ Φ x }} e {{ _, Ψ x }})
34
   WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
35
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
37
  iDestruct 1 as (x) "[#Hγ Hx]".
38
  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
39
  iIntros (v) "?"; iExists x; by iSplit.
Ralf Jung's avatar
Ralf Jung committed
40 41
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44
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}.
Ralf Jung's avatar
Ralf Jung committed
45

46
Lemma P_res_split γ : barrier_res γ Φ  barrier_res γ Φ1  barrier_res γ Φ2.
Ralf Jung's avatar
Ralf Jung committed
47
Proof.
48
  iDestruct 1 as (x) "[#Hγ Hx]".
49
  iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Ralf Jung's avatar
Ralf Jung committed
50 51
Qed.

52
Lemma Q_res_join γ : barrier_res γ Ψ1  barrier_res γ Ψ2   barrier_res γ Ψ.
Ralf Jung's avatar
Ralf Jung committed
53
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  iIntros "[Hγ Hγ']";
55
  iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
56
  iAssert ( (x  x'))%I as "Hxx" .
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57 58 59
  { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
    rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
    rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
    rewrite (ne_proper (cFunctor_map G) (cid, cid) (_  _, _  _)); last first.
    { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
62
    rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64
  iNext. iRewrite -"Hxx" in "Hx'".
  iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
Ralf Jung's avatar
Ralf Jung committed
65 66
Qed.

67 68
Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
  heapN  N 
69
  heap_ctx heapN  P
70 71
   {{ P }} eM {{ _,  x, Φ x }}
   ( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
72
   ( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
73
   WP client eM eW1 eW2 {{ _,  γ, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
74
Proof.
75
  iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
76
  iPvs (own_alloc (Cinl (Excl ()))) as (γ) "Hγ". done.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
78
  iFrame "Hh". iIntros (l) "[Hr Hs]".
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  set (workers_post (v : val) := (barrier_res γ Ψ1  barrier_res γ Ψ2)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81 82
  wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post);
    try iFrame "Hh"; first done.
  iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
83
  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
84
    iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85 86
    iPvs (own_update _ _ (Cinr (to_agree _)) with "Hγ") as "Hx".
    by apply cmra_update_exclusive.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    iApply signal_spec; iFrame "Hs"; iSplit; last done.
88
    iExists x; auto.
89
  - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
90
    iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
      (λ _, barrier_res γ Ψ2)%I); try iFrame "Hh"; first done.
    iSplitL "H1"; [|iSplitL "H2"].
94 95 96
    + iApply worker_spec; auto.
    + iApply worker_spec; auto.
    + auto.
97
  - iIntros (_ v) "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
Ralf Jung's avatar
Ralf Jung committed
98 99
Qed.
End proof.