vcgen.v 17.8 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
2
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
3
From iris_c.vcgen Require Import dcexpr.
Dan Frumin's avatar
Dan Frumin committed
4
5
6
7
8
9
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

Section vcg.
  Context `{amonadG Σ}.

10
11

  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
    | Base : iProp Σ  wp_expr
    | Inhale : dloc  (dval  wp_expr)  wp_expr
    | Exhale : dloc  dval  level  wp_expr  wp_expr
    | IsSome {A} : doption A  (A  wp_expr)  wp_expr
    | IsLoc : dval  (dloc  wp_expr)  wp_expr
    | UMod : wp_expr  wp_expr
    | Par :
       ((dval  iProp Σ)  wp_expr) 
       ((dval  iProp Σ)  wp_expr) 
       (dval  dval  wp_expr)  wp_expr.
   Arguments Base _%I.

  Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
    match a with
    | Base P => P
    | Inhale dl Φ =>
       dv, dloc_interp E dl U dval_interp E dv  wp_interp E (Φ dv)
    | Exhale dl dv x Φ =>
      dloc_interp E dl [x] dval_interp E dv - wp_interp E Φ
    | 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)
    | Par P1 P2 P3 =>  (Ψ1 Ψ2 : dval  iProp Σ),
       wp_interp E (P1 Ψ1) 
       wp_interp E (P2 Ψ2) 
        (dv1 dv2 : dval), Ψ1 dv1 - Ψ2 dv2 - wp_interp E (P3 dv1 dv2)
  end%I.

  Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
    match a with
    | Base Φ => Φ
    | Inhale dl Φ =>
       v, dloc_interp E dl U v  wp_interp_sane E (Φ (dValUnknown v))
    | Exhale dl dv x Φ =>
      dloc_interp E dl [x] dval_interp E dv - wp_interp_sane E Φ
    | 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 Σ,
       wp_interp_sane E (P1 (λ dv, Ψ1 (dval_interp E dv))) 
       wp_interp_sane E (P2 (λ dv, Ψ2 (dval_interp E dv))) 
        v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
  end%I.

59
60
61
62
63
64
65
66

  Fixpoint vcg_wp (E: list loc) (s: list (nat * dval)) (de : dcexpr) (t: dval  wp_expr) : wp_expr :=
    match de with
    | dCVal dv => t dv
    | dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (t w))))
    | _ => t (dValUnknown #())
    end.

Dan Frumin's avatar
Dan Frumin committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
  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". 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 (λ dv, Ψ1 (dval_interp E dv)), (λ dv, Ψ2 (dval_interp E dv)).
      iSplitL "HΨ1". by iApply H0.
      iSplitL "HΨ2". by iApply H1.
      iIntros (dv1 dv2) "Hv1 Hv2". iApply H2.
86
87
88
89
      admit.
Admitted.

 (* No need for those classes any more)
Dan Frumin's avatar
Dan Frumin committed
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141

  Class AWpQuote (E : list loc) (e : expr) (R : iProp Σ) (Φ : dval → wp_expr) (t : wp_expr) :=
    wp_quote :
      wp_interp E t ⊢
      awp e R (λ v, ∃ dv, ⌜ dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv)).

  Global Instance awp_quote_default E e R Φ :
    AWpQuote E e R Φ (Base (awp e R (λ v, wp_interp E (Φ (dValUnknown v))))) | 1000.
  Proof.
    rewrite /AWpQuote /=. iIntros "H". iApply (awp_wand with "H").
    iIntros (v) "H". iExists (dValUnknown v); auto.
  Qed.

  (* TODO: awp ret for a general expression *)
  Instance awp_quote_ret E e dv R Φ :
    IntoDVal E e dv → AWpQuote E (a_ret e) R Φ (Φ dv).
  Proof.
    rewrite /AWpQuote. iIntros (->) "H".
    iApply awp_ret. iApply wp_value. eauto.
  Qed.

  Global Instance awp_quote_load E e R Φ t :
    AWpQuote E e R (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (Φ w)))) t →
    AWpQuote E (a_load e) R Φ t.
  Proof.
    rewrite /AWpQuote /= => ->. iIntros "H".
    awp_apply (a_wp_awp with "H").
    iIntros (a) "Ha".
    iApply a_load_spec.
    iApply (awp_wand with "Ha").
    iIntros (?). iDestruct 1 as (dv <- l -> w) "[Hl H]".
    iExists _, _; iSplit; eauto. iFrame "Hl".
    iIntros "Hl". iExists _; iSplit; eauto.
    by iApply "H".
  Qed.

  Global Instance wp_quote_store E e1 e2 R Φ (t1 t2 : ((dval → iProp Σ) → wp_expr)) :
    (∀ Ψ1 : dval → iProp Σ, AWpQuote E e1 R (λ v1, IsLoc v1 (λ l, Base (Ψ1 (dValUnknown #(dloc_interp E l)))))
                                     (t1 Ψ1)) →
    (∀ Ψ2 : dval → iProp Σ, AWpQuote E e2 R (λ v, Base (Ψ2 (dValUnknown (dval_interp E v))))
                                     (t2 Ψ2)) →
    AWpQuote E (a_store e1 e2) R Φ
             (Par t1 t2 (λ v1 v2, IsLoc v1 (λ l, Inhale l (λ _, Exhale l v2 LLvl (Φ v2))))).
  Proof.
    rewrite /AWpQuote /= => He1 He2.
    iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
    iApply (a_store_spec _ _ (λ l, Ψ1 (dValUnknown #l))
                         (λ v, Ψ2 (dValUnknown v)) with "[HΨ1] [HΨ2]").
    - iPoseProof (He1 with "HΨ1") as "H".
      iApply (awp_wand with "H"). iIntros (?).
      iDestruct 1 as (dv <- dl ?) "HΨ1". iExists _.
      iSplit; eauto.
142
    - iPoseProof (He2 with "HΨ2") as "H".
Dan Frumin's avatar
Dan Frumin committed
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
      iApply (awp_wand with "H"). iIntros (?).
      iDestruct 1 as (dv <-) "$".
    - iNext. iIntros (l w) "HΨ1 HΨ2".
      iDestruct ("HΦ" with "HΨ1 HΨ2") as (dl ?) "H".
      iDestruct "H" as (dv) "[Hl H]". simplify_eq/=.
      iExists _; iFrame. iIntros "Hl".
      iExists (dValUnknown w); iSplit; eauto. by iApply "H".
  Qed.

  (*
  Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
   (∀ dv1, WpQuote E e2 (λ dv2, IsSome (dbin_op_eval E op dv1 dv2) Φ) (Ψ dv1)) →
   WpQuote E e1 Ψ t → WpQuote E (BinOp op e1 e2) Φ t.
  Proof.
    rewrite /WpQuote /= => He2 ->. iIntros "H".
    wp_apply (wp_wand with "H"); iIntros (v1).
    iDestruct 1 as (dv <-) "H". rewrite He2.
    wp_apply (wp_wand with "H"); iIntros (v2).
    iDestruct 1 as (dv' <- w ?) "H".
    wp_op.
    - by apply dbin_op_eval_correct.
    - iExists w. auto.
165
  Qed.
Dan Frumin's avatar
Dan Frumin committed
166
167
168
169
170
171
172
173
174
175
176
177
178
179


  Global Instance wp_quote_seq E e1 e2 Φ Ψ t `{Closed [] e2}:
    WpQuote E e2 Φ Ψ →
    WpQuote E e1 (λ _, Ψ) t →
    WpQuote E (e1 ;; e2) Φ t.
  Proof.
    rewrite /WpQuote /= => He2 ->. iIntros "H".
    wp_apply (wp_wand with "H"). iIntros (v1).
    iDestruct 1 as (dv1 <-) "H". wp_seq.
    by rewrite He2.
  Qed.
   *)

180
181
*)

Dan Frumin's avatar
Dan Frumin committed
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
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
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
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
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
  Fixpoint exhale_list (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
    match s with
    | (i, v) :: s' => Exhale (dLoc i) v ULvl (exhale_list s' Φ)
    | [] => Φ
    end.

  Definition exhale_list_interp E (pl : list (nat * dval)) : iProp Σ :=
    ([ list] lw  pl, dloc_interp E (dLoc lw.1) U dval_interp E lw.2)%I.


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

  Fixpoint find_and_remove (pl: list (nat * dval)) (dl: dloc) :
    option (list (nat * dval) * dval) :=
    match pl with
    | [] => None
    | (i,v) :: pl' =>
      if (bool_decide (dl = dLoc i)) then Some (pl', v)
      else match find_and_remove pl' dl with
           | None => None
           | Some (rl, w) => Some ((i,v) :: rl, w)
           end
    end.

  Lemma find_and_remove_dLocUnknown pl l :
    find_and_remove pl (dLocUnknown l) =  None.
  Proof. induction pl as [|[? ?] ?]; eauto; simpl; by rewrite IHpl. Qed.

  Lemma find_and_remove_dLocKnown pl pl' d w' :
    find_and_remove pl d = Some (pl', w')   i, d = dLoc i.
  Proof.
    case d; eauto; intros ?; rewrite find_and_remove_dLocUnknown; inversion 1.
  Qed.

  Lemma find_and_remove_big_sepL pl i pl' w' (Φ : nat * dval  iProp Σ) :
    find_and_remove pl (dLoc i) = Some (pl', w') 
    ([ list] lw  pl, Φ lw)%I  (([ list] lw  pl', Φ lw)  Φ (i, w'))%I.
  Proof.
    iIntros (Hfind). iInduction pl as [|hd tl] "IH" forall (pl' Hfind);
     simpl; iSplit; try (done || simpl in H0; case_bool_decide;
     simplify_eq /=; iIntros "[H1 H2]"; iFrame); simpl in Hfind; destruct hd;
     iIntros "[HΦ Hlst]"; case_bool_decide; simplify_eq /=; [iFrame| |iFrame|].
     - destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
       destruct p; simplify_eq /=. iFrame. by iApply "IH".
     - destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
       destruct p; simplify_eq /=. iDestruct "HΦ" as "[HΦ Hl]".
       iFrame. iApply ("IH" $! l); first done. iFrame.
  Qed.

  Fixpoint mem (s : list (nat * dval)) (i: nat) : bool :=
    match s with
    | [] => false
    | (j, _) :: s' => if (bool_decide (i = j)) then true else mem s' i
    end.

  Lemma mem_no_dup s i : false = mem s i  i  s.*1.
  Proof.
    induction s; intros Hf.
    - by apply not_elem_of_nil.
    -  apply not_elem_of_cons. simpl in Hf. destruct a as [i' ?].
       case_bool_decide; first done. naive_solver.
  Qed.

  Fixpoint optimize (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
    match Φ with
    | Base Φ1 => exhale_list s Φ
    | Inhale dl Φ1 =>
      match find_and_remove s dl with
      | None  => Inhale dl (λ v, optimize s (Φ1 v))
      | Some (s', w) => optimize s' (Φ1 w)
      end
    | Exhale (dLoc i) w ULvl Φ =>
      if mem s i then Base False
      else optimize ((i,w) :: s) Φ
    | Exhale (dLoc i) w LLvl Φ => Exhale (dLoc i) w LLvl (optimize s Φ)
    | Exhale (dLocUnknown l) w x Φ => Exhale (dLocUnknown l) w x (optimize s Φ)
    | IsSome dmx Φ1 =>
      match dmx with
      | dNone => Base False
      | dSome x => optimize s (Φ1 x)
      | _ => IsSome dmx (λ v, optimize s (Φ1 v))
      end
    | IsLoc dv Φ1 =>
      match dv with
      | dLitV (dLitLoc l) => optimize s (Φ1 l)
      | dLitV (dLitUnknown _) | dValUnknown _ =>
        IsLoc dv (λ v, optimize s (Φ1 v))
      | _ => Base False
      end
    | UMod P => UMod (optimize s P)
    | Par P1 P2 P3 => Par (λ Ψ1, optimize s (P1 Ψ1))
                          (λ Ψ2, optimize s (P2 Ψ2))
                          (λ v1 v2, optimize s (P3 v1 v2))
    end.

  Lemma vcg_opt_list_sound' (E: list loc) (pl: list (nat * dval)) (Φ: wp_expr) :
      wp_interp E (optimize pl Φ) -
      exhale_list_interp E pl - (wp_interp E Φ).
  Proof. (*
    generalize dependent pl.
    induction Φ; simpl.
    - intros. eapply vcg_exhale_list_sound'.
    - intros pl.
      remember (find_and_remove pl d) as far. destruct far.
      + iIntros "Hw He".
        destruct d; last by rewrite find_and_remove_dLocUnknown in Heqfar.
        unfold exhale_list_interp. symmetry in Heqfar. destruct p.
        apply find_and_remove_big_sepL
          with (Φ := λ lw, (dloc_interp E (dLoc lw.1) ↦ dval_interp E lw.2)%I)
          in Heqfar. rewrite Heqfar.
        iDestruct "He" as "[Hlst Hp]".
        iExists d. iFrame. rewrite H0. by iApply "Hw".
      +  iIntros "Hwp Hexh". simplify_eq /=.
         iDestruct "Hwp" as (d0) "[Hp Hwp]". rewrite H0.
         iExists d0. iFrame. by iApply "Hwp".
    -  intros pl.
       destruct d as [i|l].
      + remember (mem pl i) as msi. destruct msi.
        { iIntros "?"; done. }
        iIntros "Hwp Hl Hi". rewrite IHΦ /exhale_list_interp.
        iApply "Hwp". rewrite big_opL_cons. iFrame.
      + simpl. iIntros "Hwp Hexh Hl".
        rewrite IHΦ. by iApply ("Hwp" with "[Hl] [Hexh]").
    - intros pl. 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.
    - intros pl. 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.
  Qed. *) Admitted.

  Import environments.
  Import env_notations.
  From iris.proofmode Require Import coq_tactics.

 Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : list (loc * val)) := {
    mapsto_list_from_env : [] Γin  [] Γout  [ list] p  Γls, p.1 U p.2;
    mapsto_list_from_env_wf : env_wf Γin  env_wf Γout;
    mapsto_list_from_env_lookup_None i: Γin !! i = None  Γout !! i = None
  }.

  Global Instance mapsto_list_from_env_nil : MapstoListFromEnv Enil Enil nil.
  Proof. split; eauto. Qed.

  Global Instance mapsto_list_from_env_snoc_Γout Γin Γout Γls i P  :
    MapstoListFromEnv Γin Γout Γls 
    MapstoListFromEnv (Esnoc Γin i P) (Esnoc Γout i P) Γls | 100.
  Proof.
     destruct 1; split; simpl.
    - rewrite mapsto_list_from_env0. iIntros "(H1 & H2 & H3)". iFrame.
    - intro Hwf. inversion Hwf; subst. apply mapsto_list_from_env_wf0 in H4.
      apply Esnoc_wf; last done. by apply mapsto_list_from_env_lookup_None0.
    - intros j Hj. destruct (ident_beq j i); simplify_eq /=.
        by apply mapsto_list_from_env_lookup_None0.
  Qed.

   Global Instance mapsto_list_from_env_snoc_Γls Γin Γout Γls i l v :
    MapstoListFromEnv Γin Γout Γls 
    MapstoListFromEnv (Esnoc Γin i (l U v)) Γout ((l,v)::Γls).
  Proof.
    destruct 1.
    split.
    - iIntros "H". simpl. iDestruct "H" as "[H1 H2]". iFrame.
      by rewrite mapsto_list_from_env0.
    - intros Heq. inversion Heq; simplify_eq /=. by apply mapsto_list_from_env_wf0.
    - intros j Hsnoc. apply mapsto_list_from_env_lookup_None0.
      destruct (decide (i = j)) as [->|]. simplify_eq /=. by destruct (ident_beq j j ).
        by rewrite env_lookup_snoc_ne in Hsnoc.
  Qed.

  Definition env_to_known_locs (Γls : list (loc * val)) : list loc := map fst Γls.

  Class ListOfMapsto (Γls : list (loc * val)) (E : list loc) (ps : list (nat * dval)) :=
    list_of_mapsto : ([ list] p  Γls, p.1 U p.2)  exhale_list_interp E ps.

  Global Instance list_of_mapsto_Nil E : ListOfMapsto [] E [].
  Proof. unfold ListOfMapsto. simpl. eauto. Qed.

  Global Instance list_of_mapsto_cons_dLitV E Γls ps lit dlit i l :
    BaseLitQuote E lit dlit 
    LocLookup E l i 
    ListOfMapsto Γls E ps 
    ListOfMapsto ((l,LitV lit)::Γls) E ((i,dLitV dlit)::ps).
  Proof.
    rewrite /BaseLitQuote /LocLookup => Hlit Hi.
    rewrite /ListOfMapsto => HΓls /=.
    iDestruct 1 as "[Hl H]". cbn.
    rewrite Hi Hlit HΓls. iFrame.
  Qed.

  Global Instance list_of_mapsto_cons_dValUnknown E Γls ps v i l :
    LocLookup E l i 
    ListOfMapsto Γls E ps 
    ListOfMapsto ((l,v)::Γls) E ((i,dValUnknown v)::ps) | 100.
  Proof.
    rewrite /BaseLitQuote /LocLookup => Hi.
    rewrite /ListOfMapsto => HΓls /=.
    iDestruct 1 as "[Hl H]". cbn.
    rewrite Hi HΓls. iFrame.
  Qed.

  Lemma tac_envs_split_mapsto  Γs_in Γs_out Γls Γp c ps P:
    MapstoListFromEnv Γs_in Γs_out Γls 
    ListOfMapsto Γls (env_to_known_locs Γls) ps 
    envs_entails (Envs Γp Γs_out c) (exhale_list_interp (env_to_known_locs Γls) ps - P)%I 
    envs_entails (Envs Γp Γs_in c) P.
  Proof.
    intros Hsplit. rewrite /ListOfMapsto coq_tactics.envs_entails_eq=> Hexhale.
    unfold of_envs. simpl.
    rewrite mapsto_list_from_env. intros Hz.
    iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
    iApply (Hz with "[Hs]").
    - iFrame "Hp Hs". iPureIntro.
      split; eauto.
      + apply Hwf.
      + apply Hsplit. apply Hwf.
      + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
        * by left.
        * right. by apply Hsplit.
    - by iApply Hexhale.
  Qed.

418
 (* Lemma tac_vcg_opt_list_sound Γs_in Γs_out Γls Γp ps c e R Φ E t :
Dan Frumin's avatar
Dan Frumin committed
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
    MapstoListFromEnv Γs_in Γs_out Γls →
    E = env_to_known_locs Γls →
    ListOfMapsto Γls E ps →
    AWpQuote E e R (λ dv, Base (Φ (dval_interp E dv))) t →
    coq_tactics.envs_entails (Envs Γp Γs_out c) ((wp_interp_sane E (optimize ps t))) →
    coq_tactics.envs_entails (Envs Γp Γs_in c) (awp e R Φ).
  Proof.
    rewrite /AWpQuote /= => Hsplit ->.
    rewrite /ListOfMapsto=> Hexhale Hquote => Hgoal.
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite coq_tactics.envs_entails_eq.
    rewrite wp_interp_sane_sound vcg_opt_list_sound' /exhale_list_interp.
    rewrite Hquote. simpl. intros ->. iIntros "H1 H2".
    iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
    iIntros (v) "H". by iDestruct "H" as (dv) "[-> H2]".
  Qed.

End vcg.

Hint Extern 50 (AWpQuote _ _ _ _ _) =>
  notypeclasses refine (awp_quote_ret _ _ _ _ _ _) : typeclass_instances.

Ltac vcg_opt :=
  eapply tac_vcg_opt_list_sound;
    [ apply _
    | compute; reflexivity
    | apply _
    | apply _
    | simpl ].

Section Tests_vcg.
  Context `{amonadG Σ}.

  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_opt. eauto.
  Qed.

  Lemma test2 (l : loc) :
    l ↦U #1 -∗
    awp (a_store (a_ret #l) (a_ret #3))%E True (fun v => ⌜v = #1⌝ ∗ l ↦L #3).
  Proof.
    iIntros "Hl".
    vcg_opt. 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.
471
472
*)
End vcg.