vcgen.v 46.6 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
From iris_c.c_translation Require Import monad translation proofmode.

7

Dan Frumin's avatar
Dan Frumin committed
8
9
10
Section vcg.
  Context `{amonadG Σ}.

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

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

25
26
  Definition popstack (ms : list denv) : option (list denv * denv) :=
    match ms with
Dan Frumin's avatar
Dan Frumin committed
27
    | [] => None
28
    | m :: ms => Some (ms, m)
Dan Frumin's avatar
Dan Frumin committed
29
30
    end.

31
  Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
32
       : option (list denv * denv * dval) :=
33
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    | dCRet dv    => Some (ms, [], dv)
35
    | dCLoad de1  =>
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
       ''(ms1, mNew, dl)      vcg_sp E ms de1;
       i                      is_dloc E dl;
       ''(ms2, mNew2, q, dv)  denv_delete_frac_2 i ms1 mNew;
       Some (ms2, denv_insert i ULvl q dv mNew2, dv)
40
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
       ''(ms1, mNew1, dl)  vcg_sp E ms de1;
       i                   is_dloc E dl;
       ''(ms2, mNew2, dv)  vcg_sp E ms1 de2;
       ''(ms3, mNew3, _)   denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
       Some (ms3, denv_insert i LLvl 1 dv mNew3, dv)
46
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
49
50
       dv  dcbin_op_eval E op dv1 dv2;
       Some (ms2, denv_merge mNew1 mNew2, dv)
Dan Frumin's avatar
Dan Frumin committed
51
52
53
54
55
    | dCPreBinOp op de1 de2 =>
       ''(ms1, mNew1, dl)  vcg_sp E ms de1;
       i                   is_dloc E dl;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
       ''(ms3, mNew3, dv)  denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
56
57
       dv3  dcbin_op_eval E op dv dv2;
       Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
58
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
59
       ''(ms1, mNew1, dv)  vcg_sp E ms de;
60
61
       dv'  dun_op_eval E op dv;
       Some (ms1, mNew1, dv')
62
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
66
       ''(ms1, mNew1, _)    vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E (denv_unlock mNew1 :: ms1) de2;
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
Léon Gondelman's avatar
Léon Gondelman committed
67
68
69
70
    | dCPar de1 de2 =>
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
         Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
71
    | dCAlloc _ _ |  dCUnknown _ | dCInvoke _ _ => None
72
73
    end.

Léon Gondelman's avatar
Léon Gondelman committed
74
75
  Definition vcg_sp'
       (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
    ''(ms,mNew,dv)  vcg_sp E [m] de;
    ''(_, m')  popstack ms;
    Some (m', mNew, dv).
Léon Gondelman's avatar
Léon Gondelman committed
79

Robbert Krebbers's avatar
Robbert Krebbers committed
80
  Definition vcg_wp_continuation (E: known_locs)
81
82
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
83
84
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
85
         denv_wf E' m' 
86
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
87
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
88
        Φ E' m' dv)%I.
89

Léon Gondelman's avatar
Léon Gondelman committed
90
91
  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
92
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
93

94
95
96
97
98
99
  Definition vcg_wp_alloc (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    ( 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.

100
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
101
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
102
103
104
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
105
       | Some (_, dw) => Φ E m dw
106
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
107
108
109
         mapsto_wand_list E m ( q v,
           dloc_interp E (dLoc i) C{q} v 
           (dloc_interp E (dLoc i) C[ULvl]{q} dval_interp E (dValUnknown v) -
Robbert Krebbers's avatar
Robbert Krebbers committed
110
           vcg_wp_continuation E Φ v))
111
       end
112
113
114
115
    | 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
116
    end%I.
117
118

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
119
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
120
121
122
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
123
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
124
       | None =>
125
126
127
128
          mapsto_wand_list E m ( v : val,
            dloc_interp E (dLoc i) C v 
            (dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 -
             vcg_wp_continuation E Φ (dval_interp E dv2)))
129
       end
130
    | None =>
131
132
133
134
       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
135
          vcg_wp_continuation E Φ (dval_interp E dv2)))%I
Léon Gondelman's avatar
Léon Gondelman committed
136
    end%I.
137

138
139
  (* 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
140
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
141
    match dcbin_op_eval E op dv1 dv2 with
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
    | 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
157
    end%I.
158

159
  Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
Dan Frumin's avatar
Dan Frumin committed
160
161
162
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    match is_dloc E dv1 with
    | Some i =>
163
164
165
      match denv_delete_full i m with
      | Some (m', dw) =>
        match dcbin_op_eval E op dw dv2 with
166
167
168
169
170
        | 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' 
             (dloc_interp E (dLoc i) C[LLvl] w' - vcg_wp_continuation E Φ (dval_interp E dw))
171
        end
172
173
174
175
176
      | None =>
         mapsto_wand_list E m ( v w : val,
           dloc_interp E (dLoc i) C v 
            cbin_op_eval op v (dval_interp E dv2) = Some w  
           (dloc_interp E (dLoc i) C[LLvl] w - vcg_wp_continuation E Φ v))
177
      end
178
    | None =>
179
180
181
182
183
      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
184
185
    end%I.

186
  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman's avatar
Léon Gondelman committed
187
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
188
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    | dCRet dv => Φ E m dv
190
191
192
193
194
195
196
197
198
199
200
201
202
    | dCAlloc de1 de2 =>
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
            vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
               vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
          end
        end
203
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
204
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ)
205
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Robbert Krebbers's avatar
Robbert Krebbers committed
209
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
210
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
213
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
216
217
218
          end
        end
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
Robbert Krebbers's avatar
Robbert Krebbers committed
222
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
223
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
224
225
226
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
229
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
230
       end
Dan Frumin's avatar
Dan Frumin committed
231
232
233
234
235
236
237
238
239
240
241
242
243
    | dCPreBinOp op de1 de2 =>
       match vcg_sp' E m de1 with
       | Some (m', mNew, dv1) =>
          vcg_wp E m' de2 R (λ E m'' dv2,
            vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
       | None =>
          match vcg_sp' E m de2 with
          | Some (m', mNew, dv2) =>
             vcg_wp E m' de1 R (λ E m'' dv1,
               vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
          end
       end
244
    | dCUnOp op de => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ)
245
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
246
       vcg_wp E m de1 R (λ E m _,
Léon Gondelman's avatar
Léon Gondelman committed
247
         U (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
248
249
250
251
252
253
254
255
256
257
258
259
260
    | dCPar de1 de2 =>
      match vcg_sp' E m de1 with
      | Some (m', mNew, dv1) =>
        vcg_wp E m' de2 R (λ E m'' dv2,
          (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
      | None =>
        match vcg_sp' E m de2 with
        | Some (m', mNew, dv2) =>
          vcg_wp E m' de1 R (λ E m'' dv1,
            (Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
        | None => vcg_wp_awp_continuation R E de m Φ
        end
      end
261
    | dCInvoke ef de1 => vcg_wp E m de1 R (λ E m dv,
262
263
        vcg_wp_awp_continuation R E
           (dCUnknown (ef (dval_interp E dv))) m Φ)
Robbert Krebbers's avatar
Robbert Krebbers committed
264
    | _ => vcg_wp_awp_continuation R E de m Φ
Léon Gondelman's avatar
Léon Gondelman committed
265
    end%I.
266
267
268
269
270
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
271
272
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
273
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
274
        (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
275
           default inhabitant (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
Dan Frumin's avatar
Dan Frumin committed
276
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
277
278
    iIntros "H".
    iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
279
280
    - 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
281
282
283
284
285
286
      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
287
288
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
289
290
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
291
  Proof.
Dan Frumin's avatar
Dan Frumin committed
292
293
294
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
295

Dan Frumin's avatar
Dan Frumin committed
296
297
298
  Lemma vcg_sp_length E de ms ms' mNew dv :
    vcg_sp E ms de = Some (ms', mNew, dv) 
    length ms = length ms'.
Dan Frumin's avatar
Dan Frumin committed
299
  Proof.
Dan Frumin's avatar
Dan Frumin committed
300
301
302
    revert ms ms' mNew dv. induction de;
    intros ms ms' mNew dv Hsp; simplify_eq/=; eauto.
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
303
      destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
304
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
305
306
307
      transitivity (length ms1).
      + by eapply IHde.
      + by eapply denv_delete_frac_2_length.
Dan Frumin's avatar
Dan Frumin committed
308
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
309
      destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
310
311
      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/=.
312
313
314
315
      transitivity (length ms1).
      + by eapply IHde1.
      + transitivity (length ms2). by eapply IHde2.
        by eapply denv_delete_full_2_length.
Dan Frumin's avatar
Dan Frumin committed
316
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
317
318
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
      simplify_eq/=.
319
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
320
      transitivity (length ms1); eauto.
Dan Frumin's avatar
Dan Frumin committed
321
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
322
      destruct dv1 as [?|?|?|dv1]; try destruct dv1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
323
      destruct d as [i|?]; simplify_eq/=.
324
325
326
327
      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/=.
328
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
329
330
      transitivity (length ms1); eauto.
      transitivity (length ms2); eauto using denv_delete_full_2_length.
Dan Frumin's avatar
Dan Frumin committed
331
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
332
333
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
Dan Frumin's avatar
Dan Frumin committed
334
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
335
336
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
      as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
337
338
339
340
341
342
343
      destruct ms2; simplify_eq/=. transitivity (length ms1).
      + by eapply IHde1.
      + apply IHde2 in Hde2; by simplify_eq/=.
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E ms1 de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
344
      transitivity (length ms1); eauto.
Dan Frumin's avatar
Dan Frumin committed
345
346
  Qed.

Dan Frumin's avatar
Dan Frumin committed
347
348
349
  Lemma vcg_sp_correct' E de ms ms' mNew dv R :
    vcg_sp E ms de = Some (ms', mNew, dv) 
    (denv_stack_interp ms ms' E
350
351
       (awp (dcexpr_interp E de) R
          (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
352
  Proof.
Dan Frumin's avatar
Dan Frumin committed
353
354
    revert ms ms' mNew dv. induction de;
    iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
355
356
    - iFrame. iApply denv_stack_interp_intro.
      iApply awp_ret. wp_value_head. iSplit; eauto. rewrite /denv_interp //.
Dan Frumin's avatar
Dan Frumin committed
357
358
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
359
      destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
360
361
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde as "Hawp"; first done.
362
      iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
363
364
365
      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
366
      iIntros "[Hawp Hm]".
Léon Gondelman's avatar
Léon Gondelman committed
367
368
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
369
      iIntros (?) "[% HmNew1]". simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
370
371
      iExists _, _. iSplit; eauto.
      iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
Dan Frumin's avatar
Dan Frumin committed
372
      iIntros "Hl". iSplit; eauto.
373
374
      rewrite -denv_insert_interp. by iFrame.
      - specialize (IHde1 ms).
Dan Frumin's avatar
Dan Frumin committed
375
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
376
      destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
377
378
379
380
381
382
383
384
385
386
      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
387
388
389
390
391
      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
392
393
394
      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
395
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
396
397
398
399
    - 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 /=.
400
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
401
402
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
403
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
404
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
405
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
406
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
407
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
408
      iExists (dval_interp E dv). repeat iSplit; eauto.
409
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
410
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
411
412
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
413
      destruct dv1 as [?|?|d|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
414
415
416
417
418
      destruct d as [i|?]; simplify_eq/=.
      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/=.
419
      destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
420
421
422
423
424
425
426
427
428
429
430
431
432
      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.
      iExists (dloc_interp E (dLoc i)), (dval_interp E dv), (dval_interp E d).
      iDestruct ("Hl" with "HmNew") as "[HmNew $]".
      repeat iSplit; eauto.
433
      + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe.
Dan Frumin's avatar
Dan Frumin committed
434
435
      + iIntros "Hl". iFrame. iSplit; first done.
        rewrite -denv_insert_interp. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
436
437
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
438
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
439
440
      iPoseProof IHde as "Hawp"; first done.
      iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
441
      iIntros "Hawp".
442
443
444
445
      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
446
447
448
449
450
451
    - 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
452
      unfold popstack in Hsp.
Dan Frumin's avatar
Dan Frumin committed
453
      destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
454
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
455
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
456
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
457
      iApply a_sequence_spec'. iNext. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
458
      iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
459
      rewrite (denv_unlock_interp E mNew1).
460
      iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
461
462
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
      rewrite -denv_merge_interp. iSplit; eauto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
463
464
465
466
467
468
469
470
471
472
    - 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").
473
474
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
      simplify_eq/=; iSplit; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
475
      rewrite -denv_merge_interp. iFrame.
476
  Qed.
Dan Frumin's avatar
Dan Frumin committed
477

Dan Frumin's avatar
Dan Frumin committed
478
479
  Lemma vcg_sp_correct E de m ms mNew dv R :
    vcg_sp E [m] de = Some (ms, mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
480
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
481
482
483
      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
484
  Proof.
485
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
486
487
488
489
490
    iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert ( m', ms = [m']) as [m' ->]=>/=.
    { destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
    rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
Dan Frumin's avatar
Dan Frumin committed
491
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
492

Dan Frumin's avatar
Dan Frumin committed
493
494
495
  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
496
497
498
      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
499
  Proof.
Dan Frumin's avatar
Dan Frumin committed
500
501
502
503
504
505
506
507
    rewrite /vcg_sp'.
    iIntros (Hsp') "Hm".
    destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
    destruct ms as [|?m' ms]; simplify_eq/=.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
    rewrite vcg_sp_correct; last eassumption. simpl.
    rewrite denv_merge_nil_r. iFrame.
Dan Frumin's avatar
Dan Frumin committed
508
509
  Qed.

Dan Frumin's avatar
Dan Frumin committed
510
511
  Lemma vcg_sp_wf' E de ms ms' mNew dv :
    Forall (denv_wf E) ms 
Dan Frumin's avatar
Dan Frumin committed
512
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
513
514
    vcg_sp E ms de = Some (ms', mNew, dv) 
    Forall (denv_wf E) ms'  denv_wf E mNew  dval_wf E dv .
Dan Frumin's avatar
Dan Frumin committed
515
  Proof.
Dan Frumin's avatar
Dan Frumin committed
516
517
    revert ms ms' mNew dv. induction de;
    intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
518
    - split; first done. unfold denv_wf. split; last done. apply andb_True. by destruct E.
Dan Frumin's avatar
Dan Frumin committed
519
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
520
      destruct dv1 as [|?|[i|?]|]; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
521
522
      destruct (denv_delete_frac_2 i ms1 mNew1)
        as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
523
524
525
      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
526
      repeat split; eauto using denv_wf_insert.
Léon Gondelman's avatar
Léon Gondelman committed
527
528
    - destruct (vcg_sp E ms de1)
        as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
529
      destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
530
531
532
533
      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
534
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
535
536
537
538
      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
539
540
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
541
542
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
543
544
      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
      simplify_eq/=.
545
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
546
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
547
548
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
549
      repeat split; eauto. apply denv_wf_merge; eauto.
550
      eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
551
552
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
      simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
553
      destruct dv1 as [|?|d|]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
554
      destruct d as [i|?]; simplify_eq/=.
555
556
557
558
      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
559
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
560
      destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
561
562
563
564
565
566
      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.
567
      eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
568
      by eapply denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
569
570
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
571
      destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
572
      repeat split; eauto.
573
      eapply dun_op_eval_Some_wf; eauto.
Dan Frumin's avatar
Dan Frumin committed
574
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
575
576
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
        as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
577
      destruct ms2 as [|t ms2]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
578
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
579
580
      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
581
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
582
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
583
584
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Léon Gondelman's avatar
Léon Gondelman committed
585
586
587
588
589
590
591
    - 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.
Dan Frumin's avatar
Dan Frumin committed
592
  Qed.
Dan Frumin's avatar
Dan Frumin committed
593

Dan Frumin's avatar
Dan Frumin committed
594
  Lemma vcg_sp'_wf E de m m' mNew dv :
595
596
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
597
598
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_wf E m'  denv_wf E mNew  dval_wf E dv .
Dan Frumin's avatar
Dan Frumin committed
599
  Proof.
Dan Frumin's avatar
Dan Frumin committed
600
601
602
603
604
605
606
607
    rewrite /vcg_sp'. intros Hm Hde Hsp'.
    assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto).
    destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
    destruct ms as [|?m' ms]; simplify_eq/=.
    pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
    assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
    destruct (vcg_sp_wf' E de [m] [m'] mNew _ Hms Hde Hsp) as (Hm'&?&?).
    repeat split; eauto. by inversion Hm'.
Dan Frumin's avatar
Dan Frumin committed
608
  Qed.
609

Robbert Krebbers's avatar
Robbert Krebbers committed
610
  Lemma vcg_wp_awp_continuation_correct R E m de Φ :
611
    denv_wf E m 
612
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
613
614
    vcg_wp_awp_continuation R E de m Φ -
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
615
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
    rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec.
617
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
618
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
619
    iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
620
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
621
622
  Qed.

623
  Lemma vcg_wp_load_correct E m dv Φ :
624
    denv_wf E m 
625
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
626
    vcg_wp_load E dv m Φ -
627
628
     (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).
629
630
631
  Proof.
    rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
    + destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
632
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
Léon Gondelman's avatar
Léon Gondelman committed
633
634
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ".
        apply is_dloc_some in Hdloc. simplify_eq/=.
635
636
637
638
        iExists (dloc_interp E (dLoc i)), q,  (dval_interp E dv');
          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.
639
640
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
641
        iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
642
        iExists (dloc_interp E (dLoc i)), q, v'; iSplit; first done. iFrame.
643
644
645
646
    + rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
      iSpecialize ("Hwp" with "Hm"); simpl.
      iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
      iExists l, q, v'. iSplit; first done. iFrame.
647
648
  Qed.

649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
  Lemma vcg_wp_un_op_correct E m dv b Φ :
    dval_wf E dv 
    denv_wf E m 
    denv_interp E m -
    vcg_wp_un_op E b dv m Φ -
     w : val,
      un_op_eval b (dval_interp E dv) = Some w 
      vcg_wp_continuation E Φ w.
  Proof.
    iIntros (Hwf Hwf2) "Hm Hwp". rewrite /vcg_wp_un_op.
    destruct (dun_op_eval E b dv) as [dw|] eqn:Hbin.
    * iExists (dval_interp E dw); iSplit.
      { iPureIntro. apply dun_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, m.
      apply dun_op_eval_Some_wf in Hbin; try done. eauto with iFrame.
    * rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
  Qed.

668
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
669
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
670
671
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
672
    vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -
673
    denv_interp E mOut -
Léon Gondelman's avatar
Léon Gondelman committed
674
675
676
     w : val,
      cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
      vcg_wp_continuation E Φ w.
677
  Proof.
678
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
679
    destruct (dcbin_op_eval E b dv1 dv2) as [dw|] eqn:Hbin.
680
    * iExists (dval_interp E dw); iSplit.
681
      { iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. }
682
      iExists E, dw, (denv_merge mOut m).
683
      apply dcbin_op_eval_Some_wf in Hbin; try done.
684
      rewrite -denv_merge_interp //. eauto with iFrame.
685
686
687
    * iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
      rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
688
  Qed.
689

Dan Frumin's avatar
Dan Frumin committed
690
691
692
693
694
  Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ :
    denv_wf E m 
    dval_wf E dv2 
    denv_interp E m -
    vcg_wp_pre_bin_op E op dv1 dv2 m Φ -
Dan Frumin's avatar
Dan Frumin committed
695
     l v w, l C v  dval_interp E dv1 = cloc_to_val l 
696
      cbin_op_eval op v (dval_interp E dv2) = Some w 
697
      (l C[LLvl] w - vcg_wp_continuation E Φ v).
Dan Frumin's avatar
Dan Frumin committed
698
699
700
701
702
703
704
705
706
707
708
  Proof.
    iIntros (? ?) "Hm Hwp". rewrite /vcg_wp_pre_bin_op.
    destruct (is_dloc E dv1) as [i|] eqn:Hloc; last first.
    { rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (l v w) "(%&Hl&%&Hwp)".
      iExists l,v,w. iFrame. eauto. }
    apply is_dloc_some in Hloc. simplify_eq/=.
    destruct (denv_delete_full i m) as [[m' dw] | ] eqn:Hdel; last first.
    - rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm") as (v w) "(Hl&%&Hwp)".
      iExists (dloc_interp E (dLoc i)),v,w. iFrame. eauto.
709
710
    - iDestruct (denv_delete_full_interp E with "Hm") as "[Hm' Hl]";
      first eassumption.
711
      destruct (dcbin_op_eval E op dw dv2) as [dw'|] eqn:Hop.
712
      { iExists (dloc_interp E (dLoc i)),
713
          (dval_interp E dw), (dval_interp E dw'). iFrame "Hl".
Dan Frumin's avatar
Dan Frumin committed
714
        repeat iSplit; eauto; try iPureIntro.
715
        - apply dcbin_op_eval_correct. by rewrite Hop.
Dan Frumin's avatar
Dan Frumin committed
716
717
718
        - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp.
          rewrite /vcg_wp_continuation. iExists E,dw,_. iFrame.
          eapply denv_wf_delete_full in Hdel; eauto. destruct_and!.
719
          apply dcbin_op_eval_Some_wf in Hop; eauto.
Dan Frumin's avatar
Dan Frumin committed
720
          repeat iSplit; eauto using denv_wf_insert. }
721
722
723
724
      rewrite mapsto_wand_list_spec.
      iDestruct ("Hwp" with "Hm'") as (w' ?) "Hwp".
      iExists (dloc_interp E (dLoc i)), (dval_interp E dw), w'. iFrame; eauto.
   Qed.
Dan Frumin's avatar
Dan Frumin committed
725

726
  Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
727
728
729
730
    denv_wf E m 
    dval_wf E dv2 
    denv_interp E m -
    vcg_wp_store E dv1 dv2 m Φ -
731
732
733
734
     (cl : cloc) (w : val),
      dval_interp E dv1 = cloc_to_val cl 
      cl C w 
      (cl C[LLvl] dval_interp E dv2 - vcg_wp_continuation E Φ (dval_interp E dv2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
735
736
737
738
739
  Proof.
    iIntros (Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
    destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
    - apply is_dloc_some in Hdloc; rewrite Hdloc.
      destruct (denv_delete_full i m)  as [[m' dv_old]|] eqn:Hdel.
Léon Gondelman's avatar
Léon Gondelman committed
740
741
      + iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old);
        iSplit; first done.
742
        iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
Dan Frumin's avatar
Dan Frumin committed
743
        iSpecialize ("Hdel" with "Hm"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
744
745
746
        iIntros "Hl".
        iExists E, dv2, (denv_insert i LLvl 1 dv2 m');
          repeat (iSplit; first done).
747
        iSplit. iPureIntro. apply denv_wf_insert; last done.
Dan Frumin's avatar
Dan Frumin committed
748
        by destruct (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as [Hdelwf ?].
Robbert Krebbers's avatar
Robbert Krebbers committed
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
        rewrite -denv_insert_interp. eauto with iFrame.
      + rewrite mapsto_wand_list_spec.
        iSpecialize ("Hwp" with "[Hm]"); iFrame.
        iDestruct "Hwp" as (dv_old) "[Hl Hwp]";
        iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
    - rewrite mapsto_wand_list_spec.
      iSpecialize ("Hwp" with "[Hm]"); iFrame.
  Qed.

  Lemma vcg_wp_continuation_mono E E' Φ w:
    E `prefix_of` E'  vcg_wp_continuation E' Φ w - vcg_wp_continuation E Φ w.
  Proof.
    iIntros (Hpre) "Hp".
    iDestruct "Hp" as (E1 dv m' ? Hpre1 ?) "(% & Hm' & H)"; simplify_eq /=.
    iExists