lifting.v 37 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
From refinedc.lang Require Import tactics.
Set Default Proof Using "Type".
Import uPred.

Class refinedcG Σ := RefinedCG {
Michael Sammler's avatar
Michael Sammler committed
10
  refinedcG_invG : invGS Σ;
Michael Sammler's avatar
Michael Sammler committed
11
12
13
  refinedcG_gen_heapG :> heapG Σ
}.

Michael Sammler's avatar
Michael Sammler committed
14
Instance c_irisG `{!refinedcG Σ} : irisGS 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
377
378
  loc_in_bounds (l2.1, l1.2) 0 -
  alloc_alive_loc l2   Φ (val_of_loc (l2.1, l1.2)) -
  WP CopyAllocId PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
379
Proof.
380
381
382
383
384
385
386
387
388
  iIntros (Hl1 Hl2) "Hl HΦ". iApply wp_lift_expr_step => //.
  iIntros (σ1) "Hctx !>".
  iAssert valid_ptr (l2.1, l1.2) σ1.(st_heap)%I as %?. {
    iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hctx")].
    iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
    iDestruct "HΦ" as "[Halive _]". by iApply alloc_alive_loc_mono; [|done].
  }
  iDestruct "HΦ" as "[_ HΦ]".
  iSplit; first by eauto 8 using CopyAllocIdPS.
389
390
391
392
393
394
395
  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 
396
397
398
  loc_in_bounds (l2.1, l1.2) 0 -
  alloc_alive_loc l2   Φ (val_of_loc (l2.1, l1.2)) -
  WP CopyAllocId (IntOp it) (Val v1) (Val v2) @ E {{ Φ }}.
399
Proof.
400
401
402
403
404
405
406
407
408
  iIntros (Hl1 Hl2) "Hl HΦ". iApply wp_lift_expr_step => //.
  iIntros (σ1) "Hctx !>".
  iAssert valid_ptr (l2.1, l1.2) σ1.(st_heap)%I as %?. {
    iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hctx")].
    iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
    iDestruct "HΦ" as "[Halive _]". by iApply alloc_alive_loc_mono; [|done].
  }
  iDestruct "HΦ" as "[_ HΦ]".
  iSplit; first by eauto 8 using CopyAllocIdIS.
409
  iIntros "!>" (???? Hstep ?) "!>". inv_expr_step. iSplit => //. iFrame.
410
  by iApply wp_value.
411
412
Qed.

413
414
415
416
417
418
419
420
421
422
423
424
425
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 -
426
  (alloc_alive_loc l1  alloc_alive_loc l2   Φ (i2v (Z_of_bool b) i32)) -
427
428
429
  WP BinOp op PtrOp PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
  iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
Michael Sammler's avatar
Michael Sammler committed
430
431
  iDestruct (loc_in_bounds_has_alloc_id with "Hl1") as %[??].
  iDestruct (loc_in_bounds_has_alloc_id with "Hl2") as %[??].
432
  iApply wp_binop. iIntros (σ) "Hσ".
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
433
  iAssert valid_ptr l1 σ.(st_heap)%I as %?. {
Michael Sammler's avatar
Michael Sammler committed
434
    iApply (alloc_alive_loc_to_valid_ptr with "Hl1 [HΦ] Hσ").
435
436
    by iDestruct "HΦ" as "[$ _]".
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
437
  iAssert valid_ptr l2 σ.(st_heap)%I as %?. {
Michael Sammler's avatar
Michael Sammler committed
438
    iApply (alloc_alive_loc_to_valid_ptr with "Hl2 [HΦ] Hσ").
439
440
441
442
    by iDestruct "HΦ" as "[_ [$ _]]".
  }
  iSplit; first by iPureIntro; eexists _; econstructor.
  iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iFrame.
Michael Sammler's avatar
Michael Sammler committed
443
444
445
  inversion Hstep; simplify_eq => //.
  all: try rewrite val_to_of_loc in Hv1; simplify_eq.
  all: try rewrite val_to_of_loc in Hv2; simplify_eq.
446
447
Qed.

Michael Sammler's avatar
Michael Sammler committed
448
449
Lemma wp_ptr_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
450
  val_to_Z_weak vo it = Some o 
451
  loc_in_bounds (l offset{ly} o) 0 -
452
453
   Φ (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
454
Proof.
455
  iIntros (Hvl Hvo) "Hl HΦ".
456
  iApply wp_binop_det. iSplit; last done.
457
458
459
  iIntros (σ v) "Hσ".
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
  iPureIntro. split.
460
461
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrOffsetOpIP.
Michael Sammler's avatar
Michael Sammler committed
462
463
Qed.

464
465
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
466
  val_to_Z_weak vo it = Some o 
467
  loc_in_bounds (l offset{ly} -o) 0 -
468
469
   Φ (val_of_loc (l offset{ly} -o)) -
  WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
470
Proof.
471
  iIntros (Hvl Hvo) "Hl HΦ".
472
  iApply wp_binop_det. iSplit; last done.
473
474
475
  iIntros (σ v) "Hσ".
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
  iPureIntro. split.
476
477
478
479
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrNegOffsetOpIP.
Qed.

Michael Sammler's avatar
Michael Sammler committed
480
481
482
Lemma wp_get_member Φ vl l sl n E:
  val_to_loc vl = Some l 
  is_Some (index_of sl.(sl_members) n) 
483
  loc_in_bounds l (ly_size sl) -
484
485
   Φ (val_of_loc (l at{sl} n)) -
  WP Val vl at{sl} n @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
486
Proof.
487
  iIntros (Hvl [i Hi]) "#Hl HΦ".
Michael Sammler's avatar
Michael Sammler committed
488
  rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
489
  have [|v Hv]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
490
    split; first by rewrite /min_int/=; lia. by apply offset_of_bound.
Michael Sammler's avatar
Michael Sammler committed
491
  }
492
  rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
493
  iApply wp_ptr_offset; [done| by apply: val_to_Z_to_int_repr_Z | | ].
494
495
  { have ? := offset_of_idx_le_size sl i. rewrite offset_loc_sz1 //.
    iApply (loc_in_bounds_offset with "Hl"); simpl; [done| destruct l => /=; lia  | destruct l => /=; lia ]. }
496
  by rewrite offset_loc_sz1.
Michael Sammler's avatar
Michael Sammler committed
497
498
499
500
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 {{ Φ }}.
501
502
503
504
505
Proof.
  iIntros (->%val_of_to_loc) "?".
  rewrite /GetMemberUnion/GetMemberUnionLoc.
  by iApply @wp_value.
Qed.
Michael Sammler's avatar
Michael Sammler committed
506

507
508
Lemma wp_offset_of Φ s m i E:
  offset_of s.(sl_members) m = Some i 
509
  ( v, val_of_Z i size_t = Some v - Φ v) -
510
511
512
  WP OffsetOf s m @ E {{ Φ }}.
Proof.
  rewrite /OffsetOf. iIntros (Ho) "HΦ".
513
  have [|? Hs]:= (val_of_Z_is_Some size_t i). {
514
515
516
517
    split; first by rewrite /min_int/=; lia.
    move: Ho => /fmap_Some[?[?->]].
    by apply offset_of_bound.
  }
518
  rewrite Ho /= Hs /=. iApply wp_value.
519
520
521
522
523
524
525
  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
526
Lemma wp_if Φ it v e1 e2 n:
527
  val_to_Z_weak v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
528
529
530
531
532
533
  (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.
534
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
Michael Sammler's avatar
Michael Sammler committed
535
536
537
538
  iSplit => //. iFrame.
  by case_decide; case_bool_decide.
Qed.

Michael Sammler's avatar
Michael Sammler committed
539
540
541
542
Lemma wp_skip Φ v E:
   Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
543
544
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using SkipES.
545
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
546
  iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
547
548
549
550
551
552
Qed.

Lemma wp_concat E Φ vs:
  Φ (mjoin vs) - WP Concat (Val <$> vs) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
553
554
555
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?".
  iModIntro. iSplit; first by eauto 8 using ConcatS.
556
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
557
  iModIntro. iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
558
559
560
Qed.

Lemma wps_concat_bind_ind vs E Φ es:
561
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
562
        (λ vl, WP coerce_rtexpr (Concat (Val <$> (vs ++ vl))) @ E {{ Φ }}) es [] -
Michael Sammler's avatar
Michael Sammler committed
563
564
565
566
567
568
569
  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".
570
571
572
573
574
575
576
577
    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
578
579
580
Qed.

Lemma wp_concat_bind E Φ es:
581
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
582
        (λ vl, WP coerce_rtexpr (Concat (Val <$> vl)) @ E {{ Φ }}) es [] -
Michael Sammler's avatar
Michael Sammler committed
583
584
585
586
587
  WP Concat es @ E {{ Φ }}.
Proof. by iApply (wps_concat_bind_ind []). Qed.

Lemma wp_struct_init E Φ sl fs:
  foldr (λ '(n, ly) f, (λ vl,
588
     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
589
590
591
592
593
594
595
596
597
598
        @ 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.

599
600
Lemma wp_call_bind_ind vs E Φ vf el:
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
601
        (λ vl, WP coerce_rtexpr (Call (Val vf) (Val <$> (vs ++ vl))) @ E {{ Φ }}) el [] -
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
  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]) }}))
Michael Sammler's avatar
Michael Sammler committed
621
        (λ vl, WP coerce_rtexpr (Call (Val vf) (Val <$> vl)) @ E {{ Φ }}) el [] }} -
622
623
624
625
626
627
628
629
630
  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
631
632
633
End expr_lifting.

(*** Lifting of statements *)
634
Definition stmt_wp_def `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) (s : stmt) : iProp Σ :=
635
636
  ( Φ rf, Q = rf.(rf_fn).(f_code) - ( v, Ψ v - WP to_rtstmt rf (Return v) {{ Φ }}) -
    WP to_rtstmt rf s @ E {{ Φ }}).
637
638
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
639
  stmt  iProp Σ := (stmt_wp_aux E Q Ψ).(unseal).
640
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
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657

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.
658
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
659
660
661
  iApply fupd_wp. by iApply "Hs".
Qed.

662
663
664
665
666
667
668
669
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.

670
671
672
673
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Ψ".
674
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
675
676
677
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

678
679
680
681
682
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
683
684
          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), Ψ' }} 
685
686
687
688
689
690
691
692
         ( 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.
693
694
  iIntros "Hf HWP". iApply wp_lift_expr_step; first done.
  iIntros (σ1) "((%&Hhctx&Hbctx)&Hfctx)".
Michael Sammler's avatar
Michael Sammler committed
695
  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %[a [? Hfn]]; subst. iModIntro.
696
  iSplit; first by eauto 10 using CallFailS.
697
  iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
698
    (* Alloc failure case. *)
699
700
    iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
    iApply wp_alloc_failed.
Michael Sammler's avatar
Michael Sammler committed
701
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
702
  iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx]") as "[Hctx Hlv]" => //.
703
  rewrite big_sepL2_sep. iDestruct "Hlv" as "[Hlv Hfree_v]".
704
  iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
705
  rewrite big_sepL2_sep. iDestruct "Hla" as "[Hla Hfree_a]".
706
707
708
709
710
711
  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.
712
  }
Michael Sammler's avatar
Michael Sammler committed
713
  iFrame. rewrite stmt_wp_eq. iApply "HQinit" => //.
714
715
716
717

  (** prove Return *)
  iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
  iApply wp_lift_stmt_step => //.
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
  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.
733
  iSplit; first by eauto 8 using ReturnS.
734
735
736
  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
737
738
739
740
Qed.

Lemma wps_return Q Ψ v:
  Ψ v - WPs (Return (Val v)) {{ Q , Ψ }}.
741
Proof. rewrite stmt_wp_unfold. iIntros "Hb" (? rf ?) "HΨ". by iApply "HΨ". Qed.
Michael Sammler's avatar
Michael Sammler committed
742
743
744
745
746

Lemma wps_goto Q Ψ b s:
  Q !! b = Some s 
   WPs s {{ Q, Ψ }} - WPs Goto b {{ Q , Ψ }}.
Proof.
747
748
  iIntros (Hs) "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step. iIntros (?) "Hσ !>".
749
  iSplit; first by eauto 10 using GotoS.
750
  iIntros (???? Hstep ?) "!> !>". inv_stmt_step.
751
  iSplit; first done. iFrame. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
752
753
754
755
756
Qed.

Lemma wps_skip Q Ψ s:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs SkipS s {{ Q , Ψ }}.
Proof.
757
758
759
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
760
  iSplit; first by eauto 10 using SkipSS.
761
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
762
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
763
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
764
765
766
767
768
Qed.

Lemma wps_exprs Q Ψ s v:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs ExprS (Val v) s {{ Q , Ψ }}.
Proof.
769
770
771
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
772
  iSplit; first by eauto 10 using ExprSS.
773
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
774
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
775
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
776
777
778
779
780
781
782
783
784
785
786
787
788
789
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 
790
791
  (|={,E}=> l|ly|   (lvr ={E,}= WPs s {{Q, Ψ}}))
    - WPs (Val vl <-{ly, o} Val vr; s) {{ Q , Ψ }}.
Michael Sammler's avatar
Michael Sammler committed
792
Proof.
793
  iIntros (E Ho Hvl Hly) "HWP". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
794
  iApply wp_lift_stmt_step_fupd. iIntros ([h1 ?]) "((%&Hhctx&Hfctx)&?) /=". iMod "HWP" as "[Hl HWP]".
Michael Sammler's avatar
Michael Sammler committed
795
  iApply (fupd_mask_weaken ); first set_solver. iIntros "HE".
796
  iDestruct "Hl" as (v' Hlyv' ?) "Hl".
797
798
  iDestruct (heap_mapsto_has_alloc_id with "Hl") as %Haid.
  unfold E. case: Ho => ->.
Michael Sammler's avatar
Michael Sammler committed
799
800
  - iModIntro.
    iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl") as %? => //.
801
    iSplit; first by eauto 12 using AssignS.
802
    iIntros (? e2 σ2 efs Hstep ?) "!> !>". inv_stmt_step. unfold end_val.
803
804
    iMod (heap_write with "Hhctx Hl") as "[$ Hl]" => //. congruence.
    iMod ("HWP" with "Hl") as "HWP".
805
    iModIntro => /=. iSplit; first done. iFrame. iSplit; first done. by iApply "HWP".
806
  - iMod (heap_write_na _ _ _ vr with "Hhctx Hl") as (?) "[Hhctx Hc]" => //; first by congruence.
807
    iModIntro. iSplit; first by eauto 12 using AssignS.
808
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_stmt_step.
Michael Sammler's avatar
Michael Sammler committed
809
    have ? : (v' = v'0) by [apply: heap_at_inj_val]; subst v'0.
810
    iFrame => /=. iMod "HE" as "_". iModIntro. iSplit; first done.
811
    iSplit; first done.
Michael Sammler's avatar
Michael Sammler committed
812

813
814
    (* second step *)
    iApply wp_lift_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
815
    iIntros ([h2 ?]) "((%&Hhctx&Hfctx)&?)" => /=.
Michael Sammler's avatar
Michael Sammler committed
816
    iMod ("Hc" with "Hhctx") as (?) "[Hhctx Hmt]".
817
    iModIntro. iSplit; first by eauto 12 using AssignS. unfold end_stmt.
818
    iIntros (? e2 σ2 efs Hst ?) "!>". inv_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
819
    have ? : (v' = v'0) by [apply: heap_lookup_loc_inj_val]; subst v'0.
Michael Sammler's avatar
Michael Sammler committed
820
    iFrame => /=. iMod ("HWP" with "Hmt") as "HWP".
821
    iModIntro. iSplit; first done. iSplit; first done. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
822
823