std/property
Reproducible pure generators with lazy, ordered shrink trees. Shrinking is structural: a mapped value need not get numerically smaller. Replay requires the same library version, generator code, captured values, and deterministic, terminating callbacks. Store the lock file with reports. Pure types alone do not prove these callback laws; function identities and hidden host effects are not reproducible data.
Each attempt has its own path-derived stream. Shrinking greedily follows
the first failing child; its budget counts predicate calls, not time or
child-list construction. smallest is the best value on that path, not a
global minimum. User thunks may diverge. Integer children cost logarithmic
space; list children can require quadratic copying. Ancestors may remain
reachable through closures. See docs/design/std-3.md P1–P9 for the protocol.
Gen
Gen(A) = ((Int, random.Generator) -> Option(Tree(A))) Tree
Tree(A) = (value = A, children = () -> List(Tree(A))) Config
Config = ( BuildError
BuildError = InvalidRange | InvalidLength | EmptyChoice Verdict
Verdict = Pass | Fail | Discard Failure
Failure(A) = ( Report
Report(A) = Passed | GaveUp | Falsified(A) | InvalidConfig defaults
The default seed, success count, size, discard budget, and shrink budget.
defaults = () -> Config { make
Stores a pure draw. None discards one attempt; there are no hidden retries.
make = <A>(draw : (Int, random.Generator) -> Option(Tree(A))) -> Gen(A) { sample
Calls the draw once, clamping negative size to zero. Random is immutable.
sample = <A>(gen : Gen(A), size : Int, random : random.Generator) -> Option( tree
The root is computed now; children are deferred until requested.
tree = <A>(value : A, children : () -> List(Tree(A))) -> Tree(A) { constant
A leaf, independent of size and random input.
constant = <A>(value : A) -> Gen(A) { map
Changes values, retaining ordered shape and duplicates, lazily below root.
map = <A, B>(gen : Gen(A), with : (A) -> B) -> Gen(B) { flat_map
Splits once. Outer shrinks regenerate the dependent tree on the same right stream and size. Outer alternatives precede inner alternatives; discarded branches are pruned, including descendants. Seeded associativity is no law.
flat_map = <A, B>(gen : Gen(A), with : (A) -> Gen(B)) -> Gen(B) { pair
Exactly flat_map followed by map, including random stream allocation.
pair = <A, B>(first : Gen(A), second : Gen(B)) -> Gen((A, B)) { filter
One root draw. Failing children and their whole subtrees are removed.
filter = <A>(gen : Gen(A), keeping : (A) -> Bool) -> Gen(A) { sized
Selects a generator using the current size, with the same random stream.
sized = <A>(with : (Int) -> Gen(A)) -> Gen(A) { resize
Replaces size, including the size captured by dependent shrink trees.
resize = <A>(gen : Gen(A), size : Int) -> Gen(A) { int
Uniform inclusive range under the uniform-word model. Shrinks toward zero or its nearest endpoint, then by halving distance, with duplicates removed.
int = (min : Int, max : Int) -> Result(Gen(Int), BuildError) { bool
True shrinks to False.
bool = () -> Gen(Bool) { map(range(0, 1), (n) { n == 1 }) } element
Draws and shrinks an index toward zero. Duplicates keep their multiplicity.
element = <A>(choices : List(A)) -> Result(Gen(A), BuildError) { list
Length is uniform in min..min(max,max(min,size)). Deletions of full chunks n,n/2,…,1 precede left-to-right element shrinks. Surviving trees are kept.
list = <A>(of : Gen(A), min : Int, max : Int) -> Result( float
Equal weight for finite bit patterns under the uniform-word model, not uniform over reals or a guarantee about finite seed coverage. Both zeros are included. Sign and magnitude shrink independently toward positive zero.
float = () -> Gen(Float) { utf_codepoint
Uniform scalar rank, skipping the surrogate block; shrinks rank toward NUL.
utf_codepoint = () -> Gen(UtfCodepoint) { string
Scalar lists of length 0..max_length, preserving valid UTF-8 while shrinking.
string = (max_length : Int) -> Result(Gen(String), BuildError) { check
Validates before any callback. Attempts j use path [j+1], size j%(max_size+1). None and Discard each consume one discard. Exhausting the candidate budget sets limited even when the next child list would be empty; zero never forces children. The first failing child is adopted and scanning restarts at zero.
check = <A>(gen : Gen(A), config : Config, property : (A) -> Verdict) -> Report( replay
Follows retained child positions without invoking a predicate. Invalid attempt, size or path entries, discarded draws and missing children miss.
replay = <A>( format
Protocol v1, decimal integers and LF separators with no final LF. Calls show twice only for Falsified; includes multiline text literally. No check or predicate is rerun, and arbitrary identities are not serialized.
format = <A>(report : Report(A), show : (A) -> String) -> String { test
Catches each case’s Assert into Fail(message). The final single assertion is sent to the caller’s Assert outside that catch. Stops remain stops; the original source stack is not retained, only its message. No runner hook.
test = <A>(