Library zoo_std.random_state

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.random_state__code.
Require Import zoo_std.random_state__types.
Require Import zoo.options.

Implicit Type t : val.

Parameter random_state ۰ model : ∀ `{zoo ۰ G : !ZooG Σ}, val → iProp Σ.

Axiom random_state ٠ create ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ},
  {{{
    True
  }}}
    random_state ٠ create ()
  {{{
    t
  , RET t ;
    random_state ۰ model t
  }}}.

Axiom random_state ٠ bits ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} t,
  {{{
    random_state ۰ model t
  }}}
    random_state ٠ bits t
  {{{
    (n : Z )
  , RET #n ;
    random_state ۰ model t
  }}}.

Axiom random_state ٠ int ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} t ub,
  (0 < ub)%Z →
  {{{
    random_state ۰ model t
  }}}
    random_state ٠ int t #ub
  {{{
    n
  , RET #n ;
    ⌜0 ≤ n < ub ⌝%Z ∗
    random_state ۰ model t
  }}}.

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

  Lemma random_state ٠ int ｰ spec ｰ nat t (ub : nat) :
    0 < ub →
    {{{
      random_state ۰ model t
    }}}
      random_state ٠ int t #ub
    {{{
      n
    , RET #n ;
      ⌜n < ub ⌝ ∗
      random_state ۰ model t
    }}}.

  Lemma random_state ٠ int_in_range ｰ spec t lb ub :
    (lb < ub)%Z →
    {{{
      random_state ۰ model t
    }}}
      random_state ٠ int_in_range t #lb #ub
    {{{
      n
    , RET #n ;
      ⌜lb ≤ n < ub ⌝%Z ∗
      random_state ۰ model t
    }}}.
  Lemma random_state ٠ int_in_range ｰ spec ｰ nat t lb ub :
    lb < ub →
    {{{
      random_state ۰ model t
    }}}
      random_state ٠ int_in_range t #lb #ub
    {{{
      n
    , RET #n ;
      ⌜lb ≤ n < ub ⌝ ∗
      random_state ۰ model t
    }}}.
End zoo ۰ G.

Require zoo_std.random_state__opaque.