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

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

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

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

34
Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
35
  ([ list] i  v  vs, (l + i)  v)%I.
36
37
38
Notation "l ↦∗ vs" := (array l vs)
  (at level 20, format "l  ↦∗  vs") : bi_scope.

39
40
41
42
43
44
45
46
47
(** 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
48
  | H : head_step ?e _ _ _ _ _ |- _ =>
49
50
51
52
53
     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.

Tej Chajed's avatar
Tej Chajed committed
54
55
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
56

57
(* [simpl apply] is too stupid, so we need extern hints here. *)
Tej Chajed's avatar
Tej Chajed committed
58
59
60
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Amin Timany's avatar
Amin Timany committed
61
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Tej Chajed's avatar
Tej Chajed committed
62
63
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
64

65
66
67
68
69
70
71
72
73
74
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].

Amin Timany's avatar
Amin Timany committed
75
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
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.
91
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
92
93
Proof. solve_atomic. Qed.

94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
Instance proph_resolve_atomic s e v1 v2 :
  Atomic s e  Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
  rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
  simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
  - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
  - rewrite fill_app. rewrite fill_app in Hfill.
    assert ( v, Val v = fill Ks e1'  False) as fill_absurd.
    { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
      apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
    destruct K; (inversion Hfill; clear Hfill; subst; try
      match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
    refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
    + destruct s; intro Hs; simpl in *.
      * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
      * apply irreducible_resolve. by rewrite fill_app in Hs.
    + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
Qed.

Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. by apply proph_resolve_atomic, skip_atomic. Qed.

Ralf Jung's avatar
fix TWP    
Ralf Jung committed
116
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
117
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
118
Local Ltac solve_pure_exec :=
119
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
120
    constructor; [solve_exec_safe | solve_exec_puredet].
121

122
123
124
125
126
127
128
129
130
131
132
133
134
135
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:

- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.

To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.

To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
136
137
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
138
139
140
141
Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
  apply AsRecV_recv : typeclass_instances.
142

143
144
145
146
147
148
149
150
151
152
153
154
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.
155

156
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
157
158
159
160
161
  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').
162
Proof. solve_pure_exec. Qed.
163

164
165
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').
166
Proof. solve_pure_exec. Qed.
167

168
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
169
Proof. solve_pure_exec. Qed.
170

171
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
172
Proof. solve_pure_exec. Qed.
173

174
175
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
176
Proof. solve_pure_exec. Qed.
177

178
179
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
180
Proof. solve_pure_exec. Qed.
181

182
183
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
184
Proof. solve_pure_exec. Qed.
185

186
187
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
188
Proof. solve_pure_exec. Qed.
189

190
Section lifting.
191
Context `{!heapG Σ}.
192
193
194
195
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
196
197
198
199
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types l : loc.
Implicit Types sz off : nat.
200

Ralf Jung's avatar
Ralf Jung committed
201
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
202
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
203
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
204
Proof.
205
206
207
  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.
208
Qed.
209

210
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
211
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
212
Proof.
213
214
215
  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.
216
217
Qed.

Amin Timany's avatar
Amin Timany committed
218
219
220
221
222
223
224
Lemma array_nil l : l ↦∗ []  emp.
Proof. by rewrite /array. Qed.

Lemma array_singleton l v : l ↦∗ [v]  l  v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.

Lemma array_app l vs ws :
225
  l ↦∗ (vs ++ ws)  l ↦∗ vs  (l + length vs) ↦∗ ws.
Amin Timany's avatar
Amin Timany committed
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
Proof.
  rewrite /array big_sepL_app.
  setoid_rewrite Nat2Z.inj_add.
  by setoid_rewrite loc_add_assoc.
Qed.

Lemma array_cons l v vs : l ↦∗ (v :: vs)  l  v  (l + 1) ↦∗ vs.
Proof.
  rewrite /array big_sepL_cons loc_add_0.
  setoid_rewrite loc_add_assoc.
  setoid_rewrite Nat2Z.inj_succ.
  by setoid_rewrite Z.add_1_l.
Qed.

Lemma heap_array_to_array l vs :
241
  ([ map] l'  v  heap_array l vs, l'  v) - l ↦∗ vs.
Amin Timany's avatar
Amin Timany committed
242
Proof.
243
244
  iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
  { by rewrite /array. }
Amin Timany's avatar
Amin Timany committed
245
246
247
  rewrite big_opM_union; last first.
  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
    intros (j&?&Hjl&_)%heap_array_lookup.
248
    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
Amin Timany's avatar
Amin Timany committed
249
250
251
252
253
  rewrite array_cons.
  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
  by iApply "IH".
Qed.

254
255
Lemma heap_array_to_seq_meta l vs n :
  length vs = n 
256
257
  ([ map] l'  _  heap_array l vs, meta_token l' ) -
  [ list] i  seq 0 n, meta_token (l + (i : nat)) .
258
259
260
261
262
263
264
265
266
267
268
269
Proof.
  iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
  rewrite big_opM_union; last first.
  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
    intros (j&?&Hjl&_)%heap_array_lookup.
    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
  rewrite loc_add_0 -fmap_seq big_sepL_fmap.
  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
  setoid_rewrite <-loc_add_assoc.
  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
Qed.

270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
Lemma update_array l vs off v :
  vs !! off = Some v 
  (l ↦∗ vs - ((l + off)  v   v', (l + off)  v' - l ↦∗ <[off:=v']>vs))%I.
Proof.
  iIntros (Hlookup) "Hl".
  rewrite -[X in (l ↦∗ X)%I](take_drop_middle _ off v); last done.
  iDestruct (array_app with "Hl") as "[Hl1 Hl]".
  iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
  assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
  rewrite take_length min_l; last by lia. iFrame "Hl2".
  iIntros (w) "Hl2".
  clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
  { apply list_lookup_insert. lia. }
  rewrite -[in (l ↦∗ <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
  iApply array_app. rewrite take_insert; last by lia. iFrame.
  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
  rewrite drop_insert; last by lia. done.
Qed.

289
(** Heap *)
Amin Timany's avatar
Amin Timany committed
290
291
Lemma wp_allocN s E v n :
  0 < n 
292
  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
293
  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v 
294
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }}}.
Amin Timany's avatar
Amin Timany committed
295
296
Proof.
  iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
297
  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
Amin Timany's avatar
Amin Timany committed
298
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
299
  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
300
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
301
    rewrite replicate_length Z2Nat.id; auto with lia. }
302
303
304
  iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
  - by iApply heap_array_to_array.
  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Amin Timany's avatar
Amin Timany committed
305
306
307
Qed.
Lemma twp_allocN s E v n :
  0 < n 
308
  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
309
  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v 
310
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }]].
Amin Timany's avatar
Amin Timany committed
311
312
313
314
Proof.
  iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
315
  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
316
  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
Amin Timany's avatar
Amin Timany committed
317
    rewrite replicate_length Z2Nat.id; auto with lia. }
318
319
320
  iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
  - by iApply heap_array_to_array.
  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Amin Timany's avatar
Amin Timany committed
321
322
Qed.

323
Lemma wp_alloc s E v :
324
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v  meta_token l  }}}.
325
Proof.
326
327
328
  iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
  iIntros "!>" (l) "/= (? & ? & _)".
  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
329
Qed.
330
Lemma twp_alloc s E v :
331
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v  meta_token l  }]].
332
Proof.
333
334
335
  iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
  iIntros (l) "/= (? & ? & _)".
  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
336
Qed.
337

338
Lemma wp_load s E l q v :
339
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
340
341
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
342
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
343
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
344
345
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
346
Lemma twp_load s E l q v :
347
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
348
349
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
350
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
351
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
352
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
353
Qed.
354

355
356
357
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
358
Proof.
359
  iIntros (Φ) ">Hl HΦ".
360
  iApply wp_lift_atomic_head_step_no_fork; auto.
361
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
362
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
363
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
364
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
365
Qed.
366
367
368
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
369
Proof.
370
  iIntros (Φ) "Hl HΦ".
371
  iApply twp_lift_atomic_head_step_no_fork; auto.
372
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
373
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
374
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
375
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
376
Qed.
377

378
Lemma wp_cas_fail s E l q v' v1 v2 :
379
  val_for_compare v'  val_for_compare v1  vals_cas_compare_safe v' v1 
380
  {{{  l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
381
382
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
383
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
384
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
385
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
386
387
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
388
Lemma twp_cas_fail s E l q v' v1 v2 :
389
  val_for_compare v'  val_for_compare v1  vals_cas_compare_safe v' v1 
390
  [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
391
392
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
393
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
394
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
395
396
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
397
Qed.
398

399
400
401
Lemma wp_cas_suc s E l v1 v2 v' :
  val_for_compare v' = val_for_compare v1  vals_cas_compare_safe v' v1 
  {{{  l  v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
402
403
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
404
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
405
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
406
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
407
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
408
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
409
Qed.
410
411
412
Lemma twp_cas_suc s E l v1 v2 v' :
  val_for_compare v' = val_for_compare v1  vals_cas_compare_safe v' v1 
  [[{ l  v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
413
414
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
415
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
416
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
417
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
418
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
419
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
420
Qed.
421

422
423
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
424
425
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
426
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
427
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
428
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
429
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
430
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
431
Qed.
432
433
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
434
435
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
436
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
437
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
438
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
439
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
440
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
441
Qed.
442

443
444
445
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
446
  {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
447
448
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
449
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
450
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
451
452
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
453
454
Qed.

455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
(* In the following, strong atomicity is required due to the fact that [e] must
be able to make a head step for [Resolve e _ _] not to be (head) stuck. *)

Lemma resolve_reducible e σ p v :
  Atomic StronglyAtomic e  reducible e σ 
  reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
Proof.
  intros A (κ & e' & σ' & efs & H).
  exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
  eapply Ectx_step with (K:=[]); try done.
  assert (w, Val w = e') as [w <-].
  { unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
    destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
  simpl. constructor. by apply prim_step_to_val_is_head_step.
Qed.

Lemma step_resolve e p v σ1 κ e2 σ2 efs :
  Atomic StronglyAtomic e 
  prim_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs 
  head_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs.
Proof.
  intros A [Ks e1' e2' Hfill -> step]. simpl in *.
  induction Ks as [|K Ks _] using rev_ind.
  + simpl in *. subst. inversion step. by constructor.
  + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
    - assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
        first by rewrite fill_app.
      assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
        first by rewrite fill_app.
      rewrite fill_app /=. rewrite Eq1 in A.
      assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
      { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
      destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
    - assert (to_val (fill Ks e1') = Some p); first by rewrite -H1 //.
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
    - assert (to_val (fill Ks e1') = Some v); first by rewrite -H2 //.
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
Qed.

494
Lemma wp_resolve s E e Φ p v pvs :
495
496
  Atomic StronglyAtomic e 
  to_val e = None 
497
498
  proph p pvs -
  WP e @ s; E {{ r,  pvs', pvs = (r, v)::pvs' - proph p pvs' - Φ r }} -
499
500
501
502
503
  WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
  (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
     here, since this breaks the WP abstraction. *)
  iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
504
  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
505
506
507
508
  - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
    iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
    inversion step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
509
  - rewrite -app_assoc.
510
    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
511
    { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
512
513
514
    iIntros (e2 σ2 efs step). apply step_resolve in step; last done.
    inversion step; simplify_list_eq.
    iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
515
    { by eexists [] _ _. }
516
517
518
    iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
    iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ HPost]".
    iModIntro. rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[HΦ $]".
519
    iMod "HΦ". iModIntro. by iApply "HΦ".
520
521
Qed.

522
523
Lemma wp_resolve_proph s E p pvs v :
  {{{ proph p pvs }}}
524
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
525
  {{{ pvs', RET (LitV LitUnit); pvs = (LitV LitUnit, v)::pvs'  proph p pvs' }}}.
526
Proof.
527
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
528
529
  iApply wp_pure_step_later=> //=. iApply wp_value.
  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
530
Qed.
531

532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
Lemma wp_allocN_vec s E v n :
  0 < n 
  {{{ True }}}
    AllocN #n v @ s ; E
  {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v 
         [ list] i  seq 0 (Z.to_nat n), meta_token (l + (i : nat))  }}}.
Proof.
  iIntros (Hzs Φ) "_ HΦ". iApply wp_allocN; [ lia | done | .. ]. iNext.
  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
Qed.

Lemma wp_load_offset s E l off vs v :
  vs !! off = Some v 
  {{{  l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET v; l ↦∗ vs }}}.
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HΦ".
  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
  iApply "Hl2". iApply "Hl1".
Qed.

Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
  {{{  l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.

Lemma wp_store_offset s E l off vs v :
  is_Some (vs !! off) 
  {{{  l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
Proof.
  iIntros ([w Hlookup] Φ) ">Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (wp_store with "Hl1"). iNext. iIntros "Hl1".
  iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.

Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  {{{  l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
Proof.
  setoid_rewrite vec_to_list_insert. apply wp_store_offset.
  eexists. by apply vlookup_lookup.
Qed.

Lemma wp_cas_suc_offset s E l off vs v1 v2 :
  vs !! off = Some v1 
  vals_cas_compare_safe v1 v1 
  {{{  l ↦∗ vs }}}
    CAS #(l + off) v1 v2 @ s; E
  {{{ RET #true; l ↦∗ <[off:=v2]> vs }}}.
Proof.
  iIntros (Hlookup Hcmp Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (wp_cas_suc with "Hl1"). { left. by destruct Hcmp. }
  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.

Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off = v1 
  vals_cas_compare_safe v1 v1 
  {{{  l ↦∗ vs }}}
    CAS #(l + off) v1 v2 @ s; E
  {{{ RET #true; l ↦∗ vinsert off v2 vs }}}.
Proof.
  intros. setoid_rewrite vec_to_list_insert. apply wp_cas_suc_offset=> //.
  by apply vlookup_lookup.
Qed.

Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 :
  vs !! off = Some v0 
  v0  v1 
  vals_cas_compare_safe v0 v1 
  {{{  l ↦∗ vs }}}
    CAS #(l + off) v1 v2 @ s; E
  {{{ RET #false; l ↦∗ vs }}}.
Proof.
  iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (wp_cas_fail with "Hl1"); first done.
  { destruct Hcmp; by [ left | right ]. }
  iIntros "!> Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
  rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
Qed.

Lemma wp_cas_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off  v1 
  vals_cas_compare_safe (vs !!! off) v1 
  {{{  l ↦∗ vs }}}
    CAS #(l + off) v1 v2 @ s; E
  {{{ RET #false; l ↦∗ vs }}}.
Proof. intros. eapply wp_cas_fail_offset=> //. by apply vlookup_lookup. Qed.

Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
  vs !! off = Some #i1 
  {{{  l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
  {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (wp_faa with "Hl1").
  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.

Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
  vs !!! off = #i1 
  {{{  l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
  {{{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }}}.
Proof.
  intros. setoid_rewrite vec_to_list_insert. apply wp_faa_offset=> //.
  by apply vlookup_lookup.
Qed.

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