vcgen.v 30.4 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
27
    | MapstoStarKnown : dloc  dval  lvl  frac  wp_expr  wp_expr
    | MapstoWand : dloc  dval  lvl  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
28
29
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
30
    | UMod : wp_expr  wp_expr.
31

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

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

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

69
  Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
70
    match m with
71
    | [] => Φ
72
73
    | dio :: m' =>
      match dio with
74
      | None => mapsto_wand_list_aux m' Φ (S i)
75
      | Some (DenvItem x q dv)  =>
76
         MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
77
      end
78
79
    end.

80
81
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
82

83
  Fixpoint mapsto_star_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
84
    match m with
Léon Gondelman's avatar
Léon Gondelman committed
85
    | [] => Φ
86
87
    | dio :: m' =>
      match dio with
88
      | None => mapsto_star_list_aux m' Φ (S i)
89
      | Some (DenvItem x q dv)  =>
90
         MapstoStarKnown (dLoc i) dv x q (mapsto_star_list_aux m' Φ (S i))
91
      end
Léon Gondelman's avatar
Léon Gondelman committed
92
93
    end.

94
95
  Definition mapsto_star_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_star_list_aux m Φ O.
96

97
  Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
98
    match de with
99
100
    | dCRet dv    => Some (m, nil, dv)
    | dCLoad de1  =>
101
102
103
104
      ''(mIn, mOut, dl)  vcg_sp E m de1;
                      i  is_dloc E dl;
        ''(mIn1, q, dv)  denv_delete_frac i mIn;
       Some (mIn1, denv_insert i ULvl q dv mOut, dv)
105
    | dCStore de1 de2 =>
106
107
108
109
110
      ''(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%Qp dv mOut3, dv)
111
    | dCBinOp op de1 de2 =>
112
113
      ''(mIn1, mOut1, dv1)  vcg_sp E m de1;
      ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 de2;
114
      match dbin_op_eval E op dv1 dv2 with
115
      | dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
Léon Gondelman's avatar
Léon Gondelman committed
116
      | dNone | dUnknown _ => None
117
      (* | dUnknown (Some dv) =>  RK: probably just fail with None *)
118
      end
119
120
121
122
123
124
    | dCUnOp op de =>
      ''(mIn, mOut, dv)  vcg_sp E m de;
       match dun_op_eval E op dv with
       | dSome dv' => Some (mIn, mOut, dv')
       | dNone | dUnknown _ => None
       end
125
126
127
128
129
130
    | dCSeq de1 de2 =>
      ''(mIn1, mOut1, _)    vcg_sp E m de1;
        ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 de2;
        (*TODO: can we improve it with (denv_unlock mIn1) instead of mIn1 *)
      Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
    | dCAlloc _ |  dCUnknown _ => None
131
132
    end.

133
  Fixpoint vcg_wp (E: known_locs) (m: denv) (de : dcexpr) (R : iProp Σ) (Φ : denv  dval  wp_expr) : wp_expr :=
134
    match de with
135
    | dCRet dv   => Φ m dv
136
    | dCLoad de1 =>
137
        vcg_wp E m de1 R (λ m' dv, IsLoc dv (λ l, MapstoStar l (λ q w, MapstoWand l w ULvl q (Φ m' w))))
138
139
140
    | dCStore de1 de2 =>
      match vcg_sp E m de1 with
      | Some (mIn, mOut, dv1) =>
141
142
        match dv1 with
        | dLitV (dLitLoc (dLoc i)) =>
143
144
          mapsto_star_list m
            (mapsto_wand_list mIn
145
146
               (vcg_wp E mIn de2 R (λ m' dv2,
                  mapsto_wand_list mOut
147
148
149
150
151
                    (MapstoStarFull (dLoc i) (λ _, MapstoWand (dLoc i) dv2 LLvl 1
                         match denv_replace_full i dv2 m' with
                         | Some mf => (Φ mf dv2)
                         | None => Base False (*TODO: maybe this is too strong, return just (Φ m' dv2) *)
                         end)))))
152
153
154
155
156
157
158
159
160
161
162
        | dLitV (dLitInt _) | dLitV (dLitBool _) | dLitV dLitUnit => Base False
        | _ =>
          IsLoc dv1 (λ dl,
            mapsto_star_list m
              (mapsto_wand_list mIn
                 (vcg_wp E mIn de2 R (λ m' dv2,
                    mapsto_wand_list mOut
                      (MapstoStarFull dl (λ _,
                         (MapstoWand dl dv2 LLvl 1%Qp (Φ m' dv2))))))))
        end
      | None => (*TODO: maybe this brunch also needs modification of the environment m' *)
163
164
        match vcg_sp E m de2 with
        | Some (mIn, mOut, dv2) =>
165
166
          mapsto_star_list m
            (mapsto_wand_list mIn
167
168
169
170
               (vcg_wp E mIn de1 R (λ m' dv1,
                  IsLoc dv1 (λ dl,
                    mapsto_wand_list mOut
                      (MapstoStarFull dl
171
                         (λ _, MapstoWand dl dv2 LLvl 1
172
173
                            (Φ m' dv2 )))))))
        | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ m (dValUnknown v))))
174
175
        end
      end
176
    | dCBinOp op de1 de2 =>
177
178
      match vcg_sp E m de1 with
      | Some (mIn, mOut, dv1) =>
179
        mapsto_star_list m
180
181
          (mapsto_wand_list mIn (vcg_wp E mIn de2 R (λ m' dv2,
            mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) (Φ (denv_merge mOut m'))))))
182
183
184
      | None =>
        match vcg_sp E m de2 with
        | Some (mIn, mOut, dv2) =>
185
          mapsto_star_list m
186
187
188
            (mapsto_wand_list mIn (vcg_wp E mIn de1 R (λ m' dv1,
               mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) (Φ (denv_merge mOut m'))))))
        | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ m (dValUnknown v))))
189
190
        end
      end
191
    | dCUnOp op de => vcg_wp E m de R (λ m' dv, IsSome (dun_op_eval E op dv) (Φ m'))
192
193
    | dCSeq de1 de2 => vcg_wp E m de1 R (λ m' _, UMod (vcg_wp E (denv_unlock m') de2 R Φ))
    | _ =>  Base (awp (dcexpr_interp E de) R (λ v, wp_interp_sane E (Φ m (dValUnknown v))))
194
195
    end.

196
197
198
  Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
    match Φ with
    | Base Φ1 => mapsto_wand_list m Φ
199
200
201
202
    | MapstoStar (dLoc i) Φ1 =>
      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))
203
        end
204
205
206
207
208
    | MapstoStarFull (dLoc i) Φ1 =>
      match denv_delete_full i m with
        | Some (m1, dv) => optimize m1 (Φ1 dv)
        | None => MapstoStarFull (dLoc i) (λ dv, optimize m (Φ1 dv))
      end
209
210
211
212
213
    | MapstoStarKnown (dLoc i) dv x q Φ1 =>
      if (bool_decide (q = 1%Qp))
      then
        match denv_delete_full i m with
        | Some (m1, dv1) =>
214
          if bool_decide (dv = dv1) then optimize m1 Φ1
215
          else MapstoStarKnown (dLoc i) dv x Qp_one (optimize m Φ1)
216
        | None => MapstoStarKnown (dLoc i) dv x 1 (optimize m Φ1)
217
218
219
220
        end
      else
        match denv_delete_frac i m with
        | Some (m1, q1, dv1) =>
221
          (*TODO: here we still have an issue with frac. *)
222
223
224
225
226
227
          if (bool_decide (q = q1) && bool_decide (dv = dv1))
          then optimize m1 Φ1
          else MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
        | None => MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
        end
    | MapstoWand (dLoc i) dv x q Φ1 => optimize (denv_insert i x q dv m) Φ1
228
229
230
    | MapstoStar dl Φ1 =>  MapstoStar dl (λ q dv, optimize m (Φ1 q dv))
    | MapstoStarFull dl Φ1 => MapstoStarFull dl (λ dv, optimize m (Φ1 dv))
    | MapstoStarKnown dl dv x q Φ1 => MapstoStarKnown dl dv x q (optimize m Φ1)
231
232
233
234
235
236
237
238
239
240
    | MapstoWand dl w x q Φ1 => MapstoWand dl w x q (optimize m Φ1)
    | IsSome dmx Φ1 =>
      match dmx with
      | dNone => Base False
      | dSome x => optimize m (Φ1 x)
      | _ => IsSome dmx (λ v, optimize m (Φ1 v))
      end
    | IsLoc dv Φ1 =>
      match dv with
      | dLitV (dLitLoc l) => optimize m (Φ1 l)
241
      | dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize m (Φ1 v))
242
243
244
245
246
      | _ => Base False
      end
    | UMod Φ => optimize (denv_unlock m) Φ
    end.

247
248
249
250
251
252
253
254
255
256
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

  Lemma wp_interp_sane_sound E a : wp_interp_sane E a  wp_interp E a.
  Proof.
    generalize dependent E.
    induction a.
    - done.
257
258
259
    - simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
      iExists q, (dValUnknown v).
       iFrame. by (iApply H0).
260
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
261
      iExists (dValUnknown v). simpl. iFrame.
262
263
264
265
266
267
268
269
270
    - 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.
  Qed.

271
272
  Lemma mapsto_star_list_spec E m t :
    wp_interp E (mapsto_star_list m t) - denv_interp E m  wp_interp E t.
273
  Proof.
274
275
  Admitted.
(*    unfold env_ps_dv_interp.
276
277
278
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
279
  Qed. *)
280

281
282
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
283
  Proof.
284
285
  Admitted.
  (*  unfold env_ps_dv_interp.
286
287
288
289
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "H [H1 H2]".
      iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
290
  Qed. *)
291

292
293
  Lemma vcg_sp_correct E m de mIn mOut dv R :
    vcg_sp E m de = Some (mIn, mOut, dv) 
294
    denv_interp E m -
295
296
      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
297
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
298
299
300
301
302
    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
303
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
304
      destruct d as [i|?]; simplify_eq/=.
305
      destruct (denv_delete_frac i mIn1) as [[[mIn1' q] dv1]|] eqn:Hfar; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
306
307
308
309
      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
310
311
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
Léon Gondelman's avatar
Léon Gondelman committed
312
313
314
      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
315
      by iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
316
317
    - specialize (IHde1 m).
      destruct (vcg_sp E m de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
318
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
319
320
321
      destruct d as [i|?]; simplify_eq/=.
      specialize (IHde2 mIn1).
      destruct (vcg_sp E mIn1 de2) as [[[mIn2 mOut2] dv2]|]; simplify_eq /=.
322
323
      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
324
325
326
327
328
329
      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
330
331
      { iApply (awp_wand with "Hawp1").
        iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
Léon Gondelman's avatar
Léon Gondelman committed
332
333
334
      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
335
      iIntros "Hl". iSplit; eauto.
Léon Gondelman's avatar
Léon Gondelman committed
336
337
338
339
340
341
      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 /=.
342
      destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
343
344
      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
345
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
Léon Gondelman's avatar
Léon Gondelman committed
346
      iNext. iIntros (? ?) "[% HmOut1] [% HmOut2]"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
347
      iExists (dval_interp E dv). repeat iSplit; eauto.
348
      + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe.
Léon Gondelman's avatar
Léon Gondelman committed
349
      + rewrite -denv_merge_interp. iFrame.
350
351
352
353
354
355
356
357
    - 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.
358
359
360
361
362
363
364
    - 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]").
365
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
366
367
368
369
370
371
372
373
      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.
374
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
375

376
377
  Lemma vcg_wp_correct R E m de Φ :
    wp_interp E (vcg_wp E m de R Φ) 
378
379
        awp (dcexpr_interp E de) R
      (λ v,  dv m', dval_interp E dv = v  wp_interp E (Φ m' dv)).
Dan Frumin's avatar
Dan Frumin committed
380
  Proof.
381
382
383
384
385
386
387
    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".
388
      iExists (dloc_interp E dl), q, (dval_interp E dw); iSplit; first done.
389
      iDestruct "H" as "[Hl Hwp]". iFrame. iIntros "Hd". iExists _, _; iSplit; first done. by iApply "Hwp".
390
391
392
    - 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.
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
434
435
436
437
438
439
440
441
442
443
444
445
        { 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").
446
          destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso.
447
          iExists dv, mf; iSplit; first auto. done.
448
        + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
          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.
473
474
      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.
475
476
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v).
          eauto 30 with iFrame. }
477
478
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1.
479
        iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
480
481
482
483
484
485
486
487
488
        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
489
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
490
491
492
493
494
      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
495
      eauto with iFrame.
496
497
498
499
500
501
502
    - 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.
503
    - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]").
504
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
505
506
507
508
      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.
509
  Qed.
Dan Frumin's avatar
Dan Frumin committed
510

511
  Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
512
513
514
515
516
    wp_interp E (optimize m Φ) -
    denv_interp E m - (wp_interp E Φ).
  Proof.
    generalize dependent m.
    induction Φ; simpl; intros m.
517
518
519
520
521
522
523
    - 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.
524
        rewrite -(denv_delete_frac_interp _ i m) //.
525
526
        iDestruct "Hm" as "[Hm' Hdv]". rewrite H0. iSpecialize ("Hwp" with "Hm'"). iFrame.
      +  simpl. iDestruct "Hwp" as (q dv) "[Hl Hdv]".
527
        rewrite H0. iExists _,_; iFrame; by iApply "Hdv".
528
    - destruct d as [i|l]; iIntros "Hwp Hm".
529
      + destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
530
531
532
        {  simpl.  iDestruct "Hwp" as (dv) "H".
           iExists dv. iDestruct "H" as "[Hl Hwp]". iFrame. rewrite H0. by iApply "Hwp". }
        iExists dv.
533
        rewrite -(denv_delete_full_interp _ i m) //.
534
535
536
        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".
537
538
539
    - destruct d as [i|?].
      + case_bool_decide; simplify_eq/=. (* location found *)
        * (* q = 1 *)
540
          destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
541
542
543
544
545
          { 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". }
546
          rewrite -(denv_delete_full_interp _ i m) //.
547
          rewrite IHΦ. iIntros "Hdv".
548
549
550
          iIntros "[Hm' Hi]". iFrame.
          iSplitL "Hi"; last by iApply "Hdv".
          by iApply mapsto_downgrade.
551
        * (* q <> 1 *)
552
          destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hdl; last first.
553
554
555
556
557
558
559
560
561
          { 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'".
562
          rewrite -(denv_delete_frac_interp _ i m) //.
563
564
565
          iIntros "[Hm Hi]". iFrame.
          iSplitL "Hi"; last by iApply "Hdv'".
          by iApply mapsto_downgrade.
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
      + (* 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Φ".
589
  Qed.
590
591

  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
592
    MapstoListFromEnv Γs_in Γs_out Γls 
593
594
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
595
    IntoDCexpr E e dce 
596
597
598
    environments.envs_entails (environments.Envs Γp Γs_out c)
      (denv_interp E m - wp_interp E (vcg_wp E m dce R (λ _ dv, Base (Φ (dval_interp E dv))))) 
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
599
  Proof.
600
    rewrite /IntoDCexpr /=. intros Hsplit ->.
601
    rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
Dan Frumin's avatar
Dan Frumin committed
602
    eapply tac_envs_split_mapsto; try eassumption.
603
    revert Hgoal. rewrite environments.envs_entails_eq.
604
    rewrite (vcg_wp_correct R).
605
    intros ->. iIntros "H1 H2".
Dan Frumin's avatar
Dan Frumin committed
606
    iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
607
    iIntros (v) "H". by iDestruct "H" as (dv _) "[-> H]".
608
609
610
611
612
613
614
  Qed.

  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 
615
616
617
    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 Φ).
618
619
  Proof.
    intros ???? Hgoal. eapply tac_vcg_sound; try eassumption.
620
    revert Hgoal. rewrite environments.envs_entails_eq. intros ->.
621
622
    rewrite wp_interp_sane_sound optimize_sound. done.
  Qed.
623
End vcg_spec.
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639

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 *)
    | rewrite -wp_interp_sane_sound ].

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 ].