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

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
67
    | 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)
    | dEUnknown e => dEUnknown (subst x (dval_interp E dv) e)
Léon Gondelman 's avatar
Léon Gondelman committed
68
69
70
  end.


71
72
  Fixpoint dce_subst (E: known_locs)
           (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
Léon Gondelman 's avatar
Léon Gondelman committed
73
    match dce with
74
    | dCRet de1 => dCRet (de_subst E x dv de1)
Léon Gondelman 's avatar
Léon Gondelman committed
75
76
    | dCBind y de1 de2 =>
      if decide (x = y)
77
78
79
80
81
      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
82
    | dCBinOp op de1 de2 =>
83
      dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
Léon Gondelman 's avatar
Léon Gondelman committed
84
    | dCPreBinOp op de1 de2 =>
85
86
87
88
89
90
      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)
    | dCUnknown e => dCUnknown (subst x (dval_interp E dv) e)
Léon Gondelman 's avatar
Léon Gondelman committed
91
92
93
    end.


Dan Frumin's avatar
Dan Frumin committed
94
95
96
  (** 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
97
98
99
100
101
102
103
  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) 
104
           vcg_sp E (mNew1 :: ms1) (dce_subst E x dv1 de2) p;
Léon Gondelman 's avatar
Léon Gondelman committed
105
106
107
108
       ''(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
109
110
111
       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
112
113
    | dCStore de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
114
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
115
       ''(ms2, mNew2, dv)  vcg_sp E ms1 de2 p;
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
       ''(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
118
119
120
    | dCBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1 p;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
121
122
       dv  dcbin_op_eval E op dv1 dv2;
       Some (ms2, denv_merge mNew1 mNew2, dv)
Léon Gondelman 's avatar
Léon Gondelman committed
123
124
    | dCPreBinOp op de1 de2, S p =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1 p;
Dan Frumin's avatar
Dan Frumin committed
125
       i                   is_dloc E dl;
Léon Gondelman 's avatar
Léon Gondelman committed
126
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2 p;
Dan Frumin's avatar
Dan Frumin committed
127
       ''(ms3, mNew3, dv)  denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
128
129
       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
130
131
    | dCUnOp op de, S p =>
       ''(ms1, mNew1, dv)  vcg_sp E ms de p ;
132
133
       dv'  dun_op_eval E op dv;
       Some (ms1, mNew1, dv')
Léon Gondelman 's avatar
Léon Gondelman committed
134
135
136
    | 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
137
138
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
Léon Gondelman 's avatar
Léon Gondelman committed
139
140
141
    | 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
142
         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
Léon Gondelman 's avatar
Léon Gondelman committed
143
144
    | dCAlloc _ _, _ |  dCUnknown _, _ | dCInvoke _ _, _ => None
    | _, O => None
145
146
    end.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
155
  Definition vcg_wp_continuation (E: known_locs)
156
157
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
158
159
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
160
         denv_wf E' m' 
161
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
162
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
163
        Φ E' m' dv)%I.
164

Léon Gondelman's avatar
Léon Gondelman committed
165
166
  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
167
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
168

169
170
  Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
171
    mapsto_wand_list E m ( n : nat,
172
173
174
       dval_interp E dv1 = #n  
       l, l C replicate n (dval_interp E dv2) - vcg_wp_continuation E Φ (cloc_to_val l))%I.

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

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

213
214
  (* 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
215
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
216
    match dcbin_op_eval E op dv1 dv2 with
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
    | 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
232
    end%I.
233

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

261
    Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman 's avatar
Léon Gondelman committed
262
263
264
265
266
267
268
269
      (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 =>
270
      vcg_wp E m de1 R (λ E m' dv1,
271
        vcg_wp E m' (dce_subst E x dv1 de2) R Φ p) p
Léon Gondelman 's avatar
Léon Gondelman committed
272
    | dCAlloc de1 de2, S p =>
273
274
275
       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
276
            vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p
277
278
279
280
       | 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
281
               vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)  p
282
283
284
          | None => vcg_wp_awp_continuation R E de m Φ
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
285
286
287
    | 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
288
289
290
       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
291
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
292
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
295
          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
296
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
297
          | None => vcg_wp_awp_continuation R E de m Φ
298
299
          end
        end
Léon Gondelman 's avatar
Léon Gondelman committed
300
    | dCBinOp op de1 de2, S p =>
Robbert Krebbers's avatar
Robbert Krebbers 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
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
305
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
308
          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
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Robbert Krebbers's avatar
Robbert Krebbers committed
310
          | None => vcg_wp_awp_continuation R E de m Φ
311
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
312
       end
Léon Gondelman 's avatar
Léon Gondelman committed
313
    | dCPreBinOp op de1 de2, S p =>
Dan Frumin's avatar
Dan Frumin committed
314
315
316
       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
317
            vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
318
319
320
321
       | 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
322
               vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
Dan Frumin's avatar
Dan Frumin committed
323
324
325
          | None => vcg_wp_awp_continuation R E de m Φ
          end
       end
Léon Gondelman 's avatar
Léon Gondelman committed
326
327
    | 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
328
       vcg_wp E m de1 R (λ E m _,
Léon Gondelman 's avatar
Léon Gondelman committed
329
330
         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
331
332
333
      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
334
          (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
335
336
337
338
      | 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
339
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
Léon Gondelman's avatar
Léon Gondelman committed
340
341
342
        | None => vcg_wp_awp_continuation R E de m Φ
        end
      end
Léon Gondelman 's avatar
Léon Gondelman committed
343
    | dCInvoke ef de1, S p => vcg_wp E m de1 R (λ E m dv,
344
        vcg_wp_awp_continuation R E
Léon Gondelman 's avatar
Léon Gondelman committed
345
346
347
           (dCUnknown (ef (dval_interp E dv))) m Φ) p
    | _, S p => vcg_wp_awp_continuation R E de m Φ
    | _, O => False
Léon Gondelman's avatar
Léon Gondelman committed
348
    end%I.
349
350
351
352
353
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman 's avatar
wip    
Léon Gondelman committed
354
355
356
357
358
359
360

  Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
    dcexpr_interp E (dce_subst E x dv de) =
    (let: x := (dval_interp E dv) in (dcexpr_interp E de))%E.
  Proof.
    Admitted.

Léon Gondelman's avatar
Léon Gondelman committed
361
362
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
363
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
364
        (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
365
           dloc_interp E (dLoc (k + n) 0) C[lv]{q} dval_interp E dv) True dio) - Φ.
Dan Frumin's avatar
Dan Frumin committed
366
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
367
368
    iIntros "H".
    iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
369
370
    - 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
371
372
373
374
375
376
      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
377
378
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
379
380
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
381
  Proof.
Dan Frumin's avatar
Dan Frumin committed
382
383
384
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
385

Léon Gondelman 's avatar
Léon Gondelman committed
386
387
  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
388
    length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
389
  Proof.
390
391
392
393
394
395
396
    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
397
      destruct (vcg_sp E ms de (S n)) as [[[ms1 mNew1] dv1]|] eqn:Hout.
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
      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/=.
429
430
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
431
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
432
      transitivity (length ms1); eauto.
433
    + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
434
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
435
436
437
438
      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/=.
439
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
440
441
      transitivity (length ms1); eauto.
      transitivity (length ms2); eauto using denv_delete_full_2_length.
442
    + destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
443
      destruct (dun_op_eval E u dv1); simplify_eq/=.
444
445
      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
446
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
447
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
448
      destruct ms2; simplify_eq/=. transitivity (length ms1).
449
450
451
      * by eapply IHn.
      * apply IHn in Hde2; by simplify_eq/=.
    + destruct (vcg_sp E ms de1)
452
453
454
        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
455
      transitivity (length ms1); eauto.
456
457
    + done.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
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
  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
483
    dexpr_wf E de  dval_wf E dv.
484
485
486
487
488
489
490
491
492
493
494
495
496
497
  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
498
499
  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
500
    (denv_stack_interp ms ms' E
501
502
       (awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
503
  Proof.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
504
505
506
507
    revert de ms ms' mNew dv. induction n.
    (* Base Case *)
    - iIntros (de ms ms' mNew dv Hsp); simplify_eq/=.
      destruct de; simplify_option_eq.
508
509
510
      iApply denv_stack_interp_intro.
      iApply awp_ret. 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
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
560
    - iIntros (de ms ms' mNew dv Hsp).
      destruct de; simplify_option_eq.
      + iApply denv_stack_interp_intro; iApply awp_ret;
          iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
        iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
      + destruct (vcg_sp E ms de1 n)
          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/=.
        (* specialize (IHn (mNew1 :: ms1)). *)
        (* specialize (IHn de1). *)
        iPoseProof (IHn de1 ms) as "Hawp1"; first done.
        iPoseProof (IHn (dce_subst E s dv1 de2) (mNew1 :: ms1))
          as "Hawp2"; first done.
        iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
        iClear "Hawp1 Hawp2".
        iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
        iApply awp_bind.
        * admit.
        * iApply (awp_wand with "Hawp1").
        iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
        iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
        rewrite dce_subst_subst_comm. iApply (awp_wand with "Hawp2").
        iIntros (?) "[% HmNew1]". simplify_eq/=. iSplit; eauto.
        rewrite- denv_merge_interp. iFrame.
      + destruct (vcg_sp E ms de n)
          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/=.
        specialize (IHn de ms).
        iPoseProof IHn as "Hawp"; first done.
        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.
Admitted.
       (*

Dan Frumin's avatar
Dan Frumin committed
561
562
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
563
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
564
565
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde as "Hawp"; first done.
566
      iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
567
568
569
      iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
      iClear "Hawp Hm".
      iApply (denv_stack_interp_mono with "Hawp'").
Dan Frumin's avatar
Dan Frumin committed
570
      iIntros "[Hawp Hm]".
Léon Gondelman's avatar
Léon Gondelman committed
571
572
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
573
      iIntros (?) "[% HmNew1]". simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
574
575
      iExists _, _. iSplit; eauto.
      iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
Dan Frumin's avatar
Dan Frumin committed
576
      iIntros "Hl". iSplit; eauto.
577
      rewrite -denv_insert_interp. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
578
    - specialize (IHde1 ms).
Dan Frumin's avatar
Dan Frumin committed
579
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
580
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
581
582
583
584
585
586
587
588
589
590
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv3] |] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iPoseProof denv_delete_full_2_interp as "Hl"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
      iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
      iClear "Hawp1 Hawp2 Hl Hawp'".
Dan Frumin's avatar
Dan Frumin committed
591
592
593
594
595
      iApply (denv_stack_interp_mono with "Hawp").
      iIntros "[[Hawp1  Hawp2] Hl]".
      iApply (a_store_spec with "Hawp1 Hawp2").
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=.
      iExists _, _; iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
596
597
598
      iCombine "HmNew1 HmNew2" as "HmNew".
      rewrite denv_merge_interp -denv_insert_interp.
      iDestruct ("Hl" with "HmNew") as "[HmNew3 $]".
Dan Frumin's avatar
Dan Frumin committed
599
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
600
601
602
603
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
604
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
605
606
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
607
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
608
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
609
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
610
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
611
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
612
      iExists (dval_interp E dv). repeat iSplit; eauto.
613
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
614
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
615
616
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
617
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
618
619
620
621
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
        as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=.
622
      destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
623
624
625
626
627
628
629
630
631
632
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iPoseProof denv_delete_full_2_interp as "Hl"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp'".
      iDestruct (denv_stack_interp_trans with "Hawp' Hl") as "Hawp".
      iClear "Hawp1 Hawp2 Hawp' Hl".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[[Hawp1 Hawp2] Hl]".
      iApply (a_pre_bin_op_spec with "Hawp1 Hawp2").
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] HR"; simplify_eq/=.
      iCombine "HmNew1 HmNew2" as "HmNew". rewrite denv_merge_interp.
633
      iExists (dloc_interp E (dLoc i 0)), (dval_interp E dv), (dval_interp E d).
Dan Frumin's avatar
Dan Frumin committed
634
635
      iDestruct ("Hl" with "HmNew") as "[HmNew $]".
      repeat iSplit; eauto.
636
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Dan Frumin's avatar
Dan Frumin committed
637
638
      + iIntros "Hl". iFrame. iSplit; first done.
        rewrite -denv_insert_interp. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
639
640
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
641
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
642
643
      iPoseProof IHde as "Hawp"; first done.
      iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
644
      iIntros "Hawp".
645
646
647
648
      iApply a_un_op_spec.
      iApply (awp_wand with "Hawp"). iIntros (v) "[% H]". simplify_eq/=.
      iExists (dval_interp E dv). repeat iSplit; eauto.
      iPureIntro. apply dun_op_eval_correct. by rewrite -HeqHu.
Dan Frumin's avatar
Dan Frumin committed
649
650
651
652
653
654
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 (denv_unlock mNew1 :: ms1)).
      destruct (vcg_sp E _ de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
655
      unfold popstack in Hsp.
Dan Frumin's avatar
Dan Frumin committed
656
      destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
657
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
658
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
659
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
660
      iApply a_sequence_spec'.
Léon Gondelman 's avatar
Léon Gondelman committed
661
      iNext. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
662
      iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
663
      rewrite (denv_unlock_interp E mNew1).
664
      iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
665
666
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
      rewrite -denv_merge_interp. iSplit; eauto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
667
668
669
670
671
672
673
674
675
676
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
      specialize (IHde2 ms1).
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=.
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
      iClear "Hawp1 Hawp2".
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
      iApply (awp_par with "Hawp1 Hawp2").
677
678
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
      simplify_eq/=; iSplit; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
679
      rewrite -denv_merge_interp. iFrame.
Léon Gondelman 's avatar
wip    
Léon Gondelman committed
680
  Qed. *)
Dan Frumin's avatar
Dan Frumin committed
681

Léon Gondelman 's avatar
Léon Gondelman committed
682
683
  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
684
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
685
686
687
      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
688
  Proof.
689
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
690
    iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
Léon Gondelman 's avatar
Léon Gondelman committed
691
    pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
Dan Frumin's avatar
Dan Frumin committed
692
693
694
    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
695
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
696

Dan Frumin's avatar
Dan Frumin committed
697
698
699
  Lemma vcg_sp'_correct E de m m' mNew dv R :
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
700
701
702
      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
Léon Gondelman committed
703
704
  Proof. Admitted.
(*    rewrite /vcg_sp'.
Dan Frumin's avatar
Dan Frumin committed
705
706
707
708
709
710
711
    iIntros (Hsp') "Hm".
    destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
    destruct ms as [|?m' ms]; simplify_eq/=.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
    rewrite vcg_sp_correct; last eassumption. simpl.
    rewrite denv_merge_nil_r. iFrame.
Léon Gondelman 's avatar
Léon Gondelman committed
712
  Qed. *)
Dan Frumin's avatar
Dan Frumin committed
713

Léon Gondelman 's avatar
Léon Gondelman committed
714
  Lemma vcg_sp_wf' E de ms ms' mNew dv n:
Dan Frumin's avatar
Dan Frumin committed
715
    Forall (denv_wf E) ms 
Léon Gondelman 's avatar
Léon Gondelman committed
716
717
    dcexpr_wf E de 
    vcg_sp E ms de n = Some (ms', mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
718
    Forall (denv_wf E) ms'  denv_wf E mNew  dval_wf E dv .
Léon Gondelman 's avatar
Léon Gondelman committed
719
720
  Proof. Admitted.
(*    revert ms ms' mNew dv. induction de;
Dan Frumin's avatar
Dan Frumin committed
721
    intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
722
723
    - simplify_option_eq. split_and?; auto; first by destruct E.
      by eapply vcg_eval_dexpr_wf.
Dan Frumin's avatar
Dan Frumin committed
724
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
725
      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
726
727
      destruct (denv_delete_frac_2 i ms1 mNew1)
        as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
728
729
730
      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
731
      repeat split; eauto using denv_wf_insert.
Léon Gondelman's avatar
Léon Gondelman committed
732
733
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
734
      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
735
736
737
738
      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
739
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
740
741
742
743
      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
744
745
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
746
747
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
748
749
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
750
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
751
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
752
753
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
754
      repeat split; eauto. apply denv_wf_merge; eauto.
755
      eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
756
757
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
758
      destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
759
760
761
762
      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
763
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
764
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
765
766
767
768
769
770
      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.
771
      eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
772
      by eapply denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
773
774
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
775
      destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
776
      repeat split; eauto.
777
      eapply dun_op_eval_Some_wf; eauto.
Dan Frumin's avatar
Dan Frumin committed
778
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
779
780
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
781
      destruct ms2 as [|t ms2]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
782
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
783
784
      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
785
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
786
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
787
788
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Léon Gondelman's avatar
Léon Gondelman committed
789
790
791
792
793
794
795
    - 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
796
  Qed. *)
Dan Frumin's avatar
Dan Frumin committed
797

Dan Frumin's avatar
Dan Frumin committed
798
  Lemma vcg_sp'_wf E de m m' mNew dv :
799
    denv_wf E m 
Léon Gondelman 's avatar
Léon Gondelman committed
800
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
801
802
    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
803
804
  Proof. Admitted.
(*    rewrite /vcg_sp'. intros Hm Hde Hsp'.
Dan Frumin's avatar
Dan Frumin committed
805
806
807
808
809
810
811
    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
812
  Qed. *)
813

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

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

853
854
855