Library zoo_std.random

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  random__code.
From zoo Require Import
  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.

From zoo_std Require
  random__opaque.