Library zoo_std.dynarray_2

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Export zoo_std.dynarray_2__code.
Require Import zoo_std.dynarray_2__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type i : nat.
Implicit Type l elem : location.
Implicit Type elems : list location.
Implicit Type v t data slot fn : val.
Implicit Type vs slots : list val.

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  #[local] Definition element۰model elem v : iProp Σ :=
    elem ↦ₕ Header 1 §Element ∗
    elem.[value] ↦ v.
  #[local] Instance : CustomIpat "element۰model" :=
    " ( Helem_header & Helem_value ) ".
  Definition dynarray_2۰model t vs : iProp Σ :=
    ∃ l data elems extra,
    ⌜t = #l⌝ ∗
    l.[size] ↦ #(length vs) ∗
    l.[data] ↦ data ∗
    array۰model data (DfracOwn 1) ((#*@{location} elems) ++ replicate extra §Empty%V) ∗
    [∗ list] elem; v ∈ elems; vs, element۰model elem v.
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %data & %elems & %extra & -> & Hl_size & Hl_data & Hmodel & Helems ) ".

  #[global] Instance dynarray_2۰modelｰtimeless t vs :
    Timeless (dynarray_2۰model t vs).

  #[local] Lemma dynarray_2٠elementｰspec v :
    {{{
      True
    }}}
      dynarray_2٠element v
    {{{
      elem
    , RET #elem;
      element۰model elem v
    }}}.

  Lemma dynarray_2٠createｰspec' :
    {{{
      True
    }}}
      dynarray_2٠create ()
    {{{
      l
    , RET #l;
      dynarray_2۰model #l [] ∗
      meta_token l (↑nroot.@"user")
    }}}.
  Lemma dynarray_2٠createｰspec :
    {{{
      True
    }}}
      dynarray_2٠create ()
    {{{
      t
    , RET t;
      dynarray_2۰model t []
    }}}.

  Lemma dynarray_2٠makeｰspec sz v :
    {{{
      True
    }}}
      dynarray_2٠make #sz v
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      dynarray_2۰model t (replicate ₊sz v)
    }}}.
  Lemma dynarray_2٠initiｰspec Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      □ (
        ∀ i vs,
        ⌜i < ₊sz ∧ i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn #i {{ v,
          ▷ Ψ ˖i (vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜sz = length vs⌝ ∗
      dynarray_2۰model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma dynarray_2٠initiｰspec' Ψ sz fn :
    {{{
      ▷ Ψ 0 [] ∗
      ( [∗ list] i ∈ seq 0 ₊sz,
        ∀ vs,
        ⌜i = length vs⌝ -∗
        Ψ i vs -∗
        WP fn #i {{ v,
          ▷ Ψ ˖i (vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜sz = length vs⌝ ∗
      dynarray_2۰model t vs ∗
      Ψ ₊sz vs
    }}}.
  Lemma dynarray_2٠initiｰspecｰdisentangled Ψ sz fn :
    {{{
      □ (
        ∀ i,
        ⌜i < ₊sz⌝ -∗
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜sz = length vs⌝ ∗
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma dynarray_2٠initiｰspecｰdisentangled' Ψ sz fn :
    {{{
      ( [∗ list] i ∈ seq 0 ₊sz,
        WP fn #i {{ v,
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠initi #sz fn
    {{{
      t vs
    , RET t;
      ⌜sz = length vs⌝ ∗
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma dynarray_2٠sizeｰspec t vs :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠size t
    {{{
      RET #(length vs);
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠capacityｰspec t vs :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠capacity t
    {{{
      cap
    , RET #cap;
      ⌜length vs ≤ cap⌝ ∗
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠is_emptyｰspec t vs :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠getｰspec t vs (i : Z) v :
    (0 ≤ i)%Z →
    vs !! ₊i = Some v →
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠get t #i
    {{{
      RET v;
      ⌜0 ≤ i < length vs⌝%Z ∗
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠setｰspec t vs (i : Z) v :
    (0 ≤ i < length vs)%Z →
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠set t #i v
    {{{
      RET ();
      ⌜0 ≤ i < length vs⌝%Z ∗
      dynarray_2۰model t (<[₊i := v]> vs)
    }}}.

  #[local] Lemma dynarray_2٠next_capacityｰspec n :
    (0 ≤ n)%Z →
    {{{
      True
    }}}
      dynarray_2٠next_capacity #n
    {{{
      m
    , RET #m;
      ⌜n ≤ m⌝%Z
    }}}.
  Lemma dynarray_2٠reserveｰspec t vs (n : Z) :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠reserve t #n
    {{{
      RET ();
      ⌜0 ≤ n⌝%Z ∗
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠reserve_extraｰspec t vs (n : Z) :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠reserve_extra t #n
    {{{
      RET ();
      ⌜0 ≤ n⌝%Z ∗
      dynarray_2۰model t vs
    }}}.

  #[local] Lemma dynarray_2٠try_growｰspec t vs sz v :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠try_grow t #sz v
    {{{
      b
    , RET #b;
      if b then
        dynarray_2۰model t (vs ++ replicate (₊sz - length vs) v)
      else
        dynarray_2۰model t vs
    }}}.
  #[local] Lemma dynarray_2٠grow₁ｰspec t vs sz v :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠grow₁ t #sz v
    {{{
      RET ();
      dynarray_2۰model t (vs ++ replicate (₊sz - length vs) v)
    }}}.
  Lemma dynarray_2٠growｰspec t vs sz v :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠grow t #sz v
    {{{
      RET ();
      dynarray_2۰model t (vs ++ replicate (₊sz - length vs) v)
    }}}.

  #[local] Lemma dynarray_2٠try_pushｰspec t vs elem v :
    {{{
      dynarray_2۰model t vs ∗
      element۰model elem v
    }}}
      dynarray_2٠try_push t #elem
    {{{
      b
    , RET #b;
      if b then
        dynarray_2۰model t (vs ++ [v])
      else
        dynarray_2۰model t vs ∗
        element۰model elem v
    }}}.
  #[local] Lemma dynarray_2٠push₁ｰspec t vs elem v :
    {{{
      dynarray_2۰model t vs ∗
      element۰model elem v
    }}}
      dynarray_2٠push₁ t #elem
    {{{
      RET ();
      dynarray_2۰model t (vs ++ [v])
    }}}.
  Lemma dynarray_2٠pushｰspec t vs v :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠push t v
    {{{
      RET ();
      dynarray_2۰model t (vs ++ [v])
    }}}.

  Lemma dynarray_2٠popｰspec {t vs} vs' v :
    vs = vs' ++ [v] →
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠pop t
    {{{
      RET v;
      dynarray_2۰model t vs'
    }}}.

  Lemma dynarray_2٠fit_capacityｰspec t vs :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠fit_capacity t
    {{{
      RET ();
      dynarray_2۰model t vs
    }}}.

  Lemma dynarray_2٠resetｰspec t vs :
    {{{
      dynarray_2۰model t vs
    }}}
      dynarray_2٠reset t
    {{{
      RET ();
      dynarray_2۰model t []
    }}}.

  Lemma dynarray_2٠iteriｰspec Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_2۰model t vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ ˖i (take i vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠iteri fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_2٠iteriｰspec' Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ ˖i (take i vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠iteri fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_2٠iteriｰspecｰdisentangled Ψ fn t vs :
    {{{
      dynarray_2۰model t vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠iteri fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma dynarray_2٠iteriｰspecｰdisentangled' Ψ fn t vs :
    {{{
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn #i v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠iteri fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Lemma dynarray_2٠iterｰspec Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_2۰model t vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ ˖i (take i vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠iter fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_2٠iterｰspec' Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ ˖i (take i vs ++ [v])
        }}
      )
    }}}
      dynarray_2٠iter fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_2٠iterｰspecｰdisentangled Ψ fn t vs :
    {{{
      dynarray_2۰model t vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠iter fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma dynarray_2٠iterｰspecｰdisentangled' Ψ fn t vs :
    {{{
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_2٠iter fn t
    {{{
      RET ();
      dynarray_2۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.

  Context τ `{!iType (iPropI Σ) τ}.

  #[local] Definition itype۰element elem : iProp Σ :=
    elem ↦ₕ Header 1 §Element ∗
    inv nroot (
      ∃ v,
      elem.[value] ↦ v ∗
      τ v
    ).

  Lemma element_getｰtype elem :
    {{{
      itype۰element elem
    }}}
      (#elem).{value}
    {{{
      v
    , RET v;
      τ v
    }}}.

  Lemma element_setｰtype elem v :
    {{{
      itype۰element elem ∗
      τ v
    }}}
      #elem <-{value} v
    {{{
      RET ();
      True
    }}}.

  #[local] Definition itype۰slot slot : iProp Σ :=
      ⌜slot = §Empty%V⌝
    ∨ ∃ elem,
      ⌜slot = #elem⌝ ∗
      itype۰element elem.
  #[local] Instance itype۰slotｰitype :
    iType _ itype۰slot.

  #[local] Lemma wpｰmatchｰslot slot e1 x e2 Φ :
    itype۰slot slot -∗
    ( WP e1 {{ Φ }} ∧
      ∀ elem, itype۰element elem -∗ WP subst' x #elem e2 {{ Φ }}
    ) -∗
    WP 𝗺𝗮𝘁𝗰𝗵 slot 𝘄𝗶𝘁𝗵 Empty → e1 | Element ⎽ 𝗮𝘀: x → e2 𝗲𝗻𝗱 {{ Φ }}.

  Definition itype۰dynarray_2 t : iProp Σ :=
    ∃ l,
    ⌜t = #l⌝ ∗
    inv nroot (
      ∃ (sz : nat) cap data,
      l.[size] ↦ #sz ∗
      l.[data] ↦ data ∗ itype۰array itype۰slot cap data
    ).
  #[global] Instance itype۰dynarray_2ｰitype :
    iType _ itype۰dynarray_2.

  #[local] Lemma dynarray_2٠elementｰtype v :
    {{{
      τ v
    }}}
      dynarray_2٠element v
    {{{
      slot
    , RET slot;
      itype۰slot slot
    }}}.

  Lemma dynarray_2٠createｰtype :
    {{{
      True
    }}}
      dynarray_2٠create ()
    {{{
      t
    , RET t;
      itype۰dynarray_2 t
    }}}.

  Lemma dynarray_2٠makeｰtype (sz : Z) v :
    {{{
      τ v
    }}}
      dynarray_2٠make #sz v
    {{{
      t
    , RET t;
      ⌜0 ≤ sz⌝%Z ∗
      itype۰dynarray_2 t
    }}}.

  Lemma dynarray_2٠initiｰtype sz fn :
    {{{
      (itype۰nat_upto ₊sz --> τ)%T fn
    }}}
      dynarray_2٠initi #sz fn
    {{{
      t
    , RET t;
      itype۰dynarray_2 t
    }}}.

  Lemma dynarray_2٠sizeｰtype t :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠size t
    {{{
      (sz : nat)
    , RET #sz;
      True
    }}}.

  Lemma dynarray_2٠capacityｰtype t :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠size t
    {{{
      (cap : nat)
    , RET #cap;
      True
    }}}.

  #[local] Lemma dynarray_2٠dataｰtype t :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠data t
    {{{
      cap data
    , RET data;
      itype۰array itype۰slot cap data
    }}}.

  #[local] Lemma dynarray_2٠set_sizeｰtype t sz :
    (0 ≤ sz)%Z →
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠set_size t #sz
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma dynarray_2٠set_dataｰtype t cap data :
    {{{
      itype۰dynarray_2 t ∗
      itype۰array itype۰slot cap data
    }}}
      dynarray_2٠set_data t data
    {{{
      RET ();
      True
    }}}.

  Lemma dynarray_2٠is_emptyｰtype t :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠is_empty t
    {{{
      b
    , RET #b;
      True
    }}}.

  Lemma dynarray_2٠getｰtype t (i : Z) :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠get t #i
    {{{
      v
    , RET v;
      ⌜0 ≤ i⌝%Z ∗
      τ v
    }}}.

  Lemma dynarray_2٠setｰtype t (i : Z) v :
    {{{
      itype۰dynarray_2 t ∗
      τ v
    }}}
      dynarray_2٠set t #i v
    {{{
      RET ();
      ⌜0 ≤ i⌝%Z
    }}}.

  Lemma dynarray_2٠reserveｰtype t n :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠reserve t #n
    {{{
      RET ();
      ⌜0 ≤ n⌝%Z
    }}}.
  Lemma dynarray_2٠reserve_extraｰtype t n :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠reserve_extra t #n
    {{{
      RET ();
      ⌜0 ≤ n⌝%Z
    }}}.

  #[local] Lemma dynarray_2٠try_growｰtype t (sz' : Z) v :
    {{{
      itype۰dynarray_2 t ∗
      τ v
    }}}
      dynarray_2٠try_grow t #sz' v
    {{{
      b
    , RET #b;
      True
    }}}.
  #[local] Lemma dynarray_2٠grow₁ｰtype t (sz' : Z) v :
    {{{
      itype۰dynarray_2 t ∗
      τ v
    }}}
      dynarray_2٠grow₁ t #sz' v
    {{{
      RET ();
      True
    }}}.
  #[local] Lemma dynarray_2٠growｰtype t (sz' : Z) v :
    {{{
      itype۰dynarray_2 t ∗
      τ v
    }}}
      dynarray_2٠grow t #sz' v
    {{{
      RET ();
      True
    }}}.

  #[local] Lemma dynarray_2٠try_pushｰtype t slot :
    {{{
      itype۰dynarray_2 t ∗
      itype۰slot slot
    }}}
      dynarray_2٠try_push t slot
    {{{
      b
    , RET #b;
      True
    }}}.
  #[local] Lemma dynarray_2٠push₁ｰtype t slot :
    {{{
      itype۰dynarray_2 t ∗
      itype۰slot slot
    }}}
      dynarray_2٠push₁ t slot
    {{{
      RET ();
      True
    }}}.
  Lemma dynarray_2٠pushｰtype t v :
    {{{
      itype۰dynarray_2 t ∗
      τ v
    }}}
      dynarray_2٠push t v
    {{{
      RET ();
      True
    }}}.

  Lemma dynarray_2٠popｰtype t :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠pop t
    {{{
      v
    , RET v;
      τ v
    }}}.

  Lemma dynarray_2٠fit_capacityｰtype t v :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠fit_capacity t
    {{{
      RET ();
      True
    }}}.

  Lemma dynarray_2٠resetｰtype t v :
    {{{
      itype۰dynarray_2 t
    }}}
      dynarray_2٠reset t
    {{{
      RET ();
      True
    }}}.

  Lemma dynarray_2٠iteriｰtype fn t :
    {{{
      itype۰dynarray_2 t ∗
      (itype۰nat --> τ --> itype۰unit)%T fn
    }}}
      dynarray_2٠iteri fn t
    {{{
      RET ();
      True
    }}}.

  Lemma dynarray_2٠iterｰtype fn t :
    {{{
      itype۰dynarray_2 t ∗
      (τ --> itype۰unit)%T fn
    }}}
      dynarray_2٠iter fn t
    {{{
      RET ();
      True
    }}}.
End zoo۰G.

Require zoo_std.dynarray_2__opaque.

#[global] Opaque dynarray_2۰model.
#[global] Opaque itype۰dynarray_2.