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

9
Section lifting.
10
Context {Σ : iFunctor}.
11 12
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
13
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 Φ :
18 19
  WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
20

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

42
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
43
  σ !! l = Some v 
44
  ( ownP σ   (ownP σ - Φ v))  WP Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
45
Proof.
46
  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
47
    last (by intros; inv_step; eauto using to_of_val); simpl; by eauto.
Ralf Jung's avatar
Ralf Jung committed
48
Qed.
49

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

59
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
60
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
61
  ( ownP σ   (ownP σ - Φ (LitV $ LitBool false)))
62
   WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
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 66
    ?right_id //; last (by intros; inv_step; eauto);
    simpl; split_and?; by eauto.
Ralf Jung's avatar
Ralf Jung committed
67
Qed.
68

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

79
(** Base axioms for core primitives of the language: Stateless reductions *)
80
Lemma wp_fork E e Φ :
81
  ( Φ (LitV LitUnit)   WP e {{ λ _, True }})  WP Fork e @ E {{ Φ }}.
82
Proof.
83
  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
84
    last by intros; inv_step; eauto.
85
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
86
Qed.
87

88
Lemma wp_rec E f x e1 e2 v Φ :
89
  to_val e2 = Some v 
90 91
   WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
   WP App (Rec f x e1) e2 @ E {{ Φ }}.
92
Proof.
93
  intros. rewrite -(wp_lift_pure_det_step (App _ _)
94
    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
95
    intros; inv_step; eauto.
96
Qed.
97

98 99
Lemma wp_rec' E f x erec e1 e2 v2 Φ :
  e1 = Rec f x erec 
100
  to_val e2 = Some v2 
101 102
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
   WP App e1 e2 @ E {{ Φ }}.
103 104
Proof. intros ->. apply wp_rec. Qed.

105
Lemma wp_un_op E op l l' Φ :
106
  un_op_eval op l = Some l' 
107
   Φ (LitV l')  WP UnOp op (Lit l) @ E {{ Φ }}.
108
Proof.
109
  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
110
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
111
Qed.
112

113
Lemma wp_bin_op E op l1 l2 l' Φ :
114
  bin_op_eval op l1 l2 = Some l' 
115
   Φ (LitV l')  WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
116
Proof.
117
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
118
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
119
Qed.
120

121
Lemma wp_if_true E e1 e2 Φ :
122
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
123
Proof.
124
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
125
    ?right_id //; intros; inv_step; eauto.
126 127
Qed.

128
Lemma wp_if_false E e1 e2 Φ :
129
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
130 131
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
132
    ?right_id //; intros; inv_step; eauto.
133
Qed.
134

135
Lemma wp_fst E e1 v1 e2 v2 Φ :
136
  to_val e1 = Some v1  to_val e2 = Some v2 
137
   Φ v1  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
138
Proof.
139
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
140
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
141
Qed.
142

143
Lemma wp_snd E e1 v1 e2 v2 Φ :
144
  to_val e1 = Some v1  to_val e2 = Some v2 
145
   Φ v2  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
146
Proof.
147
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
148
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
149
Qed.
150

151
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
152
  to_val e0 = Some v0 
153
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
154
Proof.
155 156
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
    (App e1 e0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
157
Qed.
158

159
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
160
  to_val e0 = Some v0 
161
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
162
Proof.
163 164
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
    (App e2 e0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
165
Qed.
166

167
End lifting.