Library zoo_std.array

From Stdlib Require Import
  ZifyNat.

From zoo Require Import
  prelude.
From zoo.common Require Import
  list
  math.
From zoo.iris.bi Require Import
  big_op.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  array__code.
From zoo_std Require Import
  for_
  assume
  chunk.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types i j k n : nat.
Implicit Types l : location.
Implicit Types v t fn acc : val.
Implicit Types vs vs_left vs_right ws : list val.

Definition array٠unsafe_xchg : val :=
  fun: "t" "i" "v" ⇒
    Xchg ("t", "i") "v".

Definition array٠unsafe_cas : val :=
  fun: "t" "i" "v1" "v2" ⇒
    CAS ("t", "i") "v1" "v2".

Definition array٠unsafe_faa : val :=
  fun: "t" "i" "incr" ⇒
    FAA ("t", "i") "incr".

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Section array_inv.
    Definition array_inv t (sz : nat) : iProp Σ :=
      ∃ l,
      ⌜t = #l⌝ ∗
      l ↦ₕ Header 0 sz.

    #[global] Instance array_inv_timeless t sz :
      Timeless (array_inv t sz).

    #[global] Instance array_inv_persistent t sz :
      Persistent (array_inv t sz).

    Lemma array_inv_agree t sz1 sz2 :
      array_inv t sz1 -∗
      array_inv t sz2 -∗
      ⌜sz1 = sz2⌝.
  End array_inv.

  Section array_slice.
    Definition array_slice t i dq vs : iProp Σ :=
      ∃ l,
      ⌜t = #l⌝ ∗
      chunk_model (l +ₗ i) dq vs.

    #[global] Instance array_slice_timeless t i dq vs :
      Timeless (array_slice t i dq vs).

    #[global] Instance array_slice_persistent t i vs :
      Persistent (array_slice t i DfracDiscarded vs).

    #[global] Instance array_slice_fractional t i vs :
      Fractional (λ q, array_slice t i (DfracOwn q) vs).
    #[global] Instance array_slice_as_fractional t i q vs :
      AsFractional (array_slice t i (DfracOwn q) vs) (λ q, array_slice t i (DfracOwn q) vs) q.

    Lemma array_slice_valid t i dq vs :
      0 < length vs →
      array_slice t i dq vs ⊢
      ⌜✓ dq⌝.
    Lemma array_slice_combine t i dq1 vs1 dq2 vs2 :
      length vs1 = length vs2 →
      array_slice t i dq1 vs1 -∗
      array_slice t i dq2 vs2 -∗
        ⌜vs1 = vs2⌝ ∗
        array_slice t i (dq1 ⋅ dq2) vs1.
    Lemma array_slice_valid_2 t i dq1 vs1 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_slice t i dq1 vs1 -∗
      array_slice t i dq2 vs2 -∗
        ⌜✓ (dq1 ⋅ dq2)⌝ ∗
        ⌜vs1 = vs2⌝.
    Lemma array_slice_agree t i dq1 vs1 dq2 vs2 :
      length vs1 = length vs2 →
      array_slice t i dq1 vs1 -∗
      array_slice t i dq2 vs2 -∗
      ⌜vs1 = vs2⌝.
    Lemma array_slice_dfrac_ne t1 i1 dq1 vs1 t2 i2 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      ¬ ✓ (dq1 ⋅ dq2) →
      array_slice t1 i1 dq1 vs1 -∗
      array_slice t2 i2 dq2 vs2 -∗
      ⌜t1 ≠ t2 ∨ i1 ≠ i2⌝.
    Lemma array_slice_ne t1 i1 vs1 t2 i2 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_slice t1 i1 (DfracOwn 1) vs1 -∗
      array_slice t2 i2 dq2 vs2 -∗
      ⌜t1 ≠ t2 ∨ i1 ≠ i2⌝.
    Lemma array_slice_exclusive t i vs1 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_slice t i (DfracOwn 1) vs1 -∗
      array_slice t i dq2 vs2 -∗
      False.
    Lemma array_slice_persist t i dq vs :
      array_slice t i dq vs ⊢ |==>
      array_slice t i DfracDiscarded vs.

    Lemma array_slice_nil {t i1 dq1 vs1} i2 dq2 :
      array_slice t i1 dq1 vs1 ⊢
      array_slice t i2 dq2 [].

    Lemma array_slice_app t i dq vs1 vs2 :
      array_slice t i dq vs1 ∗
      array_slice t (i + length vs1) dq vs2 ⊣⊢
      array_slice t i dq (vs1 ++ vs2).
    Lemma array_slice_app_1 t i dq vs1 vs2 :
      array_slice t i dq vs1 -∗
      array_slice t (i + length vs1) dq vs2 -∗
      array_slice t i dq (vs1 ++ vs2).
    Lemma array_slice_app_1' {t dq i1 vs1} i2 vs2 :
      i2 = i1 + length vs1 →
      array_slice t i1 dq vs1 -∗
      array_slice t i2 dq vs2 -∗
      array_slice t i1 dq (vs1 ++ vs2).
    Lemma array_slice_app_2 {t i dq vs} vs1 vs2 :
      vs = vs1 ++ vs2 →
      array_slice t i dq vs ⊢
        array_slice t i dq vs1 ∗
        array_slice t (i + length vs1) dq vs2.

    Lemma array_slice_app3 {t i dq} vs1 vs2 vs3 :
      array_slice t i dq vs1 ∗
      array_slice t (i + length vs1) dq vs2 ∗
      array_slice t (i + length vs1 + length vs2) dq vs3 ⊣⊢
      array_slice t i dq (vs1 ++ vs2 ++ vs3).
    Lemma array_slice_app3_1 t dq i1 vs1 i2 vs2 i3 vs3 :
      i2 = i1 + length vs1 →
      i3 = i1 + length vs1 + length vs2 →
      array_slice t i1 dq vs1 -∗
      array_slice t i2 dq vs2 -∗
      array_slice t i3 dq vs3 -∗
      array_slice t i1 dq (vs1 ++ vs2 ++ vs3).
    Lemma array_slice_app3_2 {t i dq vs} vs1 vs2 vs3 :
      vs = vs1 ++ vs2 ++ vs3 →
      array_slice t i dq vs ⊢
        array_slice t i dq vs1 ∗
        array_slice t (i + length vs1) dq vs2 ∗
        array_slice t (i + length vs1 + length vs2) dq vs3.

    Lemma array_slice_cons t i dq v vs :
      array_slice t i dq (v :: vs) ⊣⊢
        array_slice t i dq [v] ∗
        array_slice t (S i) dq vs.
    Lemma array_slice_cons_1 t i dq v vs :
      array_slice t i dq (v :: vs) ⊢
        array_slice t i dq [v] ∗
        array_slice t (S i) dq vs.
    Lemma array_slice_cons_2 t i dq v vs :
      array_slice t i dq [v] -∗
      array_slice t (S i) dq vs -∗
      array_slice t i dq (v :: vs).
    Lemma array_slice_cons_2' t i1 dq v i2 vs :
      i2 = S i1 →
      array_slice t i1 dq [v] -∗
      array_slice t i2 dq vs -∗
      array_slice t i1 dq (v :: vs).

    Lemma array_slice_atomize t i dq vs :
      array_slice t i dq vs ⊢
      [∗ list] j ↦ v ∈ vs,
        array_slice t (i + j) dq [v].

    Lemma array_slice_update {t i dq vs} j v :
      vs !! j = Some v →
      array_slice t i dq vs ⊢
        array_slice t (i + j) dq [v] ∗
        ( ∀ w,
          array_slice t (i + j) dq [w] -∗
          array_slice t i dq (<[j := w]> vs)
        ).
    Lemma array_slice_lookup_acc {t i dq vs} j v :
      vs !! j = Some v →
      array_slice t i dq vs ⊢
        array_slice t (i + j) dq [v] ∗
        ( array_slice t (i + j) dq [v] -∗
          array_slice t i dq vs
        ).
    Lemma array_slice_lookup {t i dq vs} j v :
      vs !! j = Some v →
      array_slice t i dq vs ⊢
      array_slice t (i + j) dq [v].
  End array_slice.

  Section array_model.
    Definition array_model t dq vs : iProp Σ :=
      ∃ l,
      ⌜t = #l⌝ ∗
      l ↦ₕ Header 0 (length vs) ∗
      chunk_model l dq vs.

    Lemma array_model_to_inv t dq vs :
      array_model t dq vs ⊢
      array_inv t (length vs).
    Lemma array_slice_to_model t sz dq vs :
      sz = length vs →
      array_inv t sz -∗
      array_slice t 0 dq vs -∗
      array_model t dq vs.
    Lemma array_model_to_slice t dq vs :
      array_model t dq vs ⊣⊢
        array_inv t (length vs) ∗
        array_slice t 0 dq vs.
    Lemma array_model_to_slice' t dq vs :
      array_model t dq vs ⊢
        array_slice t 0 dq vs ∗
        □ (
          ∀ vs',
          ⌜length vs' = length vs⌝ -∗
          array_slice t 0 dq vs' -∗
          array_model t dq vs'
        ).

    #[global] Instance array_model_timeless t dq vs :
      Timeless (array_model t dq vs).

    #[global] Instance array_model_persistent t vs :
      Persistent (array_model t DfracDiscarded vs).

    #[global] Instance array_model_fractional t vs :
      Fractional (λ q, array_model t (DfracOwn q) vs).
    #[global] Instance array_model_as_fractional t q vs :
      AsFractional (array_model t (DfracOwn q) vs) (λ q, array_model t (DfracOwn q) vs) q.

    Lemma array_inv_model_agree t sz dq vs :
      array_inv t sz -∗
      array_model t dq vs -∗
      ⌜length vs = sz⌝.

    Lemma array_model_valid t dq vs :
      0 < length vs →
      array_model t dq vs ⊢
      ⌜✓ dq⌝.
    Lemma array_model_combine t dq1 vs1 dq2 vs2 :
      array_model t dq1 vs1 -∗
      array_model t dq2 vs2 -∗
        ⌜vs1 = vs2⌝ ∗
        array_model t (dq1 ⋅ dq2) vs1.
    Lemma array_model_valid_2 t dq1 vs1 dq2 vs2 :
      0 < length vs1 →
      array_model t dq1 vs1 -∗
      array_model t dq2 vs2 -∗
        ⌜✓ (dq1 ⋅ dq2)⌝ ∗
        ⌜vs1 = vs2⌝.
    Lemma array_model_agree t dq1 vs1 dq2 vs2 :
      array_model t dq1 vs1 -∗
      array_model t dq2 vs2 -∗
      ⌜vs1 = vs2⌝.
    Lemma array_model_dfrac_ne t1 dq1 vs1 t2 dq2 vs2 :
      0 < length vs1 →
      ¬ ✓ (dq1 ⋅ dq2) →
      array_model t1 dq1 vs1 -∗
      array_model t2 dq2 vs2 -∗
      ⌜t1 ≠ t2⌝.
    Lemma array_model_ne t1 vs1 t2 dq2 vs2 :
      0 < length vs1 →
      array_model t1 (DfracOwn 1) vs1 -∗
      array_model t2 dq2 vs2 -∗
      ⌜t1 ≠ t2⌝.
    Lemma array_model_exclusive t vs1 dq2 vs2 :
      0 < length vs1 →
      array_model t (DfracOwn 1) vs1 -∗
      array_model t dq2 vs2 -∗
      False.
    Lemma array_model_persist t dq vs :
      array_model t dq vs ⊢ |==>
      array_model t DfracDiscarded vs.

    Lemma array_model_atomize t dq vs :
      array_model t dq vs ⊢
        array_inv t (length vs) ∗
        [∗ list] i ↦ v ∈ vs,
          array_slice t i dq [v].

    #[local] Typeclasses Opaque array_slice.
    Lemma array_model_update {t dq vs} i v :
      vs !! i = Some v →
      array_model t dq vs ⊢
        array_inv t (length vs) ∗
        array_slice t i dq [v] ∗
        ( ∀ w,
          array_slice t i dq [w] -∗
          array_model t dq (<[i := w]> vs)
        ).
    Lemma array_model_lookup_acc {t dq vs} i v :
      vs !! i = Some v →
      array_model t dq vs ⊢
        array_slice t i dq [v] ∗
        ( array_slice t i dq [v] -∗
          array_model t dq vs
        ).
    Lemma array_model_lookup {t dq vs} i v :
      vs !! i = Some v →
      array_model t dq vs ⊢
      array_slice t i dq [v].
  End array_model.

  Section array_cslice.
    Definition array_cslice t (sz : nat) i dq vs : iProp Σ :=
      ∃ l,
      ⌜t = #l⌝ ∗
      l ↦ₕ Header 0 sz ∗
      chunk_cslice l sz i dq vs.

    Lemma array_cslice_to_inv t sz i dq vs :
      array_cslice t sz i dq vs ⊢
      array_inv t sz.
    Lemma array_model_to_cslice t dq vs :
      array_model t dq vs ⊢
      array_cslice t (length vs) 0 dq vs.
    Lemma array_cslice_to_slice t sz i dq vs :
      0 < sz →
      length vs ≤ sz →
      array_cslice t sz i dq vs ⊣⊢
        array_inv t sz ∗
        array_slice t (i `mod` sz) dq (take (sz - i `mod` sz) vs) ∗
        array_slice t 0 dq (drop (sz - i `mod` sz) vs).
    Lemma array_cslice_to_slice' t sz i dq vs :
      0 < sz →
      length vs ≤ sz →
      array_cslice t sz i dq vs ⊢
        array_slice t (i `mod` sz) dq (take (sz - i `mod` sz) vs) ∗
        array_slice t 0 dq (drop (sz - i `mod` sz) vs).
    Lemma array_cslice_to_model t sz i dq vs :
      0 < sz →
      length vs = sz →
      array_cslice t sz i dq vs ⊣⊢
      array_model t dq (rotation (sz - i `mod` sz) vs).
    Lemma array_cslice_to_slice_cell t sz i dq v :
      array_cslice t sz i dq [v] ⊣⊢
        array_inv t sz ∗
        array_slice t (i `mod` sz) dq [v].
    Lemma array_cslice_to_slice_cell' t sz i dq v :
      array_cslice t sz i dq [v] ⊢
      array_slice t (i `mod` sz) dq [v].
    Lemma array_slice_to_cslice_cell t sz i dq v :
      array_inv t sz -∗
      array_slice t (i `mod` sz) dq [v] -∗
      array_cslice t sz i dq [v].

    #[global] Instance array_cslice_timeless t sz i dq vs :
      Timeless (array_cslice t sz i dq vs).

    #[global] Instance array_cslice_persistent t sz i vs :
      Persistent (array_cslice t sz i DfracDiscarded vs).

    #[global] Instance array_cslice_fractional t sz i vs :
      Fractional (λ q, array_cslice t sz i (DfracOwn q) vs).
    #[global] Instance array_cslice_as_fractionak t sz i q vs :
      AsFractional (array_cslice t sz i (DfracOwn q) vs) (λ q, array_cslice t sz i (DfracOwn q) vs) q.

    Lemma array_inv_cslice_agree t sz1 sz2 i dq vs :
      array_inv t sz1 -∗
      array_cslice t sz2 i dq vs -∗
      ⌜sz1 = sz2⌝.

    Lemma array_cslice_nil t sz i dq :
      array_inv t sz ⊢
      array_cslice t sz i dq [].

    Lemma array_cslice_app t sz i dq vs1 vs2 :
      array_cslice t sz i dq vs1 ∗
      array_cslice t sz (i + length vs1) dq vs2 ⊣⊢
      array_cslice t sz i dq (vs1 ++ vs2).
    Lemma array_cslice_app_1 t sz dq i1 vs1 i2 vs2 :
      i2 = i1 + length vs1 →
      array_cslice t sz i1 dq vs1 -∗
      array_cslice t sz i2 dq vs2 -∗
      array_cslice t sz i1 dq (vs1 ++ vs2).
    Lemma array_cslice_app_2 {t sz i dq vs} vs1 vs2 :
      vs = vs1 ++ vs2 →
      array_cslice t sz i dq vs ⊢
        array_cslice t sz i dq vs1 ∗
        array_cslice t sz (i + length vs1) dq vs2.

    Lemma array_cslice_app3 t sz i dq vs1 vs2 vs3 :
      array_cslice t sz i dq vs1 ∗
      array_cslice t sz (i + length vs1) dq vs2 ∗
      array_cslice t sz (i + length vs1 + length vs2) dq vs3 ⊣⊢
      array_cslice t sz i dq (vs1 ++ vs2 ++ vs3).
    Lemma array_cslice_app3_1 t sz dq i1 vs1 i2 vs2 i3 vs3 :
      i2 = i1 + length vs1 →
      i3 = i1 + length vs1 + length vs2 →
      array_cslice t sz i1 dq vs1 -∗
      array_cslice t sz i2 dq vs2 -∗
      array_cslice t sz i3 dq vs3 -∗
      array_cslice t sz i1 dq (vs1 ++ vs2 ++ vs3).
    Lemma array_cslice_app3_2 {t sz i dq vs} vs1 vs2 vs3 :
      vs = vs1 ++ vs2 ++ vs3 →
      array_cslice t sz i dq vs ⊢
        array_cslice t sz i dq vs1 ∗
        array_cslice t sz (i + length vs1) dq vs2 ∗
        array_cslice t sz (i + length vs1 + length vs2) dq vs3.

    Lemma array_cslice_cons t sz i dq v vs :
      array_cslice t sz i dq (v :: vs) ⊣⊢
        array_cslice t sz i dq [v] ∗
        array_cslice t sz (S i) dq vs.
    Lemma array_cslice_cons_1 t sz i dq v vs :
      array_cslice t sz i dq (v :: vs) ⊢
        array_cslice t sz i dq [v] ∗
        array_cslice t sz (S i) dq vs.
    Lemma array_cslice_cons_2 t sz i dq v vs :
      array_cslice t sz i dq [v] -∗
      array_cslice t sz (S i) dq vs -∗
      array_cslice t sz i dq (v :: vs).
    Lemma array_cslice_cons_2' t sz i1 dq v i2 vs :
      i2 = S i1 →
      array_cslice t sz i1 dq [v] -∗
      array_cslice t sz i2 dq vs -∗
      array_cslice t sz i1 dq (v :: vs).

    Lemma array_cslice_atomize sz t i dq vs :
      array_cslice t sz i dq vs ⊢
      [∗ list] j ↦ v ∈ vs,
        array_cslice t sz (i + j) dq [v].

    Lemma array_cslice_update {t sz i dq vs} j v :
      vs !! j = Some v →
      array_cslice t sz i dq vs ⊢
        array_cslice t sz (i + j) dq [v] ∗
        ( ∀ w,
          array_cslice t sz (i + j) dq [w] -∗
          array_cslice t sz i dq (<[j := w]> vs)
        ).
    Lemma array_cslice_lookup_acc {t sz i dq vs} j v :
      vs !! j = Some v →
      array_cslice t sz i dq vs ⊢
        array_cslice t sz (i + j) dq [v] ∗
        ( array_cslice t sz (i + j) dq [v] -∗
          array_cslice t sz i dq vs
        ).
    Lemma array_cslice_lookup {t sz i dq vs} j v :
      vs !! j = Some v →
      array_cslice t sz i dq vs ⊢
      array_cslice t sz (i + j) dq [v].

    Lemma array_cslice_shift t sz i dq vs :
      array_cslice t sz i dq vs ⊣⊢
      array_cslice t sz (i + sz) dq vs.

    Lemma array_cslice_shift_right t sz i dq vs :
      array_cslice t sz i dq vs ⊢
      array_cslice t sz (i + sz) dq vs.
    Lemma array_cslice_shift_right' {t sz i1 dq vs} i2 :
      i2 = i1 + sz →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq vs.

    Lemma array_cslice_shift_left t sz i dq vs :
      sz ≤ i →
      array_cslice t sz i dq vs ⊢
      array_cslice t sz (i - sz) dq vs.
    Lemma array_cslice_shift_left' {t sz i1 dq vs} i2 :
      sz ≤ i1 →
      i2 = i1 - sz →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq vs.

    Lemma array_cslice_rotation_right {t sz i dq vs} n :
      0 < sz →
      length vs = sz →
      array_cslice t sz i dq vs ⊣⊢
      array_cslice t sz (i + n) dq (rotation (n `mod` sz) vs).
    Lemma array_cslice_rotation_right_1 {t sz i dq vs} n :
      0 < sz →
      length vs = sz →
      array_cslice t sz i dq vs ⊢
      array_cslice t sz (i + n) dq (rotation (n `mod` sz) vs).
    Lemma array_cslice_rotation_right_0 {t sz dq vs} i :
      0 < sz →
      length vs = sz →
      array_cslice t sz 0 dq vs ⊣⊢
      array_cslice t sz i dq (rotation (i `mod` sz) vs).

    Lemma array_cslice_rotation_right' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i2 = i1 + n →
      array_cslice t sz i1 dq vs ⊣⊢
      array_cslice t sz i2 dq (rotation (n `mod` sz) vs).
    Lemma array_cslice_rotation_right_1' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i2 = i1 + n →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq (rotation (n `mod` sz) vs).

    Lemma array_cslice_rotation_right_small {t sz i dq vs} n :
      0 < sz →
      length vs = sz →
      n < sz →
      array_cslice t sz i dq vs ⊣⊢
      array_cslice t sz (i + n) dq (rotation n vs).
    Lemma array_cslice_rotation_right_small_1 {t sz i dq vs} n :
      0 < sz →
      length vs = sz →
      n < sz →
      array_cslice t sz i dq vs ⊢
      array_cslice t sz (i + n) dq (rotation n vs).

    Lemma array_cslice_rotation_right_small' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i2 = i1 + n →
      n < sz →
      array_cslice t sz i1 dq vs ⊣⊢
      array_cslice t sz i2 dq (rotation n vs).
    Lemma array_cslice_rotation_right_small_1' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i2 = i1 + n →
      n < sz →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq (rotation n vs).

    Lemma array_cslice_rotation_left t sz i n dq vs :
      0 < sz →
      length vs = sz →
      array_cslice t sz (i + n) dq vs ⊣⊢
      array_cslice t sz i dq (rotation (sz - n `mod` sz) vs).
    Lemma array_cslice_rotation_left_1 t sz i n dq vs :
      0 < sz →
      length vs = sz →
      array_cslice t sz (i + n) dq vs ⊢
      array_cslice t sz i dq (rotation (sz - n `mod` sz) vs).
    Lemma array_cslice_rotation_left_0 t sz i dq vs :
      0 < sz →
      length vs = sz →
      array_cslice t sz i dq vs ⊣⊢
      array_cslice t sz 0 dq (rotation (sz - i `mod` sz) vs).

    Lemma array_cslice_rotation_left' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i1 = i2 + n →
      array_cslice t sz i1 dq vs ⊣⊢
      array_cslice t sz i2 dq (rotation (sz - n `mod` sz) vs).
    Lemma array_cslice_rotation_left_1' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i1 = i2 + n →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq (rotation (sz - n `mod` sz) vs).

    Lemma array_cslice_rotation_left_small t sz i n dq vs :
      0 < sz →
      length vs = sz →
      n < sz →
      array_cslice t sz (i + n) dq vs ⊣⊢
      array_cslice t sz i dq (rotation (sz - n) vs).
    Lemma array_cslice_rotation_left_small_1 t sz i n dq vs :
      0 < sz →
      length vs = sz →
      n < sz →
      array_cslice t sz (i + n) dq vs ⊢
      array_cslice t sz i dq (rotation (sz - n) vs).

    Lemma array_cslice_rotation_left_small' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i1 = i2 + n →
      n < sz →
      array_cslice t sz i1 dq vs ⊣⊢
      array_cslice t sz i2 dq (rotation (sz - n) vs).
    Lemma array_cslice_rotation_left_small_1' {t sz i1 dq vs} i2 n :
      0 < sz →
      length vs = sz →
      i1 = i2 + n →
      n < sz →
      array_cslice t sz i1 dq vs ⊢
      array_cslice t sz i2 dq (rotation (sz - n) vs).

    Lemma array_cslice_rebase {t sz i1 dq vs1} i2 :
      0 < sz →
      length vs1 = sz →
      array_cslice t sz i1 dq vs1 ⊢
        ∃ vs2 n,
        ⌜vs2 = rotation n vs1⌝ ∗
        array_cslice t sz i2 dq vs2 ∗
        ( array_cslice t sz i2 dq vs2 -∗
          array_cslice t sz i1 dq vs1
        ).

    Lemma array_cslice_valid t sz i dq vs :
      0 < length vs →
      array_cslice t sz i dq vs ⊢
      ⌜✓ dq⌝.
    Lemma array_cslice_combine t sz i dq1 vs1 dq2 vs2 :
      length vs1 = length vs2 →
      array_cslice t sz i dq1 vs1 -∗
      array_cslice t sz i dq2 vs2 -∗
        ⌜vs1 = vs2⌝ ∗
        array_cslice t sz i (dq1 ⋅ dq2) vs1.
    Lemma array_cslice_valid_2 t sz i dq1 vs1 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_cslice t sz i dq1 vs1 -∗
      array_cslice t sz i dq2 vs2 -∗
        ⌜✓ (dq1 ⋅ dq2)⌝ ∗
        ⌜vs1 = vs2⌝.
    Lemma array_cslice_agree t sz i dq1 vs1 dq2 vs2 :
      length vs1 = length vs2 →
      array_cslice t sz i dq1 vs1 -∗
      array_cslice t sz i dq2 vs2 -∗
      ⌜vs1 = vs2⌝.
    Lemma array_cslice_dfrac_ne t sz i1 dq1 vs1 i2 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      ¬ ✓ (dq1 ⋅ dq2) →
      array_cslice t sz i1 dq1 vs1 -∗
      array_cslice t sz i2 dq2 vs2 -∗
      ⌜i1 ≠ i2⌝.
    Lemma array_cslice_ne t sz i1 vs1 i2 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_cslice t sz i1 (DfracOwn 1) vs1 -∗
      array_cslice t sz i2 dq2 vs2 -∗
      ⌜i1 ≠ i2⌝.
    Lemma array_cslice_exclusive t sz i vs1 dq2 vs2 :
      0 < length vs1 →
      length vs1 = length vs2 →
      array_cslice t sz i (DfracOwn 1) vs1 -∗
      array_cslice t sz i dq2 vs2 -∗
      False.
    Lemma array_cslice_persist t sz i dq vs :
      array_cslice t sz i dq vs ⊢ |==>
      array_cslice t sz i DfracDiscarded vs.

    Lemma array_cslice_length t sz i vs :
      0 < sz →
      array_cslice t sz i (DfracOwn 1) vs ⊢
      ⌜length vs ≤ sz⌝.
  End array_cslice.

  #[local] Typeclasses Opaque
    array_inv
    array_slice
    array_model
    array_cslice.

  Notation au_load t i Φ := (
    AU <{
      ∃∃ dq v,
      array_slice t i dq [v]
    }> @ ⊤, ∅ <{
      array_slice t i dq [v],
    COMM
      Φ v
    }>
  )%I.
  Notation au_store t i v P := (
    AU <{
      ∃∃ w,
      array_slice t i (DfracOwn 1) [w]
    }> @ ⊤, ∅ <{
      array_slice t i (DfracOwn 1) [v],
    COMM
      P
    }>
  )%I.

  Lemma array٠unsafe_alloc𑁒spec sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      array٠unsafe_alloc #sz
    {{{
      t
    , RET t;
      array_model t (DfracOwn 1) (replicate ₊sz ()%V)
    }}}.

  Lemma array٠alloc𑁒spec sz :
    {{{
      True
    }}}
      array٠alloc #sz
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      array_model t (DfracOwn 1) (replicate ₊sz ()%V)
    }}}.

  Lemma array٠create𑁒spec :
    {{{
      True
    }}}
      array٠create ()
    {{{
      t
    , RET t;
      array_model t (DfracOwn 1) []
    }}}.

  Lemma array٠size𑁒spec_inv t sz :
    {{{
      array_inv t sz
    }}}
      array٠size t
    {{{
      RET #sz;
      True
    }}}.
  Lemma array٠size𑁒spec_atomic t :
    <<<
      True
    | ∀∀ dq vs,
      array_model t dq vs
    >>>
      array٠size t
    <<<
      array_model t dq vs
    | RET #(length vs);
      £ 1 ∗
      array_inv t (length vs)
    >>>.
  Lemma array٠size𑁒spec_atomic_cslice t :
    <<<
      True
    | ∀∀ sz i dq vs,
      array_cslice t sz i dq vs
    >>>
      array٠size t
    <<<
      array_cslice t sz i dq vs
    | RET #sz;
      £ 1 ∗
      array_inv t sz
    >>>.
  Lemma array٠size𑁒spec t dq vs :
    {{{
      array_model t dq vs
    }}}
      array٠size t
    {{{
      RET #(length vs);
      array_model t dq vs
    }}}.
  Lemma array٠size𑁒spec_cslice t sz i dq vs :
    {{{
      array_cslice t sz i dq vs
    }}}
      array٠size t
    {{{
      RET #sz;
      array_cslice t sz i dq vs
    }}}.

  Lemma array٠unsafe_get𑁒spec_atomic_slice t (j : Z) :
    <<<
      True
    | ∀∀ dq vs i v,
      ⌜(i ≤ j)%Z⌝ ∗
      ⌜vs !! (₊j - i) = Some v⌝ ∗
      array_slice t i dq vs
    >>>
      array٠unsafe_get t #j
    <<<
      array_slice t i dq vs
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_get𑁒spec_atomic_cell t (i : Z) :
    <<<
      True
    | ∀∀ i_ dq v,
      ⌜i = ⁺i_⌝ ∗
      array_slice t i_ dq [v]
    >>>
      array٠unsafe_get t #i
    <<<
      array_slice t ₊i dq [v]
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_get𑁒spec_atomic t (i : Z) :
    (0 ≤ i)%Z →
    <<<
      True
    | ∀∀ dq vs v,
      ⌜vs !! ₊i = Some v⌝ ∗
      array_model t dq vs
    >>>
      array٠unsafe_get t #i
    <<<
      array_model t dq vs
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_get𑁒spec_atomic_inv t (sz : nat) (i : Z) :
    (0 ≤ i < sz)%Z →
    <<<
      array_inv t sz
    | ∀∀ vs,
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_get t #i
    <<<
      ∃∃ v,
      ⌜vs !! ₊i = Some v⌝ ∗
      array_model t (DfracOwn 1) vs
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_get𑁒spec_slice k t i dq vs (j : Z) v :
    (i ≤ j)%Z →
    vs !! k = Some v →
    k = ₊j - i →
    {{{
      array_slice t i dq vs
    }}}
      array٠unsafe_get t #j
    {{{
      RET v;
      array_slice t i dq vs
    }}}.
  Lemma array٠unsafe_get𑁒spec_cell t (i : Z) i_ dq v :
    i = ₊i_ →
    {{{
      array_slice t i_ dq [v]
    }}}
      array٠unsafe_get t #i
    {{{
      RET v;
      array_slice t i_ dq [v]
    }}}.
  Lemma array٠unsafe_get𑁒spec i_ t (i : Z) dq vs v :
    (0 ≤ i)%Z →
    vs !! i_ = Some v →
    i_ = ₊i →
    {{{
      array_model t dq vs
    }}}
      array٠unsafe_get t #i
    {{{
      RET v;
      array_model t dq vs
    }}}.

  Lemma array٠get𑁒spec_atomic_slice t sz (j : Z) :
    <<<
      array_inv t sz
    | ∀∀ dq vs i v,
      ⌜0 ≤ j < sz⌝%Z -∗
        ⌜i ≤ ₊j⌝ ∗
        ⌜vs !! (₊j - i) = Some v⌝ ∗
        array_slice t i dq vs
    >>>
      array٠get t #j
    <<<
      array_slice t i dq vs
    | RET v;
      ⌜0 ≤ j < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠get𑁒spec_atomic_cell t sz (i : Z) i_ :
    i_ = ₊i →
    <<<
      array_inv t sz
    | ∀∀ dq v,
      ⌜0 ≤ i < sz⌝%Z -∗
      array_slice t i_ dq [v]
    >>>
      array٠get t #i
    <<<
      array_slice t i_ dq [v]
    | RET v;
      ⌜0 ≤ i < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠get𑁒spec_atomic t sz (i : Z) :
    <<<
      array_inv t sz
    | ∀∀ dq vs v,
      ⌜0 ≤ i < sz⌝%Z -∗
        ⌜vs !! ₊i = Some v⌝ ∗
        array_model t dq vs
    >>>
      array٠get t #i
    <<<
      array_model t dq vs
    | RET v;
      ⌜0 ≤ i < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠get𑁒spec_slice k t sz i dq vs (j : Z) v :
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ j < sz⌝%Z -∗
          ⌜i ≤ ₊j⌝ ∗
          ⌜vs !! k = Some v⌝ ∗
          ⌜k = ₊j - i⌝ ∗
          array_slice t i dq vs
      )
    }}}
      array٠get t #j
    {{{
      RET v;
      ⌜0 ≤ j < sz⌝%Z ∗
      array_slice t i dq vs
    }}}.
  Lemma array٠get𑁒spec_cell t sz (i : Z) i_ dq v :
    i_ = ₊i →
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ i < sz⌝%Z -∗
        array_slice t i_ dq [v]
      )
    }}}
      array٠get t #i
    {{{
      RET v;
      ⌜0 ≤ i < sz⌝%Z ∗
      array_slice t i_ dq [v]
    }}}.
  Lemma array٠get𑁒spec t (i : Z) dq vs v :
    {{{
      array_model t dq vs ∗
      ( ⌜0 ≤ i < length vs⌝%Z -∗
        ⌜vs !! ₊i = Some v⌝
      )
    }}}
      array٠get t #i
    {{{
      RET v;
      ⌜0 ≤ i < length vs⌝%Z ∗
      array_model t dq vs
    }}}.

  Lemma array٠unsafe_set𑁒spec_atomic_slice t (j : Z) v :
    <<<
      True
    | ∀∀ vs i,
      ⌜i ≤ j < i + length vs⌝%Z ∗
      array_slice t i (DfracOwn 1) vs
    >>>
      array٠unsafe_set t #j v
    <<<
      ∃∃ w,
      ⌜vs !! (₊j - i) = Some w⌝ ∗
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_set𑁒spec_atomic_cell t (i : Z) v :
    <<<
      True
    | ∀∀ i_ w,
      ⌜i = ⁺i_⌝ ∗
      array_slice t i_ (DfracOwn 1) [w]
    >>>
      array٠unsafe_set t #i v
    <<<
      array_slice t i_ (DfracOwn 1) [v]
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_set𑁒spec_atomic t (i : Z) v :
    (0 ≤ i)%Z →
    <<<
      True
    | ∀∀ vs,
      ⌜i < length vs⌝%Z ∗
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_set t #i v
    <<<
      ∃∃ w,
      ⌜vs !! ₊i = Some w⌝ ∗
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_set𑁒spec_atomic_inv t (sz : nat) (i : Z) v :
    (0 ≤ i < sz)%Z →
    <<<
      array_inv t sz
    | ∀∀ vs,
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_set t #i v
    <<<
      ∃∃ w,
      ⌜vs !! ₊i = Some w⌝ ∗
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_set𑁒spec_slice t i vs (j : Z) v :
    (i ≤ j < i + length vs)%Z →
    {{{
      array_slice t i (DfracOwn 1) vs
    }}}
      array٠unsafe_set t #j v
    {{{
      RET ();
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    }}}.
  Lemma array٠unsafe_set𑁒spec_cell t (i : Z) i_ w v :
    i = ⁺i_ →
    {{{
      array_slice t i_ (DfracOwn 1) [w]
    }}}
      array٠unsafe_set t #i v
    {{{
      RET ();
      array_slice t i_ (DfracOwn 1) [v]
    }}}.
  Lemma array٠unsafe_set𑁒spec t (i : Z) vs v :
    (0 ≤ i < length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_set t #i v
    {{{
      RET ();
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    }}}.

  Lemma array٠set𑁒spec_atomic_slice t sz (j : Z) v :
    <<<
      array_inv t sz
    | ∀∀ vs i,
      ⌜0 ≤ j < sz⌝%Z -∗
        ⌜i ≤ ₊j < i + length vs⌝ ∗
        array_slice t i (DfracOwn 1) vs
    >>>
      array٠set t #j v
    <<<
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    | RET ();
      ⌜0 ≤ j < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠set𑁒spec_atomic_cell t sz (i : Z) i_ v :
    i_ = ₊i →
    <<<
      array_inv t sz
    | ∀∀ w,
      ⌜0 ≤ i < sz⌝%Z -∗
      array_slice t i_ (DfracOwn 1) [w]
    >>>
      array٠set t #i v
    <<<
      array_slice t i_ (DfracOwn 1) [v]
    | RET ();
      ⌜0 ≤ i < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠set𑁒spec_atomic t sz (i : Z) v :
    <<<
      array_inv t sz
    | ∀∀ vs,
      ⌜0 ≤ i < sz⌝%Z -∗
        ⌜(₊i < length vs)%Z⌝ ∗
        array_model t (DfracOwn 1) vs
    >>>
      array٠set t #i v
    <<<
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    | RET ();
      ⌜0 ≤ i < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠set𑁒spec_slice t sz i vs (j : Z) v :
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ j < sz⌝%Z -∗
          ⌜i ≤ ₊j < i + length vs⌝ ∗
          array_slice t i (DfracOwn 1) vs
      )
    }}}
      array٠set t #j v
    {{{
      RET ();
      ⌜0 ≤ j < sz⌝%Z ∗
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    }}}.
  Lemma array٠set𑁒spec_cell t sz (i : Z) i_ w v :
    i_ = ₊i →
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ i < sz⌝%Z -∗
        array_slice t i_ (DfracOwn 1) [w]
      )
    }}}
      array٠set t #i v
    {{{
      RET ();
      ⌜0 ≤ i < sz⌝%Z ∗
      array_slice t i_ (DfracOwn 1) [v]
    }}}.
  Lemma array٠set𑁒spec t (i : Z) vs v :
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠set t #i v
    {{{
      RET ();
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    }}}.

  Lemma array٠unsafe_xchg𑁒spec_atomic_slice t (j : Z) v :
    <<<
      True
    | ∀∀ vs i,
      ⌜i ≤ j < i + length vs⌝%Z ∗
      array_slice t i (DfracOwn 1) vs
    >>>
      array٠unsafe_xchg t #j v
    <<<
      ∃∃ w,
      ⌜vs !! (₊j - i) = Some w⌝ ∗
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    | RET w;
      £ 1
    >>>.
  Lemma array٠unsafe_xchg𑁒spec_atomic_cell t (i : Z) v :
    <<<
      True
    | ∀∀ i_ w,
      ⌜i = ⁺i_⌝ ∗
      array_slice t i_ (DfracOwn 1) [w]
    >>>
      array٠unsafe_xchg t #i v
    <<<
      array_slice t i_ (DfracOwn 1) [v]
    | RET w;
      £ 1
    >>>.
  Lemma array٠unsafe_xchg𑁒spec_atomic t (i : Z) v :
    (0 ≤ i)%Z →
    <<<
      True
    | ∀∀ vs,
      ⌜i < length vs⌝%Z ∗
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_xchg t #i v
    <<<
      ∃∃ w,
      ⌜vs !! ₊i = Some w⌝ ∗
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    | RET w;
      £ 1
    >>>.
  Lemma array٠unsafe_xchg𑁒spec_atomic_inv t (sz : nat) (i : Z) v :
    (0 ≤ i < sz)%Z →
    <<<
      array_inv t sz
    | ∀∀ vs,
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_xchg t #i v
    <<<
      ∃∃ w,
      ⌜vs !! ₊i = Some w⌝ ∗
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    | RET w;
      £ 1
    >>>.
  Lemma array٠unsafe_xchg𑁒spec_slice t i vs (j : Z) v :
    (i ≤ j < i + length vs)%Z →
    {{{
      array_slice t i (DfracOwn 1) vs
    }}}
      array٠unsafe_xchg t #j v
    {{{
      w
    , RET w;
      ⌜vs !! (₊j - i) = Some w⌝ ∗
      array_slice t i (DfracOwn 1) (<[₊j - i := v]> vs)
    }}}.
  Lemma array٠unsafe_xchg𑁒spec_cell t (i : Z) i_ w v :
    i = ⁺i_ →
    {{{
      array_slice t i_ (DfracOwn 1) [w]
    }}}
      array٠unsafe_xchg t #i v
    {{{
      RET w;
      array_slice t i_ (DfracOwn 1) [v]
    }}}.
  Lemma array٠unsafe_xchg𑁒spec t (i : Z) vs v :
    (0 ≤ i < length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_xchg t #i v
    {{{
      w
    , RET w;
      ⌜vs !! ₊i = Some w⌝ ∗
      array_model t (DfracOwn 1) (<[₊i := v]> vs)
    }}}.

  Lemma array٠unsafe_cas𑁒spec_atomic_slice t (j : Z) v1 v2 :
    <<<
      True
    | ∀∀ vs i,
      ⌜i ≤ j < i + length vs⌝%Z ∗
      array_slice t i (DfracOwn 1) vs
    >>>
      array٠unsafe_cas t #j v1 v2
    <<<
      ∃∃ b v,
      ⌜vs !! (₊j - i) = Some v⌝ ∗
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_slice t i (DfracOwn 1) (if b then <[₊j - i := v2]> vs else vs)
    | RET #b;
      £ 1
    >>>.
  Lemma array٠unsafe_cas𑁒spec_atomic_cell t (i : Z) v1 v2 :
    <<<
      True
    | ∀∀ i_ v,
      ⌜i = ⁺i_⌝ ∗
      array_slice t i_ (DfracOwn 1) [v]
    >>>
      array٠unsafe_cas t #i v1 v2
    <<<
      ∃∃ b,
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_slice t i_ (DfracOwn 1) [if b then v2 else v]
    | RET #b;
      £ 1
    >>>.
  Lemma array٠unsafe_cas𑁒spec_atomic t (i : Z) v1 v2 :
    (0 ≤ i)%Z →
    <<<
      True
    | ∀∀ vs,
      ⌜i < length vs⌝%Z ∗
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_cas t #i v1 v2
    <<<
      ∃∃ b v,
      ⌜vs !! ₊i = Some v⌝ ∗
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_model t (DfracOwn 1) (if b then <[₊i := v2]> vs else vs)
    | RET #b;
      £ 1
    >>>.
  Lemma array٠unsafe_cas𑁒spec_atomic_inv t (sz : nat) (i : Z) v1 v2 :
    (0 ≤ i < sz)%Z →
    <<<
      array_inv t sz
    | ∀∀ vs,
      array_model t (DfracOwn 1) vs
    >>>
      array٠unsafe_cas t #i v1 v2
    <<<
      ∃∃ b v,
      ⌜vs !! ₊i = Some v⌝ ∗
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_model t (DfracOwn 1) (if b then <[₊i := v2]> vs else vs)
    | RET #b;
      £ 1
    >>>.
  Lemma array٠unsafe_cas𑁒spec_slice t i vs (j : Z) v1 v2 :
    (i ≤ j < i + length vs)%Z →
    {{{
      array_slice t i (DfracOwn 1) vs
    }}}
      array٠unsafe_cas t #j v1 v2
    {{{
      b v
    , RET #b;
      ⌜vs !! (₊j - i) = Some v⌝ ∗
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_slice t i (DfracOwn 1) (if b then <[₊j - i := v2]> vs else vs)
    }}}.
  Lemma array٠unsafe_cas𑁒spec_cell t (i : Z) i_ v v1 v2 :
    i = ⁺i_ →
    {{{
      array_slice t i_ (DfracOwn 1) [v]
    }}}
      array٠unsafe_cas t #i v1 v2
    {{{
      b
    , RET #b;
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_slice t i_ (DfracOwn 1) [if b then v2 else v]
    }}}.
  Lemma array٠unsafe_cas𑁒spec t (i : Z) vs v1 v2 :
    (0 ≤ i < length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_cas t #i v1 v2
    {{{
      b v
    , RET #b;
      ⌜vs !! ₊i = Some v⌝ ∗
      ⌜(if b then (≈) else (≉)) v v1⌝ ∗
      array_model t (DfracOwn 1) (if b then <[₊i := v2]> vs else vs)
    }}}.

  Lemma array٠unsafe_swap𑁒spec_slice {t i vs} {i1 : Z} k1 {v1} {i2 : Z} k2 v2 :
    (i ≤ i1)%Z →
    (i ≤ i2)%Z →
    vs !! k1 = Some v1 →
    k1 = ₊i1 - i →
    vs !! k2 = Some v2 →
    k2 = ₊i2 - i →
    {{{
      array_slice t i (DfracOwn 1) vs
    }}}
      array٠unsafe_swap t #i1 #i2
    {{{
      RET ();
      array_slice t i (DfracOwn 1) (<[k2 := v1]> $ <[k1 := v2]> vs)
    }}}.
  Lemma array٠unsafe_swap𑁒spec_slice_id t i vs (i1 i2 : Z) :
    i1 = i2 →
    (i ≤ i1 < i + length vs)%Z →
    {{{
      array_slice t i (DfracOwn 1) vs
    }}}
      array٠unsafe_swap t #i1 #i2
    {{{
      RET ();
      array_slice t i (DfracOwn 1) vs
    }}}.
  Lemma array٠unsafe_swap𑁒spec {t vs} {i1 : Z} i1_ {v1} {i2 : Z} i2_ v2 :
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    vs !! i1_ = Some v1 →
    i1_ = ₊i1 →
    vs !! i2_ = Some v2 →
    i2_ = ₊i2 →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_swap t #i1 #i2
    {{{
      RET ();
      array_model t (DfracOwn 1) (<[i2_ := v1]> $ <[i1_ := v2]> vs)
    }}}.

  Lemma array٠unsafe_fill_slice𑁒spec_atomic Ψ t (i n : Z) v :
    (0 ≤ i)%Z →
    {{{
      ▷ Ψ 0 ∗
      □ (
        ∀ j,
        ⌜j < ₊n⌝ -∗
        Ψ j -∗
        au_store t (₊i + j) v (
          ▷ Ψ (S j)
        )
      )
    }}}
      array٠unsafe_fill_slice t #i #n v
    {{{
      RET ();
      Ψ ₊n
    }}}.
  Lemma array٠unsafe_fill_slice𑁒spec_slice_fit t vs (i : Z) i_ (n : Z) v :
    i = ⁺i_ →
    ₊n = length vs →
    {{{
      array_slice t i_ (DfracOwn 1) vs
    }}}
      array٠unsafe_fill_slice t #i #n v
    {{{
      RET ();
      array_slice t i_ (DfracOwn 1) (replicate ₊n v)
    }}}.
  Lemma array٠unsafe_fill_slice𑁒spec_slice t vs (i : Z) j (n : Z) v :
    (j ≤ i)%Z →
    ₊i + ₊n ≤ j + length vs →
    {{{
      array_slice t j (DfracOwn 1) vs
    }}}
      array٠unsafe_fill_slice t #i #n v
    {{{
      RET ();
      array_slice t j (DfracOwn 1) (with_slice (₊i - j) ₊n vs (replicate ₊n v))
    }}}.
  Lemma array٠unsafe_fill_slice𑁒spec t vs (i : Z) (n : Z) v :
    (0 ≤ i)%Z →
    ₊i + ₊n ≤ length vs →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_fill_slice t #i #n v
    {{{
      RET ();
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs (replicate ₊n v))
    }}}.

  Lemma array٠fill_slice𑁒spec t sz vs (i : Z) i_ (n : Z) v :
    i_ = ₊i →
    ₊n = length vs →
    {{{
      array_inv t sz ∗
      array_slice t i_ (DfracOwn 1) vs
    }}}
      array٠fill_slice t #i #n v
    {{{
      RET ();
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      array_slice t i_ (DfracOwn 1) (replicate ₊n v)
    }}}.

  Lemma array٠fill𑁒spec t vs v :
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠fill t v
    {{{
      RET ();
      array_model t (DfracOwn 1) (replicate (length vs) v)
    }}}.

  Lemma array٠unsafe_make𑁒spec sz v :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      array٠unsafe_make #sz v
    {{{
      t
    , RET t;
      array_model t (DfracOwn 1) (replicate ₊sz v)
    }}}.

  Lemma array٠make𑁒spec sz v :
    {{{
      True
    }}}
      array٠make #sz v
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      array_model t (DfracOwn 1) (replicate ₊sz v)
    }}}.

  #[local] Lemma array٠foldli_aux𑁒spec vs Ψ fn t sz i acc :
    i ≤ sz →
    i = length vs →
    {{{
      ▷ Ψ i vs None acc ∗
      □ (
        ∀ i vs (o : option val) acc,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ i vs o acc -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v) acc
            )
        | Some v ⇒
            WP fn #i acc v {{ acc,
              ▷ Ψ (S i) (vs ++ [v]) None acc
            }}
        end
      )
    }}}
      array٠foldli_aux fn t #sz #i acc
    {{{
      vs' acc
    , RET acc;
      ⌜(length vs + length vs')%nat = sz⌝ ∗
      Ψ sz (vs ++ vs') None acc
    }}}.
  Lemma array٠foldli𑁒spec_atomic Ψ fn acc t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None acc ∗
      □ (
        ∀ i vs (o : option val) acc,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ i vs o acc -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v) acc
            )
        | Some v ⇒
            WP fn #i acc v {{ acc,
              ▷ Ψ (S i) (vs ++ [v]) None acc
            }}
        end
      )
    }}}
      array٠foldli fn acc t
    {{{
      vs acc
    , RET acc;
      ⌜length vs = sz⌝ ∗
      Ψ sz vs None acc
    }}}.
  Lemma array٠foldli𑁒spec Ψ fn acc t dq vs :
    {{{
      ▷ Ψ 0 [] acc ∗
      array_model t dq vs ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) acc -∗
        WP fn #i acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      array٠foldli fn acc t
    {{{
      acc
    , RET acc;
      array_model t dq vs ∗
      Ψ (length vs) vs acc
    }}}.
  Lemma array٠foldli𑁒spec' Ψ fn acc t dq vs :
    {{{
      ▷ Ψ 0 [] acc ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ i (take i vs) acc -∗
        WP fn #i acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      array٠foldli fn acc t
    {{{
      acc
    , RET acc;
      array_model t dq vs ∗
      Ψ (length vs) vs acc
    }}}.

  Lemma array٠foldl𑁒spec_atomic Ψ fn acc t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None acc ∗
      □ (
        ∀ i vs (o : option val) acc,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ i vs o acc -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v) acc
            )
        | Some v ⇒
            WP fn acc v {{ acc,
              ▷ Ψ (S i) (vs ++ [v]) None acc
            }}
        end
      )
    }}}
      array٠foldl fn acc t
    {{{
      vs acc
    , RET acc;
      ⌜length vs = sz⌝ ∗
      Ψ sz vs None acc
    }}}.
  Lemma array٠foldl𑁒spec Ψ fn acc t dq vs :
    {{{
      ▷ Ψ 0 [] acc ∗
      array_model t dq vs ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) acc -∗
        WP fn acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      array٠foldl fn acc t
    {{{
      acc
    , RET acc;
      array_model t dq vs ∗
      Ψ (length vs) vs acc
    }}}.
  Lemma array٠foldl𑁒spec' Ψ fn acc t dq vs :
    {{{
      ▷ Ψ 0 [] acc ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ i (take i vs) acc -∗
        WP fn acc v {{ acc,
          ▷ Ψ (S i) (take i vs ++ [v]) acc
        }}
      )
    }}}
      array٠foldl fn acc t
    {{{
      acc
    , RET acc;
      array_model t dq vs ∗
      Ψ (length vs) vs acc
    }}}.

  #[local] Lemma array٠foldri_aux𑁒spec sz vs Ψ fn t (i : Z) acc :
    ₊i + length vs = sz →
    {{{
      ▷ Ψ ₊i acc None vs ∗
      □ (
        ∀ i acc (o : option val) vs,
        ⌜(S i + length vs)%nat = sz⌝ -∗
        Ψ (S i) acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ (S i) acc (Some v) vs
            )
        | Some v ⇒
            WP fn #i v acc {{ acc,
              ▷ Ψ i acc None (v :: vs)
            }}
        end
      )
    }}}
      array٠foldri_aux fn t #i acc
    {{{
      acc vs'
    , RET acc;
      ⌜(length vs' + length vs)%nat = sz⌝ ∗
      Ψ 0 acc None (vs' ++ vs)
    }}}.
  Lemma array٠foldri𑁒spec_atomic Ψ fn t sz acc :
    {{{
      array_inv t sz ∗
      ▷ Ψ sz acc None [] ∗
      □ (
        ∀ i acc (o : option val) vs,
        ⌜(S i + length vs)%nat = sz⌝ -∗
        Ψ (S i) acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ (S i) acc (Some v) vs
            )
        | Some v ⇒
            WP fn #i v acc {{ acc,
              ▷ Ψ i acc None (v :: vs)
            }}
        end
      )
    }}}
      array٠foldri fn t acc
    {{{
      acc vs
    , RET acc;
      ⌜length vs = sz⌝ ∗
      Ψ 0 acc None vs
    }}}.
  Lemma array٠foldri𑁒spec Ψ fn t dq vs acc :
    {{{
      array_model t dq vs ∗
      ▷ Ψ (length vs) acc [] ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      array٠foldri fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs ∗
      array_model t dq vs
    }}}.
  Lemma array٠foldri𑁒spec' Ψ fn t dq vs acc :
    {{{
      array_model t dq vs ∗
      ▷ Ψ (length vs) acc [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      array٠foldri fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs ∗
      array_model t dq vs
    }}}.

  Lemma array٠foldr𑁒spec_atomic Ψ fn t sz acc :
    {{{
      array_inv t sz ∗
      ▷ Ψ sz acc None [] ∗
      □ (
        ∀ i acc (o : option val) vs,
        ⌜(S i + length vs)%nat = sz⌝ -∗
        Ψ (S i) acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ (S i) acc (Some v) vs
            )
        | Some v ⇒
            WP fn v acc {{ acc,
              ▷ Ψ i acc None (v :: vs)
            }}
        end
      )
    }}}
      array٠foldr fn t acc
    {{{
      acc vs
    , RET acc;
      ⌜length vs = sz⌝ ∗
      Ψ 0 acc None vs
    }}}.
  Lemma array٠foldr𑁒spec Ψ fn t dq vs acc :
    {{{
      array_model t dq vs ∗
      ▷ Ψ (length vs) acc [] ∗
      □ (
        ∀ i v acc,
        ⌜vs !! i = Some v⌝ -∗
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      array٠foldr fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs ∗
      array_model t dq vs
    }}}.
  Lemma array٠foldr𑁒spec' Ψ fn t dq vs acc :
    {{{
      array_model t dq vs ∗
      ▷ Ψ (length vs) acc [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ acc,
        Ψ (S i) acc (drop (S i) vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop (S i) vs)
        }}
      )
    }}}
      array٠foldr fn t acc
    {{{
      acc
    , RET acc;
      Ψ 0 acc vs ∗
      array_model t dq vs
    }}}.

  Lemma array٠unsafe_iteri_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs (o : option val),
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            WP fn #k v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S k) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      vs
    , RET ();
      ⌜length vs = ₊n⌝ ∗
      Ψ ₊n vs None
    }}}.
  Lemma array٠unsafe_iteri_slice𑁒spec Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠unsafe_iteri_slice𑁒spec' Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k (slice ₊i k vs) -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠unsafe_iteri_slice𑁒spec_disentangled Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.
  Lemma array٠unsafe_iteri_slice𑁒spec_disentangled' Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.

  Lemma array٠iteri_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs (o : option val),
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            WP fn #k v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S k) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      vs
    , RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      ⌜length vs = ₊n⌝ ∗
      Ψ ₊n vs None
    }}}.
  Lemma array٠iteri_slice𑁒spec Ψ fn t dq vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠iteri_slice𑁒spec' Ψ fn t dq vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k (slice ₊i k vs) -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠iteri_slice𑁒spec_disentangled Ψ fn t dq vs (i n : Z) :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.
  Lemma array٠iteri_slice𑁒spec_disentangled' Ψ fn t dq vs (i n : Z) :
    {{{
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn #k v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.

  Lemma array٠unsafe_iter_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs (o : option val),
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            WP fn v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S k) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      vs
    , RET ();
      ⌜length vs = ₊n⌝ ∗
      Ψ ₊n vs None
    }}}.
  Lemma array٠unsafe_iter_slice𑁒spec Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠unsafe_iter_slice𑁒spec' Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k (slice ₊i k vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠unsafe_iter_slice𑁒spec_disentangled Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.
  Lemma array٠unsafe_iter_slice𑁒spec_disentangled' Ψ fn t dq vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.

  Lemma array٠iter_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs (o : option val),
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            WP fn v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S k) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠iter_slice fn t #i #n
    {{{
      vs
    , RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      ⌜length vs = ₊n⌝ ∗
      Ψ ₊n vs None
    }}}.
  Lemma array٠iter_slice𑁒spec Ψ fn t dq vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠iter_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠iter_slice𑁒spec' Ψ fn t dq vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k (slice ₊i k vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S k) (slice ₊i k vs ++ [v])
        }}
      )
    }}}
      array٠iter_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      Ψ ₊n (slice ₊i ₊n vs)
    }}}.
  Lemma array٠iter_slice𑁒spec_disentangled Ψ fn t dq vs (i n : Z) :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠iter_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.
  Lemma array٠iter_slice𑁒spec_disentangled' Ψ fn t dq vs (i n : Z) :
    {{{
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ k v
        }}
      )
    }}}
      array٠iter_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        Ψ k v
      )
    }}}.

  Lemma array٠iteri𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ i vs (o : option val),
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ i vs o -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v)
            )
        | Some v ⇒
            WP fn #i v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S i) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠iteri fn t
    {{{
      vs
    , RET ();
      ⌜length vs = sz⌝ ∗
      Ψ sz vs None
    }}}.
  Lemma array٠iteri𑁒spec Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      array٠iteri fn t
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma array٠iteri𑁒spec' Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      array٠iteri fn t
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma array٠iteri𑁒spec_disentangled Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      array٠iteri fn t
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠iteri𑁒spec_disentangled' Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      array٠iteri fn t
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠iter𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ i vs (o : option val),
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ i vs o -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v)
            )
        | Some v ⇒
            WP fn v {{ res,
              ⌜res = ()%V⌝ ∗
              ▷ Ψ (S i) (vs ++ [v]) None
            }}
        end
      )
    }}}
      array٠iter fn t
    {{{
      vs
    , RET ();
      ⌜length vs = sz⌝ ∗
      Ψ sz vs None
    }}}.
  Lemma array٠iter𑁒spec Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      array٠iter fn t
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma array٠iter𑁒spec' Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (S i) (take i vs ++ [v])
        }}
      )
    }}}
      array٠iter fn t
    {{{
      RET ();
      array_model t dq vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma array٠iter𑁒spec_disentangled Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      array٠iter fn t
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠iter𑁒spec_disentangled' Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      array٠iter fn t
    {{{
      RET ();
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠unsafe_applyi_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ k vs (o : option (val + val × val)) ws,
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ k vs o ws -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn #k v {{ w,
              ▷ Ψ k vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t (₊i + k) w (
              ▷ Ψ (S k) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      vs ws
    , RET ();
      ⌜length vs = ₊n⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ ₊n vs None ws
    }}}.
  Lemma array٠unsafe_applyi_slice𑁒spec Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v ws,
        ⌜k = length ws⌝ -∗
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn #k v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠unsafe_applyi_slice𑁒spec' Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        ∀ ws,
        ⌜k = length ws⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn #k v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠unsafe_applyi_slice𑁒spec_disentangled Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn #k v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠unsafe_applyi_slice𑁒spec_disentangled' Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn #k v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠applyi_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ k vs (o : option (val + val × val)) ws,
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ k vs o ws -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn #k v {{ w,
              ▷ Ψ k vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t (₊i + k) w (
              ▷ Ψ (S k) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      vs ws
    , RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      ⌜length vs = ₊n⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ ₊n vs None ws
    }}}.
  Lemma array٠applyi_slice𑁒spec Ψ fn t vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v ws,
        ⌜k = length ws⌝ -∗
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn #k v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠applyi_slice𑁒spec' Ψ fn t vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        ∀ ws,
        ⌜k = length ws⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn #k v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠applyi_slice𑁒spec_disentangled Ψ fn t vs (i n : Z) :
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn #k v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠applyi_slice𑁒spec_disentangled' Ψ fn t vs (i n : Z) :
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn #k v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠unsafe_apply_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ k vs (o : option (val + val × val)) ws,
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ k vs o ws -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn v {{ w,
              ▷ Ψ k vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t (₊i + k) w (
              ▷ Ψ (S k) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      vs ws
    , RET ();
      ⌜length vs = ₊n⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ ₊n vs None ws
    }}}.
  Lemma array٠unsafe_apply_slice𑁒spec Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v ws,
        ⌜k = length ws⌝ -∗
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠unsafe_apply_slice𑁒spec' Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        ∀ ws,
        ⌜k = length ws⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠unsafe_apply_slice𑁒spec_disentangled Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠unsafe_apply_slice𑁒spec_disentangled' Ψ fn t vs (i n : Z) :
    (0 ≤ i ≤ length vs)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠apply_slice𑁒spec_atomic Ψ fn t (sz : nat) (i n : Z) :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ k vs (o : option (val + val × val)) ws,
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ k vs o ws -∗
        match o with
        | None ⇒
            au_load t (₊i + k) (λ v,
              ▷ Ψ k vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn v {{ w,
              ▷ Ψ k vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t (₊i + k) w (
              ▷ Ψ (S k) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠apply_slice fn t #i #n
    {{{
      vs ws
    , RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      ⌜length vs = ₊n⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ ₊n vs None ws
    }}}.
  Lemma array٠apply_slice𑁒spec Ψ fn t vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v ws,
        ⌜k = length ws⌝ -∗
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠apply_slice𑁒spec' Ψ fn t vs (i n : Z) :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        ∀ ws,
        ⌜k = length ws⌝ -∗
        Ψ k (slice ₊i k vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S k) (slice ₊i k vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      Ψ ₊n (slice ₊i ₊n vs) ws
    }}}.
  Lemma array٠apply_slice𑁒spec_disentangled Ψ fn t vs (i n : Z) :
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ k v,
        ⌜k < ₊n⌝ -∗
        ⌜vs !! (₊i + k)%nat = Some v⌝ -∗
        WP fn v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      ⌜length ws = ₊n⌝ ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠apply_slice𑁒spec_disentangled' Ψ fn t vs (i n : Z) :
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] k ↦ v ∈ slice ₊i ₊n vs,
        WP fn v {{ w,
          ▷ Ψ k w
        }}
      )
    }}}
      array٠apply_slice fn t #i #n
    {{{
      ws
    , RET ();
      ⌜0 ≤ i ≤ length vs⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t (DfracOwn 1) (with_slice ₊i ₊n vs ws) ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠applyi𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ i vs (o : option (val + val × val)) ws,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ i vs o ws -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn #i v {{ w,
              ▷ Ψ i vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t i w (
              ▷ Ψ (S i) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠applyi fn t
    {{{
      vs ws
    , RET ();
      ⌜length vs = sz⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ sz vs None ws
    }}}.
  Lemma array٠applyi𑁒spec Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ i v ws,
        ⌜i = length ws⌝ -∗
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠applyi fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠applyi𑁒spec' Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠applyi fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠applyi𑁒spec_disentangled Ψ fn t vs :
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ w,
          ▷ Ψ i w
        }}
      )
    }}}
      array٠applyi fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠applyi𑁒spec_disentangled' Ψ fn t vs :
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ w,
          ▷ Ψ i w
        }}
      )
    }}}
      array٠applyi fn t
    {{{
      ws
    , RET ();
      array_model t (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠apply𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ i vs (o : option (val + val × val)) ws,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ i vs o ws -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some $ inl v) ws
            )
        | Some (inl v) ⇒
            WP fn v {{ w,
              ▷ Ψ i vs (Some $ inr (v, w)) ws
            }}
        | Some (inr (v, w)) ⇒
            au_store t i w (
              ▷ Ψ (S i) (vs ++ [v]) None (ws ++ [w])
            )
        end
      )
    }}}
      array٠apply fn t
    {{{
      vs ws
    , RET ();
      ⌜length vs = sz⌝ ∗
      ⌜length vs = length ws⌝ ∗
      Ψ sz vs None ws
    }}}.
  Lemma array٠apply𑁒spec Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ i v ws,
        ⌜i = length ws⌝ -∗
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠apply fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠apply𑁒spec' Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠apply fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠apply𑁒spec_disentangled Ψ fn t vs :
    {{{
      array_model t (DfracOwn 1) vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ w,
          ▷ Ψ i w
        }}
      )
    }}}
      array٠apply fn t
    {{{
      ws
    , RET ();
      ⌜length vs = length ws⌝ ∗
      array_model t (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.
  Lemma array٠apply𑁒spec_disentangled' Ψ fn t vs :
    {{{
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ w,
          ▷ Ψ i w
        }}
      )
    }}}
      array٠apply fn t
    {{{
      ws
    , RET ();
      array_model t (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ w ∈ ws,
        Ψ i w
      )
    }}}.

  Lemma array٠unsafe_initi𑁒spec Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      □ (
        ∀ t i vs,
        ⌜i < ₊sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn #i {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠unsafe_initi𑁒spec' Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ t vs,
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn #i {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠unsafe_initi𑁒spec_disentangled_strong Χ Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Χ t
      ) ∗
      □ (
        ∀ t i,
        Χ t -∗
        ⌜i < ₊sz⌝ -∗
        WP fn #i {{ v,
          Χ t ∗
          ▷ Ψ t i v
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Χ t ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ t i v
      )
    }}}.
  Lemma array٠unsafe_initi𑁒spec_disentangled Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠unsafe_initi𑁒spec_disentangled_strong' Χ Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Χ t
      ) ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ t,
        Χ t -∗
        WP fn #i {{ v,
          Χ t ∗
          ▷ Ψ t i v
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Χ t ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ t i v
      )
    }}}.
  Lemma array٠unsafe_initi𑁒spec_disentangled' Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ( [∗ list] i ∈ seq 0 ₊sz,
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠initi𑁒spec Ψ sz fn :
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      □ (
        ∀ t i vs,
        ⌜i < ₊sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn #i {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠initi𑁒spec' Ψ sz fn :
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ t vs,
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn #i {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠initi𑁒spec_disentangled Ψ sz fn :
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠initi𑁒spec_disentangled' Ψ sz fn :
    {{{
      ( [∗ list] i ∈ seq 0 ₊sz,
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠unsafe_init𑁒spec Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      □ (
        ∀ t i vs,
        ⌜i < ₊sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn () {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠unsafe_init𑁒spec' Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ t vs,
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn () {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠unsafe_init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠unsafe_init𑁒spec_disentangled Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn () {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠unsafe_init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠unsafe_init𑁒spec_disentangled' Ψ sz fn :
    (0 ≤ sz)%Z →
    {{{
      ( [∗ list] i ∈ seq 0 ₊sz,
        WP fn () {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠unsafe_init #sz fn
    {{{
      t vs
    , RET t;
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠init𑁒spec Ψ sz fn :
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      □ (
        ∀ t i vs,
        ⌜i < ₊sz⌝ -∗
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn () {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠init𑁒spec' Ψ sz fn :
    {{{
      ▷ (
        ∀ t,
        |={⊤}=> Ψ t 0 []
      ) ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ t vs,
        ⌜i = length vs⌝ -∗
        Ψ t i vs -∗
        WP fn () {{ v,
          ▷ Ψ t (S i) (vs ++ [v])
        }}
      )
    }}}
      array٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      Ψ t ₊sz vs
    }}}.
  Lemma array٠init𑁒spec_disentangled Ψ sz fn :
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn () {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma array٠init𑁒spec_disentangled' Ψ sz fn :
    {{{
      ( [∗ list] i ∈ seq 0 ₊sz,
        WP fn () {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      array٠init #sz fn
    {{{
      t vs
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      ⌜length vs = ₊sz⌝ ∗
      array_model t (DfracOwn 1) vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma array٠mapi𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ i vs (o : option val) ws,
        ⌜i < sz⌝ -∗
        ⌜i = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ i vs o ws -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v) ws
            )
        | Some v ⇒
            WP fn #i v {{ w,
              ▷ Ψ (S i) (vs ++ [v]) None (ws ++ [w])
            }}
        end
      )
    }}}
      array٠mapi fn t
    {{{
      t' vs ws
    , RET t';
      ⌜length vs = sz⌝ ∗
      ⌜length vs = length ws⌝ ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ sz vs None ws
    }}}.
  Lemma array٠mapi𑁒spec Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t dq vs ∗
      □ (
        ∀ i v ws,
        ⌜vs !! i = Some v⌝ -∗
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠mapi𑁒spec' Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn #i v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠mapi𑁒spec_disentangled Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      array٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.
  Lemma array٠mapi𑁒spec_disentangled' Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      array٠mapi fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.

  Lemma array٠map𑁒spec_atomic Ψ fn t sz :
    {{{
      array_inv t sz ∗
      ▷ Ψ 0 [] None [] ∗
      □ (
        ∀ i vs (o : option val) ws,
        ⌜i < ₊sz⌝ -∗
        ⌜i = length vs⌝ -∗
        ⌜length vs = length ws⌝ -∗
        Ψ i vs o ws -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ i vs (Some v) ws
            )
        | Some v ⇒
            WP fn v {{ w,
              ▷ Ψ (S i) (vs ++ [v]) None (ws ++ [w])
            }}
        end
      )
    }}}
      array٠map fn t
    {{{
      t' vs ws
    , RET t';
      ⌜length vs = sz⌝ ∗
      ⌜length vs = length ws⌝ ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ sz vs None ws
    }}}.
  Lemma array٠map𑁒spec Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t dq vs ∗
      □ (
        ∀ i v ws,
        ⌜vs !! i = Some v⌝ -∗
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠map𑁒spec' Ψ fn t dq vs :
    {{{
      ▷ Ψ 0 [] [] ∗
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        ∀ ws,
        ⌜i = length ws⌝ -∗
        Ψ i (take i vs) ws -∗
        WP fn v {{ w,
          ▷ Ψ (S i) (take i vs ++ [v]) (ws ++ [w])
        }}
      )
    }}}
      array٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      Ψ (length vs) vs ws
    }}}.
  Lemma array٠map𑁒spec_disentangled Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      array٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.
  Lemma array٠map𑁒spec_disentangled' Ψ fn t dq vs :
    {{{
      array_model t dq vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ w,
          ▷ Ψ i v w
        }}
      )
    }}}
      array٠map fn t
    {{{
      t' ws
    , RET t';
      ⌜length ws = length vs⌝ ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) ws ∗
      ( [∗ list] i ↦ v; w ∈ vs; ws,
        Ψ i v w
      )
    }}}.

  Lemma array٠unsafe_copy_slice𑁒spec_atomic Ψ t1 (i1 : Z) t2 (i2 n : Z) :
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    (0 ≤ n)%Z →
    {{{
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs o,
        ⌜k < ₊n⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t1 (₊i1 + k) (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            au_store t2 (₊i2 + k) v (
              ▷ Ψ (S k) (vs ++ [v]) None
            )
        end
      )
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #i2 #n
    {{{
      vs
    , RET ();
      ⌜length vs = ₊n⌝ ∗
      Ψ ₊n vs None
    }}}.
  Lemma array٠unsafe_copy_slice𑁒spec_slice_fit t1 (i1 : Z) i1_ dq1 vs1 t2 (i2 : Z) i2_ vs2 (n : Z) :
    i1 = ⁺i1_ →
    i2 = ⁺i2_ →
    n = length vs1 →
    length vs1 = length vs2 →
    {{{
      array_slice t1 i1_ dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      array_slice t1 i1_ dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠unsafe_copy_slice𑁒spec_slice_fit_src t1 (i1 : Z) i1_ dq1 vs1 t2 i2 (j2 : Z) vs2 (n : Z) :
    i1 = ⁺i1_ →
    (i2 ≤ j2)%Z →
    n = length vs1 →
    (j2 + n ≤ i2 + length vs2)%Z →
    {{{
      array_slice t1 i1_ dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #j2 #n
    {{{
      RET ();
      array_slice t1 i1_ dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 vs1)
    }}}.
  Lemma array٠unsafe_copy_slice𑁒spec_slice_fit_dst t1 i1 (j1 : Z) dq1 vs1 t2 (i2 : Z) i2_ vs2 (n : Z) :
    (i1 ≤ j1)%Z →
    i2 = ⁺i2_ →
    n = length vs2 →
    (j1 + n ≤ i1 + length vs1)%Z →
    {{{
      array_slice t1 i1 dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy_slice t1 #j1 t2 #i2 #n
    {{{
      RET ();
      array_slice t1 i1 dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) (slice (₊j1 - i1) ₊n vs1)
    }}}.
  Lemma array٠unsafe_copy_slice𑁒spec_slice t1 i1 (j1 : Z) dq1 vs1 t2 i2 (j2 : Z) vs2 (n : Z) :
    (i1 ≤ j1)%Z →
    (i2 ≤ j2)%Z →
    (0 ≤ n)%Z →
    (j1 + n ≤ i1 + length vs1)%Z →
    (j2 + n ≤ i2 + length vs2)%Z →
    {{{
      array_slice t1 i1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy_slice t1 #j1 t2 #j2 #n
    {{{
      RET ();
      array_slice t1 i1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 (take ₊n (drop (₊j1 - i1) vs1)))
    }}}.
  Lemma array٠unsafe_copy_slice𑁒spec t1 (i1 : Z) dq1 vs1 t2 (i2 : Z) vs2 (n : Z) :
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    (0 ≤ n)%Z →
    (i1 + n ≤ length vs1)%Z →
    (i2 + n ≤ length vs2)%Z →
    {{{
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) (with_slice ₊i2 ₊n vs2 (take ₊n (drop ₊i1 vs1)))
    }}}.

  Lemma array٠copy_slice𑁒spec_slice_fit t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 (n : Z) :
    i1_ = ₊i1 →
    i2_ = ₊i2 →
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 ≤ i1⌝%Z -∗
        ⌜0 ≤ i2⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜i1 + n ≤ sz1⌝%Z -∗
        ⌜i2 + n ≤ sz2⌝%Z -∗
          ⌜₊n = length vs1⌝ ∗
          ⌜length vs1 = length vs2⌝ ∗
          array_slice t1 i1_ dq1 vs1 ∗
          array_slice t2 i2_ (DfracOwn 1) vs2
      )
    }}}
      array٠copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i1 + n ≤ sz1⌝%Z ∗
      ⌜i2 + n ≤ sz2⌝%Z ∗
      array_slice t1 i1_ dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠copy_slice𑁒spec_slice t1 sz1 i1 (j1 : Z) dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 (n : Z) :
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 ≤ j1⌝%Z -∗
        ⌜0 ≤ j2⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜j1 + n ≤ sz1⌝%Z -∗
        ⌜j2 + n ≤ sz2⌝%Z -∗
          ⌜i1 ≤ ₊j1⌝ ∗
          ⌜i2 ≤ ₊j2⌝ ∗
          ⌜₊j1 + n ≤ i1 + length vs1⌝%Z ∗
          ⌜₊j2 + n ≤ i2 + length vs2⌝%Z ∗
          array_slice t1 i1 dq1 vs1 ∗
          array_slice t2 i2 (DfracOwn 1) vs2
      )
    }}}
      array٠copy_slice t1 #j1 t2 #j2 #n
    {{{
      RET ();
      ⌜0 ≤ j1⌝%Z ∗
      ⌜0 ≤ j2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜j1 + n ≤ sz1⌝%Z ∗
      ⌜j2 + n ≤ sz2⌝%Z ∗
      array_slice t1 i1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 (take ₊n (drop (₊j1 - i1) vs1)))
    }}}.
  Lemma array٠copy_slice𑁒spec t1 (i1 : Z) dq1 vs1 t2 (i2 : Z) vs2 (n : Z) :
    {{{
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) vs2
    }}}
      array٠copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i1 + n ≤ length vs1⌝%Z ∗
      ⌜i2 + n ≤ length vs2⌝%Z ∗
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) (with_slice ₊i2 ₊n vs2 (take ₊n (drop ₊i1 vs1)))
    }}}.

  Lemma array٠unsafe_copy𑁒spec_atomic Ψ t1 sz1 t2 sz2 (i2 : Z) :
    (0 ≤ i2)%Z →
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ▷ Ψ 0 [] None ∗
      □ (
        ∀ k vs o,
        ⌜k < sz1⌝ -∗
        ⌜k = length vs⌝ -∗
        Ψ k vs o -∗
        match o with
        | None ⇒
            au_load t1 k (λ v,
              ▷ Ψ k vs (Some v)
            )
        | Some v ⇒
            au_store t2 (₊i2 + k) v (
              ▷ Ψ (S k) (vs ++ [v]) None
            )
        end
      )
    }}}
      array٠unsafe_copy t1 t2 #i2
    {{{
      vs
    , RET ();
      ⌜length vs = sz1⌝ ∗
      Ψ sz1 vs None
    }}}.
  Lemma array٠unsafe_copy𑁒spec_slice_fit t1 dq1 vs1 t2 (i2 : Z) i2_ vs2 :
    i2 = ⁺i2_ →
    length vs1 = length vs2 →
    {{{
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy t1 t2 #i2
    {{{
      RET ();
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠unsafe_copy𑁒spec_slice t1 dq1 vs1 t2 i2 (j2 : Z) vs2 :
    (i2 ≤ j2)%Z →
    (j2 + length vs1 ≤ i2 + length vs2)%Z →
    {{{
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy t1 t2 #j2
    {{{
      RET ();
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) (length vs1) vs2 vs1)
    }}}.
  Lemma array٠unsafe_copy𑁒spec t1 dq1 vs1 t2 (i2 : Z) vs2 :
    (0 ≤ i2)%Z →
    (i2 + length vs1 ≤ length vs2)%Z →
    {{{
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_copy t1 t2 #i2
    {{{
      RET ();
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) (with_slice ₊i2 (length vs1) vs2 vs1)
    }}}.

  Lemma array٠copy𑁒spec_slice_fit t1 dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 :
    i2_ = ₊i2 →
    {{{
      array_model t1 dq1 vs1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 ≤ i2⌝%Z -∗
        ⌜i2 + length vs1 ≤ sz2⌝%Z -∗
          ⌜length vs1 = length vs2⌝ ∗
          array_slice t2 i2_ (DfracOwn 1) vs2
      )
    }}}
      array٠copy t1 t2 #i2
    {{{
      RET ();
      ⌜0 ≤ i2⌝%Z ∗
      ⌜i2 + length vs1 ≤ sz2⌝%Z ∗
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠copy𑁒spec_slice t1 dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 :
    {{{
      array_model t1 dq1 vs1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 ≤ j2⌝%Z -∗
        ⌜j2 + length vs1 ≤ sz2⌝%Z -∗
          ⌜i2 ≤ j2⌝%Z ∗
          ⌜j2 + length vs1 ≤ i2 + length vs2⌝%Z ∗
          array_slice t2 i2 (DfracOwn 1) vs2
      )
    }}}
      array٠copy t1 t2 #j2
    {{{
      RET ();
      ⌜0 ≤ i2⌝ ∗
      ⌜i2 + length vs1 ≤ sz2⌝ ∗
      array_model t1 dq1 vs1 ∗
      array_slice t2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) (length vs1) vs2 vs1)
    }}}.
  Lemma array٠copy𑁒spec t1 dq1 vs1 t2 (i2 : Z) vs2 :
    {{{
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) vs2
    }}}
      array٠copy t1 t2 #i2
    {{{
      RET ();
      ⌜0 ≤ i2⌝%Z ∗
      ⌜i2 + length vs1 ≤ length vs2⌝%Z ∗
      array_model t1 dq1 vs1 ∗
      array_model t2 (DfracOwn 1) (with_slice ₊i2 (length vs1) vs2 vs1)
    }}}.

  Lemma array٠unsafe_grow𑁒spec t dq vs sz' v' :
    (length vs ≤ sz')%Z →
    {{{
      array_model t dq vs
    }}}
      array٠unsafe_grow t #sz' v'
    {{{
      t'
    , RET t';
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (vs ++ replicate (₊sz' - length vs) v')
    }}}.

  Lemma array٠grow𑁒spec t dq vs sz' v' :
    {{{
      array_model t dq vs
    }}}
      array٠grow t #sz' v'
    {{{
      t'
    , RET t';
      ⌜length vs ≤ sz'⌝%Z ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (vs ++ replicate (₊sz' - length vs) v')
    }}}.

  Lemma array٠unsafe_sub𑁒spec_slice_fit t dq vs (i : Z) i_ (n : Z) :
    i = ⁺i_ →
    n = length vs →
    {{{
      array_slice t i_ dq vs
    }}}
      array٠unsafe_sub t #i #n
    {{{
      t'
    , RET t';
      array_slice t i_ dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n vs)
    }}}.
  Lemma array٠unsafe_sub𑁒spec_slice t dq vs i (j n : Z) :
    (i ≤ j)%Z →
    (0 ≤ n)%Z →
    (j + n ≤ i + length vs)%Z →
    {{{
      array_slice t i dq vs
    }}}
      array٠unsafe_sub t #j #n
    {{{
      t'
    , RET t';
      array_slice t i dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n (drop (₊j - ₊i) vs))
    }}}.
  Lemma array٠unsafe_sub𑁒spec t dq vs (i n : Z) :
    (0 ≤ i)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ length vs)%Z →
    {{{
      array_model t dq vs
    }}}
      array٠unsafe_sub t #i #n
    {{{
      t'
    , RET t';
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n (drop ₊i vs))
    }}}.

  Lemma array٠sub𑁒spec_slice_fit t sz dq vs (i : Z) i_ (n : Z) :
    i_ = ₊i →
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ i⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜i + n ≤ sz⌝%Z -∗
          ⌜₊n = length vs⌝ ∗
          array_slice t i_ dq vs
      )
    }}}
      array٠sub t #i #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      array_slice t i_ dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n vs)
    }}}.
  Lemma array٠sub𑁒spec_slice t sz dq vs i (j n : Z) :
    {{{
      array_inv t sz ∗
      ( ⌜0 ≤ j⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜j + n ≤ sz⌝%Z -∗
          ⌜i ≤ ₊j⌝ ∗
          ⌜₊j + ₊n ≤ i + length vs⌝ ∗
          array_slice t i dq vs
      )
    }}}
      array٠sub t #j #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ j⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜j + n ≤ sz⌝%Z ∗
      array_slice t i dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n (drop (₊j - ₊i) vs))
    }}}.
  Lemma array٠sub𑁒spec t dq vs (i n : Z) :
    {{{
      array_model t dq vs
    }}}
      array٠sub t #i #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n (drop ₊i vs))
    }}}.

  Lemma array٠unsafe_shrink𑁒spec t dq vs (n : Z) :
    (0 ≤ n ≤ length vs)%Z →
    {{{
      array_model t dq vs
    }}}
      array٠unsafe_shrink t #n
    {{{
      t'
    , RET t';
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n vs)
    }}}.

  Lemma array٠shrink𑁒spec t dq vs (n : Z) :
    {{{
      array_model t dq vs
    }}}
      array٠shrink t #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ n ≤ length vs⌝%Z ∗
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) (take ₊n vs)
    }}}.

  Lemma array٠clone𑁒spec t dq vs :
    {{{
      array_model t dq vs
    }}}
      array٠clone t
    {{{
      t'
    , RET t';
      array_model t dq vs ∗
      array_model t' (DfracOwn 1) vs
    }}}.

  Lemma array٠unsafe_cget𑁒spec_atomic t (j : Z) :
    <<<
      True
    | ∀∀ sz i dq vs v,
      ⌜(i ≤ j)%Z⌝ ∗
      ⌜vs !! (₊j - i) = Some v⌝ ∗
      array_cslice t sz i dq vs
    >>>
      array٠unsafe_cget t #j
    <<<
      array_cslice t sz i dq vs
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_cget𑁒spec_atomic_weak t (i : Z) :
    (0 ≤ i)%Z →
    <<<
      True
    | ∀∀ sz j dq vs,
      array_cslice t sz j dq vs ∗
      ⌜0 < sz⌝ ∗
      ⌜length vs = sz⌝
    >>>
      array٠unsafe_cget t #i
    <<<
      array_cslice t sz j dq vs
    | v,
      RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_cget𑁒spec_atomic_cell t sz (i : Z) :
    <<<
      True
    | ∀∀ i_ dq v,
      ⌜i = ⁺i_⌝ ∗
      array_cslice t sz i_ dq [v]
    >>>
      array٠unsafe_cget t #i
    <<<
      array_cslice t sz i_ dq [v]
    | RET v;
      £ 1
    >>>.
  Lemma array٠unsafe_cget𑁒spec k v t sz i dq vs (j : Z) :
    (i ≤ j)%Z →
    vs !! k = Some v →
    k = ₊j - i →
    {{{
      array_cslice t sz i dq vs
    }}}
      array٠unsafe_cget t #j
    {{{
      RET v;
      array_cslice t sz i dq vs
    }}}.
  Lemma array٠unsafe_cget𑁒spec_cell t sz (i : Z) i_ dq v :
    i = ⁺i_ →
    {{{
      array_cslice t sz i_ dq [v]
    }}}
      array٠unsafe_cget t #i
    {{{
      RET v;
      array_cslice t sz i_ dq [v]
    }}}.
  Lemma array٠unsafe_cget𑁒spec_model v t dq vs (j : Z) :
    (0 ≤ j)%Z →
    vs !! (₊j `mod` length vs) = Some v →
    {{{
      array_model t dq vs
    }}}
      array٠unsafe_cget t #j
    {{{
      RET v;
      array_model t dq vs
    }}}.

  Lemma array٠cget𑁒spec_atomic t sz (j : Z) :
    <<<
      array_inv t sz
    | ∀∀ dq vs i v,
      ⌜0 ≤ j⌝%Z -∗
      ⌜0 < sz⌝%Z -∗
        ⌜i ≤ ₊j⌝ ∗
        ⌜vs !! (₊j - i) = Some v⌝ ∗
        array_cslice t sz i dq vs
    >>>
      array٠cget t #j
    <<<
      array_cslice t sz i dq vs
    | RET v;
      ⌜0 ≤ j⌝%Z ∗
      ⌜0 < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠cget𑁒spec_atomic_weak t sz (i : Z) :
    <<<
      array_inv t sz
    | ∀∀ j dq vs,
      array_cslice t sz j dq vs ∗
      ⌜length vs = sz⌝
    >>>
      array٠cget t #i
    <<<
      array_cslice t sz j dq vs
    | v,
      RET v;
      £ 1
    >>>.
  Lemma array٠cget𑁒spec_atomic_cell t sz (i : Z) i_ :
    i_ = ₊i →
    <<<
      array_inv t sz
    | ∀∀ dq v,
      ⌜0 ≤ i⌝%Z -∗
      ⌜0 < sz⌝%Z -∗
      array_cslice t sz i_ dq [v]
    >>>
      array٠cget t #i
    <<<
      array_cslice t sz i_ dq [v]
    | RET v;
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 < sz⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠cget𑁒spec k v t sz i dq vs (j : Z) :
    {{{
      array_inv t sz ∗
      ( ⌜0 < sz⌝ -∗
        ⌜0 ≤ j⌝%Z -∗
          ⌜i ≤ ₊j⌝ ∗
          ⌜vs !! k = Some v⌝ ∗
          ⌜k = ₊j - i⌝ ∗
          array_cslice t sz i dq vs
      )
    }}}
      array٠cget t #j
    {{{
      RET v;
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ j⌝%Z ∗
      array_cslice t sz i dq vs
    }}}.
  Lemma array٠cget𑁒spec_cell t sz (i : Z) i_ dq v :
    i_ = ₊i →
    {{{
      array_inv t sz ∗
      ( ⌜0 < sz⌝ -∗
        ⌜0 ≤ i⌝%Z -∗
        array_cslice t sz i_ dq [v]
      )
    }}}
      array٠cget t #i
    {{{
      RET v;
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ i⌝%Z ∗
      array_cslice t sz i_ dq [v]
    }}}.
  Lemma array٠cget𑁒spec_model v t dq vs (j : Z) :
    vs !! (₊j `mod` length vs) = Some v →
    {{{
      array_model t dq vs
    }}}
      array٠cget t #j
    {{{
      RET v;
      array_model t dq vs
    }}}.

  Lemma array٠unsafe_cset𑁒spec_atomic t (j : Z) v :
    <<<
      True
    | ∀∀ sz i vs,
      ⌜i ≤ j < i + length vs⌝%Z ∗
      array_cslice t sz i (DfracOwn 1) vs
    >>>
      array٠unsafe_cset t #j v
    <<<
      array_cslice t sz i (DfracOwn 1) (<[₊j - i := v]> vs)
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_cset𑁒spec_atomic_cell t sz (i : Z) v :
    <<<
      True
    | ∀∀ i_ w,
      ⌜i = ⁺i_⌝ ∗
      array_cslice t sz i_ (DfracOwn 1) [w]
    >>>
      array٠unsafe_cset t #i v
    <<<
      array_cslice t sz i_ (DfracOwn 1) [v]
    | RET ();
      £ 1
    >>>.
  Lemma array٠unsafe_cset𑁒spec t sz i vs (j : Z) v :
    (i ≤ j < i + length vs)%Z →
    {{{
      array_cslice t sz i (DfracOwn 1) vs
    }}}
      array٠unsafe_cset t #j v
    {{{
      RET ();
      array_cslice t sz i (DfracOwn 1) (<[₊j - i := v]> vs)
    }}}.
  Lemma array٠unsafe_cset𑁒spec_cell t sz (i : Z) i_ w v :
    i = ⁺i_ →
    {{{
      array_cslice t sz i_ (DfracOwn 1) [w]
    }}}
      array٠unsafe_cset t #i v
    {{{
      RET ();
      array_cslice t sz i_ (DfracOwn 1) [v]
    }}}.
  Lemma array٠unsafe_cset𑁒spec_model t vs (j : Z) v :
    0 < length vs →
    (0 ≤ j)%Z →
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠unsafe_cset t #j v
    {{{
      RET ();
      array_model t (DfracOwn 1) (<[₊j `mod` length vs := v]> vs)
    }}}.

  Lemma array٠cset𑁒spec_atomic t sz (j : Z) v :
    <<<
      array_inv t sz
    | ∀∀ vs i,
      ⌜0 < sz⌝ -∗
      ⌜0 ≤ j⌝%Z -∗
        ⌜i ≤ ₊j < i + length vs⌝ ∗
        array_cslice t sz i (DfracOwn 1) vs
    >>>
      array٠cset t #j v
    <<<
      array_cslice t sz i (DfracOwn 1) (<[₊j - i := v]> vs)
    | RET ();
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ j⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠cset𑁒spec_atomic_cell t sz (i : Z) i_ v :
    i_ = ₊i →
    <<<
      array_inv t sz
    | ∀∀ w,
      ⌜0 < sz⌝ -∗
      ⌜0 ≤ i⌝%Z -∗
      array_cslice t sz i_ (DfracOwn 1) [w]
    >>>
      array٠cset t #i v
    <<<
      array_cslice t sz i_ (DfracOwn 1) [v]
    | RET ();
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ i⌝%Z ∗
      £ 1
    >>>.
  Lemma array٠cset𑁒spec t sz i vs (j : Z) v :
    {{{
      array_inv t sz ∗
      ( ⌜0 < sz⌝ -∗
        ⌜0 ≤ j⌝%Z -∗
          ⌜i ≤ ₊j < i + length vs⌝ ∗
          array_cslice t sz i (DfracOwn 1) vs
      )
    }}}
      array٠cset t #j v
    {{{
      RET ();
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ j⌝%Z ∗
      array_cslice t sz i (DfracOwn 1) (<[₊j - i := v]> vs)
    }}}.
  Lemma array٠cset𑁒spec_cell t sz (i : Z) i_ w v :
    i_ = ₊i →
    {{{
      array_inv t sz ∗
      ( ⌜0 < sz⌝ -∗
        ⌜0 ≤ i⌝%Z -∗
        array_cslice t sz i_ (DfracOwn 1) [w]
      )
    }}}
      array٠cset t #i v
    {{{
      RET ();
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ i⌝%Z ∗
      array_cslice t sz i_ (DfracOwn 1) [v]
    }}}.
  Lemma array٠cset𑁒spec_model t vs (j : Z) v :
    {{{
      array_model t (DfracOwn 1) vs
    }}}
      array٠cset t #j v
    {{{
      RET ();
      array_model t (DfracOwn 1) (<[₊j `mod` length vs := v]> vs)
    }}}.

  #[local] Lemma array٠unsafe_ccopy_slice₀𑁒spec t1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 (n : Z) :
    0 < sz2 →
    i1 = ⁺i1_ →
    i2 = ⁺i2_ →
    n = length vs1 →
    length vs1 = length vs2 →
    {{{
      array_slice t1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy_slice₀ t1 #i1 t2 #i2 #n
    {{{
      RET ();
      array_slice t1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒spec_fit t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 (n : Z) :
    0 < sz1 →
    length vs1 ≤ sz1 →
    0 < sz2 →
    i1 = ⁺i1_ →
    i2 = ⁺i2_ →
    n = length vs1 →
    length vs1 = length vs2 →
    {{{
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒spec_fit_src t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 (n : Z) :
    0 < sz1 →
    length vs1 ≤ sz1 →
    0 < sz2 →
    i1 = ⁺i1_ →
    (i2 ≤ j2)%Z →
    n = length vs1 →
    (j2 + n ≤ i2 + length vs2)%Z →
    {{{
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy_slice t1 #i1 t2 #j2 #n
    {{{
      RET ();
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 vs1)
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒spec_fit_dst t1 sz1 i1 (j1 : Z) dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 (n : Z) :
    0 < sz1 →
    length vs1 ≤ sz1 →
    0 < sz2 →
    (i1 ≤ j1)%Z →
    i2 = ⁺i2_ →
    n = length vs2 →
    (j1 + n ≤ i1 + length vs1)%Z →
    {{{
      array_cslice t1 sz1 i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy_slice t1 #j1 t2 #i2 #n
    {{{
      RET ();
      array_cslice t1 sz1 i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) (slice (₊j1 - i1) ₊n vs1)
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒spec t1 sz1 i1 (j1 : Z) dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 (n : Z) :
    0 < sz1 →
    length vs1 ≤ sz1 →
    0 < sz2 →
    (i1 ≤ j1)%Z →
    (i2 ≤ j2)%Z →
    (0 ≤ n)%Z →
    (j1 + n ≤ i1 + length vs1)%Z →
    (j2 + n ≤ i2 + length vs2)%Z →
    {{{
      array_cslice t1 sz1 i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy_slice t1 #j1 t2 #j2 #n
    {{{
      RET ();
      array_cslice t1 sz1 i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 (take ₊n (drop (₊j1 - i1) vs1)))
    }}}.

  Lemma array٠ccopy_slice𑁒spec_fit t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 (n : Z) :
    i1_ = ₊i1 →
    i2_ = ₊i2 →
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 < sz1⌝ -∗
        ⌜0 < sz2⌝ -∗
        ⌜0 ≤ i1⌝%Z -∗
        ⌜0 ≤ i2⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜n ≤ sz1⌝%Z -∗
        ⌜n ≤ sz2⌝%Z -∗
          ⌜₊n = length vs1⌝ ∗
          ⌜length vs1 = length vs2⌝ ∗
          array_cslice t1 sz1 i1_ dq1 vs1 ∗
          array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
      )
    }}}
      array٠ccopy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜n ≤ sz1⌝%Z ∗
      ⌜n ≤ sz2⌝%Z ∗
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠ccopy_slice𑁒spec t1 sz1 i1 (j1 : Z) dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 (n : Z) :
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 < sz1⌝ -∗
        ⌜0 < sz2⌝ -∗
        ⌜0 ≤ j1⌝%Z -∗
        ⌜0 ≤ j2⌝%Z -∗
        ⌜0 ≤ n⌝%Z -∗
        ⌜n ≤ sz1⌝%Z -∗
        ⌜n ≤ sz2⌝%Z -∗
          ⌜length vs1 ≤ sz1⌝ ∗
          ⌜i1 ≤ ₊j1⌝ ∗
          ⌜i2 ≤ ₊j2⌝ ∗
          ⌜₊j1 + n ≤ i1 + length vs1⌝%Z ∗
          ⌜₊j2 + n ≤ i2 + length vs2⌝%Z ∗
          array_cslice t1 sz1 i1 dq1 vs1 ∗
          array_cslice t2 sz2 i2 (DfracOwn 1) vs2
      )
    }}}
      array٠ccopy_slice t1 #j1 t2 #j2 #n
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ j1⌝%Z ∗
      ⌜0 ≤ j2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜n ≤ sz1⌝%Z ∗
      ⌜n ≤ sz2⌝%Z ∗
      array_cslice t1 sz1 i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) ₊n vs2 (take ₊n (drop (₊j1 - i1) vs1)))
    }}}.

  Lemma array٠unsafe_ccopy𑁒spec_fit t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 :
    0 < sz1 →
    0 < sz2 →
    i1 = ⁺i1_ →
    i2 = ⁺i2_ →
    length vs1 = sz1 →
    length vs1 = length vs2 →
    {{{
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy t1 #i1 t2 #i2
    {{{
      RET ();
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠unsafe_ccopy𑁒spec t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 :
    0 < sz1 →
    0 < sz2 →
    i1 = ⁺i1_ →
    length vs1 = sz1 →
    (i2 ≤ j2)%Z →
    (j2 + length vs1 ≤ i2 + length vs2)%Z →
    {{{
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) vs2
    }}}
      array٠unsafe_ccopy t1 #i1 t2 #j2
    {{{
      RET ();
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) (length vs1) vs2 vs1)
    }}}.

  Lemma array٠ccopy𑁒spec_fit t1 sz1 (i1 : Z) i1_ dq1 vs1 t2 sz2 (i2 : Z) i2_ vs2 :
    i1_ = ₊i1 →
    i2_ = ₊i2 →
    length vs1 = sz1 →
    length vs1 = length vs2 →
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 < sz1⌝ -∗
        ⌜0 < sz2⌝ -∗
        ⌜0 ≤ i1⌝%Z -∗
        ⌜0 ≤ i2⌝%Z -∗
          array_cslice t1 sz1 i1_ dq1 vs1 ∗
          array_cslice t2 sz2 i2_ (DfracOwn 1) vs2
      )
    }}}
      array٠ccopy t1 #i1 t2 #i2
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z ∗
      array_cslice t1 sz1 i1_ dq1 vs1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs1
    }}}.
  Lemma array٠ccopy𑁒spec t1 sz1 (i1 : Z) dq1 vs1 t2 sz2 i2 (j2 : Z) vs2 :
    length vs1 = sz1 →
    {{{
      array_inv t1 sz1 ∗
      array_inv t2 sz2 ∗
      ( ⌜0 < sz1⌝ -∗
        ⌜0 < sz2⌝ -∗
        ⌜0 ≤ i1⌝%Z -∗
        ⌜0 ≤ j2⌝%Z -∗
          ⌜i2 ≤ ₊j2⌝%Z ∗
          ⌜₊j2 + length vs1 ≤ i2 + length vs2⌝%Z ∗
          array_cslice t1 sz1 ₊i1 dq1 vs1 ∗
          array_cslice t2 sz2 i2 (DfracOwn 1) vs2
      )
    }}}
      array٠ccopy t1 #i1 t2 #j2
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ j2⌝%Z ∗
      array_cslice t1 sz1 ₊i1 dq1 vs1 ∗
      array_cslice t2 sz2 i2 (DfracOwn 1) (with_slice (₊j2 - i2) (length vs1) vs2 vs1)
    }}}.

  Lemma array٠unsafe_cgrow_slice𑁒spec t sz (i : Z) i_ dq vs (n : Z) sz' v :
    0 < sz →
    length vs ≤ sz →
    i = ⁺i_ →
    n = ⁺(length vs) →
    (0 < sz')%Z →
    (n ≤ sz')%Z →
    {{{
      array_cslice t sz i_ dq vs
    }}}
      array٠unsafe_cgrow_slice t #i #n #sz' v
    {{{
      t'
    , RET t';
      array_cslice t sz i_ dq vs ∗
      array_cslice t' ₊sz' i_ (DfracOwn 1) (vs ++ replicate (₊sz' - ₊n) v)
    }}}.

  Lemma array٠unsafe_cgrow𑁒spec t (sz : nat) (i : Z) i_ dq vs sz' v :
    0 < sz →
    i = ⁺i_ →
    length vs = sz →
    (0 < sz')%Z →
    (sz ≤ sz')%Z →
    {{{
      array_cslice t sz i_ dq vs
    }}}
      array٠unsafe_cgrow t #i #sz' v
    {{{
      t'
    , RET t';
      array_cslice t sz i_ dq vs ∗
      array_cslice t' ₊sz' i_ (DfracOwn 1) (vs ++ replicate (₊sz' - sz) v)
    }}}.

  Lemma array٠unsafe_cshrink_slice𑁒spec_fit t sz (i : Z) i_ dq vs sz' :
    0 < sz →
    length vs ≤ sz →
    i = ⁺i_ →
    (0 < sz' ≤ length vs)%Z →
    {{{
      array_cslice t sz i_ dq vs
    }}}
      array٠unsafe_cshrink_slice t #i #sz'
    {{{
      t'
    , RET t';
      array_cslice t sz i_ dq vs ∗
      array_cslice t' ₊sz' i_ (DfracOwn 1) (take ₊sz' vs)
    }}}.
  Lemma array٠unsafe_cshrink_slice𑁒spec t sz i dq vs (j : Z) sz' :
    0 < sz →
    length vs ≤ sz →
    (i ≤ j)%Z →
    (0 < sz')%Z →
    (j + sz' ≤ i + length vs)%Z →
    {{{
      array_cslice t sz i dq vs
    }}}
      array٠unsafe_cshrink_slice t #j #sz'
    {{{
      t'
    , RET t';
      array_cslice t sz i dq vs ∗
      array_cslice t' ₊sz' ₊j (DfracOwn 1) (slice (₊j - i) ₊sz' vs)
    }}}.

  Definition itype_array τ `{!iType _ τ} (sz : nat) t : iProp Σ :=
    ∃ l,
    ⌜t = #l⌝ ∗
    l ↦ₕ Header 0 sz ∗
    itype_chunk τ sz l.
  #[global] Instance itype_array_itype τ `{!iType _ τ} sz :
    iType _ (itype_array τ sz).

  Lemma itype_array_intro τ `{!iType _ τ} t vs :
    array_model t (DfracOwn 1) vs -∗
    ([∗ list] v ∈ vs, τ v) ={⊤}=∗
    itype_array τ (length vs) t.
  Lemma itype_array_intro_slice τ `{!iType _ τ} t sz vs :
    length vs = sz →
    array_inv t sz -∗
    array_slice t 0 (DfracOwn 1) vs -∗
    ([∗ list] v ∈ vs, τ v) ={⊤}=∗
    itype_array τ sz t.
  Lemma itype_array_intro_cslice τ `{!iType _ τ} t sz i vs :
    0 < sz →
    length vs = sz →
    array_cslice t sz i (DfracOwn 1) vs -∗
    ([∗ list] v ∈ vs, τ v) ={⊤}=∗
    itype_array τ sz t.
  Lemma itype_array_to_inv τ `{!iType _ τ} sz t :
    itype_array τ sz t ⊢
    array_inv t sz.

  Lemma array٠create𑁒type τ `{!iType _ τ} :
    {{{
      True
    }}}
      array٠create ()
    {{{
      t
    , RET t;
      itype_array τ 0 t
    }}}.

  Lemma array٠size𑁒type τ `{!iType _ τ} t sz :
    {{{
      itype_array τ sz t
    }}}
      array٠size t
    {{{
      RET #sz;
      True
    }}}.

  Lemma array٠unsafe_get𑁒type τ `{!iType _ τ} t (sz : nat) (i : Z) :
    (0 ≤ i < sz)%Z →
    {{{
      itype_array τ sz t
    }}}
      array٠unsafe_get t #i
    {{{
      v
    , RET v;
      τ v
    }}}.

  Lemma array٠get𑁒type τ `{!iType _ τ} t sz (i : Z) :
    {{{
      itype_array τ sz t
    }}}
      array٠get t #i
    {{{
      v
    , RET v;
      ⌜0 ≤ i < sz⌝%Z ∗
      τ v
    }}}.

  Lemma array٠unsafe_set𑁒type τ `{!iType _ τ} t (sz : nat) (i : Z) v :
    (0 ≤ i < sz)%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_set t #i v
    {{{
      RET ();
      True
    }}}.

  Lemma array٠set𑁒type τ `{!iType _ τ} t sz (i : Z) v :
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠set t #i v
    {{{
      RET ();
      ⌜0 ≤ i < sz⌝%Z
    }}}.

  Lemma array٠unsafe_xchg𑁒type τ `{!iType _ τ} t (sz : nat) (i : Z) v :
    (0 ≤ i < sz)%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_xchg t #i v
    {{{
      w
    , RET w;
      τ w
    }}}.

  Lemma array٠unsafe_cas𑁒type τ `{!iType _ τ} t (sz : nat) (i : Z) v1 v2 :
    (0 ≤ i < sz)%Z →
    {{{
      itype_array τ sz t ∗
      τ v1 ∗
      τ v2
    }}}
      array٠unsafe_cas t #i v1 v2
    {{{
      b
    , RET #b;
      True
    }}}.

  Lemma array٠unsafe_fill_slice𑁒type τ `{!iType _ τ} t (sz : nat) (i n : Z) v :
    (0 ≤ i)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_fill_slice t #i #n v
    {{{
      RET ();
      True
    }}}.

  Lemma array٠fill_slice𑁒type τ `{!iType _ τ} t sz (i n : Z) v :
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠fill_slice t #i #n v
    {{{
      RET ();
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z
    }}}.

  Lemma array٠fill𑁒type τ `{!iType _ τ} t sz v :
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠fill t v
    {{{
      RET ();
      True
    }}}.

  Lemma array٠unsafe_make𑁒type τ `{!iType _ τ} sz v :
    (0 ≤ sz)%Z →
    {{{
      τ v
    }}}
      array٠unsafe_make #sz v
    {{{
      t
    , RET t;
      itype_array τ ₊sz t
    }}}.

  Lemma array٠make𑁒type τ `{!iType _ τ} sz v :
    {{{
      τ v
    }}}
      array٠make #sz v
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      itype_array τ ₊sz t
    }}}.

  Lemma array٠foldli𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn acc t sz :
    {{{
      itype_array τ sz t ∗
      υ acc ∗
      (itype_nat_upto sz --> υ --> τ --> υ)%T fn
    }}}
      array٠foldli fn acc t
    {{{
      acc'
    , RET acc';
      υ acc'
    }}}.

  Lemma array٠foldl𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn acc t sz :
    {{{
      itype_array τ sz t ∗
      υ acc ∗
      (υ --> τ --> υ)%T fn
    }}}
      array٠foldl fn acc t
    {{{
      acc'
    , RET acc';
      υ acc'
    }}}.

  Lemma array٠foldri𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn acc t sz :
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto sz --> τ --> υ --> υ)%T fn ∗
      υ acc
    }}}
      array٠foldri fn t acc
    {{{
      acc'
    , RET acc';
      υ acc'
    }}}.

  Lemma array٠foldr𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn t sz acc :
    {{{
      itype_array τ sz t ∗
      (τ --> υ --> υ)%T fn ∗
      υ acc
    }}}
      array٠foldr fn t acc
    {{{
      acc'
    , RET acc';
      υ acc'
    }}}.

  Lemma array٠unsafe_iteri_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto ₊n --> τ --> itype_unit)%T fn
    }}}
      array٠unsafe_iteri_slice fn t #i #n
    {{{
      RET ();
      True
    }}}.

  Lemma array٠iteri_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto ₊n --> τ --> itype_unit)%T fn
    }}}
      array٠iteri_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z
    }}}.

  Lemma array٠unsafe_iter_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t ∗
      (τ --> itype_unit)%T fn
    }}}
      array٠unsafe_iter_slice fn t #i #n
    {{{
      RET ();
      True
    }}}.

  Lemma array٠iter_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    {{{
      itype_array τ sz t ∗
      (τ --> itype_unit)%T fn
    }}}
      array٠iter_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z
    }}}.

  Lemma array٠iteri𑁒type τ `{!iType _ τ} fn t sz :
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto sz --> τ --> itype_unit)%T fn
    }}}
      array٠iteri fn t
    {{{
      RET ();
      True
    }}}.

  Lemma array٠iter𑁒type τ `{!iType _ τ} fn t sz :
    {{{
      itype_array τ sz t ∗
      (τ --> itype_unit)%T fn
    }}}
      array٠iter fn t
    {{{
      RET ();
      True
    }}}.

  Lemma array٠unsafe_applyi_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto ₊n --> τ --> τ)%T fn
    }}}
      array٠unsafe_applyi_slice fn t #i #n
    {{{
      RET ();
      True
    }}}.

  Lemma array٠applyi_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto ₊n --> τ --> τ)%T fn
    }}}
      array٠applyi_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z
    }}}.

  Lemma array٠unsafe_apply_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    (0 ≤ i ≤ sz)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t ∗
      (τ --> τ)%T fn
    }}}
      array٠unsafe_apply_slice fn t #i #n
    {{{
      RET ();
      True
    }}}.

  Lemma array٠apply_slice𑁒type τ `{!iType _ τ} fn t (sz : nat) (i n : Z) :
    {{{
      itype_array τ sz t ∗
      (τ --> τ)%T fn
    }}}
      array٠apply_slice fn t #i #n
    {{{
      RET ();
      ⌜0 ≤ i ≤ sz⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z
    }}}.

  Lemma array٠applyi𑁒type τ `{!iType _ τ} fn t sz :
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto sz --> τ --> τ)%T fn
    }}}
      array٠applyi fn t
    {{{
      RET ();
      True
    }}}.

  Lemma array٠apply𑁒type τ `{!iType _ τ} fn t sz :
    {{{
      itype_array τ sz t ∗
      (τ --> τ)%T fn
    }}}
      array٠apply fn t
    {{{
      RET ();
      True
    }}}.

  Lemma array٠unsafe_initi𑁒type τ `{!iType _ τ} sz sz_ fn :
    sz = ⁺sz_ →
    {{{
      (itype_nat_upto sz_ --> τ)%T fn
    }}}
      array٠unsafe_initi #sz fn
    {{{
      t
    , RET t;
      itype_array τ sz_ t
    }}}.

  Lemma array٠initi𑁒type τ `{!iType _ τ} sz fn :
    {{{
      (itype_nat_upto ₊sz --> τ)%T fn
    }}}
      array٠initi #sz fn
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      itype_array τ ₊sz t
    }}}.

  Lemma array٠unsafe_init𑁒type τ `{!iType _ τ} sz fn :
    (0 ≤ sz)%Z →
    {{{
      (itype_unit --> τ)%T fn
    }}}
      array٠unsafe_init #sz fn
    {{{
      t
    , RET t;
      itype_array τ ₊sz t
    }}}.

  Lemma array٠init𑁒type τ `{!iType _ τ} sz fn :
    {{{
      (itype_unit --> τ)%T fn
    }}}
      array٠init #sz fn
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      itype_array τ ₊sz t
    }}}.

  Lemma array٠mapi𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn t sz sz_ :
    sz_ = ⁺sz →
    {{{
      itype_array τ sz t ∗
      (itype_nat_upto sz --> τ --> υ)%T fn
    }}}
      array٠mapi fn t
    {{{
      t'
    , RET t';
      itype_array υ sz t'
    }}}.

  Lemma array٠map𑁒type τ `{!iType _ τ} υ `{!iType _ υ} fn t sz sz_ :
    sz_ = ⁺sz →
    {{{
      itype_array τ sz t ∗
      (τ --> υ)%T fn
    }}}
      array٠map fn t
    {{{
      t'
    , RET t';
      itype_array υ sz t'
    }}}.

  Lemma array٠unsafe_copy_slice𑁒type τ `{!iType _ τ} t1 (sz1 : nat) (i1 : Z) t2 (sz2 : nat) (i2 n : Z) :
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    (0 ≤ n)%Z →
    (i1 + n ≤ sz1)%Z →
    (i2 + n ≤ sz2)%Z →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      True
    }}}.
  Lemma array٠unsafe_copy_slice𑁒type' τ `{!iType _ τ} t1 (sz : nat) (i1 : Z) t2 (i2 : Z) i2_ vs (n : Z) :
    (0 ≤ i1)%Z →
    i2 = ⁺i2_ →
    n = length vs →
    (i1 + n ≤ sz)%Z →
    {{{
      itype_array τ sz t1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs
    }}}
      array٠unsafe_copy_slice t1 #i1 t2 #i2 #n
    {{{
      ws
    , RET ();
      ⌜length ws = length vs⌝ ∗
      array_slice t2 i2_ (DfracOwn 1) ws ∗
      [∗ list] w ∈ ws, τ w
    }}}.

  Lemma array٠copy_slice𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 n : Z) :
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠copy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i1 + n ≤ sz1⌝%Z ∗
      ⌜i2 + n ≤ sz2⌝%Z
    }}}.

  Lemma array٠unsafe_copy𑁒type τ `{!iType _ τ} t1 (sz1 : nat) t2 (sz2 : nat) (i2 : Z) :
    (0 ≤ i2)%Z →
    (i2 + sz1 ≤ sz2)%Z →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠unsafe_copy t1 t2 #i2
    {{{
      RET ();
      ⌜i2 + sz1 ≤ sz2⌝%Z
    }}}.
  Lemma array٠unsafe_copy𑁒type' τ `{!iType _ τ} t1 sz t2 (i2 : Z) i2_ vs :
    i2 = ⁺i2_ →
    sz = length vs →
    {{{
      itype_array τ sz t1 ∗
      array_slice t2 i2_ (DfracOwn 1) vs
    }}}
      array٠unsafe_copy t1 t2 #i2
    {{{
      ws
    , RET ();
      ⌜length ws = length vs⌝ ∗
      array_slice t2 i2_ (DfracOwn 1) ws ∗
      [∗ list] w ∈ ws, τ w
    }}}.

  Lemma array٠copy𑁒type τ `{!iType _ τ} t1 sz1 t2 sz2 (i2 : Z) :
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠copy t1 t2 #i2
    {{{
      RET ();
      ⌜0 ≤ i2⌝%Z ∗
      ⌜i2 + sz1 ≤ sz2⌝%Z
    }}}.

  Lemma array٠unsafe_grow𑁒type τ `{!iType _ τ} t (sz : nat) sz' v' :
    (sz ≤ sz')%Z →
    {{{
      itype_array τ sz t ∗
      τ v'
    }}}
      array٠unsafe_grow t #sz' v'
    {{{
      t'
    , RET t';
      itype_array τ ₊sz' t'
    }}}.

  Lemma array٠grow𑁒type τ `{!iType _ τ} t sz sz' v' :
    {{{
      itype_array τ sz t ∗
      τ v'
    }}}
      array٠grow t #sz' v'
    {{{
      t'
    , RET t';
      ⌜sz ≤ sz'⌝ ∗
      itype_array τ ₊sz' t'
    }}}.

  Lemma array٠unsafe_sub𑁒type τ `{!iType _ τ} t (sz : nat) (i n : Z) :
    (0 ≤ i)%Z →
    (0 ≤ n)%Z →
    (i + n ≤ sz)%Z →
    {{{
      itype_array τ sz t
    }}}
      array٠unsafe_sub t #i #n
    {{{
      t'
    , RET t';
      itype_array τ ₊n t'
    }}}.
  Lemma array٠sub𑁒type τ `{!iType _ τ} t sz (i n : Z) :
    {{{
      itype_array τ sz t
    }}}
      array٠sub t #i #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ i⌝%Z ∗
      ⌜0 ≤ n⌝%Z ∗
      ⌜i + n ≤ sz⌝%Z ∗
      itype_array τ ₊n t'
    }}}.

  Lemma array٠unsafe_shrink𑁒type τ `{!iType _ τ} t (sz : nat) (n : Z) :
    (0 ≤ n ≤ sz)%Z →
    {{{
      itype_array τ sz t
    }}}
      array٠unsafe_shrink t #n
    {{{
      t'
    , RET t';
      itype_array τ ₊n t'
    }}}.

  Lemma array٠shrink𑁒type τ `{!iType _ τ} t sz (n : Z) :
    {{{
      itype_array τ sz t
    }}}
      array٠shrink t #n
    {{{
      t'
    , RET t';
      ⌜0 ≤ n ≤ sz⌝%Z ∗
      itype_array τ ₊n t'
    }}}.

  Lemma array٠clone𑁒type τ `{!iType _ τ} t sz :
    {{{
      itype_array τ sz t
    }}}
      array٠clone t
    {{{
      t'
    , RET t';
      itype_array τ sz t'
    }}}.

  Lemma array٠unsafe_cget𑁒type τ `{!iType _ τ} t sz (i : Z) :
    0 < sz →
    (0 ≤ i)%Z →
    {{{
      itype_array τ sz t
    }}}
      array٠unsafe_cget t #i
    {{{
      v
    , RET v;
      τ v
    }}}.
  Lemma array٠cget𑁒type τ `{!iType _ τ} t sz (i : Z) :
    {{{
      itype_array τ sz t
    }}}
      array٠cget t #i
    {{{
      v
    , RET v;
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ i⌝%Z ∗
      τ v
    }}}.

  Lemma array٠unsafe_cset𑁒type τ `{!iType _ τ} t sz (i : Z) v :
    0 < sz →
    (0 ≤ i)%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_cset t #i v
    {{{
      RET ();
      True
    }}}.
  Lemma array٠cset𑁒type τ `{!iType _ τ} t sz (i : Z) v :
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠cset t #i v
    {{{
      RET ();
      ⌜0 < sz⌝ ∗
      ⌜0 ≤ i⌝%Z
    }}}.

  #[local] Lemma array٠unsafe_ccopy_slice₀𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 n : Z) :
    0 < sz1 →
    0 < sz2 →
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    (0 ≤ n)%Z →
    (i1 + n ≤ sz1)%Z →
    (n ≤ sz2)%Z →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠unsafe_ccopy_slice₀ t1 #i1 t2 #i2 #n
    {{{
      RET ();
      True
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 n : Z) :
    0 < sz1 →
    0 < sz2 →
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    (0 ≤ n)%Z →
    (n ≤ sz1)%Z →
    (n ≤ sz2)%Z →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠unsafe_ccopy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      True
    }}}.
  #[local] Lemma array٠unsafe_ccopy_slice₀𑁒type' τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 : Z) i2_ vs (n : Z) :
    0 < sz1 →
    0 < sz2 →
    length vs ≤ sz2 →
    (0 ≤ i1)%Z →
    (i1 + length vs ≤ sz1)%Z →
    i2 = ⁺i2_ →
    n = length vs →
    {{{
      itype_array τ sz1 t1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs
    }}}
      array٠unsafe_ccopy_slice₀ t1 #i1 t2 #i2 #n
    {{{
      ws
    , RET ();
      ⌜length ws = length vs⌝ ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) ws ∗
      [∗ list] w ∈ ws, τ w
    }}}.
  Lemma array٠unsafe_ccopy_slice𑁒type' τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 : Z) i2_ vs (n : Z) :
    0 < sz1 →
    length vs ≤ sz1 →
    0 < sz2 →
    length vs ≤ sz2 →
    (0 ≤ i1)%Z →
    i2 = ⁺i2_ →
    n = length vs →
    {{{
      itype_array τ sz1 t1 ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) vs
    }}}
      array٠unsafe_ccopy_slice t1 #i1 t2 #i2 #n
    {{{
      ws
    , RET ();
      ⌜length ws = length vs⌝ ∗
      array_cslice t2 sz2 i2_ (DfracOwn 1) ws ∗
      [∗ list] w ∈ ws, τ w
    }}}.

  Lemma array٠ccopy_slice𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 : Z) (n : Z) :
    0 < sz1 →
    0 < sz2 →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠ccopy_slice t1 #i1 t2 #i2 #n
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z
    }}}.

  Lemma array٠unsafe_ccopy𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 : Z) :
    0 < sz1 →
    0 < sz2 →
    sz1 ≤ sz2 →
    (0 ≤ i1)%Z →
    (0 ≤ i2)%Z →
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠unsafe_ccopy t1 #i1 t2 #i2
    {{{
      RET ();
      True
    }}}.

  Lemma array٠ccopy𑁒type τ `{!iType _ τ} t1 sz1 (i1 : Z) t2 sz2 (i2 : Z) :
    {{{
      itype_array τ sz1 t1 ∗
      itype_array τ sz2 t2
    }}}
      array٠ccopy t1 #i1 t2 #i2
    {{{
      RET ();
      ⌜0 < sz1⌝ ∗
      ⌜0 < sz2⌝ ∗
      ⌜0 ≤ i1⌝%Z ∗
      ⌜0 ≤ i2⌝%Z
    }}}.

  Lemma array٠unsafe_cgrow_slice𑁒type τ `{!iType _ τ} sz t (i n : Z) sz' v :
    0 < sz →
    (0 ≤ i)%Z →
    (0 ≤ n)%Z →
    (0 < sz')%Z →
    (n ≤ sz)%Z →
    (n ≤ sz')%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_cgrow_slice t #i #n #sz' v
    {{{
      t'
    , RET t';
      itype_array τ ₊sz' t'
    }}}.

  Lemma array٠unsafe_cgrow𑁒type τ `{!iType _ τ} sz t (i n : Z) sz' v :
    0 < sz →
    (0 ≤ i)%Z →
    (0 < sz')%Z →
    (sz ≤ sz')%Z →
    {{{
      itype_array τ sz t ∗
      τ v
    }}}
      array٠unsafe_cgrow t #i #sz' v
    {{{
      t'
    , RET t';
      itype_array τ ₊sz' t'
    }}}.

  Lemma array٠unsafe_cshrink_slice𑁒type τ `{!iType _ τ} sz t (i : Z) sz' :
    0 < sz →
    (0 ≤ i)%Z →
    (0 < sz')%Z →
    (sz' ≤ sz)%Z →
    {{{
      itype_array τ sz t
    }}}
      array٠unsafe_cshrink_slice t #i #sz'
    {{{
      t'
    , RET t';
      itype_array τ ₊sz' t'
    }}}.
End zoo_G.

From zoo_std Require
  array__opaque.
#[global] Opaque array٠unsafe_xchg.
#[global] Opaque array٠unsafe_cas.
#[global] Opaque array٠unsafe_faa.

#[global] Opaque array_inv.
#[global] Opaque array_slice.
#[global] Opaque array_model.
#[global] Opaque array_cslice.
#[global] Opaque itype_array.