vcgen.v 57.5 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 Σ}.

Dan Frumin's avatar
Dan Frumin committed
10
11
  (** `mapsto_wand_list E [l1:=v1,l2:=v2,...ln:=vn] Φ`
       = `l1 ↦C v1 -∗ l2 ↦C v2 -∗ ... -∗ ln ↦C vn -∗ Φ` *)
Léon Gondelman's avatar
Léon Gondelman committed
12
13
  Fixpoint mapsto_wand_list_aux
       (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
14
    match m with
15
    | [] => Φ
Léon Gondelman's avatar
Léon Gondelman committed
16
    | None :: m' => mapsto_wand_list_aux E m' Φ (S i)
17
    | Some (DenvItem x q dv) :: m' =>
18
      dloc_interp E (dLoc i 0) C[x]{q} dval_interp E dv -
Léon Gondelman's avatar
Léon Gondelman committed
19
        mapsto_wand_list_aux E m' Φ (S i)
Léon Gondelman's avatar
Léon Gondelman committed
20
    end%I.
21

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

27
28
  Definition popstack (ms : list denv) : option (list denv * denv) :=
    match ms with
Dan Frumin's avatar
Dan Frumin committed
29
    | [] => None
30
    | m :: ms => Some (ms, m)
Dan Frumin's avatar
Dan Frumin committed
31
    end.
32
33
  Global Arguments popstack !_ /.

Dan Frumin's avatar
Dan Frumin committed
34
  (** Evaluation of simple expressions *)
35
36
37
  Fixpoint vcg_eval_dexpr (de : dexpr) : option dval :=
    match de with
    | dEVal dv    => Some dv
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
38
    | dEVar x     => None
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
    | 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
57

Léon Gondelman 's avatar
Léon Gondelman committed
58
  (** substitution *)
59
60
  Fixpoint de_subst
    (E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
Léon Gondelman 's avatar
Léon Gondelman committed
61
62
63
    match de with
    | dEVal _ => de
    | dEVar y  =>  if decide (x = y) then dEVal dv else de
64
65
66
    | dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
    | dEFst de1 => dEFst (de_subst E x dv de1)
    | dESnd de1 => dESnd (de_subst E x dv de1)
67
68
69
70
71
    | dEUnknown we =>
      dEUnknown (W.subst x
                         (W.Val (dval_interp E dv)
                                (of_val (dval_interp E dv))
                                (to_of_val _ )) we)
Léon Gondelman 's avatar
Léon Gondelman committed
72
73
74
  end.


75
76
  Fixpoint dce_subst (E: known_locs)
           (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
Léon Gondelman 's avatar
Léon Gondelman committed
77
    match dce with
78
    | dCRet de1 => dCRet (de_subst E x dv de1)
Léon Gondelman 's avatar
Léon Gondelman committed
79
80
    | dCBind y de1 de2 =>
      if decide (x = y)
81
82
83
84
85
      then dCBind y (dce_subst E x dv de1) de2
      else dCBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
    | dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
    | dCLoad de1 =>  dCLoad (dce_subst E x dv de1)
    | dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
Léon Gondelman 's avatar
Léon Gondelman committed
86
    | dCBinOp op de1 de2 =>
87
      dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
Léon Gondelman 's avatar
Léon Gondelman committed
88
    | dCPreBinOp op de1 de2 =>
89
90
91
92
93
      dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
    | dCUnOp op de1 =>  dCUnOp op (dce_subst E x dv de1)
    | dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
    | dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
    | dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
94
95
96
    | dCUnknown we => dCUnknown (W.subst x (W.Val (dval_interp E dv)
                                (of_val (dval_interp E dv))
                                (to_of_val _ )) we)
Léon Gondelman 's avatar
Léon Gondelman committed
97
98
99
    end.


Dan Frumin's avatar
Dan Frumin committed
100
101
102
  (** Computes the framing for the resources, necessary for the safety of the
      expression, and simulatenously computes the strongest postcondition based on that.
      See `vcg_sp_correct` and `vcg_sp'_correct`. *)
Léon Gondelman 's avatar
Léon Gondelman committed
103
104
105
106
107
108
109
  Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr) (n: nat)
       { struct n }: option (list denv * denv * dval) :=
    match de, n with
    | dCRet de, _ => dv  vcg_eval_dexpr de; Some (ms, [], dv)
    | dCBind x de1 de2, S p =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1 p;
         ''(ms2, mNew2, dv2) 
110
           vcg_sp E (mNew1 :: ms1) (dce_subst E x dv1 de2) p;
Léon Gondelman 's avatar
Léon Gondelman committed
111
112
113
114
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
    | dCLoad de1, S p  =>
       ''(ms1, mNew, dl)      vcg_sp E ms de1 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
117
       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)
Léon Gondelman 's avatar
Léon Gondelman committed
118
119
    | dCStore de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
120
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
121
       ''(ms2, mNew2, dv)  vcg_sp E ms1 de2 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
       ''(ms3, mNew3, _)   denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
       Some (ms3, denv_insert i LLvl 1 dv mNew3, dv)
Léon Gondelman 's avatar
Léon Gondelman committed
124
125
126
    | dCBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1 p;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
127
128
       dv  dcbin_op_eval E op dv1 dv2;
       Some (ms2, denv_merge mNew1 mNew2, dv)
Léon Gondelman 's avatar
Léon Gondelman committed
129
130
    | dCPreBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Dan Frumin's avatar
Dan Frumin committed
131
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
132
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
Dan Frumin's avatar
Dan Frumin committed
133
       ''(ms3, mNew3, dv)  denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
134
135
       dv3  dcbin_op_eval E op dv dv2;
       Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
Léon Gondelman 's avatar
Léon Gondelman committed
136
137
    | dCUnOp op de, S p =>
       ''(ms1, mNew1, dv)  vcg_sp E ms de p ;
138
139
       dv'  dun_op_eval E op dv;
       Some (ms1, mNew1, dv')
Léon Gondelman 's avatar
Léon Gondelman committed
140
141
142
    | dCSeq de1 de2, S p =>
       ''(ms1, mNew1, _)    vcg_sp E ms de1 p;
       ''(ms2, mNew2, dv2)  vcg_sp E (denv_unlock mNew1 :: ms1) de2 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
Léon Gondelman 's avatar
Léon Gondelman committed
145
146
147
    | dCPar de1 de2, S p =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1 p;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
Léon Gondelman's avatar
Léon Gondelman committed
148
         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
Léon Gondelman 's avatar
Léon Gondelman committed
149
150
    | dCAlloc _ _, _ |  dCUnknown _, _ | dCInvoke _ _, _ => None
    | _, O => None
151
152
    end.

Léon Gondelman's avatar
Léon Gondelman committed
153
154
  Definition vcg_sp'
       (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Léon Gondelman 's avatar
Léon Gondelman committed
155
156
    ''(ms,mNew,dv)  vcg_sp E [m] de 1024
    (*TODO: add some better measure than a constant :) *);
Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
    ''(_, m')  popstack ms;
    Some (m', mNew, dv).
159
  Global Arguments vcg_sp' _ _ !_ /.
Léon Gondelman's avatar
Léon Gondelman committed
160

Robbert Krebbers's avatar
Robbert Krebbers committed
161
  Definition vcg_wp_continuation (E: known_locs)
162
163
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
164
165
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
166
         denv_wf E' m' 
167
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
168
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
169
        Φ E' m' dv)%I.
170

Léon Gondelman's avatar
Léon Gondelman committed
171
172
  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
173
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
174

175
176
  Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
177
    mapsto_wand_list E m ( n : nat,
178
179
180
       dval_interp E dv1 = #n  
       l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I.

181
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
182
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
183
184
185
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
186
       | Some (_, dw) => Φ E m dw
187
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
188
         mapsto_wand_list E m ( q v,
189
190
           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
191
           vcg_wp_continuation E Φ v))
192
       end
193
194
195
196
    | 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
197
    end%I.
198
199

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
200
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
201
202
203
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
204
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
205
       | None =>
206
          mapsto_wand_list E m ( v : val,
207
208
            dloc_interp E (dLoc i 0) C v 
            (dloc_interp E (dLoc i 0) C[LLvl] dval_interp E dv2 -
209
             vcg_wp_continuation E Φ (dval_interp E dv2)))
210
       end
211
    | None =>
212
213
214
215
       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
216
          vcg_wp_continuation E Φ (dval_interp E dv2)))%I
Léon Gondelman's avatar
Léon Gondelman committed
217
    end%I.
218

219
220
  (* 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
221
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
222
    match dcbin_op_eval E op dv1 dv2 with
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
    | 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
238
    end%I.
239

240
  Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
Dan Frumin's avatar
Dan Frumin committed
241
242
243
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match is_dloc E dv1 with
    | Some i =>
244
245
246
      match denv_delete_full i m with
      | Some (m', dw) =>
        match dcbin_op_eval E op dw dv2 with
247
248
249
250
        | 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' 
251
             (dloc_interp E (dLoc i 0) C[LLvl] w' - vcg_wp_continuation E Φ (dval_interp E dw))
252
        end
253
254
      | None =>
         mapsto_wand_list E m ( v w : val,
255
           dloc_interp E (dLoc i 0) C v 
256
            cbin_op_eval op v (dval_interp E dv2) = Some w  
257
           (dloc_interp E (dLoc i 0) C[LLvl] w - vcg_wp_continuation E Φ v))
258
      end
259
    | None =>
260
261
262
263
264
      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
265
266
    end%I.

267
    Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman 's avatar
Léon Gondelman committed
268
269
270
271
272
273
274
275
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) (n: nat) {struct n}: iProp Σ :=
    match de, n with
    | dCRet de', _ =>
      match vcg_eval_dexpr de' with
      | Some dv => Φ E m dv
      | None => vcg_wp_awp_continuation R E de m Φ
      end
    | dCBind x de1 de2, S p =>
276
      vcg_wp E m de1 R (λ E m' dv1,
277
        vcg_wp E m' (dce_subst E x dv1 de2) R Φ p) p
Léon Gondelman 's avatar
Léon Gondelman committed
278
    | dCAlloc de1 de2, S p =>
279
280
281
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Léon Gondelman 's avatar
Léon Gondelman committed
282
            vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p
283
284
285
286
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Léon Gondelman 's avatar
Léon Gondelman committed
287
               vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)  p
288
289
290
          | None => vcg_wp_awp_continuation R E de m Φ
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
291
292
293
    | dCLoad de1, S p =>
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ) p
    | dCStore de1 de2, S p =>
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
296
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Léon Gondelman 's avatar
Léon Gondelman committed
297
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
298
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
301
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Léon Gondelman 's avatar
Léon Gondelman committed
302
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
303
          | None => vcg_wp_awp_continuation R E de m Φ
304
305
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
306
    | dCBinOp op de1 de2, S p =>
Robbert Krebbers's avatar
Robbert Krebbers committed
307
308
309
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Léon Gondelman 's avatar
Léon Gondelman committed
310
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
311
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
312
313
314
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Léon Gondelman 's avatar
Léon Gondelman committed
315
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
316
          | None => vcg_wp_awp_continuation R E de m Φ
317
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
318
       end
Léon Gondelman 's avatar
Léon Gondelman committed
319
    | dCPreBinOp op de1 de2, S p =>
Dan Frumin's avatar
Dan Frumin committed
320
321
322
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Léon Gondelman 's avatar
Léon Gondelman committed
323
            vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
324
325
326
327
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Léon Gondelman 's avatar
Léon Gondelman committed
328
               vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
329
330
331
          | None => vcg_wp_awp_continuation R E de m Φ
          end
       end
Léon Gondelman 's avatar
Léon Gondelman committed
332
333
    | dCUnOp op de, S p => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ) p
    | dCSeq de1 de2, S p =>
Robbert Krebbers's avatar
Robbert Krebbers committed
334
       vcg_wp E m de1 R (λ E m _,
Léon Gondelman 's avatar
Léon Gondelman committed
335
336
         U (vcg_wp E (denv_unlock m) de2 R Φ  p)) p
    | dCPar de1 de2, S p =>
Léon Gondelman's avatar
Léon Gondelman committed
337
338
339
      match vcg_sp' E m de1 with
      | Some (m', mNew, dv1) =>
        vcg_wp E m' de2 R (λ E m'' dv2,
Léon Gondelman 's avatar
Léon Gondelman committed
340
          (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
341
342
343
344
      | None =>
        match vcg_sp' E m de2 with
        | Some (m', mNew, dv2) =>
          vcg_wp E m' de1 R (λ E m'' dv1,
Léon Gondelman 's avatar
Léon Gondelman committed
345
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
346
347
348
        | None => vcg_wp_awp_continuation R E de m Φ
        end
      end
Léon Gondelman 's avatar
Léon Gondelman committed
349
    | dCInvoke ef de1, S p => vcg_wp E m de1 R (λ E m dv,
350
        vcg_wp_awp_continuation R E
351
           (dCUnknown (W.ClosedExpr (ef (dval_interp E dv)))) m Φ) p
Léon Gondelman 's avatar
Léon Gondelman committed
352
353
    | _, S p => vcg_wp_awp_continuation R E de m Φ
    | _, O => False
Léon Gondelman's avatar
Léon Gondelman committed
354
    end%I.
355
356
357
358
359
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman 's avatar
Léon Gondelman committed
360
361
362
363
  Arguments subst _ _ !_ /.

  Lemma de_subst_subst_comm E x de dv :
    (dexpr_interp E (de_subst E x dv de)) =
364
    subst x (dval_interp E dv) (dexpr_interp E de).
Léon Gondelman 's avatar
Léon Gondelman committed
365
  Proof.
366
367
368
369
370
371
372
373
374
375
    induction de; simplify_eq /=.
    - by simpl_subst.
    - by destruct (decide (x = s)).
    - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                  end; by simpl_subst).
    - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                  end; by simpl_subst).
    - try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                  end; by simpl_subst).
    - by rewrite! W.to_expr_subst.
Léon Gondelman 's avatar
Léon Gondelman committed
376
377
  Qed.

Léon Gondelman 's avatar
wip    
Léon Gondelman committed
378
379
  Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
    dcexpr_interp E (dce_subst E x dv de) =
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
380
    (subst x (dval_interp E dv) (dcexpr_interp E de))%E.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
381
  Proof.
Léon Gondelman 's avatar
Léon Gondelman committed
382
383
384
385
386
387
388
389
390
    induction de; simplify_eq /=; simpl_subst;
      try (repeat match goal with | [ H: _ = subst _ _ _ |- _  ] => rewrite H
                  end; by simpl_subst).
    - by rewrite de_subst_subst_comm.
    - destruct (decide (x = s)); simplify_eq /=; rewrite IHde1.
      + rewrite decide_False; naive_solver.
      + rewrite IHde2 decide_True; naive_solver.
  Qed.

391
392
393
394
395
396
  Lemma dce_subst_dcexpr_wf E s dv1 de2 :
    dval_wf E dv1 
    dcexpr_wf [s] E de2 
    dcexpr_wf [] E (dce_subst E s dv1 de2).
  Proof. Admitted.

Léon Gondelman 's avatar
Léon Gondelman committed
397
  Arguments subst : simpl never.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
398

Robbert Krebbers's avatar
Robbert Krebbers committed
399
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
Léon Gondelman's avatar
Léon Gondelman committed
400
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
401
    ([ list] ndio  m, from_option
402
403
     (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
      dloc_interp E (dLoc (k + n) 0) C[lv]{q} dval_interp E dv) True dio) - Φ.
Dan Frumin's avatar
Dan Frumin committed
404
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
405
406
    iIntros "H".
    iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
407
408
    - 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
409
410
411
412
413
414
      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
415
416
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
417
418
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
419
  Proof.
Dan Frumin's avatar
Dan Frumin committed
420
421
422
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
423

Léon Gondelman 's avatar
Léon Gondelman committed
424
425
  Lemma vcg_sp_length E de ms ms' mNew dv n:
    vcg_sp E ms de n = Some (ms', mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
426
    length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
427
  Proof.
428
429
430
431
432
433
434
    revert ms ms' mNew dv de.
    induction n.
    (*Base case*)
    - intros ms ms' mNew dv de Hsp.
      destruct de; by simplify_option_eq.
    (*Induction case*)
    - intros ms ms' mNew dv de Hsp;
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
435
      destruct (vcg_sp E ms de (S n)) as [[[ms1 mNew1] dv1]|] eqn:Hout.
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
      destruct de; simplify_eq /=; try by simplify_option_eq.
      + (*bind case*)
        destruct (vcg_sp E ms de1 n)
          as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
        destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n)
          as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
        destruct ms2; simplify_eq/=. transitivity (length ms1).
        * by eapply IHn.
        * apply IHn in Hde2; by simplify_eq/=.
      + destruct (vcg_sp E ms de n)
          as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
        destruct (is_dloc _ _)
          as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
        destruct (denv_delete_frac_2 i ms1 mNew1)
          as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
        transitivity (length ms1).
        * by eapply IHn.
        * by eapply denv_delete_frac_2_length.
      + destruct (vcg_sp E ms de1)
          as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
        destruct (is_dloc _ _)
          as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
        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/=.
        transitivity (length ms1).
        * by eapply IHn.
        * transitivity (length ms2). by eapply IHn.
            by eapply denv_delete_full_2_length.
    + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
467
468
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
469
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
470
      transitivity (length ms1); eauto.
471
    + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
472
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
473
474
475
476
      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/=.
477
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
478
479
      transitivity (length ms1); eauto.
      transitivity (length ms2); eauto using denv_delete_full_2_length.
480
    + destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
481
      destruct (dun_op_eval E u dv1); simplify_eq/=.
482
483
      by eapply IHn.
    + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
484
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
485
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
486
      destruct ms2; simplify_eq/=. transitivity (length ms1).
487
488
489
      * by eapply IHn.
      * apply IHn in Hde2; by simplify_eq/=.
    + destruct (vcg_sp E ms de1)
490
491
492
        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
493
      transitivity (length ms1); eauto.
494
495
    + done.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
496

497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
  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 
Léon Gondelman 's avatar
Léon Gondelman committed
521
    dexpr_wf [] E de  dval_wf E dv.
522
523
524
525
526
527
528
529
530
531
532
533
534
535
  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.
Léon Gondelman 's avatar
Léon Gondelman committed
536

537
538
539
540
541
  Lemma vcg_sp_dval_wf E de ms ms' mNew dv n :
    vcg_sp E ms de n = Some (ms', mNew, dv) 
    dval_wf E dv.
  Proof. Admitted.

Léon Gondelman 's avatar
Léon Gondelman committed
542
543
  Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
    vcg_sp E ms de n = Some (ms', mNew, dv) 
544
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
545
    (denv_stack_interp ms ms' E
546
547
       (awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
548
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
549
    revert de ms ms' mNew dv. induction n as [|n IH].
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
550
    (* Base Case *)
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
551
    { iIntros (de ms ms' mNew dv Hsp Hwf); simplify_eq/=.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
552
      destruct de; simplify_option_eq.
553
554
      iApply denv_stack_interp_intro.
      iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
555
556
      iIntros (? ->). iSplit; eauto. rewrite /denv_interp //. }
    { iIntros (de ms ms' mNew dv Hsp Hwf).
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
557
      destruct de; simplify_option_eq.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
558
      - iApply denv_stack_interp_intro; iApply awp_ret;
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
559
560
          iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
        iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
561
      - destruct (vcg_sp E ms de1 n)
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
562
563
564
565
566
          as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
        destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n)
          as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
        unfold popstack in Hsp.
        destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
567
568
569
        apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
        iPoseProof (IH de1 ms) as "Hawp1"; first done. done.
        iPoseProof (IH (dce_subst E s dv1 de2) (mNew1 :: ms1))
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
570
          as "Hawp2"; first done.
571
        apply dce_subst_dcexpr_wf. eapply vcg_sp_dval_wf. eassumption. done.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
572
573
574
        iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
        iClear "Hawp1 Hawp2".
        iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
575
576
        assert (Closed ( [s]) (dcexpr_interp E de2)).
        { apply dcexpr_closed. apply Hwf2. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
577
        iApply awp_bind.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
578
        * exists (λ: s, dcexpr_interp E de2)%V. by unlock.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
579
        * iApply (awp_wand with "Hawp1").
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
580
581
582
583
584
585
          iIntros (v) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
          iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
          awp_let.
          rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2").
          iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto.
          rewrite- denv_merge_interp. iFrame.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
586
      - destruct (vcg_sp E ms de n)
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
587
588
589
590
591
          as [[[ms1 mNew1] dv1]|] eqn:Hsp'; simplify_eq /=.
        destruct (is_dloc _ _)
          as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
        destruct (denv_delete_frac_2 i ms1 mNew1)
          as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
592
593
        specialize (IH de ms).
        iPoseProof IH as "Hawp"; first done. done.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
594
595
596
597
598
599
600
601
602
603
604
605
        iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
        iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
        iClear "Hawp Hm".
        iApply (denv_stack_interp_mono with "Hawp'").
        iIntros "[Hawp Hm]".
        iApply a_load_spec.
        iApply (awp_wand with "Hawp").
        iIntros (?) "[% HmNew1]". simplify_eq/=.
        iExists _, _. iSplit; eauto.
        iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
        iIntros "Hl". iSplit; eauto.
        rewrite -denv_insert_interp. by iFrame.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
      - destruct (vcg_sp E ms de1)
          as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
        destruct (is_dloc _ _)
          as [i|] eqn:Hdl;
          try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
        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] dv3] |] eqn:Hfar; simplify_eq/=.
        iPoseProof (IH de1) as "Hawp1"; destruct_and!; try done.
        iPoseProof (IH de2) as "Hawp2"; try 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'".
        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.
        iCombine "HmNew1 HmNew2" as "HmNew".
        rewrite denv_merge_interp -denv_insert_interp.
        iDestruct ("Hl" with "HmNew") as "[HmNew3 $]".
        iIntros "Hl". by iFrame.
      - 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 /=.
        destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe;
          simplify_eq/=; destruct_and!.
        iPoseProof (IH de1 ms) as "Hawp1"; try done.
        iPoseProof (IH de2 ms1) as "Hawp2"; try 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 (a_bin_op_spec with "Hawp1 Hawp2").
        iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
        iExists (dval_interp E dv). repeat iSplit; eauto.
        + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
        + rewrite -denv_merge_interp. iFrame.
      - destruct (vcg_sp E ms de1)
          as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
        destruct (is_dloc _ _)
          as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
        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] dv'] |] eqn:Hfar; simplify_eq/=.
        destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe;
          simplify_eq/=; destruct_and!.
        iPoseProof (IH de1 ms) as "Hawp1"; try done.
        iPoseProof (IH de2 ms1) as "Hawp2"; try 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.
        iExists
          (dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d).
        iDestruct ("Hl" with "HmNew") as "[HmNew $]".
        repeat iSplit; eauto.
        + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
        + iIntros "Hl". iFrame. iSplit; first done.
          rewrite -denv_insert_interp. by iFrame.
      - destruct (vcg_sp E ms de)
          as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
        remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
        iPoseProof (IH de ms) as "Hawp"; try done.
        iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
        iIntros "Hawp".
        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.
      - destruct (vcg_sp E ms de1)
          as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
        destruct (vcg_sp E _ de2)
          as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=; destruct_and!.
        iPoseProof (IH de1 ms) as "Hawp1"; try done.
        iPoseProof (IH de2 (denv_unlock mNew1 :: ms1)) as "Hawp2"; try done.
        unfold popstack in Hsp.
        destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
        iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
        iClear "Hawp1 Hawp2".
        iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
        iApply a_sequence_spec'.
        { by apply dcexpr_closed. }
        iNext. iApply (awp_wand with "Hawp1").
        iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
        rewrite (denv_unlock_interp E mNew1).
        iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
        iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
        rewrite -denv_merge_interp. iSplit; eauto with iFrame.
      - 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 /=; destruct_and!.
        iPoseProof (IH de1) as "Hawp1"; try done.
        iPoseProof (IH de2) as "Hawp2"; try 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").
        iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
                 simplify_eq/=; iSplit; eauto.
        rewrite -denv_merge_interp. iFrame. }
  Qed.
Dan Frumin's avatar
Dan Frumin committed
717

Léon Gondelman 's avatar
Léon Gondelman committed
718
719
  Lemma vcg_sp_correct E de m ms mNew dv R n:
    vcg_sp E [m] de n = Some (ms, mNew, dv) 
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
720
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
721
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
722
723
724
      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
725
  Proof.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
726
    iIntros (Hsp Hwf) "Hm".
Dan Frumin's avatar
Dan Frumin committed
727
    iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
728
    pose (vcg_sp_length  _ _ _ _ _ _ _ Hsp) as Hlen.
Dan Frumin's avatar
Dan Frumin committed
729
730
    assert ( m', ms = [m']) as [m' ->]=>/=.
    { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
731
732
733
734
    { done. }
  Admitted.
    (* rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
  Qed.*)
Léon Gondelman's avatar
Léon Gondelman committed
735

Dan Frumin's avatar
Dan Frumin committed
736
737
  Lemma vcg_sp'_correct E de m m' mNew dv R :
    vcg_sp' E m de = Some (m', mNew, dv) 
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
738
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
739
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
740
741
742
      denv_interp E m' 
        awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew).
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
743
744
745
746
747
748
749
750
751
752
  Proof.
    rewrite /vcg_sp'.
    iIntros (Hsp' Hwf) "Hm".
    destruct (vcg_sp E [m] de 1024) 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); simplify_eq.
    rewrite vcg_sp_correct; last eassumption; simplify_eq; last done. simpl.
    rewrite denv_merge_nil_r.  iFrame. eauto 422 with iFrame. simplify_option_eq.
  Admitted.
Dan Frumin's avatar
Dan Frumin committed
753

Léon Gondelman 's avatar
Léon Gondelman committed
754
  Lemma vcg_sp_wf' E de ms ms' mNew dv n:
Dan Frumin's avatar
Dan Frumin committed
755
    Forall (denv_wf E) ms 
Léon Gondelman 's avatar
Léon Gondelman committed
756
757
    dcexpr_wf E de 
    vcg_sp E ms de n = Some (ms', mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
758
    Forall (denv_wf E) ms'  denv_wf E mNew  dval_wf E dv .
Léon Gondelman 's avatar
Léon Gondelman committed
759
760
  Proof. Admitted.
(*    revert ms ms' mNew dv. induction de;
Dan Frumin's avatar
Dan Frumin committed
761
    intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
762
763
    - simplify_option_eq. split_and?; auto; first by destruct E.
      by eapply vcg_eval_dexpr_wf.
Dan Frumin's avatar
Dan Frumin committed
764
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
765
      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
766
767
      destruct (denv_delete_frac_2 i ms1 mNew1)
        as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
768
769
770
      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
771
      repeat split; eauto using denv_wf_insert.
Léon Gondelman's avatar
Léon Gondelman committed
772
773
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
774
      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
775
776
777
778
      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
779
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
780
781
782
783
      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
784
785
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
786
787
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
788
789
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
790
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
791
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
792
793
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
794
      repeat split; eauto. apply denv_wf_merge; eauto.
795
      eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
796
797
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
798
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
799
800
801
802
      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
803
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
804
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
805
806
807
808
809
810
      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.
811
      eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
812
      by eapply denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
813
814
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
815
      destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
816
      repeat split; eauto.
817
      eapply dun_op_eval_Some_wf; eauto.
Dan Frumin's avatar
Dan Frumin committed
818
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
819
820
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
821
      destruct ms2 as [|t ms2]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
822
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
823
824
      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
825
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
826
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
827
828
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Léon Gondelman's avatar
Léon Gondelman committed
829
830
831
832
833
834
835
    - 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.
Léon Gondelman 's avatar
Léon Gondelman committed
836
  Qed. *)
Dan Frumin's avatar
Dan Frumin committed
837

Dan Frumin's avatar
Dan Frumin committed
838
  Lemma vcg_sp'_wf E de m m' mNew dv :
839
    denv_wf E m 
Léon Gondelman 's avatar
Léon Gondelman committed
840
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
841
842
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_wf E m'  denv_wf E mNew  dval_wf E dv .
Léon Gondelman 's avatar
Léon Gondelman committed
843
844
  Proof. Admitted.
(*    rewrite /vcg_sp'. intros Hm Hde Hsp'.
Dan Frumin's avatar
Dan Frumin committed
845
846
847
848
849
850
851
    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'.
Léon Gondelman 's avatar
Léon Gondelman committed
852
  Qed. *)
853

Robbert Krebbers's avatar
Robbert Krebbers committed
854
  Lemma vcg_wp_awp_continuation_correct R E m de Φ :
855
    denv_wf E m 
856
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
857
858
    vcg_wp_awp_continuation R E de m Φ -
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
859
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
860
    rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec.
861
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
862
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
863
    iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
864
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
865
866
  Qed.

867
  Lemma vcg_wp_load_correct E m dv Φ :