vcgen.v 13.1 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 env splitenv.
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
16
17
18
19
20

(*TODO:

Understand how to correctly deal with levels and fractions in
   - exhale_list, i.e., what are levels and fractions of those ressources that
     are given in the very end to the postcondition
   - computations of vcg_sp, i.e. what are levels and fractions given back
Dan Frumin's avatar
Dan Frumin committed
21
22
23
24
25
26
      by vcg_sp in case of load and store
   - Add ExistsFracLevel to wp_expr
      ExistsFracLevel Φ ~ ∃ q x, Φ q x
   - Add levels to env_ps/env_ps_dv
   - Deep embedding of fractions
 *)
27

Dan Frumin's avatar
Dan Frumin committed
28
29
30
Section vcg.
  Context `{amonadG Σ}.

31
32
  (** Deep embedding of formulae used to build the verification condition generator *)

Robbert Krebbers's avatar
Robbert Krebbers committed
33
  (** TODO: remove Par *)
34
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
35
    | Base : iProp Σ  wp_expr
36
    | Inhale : dloc  frac  (dval  wp_expr)  wp_expr
Léon Gondelman's avatar
Léon Gondelman committed
37
    | InhaleKnown : dloc  dval  level  frac  wp_expr  wp_expr
Léon Gondelman's avatar
Léon Gondelman committed
38
    | Exhale : dloc  dval  level  frac  wp_expr  wp_expr
Dan Frumin's avatar
Dan Frumin committed
39
40
41
42
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
    | UMod : wp_expr  wp_expr
    | Par :
43
44
       ((val  iProp Σ)  wp_expr) 
       ((val  iProp Σ)  wp_expr) 
Dan Frumin's avatar
Dan Frumin committed
45
       (dval  dval  wp_expr)  wp_expr.
46

47
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
48

49
  Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
50
51
    match a with
    | Base P => P
52
53
    | Inhale dl q Φ =>
       dv, dloc_interp E dl U{q} dval_interp E dv  wp_interp E (Φ dv)
Léon Gondelman's avatar
Léon Gondelman committed
54
55
56
57
    | InhaleKnown dl dv x q Φ =>
      mapsto (dloc_interp E dl) x q (dval_interp E dv)  wp_interp E Φ
    | Exhale dl dv x q Φ =>
      mapsto (dloc_interp E dl) x q (dval_interp E dv) - wp_interp E Φ
Dan Frumin's avatar
Dan Frumin committed
58
59
60
61
    | IsSome dmx Φ  =>  x, doption_interp dmx = Some x  wp_interp E (Φ x)
    | IsLoc dv Φ =>
       dl : dloc, dval_interp E dv = #(dloc_interp E dl)  wp_interp E (Φ dl)
    | UMod P => U (wp_interp E P)
62
    | Par P1 P2 P3 =>  (Ψ1 Ψ2 : val  iProp Σ),
Dan Frumin's avatar
Dan Frumin committed
63
64
       wp_interp E (P1 Ψ1) 
       wp_interp E (P2 Ψ2) 
65
        (v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
66
  end%I.
Dan Frumin's avatar
Dan Frumin committed
67

68
  Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
69
70
    match a with
    | Base Φ => Φ
71
72
    | Inhale dl q Φ =>
       v, dloc_interp E dl U{q} v  wp_interp_sane E (Φ (dValUnknown v))
Léon Gondelman's avatar
Léon Gondelman committed
73
74
75
76
    | InhaleKnown dl dv x q Φ =>
      mapsto (dloc_interp E dl) x q (dval_interp E dv)  wp_interp_sane E Φ
    | Exhale dl dv x q Φ =>
       mapsto (dloc_interp E dl) x q (dval_interp E dv) - wp_interp_sane E Φ
Dan Frumin's avatar
Dan Frumin committed
77
78
79
80
81
82
    | IsSome dmx Φ  =>
       x, doption_interp dmx = Some x  wp_interp_sane E (Φ x)
    | IsLoc dv Φ =>
       l : loc, dval_interp E dv = #l  wp_interp_sane E (Φ (dLocUnknown l))
    | UMod P => U (wp_interp_sane E P)
    | Par P1 P2 P3 =>  Ψ1 Ψ2 : val  iProp Σ,
83
84
       wp_interp_sane E (P1 Ψ1) 
       wp_interp_sane E (P2 Ψ2) 
Dan Frumin's avatar
Dan Frumin committed
85
86
87
88
        v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
  end%I.


89
  Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
90
    match ps with
91
    | (i, ((x,q), dv)) :: s' => Exhale (dLoc i) dv x q (append_exhale_list s' Φ)
92
93
94
    | [] => Φ
    end.

Léon Gondelman's avatar
Léon Gondelman committed
95
96
97
98
99
100
  Fixpoint append_inhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
    match ps with
    | (i, ((x,q), dv)) :: s' => InhaleKnown (dLoc i) dv x q (append_inhale_list s' Φ)
    | [] => Φ
    end.

101
   (* vcg_sp E s de = Some (s1, s2, dv)
102
103
104
     - s1 = s / resources for de
     - s2 = new resources that you get from de
   *)
105
  Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) :
106
    option (env_ps_dv * env_ps_dv * dval) :=
107
    match de with
Dan Frumin's avatar
Dan Frumin committed
108
    | dCVal dv => Some (s, nil, dv)
109
    | dCLoad de1 =>
110
                ''(s1, s2, dv1)  vcg_sp E s de1;
111
112
                              i  is_dloc E dv1;
         ''(s1', ((x, q), dv2))  find_and_remove s1 (dLoc i);
113
     if (bool_decide (x = ULvl))
Léon Gondelman's avatar
Léon Gondelman committed
114
115
     then
         (* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *)
116
         Some ((i, ((x, (q/2)%Qp), dv2)) :: s1', (i, ((x, (q/2)%Qp), dv2)) :: s2, dv2)
Léon Gondelman's avatar
Léon Gondelman committed
117
     else None
118
    | dCStore de1 de2 =>
Léon Gondelman's avatar
Léon Gondelman committed
119
120
               ''(s1, s2, dv1)  vcg_sp E s de1;
                             i  is_dloc E dv1;
121
122
123
124
             ''(s1', s2', dv2)  vcg_sp E s1 de2;
             (* we can't use s1 below any more *)
             ''(s1'', s2'', ((x, q), _))  find_and_remove_2 s1' (s2 ++ s2') (dLoc i);
             (* NB: this should be fixed, adding 'q' & 'x' to env *)
125
     if (bool_decide (q = Qp_one) && bool_decide (x = ULvl))
126
     then Some (s1'', (i, ((LLvl, 1%Qp), dv2)) :: s2'', dv2)
127
     else None
128
    | dCBinOp op de1 de2 =>
Léon Gondelman's avatar
Léon Gondelman committed
129
        ''(s1, s2, dv1)  vcg_sp E s de1;
130
131
      ''(s1', s2', dv2)  vcg_sp E s1 de2;
      match dbin_op_eval E op dv1 dv2 with
Léon Gondelman's avatar
Léon Gondelman committed
132
      | dSome dv => Some (s1', s2 ++ s2', dv)
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
      (* | dUnknown (Some dv) => Some (s1', s2 ++ s2', dv) (*TODO: not sure here *)
         RK: probably just fail with None *)
Léon Gondelman's avatar
Léon Gondelman committed
135
      | dNone | dUnknown _ => None
136
      end
137
138
    end.

139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
  Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval  wp_expr) : wp_expr :=
    match de with
    | dCVal dv => Φ dv
    | dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
    | dCBinOp op de1 de2 =>
      match vcg_sp E s de1 with
      | Some (s1, s2, dv1) =>
          append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
            append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
      | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
      end
    | _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
    end.

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.
    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
      iExists (dValUnknown v). simpl. iFrame. by iApply H0.
    - 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.
    - simpl. intros E.
      iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
      iExists _,_.
      iSplitL "HΨ1". by iApply H0.
      iSplitL "HΨ2". by iApply H1.
      iIntros (v1 v2) "Hv1 Hv2". iApply H2.
      iApply ("HΦ" with "Hv1 Hv2").
  Qed.

  Lemma vcg_inhale_list_sound E s t :
    wp_interp E (append_inhale_list s t) - env_ps_dv_interp E s  wp_interp E t.
  Proof.
    unfold env_ps_dv_interp.
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
  Qed.

  Lemma vcg_exhale_list_sound E s t :
    wp_interp E (append_exhale_list s t) - env_ps_dv_interp E s - wp_interp E t.
  Proof.
    unfold env_ps_dv_interp.
    induction s as [| [i [[x q] w]] s']; simpl.
    - by iIntros "$ _".
    - iIntros "H [H1 H2]".
      iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
  Qed.

200
201
  Lemma vcg_sp_correct E s de ps1 ps2 dv R :
    vcg_sp E s de = Some (ps1, ps2, dv) 
Léon Gondelman's avatar
Léon Gondelman committed
202
    env_ps_dv_interp E s -
203
204
      env_ps_dv_interp E ps1 
      awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv  env_ps_dv_interp E ps2).
Dan Frumin's avatar
Dan Frumin committed
205
  Proof.
206
207
    revert s ps1 ps2 dv. induction de;
    iIntros (s ps1 ps2 dv Hsp) "Hs"; simplify_eq/=.
Léon Gondelman's avatar
Léon Gondelman committed
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
    - iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold env_ps_dv_interp. done.
    - specialize (IHde s).
      destruct (vcg_sp E s de) as [[[s1' s2'] dv1]|]; simplify_eq /=.
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [l|?]; simplify_eq/=.
      remember (find_and_remove s1' (dLoc l)) as Hfar.
      destruct Hfar as [[s1'' [[x q] dv'']]|]; simplify_eq/=.
      case_bool_decide; simplify_eq/=.
      rewrite IHde; last done. iDestruct "Hs" as "[Hs1' Hawp]".
      rewrite find_and_remove_env_ps_dv_interp; last done.
      iDestruct "Hs1'" as "[Hs1'' [Hl1 Hl2]]".
      iFrame "Hl1 Hs1''".
      iApply a_load_spec.
      iApply (awp_wand with "Hawp").
      iIntros (?) "[% Hs2']". simplify_eq/=. iExists _, _. iSplit; eauto.
      iFrame "Hl2". iIntros "Hl2". iSplit; eauto.
      by iFrame.
225
226
    - specialize (IHde1 s).
      destruct (vcg_sp E s de1) as [[[s1 s2] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
227
228
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [l|?]; simplify_eq/=.
229
230
231
232
233
234
235
236
237
238
      specialize (IHde2 s1).
      destruct (vcg_sp E s1 de2) as [[[s1' s2'] dv2]|]; simplify_eq /=.
      remember (find_and_remove_2 s1' (s2++s2') (dLoc l)) as Hfar.
      destruct Hfar as [[[s1'' s2''] [[x q] dv'']]|]; simplify_eq/=.
      repeat (case_bool_decide; simplify_eq/=).
      rewrite IHde1; last done. iDestruct "Hs" as "[Hs1 Hawp1]".
      rewrite IHde2; last done. iDestruct "Hs1" as "[Hs1' Hawp2]".
      rewrite find_and_remove_2_env_ps_dv_interp; last done.
      iDestruct "Hs1'" as "[$ Hl]".
      iApply (a_store_spec _ _ (λ j, j = dloc_interp E (dLoc l)  env_ps_dv_interp E s2)%I with "[Hawp1] Hawp2").
Léon Gondelman's avatar
Léon Gondelman committed
239
240
      { iApply (awp_wand with "Hawp1").
        iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
241
242
243
      iNext. iIntros (? ?) "[% Hs2] [% Hs2']". simplify_eq/=.
      iExists _. rewrite -env_ps_dv_interp_app.
      iDestruct ("Hl" with "[$Hs2 $Hs2']") as "[Hs2'' $]".
Léon Gondelman's avatar
Léon Gondelman committed
244
      iIntros "Hl". iSplit; eauto.
245
      iFrame "Hl Hs2''".
Léon Gondelman's avatar
Léon Gondelman committed
246
247
248
249
250
251
252
253
254
255
256
257
    - specialize (IHde1 s).
      destruct (vcg_sp E s de1) as [[[s1' s2'] dv1]|]; simplify_eq /=.
      specialize (IHde2 s1').
      destruct (vcg_sp E s1' de2) as [[[s1'' s2''] dv2]|]; simplify_eq /=.
      remember (dbin_op_eval E b dv1 dv2) as Hboe.
      destruct Hboe; simplify_eq/=.
      rewrite IHde1; last done. iDestruct "Hs" as "[Hs1' Hawp1]".
      rewrite IHde2; last done. iDestruct "Hs1'" as "[$ Hawp2]".
      iApply (a_bin_op_spec with "Hawp1 Hawp2").
      iNext. iIntros (? ?) "[% Hs2'] [% Hs2'']"; simplify_eq/=.
      iExists (dval_interp E dv). repeat iSplit; eauto.
      + iPureIntro. apply dbin_op_eval_correct. rewrite -HeqHboe. reflexivity.
Léon Gondelman's avatar
Léon Gondelman committed
258
      +  iCombine "Hs2' Hs2''" as "Hs2". iFrame.
259
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
260

261
  Lemma vcg_wp_correct R E s de Φ :
Dan Frumin's avatar
Dan Frumin committed
262
    wp_interp E (vcg_wp E s de R Φ) 
263
    awp (dcexpr_interp E de) R (λ v,  dv, dval_interp E dv = v   wp_interp E (Φ dv)).
Dan Frumin's avatar
Dan Frumin committed
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
  Proof.
    revert Φ s. induction de; simpl; intros Φ s.
    - iIntros "Hd". iApply awp_ret. wp_value_head.
      iExists d. eauto.
    - iIntros "Hd".
      iApply a_load_spec.
      rewrite IHde.
      iApply (awp_wand with "Hd").
      iIntros (?). iDestruct 1 as (dv <-) "Hd /=".
      iDestruct "Hd" as (dl ?) "Hd".
      iDestruct "Hd" as (dw) "[Hl Hd]".
      iExists _,_; iFrame. iSplit; eauto.
      iIntros "H". iExists _. iSplit; eauto.
      by iApply "Hd".
    - iIntros "H". iApply (awp_wand with "H").
      iIntros (v) "H". iExists (dValUnknown v).
      eauto 30 with iFrame.
    - iIntros "H".
      remember (vcg_sp E s de1) as sp. symmetry in Heqsp.
Léon Gondelman's avatar
Léon Gondelman committed
283
      destruct sp as [[[s1 s2] dv]|]; last first.
Léon Gondelman's avatar
Léon Gondelman committed
284
285
286
      {  iApply (awp_wand with "H").
      iIntros (v) "H". iExists (dValUnknown v).
      eauto 30 with iFrame.  }
287
      rewrite vcg_inhale_list_sound.
Léon Gondelman's avatar
Léon Gondelman committed
288
      iDestruct "H" as "[Henv Hde2]".
Léon Gondelman's avatar
Léon Gondelman committed
289
      rewrite IHde2.
Léon Gondelman's avatar
Léon Gondelman committed
290
291
292
293
294
295
      iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
      iDestruct ("Hsp" with "Henv") as "[Henv Hde1]".
      iApply (a_bin_op_spec with "Hde1 Hde2").
      iNext. iIntros (? ?) "(% & H)  Hex".
      iDestruct "Hex" as (? <-) "Hwp".
      simplify_eq /=.
296
      rewrite vcg_exhale_list_sound.
Léon Gondelman's avatar
Léon Gondelman committed
297
298
299
300
301
302
303
304
      rewrite -env_ps_dv_interp_app.
      iSpecialize ("Hwp" with "[$Henv $H]").
      simpl.
      iDestruct "Hwp" as (w) "(% & Hwp)".
      iExists (dval_interp E w).
      iSplit.
      iPureIntro. by apply dbin_op_eval_correct.
      eauto with iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
305
  Qed.
Dan Frumin's avatar
Dan Frumin committed
306

307
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
308
309
310
    MapstoListFromEnv Γs_in Γs_out Γls 
    E = env_to_known_locs Γls 
    ListOfMapsto Γls E ps 
311
    IntoDCexpr E e dce 
312
313
     coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c)
       (env_ps_dv_interp E ps - wp_interp_sane E (vcg_wp E ps dce R (λ dv, Base (Φ (dval_interp E dv))))) 
314
    coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
315
  Proof.
316
    rewrite /IntoDCexpr /=. intros Hsplit ->.
317
    rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
Dan Frumin's avatar
Dan Frumin committed
318
319
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite coq_tactics.envs_entails_eq.
Dan Frumin's avatar
Dan Frumin committed
320
    rewrite wp_interp_sane_sound (vcg_wp_correct R).
321
    intros ->. iIntros "H1 H2".
Dan Frumin's avatar
Dan Frumin committed
322
    iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
323
    iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Dan Frumin's avatar
Dan Frumin committed
324
325
  Qed.

326
End vcg_spec.