vcgen.v 58.1 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

Dan Frumin's avatar
Dan Frumin committed
58
59
60
  (** 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
61
62
63
64
65
66
67
  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) 
68
           vcg_sp E (mNew1 :: ms1) (dce_subst E x dv1 de2) p;
Léon Gondelman 's avatar
Léon Gondelman committed
69
70
71
72
       ''(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
73
74
75
       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
76
77
    | dCStore de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
78
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
79
       ''(ms2, mNew2, dv)  vcg_sp E ms1 de2 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
       ''(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
82
83
84
    | dCBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1 p;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
85
86
       dv  dcbin_op_eval E op dv1 dv2;
       Some (ms2, denv_merge mNew1 mNew2, dv)
Léon Gondelman 's avatar
Léon Gondelman committed
87
88
    | dCPreBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Dan Frumin's avatar
Dan Frumin committed
89
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
90
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
Dan Frumin's avatar
Dan Frumin committed
91
       ''(ms3, mNew3, dv)  denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
92
93
       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
94
95
    | dCUnOp op de, S p =>
       ''(ms1, mNew1, dv)  vcg_sp E ms de p ;
96
97
       dv'  dun_op_eval E op dv;
       Some (ms1, mNew1, dv')
Léon Gondelman 's avatar
Léon Gondelman committed
98
99
100
    | 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
101
102
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
Léon Gondelman 's avatar
Léon Gondelman committed
103
104
105
    | 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
106
         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
Léon Gondelman 's avatar
Léon Gondelman committed
107
108
    | dCAlloc _ _, _ |  dCUnknown _, _ | dCInvoke _ _, _ => None
    | _, O => None
109
110
    end.

Léon Gondelman's avatar
Léon Gondelman committed
111
112
  Definition vcg_sp'
       (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Léon Gondelman 's avatar
Léon Gondelman committed
113
114
    ''(ms,mNew,dv)  vcg_sp E [m] de 1024
    (*TODO: add some better measure than a constant :) *);
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
    ''(_, m')  popstack ms;
    Some (m', mNew, dv).
117
  Global Arguments vcg_sp' _ _ !_ /.
Léon Gondelman's avatar
Léon Gondelman committed
118

Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Definition vcg_wp_continuation (E: known_locs)
120
121
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
122
123
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
124
         denv_wf E' m' 
125
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
126
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
127
        Φ E' m' dv)%I.
128

Léon Gondelman's avatar
Léon Gondelman committed
129
130
  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
131
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
132

133
134
  Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
135
136
137
138
139
140
141
142
143
    match dval_to_nat dv1 with
    | Some n =>
      mapsto_wand_list E m (
         l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I
    | None =>
      mapsto_wand_list E m ( n : nat,
         dval_interp E dv1 = #n  
         l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I
    end.
144

145
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
146
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
147
148
149
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
150
       | Some (_, dw) => Φ E m dw
151
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
152
         mapsto_wand_list E m ( q v,
153
154
           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
155
           vcg_wp_continuation E Φ v))
156
       end
157
158
159
160
    | 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
161
    end%I.
162
163

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
164
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
165
166
167
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
168
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
169
       | None =>
170
          mapsto_wand_list E m ( v : val,
171
172
            dloc_interp E (dLoc i 0) C v 
            (dloc_interp E (dLoc i 0) C[LLvl] dval_interp E dv2 -
173
             vcg_wp_continuation E Φ (dval_interp E dv2)))
174
       end
175
    | None =>
176
177
178
179
       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
180
          vcg_wp_continuation E Φ (dval_interp E dv2)))%I
Léon Gondelman's avatar
Léon Gondelman committed
181
    end%I.
182

183
184
  (* 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
185
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
186
    match dcbin_op_eval E op dv1 dv2 with
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
    | 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
202
    end%I.
203

204
  Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
Dan Frumin's avatar
Dan Frumin committed
205
206
207
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match is_dloc E dv1 with
    | Some i =>
208
209
210
      match denv_delete_full i m with
      | Some (m', dw) =>
        match dcbin_op_eval E op dw dv2 with
211
212
213
214
        | 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' 
215
             (dloc_interp E (dLoc i 0) C[LLvl] w' - vcg_wp_continuation E Φ (dval_interp E dw))
216
        end
217
218
      | None =>
         mapsto_wand_list E m ( v w : val,
219
           dloc_interp E (dLoc i 0) C v 
220
            cbin_op_eval op v (dval_interp E dv2) = Some w  
221
           (dloc_interp E (dLoc i 0) C[LLvl] w - vcg_wp_continuation E Φ v))
222
      end
223
    | None =>
224
225
226
227
228
      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
229
230
    end%I.

231
    Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman 's avatar
Léon Gondelman committed
232
233
234
235
236
237
238
239
      (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 =>
240
      vcg_wp E m de1 R (λ E m' dv1,
241
        vcg_wp E m' (dce_subst E x dv1 de2) R Φ p) p
Léon Gondelman 's avatar
Léon Gondelman committed
242
    | dCAlloc de1 de2, S p =>
243
244
245
       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
246
            vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p
247
248
249
250
       | 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
251
               vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)  p
252
253
254
          | None => vcg_wp_awp_continuation R E de m Φ
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
255
256
257
    | 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
258
259
260
       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
261
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
262
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
          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
266
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
267
          | None => vcg_wp_awp_continuation R E de m Φ
268
269
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
270
    | dCBinOp op de1 de2, S p =>
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
273
       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
274
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
275
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
276
277
278
          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
279
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
280
          | None => vcg_wp_awp_continuation R E de m Φ
281
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
282
       end
Léon Gondelman 's avatar
Léon Gondelman committed
283
    | dCPreBinOp op de1 de2, S p =>
Dan Frumin's avatar
Dan Frumin committed
284
285
286
       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
287
            vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
288
289
290
291
       | 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
292
               vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
293
294
295
          | None => vcg_wp_awp_continuation R E de m Φ
          end
       end
Léon Gondelman 's avatar
Léon Gondelman committed
296
297
    | 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
298
       vcg_wp E m de1 R (λ E m _,
299
         U (vcg_wp E (denv_unlock m) de2 R Φ p)) p
Léon Gondelman 's avatar
Léon Gondelman committed
300
    | dCPar de1 de2, S p =>
Léon Gondelman's avatar
Léon Gondelman committed
301
302
303
      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
304
          (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
305
306
307
308
      | 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
309
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
310
311
312
        | None => vcg_wp_awp_continuation R E de m Φ
        end
      end
Léon Gondelman 's avatar
Léon Gondelman committed
313
    | dCInvoke ef de1, S p => vcg_wp E m de1 R (λ E m dv,
314
        vcg_wp_awp_continuation R E
315
           (dCUnknown (W.ClosedExpr (ef (dval_interp E dv)))) m Φ) p
Léon Gondelman 's avatar
Léon Gondelman committed
316
317
    | _, S p => vcg_wp_awp_continuation R E de m Φ
    | _, O => False
Léon Gondelman's avatar
Léon Gondelman committed
318
    end%I.
319
320
321
322
323
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
324
325
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
326
    ([ list] ndio  m, from_option
327
328
     (λ '{| 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
329
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
330
331
    iIntros "H".
    iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
332
333
    - 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
334
335
336
337
338
339
      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
340
341
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
342
343
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
344
  Proof.
Dan Frumin's avatar
Dan Frumin committed
345
346
347
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
348

Léon Gondelman 's avatar
Léon Gondelman committed
349
350
  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
351
    length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
352
  Proof.
353
354
355
356
357
358
359
    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
360
      destruct (vcg_sp E ms de (S n)) as [[[ms1 mNew1] dv1]|] eqn:Hout.
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
      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/=.
392
393
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
394
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
395
      transitivity (length ms1); eauto.
396
    + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
397
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
398
399
400
401
      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/=.
402
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
403
404
      transitivity (length ms1); eauto.
      transitivity (length ms2); eauto using denv_delete_full_2_length.
405
    + destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
406
      destruct (dun_op_eval E u dv1); simplify_eq/=.
407
408
      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
409
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
410
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
411
      destruct ms2; simplify_eq/=. transitivity (length ms1).
412
413
414
      * by eapply IHn.
      * apply IHn in Hde2; by simplify_eq/=.
    + destruct (vcg_sp E ms de1)
415
416
417
        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
418
      transitivity (length ms1); eauto.
419
    + done.
Dan Frumin's avatar
Dan Frumin committed
420
421
  Qed.

Dan Frumin's avatar
Dan Frumin committed
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
  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.

  Lemma vcg_sp_wf' E de ms ms' mNew dv n:
    Forall (denv_wf E) ms 
    dcexpr_wf [] E de 
    vcg_sp E ms de n = Some (ms', mNew, dv) 
    Forall (denv_wf E) ms'  denv_wf E mNew  dval_wf E dv .
  Proof.
    revert de ms ms' mNew dv. induction n as [|n IH];
    intros de ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
Dan Frumin's avatar
Dan Frumin committed
449
450
451
    { destruct de; simplify_option_eq.
      repeat split_and; eauto.
      by eapply vcg_eval_dexpr_wf. }
Dan Frumin's avatar
Dan Frumin committed
452
    destruct de; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
453
454
455
    -  simplify_option_eq.
       repeat split_and; eauto.
       by eapply vcg_eval_dexpr_wf.
Dan Frumin's avatar
Dan Frumin committed
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
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
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2))
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
      destruct ms2 as [|t ms2]; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      assert (Forall (denv_wf E) (mNew1 :: ms1)) as Hwfms2.
      { apply Forall_cons. split; eauto. }
      assert (dcexpr_wf [] E (dce_subst E s dv1 de2)) as Hwfsubst.
        by apply dce_subst_dcexpr_wf.
      destruct (IH (dce_subst E s dv1 de2) _ _ _ _ Hwfms2 Hwfsubst Hsp2) as (Hall&?&?).
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
    - destruct (vcg_sp E ms de) 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 (denv_delete_frac_2 i ms1 mNew1)
        as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
      eapply denv_wf_delete_frac_2 in Hout1; eauto.
      destruct Hout1 as (?&?&?).
      repeat split; eauto using denv_wf_insert.
    - 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] dv1]|] eqn:Hout1; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      eapply denv_wf_delete_full_2 in Hout1; try eassumption.
      destruct Hout1 as (?&?&?).
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
    - 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/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      repeat split; eauto. apply denv_wf_merge; eauto.
      eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
    - 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] dv1]|] eqn:Hout1; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
      destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IH de2 _ _ _ _ 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.
      eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
      by eapply denv_wf_merge.
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IH de _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
      repeat split; eauto.
      eapply dun_op_eval_Some_wf; eauto.
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
      destruct ms2 as [|t ms2]; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      assert (Forall (denv_wf E) (denv_unlock mNew1 :: ms1)) as Hwfms2.
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
      destruct (IH de2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
    - 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 (IH de1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IH de2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
      repeat split; eauto. apply denv_wf_merge; eauto.
  Qed.

  Lemma vcg_sp'_wf E de m m' mNew dv :
    denv_wf E m 
    dcexpr_wf [] E de 
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_wf E m'  denv_wf E mNew  dval_wf E dv.
  Proof.
    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). simpl in Hsp'.
    inversion Hsp'. subst.
    destruct (vcg_sp_wf' E de [m] [m'] mNew _ _ Hms Hde Hsp) as (Hm'&?&?).
    repeat split; eauto. by inversion Hm'.
  Qed.

560
561
562
563
564
565
566
567
568
  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 de2). iApply wp_wand; first by iApply IHde2.
      iIntros (? ->).
Dan Frumin's avatar
Dan Frumin committed
569
570
      wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1.
      iIntros (? ->).
571
572
573
574
575
576
577
578
579
580
581
      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.

Léon Gondelman 's avatar
Léon Gondelman committed
582
583
  Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
    vcg_sp E ms de n = Some (ms', mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
584
    Forall (denv_wf E) ms 
585
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
586
    (denv_stack_interp ms ms' E
587
588
       (awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
589
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
590
    revert de ms ms' mNew dv. induction n as [|n IH].
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
591
    (* Base Case *)
Dan Frumin's avatar
Dan Frumin committed
592
    { iIntros (de ms ms' mNew dv Hsp Hwfms Hwf); simplify_eq/=.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
593
      destruct de; simplify_option_eq.
594
595
      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
596
      iIntros (? ->). iSplit; eauto. rewrite /denv_interp //. }
Dan Frumin's avatar
Dan Frumin committed
597
    { iIntros (de ms ms' mNew dv Hsp Hwfms Hwf).
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
598
      destruct de; simplify_option_eq.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
599
      - iApply denv_stack_interp_intro; iApply awp_ret;
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
600
601
          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
602
      - destruct (vcg_sp E ms de1 n)
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
603
604
605
606
607
          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/=.
608
        apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
609
610
611
612
613
614
615
616
617
618
619
        iPoseProof (IH de1 ms) as "Hawp1"; eauto.
        assert (Forall (denv_wf E) ms1
                 denv_wf E mNew1  dval_wf E dv1).
        { eapply vcg_sp_wf'; eauto. }
        destruct_and!.
        assert (Forall (denv_wf E) (mNew1 :: ms1)).
        { econstructor; eauto. }
        assert (Forall (denv_wf E) (t :: ms')
                 denv_wf E mNew2  dval_wf E dv).
        { eapply (vcg_sp_wf' _ (dce_subst E s dv1 de2)); eauto.
          apply dce_subst_dcexpr_wf; eauto. }
620
        iPoseProof (IH (dce_subst E s dv1 de2) (mNew1 :: ms1))
Dan Frumin's avatar
Dan Frumin committed
621
622
          as "Hawp2"; eauto.
        { apply dce_subst_dcexpr_wf; eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
623
624
625
        iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
        iClear "Hawp1 Hawp2".
        iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
626
627
        assert (Closed ( [s]) (dcexpr_interp E de2)).
        { apply dcexpr_closed. apply Hwf2. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
628
        iApply awp_bind.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
629
        * exists (λ: s, dcexpr_interp E de2)%V. by unlock.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
630
        * iApply (awp_wand with "Hawp1").
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
631
632
633
634
635
636
          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
637
      - destruct (vcg_sp E ms de n)
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
638
639
640
641
642
          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/=.
643
        specialize (IH de ms).
Dan Frumin's avatar
Dan Frumin committed
644
        iPoseProof IH as "Hawp"; eauto.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
645
646
647
648
649
650
651
652
653
654
655
        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.
Dan Frumin's avatar
Dan Frumin committed
656
        rewrite -denv_insert_interp. by iFrame.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
657
658
659
660
661
662
663
664
665
      - 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/=.
Dan Frumin's avatar
Dan Frumin committed
666
667
668
        iPoseProof (IH de1) as "Hawp1"; destruct_and!; eauto.
        iPoseProof (IH de2) as "Hawp2"; eauto.
        { eapply (vcg_sp_wf' _ de1); eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
        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!.
Dan Frumin's avatar
Dan Frumin committed
688
689
690
        iPoseProof (IH de1 ms) as "Hawp1"; eauto.
        iPoseProof (IH de2 ms1) as "Hawp2"; eauto.
        { eapply (vcg_sp_wf' _ de1); eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
        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.
Dan Frumin's avatar
Dan Frumin committed
710
711
        iPoseProof (IH de2 ms1) as "Hawp2"; eauto.
        { eapply (vcg_sp_wf' _ de1); eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
        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!.
Dan Frumin's avatar
Dan Frumin committed
742
743
744
745
        iPoseProof (IH de1 ms) as "Hawp1"; eauto.
        iPoseProof (IH de2 (denv_unlock mNew1 :: ms1)) as "Hawp2"; eauto.
        { econstructor; [eapply denv_wf_unlock |];
          eapply (vcg_sp_wf' _ de1); eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
746
747
748
749
750
751
752
        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. }
Dan Frumin's avatar
Dan Frumin committed
753
        iApply (awp_wand with "Hawp1").
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
754
755
756
757
758
759
760
761
762
763
        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.
Dan Frumin's avatar
Dan Frumin committed
764
765
        iPoseProof (IH de2) as "Hawp2"; eauto.
        { eapply (vcg_sp_wf' _ de1); eauto. }
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
766
767
768
769
770
771
772
        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. }
773
  Qed.
Dan Frumin's avatar
Dan Frumin committed
774

Léon Gondelman 's avatar
Léon Gondelman committed
775
776
  Lemma vcg_sp_correct E de m ms mNew dv R n:
    vcg_sp E [m] de n = Some (ms, mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
777
    denv_wf E m 
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
778
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
779
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
780
781
782
      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
783
  Proof.
Dan Frumin's avatar
Dan Frumin committed
784
785
    iIntros (Hsp Hwfm Hwf) "Hm".
    iPoseProof vcg_sp_correct' as "Hawp"; eauto.
786
    pose (vcg_sp_length  _ _ _ _ _ _ _ Hsp) as Hlen;
Dan Frumin's avatar
Dan Frumin committed
787
788
789
    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
790
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
791

Dan Frumin's avatar
Dan Frumin committed
792
793
  Lemma vcg_sp'_correct E de m m' mNew dv R :
    vcg_sp' E m de = Some (m', mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
794
    denv_wf E m 
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
795
    dcexpr_wf [] E de 
Dan Frumin's avatar
Dan Frumin committed
796
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
797
798
799
      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
800
  Proof.
Dan Frumin's avatar
Dan Frumin committed
801
    rewrite /vcg_sp'.
Dan Frumin's avatar
Dan Frumin committed
802
    iIntros (Hsp' Hwfm Hwf) "Hm".
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
803
804
805
806
    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.
Dan Frumin's avatar
Dan Frumin committed
807
    rewrite vcg_sp_correct; eauto. simpl.
808
809
    rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=.
    by iFrame.
Dan Frumin's avatar
Dan Frumin committed
810
811
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
812
  Lemma vcg_wp_awp_continuation_correct R E m de Φ :
813
    denv_wf E m 
814
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
815
816
    vcg_wp_awp_continuation R E de m Φ -
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
817
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
818
    rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec.
819
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
820
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
821
    iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
822
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
823
824
  Qed.

825
  Lemma vcg_wp_load_correct E m dv Φ :
826
    denv_wf E m 
827
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
828
    vcg_wp_load E dv m Φ -
829
830
     (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).
831
832
  Proof.
    rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
Dan Frumin's avatar
Dan Frumin committed
833
834
    - destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
      + destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
Léon Gondelman's avatar
Léon Gondelman committed
835
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ".
836
837
        apply is_dloc_Some in Hdloc. simplify_eq/=.
        iExists (dloc_interp E (dLoc i 0)), q,  (dval_interp E dv');
838
839
840
          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.
Dan Frumin's avatar
Dan Frumin committed
841
      + rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
842
        iSpecialize ("Hwp" with "Hm"). simpl.
843
844
        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.
Dan Frumin's avatar
Dan Frumin committed
845
    - rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
846
847
848
      iSpecialize ("Hwp" with "Hm"); simpl.
      iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
      iExists l, q, v'. iSplit; first done. iFrame.
849
850
  Qed.

851
852
853
854
855
856
857
858
859
860
861
  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.
Dan Frumin's avatar
Dan Frumin committed
862
    - iExists (dval_interp E dw); iSplit.
863
864
865
      { 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.
Dan Frumin's avatar
Dan Frumin committed
866
    - rewrite mapsto_wand_list_spec.
867
868
869
      iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
  Qed.

870
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
871
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
872
873
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
874
    vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -
875
    denv_interp E mOut -
Léon Gondelman's avatar
Léon Gondelman committed
876
877
878
     w : val,
      cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
      vcg_wp_continuation