lifting.v 13.8 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
  state_interp σ κs :=
20
    (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I
21
22
23
24
}.

(** 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
25
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
26
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
28
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
31

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

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

50
51
52
53
54
(* [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.
55
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
56
Local Hint Resolve to_of_val.
57

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
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
87
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
88
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
89
Local Ltac solve_pure_exec :=
90
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
91
    constructor; [solve_exec_safe | solve_exec_puredet].
92

93
94
95
96
97
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.
Instance AsRecV_recv_locked v f x e :
  AsRecV v f x e  AsRecV (locked v) f x e.
98
99
Proof. by unlock. Qed.

100
101
102
103
104
105
106
107
108
109
110
111
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.
112

113
114
115
116
117
118
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').
119
Proof. solve_pure_exec. Qed.
120

121
122
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').
123
Proof. solve_pure_exec. Qed.
124

125
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
126
Proof. solve_pure_exec. Qed.
127

128
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
129
Proof. solve_pure_exec. Qed.
130

131
132
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
133
Proof. solve_pure_exec. Qed.
134

135
136
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
137
Proof. solve_pure_exec. Qed.
138

139
140
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
141
Proof. solve_pure_exec. Qed.
142

143
144
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
145
Proof. solve_pure_exec. Qed.
146

147
148
149
150
151
152
153
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
154
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
155
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
156
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
157
Proof.
Ralf Jung's avatar
Ralf Jung committed
158
  iIntros "He HΦ".
Ralf Jung's avatar
Ralf Jung committed
159
  iApply wp_lift_pure_det_head_step; [by eauto|intros; inv_head_step; by eauto|].
160
161
  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
162

163
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
164
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
165
Proof.
Ralf Jung's avatar
Ralf Jung committed
166
  iIntros "He HΦ".
167
  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
168
169
170
  iIntros "!> /= {$He}". by iApply twp_value.
Qed.

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

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

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

231
232
233
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
234
235
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
236
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
237
238
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
239
240
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
241
242
243
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
244
245
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
246
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
247
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
248
249
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
250
Qed.
251

252
253
254
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
255
256
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
257
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
258
259
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
260
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
261
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
262
Qed.
263
264
265
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
266
267
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
268
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
269
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
270
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
271
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
272
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
273
Qed.
274

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

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
298
  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
299
300
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
301
302
303
304
  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
305
306
307
308
309
310
  { 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
311
  - iApply "HΦ". done.
312
313
314
315
316
Qed.

Lemma wp_resolve_proph e1 e2 p v w:
  IntoVal e1 (LitV (LitProphecy p)) 
  IntoVal e2 w 
317
  {{{ proph p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); v = Some w }}}.
318
319
Proof.
  iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
320
321
322
323
  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  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.
324
  iSplit=> //. iFrame.
Ralf Jung's avatar
Ralf Jung committed
325
  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
326
327
328
329
330
331
  iSplitR "HΦ".
  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.

Ralf Jung's avatar
Ralf Jung committed
332
End lifting.