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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Michael Sammler's avatar
Michael Sammler committed
415
416
Lemma wp_ptr_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
417
  val_to_Z vo it = Some o 
Michael Sammler's avatar
Michael Sammler committed
418
419
420
421
  0  o 
   Φ (val_of_loc (l offset{ly} o)) - WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
  iIntros (Hvl Hvo Ho) "HΦ".
422
423
424
425
  iApply wp_binop_det. iSplit; last done.
  iIntros (σ v) "_ !%". split.
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrOffsetOpIP.
Michael Sammler's avatar
Michael Sammler committed
426
427
Qed.

428
429
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
  val_to_loc vl = Some l 
430
  val_to_Z vo it = Some o 
431
432
433
434
435
436
437
438
439
   Φ (val_of_loc (l offset{ly} -o)) - WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
  iIntros (Hvl Hvo) "HΦ".
  iApply wp_binop_det. iSplit; last done.
  iIntros (σ v) "_ !%". split.
  - inversion 1. by simplify_eq.
  - move => ->. by apply PtrNegOffsetOpIP.
Qed.

Michael Sammler's avatar
Michael Sammler committed
440
441
442
443
444
445
446
Lemma wp_get_member Φ vl l sl n E:
  val_to_loc vl = Some l 
  is_Some (index_of sl.(sl_members) n) 
   Φ (val_of_loc (l at{sl} n)) - WP Val vl at{sl} n @ E {{ Φ }}.
Proof.
  iIntros (Hvl [i Hi]) "HΦ".
  rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
447
  have [|? Hs]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
448
    split; first by rewrite /min_int/=; lia.
Michael Sammler's avatar
Michael Sammler committed
449
450
    by apply offset_of_bound.
  }
451
  rewrite Hs /=. move: Hs => /val_to_of_Z Hs.
452
453
  iApply wp_binop_det. iSplit; last done.
  iIntros (σ v) "_ !%". split.
Michael Sammler's avatar
Michael Sammler committed
454
455
  - inversion 1; simplify_eq. by rewrite offset_loc_sz1.
  - move => ->. rewrite -(offset_loc_sz1 u8) //. apply: PtrOffsetOpIP => //. lia.
Michael Sammler's avatar
Michael Sammler committed
456
457
458
459
460
461
462
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 {{ Φ }}.
Proof. iIntros (->%val_of_to_loc) "?". rewrite /GetMemberUnion/GetMemberUnionLoc. by iApply @wp_value. Qed.

463
464
Lemma wp_offset_of Φ s m i E:
  offset_of s.(sl_members) m = Some i 
465
  ( v, val_of_Z i size_t = Some v - Φ v) -
466
467
468
  WP OffsetOf s m @ E {{ Φ }}.
Proof.
  rewrite /OffsetOf. iIntros (Ho) "HΦ".
469
  have [|? Hs]:= (val_of_Z_is_Some size_t i). {
470
471
472
473
    split; first by rewrite /min_int/=; lia.
    move: Ho => /fmap_Some[?[?->]].
    by apply offset_of_bound.
  }
474
  rewrite Ho /= Hs /=. iApply wp_value.
475
476
477
478
479
480
481
  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
482
Lemma wp_if Φ it v e1 e2 n:
483
  val_to_Z v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
484
485
486
487
488
489
  (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.
490
  iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
Michael Sammler's avatar
Michael Sammler committed
491
492
493
494
  iSplit => //. iFrame.
  by case_decide; case_bool_decide.
Qed.

Michael Sammler's avatar
Michael Sammler committed
495
496
497
498
Lemma wp_skip Φ v E:
   Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
499
500
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using SkipES.
501
  iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_expr_step.
502
  iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
503
504
505
506
507
508
Qed.

Lemma wp_concat E Φ vs:
  Φ (mjoin vs) - WP Concat (Val <$> vs) @ E {{ Φ }}.
Proof.
  iIntros "HΦ".
509
510
511
  iApply wp_lift_expr_step; auto.
  iIntros (σ1) "?".
  iModIntro. iSplit; first by eauto 8 using ConcatS.
512
  iIntros "!#" (? e2 σ2 efs Hst ?). inv_expr_step.
513
  iModIntro. iSplit => //. iFrame. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
514
515
516
Qed.

Lemma wps_concat_bind_ind vs E Φ es:
517
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
518
519
520
521
522
523
524
525
        (λ vl, WP Concat (Val <$> (vs ++ vl)) @ E {{ Φ }}) es [] -
  WP Concat ((Val <$> vs) ++ es) @ E {{ Φ }}.
Proof.
  rewrite -{2}(app_nil_r vs).
  move: {2 3}[] => vl2.
  elim: es vs vl2 => /=.
  - iIntros (vs vl2) "He". by rewrite !app_nil_r.
  - iIntros (e el IH vs vl2) "Hf".
526
527
528
529
530
531
532
533
    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
534
535
536
Qed.

Lemma wp_concat_bind E Φ es:
537
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
Michael Sammler's avatar
Michael Sammler committed
538
539
540
541
542
543
        (λ vl, WP Concat (Val <$> vl) @ E {{ Φ }}) es [] -
  WP Concat es @ E {{ Φ }}.
Proof. by iApply (wps_concat_bind_ind []). Qed.

Lemma wp_struct_init E Φ sl fs:
  foldr (λ '(n, ly) f, (λ vl,
544
     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
545
546
547
548
549
550
551
552
553
554
        @ 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.

555
556
557
558
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
Lemma wp_call_bind_ind vs E Φ vf el:
  foldr (λ e f, (λ vl, WP coerce_rtexpr e @ E {{ v, f (vl ++ [v]) }}))
        (λ vl, WP (Call (Val vf) (Val <$> (vs ++ vl))) @ E {{ Φ }}) el [] -
  WP (Call (Val vf) ((Val <$> vs) ++ el)) @ E {{ Φ}}.
Proof.
  rewrite -{2}(app_nil_r vs).
  move: {2 3}[] => vl2.
  elim: el vs vl2 => /=.
  - iIntros (vs vl2) "He". by rewrite !app_nil_r.
  - iIntros (e el IH vs vl2) "Hf".
    have -> : (coerce_rtexpr (Call (Val vf) ((Val <$> vs ++ vl2) ++ e :: el)))%E = (fill [ExprCtx (CallRCtx vf (vs ++ vl2) (to_rtexpr <$> el))] (to_rtexpr e)). {
        by rewrite /coerce_rtexpr/= fmap_app fmap_cons -!list_fmap_compose.
    }
    iApply wp_bind. iApply (wp_wand with "Hf").
    iIntros (v) "Hf" => /=.
    have -> : Expr (RTCall vf ((Expr <$> (RTVal <$> vs ++ vl2)) ++ of_val v :: (to_rtexpr <$> el)))
             = Call vf ((Val <$> vs ++ (vl2 ++ [v])) ++ el). 2: by iApply IH.
    by rewrite /coerce_rtexpr /= !fmap_app /= (cons_middle (of_val v)) !app_assoc -!list_fmap_compose.
Qed.

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

Michael Sammler's avatar
Michael Sammler committed
587
588
589
End expr_lifting.

(*** Lifting of statements *)
590
Definition stmt_wp_def `{!refinedcG Σ} (E : coPset) (Q : gmap label stmt) (Ψ : val  iProp Σ) (s : stmt) : iProp Σ :=
591
592
  ( Φ rf, Q = rf.(rf_fn).(f_code) - ( v, Ψ v - WP to_rtstmt rf (Return v) {{ Φ }}) -
    WP to_rtstmt rf s @ E {{ Φ }}).
593
594
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
595
  stmt  iProp Σ := (stmt_wp_aux E Q Ψ).(unseal).
596
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
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613

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.
614
  rewrite stmt_wp_unfold. iIntros "Hs" (? rf HQ) "HΨ".
615
616
617
  iApply fupd_wp. by iApply "Hs".
Qed.

618
619
620
621
622
623
624
625
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.

626
627
628
629
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Ψ".
630
  iApply "HΦ"; [ done | ..]. iIntros (v) "Hv".
631
632
633
  iApply "HΨ". iApply "H". iApply "Hv".
Qed.

634
635
636
637
638
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
639
640
          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), Ψ' }} 
641
642
643
644
645
646
647
648
         ( 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.
649
650
  iIntros "Hf HWP". iApply wp_lift_expr_step; first done.
  iIntros (σ1) "((%&Hhctx&Hbctx)&Hfctx)".
651
652
  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %Hfn. iModIntro.
  iSplit; first by eauto 10 using CallFailS.
653
  iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
654
    (* Alloc failure case. *)
655
656
    iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
    iApply wp_alloc_failed.
Michael Sammler's avatar
Michael Sammler committed
657
  }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
658
  iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx]") as "[Hctx Hlv]" => //.
659
  rewrite big_sepL2_sep. iDestruct "Hlv" as "[Hlv Hfree_v]".
660
  iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
661
  rewrite big_sepL2_sep. iDestruct "Hla" as "[Hla Hfree_a]".
662
663
664
665
666
667
  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.
668
  }
Michael Sammler's avatar
Michael Sammler committed
669
  iFrame. rewrite stmt_wp_eq. iApply "HQinit" => //.
670
671
672
673

  (** prove Return *)
  iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
  iApply wp_lift_stmt_step => //.
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
  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.
689
  iSplit; first by eauto 8 using ReturnS.
690
691
692
  iIntros (os ts3 σ2' ? Hst ?). inv_stmt_step. iIntros "!>". iSplitR => //.
  have ->: (σ2 = hs) by apply: free_blocks_inj.
  iFrame. iModIntro. by iApply wp_value.
Michael Sammler's avatar
Michael Sammler committed
693
694
695
696
Qed.

Lemma wps_return Q Ψ v:
  Ψ v - WPs (Return (Val v)) {{ Q , Ψ }}.
697
Proof. rewrite stmt_wp_unfold. iIntros "Hb" (? rf ?) "HΨ". by iApply "HΨ". Qed.
Michael Sammler's avatar
Michael Sammler committed
698
699
700
701
702

Lemma wps_goto Q Ψ b s:
  Q !! b = Some s 
   WPs s {{ Q, Ψ }} - WPs Goto b {{ Q , Ψ }}.
Proof.
703
704
  iIntros (Hs) "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step. iIntros (?) "Hσ !>".
705
  iSplit; first by eauto 10 using GotoS.
706
  iIntros (???? Hstep ?) "!> !>". inv_stmt_step.
707
  iSplit; first done. iFrame. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
708
709
710
711
712
Qed.

Lemma wps_skip Q Ψ s:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs SkipS s {{ Q , Ψ }}.
Proof.
713
714
715
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
716
  iSplit; first by eauto 10 using SkipSS.
717
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
718
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
719
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
720
721
722
723
724
Qed.

Lemma wps_exprs Q Ψ s v:
  (|={}[]=> WPs s {{ Q, Ψ }}) - WPs ExprS (Val v) s {{ Q , Ψ }}.
Proof.
725
726
727
  iIntros "HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
  iApply wp_lift_stmt_step_fupd. iIntros (?) "Hσ".
  iMod "HWP" as "HWP". iModIntro.
728
  iSplit; first by eauto 10 using ExprSS.
729
  iIntros (???? Hstep ?). inv_stmt_step. iModIntro. iNext.
730
  iMod "HWP". iModIntro. iSplit; first done. iFrame.
731
  by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
732
733
734
735
736
737
738
739
740
741
742
743
744
745
Qed.

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

Lemma wps_assign Q Ψ vl ly vr s l o:
  let E := if o is ScOrd then  else  in
  o = ScOrd  o = Na1Ord 
  val_to_loc vl = Some l 
  vr `has_layout_val` ly 
746
747
  (|={,E}=> l|ly|   (lvr ={E,}= WPs s {{Q, Ψ}}))
    - WPs (Val vl <-{ly, o} Val vr; s) {{ Q , Ψ }}.
Michael Sammler's avatar
Michael Sammler committed
748
Proof.
749
  iIntros (E Ho Hvl Hly) "HWP". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
750
  iApply wp_lift_stmt_step_fupd. iIntros ([h1 ?]) "((%&Hhctx&Hfctx)&?) /=". iMod "HWP" as "[Hl HWP]".
Michael Sammler's avatar
Michael Sammler committed
751
  iApply (fupd_mask_weaken ); first set_solver. iIntros "HE".
752
  iDestruct "Hl" as (v' Hlyv' ?) "Hl".
753
754
  iDestruct (heap_mapsto_has_alloc_id with "Hl") as %Haid.
  unfold E. case: Ho => ->.
Michael Sammler's avatar
Michael Sammler committed
755
756
  - iModIntro.
    iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl") as %? => //.
757
    iSplit; first by eauto 12 using AssignS.
758
    iIntros (? e2 σ2 efs Hstep ?) "!> !>". inv_stmt_step. unfold end_val.
759
760
    iMod (heap_write with "Hhctx Hl") as "[$ Hl]" => //. congruence.
    iMod ("HWP" with "Hl") as "HWP".
761
    iModIntro => /=. iSplit; first done. iFrame. iSplit; first done. by iApply "HWP".
762
  - iMod (heap_write_na _ _ _ vr with "Hhctx Hl") as (?) "[Hhctx Hc]" => //; first by congruence.
763
    iModIntro. iSplit; first by eauto 12 using AssignS.
764
    iIntros (? e2 σ2 efs Hst ?) "!> !>". inv_stmt_step.
Michael Sammler's avatar
Michael Sammler committed
765
    have ? : (v' = v'0) by [apply: heap_at_inj_val]; subst v'0.
766
    iFrame => /=. iMod "HE" as "_". iModIntro. iSplit; first done.
767
    iSplit; first done.
Michael Sammler's avatar
Michael Sammler committed
768

769
770
    (* second step *)
    iApply wp_lift_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
771
    iIntros ([h2 ?]) "((%&Hhctx&Hfctx)&?)" => /=.
Michael Sammler's avatar
Michael Sammler committed
772
    iMod ("Hc" with "Hhctx") as (?) "[Hhctx Hmt]".
773
    iModIntro. iSplit; first by eauto 12 using AssignS. unfold end_stmt.
774
    iIntros (? e2 σ2 efs Hst ?) "!>". inv_stmt_step.
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
775
    have ? : (v' = v'0) by [apply: heap_lookup_loc_inj_val]; subst v'0.
Michael Sammler's avatar
Michael Sammler committed
776
    iFrame => /=. iMod ("HWP" with "Hmt") as "HWP".
777
    iModIntro. iSplit; first done. iSplit; first done. by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
778
779
780
Qed.

Lemma wps_switch Q Ψ v n ss def m it:
781
  val_to_Z v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
782
783
784
  ( i, m !! n = Some i  is_Some (ss !! i)) 
  WPs default def (i  m !! n; ss !! i) {{ Q, Ψ }} - WPs (Switch it (Val v) m ss def) {{ Q , Ψ }}.
Proof.
785
786
  iIntros (Hv Hm) "HWP". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
  iApply wp_lift_stmt_step. iIntros (?) "Hσ".
787
  iModIntro. iSplit; first by eauto 8 using SwitchS.
788
  iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
789
  iFrame "Hσ". by iApply "HWP".
Michael Sammler's avatar
Michael Sammler committed
790
791
792
793
Qed.

(** a version of wps_switch which is directed by ss instead of n *)
Lemma wps_switch' Q Ψ v n ss def m it:
794
  val_to_Z v it = Some n 
Michael Sammler's avatar
Michael Sammler committed
795
796
797
798
799
800
801
802
803
804
805
806
807
808
  map_Forall (λ _ i, is_Some (ss !! i)) m 
  ([ list] isss, m !! n = Some i - WPs s {{ Q, Ψ }}) 
  (m !! n = None - WPs def {{ Q, Ψ }}) -
  WPs (Switch it (Val v) m ss def) {{ Q , Ψ }}.
Proof.
  iIntros (Hn Hm) "Hs". iApply wps_switch; eauto.
  destruct (m !! n) as [i|] eqn:Hi => /=.
  - iDestruct "Hs" as "[Hs _]".
    destruct (ss !! i) as [s|] eqn:? => /=. 2: by move: (Hm _ _ Hi) => [??]; simplify_eq.
    by iApply (big_andL_lookup with "Hs").
  - iDestruct "Hs" as "[_ Hs]". by iApply "Hs".
Qed.

Lemma wps_if Q Ψ v s1 s2 n:
809
  val_to_Z v bool_it = Some n 
Michael Sammler's avatar
Michael Sammler committed
810
811
812
813
814
815
816
817
818
  (if decide (n = 0) then WPs s2 {{ Q, Ψ }} else WPs s1 {{ Q, Ψ }}) -
  WPs (if: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
  iIntros (Hn) "Hs". iApply wps_switch' => //=.
  1: by apply map_Forall_insert_2; eauto; apply map_Forall_empty.
  rewrite right_id. by iSplit; iIntros (?); simplify_map_eq.
Qed.

Lemma wps_assert Q Ψ v s n:
819
  val_to_Z v bool_it = Some n  n  0 
Michael Sammler's avatar
Michael Sammler committed
820
821
  WPs s {{ Q, Ψ }} -
  WPs (assert: Val v; s) {{ Q , Ψ }}.
822
823
824
825
Proof.
  iIntros (Hv Hn) "Hs". rewrite /notation.Assert.
  iApply wps_if => //. by case_decide.
Qed.
Michael Sammler's avatar
Michael Sammler committed
826

827
Definition wps_block (P : iProp Σ) (b : label) (Q : gmap label stmt) (Ψ : val  iProp Σ) : iProp Σ :=
Michael Sammler's avatar
Michael Sammler committed
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
  ( (P - WPs Goto b {{ Q, Ψ }})).

Lemma wps_block_rec Ps Q Ψ :
  ([ map] b  P  Ps,  s, Q !! b = Some s  (([ map] b  P  Ps, wps_block P b Q Ψ) - P - WPs s {{ Q, Ψ }})) -
  [ map] b  P  Ps, wps_block P b Q Ψ.
Proof.
  iIntros "#HQ". iLöb as "IH".
  iApply (big_sepM_impl with "HQ").
  iIntros "!#" (b P HPs).
  iDestruct 1 as (s HQ) "#Hs".
  iIntros "!# HP".
  iApply wps_goto. by apply: lookup_weaken.
  iModIntro. by iApply "Hs".
Qed.

End stmt_lifting.