vcgen.v 50.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 denv.
Dan Frumin's avatar
Dan Frumin committed
5
6
7
8
9
From iris_c.c_translation Require Import monad translation proofmode.

Section vcg.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
10
11
  Fixpoint mapsto_wand_list_aux
       (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
12
    match m with
13
    | [] => Φ
Léon Gondelman's avatar
Léon Gondelman committed
14
    | None :: m' => mapsto_wand_list_aux E m' Φ (S i)
15
    | Some (DenvItem x q dv) :: m' =>
16
      dloc_interp E (dLoc i 0) C[x]{q} dval_interp E dv -
Léon Gondelman's avatar
Léon Gondelman committed
17
        mapsto_wand_list_aux E m' Φ (S i)
Léon Gondelman's avatar
Léon Gondelman committed
18
    end%I.
19

Léon Gondelman's avatar
Léon Gondelman committed
20
21
  Definition mapsto_wand_list
       (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
Léon Gondelman's avatar
Léon Gondelman committed
22
    mapsto_wand_list_aux E m Φ O.
23
  Global Arguments mapsto_wand_list _ !_ /.
24

25
26
  Definition popstack (ms : list denv) : option (list denv * denv) :=
    match ms with
Dan Frumin's avatar
Dan Frumin committed
27
    | [] => None
28
    | m :: ms => Some (ms, m)
Dan Frumin's avatar
Dan Frumin committed
29
    end.
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
  Global Arguments popstack !_ /.

  Fixpoint vcg_eval_dexpr (de : dexpr) : option dval :=
    match de with
    | dEVal dv    => Some dv
    | dEPair de1 de2 =>
       dv1  vcg_eval_dexpr de1;
       dv2  vcg_eval_dexpr de2;
       Some (dPairV dv1 dv2)
    | dEFst de =>
       dv  vcg_eval_dexpr de;
       match dv with
       | dPairV dv1 _ => Some dv1
       | _ => None
       end
    | dESnd de =>
       dv  vcg_eval_dexpr de;
       match dv with
       | dPairV _ dv2 => Some dv2
       | _ => None
       end
    | dEUnknown _ => None
    end.
Dan Frumin's avatar
Dan Frumin committed
53

54
  Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
55
       : option (list denv * denv * dval) :=
56
    match de with
57
    | dCRet de    => dv  vcg_eval_dexpr de; Some (ms, [], dv)
58
    | dCLoad de1  =>
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
       ''(ms1, mNew, dl)      vcg_sp E ms de1;
       i                      is_dloc E dl;
       ''(ms2, mNew2, q, dv)  denv_delete_frac_2 i ms1 mNew;
       Some (ms2, denv_insert i ULvl q dv mNew2, dv)
63
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
       ''(ms1, mNew1, dl)  vcg_sp E ms de1;
       i                   is_dloc E dl;
       ''(ms2, mNew2, dv)  vcg_sp E ms1 de2;
       ''(ms3, mNew3, _)   denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
       Some (ms3, denv_insert i LLvl 1 dv mNew3, dv)
69
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
72
73
       dv  dcbin_op_eval E op dv1 dv2;
       Some (ms2, denv_merge mNew1 mNew2, dv)
Dan Frumin's avatar
Dan Frumin committed
74
75
76
77
78
    | dCPreBinOp op de1 de2 =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1;
       i                   is_dloc E dl;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
       ''(ms3, mNew3, dv)  denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
79
80
       dv3  dcbin_op_eval E op dv dv2;
       Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
81
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
82
       ''(ms1, mNew1, dv)  vcg_sp E ms de;
83
84
       dv'  dun_op_eval E op dv;
       Some (ms1, mNew1, dv')
85
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
89
       ''(ms1, mNew1, _)    vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E (denv_unlock mNew1 :: ms1) de2;
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
Léon Gondelman's avatar
Léon Gondelman committed
90
91
92
93
    | dCPar de1 de2 =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
94
    | dCAlloc _ _ |  dCUnknown _ | dCInvoke _ _ => None
95
96
    end.

Léon Gondelman's avatar
Léon Gondelman committed
97
98
  Definition vcg_sp'
       (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
    ''(ms,mNew,dv)  vcg_sp E [m] de;
    ''(_, m')  popstack ms;
    Some (m', mNew, dv).
102
  Global Arguments vcg_sp' _ _ !_ /.
Léon Gondelman's avatar
Léon Gondelman committed
103

Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Definition vcg_wp_continuation (E: known_locs)
105
106
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
107
108
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
109
         denv_wf E' m' 
110
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
111
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
112
        Φ E' m' dv)%I.
113

Léon Gondelman's avatar
Léon Gondelman committed
114
115
  Definition vcg_wp_awp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr)
      (m: denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
117

118
119
  Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
120
    mapsto_wand_list E m ( n : nat,
121
122
123
       dval_interp E dv1 = #n  
       l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I.

124
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
125
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
126
127
128
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
129
       | Some (_, dw) => Φ E m dw
130
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
131
         mapsto_wand_list E m ( q v,
132
133
           dloc_interp E (dLoc i 0) C{q} v 
           (dloc_interp E (dLoc i 0) C[ULvl]{q} dval_interp E (dValUnknown v) -
Robbert Krebbers's avatar
Robbert Krebbers committed
134
           vcg_wp_continuation E Φ v))
135
       end
136
137
138
139
    | None =>
       mapsto_wand_list E m ( (cl : cloc) q v,
         dval_interp E dv = cloc_to_val cl 
         cl C{q} v  (cl C{q} v - vcg_wp_continuation E Φ v))%I
Léon Gondelman's avatar
Léon Gondelman committed
140
    end%I.
141
142

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
143
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
144
145
146
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
147
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
148
       | None =>
149
          mapsto_wand_list E m ( v : val,
150
151
            dloc_interp E (dLoc i 0) C v 
            (dloc_interp E (dLoc i 0) C[LLvl] dval_interp E dv2 -
152
             vcg_wp_continuation E Φ (dval_interp E dv2)))
153
       end
154
    | None =>
155
156
157
158
       mapsto_wand_list E m ( (cl : cloc) (v : val),
         dval_interp E dv1 = cloc_to_val cl 
         cl C v 
         (cl C[LLvl] dval_interp E dv2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
159
          vcg_wp_continuation E Φ (dval_interp E dv2)))%I
Léon Gondelman's avatar
Léon Gondelman committed
160
    end%I.
161

162
163
  (* DF: the handling of pointer operations is uniform wrt other binary operations, but it doesnt work very well because of the deep embedding of cbin_op_eval *)
  Definition vcg_wp_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
Robbert Krebbers's avatar
Robbert Krebbers committed
164
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
165
    match dcbin_op_eval E op dv1 dv2 with
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
    | Some dw => Φ E m dw
    | None =>
       mapsto_wand_list E m ( v,
          cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some v  
         vcg_wp_continuation E Φ v)
    end%I.

  Definition vcg_wp_un_op (E : known_locs) (op : un_op) (dv : dval)
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match dun_op_eval E op dv with
    | Some dw => Φ E m dw
    | None =>
       mapsto_wand_list E m ( w,
         un_op_eval op (dval_interp E dv) = Some w 
         vcg_wp_continuation E Φ w)
Léon Gondelman's avatar
Léon Gondelman committed
181
    end%I.
182

183
  Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
Dan Frumin's avatar
Dan Frumin committed
184
185
186
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match is_dloc E dv1 with
    | Some i =>
187
188
189
      match denv_delete_full i m with
      | Some (m', dw) =>
        match dcbin_op_eval E op dw dv2 with
190
191
192
193
        | Some dw' => Φ E (denv_insert i LLvl 1 dw' m') dw
        | None =>
           mapsto_wand_list E m' $  w',
              cbin_op_eval op (dval_interp E dw) (dval_interp E dv2) = Some w' 
194
             (dloc_interp E (dLoc i 0) C[LLvl] w' - vcg_wp_continuation E Φ (dval_interp E dw))
195
        end
196
197
      | None =>
         mapsto_wand_list E m ( v w : val,
198
           dloc_interp E (dLoc i 0) C v 
199
            cbin_op_eval op v (dval_interp E dv2) = Some w  
200
           (dloc_interp E (dLoc i 0) C[LLvl] w - vcg_wp_continuation E Φ v))
201
      end
202
    | None =>
203
204
205
206
207
      mapsto_wand_list E m ( (cl : cloc) (v w : val),
        dval_interp E dv1 = cloc_to_val cl 
        cl C v 
        cbin_op_eval op v (dval_interp E dv2) = Some w 
        (cl C[LLvl] w - vcg_wp_continuation E Φ v))
Dan Frumin's avatar
Dan Frumin committed
208
209
    end%I.

210
  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman's avatar
Léon Gondelman committed
211
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
212
    match de with
Dan Frumin's avatar
Dan Frumin committed
213
    | dCRet de' =>
214
215
216
217
       match vcg_eval_dexpr de' with
       | Some dv => Φ E m dv
       | None => vcg_wp_awp_continuation R E de m Φ
       end
218
219
220
221
222
223
224
225
226
227
228
229
230
    | dCAlloc de1 de2 =>
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
            vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
               vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
          end
        end
231
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
232
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ)
233
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
234
235
236
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Robbert Krebbers's avatar
Robbert Krebbers committed
237
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
238
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
244
245
246
          end
        end
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
247
248
249
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Robbert Krebbers's avatar
Robbert Krebbers committed
250
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
251
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
257
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
258
       end
Dan Frumin's avatar
Dan Frumin committed
259
260
261
262
263
264
265
266
267
268
269
270
271
    | dCPreBinOp op de1 de2 =>
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
            vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
               vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
          end
       end
272
    | dCUnOp op de => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ)
273
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
274
       vcg_wp E m de1 R (λ E m _,
Léon Gondelman's avatar
Léon Gondelman committed
275
         U (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
276
277
278
279
280
281
282
283
284
285
286
287
288
    | dCPar de1 de2 =>
      match vcg_sp' E m de1 with
      | Some (m', mNew, dv1) =>
        vcg_wp E m' de2 R (λ E m'' dv2,
          (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
      | None =>
        match vcg_sp' E m de2 with
        | Some (m', mNew, dv2) =>
          vcg_wp E m' de1 R (λ E m'' dv1,
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
        | None => vcg_wp_awp_continuation R E de m Φ
        end
      end
289
    | dCInvoke ef de1 => vcg_wp E m de1 R (λ E m dv,
290
291
        vcg_wp_awp_continuation R E
           (dCUnknown (ef (dval_interp E dv))) m Φ)
Robbert Krebbers's avatar
Robbert Krebbers committed
292
    | _ => vcg_wp_awp_continuation R E de m Φ
Léon Gondelman's avatar
Léon Gondelman committed
293
    end%I.
294
295
296
297
298
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
299
300
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
301
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
302
        (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
303
           dloc_interp E (dLoc (k + n) 0) C[lv]{q} dval_interp E dv) True dio) - Φ.
Dan Frumin's avatar
Dan Frumin committed
304
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
305
306
    iIntros "H".
    iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
307
308
    - iIntros "[H1 H2]". rewrite -plus_n_O. iSpecialize ("H" with "H1").
      iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2").
Léon Gondelman's avatar
Léon Gondelman committed
309
310
311
312
313
314
      iIntros "!>" (n y ?) "/= H".
      by replace (k + S n)%nat with (S k + n)%nat by omega.
    - iIntros "[_ H2]". iApply ("IH" with "H [H2]").
      iApply (big_sepL_impl with "H2").
      iIntros "!>" (n y ?) "/= H".
      by replace (k + S n)%nat with (S k + n)%nat by omega.
Dan Frumin's avatar
Dan Frumin committed
315
316
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
317
318
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
319
  Proof.
Dan Frumin's avatar
Dan Frumin committed
320
321
322
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
323

Dan Frumin's avatar
Dan Frumin committed
324
325
326
  Lemma vcg_sp_length E de ms ms' mNew dv :
    vcg_sp E ms de = Some (ms', mNew, dv) 
    length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
327
  Proof.
Dan Frumin's avatar
Dan Frumin committed
328
329
    revert ms ms' mNew dv. induction de;
    intros ms ms' mNew dv Hsp; simplify_eq/=; eauto.
330
    - by simplify_option_eq.
Dan Frumin's avatar
Dan Frumin committed
331
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=.
332
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
333
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
334
335
336
      transitivity (length ms1).
      + by eapply IHde.
      + by eapply denv_delete_frac_2_length.
Dan Frumin's avatar
Dan Frumin committed
337
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
338
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
339
340
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
341
342
343
344
      transitivity (length ms1).
      + by eapply IHde1.
      + transitivity (length ms2). by eapply IHde2.
        by eapply denv_delete_full_2_length.
Dan Frumin's avatar
Dan Frumin committed
345
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
346
347
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
348
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
349
      transitivity (length ms1); eauto.
Dan Frumin's avatar
Dan Frumin committed
350
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
351
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
352
353
354
355
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
356
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
357
358
      transitivity (length ms1); eauto.
      transitivity (length ms2); eauto using denv_delete_full_2_length.
Dan Frumin's avatar
Dan Frumin committed
359
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
360
361
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
Dan Frumin's avatar
Dan Frumin committed
362
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
363
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
364
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
365
366
367
368
369
370
371
      destruct ms2; simplify_eq/=. transitivity (length ms1).
      + by eapply IHde1.
      + apply IHde2 in Hde2; by simplify_eq/=.
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E ms1 de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
372
      transitivity (length ms1); eauto.
Dan Frumin's avatar
Dan Frumin committed
373
374
  Qed.

375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
  Lemma vcg_eval_dexpr_correct E de dv :
    vcg_eval_dexpr de = Some dv 
    WP dexpr_interp E de {{ v, v = dval_interp E dv }}%I.
  Proof.
    generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=.
    - by iApply wp_value.
    - simplify_option_eq.
      wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1.
      iIntros (? ->).
      wp_bind (dexpr_interp E de2). iApply wp_wand; first by iApply IHde2.
      iIntros (? ->).
      by iApply wp_value.
    - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
      destruct dv'; simplify_eq/=.
      wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde.
      iIntros (? ->). simpl. by wp_proj.
    - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
      destruct dv'; simplify_eq/=.
      wp_bind (dexpr_interp E de). iApply wp_wand; first by iApply IHde.
      iIntros (? ->). simpl. by wp_proj.
  Qed.

  Lemma vcg_eval_dexpr_wf E de dv :
    vcg_eval_dexpr de = Some dv 
    dexpr_wf E de  dval_wf E dv.
  Proof.
    generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=; eauto.
    - simplify_option_eq. naive_solver.
    - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
      destruct dv'; simplify_eq/=. intros Hwfde.
      specialize (IHde (dPairV dv dv'2) eq_refl Hwfde).
      (* THIS IS UGLY AF ^ *) simpl in IHde.
      destruct_and!. auto.
    - destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
      destruct dv'; simplify_eq/=. intros Hwfde.
      specialize (IHde (dPairV dv'1 dv) eq_refl Hwfde).
      (* THIS IS UGLY AF ^ *) simpl in IHde.
      destruct_and!. auto.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
415
416
417
  Lemma vcg_sp_correct' E de ms ms' mNew dv R :
    vcg_sp E ms de = Some (ms', mNew, dv) 
    (denv_stack_interp ms ms' E
418
419
       (awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
420
  Proof.
Dan Frumin's avatar
Dan Frumin committed
421
422
    revert ms ms' mNew dv. induction de;
    iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
423
424
425
426
    - simplify_option_eq.
      iApply denv_stack_interp_intro.
      iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
      iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
Dan Frumin's avatar
Dan Frumin committed
427
428
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
429
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
430
431
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde as "Hawp"; first done.
432
      iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
433
434
435
      iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
      iClear "Hawp Hm".
      iApply (denv_stack_interp_mono with "Hawp'").
Dan Frumin's avatar
Dan Frumin committed
436
      iIntros "[Hawp Hm]".
Léon Gondelman's avatar
Léon Gondelman committed
437
438
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
439
      iIntros (?) "[% HmNew1]". simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
440
441
      iExists _, _. iSplit; eauto.
      iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
Dan Frumin's avatar
Dan Frumin committed
442
      iIntros "Hl". iSplit; eauto.
443
444
      rewrite -denv_insert_interp. by iFrame.
      - specialize (IHde1 ms).
Dan Frumin's avatar
Dan Frumin committed
445
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
446
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
447
448
449
450
451
452
453
454
455
456
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv3] |] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iPoseProof denv_delete_full_2_interp as "Hl"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
      iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
      iClear "Hawp1 Hawp2 Hl Hawp'".
Dan Frumin's avatar
Dan Frumin committed
457
458
459
460
461
      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.
Dan Frumin's avatar
Dan Frumin committed
462
463
464
      iCombine "HmNew1 HmNew2" as "HmNew".
      rewrite denv_merge_interp -denv_insert_interp.
      iDestruct ("Hl" with "HmNew") as "[HmNew3 $]".
Dan Frumin's avatar
Dan Frumin committed
465
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
466
467
468
469
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
470
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
471
472
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
473
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
474
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
475
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
476
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
477
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
478
      iExists (dval_interp E dv). repeat iSplit; eauto.
479
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
480
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
481
482
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
483
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
484
485
486
487
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=.
488
      destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
489
490
491
492
493
494
495
496
497
498
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iPoseProof denv_delete_full_2_interp as "Hl"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
      iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
      iClear "Hawp1 Hawp2 Hawp' Hl".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[[Hawp1 Hawp2] Hl]".
      iApply (a_pre_bin_op_spec with "Hawp1 Hawp2").
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] HR"; simplify_eq/=.
      iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp.
499
      iExists (dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d).
Dan Frumin's avatar
Dan Frumin committed
500
501
      iDestruct ("Hl" with "HmNew") as "[HmNew $]".
      repeat iSplit; eauto.
502
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Dan Frumin's avatar
Dan Frumin committed
503
504
      + iIntros "Hl". iFrame. iSplit; first done.
        rewrite -denv_insert_interp. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
505
506
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
507
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
508
509
      iPoseProof IHde as "Hawp"; first done.
      iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
510
      iIntros "Hawp".
511
512
513
514
      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
515
516
517
518
519
520
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 (denv_unlock mNew1 :: ms1)).
      destruct (vcg_sp E _ de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
521
      unfold popstack in Hsp.
Dan Frumin's avatar
Dan Frumin committed
522
      destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
523
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
524
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
525
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
526
      iApply a_sequence_spec'. iNext. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
527
      iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
528
      rewrite (denv_unlock_interp E mNew1).
529
      iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
530
531
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
      rewrite -denv_merge_interp. iSplit; eauto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
532
533
534
535
536
537
538
539
540
541
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
      iClear "Hawp1 Hawp2".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
      iApply (awp_par with "Hawp1 Hawp2").
542
543
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
      simplify_eq/=; iSplit; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
544
      rewrite -denv_merge_interp. iFrame.
545
  Qed.
Dan Frumin's avatar
Dan Frumin committed
546

Dan Frumin's avatar
Dan Frumin committed
547
548
  Lemma vcg_sp_correct E de m ms mNew dv R :
    vcg_sp E [m] de = Some (ms, mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
549
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
550
551
552
      denv_interp E (denv_stack_merge ms) 
        awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew).
Dan Frumin's avatar
Dan Frumin committed
553
  Proof.
554
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
555
556
557
558
559
    iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert ( m', ms = [m']) as [m' ->]=>/=.
    { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
    rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
Dan Frumin's avatar
Dan Frumin committed
560
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
561

Dan Frumin's avatar
Dan Frumin committed
562
563
564
  Lemma vcg_sp'_correct E de m m' mNew dv R :
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
565
566
567
      denv_interp E m' 
        awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew).
Dan Frumin's avatar
Dan Frumin committed
568
  Proof.
Dan Frumin's avatar
Dan Frumin committed
569
570
571
572
573
574
575
576
    rewrite /vcg_sp'.
    iIntros (Hsp') "Hm".
    destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
    destruct ms as [|?m' ms]; simplify_eq/=.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
    rewrite vcg_sp_correct; last eassumption. simpl.
    rewrite denv_merge_nil_r. iFrame.
Dan Frumin's avatar
Dan Frumin committed
577
578
  Qed.

Dan Frumin's avatar
Dan Frumin committed
579
580
  Lemma vcg_sp_wf' E de ms ms' mNew dv :
    Forall (denv_wf E) ms 
Dan Frumin's avatar
Dan Frumin committed
581
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
582
583
    vcg_sp E ms de = Some (ms', mNew, dv) 
    Forall (denv_wf E) ms'  denv_wf E mNew  dval_wf E dv .
Dan Frumin's avatar
Dan Frumin committed
584
  Proof.
Dan Frumin's avatar
Dan Frumin committed
585
586
    revert ms ms' mNew dv. induction de;
    intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
587
588
    - simplify_option_eq. split_and?; auto; first by destruct E.
      by eapply vcg_eval_dexpr_wf.
Dan Frumin's avatar
Dan Frumin committed
589
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
590
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
591
592
      destruct (denv_delete_frac_2 i ms1 mNew1)
        as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
593
594
595
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
      eapply denv_wf_delete_frac_2 in Hout1; eauto.
      destruct Hout1 as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
596
      repeat split; eauto using denv_wf_insert.
Léon Gondelman's avatar
Léon Gondelman committed
597
598
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
599
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
600
601
602
603
      destruct (vcg_sp E ms1 de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
604
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
605
606
607
608
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      eapply denv_wf_delete_full_2 in Hout1; try eassumption.
      destruct Hout1 as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
609
610
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
611
612
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
613
614
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
615
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
616
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
617
618
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
619
      repeat split; eauto. apply denv_wf_merge; eauto.
620
      eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
621
622
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
623
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
624
625
626
627
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
628
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
629
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
630
631
632
633
634
635
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      eapply denv_wf_delete_full_2 in Hout1; try eassumption.
      destruct Hout1 as (?&?&?).
      repeat split; eauto using denv_wf_insert, denv_wf_merge.
      eapply denv_wf_insert; eauto.
636
      eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
637
      by eapply denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
638
639
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
640
      destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
641
      repeat split; eauto.
642
      eapply dun_op_eval_Some_wf; eauto.
Dan Frumin's avatar
Dan Frumin committed
643
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
644
645
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
646
      destruct ms2 as [|t ms2]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
647
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
648
649
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2.
Dan Frumin's avatar
Dan Frumin committed
650
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
651
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
652
653
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Léon Gondelman's avatar
Léon Gondelman committed
654
655
656
657
658
659
660
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      repeat split; eauto. apply denv_wf_merge; eauto.
661
  Qed.
Dan Frumin's avatar
Dan Frumin committed
662

Dan Frumin's avatar
Dan Frumin committed
663
  Lemma vcg_sp'_wf E de m m' mNew dv :
664
665
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
666
667
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_wf E m'  denv_wf E mNew  dval_wf E dv .
Dan Frumin's avatar
Dan Frumin committed
668
  Proof.
Dan Frumin's avatar
Dan Frumin committed
669
670
671
672
673
674
675
676
    rewrite /vcg_sp'. intros Hm Hde Hsp'.
    assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto).
    destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
    destruct ms as [|?m' ms]; simplify_eq/=.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
    destruct (vcg_sp_wf' E de [m] [m'] mNew _ Hms Hde Hsp) as (Hm'&?&?).
    repeat split; eauto. by inversion Hm'.
Dan Frumin's avatar
Dan Frumin committed
677
  Qed.
678

Robbert Krebbers's avatar
Robbert Krebbers committed
679
  Lemma vcg_wp_awp_continuation_correct R E m de Φ :
680
    denv_wf E m 
681
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
682
683
    vcg_wp_awp_continuation R E de m Φ -
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
684
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
685
    rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec.
686
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
687
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
688
    iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
689
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
690
691
  Qed.

692
  Lemma vcg_wp_load_correct E m dv Φ :
693
    denv_wf E m 
694
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
695
    vcg_wp_load E dv m Φ -
696
697
     (cl : cloc) q w, dval_interp E dv = cloc_to_val cl 
       cl C{q} w  (cl C{q} w - vcg_wp_continuation E Φ w).
698
699
700
  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
701
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
Léon Gondelman's avatar
Léon Gondelman committed
702
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ".
703
704
        apply is_dloc_Some in Hdloc. simplify_eq/=.
        iExists (dloc_interp E (dLoc i 0)), q,  (dval_interp E dv');
705
706
707
          iSplit; first done. iFrame.  iIntros "Hl".
        iExists E, dv', m; repeat (iSplit; first done). iFrame.
        rewrite Hm0.  eapply denv_lookup_wf in Hlkp; eauto with iFrame.
708
709
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
710
711
        iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_Some in Hdloc. subst.
        iExists (dloc_interp E (dLoc i 0)), q, v'; iSplit; first done. iFrame.
712
713
714
715
    + rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
      iSpecialize ("Hwp" with "Hm"); simpl.
      iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
      iExists l, q, v'. iSplit; first done. iFrame.
716
717
  Qed.

718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
  Lemma vcg_wp_un_op_correct E m dv b Φ :
    dval_wf E dv 
    denv_wf E m 
    denv_interp E m -
    vcg_wp_un_op E b dv m Φ -
     w : val,
      un_op_eval b (dval_interp E dv) = Some w 
      vcg_wp_continuation E Φ w.
  Proof.
    iIntros (Hwf Hwf2) "Hm Hwp". rewrite /vcg_wp_un_op.
    destruct (dun_op_eval E b dv) as [dw|] eqn:Hbin.
    * iExists (dval_interp E dw); iSplit.
      { iPureIntro. apply dun_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, m.
      apply dun_op_eval_Some_wf in Hbin; try done. eauto with iFrame.
    * rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
  Qed.

737
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
738
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
739
740
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
741
    vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -
742
    denv_interp E mOut -
Léon Gondelman's avatar
Léon Gondelman committed
743
744
745
     w : val,
      cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
      vcg_wp_continuation E Φ w.
746
  Proof.
747
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
748
    destruct (dcbin_op_eval E b dv1 dv2) as [dw|] eqn:Hbin.
749
    * iExists (dval_interp E dw); iSplit.
750
      { iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. }
751
      iExists E, dw, (denv_merge mOut m).
752
      apply dcbin_op_eval_Some_wf in Hbin; try done.
753
      rewrite -denv_merge_interp //. eauto with iFrame.
754
755
756
    * iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
      rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
757
  Qed.
758

Dan Frumin's avatar
Dan Frumin committed
759
760
761
762
763
  Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ :
    denv_wf E m 
    dval_wf E dv2 
    denv_interp E m -
    vcg_wp_pre_bin_op E op dv1 dv2 m Φ -
Dan Frumin's avatar
Dan Frumin committed
764
     l v w, l C v  dval_interp E dv1 = cloc_to_val l 
765
      cbin_op_eval op v (dval_interp E dv2) = Some w 
766
      (l C[LLvl] w - vcg_wp_continuation E Φ v).
Dan Frumin's avatar
Dan Frumin committed
767
768
769
770
771
772
  Proof.
    iIntros (? ?) "Hm Hwp". rewrite /vcg_wp_pre_bin_op.
    destruct (is_dloc E dv1) as [i|] eqn:Hloc; last first.
    { rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (l v w) "(%&Hl&%&Hwp)".
      iExists l,v,w. iFrame. eauto. }
773
    apply is_dloc_Some in Hloc. simplify_eq/=.