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

Dan Frumin's avatar
Dan Frumin committed
51
52
53
54
55
56
57

  Definition popstack (mOut : list denv) : option (list denv * denv) :=
    match mOut with
    | [] => None
    | m::ms => Some (ms, m)
    end.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
  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
98
99

  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
Léon Gondelman's avatar
Léon Gondelman committed
100
101
102
      (Φ : known_locs  denv  dval  iProp Σ) : iProp Σ :=
    mapsto_wand_list E m
      (awp (dcexpr_interp E de) R (λ v,
Léon Gondelman's avatar
Léon Gondelman committed
103
104
105
         E' m' dv,
         v = dval_interp E' dv  
         E `prefix_of` E'  
106
107
         (denv_wf E' m') 
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
108
        denv_interp E' m' 
Léon Gondelman's avatar
Léon Gondelman committed
109
        (Φ E' m' dv)))%I.
Léon Gondelman's avatar
Léon Gondelman committed
110
111
  Arguments vcg_wp_unknown : simpl never.

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

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

  Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
Léon Gondelman's avatar
Léon Gondelman committed
147
      (m : denv) (Φ : denv  dval  iProp Σ) : iProp Σ :=
148
149
    match dbin_op_eval E op dv1 dv2 with
    | dSome dw => Φ m dw
150
    | dUnknown (Some dw) => Φ m dw
Léon Gondelman's avatar
Léon Gondelman committed
151
152
    | _ => False
    end%I.
153
154

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

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
202
203
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
204
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
205
206
        (λ '{| 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
207
208
209
210
211
212
213
214
215
216
217
218
  Proof.
    generalize dependent k.
    induction m; simpl. eauto.
    iIntros (k) "H1 [Hl H2]".
    destruct a as [[x q dv]|]; simpl.
    - rewrite -plus_n_O. iSpecialize ("H1" with "Hl").
      iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
    - iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
  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/=.
Dan Frumin's avatar
Dan Frumin committed
251
      transitivity (length ms1).
Dan Frumin's avatar
Dan Frumin committed
252
253
      + by eapply IHde1.
      + by eapply IHde2.
Dan Frumin's avatar
Dan Frumin committed
254
    - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
255
256
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
Dan Frumin's avatar
Dan Frumin committed
257
258
259
260
    - 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
261
262
263
264
      + by eapply IHde1.
      + apply IHde2 in Hde2. by simplify_eq/=.
  Qed.

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

Dan Frumin's avatar
Dan Frumin committed
363
364
  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
365
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
366
    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
367
  Proof.
368
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
369
370
371
372
373
    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
374
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
375

Dan Frumin's avatar
Dan Frumin committed
376
377
378
379
  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
380
  Proof.
Dan Frumin's avatar
Dan Frumin committed
381
382
383
384
385
386
387
388
    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
389
390
  Qed.

Dan Frumin's avatar
Dan Frumin committed
391
392
  Lemma vcg_sp_wf' E de ms ms' mNew dv :
    Forall (denv_wf E) ms 
Dan Frumin's avatar
Dan Frumin committed
393
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
394
395
    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
396
  Proof.
Dan Frumin's avatar
Dan Frumin committed
397
398
399
    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
400
401
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
402
403
404
405
      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
406
      repeat split; eauto using denv_wf_insert.
Dan Frumin's avatar
Dan Frumin committed
407
    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
408
409
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
410
411
      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
412
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
413
414
415
416
      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
417
418
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
419
420
    - 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
421
422
      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
423
424
      destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
Dan Frumin's avatar
Dan Frumin committed
425
426
      repeat split; eauto. apply denv_wf_merge; eauto.
      eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
427
428
    - 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
429
430
431
      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
432
433
434
    - 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
435
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
Dan Frumin's avatar
Dan Frumin committed
436
437
      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
438
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
Dan Frumin's avatar
Dan Frumin committed
439
      destruct (IHde2 _ _ _ _ Hwfms2 Hwfde2 Hsp2) as (Hall&?&?).
Dan Frumin's avatar
Dan Frumin committed
440
441
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
442
  Qed.
Dan Frumin's avatar
Dan Frumin committed
443

Dan Frumin's avatar
Dan Frumin committed
444
  Lemma vcg_sp'_wf E de m m' mNew dv :
445
446
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
447
448
    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
449
  Proof.
Dan Frumin's avatar
Dan Frumin committed
450
451
452
453
454
455
456
457
    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
458
  Qed.
459

460
  Lemma vcg_wp_unknown_correct R E m de Φ :
461
    denv_wf E m 
462
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
463
    vcg_wp_unknown R E de m Φ -
464
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
465
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
Léon Gondelman's avatar
Léon Gondelman committed
466
      denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
467
468
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
469
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
470
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
471
472
    iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
473
474
  Qed.

475
  Lemma vcg_wp_load_correct E m dv Φ :
476
    denv_wf E m 
477
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
478
    vcg_wp_load E dv m (Φ E) -
479
     (l:loc) q w, dval_interp E dv = #l  l C{q} w   (l C{q} w -
480
     E' dv' m', E `prefix_of` E'  dval_interp E' dv' = w  dval_wf E' dv' 
Léon Gondelman's avatar
Léon Gondelman committed
481
      denv_wf E' m'  denv_interp E' m'  Φ E' m' dv').
482
483
484
  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
485
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
486
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
487
488
489
        iExists (dloc_interp E (dLoc i)), q,  (dval_interp E dv').
        iSplit. simplify_eq /=; done. iFrame. iIntros "Hl".
        iExists E, dv', m; iSplit; first done. iFrame.
490
491
        rewrite Hm0. iSplit; first done.
        eapply denv_lookup_wf in Hlkp; eauto with iFrame.
492
493
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
494
495
        iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
        iExists (dloc_interp E (dLoc i)), q, v'. iSplit; first done.
496
        iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
497
        iExists E, (dValUnknown v'), []; repeat (iSplit; first done); iFrame.
498
499
500
        unfold denv_interp, denv_wf. eauto.
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
501
502
       iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
       iExists l, q, v'. iSplit; first done.
503
       iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
504
505
       iExists E, (dValUnknown v'), []; iSplit; first done.
       iFrame. unfold denv_interp, denv_wf. eauto.
506
507
  Qed.

508
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
509
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
510
511
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
512
    vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E) -
513
514
    denv_interp E mOut -
     w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
515
     ( E' dv m', E0 `prefix_of` E'  dval_interp E' dv = w  dval_wf E' dv 
Léon Gondelman's avatar
Léon Gondelman committed
516
                  denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
517
  Proof.
518
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
519
    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
520
    * iExists (dval_interp E dw); iSplit.
521
522
      { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, (denv_merge mOut m).
523
524
      apply dbin_op_eval_dSome_wf in Hbin; try done.
      rewrite -denv_merge_interp //. eauto with iFrame.
525
526
    * destruct dw as [dw1|] eqn:Hdw; last done.
      iExists  (dval_interp E dw1); iSplit.
527
      iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
528
      iExists E, dw1, (denv_merge mOut m).
529
530
      rewrite -denv_merge_interp.
      apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
531
  Qed.
532

533
  Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
534
   E0 `prefix_of` E 
535
536
   denv_wf E m 
   dval_wf E dv2 
537
   denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
538
   vcg_wp_store E dv1 dv2 m (Φ E) -
Robbert Krebbers's avatar
Robbert Krebbers committed
539
540
    (l : loc) (w : val), dval_interp E dv1 = #l 
     l C w  (l C[LLvl] dval_interp E dv2 -
541
          E' dv m', E0 `prefix_of` E'  dval_interp E' dv = dval_interp E dv2 
Léon Gondelman's avatar
Léon Gondelman committed
542
        dval_wf E' dv  denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
543
  Proof.
544
545
546
547
   iIntros (Hpre 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.
548
549
550
551
552
     +  iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old); iSplit; first done.
        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.
553
554
555
556
       by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
       rewrite -denv_insert_interp. iFrame.
     + rewrite mapsto_wand_list_spec.
       iSpecialize ("Hwp" with "[Hm]"); iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
557
       iDestruct "Hwp" as (dv_old) "[Hl Hwp]";
558
       iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
559
560
561
562
       iIntros "Hl". iSpecialize ("Hwp" with "Hl").
       iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
   - rewrite mapsto_wand_list_spec.
     iSpecialize ("Hwp" with "[Hm]"); iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
563
564
     iDestruct "Hwp" as (l ->) "Hwp";
     iDestruct "Hwp" as (v) "[Hdv Hwp]";
565
     iExists l,v ; iSplit; first done. iFrame.
566
567
     iIntros "Hl". iSpecialize ("Hwp" with "Hl").
     iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
568
  Qed.
569

Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
572
  (* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the
  conjunctions in the same order. *)
  Lemma vcg_wp_correct R E m de Φ :
573
    dcexpr_wf E de 
574
    denv_wf E m 
575
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
576
    vcg_wp E m de R Φ -
577
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
578
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
Léon Gondelman's avatar
Léon Gondelman committed
579
      denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
580
  Proof.
581
582
583
584
    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.
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
585
    - rewrite IHde //. iRename "Hm" into "Hawp".
586
587
      iSpecialize ("Hawp" with "Hwp"); simpl.
      iApply (a_load_spec_exists_frac with "[Hawp]").  iApply (awp_wand with "Hawp").
588
589
      iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <- Hm'wf Hwf2) "(Hm & Hwp)".
      iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done.
Léon Gondelman's avatar
Léon Gondelman committed
590
591
      iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
      iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
592
593
594
      iSpecialize ("Hwp" with "Hl").
      iDestruct "Hwp" as (Ef dvf mf Hpre' <- Hwf3 Hwf4) "(Hmf & Hwp)".
      iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro; trans E'. done.
595
    - rewrite{1} /vcg_wp; fold vcg_wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
596
      simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
597
598
      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.
599
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
600
601
        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
602
        clear Heqsp2 Heqsp.
Dan Frumin's avatar
Dan Frumin committed
603
        iDestruct (IHde1 with "Hm' Hwp") as "Hde1"; try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
Dan Frumin's avatar
Dan Frumin committed
605
        iDestruct 1 as (E' dw m1 ? <- ?) "(% & Hm' & H)". iIntros "[-> HmNew]".
606
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
607
        iApply (vcg_wp_store_correct with "[-H] H");
608
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
609
        rewrite -!denv_merge_interp. iFrame "Hm'".
Dan Frumin's avatar
Dan Frumin committed
610
611
612
613
        rewrite -!(denv_interp_mono E E'); eauto.
      + 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.
614
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
Dan Frumin's avatar
Dan Frumin committed
615
        iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m1 ? <- ?) "(% & Hm' & H)".
Robbert Krebbers's avatar
Robbert Krebbers committed
616
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
617
        iApply (vcg_wp_store_correct with "[-H] H");
Robbert Krebbers's avatar
Robbert Krebbers committed
618
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Léon Gondelman's avatar
Léon Gondelman committed
619
        rewrite -!denv_merge_interp. iFrame "Hm'".
Dan Frumin's avatar
Dan Frumin committed
620
        rewrite -!(denv_interp_mono E E'); eauto.
Léon Gondelman's avatar
Léon Gondelman committed
621
    - rewrite{1} /vcg_wp; fold vcg_wp.
622
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
623
624
      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.
625
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
626
627
628
629
630
631
        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
632
        iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
Dan Frumin's avatar
Dan Frumin committed
633
        iDestruct "Hex" as (E' dv1 m1 Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
634
        rewrite (dval_interp_mono E E' dv2); eauto.
Dan Frumin's avatar
Dan Frumin committed
635
636
        iPoseProof (denv_interp_mono with "Hm'") as "Hm'"; [done | done |].
        iApply (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]");
Dan Frumin's avatar
Dan Frumin committed
637
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
638
639
640
641
642
643
        iApply (denv_interp_mono with "HmNew"); eauto.
      + 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
644
645
        iApply (a_bin_op_spec with "Hde1 Hde2");  fold dcexpr_interp.
        iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
Dan Frumin's avatar
Dan Frumin committed
646
        iDestruct "Hex" as (E' dv2 m2 Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
647
        rewrite (dval_interp_mono E E' dv1); eauto.
Dan Frumin's avatar
Dan Frumin committed
648
649
        iPoseProof (denv_interp_mono with "Hm'") as "Hm'"; [done | done |].
        iApply (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]");
Dan Frumin's avatar
Dan Frumin committed
650
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
651
        iApply (denv_interp_mono with "HmNew"); eauto.
652
    - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
653
      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
654
      iDestruct "Hex" as (E' dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)".
655
656
657
658
      destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
      + iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
      + iExists (dval_interp E' dw); iSplit.
        iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
659
660
        iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
        eauto with iFrame.
661
662
663
      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
        iExists (dval_interp E' w). iSplit. iPureIntro.
        apply dun_op_eval_correct. by rewrite Hop.
664
665
666
667
        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.
668
669
670
      iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
      iApply (awp_wand with "Hm").  iIntros (v) "Hex".
671
      iDestruct "Hex" as (Enew dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)". simpl.
672
      rewrite denv_unlock_interp.
673
674
      iModIntro. rewrite IHde2 //. awp_seq. iSpecialize ("Hm" with "Hwp").
      specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre).
Léon Gondelman's avatar
Léon Gondelman committed
675
676
677
      intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
      iIntros (v) "Hex".
      iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
678
      iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
679
      iFrame. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock.
680
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
681
 Qed.
682

Léon Gondelman's avatar
Léon Gondelman committed
683
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
Dan Frumin's avatar
Dan Frumin committed
684
    MapstoListFromEnv Γs_in Γs_out Γls 
685
    E = penv_to_known_locs Γls 
Léon Gondelman's avatar
Léon Gondelman committed
686
    dcexpr_wf E de 
687
    denv_wf (penv_to_known_locs Γls) m 
688
    ListOfMapsto Γls E m 
Léon Gondelman's avatar
Léon Gondelman committed
689
    IntoDCexpr E e de 
690
    environments.envs_entails (environments.Envs Γp Γs_out c)
Léon Gondelman's avatar
Léon Gondelman committed
691
692
      (vcg_wp E m de R (λ E m dv,
        mapsto_wand_list E m (Φ (dval_interp E dv)))) 
693
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
694
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
695
    rewrite /IntoDCexpr /=. intros Hsplit ->.
696
    rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
Léon Gondelman's avatar
Léon Gondelman committed
697
698
699
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
    rewrite (vcg_wp_correct R); last done.
700
    iIntros (->) "H1 H2".