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

Léon Gondelman's avatar
Léon Gondelman committed
58
  Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr)
Dan Frumin's avatar
Dan Frumin committed
59
       : option (denv * list denv * denv * dval) :=
60
    match de with
Dan Frumin's avatar
Dan Frumin committed
61
    | dCRet dv    => Some (mIn, mOut, [], dv)
62
    | dCLoad de1  =>
Dan Frumin's avatar
Dan Frumin committed
63
64
65
66
       ''(mIn1, mOut1, mNew, dl)       vcg_sp E mIn mOut de1;
       i                               is_dloc E dl;
       ''(mIn2, mOut2, mNew2, q, dv)   denv_delete_frac_3 i mIn1 mOut1 mNew;
       Some (mIn2, mOut2, denv_insert i ULvl q dv mNew2, dv)
67
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
68
69
70
71
72
       ''(mIn1, mOut1, mNew1, dl)  vcg_sp E mIn mOut de1;
       i                           is_dloc E dl;
       ''(mIn2, mOut2, mNew2, dv)  vcg_sp E mIn1 mOut1 de2;
       ''(mIn3, mOut3, mNew3, _)   denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2);
       Some (mIn3, mOut3, denv_insert i LLvl 1 dv mNew3, dv)
73
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
74
75
       ''(mIn1, mOut1, mNew1, dv1)  vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, mNew2, dv2)  vcg_sp E mIn1 mOut1 de2;
76
       match dbin_op_eval E op dv1 dv2 with
Dan Frumin's avatar
Dan Frumin committed
77
       | dSome dv => Some (mIn2, mOut2, denv_merge mNew1 mNew2, dv)
78
79
       | dNone | dUnknown _ => None
       end
80
    | dCUnOp op de =>
Dan Frumin's avatar
Dan Frumin committed
81
       ''(mIn1, mOut1, mNew1, dv)  vcg_sp E mIn mOut de;
82
       match dun_op_eval E op dv with
Dan Frumin's avatar
Dan Frumin committed
83
       | dSome dv' => Some (mIn1, mOut1, mNew1, dv')
84
85
       | dNone | dUnknown _ => None
       end
86
    | dCSeq de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
87
88
89
90
       ''(mIn1, mOut1, mNew1, _)    vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, mNew2, dv2)  vcg_sp E mIn1 (denv_unlock mNew1::mOut1) de2;
       ''(mOut3, mNew3)  popstack mOut2;
       Some (mIn2, mOut3, denv_merge mNew2 mNew3, dv2)
91
    | dCAlloc _ |  dCUnknown _ => None
92
93
    end.

Léon Gondelman's avatar
Léon Gondelman committed
94
95

  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
Léon Gondelman's avatar
Léon Gondelman committed
96
97
98
      (Φ : 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
99
100
101
         E' m' dv,
         v = dval_interp E' dv  
         E `prefix_of` E'  
102
103
         (denv_wf E' m') 
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
104
        denv_interp E' m' 
Léon Gondelman's avatar
Léon Gondelman committed
105
        (Φ E' m' dv)))%I.
Léon Gondelman's avatar
Léon Gondelman committed
106
107
  Arguments vcg_wp_unknown : simpl never.

108
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
Léon Gondelman's avatar
Léon Gondelman committed
109
      (Φ : denv  dval  iProp Σ) : iProp Σ :=
110
111
112
113
114
    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
115
116
117
118
         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)))
119
       end
Léon Gondelman's avatar
Léon Gondelman committed
120
121
122
    | _ => 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.
123
124

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
Léon Gondelman's avatar
Léon Gondelman committed
125
      (Φ : denv  dval  iProp Σ) : iProp Σ :=
126
127
128
129
130
    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
131
132
133
         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))
134
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    | _ =>
Léon Gondelman's avatar
Léon Gondelman committed
136
137
138
139
140
       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.
141
142

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

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

Section vcg_spec.
  Context `{amonadG Σ}.

Léon Gondelman's avatar
Léon Gondelman committed
198
199
  Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
    mapsto_wand_list_aux E m Φ k -
Dan Frumin's avatar
Dan Frumin committed
200
    ([ list] ndio  m, from_option
Léon Gondelman's avatar
Léon Gondelman committed
201
202
        (λ '{| 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
203
204
205
206
207
208
209
210
211
212
213
214
  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
215
216
  Lemma mapsto_wand_list_spec E m Φ :
    mapsto_wand_list E m Φ - denv_interp E m - Φ.
217
  Proof.
Dan Frumin's avatar
Dan Frumin committed
218
219
220
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
221

Dan Frumin's avatar
Dan Frumin committed
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
  Lemma vcg_sp_length E de mIn mOut mIn' mOut' mNew' dv :
    vcg_sp E mIn mOut de = Some (mIn', mOut', mNew', dv) 
    length mOut = length mOut'.
  Proof.
    revert mIn mOut mIn' mOut' mNew' dv. induction de;
    intros mIn mOut mIn' mOut' mNew' dv Hsp; simplify_eq/=; eauto.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hout; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (denv_delete_frac_3 i mIn1 mOut1 mNew1) as [[[[[mIn2 mOut2] mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde.
      + by eapply denv_delete_frac_3_length.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
      destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2)) as [[[[mIn3 mOut3] mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + transitivity (length mOut2). by eapply IHde2.
        by eapply denv_delete_full_3_length.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + by eapply IHde2.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde; simplify_eq/=.
      destruct (dun_op_eval E u dv1); simplify_eq/=.
      by eapply IHde.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
      destruct (vcg_sp E mIn1 (denv_unlock mNew1 :: mOut1) de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
      destruct mOut2; simplify_eq/=.
      transitivity (length mOut1).
      + by eapply IHde1.
      + apply IHde2 in Hde2. by simplify_eq/=.
  Qed.

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

Dan Frumin's avatar
Dan Frumin committed
359
360
  Lemma vcg_sp_correct E de m mIn mOut mNew dv R :
    vcg_sp E m [] de = Some (mIn, mOut, mNew, dv) 
Dan Frumin's avatar
Dan Frumin committed
361
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
362
    denv_interp E mIn  denv_interp E (denv_stack_merge mOut)  awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mNew).
Dan Frumin's avatar
Dan Frumin committed
363
  Proof.
364
    iIntros (Hsp) "Hm".
Dan Frumin's avatar
Dan Frumin committed
365
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
366
367
368
    pose (vcg_sp_length _ _ _ _ _ _ _ _ Hsp) as Hlen.
    assert (mOut = []) as -> by (destruct mOut; eauto; inversion Hlen).
    iFrame "Hawp". by rewrite /denv_interp //.
Dan Frumin's avatar
Dan Frumin committed
369
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
370

Dan Frumin's avatar
Dan Frumin committed
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
  Lemma denv_wf_stack_merge ms E :
    Forall (denv_wf E) ms 
    denv_wf E (denv_stack_merge ms).
  Proof.
    induction ms as [|m ms]; simpl; eauto. rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
    apply denv_wf_merge; eauto.
  Qed.

  Lemma vcg_sp_wf' E de mIn mOut mIn' mOut' mNew dv :
    denv_wf E mIn 
    Forall (denv_wf E) mOut 
    dcexpr_wf E de 
    vcg_sp E mIn mOut de = Some (mIn', mOut', mNew, dv) 
    denv_wf E mIn'  Forall (denv_wf E) mOut'  denv_wf E mNew  dval_wf E dv .
  Proof.
    revert mIn mOut mIn' mOut' mNew dv. induction de;
    intros mIn mOut mIn' mOut' mNew dv HwfIn HwfOut Hwfde Hsp; simplify_eq/=; eauto.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (denv_delete_frac_3 i mIn1 mOut1 mNew1) as [[[[[mIn2 mOut2] mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
      destruct (IHde _ _ _ _ _ _ HwfIn HwfOut Hwfde Hsp1) as (?&?&?&?).
Dan Frumin's avatar
Dan Frumin committed
393
394
395
      eapply denv_wf_delete_frac_3 in Hout1; eauto.
      destruct Hout1 as (?&?&?&?).
      repeat split; eauto using denv_wf_insert.
Dan Frumin's avatar
Dan Frumin committed
396
397
398
399
400
401
402
403
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [i|?]; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
      destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2)) as [[[[mIn3 mOut3] mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut1 Hwfde2 Hsp2) as (?&?&?&?).
Dan Frumin's avatar
Dan Frumin committed
404
405
406
407
      eapply denv_wf_delete_full_3 in Hout1; try eassumption.
      destruct Hout1 as (?&?&?&?).
      repeat split; eauto using denv_wf_insert.
      eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
      destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut1 Hwfde2 Hsp2) as (?&?&?&?).
      repeat split; eauto. apply denv_wf_merge; eauto.
      eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto.
    - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (IHde _ _ _ _ _ _ HwfIn HwfOut Hwfde Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
      destruct (dun_op_eval E u dv1) as [|?|?] eqn:Hop; simplify_eq/=.
      repeat split; eauto.
      eapply dun_op_eval_dSome_wf; eauto.
    - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
      destruct (vcg_sp E mIn1 (denv_unlock mNew1 :: mOut1) de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
      destruct mOut2; simplify_eq/=.
      apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
      destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
      assert (Forall (denv_wf E) (denv_unlock mNew1 :: mOut1)) as HwfOut2.
      { apply Forall_cons. split; eauto. by apply denv_wf_unlock. }
      destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut2 Hwfde2 Hsp2) as (?&Hall&?&?).
      apply Forall_cons in Hall. destruct Hall.
      repeat split; eauto using denv_wf_merge.
Dan Frumin's avatar
Dan Frumin committed
431
  Qed.
Dan Frumin's avatar
Dan Frumin committed
432

Dan Frumin's avatar
Dan Frumin committed
433
  Lemma vcg_sp_wf E de m mIn mOut mNew dv :
434
435
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
436
437
    vcg_sp E m [] de = Some (mIn, mOut, mNew, dv) 
    denv_wf E mIn  denv_wf E (denv_stack_merge mOut)  denv_wf E mNew  dval_wf E dv .
Dan Frumin's avatar
Dan Frumin committed
438
439
440
441
442
443
444
  Proof.
    intros Hm Hde Hsp.
    assert (Forall (denv_wf E) []) as Hout by econstructor.
    destruct (vcg_sp_wf' E de m [] mIn mOut mNew _ Hm Hout Hde Hsp) as (?&?&?&?).
    repeat split; eauto.
    by apply denv_wf_stack_merge.
  Qed.
445

446
  Lemma vcg_wp_unknown_correct R E m de Φ :
447
    denv_wf E m 
448
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
449
    vcg_wp_unknown R E de m Φ -
450
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
451
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
Léon Gondelman's avatar
Léon Gondelman committed
452
      denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
453
454
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
455
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
456
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
457
458
    iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
459
460
  Qed.

461
  Lemma vcg_wp_load_correct E m dv Φ :
462
    denv_wf E m 
463
    denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
464
    vcg_wp_load E dv m (Φ E) -
465
     (l:loc) q w, dval_interp E dv = #l  l C{q} w   (l C{q} w -
466
     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
467
      denv_wf E' m'  denv_interp E' m'  Φ E' m' dv').
468
469
470
  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
471
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
472
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
473
474
475
        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.
476
477
        rewrite Hm0. iSplit; first done.
        eapply denv_lookup_wf in Hlkp; eauto with iFrame.
478
479
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
480
481
        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.
482
        iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
483
        iExists E, (dValUnknown v'), []; repeat (iSplit; first done); iFrame.
484
485
486
        unfold denv_interp, denv_wf. eauto.
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
487
488
       iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
       iExists l, q, v'. iSplit; first done.
489
       iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
490
491
       iExists E, (dValUnknown v'), []; iSplit; first done.
       iFrame. unfold denv_interp, denv_wf. eauto.
492
493
  Qed.

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

519
  Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
520
   E0 `prefix_of` E 
521
522
   denv_wf E m 
   dval_wf E dv2 
523
   denv_interp E m -
Léon Gondelman's avatar
Léon Gondelman committed
524
   vcg_wp_store E dv1 dv2 m (Φ E) -
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
    (l : loc) (w : val), dval_interp E dv1 = #l 
     l C w  (l C[LLvl] dval_interp E dv2 -
527
          E' dv m', E0 `prefix_of` E'  dval_interp E' dv = dval_interp E dv2 
Léon Gondelman's avatar
Léon Gondelman committed
528
        dval_wf E' dv  denv_wf E' m'  denv_interp E' m'  Φ E' m' dv).
529
  Proof.
530
531
532
533
   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.
534
535
536
537
538
     +  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.
539
540
541
542
       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
543
       iDestruct "Hwp" as (dv_old) "[Hl Hwp]";
544
       iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
545
546
547
548
       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
549
550
     iDestruct "Hwp" as (l ->) "Hwp";
     iDestruct "Hwp" as (v) "[Hdv Hwp]";
551
     iExists l,v ; iSplit; first done. iFrame.
552
553
     iIntros "Hl". iSpecialize ("Hwp" with "Hl").
     iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
554
  Qed.
555

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

Léon Gondelman's avatar
Léon Gondelman committed
670
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
Dan Frumin's avatar
Dan Frumin committed
671
    MapstoListFromEnv Γs_in Γs_out Γls 
672
    E = penv_to_known_locs Γls 
Léon Gondelman's avatar
Léon Gondelman committed
673
    dcexpr_wf E de 
674
    denv_wf (penv_to_known_locs Γls) m 
675
    ListOfMapsto Γls E m 
Léon Gondelman's avatar
Léon Gondelman committed
676
    IntoDCexpr E e de 
677
    environments.envs_entails (environments.Envs Γp Γs_out c)
Léon Gondelman's avatar
Léon Gondelman committed
678
679
      (vcg_wp E m de R (λ E m dv,
        mapsto_wand_list E m (Φ (dval_interp E dv)))) 
680
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
681
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
682
    rewrite /IntoDCexpr /=. intros Hsplit ->.
683
    rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
Léon Gondelman's avatar
Léon Gondelman committed
684
685
686
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
    rewrite (vcg_wp_correct R); last done.
687
    iIntros (->) "H1 H2".
Léon Gondelman's avatar
Léon Gondelman committed
688
    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
689
    iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & % & % & Hm & Hwp)".
690
691
    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
   Qed.
692
End vcg_spec.