Library zoo_std.array

Require Import Stdlib.micromega.ZifyNat.

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.common.math.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo_std.chunk.
Require Export zoo_std.array__code.
Require Import zoo_std.array__types.
Require Import zoo.options.

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

Definition array٠unsafe_xchg : val :=
  𝗳𝘂𝗻 "t" "i" "v" →
    Xchg ("t", "i") "v".

Definition array٠unsafe_cas : val :=
  𝗳𝘂𝗻 "t" "i" "v1" "v2" →
    CAS ("t", "i") "v1" "v2".

Definition array٠unsafe_faa : val :=
  𝗳𝘂𝗻 "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₁ 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₁' {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₂ {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ｰappｰ3 {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ｰappｰ3₁ 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ｰappｰ3₂ {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 ˖i dq vs.
    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 ˖i dq vs.
    Lemma array۰sliceｰcons₂ t i dq v vs :
      array۰slice t i dq [v] -∗
      array۰slice t ˖i dq vs -∗
      array۰slice t i dq (v :: vs).
    Lemma array۰sliceｰcons₂' t i1 dq v i2 vs :
      i2 = ˖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_fractional 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₁ 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₂ {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ｰappｰ3 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ｰappｰ3₁ 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ｰappｰ3₂ {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 ˖i dq vs.
    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 ˖i dq vs.
    Lemma array۰csliceｰcons₂ t sz i dq v vs :
      array۰cslice t sz i dq [v] -∗
      array۰cslice t sz ˖i dq vs -∗
      array۰cslice t sz i dq (v :: vs).
    Lemma array۰csliceｰcons₂' t sz i1 dq v i2 vs :
      i2 = ˖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₁ {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₁' {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₁ {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₁' {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₁ 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₁' {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₁ 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₁' {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 (
          ▷ Ψ ˖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,
              ▷ Ψ ˖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,
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
        ⌜(˖i + length vs)%nat = sz⌝ -∗
        Ψ ˖i acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ ˖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,
        ⌜(˖i + length vs)%nat = sz⌝ -∗
        Ψ ˖i acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ ˖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⌝ -∗
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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,
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn #i v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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,
        ⌜(˖i + length vs)%nat = sz⌝ -∗
        Ψ ˖i acc o vs -∗
        match o with
        | None ⇒
            au_load t i (λ v,
              ▷ Ψ ˖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⌝ -∗
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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,
        Ψ ˖i acc (drop ˖i vs) -∗
        WP fn v acc {{ acc,
          ▷ Ψ i acc (v :: drop ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
              ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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⌝ ∗
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 ˖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 ˖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 ˖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 ˖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 ˖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 ˖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 ˖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 ˖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,
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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,
              ▷ Ψ ˖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,
          ▷ Ψ ˖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,
          ▷ Ψ ˖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 (
              ▷ Ψ ˖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 (
              ▷ Ψ ˖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.

Require zoo_std.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.