vcgen.v 33.7 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
265
266
  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' 
     denv_stack_interp (reverse mOut) (reverse mOut') E
        (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
346
347
348
349
350
      unfold popstack in Hsp.
      destruct mOut2 as [|t mOut2'] eqn:Houteq; simplify_eq/=.
      iFrame "HmIn2". rewrite !reverse_cons.
      rewrite -denv_stack_interp_snoc; last first.
      { rewrite !reverse_length. apply vcg_sp_length in Hsp2. eauto. }
      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
351
      iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
352
353
354
      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
355
      iModIntro.
Dan Frumin's avatar
Dan Frumin committed
356
357
358
      awp_seq. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]". rewrite -denv_merge_interp.
      iSplit; eauto. iFrame.
359
  Qed.
Dan Frumin's avatar
Dan Frumin committed
360

Dan Frumin's avatar
Dan Frumin committed
361
362
  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
363
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
364
    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
365
366
367
  Proof.
    iIntros (?) "Hm".
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
368
369
370
    rewrite reverse_nil denv_stack_interp_nil_l.
    iDestruct "Hawp" as "[HmOut $]". iApply denv_stack_merge_interp.
    by iApply denv_stack_reverse.
Dan Frumin's avatar
Dan Frumin committed
371
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
372

Dan Frumin's avatar
Dan Frumin committed
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
  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
395
396
397
      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
398
399
400
401
402
403
404
405
    - 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
406
407
408
409
      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
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
    - 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
433
  Qed.
Dan Frumin's avatar
Dan Frumin committed
434

Dan Frumin's avatar
Dan Frumin committed
435
  Lemma vcg_sp_wf E de m mIn mOut mNew dv :
436
437
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
438
439
    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
440
441
442
443
444
445
446
  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.
447

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

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

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

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

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

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