vcgen.v 23.2 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
16
17
18
19
20
21
22
23
24
25
26
27
28
29
- Support alloc in `vcg_wp`
- Automatically come up with the new `E`, `m` and `dv` and stuff in the
  unknown case
- 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
30
31
32
33
34
35
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
36
37


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

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

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

53
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
54

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

70
  Fixpoint wp_interp_sane (E : known_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
71
72
    match a with
    | Base Φ => Φ
73
    | MapstoStar dl Φ =>
74
        q v, dloc_interp E dl C{q} v  wp_interp_sane E (Φ q (dValUnknown v))
75
    | MapstoStarFull dl Φ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
76
        v, dloc_interp E dl C{1} v  wp_interp_sane E (Φ (dValUnknown v))
77
    | MapstoWand dl dv x q Φ =>
78
       dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp_sane E Φ
Dan Frumin's avatar
Dan Frumin committed
79
    | IsSome dmx Φ  =>
80
        x, doption_interp dmx = Some x  wp_interp_sane E (Φ x)
Dan Frumin's avatar
Dan Frumin committed
81
    | IsLoc dv Φ =>
82
        l : loc, dval_interp E dv = #l  wp_interp_sane E (Φ (dLocUnknown l))
Dan Frumin's avatar
Dan Frumin committed
83
    | UMod P => U (wp_interp_sane E P)
84
    end%I.
Dan Frumin's avatar
Dan Frumin committed
85

86
  Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
87
    match m with
88
    | [] => Φ
89
90
    | dio :: m' =>
      match dio with
91
      | None => mapsto_wand_list_aux m' Φ (S i)
92
      | Some (DenvItem x q dv)  =>
93
         MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
94
      end
95
96
    end.

97
98
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
99

100
  Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
101
    match de with
102
103
    | dCRet dv    => Some (m, nil, dv)
    | dCLoad de1  =>
104
105
106
107
       ''(mIn, mOut, dl)       vcg_sp E m de1;
       i                       is_dloc E dl;
       ''(mIn1, mOut2, q, dv)  denv_delete_frac_2 i mIn mOut;
       Some (mIn1, denv_insert i ULvl q dv mOut2, dv)
108
    | dCStore de1 de2 =>
109
110
111
112
113
       ''(mIn1, mOut1, dl)  vcg_sp E m de1;
       i                    is_dloc E dl;
       ''(mIn2, mOut2, dv)  vcg_sp E mIn1 de2;
       ''(mIn3, mOut3, _)   denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2);
       Some (mIn3, denv_insert i LLvl 1 dv mOut3, dv)
114
    | dCBinOp op de1 de2 =>
115
116
117
118
119
120
       ''(mIn1, mOut1, dv1)  vcg_sp E m de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 de2;
       match dbin_op_eval E op dv1 dv2 with
       | dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
       | dNone | dUnknown _ => None
       end
121
    | dCUnOp op de =>
122
       ''(mIn, mOut, dv)  vcg_sp E m de;
123
124
125
126
       match dun_op_eval E op dv with
       | dSome dv' => Some (mIn, mOut, dv')
       | dNone | dUnknown _ => None
       end
127
    | dCSeq de1 de2 =>
128
129
130
       ''(mIn1, mOut1, _)    vcg_sp E m de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E (denv_unlock mIn1) de2;
       Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
131
    | dCAlloc _ |  dCUnknown _ => None
132
133
    end.

134
  (* TODO: change the fail though cases, in the same way as the unknown case
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  of vcg_wp. Also factor that out in a function vcg_unknown *)
136
137
138
139
140
141
142
143
144
145
  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
146
147
148
149
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
150
151
152
153
154
155
156
157
158
159
160
161
    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
162
163
164
165
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
166
167
168
169
170
171
172
173
174
175
    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
    | mdw => mapsto_wand_list m $ IsSome mdw (Φ [])
    end.

  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
176
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
177
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    | dCRet dv => Φ E m dv
179
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
180
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E))
181
182
183
    | dCStore de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
186
187
188
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
191
192
          | None =>
             mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
193
               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
194
195
196
197
198
          end
        end
    | dCBinOp op de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
201
202
203
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
206
207
          | None =>
             mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
208
               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
209
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
210
       end
211
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
212
       vcg_wp E m de R (λ E m dv,
213
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
216
217
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
218
       vcg_wp E m de1 R (λ E m _,
219
220
221
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
    | _ =>
       mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
225
226
227
         awp (dcexpr_interp E de) R (λ v,
            E' m' dv,
            v = dval_interp E' dv  
            E `prefix_of` E'  
           denv_interp E' m' 
           wp_interp_sane E' (Φ E' m' dv))%I
228
    end.
229
230
231
232
233
234
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

  Lemma wp_interp_sane_sound E a : wp_interp_sane E a  wp_interp E a.
235
  Proof.
236
237
238
    generalize dependent E.
    induction a.
    - done.
239
    - simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
240
      iExists q, (dValUnknown v). iFrame. by (iApply H0).
241
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
242
      iExists (dValUnknown v). simpl. iFrame. by (iApply H0).
243
244
245
246
247
248
    - simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
      iExists v. iFrame. by iApply H0.
    - simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
      iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
    - simpl. intros E. by apply U_mono.
249
  Qed.
250

251
252


253

254
255
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
256
  Proof.
257
258
  Admitted.
  (*  unfold env_ps_dv_interp.
259
260
261
262
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "H [H1 H2]".
      iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
263
  Qed. *)
264

265
266
  Lemma vcg_sp_correct E m de mIn mOut dv R :
    vcg_sp E m de = Some (mIn, mOut, dv) 
267
    denv_interp E m -
268
269
    denv_interp E mIn 
    awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mOut).
270
271
  Proof. Admitted.
  (*  revert m mIn mOut dv. induction de;
Léon Gondelman's avatar
Léon Gondelman committed
272
273
274
275
    iIntros (m mIn mOut dv Hsp) "Hm"; simplify_eq/=.
    - iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold denv_interp. done.
    - specialize (IHde m).
      destruct (vcg_sp E m de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
276
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
277
      destruct d as [i|?]; simplify_eq/=.
278
      destruct (denv_delete_frac i mIn1) as [[[mIn1' q] dv1]|] eqn:Hfar; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
279
280
281
282
      rewrite IHde; last done. iDestruct "Hm" as "[HmIn1 Hawp]".
      rewrite -denv_delete_frac_interp; last done.
      iDestruct "HmIn1" as "[HmIn Hl]".
      iFrame "HmIn".
Léon Gondelman's avatar
Léon Gondelman committed
283
284
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Léon Gondelman's avatar
Léon Gondelman committed
285
286
287
      iIntros (?) "[% HmOut1]". simplify_eq/=. iExists _, _. iSplit; eauto.
      iFrame "Hl". iIntros "Hl". iSplit; eauto.
      rewrite denv_insert_interp.
Léon Gondelman's avatar
Léon Gondelman committed
288
      by iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
289
290
    - specialize (IHde1 m).
      destruct (vcg_sp E m de1) as [[[mIn1 mOut1] 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
293
294
      destruct d as [i|?]; simplify_eq/=.
      specialize (IHde2 mIn1).
      destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
295
296
      destruct (denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2))
        as [[[mIn3 mOut3 ] dv3] |] eqn:Hfar; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
297
298
299
300
301
302
      rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
      rewrite IHde2; last done. iDestruct "HmIn1" as "[HmIn2' Hawp2]".
      rewrite denv_delete_full_2_interp; last done.
      iDestruct "HmIn2'" as "[$ Hl]".
      iApply (a_store_spec _ _
            (λ j, ⌜j = dloc_interp E (dLoc i)⌝ ∧ denv_interp E mOut1)%I with "[Hawp1] Hawp2").
Léon Gondelman's avatar
Léon Gondelman committed
303
304
      { iApply (awp_wand with "Hawp1").
        iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
Léon Gondelman's avatar
Léon Gondelman committed
305
306
307
      iNext. iIntros (? ?) "[% HmOut1] [% HmOut2]". simplify_eq/=.
      iExists _. rewrite -denv_merge_interp.
      iDestruct ("Hl" with "[$HmOut1 $HmOut2]") as "[HmOut3 $]".
Léon Gondelman's avatar
Léon Gondelman committed
308
      iIntros "Hl". iSplit; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
309
310
311
312
313
314
      rewrite denv_insert_interp.
      iFrame "Hl HmOut3".
    - specialize (IHde1 m).
      destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
      specialize (IHde2 mIn1).
      destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
315
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
316
317
      rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
      rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
Léon Gondelman's avatar
Léon Gondelman committed
318
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Léon Gondelman's avatar
Léon Gondelman committed
319
      iNext. iIntros (? ?) "[% HmOut1] [% HmOut2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
320
      iExists (dval_interp E dv). repeat iSplit; eauto.
321
      + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
322
      + rewrite -denv_merge_interp. iFrame.
323
324
325
326
327
328
329
330
    - specialize (IHde m).
      destruct (vcg_sp E m de) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
      remember (dun_op_eval E u dv1) as Hu; destruct Hu; simplify_eq/=.
      rewrite IHde; last done. iDestruct "Hm" as "[$ Hawp]".
      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.
331
332
333
334
335
336
337
    - specialize (IHde1 m).
      destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
      specialize (IHde2 mIn1).
      destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
      rewrite IHde1; last done. iDestruct "Hm" as "[HmIn1 Hawp1]".
      rewrite IHde2; last done. iDestruct "HmIn1" as "[$ Hawp2]".
      iApply (a_sequence_spec with "[Hawp1 Hawp2]").
338
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
339
340
341
342
343
344
345
346
      iApply (awp_wand with "Hawp1").
      iIntros (?) "[-> HmOut1]"; simplify_eq/=.
      rewrite (denv_unlock_interp E mOut1).
      iModIntro. awp_seq.
      iApply (awp_wand with "Hawp2").
      iIntros (v) "[-> HmOut2]".
      iSplit; first done.
      rewrite -denv_merge_interp. iFrame.
347
  Qed. *)
Léon Gondelman's avatar
Léon Gondelman committed
348

349
  Lemma vcg_wp_correct R E m de Φ :
350
351
352
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
    awp (dcexpr_interp E de) R
353
354
      (λ v,  E' dv m', dval_interp E dv = v  wp_interp E (Φ E' m' dv)).
  Proof. Admitted. (*
355
356
357
358
359
360
361
    revert Φ m. induction de; intros Φ m.
    - iIntros "Hd". iApply awp_ret. wp_value_head. eauto.
    - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
      rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
    - iIntros "Hd". rewrite (IHde _ _). iApply (a_load_spec_exists_frac with "[Hd]").
      iApply (awp_wand with "Hd"). iIntros (?). iDestruct 1 as (dv m' <-) "Hd /=".
      iDestruct "Hd" as (dl ?) "Hd". iDestruct "Hd" as (q dw) "H".
362
      iExists (dloc_interp E dl), q, (dval_interp E dw); iSplit; first done.
363
      iDestruct "H" as "[Hl Hwp]". iFrame. iIntros "Hd". iExists _, _; iSplit; first done. by iApply "Hwp".
364
365
366
    - iIntros "H". simpl.
      destruct (vcg_sp E m de1) as [[[mIn mOut] dv]|] eqn:Heqsp; last first.
      { destruct (vcg_sp E m de2) as [[[mIn mOut] dv]|] eqn:Heqsp2; last first.
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. }
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
        iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1").
        iApply (a_store_spec _ _ (λ l, ∃ dl m', ⌜dloc_interp E dl = l⌝ ∧
          wp_interp E (mapsto_wand_list mOut
            (MapstoStarFull dl (λ _ : dval, MapstoWand dl dv LLvl 1 (Φ m' dv)))))%I with "[Hde1] [$Hde2]").
        { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (dv0 m' <-) "Hwp"; simplify_eq /=.
          iDestruct "Hwp" as (dl ->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
          iExists dl, m'; iSplit; first auto. eauto with iFrame. }
        iNext. iIntros (l w) "Hex". iDestruct "Hex" as (dl m' <-) "Hwp"; simplify_eq /=.
        rewrite mapsto_wand_list_spec. iIntros "[-> H]". iSpecialize ("Hwp" with "[$H]"); simpl.
        iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame.
        iIntros "Hdl". iExists _, m'; iSplit; first done. by iApply "Hwp". }
      destruct dv; last first.
      { simpl. iDestruct "H" as (dl ->) "H".
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
      iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
      { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
        iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
        eauto with iFrame. }
      iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
      rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
      iDestruct "Hwp" as (w) "(Hdl & Hwp)".
      iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists dv, m'; iSplit; first done; eauto with iFrame.
      by iApply "Hwp". }
      destruct d; simpl; try by iExFalso.
      { destruct d as [i|].
        + rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2.
          iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
          iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
          iApply ((a_store_spec _ _ (λ l, ⌜l = dloc_interp E (dLoc i)⌝ ∧ denv_interp E mOut)%I
                  (λ v : val,
              (∃ (dv : dval) (m' : denv),
               ⌜dval_interp E dv = v⌝
               ∧ wp_interp E
                   (mapsto_wand_list mOut
                      (MapstoStarFull (dLoc i)
                         (λ _ : dval,
                          MapstoWand (dLoc i) dv LLvl 1
                            match denv_replace_full i dv m' with
                            | Some mf => Φ mf dv
                            | None => Base False
                            end))))%I))
          with "[Hde1] [$Hde2]").
          { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp".
              by iExists (dloc_interp E (dLoc i)); repeat (iSplit; first done). }
          iNext. iIntros (l w) "[-> Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
          rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"). simpl.
          iDestruct "Hwp" as (dv0) "[Hl Hwp]".  iExists (dval_interp E dv0).
          iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
420
          destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso.
421
          iExists dv, mf; iSplit; first auto. done.
422
        + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
          rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
          iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
          iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
          { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
            iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
            eauto with iFrame. }
          iNext. iIntros (l0 w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
          rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
          iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl".
          iExists dv, m'; iSplit; first done; eauto with iFrame. by iApply "Hwp". }
      iDestruct "H" as (dl Hdl) "H".
      rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
      iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
      { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
        iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
        eauto with iFrame. }
      iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
      rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
      iDestruct "Hwp" as (w) "(Hdl & Hwp)".
      iExists (dval_interp E w). iFrame. iIntros "Hdl".  iExists dv, m'; iSplit; first done; eauto with iFrame.
      by iApply "Hwp".
    - iIntros "H". simpl.
447
448
      destruct (vcg_sp E m de1) as [[[m1 m2] dv]|] eqn:Heqsp; last first.
      { destruct (vcg_sp E m de2) as [[[m1 m2] dv]|] eqn:Heqsp'; last first.
449
450
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v).
          eauto 30 with iFrame. }
451
452
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1.
453
        iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
454
455
456
457
458
459
460
461
462
        iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1").
        iApply (a_bin_op_spec with "[$Hde1] [$Hde2]").  iNext. iIntros (? ?) "Hex".
        iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=.
        rewrite mapsto_wand_list_spec. iIntros "[-> H]".
        iSpecialize ("Hwp" with "[$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)".
        iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct.
        iExists _, _; iSplit; first done. eauto with iFrame. }
      rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.
Léon Gondelman's avatar
Léon Gondelman committed
463
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
464
465
466
467
468
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iSpecialize ("Hde2" with "Hm1").
      iApply (a_bin_op_spec with "[$Hde1] [$Hde2]"). iNext. iIntros (? ?) "(% & H)  Hex".
      iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec.
      iSpecialize ("Hwp" with "[$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)".
      iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct.
Léon Gondelman's avatar
Léon Gondelman committed
469
      eauto with iFrame.
470
471
472
473
474
475
476
    - iIntros "H".
      rewrite IHde. iApply a_un_op_spec.
      iApply (awp_wand with "H").
      iIntros (v) "Hex". iDestruct "Hex" as (dv m' <-) "H /=".
      iDestruct "H" as (dw) "[% H]".
      iExists _; iFrame. iSplit; eauto.
      iPureIntro. by apply dun_op_eval_correct.
477
    - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]").
478
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
479
480
481
482
      iApply (awp_wand with "H"). iIntros (v) "Hex". iDestruct "Hex" as (? ? <-) "H".
      simpl. iModIntro. rewrite IHde2.  awp_seq. iApply (awp_wand with "H"). eauto.
    - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
      rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
483
  Qed.
484
*)
485
486

  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
487
    MapstoListFromEnv Γs_in Γs_out Γls 
488
489
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
490
    IntoDCexpr E e dce 
491
    environments.envs_entails (environments.Envs Γp Γs_out c)
Robbert Krebbers's avatar
Robbert Krebbers committed
492
      (wp_interp_sane E (vcg_wp E m dce R (λ E m dv,
493
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
494
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
495
  Proof.
496
  Admitted.
497

498
End vcg_spec.
499

500
501
Arguments wp_interp : simpl never.

502
503
504
505
506
507
Ltac vcg_solver :=
  eapply tac_vcg_sound;
    [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
    | compute; reflexivity (*  E = penv_to_known_locs Γls *)
    | apply _ (* ListOfMapsto Γls E m *)
    | apply _ (* IntoDCexpr E e dce *)
508
    | simpl ].