lifting.v 5.54 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import prelude.gmap program_logic.lifting program_logic.ownership.
2
Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
3
Import uPred heap_lang.
4
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
5

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

(** Bind. *)
14
Lemma wp_bind {E e} K Q :
15
  wp E e (λ v, wp E (fill K (of_val v)) Q)  wp E (fill K e) Q.
16 17 18 19 20
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
21

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

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

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

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

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

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

84 85 86
Lemma wp_rec E f x e1 e2 v Q :
  to_val e2 = Some v 
   wp E (subst (subst e1 f (RecV f x e1)) x v) Q  wp E (App (Rec f x e1) e2) Q.
87
Proof.
88 89 90
  intros. rewrite -(wp_lift_pure_det_step (App _ _)
    (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
    last by intros; inv_step; eauto.
91
Qed.
92

93 94 95
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.
96
Proof.
97
  intros Heval. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
98
    ?right_id //; last by intros; inv_step; eauto.
99
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
100
Qed.
101

102 103 104
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
105
Proof.
106 107
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
    ?right_id //; last by intros; inv_step; eauto.
108
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
109
Qed.
110

111
Lemma wp_if_true E e1 e2 Q :  wp E e1 Q  wp E (If (Lit LitTrue) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
112
Proof.
113 114 115 116
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
    ?right_id //; last by intros; inv_step; eauto.
Qed.

117
Lemma wp_if_false E e1 e2 Q :  wp E e2 Q  wp E (If (Lit LitFalse) e1 e2) Q.
118 119 120
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
    ?right_id //; last by intros; inv_step; eauto.
121
Qed.
122

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

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

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

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

157
End lifting.