Library zoo_std.random_state

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  random_state__code.
From zoo Require Import
  options.

Implicit Types 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.

From zoo_std Require
  random_state__opaque.