Library zoo_std.dynarray_1

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.dynarray_1__code.
Require Import zoo_std.dynarray_1__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type i : nat.
Implicit Type l : location.
Implicit Type v t fn : val.
Implicit Type vs : list val.

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

  #[local] Definition model' t vs extra : iProp Σ :=
    ∃ l data,
    ⌜t = #l⌝ ∗
    l.[size] ↦ #(length vs) ∗
    l.[data] ↦ data ∗
    array۰model data (DfracOwn 1) (vs ++ replicate extra ()%V).
  #[local] Instance : CustomIpat "model'" :=
    " ( %l{} & %data{} & -> & Hl{}_size & Hl{}_data & Hmodel ) ".
  Definition dynarray_1۰model t vs : iProp Σ :=
    ∃ extra,
    model' t vs extra.
  #[local] Instance : CustomIpat "model" :=
    " ( %extra & {{lazy}Hmodel;(:model')} ) ".

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

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

  Lemma dynarray_1٠makeｰspec sz v :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      dynarray_1٠make #sz v
    {{{
      t
    , RET t;
      dynarray_1۰model t (replicate ₊sz v)
    }}}.

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

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

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

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

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

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

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

  #[local] Lemma dynarray_1٠reserve_extraｰspec' t vs n :
    (0 ≤ n)%Z →
    {{{
      dynarray_1۰model t vs
    }}}
      dynarray_1٠reserve_extra t #n
    {{{
      extra
    , RET ();
      ⌜₊n ≤ extra⌝ ∗
      model' t vs extra
    }}}.
  Lemma dynarray_1٠reserve_extraｰspec t vs n :
    (0 ≤ n)%Z →
    {{{
      dynarray_1۰model t vs
    }}}
      dynarray_1٠reserve_extra t #n
    {{{
      RET ();
      dynarray_1۰model t vs
    }}}.

  Lemma dynarray_1٠growｰspec t vs sz v :
    (0 ≤ sz)%Z →
    {{{
      dynarray_1۰model t vs
    }}}
      dynarray_1٠grow t #sz v
    {{{
      RET ();
      dynarray_1۰model t (vs ++ replicate (₊sz - length vs) v)
    }}}.

  Lemma dynarray_1٠pushｰspec t vs v :
    {{{
      dynarray_1۰model t vs
    }}}
      dynarray_1٠push t v
    {{{
      RET ();
      dynarray_1۰model t (vs ++ [v])
    }}}.

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

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

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

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

  Lemma dynarray_1٠iterｰspec Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_1۰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_1٠iter fn t
    {{{
      RET ();
      dynarray_1۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_1٠iterｰspec' Ψ fn t vs :
    {{{
      ▷ Ψ 0 [] ∗
      dynarray_1۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ ˖i (take i vs ++ [v])
        }}
      )
    }}}
      dynarray_1٠iter fn t
    {{{
      RET ();
      dynarray_1۰model t vs ∗
      Ψ (length vs) vs
    }}}.
  Lemma dynarray_1٠iterｰspecｰdisentangled Ψ fn t vs :
    {{{
      dynarray_1۰model t vs ∗
      □ (
        ∀ i v,
        ⌜vs !! i = Some v⌝ -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_1٠iter fn t
    {{{
      RET ();
      dynarray_1۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
  Lemma dynarray_1٠iterｰspecｰdisentangled' Ψ fn t vs :
    {{{
      dynarray_1۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ i v
        }}
      )
    }}}
      dynarray_1٠iter fn t
    {{{
      RET ();
      dynarray_1۰model t vs ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ i v
      )
    }}}.
End zoo۰G.

Require zoo_std.dynarray_1__opaque.

#[global] Opaque dynarray_1۰model.