random

python.Words

data Words

The 624 words in a complete binary tree of depth 10 (the leaves past 623 are unused zeros): reads and writes take ten steps (the standard library’s Array carries a proof in each array, which makes evaluating 624 writes in the checker too slow).

python.Words.depth

def Words.depth : Nat

The depth of the tree of words.

python.Words.ofList

def Words.ofList (depth : Nat) (xs : List Nat) : Words

A tree of depth depth holding the words xs in order (missing ones are 0).

python.Words.at

def Words.at (depth : Nat) (t : Words) (i : Nat) : Nat

The word at index i of the tree t of depth depth.

python.Words.store

def Words.store (depth : Nat) (t : Words) (i : Nat) (x : Nat) : Words

The tree t of depth depth with the word at index i replaced by x.

python.Generator

record Generator

The generator’s state: 624 words of 32 bits and the position of the next one (624: all used); whether CPython would have seeded it from the operating system (the model has seed(0)’s words instead), and whether a draw was made in that state.

python.Random.wordSize

def Random.wordSize : Nat

2^32.

python.Random.word

def Random.word (x : Nat) : Nat

The natural x kept to 32 bits.

python.Random.xor

def Random.xor (a : Nat) (b : Nat) : Nat

Exclusive or of the 32-bit words a and b.

python.Random.and

def Random.and (a : Nat) (b : Nat) : Nat

And of the 32-bit words a and b.

python.Random.shiftRight

def Random.shiftRight (x : Nat) (k : Nat) : Nat

The word x shifted right by k bits.

python.Random.at

def Random.at (words : Words) (k : Nat) : Nat

The word at position k of words.

python.Random.store

def Random.store (words : Words) (k : Nat) (x : Nat) : Words

The words with the one at position k replaced by x.

python.Random.mixed

def Random.mixed (x : Nat) : Nat

x ^ (x >> 30), the mixing both initializations use.

python.Random.fill

def Random.fill (fuel : Nat) (k : Nat) (previous : Nat) : List Nat

init_genrand(s): mt[i] = 1812433253 * (mt[i-1] ^ (mt[i-1] >> 30)) + i, from position k after the word previous, fuel words.

python.Random.initial

def Random.initial (s : Nat) : Words

init_genrand(s).

python.Random.advance

def Random.advance (words : Words) (i : Nat) : Words * Nat

The position after i in words: back to 1 past the end, with mt[0] set to mt[623].

python.Random.keyed

def Random.keyed (k : Nat) (key : List Nat) (words : Words) (i : Nat) (j : Nat) : Words * Nat

init_by_array’s first loop on words: mt[i] = (mt[i] ^ (mix(mt[i-1]) * 1664525)) + key[j] + j, k steps from position i and the index j into key.

python.Random.unkeyed

def Random.unkeyed (k : Nat) (words : Words) (i : Nat) : Words

init_by_array’s second loop on words: mt[i] = (mt[i] ^ (mix(mt[i-1]) * 1566083941)) - i, k steps from position i.

python.Random.keyWords

def Random.keyWords (fuel : Nat) (n : Nat) : List Nat

The 32-bit words of the natural n, least significant first (one word for 0), within fuel words.

python.Random.seeded

def Random.seeded (n : Nat) : Generator

The generator seed(n) gives for a natural (init_by_array with its words).

python.Random.unseeded

def Random.unseeded : Generator

The generator before any seed: CPython seeds it from the operating system; the model starts from seed(0)’s.

python.Random.twistAt

def Random.twistAt (words : Words) (kk : Nat) : Words

One step of the twist of words at position kk: y from mt[kk]’s top bit and mt[kk+1]’s other bits.

python.Random.twist

def Random.twist (k : Nat) (kk : Nat) (words : Words) : Words

The twist of words from position kk on, k steps.

python.Random.temper

def Random.temper (y : Nat) : Nat

Tempering the word y.

python.Random.next

def Random.next (g : Generator) : Nat * Generator

The next 32-bit word of the generator g and the generator after it (genrand_uint32).

python.Random.bitsWithin

def Random.bitsWithin (fuel : Nat) (g : Generator) (k : Nat) (scale : Nat) (value : Nat) : Nat * Generator

getrandbits(k) from the generator g, word to word, least significant first, within fuel words: k the bits still to draw, value the value so far and scale the weight of the next word.

python.Random.bits

def Random.bits (g : Generator) (k : Nat) : Nat * Generator

getrandbits(k) from the generator g.

python.Random.belowWithin

def Random.belowWithin (fuel : Nat) (g : Generator) (n : Nat) : Option (Nat * Generator)

_randbelow(n) for n at least 1: k-bit draws from the generator g (k: n’s bit length) until one is below n, within fuel draws (each is refused with probability below a half; past the fuel the model gives up: unsupported).

python.Random.ratio

def Random.ratio (a : Nat) (b : Nat) : Float

(a * 2^26 + b) / 2^53 from two words’ top 27 and 26 bits, exact.

python.Random.unit

def Random.unit (g : Generator) : Float * Generator

random() from the generator g.

python.Random.natural

def Random.natural (n : Nat) : Value

An int of the natural value n.

python.Drawn

data Drawn

What a random function gives: the generator after it, and the heap and outcome.

python.Random.fails

def Random.fails (g : Generator) (h : Heap) (e : Raised) : Drawn

The exception e raised, with the generator g and the heap h unchanged.

python.Random.bound

def Random.bound (h : Heap) (name : String) (parameters : List String) (defaults : List Value) (positional : List Value) (keywords : List (Codes * Value)) : Either Raised (List Value)

The positional and keywords arguments of the Python-level function name bound on the heap h to its parameters, the last ones taking the defaults (self first, given as None), or the exception.

python.Random.below

def Random.below (g : Generator) (h : Heap) (n : Nat) (rest : Generator -> Nat -> Drawn) : Drawn

_randbelow(n) from the generator g as a draw of an int below n, then rest given the generator after it and the int; refused 256 times it is unsupported, the heap h unchanged.

python.Random.seed

def Random.seed (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

seed(a=None, version=2) with the positional and keywords arguments, on the generator g and the heap h.

python.Random.random

def Random.random (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

random() with the positional and keywords arguments, on the generator g and the heap h.

python.Random.getrandbits

def Random.getrandbits (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

getrandbits(k) with the positional and keywords arguments, on the generator g and the heap h.

python.Random.index

def Random.index (h : Heap) (v : Value) : Either Raised Int

The index of the argument v (operator.index), or the TypeError naming its type on the heap h.

python.Random.offset

def Random.offset (g : Generator) (h : Heap) (start : Int) (step : Int) (n : Nat) : Drawn

An int drawn from the generator g: start plus step times a draw below n, on the heap h.

python.Random.rangeWithStop

def Random.rangeWithStop (g : Generator) (h : Heap) (start : Value) (stop : Value) (step : Value) (a : Int) (b : Int) : Drawn

randrange(start, stop, step) of the values start, stop and step once start and stop are the ints a and b (CPython 3.14’s code after the stop check), on the generator g and the heap h.

python.Random.isOne

def Random.isOne (v : Value) : Bool

Whether the value v is the int 1 itself (CPython’s step is not _ONE: True and 1.0 are not).

python.Random.randrange

def Random.randrange (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

randrange(start, stop=None, step=1) with the positional and keywords arguments, on the generator g and the heap h.

python.Random.randint

def Random.randint (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

randint(a, b) with the positional and keywords arguments, on the generator g and the heap h.

python.Random.size

def Random.size (h : Heap) (x : Value) : Either Raised Nat

len(x) of the value x on the heap h for the module’s functions: a user’s __len__ would run its code (unsupported here).

python.Random.pickFrom

def Random.pickFrom (h : Heap) (seq : Value) (next : Generator) (k : Nat) : Drawn

The item of the sequence seq on the heap h at the drawn index k, with next the generator after the draw.

python.Random.choice

def Random.choice (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

choice(seq): by len and indexing, with the positional and keywords arguments, on the generator g and the heap h.

python.Random.swaps

def Random.swaps (fuel : Nat) (g : Generator) (h : Heap) (x : Value) (i : Nat) : Drawn

shuffle(x)’s swaps of the sequence x on the heap h for i from the end down to 1, within fuel swaps: j drawn from the generator g below i + 1, then x[i], x[j] = x[j], x[i].

python.Random.shuffle

def Random.shuffle (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

shuffle(x) with the positional and keywords arguments, on the generator g and the heap h.

python.Random.uniform

def Random.uniform (g : Generator) (h : Heap) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

uniform(a, b): a + (b - a) * random(), b - a first; with the positional and keywords arguments, on the generator g and the heap h.

python.RandomFunction

def RandomFunction : Type

A random function: its name and what calling it does.

python.Random.functions

def Random.functions : List RandomFunction

The random module’s functions the model provides.

python.Random.call

def Random.call (g : Generator) (h : Heap) (name : String) (positional : List Value) (keywords : List (Codes * Value)) : Drawn

Calling random.name(...) for the function name with the positional and keywords arguments, on the generator g and the heap h; a name the model does not provide is unsupported.