Library zoo_std.dynarray_1

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  dynarray_1__code.
From zoo_std Require Import
  array
  dynarray_1__types
  int.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types i : nat.
Implicit Types l : location.
Implicit Types v t fn : val.
Implicit Types 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,
          ▷ Ψ (S 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,
          ▷ Ψ (S 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⌝ ∗
          ▷ Ψ (S 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⌝ ∗
          ▷ Ψ (S 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⌝ ∗
          ▷ Ψ (S 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⌝ ∗
          ▷ Ψ (S 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.

From zoo_std Require
  dynarray_1__opaque.

#[global] Opaque dynarray_1_model.