vcgen.v 31.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 splitenv denv.
Dan Frumin's avatar
Dan Frumin committed
5
6
7
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
(*
TODO

11
[DONE] Fix all the unknown cases, introduce a function for that (which should be
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
  simpl never)
- Write more tests with unknown stuff in it
14
  add tests like `!(l := 10;;;; l)`
Léon Gondelman's avatar
Léon Gondelman committed
15
[DONE] Support alloc in `vcg_wp`
Robbert Krebbers's avatar
Robbert Krebbers committed
16
- Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case
Robbert Krebbers's avatar
Robbert Krebbers committed
17
- Finish the proofs
Léon Gondelman's avatar
Léon Gondelman committed
18
[DONE] Maybe drop `wp_expr`? We are not taking it as an input of anything anymore
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
21
22
23
24
25
26
27
28

Less urgent TODO

- Symbolic fractions
- Support bind
- Support conditional
- Write examples with R
- Deal with functions
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
35
36


Dan Frumin's avatar
Dan Frumin committed
37
38
39
Section vcg.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
40
  Fixpoint mapsto_wand_list_aux (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
41
    match m with
42
    | [] => Φ
Léon Gondelman's avatar
Léon Gondelman committed
43
    | None :: m' => mapsto_wand_list_aux E m' Φ (S i)
44
    | Some (DenvItem x q dv) :: m' =>
Léon Gondelman's avatar
Léon Gondelman committed
45
46
       dloc_interp E (dLoc i) C[x]{q} dval_interp E dv - mapsto_wand_list_aux E m' Φ (S i)
    end%I.
47

Léon Gondelman's avatar
Léon Gondelman committed
48
49
  Definition mapsto_wand_list (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
    mapsto_wand_list_aux E m Φ O.
50

51
52
  Definition popstack (ms : list denv) : option (list denv * denv) :=
    match ms with
Dan Frumin's avatar
Dan Frumin committed
53
    | [] => None
54
    | m :: ms => Some (ms, m)
Dan Frumin's avatar
Dan Frumin committed
55
56
    end.

57
  Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
58
       : option (list denv * denv * dval) :=
59
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    | dCRet dv    => Some (ms, [], dv)
61
    | dCLoad de1  =>
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
       ''(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)
66
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
       ''(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)
72
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
       ''(ms1, mNew1, dv1)  vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E ms1 de2;
75
       match dbin_op_eval E op dv1 dv2 with
Robbert Krebbers's avatar
Robbert Krebbers committed
76
       | dSome dv => Some (ms2, denv_merge mNew1 mNew2, dv)
77
78
       | dNone | dUnknown _ => None
       end
79
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
80
       ''(ms1, mNew1, dv)  vcg_sp E ms de;
81
       match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
82
       | dSome dv' => Some (ms1, mNew1, dv')
83
84
       | dNone | dUnknown _ => None
       end
85
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
89
       ''(ms1, mNew1, _)    vcg_sp E ms de1;
       ''(ms2, mNew2, dv2)  vcg_sp E (denv_unlock mNew1 :: ms1) de2;
       ''(ms3, mNew3)  popstack ms2;
       Some (ms3, denv_merge mNew2 mNew3, dv2)
90
    | dCAlloc _ |  dCUnknown _ => None
91
92
    end.

Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
  Definition vcg_sp' (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
    ''(ms,mNew,dv)  vcg_sp E [m] de;
    ''(_, m')  popstack ms;
    Some (m', mNew, dv).
Léon Gondelman's avatar
Léon Gondelman committed
97

Robbert Krebbers's avatar
Robbert Krebbers committed
98
  Definition vcg_wp_continuation (E: known_locs)
99
100
      (Φ : known_locs  denv  dval  iProp Σ) : val  iProp Σ :=
    λ v, ( E' dv m',
Léon Gondelman's avatar
Léon Gondelman committed
101
102
         v = dval_interp E' dv  
         E `prefix_of` E'  
Robbert Krebbers's avatar
Robbert Krebbers committed
103
         denv_wf E' m' 
104
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
105
        denv_interp E' m' 
Robbert Krebbers's avatar
Robbert Krebbers committed
106
        Φ E' m' dv)%I.
107

Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Definition vcg_wp_awp_continuation (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
109
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
110
    mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ)).
111

112
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
113
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
114
115
116
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
117
       | Some (_, dw) => Φ E m dw
118
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
119
120
121
         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
122
           vcg_wp_continuation E Φ v))
123
       end
124
125
126
    | _ =>
      mapsto_wand_list E m ( (l : loc) q v,
        dval_interp E dv = #l 
Robbert Krebbers's avatar
Robbert Krebbers committed
127
        l C{q} v  (l C{q} v - vcg_wp_continuation E Φ v))%I
Léon Gondelman's avatar
Léon Gondelman committed
128
    end%I.
129
130

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Robbert Krebbers's avatar
Robbert Krebbers committed
131
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
132
133
134
    match is_dloc E dv1 with
    | Some i =>
       match denv_delete_full i m with
Robbert Krebbers's avatar
Robbert Krebbers committed
135
       | Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
136
       | None =>
Léon Gondelman's avatar
Léon Gondelman committed
137
138
         mapsto_wand_list E m ( v : val,
           dloc_interp E (dLoc i) C v 
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
           (dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 -
            vcg_wp_continuation E Φ (dval_interp E dv2)))
141
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    | _ =>
143
144
145
       mapsto_wand_list E m ( (l : loc) (v : val),
         dval_interp E dv1 = #l 
         dloc_interp E (dLocUnknown l) C v 
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
         (dloc_interp E (dLocUnknown l) C[LLvl] dval_interp E dv2 -
          vcg_wp_continuation E Φ (dval_interp E dv2)))%I
Léon Gondelman's avatar
Léon Gondelman committed
148
    end%I.
149
150

  Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
      (m : denv) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
152
    match dbin_op_eval E op dv1 dv2 with
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
    | dSome dw => Φ E m dw
    | mdw =>  dw,  doption_interp mdw = Some dw   vcg_wp_continuation E Φ (dval_interp E dw)
Léon Gondelman's avatar
Léon Gondelman committed
155
    end%I.
156
157

  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Léon Gondelman's avatar
Léon Gondelman committed
158
      (R : iProp Σ) (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
159
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
160
    | dCRet dv => Φ E m dv
161
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
162
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ)
163
    | dCStore de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
       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
167
            vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
168
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
          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
172
173
               vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
174
175
176
          end
        end
    | dCBinOp op de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
179
       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
180
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
181
       | None =>
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
          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
185
186
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
          | None => vcg_wp_awp_continuation R E de m Φ
187
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
188
       end
189
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
190
       vcg_wp E m de R (λ E m dv,
191
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
192
         | dSome dw => Φ E m dw
Robbert Krebbers's avatar
Robbert Krebbers committed
193
         | mdw =>  dw, doption_interp mdw = Some dw  Φ E m dw
194
195
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
196
       vcg_wp E m de1 R (λ E m _,
Léon Gondelman's avatar
Léon Gondelman committed
197
         U (vcg_wp E (denv_unlock m) de2 R Φ))
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    | _ => vcg_wp_awp_continuation R E de m Φ
Léon Gondelman's avatar
Léon Gondelman committed
199
    end%I.
200
201
202
203
204
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
205
206
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
207
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
208
209
        (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
           default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
Dan Frumin's avatar
Dan Frumin committed
210
  Proof.
211
212
213
214
215
216
    iIntros "H". iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
    - iIntros "[H1 H2]". rewrite -plus_n_O. iSpecialize ("H" with "H1").
      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.
    - 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
217
218
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
219
220
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
221
  Proof.
Dan Frumin's avatar
Dan Frumin committed
222
223
224
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
225

Dan Frumin's avatar
Dan Frumin committed
226
227
228
  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
229
  Proof.
Dan Frumin's avatar
Dan Frumin committed
230
231
232
    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
233
234
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
235
236
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      transitivity (length ms1).
Dan Frumin's avatar
Dan Frumin committed
237
      + by eapply IHde.
Dan Frumin's avatar
Dan Frumin committed
238
239
      + by eapply denv_delete_frac_2_length.
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
240
241
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
242
243
244
      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).
Dan Frumin's avatar
Dan Frumin committed
245
      + by eapply IHde1.
Dan Frumin's avatar
Dan Frumin committed
246
247
248
249
      + transitivity (length ms2). by eapply IHde2.
        by eapply denv_delete_full_2_length.
    - 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/=.
Dan Frumin's avatar
Dan Frumin committed
250
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
251
      transitivity (length ms1); eauto.
Dan Frumin's avatar
Dan Frumin committed
252
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
253
254
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
Dan Frumin's avatar
Dan Frumin committed
255
256
257
258
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
      destruct ms2; simplify_eq/=.
      transitivity (length ms1).
Dan Frumin's avatar
Dan Frumin committed
259
260
261
262
      + by eapply IHde1.
      + apply IHde2 in Hde2. by simplify_eq/=.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
263
264
265
266
  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
        (awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mNew)))%I.
267
  Proof.
Dan Frumin's avatar
Dan Frumin committed
268
269
    revert ms ms' mNew dv. induction de;
    iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
270
271
    - iFrame. iApply denv_stack_interp_intro.
      iApply awp_ret. wp_value_head. iSplit; eauto. rewrite /denv_interp //.
Dan Frumin's avatar
Dan Frumin committed
272
273
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
274
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
275
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
276
277
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
      iPoseProof IHde as "Hawp"; first done.
278
      iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
279
280
281
      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
282
      iIntros "[Hawp Hm]".
Léon Gondelman's avatar
Léon Gondelman committed
283
284
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
285
286
287
      iIntros (?) "[% HmNew1]". simplify_eq/=.
      iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
      iIntros "Hl". iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
288
      rewrite -denv_insert_interp.
Léon Gondelman's avatar
Léon Gondelman committed
289
      by iFrame.
Dan Frumin's avatar
Dan Frumin committed
290
291
    - specialize (IHde1 ms).
      destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
292
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
293
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
294
295
296
297
298
299
300
301
302
303
      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
304
305
306
307
308
      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
309
310
311
      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
312
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
313
314
315
316
    - 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 /=.
317
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
318
319
      iPoseProof IHde1 as "Hawp1"; first done.
      iPoseProof IHde2 as "Hawp2"; first done.
Dan Frumin's avatar
Dan Frumin committed
320
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
321
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
322
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
323
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
324
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
325
      iExists (dval_interp E dv). repeat iSplit; eauto.
326
      + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
327
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
328
329
    - specialize (IHde ms).
      destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
330
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
331
332
      iPoseProof IHde as "Hawp"; first done.
      iApply (denv_stack_interp_mono with "Hawp"). iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
333
      iIntros "Hawp".
334
335
336
337
      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
338
339
340
341
342
343
    - 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
344
      unfold popstack in Hsp.
Dan Frumin's avatar
Dan Frumin committed
345
      destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
346
      iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
Dan Frumin's avatar
Dan Frumin committed
347
      iClear "Hawp1 Hawp2".
Dan Frumin's avatar
Dan Frumin committed
348
      iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
349
      iApply a_sequence_spec'. iNext. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
350
      iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
Dan Frumin's avatar
Dan Frumin committed
351
      rewrite (denv_unlock_interp E mNew1).
352
      iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
353
354
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]".
      rewrite -denv_merge_interp. iSplit; eauto with iFrame.
355
  Qed.
Dan Frumin's avatar
Dan Frumin committed
356

Dan Frumin's avatar
Dan Frumin committed
357
358
  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
359
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
360
    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
361
  Proof.
362
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
363
364
365
366
367
    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
368
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
369

Dan Frumin's avatar
Dan Frumin committed
370
371
372
373
  Lemma vcg_sp'_correct E de m m' mNew dv R :
    vcg_sp' E m de = Some (m', mNew, dv) 
    denv_interp E m -
    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
374
  Proof.
Dan Frumin's avatar
Dan Frumin committed
375
376
377
378
379
380
381
382
    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
383
384
  Qed.

Dan Frumin's avatar
Dan Frumin committed
385
386
  Lemma vcg_sp_wf' E de ms ms' mNew dv :
    Forall (denv_wf E) ms 
Dan Frumin's avatar
Dan Frumin committed
387
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
388
389
    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
390
  Proof.
Dan Frumin's avatar
Dan Frumin committed
391
392
393
    revert ms ms' mNew dv. induction de;
    intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
394
395
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
396
397
398
399
      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      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
400
      repeat split; eauto using denv_wf_insert.
Dan Frumin's avatar
Dan Frumin committed
401
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
402
403
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
404
405
      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
406
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
407
408
409
410
      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
411
412
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
413
414
    - 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/=.
Dan Frumin's avatar
Dan Frumin committed
415
416
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
417
418
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
419
420
      repeat split; eauto. apply denv_wf_merge; eauto.
      eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
421
422
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
Dan Frumin's avatar
Dan Frumin committed
423
424
425
      destruct (dun_op_eval E u dv1) as [|?|?] eqn:Hop; simplify_eq/=.
      repeat split; eauto.
      eapply dun_op_eval_dSome_wf; eauto.
Dan Frumin's avatar
Dan Frumin committed
426
427
428
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
      destruct ms2 as [|t ms2]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
429
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
430
431
      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
432
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
433
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
434
435
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
436
  Qed.
Dan Frumin's avatar
Dan Frumin committed
437

Dan Frumin's avatar
Dan Frumin committed
438
  Lemma vcg_sp'_wf E de m m' mNew dv :
439
440
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
441
442
    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
443
  Proof.
Dan Frumin's avatar
Dan Frumin committed
444
445
446
447
448
449
450
451
    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
452
  Qed.
453

Robbert Krebbers's avatar
Robbert Krebbers committed
454
  Lemma vcg_wp_awp_continuation_correct R E m de Φ :
455
    denv_wf E m 
456
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
    vcg_wp_awp_continuation R E de m Φ -
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
459
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
    rewrite /vcg_wp_awp_continuation mapsto_wand_list_spec.
461
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
462
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
463
    iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
464
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
465
466
  Qed.

467
  Lemma vcg_wp_load_correct E m dv Φ :
468
    denv_wf E m 
469
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
472
    vcg_wp_load E dv m Φ -
     (l : loc) q w, dval_interp E dv = #l 
       l C{q} w  (l C{q} w - vcg_wp_continuation E Φ w).
473
474
475
  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
476
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
477
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
478
479
480
481
        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.
482
483
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
484
        iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
485
        iExists (dloc_interp E (dLoc i)), q, v'; iSplit; first done. iFrame.
486
487
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
488
       iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
Robbert Krebbers's avatar
Robbert Krebbers committed
489
       iExists l, q, v'. iSplit; first done. iFrame.
490
491
  Qed.

492
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
493
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
494
495
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
Robbert Krebbers's avatar
Robbert Krebbers committed
496
    vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -
497
498
    denv_interp E mOut -
     w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
Robbert Krebbers's avatar
Robbert Krebbers committed
499
               vcg_wp_continuation E Φ w.
500
  Proof.
501
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin. (*
503
    * iExists (dval_interp E dw); iSplit.
504
505
      { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, (denv_merge mOut m).
506
507
      apply dbin_op_eval_dSome_wf in Hbin; try done.
      rewrite -denv_merge_interp //. eauto with iFrame.
508
509
    * destruct dw as [dw1|] eqn:Hdw; last done.
      iExists  (dval_interp E dw1); iSplit.
510
      iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
511
      iExists E, dw1, (denv_merge mOut m).
512
513
      rewrite -denv_merge_interp.
      apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
  Qed. *) Admitted.
515

Robbert Krebbers's avatar
Robbert Krebbers committed
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
  Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
    denv_wf E m 
    dval_wf E dv2 
    denv_interp E m -
    vcg_wp_store E dv1 dv2 m Φ -
     (l : loc) (w : val),
      dval_interp E dv1 = #l 
      l C w 
      (l C[LLvl] dval_interp E dv2 - vcg_wp_continuation E Φ (dval_interp E dv2)).
  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.
      + iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old); iSplit; first done.
531
532
533
534
        iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
        iSpecialize ("Hdel" with "[$Hm]"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
        iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
        iSplit. iPureIntro. apply denv_wf_insert; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
        by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
        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 E1, dv, m'; repeat (iSplit; first done).
    iSplit. iPureIntro. by trans E'. eauto with iFrame.
  Qed.

  Lemma vcg_wp_correct R E m de Φ :
555
    dcexpr_wf E de 
556
    denv_wf E m 
557
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
558
    vcg_wp E m de R Φ -
Robbert Krebbers's avatar
Robbert Krebbers committed
559
    awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
560
  Proof.
561
562
563
    revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
    - iApply awp_ret. wp_value_head.
      iExists E, d, m. iSplit; first done; by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
    - by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
565
    - rewrite IHde //. iRename "Hm" into "Hawp".
566
      iSpecialize ("Hawp" with "Hwp"); simpl.
567
      iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
Robbert Krebbers's avatar
Robbert Krebbers committed
568
      iIntros (v) "H".
569
      iDestruct "H" as (E' dv m' Heq Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
570
      iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done.
571
572
      iDestruct "Hload" as (l q w) "(% & Hl & Hwp)". rewrite Heq.
      iExists l, q, w. iSplit; first done. iFrame. iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
573
      iSpecialize ("Hwp" with "Hl").
574
575
576
      iDestruct "Hwp" as (Ef dvf mf Hpre' Hwf5 Hwf3 Hwf4) "(Hmf & Hwp)".
      iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro. iSplit.
      iPureIntro. trans E'; done. done.
577
    - rewrite{1} /vcg_wp; fold vcg_wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
      simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
579
580
      destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first.
      + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
        { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
582
583
        specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (? & ? & ?).
        iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde2]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
        clear Heqsp2 Heqsp.
Dan Frumin's avatar
Dan Frumin committed
585
        iDestruct (IHde1 with "Hm' Hwp") as "Hde1"; try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
587
588
        iDestruct 1 as (E' dw m'' ? Hpre ? ?) "(Hm' & H)". iIntros "[-> HmNew]".
        rewrite (dval_interp_mono E E') //. subst v1.
Robbert Krebbers's avatar
Robbert Krebbers committed
589
        iDestruct (vcg_wp_store_correct with "[-H] H") as (l w ?) "[Hl H]";
590
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
592
593
594
        { rewrite -!denv_merge_interp. iFrame "Hm'".
          rewrite -!(denv_interp_mono E E'); eauto. }
        iExists l, w. iSplit; first done. iIntros "{$Hl} Hl".
        iApply vcg_wp_continuation_mono; last by iApply "H". done.
Dan Frumin's avatar
Dan Frumin committed
595
596
597
      + specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
        iDestruct (vcg_sp'_correct with "Hm") as "[Hm' Hde1]"; first done. clear Heqsp.
        iDestruct (IHde2 with "Hm' Hwp") as "Hde2"; try done.
598
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
599
600
        iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? ? ?) "(% & Hm' & H)".
        rewrite (dval_interp_mono E E') //. subst v2.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
        iDestruct (vcg_wp_store_correct with "[-H] H") as (l w ?) "[Hl H]";
Robbert Krebbers's avatar
Robbert Krebbers committed
602
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
605
606
        { rewrite -!denv_merge_interp. iFrame "Hm'".
          rewrite -!(denv_interp_mono E E'); eauto. }
        iExists l, w. iSplit; first done. iIntros "{$Hl} Hl".
        iApply vcg_wp_continuation_mono; last by iApply "H". done.
Léon Gondelman's avatar
Léon Gondelman committed
607
    - rewrite{1} /vcg_wp; fold vcg_wp.
608
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
609
610
      destruct (vcg_sp' E m de1) as [[[m' mNew] dv1]|] eqn:Heqsp; last first.
      + destruct (vcg_sp' E m de2) as [[[m' mNew] dv2]|] eqn:Heqsp2; last first.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
        { by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
612
613
614
615
616
617
        iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption.
        specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (?&?&?).
        iDestruct ("Hsp" with "Hm") as "[Hm' Hde2]".
        iClear "Hsp"; clear Heqsp2 Heqsp.
        rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp").
        iApply (a_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp.
Dan Frumin's avatar
Dan Frumin committed
618
        iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
619
        iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
620
        rewrite (dval_interp_mono E E' dv2); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
        iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H";
Dan Frumin's avatar
Dan Frumin committed
622
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
624
        { iApply (denv_interp_mono with "HmNew"); eauto. }
        iExists w. iSplit; first done. by iApply vcg_wp_continuation_mono.
Dan Frumin's avatar
Dan Frumin committed
625
626
627
628
629
      + iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption.
        specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
        iDestruct ("Hsp" with "Hm") as "[Hm' Hde1]"; iClear "Hsp"; clear Heqsp.
        rewrite IHde2; [| done | done]. iSpecialize ("Hm'" with "Hwp").
        iRename "Hm'" into "Hde2".
Dan Frumin's avatar
Dan Frumin committed
630
631
        iApply (a_bin_op_spec with "Hde1 Hde2");  fold dcexpr_interp.
        iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
632
        iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
        iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w ?) "H";
Dan Frumin's avatar
Dan Frumin committed
634
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
636
637
        { iApply (denv_interp_mono with "HmNew"); eauto. }
        iExists w. rewrite (dval_interp_mono E E') //.
        iSplit; first done. by iApply vcg_wp_continuation_mono.
638
    - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
639
      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
640
      iDestruct "Hex" as (E' dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)".
641
642
      destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
      + iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
643
644
      + rewrite Hpre. iExists (dval_interp E' dw); iSplit.
        iPureIntro. eapply dun_op_eval_correct. by rewrite Hop.
645
646
        iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
        eauto with iFrame.
647
648
649
      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
        iExists (dval_interp E' w). iSplit. iPureIntro.
        apply dun_op_eval_correct. by rewrite Hop.
650
651
652
653
        iExists E', w, m'. apply dun_op_eval_dUnknown_wf in Hop; last done.
        eauto with iFrame.
    - simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
      rewrite IHde1 //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
654
655
      iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp.
      iNext. iApply (awp_wand with "Hm").  iIntros (v) "Hex".
656
      iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl.
657
      rewrite denv_unlock_interp.
658
      iModIntro. rewrite IHde2 //. iSpecialize ("Hm" with "Hwp").
659
      specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre').
Léon Gondelman's avatar
Léon Gondelman committed
660
      intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
661
662
663
664
665
666
      iIntros (v1) "Hex".
      iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl.
      iExists Ef, dvf, mf; iSplit; first done. iSplit. iPureIntro. trans Enew ; done.
      iSplit; first done.
      iFrame. iPureIntro; done. eapply dcexpr_wf_mono in Hwf2.
      done. done. by apply denv_wf_unlock.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
    - by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
668
  Qed.
669
End vcg_spec.