lifting.v 6.24 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.program_logic Require Import ectx_lifting.
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import tactics.
5
From iris.proofmode Require Import tactics.
6
From iris.prelude Require Import fin_maps.
7
Import uPred.
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : head_step ?e _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.

Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
30

31
Section lifting.
32
33
34
Context `{irisG heap_lang Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
35
Implicit Types efs : list expr.
36
Implicit Types σ : state.
Ralf Jung's avatar
Ralf Jung committed
37

38
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
39
Lemma wp_bind {E e} K Φ :
40
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
41
Proof. exact: wp_ectx_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
42

43
Lemma wp_bind_ctxi {E e} Ki Φ :
Ralf Jung's avatar
Ralf Jung committed
44
45
46
47
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

48
(** Base axioms for core primitives of the language: Stateful reductions. *)
49
50
Lemma wp_alloc_pst E σ v :
  {{{  ownP σ }}} Alloc (of_val v) @ E
Ralf Jung's avatar
Ralf Jung committed
51
  {{{ l, RET LitV (LitLoc l); ⌜σ !! l = None  ownP (<[l:=v]>σ) }}}.
52
Proof.
Ralf Jung's avatar
Ralf Jung committed
53
  iIntros (Φ) "HP HΦ".
54
  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
Ralf Jung's avatar
Ralf Jung committed
55
  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
56
  iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
57
Qed.
58

59
Lemma wp_load_pst E σ l v :
Ralf Jung's avatar
Ralf Jung committed
60
  σ !! l = Some v 
61
  {{{  ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
Ralf Jung's avatar
Ralf Jung committed
62
Proof.
63
  intros ? Φ. apply wp_lift_atomic_det_head_step'; eauto.
64
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
65
Qed.
66

67
Lemma wp_store_pst E σ l v v' :
68
  σ !! l = Some v' 
69
  {{{  ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
70
  {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
Ralf Jung's avatar
Ralf Jung committed
71
Proof.
72
  intros. apply wp_lift_atomic_det_head_step'; eauto.
73
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
74
Qed.
75

76
Lemma wp_cas_fail_pst E σ l v1 v2 v' :
77
  σ !! l = Some v'  v'  v1 
78
  {{{  ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
79
  {{{ RET LitV $ LitBool false; ownP σ }}}.
Ralf Jung's avatar
Ralf Jung committed
80
Proof.
81
  intros. apply wp_lift_atomic_det_head_step'; eauto.
82
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
83
Qed.
84

85
Lemma wp_cas_suc_pst E σ l v1 v2 :
86
  σ !! l = Some v1 
87
  {{{  ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
88
  {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
Ralf Jung's avatar
Ralf Jung committed
89
Proof.
90
  intros. apply wp_lift_atomic_det_head_step'; eauto.
91
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
92
93
Qed.

94
(** Base axioms for core primitives of the language: Stateless reductions *)
95
Lemma wp_fork E e Φ :
96
   Φ (LitV LitUnit)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
97
Proof.
98
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
99
  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
100
  - intros; inv_head_step; eauto.
101
Qed.
102

103
Lemma wp_rec E f x erec e1 e2 Φ :
104
  e1 = Rec f x erec 
105
  is_Some (to_val e2) 
106
  Closed (f :b: x :b: []) erec 
Robbert Krebbers's avatar
Robbert Krebbers committed
107
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
108
Proof.
109
110
  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step' (App _ _)
    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
111
  intros; inv_head_step; eauto.
112
Qed.
113

114
Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} :
115
116
117
  e1 = of_val $ locked (RecV f x erec) 
  is_Some (to_val e2) 
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
118
Proof. unlock. auto using wp_rec. Qed.
119

120
121
122
Lemma wp_un_op E op e v v' Φ :
  to_val e = Some v 
  un_op_eval op v = Some v' 
123
   Φ v'  WP UnOp op e @ E {{ Φ }}.
124
Proof.
125
  intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
126
    -?wp_value'; eauto.
127
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
128
Qed.
129

130
131
132
Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  bin_op_eval op v1 v2 = Some v' 
133
   (Φ v')  WP BinOp op e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
134
Proof.
135
  intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
136
    -?wp_value'; eauto.
137
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
138
Qed.
139

140
Lemma wp_if_true E e1 e2 Φ :
141
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
142
Proof.
143
  apply wp_lift_pure_det_head_step'; eauto.
144
  intros; inv_head_step; eauto.
145
146
Qed.

147
Lemma wp_if_false E e1 e2 Φ :
148
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
149
Proof.
150
  apply wp_lift_pure_det_head_step'; eauto.
151
  intros; inv_head_step; eauto.
152
Qed.
153

154
155
Lemma wp_fst E e1 v1 e2 Φ :
  to_val e1 = Some v1  is_Some (to_val e2) 
156
   Φ v1  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
157
Proof.
158
  intros ? [v2 ?].
159
  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value; eauto.
160
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
161
Qed.
162

163
164
Lemma wp_snd E e1 e2 v2 Φ :
  is_Some (to_val e1)  to_val e2 = Some v2 
165
   Φ v2  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
166
Proof.
167
  intros [v1 ?] ?.
168
  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value; eauto.
169
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
170
Qed.
171

172
173
Lemma wp_case_inl E e0 e1 e2 Φ :
  is_Some (to_val e0) 
174
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
175
Proof.
176
177
  intros [v0 ?].
  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e1 e0)); eauto.
178
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
179
Qed.
180

181
182
Lemma wp_case_inr E e0 e1 e2 Φ :
  is_Some (to_val e0) 
183
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
184
Proof.
185
186
  intros [v0 ?].
  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e2 e0)); eauto.
187
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
188
Qed.
189
End lifting.