lifting.v 40.2 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
Proof. done. Qed.

Michael Sammler's avatar
Michael Sammler committed
26
27
28
Global Instance wp_expr_wp `{!refinedcG Σ} : Wp (iProp Σ) expr val stuckness :=
  λ s E e Φ, (WP (coerce_rtexpr e) @ s; E {{ Φ }})%I.

Michael Sammler's avatar
Michael Sammler committed
29
30
31
32
33
34
35
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;
36
37
    [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
38

39
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
40
Proof. solve_atomic. Qed.
41
Instance skipe_atomic s (v : val) : Atomic s (coerce_rtexpr (SkipE v)).
Michael Sammler's avatar
Michael Sammler committed
42
Proof. solve_atomic. Qed.
43
44
45
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)).
46
Proof. solve_atomic. Qed.
Michael Sammler's avatar
Michael Sammler committed
47

48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(*** 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 
67
        ( os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
68
69
70
71
72
          ={}=  (|={,E}=> tsl = []  state_ctx σ2  WP e2 @ E {{ Φ }})))
      - WP e @ E {{ Φ }}.
  Proof.
    iIntros (He ?) "HWP".
    iApply wp_lift_head_step_fupd => //.
73
74
    iIntros (σ1 κ κs n ?) "[[% Hhctx] Hfnctx]".
    iMod ("HWP" $! σ1 with "[$Hhctx $Hfnctx//]") as (Hstep) "HWP".
75
76
77
78
79
    iModIntro. iSplit. {
      iPureIntro. destruct Hstep as (?&?&?&?&?).
      naive_solver eauto using ExprStep, StmtStep.
    }
    clear Hstep. iIntros (??? Hstep).
80
    move: (Hstep) => /runtime_step_preserves_invariant?.
81
82
83
    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.
84
    all: iMod ("HWP" with "[//] [%]") as "HWP"; first naive_solver.
85
86
87
88
89
90
91
92
    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 
93
        ( os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
94
95
96
97
98
99
100
          ={}=  (|={,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 
101
        ( os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
102
103
104
105
106
107
108
109
110
111
          ={}=  (|={,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 
112
         ( os e2 σ2 tsl, step_rel σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
113
114
115
116
117
118
          ={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
119
    iApply fupd_mask_intro; first set_solver. iIntros "HE".
120
    iIntros (??????) "!> !>". iMod "HE". by iMod ("HWP" with "[//] [//]") as "$".
121
122
123
124
125
126
  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 
127
         ( os e2 σ2 tsl, expr_step e σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
128
129
130
131
132
133
134
          ={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 
135
         ( os e2 σ2 tsl, stmt_step s rf σ1 os e2 σ2 tsl - heap_state_invariant σ2.(st_heap)
136
137
138
139
140
          ={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
141

142
(*** Lifting of expressions *)
Michael Sammler's avatar
Michael Sammler committed
143
144
145
Section expr_lifting.
Context `{!refinedcG Σ}.

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

Lemma wp_binop_det v' v1 v2 Φ op E ot1 ot2:
163
  ( σ, state_ctx σ ={E, }=  v, eval_bin_op op ot1 ot2 σ v1 v2 v  v = v'  ( |={, E}=> state_ctx σ  Φ v')) -
164
    WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
165
Proof.
166
  iIntros "H".
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
  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
182
183
Qed.

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

Lemma wp_unop_det v' v1 Φ op E ot:
201
  ( σ, state_ctx σ ={E, }=  v, eval_un_op op ot σ v1 v  v = v'  ( |={, E}=> state_ctx σ  Φ v')) -
202
  WP UnOp op ot (Val v1) @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
203
Proof.
204
  iIntros "H".
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
  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
220
221
Qed.

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

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

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

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

371
Lemma wp_cast_ptr_int Φ v v' l it p:
372
  val_to_loc v = Some l 
Michael Sammler's avatar
Michael Sammler committed
373
374
  l.1 = ProvAlloc p 
  val_of_Z l.2 it p = Some v' 
375
  alloc_alive_loc l   Φ (v') -
376
  WP UnOp (CastOp (IntOp it)) PtrOp (Val v) {{ Φ }}.
377
Proof.
Michael Sammler's avatar
Michael Sammler committed
378
  iIntros (Hv Hp Hv') "HΦ".
379
380
381
382
383
384
385
386
387
388
389
  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.
390
391
392
Qed.

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

Michael Sammler's avatar
Michael Sammler committed
407
408
409
Lemma wp_cast_int_ptr_weak Φ v a E it:
  val_to_Z v it = Some a 
  ( i,  Φ (val_of_loc (i, a))) -
410
  WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
411
412
Proof.
  iIntros (Hv) "HΦ".
413
  iApply wp_unop.
414
415
416
  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
417
418
  inversion Hv'; simplify_eq.
  case_bool_decide; [ iApply "HΦ"|].
419
  case_bool_decide; simplify_eq; [ iApply "HΦ"|].
420
421
422
  case_bool_decide; simplify_eq; iApply "HΦ".
Qed.

423
Lemma wp_cast_int_ptr_alive Φ v a p l it:
Michael Sammler's avatar
Michael Sammler committed
424
425
426
  val_to_Z v it = Some a 
  val_to_byte_prov v = Some p 
  l = (ProvAlloc (Some p), a) 
427
  loc_in_bounds l 0 -
428
  alloc_alive_loc l   Φ (val_of_loc l) -
429
  WP UnOp (CastOp PtrOp) (IntOp it) (Val v) {{ Φ }}.
430
Proof.
Michael Sammler's avatar
Michael Sammler committed
431
  iIntros (Hv Hp ->) "#Hlib HΦ".
432
433
434
435
436
437
438
439
  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.
440
  }
441
  iModIntro. iMod "HE". by iFrame.
442
443
Qed.

444
Lemma wp_copy_alloc_id Φ it a l v1 v2:
Michael Sammler's avatar
Michael Sammler committed
445
  val_to_Z v1 it = Some a 
446
447
448
  val_to_loc v2 = Some l 
  loc_in_bounds (l.1, a) 0 -
  alloc_alive_loc l   Φ (val_of_loc (l.1, a)) -
449
  WP CopyAllocId (IntOp it) (Val v1) (Val v2) {{ Φ }}.
450
Proof.
451
452
453
454
455
456
  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].
457
  }
458
  iDestruct "HΦ" as "[_ HΦ]". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
459
  iSplit; first by eauto 8 using CopyAllocIdS.
460
  iIntros (???? Hstep ?) "!>!>". inv_expr_step. iMod "HE". iModIntro. iSplit => //. iFrame.
461
  by iApply wp_value.
462
463
Qed.

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

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

522
523
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
524
  val_to_Z vo it = Some o 
525
  loc_in_bounds (l offset{ly} -o) 0 -
526
527
   Φ (val_of_loc (l offset{ly} -o)) -
  WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
528
Proof.
529
  iIntros (Hvl Hvo) "Hl HΦ".
530
531
  iApply wp_binop_det. iIntros (σ) "Hσ".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
532
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
533
534
535
536
537
538
  iSplit. {
    iPureIntro. split.
    - inversion 1. by simplify_eq.
    - move => ->. by apply PtrNegOffsetOpIP.
  }
  iModIntro. iMod "HE". by iFrame.
539
540
Qed.

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

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

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

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

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

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

Lemma wp_struct_init E Φ sl fs:
  foldr (λ '(n, ly) f, (λ vl,
Michael Sammler's avatar
Michael Sammler committed
681
     WP (default (Val (replicate (ly_size ly) MPoison)) (n'  n; (list_to_map fs : gmap _ _) !! n'))
Michael Sammler's avatar
Michael Sammler committed
682
683
684
685
686
687
688
689
690
691
        @ 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.

692
Lemma wp_call_bind_ind vs E Φ vf el:
Michael Sammler's avatar
Michael Sammler committed
693
694
  foldr (λ e f, (λ vl, WP e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP Call (Val vf) (Val <$> (vs ++ vl)) @ E {{ Φ }}) el [] -
695
696
697
698
699
700
701
  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".
Michael Sammler's avatar
Michael Sammler committed
702
    rewrite /wp/wp_expr_wp.
703
704
705
706
707
708
709
710
711
712
713
    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:
Michael Sammler's avatar
Michael Sammler committed
714
715
  WP ef @ E {{ vf, foldr (λ e f, (λ vl, WP e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP Call (Val vf) (Val <$> vl) @ E {{ Φ }}) el [] }} -
716
717
718
  WP (Call ef el) @ E {{ Φ }}.
Proof.
  iIntros "HWP".
Michael Sammler's avatar
Michael Sammler committed
719
  rewrite /wp/wp_expr_wp.
720
721
722
723
724
725
  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
726
727
728
End expr_lifting.

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

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.
753
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
754
755
756
  iApply fupd_wp. by iApply "Hs".
Qed.

757
758
759
760
761
762
763
764
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.

765
766
767
768
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Ψ".
769
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
770
771
772
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

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