Random

Linear pseudo-random generators (issue #441). Modelling `random.random()` as a pure `Unit -> {r:Float | 0.0 <= r < 1.0}` is unsound: the refinement logic treats it as referentially transparent, so two draws look *equal* to the SMT solver and a single draw can be silently shared. Purity is a precondition for the refinement logic to be sound, so an impure value with a refinement is a hole. Here randomness is threaded through an explicit generator used at multiplicity 1. Every draw consumes its generator and produces a result carrying both the sample and a *successor* generator; to draw again, bind the successor (`*_next`) to a `let 1` and draw from it. A value can never be drawn twice from the same generator, and the logic never sees a draw as a pure function. The numeric draws expose the sample through a refined projection, so the bound survives and composes into proofs. To finish a chain, just project the last sample and stop — the unextracted successor imposes no obligation (the `*Draw` result is an ordinary value). For example, two dice provably sum to [2, 12]: def two_dice (seed: Int) : {s:Int | s >= 2 && s <= 12} := let 1 g0 := new_rng seed in let d1 := draw_int 1 6 g0 in let a := int_value 1 6 d1 in # a : {r:Int | 1 <= r <= 6} let 1 g1 := int_next d1 in # continue from the successor let d2 := draw_int 1 6 g1 in let b := int_value 1 6 d2 in # last draw: project and stop a + b `close_rng` is needed only to discharge a generator you *hold* but never draw from — e.g. a helper handed a `(1 g: Rng)` it ends up not using. An opaque pseudo-random generator (a Python `random.Random` at runtime), used linearly: every draw consumes it and produces a fresh successor. Being a `linear type`, every binder holding an `Rng` must be declared with multiplicity 1.
Imports
open Array;
Table of Contents

Types

Rng

(type) linear
An opaque pseudo-random generator (a Python `random.Random` at runtime), used linearly: every draw consumes it and produces a fresh successor. Being a `linear type`, every binder holding an `Rng` must be declared with multiplicity 1.
linear type Rng

Draw

(type)
Results of a draw: the sample paired with the successor generator. These are ordinary (non-linear) values — the generator re-enters the linear discipline only when the `*_next` projection is bound to a `let 1`, so stopping a chain is just declining to project the successor.
type Draw

IntDraw

(type)
type IntDraw

RangeDraw

(type)
type RangeDraw

Functions

new_rng

A fresh generator seeded deterministically. The `Int` argument makes this an *applied* action, so each call yields a new generator — a nullary `def` would be a memoised value, aliasing one generator everywhere.
def new_rng (seed : Int) : Rng

draw

── Float draw in [0.0, 1.0) ────────────────────────────────────────────
def draw (1 g : Rng) : Draw

draw_value

def draw_value (d : Draw) : {r : Float | r ≥ 0.0 && r < 1.0}

draw_next

def draw_next (d : Draw) : Rng

draw_int

── Integer draw in [lo, hi] ──────────────────────────────────────────── The bounds are repeated on the projection so the refinement survives the opaque `IntDraw`.
def draw_int (lo : Int) (hi : Int | hi ≥ lo) (1 g : Rng) : IntDraw

int_value

def int_value (lo : Int) (hi : Int | hi ≥ lo) (d : IntDraw) : {r : Int | r ≥ lo && r ≤ hi}

int_next

def int_next (d : IntDraw) : Rng

draw_range

── Float draw in [lo, hi) ──────────────────────────────────────────────
def draw_range (lo : Float) (hi : Float | hi > lo) (1 g : Rng) : RangeDraw

range_value

def range_value (lo : Float) (hi : Float | hi > lo) (d : RangeDraw) : {r : Float | r ≥ lo && r < hi}

range_next

def range_next (d : RangeDraw) : Rng

choose

── Uniform choice from a non-empty array (polymorphic) ─────────────────
def choose (1 xs : Array a | Array.size xs > 0) (1 g : Rng) : a

close_rng

Discharge a generator you hold but never draw from (e.g. a helper handed a generator it ends up not using). Straight-line draw chains never need this — just stop projecting the successor.
def close_rng (1 g : Rng) : Unit