Library zoo_std.random_round

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Export zoo_std.random_round__code.
Require Import zoo_std.random_round__types.
Require Import zoo.options.

Implicit Type i n cnt : nat.
Implicit Type prevs nexts : list nat.
Implicit Type l : location.
Implicit Type t rand arr : val.

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

  Definition random_round ۰ model t sz prevs : iProp Σ :=
    ∃ l rand arr nexts ,
    ⌜t = #l ⌝ ∗
    ⌜nexts ++ reverse prevs ≡ₚ seq 0 sz ⌝ ∗
    l .[random ] ↦ rand ∗
    l .[array ] ↦ arr ∗
    l .[index ] ↦ #(length nexts ) ∗
    random_state ۰ model rand ∗
    array ۰ model arr (DfracOwn 1) (#*@{nat } $ nexts ++ reverse prevs).
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %rand & %arr & %nexts & -> & %Hpermutation & Hl_random & Hl_array & Hl_index & Hrand & Harr ) ".

  Lemma random_round ٠ create ｰ spec sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      random_round ٠ create #sz
    {{{
      t
    , RET t ;
      random_round ۰ model t ₊sz []
    }}}.

  Lemma random_round ٠ reset ｰ spec t sz prevs :
    {{{
      random_round ۰ model t sz prevs
    }}}
      random_round ٠ reset t
    {{{
      RET ();
      random_round ۰ model t sz []
    }}}.

  Lemma random_round ٠ next ｰ spec t sz prevs :
    length prevs ≠ sz →
    {{{
      random_round ۰ model t sz prevs
    }}}
      random_round ٠ next t
    {{{
      n
    , RET #n ;
      ⌜n < sz ⌝ ∗
      ⌜n ∉ prevs ⌝ ∗
      random_round ۰ model t sz (prevs ++ [n])
    }}}.
End zoo ۰ G.

Require zoo_std.random_round__opaque.

#[global] Opaque random_round ۰ model.

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

  Definition random_round ۰ model' t sz cnt : iProp Σ :=
    ∃ prevs ,
    ⌜(cnt + length prevs)%nat = sz ⌝ ∗
    random_round ۰ model t sz prevs.
  #[local] Instance : CustomIpat "model'" :=
    " ( %prevs & %H & Ht ) ".

  Lemma random_round ٠ create ｰ spec' sz :
    (0 ≤ sz)%Z →
    {{{
      True
    }}}
      random_round ٠ create #sz
    {{{
      t
    , RET t ;
      random_round ۰ model' t ₊sz ₊sz
    }}}.

  Lemma random_round ٠ reset ｰ spec' t sz cnt :
    {{{
      random_round ۰ model' t sz cnt
    }}}
      random_round ٠ reset t
    {{{
      RET ();
      random_round ۰ model' t sz sz
    }}}.

  Lemma random_round ٠ next ｰ spec' t sz cnt :
    0 < cnt →
    {{{
      random_round ۰ model' t sz cnt
    }}}
      random_round ٠ next t
    {{{
      n
    , RET #n ;
      ⌜n < sz ⌝ ∗
      random_round ۰ model' t sz (cnt - 1)
    }}}.
End zoo ۰ G.

#[global] Opaque random_round ۰ model'.