lifting.v 35.8 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
4
From refinedc.lang Require Export lang ghost_state notation.
Michael Sammler's avatar
Michael Sammler committed
5
6
7
8
9
10
11
12
13
From refinedc.lang Require Import tactics.
Set Default Proof Using "Type".
Import uPred.

Class refinedcG Σ := RefinedCG {
  refinedcG_invG : invG Σ;
  refinedcG_gen_heapG :> heapG Σ
}.

14
Instance c_irisG `{!refinedcG Σ} : irisG c_lang Σ := {
Michael Sammler's avatar
Michael Sammler committed
15
  iris_invG := refinedcG_invG;
Michael Sammler's avatar
Michael Sammler committed
16
  state_interp σ κs _ _ := state_ctx σ;
Michael Sammler's avatar
Michael Sammler committed
17
  fork_post _ := True%I;
Michael Sammler's avatar
Michael Sammler committed
18
19
  num_laters_per_step _ := 0%nat;
  state_interp_mono _ _ _ _ := fupd_intro _ _;
Michael Sammler's avatar
Michael Sammler committed
20
21
22
}.
Global Opaque iris_invG.

23
Instance into_val_val v : IntoVal (to_rtexpr (Val v)) v.
Michael Sammler's avatar
Michael Sammler committed
24
25
26
27
28
29
30
31
32
Proof. done. Qed.

Local Hint Extern 0 (reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Unfold heap_at : core.


Local Ltac solve_atomic :=
  apply strongly_atomic_atomic, ectx_language_atomic;
33
34
    [inversion 1; unfold coerce_rtexpr in *; simplify_eq; inv_expr_step; naive_solver
    |unfold coerce_rtexpr in *;apply ectxi_language_sub_redexes_are_values; intros [[]|[]] **; naive_solver].
Michael Sammler's avatar
Michael Sammler committed
35

36
Instance cas_atomic s ot (v1 v2 v3 : val) : Atomic s (coerce_rtexpr (CAS ot v1 v2 v3)).
Michael Sammler's avatar
Michael Sammler committed
37
Proof. solve_atomic. Qed.
38
Instance skipe_atomic s (v : val) : Atomic s (coerce_rtexpr (SkipE v)).
Michael Sammler's avatar
Michael Sammler committed
39
Proof. solve_atomic. Qed.
40
41
42
Instance deref_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Deref ScOrd ly l)).
Proof. solve_atomic. Qed.
Instance use_atomic s (l : loc) ly : Atomic s (coerce_rtexpr (Use ScOrd ly l)).
43
Proof. solve_atomic. Qed.
Michael Sammler's avatar
Michael Sammler committed
44

45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(*** General lifting lemmas *)

Section lifting.
  Context `{!refinedcG Σ}.
  Lemma wp_alloc_failed E Φ:
     WP AllocFailed @ E {{ Φ }}.
  Proof.
    iLöb as "IH".
    iApply wp_lift_pure_det_head_step_no_fork' => //; first by eauto using AllocFailedStep.
    move => ????? . inversion 1; simplify_eq => //.
    match goal with | H: to_rtexpr ?e = AllocFailed |- _ => destruct e; discriminate end.
  Qed.

  Lemma wp_c_lift_step_fupd E e step_rel Φ:
    (( e', e = to_rtexpr e'  step_rel = expr_step e') 
     ( rf s, e = to_rtstmt rf s  step_rel = stmt_step s rf)) 
    to_val e = None 
    ( (σ1 : state), state_ctx σ1 ={E,}=
        os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl 
64
        ( os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
65
66
67
68
69
          ={}=  (|={,E}=> tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }})))
      - WP e @ E {{ Φ }}.
  Proof.
    iIntros (He ?) "HWP".
    iApply wp_lift_head_step_fupd => //.
70
71
    iIntros (σ1 κ κs n ?) "[[% Hhctx] Hfnctx]".
    iMod ("HWP" $! σ1 with "[$Hhctx $Hfnctx//]") as (Hstep) "HWP".
72
73
74
75
76
    iModIntro. iSplit. {
      iPureIntro. destruct Hstep as (?&?&?&?&?).
      naive_solver eauto using ExprStep, StmtStep.
    }
    clear Hstep. iIntros (??? Hstep).
77
    move: (Hstep) => /runtime_step_preserves_invariant?.
78
79
80
    destruct He as [[e' [??]]|[? [s [??]]]]; inversion Hstep; simplify_eq.
    all: try by [destruct e'; discriminate].
    all: try match goal with | H : to_rtexpr ?e = to_rtstmt _ _ |- _ => destruct e; discriminate end.
81
    all: iMod ("HWP" with "[//] [%]") as "HWP"; first naive_solver.
82
83
84
85
86
87
88
89
    all: do 2 iModIntro.
    all: iMod "HWP" as (->) "[$ HWP]"; iModIntro => /=; by rewrite right_id.
  Qed.

  Lemma wp_lift_expr_step_fupd E (e : expr) Φ:
    to_val e = None 
    ( (σ1 : state), state_ctx σ1 ={E,}=
        os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl 
90
        ( os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
91
92
93
94
95
96
97
          ={}=  (|={,E}=> tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }})))
      - WP e @ E {{ Φ }}.
  Proof. iIntros (?) "HWP". iApply wp_c_lift_step_fupd => //. naive_solver. Qed.

  Lemma wp_lift_stmt_step_fupd E s rf Φ:
    ( (σ1 : state), state_ctx σ1 ={E,}=
        os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl 
98
        ( os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
99
100
101
102
103
104
105
106
107
108
          ={}=  (|={,E}=> tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }})))
      - WP to_rtstmt rf s @ E {{ Φ }}.
  Proof. iIntros "HWP". iApply wp_c_lift_step_fupd => //. naive_solver. Qed.

  Lemma wp_c_lift_step E e step_rel Φ:
    (( e', e = to_rtexpr e'  step_rel = expr_step e') 
     ( rf s, e = to_rtstmt rf s  step_rel = stmt_step s rf)) 
    to_val e = None 
    ( (σ1 : state), state_ctx σ1 ={E}=
        os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl 
109
         ( os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
110
111
112
113
114
115
          ={E}= tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }}))
      - WP e @ E {{ Φ }}.
  Proof.
    iIntros (??) "HWP".
    iApply wp_c_lift_step_fupd => //.
    iIntros (?) "Hσ". iMod ("HWP" with "Hσ") as "[$ HWP]".
Michael Sammler's avatar
Michael Sammler committed
116
    iApply fupd_mask_intro; first set_solver. iIntros "HE".
117
    iIntros (??????) "!> !>". iMod "HE". by iMod ("HWP" with "[//] [//]") as "$".
118
119
120
121
122
123
  Qed.

  Lemma wp_lift_expr_step E (e : expr) Φ:
    to_val e = None 
    ( (σ1 : state), state_ctx σ1 ={E}=
        os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl 
124
         ( os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
125
126
127
128
129
130
131
          ={E}= tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }}))
      - WP e @ E {{ Φ }}.
  Proof. iIntros (?) "HWP". iApply wp_c_lift_step => //. naive_solver. Qed.

  Lemma wp_lift_stmt_step E s rf Φ:
    ( (σ1 : state), state_ctx σ1 ={E}=
        os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl 
132
         ( os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
133
134
135
136
137
          ={E}= tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }}))
      - WP to_rtstmt rf s @ E {{ Φ }}.
  Proof. iIntros "HWP". iApply wp_c_lift_step => //. naive_solver. Qed.

End lifting.
Michael Sammler's avatar
Michael Sammler committed
138

139
(*** Lifting of expressions *)
Michael Sammler's avatar
Michael Sammler committed
140
141
142
Section expr_lifting.
Context `{!refinedcG Σ}.

143
144
145
146
147
Lemma wp_binop v1 v2 Φ op E ot1 ot2:
  ( σ, state_ctx σ -
     v', eval_bin_op op ot1 ot2 σ v1 v2 v' 
     ( v', eval_bin_op op ot1 ot2 σ v1 v2 v' - state_ctx σ  Φ v')) -
  WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
148
Proof.
149
  iIntros "HΦ".
150
151
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "Hctx !>".
152
  iDestruct ("HΦ" with "Hctx") as ([v' Heval]) "HΦ".
153
  iSplit; first by eauto 8 using BinOpS.
154
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
155
156
  iDestruct ("HΦ" with "[//]") as "[$ HΦ]".
  iModIntro. iSplit => //. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
157
158
159
Qed.

Lemma wp_binop_det v' v1 v2 Φ op E ot1 ot2:
160
161
  ( σ v, state_ctx σ - eval_bin_op op ot1 ot2 σ v1 v2 v  v = v')   Φ v' -
    WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
162
Proof.
163
164
165
166
167
168
169
  iIntros "H".
  iApply wp_binop. iIntros (σ) "Hctx". iSplit.
  { iExists v'. iDestruct "H" as "[Hσ _]". by iDestruct ("Hσ" with "Hctx") as %->. }
  iIntros "!>" (v Hbinop). iAssert (v = v')%I as %->.
  { iDestruct "H" as "[Hσ _]". iDestruct ("Hσ" with "Hctx") as %Hvv'.
    iPureIntro. naive_solver. }
  by iDestruct "H" as "[_ $]".
Michael Sammler's avatar
Michael Sammler committed
170
171
Qed.

172
173
174
175
Lemma wp_unop v1 Φ op E ot:
  ( σ, state_ctx σ -
     v', eval_un_op op ot σ v1 v' 
     ( v', eval_un_op op ot σ v1 v' - state_ctx σ  Φ v')) -
Michael Sammler's avatar
Michael Sammler committed
176
177
   WP UnOp op ot (Val v1) @ E {{ Φ }}.
Proof.
178
  iIntros "HΦ".
179
180
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "Hctx !>".
181
  iDestruct ("HΦ" with "Hctx") as ([v' Heval]) "HΦ".
182
  iSplit; first by eauto 8 using UnOpS.
183
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
184
185
  iDestruct ("HΦ" with "[//]") as "[$ HΦ]".
  iModIntro. iSplit => //. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
186
187
188
Qed.

Lemma wp_unop_det v' v1 Φ op E ot:
189
190
  ( σ v, state_ctx σ - eval_un_op op ot σ v1 v  v = v')   Φ v' -
  WP UnOp op ot (Val v1) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
191
Proof.
192
193
194
195
196
197
198
  iIntros "H".
  iApply wp_unop. iIntros (σ) "Hctx". iSplit.
  { iExists v'. iDestruct "H" as "[Hσ _]". by iDestruct ("Hσ" with "Hctx") as %->. }
  iIntros "!>" (v Hbinop). iAssert (v = v')%I as %->.
  { iDestruct "H" as "[Hσ _]". iDestruct ("Hσ" with "Hctx") as %Hvv'.
    iPureIntro. naive_solver. }
  by iDestruct "H" as "[_ $]".
Michael Sammler's avatar
Michael Sammler committed
199
200
Qed.

201
202
Lemma wp_deref v Φ vl l ly q E o:
  o = ScOrd  o = Na1Ord 
Michael Sammler's avatar
Michael Sammler committed
203
204
205
  val_to_loc vl = Some l 
  l `has_layout_loc` ly 
  v `has_layout_val` ly 
206
  l{q}v -  (l {q} v - Φ v) - WP !{ly, o} (Val vl) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
207
Proof.
208
  iIntros (Ho Hl Hll Hlv) "Hmt HΦ".
209
  iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
210
  iIntros ([[h ub] fn]) "((%&Hhctx&Hactx)&Hfctx)/=".
211
  iDestruct (heap_mapsto_has_alloc_id with "Hmt") as %Haid.
212
  destruct o; try by destruct Ho.
213
214
  - iModIntro. iDestruct (heap_mapsto_lookup_q (λ st,  n, st = RSt n) with "Hhctx Hmt") as %Hat. naive_solver.
    iSplit; first by eauto 11 using DerefS.
215
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
216
    iSplit => //. unfold end_st, end_expr.
217
218
    have <- : (v = v') by apply: heap_at_inj_val.
    rewrite /heap_fmap/=. erewrite heap_upd_heap_at_id => //.
219
    iFrame. iSplit; first done. iApply wp_value. by iApply "HΦ".
220
221
  - iMod (heap_read_na with "Hhctx Hmt") as "(% & Hσ & Hσclose)" => //. iModIntro.
    iSplit; first by eauto 11 using DerefS.
222
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
223
    iSplit => //. unfold end_st, end_expr.
224
225
    have ? : (v = v') by apply: heap_at_inj_val. subst v'.
    iFrame => /=. iSplit; first done.
226
    iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
227
    iIntros ([[h2 ub2] fn2]) "((%&Hhctx&Hactx)&Hfctx)/=".
228
229
    iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
    iModIntro; iSplit; first by eauto 11 using DerefS.
230
231
232
233
    iIntros "!#" (? e2 σ2 efs Hst ?) "!#". inv_expr_step. iSplit => //.
    have ? : (v = v') by apply: (heap_at_inj_val _ _ h2). subst.
    iFrame. iSplit; first done.
    iApply wp_value. by iApply "HΦ".
Michael Sammler's avatar
Michael Sammler committed
234
235
Qed.

236
237
238
239
240
241
242
(*
  Alternative version of the CAS rule which does not rely on the Atomic infrastructure:
  Lemma wp_cas vl1 vl2 vd Φ l1 l2 it E:
  val_to_loc vl1 = Some l1 →
  val_to_loc vl2 = Some l2 →
  (bytes_per_int it ≤ bytes_per_addr)%nat →
  (|={E, ∅}=> ∃ (q1 q2 : Qp) vo ve z1 z2,
243
     ⌜val_to_Z vo it = Some z1⌝ ∗ ⌜val_to_Z ve it = Some z2⌝ ∗
244
245
246
247
248
249
250
251
252
     ⌜l1 `has_layout_loc` it_layout it⌝ ∗ ⌜l2 `has_layout_loc` it_layout it⌝ ∗
     ⌜length vd = bytes_per_int it⌝ ∗ ⌜if bool_decide (z1 = z2) then q1 = 1%Qp else q2 = 1%Qp⌝ ∗
     l1↦{q1}vo ∗ l2↦{q2}ve ∗ ▷ (
       l1↦{q1} (if bool_decide (z1 = z2) then vd else vo) -∗
       l2↦{q2} (if bool_decide (z1 = z2) then ve else vo)
       ={∅, E}=∗ Φ (val_of_bool (bool_decide (z1 = z2))))) -∗
   WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
*)

Michael Sammler's avatar
Michael Sammler committed
253
254
255
256
257
Lemma wp_cas_fail vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it q E:
  val_to_loc vl1 = Some l1 
  val_to_loc vl2 = Some l2 
  l1 `has_layout_loc` it_layout it 
  l2 `has_layout_loc` it_layout it 
258
259
  val_to_Z_weak vo it = Some z1 
  val_to_Z_weak ve it = Some z2 
260
261
  length vd = bytes_per_int it 
  (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
262
263
264
265
266
  z1  z2 
  l1{q}vo - l2ve -  (l1 {q} vo - l2vo - Φ (val_of_bool false)) -
   WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
Proof.
  iIntros (Hl1 Hl2 Hly1 Hly2 Hvo Hve Hlen1 Hlen2 Hneq) "Hl1 Hl2 HΦ".
267
  iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
268
  iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
269
270
  iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
  iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
271
  move: (Hvo) (Hve) => /val_to_Z_weak_length ? /val_to_Z_weak_length ?.
Michael Sammler's avatar
Michael Sammler committed
272
273
  iDestruct (heap_mapsto_lookup_q (λ st : lock_state,  n : nat, st = RSt n) with "Hhctx Hl1") as %? => //. { naive_solver. }
  iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl2") as %? => //.
274
  iModIntro. iSplit; first by eauto 15 using CasFailS.
275
  iIntros (? e2 σ2 efs Hst ?) "!>". inv_expr_step;
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
276
277
    have ? : (vo = vo0) by [apply: heap_lookup_loc_inj_val => //; congruence];
    have ? : (ve = ve0) by [apply: heap_lookup_loc_inj_val => //; congruence]; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
278
  have ? : (length ve0 = length vo0) by congruence.
279
  iMod (heap_write with "Hhctx Hl2") as "[$ Hl2]" => //. iModIntro.
280
281
  iFrame. iSplit => //. iSplit; first done.
  iApply wp_value. by iApply ("HΦ" with "[$]").
Michael Sammler's avatar
Michael Sammler committed
282
283
284
285
286
287
288
Qed.

Lemma wp_cas_suc vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it E q:
  val_to_loc vl1 = Some l1 
  val_to_loc vl2 = Some l2 
  l1 `has_layout_loc` it_layout it 
  l2 `has_layout_loc` it_layout it 
289
290
  val_to_Z_weak vo it = Some z1 
  val_to_Z_weak ve it = Some z2 
291
292
  length vd = bytes_per_int it 
  (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
293
294
  z1 = z2 
  l1vo - l2{q}ve -  (l1  vd - l2{q}ve - Φ (val_of_bool true)) -
295
  WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
296
Proof.
297
298
  iIntros (Hl1 Hl2 Hly1 Hly2 Hvo Hve Hlen1 Hlen2 Hneq) "Hl1 Hl2 HΦ".
  iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
299
  iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
300
301
  iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
  iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
302
  move: (Hvo) (Hve) => /val_to_Z_weak_length ? /val_to_Z_weak_length ?.
Michael Sammler's avatar
Michael Sammler committed
303
304
  iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl1") as %? => //.
  iDestruct (heap_mapsto_lookup_q (λ st : lock_state,  n : nat, st = RSt n) with "Hhctx Hl2") as %? => //. { naive_solver. }
305
  iModIntro. iSplit; first by eauto 15 using CasSucS.
306
  iIntros (? e2 σ2 efs Hst ?) "!>". inv_expr_step;
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
307
308
      have ? : (ve = ve0) by [apply: heap_lookup_loc_inj_val => //; congruence];
      have ? : (vo = vo0) by [apply: heap_lookup_loc_inj_val => //; congruence]; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
309
  have ? : (length vo0 = length vd) by congruence.
310
  iMod (heap_write with "Hhctx Hl1") as "[$ Hmt]" => //. iModIntro.
311
312
  iFrame. iSplit => //. iSplit; first done.
  iApply wp_value. by iApply ("HΦ" with "[$]").
Michael Sammler's avatar
Michael Sammler committed
313
314
315
Qed.

Lemma wp_neg_int Φ v v' n E it:
316
  val_to_Z_weak v it = Some n 
317
  val_of_Z (-n) it = Some v' 
Michael Sammler's avatar
Michael Sammler committed
318
319
320
   Φ (v') - WP UnOp NegOp (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv Hv') "HΦ".
321
322
323
324
  iApply wp_unop_det. iSplit => //.
  iIntros (σ v2) "_ !%". split.
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
325
326
Qed.

327
328
329
Lemma wp_cast_int Φ v v' i E its itt:
  val_to_int_repr v its = Some i 
  val_of_int_repr i itt = Some v' 
Michael Sammler's avatar
Michael Sammler committed
330
331
332
   Φ (v') - WP UnOp (CastOp (IntOp itt)) (IntOp its) (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv Hv') "HΦ".
333
334
335
336
  iApply wp_unop_det. iSplit => //.
  iIntros (σ v2) "_ !%". split.
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
337
338
339
340
341
342
343
Qed.

Lemma wp_cast_loc Φ v l E:
  val_to_loc v = Some l 
   Φ (val_of_loc l) - WP UnOp (CastOp PtrOp) PtrOp (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv) "HΦ".
344
345
346
347
  iApply wp_unop_det. iSplit => //.
  iIntros (σ v2) "_ !%". split.
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
348
349
Qed.

350
351
Lemma wp_cast_ptr_int Φ v v' l E it:
  val_to_loc v = Some l 
352
  val_of_int_repr (IRLoc l) it = Some v' 
353
354
355
356
357
358
359
360
361
   Φ (v') - WP UnOp (CastOp (IntOp it)) PtrOp (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv Hv') "HΦ".
  iApply wp_unop_det. iSplit => //.
  iIntros (σ ?) "_ !%". split.
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Qed.

362
363
364
Lemma wp_cast_int_ptr Φ v l E it:
  val_to_loc_weak v it = Some l 
   Φ (val_of_loc l) - WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
365
366
367
368
369
370
371
372
373
374
375
Proof.
  iIntros (Hv) "HΦ".
  iApply wp_unop_det. iSplit => //.
  iIntros (σ ?) "_ !%". split.
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Qed.

Lemma wp_copy_alloc_id Φ l1 l2 v1 v2 E:
  val_to_loc v1 = Some l1 
  val_to_loc v2 = Some l2 
376
   Φ (val_of_loc (l2.1, l1.2)) - WP CopyAllocId PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
377
Proof.
378
  iIntros (Hl1 Hl2) "HΦ". iApply wp_lift_expr_step => //.
379
380
381
382
383
384
385
386
387
388
389
390
  iIntros (σ1) "Hctx !>". iSplit; first by eauto 8 using CopyAllocIdPS.
  iIntros "!>" (???? Hstep ?) "!>". inv_expr_step. iSplit => //. iFrame.
  by iApply wp_value.
Qed.

Lemma wp_copy_alloc_id_int Φ it l1 l2 v1 v2 E:
  val_to_loc v1 = Some l1 
  val_to_loc_weak v2 it = Some l2 
   Φ (val_of_loc (l2.1, l1.2)) - WP CopyAllocId (IntOp it) (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
  iIntros (Hl1 Hl2) "HΦ". iApply wp_lift_expr_step => //.
  iIntros (σ1) "Hctx !>". iSplit; first by eauto 8 using CopyAllocIdIS.
391
  iIntros "!>" (???? Hstep ?) "!>". inv_expr_step. iSplit => //. iFrame.
392
  by iApply wp_value.
393
394
Qed.

395
396
397
398
399
400
401
402
403
404
405
406
407
Lemma wp_ptr_relop Φ op v1 v2 l1 l2 E b:
  val_to_loc v1 = Some l1 
  val_to_loc v2 = Some l2 
  match op with
  | EqOp => Some (bool_decide (l1.2 = l2.2))
  | NeOp => Some (bool_decide (l1.2  l2.2))
  | LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
  | GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
  | LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
  | GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
  | _ => None
  end = Some b 
  loc_in_bounds l1 0 - loc_in_bounds l2 0 -
408
  (alloc_alive_loc l1  alloc_alive_loc l2   Φ (i2v (Z_of_bool b) i32)) -
409
410
411
412
  WP BinOp op PtrOp PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
  iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
  iApply wp_binop. iIntros (σ) "Hσ".
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
413
  iAssert valid_ptr l1 σ.(st_heap)%I as %?. {
Michael Sammler's avatar
Michael Sammler committed
414
    iApply (alloc_alive_loc_to_valid_ptr with "Hl1 [HΦ] Hσ").
415
416
    by iDestruct "HΦ" as "[$ _]".
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
417
  iAssert valid_ptr l2 σ.(st_heap)%I as %?. {
Michael Sammler's avatar
Michael Sammler committed
418
    iApply (alloc_alive_loc_to_valid_ptr with "Hl2 [HΦ] Hσ").
419
420
421
422
423
424
425
    by iDestruct "HΦ" as "[_ [$ _]]".
  }
  iSplit; first by iPureIntro; eexists _; econstructor.
  iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iFrame.
  inversion Hstep; simplify_eq => //; by move: Hv1 Hv2 => /val_of_to_loc ?/val_of_to_loc?; subst.
Qed.

Michael Sammler's avatar
Michael Sammler committed
426
427
Lemma wp_ptr_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
428
  val_to_Z_weak vo it = Some o 
Michael Sammler's avatar
Michael Sammler committed
429
  0  o 
430
431
   Φ (val_of_loc (l offset{ly} o)) -
  WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
432
433
Proof.
  iIntros (Hvl Hvo Ho) "HΦ".
434
435
436
437
  iApply wp_binop_det. iSplit; last done.
  iIntros (σ v) "_ !%". split.
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrOffsetOpIP.
Michael Sammler's avatar
Michael Sammler committed
438
439
Qed.

440
441
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
442
443
444
  val_to_Z_weak vo it = Some o 
   Φ (val_of_loc (l offset{ly} -o)) -
  WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
445
446
447
448
449
450
451
452
Proof.
  iIntros (Hvl Hvo) "HΦ".
  iApply wp_binop_det. iSplit; last done.
  iIntros (σ v) "_ !%". split.
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrNegOffsetOpIP.
Qed.

Michael Sammler's avatar
Michael Sammler committed
453
454
455
Lemma wp_get_member Φ vl l sl n E:
  val_to_loc vl = Some l 
  is_Some (index_of sl.(sl_members) n) 
456
457
   Φ (val_of_loc (l at{sl} n)) -
  WP Val vl at{sl} n @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
458
459
460
Proof.
  iIntros (Hvl [i Hi]) "HΦ".
  rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
461
462
  have [|v Hv]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
    split; first by rewrite /min_int/=; lia.  by apply offset_of_bound.
Michael Sammler's avatar
Michael Sammler committed
463
  }
464
  rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
465
  iApply wp_binop_det. iSplit; last done.
466
467
468
469
470
471
  iIntros (σ v') "_ !%". split.
  - inversion 1; simplify_eq. rewrite offset_loc_sz1; last done.
    apply val_to_Z_to_int_repr_Z in Hv. by simplify_eq.
  - move => ->. rewrite -(offset_loc_sz1 u8) //.
    apply: PtrOffsetOpIP => //; last lia.
    by rewrite /val_to_Z_weak /val_to_int_repr Hv.
Michael Sammler's avatar
Michael Sammler committed
472
473
474
475
476
Qed.

Lemma wp_get_member_union Φ vl l ul n E:
  val_to_loc vl = Some l 
  Φ (val_of_loc (l at_union{ul} n)) - WP Val vl at_union{ul} n @ E {{ Φ }}.
477
478
479
480
481
Proof.
  iIntros (->%val_of_to_loc) "?".
  rewrite /GetMemberUnion/GetMemberUnionLoc.
  by iApply @wp_value.
Qed.
Michael Sammler's avatar
Michael Sammler committed
482

483
484
Lemma wp_offset_of Φ s m i E:
  offset_of s.(sl_members) m = Some i 
485
  ( v, val_of_Z i size_t = Some v - Φ v) -
486
487
488
  WP OffsetOf s m @ E {{ Φ }}.
Proof.
  rewrite /OffsetOf. iIntros (Ho) "HΦ".
489
  have [|? Hs]:= (val_of_Z_is_Some size_t i). {
490
491
492
493
    split; first by rewrite /min_int/=; lia.
    move: Ho => /fmap_Some[?[?->]].
    by apply offset_of_bound.
  }
494
  rewrite Ho /= Hs /=. iApply wp_value.
495
496
497
498
499
500
501
  by iApply "HΦ".
Qed.

Lemma wp_offset_of_union Φ ul m E:
  Φ (i2v 0 size_t) - WP OffsetOfUnion ul m @ E {{ Φ }}.
Proof. by iApply @wp_value. Qed.

Michael Sammler's avatar
Michael Sammler committed
502
Lemma wp_if Φ it v e1 e2 n:
503
  val_to_Z_weak v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
504
505
506
507
508
509
  (if decide (n = 0) then WP coerce_rtexpr e2 {{ Φ }} else WP coerce_rtexpr e1 {{ Φ }}) -
  WP IfE (IntOp it) (Val v) e1 e2 {{ Φ }}.
Proof.
  iIntros (?) "HΦ".
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using IfES.
510
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
Michael Sammler's avatar
Michael Sammler committed
511
512
513
514
  iSplit => //. iFrame.
  by case_decide; case_bool_decide.
Qed.

Michael Sammler's avatar
Michael Sammler committed
515
516
517
518
Lemma wp_skip Φ v E:
   Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
519
520
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using SkipES.
521
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
522
  iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
523
524
525
526
527
528
Qed.

Lemma wp_concat E Φ vs:
  Φ (mjoin vs) - WP Concat (Val <$> vs) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
529
530
531
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?".
  iModIntro. iSplit; first by eauto 8 using ConcatS.
532
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
533
  iModIntro. iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
534
535
536
Qed.

Lemma wps_concat_bind_ind vs E Φ es:
537
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
538
539
540
541
542
543
544
545
        (λ vl, WP Concat (Val <$> (vs ++ vl)) @ E {{ Φ }}) es [] -
  WP Concat ((Val <$> vs) ++ es) @ E {{ Φ }}.
Proof.
  rewrite -{2}(app_nil_r vs).
  move: {2 3}[] => vl2.
  elim: es vs vl2 => /=.
  - iIntros (vs vl2) "He". by rewrite !app_nil_r.
  - iIntros (e el IH vs vl2) "Hf".
546
547
548
549
550
551
552
553
    have -> : (coerce_rtexpr (Concat ((Val <$> vs ++ vl2) ++ e :: el)))%E = (fill [ExprCtx (ConcatCtx (vs ++ vl2) (to_rtexpr <$> el))] (to_rtexpr e)). {
        by rewrite /coerce_rtexpr/= fmap_app fmap_cons -!list_fmap_compose.
    }
    iApply wp_bind. iApply (wp_wand with "Hf").
    iIntros (v) "Hf" => /=.
    have -> : Expr (RTConcat ((Expr <$> (RTVal <$> vs ++ vl2)) ++ of_val v :: (to_rtexpr <$> el)))
             = Concat ((Val <$> vs ++ (vl2 ++ [v])) ++ el). 2: by iApply IH.
    by rewrite /coerce_rtexpr /= !fmap_app /= (cons_middle (of_val v)) !app_assoc -!list_fmap_compose.
Michael Sammler's avatar
Michael Sammler committed
554
555
556
Qed.

Lemma wp_concat_bind E Φ es:
557
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
558
559
560
561
562
563
        (λ vl, WP Concat (Val <$> vl) @ E {{ Φ }}) es [] -
  WP Concat es @ E {{ Φ }}.
Proof. by iApply (wps_concat_bind_ind []). Qed.

Lemma wp_struct_init E Φ sl fs:
  foldr (λ '(n, ly) f, (λ vl,
564
     WP coerce_rtexpr (default (Val (replicate (ly_size ly) MPoison)) (n'  n; (list_to_map fs : gmap _ _) !! n'))
Michael Sammler's avatar
Michael Sammler committed
565
566
567
568
569
570
571
572
573
574
        @ E {{ v, f (vl ++ [v]) }}))
    (λ vl, Φ (mjoin vl)) sl.(sl_members) [] -
  WP StructInit sl fs @ E {{ Φ }}.
Proof.
  iIntros "He". unfold StructInit. iApply wp_concat_bind.
  move: {2 4}[] => vs.
  iInduction (sl_members sl) as [|[o?]?] "IH" forall (vs) => /=. by iApply wp_concat.
  iApply (wp_wand with "He"). iIntros (v') "Hfold". by iApply "IH".
Qed.

575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
Lemma wp_call_bind_ind vs E Φ vf el:
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP (Call (Val vf) (Val <$> (vs ++ vl))) @ E {{ Φ }}) el [] -
  WP (Call (Val vf) ((Val <$> vs) ++ el)) @ E {{ Φ}}.
Proof.
  rewrite -{2}(app_nil_r vs).
  move: {2 3}[] => vl2.
  elim: el vs vl2 => /=.
  - iIntros (vs vl2) "He". by rewrite !app_nil_r.
  - iIntros (e el IH vs vl2) "Hf".
    have -> : (coerce_rtexpr (Call (Val vf) ((Val <$> vs ++ vl2) ++ e :: el)))%E = (fill [ExprCtx (CallRCtx vf (vs ++ vl2) (to_rtexpr <$> el))] (to_rtexpr e)). {
        by rewrite /coerce_rtexpr/= fmap_app fmap_cons -!list_fmap_compose.
    }
    iApply wp_bind. iApply (wp_wand with "Hf").
    iIntros (v) "Hf" => /=.
    have -> : Expr (RTCall vf ((Expr <$> (RTVal <$> vs ++ vl2)) ++ of_val v :: (to_rtexpr <$> el)))
             = Call vf ((Val <$> vs ++ (vl2 ++ [v])) ++ el). 2: by iApply IH.
    by rewrite /coerce_rtexpr /= !fmap_app /= (cons_middle (of_val v)) !app_assoc -!list_fmap_compose.
Qed.

Lemma wp_call_bind E Φ el ef:
  WP (coerce_rtexpr ef) @ E {{ vf, foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP (Call (Val vf) (Val <$> vl)) @ E {{ Φ }}) el [] }} -
  WP (Call ef el) @ E {{ Φ }}.
Proof.
  iIntros "HWP".
  have -> : coerce_rtexpr (Call ef el) = fill [ExprCtx $ CallLCtx (coerce_rtexpr <$> el)] (coerce_rtexpr ef) by [].
  iApply wp_bind.
  iApply (wp_wand with "HWP"). iIntros (vf) "HWP".
  by iApply (wp_call_bind_ind []).
Qed.

Michael Sammler's avatar
Michael Sammler committed
607
608
609
End expr_lifting.

(*** Lifting of statements *)
610
Definition stmt_wp_def `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) (s : stmt) : iProp Σ :=
611
612
  ( Φ rf, Q = rf.(rf_fn).(f_code) - ( v, Ψ v - WP to_rtstmt rf (Return v) {{ Φ }}) -
    WP to_rtstmt rf s @ E {{ Φ }}).
613
614
Definition stmt_wp_aux `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) : seal (@stmt_wp_def Σ _ E Q Ψ). by eexists. Qed.
Definition stmt_wp `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) :
Michael Sammler's avatar
Michael Sammler committed
615
  stmt  iProp Σ := (stmt_wp_aux E Q Ψ).(unseal).
616
Definition stmt_wp_eq `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) : stmt_wp E Q Ψ = @stmt_wp_def Σ _ E Q Ψ := (stmt_wp_aux E Q Ψ).(seal_eq).
Michael Sammler's avatar
Michael Sammler committed
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633

Notation "'WPs' s @ E {{ Q , Ψ } }" := (stmt_wp E Q Ψ s%E)
  (at level 20, s, Q, Ψ at level 200, format "'[' 'WPs'  s  '/' '[       ' @  E  {{  Q ,  Ψ  } } ']' ']'" ) : bi_scope.

Notation "'WPs' s {{ Q , Ψ } }" := (stmt_wp  Q Ψ s%E)
  (at level 20, s, Q, Ψ at level 200, format "'[' 'WPs'  s  '/' '[   ' {{  Q ,  Ψ  } } ']' ']'") : bi_scope.

Section stmt_lifting.
Context `{!refinedcG Σ}.

Lemma stmt_wp_unfold s E Q Ψ  :
  WPs s @ E {{ Q, Ψ }}  stmt_wp_def E Q Ψ s.
Proof. by rewrite stmt_wp_eq. Qed.

Lemma fupd_wps s E Q Ψ :
  (|={E}=> WPs s @ E {{ Q, Ψ }}) - WPs s @ E{{ Q, Ψ }}.
Proof.
634
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
635
636
637
  iApply fupd_wp. by iApply "Hs".
Qed.

638
639
640
641
642
643
644
645
Global Instance elim_modal_bupd_wps p s Q Ψ P E :
    ElimModal True p false (|==> P) P (WPs s @ E {{ Q, Ψ }}) (WPs s @ E {{ Q, Ψ }}).
Proof. by rewrite /ElimModal intuitionistically_if_elim (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wps. Qed.

Global Instance elim_modal_fupd_wps p s Q Ψ P E :
    ElimModal True p false (|={E}=> P) P (WPs s @ E {{ Q, Ψ }}) (WPs s @ E {{ Q, Ψ }}).
Proof. by rewrite /ElimModal intuitionistically_if_elim fupd_frame_r wand_elim_r fupd_wps. Qed.

646
647
648
649
Lemma wps_wand s E Q Φ Ψ:
  WPs s @ E {{ Q , Φ }} - ( v, Φ v - Ψ v) - WPs s @ E {{ Q , Ψ }}.
Proof.
  rewrite !stmt_wp_unfold. iIntros "HΦ H" (???) "HΨ".
650
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
651
652
653
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

654
655
656
657
658
Lemma wp_call vf vl f fn Φ:
  val_to_loc vf = Some f 
  Forall2 has_layout_val vl (f_args fn).*2 
  fntbl_entry f fn - ( lsa lsv, Forall2 has_layout_loc lsa (f_args fn).*2 -
     ([ list] l; v  lsa; vl, lv) - ([ list] l; v  lsv; fn.(f_local_vars), l|v.2|) -  Ψ',
Michael Sammler's avatar
Michael Sammler committed
659
660
          WPs Goto fn.(f_init) {{ (subst_stmt (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
                            (val_of_loc <$> (lsa ++ lsv)))) <$> fn.(f_code), Ψ' }} 
661
662
663
664
665
666
667
668
         ( v, Ψ' v -
                  ([ list] l; v  lsa; fn.(f_args), l|v.2|) 
                  ([ list] l; v  lsv; fn.(f_local_vars), l|v.2|) 
                  Φ v)
   ) -
   WP (Call (Val vf) (Val <$> vl)) {{ Φ }}.
Proof.
  move => Hf Hly. move: (Hly) => /Forall2_length. rewrite fmap_length => Hlen_vs.
669
670
  iIntros "Hf HWP". iApply wp_lift_expr_step; first done.
  iIntros (σ1) "((%&Hhctx&Hbctx)&Hfctx)".
671
672
  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %Hfn. iModIntro.
  iSplit; first by eauto 10 using CallFailS.
673
  iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
674
    (* Alloc failure case. *)
675
676
    iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
    iApply wp_alloc_failed.
Michael Sammler's avatar
Michael Sammler committed
677
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
678
  iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx]") as "[Hctx Hlv]" => //.
679
  rewrite big_sepL2_sep. iDestruct "Hlv" as "[Hlv Hfree_v]".
680
  iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
681
  rewrite big_sepL2_sep. iDestruct "Hla" as "[Hla Hfree_a]".
682
683
684
685
686
687
  iModIntro. iSplit => //.

  iDestruct ("HWP" $! lsa lsv with "[//] Hla [Hlv]") as (Ψ') "(HQinit & HΨ')". {
    rewrite big_sepL2_fmap_r. iApply (big_sepL2_mono with "Hlv") => ??? ?? /=.
    iIntros "?". iExists _. iFrame. iPureIntro. split; first by apply replicate_length.
    apply: Forall2_lookup_lr. 2: done. done. rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
688
  }
Michael Sammler's avatar
Michael Sammler committed
689
  iFrame. rewrite stmt_wp_eq. iApply "HQinit" => //.
690
691
692
693

  (** prove Return *)
  iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
  iApply wp_lift_stmt_step => //.
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
  iIntros (σ3) "(Hctx&?)".
  iMod (heap_free_blocks_upd (zip lsa (f_args fn).*2 ++ zip lsv (f_local_vars fn).*2) with "[Ha Hfree_a Hv Hfree_v] Hctx") as (σ2 Hfree) "Hctx". {
    rewrite big_sepL_app !big_sepL_sep !big_sepL2_alt.
    iDestruct "Ha" as "[% Ha]". iDestruct "Hv" as "[% Hv]".
    iDestruct "Hfree_a" as "[% Hfree_a]". iDestruct "Hfree_v" as "[% Hfree_v]".
    rewrite !zip_fmap_r !big_sepL_fmap/=. iFrame.
    setoid_rewrite replicate_length. iFrame.
    iApply (big_sepL_impl' with "Hfree_a").
    { rewrite !zip_with_length !min_l ?fmap_length //; lia. }
    iIntros (??? [?[v0[?[??]]]]%lookup_zip_with_Some [?[ly0[?[??]]]]%lookup_zip_with_Some) "!> H2"; simplify_eq/=.
    have -> : v0 `has_layout_val` ly0.2; last done.
    eapply Forall2_lookup_lr; [done..|].
    rewrite list_lookup_fmap fmap_Some. naive_solver.
  }
  iModIntro.
709
  iSplit; first by eauto 8 using ReturnS.
710
711
712
  iIntros (os ts3 σ2' ? Hst ?). inv_stmt_step. iIntros "!>". iSplitR => //.
  have ->: (σ2 = hs) by apply: free_blocks_inj.
  iFrame. iModIntro. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
713
714
715
716
Qed.

Lemma wps_return Q Ψ v:
  Ψ v - WPs (Return (Val v)) {{ Q , Ψ }}.
717
Proof. rewrite stmt_wp_unfold. iIntros "Hb" (? rf ?) "HΨ". by iApply "HΨ". Qed.
Michael Sammler's avatar
Michael Sammler committed
718
719
720
721
722

Lemma wps_goto Q Ψ b s:
  Q !! b = Some s 
   WPs s {{ Q, Ψ }} - WPs Goto b {{ Q , Ψ }}.
Proof.
723
724
  iIntros (Hs) "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step. iIntros (?) "Hσ !>".
725
  iSplit; first by eauto 10 using GotoS.
726
  iIntros (???? Hstep ?) "!> !>". inv_stmt_step.
727
  iSplit; first done. iFrame. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
728
729
730
731
732
Qed.

Lemma wps_skip Q Ψ s:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs SkipS s {{ Q , Ψ }}.
Proof.
733
734
735
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
736
  iSplit; first by eauto 10 using SkipSS.
737
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
738
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
739
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
740
741
742
743
744
Qed.

Lemma wps_exprs Q Ψ s v:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs ExprS (Val v) s {{ Q , Ψ }}.
Proof.
745
746
747
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
748
  iSplit; first by eauto 10 using ExprSS.
749
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
750
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
751
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
752
753
754
755
756
757
758
759
760
761
762
763
764
765
Qed.

Lemma wps_annot n A (a : A) Q Ψ s:
  (|={}[]=>^n WPs s {{ Q, Ψ }}) - WPs AnnotStmt n a s {{ Q , Ψ }}.
Proof.
  iIntros "Hs". iInduction n as [|n] "IH" => /=. by iApply "Hs".
  rewrite /AnnotStmt. iApply wps_skip. by iApply (step_fupd_wand with "Hs IH").
Qed.

Lemma wps_assign Q Ψ vl ly vr s l o:
  let E := if o is ScOrd then  else  in
  o = ScOrd  o = Na1Ord 
  val_to_loc vl = Some l 
  vr `has_layout_val` ly 
766
767
  (|={,E}=> l|ly|   (lvr ={E,}= WPs s {{Q, Ψ}}))
    - WPs (Val vl <-{ly, o} Val vr; s) {{ Q , Ψ }}.
Michael Sammler's avatar
Michael Sammler committed
768
Proof.
769
  iIntros (E Ho Hvl Hly) "HWP". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
770
  iApply wp_lift_stmt_step_fupd. iIntros ([h1 ?]) "((%&Hhctx&Hfctx)&?) /=". iMod "HWP" as "[Hl HWP]".
Michael Sammler's avatar
Michael Sammler committed
771
  iApply (fupd_mask_weaken ); first set_solver. iIntros "HE".
772
  iDestruct "Hl" as (v' Hlyv' ?) "Hl".
773
774
  iDestruct (heap_mapsto_has_alloc_id with "Hl") as %Haid.
  unfold E. case: Ho => ->.
Michael Sammler's avatar
Michael Sammler committed
775
776
  - iModIntro.
    iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl") as %? => //.
777
    iSplit; first by eauto 12 using AssignS.
778
    iIntros (? e2 σ2 efs Hstep ?) "!> !>". inv_stmt_step. unfold end_val.
779
780
    iMod (heap_write with "Hhctx Hl") as "[$ Hl]" => //. congruence.
    iMod ("HWP" with "Hl") as "HWP".
781
    iModIntro => /=. iSplit; first done. iFrame. iSplit; first done. by iApply "HWP".
782
  - iMod (heap_write_na _ _ _ vr with "Hhctx Hl") as (?) "[Hhctx Hc]" => //; first by congruence.
783
    iModIntro. iSplit; first by eauto 12 using AssignS.
784
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_stmt_step.
Michael Sammler's avatar
Michael Sammler committed
785
    have ? : (v' = v'0) by [apply: heap_at_inj_val]; subst v'0.
786
    iFrame => /=. iMod "HE" as "_". iModIntro. iSplit; first done.
787
    iSplit; first done.
Michael Sammler's avatar
Michael Sammler committed
788

789
790
    (* second step *)
    iApply wp_lift_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
791
    iIntros ([h2 ?]) "((%&Hhctx&Hfctx)&?)" => /=.
Michael Sammler's avatar
Michael Sammler committed
792
    iMod ("Hc" with "Hhctx") as (?) "[Hhctx Hmt]".
793
    iModIntro. iSplit; first by eauto 12 using AssignS. unfold end_stmt.
794
    iIntros (? e2 σ2 efs Hst ?) "!>". inv_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
795
    have ? : (v' = v'0) by [apply: heap_lookup_loc_inj_val]; subst v'0.
Michael Sammler's avatar
Michael Sammler committed
796
    iFrame => /=. iMod ("HWP" with "Hmt") as "HWP".
797
    iModIntro. iSplit; first done. iSplit; first done. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
798
799
800
Qed.

Lemma wps_switch Q Ψ v n ss def m it:
801
  val_to_Z_weak v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
802
803
804
  ( i, m !! n = Some i  is_Some (ss !! i)) 
  WPs default def (i  m !! n; ss !! i) {{ Q, Ψ }} - WPs (Switch it (Val v) m ss def) {{ Q , Ψ }}.
Proof.
805
806
  iIntros (Hv Hm) "HWP". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
  iApply wp_lift_stmt_step. iIntros (?) "Hσ".
807
  iModIntro. iSplit; first by eauto 8 using SwitchS.
808
  iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
809
  iFrame "Hσ". by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
810
811
812
813
Qed.

(** a version of wps_switch which is directed by ss instead of n *)
Lemma wps_switch' Q Ψ v n ss def m it:
814
  val_to_Z_weak v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
815
816
817
818
819
820
821
822
823
824
825
826
827
828
  map_Forall (λ _ i, is_Some (ss !! i)) m 
  ([ list] isss, m !! n = Some i - WPs s {{ Q, Ψ }}) 
  (m !! n = None - WPs def {{ Q, Ψ }}) -
  WPs (Switch it (Val v) m ss def) {{ Q , Ψ }}.
Proof.
  iIntros (Hn Hm) "Hs". iApply wps_switch; eauto.
  destruct (m !! n) as [i|] eqn:Hi => /=.
  - iDestruct "Hs" as "[Hs _]".
    destruct (ss !! i) as [s|] eqn:? => /=. 2: by move: (Hm _ _ Hi) => [??]; simplify_eq.
    by iApply (big_andL_lookup with "Hs").
  - iDestruct "Hs" as "[_ Hs]". by iApply "Hs".
Qed.

Lemma wps_if Q Ψ v s1 s2 n:
829
  val_to_Z_weak v bool_it = Some n 
Michael Sammler's avatar
Michael Sammler committed
830
831
832
833
834
835
836
837
838
  (if decide (n = 0) then WPs s2 {{ Q, Ψ }} else WPs s1 {{ Q, Ψ }}) -
  WPs (if: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
  iIntros (Hn) "Hs". iApply wps_switch' => //=.
  1: by apply map_Forall_insert_2; eauto; apply map_Forall_empty.
  rewrite right_id. by iSplit; iIntros (?); simplify_map_eq.
Qed.

Lemma wps_assert Q Ψ v s n:
839
  val_to_Z_weak v bool_it = Some n  n  0 
Michael Sammler's avatar
Michael Sammler committed
840
841
  WPs s {{ Q, Ψ }} -
  WPs (assert: Val v; s) {{ Q , Ψ }}.
842
843
844
845
Proof.
  iIntros (Hv Hn) "Hs". rewrite /notation.Assert.
  iApply wps_if => //. by case_decide.
Qed.
Michael Sammler's avatar
Michael Sammler committed
846

847
Definition wps_block (P : iProp Σ) (b : label) (Q : gmap label stmt) (Ψ : val  iProp Σ) : iProp Σ :=
Michael Sammler's avatar
Michael Sammler committed
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
  ( (P - WPs Goto b