lifting.v 29.1 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.
Ralf Jung's avatar
Ralf Jung committed
59
Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : 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.
Ralf Jung's avatar
Ralf Jung committed
80
Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (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
Instance pure_binop op v1 v2 v' :
164
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
165
Proof. solve_pure_exec. Qed.
166 167 168 169 170 171 172 173 174 175 176
(* Higher-priority instance for EqOp. *)
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. }
  rewrite /bin_op_eval /= bool_decide_true //.
Qed.
177

178
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
179
Proof. solve_pure_exec. Qed.
180

181
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
182
Proof. solve_pure_exec. Qed.
183

184 185
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
186
Proof. solve_pure_exec. Qed.
187

188 189
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
190
Proof. solve_pure_exec. Qed.
191

192 193
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
194
Proof. solve_pure_exec. Qed.
195

196 197
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
198
Proof. solve_pure_exec. Qed.
199

200
Section lifting.
201
Context `{!heapG Σ}.
202 203 204 205
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
206 207 208 209
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types l : loc.
Implicit Types sz off : nat.
210

Ralf Jung's avatar
Ralf Jung committed
211
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
212
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
213
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
214
Proof.
215 216 217
  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.
218
Qed.
219

220
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
221
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
222
Proof.
223 224 225
  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.
226 227
Qed.

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

264 265
Lemma heap_array_to_seq_meta l vs n :
  length vs = n 
266 267
  ([ map] l'  _  heap_array l vs, meta_token l' ) -
  [ list] i  seq 0 n, meta_token (l + (i : nat)) .
268 269 270 271 272 273 274 275 276 277 278 279
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.

280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
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.

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

333
Lemma wp_alloc s E v :
334
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v  meta_token l  }}}.
335
Proof.
336 337 338
  iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
  iIntros "!>" (l) "/= (? & ? & _)".
  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
339
Qed.
340
Lemma twp_alloc s E v :
341
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v  meta_token l  }]].
342
Proof.
343 344 345
  iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
  iIntros (l) "/= (? & ? & _)".
  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
346
Qed.
347

348
Lemma wp_load s E l q v :
349
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
350 351
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
352
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
353
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
354 355
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
356
Lemma twp_load s E l q v :
357
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
358 359
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_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. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
362
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
363
Qed.
364

365 366 367
Lemma wp_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 wp_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. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
373
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
374
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
375
Qed.
376 377 378
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
379
Proof.
380
  iIntros (Φ) "Hl HΦ".
381
  iApply twp_lift_atomic_head_step_no_fork; auto.
382
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
383
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
384
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
385
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
386
Qed.
387

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

Ralf Jung's avatar
Ralf Jung committed
411
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
412
  v' = v1  vals_compare_safe v' v1 
Ralf Jung's avatar
Ralf Jung committed
413
  {{{  l  v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
414
  {{{ RET PairV v' (LitV $ LitBool true); l  v2 }}}.
415
Proof.
416
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
417
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
418
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
419
  rewrite bool_decide_true //.
420
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
421
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
422
Qed.
Ralf Jung's avatar
Ralf Jung committed
423
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
424
  v' = v1  vals_compare_safe v' v1 
Ralf Jung's avatar
Ralf Jung committed
425
  [[{ l  v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
426
  [[{ RET PairV v' (LitV $ LitBool true); l  v2 }]].
427
Proof.
428
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
429
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
430
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
431
  rewrite bool_decide_true //.
432
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
433
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
434
Qed.
435

436 437
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
438 439
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
440
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
441
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
442
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
443
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
444
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
445
Qed.
446 447
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
448 449
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
450
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
451
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
452
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
453
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
454
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
455
Qed.
456

457 458 459
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
460
  {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
461 462
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
463
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
464
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
465 466
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
467 468
Qed.

469 470 471
(* 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. *)

472
Lemma resolve_reducible e σ (p : proph_id) v :
473 474 475 476 477 478 479 480 481 482 483 484
  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.

485
Lemma step_resolve e vp vt σ1 κ e2 σ2 efs :
486
  Atomic StronglyAtomic e 
487 488
  prim_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs 
  head_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs.
489 490 491 492 493 494 495 496 497 498 499 500 501
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.
502
    - assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
503
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
504
    - assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
505 506 507
      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
Qed.

508
Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
509 510
  Atomic StronglyAtomic e 
  to_val e = None 
511 512
  proph p pvs -
  WP e @ s; E {{ r,  pvs', pvs = (r, v)::pvs' - proph p pvs' - Φ r }} -
513 514 515 516 517
  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 *.
518
  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
519 520 521 522
  - 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.
523
  - rewrite -app_assoc.
524
    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
525
    { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
526 527 528
    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".
529
    { by eexists [] _ _. }
530 531 532
    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Φ $]".
533
    iMod "HΦ". iModIntro. by iApply "HΦ".
534 535
Qed.

536
(** Lemmas for some particular expression inside the [Resolve]. *)
537
Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
538
  {{{ proph p pvs }}}
539
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
540
  {{{ pvs', RET (LitV LitUnit); pvs = (LitV LitUnit, v)::pvs'  proph p pvs' }}}.
541
Proof.
542
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
543 544
  iApply wp_pure_step_later=> //=. iApply wp_value.
  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
545
Qed.
546

Ralf Jung's avatar
Ralf Jung committed
547
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
548
  vals_compare_safe v1 v1 
549
  {{{ proph p pvs   l  v1 }}}
Ralf Jung's avatar
Ralf Jung committed
550 551
    Resolve (CmpXchg #l v1 v2) #p v @ s; E
  {{{ RET (v1, #true) ;  pvs', pvs = ((v1, #true)%V, v)::pvs'  proph p pvs'  l  v2 }}}.
552 553 554 555
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
556
  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
557 558 559
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

Ralf Jung's avatar
Ralf Jung committed
560
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
561
  v'  v1  vals_compare_safe v' v1 
562
  {{{ proph p pvs   l {q} v' }}}
Ralf Jung's avatar
Ralf Jung committed
563 564
    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' }}}.
565 566 567
Proof.
  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
Ralf Jung's avatar
Ralf Jung committed
568
  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
569 570 571 572
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.

(** Array lemmas *)
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
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
616
Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
Ralf Jung's avatar
Ralf Jung committed
617
  vs !! off = Some v' 
618 619
  v' = v1 
  vals_compare_safe v' v1 
620
  {{{  l ↦∗ vs }}}
Ralf Jung's avatar
Ralf Jung committed
621 622
    CmpXchg #(l + off) v1 v2 @ s; E
  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
623
Proof.
Ralf Jung's avatar
Ralf Jung committed
624
  iIntros (Hlookup ?? Φ) "Hl HΦ".
625
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Ralf Jung's avatar
Ralf Jung committed
626
  iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
627 628 629
  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.

Ralf Jung's avatar
Ralf Jung committed
630
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
631 632
  (vs !!! off) = v1 
  vals_compare_safe (vs !!! off) v1 
633
  {{{  l ↦∗ vs }}}
Ralf Jung's avatar
Ralf Jung committed
634 635
    CmpXchg #(l + off) v1 v2 @ s; E
  {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
636
Proof.
Ralf Jung's avatar
Ralf Jung committed
637
  intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
638 639 640
  by apply vlookup_lookup.
Qed.

Ralf Jung's avatar
Ralf Jung committed
641
Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
642
  vs !! off = Some v0 
643 644
  v0  v1 
  vals_compare_safe v0 v1 
645
  {{{  l ↦∗ vs }}}
Ralf Jung's avatar
Ralf Jung committed
646 647
    CmpXchg #(l + off) v1 v2 @ s; E
  {{{ RET (v0, #false); l ↦∗ vs }}}.
648 649 650
Proof.
  iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
Ralf Jung's avatar
Ralf Jung committed
651
  iApply (wp_cmpxchg_fail with "Hl1"); first done.
652 653 654 655 656
  { 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.

Ralf Jung's avatar
Ralf Jung committed
657
Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
658 659
  (vs !!! off)  v1 
  vals_compare_safe (vs !!! off) v1 
660
  {{{  l ↦∗ vs }}}
Ralf Jung's avatar
Ralf Jung committed
661 662 663
    CmpXchg #(l + off) v1 v2 @ s; E
  {{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684

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
685
End lifting.