lifting.v 5.53 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
51
  to_val e = Some v  σ !! l = Some v' 
  (ownP σ   (ownP (<[l:=v]>σ) - Q LitUnitV))  wp E (Store (Loc l) e) Q.
Ralf Jung's avatar
Ralf Jung committed
52
Proof.
53
54
  intros. rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None)
    ?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
59
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
  (ownP σ   (ownP σ - Q LitFalseV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
60
Proof.
61
  intros. rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
62
    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
67
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
  (ownP σ   (ownP (<[l:=v2]>σ) - Q LitTrueV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
68
Proof.
69
70
  intros. rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None)
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
71
72
Qed.

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

83
Lemma wp_rec E erec e v Q :
84
  to_val e = Some v 
85
   wp E erec.[Rec erec, e /] Q  wp E (App (Rec erec) e) Q.
86
Proof.
87
88
  intros. rewrite -(wp_lift_pure_det_step (App _ _) erec.[Rec erec, e /] None)
    ?right_id //=; last by intros; inv_step; eauto.
89
Qed.
90

91
Lemma wp_plus E n1 n2 Q :
92
   Q (LitNatV (n1 + n2))  wp E (Plus (LitNat n1) (LitNat n2)) Q.
93
Proof.
94
95
  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None)
    ?right_id //; last by intros; inv_step; eauto.
96
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
97
Qed.
98

99
Lemma wp_le_true E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
100
  n1  n2 
101
   Q LitTrueV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
102
Proof.
103
  intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
Ralf Jung's avatar
Ralf Jung committed
104
    last by intros; inv_step; eauto with omega.
105
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
106
Qed.
107

108
Lemma wp_le_false E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
109
  n1 > n2 
110
   Q LitFalseV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
111
Proof.
112
  intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
Ralf Jung's avatar
Ralf Jung committed
113
    last by intros; inv_step; eauto with omega.
114
  by rewrite -wp_value'.
115
Qed.
116

117
Lemma wp_fst E e1 v1 e2 v2 Q :
118
  to_val e1 = Some v1  to_val e2 = Some v2 
119
  Q v1  wp E (Fst (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
120
Proof.
121
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
122
123
    last by intros; inv_step; eauto.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
124
Qed.
125

126
Lemma wp_snd E e1 v1 e2 v2 Q :
127
128
  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
129
Proof.
130
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
131
132
    last by intros; inv_step; eauto.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
133
Qed.
134

135
Lemma wp_case_inl E e0 v0 e1 e2 Q :
136
137
  to_val e0 = Some v0 
   wp E e1.[e0/] Q  wp E (Case (InjL e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
138
Proof.
139
140
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None)
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
141
Qed.
142

143
Lemma wp_case_inr E e0 v0 e1 e2 Q :
144
145
  to_val e0 = Some v0 
   wp E e2.[e0/] Q  wp E (Case (InjR e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
146
Proof.
147
148
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None)
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
149
Qed.
150

Ralf Jung's avatar
Ralf Jung committed
151
(** Some derived stateless axioms *)
152
Lemma wp_le E n1 n2 P Q :
153
154
  (n1  n2  P   Q LitTrueV) 
  (n1 > n2  P   Q LitFalseV) 
155
  P  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
156
Proof.
157
158
  intros; destruct (decide (n1  n2)).
  * rewrite -wp_le_true; auto.
Ralf Jung's avatar
Ralf Jung committed
159
  * rewrite -wp_le_false; auto with omega.
Ralf Jung's avatar
Ralf Jung committed
160
Qed.
161

162
End lifting.