vcgen.v 28.2 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
- Support alloc in `vcg_wp`
Robbert Krebbers's avatar
Robbert Krebbers committed
16
- Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
21
22
23
24
25
26
27
28
- 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
29
30
31
32
33
34
(*
TODO:
Inductive dfrac :=
  | dFrac : frac → dfrac
  | dFracUnknown : nat → nat → frac → dfrac.
*)
35
36


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

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

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

51
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
52

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

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

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

95
96
  Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
    mapsto_wand_list_aux m Φ O.
97

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

Léon Gondelman's avatar
Léon Gondelman committed
132
133
134
135
136
137
138
139

  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
      (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
    mapsto_wand_list m $ Base $
      awp (dcexpr_interp E de) R (λ v,
         E' m' dv,
         v = dval_interp E' dv  
         E `prefix_of` E'  
Léon Gondelman's avatar
Léon Gondelman committed
140
       (denv_wf E' m') 
Léon Gondelman's avatar
Léon Gondelman committed
141
142
143
144
        denv_interp E' m' 
        wp_interp_sane E' (Φ E' m' dv))%I.
  Arguments vcg_wp_unknown : simpl never.

145
146
147
148
149
150
151
152
153
154
  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
155
156
157
158
    | _ =>
       mapsto_wand_list m $ IsLoc dv (λ dl,
         MapstoStar dl $ λ q dw,
           MapstoWand dl dw ULvl q (Φ [] dw))
159
160
161
162
163
164
165
166
167
168
169
170
    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
171
172
173
174
    | _ =>
       mapsto_wand_list m $ IsLoc dv1 (λ dl,
         MapstoStarFull dl $ λ _,
            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
175
176
177
178
179
180
    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
181
182
    | dUnknown (Some dw) => Φ m dw
    | _ => Base False
183
184
185
    end.

  Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Robbert Krebbers's avatar
Robbert Krebbers committed
186
      (R : iProp Σ) (Φ : known_locs  denv  dval  wp_expr) : wp_expr :=
187
    match de with
Robbert Krebbers's avatar
Robbert Krebbers committed
188
    | dCRet dv => Φ E m dv
189
    | dCLoad de1 =>
190
       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' (Φ E))
191
    | dCStore de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
192
       match vcg_sp E m [] de1 with
193
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
194
          vcg_wp E mIn de2 R (λ E mIn dv2,
Robbert Krebbers's avatar
Robbert Krebbers committed
195
            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
196
       | None =>
Dan Frumin's avatar
Dan Frumin committed
197
          match vcg_sp E m [] de2 with
198
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
199
             vcg_wp E mIn de1 R (λ E mIn dv1,
Robbert Krebbers's avatar
Robbert Krebbers committed
200
               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
201
          | None => vcg_wp_unknown R E de m Φ
202
203
204
          end
        end
    | dCBinOp op de1 de2 =>
Dan Frumin's avatar
Dan Frumin committed
205
       match vcg_sp E m [] de1 with
206
       | Some (mIn, mOut, dv1) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
          vcg_wp E mIn de2 R (λ E mIn dv2,
            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
209
       | None =>
Dan Frumin's avatar
Dan Frumin committed
210
          match vcg_sp E m [] de2 with
211
          | Some (mIn, mOut, dv2) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
             vcg_wp E mIn de1 R (λ E mIn dv1,
               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
Léon Gondelman's avatar
Léon Gondelman committed
214
          | None => vcg_wp_unknown R E de m Φ
215
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
216
       end
217
    | dCUnOp op de =>
Robbert Krebbers's avatar
Robbert Krebbers committed
218
       vcg_wp E m de R (λ E m dv,
219
         match dun_op_eval E op dv with
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
         | dSome dw => Φ E m dw
         | mdw => IsSome mdw (Φ E m)
222
223
         end)
    | dCSeq de1 de2 =>
Robbert Krebbers's avatar
Robbert Krebbers committed
224
       vcg_wp E m de1 R (λ E m _,
225
         UMod (vcg_wp E (denv_unlock m) de2 R Φ))
Léon Gondelman's avatar
Léon Gondelman committed
226
    | _ => vcg_wp_unknown R E de m Φ
227
    end.
228
229
230
231
232
233
End vcg.

Section vcg_spec.
  Context `{amonadG Σ}.

  Lemma wp_interp_sane_sound E a : wp_interp_sane E a  wp_interp E a.
234
  Proof.
235
236
237
    generalize dependent E.
    induction a.
    - done.
238
    - simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
239
      iExists q, (dValUnknown v). iFrame. by (iApply H0).
240
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
241
      iExists (dValUnknown v). simpl. iFrame. by (iApply H0).
242
243
244
245
246
247
    - simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
      iExists v. iFrame. by iApply H0.
    - simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
      iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
    - simpl. intros E. by apply U_mono.
248
  Qed.
249

Dan Frumin's avatar
Dan Frumin committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268

  Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
    wp_interp E (mapsto_wand_list_aux m t k) -
    ([ list] ndio  m, from_option
                              (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
                               default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) -
    wp_interp E t.
  Proof.
    generalize dependent k.
    induction m; simpl. eauto.
    iIntros (k) "H1 [Hl H2]".
    destruct a as [[x q dv]|]; simpl.
    - rewrite -plus_n_O. iSpecialize ("H1" with "Hl").
      iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
    - iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
      intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
  Qed.

269
270
  Lemma mapsto_wand_list_spec E m t :
    wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
271
  Proof.
Dan Frumin's avatar
Dan Frumin committed
272
273
274
    unfold mapsto_wand_list, denv_interp.
    iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
  Qed.
275

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

Robbert Krebbers's avatar
Robbert Krebbers committed
362
  Lemma vcg_sp_correct R E de m mIn mOut dv :
Dan Frumin's avatar
Dan Frumin committed
363
364
365
366
367
368
369
370
    vcg_sp E m [] de = Some (mIn, mOut, dv) 
    denv_interp E m -
    denv_interp E mIn  awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  denv_interp E mOut).
  Proof.
    iIntros (?) "Hm".
    iDestruct (vcg_sp_correct' with "Hm") as "[$ Hawp]"; first eassumption.
    iApply "Hawp". by rewrite /denv_interp.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
371

372
373
374
375
376
377
378
  Lemma vcg_sp_wf E de m mIn mOut dv :
    denv_wf E m 
    dcexpr_wf E de 
    vcg_sp E m [] de = Some (mIn, mOut, dv) 
    denv_wf E mIn  denv_wf E mOut  dval_wf E dv .
  Proof. Admitted.

379
  Lemma vcg_wp_unknown_correct R E m de Φ :
380
    denv_wf E m 
381
382
    denv_interp E m -
    wp_interp E (vcg_wp_unknown R E de m Φ) -
383
384
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
      E `prefix_of` E'  dval_interp E' dv = v 
385
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
386
387
  Proof.
    rewrite /vcg_wp_unknown mapsto_wand_list_spec.
388
    iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
389
    iApply (awp_wand with "Hwp"). iIntros (v) "H".
390
    iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
391
    rewrite wp_interp_sane_sound.
392
    iExists E', dv, m'. repeat (iSplit; first done); iFrame.
393
394
  Qed.

395
  Lemma vcg_wp_load_correct E m dv Φ :
396
    denv_wf E m 
397
398
399
    denv_interp E m -
    wp_interp E (vcg_wp_load E dv m (Φ E)) -
     (l:loc) q w, dval_interp E dv = #l  l C{q} w   (l C{q} w -
400
     E' dv' m', E `prefix_of` E'  dval_interp E' dv' = w 
401
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv')).
402
403
404
  Proof.
    rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
    + destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
405
      * destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
406
        rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
407
408
409
        iExists (dloc_interp E (dLoc i)), q,  (dval_interp E dv').
        iSplit. simplify_eq /=; done. iFrame. iIntros "Hl".
        iExists E, dv', m; iSplit; first done. iFrame.
410
411
412
        rewrite Hm0. iSplit; first done. eauto with iFrame.
      * rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
        iSpecialize ("Hwp" with "Hm"). simpl.
413
414
415
        iDestruct "Hwp" as (q dv') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
        iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). iSplit; first done.
        iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
416
417
418
419
        iExists E, dv', []; repeat (iSplit; first done); iFrame.
        unfold denv_interp, denv_wf. eauto.
    +  rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
       iSpecialize ("Hwp" with "Hm"); simpl.
420
421
422
       iDestruct "Hwp" as (dl) "(-> & Hwp)". iDestruct "Hwp" as (q dv') "[Hl Hwp]".
       iExists (dloc_interp E dl), q, (dval_interp E dv'). iSplit; first done.
       iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
423
       iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp, denv_wf. eauto.
424
425
  Qed.

426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
  Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
    E0 `prefix_of` E 
    denv_wf E (denv_merge mOut m) 
    denv_interp E m -
    wp_interp E (vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E)) -
    denv_interp E mOut -
     w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w 
     ( E' dv m', E0 `prefix_of` E'  dval_interp E' dv = w 
                  denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
  Proof.
    iIntros (Hpre Hwf) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
    * iExists  (dval_interp E dw); iSplit.
      { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
      iExists E, dw, (denv_merge mOut m).
      rewrite -denv_merge_interp. repeat (iSplit; first done); iFrame.
    * destruct dw as [dw1|] eqn:Hdw; last done.
      iExists  (dval_interp E dw1); iSplit.
      iPureIntro.  apply dbin_op_eval_correct. by rewrite Hbin.
      iExists E, dw1, (denv_merge mOut m).
      rewrite -denv_merge_interp. repeat (iSplit; first done). iFrame.
  Qed.
448

449
 Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
450
   E0 `prefix_of` E 
451
452
   denv_wf E m 
   dval_wf E dv2 
453
   denv_interp E m -
454
   wp_interp E (vcg_wp_store E dv1 dv2 m (Φ E)) -
Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
    (l : loc) (w : val), dval_interp E dv1 = #l 
     l C w  (l C[LLvl] dval_interp E dv2 -
457
          E' dv m', E0 `prefix_of` E'  dval_interp E' dv = dval_interp E dv2 
Robbert Krebbers's avatar
Robbert Krebbers committed
458
459
         denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
 Proof. (*
460
461
462
   iIntros (Hpre Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
    destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
   - apply is_dloc_some in Hdloc; rewrite Hdloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
     iExists (dloc_interp E (dLoc i)). iSplit; first done.
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
     destruct (denv_delete_full i m)  as [[m' dv_old]|] eqn:Hdel.
     + iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
       iSpecialize ("Hdel" with "[Hm]"); iFrame.
       iDestruct "Hdel" as "[HmDel Hl]".
       iExists (dval_interp E dv_old). iFrame.
       iIntros "Hl".
       iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
       iSplit. iPureIntro. apply denv_wf_insert; last done.
       by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
       rewrite -denv_insert_interp. iFrame.
     + rewrite mapsto_wand_list_spec.
       iSpecialize ("Hwp" with "[Hm]"); iFrame.
       iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; fold wp_interp.
       iExists (dval_interp E dv_old). iFrame.
       iIntros "Hl". iSpecialize ("Hwp" with "Hl").
       iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
   - rewrite mapsto_wand_list_spec.
     iSpecialize ("Hwp" with "[Hm]"); iFrame.
     iDestruct "Hwp" as (dl ->) "Hwp"; fold wp_interp.
     iDestruct "Hwp" as (dv) "[Hdv Hwp]"; fold wp_interp.
     iExists (dloc_interp E dl); iSplit; first done.
     iExists (dval_interp E dv). iFrame.
     iIntros "Hl". iSpecialize ("Hwp" with "Hl").
     iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
 Qed. *) Admitted.
489

Robbert Krebbers's avatar
Robbert Krebbers committed
490
491
492
  (* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the
  conjunctions in the same order. *)
  Lemma vcg_wp_correct R E m de Φ :
493
    dcexpr_wf E de 
494
    denv_wf E m 
495
496
    denv_interp E m -
    wp_interp E (vcg_wp E m de R Φ) -
497
498
    awp (dcexpr_interp E de) R (λ v,  E' dv m',
      E `prefix_of` E'  dval_interp E' dv = v 
499
      denv_wf E' m'  denv_interp E' m'  wp_interp E' (Φ E' m' dv)).
500
  Proof.
501
502
503
504
505
506
507
508
509
    revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
    - iApply awp_ret. wp_value_head.
      iExists E, d, m. iSplit; first done; by iFrame.
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
    - rewrite IHde; last done. iRename "Hm" into "Hawp".
      iSpecialize ("Hawp" with "Hwp"); simpl.
      iApply (a_load_spec_exists_frac with "[Hawp]").  iApply (awp_wand with "Hawp").
      iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <- Hm'wf) "(Hm & Hwp)".
      iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload". done.
Léon Gondelman's avatar
Léon Gondelman committed
510
511
512
      iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
      iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
      iSpecialize ("Hwp" with "Hl"). iDestruct "Hwp" as (Ef dvf mf Hpre' <-) "(Hmf & Hwp)".
513
      iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done. done.
514
    - rewrite{1} /vcg_wp; fold vcg_wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
      simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
516
517
518
519
      destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
      + destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
        specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (H1 & H2 & Hwf).
Robbert Krebbers's avatar
Robbert Krebbers committed
520
521
522
523
524
525
526
527
528
529
        iDestruct (vcg_sp_correct R with "Hm") as "[HmIn Hde2]"; first done.
        clear Heqsp2 Heqsp.
        iDestruct (IHde1 with "HmIn Hwp") as "Hde1"; try done.
        iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
        iDestruct 1 as (E' dw m' ? <- ?) "[Hm' H]". iIntros "[-> HmOut]".
        rewrite (dval_interp_mono E E') //.
        iApply (vcg_wp_store_correct with "[Hm' HmOut] H");
          eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
        iApply denv_merge_interp. iFrame "Hm'". by iApply (denv_interp_mono with "HmOut").
      + admit.
Léon Gondelman's avatar
Léon Gondelman committed
530
    - rewrite{1} /vcg_wp; fold vcg_wp.
531
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
Léon Gondelman's avatar
Léon Gondelman committed
532
      destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
533
      + destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
534
        { by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
Robbert Krebbers's avatar
Robbert Krebbers committed
535
        iPoseProof (vcg_sp_correct R) as "Hsp". eassumption.
536
537
        specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (H1 & H2 & Hwf).
        iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde2]"; iClear "Hsp"; clear Heqsp2 Heqsp.
538
        rewrite IHde1; [| done | done]. iSpecialize ("HmIn" with "Hwp").
539
        iApply (a_bin_op_spec with "[$HmIn] [$Hde2]"); fold dcexpr_interp.
Léon Gondelman's avatar
Léon Gondelman committed
540
        iNext. iIntros (v1 v2) "Hex (-> & HmOut)".
541
        iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
542
543
544
545
546
        specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
        specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
        specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
        iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
547
      + iPoseProof (vcg_sp_correct R) as "Hsp". eassumption.
548
549
550
551
552
553
554
555
556
557
558
559
        specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (H1 & H2 & Hwf).
        iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde1]"; iClear "Hsp"; clear Heqsp.
        rewrite IHde2; [| done | done]. iSpecialize ("HmIn" with "Hwp").
        iRename "HmIn" into "Hde2".
        iApply (a_bin_op_spec with "[$Hde1] [$Hde2]");  fold dcexpr_interp.
        iNext. iIntros (v1 v2) "(-> & HmOut) Hex".
        iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
        specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
        specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
        iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
        specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
        iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
560
    - rewrite IHde; last done. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
561
      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
562
      iDestruct "Hex" as (E' dv m' Hpre <- Hm'wf) "(Hm & Hwp)".
563
564
565
566
      destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
      + iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
      + iExists (dval_interp E' dw); iSplit.
        iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
567
        iExists E', dw, m'; eauto with iFrame.
568
569
570
      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
        iExists (dval_interp E' w). iSplit. iPureIntro.
        apply dun_op_eval_correct. by rewrite Hop.
571
        iExists E', w, m'; eauto with iFrame.
572
573
      + done.
    - rewrite IHde1; last first. done.
574
575
      { simpl in Hwf. apply andb_prop_elim in Hwf. by destruct Hwf. }
      iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
576
577
578
      iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
      iApply (awp_wand with "Hm").  iIntros (v) "Hex".
579
      iDestruct "Hex" as (Enew dv m' Hpre <- Hm'wf) "(Hm & Hwp)". simpl.
580
      rewrite denv_unlock_interp.
581
      iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
582
583
      simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
      specialize (dcexpr_interp_mono E Enew de2 H1 Hpre).
Léon Gondelman's avatar
Léon Gondelman committed
584
585
586
      intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
      iIntros (v) "Hex".
      iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
587
588
      iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
      iFrame. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
589
590
591
        by eapply dcexpr_wf_mono in Hpre.
        by apply denv_wf_unlock.
    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
Robbert Krebbers's avatar
Robbert Krebbers committed
592
  Admitted.
593

Léon Gondelman's avatar
Léon Gondelman committed
594
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
Dan Frumin's avatar
Dan Frumin committed
595
    MapstoListFromEnv Γs_in Γs_out Γls 
596
    E = penv_to_known_locs Γls 
Léon Gondelman's avatar
Léon Gondelman committed
597
    dcexpr_wf E de 
598
    denv_wf (penv_to_known_locs Γls) m 
599
    ListOfMapsto Γls E m 
Léon Gondelman's avatar
Léon Gondelman committed
600
    IntoDCexpr E e de 
601
    environments.envs_entails (environments.Envs Γp Γs_out c)
Léon Gondelman's avatar
Léon Gondelman committed
602
      (wp_interp_sane E (vcg_wp E m de R (λ E m dv,
603
        mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) 
604
    environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
605
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
606
    rewrite /IntoDCexpr /=. intros Hsplit ->.
607
    rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
Léon Gondelman's avatar
Léon Gondelman committed
608
609
610
611
612
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
    rewrite (vcg_wp_correct R); last done.
    iIntros (->) "H1 H2". rewrite wp_interp_sane_sound.
    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
613
614
615
    iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hmwf & Hm & Hwp)".
    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
   Qed.
616
End vcg_spec.
617

618
619
Arguments wp_interp : simpl never.

620
621
622
623
Ltac vcg_solver :=
  eapply tac_vcg_sound;
    [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
    | compute; reflexivity (*  E = penv_to_known_locs Γls *)
624
625
    |       (* dcexpr_wf E de *)
    |       (* denv_wf E m *)
626
627
    | apply _ (* ListOfMapsto Γls E m *)
    | apply _ (* IntoDCexpr E e dce *)
Léon Gondelman's avatar
Léon Gondelman committed
628
    | simpl ]; intuition.