Library zoo_std.random

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.random__code.
Require Import zoo_std.random__types.
Require Import zoo.options.

Axiom random ٠ init ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} Φ,
  Φ ()%V ⊢
  WP random ٠ init () {{ Φ }}.

Axiom random ٠ bits ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} Φ,
  ( ∀ n : Z ,
    Φ #n
  ) ⊢
  WP random ٠ bits () {{ Φ }}.

Axiom random ٠ int ｰ spec : ∀ `{zoo ۰ G : !ZooG Σ} ub Φ,
  (0 < ub)%Z →
  ( ∀ n ,
    ⌜0 ≤ n < ub ⌝%Z -∗
    Φ #n
  ) ⊢
  WP random ٠ int #ub {{ Φ }}.

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

  Lemma random ٠ int ｰ spec ｰ nat (ub : nat) Φ :
    0 < ub →
    ( ∀ n ,
      ⌜n < ub ⌝ -∗
      Φ #n
    ) ⊢
    WP random ٠ int #ub {{ Φ }}.

  Lemma random ٠ int_in_range ｰ spec lb ub Φ :
    (lb < ub)%Z →
    ( ∀ n ,
      ⌜lb ≤ n < ub ⌝%Z -∗
      Φ #n
    ) ⊢
    WP random ٠ int_in_range #lb #ub {{ Φ }}.
  Lemma random ٠ int_in_range ｰ spec ｰ nat lb ub Φ :
    lb < ub →
    ( ∀ n ,
      ⌜lb ≤ n < ub ⌝ -∗
      Φ #n
    ) ⊢
    WP random ٠ int_in_range #lb #ub {{ Φ }}.
End zoo ۰ G.

Require zoo_std.random__opaque.