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

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

(** Bind. *)
15
Lemma wp_bind {E e} K Q :
16
  wp E e (λ v, wp E (fill K (of_val v)) Q)  wp E (fill K e) Q.
17
Proof. apply wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
18

19
(** Base axioms for core primitives of the language: Stateful reductions. *)
20
Lemma wp_alloc_pst E σ e v Q :
21
22
  to_val e = Some v 
  (ownP σ   ( l, (σ !! l = None)  ownP (<[l:=v]>σ) - Q (LocV l)))
23
        wp E (Alloc e) Q.
24
Proof.
25
26
27
  intros; set (φ e' σ' ef :=  l, e' = Loc l  σ' = <[l:=v]>σ  σ !! l = None
                                 ef = (None : option expr)).
  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last (by intros; inv_step; eauto); [].
28
  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
29
30
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
31
  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
32
33
34
  apply const_elim_l=>-[l [-> [-> [? ->]]]].
  rewrite right_id (forall_elim l) const_equiv //.
  by rewrite left_id wand_elim_r -wp_value'.
35
Qed.
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
  to_val e1 = None 
  head_reducible e1 σ1 
  ( e' σ' ef, head_step e1 σ1 e' σ' ef  ef = None  e' = of_val v2  σ' = σ2) 
  (ownP σ1   (ownP σ2 - Q v2))  wp E e1 Q.
Proof.
  intros He Hsafe Hstep.
  rewrite -(wp_lift_step E E (λ e' σ' ef, ef = None  e' = of_val v2  σ' = σ2) _ e1 σ1) //; last first. 
  { intros. by apply Hstep, prim_head_step. }
  { by apply head_reducible_reducible. }
  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
  apply forall_intro=>e2'; apply forall_intro=>σ2'.
  apply forall_intro=>ef; apply wand_intro_l.
  rewrite always_and_sep_l' -associative -always_and_sep_l'.
  apply const_elim_l=>-[-> [-> ->]] /=.
  rewrite -pvs_intro right_id -wp_value.
  by rewrite wand_elim_r.
Qed.


57
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
58
  σ !! l = Some v 
59
  (ownP σ   (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
60
Proof.
61
62
  intros; rewrite -(wp_lift_atomic_det_step σ v σ) //;
    last (by intros; inv_step; eauto).
Ralf Jung's avatar
Ralf Jung committed
63
Qed.
64

65
Lemma wp_store_pst E σ l e v v' Q :
66
67
  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
68
Proof.
69
  intros.
70
  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //;
71
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
72
Qed.
73

74
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
75
76
  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
77
Proof.
78
  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //;
79
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
80
Qed.
81

82
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
83
84
  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
85
Proof.
86
  intros.
87
  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //;
88
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
89
90
Qed.

91
92
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
93
   wp (Σ:=Σ) coPset_all e (λ _, True)  wp E (Fork e) (λ v, (v = LitUnitV)).
94
Proof.
95
96
97
98
99
100
  rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit  ef = Some e)) //=;
    last by intros; inv_step; eauto.
  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
  apply sep_intro_True_l; last done.
  by rewrite -wp_value' //; apply const_intro.
101
Qed.
102

103
104
105
106
Lemma wp_lift_pure_step E (φ : expr  Prop) Q e1 :
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  ef = None  φ e2) 
107
  (  e2,  φ e2  wp E e2 Q)  wp E e1 Q.
108
Proof.
109
110
111
112
  intros; rewrite -(wp_lift_pure_step E (λ e' ef, ef = None  φ e')) //=.
  apply later_mono, forall_mono=>e2; apply forall_intro=>ef.
  apply impl_intro_l, const_elim_l=>-[-> ?] /=.
  by rewrite const_equiv // left_id right_id.
113
Qed.
114

115
Lemma wp_rec E ef e v Q :
116
117
  to_val e = Some v 
   wp E ef.[Rec ef, e /] Q  wp E (App (Rec ef) e) Q.
118
Proof.
119
120
121
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = ef.[Rec ef, e /])
    Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
  by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
122
Qed.
123

124
Lemma wp_plus E n1 n2 Q :
125
   Q (LitNatV (n1 + n2))  wp E (Plus (LitNat n1) (LitNat n2)) Q.
126
Proof.
127
128
129
130
  rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=;
    last by intros; inv_step; eauto.
  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
131
Qed.
132

133
Lemma wp_le_true E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
134
  n1  n2 
135
   Q LitTrueV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
136
Proof.
137
138
139
140
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitTrue)) //=;
    last by intros; inv_step; eauto with lia.
  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
141
Qed.
142

143
Lemma wp_le_false E n1 n2 Q :
Ralf Jung's avatar
Ralf Jung committed
144
  n1 > n2 
145
   Q LitFalseV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
146
Proof.
147
148
149
150
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitFalse)) //=;
    last by intros; inv_step; eauto with lia.
  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
  by rewrite -wp_value'.
151
Qed.
152

153
Lemma wp_fst E e1 v1 e2 v2 Q :
154
  to_val e1 = Some v1  to_val e2 = Some v2 
155
  Q v1  wp E (Fst (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
156
Proof.
157
158
159
160
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1)) //=;
    last by intros; inv_step; eauto.
  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
161
Qed.
162

163
Lemma wp_snd E e1 v1 e2 v2 Q :
164
165
  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
166
Proof.
167
168
169
170
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2)) //=;
    last by intros; inv_step; eauto.
  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
  by rewrite -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
171
Qed.
172

173
Lemma wp_case_inl E e0 v0 e1 e2 Q :
174
175
  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
176
Proof.
177
178
179
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1.[e0/]) _
    (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
Ralf Jung's avatar
Ralf Jung committed
180
Qed.
181

182
Lemma wp_case_inr E e0 v0 e1 e2 Q :
183
184
  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
185
Proof.
186
187
188
  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2.[e0/]) _
    (Case (InjR e0) e1 e2)) //=; last by intros; inv_step; eauto.
  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
Ralf Jung's avatar
Ralf Jung committed
189
Qed.
190

Ralf Jung's avatar
Ralf Jung committed
191
(** Some derived stateless axioms *)
192
Lemma wp_le E n1 n2 P Q :
193
194
  (n1  n2  P   Q LitTrueV) 
  (n1 > n2  P   Q LitFalseV) 
195
  P  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
196
Proof.
197
198
199
  intros; destruct (decide (n1  n2)).
  * rewrite -wp_le_true; auto.
  * rewrite -wp_le_false; auto with lia.
Ralf Jung's avatar
Ralf Jung committed
200
Qed.
201

202
End lifting.