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

Dan Frumin's avatar
Dan Frumin committed
100
  Fixpoint vcg_sp (E: known_locs) (mIn mOut : denv) (de : dcexpr) : option (denv * denv * dval) :=
101
    match de with
Dan Frumin's avatar
Dan Frumin committed
102
    | dCRet dv    => Some (mIn, mOut, dv)
103
    | dCLoad de1  =>
Dan Frumin's avatar
Dan Frumin committed
104
105
106
107
       ''(mIn1, mOut1, dl)      vcg_sp E mIn mOut de1;
       i                        is_dloc E dl;
       ''(mIn2, mOut2, q, dv)   denv_delete_frac_2 i mIn1 mOut1;
       Some (mIn2, denv_insert i ULvl q dv mOut2, dv)
108
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
109
       ''(mIn1, mOut1, dl)  vcg_sp E mIn mOut de1;
110
       i                    is_dloc E dl;
Dan Frumin's avatar
Dan Frumin committed
111
       ''(mIn2, mOut2, dv)  vcg_sp E mIn1 [] de2;
112
113
       ''(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 =>
Dan Frumin's avatar
Dan Frumin committed
115
116
       ''(mIn1, mOut1, dv1)  vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 [] de2;
117
118
119
120
       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 =>
Dan Frumin's avatar
Dan Frumin committed
122
       ''(mIn1, mOut1, dv)  vcg_sp E mIn mOut de;
123
       match dun_op_eval E op dv with
Dan Frumin's avatar
Dan Frumin committed
124
       | dSome dv' => Some (mIn1, mOut1, dv')
125
126
       | dNone | dUnknown _ => None
       end
127
    | dCSeq de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
128
129
       ''(mIn1, mOut1, _)    vcg_sp E mIn mOut de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 (denv_unlock mOut1) de2;
Dan Frumin's avatar
Dan Frumin committed
130
       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
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
192
       match vcg_sp E m [] de1 with
193
       | 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
       | None =>
Dan Frumin's avatar
Dan Frumin committed
197
          match vcg_sp E m [] de2 with
198
          | 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
          end
        end
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
205
       match vcg_sp E m [] de1 with
206
       | 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
       | None =>
Dan Frumin's avatar
Dan Frumin committed
210
          match vcg_sp E m [] de2 with
211
          | 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

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

  Lemma vcg_sp_correct E de m mIn mOut dv R :
    vcg_sp E m [] de = Some (mIn, mOut, dv) 
    denv_interp E m -
    denv_interp E mIn  awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mOut).
  Proof.
    iIntros (?) "Hm".
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
    iApply "Hawp". by rewrite /denv_interp.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
356

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

  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
495
    MapstoListFromEnv Γs_in Γs_out Γls 
496
497
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
498
    IntoDCexpr E e dce 
499
    environments.envs_entails (environments.Envs Γp Γs_out c)
Robbert Krebbers's avatar
Robbert Krebbers committed
500
      (wp_interp_sane E (vcg_wp E m dce R (λ E m dv,
501
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
502
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
503
  Proof.
504
  Admitted.
505

506
End vcg_spec.
507

508
509
Arguments wp_interp : simpl never.

510
511
512
513
514
515
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 *)
516
    | simpl ].