lifting.v 5.7 KB
Newer Older
1
From program_logic Require Export weakestpre.
2
From heap_lang Require Export lang.
3
4
5
From program_logic Require Import lifting.
From program_logic Require Import ownership. (* for ownP *)
From heap_lang Require Import tactics.
6
7
Export heap_lang. (* Prefer heap_lang names over language names. *)
Import uPred.
8
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
9

10
Section lifting.
11
Context {Σ : iFunctor}.
12
13
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
14
Implicit Types K : ectx.
15
Implicit Types ef : option expr.
Ralf Jung's avatar
Ralf Jung committed
16
17

(** Bind. *)
18
19
Lemma wp_bind {E e} K Φ :
  wp E e (λ v, wp E (fill K (of_val v)) Φ)  wp E (fill K e) Φ.
20
21
Proof. apply weakestpre.wp_bind. Qed.

22
23
Lemma wp_bindi {E e} Ki Φ :
  wp E e (λ v, wp E (fill_item Ki (of_val v)) Φ)  wp E (fill_item Ki e) Φ.
24
Proof. apply weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
25

26
(** Base axioms for core primitives of the language: Stateful reductions. *)
27
Lemma wp_alloc_pst E σ e v Φ :
28
  to_val e = Some v 
29
30
  (ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) - Φ (LocV l)))
        wp E (Alloc e) Φ.
31
Proof.
32
  (* TODO RJ: This works around ssreflect bug #22. *)
33
34
  intros. set (φ v' σ' ef :=  l,
    ef = None  v' = LocV l  σ' = <[l:=v]>σ  σ !! l = None).
35
  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
Ralf Jung's avatar
Ralf Jung committed
36
    last by intros; inv_step; eauto 8.
37
  apply sep_mono, later_mono; first done.
38
39
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
40
  rewrite always_and_sep_l -assoc -always_and_sep_l.
41
42
  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
43
Qed.
44

45
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
46
  σ !! l = Some v 
47
  (ownP σ   (ownP σ - Φ v))  wp E (Load (Loc l)) Φ.
Ralf Jung's avatar
Ralf Jung committed
48
Proof.
49
50
  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
    last by intros; inv_step; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
51
Qed.
52

53
Lemma wp_store_pst E σ l e v v' Φ :
54
  to_val e = Some v  σ !! l = Some v' 
55
  (ownP σ   (ownP (<[l:=v]>σ) - Φ (LitV LitUnit)))  wp E (Store (Loc l) e) Φ.
Ralf Jung's avatar
Ralf Jung committed
56
Proof.
57
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
58
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
59
Qed.
60

61
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
62
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
63
  (ownP σ   (ownP σ - Φ (LitV $ LitBool false)))  wp E (Cas (Loc l) e1 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
64
Proof.
Ralf Jung's avatar
Ralf Jung committed
65
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
66
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
67
Qed.
68

69
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
70
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
71
72
  (ownP σ   (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true)))
   wp E (Cas (Loc l) e1 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
73
Proof.
Ralf Jung's avatar
Ralf Jung committed
74
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
75
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
76
77
Qed.

78
(** Base axioms for core primitives of the language: Stateless reductions *)
79
80
Lemma wp_fork E e Φ :
  ( Φ (LitV LitUnit)   wp (Σ:=Σ)  e (λ _, True))  wp E (Fork e) Φ.
81
Proof.
82
  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
83
    last by intros; inv_step; eauto.
84
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
85
Qed.
86

87
88
(* For the lemmas involving substitution, we only derive a preliminary version.
   The final version is defined in substitution.v. *)
89
Lemma wp_rec' E f x e1 e2 v Φ :
90
  to_val e2 = Some v 
91
   wp E (subst (subst e1 f (RecV f x e1)) x v) Φ  wp E (App (Rec f x e1) e2) Φ.
92
Proof.
93
  intros. rewrite -(wp_lift_pure_det_step (App _ _)
94
    (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
95
    intros; inv_step; eauto.
96
Qed.
97

98
Lemma wp_un_op E op l l' Φ :
99
  un_op_eval op l = Some l' 
100
   Φ (LitV l')  wp E (UnOp op (Lit l)) Φ.
101
Proof.
102
  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
103
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
104
Qed.
105

106
Lemma wp_bin_op E op l1 l2 l' Φ :
107
  bin_op_eval op l1 l2 = Some l' 
108
   Φ (LitV l')  wp E (BinOp op (Lit l1) (Lit l2)) Φ.
Ralf Jung's avatar
Ralf Jung committed
109
Proof.
110
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
111
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
112
Qed.
113

114
115
Lemma wp_if_true E e1 e2 Φ :
   wp E e1 Φ  wp E (If (Lit $ LitBool true) e1 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
116
Proof.
117
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
118
    ?right_id //; intros; inv_step; eauto.
119
120
Qed.

121
122
Lemma wp_if_false E e1 e2 Φ :
   wp E e2 Φ  wp E (If (Lit $ LitBool false) e1 e2) Φ.
123
124
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
125
    ?right_id //; intros; inv_step; eauto.
126
Qed.
127

128
Lemma wp_fst E e1 v1 e2 v2 Φ :
129
  to_val e1 = Some v1  to_val e2 = Some v2 
130
   Φ v1  wp E (Fst $ Pair e1 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
131
Proof.
132
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
133
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
134
Qed.
135

136
Lemma wp_snd E e1 v1 e2 v2 Φ :
137
  to_val e1 = Some v1  to_val e2 = Some v2 
138
   Φ v2  wp E (Snd $ Pair e1 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
139
Proof.
140
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
141
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
142
Qed.
143

144
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Φ :
145
  to_val e0 = Some v0 
146
   wp E (subst e1 x1 v0) Φ  wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
147
Proof.
148
149
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
    (subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
150
Qed.
151

152
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Φ :
153
  to_val e0 = Some v0 
154
   wp E (subst e2 x2 v0) Φ  wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
Ralf Jung's avatar
Ralf Jung committed
155
Proof.
156
157
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
    (subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
158
Qed.
159

160
End lifting.