vcgen.v 27.3 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 =>
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
358
359
360
361
362
363
364
365
366
367
368
369
370
  Lemma vcg_wp_unknown_correct R E m de Φ :
    denv_interp E m -
    wp_interp E (vcg_wp_unknown R E de m Φ) -
    awp (dcexpr_interp E de) R
      (λ v,  E' dv m', dval_interp E' dv = v  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
    iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm").
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
    iDestruct "H" as (E' m' dv ->) "(Hpre & Hm & Hwp)".
    rewrite wp_interp_sane_sound.
    iExists E', dv, m'. iSplit; first done; iFrame.
  Qed.

371
  Lemma vcg_wp_correct R E m de Φ :
372
373
374
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
    awp (dcexpr_interp E de) R
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
428
429
430
431
432
433
      (λ v,  E' dv m', dval_interp E' dv = v  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
    revert Φ m. induction de; intros Φ m; iIntros "Hm".
    - iIntros "Hd". iApply awp_ret. wp_value_head.
      iExists E, d, m. iSplit; first done; iFrame.
    - iIntros "Hawp". iApply (vcg_wp_unknown_correct with "Hm Hawp").
    - iIntros "Hd". rewrite IHde. iSpecialize ("Hm" with "Hd"). simpl.
      iApply (a_load_spec_exists_frac with "[Hm]"). iApply (awp_wand with "Hm").
      iIntros (v) "H". iDestruct "H" as (E' dv m' <-) "(Hm & Hwp)".
      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 /=.
        * apply (denv_lookup_interp i q dv' m') in Hlkp. apply is_dloc_some in Hdloc.
          destruct Hlkp as [m0 Hlkp]. subst. iExists (dloc_interp E' (dLoc i)), q,  (dval_interp E' dv').
          rewrite denv_insert_interp. iDestruct "Hm" as "[Hm0 Hi]". iFrame.
          iSplit. simplify_eq /=; done.  iIntros "Hl".
          iExists E', dv', (denv_insert i ULvl q dv' m0); iSplit; first done. iFrame.
          rewrite denv_insert_interp. iFrame.
        * rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm"). simpl.
          iDestruct "Hwp" as (q dv') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
          iExists (dloc_interp E' (dLoc i)), q, (dval_interp E' dv'). iSplit; first done.
          iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
          iExists E', dv', []; iSplit; first done. iFrame. by unfold denv_interp.
       +  rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm"); simpl.
          iDestruct "Hwp" as (dl) "(-> & Hwp)". iDestruct "Hwp" as (q dv') "[Hl Hwp]".
           iExists (dloc_interp E' dl), q, (dval_interp E' dv'). iSplit; first done.
          iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
          iExists E', dv', []; iSplit; first done. iFrame. by unfold denv_interp. Admitted.
    (* - iIntros "H". rewrite /vcg_wp.
      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.
        { iApply (vcg_wp_unknown_correct with "[$Hm] [$H]"). }
        fold vcg_wp.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
        iDestruct ("Hsp" with "Hm") as "[Hm Hde2]". iClear "Hsp". clear Heqsp2 Heqsp.
        rewrite IHde1.  iSpecialize ("Hm" with "H").
        iApply (a_store_spec _ _ (λ l,
             ∃ (E' : known_locs) (dv0 : dval) (m' : denv),
            ⌜dval_interp E' dv0 = #l⌝
            ∧ denv_interp E' m' ∗ wp_interp E' (vcg_wp_store E' dv0 dv (denv_merge mOut m') (Φ E')) )%I                       (λ v : val, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut)%I
                  with "[Hm] [$Hde2]"); fold dcexpr_interp.
        * iApply (awp_wand with "Hm"). iIntros (v) "H".
          iDestruct "H" as (E' dv1 m') "(<- & Hdv1 & Hwp)".
          unfold vcg_wp_store.  destruct (is_dloc E' dv1) as [i|] eqn:Hdloc.
          ** apply is_dloc_some in Hdloc. subst. iExists (dloc_interp E' (dLoc i)); iSplit; first done.
             destruct (denv_delete_full i (denv_merge mOut m')) as [[m'0 dv_old]|] eqn:Hdel; simplify_eq/=.
             ***  apply (denv_delete_full_interp E') in Hdel. rewrite denv_insert_interp.
          rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]".
          admit.
        * admit.

          (*wp_interp E' (MapstoStarFull (dLoc i) (λ _ : dval, MapstoWand (dLoc i) dv LLvl 1 (Φ E' [] dv)))*)
        *
          rewrite IHde1.


      }
      fold vcg_wp.


          iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. }
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
        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").
486
          destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso.
487
          iExists dv, mf; iSplit; first auto. done.
488
        + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
          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.
513
514
      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.
515
516
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v).
          eauto 30 with iFrame. }
517
518
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1.
519
        iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
520
521
522
523
524
525
526
527
528
        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
529
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
530
531
532
533
534
      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
535
      eauto with iFrame.
536
537
538
539
540
541
542
    - 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.
543
    - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]").
544
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
545
546
547
548
      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.
549
  Qed.
550
*)
551
552

  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
553
    MapstoListFromEnv Γs_in Γs_out Γls 
554
555
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
556
    IntoDCexpr E e dce 
557
    environments.envs_entails (environments.Envs Γp Γs_out c)
Robbert Krebbers's avatar
Robbert Krebbers committed
558
      (wp_interp_sane E (vcg_wp E m dce R (λ E m dv,
559
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
560
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
561
  Proof.
562
  Admitted.
563

564
End vcg_spec.
565

566
567
Arguments wp_interp : simpl never.

568
569
570
571
572
573
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 *)
574
    | simpl ].