lifting.v 39.9 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
Lemma wp_binop v1 v2 Φ op E ot1 ot2:
144
  ( σ, state_ctx σ ={E, }=
145
     v', eval_bin_op op ot1 ot2 σ v1 v2 v' 
146
     ( v', eval_bin_op op ot1 ot2 σ v1 v2 v' ={, E}= state_ctx σ  Φ v')) -
147
  WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
148
Proof.
149
  iIntros "HΦ".
150
151
152
  iApply wp_lift_expr_step_fupd; auto.
  iIntros (σ1) "Hctx".
  iMod ("HΦ" with "Hctx") as ([v' Heval]) "HΦ". iModIntro.
153
  iSplit; first by eauto 8 using BinOpS.
154
155
  iIntros (? e2 σ2 efs Hst ?) "!>!>". inv_expr_step.
  iMod ("HΦ" with "[//]") as "[$ HΦ]".
156
  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
  ( σ, state_ctx σ ={E, }=  v, eval_bin_op op ot1 ot2 σ v1 v2 v  v = v'  ( |={, E}=> state_ctx σ  Φ v')) -
161
    WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
162
Proof.
163
  iIntros "H".
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
  iApply wp_binop. iIntros (σ) "Hctx".
  iMod ("H" with "Hctx") as (Hv) "HΦ". iModIntro.
  iSplit.
  { iExists v'. by rewrite Hv. }
  by iIntros "!>" (v ->%Hv).
Qed.

Lemma wp_binop_det_pure v' v1 v2 Φ op E ot1 ot2:
  ( σ v, eval_bin_op op ot1 ot2 σ v1 v2 v  v = v') 
   Φ v' -
  WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
  iIntros (Hop) "HΦ". iApply (wp_binop_det v').
  iIntros (σ) "Hσ". iApply fupd_mask_intro; [set_solver|]. iIntros "He".
  iSplit; [done|]. iModIntro. iMod "He". by iFrame.
Michael Sammler's avatar
Michael Sammler committed
179
180
Qed.

181
Lemma wp_unop v1 Φ op E ot:
182
  ( σ, state_ctx σ ={E, }=
183
     v', eval_un_op op ot σ v1 v' 
184
     ( v', eval_un_op op ot σ v1 v' ={, E}= state_ctx σ  Φ v')) -
Michael Sammler's avatar
Michael Sammler committed
185
186
   WP UnOp op ot (Val v1) @ E {{ Φ }}.
Proof.
187
  iIntros "HΦ".
188
189
190
  iApply wp_lift_expr_step_fupd; auto.
  iIntros (σ1) "Hctx".
  iMod ("HΦ" with "Hctx") as ([v' Heval]) "HΦ". iModIntro.
191
  iSplit; first by eauto 8 using UnOpS.
192
193
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
  iMod ("HΦ" with "[//]") as "[$ HΦ]".
194
  iModIntro. iSplit => //. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
195
196
197
Qed.

Lemma wp_unop_det v' v1 Φ op E ot:
198
  ( σ, state_ctx σ ={E, }=  v, eval_un_op op ot σ v1 v  v = v'  ( |={, E}=> state_ctx σ  Φ v')) -
199
  WP UnOp op ot (Val v1) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
200
Proof.
201
  iIntros "H".
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
  iApply wp_unop. iIntros (σ) "Hctx".
  iMod ("H" with "Hctx") as (Hv) "HΦ". iModIntro.
  iSplit.
  { iExists v'. by rewrite Hv. }
  by iIntros "!>" (v ->%Hv).
Qed.

Lemma wp_unop_det_pure v' v1 Φ op E ot:
  ( σ v, eval_un_op op ot σ v1 v  v = v') 
   Φ v' -
  WP UnOp op ot (Val v1) @ E {{ Φ }}.
Proof.
  iIntros (Hop) "HΦ". iApply (wp_unop_det v').
  iIntros (σ) "Hσ". iApply fupd_mask_intro; [set_solver|]. iIntros "He".
  iSplit; [done|]. iModIntro. iMod "He". by iFrame.
Michael Sammler's avatar
Michael Sammler committed
217
218
Qed.

219
220
Lemma wp_deref v Φ vl l ly q E o:
  o = ScOrd  o = Na1Ord 
Michael Sammler's avatar
Michael Sammler committed
221
222
223
  val_to_loc vl = Some l 
  l `has_layout_loc` ly 
  v `has_layout_val` ly 
224
  l{q}v -  (l {q} v - Φ v) - WP !{ly, o} (Val vl) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
225
Proof.
226
  iIntros (Ho Hl Hll Hlv) "Hmt HΦ".
227
  iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
228
  iIntros ([[h ub] fn]) "((%&Hhctx&Hactx)&Hfctx)/=".
229
  iDestruct (heap_mapsto_has_alloc_id with "Hmt") as %Haid.
230
  destruct o; try by destruct Ho.
231
232
  - 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.
233
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
234
    iSplit => //. unfold end_st, end_expr.
235
236
    have <- : (v = v') by apply: heap_at_inj_val.
    rewrite /heap_fmap/=. erewrite heap_upd_heap_at_id => //.
237
    iFrame. iSplit; first done. iApply wp_value. by iApply "HΦ".
238
239
  - iMod (heap_read_na with "Hhctx Hmt") as "(% & Hσ & Hσclose)" => //. iModIntro.
    iSplit; first by eauto 11 using DerefS.
240
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
241
    iSplit => //. unfold end_st, end_expr.
242
243
    have ? : (v = v') by apply: heap_at_inj_val. subst v'.
    iFrame => /=. iSplit; first done.
244
    iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
245
    iIntros ([[h2 ub2] fn2]) "((%&Hhctx&Hactx)&Hfctx)/=".
246
247
    iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
    iModIntro; iSplit; first by eauto 11 using DerefS.
248
249
250
251
    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
252
253
Qed.

254
255
256
257
258
259
260
(*
  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,
261
     ⌜val_to_Z vo it = Some z1⌝ ∗ ⌜val_to_Z ve it = Some z2⌝ ∗
262
263
264
265
266
267
268
269
270
     ⌜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
271
272
273
274
275
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 
Michael Sammler's avatar
Michael Sammler committed
276
277
  val_to_Z vo it = Some z1 
  val_to_Z ve it = Some z2 
278
279
  length vd = bytes_per_int it 
  (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
280
281
282
283
284
  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Φ".
285
  iApply wp_lift_expr_step; auto.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
286
  iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
287
288
  iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
  iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
Michael Sammler's avatar
Michael Sammler committed
289
  move: (Hvo) (Hve) => /val_to_Z_length ? /val_to_Z_length ?.
Michael Sammler's avatar
Michael Sammler committed
290
291
  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 %? => //.
292
  iModIntro. iSplit; first by eauto 15 using CasFailS.
293
  iIntros (? e2 σ2 efs Hst ?) "!>". inv_expr_step;
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
294
295
    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
296
  have ? : (length ve0 = length vo0) by congruence.
297
  iMod (heap_write with "Hhctx Hl2") as "[$ Hl2]" => //. iModIntro.
298
299
  iFrame. iSplit => //. iSplit; first done.
  iApply wp_value. by iApply ("HΦ" with "[$]").
Michael Sammler's avatar
Michael Sammler committed
300
301
302
303
304
305
306
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 
Michael Sammler's avatar
Michael Sammler committed
307
308
  val_to_Z vo it = Some z1 
  val_to_Z ve it = Some z2 
309
310
  length vd = bytes_per_int it 
  (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
311
312
  z1 = z2 
  l1vo - l2{q}ve -  (l1  vd - l2{q}ve - Φ (val_of_bool true)) -
313
  WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
314
Proof.
315
316
  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
317
  iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
318
319
  iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
  iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
Michael Sammler's avatar
Michael Sammler committed
320
  move: (Hvo) (Hve) => /val_to_Z_length ? /val_to_Z_length ?.
Michael Sammler's avatar
Michael Sammler committed
321
322
  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. }
323
  iModIntro. iSplit; first by eauto 15 using CasSucS.
324
  iIntros (? e2 σ2 efs Hst ?) "!>". inv_expr_step;
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
325
326
      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
327
  have ? : (length vo0 = length vd) by congruence.
328
  iMod (heap_write with "Hhctx Hl1") as "[$ Hmt]" => //. iModIntro.
329
330
  iFrame. iSplit => //. iSplit; first done.
  iApply wp_value. by iApply ("HΦ" with "[$]").
Michael Sammler's avatar
Michael Sammler committed
331
332
333
Qed.

Lemma wp_neg_int Φ v v' n E it:
Michael Sammler's avatar
Michael Sammler committed
334
335
  val_to_Z v it = Some n 
  val_of_Z (-n) it None = Some v' 
Michael Sammler's avatar
Michael Sammler committed
336
337
338
   Φ (v') - WP UnOp NegOp (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv Hv') "HΦ".
339
340
  iApply (wp_unop_det_pure v'); [|done].
  move => ??. split.
341
342
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
343
344
Qed.

345
Lemma wp_cast_int Φ v v' i E its itt:
Michael Sammler's avatar
Michael Sammler committed
346
347
  val_to_Z v its = Some i 
  val_of_Z i itt (val_to_byte_prov v) = Some v' 
Michael Sammler's avatar
Michael Sammler committed
348
349
350
   Φ (v') - WP UnOp (CastOp (IntOp itt)) (IntOp its) (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv Hv') "HΦ".
351
352
  iApply wp_unop_det_pure; [|done].
  move => ??. split.
353
354
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
355
356
357
358
359
360
361
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Φ".
362
363
  iApply wp_unop_det_pure; [|done].
  move => ??. split.
364
365
  - by inversion 1; simplify_eq.
  - move => ->. by econstructor.
Michael Sammler's avatar
Michael Sammler committed
366
367
Qed.

368
Lemma wp_cast_ptr_int Φ v v' l it p:
369
  val_to_loc v = Some l 
Michael Sammler's avatar
Michael Sammler committed
370
371
  l.1 = ProvAlloc p 
  val_of_Z l.2 it p = Some v' 
372
  alloc_alive_loc l   Φ (v') -
373
  WP UnOp (CastOp (IntOp it)) PtrOp (Val v) {{ Φ }}.
374
Proof.
Michael Sammler's avatar
Michael Sammler committed
375
  iIntros (Hv Hp Hv') "HΦ".
376
377
378
379
380
381
382
383
384
385
386
  iApply (wp_unop_det v').
  iIntros (σ) "Hctx".
  destruct (decide (block_alive l (st_heap σ))).
  2: { iDestruct "HΦ" as "[Ha _]". by iMod (alloc_alive_loc_to_block_alive with "Ha Hctx") as %Hb. }
  iApply fupd_mask_intro; [done|]. iIntros "HE". iDestruct "HΦ" as "[_ HΦ]".
  iSplit. {
    iPureIntro. split.
    - have ? := val_to_of_loc NULL_loc. inversion 1; unfold NULL in *; destruct l; by simplify_eq/=.
    - move => ->. by econstructor.
  }
  iModIntro. iMod "HE". by iFrame.
387
388
389
Qed.

Lemma wp_cast_null_int Φ v E it:
Michael Sammler's avatar
Michael Sammler committed
390
  val_of_Z 0 it None = Some v 
391
392
393
394
   Φ v -
  WP UnOp (CastOp (IntOp it)) PtrOp (Val NULL) @ E {{ Φ }}.
Proof.
  iIntros (Hv) "HΦ".
395
396
  iApply wp_unop_det_pure; [|done].
  move => ??. split.
397
398
399
400
  - inversion 1; simplify_eq => //.
    all: destruct l; simplify_eq/=.
    all: have ? := val_to_of_loc NULL_loc.
    all: unfold NULL in *; by simplify_eq.
401
402
403
  - move => ->. by econstructor.
Qed.

Michael Sammler's avatar
Michael Sammler committed
404
405
406
Lemma wp_cast_int_ptr_weak Φ v a E it:
  val_to_Z v it = Some a 
  ( i,  Φ (val_of_loc (i, a))) -
407
  WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
408
409
Proof.
  iIntros (Hv) "HΦ".
410
  iApply wp_unop.
411
412
413
  iIntros (σ) "Hctx". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
  iSplit; [iPureIntro; eexists _; by econstructor |].
  iIntros "!>" (v' Hv'). iMod "HE". iModIntro. iFrame.
Michael Sammler's avatar
Michael Sammler committed
414
415
  inversion Hv'; simplify_eq.
  case_bool_decide; [ iApply "HΦ"|].
416
  case_bool_decide; simplify_eq; [ iApply "HΦ"|].
417
418
419
  case_bool_decide; simplify_eq; iApply "HΦ".
Qed.

420
Lemma wp_cast_int_ptr_alive Φ v a p l it:
Michael Sammler's avatar
Michael Sammler committed
421
422
423
  val_to_Z v it = Some a 
  val_to_byte_prov v = Some p 
  l = (ProvAlloc (Some p), a) 
424
  loc_in_bounds l 0 -
425
  alloc_alive_loc l   Φ (val_of_loc l) -
426
  WP UnOp (CastOp PtrOp) (IntOp it) (Val v) {{ Φ }}.
427
Proof.
Michael Sammler's avatar
Michael Sammler committed
428
  iIntros (Hv Hp ->) "#Hlib HΦ".
429
430
431
432
433
434
435
436
  iApply wp_unop_det. iIntros (σ) "Hctx".
  destruct (decide (valid_ptr (ProvAlloc (Some p), a) σ.(st_heap))).
  2: { iDestruct "HΦ" as "[Ha _]". by iMod (alloc_alive_loc_to_valid_ptr with "Hlib Ha Hctx") as %Hb. }
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE". iDestruct "HΦ" as "[_ HΦ]".
  iSplit. {
    iPureIntro. split.
    - inversion 1; simplify_eq; case_bool_decide; by rewrite ->Hp in *.
    - move => ->. econstructor; [done..|]. rewrite Hp. by case_bool_decide.
437
  }
438
  iModIntro. iMod "HE". by iFrame.
439
440
Qed.

441
Lemma wp_copy_alloc_id Φ it a l v1 v2:
Michael Sammler's avatar
Michael Sammler committed
442
  val_to_Z v1 it = Some a 
443
444
445
  val_to_loc v2 = Some l 
  loc_in_bounds (l.1, a) 0 -
  alloc_alive_loc l   Φ (val_of_loc (l.1, a)) -
446
  WP CopyAllocId (IntOp it) (Val v1) (Val v2) {{ Φ }}.
447
Proof.
448
449
450
451
452
453
  iIntros (Ha Hl) "#Hlib HΦ". iApply wp_lift_expr_step_fupd => //.
  iIntros (σ1) "Hctx".
  destruct (decide (valid_ptr (l.1, a) σ1.(st_heap))). 2: {
    iDestruct "HΦ" as "[Ha _]".
    iMod (alloc_alive_loc_to_valid_ptr with "Hlib [Ha] Hctx") as %Hb; [|done].
    by iApply alloc_alive_loc_mono; [|done].
454
  }
455
  iDestruct "HΦ" as "[_ HΦ]". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
456
  iSplit; first by eauto 8 using CopyAllocIdS.
457
  iIntros (???? Hstep ?) "!>!>". inv_expr_step. iMod "HE". iModIntro. iSplit => //. iFrame.
458
  by iApply wp_value.
459
460
Qed.

461
Lemma wp_ptr_relop Φ op v1 v2 v l1 l2 b:
462
463
  val_to_loc v1 = Some l1 
  val_to_loc v2 = Some l2 
Michael Sammler's avatar
Michael Sammler committed
464
  val_of_Z (Z_of_bool b) i32 None = Some v 
465
466
467
468
469
470
471
472
473
474
  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 -
Michael Sammler's avatar
Michael Sammler committed
475
  (alloc_alive_loc l1  alloc_alive_loc l2   Φ v) -
476
  WP BinOp op PtrOp PtrOp (Val v1) (Val v2) {{ Φ }}.
477
Proof.
Michael Sammler's avatar
Michael Sammler committed
478
  iIntros (Hv1 Hv2 Hv Hop) "#Hl1 #Hl2 HΦ".
Michael Sammler's avatar
Michael Sammler committed
479
480
  iDestruct (loc_in_bounds_has_alloc_id with "Hl1") as %[??].
  iDestruct (loc_in_bounds_has_alloc_id with "Hl2") as %[??].
481
  iApply wp_binop. iIntros (σ) "Hσ".
482
483
484
  destruct (decide (valid_ptr l1 σ.(st_heap))). 2: {
    iDestruct "HΦ" as "[Ha _]".
    by iMod (alloc_alive_loc_to_valid_ptr with "Hl1 Ha Hσ") as %?.
485
  }
486
487
488
  destruct (decide (valid_ptr l2 σ.(st_heap))). 2: {
    iDestruct "HΦ" as "[_ [Ha _]]".
    by iMod (alloc_alive_loc_to_valid_ptr with "Hl2 Ha Hσ") as %?.
489
  }
490
  iApply fupd_mask_intro; [done|]. iIntros "HE".
Michael Sammler's avatar
Michael Sammler committed
491
492
  destruct l1, l2; simplify_eq/=. iSplit.
  { iPureIntro. destruct op; eexists _; apply: RelOpPP => //; repeat case_bool_decide; naive_solver. }
493
  iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iMod "HE". iModIntro. iFrame.
Michael Sammler's avatar
Michael Sammler committed
494
495
496
  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.
Michael Sammler's avatar
Michael Sammler committed
497
  destruct op; repeat case_bool_decide; by simplify_eq.
498
499
Qed.

Michael Sammler's avatar
Michael Sammler committed
500
501
Lemma wp_ptr_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
Michael Sammler's avatar
Michael Sammler committed
502
  val_to_Z vo it = Some o 
503
  loc_in_bounds (l offset{ly} o) 0 -
504
505
   Φ (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
506
Proof.
507
  iIntros (Hvl Hvo) "Hl HΦ".
508
509
  iApply wp_binop_det. iIntros (σ) "Hσ".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
510
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
511
512
513
514
515
516
  iSplit. {
    iPureIntro. split.
    - inversion 1. by simplify_eq.
    - move => ->. by apply PtrOffsetOpIP.
  }
  iModIntro. iMod "HE". by iFrame.
Michael Sammler's avatar
Michael Sammler committed
517
518
Qed.

519
520
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
Michael Sammler's avatar
Michael Sammler committed
521
  val_to_Z vo it = Some o 
522
  loc_in_bounds (l offset{ly} -o) 0 -
523
524
   Φ (val_of_loc (l offset{ly} -o)) -
  WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
525
Proof.
526
  iIntros (Hvl Hvo) "Hl HΦ".
527
528
  iApply wp_binop_det. iIntros (σ) "Hσ".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
529
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
530
531
532
533
534
535
  iSplit. {
    iPureIntro. split.
    - inversion 1. by simplify_eq.
    - move => ->. by apply PtrNegOffsetOpIP.
  }
  iModIntro. iMod "HE". by iFrame.
536
537
Qed.

538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
Lemma wp_ptr_diff Φ vl1 l1 vl2 l2 ly vo:
  val_to_loc vl1 = Some l1 
  val_to_loc vl2 = Some l2 
  val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some vo 
  l1.1 = l2.1 
  0 < ly.(ly_size) 
  loc_in_bounds l1 0 -
  loc_in_bounds l2 0 -
  (alloc_alive_loc l1   Φ vo) -
  WP Val vl1 sub_ptr{ly , PtrOp, PtrOp} Val vl2 {{ Φ }}.
Proof.
  iIntros (Hvl1 Hvl2 Hvo ??) "Hl1 Hl2 HΦ".
  iApply wp_binop_det. iIntros (σ) "Hσ".
  destruct (decide (valid_ptr l1 σ.(st_heap))). 2: {
    iDestruct "HΦ" as "[Ha _]".
    by iMod (alloc_alive_loc_to_valid_ptr with "Hl1 Ha Hσ") as %?.
  }
  destruct (decide (valid_ptr l2 σ.(st_heap))). 2: {
    iDestruct "HΦ" as "[Ha _]".
    iMod (alloc_alive_loc_to_valid_ptr with "Hl2 [Ha] Hσ") as %?; [|done].
    by iApply alloc_alive_loc_mono.
  }
  iDestruct "HΦ" as "[_ ?]".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
  iSplit. {
    iPureIntro. split.
    - inversion 1; by simplify_eq.
    - move => ->. by apply: PtrDiffOpPP.
  }
  iModIntro. iMod "HE". by iFrame.
Qed.

Michael Sammler's avatar
Michael Sammler committed
570
571
572
Lemma wp_get_member Φ vl l sl n E:
  val_to_loc vl = Some l 
  is_Some (index_of sl.(sl_members) n) 
573
  loc_in_bounds l (ly_size sl) -
574
575
   Φ (val_of_loc (l at{sl} n)) -
  WP Val vl at{sl} n @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
576
Proof.
577
  iIntros (Hvl [i Hi]) "#Hl HΦ".
Michael Sammler's avatar
Michael Sammler committed
578
  rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
Michael Sammler's avatar
Michael Sammler committed
579
  have [|v Hv]:= (val_of_Z_is_Some None size_t (offset_of_idx sl.(sl_members) i)). {
580
    split; first by rewrite /min_int/=; lia. by apply offset_of_bound.
Michael Sammler's avatar
Michael Sammler committed
581
  }
582
  rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
Michael Sammler's avatar
Michael Sammler committed
583
  iApply wp_ptr_offset; [done| done | | ].
584
585
  { 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 ]. }
586
  by rewrite offset_loc_sz1.
Michael Sammler's avatar
Michael Sammler committed
587
588
589
590
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 {{ Φ }}.
591
592
593
594
595
Proof.
  iIntros (->%val_of_to_loc) "?".
  rewrite /GetMemberUnion/GetMemberUnionLoc.
  by iApply @wp_value.
Qed.
Michael Sammler's avatar
Michael Sammler committed
596

597
598
Lemma wp_offset_of Φ s m i E:
  offset_of s.(sl_members) m = Some i 
Michael Sammler's avatar
Michael Sammler committed
599
  ( v, val_of_Z i size_t None = Some v - Φ v) -
600
601
602
  WP OffsetOf s m @ E {{ Φ }}.
Proof.
  rewrite /OffsetOf. iIntros (Ho) "HΦ".
Michael Sammler's avatar
Michael Sammler committed
603
  have [|? Hs]:= (val_of_Z_is_Some None size_t i). {
604
605
606
607
    split; first by rewrite /min_int/=; lia.
    move: Ho => /fmap_Some[?[?->]].
    by apply offset_of_bound.
  }
608
  rewrite Ho /= Hs /=. iApply wp_value.
609
610
611
612
613
614
615
  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
616
Lemma wp_if Φ it v e1 e2 n:
Michael Sammler's avatar
Michael Sammler committed
617
  val_to_Z v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
618
619
620
621
622
623
  (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.
624
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
Michael Sammler's avatar
Michael Sammler committed
625
626
627
628
  iSplit => //. iFrame.
  by case_decide; case_bool_decide.
Qed.

Michael Sammler's avatar
Michael Sammler committed
629
630
631
632
Lemma wp_skip Φ v E:
   Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
633
634
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using SkipES.
635
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
636
  iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
637
638
639
640
641
642
Qed.

Lemma wp_concat E Φ vs:
  Φ (mjoin vs) - WP Concat (Val <$> vs) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
643
644
645
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?".
  iModIntro. iSplit; first by eauto 8 using ConcatS.
646
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
647
  iModIntro. iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
648
649
650
Qed.

Lemma wps_concat_bind_ind vs E Φ es:
651
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
652
        (λ vl, WP coerce_rtexpr (Concat (Val <$> (vs ++ vl))) @ E {{ Φ }}) es [] -
Michael Sammler's avatar
Michael Sammler committed
653
654
655
656
657
658
659
  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".
660
661
662
663
664
665
666
667
    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
668
669
670
Qed.

Lemma wp_concat_bind E Φ es:
671
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
672
        (λ vl, WP coerce_rtexpr (Concat (Val <$> vl)) @ E {{ Φ }}) es [] -
Michael Sammler's avatar
Michael Sammler committed
673
674
675
676
677
  WP Concat es @ E {{ Φ }}.
Proof. by iApply (wps_concat_bind_ind []). Qed.

Lemma wp_struct_init E Φ sl fs:
  foldr (λ '(n, ly) f, (λ vl,
678
     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
679
680
681
682
683
684
685
686
687
688
        @ 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.

689
690
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
691
        (λ vl, WP coerce_rtexpr (Call (Val vf) (Val <$> (vs ++ vl))) @ E {{ Φ }}) el [] -
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
  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
711
        (λ vl, WP coerce_rtexpr (Call (Val vf) (Val <$> vl)) @ E {{ Φ }}) el [] }} -
712
713
714
715
716
717
718
719
720
  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
721
722
723
End expr_lifting.

(*** Lifting of statements *)
724
Definition stmt_wp_def `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) (s : stmt) : iProp Σ :=
725
726
  ( Φ rf, Q = rf.(rf_fn).(f_code) - ( v, Ψ v - WP to_rtstmt rf (Return v) {{ Φ }}) -
    WP to_rtstmt rf s @ E {{ Φ }}).
727
728
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
729
  stmt  iProp Σ := (stmt_wp_aux E Q Ψ).(unseal).
730
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
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747

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.
748
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
749
750
751
  iApply fupd_wp. by iApply "Hs".
Qed.

752
753
754
755
756
757
758
759
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.

760
761
762
763
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Ψ".
764
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
765
766
767
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

768
769
770
771
772
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
773
774
          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), Ψ' }} 
775
776
777
778
779
780
781
782
         ( 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.
783
784
  iIntros "Hf HWP". iApply wp_lift_expr_step; first done.
  iIntros (σ1) "((%&Hhctx&Hbctx)&Hfctx)".
Michael Sammler's avatar
Michael Sammler committed
785
  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %[a [? Hfn]]; subst. iModIntro.
786
  iSplit; first by eauto 10 using CallFailS.
787
  iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
788
    (* Alloc failure case. *)
789
790
    iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
    iApply wp_alloc_failed.
Michael Sammler's avatar
Michael Sammler committed
791
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
792
  iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx]") as "[Hctx Hlv]" => //.
793
  rewrite big_sepL2_sep. iDestruct "Hlv" as "[Hlv Hfree_v]".
794
  iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
795
  rewrite big_sepL2_sep. iDestruct "Hla" as "[Hla Hfree_a]".
796
797
798
799
800
801
  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.
802
  }
Michael Sammler's avatar
Michael Sammler committed
803
  iFrame. rewrite stmt_wp_eq. iApply "HQinit" => //.
804
805
806
807

  (** prove Return *)
  iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
  iApply wp_lift_stmt_step => //.
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
  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.
823
  iSplit; first by eauto 8 using ReturnS.
824