vcgen.v 28.5 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
11
12
13
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
14
15


Dan Frumin's avatar
Dan Frumin committed
16
17
18
Section vcg.
  Context `{amonadG Σ}.

19
20
  (** Deep embedding of formulae used to build the verification condition generator *)

Robbert Krebbers's avatar
Robbert Krebbers committed
21
  (** TODO: remove Par *)
22
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
23
    | Base : iProp Σ  wp_expr
24
25
    | MapstoStar : dloc  (frac  dval  wp_expr)  wp_expr
    | MapstoStarFull : dloc  (dval  wp_expr)  wp_expr
26
    | MapstoWand : dloc  dval  lvl  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
27
28
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
29
    | UMod : wp_expr  wp_expr.
30

31
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
32

33
  Fixpoint wp_interp (E : known_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
34
35
    match a with
    | Base P => P
36
    | MapstoStar dl Φ =>
37
        q dv, dloc_interp E dl C{q} dval_interp E dv  wp_interp E (Φ q dv)
38
    | MapstoStarFull dl Φ =>
39
        dv, dloc_interp E dl C{1} dval_interp E dv  wp_interp E (Φ dv)
40
    | MapstoWand dl dv x q Φ =>
41
       dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp E Φ
Dan Frumin's avatar
Dan Frumin committed
42
43
    | IsSome dmx Φ  =>  x, doption_interp dmx = Some x  wp_interp E (Φ x)
    | IsLoc dv Φ =>
44
        dl : dloc, dval_interp E dv = #(dloc_interp E dl)  wp_interp E (Φ dl)
Dan Frumin's avatar
Dan Frumin committed
45
    | UMod P => U (wp_interp E P)
46
    end%I.
Dan Frumin's avatar
Dan Frumin committed
47

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

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

75
76
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
77

78
  Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
79
    match de with
80
81
    | dCRet dv    => Some (m, nil, dv)
    | dCLoad de1  =>
82
83
84
85
       ''(mIn, mOut, dl)       vcg_sp E m de1;
       i                       is_dloc E dl;
       ''(mIn1, mOut2, q, dv)  denv_delete_frac_2 i mIn mOut;
       Some (mIn1, denv_insert i ULvl q dv mOut2, dv)
86
    | dCStore de1 de2 =>
87
88
89
90
91
       ''(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)
92
    | dCBinOp op de1 de2 =>
93
94
95
96
97
98
       ''(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
99
    | dCUnOp op de =>
100
       ''(mIn, mOut, dv)  vcg_sp E m de;
101
102
103
104
       match dun_op_eval E op dv with
       | dSome dv' => Some (mIn, mOut, dv')
       | dNone | dUnknown _ => None
       end
105
    | dCSeq de1 de2 =>
106
107
108
       ''(mIn1, mOut1, _)    vcg_sp E m de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E (denv_unlock mIn1) de2;
       Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
109
    | dCAlloc _ |  dCUnknown _ => None
110
111
    end.

112
113
  Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
    match Φ with
114
    | Base Φ1 => mapsto_wand_list m (Base Φ1)
115
    | MapstoStar (dLoc i) Φ1 =>
116
117
118
119
       match denv_delete_frac i m with
       | Some (m1, q1, dv) => optimize m1 (Φ1 q1 dv)
       | None => MapstoStar (dLoc i) (λ q dv, optimize m (Φ1 q dv))
       end
120
    | MapstoStarFull (dLoc i) Φ1 =>
121
122
123
124
       match denv_delete_full i m with
       | Some (m1, dv) => optimize m1 (Φ1 dv)
       | None => MapstoStarFull (dLoc i) (λ dv, optimize m (Φ1 dv))
       end
125
    | MapstoWand (dLoc i) dv x q Φ1 => optimize (denv_insert i x q dv m) Φ1
126
127
    | MapstoStar dl Φ1 =>  MapstoStar dl (λ q dv, optimize m (Φ1 q dv))
    | MapstoStarFull dl Φ1 => MapstoStarFull dl (λ dv, optimize m (Φ1 dv))
128
129
    | MapstoWand dl w x q Φ1 => MapstoWand dl w x q (optimize m Φ1)
    | IsSome dmx Φ1 =>
130
131
132
133
134
        match dmx with
        | dNone => Base False
        | dSome x => optimize m (Φ1 x)
        | _ => IsSome dmx (λ v, optimize m (Φ1 v))
        end
135
    | IsLoc dv Φ1 =>
136
137
138
139
140
        match dv with
        | dLitV (dLitLoc l) => optimize m (Φ1 l)
        | dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize m (Φ1 v))
        | _ => Base False
        end
141
142
143
    | UMod Φ => optimize (denv_unlock m) Φ
    end.

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

Section vcg_spec.
  Context `{amonadG Σ}.

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

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

261
262
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) -∗ denv_interp E m -∗ wp_interp E t.
263
  Proof.
264
265
  Admitted.
  (*  unfold env_ps_dv_interp.
266
267
268
269
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "H [H1 H2]".
      iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
270
  Qed. *)
271

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

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

493
  Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
494
495
    wp_interp E (optimize m Φ) -
    denv_interp E m - (wp_interp E Φ).
496
  Proof. (*
497
498
    generalize dependent m.
    induction Φ; simpl; intros m.
499
500
501
502
503
504
505
    - rewrite mapsto_wand_list_spec /=; done.
    - destruct d as [i|l]; iIntros "Hwp Hm".
      + remember (denv_delete_frac i m) as Hdl.
        destruct Hdl as [[[m' q] dv]|]; last first.
        {  simpl.  iDestruct "Hwp" as (q dv) "H".
           iExists q, dv. iDestruct "H" as "[Hl Hwp]". iFrame. rewrite H0. by iApply "Hwp". }
        iExists q, dv.
506
        rewrite -(denv_delete_frac_interp _ i m) //.
507
508
        iDestruct "Hm" as "[Hm' Hdv]". rewrite H0. iSpecialize ("Hwp" with "Hm'"). iFrame.
      +  simpl. iDestruct "Hwp" as (q dv) "[Hl Hdv]".
509
        rewrite H0. iExists _,_; iFrame; by iApply "Hdv".
510
    - destruct d as [i|l]; iIntros "Hwp Hm".
511
      + destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
512
513
514
        {  simpl.  iDestruct "Hwp" as (dv) "H".
           iExists dv. iDestruct "H" as "[Hl Hwp]". iFrame. rewrite H0. by iApply "Hwp". }
        iExists dv.
515
        rewrite -(denv_delete_full_interp _ i m) //.
516
517
518
        iDestruct "Hm" as "[Hm' Hdv]". rewrite H0. iSpecialize ("Hwp" with "Hm'"). iFrame.
      +  simpl. iDestruct "Hwp" as (dv) "[Hl Hdv]".
        rewrite H0.  iExists _; iFrame; by iApply "Hdv".
519
520
521
    - destruct d as [i|?].
      + case_bool_decide; simplify_eq/=. (* location found *)
        * (* q = 1 *)
522
          destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
523
524
525
526
527
          { simpl. iIntros "[Hl Hdv]".
            rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
          case_bool_decide; simplify_eq/=; simpl; last first.
          { simpl. iIntros "[Hl Hdv]".
            rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
528
          rewrite -(denv_delete_full_interp _ i m) //.
529
          rewrite IHΦ. iIntros "Hdv".
530
531
532
          iIntros "[Hm' Hi]". iFrame.
          iSplitL "Hi"; last by iApply "Hdv".
          by iApply mapsto_downgrade.
533
        * (* q <> 1 *)
534
          destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hdl; last first.
535
536
537
538
539
540
541
542
543
          { simpl. iIntros "[Hl Hdv]".
            rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
          case_bool_decide; simplify_eq/=; last first.
          { simpl. iIntros "[Hl Hdv]".
            rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
          case_bool_decide; simplify_eq/=; simpl; last first.
          { simpl. iIntros "[Hl Hdv]".
            rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
          rewrite IHΦ. iIntros "Hdv'".
544
          rewrite -(denv_delete_frac_interp _ i m) //.
545
546
547
          iIntros "[Hm Hi]". iFrame.
          iSplitL "Hi"; last by iApply "Hdv'".
          by iApply mapsto_downgrade.
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
      + (* location wasn't found *)
        simpl. iIntros "[Hl Hdv]".
        rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv".
    - destruct d as [i|?].
      + rewrite IHΦ. iIntros "HΦ Hm Hi".
        rewrite denv_insert_interp. iApply "HΦ". iFrame.
      + simpl. iIntros "HΦ Hm Hl".
        rewrite IHΦ. iApply ("HΦ" with "Hl Hm").
    -  destruct d; simpl.
      + iIntros "[]".
      + rewrite H0. f_equiv. iIntros "H"; iExists a; auto.
      + iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
        rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
    - destruct d; simpl; try by iIntros "[]".
      + destruct d; simpl; try by iIntros "[]".
        * rewrite H0. f_equiv. iIntros "H". iExists d; auto.
        * iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
          rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
      +  iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
         rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
    - iIntros "HΦ Hm".
      rewrite IHΦ. iDestruct (denv_unlock_interp with "Hm") as "Hm".
      iModIntro. by iApply "HΦ".
571
572
  *)
  Admitted.
573
574

  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
575
    MapstoListFromEnv Γs_in Γs_out Γls 
576
577
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
578
    IntoDCexpr E e dce 
579
    environments.envs_entails (environments.Envs Γp Γs_out c)
580
581
      (wp_interp_sane E (vcg_wp E m dce R (λ m dv,
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
582
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
583
  Proof.
584
  Admitted.
585

586
(*
587
588
589
590
591
  Lemma tac_vcg_opt_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
    MapstoListFromEnv Γs_in Γs_out Γls →
    E = penv_to_known_locs Γls →
    ListOfMapsto Γls E m →
    IntoDCexpr E e dce →
592
593
594
    environments.envs_entails (environments.Envs Γp Γs_out c)
      (wp_interp_sane E (optimize m (vcg_wp E m dce R (λ _ dv, Base (Φ (dval_interp E dv)))))) →
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
595
596
  Proof.
    intros ???? Hgoal. eapply tac_vcg_sound; try eassumption.
597
    revert Hgoal. rewrite environments.envs_entails_eq. intros ->.
598
599
    rewrite wp_interp_sane_sound optimize_sound. done.
  Qed.
600
*)
601
End vcg_spec.
602

603
604
Arguments wp_interp : simpl never.

605
606
607
608
609
610
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 *)
611
    | simpl ].
612

613
(*
614
615
616
617
618
619
620
Ltac vcg_opt_solver :=
  eapply tac_vcg_opt_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 *)
    | simpl ].
621
*)