vcgen.v 4.53 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.
Dan Frumin's avatar
Dan Frumin committed
5
6
7
8
9
10
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.

Section vcg.
  Context `{amonadG Σ}.

11
  Inductive wp_expr :=
Dan Frumin's avatar
Dan Frumin committed
12
13
14
15
16
17
18
    | 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 :
19
20
       ((val  iProp Σ)  wp_expr) 
       ((val  iProp Σ)  wp_expr) 
Dan Frumin's avatar
Dan Frumin committed
21
       (dval  dval  wp_expr)  wp_expr.
22
  Arguments Base _%I.
Dan Frumin's avatar
Dan Frumin committed
23
24
25
26
27
28
29
30
31
32
33
34

  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)
35
    | Par P1 P2 P3 =>  (Ψ1 Ψ2 : val  iProp Σ),
Dan Frumin's avatar
Dan Frumin committed
36
37
       wp_interp E (P1 Ψ1) 
       wp_interp E (P2 Ψ2) 
38
        (v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
Dan Frumin's avatar
Dan Frumin committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
  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 Σ,
54
55
       wp_interp_sane E (P1 Ψ1) 
       wp_interp_sane E (P2 Ψ2) 
Dan Frumin's avatar
Dan Frumin committed
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
        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.
    - 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Φ)".
74
      iExists _,_.
Dan Frumin's avatar
Dan Frumin committed
75
76
      iSplitL "HΨ1". by iApply H0.
      iSplitL "HΨ2". by iApply H1.
77
78
      iIntros (v1 v2) "Hv1 Hv2". iApply H2.
      iApply ("HΦ" with "Hv1 Hv2").
Dan Frumin's avatar
Dan Frumin committed
79
80
  Qed.

81
82
83
84
85
  Fixpoint vcg_wp (E: list loc) (s: list (nat * (frac * dval))) (de : dcexpr) (Φ: dval  wp_expr) : wp_expr :=
    match de with
    | dCVal dv => Φ dv
    | dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (Φ w))))
    | _ => Φ (dValUnknown #())
Dan Frumin's avatar
Dan Frumin committed
86
87
    end.

88
89
90
91
  Lemma vcg_wp_correct R E s de Φ :
    wp_interp E (vcg_wp E s de Φ) 
    awp (dcexpr_interp E de) R (λ v,  dv, dval_interp E dv = v   wp_interp E (Φ dv)).
  Proof. Admitted.
Dan Frumin's avatar
Dan Frumin committed
92

93
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E F dce :
Dan Frumin's avatar
Dan Frumin committed
94
95
96
    MapstoListFromEnv Γs_in Γs_out Γls 
    E = env_to_known_locs Γls 
    ListOfMapsto Γls E ps 
97
98
99
100
    IntoDCexpr E e dce 
    vcg_wp E ps dce (λ dv, Base (Φ (dval_interp E dv))) = F 
    coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c) (exhale_list_interp E ps - wp_interp_sane E F) 
    coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
101
  Proof.
102
103
    rewrite /IntoDCexpr /=. intros Hsplit ->.
    rewrite /ListOfMapsto. intros Hexhale -> <- Hgoal.
Dan Frumin's avatar
Dan Frumin committed
104
105
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite coq_tactics.envs_entails_eq.
106
107
    rewrite wp_interp_sane_sound (vcg_wp_correct R) /exhale_list_interp.
    intros ->. iIntros "H1 H2".
Dan Frumin's avatar
Dan Frumin committed
108
    iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
109
    iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Dan Frumin's avatar
Dan Frumin committed
110
111
  Qed.

112
End vcg.