vcgen.v 31.3 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
From iris.heap_lang Require Export proofmode notation.
2
From iris.algebra Require Import frac.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.bi Require Import big_op.
4
From iris_c.vcgen Require Import dcexpr splitenv denv.
Dan Frumin's avatar
Dan Frumin committed
5
6
7
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
(*
TODO

11
[DONE] Fix all the unknown cases, introduce a function for that (which should be
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
  simpl never)
- Write more tests with unknown stuff in it
14
  add tests like `!(l := 10;;;; l)`
Robbert Krebbers's avatar
Robbert Krebbers committed
15
- Support alloc in `vcg_wp`
Robbert Krebbers's avatar
Robbert Krebbers committed
16
- Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
21
22
23
24
25
26
27
28
- Finish the proofs
- Maybe drop `wp_expr`? We are not taking it as an input of anything anymore

Less urgent TODO

- Symbolic fractions
- Support bind
- Support conditional
- Write examples with R
- Deal with functions
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
35
36


Dan Frumin's avatar
Dan Frumin committed
37
38
39
Section vcg.
  Context `{amonadG Σ}.

40
41
  (** Deep embedding of formulae used to build the verification condition generator *)

42
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
43
    | Base : iProp Σ  wp_expr
44
45
    | MapstoStar : dloc  (frac  dval  wp_expr)  wp_expr
    | MapstoStarFull : dloc  (dval  wp_expr)  wp_expr
46
    | MapstoWand : dloc  dval  lvl  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
47
48
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
49
    | UMod : wp_expr  wp_expr.
50

51
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
52

53
  Fixpoint wp_interp (E : known_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
54
55
    match a with
    | Base Φ => Φ
56
    | MapstoStar dl Φ =>
57
        q v, dloc_interp E dl C{q} v  wp_interp E (Φ q (dValUnknown v))
58
    | MapstoStarFull dl Φ =>
59
        v, dloc_interp E dl C{1} v  wp_interp E (Φ (dValUnknown v))
60
    | MapstoWand dl dv x q Φ =>
61
       dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp E Φ
Dan Frumin's avatar
Dan Frumin committed
62
    | IsSome dmx Φ  =>
63
        x, doption_interp dmx = Some x  wp_interp E (Φ x)
Dan Frumin's avatar
Dan Frumin committed
64
    | IsLoc dv Φ =>
65
66
        l : loc, dval_interp E dv = #l  wp_interp E (Φ (dLocUnknown l))
    | UMod P => U (wp_interp E P)
67
    end%I.
Dan Frumin's avatar
Dan Frumin committed
68

69
  Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
70
    match m with
71
    | [] => Φ
72
73
74
    | None :: m' => mapsto_wand_list_aux m' Φ (S i)
    | Some (DenvItem x q dv) :: m' =>
       MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
75
76
    end.

77
78
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
79

Dan Frumin's avatar
Dan Frumin committed
80
81
82
83
84
85
86
87
88

  Definition popstack (mOut : list denv) : option (list denv * denv) :=
    match mOut with
    | [] => None
    | m::ms => Some (ms, m)
    end.

  Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr) 
       : option (denv * list denv * denv * dval) :=
89
    match de with
Dan Frumin's avatar
Dan Frumin committed
90
    | dCRet dv    => Some (mIn, mOut, [], dv)
91
    | dCLoad de1  =>
Dan Frumin's avatar
Dan Frumin committed
92
93
94
95
       ''(mIn1, mOut1, mNew, dl)       vcg_sp E mIn mOut de1;
       i                               is_dloc E dl;
       ''(mIn2, mOut2, mNew2, q, dv)   denv_delete_frac_3 i mIn1 mOut1 mNew;
       Some (mIn2, mOut2, denv_insert i ULvl q dv mNew2, dv)
96
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
97
98
99
100
101
       ''(mIn1, mOut1, mNew1, dl)  vcg_sp E mIn mOut de1;
       i                           is_dloc E dl;
       ''(mIn2, mOut2, mNew2, dv)  vcg_sp E mIn1 mOut1 de2;
       ''(mIn3, mOut3, mNew3, _)   denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2);
       Some (mIn3, mOut3, denv_insert i LLvl 1 dv mNew3, dv)
102
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
103
104
       ''(mIn1, mOut1, mNew1, dv1)  vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, mNew2, dv2)  vcg_sp E mIn1 mOut1 de2;
105
       match dbin_op_eval E op dv1 dv2 with
Dan Frumin's avatar
Dan Frumin committed
106
       | dSome dv => Some (mIn2, mOut2, denv_merge mNew1 mNew2, dv)
107
108
       | dNone | dUnknown _ => None
       end
109
    | dCUnOp op de =>
Dan Frumin's avatar
Dan Frumin committed
110
       ''(mIn1, mOut1, mNew1, dv)  vcg_sp E mIn mOut de;
111
       match dun_op_eval E op dv with
Dan Frumin's avatar
Dan Frumin committed
112
       | dSome dv' => Some (mIn1, mOut1, mNew1, dv')
113
114
       | dNone | dUnknown _ => None
       end
115
    | dCSeq de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
116
117
118
119
       ''(mIn1, mOut1, mNew1, _)    vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, mNew2, dv2)  vcg_sp E mIn1 (denv_unlock mNew1::mOut1) de2;
       ''(mOut3, mNew3)  popstack mOut2;
       Some (mIn2, mOut3, denv_merge mNew2 mNew3, dv2)
120
    | dCAlloc _ |  dCUnknown _ => None
121
122
    end.

Léon Gondelman's avatar
Léon Gondelman committed
123
124
125
126
127
128
129
130

  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
      (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
    mapsto_wand_list m $ Base $
      awp (dcexpr_interp E de) R (λ v,
         E' m' dv,
         v = dval_interp E' dv  
         E `prefix_of` E'  
131
132
         (denv_wf E' m') 
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
133
        denv_interp E' m' 
134
        wp_interp E' (Φ E' m' dv))%I.
Léon Gondelman's avatar
Léon Gondelman committed
135
136
  Arguments vcg_wp_unknown : simpl never.

137
138
139
140
141
142
143
144
145
146
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
      (Φ : denv  dval  wp_expr) : wp_expr :=
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
       | Some (_, dw) => Φ m dw
       | None =>
          mapsto_wand_list m $ MapstoStar (dLoc i) $ λ q dw,
            MapstoWand (dLoc i) dw ULvl q (Φ [] dw)
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
149
150
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
151
152
153
154
155
156
157
158
159
160
161
162
    end.

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : denv  dval  wp_expr) : wp_expr :=
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
       | Some (m', dw) => Φ (denv_insert i LLvl 1 dv2 m') dv2
       | None =>
          mapsto_wand_list m $ MapstoStarFull (dLoc i) $ λ _,
            MapstoWand (dLoc i) dv2 LLvl 1 (Φ [] dv2)
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
167
168
169
170
171
172
    end.

  Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
      (m : denv) (Φ : denv  dval  wp_expr) : wp_expr :=
    match dbin_op_eval E op dv1 dv2 with
    | dSome dw => Φ m dw
173
174
    | dUnknown (Some dw) => Φ m dw
    | _ => Base False
175
176
177
    end.

  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
178
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
179
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
180
    | dCRet dv => Φ E m dv
181
    | dCLoad de1 =>
182
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' (Φ E))
183
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
184
       match vcg_sp E m [] de1 with
Dan Frumin's avatar
Dan Frumin committed
185
       | Some (mIn, mOut, mNew, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
186
          vcg_wp E mIn de2 R (λ E mIn dv2,
Dan Frumin's avatar
Dan Frumin committed
187
            vcg_wp_store E dv1 dv2 (denv_merge (denv_merge mNew (denv_stack_merge mOut)) mIn) (Φ E))
188
       | None =>
Dan Frumin's avatar
Dan Frumin committed
189
          match vcg_sp E m [] de2 with
Dan Frumin's avatar
Dan Frumin committed
190
          | Some (mIn, mOut, mNew, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
191
             vcg_wp E mIn de1 R (λ E mIn dv1,
Dan Frumin's avatar
Dan Frumin committed
192
               vcg_wp_store E dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
193
          | None => vcg_wp_unknown R E de m Φ
194
195
196
          end
        end
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
197
       match vcg_sp E m [] de1 with
Dan Frumin's avatar
Dan Frumin committed
198
       | Some (mIn, mOut, mNew, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
          vcg_wp E mIn de2 R (λ E mIn dv2,
Dan Frumin's avatar
Dan Frumin committed
200
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E))
201
       | None =>
Dan Frumin's avatar
Dan Frumin committed
202
          match vcg_sp E m [] de2 with
Dan Frumin's avatar
Dan Frumin committed
203
          | Some (mIn, mOut, mNew, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
204
             vcg_wp E mIn de1 R (λ E mIn dv1,
Dan Frumin's avatar
Dan Frumin committed
205
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
206
          | None => vcg_wp_unknown R E de m Φ
207
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
208
       end
209
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
210
       vcg_wp E m de R (λ E m dv,
211
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
214
215
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
216
       vcg_wp E m de1 R (λ E m _,
217
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
218
    | _ => vcg_wp_unknown R E de m Φ
219
    end.
220
221
222
223
224
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Dan Frumin's avatar
Dan Frumin committed
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
  Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
    wp_interp E (mapsto_wand_list_aux m t k) -
    ([ list] ndio  m, from_option
                              (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
                               default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) -
    wp_interp E t.
  Proof.
    generalize dependent k.
    induction m; simpl. eauto.
    iIntros (k) "H1 [Hl H2]".
    destruct a as [[x q dv]|]; simpl.
    - rewrite -plus_n_O. iSpecialize ("H1" with "Hl").
      iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
    - iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
  Qed.

243
244
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
245
  Proof.
Dan Frumin's avatar
Dan Frumin committed
246
247
248
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
249

Dan Frumin's avatar
Dan Frumin committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
  Lemma vcg_sp_length E de mIn mOut mIn' mOut' mNew' dv :
    vcg_sp E mIn mOut de = Some (mIn', mOut', mNew', dv) 
    length mOut = length mOut'.
  Proof.
    revert mIn mOut mIn' mOut' mNew' dv. induction de;
    intros mIn mOut mIn' mOut' mNew' dv Hsp; simplify_eq/=; eauto.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hout; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (denv_delete_frac_3 i mIn1 mOut1 mNew1) as [[[[[mIn2 mOut2] mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde.
      + by eapply denv_delete_frac_3_length.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
      destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2)) as [[[[mIn3 mOut3] mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + transitivity (length mOut2). by eapply IHde2.
        by eapply denv_delete_full_3_length.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + by eapply IHde2.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde; simplify_eq/=.
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E mIn1 (denv_unlock mNew1 :: mOut1) de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
      destruct mOut2; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + apply IHde2 in Hde2. by simplify_eq/=.
  Qed.

  Lemma vcg_sp_correct' E de mIn mOut mIn' mOut' mNew' dv R :
    vcg_sp E mIn mOut de = Some (mIn', mOut', mNew', dv) 
    (denv_interp E mIn -
     denv_interp E mIn' 
     denv_stack_interp (reverse mOut) (reverse mOut') E
        (awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mNew'))).
  Proof.
296
  Proof.
Dan Frumin's avatar
Dan Frumin committed
297
298
299
300
    revert mIn mOut mIn' mOut' mNew' dv. induction de;
    iIntros (mIn mOut mIn' mOut' mNew' dv Hsp) "HmIn"; simplify_eq/=.
    - iFrame. iApply denv_stack_interp_intro.
      iApply awp_ret. wp_value_head. iSplit; eauto. rewrite /denv_interp //.
Dan Frumin's avatar
Dan Frumin committed
301
    - specialize (IHde mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
302
      destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
303
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
304
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
305
      destruct (denv_delete_frac_3 i mIn1 mOut1 mNew1) as [[[[[mIn2 mOut2] mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
306
      rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]".
Dan Frumin's avatar
Dan Frumin committed
307
308
309
310
      iDestruct (denv_delete_frac_3_interp with "HmIn1") as "[$ Hm]"; first eassumption.
      iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp".
      iApply (denv_stack_interp_mono with "Hawp").
      iIntros "[Hawp Hm]".
Léon Gondelman's avatar
Léon Gondelman committed
311
312
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
313
314
315
      iIntros (?) "[% HmNew1]". simplify_eq/=.
      iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
      iIntros "Hl". iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
316
      rewrite -denv_insert_interp.
Léon Gondelman's avatar
Léon Gondelman committed
317
      by iFrame.
Dan Frumin's avatar
Dan Frumin committed
318
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
319
      destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
320
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
321
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
322
323
324
325
      specialize (IHde2 mIn1 mOut1).
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|]; simplify_eq /=.
      destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2))
        as [[[[mIn3 mOut3] mNew3] dv3] |] eqn:Hfar; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
326
327
      rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
      rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2 Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
328
329
330
331
332
333
334
335
336
337
338
339
      rewrite denv_delete_full_3_interp; last done.
      iDestruct "HmIn2" as "[$ Hl]".
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
      iDestruct (denv_stack_interp_trans with "Hawp Hl") as "Hawp".
      iApply (denv_stack_interp_mono with "Hawp").
      iIntros "[[Hawp1  Hawp2] Hl]".
      iApply (a_store_spec with "Hawp1 Hawp2").
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=.
      iExists _, _; iSplit; eauto.
      rewrite -denv_merge_interp -denv_insert_interp.
      iDestruct ("Hl" with "[$HmNew1 $HmNew2]") as "[$ $]". 
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
340
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
341
342
343
      destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 mIn1 mOut1).
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|]; simplify_eq /=.
344
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
345
      rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
Léon Gondelman's avatar
Léon Gondelman committed
346
      rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
347
348
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
349
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
350
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
351
      iExists (dval_interp E dv). repeat iSplit; eauto.
352
      + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
353
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
354
    - specialize (IHde mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
355
      destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
356
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
357
      rewrite IHde; last done. iDestruct "HmIn" as "[$ Hawp]".
Dan Frumin's avatar
Dan Frumin committed
358
359
      iApply (denv_stack_interp_mono with "Hawp").
      iIntros "Hawp".
360
361
362
363
      iApply a_un_op_spec.
      iApply (awp_wand with "Hawp"). iIntros (v) "[% H]". simplify_eq/=.
      iExists (dval_interp E dv). repeat iSplit; eauto.
      iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu.
Dan Frumin's avatar
Dan Frumin committed
364
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
365
366
367
      destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 mIn1 (denv_unlock mNew1 :: mOut1)).
      destruct (vcg_sp E mIn1 _ de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
368
      rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
Dan Frumin's avatar
Dan Frumin committed
369
      rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2 Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
370
      (* TODO: wtf? *)
Dan Frumin's avatar
Dan Frumin committed
371
      assert (AsVal (λ: <>, dcexpr_interp E de2)).
372
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
Dan Frumin's avatar
Dan Frumin committed
373
374
375
376
377
378
379
      unfold popstack in Hsp.
      destruct mOut2 as [|t mOut2'] eqn:Houteq; simplify_eq/=.
      iFrame "HmIn2". rewrite !reverse_cons.
      rewrite -denv_stack_interp_snoc; last first.
      { rewrite !reverse_length. apply vcg_sp_length in Hsp2. eauto. }
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
380
      iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
381
382
383
384
385
386
387
      iIntros (?) "[% HmNew1]".
      rewrite (denv_unlock_interp E mNew1).
      (* rewrite (denv_unlock_interp E (denv_stack_merge mOut1)). *)
      iModIntro. 
      awp_seq. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]". rewrite -denv_merge_interp.
      iSplit; eauto. iFrame.
388
  Qed.
Dan Frumin's avatar
Dan Frumin committed
389

Dan Frumin's avatar
Dan Frumin committed
390
391
  Lemma vcg_sp_correct E de m mIn mOut mNew dv R :
    vcg_sp E m [] de = Some (mIn, mOut, mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
392
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
393
    denv_interp E mIn  denv_interp E (denv_stack_merge mOut)  awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mNew).
Dan Frumin's avatar
Dan Frumin committed
394
395
396
  Proof.
    iIntros (?) "Hm".
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
397
398
399
    rewrite reverse_nil denv_stack_interp_nil_l.
    iDestruct "Hawp" as "[HmOut $]". iApply denv_stack_merge_interp.
    by iApply denv_stack_reverse.
Dan Frumin's avatar
Dan Frumin committed
400
  Qed.
Dan Frumin's avatar
Dan Frumin committed
401
402
  
  Lemma vcg_sp_wf E de m mIn mOut mNew dv :
403
404
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
405
406
    vcg_sp E m [] de = Some (mIn, mOut, mNew, dv) 
    denv_wf E mIn  denv_wf E (denv_stack_merge mOut)  denv_wf E mNew  dval_wf E dv .
407
408
  Proof. Admitted.

409
  Lemma vcg_wp_unknown_correct R E m de Φ :
410
    denv_wf E m 
411
412
    denv_interp E m -
    wp_interp E (vcg_wp_unknown R E de m Φ) -
413
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
414
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
415
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
416
417
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
418
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
419
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
420
421
    iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
422
423
  Qed.

424
  Lemma vcg_wp_load_correct E m dv Φ :
425
    denv_wf E m 
426
427
428
    denv_interp E m -
    wp_interp E (vcg_wp_load E dv m (Φ E)) -
     (l:loc) q w, dval_interp E dv = #l  l C{q} w   (l C{q} w -
429
     E' dv' m', E `prefix_of` E'  dval_interp E' dv' = w  dval_wf E' dv' 
430
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv')).
431
432
433
  Proof.
    rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
    + destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
434
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
435
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
436
437
438
        iExists (dloc_interp E (dLoc i)), q,  (dval_interp E dv').
        iSplit. simplify_eq /=; done. iFrame. iIntros "Hl".
        iExists E, dv', m; iSplit; first done. iFrame.
439
440
        rewrite Hm0. iSplit; first done.
        eapply denv_lookup_wf in Hlkp; eauto with iFrame.
441
442
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
443
444
        iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
        iExists (dloc_interp E (dLoc i)), q, v'. iSplit; first done.
445
        iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
446
        iExists E, (dValUnknown v'), []; repeat (iSplit; first done); iFrame.
447
448
449
        unfold denv_interp, denv_wf. eauto.
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
450
451
       iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
       iExists l, q, v'. iSplit; first done.
452
       iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
453
454
       iExists E, (dValUnknown v'), []; iSplit; first done.
       iFrame. unfold denv_interp, denv_wf. eauto.
455
456
  Qed.

457
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
458
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
459
460
461
462
463
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
    wp_interp E (vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E)) -
    denv_interp E mOut -
     w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
464
     ( E' dv m', E0 `prefix_of` E'  dval_interp E' dv = w  dval_wf E' dv 
465
466
                  denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
467
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
468
    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
469
    * iExists (dval_interp E dw); iSplit.
470
471
      { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, (denv_merge mOut m).
472
473
      apply dbin_op_eval_dSome_wf in Hbin; try done.
      rewrite -denv_merge_interp //. eauto with iFrame.
474
475
    * destruct dw as [dw1|] eqn:Hdw; last done.
      iExists  (dval_interp E dw1); iSplit.
476
      iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
477
      iExists E, dw1, (denv_merge mOut m).
478
479
      rewrite -denv_merge_interp.
      apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
480
  Qed.
481

482
  Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
483
   E0 `prefix_of` E 
484
485
   denv_wf E m 
   dval_wf E dv2 
486
   denv_interp E m -
487
   wp_interp E (vcg_wp_store E dv1 dv2 m (Φ E)) -
Robbert Krebbers's avatar
Robbert Krebbers committed
488
489
    (l : loc) (w : val), dval_interp E dv1 = #l 
     l C w  (l C[LLvl] dval_interp E dv2 -
490
          E' dv m', E0 `prefix_of` E'  dval_interp E' dv = dval_interp E dv2 
491
492
        dval_wf E' dv  denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
493
494
495
496
   iIntros (Hpre Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
    destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
   - apply is_dloc_some in Hdloc; rewrite Hdloc.
     destruct (denv_delete_full i m)  as [[m' dv_old]|] eqn:Hdel.
497
498
499
500
501
     +  iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old); iSplit; first done.
        iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
        iSpecialize ("Hdel" with "[$Hm]"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
        iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
        iSplit. iPureIntro. apply denv_wf_insert; last done.
502
503
504
505
506
       by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
       rewrite -denv_insert_interp. iFrame.
     + rewrite mapsto_wand_list_spec.
       iSpecialize ("Hwp" with "[Hm]"); iFrame.
       iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; fold wp_interp.
507
       iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
508
509
510
511
       iIntros "Hl". iSpecialize ("Hwp" with "Hl").
       iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
   - rewrite mapsto_wand_list_spec.
     iSpecialize ("Hwp" with "[Hm]"); iFrame.
512
513
514
     iDestruct "Hwp" as (l ->) "Hwp"; fold wp_interp.
     iDestruct "Hwp" as (v) "[Hdv Hwp]"; fold wp_interp.
     iExists l,v ; iSplit; first done. iFrame.
515
516
     iIntros "Hl". iSpecialize ("Hwp" with "Hl").
     iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
517
  Qed.
518

Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
521
  (* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the
  conjunctions in the same order. *)
  Lemma vcg_wp_correct R E m de Φ :
522
    dcexpr_wf E de 
523
    denv_wf E m 
524
525
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
526
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
527
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
528
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
529
  Proof.
530
531
532
533
    revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
    - iApply awp_ret. wp_value_head.
      iExists E, d, m. iSplit; first done; by iFrame.
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
534
    - rewrite IHde //. iRename "Hm" into "Hawp".
535
536
      iSpecialize ("Hawp" with "Hwp"); simpl.
      iApply (a_load_spec_exists_frac with "[Hawp]").  iApply (awp_wand with "Hawp").
537
538
      iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <- Hm'wf Hwf2) "(Hm & Hwp)".
      iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done.
Léon Gondelman's avatar
Léon Gondelman committed
539
540
      iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
      iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
541
542
543
      iSpecialize ("Hwp" with "Hl").
      iDestruct "Hwp" as (Ef dvf mf Hpre' <- Hwf3 Hwf4) "(Hmf & Hwp)".
      iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro; trans E'. done.
544
    - rewrite{1} /vcg_wp; fold vcg_wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
      simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
546
547
      destruct (vcg_sp E m [] de1) as [[[[mIn mOut] mNew] dv1]|] eqn:Heqsp; last first.
      + destruct (vcg_sp E m [] de2) as [[[[mIn mOut] mNew] dv2]|] eqn:Heqsp2; last first.
548
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
549
550
        specialize (vcg_sp_wf _ _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ? & ?).
        iDestruct (vcg_sp_correct with "Hm") as "[HmIn [HmOut Hde2]]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
552
553
        clear Heqsp2 Heqsp.
        iDestruct (IHde1 with "HmIn Hwp") as "Hde1"; try done.
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
Dan Frumin's avatar
Dan Frumin committed
554
        iDestruct 1 as (E' dw m' ? <- ?) "(% & Hm' & H)". iIntros "[-> HmNew]".
555
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
556
        iApply (vcg_wp_store_correct with "[-H] H");
557
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
558
559
560
561
        rewrite -!denv_merge_interp. iFrame "Hm'".
        rewrite -!(denv_interp_mono E E'); eauto. iFrame.
      + specialize (vcg_sp_wf _ _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?&?).
        iDestruct (vcg_sp_correct with "Hm") as "[HmIn [HmOut Hde1]]"; first done. clear Heqsp.
562
563
        iDestruct (IHde2 with "HmIn Hwp") as "Hde2"; try done.
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
Dan Frumin's avatar
Dan Frumin committed
564
        iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m' ? <- ?) "(% & Hm' & H)".
Robbert Krebbers's avatar
Robbert Krebbers committed
565
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
566
        iApply (vcg_wp_store_correct with "[-H] H");
Robbert Krebbers's avatar
Robbert Krebbers committed
567
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
568
569
        rewrite -!denv_merge_interp. iFrame "Hm'". 
        rewrite -!(denv_interp_mono E E'); eauto. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
570
    - rewrite{1} /vcg_wp; fold vcg_wp.
571
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
572
573
      destruct (vcg_sp E m [] de1) as [[[[mIn mOut] mNew] dv1]|] eqn:Heqsp; last first.
      + destruct (vcg_sp E m [] de2) as [[[[mIn mOut] mNew] dv2]|] eqn:Heqsp2; last first.
574
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
575
576
577
        iPoseProof (vcg_sp_correct) as "Hsp". eassumption.
        specialize (vcg_sp_wf _ _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?&?).
        iDestruct ("Hsp" with "[$Hm]") as "[HmIn [HmOut Hde2]]"; iClear "Hsp"; clear Heqsp2 Heqsp.
578
        rewrite IHde1; [| done | done]. iSpecialize ("HmIn" with "Hwp").
Dan Frumin's avatar
Dan Frumin committed
579
580
        iApply (a_bin_op_spec with "HmIn Hde2"); fold dcexpr_interp.
        iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
581
        iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
582
        rewrite (dval_interp_mono E E' dv2); eauto.
583
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
Dan Frumin's avatar
Dan Frumin committed
584
585
586
587
588
589
590
        iApply (vcg_wp_bin_op_correct with "[Hm' HmOut'] Hwp [HmNew]");
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
        * rewrite -denv_merge_interp. iFrame.
        * iApply (denv_interp_mono with "HmNew"); eauto.
      + iPoseProof (vcg_sp_correct) as "Hsp". eassumption.
        specialize (vcg_sp_wf _ _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?&?).
        iDestruct ("Hsp" with "Hm") as "[HmIn [HmOut Hde1]]"; iClear "Hsp"; clear Heqsp.
591
592
        rewrite IHde2; [| done | done]. iSpecialize ("HmIn" with "Hwp").
        iRename "HmIn" into "Hde2".
Dan Frumin's avatar
Dan Frumin committed
593
594
        iApply (a_bin_op_spec with "Hde1 Hde2");  fold dcexpr_interp.
        iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
595
        iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
596
        rewrite (dval_interp_mono E E' dv1); eauto.
597
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
Dan Frumin's avatar
Dan Frumin committed
598
599
600
601
        iApply (vcg_wp_bin_op_correct with "[Hm' HmOut'] Hwp [HmNew]");
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
        * rewrite -denv_merge_interp. iFrame.
        * iApply (denv_interp_mono with "HmNew"); eauto.
602
    - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
603
      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
604
      iDestruct "Hex" as (E' dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)".
605
606
607
608
      destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
      + iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
      + iExists (dval_interp E' dw); iSplit.
        iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
609
610
        iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
        eauto with iFrame.
611
612
613
      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
        iExists (dval_interp E' w). iSplit. iPureIntro.
        apply dun_op_eval_correct. by rewrite Hop.
614
615
616
617
        iExists E', w, m'. apply dun_op_eval_dUnknown_wf in Hop; last done.
        eauto with iFrame.
    - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
      rewrite IHde1 //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
618
619
620
      iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
      iApply (awp_wand with "Hm").  iIntros (v) "Hex".
621
      iDestruct "Hex" as (Enew dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)". simpl.
622
      rewrite denv_unlock_interp.
623
624
      iModIntro. rewrite IHde2 //. awp_seq. iSpecialize ("Hm" with "Hwp").
      specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre).
Léon Gondelman's avatar
Léon Gondelman committed
625
626
627
      intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
      iIntros (v) "Hex".
      iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
628
      iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
629
      iFrame. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock.
630
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
631
 Qed.
632

Léon Gondelman's avatar
Léon Gondelman committed
633
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
Dan Frumin's avatar
Dan Frumin committed
634
    MapstoListFromEnv Γs_in Γs_out Γls 
635
    E = penv_to_known_locs Γls 
Léon Gondelman's avatar
Léon Gondelman committed
636
    dcexpr_wf E de 
637
    denv_wf (penv_to_known_locs Γls) m 
638
    ListOfMapsto Γls E m 
Léon Gondelman's avatar
Léon Gondelman committed
639
    IntoDCexpr E e de 
640
    environments.envs_entails (environments.Envs Γp Γs_out c)
641
      (wp_interp E (vcg_wp E m de R (λ E m dv,
642
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
643
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
644
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
645
    rewrite /IntoDCexpr /=. intros Hsplit ->.
646
    rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
Léon Gondelman's avatar
Léon Gondelman committed
647
648
649
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
    rewrite (vcg_wp_correct R); last done.
650
    iIntros (->) "H1 H2".
Léon Gondelman's avatar
Léon Gondelman committed
651
    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
652
    iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & % & % & Hm & Hwp)".
653
654
    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
   Qed.
655
End vcg_spec.
656

657
(* Arguments wp_interp : simpl never. *)
658

659
660
661
662
Ltac vcg_solver :=
  eapply tac_vcg_sound;
    [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
    | compute; reflexivity (*  E = penv_to_known_locs Γls *)
663
664
    |       (* dcexpr_wf E de *)
    |       (* denv_wf E m *)
665
666
    | apply _ (* ListOfMapsto Γls E m *)
    | apply _ (* IntoDCexpr E e dce *)
Léon Gondelman's avatar
Léon Gondelman committed
667
    | simpl ]; intuition.