vcgen.v 35.1 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
From iris.heap_lang Require Export proofmode notation.
2
From iris.algebra Require Import frac.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.bi Require Import big_op.
4
From iris_c.vcgen Require Import dcexpr splitenv denv.
Dan Frumin's avatar
Dan Frumin committed
5
6
7
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

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

11
[DONE] Fix all the unknown cases, introduce a function for that (which should be
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
  simpl never)
- Write more tests with unknown stuff in it
14
  add tests like `!(l := 10;;;; l)`
Robbert Krebbers's avatar
Robbert Krebbers committed
15
- 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
18
19
20
21
22
23
24
25
26
27
28
- Finish the proofs
- Maybe drop `wp_expr`? We are not taking it as an input of anything anymore

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 Σ}.

40
41
  (** Deep embedding of formulae used to build the verification condition generator *)

42
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
43
    | Base : iProp Σ  wp_expr
44
45
    | MapstoStar : dloc  (frac  dval  wp_expr)  wp_expr
    | MapstoStarFull : dloc  (dval  wp_expr)  wp_expr
46
    | MapstoWand : dloc  dval  lvl  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
47
48
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
49
    | UMod : wp_expr  wp_expr.
50

51
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
52

53
  Fixpoint wp_interp (E : known_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
54
55
    match a with
    | Base Φ => Φ
56
    | MapstoStar dl Φ =>
57
        q v, dloc_interp E dl C{q} v  wp_interp E (Φ q (dValUnknown v))
58
    | MapstoStarFull dl Φ =>
59
        v, dloc_interp E dl C{1} v  wp_interp E (Φ (dValUnknown v))
60
    | MapstoWand dl dv x q Φ =>
61
       dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp E Φ
Dan Frumin's avatar
Dan Frumin committed
62
    | IsSome dmx Φ  =>
63
        x, doption_interp dmx = Some x  wp_interp E (Φ x)
Dan Frumin's avatar
Dan Frumin committed
64
    | IsLoc dv Φ =>
65
66
        l : loc, dval_interp E dv = #l  wp_interp E (Φ (dLocUnknown l))
    | UMod P => U (wp_interp E P)
67
    end%I.
Dan Frumin's avatar
Dan Frumin committed
68

69
  Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
70
    match m with
71
    | [] => Φ
72
73
74
    | None :: m' => mapsto_wand_list_aux m' Φ (S i)
    | Some (DenvItem x q dv) :: m' =>
       MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
75
76
    end.

77
78
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
79

Dan Frumin's avatar
Dan Frumin committed
80
81
82
83
84
85
86
87
88

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

  Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr) 
       : option (denv * list denv * denv * dval) :=
89
    match de with
Dan Frumin's avatar
Dan Frumin committed
90
    | dCRet dv    => Some (mIn, mOut, [], dv)
91
    | dCLoad de1  =>
Dan Frumin's avatar
Dan Frumin committed
92
93
94
95
       ''(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)
96
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
97
98
99
100
101
       ''(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)
102
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
103
104
       ''(mIn1, mOut1, mNew1, dv1)  vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, mNew2, dv2)  vcg_sp E mIn1 mOut1 de2;
105
       match dbin_op_eval E op dv1 dv2 with
Dan Frumin's avatar
Dan Frumin committed
106
       | dSome dv => Some (mIn2, mOut2, denv_merge mNew1 mNew2, dv)
107
108
       | dNone | dUnknown _ => None
       end
109
    | dCUnOp op de =>
Dan Frumin's avatar
Dan Frumin committed
110
       ''(mIn1, mOut1, mNew1, dv)  vcg_sp E mIn mOut de;
111
       match dun_op_eval E op dv with
Dan Frumin's avatar
Dan Frumin committed
112
       | dSome dv' => Some (mIn1, mOut1, mNew1, dv')
113
114
       | dNone | dUnknown _ => None
       end
115
    | dCSeq de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
116
117
118
119
       ''(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)
120
    | dCAlloc _ |  dCUnknown _ => None
121
122
    end.

Léon Gondelman's avatar
Léon Gondelman committed
123
124
125
126
127
128
129
130

  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
      (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
    mapsto_wand_list m $ Base $
      awp (dcexpr_interp E de) R (λ v,
         E' m' dv,
         v = dval_interp E' dv  
         E `prefix_of` E'  
131
132
         (denv_wf E' m') 
         dval_wf E' dv  
Léon Gondelman's avatar
Léon Gondelman committed
133
        denv_interp E' m' 
134
        wp_interp E' (Φ E' m' dv))%I.
Léon Gondelman's avatar
Léon Gondelman committed
135
136
  Arguments vcg_wp_unknown : simpl never.

137
138
139
140
141
142
143
144
145
146
  Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
      (Φ : denv  dval  wp_expr) : wp_expr :=
    match is_dloc E dv with
    | Some i =>
       match denv_lookup i m with
       | Some (_, dw) => Φ m dw
       | None =>
          mapsto_wand_list m $ MapstoStar (dLoc i) $ λ q dw,
            MapstoWand (dLoc i) dw ULvl q (Φ [] dw)
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
149
150
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
151
152
153
154
155
156
157
158
159
160
161
162
    end.

  Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
      (Φ : denv  dval  wp_expr) : wp_expr :=
    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 =>
          mapsto_wand_list m $ MapstoStarFull (dLoc i) $ λ _,
            MapstoWand (dLoc i) dv2 LLvl 1 (Φ [] dv2)
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
167
168
169
170
171
172
    end.

  Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
      (m : denv) (Φ : denv  dval  wp_expr) : wp_expr :=
    match dbin_op_eval E op dv1 dv2 with
    | dSome dw => Φ m dw
173
174
    | dUnknown (Some dw) => Φ m dw
    | _ => Base False
175
176
177
    end.

  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
178
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
179
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
180
    | dCRet dv => Φ E m dv
181
    | dCLoad de1 =>
182
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' (Φ E))
183
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
184
       match vcg_sp E m [] de1 with
Dan Frumin's avatar
Dan Frumin committed
185
       | Some (mIn, mOut, mNew, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
186
          vcg_wp E mIn de2 R (λ E mIn dv2,
Dan Frumin's avatar
Dan Frumin committed
187
            vcg_wp_store E dv1 dv2 (denv_merge (denv_merge mNew (denv_stack_merge mOut)) mIn) (Φ E))
188
       | None =>
Dan Frumin's avatar
Dan Frumin committed
189
          match vcg_sp E m [] de2 with
Dan Frumin's avatar
Dan Frumin committed
190
          | Some (mIn, mOut, mNew, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
191
             vcg_wp E mIn de1 R (λ E mIn dv1,
Dan Frumin's avatar
Dan Frumin committed
192
               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
193
          | None => vcg_wp_unknown R E de m Φ
194
195
196
          end
        end
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
197
       match vcg_sp E m [] de1 with
Dan Frumin's avatar
Dan Frumin committed
198
       | Some (mIn, mOut, mNew, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
          vcg_wp E mIn de2 R (λ E mIn dv2,
Dan Frumin's avatar
Dan Frumin committed
200
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E))
201
       | None =>
Dan Frumin's avatar
Dan Frumin committed
202
          match vcg_sp E m [] de2 with
Dan Frumin's avatar
Dan Frumin committed
203
          | Some (mIn, mOut, mNew, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
204
             vcg_wp E mIn de1 R (λ E mIn dv1,
Dan Frumin's avatar
Dan Frumin committed
205
               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
206
          | None => vcg_wp_unknown R E de m Φ
207
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
208
       end
209
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
210
       vcg_wp E m de R (λ E m dv,
211
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
214
215
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
216
       vcg_wp E m de1 R (λ E m _,
217
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
218
    | _ => vcg_wp_unknown R E de m Φ
219
    end.
220
221
222
223
224
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

Dan Frumin's avatar
Dan Frumin committed
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
  Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
    wp_interp E (mapsto_wand_list_aux m t k) -
    ([ list] ndio  m, from_option
                              (λ '{| 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) -
    wp_interp E t.
  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.

243
244
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
245
  Proof.
Dan Frumin's avatar
Dan Frumin committed
246
247
248
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
249

Dan Frumin's avatar
Dan Frumin committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
  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'))).
  Proof.
296
  Proof.
Dan Frumin's avatar
Dan Frumin committed
297
298
299
300
    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
301
    - specialize (IHde mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
302
      destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
303
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
304
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
305
      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
306
      rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]".
Dan Frumin's avatar
Dan Frumin committed
307
308
309
310
      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
311
312
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Dan Frumin's avatar
Dan Frumin committed
313
314
315
      iIntros (?) "[% HmNew1]". simplify_eq/=.
      iExists _, _. iSplit; eauto. iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
      iIntros "Hl". iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
316
      rewrite -denv_insert_interp.
Léon Gondelman's avatar
Léon Gondelman committed
317
      by iFrame.
Dan Frumin's avatar
Dan Frumin committed
318
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
319
      destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
320
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
321
      destruct d as [i|?]; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
322
323
324
325
      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
326
327
      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
328
329
330
331
332
333
334
335
336
337
338
339
      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.
      iDestruct ("Hl" with "[$HmNew1 $HmNew2]") as "[$ $]". 
      iIntros "Hl". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
340
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
341
342
343
      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 /=.
344
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
345
      rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
Léon Gondelman's avatar
Léon Gondelman committed
346
      rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
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]".
Léon Gondelman's avatar
Léon Gondelman committed
349
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Dan Frumin's avatar
Dan Frumin committed
350
      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
351
      iExists (dval_interp E dv). repeat iSplit; eauto.
352
      + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
353
      + rewrite -denv_merge_interp. iFrame.
Dan Frumin's avatar
Dan Frumin committed
354
    - specialize (IHde mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
355
      destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
356
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
357
      rewrite IHde; last done. iDestruct "HmIn" as "[$ Hawp]".
Dan Frumin's avatar
Dan Frumin committed
358
359
      iApply (denv_stack_interp_mono with "Hawp").
      iIntros "Hawp".
360
361
362
363
      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
364
    - specialize (IHde1 mIn mOut).
Dan Frumin's avatar
Dan Frumin committed
365
366
367
      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
368
      rewrite IHde1; last done. iDestruct "HmIn" as "[HmIn1 Hawp1]".
Dan Frumin's avatar
Dan Frumin committed
369
      rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2 Hawp2]".
Dan Frumin's avatar
Dan Frumin committed
370
      (* TODO: wtf? *)
Dan Frumin's avatar
Dan Frumin committed
371
      assert (AsVal (λ: <>, dcexpr_interp E de2)).
372
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
Dan Frumin's avatar
Dan Frumin committed
373
374
375
376
377
378
379
      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
380
      iApply a_sequence_spec. iApply (awp_wand with "Hawp1").
Dan Frumin's avatar
Dan Frumin committed
381
382
383
384
385
386
387
      iIntros (?) "[% HmNew1]".
      rewrite (denv_unlock_interp E mNew1).
      (* rewrite (denv_unlock_interp E (denv_stack_merge mOut1)). *)
      iModIntro. 
      awp_seq. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
      iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]". rewrite -denv_merge_interp.
      iSplit; eauto. iFrame.
388
  Qed.
Dan Frumin's avatar
Dan Frumin committed
389

Dan Frumin's avatar
Dan Frumin committed
390
391
  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
392
    denv_interp E m -
Dan Frumin's avatar
Dan Frumin committed
393
    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
394
395
396
  Proof.
    iIntros (?) "Hm".
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
Dan Frumin's avatar
Dan Frumin committed
397
398
399
    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
400
  Qed.
Dan Frumin's avatar
Dan Frumin committed
401
  
Dan Frumin's avatar
Dan Frumin committed
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
  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
424
425
426
      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
427
428
429
430
431
432
433
434
    - 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
435
436
437
438
      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
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
    - 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
462
  Qed.
Dan Frumin's avatar
Dan Frumin committed
463

Dan Frumin's avatar
Dan Frumin committed
464
  Lemma vcg_sp_wf E de m mIn mOut mNew dv :
465
466
    denv_wf E m 
    dcexpr_wf E de 
Dan Frumin's avatar
Dan Frumin committed
467
468
    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
469
470
471
472
473
474
475
  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.
476

477
  Lemma vcg_wp_unknown_correct R E m de Φ :
478
    denv_wf E m 
479
480
    denv_interp E m -
    wp_interp E (vcg_wp_unknown R E de m Φ) -
481
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
482
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
483
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
484
485
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
486
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
487
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
488
489
    iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
490
491
  Qed.

492
  Lemma vcg_wp_load_correct E m dv Φ :
493
    denv_wf E m 
494
495
496
    denv_interp E m -
    wp_interp E (vcg_wp_load E dv m (Φ E)) -
     (l:loc) q w, dval_interp E dv = #l  l C{q} w   (l C{q} w -
497
     E' dv' m', E `prefix_of` E'  dval_interp E' dv' = w  dval_wf E' dv' 
498
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv')).
499
500
501
  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
502
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
503
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
504
505
506
        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.
507
508
        rewrite Hm0. iSplit; first done.
        eapply denv_lookup_wf in Hlkp; eauto with iFrame.
509
510
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
511
512
        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.
513
        iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
514
        iExists E, (dValUnknown v'), []; repeat (iSplit; first done); iFrame.
515
516
517
        unfold denv_interp, denv_wf. eauto.
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
518
519
       iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
       iExists l, q, v'. iSplit; first done.
520
       iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
521
522
       iExists E, (dValUnknown v'), []; iSplit; first done.
       iFrame. unfold denv_interp, denv_wf. eauto.
523
524
  Qed.

525
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
526
    E0 `prefix_of` E  dval_wf E dv1  dval_wf E dv2 
527
528
529
530
531
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
    wp_interp E (vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E)) -
    denv_interp E mOut -
     w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
532
     ( E' dv m', E0 `prefix_of` E'  dval_interp E' dv = w  dval_wf E' dv 
533
534
                  denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
535
    iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
536
    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
537
    * iExists (dval_interp E dw); iSplit.
538
539
      { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, (denv_merge mOut m).
540
541
      apply dbin_op_eval_dSome_wf in Hbin; try done.
      rewrite -denv_merge_interp //. eauto with iFrame.
542
543
    * destruct dw as [dw1|] eqn:Hdw; last done.
      iExists  (dval_interp E dw1); iSplit.
544
      iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
545
      iExists E, dw1, (denv_merge mOut m).
546
547
      rewrite -denv_merge_interp.
      apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
548
  Qed.
549

550
  Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
551
   E0 `prefix_of` E 
552
553
   denv_wf E m 
   dval_wf E dv2 
554
   denv_interp E m -
555
   wp_interp E (vcg_wp_store E dv1 dv2 m (Φ E)) -
Robbert Krebbers's avatar
Robbert Krebbers committed
556
557
    (l : loc) (w : val), dval_interp E dv1 = #l 
     l C w  (l C[LLvl] dval_interp E dv2 -
558
          E' dv m', E0 `prefix_of` E'  dval_interp E' dv = dval_interp E dv2 
559
560
        dval_wf E' dv  denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
561
562
563
564
   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.
565
566
567
568
569
     +  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.
570
571
572
573
574
       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.
       iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; fold wp_interp.
575
       iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
576
577
578
579
       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.
580
581
582
     iDestruct "Hwp" as (l ->) "Hwp"; fold wp_interp.
     iDestruct "Hwp" as (v) "[Hdv Hwp]"; fold wp_interp.
     iExists l,v ; iSplit; first done. iFrame.
583
584
     iIntros "Hl". iSpecialize ("Hwp" with "Hl").
     iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
585
  Qed.
586

Robbert Krebbers's avatar
Robbert Krebbers committed
587
588
589
  (* 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 Φ :
590
    dcexpr_wf E de 
591
    denv_wf E m 
592
593
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
594
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
595
      E `prefix_of` E'  dval_interp E' dv = v  dval_wf E' dv 
596
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
597
  Proof.
598
599
600
601
    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").
602
    - rewrite IHde //. iRename "Hm" into "Hawp".
603
604
      iSpecialize ("Hawp" with "Hwp"); simpl.
      iApply (a_load_spec_exists_frac with "[Hawp]").  iApply (awp_wand with "Hawp").
605
606
      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
607
608
      iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
      iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
609
610
611
      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.
612
    - rewrite{1} /vcg_wp; fold vcg_wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
      simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
614
615
      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.
616
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
617
618
        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
619
620
621
        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
622
        iDestruct 1 as (E' dw m' ? <- ?) "(% & Hm' & H)". iIntros "[-> HmNew]".
623
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
624
        iApply (vcg_wp_store_correct with "[-H] H");
625
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
626
627
628
629
        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.
630
631
        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
632
        iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m' ? <- ?) "(% & Hm' & H)".
Robbert Krebbers's avatar
Robbert Krebbers committed
633
        rewrite (dval_interp_mono E E') //.
Dan Frumin's avatar
Dan Frumin committed
634
        iApply (vcg_wp_store_correct with "[-H] H");
Robbert Krebbers's avatar
Robbert Krebbers committed
635
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
Dan Frumin's avatar
Dan Frumin committed
636
637
        rewrite -!denv_merge_interp. iFrame "Hm'". 
        rewrite -!(denv_interp_mono E E'); eauto. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
638
    - rewrite{1} /vcg_wp; fold vcg_wp.
639
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
Dan Frumin's avatar
Dan Frumin committed
640
641
      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.
642
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Dan Frumin's avatar
Dan Frumin committed
643
644
645
        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.
646
        rewrite IHde1; [| done | done]. iSpecialize ("HmIn" with "Hwp").
Dan Frumin's avatar
Dan Frumin committed
647
648
        iApply (a_bin_op_spec with "HmIn Hde2"); fold dcexpr_interp.
        iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
649
        iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
650
        rewrite (dval_interp_mono E E' dv2); eauto.
651
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
Dan Frumin's avatar
Dan Frumin committed
652
653
654
655
656
657
658
        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.
659
660
        rewrite IHde2; [| done | done]. iSpecialize ("HmIn" with "Hwp").
        iRename "HmIn" into "Hde2".
Dan Frumin's avatar
Dan Frumin committed
661
662
        iApply (a_bin_op_spec with "Hde1 Hde2");  fold dcexpr_interp.
        iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
663
        iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
664
        rewrite (dval_interp_mono E E' dv1); eauto.
665
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
Dan Frumin's avatar
Dan Frumin committed
666
667
668
669
        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.
670
    - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
671
      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
672
      iDestruct "Hex" as (E' dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)".
673
674
675
676
      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.
677
678
        iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
        eauto with iFrame.
679
680
681
      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
        iExists (dval_interp E' w). iSplit. iPureIntro.
        apply dun_op_eval_correct. by rewrite Hop.
682
683
684
685
        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.
686
687
688
      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".
689
      iDestruct "Hex" as (Enew dv m' Hpre <- Hm'wf) "(% & Hm & Hwp)". simpl.
690
      rewrite denv_unlock_interp.
691
692
      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
693
694
695
      intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
      iIntros (v) "Hex".
      iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
696
      iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
697
      iFrame. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock.
698
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
699
 Qed.
700

Léon Gondelman's avatar
Léon Gondelman committed
701
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
Dan Frumin's avatar
Dan Frumin committed
702
    MapstoListFromEnv Γs_in Γs_out Γls 
703
    E = penv_to_known_locs Γls 
Léon Gondelman's avatar
Léon Gondelman committed
704
    dcexpr_wf E de 
705
    denv_wf (penv_to_known_locs Γls) m 
706
    ListOfMapsto Γls E m 
Léon Gondelman's avatar
Léon Gondelman committed
707
    IntoDCexpr E e de 
708
    environments.envs_entails (environments.Envs Γp Γs_out c)
709
      (wp_interp E (vcg_wp E m de R (λ E m dv,
710
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
711
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
712
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
713
    rewrite /IntoDCexpr /=. intros Hsplit ->.
714
    rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
Léon Gondelman's avatar
Léon Gondelman committed
715
716
717
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
    rewrite (vcg_wp_correct R); last done.
718
    iIntros (->) "H1 H2".
Léon Gondelman's avatar
Léon Gondelman committed
719
    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
720
    iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & % & % & Hm & Hwp)".
721
722
    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
   Qed.
723
End vcg_spec.
724

725
(* Arguments wp_interp : simpl never. *)
726

727
728
729
730
Ltac vcg_solver :=
  eapply tac_vcg_sound;
    [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
    | compute; reflexivity (*  E = penv_to_known_locs Γls *)
731
732
    |       (* dcexpr_wf E de *)
    |       (* denv_wf E m *)
733
734
    | apply _ (* ListOfMapsto Γls E m *)
    | apply _ (* IntoDCexpr E e dce *)
Léon Gondelman's avatar
Léon Gondelman committed
735
    | simpl ]; intuition.