lifting.v 43.5 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
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
Lemma wp_cast_int_null Φ v E it:
  val_to_Z v it = Some 0 
   Φ (val_of_loc NULL_loc) -
  WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
  iIntros (Hv) "HΦ".
  iApply wp_unop_det_pure; [|done].
  move => ??. split.
  - inversion 1; simplify_eq => //. case_bool_decide; last done. exfalso.
    revert select (valid_ptr _ _) => /valid_ptr_in_allocation_range []/=.
    rewrite /min_alloc_start //.
  - move => ->. econstructor => //. case_bool_decide; last done. exfalso.
    revert select (valid_ptr _ _) => /valid_ptr_in_allocation_range []/=.
    rewrite /min_alloc_start //.
Qed.

460
Lemma wp_copy_alloc_id Φ it a l v1 v2:
Michael Sammler's avatar
Michael Sammler committed
461
  val_to_Z v1 it = Some a 
462
463
464
  val_to_loc v2 = Some l 
  loc_in_bounds (l.1, a) 0 -
  alloc_alive_loc l   Φ (val_of_loc (l.1, a)) -
465
  WP CopyAllocId (IntOp it) (Val v1) (Val v2) {{ Φ }}.
466
Proof.
467
468
469
470
471
472
  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].
473
  }
474
  iDestruct "HΦ" as "[_ HΦ]". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
475
  iSplit; first by eauto 8 using CopyAllocIdS.
476
  iIntros (???? Hstep ?) "!>!>". inv_expr_step. iMod "HE". iModIntro. iSplit => //. iFrame.
477
  by iApply wp_value.
478
479
Qed.

480
Lemma wp_ptr_relop Φ op v1 v2 v l1 l2 b rit:
481
482
  val_to_loc v1 = Some l1 
  val_to_loc v2 = Some l2 
483
  val_of_Z (Z_of_bool b) rit None = Some v 
484
  match op with
485
486
487
488
489
490
  | 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
491
  | _ => None
492
  end = Some (b, rit) 
493
  loc_in_bounds l1 0 - loc_in_bounds l2 0 -
Michael Sammler's avatar
Michael Sammler committed
494
  (alloc_alive_loc l1  alloc_alive_loc l2   Φ v) -
495
  WP BinOp op PtrOp PtrOp (Val v1) (Val v2) {{ Φ }}.
496
Proof.
Michael Sammler's avatar
Michael Sammler committed
497
  iIntros (Hv1 Hv2 Hv Hop) "#Hl1 #Hl2 HΦ".
Michael Sammler's avatar
Michael Sammler committed
498
499
  iDestruct (loc_in_bounds_has_alloc_id with "Hl1") as %[??].
  iDestruct (loc_in_bounds_has_alloc_id with "Hl2") as %[??].
500
  iApply wp_binop. iIntros (σ) "Hσ".
501
502
503
  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 %?.
504
  }
505
506
507
  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 %?.
508
  }
509
  iApply fupd_mask_intro; [done|]. iIntros "HE".
Michael Sammler's avatar
Michael Sammler committed
510
511
512
513
  destruct l1, l2; simplify_eq/=. iSplit. {
    iPureIntro. destruct op; simplify_eq/=; eexists _; try by apply: RelOpPP => //; repeat case_bool_decide; naive_solver.
    all: apply: CmpOpPP => //; by rewrite ?heap_loc_eq_alloc_alloc//= negb_bool_decide_eq.
  }
514
  iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iMod "HE". iModIntro. iFrame.
Michael Sammler's avatar
Michael Sammler committed
515
  inversion Hstep; simplify_eq => //.
Michael Sammler's avatar
Michael Sammler committed
516
517
518
  - revert select (heap_loc_eq _ _ _ = _). rewrite heap_loc_eq_alloc_alloc // => ?. simplify_eq.
    destruct op; simplify_eq/= => //. by repeat case_bool_decide => //; simplify_eq/=.
  - destruct op; repeat case_bool_decide; by simplify_eq.
519
520
Qed.

Michael Sammler's avatar
Michael Sammler committed
521
522
Lemma wp_ptr_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
Michael Sammler's avatar
Michael Sammler committed
523
  val_to_Z vo it = Some o 
524
  loc_in_bounds (l offset{ly} o) 0 -
525
526
   Φ (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
527
Proof.
528
  iIntros (Hvl Hvo) "Hl HΦ".
529
530
  iApply wp_binop_det. iIntros (σ) "Hσ".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
531
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
532
533
534
535
536
537
  iSplit. {
    iPureIntro. split.
    - inversion 1. by simplify_eq.
    - move => ->. by apply PtrOffsetOpIP.
  }
  iModIntro. iMod "HE". by iFrame.
Michael Sammler's avatar
Michael Sammler committed
538
539
Qed.

540
541
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
542
  val_to_Z vo it = Some o 
543
  loc_in_bounds (l offset{ly} -o) 0 -
544
545
   Φ (val_of_loc (l offset{ly} -o)) -
  WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
546
Proof.
547
  iIntros (Hvl Hvo) "Hl HΦ".
548
549
  iApply wp_binop_det. iIntros (σ) "Hσ".
  iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
550
  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
551
552
553
554
555
556
  iSplit. {
    iPureIntro. split.
    - inversion 1. by simplify_eq.
    - move => ->. by apply PtrNegOffsetOpIP.
  }
  iModIntro. iMod "HE". by iFrame.
557
558
Qed.

559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
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
591
592
593
Lemma wp_get_member Φ vl l sl n E:
  val_to_loc vl = Some l 
  is_Some (index_of sl.(sl_members) n) 
594
  loc_in_bounds l (ly_size sl) -
595
596
   Φ (val_of_loc (l at{sl} n)) -
  WP Val vl at{sl} n @ E {{ Φ }}.
Michael Sammler's avatar
Michael Sammler committed
597
Proof.
598
  iIntros (Hvl [i Hi]) "#Hl HΦ".
Michael Sammler's avatar
Michael Sammler committed
599
  rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
Michael Sammler's avatar
Michael Sammler committed
600
  have [|v Hv]:= (val_of_Z_is_Some None size_t (offset_of_idx sl.(sl_members) i)). {
601
    split; first by rewrite /min_int/=; lia. by apply offset_of_bound.
Michael Sammler's avatar
Michael Sammler committed
602
  }
603
  rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
Michael Sammler's avatar
Michael Sammler committed
604
  iApply wp_ptr_offset; [done| done | | ].
605
606
  { 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 ]. }
607
  by rewrite offset_loc_sz1.
Michael Sammler's avatar
Michael Sammler committed
608
609
610
611
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 {{ Φ }}.
612
613
614
615
616
Proof.
  iIntros (->%val_of_to_loc) "?".
  rewrite /GetMemberUnion/GetMemberUnionLoc.
  by iApply @wp_value.
Qed.
Michael Sammler's avatar
Michael Sammler committed
617

618
619
Lemma wp_offset_of Φ s m i E:
  offset_of s.(sl_members) m = Some i 
Michael Sammler's avatar
Michael Sammler committed
620
  ( v, val_of_Z i size_t None = Some v - Φ v) -
621
622
623
  WP OffsetOf s m @ E {{ Φ }}.
Proof.
  rewrite /OffsetOf. iIntros (Ho) "HΦ".
Michael Sammler's avatar
Michael Sammler committed
624
  have [|? Hs]:= (val_of_Z_is_Some None size_t i). {
625
626
627
628
    split; first by rewrite /min_int/=; lia.
    move: Ho => /fmap_Some[?[?->]].
    by apply offset_of_bound.
  }
629
  rewrite Ho /= Hs /=. iApply wp_value.
630
631
632
633
634
635
636
  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
637
Lemma wp_if_int Φ it v e1 e2 n:
Michael Sammler's avatar
Michael Sammler committed
638
  val_to_Z v it = Some n 
639
  (if bool_decide (n  0) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -
Michael Sammler's avatar
Michael Sammler committed
640
641
642
643
  WP IfE (IntOp it) (Val v) e1 e2 {{ Φ }}.
Proof.
  iIntros (?) "HΦ".
  iApply wp_lift_expr_step; auto.
Michael Sammler's avatar
Michael Sammler committed
644
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using IfESI.
645
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
646
  iSplit => //. iFrame. by case_bool_decide.
Michael Sammler's avatar
Michael Sammler committed
647
648
Qed.

Michael Sammler's avatar
Michael Sammler committed
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
Definition wp_if_precond (l : loc) : iProp Σ :=
  match l.1 with | ProvNull => l = NULL_loc | ProvAlloc _ => loc_in_bounds l 0 | _ => True end.

Lemma wp_if_precond_null:
   wp_if_precond NULL_loc.
Proof. rewrite /wp_if_precond/=. by iPureIntro. Qed.

Lemma wp_if_precond_alloc l:
  loc_in_bounds l 0 -
  wp_if_precond l.
Proof.
  iIntros "Hlib". rewrite /wp_if_precond.
  by iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? ->].
Qed.

Lemma wp_if_precond_heap_loc_eq l σ:
  wp_if_precond l -
  state_ctx σ -
  heap_loc_eq l NULL_loc σ.(st_heap) = Some (bool_decide (l = NULL_loc)).
Proof.
  rewrite/wp_if_precond. iIntros "Hlib Hσ". case_match.
  - iDestruct "Hlib" as %?; simplify_eq. iPureIntro. rewrite heap_loc_eq_NULL_NULL. by case_bool_decide.
  - iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ") as %Hlib. iPureIntro.
    rewrite heap_loc_eq_alloc_NULL //. case_bool_decide => //; simplify_eq.
  - iPureIntro. rewrite heap_loc_eq_fnptr_NULL //. case_bool_decide => //; simplify_eq.
Qed.

676
677
Lemma wp_if_ptr Φ v e1 e2 l:
  val_to_loc v = Some l 
Michael Sammler's avatar
Michael Sammler committed
678
  wp_if_precond l -
679
680
681
682
683
  (if bool_decide (l  NULL_loc) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -
  WP IfE PtrOp (Val v) e1 e2 {{ Φ }}.
Proof.
  iIntros (?) "Hlib HΦ".
  iApply wp_lift_expr_step; auto.
Michael Sammler's avatar
Michael Sammler committed
684
685
686
687
688
  iIntros (σ1) "Hσ1". iModIntro.
  iDestruct (wp_if_precond_heap_loc_eq with "Hlib Hσ1") as %?.
  iSplit; first by eauto 8 using IfESP.
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
  iSplit => //. iFrame. by repeat case_bool_decide.
689
690
Qed.

Michael Sammler's avatar
Michael Sammler committed
691
692
693
694
Lemma wp_skip Φ v E:
   Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
695
696
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using SkipES.
697
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
698
  iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
699
700
701
702
703
704
Qed.

Lemma wp_concat E Φ vs:
  Φ (mjoin vs) - WP Concat (Val <$> vs) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
705
706
707
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?".
  iModIntro. iSplit; first by eauto 8 using ConcatS.
708
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
709
  iModIntro. iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
710
711
712
Qed.

Lemma wps_concat_bind_ind vs E Φ es:
Michael Sammler's avatar
Michael Sammler committed
713
714
  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
715
716
717
718
719
720
721
  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
722
    rewrite /wp/wp_expr_wp.
723
724
725
726
727
728
729
730
    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
731
732
733
Qed.

Lemma wp_concat_bind E Φ es:
Michael Sammler's avatar
Michael Sammler committed
734
735
  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
736
737
738
739
740
  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
741
     WP (default (Val (replicate (ly_size ly) MPoison)) (n'  n; (list_to_map fs : gmap _ _) !! n'))
Michael Sammler's avatar
Michael Sammler committed
742
743
744
745
746
747
748
749
750
751
        @ 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.

752
Lemma wp_call_bind_ind vs E Φ vf el:
Michael Sammler's avatar
Michael Sammler committed
753
754
  foldr (λ e f, (λ vl, WP e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP Call (Val vf) (Val <$> (vs ++ vl)) @ E {{ Φ }}) el [] -
755
756
757
758
759
760
761
  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
762
    rewrite /wp/wp_expr_wp.
763
764
765
766
767
768
769
770
771
772
773
    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
774
775
  WP ef @ E {{ vf, foldr (λ e f, (λ vl, WP e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP Call (Val vf) (Val <$> vl) @ E {{ Φ }}) el [] }} -
776
777
778
  WP (Call ef el) @ E {{ Φ }}.
Proof.
  iIntros "HWP".
Michael Sammler's avatar
Michael Sammler committed
779
  rewrite /wp/wp_expr_wp.
780
781
782
783
784
785
  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
786
787
788
End expr_lifting.

(*** Lifting of statements *)
789
Definition stmt_wp_def `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) (s : stmt) : iProp Σ :=
790
791
  ( Φ rf, Q = rf.(rf_fn).(f_code) - ( v, Ψ v - WP to_rtstmt rf (Return v) {{ Φ }}) -
    WP to_rtstmt rf s @ E {{ Φ }}).
792
793
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
794
  stmt  iProp Σ := (stmt_wp_aux E Q Ψ).(unseal).
795
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
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812

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.
813
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
814
815
816
  iApply fupd_wp. by iApply "Hs".
Qed.

817
818
819
820
821
822
823
824
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.

825
826
827
828
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Ψ".
829
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
830
831
832
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

Michael Sammler's avatar