lifting.v 6.19 KB
Newer Older
1
From iris.program_logic Require Export ectx_weakestpre.
2
From iris.program_logic Require Import ownership. (* for ownP *)
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import tactics.
5
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
7

8
Section lifting.
9
Context {Σ : iFunctor}.
10
11
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
12
Implicit Types ef : option (expr []).
Ralf Jung's avatar
Ralf Jung committed
13

14
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
15
Lemma wp_bind {E e} K Φ :
16
  WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
17
Proof. exact: wp_ectx_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
18

19
20
21
22
23
Lemma wp_bindi {E e} Ki Φ :
  WP e @ E {{ λ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

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

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

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

62
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
63
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
64
  ( ownP σ   (ownP σ - Φ (LitV $ LitBool false)))
65
   WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
66
Proof.
67
  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
Robbert Krebbers's avatar
Robbert Krebbers committed
68
    ?right_id //; last (by intros; inv_head_step; eauto);
69
    simpl; by eauto 10.
Ralf Jung's avatar
Ralf Jung committed
70
Qed.
71

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

82
(** Base axioms for core primitives of the language: Stateless reductions *)
83
Lemma wp_fork E e Φ :
84
  ( Φ (LitV LitUnit)   WP e {{ λ _, True }})  WP Fork e @ E {{ Φ }}.
85
Proof.
86
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    last by intros; inv_head_step; eauto.
88
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
89
Qed.
90

91
Lemma wp_rec E f x e1 e2 v Φ :
92
  to_val e2 = Some v 
93
94
   WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
   WP App (Rec f x e1) e2 @ E {{ Φ }}.
95
Proof.
96
  intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
97
    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    intros; inv_head_step; eauto.
99
Qed.
100

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

108
Lemma wp_un_op E op l l' Φ :
109
  un_op_eval op l = Some l' 
110
   Φ (LitV l')  WP UnOp op (Lit l) @ E {{ Φ }}.
111
Proof.
112
  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
Robbert Krebbers's avatar
Robbert Krebbers committed
113
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
114
Qed.
115

116
Lemma wp_bin_op E op l1 l2 l' Φ :
117
  bin_op_eval op l1 l2 = Some l' 
118
   Φ (LitV l')  WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
119
Proof.
120
  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
Robbert Krebbers's avatar
Robbert Krebbers committed
121
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
122
Qed.
123

124
Lemma wp_if_true E e1 e2 Φ :
125
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
126
Proof.
127
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    ?right_id //; intros; inv_head_step; eauto.
129
130
Qed.

131
Lemma wp_if_false E e1 e2 Φ :
132
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
133
Proof.
134
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    ?right_id //; intros; inv_head_step; eauto.
136
Qed.
137

138
Lemma wp_fst E e1 v1 e2 v2 Φ :
139
  to_val e1 = Some v1  to_val e2 = Some v2 
140
   Φ v1  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
141
Proof.
142
  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
144
Qed.
145

146
Lemma wp_snd E e1 v1 e2 v2 Φ :
147
  to_val e1 = Some v1  to_val e2 = Some v2 
148
   Φ v2  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
149
Proof.
150
  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
152
Qed.
153

154
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
155
  to_val e0 = Some v0 
156
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
157
Proof.
158
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
159
    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
160
Qed.
161

162
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
163
  to_val e0 = Some v0 
164
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
165
Proof.
166
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
167
    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
168
Qed.
169
End lifting.