vcgen.v 28.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
20
21
22
23
24
25
26
27
28
29
- 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

Less urgent TODO

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

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


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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
43
  (** TODO: remove Par *)
44
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
45
    | Base : iProp Σ  wp_expr
46
47
    | MapstoStar : dloc  (frac  dval  wp_expr)  wp_expr
    | MapstoStarFull : dloc  (dval  wp_expr)  wp_expr
48
    | MapstoWand : dloc  dval  lvl  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
49
50
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
51
    | UMod : wp_expr  wp_expr.
52

53
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
54

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

70
  Fixpoint wp_interp_sane (E : known_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
71
72
    match a with
    | Base Φ => Φ
73
    | MapstoStar dl Φ =>
74
        q v, dloc_interp E dl C{q} v  wp_interp_sane E (Φ q (dValUnknown v))
75
    | MapstoStarFull dl Φ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
76
        v, dloc_interp E dl C{1} v  wp_interp_sane E (Φ (dValUnknown v))
77
    | MapstoWand dl dv x q Φ =>
78
       dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp_sane E Φ
Dan Frumin's avatar
Dan Frumin committed
79
    | IsSome dmx Φ  =>
80
        x, doption_interp dmx = Some x  wp_interp_sane E (Φ x)
Dan Frumin's avatar
Dan Frumin committed
81
    | IsLoc dv Φ =>
82
        l : loc, dval_interp E dv = #l  wp_interp_sane E (Φ (dLocUnknown l))
Dan Frumin's avatar
Dan Frumin committed
83
    | UMod P => U (wp_interp_sane E P)
84
    end%I.
Dan Frumin's avatar
Dan Frumin committed
85

86
  Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
87
    match m with
88
    | [] => Φ
89
90
    | dio :: m' =>
      match dio with
91
      | None => mapsto_wand_list_aux m' Φ (S i)
92
      | Some (DenvItem x q dv)  =>
93
         MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
94
      end
95
96
    end.

97
98
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
99

100
  Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
101
    match de with
102
103
    | dCRet dv    => Some (m, nil, dv)
    | dCLoad de1  =>
104
105
106
107
       ''(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)
108
    | dCStore de1 de2 =>
109
110
111
112
113
       ''(mIn1, mOut1, dl)  vcg_sp E m de1;
       i                    is_dloc E dl;
       ''(mIn2, mOut2, dv)  vcg_sp E mIn1 de2;
       ''(mIn3, mOut3, _)   denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2);
       Some (mIn3, denv_insert i LLvl 1 dv mOut3, dv)
114
    | dCBinOp op de1 de2 =>
115
116
117
118
119
120
       ''(mIn1, mOut1, dv1)  vcg_sp E m de1;
       ''(mIn2, mOut2, dv2)  vcg_sp E mIn1 de2;
       match dbin_op_eval E op dv1 dv2 with
       | dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
       | dNone | dUnknown _ => None
       end
121
    | dCUnOp op de =>
122
       ''(mIn, mOut, dv)  vcg_sp E m de;
123
124
125
126
       match dun_op_eval E op dv with
       | dSome dv' => Some (mIn, mOut, dv')
       | dNone | dUnknown _ => None
       end
127
    | dCSeq de1 de2 =>
128
129
130
       ''(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)
131
    | dCAlloc _ |  dCUnknown _ => None
132
133
    end.

134
  (* TODO: change the fail though cases, in the same way as the unknown case
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  of vcg_wp. Also factor that out in a function vcg_unknown *)
136
137
138
139
140
141
142
143
144
145
  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
146
147
148
149
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
150
151
152
153
154
155
156
157
158
159
160
161
    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
162
163
164
165
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
166
167
168
169
170
171
172
173
174
175
    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
176
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
177
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    | dCRet dv => Φ E m dv
179
    | dCLoad de1 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
180
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E))
181
182
183
    | dCStore de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
186
187
188
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
191
192
          | None =>
             mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
193
               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
194
195
196
197
198
          end
        end
    | dCBinOp op de1 de2 =>
       match vcg_sp E m de1 with
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
201
202
203
       | None =>
          match vcg_sp E m de2 with
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
206
207
          | None =>
             mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
208
               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
209
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
210
       end
211
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
212
       vcg_wp E m de R (λ E m dv,
213
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
216
217
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
218
       vcg_wp E m de1 R (λ E m _,
219
220
221
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
    | _ =>
       mapsto_wand_list m $ Base $
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
225
226
227
         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
228
    end.
229
230
231
232
233
234
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

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

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

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

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

357
  Lemma vcg_wp_correct R E m de Φ :
358
359
360
    denv_interp E m -∗
    wp_interp E (vcg_wp E m de R Φ) -∗
    awp (dcexpr_interp E de) R
361
      (λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
Robbert Krebbers's avatar
Robbert Krebbers committed
362
  Proof. (*
363
364
365
366
367
368
369
    revert Φ m. induction de; intros Φ m.
    - iIntros "Hd". iApply awp_ret. wp_value_head. eauto.
    - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
      rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
    - iIntros "Hd". rewrite (IHde _ _). iApply (a_load_spec_exists_frac with "[Hd]").
      iApply (awp_wand with "Hd"). iIntros (?). iDestruct 1 as (dv m' <-) "Hd /=".
      iDestruct "Hd" as (dl ?) "Hd". iDestruct "Hd" as (q dw) "H".
370
      iExists (dloc_interp E dl), q, (dval_interp E dw); iSplit; first done.
371
      iDestruct "H" as "[Hl Hwp]". iFrame. iIntros "Hd". iExists _, _; iSplit; first done. by iApply "Hwp".
372
373
374
    - iIntros "H". simpl.
      destruct (vcg_sp E m de1) as [[[mIn mOut] dv]|] eqn:Heqsp; last first.
      { destruct (vcg_sp E m de2) as [[[mIn mOut] dv]|] eqn:Heqsp2; last first.
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. }
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
        iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1").
        iApply (a_store_spec _ _ (λ l, ∃ dl m', ⌜dloc_interp E dl = l⌝ ∧
          wp_interp E (mapsto_wand_list mOut
            (MapstoStarFull dl (λ _ : dval, MapstoWand dl dv LLvl 1 (Φ m' dv)))))%I with "[Hde1] [$Hde2]").
        { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (dv0 m' <-) "Hwp"; simplify_eq /=.
          iDestruct "Hwp" as (dl ->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
          iExists dl, m'; iSplit; first auto. eauto with iFrame. }
        iNext. iIntros (l w) "Hex". iDestruct "Hex" as (dl m' <-) "Hwp"; simplify_eq /=.
        rewrite mapsto_wand_list_spec. iIntros "[-> H]". iSpecialize ("Hwp" with "[$H]"); simpl.
        iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame.
        iIntros "Hdl". iExists _, m'; iSplit; first done. by iApply "Hwp". }
      destruct dv; last first.
      { simpl. iDestruct "H" as (dl ->) "H".
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
      iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
      { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
        iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
        eauto with iFrame. }
      iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
      rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
      iDestruct "Hwp" as (w) "(Hdl & Hwp)".
      iExists (dval_interp E w). iFrame. iIntros "Hdl". iExists dv, m'; iSplit; first done; eauto with iFrame.
      by iApply "Hwp". }
      destruct d; simpl; try by iExFalso.
      { destruct d as [i|].
        + rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]". rewrite mapsto_wand_list_spec IHde2.
          iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
          iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
          iApply ((a_store_spec _ _ (λ l, ⌜l = dloc_interp E (dLoc i)⌝ ∧ denv_interp E mOut)%I
                  (λ v : val,
              (∃ (dv : dval) (m' : denv),
               ⌜dval_interp E dv = v⌝
               ∧ wp_interp E
                   (mapsto_wand_list mOut
                      (MapstoStarFull (dLoc i)
                         (λ _ : dval,
                          MapstoWand (dLoc i) dv LLvl 1
                            match denv_replace_full i dv m' with
                            | Some mf => Φ mf dv
                            | None => Base False
                            end))))%I))
          with "[Hde1] [$Hde2]").
          { iApply (awp_wand with "Hde1"). iIntros (v) "Hex". iDestruct "Hex" as (->) "Hwp".
              by iExists (dloc_interp E (dLoc i)); repeat (iSplit; first done). }
          iNext. iIntros (l w) "[-> Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
          rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"). simpl.
          iDestruct "Hwp" as (dv0) "[Hl Hwp]".  iExists (dval_interp E dv0).
          iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
428
          destruct (denv_replace_full i dv m') as [mf |]; last first; try by iExFalso.
429
          iExists dv, mf; iSplit; first auto. done.
430
        + simpl. iDestruct "H" as (dl Hdl) "H". rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
          rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
          iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
          iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
          { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
            iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
            eauto with iFrame. }
          iNext. iIntros (l0 w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
          rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
          iDestruct "Hwp" as (w) "(Hdl & Hwp)". iExists (dval_interp E w). iFrame. iIntros "Hdl".
          iExists dv, m'; iSplit; first done; eauto with iFrame. by iApply "Hwp". }
      iDestruct "H" as (dl Hdl) "H".
      rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.  iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iClear "Hsp". iSpecialize ("Hde2" with "Hm1").
      iApply (a_store_spec _ _ (λ l, ⌜dloc_interp E dl = l⌝ ∧ denv_interp E mOut)%I with "[Hde1] [$Hde2]").
      { iApply (awp_wand with "Hde1"). iIntros (v) "Hex".
        iDestruct "Hex" as (->) "Hwp"; simplify_eq /=. iExists (dloc_interp E dl); iSplit; first done.
        eauto with iFrame. }
      iNext. iIntros (l w) "[<- Hout] Hex". iDestruct "Hex" as (dv m' <-) "Hwp"; simplify_eq /=.
      rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "[$Hout]"); simpl.
      iDestruct "Hwp" as (w) "(Hdl & Hwp)".
      iExists (dval_interp E w). iFrame. iIntros "Hdl".  iExists dv, m'; iSplit; first done; eauto with iFrame.
      by iApply "Hwp".
    - iIntros "H". simpl.
455
456
      destruct (vcg_sp E m de1) as [[[m1 m2] dv]|] eqn:Heqsp; last first.
      { destruct (vcg_sp E m de2) as [[[m1 m2] dv]|] eqn:Heqsp'; last first.
457
458
        { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v).
          eauto 30 with iFrame. }
459
460
        rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]".
        rewrite mapsto_wand_list_spec IHde1.
461
        iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
462
463
464
465
466
467
468
469
470
        iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1").
        iApply (a_bin_op_spec with "[$Hde1] [$Hde2]").  iNext. iIntros (? ?) "Hex".
        iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=.
        rewrite mapsto_wand_list_spec. iIntros "[-> H]".
        iSpecialize ("Hwp" with "[$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)".
        iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct.
        iExists _, _; iSplit; first done. eauto with iFrame. }
      rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde2]".
      rewrite mapsto_wand_list_spec IHde2.
Léon Gondelman's avatar
Léon Gondelman committed
471
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
472
473
474
475
476
      iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]". iSpecialize ("Hde2" with "Hm1").
      iApply (a_bin_op_spec with "[$Hde1] [$Hde2]"). iNext. iIntros (? ?) "(% & H)  Hex".
      iDestruct "Hex" as (? ? <-) "Hwp"; simplify_eq /=. rewrite mapsto_wand_list_spec.
      iSpecialize ("Hwp" with "[$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)".
      iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct.
Léon Gondelman's avatar
Léon Gondelman committed
477
      eauto with iFrame.
478
479
480
481
482
483
484
    - iIntros "H".
      rewrite IHde. iApply a_un_op_spec.
      iApply (awp_wand with "H").
      iIntros (v) "Hex". iDestruct "Hex" as (dv m' <-) "H /=".
      iDestruct "H" as (dw) "[% H]".
      iExists _; iFrame. iSplit; eauto.
      iPureIntro. by apply dun_op_eval_correct.
485
    - iIntros "H". rewrite IHde1. iApply (a_sequence_spec with "[H]").
486
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
487
488
489
490
      iApply (awp_wand with "H"). iIntros (v) "Hex". iDestruct "Hex" as (? ? <-) "H".
      simpl. iModIntro. rewrite IHde2.  awp_seq. iApply (awp_wand with "H"). eauto.
    - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
      rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
491
  Qed.
492
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
493
  Admitted.
Dan Frumin's avatar
Dan Frumin committed
494

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

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

590
(*
591
592
593
594
595
  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 →
596
597
598
    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 Φ).
599
600
  Proof.
    intros ???? Hgoal. eapply tac_vcg_sound; try eassumption.
601
    revert Hgoal. rewrite environments.envs_entails_eq. intros ->.
602
603
    rewrite wp_interp_sane_sound optimize_sound. done.
  Qed.
604
*)
605
End vcg_spec.
606

607
608
Arguments wp_interp : simpl never.

609
610
611
612
613
614
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 *)
615
    | simpl ].
616

617
(*
618
619
620
621
622
623
624
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 ].
625
*)