vcgen.v 15.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 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
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
47

48
  Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
49
50
    match a with
    | Base P => P
51
52
    | 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
53
54
55
56
    | 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
57
58
59
60
    | 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)
61
    | Par P1 P2 P3 =>  (Ψ1 Ψ2 : val  iProp Σ),
Dan Frumin's avatar
Dan Frumin committed
62
63
       wp_interp E (P1 Ψ1) 
       wp_interp E (P2 Ψ2) 
64
        (v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
65
   end%I.
Dan Frumin's avatar
Dan Frumin committed
66

67
  Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
68
69
    match a with
    | Base Φ => Φ
70
71
    | 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
72
73
74
75
    | 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
76
77
78
79
80
81
    | 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 Σ,
82
83
       wp_interp_sane E (P1 Ψ1) 
       wp_interp_sane E (P2 Ψ2) 
Dan Frumin's avatar
Dan Frumin committed
84
85
86
87
88
89
90
91
92
93
        v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
  end%I.

  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.
Léon Gondelman's avatar
Léon Gondelman committed
94
    - simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa.
Dan Frumin's avatar
Dan Frumin committed
95
96
97
98
99
100
101
102
    - 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Φ)".
103
      iExists _,_.
Dan Frumin's avatar
Dan Frumin committed
104
105
      iSplitL "HΨ1". by iApply H0.
      iSplitL "HΨ2". by iApply H1.
106
107
      iIntros (v1 v2) "Hv1 Hv2". iApply H2.
      iApply ("HΦ" with "Hv1 Hv2").
Dan Frumin's avatar
Dan Frumin committed
108
109
  Qed.

110
  Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
111
    match ps with
112
    | (i, ((x,q), dv)) :: s' => Exhale (dLoc i) dv x q (append_exhale_list s' Φ)
113
114
115
    | [] => Φ
    end.

Léon Gondelman's avatar
Léon Gondelman committed
116
117
118
119
120
121
  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.

122
  Lemma vcg_inhale_list_sound E s t :
Léon Gondelman's avatar
Léon Gondelman committed
123
124
125
126
127
128
129
130
    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.

131
132
  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.
133
  Proof.
Léon Gondelman's avatar
Léon Gondelman committed
134
135
    unfold env_ps_dv_interp.
    induction s as [| [i [[x q] w]] s']; simpl.
136
137
138
139
140
    - by iIntros "$ _".
    - iIntros "H [H1 H2]".
      iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
  Qed.

141
142
143


  (* vcg_sp E s de = Some (s1, s2, dv)
144
145
146
     - s1 = s / resources for de
     - s2 = new resources that you get from de
   *)
147
  Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) :
148
    option (env_ps_dv * env_ps_dv * dval) :=
149
    match de with
Dan Frumin's avatar
Dan Frumin committed
150
    | dCVal dv => Some (s, nil, dv)
151
    | dCLoad de1 =>
152
                ''(s1, s2, dv1)  vcg_sp E s de1;
153
154
                              i  is_dloc E dv1;
         ''(s1', ((x, q), dv2))  find_and_remove s1 (dLoc i);
155
     if (bool_decide (x = ULvl))
Léon Gondelman's avatar
Léon Gondelman committed
156
157
     then
         (* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *)
158
         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
159
     else None
160
    | dCStore de1 de2 =>
Léon Gondelman's avatar
Léon Gondelman committed
161
162
               ''(s1, s2, dv1)  vcg_sp E s de1;
                             i  is_dloc E dv1;
163
164
165
166
             ''(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 *)
167
     if (bool_decide (q = Qp_one) && bool_decide (x = ULvl))
168
     then Some (s1'', (i, ((LLvl, 1%Qp), dv2)) :: s2'', dv2)
169
     else None
170
    | dCBinOp op de1 de2 =>
Léon Gondelman's avatar
Léon Gondelman committed
171
        ''(s1, s2, dv1)  vcg_sp E s de1;
172
173
      ''(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
174
      | dSome dv => Some (s1', s2 ++ s2', dv)
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
      (* | 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
177
      | dNone | dUnknown _ => None
178
      end
179
180
    end.

181
182
  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
183
    env_ps_dv_interp E s -
184
185
      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
186
  Proof.
187
188
    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
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
    - 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.
206
207
    - specialize (IHde1 s).
      destruct (vcg_sp E s de1) as [[[s1 s2] dv1]|]; simplify_eq /=.
Léon Gondelman's avatar
Léon Gondelman committed
208
209
      destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
      destruct d as [l|?]; simplify_eq/=.
210
211
212
213
214
215
216
217
218
219
      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
220
221
      { iApply (awp_wand with "Hawp1").
        iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
222
223
224
      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
225
      iIntros "Hl". iSplit; eauto.
226
      iFrame "Hl Hs2''".
Léon Gondelman's avatar
Léon Gondelman committed
227
228
229
230
231
232
233
234
235
236
237
238
    - 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
239
      +  iCombine "Hs2' Hs2''" as "Hs2". iFrame.
240
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
241

242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
  (* Suggestion for vcg_wp *)
  (* Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr :=
    match vcg_sp E s de with
    | Some (s1, s2, dv) => append_inhale_list s1 (append_exhale_list s2 (Φ dv))
    | None =>
      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 =>
          match vcg_sp E s de2 with
          | Some (s1, s2, dv2) =>
            append_inhale_list s (vcg_wp E s1 de1 R (λ dv1,
            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
        end
      | dCStore de1 de2 => (*TODO*) Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
      end
    end.
*)
Dan Frumin's avatar
Dan Frumin committed
267
  Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval  wp_expr) : wp_expr :=
268
269
    match de with
    | dCVal dv => Φ dv
Léon Gondelman's avatar
Léon Gondelman committed
270
    | dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
271
272
273
    | dCBinOp op de1 de2 =>
      match vcg_sp E s de1 with
      | Some (s1, s2, dv1) =>
Léon Gondelman's avatar
Léon Gondelman committed
274
          append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
275
            append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
Dan Frumin's avatar
Dan Frumin committed
276
      | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
277
      end
Dan Frumin's avatar
Dan Frumin committed
278
    | _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
Dan Frumin's avatar
Dan Frumin committed
279
280
    end.

281
  Lemma vcg_wp_correct R E s de Φ :
Dan Frumin's avatar
Dan Frumin committed
282
    wp_interp E (vcg_wp E s de R Φ) 
283
    awp (dcexpr_interp E de) R (λ v,  dv, dval_interp E dv = v   wp_interp E (Φ dv)).
Dan Frumin's avatar
Dan Frumin committed
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
  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
303
      destruct sp as [[[s1 s2] dv]|]; last first.
Léon Gondelman's avatar
Léon Gondelman committed
304
305
306
      {  iApply (awp_wand with "H").
      iIntros (v) "H". iExists (dValUnknown v).
      eauto 30 with iFrame.  }
307
      rewrite vcg_inhale_list_sound.
Léon Gondelman's avatar
Léon Gondelman committed
308
      iDestruct "H" as "[Henv Hde2]".
Léon Gondelman's avatar
Léon Gondelman committed
309
      rewrite IHde2.
Léon Gondelman's avatar
Léon Gondelman committed
310
311
312
313
314
315
      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 /=.
316
      rewrite vcg_exhale_list_sound.
Léon Gondelman's avatar
Léon Gondelman committed
317
318
319
320
321
322
323
324
      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
325
  Qed.
Dan Frumin's avatar
Dan Frumin committed
326

327
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce :
Dan Frumin's avatar
Dan Frumin committed
328
329
330
    MapstoListFromEnv Γs_in Γs_out Γls 
    E = env_to_known_locs Γls 
    ListOfMapsto Γls E ps 
331
    IntoDCexpr E e dce 
332
333
     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))))) 
334
    coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
335
  Proof.
336
    rewrite /IntoDCexpr /=. intros Hsplit ->.
337
    rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
Dan Frumin's avatar
Dan Frumin committed
338
339
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite coq_tactics.envs_entails_eq.
Dan Frumin's avatar
Dan Frumin committed
340
    rewrite wp_interp_sane_sound (vcg_wp_correct R).
341
    intros ->. iIntros "H1 H2".
Dan Frumin's avatar
Dan Frumin committed
342
    iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
343
    iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Dan Frumin's avatar
Dan Frumin committed
344
345
  Qed.

346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
End vcg.


(*
Ltac vcg_solver :=
  eapply tac_vcg_sound;
    [ apply _
    | compute; reflexivity
    | apply _
    | apply _
    | simpl ].

Section Tests_vcg.
  Context `{amonadG Σ}.

    Notation "l ↦( x , q ) v" :=
     (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v").


  Lemma test1 (l : loc) :
    l ↦U #1 -∗
    awp (a_load (a_ret #l))%E True (fun v => ⌜v = #1⌝ ∗ l ↦U #1).
  Proof.
    iIntros "Hl".
    vcg_solver.
    iIntros "[H _]"; simplify_eq /=. unfold ps_lvl, ps_frc. simpl in *.
  Admitted.



  Lemma test2 (l : loc) :
    l ↦U #1 -∗
    awp (a_store (a_ret #l) (a_ret #3))%E True (fun v => ⌜v = #3⌝ ∗ l ↦L #3).
  Proof.
    iIntros "Hl".
    vcg_solver.
     iIntros "[H _]"; simplify_eq /=. simpl.
    iExists (λ v, ∃ l : loc, ⌜v = #l⌝ ∗ l ↦U #1)%I, (λ v, l ↦U #1)%I.
    repeat iSplitL; eauto.
    iIntros (v1 v2). iDestruct 1 as (l' ->) "Hl'".
    iIntros "Hl". iExists l'. iSplit; eauto.
    iExists #1. iFrame.
  Qed.
*)