lifting.v 5.36 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
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
6

7
Section lifting.
8
9
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
10
11
Implicit Types Q : val  iProp heap_lang Σ.
Implicit Types K : ectx.
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
Proof. apply wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
17

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

37
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
38
  σ !! l = Some v 
39
  (ownP σ   (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
40
Proof.
41
  intros; rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
42
    last (by intros; inv_step; eauto).
Ralf Jung's avatar
Ralf Jung committed
43
Qed.
44

45
Lemma wp_store_pst E σ l e v v' Q :
46
47
  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
48
Proof.
49
  intros.
50
  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None) ?right_id //;
51
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
52
Qed.
53

54
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
55
56
  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
57
Proof.
58
  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
59
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
60
Qed.
61

62
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
63
64
  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
65
Proof.
66
  intros.
67
  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None) ?right_id //;
68
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
69
70
Qed.

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

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

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

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

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

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

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

134
Lemma wp_case_inl E e0 v0 e1 e2 Q :
135
136
  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
137
Proof.
138
  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None) ?right_id //;
139
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
140
Qed.
141

142
Lemma wp_case_inr E e0 v0 e1 e2 Q :
143
144
  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
145
Proof.
146
  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None) ?right_id //;
147
    last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
148
Qed.
149

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

161
End lifting.