lifting.v 14.1 KB
Newer Older
1
From iris.algebra Require Import auth gmap.
2
From iris.base_logic Require Export gen_heap.
3
4
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
5
From iris.heap_lang Require Export lang proph_map.
6
From iris.heap_lang Require Import tactics.
7
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
8
From stdpp Require Import fin_maps.
9
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
10

11
12
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
13
  heapG_gen_heapG :> gen_heapG loc val Σ;
14
  heapG_proph_mapG :> proph_mapG proph_id val Σ
15
16
17
18
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
19
20
  state_interp σ κs _ :=
    (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I;
21
  fork_post _ := True%I;
22
23
24
25
}.

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
27
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
29
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
32

33
34
35
36
37
38
39
40
41
(** 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
42
  | H : head_step ?e _ _ _ _ _ |- _ =>
43
44
45
46
47
     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.

48
49
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
50

51
52
53
54
55
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
56
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
57
Local Hint Resolve to_of_val.
58

59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.

Local Ltac solve_atomic :=
  apply strongly_atomic_atomic, ectx_language_atomic;
    [inversion 1; naive_solver
    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].

Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Instance skip_atomic s  : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. solve_atomic. Qed.

Ralf Jung's avatar
fix TWP    
Ralf Jung committed
88
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
89
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
90
Local Ltac solve_pure_exec :=
91
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
92
    constructor; [solve_exec_safe | solve_exec_puredet].
93

94
95
96
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
97
98
99
100
101
102
103

(* Pure reductions are automatically performed before any wp_ tactics
   handling impure operations. Since we do not want these tactics to
   unfold locked terms, we do not register this instance explicitely,
   but only activate it by hand in the `wp_rec` tactic, where we
   *actually* want it to unlock. *)
Lemma AsRecV_recv_locked v f x e :
104
  AsRecV v f x e  AsRecV (locked v) f x e.
105
106
Proof. by unlock. Qed.

107
108
109
110
111
112
113
114
115
116
117
118
Instance pure_recc f x (erec : expr) :
  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Instance pure_pairc (v1 v2 : val) :
  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Instance pure_injlc (v : val) :
  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Instance pure_injrc (v : val) :
  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
119

120
121
122
123
124
125
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.

Instance pure_unop op v v' :
  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
126
Proof. solve_pure_exec. Qed.
127

128
129
Instance pure_binop op v1 v2 v' :
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
130
Proof. solve_pure_exec. Qed.
131

132
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
133
Proof. solve_pure_exec. Qed.
134

135
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
136
Proof. solve_pure_exec. Qed.
137

138
139
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
140
Proof. solve_pure_exec. Qed.
141

142
143
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
144
Proof. solve_pure_exec. Qed.
145

146
147
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
148
Proof. solve_pure_exec. Qed.
149

150
151
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
152
Proof. solve_pure_exec. Qed.
153

154
155
156
157
158
159
160
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
161
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
162
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
163
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
164
Proof.
165
166
167
  iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
168
Qed.
169

170
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
171
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
172
Proof.
173
174
175
  iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
  iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
176
177
Qed.

178
(** Heap *)
179
180
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
181
Proof.
182
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
183
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
184
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
185
186
187
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
188
189
Lemma twp_alloc s E v :
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
190
Proof.
191
  iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
192
  iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
193
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
194
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
195
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
196
Qed.
197

198
Lemma wp_load s E l q v :
199
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
200
201
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
202
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
203
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
204
205
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
206
Lemma twp_load s E l q v :
207
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
208
209
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
210
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
211
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
212
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
213
Qed.
214

215
216
217
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
218
Proof.
219
  iIntros (Φ) ">Hl HΦ".
220
  iApply wp_lift_atomic_head_step_no_fork; auto.
221
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
222
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
223
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
224
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
225
Qed.
226
227
228
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
229
Proof.
230
  iIntros (Φ) "Hl HΦ".
231
  iApply twp_lift_atomic_head_step_no_fork; auto.
232
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
233
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
234
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
235
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
236
Qed.
237

238
239
240
Lemma wp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  {{{  l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
241
242
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
243
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
244
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
245
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
246
247
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
248
249
250
Lemma twp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
251
252
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
253
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
254
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
255
256
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
257
Qed.
258

259
260
261
Lemma wp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  {{{  l  v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
262
263
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
264
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
265
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
266
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
267
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
268
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
269
Qed.
270
271
272
Lemma twp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  [[{ l  v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
273
274
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
275
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
276
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
277
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
278
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
279
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
280
Qed.
281

282
283
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
284
285
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
286
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
287
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
288
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
289
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
290
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
291
Qed.
292
293
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
294
295
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
296
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
297
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
298
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
299
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
300
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
301
Qed.
302
303
304

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
305
  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
306
307
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
308
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
309
310
311
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
312
313
314
315
316
317
  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
  - iExists _. iSplit; last done.
    iPureIntro. split.
    + apply first_resolve_insert; auto.
    + rewrite dom_insert_L. by apply union_mono_l.
Ralf Jung's avatar
Ralf Jung committed
318
  - iApply "HΦ". done.
319
320
Qed.

321
322
323
324
Lemma wp_resolve_proph p v w:
  {{{ proph p v }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
  {{{ RET (LitV LitUnit); v = Some w }}}.
325
Proof.
326
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
327
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
328
329
330
  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
331
  iSplit=> //. iFrame.
Ralf Jung's avatar
Ralf Jung committed
332
  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
333
334
  iSplitR "HΦ".
  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
335
    rewrite dom_delete. set_solver.
336
337
  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.
Ralf Jung's avatar
Ralf Jung committed
338
End lifting.