Merge branch 'ralf/array' into 'master'

Move array stuff to own file

See merge request iris/iris!299

_CoqProject

@@ -100,6 +100,7 @@ theories/heap_lang/lang.v
 theories/heap_lang/metatheory.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
+theories/heap_lang/array.v
 theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v

tests/heap_lang.ref

@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
+The command has indeed failed with message:
+In nested Ltac calls to "iIntros (constr)", "iIntros_go",
+"iDestructHyp (constr) as (constr)",
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
+"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
+"iAndDestruct (constr) as (constr) (constr)", last call failed.
+Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
 1 subgoal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -155,6 +155,15 @@ Section tests.
     by iApply "HΦ".
   Qed.
 
+  Lemma test_array_app l vs1 vs2 :
+    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
+  Proof.
+    Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
+    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
+    Fail iSplitL "H1".
+    iApply array_app. iSplitL "H1"; done.
+  Qed.
+
 End tests.
 
 Section printing_tests.

theories/heap_lang/array.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lifting.
+From iris.heap_lang Require Import tactics notation.
+From iris.proofmode Require Import tactics.
+From stdpp Require Import fin_maps.
+Set Default Proof Using "Type".
+
+(** This file defines the [array] connective, a version of [mapsto] that works
+with lists of values. It also contains array versions of the basic heap
+operations of HeapLand. *)
+
+Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
+Notation "l ↦∗ vs" := (array l vs)
+  (at level 20, format "l  ↦∗  vs") : bi_scope.
+
+(** We have no [FromSep] or [IntoSep] instances to remain forwards compatible
+with a fractional array assertion, that will split the fraction, not the
+list. *)
+
+Section lifting.
+Context `{!heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types σ : state.
+Implicit Types v : val.
+Implicit Types vs : list val.
+Implicit Types l : loc.
+Implicit Types sz off : nat.
+
+Global Instance array_timeless l vs : Timeless (array l vs) := _.
+
+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 :
+  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (l +ₗ length vs) ↦∗ ws.
+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 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.
+
+(** Allocation *)
+Lemma mapsto_seq_array l v n :
+  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v) -∗
+  l ↦∗ replicate n v.
+Proof.
+  rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
+  { done. }
+  iIntros "[$ Hl]". rewrite -fmap_seq big_sepL_fmap.
+  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
+  setoid_rewrite <-loc_add_assoc. iApply "IH". done.
+Qed.
+
+Lemma wp_allocN s E v n :
+  0 < n →
+  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
+  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (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_seq; [done..|]. iNext.
+  iIntros (l) "Hlm". iApply "HΦ".
+  iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
+  by iApply mapsto_seq_array.
+Qed.
+Lemma twp_allocN s E v n :
+  0 < n →
+  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
+  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
+Proof.
+  iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
+  iIntros (l) "Hlm". iApply "HΦ".
+  iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
+  by iApply mapsto_seq_array.
+Qed.
+
+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 twp_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 twp_allocN; [ lia | done | .. ].
+  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
+Qed.
+
+(** Access to array elements *)
+
+Lemma wp_load_offset s E l off vs v :
+  vs !! off = Some v →
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗ vs }}}.
+Proof.
+  iIntros (Hlookup Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HΦ".
+  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
+  iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
+Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
+
+Lemma wp_store_offset s E l off vs v :
+  is_Some (vs !! off) →
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
+Proof.
+  iIntros ([w Hlookup] Φ) ">Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_store with "Hl1"). iNext. iIntros "Hl1".
+  iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
+Proof.
+  setoid_rewrite vec_to_list_insert. apply wp_store_offset.
+  eexists. by apply vlookup_lookup.
+Qed.
+
+Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
+  vs !! off = Some v' →
+  v' = v1 →
+  vals_compare_safe v' v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CmpXchg #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
+Proof.
+  iIntros (Hlookup ?? Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
+  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+
+Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+  vs !!! off = v1 →
+  vals_compare_safe (vs !!! off) v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CmpXchg #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
+Proof.
+  intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
+  by apply vlookup_lookup.
+Qed.
+
+Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
+  vs !! off = Some v0 →
+  v0 ≠ v1 →
+  vals_compare_safe v0 v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    CmpXchg #(l +ₗ off) v1 v2 @ s; E
+  {{{ RET (v0, #false); l ↦∗ vs }}}.
+Proof.
+  iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
+  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (wp_cmpxchg_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_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+  vs !!! off ≠ v1 →
+  vals_compare_safe (vs !!! off) v1 →
+  {{{ ▷ l ↦∗ vs }}}
+    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.
+
+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.
+
+End lifting.
+
+Typeclasses Opaque array.

theories/heap_lang/lifting.v

@@ -31,11 +31,6 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
-Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
-  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
-Notation "l ↦∗ vs" := (array l vs)
-  (at level 20, format "l  ↦∗  vs") : bi_scope.
-
 (** 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
@@ -204,9 +199,7 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
 Implicit Types σ : state.
 Implicit Types v : val.
-Implicit Types vs : list val.
 Implicit Types l : loc.
-Implicit Types sz off : nat.
 
 (** Fork: Not using Texan triples to avoid some unnecessary [True] *)
 Lemma wp_fork s E e Φ :
@@ -225,43 +218,10 @@ Proof.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
-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 :
-  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (l +ₗ length vs) ↦∗ ws.
-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 :
-  ([∗ map] l' ↦ v ∈ heap_array l vs, l' ↦ v) -∗ l ↦∗ vs.
-Proof.
-  iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
-  { by rewrite /array. }
-  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 array_cons.
-  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
-  by iApply "IH".
-Qed.
+(** Heap *)
+(** The "proper" [allocN] are derived in [array]. *)
 
-Lemma heap_array_to_seq_meta l vs n :
+Lemma heap_array_to_seq_meta l vs (n : nat) :
   length vs = n →
   ([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l' ⊤) -∗
   [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)) ⊤.
@@ -277,31 +237,27 @@ Proof.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
-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.
+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.
 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.
+  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. }
+  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.
 
-(** Heap *)
-Lemma wp_allocN s E v n :
+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); l ↦∗ replicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
+  {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
+      (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
@@ -309,15 +265,16 @@ Proof.
   iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
-  - by iApply heap_array_to_array.
+  iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ".
+  iApply big_sepL_sep. iSplitL "Hl".
+  - by iApply heap_array_to_seq_mapsto.
   - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
-Lemma twp_allocN s E v n :
+Lemma twp_allocN_seq s E v n :
   0 < n →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
-  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
+  [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
+      (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
 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.
@@ -325,24 +282,23 @@ Proof.
   iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
-  - by iApply heap_array_to_array.
+  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.
   - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 
 Lemma wp_alloc s E v :
   {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}.
 Proof.
-  iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
-  iIntros "!>" (l) "/= (? & ? & _)".
-  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
+  iIntros (Φ) "_ HΦ". iApply wp_allocN_seq; auto with lia.
+  iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 Lemma twp_alloc s E v :
   [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }]].
 Proof.
-  iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
-  iIntros (l) "/= (? & ? & _)".
-  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
+  iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; auto with lia.
+  iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 
 Lemma wp_load s E l q v :
@@ -569,117 +525,4 @@ Proof.
   iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
 Qed.
 
-(** Array lemmas *)
-Lemma wp_allocN_vec s E v n :
-  0 < n →
-  {{{ True }}}
-    AllocN #n v @ s ; E
-  {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
-Proof.
-  iIntros (Hzs Φ) "_ HΦ". iApply wp_allocN; [ lia | done | .. ]. iNext.
-  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
-Qed.
-
-Lemma wp_load_offset s E l off vs v :
-  vs !! off = Some v →
-  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗ vs }}}.
-Proof.
-  iIntros (Hlookup Φ) "Hl HΦ".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
-  iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HΦ".
-  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
-  iApply "Hl2". iApply "Hl1".
-Qed.
-
-Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
-Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
-
-Lemma wp_store_offset s E l off vs v :
-  is_Some (vs !! off) →
-  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
-Proof.
-  iIntros ([w Hlookup] Φ) ">Hl HΦ".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
-  iApply (wp_store with "Hl1"). iNext. iIntros "Hl1".
-  iApply "HΦ". iApply "Hl2". iApply "Hl1".
-Qed.
-
-Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
-Proof.
-  setoid_rewrite vec_to_list_insert. apply wp_store_offset.
-  eexists. by apply vlookup_lookup.
-Qed.
-
-Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
-  vs !! off = Some v' →
-  v' = v1 →
-  vals_compare_safe v' v1 →
-  {{{ ▷ l ↦∗ vs }}}
-    CmpXchg #(l +ₗ off) v1 v2 @ s; E
-  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
-Proof.
-  iIntros (Hlookup ?? Φ) "Hl HΦ".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
-  iApply (wp_cmpxchg_suc with "Hl1"); [done..|].
-  iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
-Qed.
-
-Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
-  vs !!! off = v1 →
-  vals_compare_safe (vs !!! off) v1 →
-  {{{ ▷ l ↦∗ vs }}}
-    CmpXchg #(l +ₗ off) v1 v2 @ s; E
-  {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
-Proof.
-  intros. setoid_rewrite vec_to_list_insert. eapply wp_cmpxchg_suc_offset=> //.
-  by apply vlookup_lookup.
-Qed.
-
-Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
-  vs !! off = Some v0 →
-  v0 ≠ v1 →
-  vals_compare_safe v0 v1 →
-  {{{ ▷ l ↦∗ vs }}}
-    CmpXchg #(l +ₗ off) v1 v2 @ s; E
-  {{{ RET (v0, #false); l ↦∗ vs }}}.
-Proof.
-  iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
-  iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".