lifting.v 28.9 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
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
59
Local Hint Extern 0 (head_step (CompareExchange _ _ _) _ _ _ _ _) => eapply CompareExchangeS : core.
Amin Timany's avatar
Amin Timany committed
60
Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
Tej Chajed's avatar
Tej Chajed committed
61 62
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
63

64 65 66 67 68 69 70 71 72 73
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
74
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
75 76 77 78 79
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.
80
Instance cas_atomic s v0 v1 v2 : Atomic s (CompareExchange (Val v0) (Val v1) (Val v2)).
81 82 83 84 85 86 87 88 89
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.
90
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
91 92
Proof. solve_atomic. Qed.

93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
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
115
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
116
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
117
Local Ltac solve_pure_exec :=
118
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
119
    constructor; [solve_exec_safe | solve_exec_puredet].
120

121 122 123 124 125 126 127 128 129 130 131 132 133 134
(** 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. *)
135 136
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
137 138 139 140
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.
141

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

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

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

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

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

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

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

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

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

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

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

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

Amin Timany's avatar
Amin Timany committed
217 218 219 220 221 222 223
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 :
224
  l ↦∗ (vs ++ ws)  l ↦∗ vs  (l + length vs) ↦∗ ws.
Amin Timany's avatar
Amin Timany committed
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
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 :
240
  ([ map] l'  v  heap_array l vs, l'  v) - l ↦∗ vs.
Amin Timany's avatar
Amin Timany committed
241
Proof.
242 243
  iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
  { by rewrite /array. }
Amin Timany's avatar
Amin Timany committed
244 245 246
  rewrite big_opM_union; last first.
  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
    intros (j&?&Hjl&_)%heap_array_lookup.
247
    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
Amin Timany's avatar
Amin Timany committed
248 249 250 251 252
  rewrite array_cons.
  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
  by iApply "IH".
Qed.

253 254
Lemma heap_array_to_seq_meta l vs n :
  length vs = n 
255 256
  ([ map] l'  _  heap_array l vs, meta_token l' ) -
  [ list] i  seq 0 n, meta_token (l + (i : nat)) .
257 258 259 260 261 262 263 264 265 266 267 268
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.

269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287
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.

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

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

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

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

377
Lemma wp_cas_fail s E l q v' v1 v2 :
378
  val_for_compare v'  val_for_compare v1  vals_cas_compare_safe v' v1 
379 380
  {{{  l {q} v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET (#false, v'); l {q} v' }}}.
381
Proof.
382
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
383
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
384
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
385
  rewrite bool_decide_false //.
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 391
  [[{ l {q} v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  [[{ RET (#false, v'); l {q} v' }]].
392
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
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
396
  rewrite bool_decide_false //.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
397
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
398
Qed.
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 
402 403
  {{{  l  v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET (#true, v'); l  v2 }}}.
404
Proof.
405
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
406
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
407
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
408
  rewrite bool_decide_true //.
409
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
410
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
411
Qed.
412 413
Lemma twp_cas_suc s E l v1 v2 v' :
  val_for_compare v' = val_for_compare v1  vals_cas_compare_safe v' v1 
414 415
  [[{ l  v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  [[{ RET (#true, v'); l  v2 }]].
416
Proof.
417
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
418
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
419
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
420
  rewrite bool_decide_true //.
421
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
422
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
423
Qed.
424

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

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

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 494 495 496
(* 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.

497
Lemma wp_resolve s E e Φ p v pvs :
498 499
  Atomic StronglyAtomic e 
  to_val e = None 
500 501
  proph p pvs -
  WP e @ s; E {{ r,  pvs', pvs = (r, v)::pvs' - proph p pvs' - Φ r }} -
502 503 504 505 506
  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 *.
507
  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
508 509 510 511
  - 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.
512
  - rewrite -app_assoc.
513
    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
514
    { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
515 516 517
    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".
518
    { by eexists [] _ _. }
519 520 521
    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Φ $]".
522
    iMod "HΦ". iModIntro. by iApply "HΦ".
523 524
Qed.

525
(** Lemmas for some particular expression inside the [Resolve]. *)
526 527
Lemma wp_resolve_proph s E p pvs v :
  {{{ proph p pvs }}}
528
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
529
  {{{ pvs', RET (LitV LitUnit); pvs = (LitV LitUnit, v)::pvs'  proph p pvs' }}}.
530
Proof.
531
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
532 533
  iApply wp_pure_step_later=> //=. iApply wp_value.
  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
534
Qed.
535

536 537 538
Lemma wp_resolve_cas_suc s E (l : loc) (p : proph_id) (pvs : list (val * val)) (v1 v2 v : val) :
  vals_cas_compare_safe v1 v1 
  {{{ proph p pvs   l  v1 }}}
539 540
    Resolve (CompareExchange #l v1 v2) #p v @ s; E
  {{{ RET (#true, v1) ;  pvs', pvs = ((#true, v1)%V, v)::pvs'  proph p pvs'  l  v2 }}}.
541 542 543 544 545 546 547 548 549 550 551
Proof.
  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
  iApply (wp_cas_suc with "Hl"); [done..|]. iIntros "!> Hl".
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

Lemma wp_resolve_cas_fail s E (l : loc) (p : proph_id) (pvs : list (val * val)) q (v' v1 v2 v : val) :
  val_for_compare v'  val_for_compare v1  vals_cas_compare_safe v' v1 
  {{{ proph p pvs   l {q} v' }}}
552 553
    Resolve (CompareExchange #l v1 v2) #p v @ s; E
  {{{ RET (#false, v') ;  pvs', pvs = ((#false, v')%V, v)::pvs'  proph p pvs'  l {q} v' }}}.
554 555 556 557 558 559 560 561
Proof.
  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
  iApply (wp_cas_fail with "Hl"); [done..|]. iIntros "!> Hl".
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

(** Array lemmas *)
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
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.

Ralf Jung's avatar
Ralf Jung committed
605 606 607 608
Lemma wp_cas_suc_offset s E l off vs v' v1 v2 :
  vs !! off = Some v' 
  val_for_compare v' = val_for_compare v1 
  vals_cas_compare_safe v' v1 
609
  {{{  l ↦∗ vs }}}
610 611
    CompareExchange #(l + off) v1 v2 @ s; E
  {{{ RET (#true, v'); l ↦∗ <[off:=v2]> vs }}}.
612
Proof.
Ralf Jung's avatar
Ralf Jung committed
613
  iIntros (Hlookup ?? Φ) "Hl HΦ".
614
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Ralf Jung's avatar
Ralf Jung committed
615
  iApply (wp_cas_suc with "Hl1"); [done..|].
616 617 618
  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.

619 620 621
Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  val_for_compare (vs !!! off) = val_for_compare v1 
  vals_cas_compare_safe (vs !!! off) v1 
622
  {{{  l ↦∗ vs }}}
623 624
    CompareExchange #(l + off) v1 v2 @ s; E
  {{{ RET (#true, vs !!! off); l ↦∗ vinsert off v2 vs }}}.
625
Proof.
Ralf Jung's avatar
Ralf Jung committed
626
  intros. setoid_rewrite vec_to_list_insert. eapply wp_cas_suc_offset=> //.
627 628 629 630 631
  by apply vlookup_lookup.
Qed.

Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 :
  vs !! off = Some v0 
Ralf Jung's avatar
Ralf Jung committed
632
  val_for_compare v0  val_for_compare v1 
633 634
  vals_cas_compare_safe v0 v1 
  {{{  l ↦∗ vs }}}
635 636
    CompareExchange #(l + off) v1 v2 @ s; E
  {{{ RET (#false, v0); l ↦∗ vs }}}.
637 638 639 640 641 642 643 644 645 646
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 :
Ralf Jung's avatar
Ralf Jung committed
647
  val_for_compare (vs !!! off)  val_for_compare v1 
648 649
  vals_cas_compare_safe (vs !!! off) v1 
  {{{  l ↦∗ vs }}}
650 651
    CompareExchange #(l + off) v1 v2 @ s; E
  {{{ RET (#false, vs !!! off); l ↦∗ vs }}}.
652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
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
674
End lifting.