lifting.v 23.9 KB
Newer Older
1
2
From stdpp Require Import fin_maps.
From iris.proofmode Require Import tactics.
3
From iris.algebra Require Import auth gmap.
4
From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
5
From iris.program_logic Require Export weakestpre total_weakestpre.
6
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
7
From iris.heap_lang Require Export lang.
8
From iris.heap_lang Require Import tactics notation.
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 Σ;
Ralf Jung's avatar
Ralf Jung committed
14
  heapG_inv_heapG :> inv_heapG loc val Σ;
Ralf Jung's avatar
Ralf Jung committed
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

Ralf Jung's avatar
Ralf Jung committed
34
35
Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
  (at level 20, format "l  ↦□  I") : bi_scope.
36
Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
Ralf Jung's avatar
Ralf Jung committed
37
  (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
38
Notation inv_heap_inv := (inv_heap_inv loc val).
Ralf Jung's avatar
Ralf Jung committed
39

40
41
42
43
44
45
46
47
48
(** 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
49
  | H : head_step ?e _ _ _ _ _ |- _ =>
50
51
52
53
54
     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
55
56
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
57

58
(* [simpl apply] is too stupid, so we need extern hints here. *)
Tej Chajed's avatar
Tej Chajed committed
59
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Ralf Jung's avatar
Ralf Jung committed
60
Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : 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].

75
76
77
78
79
80
81
82
Instance rec_atomic s f x e : Atomic s (Rec f x e).
Proof. solve_atomic. Qed.
Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance injl_atomic s v : Atomic s (InjL (Val v)).
Proof. solve_atomic. Qed.
Instance injr_atomic s v : Atomic s (InjR (Val v)).
Proof. solve_atomic. Qed.
83
(** The instance below is a more general version of [Skip] *)
84
85
86
87
88
89
90
91
92
93
94
95
96
97
Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
Proof. destruct f, x; solve_atomic. Qed.
Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
Proof. solve_atomic. Qed.
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance if_true_atomic s v1 e2 : Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
Proof. solve_atomic. Qed.
Instance if_false_atomic s e1 v2 : Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
Proof. solve_atomic. Qed.
Instance fst_atomic s v : Atomic s (Fst (Val v)).
Proof. solve_atomic. Qed.
Instance snd_atomic s v : Atomic s (Snd (Val v)).
Proof. solve_atomic. Qed.
98

99
100
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
101

Amin Timany's avatar
Amin Timany committed
102
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
103
104
105
106
107
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.
Ralf Jung's avatar
Ralf Jung committed
108
Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
109
110
111
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
112

113
114
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
115
Instance resolve_atomic s e v1 v2 :
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
  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.

Ralf Jung's avatar
fix TWP    
Ralf Jung committed
134
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
135
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
136
Local Ltac solve_pure_exec :=
137
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
138
    constructor; [solve_exec_safe | solve_exec_puredet].
139

140
141
142
143
144
145
146
147
148
149
150
151
152
153
(** 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. *)
154
155
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
156
157
158
159
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.
160

161
162
163
164
165
166
167
168
169
170
171
172
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.
173

174
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
175
176
177
178
179
  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').
180
Proof. solve_pure_exec. Qed.
181

182
Instance pure_binop op v1 v2 v' :
183
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
184
Proof. solve_pure_exec. Qed.
185
(* Higher-priority instance for [EqOp]. *)
186
187
188
189
190
191
192
193
Instance pure_eqop v1 v2 :
  PureExec (vals_compare_safe v1 v2) 1
    (BinOp EqOp (Val v1) (Val v2))
    (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
  intros Hcompare.
  cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
  { intros. revert Hcompare. solve_pure_exec. }
194
  rewrite /bin_op_eval /= decide_True //.
195
Qed.
196

197
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
198
Proof. solve_pure_exec. Qed.
199

200
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
201
Proof. solve_pure_exec. Qed.
202

203
204
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
205
Proof. solve_pure_exec. Qed.
206

207
208
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
209
Proof. solve_pure_exec. Qed.
210

211
212
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
213
Proof. solve_pure_exec. Qed.
214

215
216
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
217
Proof. solve_pure_exec. Qed.
218

219
Section lifting.
220
Context `{!heapG Σ}.
221
Implicit Types P Q : iProp Σ.
222
Implicit Types Φ Ψ : val  iProp Σ.
223
224
Implicit Types efs : list expr.
Implicit Types σ : state.
225
226
Implicit Types v : val.
Implicit Types l : loc.
227

228
229
230
231
(** Recursive functions: we do not use this lemmas as it is easier to use Löb
induction directly, but this demonstrates that we can state the expected
reasoning principle for recursive functions, without any visible ▷. *)
Lemma wp_rec_löb s E f x e Φ Ψ :
232
   (  ( v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}) -
233
234
235
236
237
      v, Ψ v - WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -
   v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}.
Proof.
  iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
  iApply lifting.wp_pure_step_later; first done.
Ralf Jung's avatar
Ralf Jung committed
238
  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
239
240
241
  iApply ("IH" with "HΨ").
Qed.

Ralf Jung's avatar
Ralf Jung committed
242
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
243
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
244
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
245
Proof.
246
247
248
  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.
249
Qed.
250

251
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
252
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
253
Proof.
254
255
256
  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.
257
258
Qed.

Ralf Jung's avatar
Ralf Jung committed
259
(** Heap *)
260
261
(** The usable rules for [allocN] stated in terms of the [array] proposition
are derived in te file [array]. *)
Ralf Jung's avatar
Ralf Jung committed
262
Lemma heap_array_to_seq_meta l vs (n : nat) :
263
  length vs = n 
264
265
  ([ map] l'  _  heap_array l vs, meta_token l' ) -
  [ list] i  seq 0 n, meta_token (l + (i : nat)) .
266
267
268
269
270
271
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. }
272
  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
273
274
275
276
277
  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.

Ralf Jung's avatar
Ralf Jung committed
278
279
280
Lemma heap_array_to_seq_mapsto l v (n : nat) :
  ([ map] l'  v  heap_array l (replicate n v), l'  v) -
  [ list] i  seq 0 n, (l + (i : nat))  v.
281
Proof.
Ralf Jung's avatar
Ralf Jung committed
282
283
284
285
286
287
  iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
  { done. }
  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. }
288
  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
Ralf Jung's avatar
Ralf Jung committed
289
290
291
  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".
292
293
Qed.

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

322
Lemma twp_alloc s E v :
323
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v  meta_token l  }]].
324
Proof.
325
  iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; [auto with lia..|].
Ralf Jung's avatar
Ralf Jung committed
326
  iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
327
Qed.
328
329
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v  meta_token l  }}}.
330
Proof.
331
332
  iIntros (Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
  iApply twp_alloc; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
333
Qed.
334

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

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

Ralf Jung's avatar
Ralf Jung committed
368
Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
369
  v'  v1  vals_compare_safe v' v1 
Ralf Jung's avatar
Ralf Jung committed
370
  [[{ l {q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
371
  [[{ RET PairV v' (LitV $ LitBool false); l {q} v' }]].
372
Proof.
373
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
374
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
375
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
376
  rewrite bool_decide_false //.
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
377
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
378
Qed.
379
380
381
382
Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
  v'  v1  vals_compare_safe v' v1 
  {{{  l {q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool false); l {q} v' }}}.
383
Proof.
384
385
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_fail with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
386
Qed.
387

Ralf Jung's avatar
Ralf Jung committed
388
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
389
  v' = v1  vals_compare_safe v' v1 
Ralf Jung's avatar
Ralf Jung committed
390
  [[{ l  v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
391
  [[{ RET PairV v' (LitV $ LitBool true); l  v2 }]].
392
Proof.
393
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
394
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
395
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
396
  rewrite bool_decide_true //.
397
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
398
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
399
Qed.
400
401
402
403
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
  v' = v1  vals_compare_safe v' v1 
  {{{  l  v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool true); l  v2 }}}.
404
Proof.
405
406
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
407
Qed.
408

409
410
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
411
412
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
413
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
414
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
415
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
416
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP    
Ralf Jung committed
417
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
418
Qed.
419
420
421
422
423
424
425
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
426

427
428
429
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
430
  {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
431
Proof.
432
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
433
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
434
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
435
436
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
437
438
Qed.

439
440
441
(* 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. *)

442
Lemma resolve_reducible e σ (p : proph_id) v :
443
444
445
446
447
448
449
450
451
452
453
454
  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.

455
Lemma step_resolve e vp vt σ1 κ e2 σ2 efs :
456
  Atomic StronglyAtomic e 
457
458
  prim_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs 
  head_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs.
459
460
461
462
463
464
465
466
467
468
469
470
471
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.
472
    - assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
473
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
474
    - assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
475
476
477
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
Qed.

478
Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
479
480
  Atomic StronglyAtomic e 
  to_val e = None 
481
482
  proph p pvs -
  WP e @ s; E {{ r,  pvs', pvs = (r, v)::pvs' - proph p pvs' - Φ r }} -
483
484
485
486
487
  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 *.
488
  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
489
490
491
492
  - 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.
493
  - rewrite -app_assoc.
494
    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
495
    { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
496
497
498
    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".
499
    { by eexists [] _ _. }
500
501
502
    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Φ $]".
503
    iMod "HΦ". iModIntro. by iApply "HΦ".
504
505
Qed.

506
(** Lemmas for some particular expression inside the [Resolve]. *)
507
Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
508
  {{{ proph p pvs }}}
509
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
510
  {{{ pvs', RET (LitV LitUnit); pvs = (LitV LitUnit, v)::pvs'  proph p pvs' }}}.
511
Proof.
512
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
513
514
  iApply wp_pure_step_later=> //=. iApply wp_value.
  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
515
Qed.
516

Ralf Jung's avatar
Ralf Jung committed
517
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
518
  vals_compare_safe v1 v1 
519
  {{{ proph p pvs   l  v1 }}}
Ralf Jung's avatar
Ralf Jung committed
520
521
    Resolve (CmpXchg #l v1 v2) #p v @ s; E
  {{{ RET (v1, #true) ;  pvs', pvs = ((v1, #true)%V, v)::pvs'  proph p pvs'  l  v2 }}}.
522
523
524
525
Proof.
  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
Ralf Jung's avatar
Ralf Jung committed
526
  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
527
528
529
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

Ralf Jung's avatar
Ralf Jung committed
530
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
531
  v'  v1  vals_compare_safe v' v1 
532
  {{{ proph p pvs   l {q} v' }}}
Ralf Jung's avatar
Ralf Jung committed
533
534
    Resolve (CmpXchg #l v1 v2) #p v @ s; E
  {{{ RET (v', #false) ;  pvs', pvs = ((v', #false)%V, v)::pvs'  proph p pvs'  l {q} v' }}}.
535
536
537
Proof.
  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
Ralf Jung's avatar
Ralf Jung committed
538
  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
539
540
541
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

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