Library zoo_std.random_round

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  random_round__code.
From zoo_std Require Import
  array
  random_state
  random_round__types.
From zoo Require Import
  options.

Implicit Types i n cnt : nat.
Implicit Types prevs nexts : list nat.
Implicit Types l : location.
Implicit Types 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.

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