translation.v 21.2 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1
From iris.heap_lang Require Export proofmode notation.
2
From iris.heap_lang Require Import assert par.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.algebra Require Import frac auth.
4
5
6
From iris_c.lib Require Import mset flock list.
From iris_c.lib Require Export locking_heap U.
From iris_c.c_translation Require Export monad.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
From iris_c.c_translation Require Import proofmode.
Léon Gondelman's avatar
Léon Gondelman committed
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
11
Notation "♯ₗ l" := (a_ret (cloc_to_val l)) (at level 8, format "♯ₗ l") : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
12

13
14
15
16
Definition a_alloc : val := λ: "x1" "x2",
  "vv" ←ᶜ "x1" ||| "x2" ;;
  let: "n" := Fst "vv" in
  let: "v" := Snd "vv" in
17
  a_atomic_env (λ: <>, (ref (SOME (lreplicate "n" "v")), #0)).
18
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
Léon Gondelman's avatar
Léon Gondelman committed
19

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
Definition a_free_check : val :=
  rec: "go" "env" "l" "i" "n" :=
  if: "i" < "n" then
    assert: (mset_member ("l", "i") "env" = #false);;
    "go" "env" "l" (#1 + "i") "n"
  else #().

Definition a_free : val := λ: "x",
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
    let: "l" := Fst "v" in
    let: "i" := Snd "v" in
    match: !"l" with
      NONE => assert #false (* double free *)
    | SOME "l" =>
       (* We need to make sure `i = 0` and that all `0 ... length of block` are
       unlocked. TODO: this means we need to change the spec of `alloc` back so
       that we can actually establish we initially have the pointer to the first
       element of the array. *)
       assert ("i" = #0);;
       let: "n" := llength "l" in
       a_free_check "env" "l" #0 "n"
       "l" <- NONE
    end
  ).

Léon Gondelman's avatar
Léon Gondelman committed
46
Definition a_store : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
    let: "l" := Fst (Fst "vv") in
    let: "i" := Snd (Fst "vv") in
    let: "v" := Snd "vv" in
    mset_add ("l", "i") "env" ;;
53
54
55
56
    match: !"l" with
      NONE => assert #false (* store after free *)
    | SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
  ).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
Léon Gondelman's avatar
Léon Gondelman committed
59
60

Definition a_load : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
  "v" ←ᶜ "x";;
  a_atomic_env (λ: "env",
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
    let: "l" := Fst "v" in
    let: "i" := Snd "v" in
    assert: (mset_member ("l", "i") "env" = #false);;
66
67
68
69
    match: !"l" with
      NONE => assert #false (* load after free *)
    | SOME "ll" => llookup "i" "ll"
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
  ).
Notation "∗ᶜ e" :=
  (a_load e)%E (at level 9, right associativity) : expr_scope.
Léon Gondelman's avatar
Léon Gondelman committed
73
74

Definition a_un_op (op : un_op) : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
  "v" ←ᶜ "x" ;;
  a_ret (UnOp op "v").
Léon Gondelman's avatar
Léon Gondelman committed
77

Dan Frumin's avatar
Dan Frumin committed
78
79
80
81
(*Definition a_pre_un_op (op : un_op) : val := λ: "x",
  "l" ←ᶜ "x" ;;ᶜ
  a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*)

Léon Gondelman's avatar
Léon Gondelman committed
82
Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
85
86
87
88
89
90
91
92
  "vv" ←ᶜ "x1" ||| "x2" ;;
  a_ret (BinOp op (Fst "vv") (Snd "vv")).
Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
Léon Gondelman's avatar
Léon Gondelman committed
93

Dan Frumin's avatar
Dan Frumin committed
94
95
Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y",
  "lv" ←ᶜ ("x" ||| "y");;
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
  a_atomic (λ: <>,
    "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
    a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
Dan Frumin's avatar
Dan Frumin committed
99
100
101
    a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.

Léon Gondelman's avatar
Léon Gondelman committed
102
103
(* M () *)
(* The eta expansion is used to turn it into a value *)
104
105
Definition a_seq : val := λ: <>,
  a_atomic_env (λ: "env", mset_clear "env").
Dan Frumin's avatar
Dan Frumin committed
106

Robbert Krebbers's avatar
Nits.    
Robbert Krebbers committed
107
Definition a_seq_bind : val := λ: "f" "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
112
113
114
  "a" ←ᶜ "x" ;;
  a_seq #() ;;
  "f" "a".
Notation "e1 ;ᶜ e2" :=
  (a_seq_bind (λ: <>, e2) e1)%E
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
115
116

Definition a_if : val := λ: "cnd" "e1" "e2",
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
121
122
  "c" ←ᶜ "cnd" ;;
  if: "c" then "e1" #() else "e2" #().
Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
  (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
  (at level 200, e1, e2, e3 at level 200,
   format "'ifᶜ'  ( e1 )  {  e2  }  'elseᶜ'  {  e3  }") : expr_scope.
123

Robbert Krebbers's avatar
WIP    
Robbert Krebbers committed
124
125
Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
129
    a_if ("cnd" #()) (λ: <>, "bdy" #() ; "while" "cnd" "bdy") a_seq%E.
Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
  (at level 200, e1, e2 at level 200,
   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
130

Dan Frumin's avatar
Dan Frumin committed
131
132
Definition a_invoke: val := λ: "f" "arg",
  a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
133
134
135
136
137
Notation "f ❲ a ❳ " :=
  ( a_invoke f a)%E
  (at level 100, a at level 200,
   format "f ❲ a ❳") : expr_scope.

Dan Frumin's avatar
Dan Frumin committed
138
139
Definition a_ptr_add : val := λ: "x" "y",
  "lo" ←ᶜ ("x" ||| "y");;
140
  let: "o'" := Snd (Fst "lo") + Snd "lo" in
Dan Frumin's avatar
Dan Frumin committed
141
142
143
144
145
146
  a_ret (Fst (Fst "lo"), "o'").

Definition a_ptr_lt : val := λ: "x" "y",
  "pq" ←ᶜ ("x" ||| "y");;
  let: "p" := Fst "pq" in
  let: "q" := Snd "pq" in
147
  if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false.
Dan Frumin's avatar
Dan Frumin committed
148
149
Notation "e1 +∗ᶜ e2" := (a_ptr_add e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <∗ᶜ e2" := (a_ptr_lt e1%E e2%E)  (at level 80) : expr_scope.
150

Dan Frumin's avatar
Dan Frumin committed
151
Section proofs.
152
  Context `{amonadG Σ}.
Dan Frumin's avatar
Dan Frumin committed
153

Dan Frumin's avatar
Dan Frumin committed
154
  Lemma a_alloc_spec R Φ Ψ1 e1 e2 :
155
    AWP e1 @ R {{ Ψ1 }} -
Dan Frumin's avatar
Dan Frumin committed
156
157
    AWP e2 @ R {{ v2,  ( v1, Ψ1 v1 -  n : nat,
                           v1 = #n  
158
                           l, l C replicate n v2 - Φ (cloc_to_val l)) }} -
159
    AWP alloc(e1, e2) @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
160
  Proof.
Dan Frumin's avatar
Dan Frumin committed
161
    iIntros "H1 HΦ".
162
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
Dan Frumin's avatar
Dan Frumin committed
163
    awp_apply (a_wp_awp with "HΦ"); iIntros (v2) "H2". awp_lam.
164
165
    iApply awp_bind. iApply (awp_par with "H1 H2").
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
Dan Frumin's avatar
Dan Frumin committed
166
    iDestruct ("H2" with "H1") as (n ->) "HΦ".
Dan Frumin's avatar
Dan Frumin committed
167
    iApply awp_atomic_env.
168
169
170
171
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
    iApply wp_fupd. wp_alloc l as "Hl".
    iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
172
    iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))].
173
174
175
    iExists X, _. iFrame.
    iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
    exists cl; split; first done. by rewrite locked_locs_alloc_heap.
176
177
  Qed.

Robbert Krebbers's avatar
WIP    
Robbert Krebbers committed
178
  Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
179
180
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ Ψ2 }} -
181
182
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  cl w,
                 v1 = cloc_to_val cl   cl C w  (cl C[LLvl] v2 - Φ v2)) -
183
    AWP e1 = e2 @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
184
  Proof.
Robbert Krebbers's avatar
WIP    
Robbert Krebbers committed
185
    iIntros "H1 H2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
    iApply awp_bind. iApply (awp_par with "H1 H2").
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
190
    iDestruct ("HΦ" with "H1 H2") as ([l i] w ->) "[Hl HΦ]".
Dan Frumin's avatar
Dan Frumin committed
191
    iApply awp_atomic_env.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1.
194
195
196
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_store with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
198
199
    wp_apply (mset_add_spec with "[$]"); first done.
    iIntros "Hlocks /="; wp_seq.
200
    wp_load; wp_match.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
204
205
    wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
    iApply wp_fupd. wp_store.
    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
    iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists ({[(#l, #i)%V]}  X), _. iFrame "Hσ". rewrite locked_locs_lock.
206
207
208
    iIntros "{$Hlocks} !%".
    intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
    eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
Dan Frumin's avatar
Dan Frumin committed
209
210
  Qed.

211
  Lemma a_load_spec_exists_frac R Φ e :
212
213
    AWP e @ R {{ v,  cl q w,  v = cloc_to_val cl  
                              cl C{q} w  (cl C{q} w - Φ w) }} -
214
    AWP ∗ᶜe @ R {{ Φ }}.
215
  Proof.
216
217
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
219
    iIntros (v). iDestruct 1 as ([l i] q w ->) "[Hl HΦ]". awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
222
    iApply awp_atomic_env. iIntros (env) "Henv HR".
    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv.
223
224
225
    assert ((#l, #i)%V  X).
    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
    iMod (locking_heap_load with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
    wp_let. wp_proj; wp_let. wp_proj; wp_let.
    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
228
    rewrite bool_decide_false //.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
    wp_op. iSplit; first done. iNext; wp_seq.
230
    wp_load; wp_match. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
233
    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
    iExists X, _. by iFrame.
234
235
  Qed.

236
  Lemma a_load_spec R Φ q e :
237
238
239
    AWP e @ R {{ v,  cl w,
                     v = cloc_to_val cl  
                    cl C{q} w  (cl C{q} w - Φ w) }} -
240
    AWP ∗ᶜe @ R {{ Φ }}.
241
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
    iIntros "H". iApply a_load_spec_exists_frac.
243
    awp_apply (awp_wand with "H").
244
    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
245
246
247
  Qed.

  Lemma a_un_op_spec R Φ e op:
248
    AWP e @ R {{ v,  w : val, un_op_eval op v = Some w  Φ w }} -
Dan Frumin's avatar
Dan Frumin committed
249
    AWP a_un_op op e @ R {{ Φ }}.
250
251
252
253
254
255
256
257
258
  Proof.
    iIntros "H".
    awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam.
    iApply awp_bind.
    iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam.
    iDestruct "HΦ" as (w0) "[% H]".
    iApply awp_ret. by wp_op.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
  (*
  Lemma a_pre_un_op_spec R Φ e op :
    AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝
                        ∗ ⌜un_op_eval op v = Some w⌝
                        ∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗
    AWP a_pre_un_op op e @ R {{ Φ }}.
  Proof.
    iIntros "He". rewrite /a_pre_un_op.
    awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam.
    iApply awp_bind. iApply (awp_wand with "HΦ").
    iIntros (vl) "H". awp_lam.
    iApply awp_atomic. iNext.
    iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)".
    simplify_eq/=.
    iExists True%I. rewrite left_id. awp_lam.
    iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I
                             (λ v', ⌜v' = w⌝ ∗ l ↦C v)%I
              with "[] [Hl] [-]").
    - iApply awp_ret. by wp_value_head.
    - iApply a_un_op_spec. iApply a_load_spec.
      iApply awp_ret. wp_value_head.
      iExists _,_; iFrame. iSplit; eauto.
    - iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=.
      iExists _,_; iFrame. iSplit; eauto.
      iIntros "? _". by iApply "HΦ".
  Qed.
  *)

287
  Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
288
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
289
     ( v1 v2, Ψ1 v1 - Ψ2 v2 -  w, bin_op_eval op v1 v2 = Some w  Φ w) -
Dan Frumin's avatar
Dan Frumin committed
290
    AWP a_bin_op op e1 e2 @ R {{ Φ }}.
291
292
293
294
295
  Proof.
    iIntros "H1 H2 HΦ".
    awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
    awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
    iApply awp_bind.
296
    iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
297
298
299
300
301
302
    iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
    iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
    iSpecialize ("HΦ" with "HΨ1 HΨ2").
    iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
303
304
305
  Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
    AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
     ( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
306
307
308
309
         cl v w,  v1 = cloc_to_val cl  
                  cl C v 
                   bin_op_eval op v v2 = Some w  
                  (cl C[LLvl] w - R  Φ v)) -
Dan Frumin's avatar
Dan Frumin committed
310
311
312
313
314
315
    AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
Dan Frumin's avatar
Dan Frumin committed
317
    iApply awp_atomic. iNext.
318
    iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
Dan Frumin's avatar
Dan Frumin committed
319
320
    simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
    iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
321
    iExists cl, v; iFrame. iSplit; first done.
Dan Frumin's avatar
Dan Frumin committed
322
    iIntros "Hl". awp_let. iApply awp_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
    iApply (a_store_spec _ _
324
      (λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
Dan Frumin's avatar
Dan Frumin committed
325
    - awp_proj. iApply awp_ret; by wp_value_head.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
    - iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
Dan Frumin's avatar
Dan Frumin committed
327
328
329
        try (try awp_proj; iApply awp_ret; by wp_value_head).
      iNext. iIntros (? ? -> ->). eauto.
    - iNext. iIntros (? ? -> ->).
330
      iExists _, _; iFrame. iSplit; first done.
Dan Frumin's avatar
Dan Frumin committed
331
332
333
334
      iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
      iIntros "_". by iApply "HΦ".
  Qed.

335
336
  Lemma a_seq_spec R Φ :
    U (Φ #()) -
337
    AWP (a_seq #()) @ R {{ Φ }}.
338
339
  Proof.
    iIntros "HΦ". rewrite /a_seq. awp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
    iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
    iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
    wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
343
    iDestruct "HΦ" as (us) "[Hus HΦ]".
Dan Frumin's avatar
Dan Frumin committed
344
    iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
346
    - iModIntro. iSplitR "HΦ".
      + iExists , σ. by iFrame.
347
348
      + by iApply "HΦ".
    - iDestruct "Hus" as "[Hu Hus]".
Dan Frumin's avatar
Dan Frumin committed
349
350
      iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz].
      iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
Robbert Krebbers's avatar
Robbert Krebbers committed
351
352
      iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
      iIntros "Hus". iApply "HΦ". by iFrame.
353
354
355
356
  Qed.

  Lemma a_sequence_spec R Φ (f e : expr) :
    AsVal f 
357
358
     AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
    AWP a_seq_bind f e @ R {{ Φ }}.
359
  Proof.
360
    iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
361
362
363
364
365
366
    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
    awp_lam. iApply awp_bind. iApply a_seq_spec.
    iModIntro. by awp_lam.
  Qed.

367
368
  Lemma a_sequence_spec' R Φ (e e' : expr) :
    Closed [] e' 
369
370
     AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -
    AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}.
371
372
373
374
375
376
377
  Proof.
    iIntros (?) "He".
    iApply a_sequence_spec.
    iApply (awp_wand with "He"). iNext.
    iIntros (?) "He'". iModIntro. by awp_lam.
  Qed.

378
  Lemma a_while_spec  R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
Robbert Krebbers's avatar
Robbert Krebbers committed
379
380
     AWP a_if c (λ: <>, (λ: <>, b) #() ; while (c) { b }) a_seq @ R {{ Φ }} -
    AWP while (c) { b } @ R {{ Φ }}.
381
382
383
384
385
386
387
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply "H".
  Qed.

  Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Robbert Krebbers's avatar
Robbert Krebbers committed
388
389
    AsVal e1 
    AsVal e2 
390
391
392
    AWP e @ R {{ v, (v = #true  AWP e1 #() @ R {{ Φ }}) 
                    (v = #false  AWP e2 #() @ R {{ Φ }}) }} -
    AWP a_if e e1 e2 @ R {{ Φ }}.
393
  Proof.
394
    iIntros ([v1 <-] [v2 <-]) "H".
395
396
397
398
399
    awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
    iApply awp_bind. iApply (awp_wand with "H"). clear v.
    iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
  Qed.

400
  Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
401
402
403
    AWP e @ R {{ v, (v = #true  AWP e1 @ R {{ Φ }}) 
                    (v = #false  AWP e2 @ R {{ Φ }}) }} -
    AWP if (e) { e1 } else { e2 } @ R {{ Φ }}.
404
405
406
407
408
409
410
  Proof.
    iIntros "He". iApply a_if_spec.
    iApply (awp_wand with "He").
    iIntros (v) "[[% Hv] | [% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto; by awp_lam.
  Qed.

  Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
411
412
413
     AWP c @ R {{ v, v = #true  AWP b @ R {{ _, U (AWP while (c) { b } @ R {{ Φ }}) }}
                     v = #false  AWP a_seq #() @ R {{ Φ }} }} -
    AWP while (c) { b } @ R {{ Φ }}.
414
415
416
417
418
419
420
421
422
423
  Proof.
    iIntros "H".
    awp_lam. awp_lam. awp_seq.
    iApply a_if_spec.
    iApply (awp_wand with "H").
    iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto.
    awp_seq. iApply a_sequence_spec'. iNext.
    awp_seq. done.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
424
  Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
Dan Frumin's avatar
Dan Frumin committed
425
    IntoVal ef f 
426
427
428
    AWP ea @ R {{ Ψ }} -
    ( a, Ψ a - U (R -  R', R'  (AWP ef a @ R' {{ v, R' - R  Φ v }}))) -
    AWP a_invoke ef ea @ R {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
429
  Proof.
430
    rewrite /IntoVal. iIntros (<-) "Ha Hfa".
Dan Frumin's avatar
Dan Frumin committed
431
432
433
434
435
    rewrite /a_invoke. awp_lam.
    awp_apply (a_wp_awp R with "Ha").
    iIntros (a) "Ha". awp_let.
    iApply a_sequence_spec.
    iApply (awp_wand with "Ha"). clear a.
436
    iNext. iIntros (a) "HΨ".
437
438
    iSpecialize ("Hfa" with "HΨ").
    iModIntro.
Dan Frumin's avatar
Dan Frumin committed
439
    awp_let.
Dan Frumin's avatar
Dan Frumin committed
440
    iApply awp_atomic. iNext. iIntros "HR".
Dan Frumin's avatar
Dan Frumin committed
441
442
    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
    iExists R'. iFrame. by awp_let.
Dan Frumin's avatar
Dan Frumin committed
443
444
  Qed.

445
  Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
446
447
    AWP e1 @ R {{ Φ }} -
    AWP if (true) { e1 } else { e2 } @ R {{ Φ }}.
448
449
450
451
452
453
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iLeft. iSplit; eauto. by awp_seq.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
454

455
  Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
456
457
    AWP e2 @ R {{ Φ }} -
    AWP if (false) { e1 } else { e2 } @ R {{ Φ }}.
458
459
460
461
462
463
464
  Proof.
    iIntros "HΦ".
    iApply a_if_spec.
    iApply awp_ret. iApply wp_value.
    iRight. iSplit; eauto. by awp_seq.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
465
466
467
468
469
  Lemma a_ptr_add_spec R Φ Ψ2 e1 e2 :
    AWP e2 @ R {{ Ψ2 }} -
    AWP e1 @ R {{ v1,   v2, Ψ2 v2 -  cl (n : nat),
                          v1 = cloc_to_val cl  
                          v2 = #n  
470
                         Φ (cloc_to_val (cloc_add cl n)) }} -
Dan Frumin's avatar
Dan Frumin committed
471
472
473
474
475
476
477
    AWP a_ptr_add e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He2 HΦ". rewrite /a_ptr_add.
    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
478
479
480
    iDestruct ("Hv1" with "Hv2") as ([l o] n -> ->) "HΦ /=".
    do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
    iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add.
Dan Frumin's avatar
Dan Frumin committed
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
  Qed.

  Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
    AWP e1 @ R {{ Ψ1 }} -
    AWP e2 @ R {{ v2,   v1, Ψ1 v1 -  p q,
                          v1 = cloc_to_val p  
                          v2 = cloc_to_val q  
                         Φ #(cloc_lt p q) }} -
    AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
  Proof.
    iIntros "He1 HΦ". rewrite /a_ptr_add.
    awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
    awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
496
497
498
499
500
501
502
503
504
505
506
    iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
    do 2 (awp_proj; awp_let). do 2 awp_proj.
    unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op.
    - destruct Hp as [-> ?%Nat2Z.inj_lt].
      rewrite bool_decide_true //. awp_if. do 2 awp_proj.
      iApply awp_ret. wp_op. rewrite bool_decide_true //.
    - apply not_and_l_alt in Hp as [?|[? ->]].
      + rewrite bool_decide_false; last congruence.
        awp_if. iApply awp_ret. by iApply wp_value.
      + rewrite bool_decide_true //. awp_if. iApply awp_ret. do 2 wp_proj.
        wp_op. by rewrite bool_decide_false; last lia.
Dan Frumin's avatar
Dan Frumin committed
507
508
  Qed.

509
510
  Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
    I -
511
     (I - AWP c @ R {{ v, (v = #false  U (Φ #())) 
512
                            (v = #true   AWP b @ R {{ _, U I }}) }}) -
513
    AWP while (c) { b } @ R {{ Φ }}.
514
515
516
517
518
519
520
521
   Proof.
     iIntros "Hi #Hinv". iLöb as "IH".
     iApply a_while_spec. iNext.
     iApply a_if_spec.
     iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv").
     iIntros (v) "[(% & H) | (% & H)] //="; subst.
     - iRight. iSplit; by eauto; iApply a_seq_spec.
     - iLeft. iSplit; first eauto. awp_seq.
522
       iApply a_sequence_spec. iNext. awp_seq.
523
       iApply (awp_wand with "H").
524
       iIntros (v) "Hi !>". awp_seq.
525
526
       by iApply ("IH" with "Hi").
   Qed.
Dan Frumin's avatar
Dan Frumin committed
527
End proofs.
Dan Frumin's avatar
Dan Frumin committed
528
529

(* Make sure that we only use the provided rules and don't break the abstraction *)
530
531
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.