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

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

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

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

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

44
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
45
  σ !! l = Some v 
46
  (ownP σ   (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
47
Proof.
48 49
  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
50
Qed.
51

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

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

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

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

87 88 89
(* For the lemmas involving substitution, we only derive a preliminary version.
   The final version is defined in substitution.v. *)
Lemma wp_rec' E f x e1 e2 v Q :
90
  to_val e2 = Some v 
91
   wp E (subst (subst e1 f (RecV f x e1)) x v) Q  wp E (App (Rec f x e1) e2) Q.
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 99 100
Lemma wp_un_op E op l l' Q :
  un_op_eval op l = Some l' 
   Q (LitV l')  wp E (UnOp op (Lit l)) Q.
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 107 108
Lemma wp_bin_op E op l1 l2 l' Q :
  bin_op_eval op l1 l2 = Some l' 
   Q (LitV l')  wp E (BinOp op (Lit l1) (Lit l2)) Q.
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

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

Ralf Jung's avatar
Ralf Jung committed
120
Lemma wp_if_false E e1 e2 Q :  wp E e2 Q  wp E (If (Lit $ LitBool false) e1 e2) Q.
121 122
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
123
    ?right_id //; intros; inv_step; eauto.
124
Qed.
125

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

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

142
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
143
  to_val e0 = Some v0 
144
   wp E (subst e1 x1 v0) Q  wp E (Case (InjL e0) x1 e1 x2 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
145
Proof.
146 147
  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
148
Qed.
149

150
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Q :
151
  to_val e0 = Some v0 
152
   wp E (subst e2 x2 v0) Q  wp E (Case (InjR e0) x1 e1 x2 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
153
Proof.
154 155
  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
156
Qed.
157

158
End lifting.