one_shot_once.v 6.02 KB
Newer Older
1
From iris.algebra Require Import frac agree csum.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.proofmode Require Import tactics.
3
4
From iris.program_logic Require Export weakestpre.
From iris.deprecated.program_logic Require Import hoare.
Ralf Jung's avatar
Ralf Jung committed
5
6
7
8
9
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
10
11
12
(** This is the introductory example from Ralf's PhD thesis.
The difference to [one_shot] is that [set] asserts to be called only once. *)

13
14
Unset Mangle Names.

Ralf Jung's avatar
Ralf Jung committed
15
16
17
18
19
20
Definition one_shot_example : val := λ: <>,
  let: "x" := ref NONE in (
  (* set *) (λ: "n",
    assert: CAS "x" NONE (SOME "n")),
  (* check  *) (λ: <>,
    let: "y" := !"x" in λ: <>,
Ralf Jung's avatar
Ralf Jung committed
21
22
23
24
25
      let: "y'" := !"x" in
      match: "y" with
        NONE => #()
      | SOME <> => assert: "y" = "y'"
      end)).
Ralf Jung's avatar
Ralf Jung committed
26
27
28
29
30
31
32

Definition one_shotR := csumR fracR (agreeR ZO).
Definition Pending (q : Qp) : one_shotR := Cinl q.
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).

Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
33
Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ  one_shotG Σ.
Ralf Jung's avatar
Ralf Jung committed
34
35
36
37
38
39
40
41
42
43
Proof. solve_inG. Qed.

Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ}.

Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
  (l  NONEV  own γ (Pending (1/2)%Qp) 
    n : Z, l  SOMEV #n  own γ (Shot n))%I.

Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
  unfold one_shot_inv : core.
Ralf Jung's avatar
Ralf Jung committed
46

Ralf Jung's avatar
Ralf Jung committed
47
48
49
Lemma pending_split γ q :
  own γ (Pending q)  own γ (Pending (q/2))  own γ (Pending (q/2)).
Proof.
50
  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp_div_2 //.
Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
Qed.

Lemma pending_shoot γ n :
  own γ (Pending 1%Qp) == own γ (Shot n).
Proof.
  iIntros "Hγ". iMod (own_update with "Hγ") as "$"; last done.
  by apply cmra_update_exclusive with (y:=Shot n).
Qed.

Lemma wp_one_shot (Φ : val  iProp Σ) :
  ( (f1 f2 : val) (T : iProp Σ), T 
     ( n : Z, T - WP f1 #n {{ w, True }}) 
     WP f2 #() {{ g,  WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
   WP one_shot_example #() {{ Φ }}.
Proof.
  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
67
  wp_lam. wp_alloc l as "Hl".
Ralf Jung's avatar
Ralf Jung committed
68
69
70
71
72
73
  iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
  iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
  { iNext. iLeft. by iFrame. }
  wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
  iSplitL; first done. iSplit.
74
  - iIntros (n) "!> Hγ1". wp_pures.
Ralf Jung's avatar
Ralf Jung committed
75
76
77
78
79
80
81
    iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
    + iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
      iMod (pending_shoot _ n with "Hγ") as "Hγ".
      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
      iNext; iRight; iExists n; by iFrame.
    + by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
82
  - iIntros "!> /=". wp_lam. wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
83
84
85
86
87
88
89
90
91
92
93
94
95
    iInv N as ">Hγ".
    iAssert ( v, l  v  (v = NONEV  own γ (Pending (1/2)%Qp) 
        n : Z, v = SOMEV #n  own γ (Shot n)))%I with "[Hγ]" as "Hv".
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
      + iExists NONEV. iFrame. eauto.
      + iExists (SOMEV #m). iFrame. eauto. }
    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
    iAssert (one_shot_inv γ l  (v = NONEV   n : Z,
      v = SOMEV #n  own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
    iSplitL "Hinv"; first by eauto.
96
    iModIntro. wp_pures. iIntros "!> !>". wp_lam. wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
97
98
99
100
101
102
103
104
    iInv N as "Hinv".
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
    + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
      wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
      wp_pures; done.
    + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
      { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
      wp_load. Show.
Ralf Jung's avatar
Ralf Jung committed
105
      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
Ralf Jung's avatar
Ralf Jung committed
106
107
      iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
      wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
Ralf Jung's avatar
Ralf Jung committed
108
109
110
Qed.

Lemma ht_one_shot (Φ : val  iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
111
   {{ True }} one_shot_example #()
Ralf Jung's avatar
Ralf Jung committed
112
113
114
115
116
    {{ ff,  T, T 
      ( n : Z, {{ T }} Fst ff #n {{ _, True }}) 
      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
    }}.
Proof.
117
  iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
Ralf Jung's avatar
Ralf Jung committed
118
  iExists T. iFrame "HT". iSplit.
119
120
  - iIntros (n) "!> HT". wp_smart_apply "Hf1". done.
  - iIntros "!> _". wp_smart_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
Ralf Jung's avatar
Ralf Jung committed
121
122
123
124
125
126
127
128
129
130
131
Qed.
End proof.

(* Have a client with a closed proof. *)
Definition client : expr :=
  let: "ff" := one_shot_example #() in
  (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).

Section client.
  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.

Gregory Malecha's avatar
Gregory Malecha committed
132
  Lemma client_safe :  WP client {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
133
134
  Proof using Type*.
    rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
135
136
    wp_let. wp_smart_apply (wp_par with "[HT]").
    - wp_smart_apply "Hf1". done.
Ralf Jung's avatar
Ralf Jung committed
137
138
139
140
141
142
143
144
145
146
147
    - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
      iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
    - auto.
  Qed.
End client.

(** Put together all library functors. *)
Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Ralf Jung's avatar
Ralf Jung committed
148
Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.