one_shot.v 5.37 KB
Newer Older
1
From iris.algebra Require Import excl 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.
5
From iris.heap_lang Require Export lang.
Ralf Jung's avatar
Ralf Jung committed
6
7
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.heap_lang.lib Require Import par.
8
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
9

Ralf Jung's avatar
Ralf Jung committed
10
11
12
(** This is the introductory example from the "Iris from the Ground Up" journal
paper. *)

13
14
Unset Mangle Names.

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

30
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
Definition Pending : one_shotR := Cinl (Excl ()).
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
33

34
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
35
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
36
Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ  one_shotG Σ.
37
Proof. solve_inG. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
38

Ralf Jung's avatar
Ralf Jung committed
39
Section proof.
40
Local Set Default Proof Using "Type*".
41
Context `{!heapG Σ, !one_shotG Σ}.
Ralf Jung's avatar
Ralf Jung committed
42

43
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
44
  (l  NONEV  own γ Pending   n : Z, l  SOMEV #n  own γ (Shot n))%I.
Ralf Jung's avatar
Ralf Jung committed
45

46
Lemma wp_one_shot (Φ : val  iProp Σ) :
47
  ( f1 f2 : val,
Ralf Jung's avatar
Ralf Jung committed
48
    ( n : Z,  WP f1 #n {{ w, w = #true  w = #false }}) 
49
     WP f2 #() {{ g,  WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
Ralf Jung's avatar
Ralf Jung committed
50
51
   WP one_shot_example #() {{ Φ }}.
Proof.
52
  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
53
  wp_lam. wp_alloc l as "Hl".
54
55
  iMod (own_alloc Pending) as (γ) "Hγ"; first done.
  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  { iNext. iLeft. by iSplitL "Hl". }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57
  wp_pures. iModIntro. iApply "Hf"; iSplit.
58
  - iIntros (n) "!>". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
Ralf Jung's avatar
Ralf Jung committed
59
60
    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
    + iMod (own_update with "Hγ") as "Hγ".
61
      { by apply cmra_update_exclusive with (y:=Shot n). }
Ralf Jung's avatar
Ralf Jung committed
62
      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
63
      iNext; iRight; iExists n; by iFrame.
Ralf Jung's avatar
Ralf Jung committed
64
    + wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
65
      rewrite /one_shot_inv; eauto 10.
66
  - iIntros "!> /=". wp_lam. wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
67
    iInv N as ">Hγ".
Ralf Jung's avatar
Ralf Jung committed
68
69
    iAssert ( v, l  v  ((v = NONEV  own γ Pending) 
        n : Z, v = SOMEV #n  own γ (Shot n)))%I with "[Hγ]" as "Hv".
70
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
71
72
      + iExists NONEV. iFrame. eauto.
      + iExists (SOMEV #m). iFrame. eauto. }
73
    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
Ralf Jung's avatar
Ralf Jung committed
74
75
    iAssert (one_shot_inv γ l  (v = NONEV   n : Z,
      v = SOMEV #n  own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
76
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
77
      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
78
      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
Ralf Jung's avatar
Ralf Jung committed
79
    iSplitL "Hinv"; first by eauto.
80
    iModIntro. wp_pures. iIntros "!> !>". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
81
82
83
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
      subst; wp_match; [done|].
    wp_bind (! _)%E.
84
    iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
85
    { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
86
    wp_load. Show.
Ralf Jung's avatar
Ralf Jung committed
87
    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
88
    iModIntro. iSplitL "Hl".
89
    { iNext; iRight; by eauto. }
90
    wp_smart_apply wp_assert. wp_pures. by case_bool_decide.
Ralf Jung's avatar
Ralf Jung committed
91
92
Qed.

93
Lemma ht_one_shot (Φ : val  iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
94
   {{ True }} one_shot_example #()
95
    {{ ff,
Ralf Jung's avatar
Ralf Jung committed
96
      ( n : Z, {{ True }} Fst ff #n {{ w, w = #true  w = #false }}) 
97
      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
Ralf Jung's avatar
Ralf Jung committed
98
99
    }}.
Proof.
100
  iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
101
102
  - iIntros (n) "!> _". wp_smart_apply "Hf1".
  - iIntros "!> _". wp_smart_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
Ralf Jung's avatar
Ralf Jung committed
103
104
Qed.
End proof.
Ralf Jung's avatar
Ralf Jung committed
105
106
107
108
109
110
111
112
113

(* 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
114
  Lemma client_safe :  WP client {{ _, True }}.
115
  Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
116
    rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
117
118
    wp_let. wp_smart_apply wp_par.
    - wp_smart_apply "Hf1".
Ralf Jung's avatar
Ralf Jung committed
119
120
121
122
123
124
125
126
127
128
129
    - 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
130
Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
Ralf Jung's avatar
Ralf Jung committed
131
132
133
134
135

(* Since we check the output of the test files, this means
our test suite will fail if we ever accidentally add an axiom
to anything used by this proof. *)
Print Assumptions client_adequate.