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

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

11
[DONE] Fix all the unknown cases, introduce a function for that (which should be
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
  simpl never)
- Write more tests with unknown stuff in it
14
  add tests like `!(l := 10;;;; l)`
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
- 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
Léon Gondelman's avatar
Léon Gondelman committed
20
- Maybe generate vcg_unknown in the cases None and '_' in vcg_store and vcg_load
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
28
29
30

Less urgent TODO

- Symbolic fractions
- Support bind
- Support conditional
- Write examples with R
- Deal with functions
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
37
38


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

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

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
       ''(mIn, mOut, dl)       vcg_sp E m de1;
       i                       is_dloc E dl;
Dan Frumin's avatar
Dan Frumin committed
106
107
       ''(mIn1, mOut1, q, dv)  denv_delete_frac_2 i mIn mOut;
       Some (mIn1, denv_insert i ULvl q dv mOut1, 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
       ''(mIn1, mOut1, _)    vcg_sp E m de1;
Dan Frumin's avatar
Dan Frumin committed
129
130
       ''(mIn2, mOut2, dv2)  vcg_sp E (denv_merge mIn1 (denv_unlock mOut1)) de2;
       Some (mIn2, mOut2, dv2)
131
    | dCAlloc _ |  dCUnknown _ => None
132
133
    end.

Léon Gondelman's avatar
Léon Gondelman committed
134
135
136
137
138
139
140
141
142
143
144
145

  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'  
        denv_interp E' m' 
        wp_interp_sane E' (Φ E' m' dv))%I.
  Arguments vcg_wp_unknown : simpl never.

146
147
148
149
150
151
152
153
154
155
  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
156
157
158
159
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
160
161
162
163
164
165
166
167
168
169
170
171
    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
172
173
174
175
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
176
177
178
179
180
181
182
183
184
185
    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
186
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
187
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
188
    | dCRet dv => Φ E m dv
189
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
190
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E))
191
192
193
    | dCStore de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
196
197
198
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
201
          | None => vcg_wp_unknown R E de m Φ
202
203
204
205
206
          end
        end
    | dCBinOp op de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
209
210
211
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
214
          | None => vcg_wp_unknown R E de m Φ
215
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
216
       end
217
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
218
       vcg_wp E m de R (λ E m dv,
219
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
222
223
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
224
       vcg_wp E m de1 R (λ E m _,
225
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
226
    | _ => vcg_wp_unknown R E de m Φ
227
    end.
228
229
230
231
232
233
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

  Lemma wp_interp_sane_sound E a : wp_interp_sane E a  wp_interp E a.
234
  Proof.
235
236
237
    generalize dependent E.
    induction a.
    - done.
238
    - simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
239
      iExists q, (dValUnknown v). iFrame. by (iApply H0).
240
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
241
      iExists (dValUnknown v). simpl. iFrame. by (iApply H0).
242
243
244
245
246
247
    - 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.
248
  Qed.
249

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

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

350
  Lemma vcg_wp_correct R E m de Φ :
351
352
353
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
    awp (dcexpr_interp E de) R
354
355
      (λ v,  E' dv m', dval_interp E dv = v  wp_interp E (Φ E' m' dv)).
  Proof. Admitted. (*
356
357
358
359
360
361
362
    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".
363
      iExists (dloc_interp E dl), q, (dval_interp E dw); iSplit; first done.
364
      iDestruct "H" as "[Hl Hwp]". iFrame. iIntros "Hd". iExists _, _; iSplit; first done. by iApply "Hwp".
365
366
367
    - 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.
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
420
        { 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").
421
          destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso.
422
          iExists dv, mf; iSplit; first auto. done.
423
        + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
          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.
448
449
      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.
450
451
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v).
          eauto 30 with iFrame. }
452
453
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1.
454
        iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
455
456
457
458
459
460
461
462
463
        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
464
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
465
466
467
468
469
      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
470
      eauto with iFrame.
471
472
473
474
475
476
477
    - 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.
478
    - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]").
479
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
480
481
482
483
      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.
484
  Qed.
485
*)
486
487

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

499
End vcg_spec.
500

501
502
Arguments wp_interp : simpl never.

503
504
505
506
507
508
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 *)
509
    | simpl ].