proptest

proptest is a property testing framework for Mojo (i.e., the QuickCheck family) inspired by the Hypothesis framework for Python, with ideas from Rust’s proptest and quickcheck, Haskell’s QuickCheck, and C++’s RapidCheck.

With proptest, you write tests that should pass for every input in a range you describe, and proptest chooses which of those inputs to try, including edge cases you might not have thought of. When it finds an input that fails, it shrinks it to a minimal failing example before reporting it:

from std.testing import assert_true
from proptest import given, lists, integers

def my_sort(xs: List[Int]) -> List[Int]:
    var ys = xs.copy()
    sort(ys)
    return ys^

def test_sort_is_ordered() raises:
    def prop(xs: List[Int]) raises:
        var ys = my_sort(xs)
        for i in range(1, len(ys)):
            assert_true(ys[i - 1] <= ys[i])
    given(lists(integers()), prop)

def main() raises:
    test_sort_is_ordered()

proptest is built on Hypothesis’s Conjecture engine. Strategies don’t generate values directly: they parse them from a recorded sequence of choices, and the shrinker simplifies that sequence. Shrinking therefore works for every strategy, including the ones you write yourself, without any shrinking code of your own. The other libraries contributed most of the typed API: inferring inputs from a property’s parameter types, constraint types such as Positive[T], coverage checking, and model-based testing.

How this book is organized

The book follows the layout of the Hypothesis documentation:

• Quickstart: the essentials on one page.
• Tutorial: an introduction to proptest, from a first test through strategies, settings, the example database, and stateful testing. Start here if you’re new to property-based testing.
• How-to guides: recipes for particular tasks, such as checking the distribution of your inputs or debugging a failure.
• Explanations: how proptest works, and why it is the way it is.
• Reference: every test function, setting, and strategy.

Where proptest behaves differently from Hypothesis, the book says so. The differences document in the repository has the full list, with the reason for each.

Requirements

proptest needs Mojo 1.3 or later. Until Mojo 1.3.0 is released, that means the nightly channel. See Introduction to proptest for installation.

Quickstart

This is a short guide to the basics of proptest. The tutorial covers the same ground in more depth.

Install proptest

proptest needs Mojo 1.3 or later. Clone the repository and put it on your include path:

git clone https://github.com/bpr/proptest
mojo run -I path/to/proptest my_tests.mojo

Or build a package once with pixi run package (in the proptest repository), and put build/proptest.mojoc on the include path.

Write your first test

Here is a run-length encoder with a bug:

from std.testing import assert_equal
from proptest import given, text, Settings

def encode(s: String) -> List[Tuple[String, Int]]:
    var out = List[Tuple[String, Int]]()
    var prev = String()
    var count = 0
    for cp in s.codepoints():
        var c = String(cp)
        if c != prev and count > 0:
            out.append((prev, count))
            count = 0
        prev = c
        count += 1
    # BUG: the last run is never appended
    return out^

def decode(runs: List[Tuple[String, Int]]) -> String:
    var s = String()
    for r in runs:
        for _ in range(r[1]):
            s += r[0]
    return s^

def main():
    def decode_inverts_encode(s: String) raises:
        assert_equal(decode(encode(s)), s)

    try:
        given(text(), decode_inverts_encode, Settings(database=None))
    except e:
        print(e)

given(text(), decode_inverts_encode) runs the test on 100 strings drawn from the text() strategy. The test fails, and proptest reports the simplest string it fails for:

Falsifying example (quickstart.mojo:41:14):
    given('0')
At quickstart.mojo:38:21: AssertionError: `left == right` comparison failed:
   left:
  right: 0

proptest found some long, complicated string that broke the test, then shrank it to '0'. The one-character string is easier to debug: the final run is missing.

Running in a test suite

A given call raises an Error when its test fails, so a property test is an ordinary Mojo test function. With std.testing.TestSuite:

from std.testing import TestSuite, assert_equal
from proptest import given, integers

def test_addition_commutes() raises:
    def prop(a: Int, b: Int) raises:
        assert_equal(a + b, b + a)
    given(integers(), integers(), prop)

def main() raises:
    TestSuite.discover_tests[__functions_in_module()]().run()

The property is a nested function. It can capture values from the enclosing function with a capture list: def prop(x: Int) raises {var limit}:.

Arguments to given

given takes one to six strategies, then the test, then optional Settings. The test’s parameters must have the types the strategies produce:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    def prop(xs: List[Int], s: String, b: Bool) raises:
        pass

    given(lists(integers()), text(), booleans(), prop)  # prop(xs: List[Int], s: String, b: Bool)

To let proptest choose the strategies from the parameter types instead, use check:

from proptest import check

def test_reverse_twice() raises:
    def prop(xs: List[Int]) -> Bool:
        var ys = xs.copy()
        ys.reverse()
        ys.reverse()
        return ys == xs
    check(prop)

def main() raises:
    test_reverse_twice()

Filtering inside a test

Sometimes a test only makes sense for some inputs. assume(condition) discards the current input if the condition is false:

from std.testing import assert_equal
from proptest import given, integers, assume

def test_division() raises:
    def prop(a: Int, b: Int) raises:
        assume(b != 0)
        assert_equal((a // b) * b + a % b, a)
    given(integers(), integers(), prop)

def main() raises:
    test_division()

Discarded inputs don’t count towards the 100 examples. If you discard too many, proptest fails the test with a health check, because it isn’t really testing anything. It’s better to generate only valid inputs: here, filter(integers(), lambda (b: Int) -> Bool: b != 0), or the constraint type NonZero[Int].

Dependent generation

When one input depends on another, draw them inside the test. given_data passes the test a ConjectureData, from which it can draw as it goes:

from std.testing import assert_true
from proptest import given_data, lists, integers, ConjectureData

def test_index() raises:
    def prop(mut data: ConjectureData) raises:
        var xs = data.draw(lists(integers(), min_size=1), "xs")
        var i = data.draw(integers(0, len(xs) - 1), "i")
        assert_true(xs[i] in xs)
    given_data(prop)

def main() raises:
    test_index()

The second argument to draw is a label, printed with the value in a failure report.

Where to go next

• Built-in strategies lists what proptest can generate.
• Configuring test settings covers the number of examples, seeds, and the other settings.
• Stateful testing tests whole sequences of operations.

Introduction to proptest

This page introduces proptest and property-based testing: how to install proptest, write a test, and read its reports.

Installing proptest

proptest needs Mojo 1.3 or later; until Mojo 1.3.0 is released, that means the nightly channel. The repository uses pixi:

git clone https://github.com/bpr/proptest
cd proptest
pixi install
pixi run test        # proptest's own test suite
pixi run package     # writes build/proptest.mojoc

To use proptest from your project, either put the repository on the include path (mojo run -I path/to/proptest ...) or put the directory containing proptest.mojoc there. proptest will be published on the modular-community channel once Mojo 1.3.0 is released; then pixi add proptest will be enough.

Defining a simple test

A property-based test has two parts: a test function that checks a property for one input, and strategies that describe which inputs to try. given connects them:

from std.testing import assert_equal
from proptest import given, integers

def main() raises:
    def addition_commutes(a: Int, b: Int) raises:
        assert_equal(a + b, b + a)

    given(integers(), integers(), addition_commutes)
    print("passed")

integers() is a strategy for Int values. given draws a value for each strategy, calls the test, and repeats, 100 times by default. If the test raises for some input, given shrinks that input and raises an error describing it. If it never does, given returns.

The test is an ordinary nested function. Its parameters must have the types the strategies produce, in order; the compiler checks this.

Testing a sorting algorithm

Suppose we want to test a sorting function. Rather than write out a few lists and their sorted forms, we state what’s true of every sorted list: it’s in order, and it has the same elements as the input.

from std.testing import assert_true, assert_equal
from proptest import given, lists, integers

def my_sort[T: Comparable & Copyable](xs: List[T]) -> List[T]:
    var ys = xs.copy()
    sort(ys)
    return ys^

def main() raises:
    def sorts(xs: List[Int]) raises:
        var ys = my_sort(xs)
        assert_equal(len(ys), len(xs))
        for i in range(1, len(ys)):
            assert_true(ys[i - 1] <= ys[i])
        for x in xs:
            assert_true(x in ys)

    given(lists(integers()), sorts)
    print("passed")

lists(integers()) generates lists of integers. Strategies combine like this: lists takes a strategy for its elements, and many others take strategies too.

Adding floats to our test

Does it work for floats? Change the element strategy:

from std.testing import assert_true
from proptest import given, lists, floats, Settings

def my_sort[T: Comparable & Copyable](xs: List[T]) -> List[T]:
    var ys = xs.copy()
    sort(ys)
    return ys^

def main():
    def ordered(xs: List[Float64]) raises:
        var ys = my_sort(xs)
        for i in range(1, len(ys)):
            assert_true(ys[i - 1] <= ys[i], String(ys[i - 1], " > ", ys[i]))

    try:
        given(lists(floats()), ordered, Settings(database=None))
    except e:
        print(e)

Falsifying example (sorting.mojo:16:14):
    given([0.0, nan])
At sorting.mojo:13:24: AssertionError: 0.0 > nan

proptest found that NaN isn’t ordered with respect to anything, so no list containing it can be in order. It shrank whatever list it first found to the simplest one with this problem.

Preventing floats() from generating NaN

Whether this is a bug depends on what my_sort promises. If it isn’t meant to handle NaN, say so in the strategy:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    def ordered(xs: List[Float64]) raises:
        var ys = xs.copy()
        sort(ys)
        for i in range(1, len(ys)):
            assert_true(ys[i - 1] <= ys[i])

    given(lists(floats(allow_nan=False)), ordered)

This is typical of property-based testing: a failure makes you decide precisely what your code should do.

Tests with multiple arguments

given takes up to six strategies. When a test with several arguments fails, all of them are shrunk:

Falsifying example (two.mojo:24:14):
    given([0, 0], '00')
both

Each value is printed as its type writes itself (Writable), with strings quoted.

Letting the types choose: check

When the plain types of the test’s parameters say enough, check infers the strategies from them:

from proptest import check

def main() raises:
    def reverse_twice(xs: List[Int]) -> Bool:
        var ys = xs.copy()
        ys.reverse()
        ys.reverse()
        return ys == xs

    check(reverse_twice)
    print("passed")

A property passed to check can raise, like a given test, or return Bool. Strategies from types covers check, and how to put constraints such as “non-empty” or “positive” in the parameter types.

Running proptest tests

A test that calls given or check raises when the property fails, so it works with any way of running Mojo tests. With std.testing.TestSuite:

from std.testing import TestSuite, assert_equal
from proptest import given, integers

def test_addition_commutes() raises:
    def prop(a: Int, b: Int) raises:
        assert_equal(a + b, b + a)
    given(integers(), integers(), prop)

def main() raises:
    TestSuite.discover_tests[__functions_in_module()]().run()

A failing example is saved in the example database, a directory named .proptest/examples under the working directory, and is tried first the next time the test runs. See Replaying failures.

When to use property-based testing

Property-based testing is useful when you can say what should be true of a result without computing the result by hand. Common kinds of property:

• Round trips: decode(encode(x)) == x; parsing what you printed.
• Invariants: a sorted list is ordered; a balanced tree stays balanced; a count is never negative.
• Equivalence with a model: a fast implementation agrees with a slow, obviously correct one, or with the same operation on a simpler data structure.
• Algebraic laws: an operation is commutative, associative, or idempotent.
• No crashes: the code doesn’t raise, or raises only documented errors, for any valid input.

It complements example-based tests rather than replacing them. A handful of examples documents behaviour you care about; properties find the inputs you didn’t think of.

Built-in strategies

A strategy describes the values a test should be given. proptest has strategies for numbers, text, and collections, and combinators that build strategies out of other strategies.

Strategies are values: integers(0, 10) returns a strategy, which you can store in a variable and pass to several tests. Strategy constructors that check their arguments raise on invalid ones (for example integers(10, 0)), so call them from a raises function.

Exploring a strategy

example(strategy) returns one random value, which is handy for seeing what a strategy produces:

from proptest import example, lists, integers, text

def main() raises:
    for _ in range(3):
        print(example(lists(integers(0, 9), max_size=5)))
    print(example(text("abc", min_size=2, max_size=4)))

Use example for exploring, not in tests: a test should let given draw its values, so that failures can be shrunk and replayed.

find(strategy, condition) searches for a value satisfying a condition and returns the simplest one it finds:

from proptest import find, lists, integers

def main() raises:
    def sums_over_100(xs: List[Int]) -> Bool:
        var total = 0
        for x in xs:
            total += x
        return total > 100

    print(find(lists(integers(0, 50)), sums_over_100))   # [1, 50, 50]

Numbers

Integers shrink towards zero, or towards the bound nearest zero. Floats shrink towards simple values: small integers first, then simple fractions. floats() generates NaN and the infinities unless bounds or the allow_ arguments exclude them.

Text

alphabet can be a String of allowed characters or a characters(...) strategy:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var hex = (
text("0123456789abcdef", min_size=1)          # hex digits
    )
    var upper = (
text(characters(categories=["Lu", "Nd"]))     # uppercase letters and digits
    )
    var email = (
from_regex("[a-z]+@[a-z]+\\.com", fullmatch=True)
    )
    print(example(hex), example(upper), example(email))

Categories are Unicode general categories ("Lu", "Nd", or a whole class like "L"), from Unicode 17.0. Without fullmatch=True, from_regex generates strings that contain a match, as Hypothesis does.

Collections

Collections shrink by deleting elements, then by shrinking the elements that remain.

Choosing among values

sampled_from and one_of shrink towards their first option. The optional weights are positive integers that bias generation (weights=[1, 1, 8] picks the third option 80% of the time); they don’t change how values shrink.

Combinators

These build a strategy from other strategies; the next two pages cover them.

Types

from_type[T]() chooses a strategy from a type: scalars, String, List, Optional, Set, Dict, tuples, and your own structs. See Strategies from types.

Everything else

The strategies reference lists every strategy and its arguments. NuMojo arrays have their own package; see Generate NuMojo arrays.

Adapting strategies

The built-in strategies rarely produce exactly the values a test needs. This page shows how to transform them: mapping, filtering, combining, and choosing between them.

proptest’s combinators are free functions that take the strategy as their first argument: map(s, f) where Hypothesis writes s.map(f). (Mojo traits can’t yet have default methods that are generic over closures of the strategy’s value type; see Why the API looks the way it does.) The functions you pass can be top-level functions, nested functions, or lambdas.

Mapping strategy inputs

map(s, f) applies f to each value drawn from s:

from proptest import map, integers, example

def main() raises:
    var evens = map(integers(0, 50), lambda (x: Int) -> Int: x * 2)
    print(example(evens))

The mapped value shrinks as the original does: evens shrinks towards 0, because integers(0, 50) does. Mapping is how you get values with a structure the built-in strategies don’t have, such as even numbers, sorted lists, or a struct built from a few fields.

apply(s1, ..., sN, f) maps a function of several arguments over several strategies (two to six). The function comes last, as in given:

from proptest import apply, integers, example

@fieldwise_init
struct Point(Copyable, Writable):
    var x: Int
    var y: Int

def make_point(x: Int, y: Int) -> Point:
    return Point(x, y)

def main() raises:
    var points = apply(integers(0, 99), integers(0, 99), make_point)
    print(example(points))

Filtering strategy inputs

filter(s, pred) keeps only the values for which pred holds:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var odd = filter(integers(), lambda (x: Int) -> Bool: x % 2 == 1)
    assert_true(example(odd) % 2 != 0)

Filtering works by rejection: proptest draws a value, and if pred rejects it, tries again, up to three times per test case before giving up on that test case. It works well when the condition usually holds, and badly when it rarely does. Prefer constructing the values you want: map(integers(), lambda (x: Int) -> Int: 2 * x + 1) generates odd numbers without any rejection, though it can overflow at the extremes of Int.

If a filter rejects most values, proptest fails the test with a health check rather than silently running a test that checks almost nothing. A reason names the condition in that report:

from proptest import given, filter, integers, Settings

def main() raises:
    def prop(x: Int) raises:
        pass

    var rare = filter(
        integers(),
        lambda (x: Int) -> Bool: x % 1000 == 7,
        reason="ends in 007",
    )
    try:
        given(rare, prop, Settings(database=None))
    except e:
        print(e)

FailedHealthCheck: It looks like this test is filtering out a lot of inputs. 0 inputs
were generated successfully, while 50 inputs were filtered out. Try to construct values
that satisfy the conditions directly instead of using filter() or assume(). Most
rejections were by: ends in 007 (50). (suppress with HealthCheck.filter_too_much)

filter_map

When checking a value and converting it are the same work, filter_map(s, f) does both: f returns an Optional, and None rejects the value.

from std.testing import assert_true, assert_equal
from proptest import *
def parse_digit(s: String) raises -> Optional[Int]:
    if s.byte_length() == 1 and s >= "0" and s <= "9":
        return Int(s)
    return None

def main() raises:
    var digits = filter_map(text(max_size=1), parse_digit)
    var d = example(digits)
    assert_true(d >= 0 and d <= 9)

Assuming away test cases

assume(condition) is a filter inside the test. It discards the current test case when the condition is false:

from std.testing import assert_true, assert_equal
from proptest import *
def prop(a: Int, b: Int) raises:
    assume(b != 0)
    assert_equal((a // b) * b + a % b, a)

def main() raises:
    given(integers(), integers(), prop, Settings(database=None))

assume versus filter

They do the same job in different places:

• filter applies to one strategy, and retries just that draw, up to three times, before giving up on the test case. Use it when the condition is about one value.
• assume discards the whole test case. Use it when the condition involves several arguments, or values computed in the test.

Discarded test cases don’t count towards max_examples, and both count towards the filter_too_much health check.

assume versus returning early

You could also return from the test when an input doesn’t apply. Don’t: proptest then counts the input as a passing test case, so a test that returns early for almost every input passes while testing almost nothing. assume tells proptest the input didn’t count, so it generates others, and the health check fires if it can’t find enough.

Choosing between strategies

one_of draws from one of two to six strategies, which must produce the same type:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var small_or_huge = one_of(integers(-10, 10), integers(1_000_000, 2_000_000))
    var x = example(small_or_huge)
    assert_true(x <= 10 or x >= 1_000_000)

It shrinks towards the first strategy. weights=[...] biases the choice without changing how values shrink:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var mostly_small = one_of(
        integers(-10, 10), integers(1_000_000, 2_000_000), weights=[9, 1]
    )
    var x = example(mostly_small)
    assert_true(x <= 10 or x >= 1_000_000)

For more than six strategies, or a number only known at run time, pass a List of BoxedStrategy values, made with boxed(s):

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var choices: List[BoxedStrategy[Int]] = [
        boxed(just(0)), boxed(integers(1, 9)), boxed(integers(100, 999))
    ]
    var s = one_of(choices^)
    assert_true(example(s) <= 999)

sampled_from([a, b, c]) chooses among fixed values rather than strategies.

Optional values

optionals(s) generates None or a value from s, shrinking towards None. It’s Hypothesis’s none() | s.

Custom strategies

Sometimes the built-in strategies and combinators aren’t enough, or a strategy gets complicated enough to deserve a name. This page shows the ways to define your own.

Writing helper functions

The simplest custom strategy is a function that returns one:

from std.testing import assert_true, assert_equal
from proptest import *
def small_lists() raises -> Lists[Integers]:
    return lists(integers(-10, 10), max_size=5)

def main() raises:
    assert_true(len(example(small_lists())) <= 5)

The return type is the strategy’s struct type. Every strategy function has one (integers returns Integers, lists returns Lists[S], map returns Mapped[S, R, F]), and the reference lists them. When the type is awkward to spell, as it is for a strategy built from a closure, you can erase it: boxed(s) returns a BoxedStrategy[T], whose type mentions only the value type.

Writing your own strategy with composite

composite(f) turns a function that draws values into a strategy. The function receives a ConjectureData and draws from other strategies with data.draw(...):

from proptest import composite, lists, integers, example, ConjectureData

def list_and_index(mut data: ConjectureData) raises -> Tuple[List[Int], Int]:
    var xs = data.draw(lists(integers(), min_size=1))
    var i = data.draw(integers(0, len(xs) - 1))
    return (xs^, i)

def main() raises:
    var s = composite(list_and_index)
    var pair = example(s)
    print(len(pair[0]), pair[1])

This is Hypothesis’s @composite. The values drawn inside f are shrunk together, so a failing (xs, i) shrinks to a short list and a small index that still fail.

Dependent generation

list_and_index is an example of dependent generation: the index’s range depends on the list. There are three ways to do it.

• composite, as above. The most flexible.

• flatmap(s, f): draw x from s, then a value from the strategy f(x):

  def lists_of_length(n: Int) raises -> Lists[Integers]:
      return lists(integers(), min_size=n, max_size=n)
  
  var square_lists = flatmap(integers(0, 5), lists_of_length)
  

• given_data, in the test itself; see below.

Mixing data generation and test code

given_data(test) passes the test the ConjectureData, so it can draw values in the middle of running (Hypothesis’s st.data()):

from std.testing import assert_true
from proptest import given_data, lists, integers, ConjectureData

def main() raises:
    def prop(mut data: ConjectureData) raises:
        var xs = data.draw(lists(integers(), min_size=1), "xs")
        var i = data.draw(integers(0, len(xs) - 1), "i")
        xs.append(xs[i])
        assert_true(xs[i] == xs[len(xs) - 1])

    given_data(prop)
    print("passed")

The label ("xs", "i") names the value in a failure report, which lists each draw. If the test instead failed whenever xs[i] > 5, the report would be:

Falsifying example (test.mojo:10:15):
    Draw 1 (xs): [6]
    Draw 2 (i): 0  # or any other generated value
too big

The comment comes from the explain phase: after shrinking, proptest checks which draws can vary without changing the failure. Use given_data when what to draw depends on what the code under test did. Otherwise, prefer given or composite, which keep generation separate from the test.

Writing a strategy struct

A strategy is any struct that conforms to the Strategy trait. It names the type it produces, Value, and implements do_draw:

from proptest import Strategy, ConjectureData, integers, example

@fieldwise_init
struct Point(Copyable, Writable):
    var x: Int
    var y: Int

struct Points(Copyable, Strategy):
    comptime Value = Point
    var limit: Int

    def __init__(out self, limit: Int):
        self.limit = limit

    def do_draw(self, mut data: ConjectureData) raises -> Point:
        var x = data.draw(integers(0, self.limit))
        var y = data.draw(integers(0, self.limit))
        return Point(x, y)

def main() raises:
    print(example(Points(10)))

Inside do_draw, draw from other strategies with data.draw(...), not by calling their do_draw directly: data.draw records the structure of the draw, which the shrinker uses. A strategy can also make primitive choices with data.draw_integer, data.draw_boolean and the like; see Writing strategies: the low-level API.

A struct is worth writing when the strategy has parameters you want to name, or when you want a strategy type that doesn’t mention closures. Otherwise composite is shorter.

Values must be printable

A strategy’s Value must be Movable and Writable, so that proptest can print failing examples. It doesn’t have to be Copyable: proptest rebuilds values from their choices rather than copying them, so move-only types such as unique handles work too. A few strategies that hand out the same value more than once (just, sampled_from, permutations, shared, set elements and dictionary keys) need Copyable values; lazy_just(f) makes a fresh value per test case instead.

Recursive data

recursive(base, extend) generates recursive structures such as trees or JSON-like values. base generates the leaves; extend receives a strategy for the whole recursive type and returns a strategy for one more level:

from proptest import recursive, lists, integers, boxed, map, example, BoxedStrategy

def leaf(x: Int) -> List[Int]:
    return [x]

def flatten(xss: List[List[Int]]) -> List[Int]:
    var out = List[Int]()
    for xs in xss:
        out.extend(xs.copy())
    return out^

def extend(inner: BoxedStrategy[List[Int]]) raises -> BoxedStrategy[List[Int]]:
    return boxed(map(lists(inner.copy(), max_size=3), flatten))

def main() raises:
    var s = recursive(map(integers(0, 9), leaf), extend, max_leaves=10)
    print(example(s))

Mojo structs can’t contain themselves directly, so recursive values are usually stored with indices into a list, or behind ArcPointer.

Strategies from types

Often the type of a value says most of what a test needs: a List[Int], a String, a struct of a few fields. proptest can derive a strategy from a type at compile time, and run a property whose inputs are drawn from its parameter types. This page covers from_type, Arbitrary, check, the constraint types, and build.

from_type

from_type[T]() is a strategy for values of type T:

from proptest import from_type, example

def main() raises:
    print(example(from_type[List[Tuple[Bool, Optional[Int8]]]]()))

It supports:

• integer scalars (Int, UInt8, …, Int128), Float64, Float32, Bool, and String;
• List, Optional, Set, Dict, and tuples of up to six elements, nested to any depth;
• any type that implements Arbitrary (below), including the constraint types;
• any other struct, built field by field, recursively.

The strategy is chosen at compile time, so an unsupported type is a compile error, not a run-time one.

Structs, field by field

A struct without an Arbitrary implementation is built by drawing each field with from_type, using Mojo’s reflection:

from proptest import from_type, example

@fieldwise_init
struct Point(Copyable, Writable):
    var x: UInt16
    var y: UInt16

@fieldwise_init
struct Sprite(Copyable, Writable):
    var position: Point
    var tags: List[String]
    var layer: Optional[Int8]

def main() raises:
    print(example(from_type[Sprite]()))

Each field is drawn in its own span, so failing structs shrink field by field. This bypasses the struct’s __init__: Mojo can reflect on a struct’s fields but not on its initializers. So a struct with invariants between its fields (lo <= hi, say) should implement Arbitrary instead.

Arbitrary: a type’s own strategy

A type that implements Arbitrary provides its own way to be drawn, with a static arbitrary method. from_type (and therefore check, and struct fields of this type) uses it:

from proptest import Arbitrary, ConjectureData, integers, from_type, example

@fieldwise_init
struct Interval(Arbitrary, Copyable, Writable):
    var lo: Int
    var hi: Int

    @staticmethod
    def arbitrary(mut data: ConjectureData) raises -> Self:
        var lo = data.draw(integers(-100, 100))
        return Self(lo, data.draw(integers(lo, 100)))

def main() raises:
    print(example(from_type[Interval]()))

This is Hypothesis’s register_type_strategy, attached to the type instead of registered at run time. For a type you don’t own, see Generate values of your own types.

check: properties over types

check(prop) draws each argument of prop with from_type, so the parameter types are the whole specification (Rust quickcheck’s quickcheck(prop)):

from proptest import check

def main() raises:
    def concat_length(a: List[Int], b: List[Int]) -> Bool:
        var c = a.copy()
        c.extend(b.copy())
        return len(c) == len(a) + len(b)

    check(concat_length)
    print("passed")

The property takes one to six arguments and can:

• raise on failure, like a given test;
• return Bool, where False is a failure;
• return an Outcome: Outcome.passed(), Outcome.discard() (like assume(False)), Outcome.fail("why"), or Outcome.of(condition, "why").

from proptest import check, Outcome

def main() raises:
    def division(a: Int8, b: Int8) -> Outcome:
        if b == 0:
            return Outcome.discard()
        var q = Int(a) // Int(b)
        return Outcome.of(q * Int(b) + Int(a) % Int(b) == Int(a), "a == q*b + r")

    check(division)
    print("passed")

Failures are reported like given’s; a Bool property that returns False reports check: the property returned False.

Constraint types

The plain types often say too little: a test might need a non-empty list, or a positive number. Constraint types put the constraint in the type (Haskell QuickCheck’s modifiers). Each implements Arbitrary, so it works with check, from_type, and struct fields; the underlying value is .value; and shrinking never breaks the constraint, because the value is always drawn through the constrained strategy.

from proptest import check, NonEmpty, NonNegative

def main() raises:
    def index_is_in_range(xs: NonEmpty[List[Int]], i: NonNegative[Int]) -> Bool:
        var k = i.value % len(xs.value)
        return xs.value[k] in xs.value

    check(index_is_in_range)
    print("passed")

Reports print the value without the wrapper. Constraints in types catch real bugs:

from proptest import check, NonZero

def main():
    def abs_is_positive(x: NonZero[Int8]) -> Bool:
        return abs(x.value) > 0

    try:
        check(abs_is_positive)
    except e:
        print(e)

Falsifying example (abs.mojo:8:14):
    given(-128)
check: the property returned False

Via: any strategy as a type

Via[f] names a draw function in a type, so any strategy can be a parameter type:

from proptest import check, Via, Positive, ConjectureData, lists, integers

def digits(mut data: ConjectureData) raises -> List[Int]:
    return data.draw(lists(integers(0, 9), max_size=4))

def main() raises:
    def prop(xs: Via[digits], n: Positive[UInt8]) -> Bool:
        for x in xs.value:
            if x < 0 or x > 9:
                return False
        return n.value > 0

    check(prop)
    print("passed")

When strategies depend on each other or on values only known at run time, use given with explicit strategies instead.

build: from_type with some fields given

build[T](field["name"](strategy), ...) builds a struct field by field, like from_type, but draws the named fields from the given strategies (RapidCheck’s gen::build, Hypothesis’s builds(Cls, name=strategy)):

from proptest import build, field, integers, text, just, example

@fieldwise_init
struct Person(Copyable, Writable):
    var name: String
    var age: Int
    var tags: List[Int]

def main() raises:
    var adults = build[Person](
        field["age"](integers(18, 99)),
        field["name"](text(min_size=1, max_size=10)),
    )
    print(example(adults))

The other fields (tags here) come from from_type. The field names, and the types of the strategies, are checked at compile time: a misspelled field, a field given twice, or a strategy of the wrong type fails to compile, with a message naming the field.

Configuring test settings

Settings controls how a test runs: how many examples to try, which random seed to use, where to save failures, and more. Hypothesis’s settings are a decorator with named profiles; proptest’s are a plain struct of keyword arguments, passed as the last argument of given, check, given_data, and the state machine runners.

Configuring a single test

from proptest import given, integers, Settings

def main() raises:
    def prop(x: Int) raises:
        pass

    given(integers(), prop, Settings(max_examples=500))
    print("passed")

Every field has a default, so you only name the ones you change.

Changing the number of test cases

max_examples (default 100) is the number of valid examples to try before the test passes. Raise it for important or subtle properties, lower it for slow ones:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    def prop(xs: List[Int]) raises:
        pass

    given(lists(integers()), prop, Settings(max_examples=5000))

The test may run more or fewer times than max_examples; see How many times will proptest run my test?

Other settings

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var settings = (
Settings(
    max_examples=500,                # valid examples to try
    seed=UInt64(1234),               # fixed seed (or derandomize=True)
    database=None,                   # don't save failures
    phases=Phases(shrink=False),     # skip shrinking
    verbosity=Verbosity.verbose,     # say what the run is doing
    report_multiple_bugs=False,      # stop at the first distinct failure
    suppress_health_check=[HealthCheck.filter_too_much],
    deadline=500.0,                  # ms per example (default 200; None disables)
    print_blob=True,                 # print a blob for reproduce=
    show_statistics=True,            # print events, tables and coverage
)
    )
    def prop(x: Int) raises:
        pass
    given(integers(), prop, settings)

The most useful:

• seed fixes the random seed, so a run is repeatable. derandomize=True derives the seed from the test’s identity instead, so every run of the test tries the same examples.

• database is the directory where failing examples are saved (default .proptest/examples); None disables it. See Replaying failures.

• deadline fails any example whose test body takes longer than this many milliseconds (time spent generating the data isn’t counted). It catches accidental slowness; set it to None for tests that are expected to be slow.

• verbosity: Verbosity.quiet, normal, verbose, or debug. Verbose output reports each run’s counts and seed, and prints the statistics and a reproduce blob with every failure:

  proptest: test.mojo:8:14: 3 valid, 0 invalid, 0 overrun examples in 10 calls (seed 17430662364796405847)
  proptest: first failure at call 2; shrinking
  

• phases turns phases of the run on or off: explicit, reuse, generate, target, shrink, and explain. For example, Phases(explain=False) skips the explain phase, which can be slow for tests with many arguments.

• report_multiple_bugs (default True): when a run finds failures with different causes, report them all. A failure’s cause is where its error was raised; see How proptest works.

• stateful_step_count (default 50): the maximum number of steps in a stateful test.

The settings reference lists every setting.

Changing settings across a test suite

proptest has no global settings profiles (Mojo has no global variables for a library to keep them in). Two things replace them.

The first is the environment. These variables change any setting that a test leaves at its default, much like loading a Hypothesis profile:

A value set explicitly in the code wins over the environment. For example, a CI job might run every test with more examples and without the database:

PROPTEST_MAX_EXAMPLES=1000 PROPTEST_DATABASE=none mojo run -I . tests/test_parser.mojo

The second is an ordinary function. A test suite can define its own defaults and pass them to every test:

from std.testing import assert_true, assert_equal
from proptest import *
def suite_settings() -> Settings:
    return Settings(max_examples=300, deadline=None)

def main() raises:
    def prop(x: Int) raises:
        pass

    given(integers(), prop, suite_settings())

Replaying failures

When a test fails, you want the failure to keep happening until you’ve fixed it, and you want to be able to rerun exactly the failing input. proptest has three tools for this: the example database, explicit examples, and reproduce blobs.

The example database

When a test fails, proptest saves the shrunk failing example in the example database: a directory, by default .proptest/examples under the working directory. The next time the test runs, proptest tries the saved examples first (the reuse phase). So a failure doesn’t disappear on the next run just because the random search went somewhere else. Once a saved example passes, it’s deleted.

Each test’s examples are kept under a key, which given and check take from the test’s source location (file:line:column). Moving a test to another line changes its key, and its saved examples are no longer found. To keep them, give the test a fixed key with Settings(database_key="parser round trip").

What’s saved is the example’s choice sequence: the choices the strategies made, one per line, not the value itself. It replays through whatever strategies the test uses now. So if you change the test’s strategies, a saved example may turn into a different value, or become invalid and be dropped.

Disabling the database

Pass Settings(database=None), or set PROPTEST_DATABASE=none in the environment to disable it for every test that uses the default. A test suite’s runner might do this in CI, where nothing is kept between runs anyway. You can also add .proptest/ to .gitignore.

Explicit examples

check_examples(examples, test) runs a test on specific inputs (Hypothesis’s @example). Use it for inputs that must always be tested, such as a regression from a bug report or a known edge case:

from proptest import check_examples, given, integers

def main():
    def small(x: Int) raises:
        if x > 100:
            raise Error("too big")

    try:
        check_examples([1, 5, 500], small)
    except e:
        print(e)

Falsifying explicit example (example.mojo:9:23):
    example(500)
too big

Explicit examples are not shrunk: the input is the one you gave.

Prefer explicit examples to the database for important cases

The database is a cache, not a test suite: a saved example is lost when the test’s strategies or location change, and it isn’t shared through version control. When a failure matters enough that it must never come back, add it as an explicit example.

Replaying a test case with reproduce

With Settings(print_blob=True), or verbose output, a failure report ends with a line like this:

Falsifying example (test.mojo:20:14):
    given(101)
    To reproduce this example, run the test with Settings(reproduce="proptest1:aToxMDEK")
too big

Running the test with Settings(reproduce="proptest1:aToxMDEK") replays exactly that example, without any search or shrinking (Hypothesis’s @reproduce_failure). The blob is the encoded choice sequence, so it’s small enough to paste into a bug report. Like a database entry, it only reproduces the failure while the test’s strategies stay the same.

Repeating a run with a seed

Verbose output also prints the run’s random seed. Settings(seed=...) or PROPTEST_SEED=... repeats the whole run, including the examples that passed. Settings(derandomize=True) makes every run of a test use the same seed, derived from its key.

Sharing failures

The database is a directory of small text files, so you can copy it between machines, or point several checkouts at one directory with PROPTEST_DATABASE=/shared/path. Keys are source locations, so the checkouts should be at the same version of the tests.

Stopping on the minimal example in a debugger

proptest calls before_minimal_test_case(name) just before it replays a shrunk failure for the last time. Set a breakpoint on it to stop only on the minimal failing example; see Debug a failing test.

Adding notes and statistics

A failure report shows the inputs. Sometimes you also want to see values the test computed from them, or to know what kinds of input the test saw over a whole run. This page covers notes, events, and run statistics.

Notes

data.note(message) adds a line to the failure report. Notes are only printed for the final, shrunk example, so they don’t clutter the output while proptest searches. Notes need the ConjectureData, so use them from given_data tests, composite strategies, or state machine rules:

from proptest import given_data, integers, ConjectureData, Settings

def main():
    def prop(mut data: ConjectureData) raises:
        var x = data.draw(integers(0, 1000), "x")
        data.note(String("x squared is ", x * x))
        if x > 100:
            raise Error("too big")

    try:
        given_data(prop, Settings(database=None))
    except e:
        print(e)

Falsifying example (notes.mojo:10:19):
    Draw 1 (x): 101
    x squared is 10201
too big

In a given test, you can put the same information in the error message instead: std.testing assertions take a message argument.

Statistics

Settings(show_statistics=True) prints a summary of what the test saw during the generate phase (Hypothesis’s --hypothesis-show-statistics). Verbose output includes it too. Three things feed it.

• Events: data.event(label) records that something happened in this test case. The statistics show the share of test cases that recorded each event.
• Tables: data.tabulate(table, value) (from QuickCheck) records a value in a named table. The statistics show how often each value occurred.
• Coverage requirements: data.cover(percent, condition, label) (from QuickCheck) says that at least percent% of test cases should satisfy condition.

from proptest import given_data, lists, integers, ConjectureData, Settings

def main() raises:
    def prop(mut data: ConjectureData) raises:
        var xs = data.draw(lists(integers(0, 9)))
        data.event("empty" if len(xs) == 0 else "non-empty")
        data.tabulate("length", String(min(len(xs), 3)))
        data.cover(30, len(xs) >= 2, "two or more")

    given_data(prop, Settings(database=None, show_statistics=True))

proptest statistics for stats.mojo:10:15:
  - 99 passing, 0 invalid and 19 overrun examples (generate phase)
  - Events:
    * 83.90%, non-empty
  - length (99 values):
    * 85.86%, 3
    * 9.09%, 2
    * 5.05%, 1
  - Coverage:
    * 94.95% two or more (required 30.0%)

Event percentages are of all test cases, including invalid and overrun ones; table percentages are of the values recorded.

The statistics can be surprising. Here no empty list appears, because proptest tries the simplest input first (an empty list, before the generate phase) and never runs an identical input twice. And 19 test cases were “overrun”: early in a run, proptest keeps test cases small, and abandons ones that grow too large. That’s why it’s worth looking at the statistics when you write a new strategy.

Statistics for given and check tests

given and check tests have no data. The strategy wrappers tabulate(s, table, key) and cover(s, percent, label, condition) record the same statistics for each value a strategy produces:

from proptest import given, cover, tabulate, lists, integers, Settings

def bucket(xs: List[Int]) -> String:
    return "short" if len(xs) < 5 else "long"

def main() raises:
    def prop(xs: List[Int]) raises:
        pass

    var xs = tabulate(
        cover(lists(integers()), 20, "long", lambda (xs: List[Int]) -> Bool: len(xs) >= 5),
        "size",
        bucket,
    )
    given(xs, prop, Settings(database=None, show_statistics=True))

Coverage requirements

An unmet cover requirement prints a warning. To make it a test failure, checked with a statistical test so that it fails only when the coverage is really too low, use Settings(check_coverage=Confidence()). See Check the distribution of inputs.

Statistics in code

The statistics are also available as data: run_test and run_property return a RunReport, whose statistics field holds the counts, events, tables, and coverage.

Flaky failures

A test is flaky if it can pass or fail on the same input. Property-based testing relies on replaying inputs: to shrink a failure, proptest runs the test again on simpler variations of the input, and to report it, runs the shrunk input once more. If the test’s outcome depends on something other than its input, none of that works.

Why flakiness is bad

When a test fails only sometimes, the shrinker gets misleading answers: a simpler input appears to pass because the flaky condition didn’t happen, not because the input avoids the bug. The reported example may not fail when you try it, and the database replays an example that doesn’t reproduce.

Common sources of flakiness

• The clock: timeouts, measurements, anything that depends on how fast the code runs.
• Randomness not drawn through proptest, such as a random generator seeded from the time.
• External state: files, the network, environment variables.
• State left over between test cases: a captured mutable variable, a cache, or a global resource that one test case changes and the next one sees.

Draw every random choice through proptest (data.draw, or a strategy), and reset state at the start of each test case.

Kinds of flakiness proptest detects

A failure that doesn’t reproduce

After shrinking, proptest runs the minimal example one last time to collect its report. If it passes, proptest says so:

Flaky: the falsifying example did not fail when replayed

A deadline failure that passes on replay is reported as a flaky deadline: an example exceeded the deadline once, but not again. For timing-sensitive tests, disable the deadline (deadline=None) or raise it.

Inconsistent data generation

proptest records the choices each test case makes in a tree, so that it doesn’t run the same input twice. If replaying a choice sequence makes different kinds of choice than before, the strategies themselves aren’t deterministic, and proptest raises:

FlakyStrategyDefinition: Inconsistent data generation! Data generation behaved differently
between different runs (...). Is the strategy or test depending on external state, such as
a captured mutable variable or the clock?

The usual cause is a strategy or given_data test that decides what to draw from something other than earlier draws: a counter captured by the closure, or the time.

Stateful testing

So far, each test has checked a function on one input. Many bugs only show up after a particular sequence of operations: add, add, remove, then look up. Stateful testing generates whole programs, sequences of operations against the system under test, and shrinks a failing program to the shortest, simplest sequence that still fails.

proptest has three ways to write a stateful test:

• StateMachine: numbered rules, as in Hypothesis’s RuleBasedStateMachine. Covered on this page.
• TypedStateMachine: each step is a value of a Transition type, as in Rust’s proptest-state-machine. Also covered on this page.
• Commands: model-based testing with one struct per operation, as in RapidCheck and Erlang QuickCheck. Covered in Model-based testing.

A rule-based state machine

Here is a set that loses elements under some conditions:

from std.testing import assert_true
from proptest import ConjectureData, integers, Settings
from proptest.stateful import StateMachine, run_state_machine_as_test

struct BuggySet(Movable):
    var items: List[Int]

    def __init__(out self):
        self.items = []

    def add(mut self, x: Int):
        if x > 10 and len(self.items) >= 2:
            return  # bug: silently drops the element
        for y in self.items:
            if y == x:
                return
        self.items.append(x)

    def contains(self, x: Int) -> Bool:
        for y in self.items:
            if y == x:
                return True
        return False

struct SetMachine(StateMachine):
    var real: BuggySet
    var model: List[Int]

    def __init__(out self):
        self.real = BuggySet()
        self.model = []

    def rule_count(self) -> Int:
        return 2

    def rule_name(self, rule: Int) -> String:
        return "add" if rule == 0 else "check"

    def precondition(self, rule: Int) -> Bool:
        return rule == 0 or len(self.model) > 0

    def run_rule(mut self, rule: Int, mut data: ConjectureData) raises:
        if rule == 0:
            var x = data.draw(integers(0, 100), "x")
            self.real.add(x)
            if x not in self.model:
                self.model.append(x)
        else:
            var i = data.draw(integers(0, len(self.model) - 1), "i")
            assert_true(self.real.contains(self.model[i]), "element went missing")

def main():
    try:
        run_state_machine_as_test[SetMachine](Settings(database=None))
    except e:
        print(e)

Falsifying example (set.mojo:54:46):
    state = SetMachine()
    state.add(x=0)
    state.add(x=1)
    state.add(x=11)
    state.check(i=2)
    state.teardown()
At set.mojo:50:24: AssertionError: element went missing

The machine holds the system under test (real) and a model of what its state should be (model, a plain list). Each step:

1. picks a rule whose precondition holds;
2. calls run_rule, which draws the rule’s arguments with data.draw(strategy, "name"), applies the operation to both the system and the model, and checks that they agree;
3. calls check_invariants.

The failure is printed as the program that caused it, with each rule’s arguments named by their labels. proptest found some long program first, then shrank it to the essential steps: two small elements, then a large one, then a lookup.

Hypothesis finds rules by looking for methods decorated with @rule. Mojo has no decorators or method reflection, so a Mojo state machine numbers its rules: rule_count says how many there are, rule_name names them for reports, and run_rule dispatches on the number.

Invariants

check_invariants runs after the machine is created and after every step. Use it for properties that should always hold, whatever the last operation was. The Die Hard example uses an invariant to solve the water jug puzzle from the film: it claims that the 5-gallon jug never holds exactly 4 gallons, and proptest finds and shrinks a sequence of pours that refutes it:

state = DieHard()
state.fill_big()
state.pour_big_into_small()
state.empty_small()
state.pour_big_into_small()
state.fill_big()
state.pour_big_into_small()
state.teardown()

Passing values between steps: bundles

Sometimes one step creates a value that later steps use: a handle returned by open, a key inserted earlier. A Bundle[T] collects such values (Hypothesis’s Bundle):

from proptest import ConjectureData, Settings, Bundle, fail
from proptest.stateful import StateMachine, run_state_machine_as_test

struct Files(Movable):
    var open_handles: List[Int]
    var next: Int

    def __init__(out self):
        self.open_handles = []
        self.next = 0

    def open(mut self) -> Int:
        self.next += 1
        self.open_handles.append(self.next)
        return self.next

    def close(mut self, h: Int) raises:
        for i in range(len(self.open_handles)):
            if self.open_handles[i] == h:
                _ = self.open_handles.pop(i)
                return
        fail(String("closed handle ", h, " twice"))

struct HandleMachine(StateMachine):
    var system: Files
    var handles: Bundle[Int]

    def __init__(out self):
        self.system = Files()
        self.handles = Bundle[Int]("handles")

    def rule_count(self) -> Int:
        return 2

    def rule_name(self, rule: Int) -> String:
        return "open" if rule == 0 else "close"

    def precondition(self, rule: Int) -> Bool:
        return rule == 0 or len(self.handles) > 0

    def run_rule(mut self, rule: Int, mut data: ConjectureData) raises:
        if rule == 0:
            self.handles.add(self.system.open())
        else:
            var h = self.handles.consume(data)   # draw(data) would keep it
            self.system.close(h)

def main() raises:
    run_state_machine_as_test[HandleMachine](Settings(database=None))

draw picks one of the values, shrinking towards the most recently added; consume also removes it. The rule’s precondition must make sure the bundle isn’t empty. In reports, a drawn value is printed with the bundle’s name, such as state.use(values[0]=500).

Initialize rules and teardown

initialize_count and run_initialize define rules that run exactly once each, before any ordinary rule, in a random order (Hypothesis’s @initialize). teardown runs at the end of every program, even a failing one, for releasing resources.

Swarm testing

In each test case, proptest disables a random subset of the rules, as Hypothesis does. A program that only adds and never removes, say, is much more likely than it would be if every step chose uniformly among all the rules, and such lopsided programs find bugs that balanced ones miss.

Settings for stateful tests

run_state_machine_as_test[M](settings) takes the usual Settings. stateful_step_count (default 50) is the maximum number of steps per program, and max_examples is the number of programs. The deadline applies to each step separately.

Typed state machines

A TypedStateMachine replaces rule numbers with values (Rust’s proptest-state-machine). Each step draws a transition, a value of the associated Transition type, from the current state, then applies it. A Variant with one struct per operation works well:

from std.testing import assert_true
from std.utils import Variant
from proptest import ConjectureData, integers, booleans, Settings
from proptest import TypedStateMachine, run_typed_state_machine_as_test

struct BuggySet(Movable):
    var items: List[Int]

    def __init__(out self):
        self.items = []

    def add(mut self, x: Int):
        if x > 10 and len(self.items) >= 2:
            return  # bug: silently drops the element
        if x not in self.items:
            self.items.append(x)

    def contains(self, x: Int) -> Bool:
        return x in self.items

@fieldwise_init
struct Add(Copyable, Writable):
    var x: Int

@fieldwise_init
struct Check(Copyable, Writable):
    var i: Int

struct TypedSetMachine(TypedStateMachine):
    comptime Transition = Variant[Add, Check]
    var real: BuggySet
    var model: List[Int]

    def __init__(out self):
        self.real = BuggySet()
        self.model = []

    def transition(self, mut data: ConjectureData) raises -> Self.Transition:
        # only valid transitions: Check needs an element to look up
        if len(self.model) == 0 or not data.draw(booleans()):
            return Add(data.draw(integers(0, 100)))
        return Check(data.draw(integers(0, len(self.model) - 1)))

    def apply(mut self, t: Self.Transition) raises:
        if t.isa[Add]():
            var x = t[Add].x
            self.real.add(x)
            if x not in self.model:
                self.model.append(x)
        else:
            assert_true(
                self.real.contains(self.model[t[Check].i]), "element went missing"
            )

def main():
    try:
        run_typed_state_machine_as_test[TypedSetMachine](Settings(database=None))
    except e:
        print(e)

Falsifying example (typed.mojo:57:57):
    state = TypedSetMachine()
    state.apply(Add(x=0))
    state.apply(Add(x=1))
    state.apply(Add(x=11))
    state.apply(Check(i=2))
    state.teardown()
At typed.mojo:51:24: AssertionError: element went missing

Transitions are printed through Writable. transition should draw only transitions that are valid in the current state. When the shrinker deletes a step, the later steps are drawn again in the new state, so they stay valid. An optional precondition(t) rejects a transition instead; after three rejections in a row, the program ends at that step. check_invariants and teardown work as for StateMachine. There’s no swarm testing, because the runner can’t tell kinds of transition apart.

Which to choose

• StateMachine has bundles, initialize rules, and swarm testing, and reads like Hypothesis’s rule-based machines.
• TypedStateMachine makes operations values with types, and is compact when the operations are simple.
• Commands (next page) give each operation its own struct, with the model kept separate from the system under test. They suit larger systems, and testing several implementations against one model.

Model-based testing

Model-based testing (from RapidCheck’s rc::state and Erlang QuickCheck) separates three things that a state machine mixes together:

• the model: a simple value describing the state the system should be in, such as a Dict standing in for a database;
• the system under test (the SUT);
• the commands: one struct per operation, each knowing how to generate itself from the model, how it changes the model, and how to run it on the system and check the result.

Because commands are generated from the model alone, proptest can generate a whole program without touching the system, then run it. The program is a value: you can print it, run it on two implementations, or run it inside an ordinary property that sets up the system however it likes.

Commands

A command implements the Command trait. It names the Model and Sut types, and provides:

• generate(model, data): a static method that draws a command valid in the model’s current state;
• precondition(model) (optional): whether the command may run in this state;
• next_state(mut model) (optional): apply the command to the model;
• run(model, mut sut) (optional): apply the command to the system and check the result. model is the state before the command;
• write_to, to print the command in reports.

Here is a key-value store with a bug: once it has held three keys, it ignores overwrites.

from std.testing import assert_true, assert_equal, assert_false
from proptest import (
    Command, Commands, commands, given, integers, sampled_from,
    ConjectureData, Settings,
)

struct KvStore(Defaultable, Movable):
    var keys: List[Int]
    var values: List[Int]
    var peak: Int

    def __init__(out self):
        self.keys = []
        self.values = []
        self.peak = 0

    def put(mut self, k: Int, v: Int):
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                if self.peak < 3:  # BUG: overwrites ignored after 3 keys
                    self.values[i] = v
                return
        self.keys.append(k)
        self.values.append(v)
        self.peak = max(self.peak, len(self.keys))

    def get(self, k: Int) -> Optional[Int]:
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                return self.values[i]
        return None

    def remove(mut self, k: Int):
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                _ = self.keys.pop(i)
                _ = self.values.pop(i)
                return

comptime KvModel = Dict[Int, Int]

@fieldwise_init
struct Put(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int
    var value: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        return Self(data.draw(integers(0, 9)), data.draw(integers(0, 9)))

    def next_state(self, mut model: KvModel) raises:
        model[self.key] = self.value

    def run(self, model: KvModel, mut sut: KvStore) raises:
        sut.put(self.key, self.value)

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Put(", self.key, ", ", self.value, ")")

@fieldwise_init
struct Get(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        var keys = List[Int]()
        for k in model.keys():
            keys.append(k)
        if len(keys) == 0:
            return Self(0)  # rejected by the precondition
        return Self(data.draw(sampled_from(keys^)))

    def precondition(self, model: KvModel) raises -> Bool:
        return self.key in model

    def run(self, model: KvModel, mut sut: KvStore) raises:
        var got = sut.get(self.key)
        assert_true(Bool(got), "key missing")
        assert_equal(got.value(), model[self.key])

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Get(", self.key, ")")

@fieldwise_init
struct Remove(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        return Self(data.draw(integers(0, 9)))

    def next_state(self, mut model: KvModel) raises:
        _ = model.pop(self.key, 0)

    def run(self, model: KvModel, mut sut: KvStore) raises:
        sut.remove(self.key)
        assert_false(Bool(sut.get(self.key)))

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Remove(", self.key, ")")

def main():
    def prop(program: Commands[Put, Get, Remove]) raises:
        var store = KvStore()
        program.run(KvModel(), store)

    try:
        given(commands[Put, Get, Remove](KvModel()), prop, Settings(database=None))
    except e:
        print(e)

Falsifying example (kv.mojo:114:14):
    given([Put(0, 1), Put(1, 0), Put(2, 0), Put(0, 0), Get(0)])
At kv.mojo:83:21: AssertionError: `left == right` comparison failed:
   left: 1
  right: 0

The shrunk program is a minimal one: three distinct keys, an overwrite, and a read of the overwritten key. (Which key is overwritten, and with which value, can vary between runs; the shape doesn’t.)

Programs

commands[Put, Get, Remove](model) is a strategy for programs: values of type Commands[Put, Get, Remove], valid when run from the state model. It takes optional weights=[...], to choose some command types more often than others, and max_commands (default 50).

A program runs with program.run(model, sut), which runs each command on the system and updates a copy of the model as it goes. Because this happens inside an ordinary property, the property can:

• generate the initial state with other strategies, and build the system and model to match;
• use a fixture, such as a temporary directory or a connection;
• test two implementations against each other: run the same program on both, and compare them.

from std.testing import assert_true, assert_equal, assert_false
from proptest import (
    Command, Commands, commands, given, integers, sampled_from,
    ConjectureData, Settings,
)

struct KvStore(Defaultable, Movable):
    var keys: List[Int]
    var values: List[Int]
    var peak: Int

    def __init__(out self):
        self.keys = []
        self.values = []
        self.peak = 0

    def put(mut self, k: Int, v: Int):
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                if self.peak < 3:  # BUG: overwrites ignored after 3 keys
                    self.values[i] = v
                return
        self.keys.append(k)
        self.values.append(v)
        self.peak = max(self.peak, len(self.keys))

    def get(self, k: Int) -> Optional[Int]:
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                return self.values[i]
        return None

    def remove(mut self, k: Int):
        for i in range(len(self.keys)):
            if self.keys[i] == k:
                _ = self.keys.pop(i)
                _ = self.values.pop(i)
                return

comptime KvModel = Dict[Int, Int]

@fieldwise_init
struct Put(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int
    var value: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        return Self(data.draw(integers(0, 9)), data.draw(integers(0, 9)))

    def next_state(self, mut model: KvModel) raises:
        model[self.key] = self.value

    def run(self, model: KvModel, mut sut: KvStore) raises:
        sut.put(self.key, self.value)

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Put(", self.key, ", ", self.value, ")")

@fieldwise_init
struct Get(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        var keys = List[Int]()
        for k in model.keys():
            keys.append(k)
        if len(keys) == 0:
            return Self(0)  # rejected by the precondition
        return Self(data.draw(sampled_from(keys^)))

    def precondition(self, model: KvModel) raises -> Bool:
        return self.key in model

    def run(self, model: KvModel, mut sut: KvStore) raises:
        var got = sut.get(self.key)
        assert_true(Bool(got), "key missing")
        assert_equal(got.value(), model[self.key])

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Get(", self.key, ")")

@fieldwise_init
struct Remove(Command):
    comptime Model = KvModel
    comptime Sut = KvStore
    var key: Int

    @staticmethod
    def generate(model: KvModel, mut data: ConjectureData) raises -> Self:
        return Self(data.draw(integers(0, 9)))

    def next_state(self, mut model: KvModel) raises:
        _ = model.pop(self.key, 0)

    def run(self, model: KvModel, mut sut: KvStore) raises:
        sut.remove(self.key)
        assert_false(Bool(sut.get(self.key)))

    def write_to(self, mut writer: Some[Writer]):
        writer.write("Remove(", self.key, ")")
comptime FastKvStore = KvStore

def prop(program: Commands[Put, Get, Remove]) raises:
    var a = KvStore()
    var b = FastKvStore()
    program.run(KvModel(), a)
    program.run(KvModel(), b)
    for k in range(10):
        assert_true(a.get(k) == b.get(k))

def main() raises:
    try:  # this page's KvStore has the bug, so Get's check fails
        given(commands[Put, Get, Remove](KvModel()), prop, Settings(database=None))
    except e:
        print(e)

program.apply_all(model) applies a program to a model only, and program.is_valid(model) checks every precondition along the way (RapidCheck’s applyAll and isValidSequence).

Shortcuts

• check_commands[Put, Get, Remove](model, settings) runs programs on a fresh, default-constructed system for each test case: the whole test above, for a Sut that is Defaultable.
• run_commands[Put, Get, Remove](model, sut, data) draws a program and runs it, inside a given_data test.

How programs shrink

A program is generated like a list: each command is drawn after a “keep going” choice, so the shrinker can delete commands. When it deletes or simplifies one, the later commands are generated again from the same choices, in the new model state, so a shrunk program is always valid. RapidCheck re-checks preconditions while shrinking for the same reason.

There’s one limitation. A command that picks a value out of the model, like Get choosing among the keys the model holds, is coupled to the earlier steps: deleting an earlier Put changes which key the same choice picks. Shrinking can then stop a step or two short of minimal. When rejections would be rare, drawing the value directly (integers(0, 9)) and rejecting invalid ones with precondition shrinks better.

Compared with state machines

Model-based testing and TypedStateMachine can express the same tests. Commands keep each operation’s generation, model update, and checks together in one struct, rather than in an isa chain, and the whole program exists before it runs. State machines draw each step from the current state of the system itself, which is simpler when there’s no separate model.

A complete example

examples/lru_cache.mojo tests an LRU cache (LeetCode 146) against a model that keeps its entries in a plain list, most recently used first. Each test case draws the cache’s capacity, then a program of put and get commands, and after the program compares the cache’s recency order with the model’s.

examples/lru_cache_pointers.mojo is the same cache built from heap-allocated nodes and raw pointers. Its commands also check the list’s links after every step, and building it with --sanitize address checks for leaks and use after free.

examples/dancing_links.mojo is Knuth’s Dancing Links, an exact cover solver whose nodes are linked by raw pointers in four directions, extended to his Algorithm C, where options can give secondary items colors and share them when the colors agree. Its Cover, Purify, and Undo commands check every column, and every node’s color, against a model after each step, and when everything has been undone they check that every link and color is back where it started.

examples/xor_list.mojo is an XOR linked list: each node stores the XOR of its neighbors’ addresses, so the same code walks it either way, and reversing it is swapping its head and tail. Its commands walk the list in both directions after every step and compare it with a List.

examples/splay_tree.mojo is a splay tree whose nodes link to their parents as well as their children. Its commands check every link, the key order, and the subtree sizes after each step, and compare the tree with a sorted list. A splay that moves a node to the root one rotation at a time still gives the right answers, only slowly, so the tree also checks the access lemma of Sleator and Tarjan’s analysis after every splay, and a second property checks that accessing every key in order takes at most 4.5 n rotations.

examples/red_black_tree.mojo is a red-black tree that, like the Linux kernel’s, stores each node’s color in the low bit of its parent pointer. After each command it checks the red-black rules, that every parent link points back and holds no stray bits, and that the height is at most 2 log2(n + 1).

examples/intrusive_list.mojo is an intrusive list in the Linux kernel’s style: the links are fields of the tasks themselves, so a task can be on two lists at once, and container_of recovers a task from its link by subtracting the field’s offset, reflect[Task].field_offset[name="ready_link"](). A scheduler’s commands (spawn, wake, block, run, kill, …) are checked against two plain lists of ids, walking both rings both ways after every step.

examples/free_list_allocator.mojo is a malloc-style allocator inside one arena. Its free blocks hold the free list’s pointers in their own payload bytes, and boundary tags let free merge neighbors. The model is the same allocator written over plain lists of integers, so it predicts every address; the commands also check every boundary tag and that each live allocation still holds the bytes written to it, which catches what AddressSanitizer can’t see inside the arena.

examples/cheney_gc.mojo is Cheney’s copying garbage collector: two semispaces of raw words, tagged integers and pointers, and forwarding addresses written over old headers. The model is a plain object graph that also replays Cheney’s breadth-first copy order, so it predicts where every object ends up and which allocations trigger a collection. After each command the heap reachable from the roots must be isomorphic to the model’s graph, with shared objects and cycles mapped one to one.

examples/union_find.mojo is a union-find forest of heap-allocated nodes with path compression and union by rank, checked against a naive partition. After every command it checks that ranks increase toward each root and that every tree is no taller than its rank, which is at most log2 of its size. Random commands seldom build deep trees, so a second property builds union by rank’s worst case, a binomial tree, and checks that a find compresses its whole path.

examples/skip_list.mojo is a skip list with spans, as in Redis’s sorted sets, so it answers rank and select queries too. Each node is one raw allocation sized for its number of links, with its String value written into the raw bytes. The test case draws each node’s level instead of leaving it to a random number generator, so shrinking reaches levels too, and the model (a sorted list of keys, values, and levels) determines every lane and every span, which the commands check after each step.

Generate values of your own types

There are several ways to generate values of a struct. Which to use depends on whether the struct has invariants, whether you own it, and whether one strategy fits every test.

A struct without invariants: nothing to do

If any combination of field values is valid, from_type[T]() (and check) already handles it, by drawing each field with from_type:

from std.testing import assert_true, assert_equal
from proptest import *
@fieldwise_init
struct Color(Copyable, Writable):
    var r: UInt8
    var g: UInt8
    var b: UInt8

def main() raises:
    def prop(c: Color) -> Bool:
        return Int(c.r) + Int(c.g) + Int(c.b) <= 765

    check(prop)   # prop(c: Color) -> Bool

A struct with invariants: implement Arbitrary

Building from fields bypasses __init__, so it can produce values that the constructor would reject. Give such a type its own strategy by implementing Arbitrary:

from proptest import Arbitrary, ConjectureData, integers, check

@fieldwise_init
struct Interval(Arbitrary, Copyable, Writable):
    var lo: Int
    var hi: Int

    @staticmethod
    def arbitrary(mut data: ConjectureData) raises -> Self:
        var lo = data.draw(integers(-100, 100))
        return Self(lo, data.draw(integers(lo, 100)))

def main() raises:
    def prop(i: Interval) -> Bool:
        return i.lo <= i.hi

    check(prop)
    print("passed")

Draw in an order that makes later choices depend on earlier ones (hi is drawn after lo, from lo up), rather than drawing freely and filtering. Values built this way shrink well: here, towards lo == hi == 0.

Some fields need particular strategies: build

When the default for most fields is fine but a few need constraints, use build and name the fields:

from std.testing import assert_true, assert_equal
from proptest import *
@fieldwise_init
struct Person(Copyable, Writable):
    var name: String
    var age: Int
    var email: String

def main() raises:
    var people = build[Person](
        field["age"](integers(0, 120)),
        field["email"](from_regex("[a-z]+@example\\.com", fullmatch=True)),
    )
    print(example(people))

Field names and the strategies’ types are checked at compile time.

A type you don’t own

You can’t add Arbitrary to a type from another package. (Mojo’s struct extensions can’t currently satisfy a trait method that returns Self from another module.) Instead:

• Wrap it. A small struct implementing Arbitrary, holding the value, works with check and from_type, like proptest’s own constraint types:

  struct AnyCelsius(Arbitrary, Copyable, Writable):
      var value: Celsius
  
      def __init__(out self, var value: Celsius):
          self.value = value^
  
      @staticmethod
      def arbitrary(mut data: ConjectureData) raises -> Self:
          return Self(Celsius(data.draw(floats(-273.15, 1000.0))))
  
      def write_to(self, mut writer: Some[Writer]):
          writer.write(self.value)
  

• Name a draw function in the type with Via[f]: def prop(c: Via[draw_celsius]) -> Bool.

• Use an explicit strategy with given, built with apply, composite, or a strategy struct.

Several strategies for one type

Arbitrary gives a type one canonical strategy. When different tests need different kinds of value (small and large, valid and invalid), write strategy functions, and pass them to given:

from std.testing import assert_true, assert_equal
from proptest import *
@fieldwise_init
struct Interval(Copyable, Writable):
    var lo: Int
    var hi: Int

def draw_small(mut data: ConjectureData) raises -> Interval:
    var lo = data.draw(integers(-10, 10))
    return Interval(lo, data.draw(integers(lo, 10)))

def draw_huge(mut data: ConjectureData) raises -> Interval:
    var lo = data.draw(integers())
    return Interval(lo, data.draw(integers(lo)))

def small_intervals() -> BoxedStrategy[Interval]:
    return boxed(composite(draw_small))

def huge_intervals() -> BoxedStrategy[Interval]:
    return boxed(composite(draw_huge))

def main() raises:
    def ordered(i: Interval) raises:
        assert_true(i.lo <= i.hi)

    given(small_intervals(), ordered, Settings(database=None))
    given(huge_intervals(), ordered, Settings(database=None))

A function returning a strategy has to spell the strategy’s type. For strategies built with closures, that type is long; boxed(...) hides it behind BoxedStrategy[Interval], at the cost of an indirect call per draw. A strategy struct (see Custom strategies) gives a short, named type and can take parameters.

Make the type printable

Every generated value must be Writable, so failures can show it. For a @fieldwise_init struct whose fields are all Writable, declaring the conformance is enough: Mojo provides write_to, which prints Interval(lo=0, hi=0). Write your own write_to when a shorter form reads better in reports.

Check the distribution of inputs

A property test can pass because the property holds, or because the strategies never produce the inputs that would break it. A strategy for “lists” that almost always makes short lists, or a filter that rejects every interesting value, makes a test that passes and checks little. Coverage requirements (from QuickCheck’s cover and checkCoverage) state what the inputs should include, and fail the test when they don’t.

Declare a requirement

In a given_data test, data.cover(percent, condition, label) requires that at least percent% of test cases satisfy condition:

from std.testing import assert_true, assert_equal
from proptest import *
def prop(mut data: ConjectureData) raises:
    var xs = data.draw(lists(integers()))
    data.cover(20, len(xs) >= 5, "long")

def main() raises:
    given_data(prop, Settings(database=None, verbosity=Verbosity.quiet))

For given and check tests, wrap the strategy instead:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    def prop(xs: List[Int]) raises:
        pass

    var xs = cover(lists(integers()), 20, "long", lambda (xs: List[Int]) -> Bool: len(xs) >= 5)
    given(xs, prop)

By default, an unmet requirement prints a warning after the run:

proptest: test.mojo:13:10: only 10.10% above 90 (in 99 examples), but expected 50.0%

Make it a failure: check_coverage

With Settings(check_coverage=Confidence()), an unmet requirement fails the test. A coverage check is statistical: with 100 examples, a condition that holds 22% of the time will sometimes be seen in fewer than 20% of them. So proptest decides with a significance test, as QuickCheck does:

• It generates past max_examples when the answer isn’t clear yet, checking again at 2×, 4×, 8×, … the number of examples.
• A requirement passes once proptest is confident that the true share is at least tolerance × percent (by default 0.9 × the requirement).
• It fails once proptest is confident the true share is below percent.
• Each conclusion is wrong with probability about 1 / certainty (by default one in a billion).

from proptest import given, cover, integers, Settings, Confidence

def main() raises:
    def prop(x: Int) raises:
        pass

    var s = cover(integers(0, 100), 50, "above 90", lambda (x: Int) -> Bool: x > 90)
    try:
        given(s, prop, Settings(database=None, check_coverage=Confidence()))
    except e:
        print(e)

Insufficient coverage (coverage.mojo:9:14):
    only 10.00% above 90 (in 100 examples), but expected 50.0%

Confidence(certainty=1e9, tolerance=0.9) sets the two parameters. Raise certainty for fewer wrong conclusions, at the cost of more examples before one is reached.

Look before you require

To see the distribution before deciding on requirements, record it with tabulate or data.event and run with Settings(show_statistics=True). See Adding notes and statistics.

Write negative tests

A negative test checks that a property test fails when it should. It’s the property-testing version of making sure a test can go red: before trusting that a property holds, check that it catches a bug you’ve planted. This is especially worthwhile for custom strategies, which can quietly fail to produce the inputs a property needs.

expect_failure

expect_failure(f) runs a test function that should fail, and returns the failure report. If the function passes, expect_failure raises (QuickCheck’s expectFailure):

from std.testing import assert_true
from proptest import expect_failure, check, Settings

def buggy_max(xs: List[Int]) -> Int:
    var m = 0          # BUG: wrong for lists of negative numbers
    for x in xs:
        m = max(m, x)
    return m

def main() raises:
    def max_is_an_element(xs: List[Int]) -> Bool:
        return len(xs) == 0 or buggy_max(xs) in xs

    def run() raises:
        check(max_is_an_element, Settings(database=None))

    var report = expect_failure(run)
    assert_true("given([-1])" in report, report)
    print("the property catches the bug")

The report is the message the test would have raised, so you can also check what was found, as above. expect_failure only accepts proptest’s own failures (falsifying examples and coverage failures); any other error, such as a health check, is raised again, since it means the test didn’t really run.

run_property: the result as data

run_property(strategy, test, settings) runs a property like given, but returns a PropertyResult instead of raising (QuickCheck’s quickCheckResult):

from proptest import run_property, lists, integers, fail, Settings

def main() raises:
    def short(xs: List[Int]) raises:
        if len(xs) >= 2:
            fail("too long")

    var r = run_property(lists(integers()), short, Settings(database=None))
    print(r.passed())                  # False
    print(r.counterexample.value())    # [0, 0]
    print(r.blob)                      # Settings(reproduce=...) replays it

A PropertyResult[T] has:

• passed(): whether the property held;
• counterexample: the shrunk failing value, typed, as an Optional[T];
• message: the report given would have raised;
• blob: a string for Settings(reproduce=...);
• report: the RunReport, with the counts of valid, invalid, and overrun examples, the number of shrinks, and the run’s statistics.

It takes a single strategy; use tuples(...) for several arguments. run_property is useful for building tools on top of proptest, and for tests that check the counterexample itself rather than the message.

Test generic code

To test a generic function, you have to pick a type to test it at. The obvious choice, Int, can hide bugs: a property may pass because of something particular to integers, such as arithmetic coincidences, or because a function quietly relies on behaviour only Int has.

PolyA, PolyB, and PolyC are opaque stand-in types for this (Haskell QuickCheck’s Test.QuickCheck.Poly). Each holds an integer, but supports only equality, ordering, hashing, and printing. Testing a generic function at PolyA shows that it works for any type with just those operations.

from proptest import check, PolyA

def reverse[T: Copyable](xs: List[T]) -> List[T]:
    var out = List[T]()
    for i in range(len(xs) - 1, -1, -1):
        out.append(xs[i].copy())
    return out^

def main() raises:
    def reverse_twice(xs: List[PolyA]) -> Bool:
        return reverse(reverse(xs)) == xs

    check(reverse_twice)
    print("passed")

They print with their tag, so a counterexample is easy to read: given([A(0), A(1)]). Use different stand-ins for different type parameters (Dict[PolyB, PolyC]), so that a function that mixes them up fails to compile, or fails the test.

Poly[tag] makes more stand-in types: Poly["Key"] prints as Key(3).

Generate functions

Code that takes a function as an argument (a sort with a custom key, a map over a container, a retry policy) should work for any function, not just the few you think to write. functions[A](returns) generates functions from A to the values of the strategy returns (Hypothesis’s functions, QuickCheck’s Fun).

from proptest import given, functions, integers, Function, fail, Settings

def main():
    def monotone(f: Function[Int, Int]) raises:
        if f(1) > f(2):
            fail("not monotone")

    try:
        given(functions[Int](integers(0, 9)), monotone, Settings(database=None))
    except e:
        print(e)

Falsifying example (functions.mojo:9:14):
    given({1->1, 2->0})
At functions.mojo:7:17: AssertionError: not monotone

A generated Function[A, R]:

• is memoized: calling it twice with the same argument gives the same result, so it behaves like a pure function;
• draws each new argument’s result from the test case, so the results shrink like any other generated value;
• prints as the table of calls made, {x->y, ...}. So that the table is complete, given prints its arguments after the test has run.

The argument type A must be usable as a dictionary key (KeyElement), Copyable, and Writable.

A function only lives as long as its test case

A Function draws its results from the test case that created it. After that test case ends, it can’t draw any more, and calling it raises an error (“… after its test case ended”) instead of returning a value. So don’t keep generated functions between test cases, and don’t use one from example(...) outside the call.

Guide the search with targets

Random generation is good at finding bugs that many inputs trigger, and bad at finding ones that only extreme inputs trigger: very large totals, very deep nesting, long-running operations. Targeted property-based testing helps. The test reports a score, and proptest searches for inputs that make the score larger (Hypothesis’s target()).

Report a score

In a given_data test, call data.target(score, label):

from proptest import given_data, lists, integers, ConjectureData, Settings

def main():
    def prop(mut data: ConjectureData) raises:
        var xs = data.draw(lists(integers(0, 1000), max_size=10), "xs")
        var total = 0
        for x in xs:
            total += x
        data.target(Float64(total), "sum")
        if total > 9000:
            raise Error(String("sum is ", total))

    try:
        given_data(prop, Settings(database=None))
    except e:
        print(e)

Falsifying example (target.mojo:15:19):
    Draw 1 (xs): [1, 1000, 1000, 1000, 1000, 1000, 1000, 1000, 1000, 1000]
sum is 9001

The bug needs a list whose sum exceeds 9000: ten elements, nine of them almost at the maximum. Random lists of this kind are almost never that big. In ten runs of this test, proptest found the failure in eight with the target, and in none of ten without it.

How it works

After half of the examples have been generated, proptest runs a target phase: for each label, it takes the inputs with the highest scores and hill-climbs from them, trying small changes to the choices that made them and keeping changes that raise the score. With the example database enabled, it also keeps a Pareto front of the best inputs across labels between runs.

Tips

• Use a score that rises steadily as inputs approach the bug: a size, a count, an error magnitude, an elapsed time. A score that’s 0 or 1 gives the hill climber nothing to follow.
• Use a separate label for each score; each is maximized separately.
• Targeting complements a test’s assertions; it doesn’t replace them. The score only steers the search towards inputs that might fail.
• Phases(target=False) turns the target phase off.

Suppress a health check

Health checks catch tests that run but can’t test well: strategies that reject almost everything, or that produce data too large or too slow to generate. When one fails, the test fails with FailedHealthCheck and a suggestion. Usually you should fix the cause; when you can’t, or the check is wrong for your test, suppress it:

from std.testing import assert_true, assert_equal
from proptest import *
def main() raises:
    var s = integers()
    def prop(x: Int) raises:
        pass

    given(s, prop, Settings(suppress_health_check=[HealthCheck.too_slow]))

The health checks

The stateful runners suppress data_too_large and large_base_example themselves, because programs of 50 steps are large by design.

Before suppressing

A health check usually points at a real problem in the test:

• filter_too_much means most of the run went to inputs that were thrown away. A test that “passes” this way has run on few inputs, and those may be the ones the filter happened to let through. See Adapting strategies.
• too_slow and data_too_large mean each example costs a lot, so fewer inputs are tried in the same time, and shrinking is slow.

Time limits on the test body aren’t a health check: that’s the deadline setting, which fails individual slow examples.

Debug a failing test

proptest’s report gives the shrunk input and the error. When that isn’t enough to see the bug, these tools help.

Replay just the failing example

With Settings(print_blob=True), the report includes a blob:

To reproduce this example, run the test with Settings(reproduce="proptest1:aToxMDEK")

Rerun the test with that setting, and proptest runs exactly that example, once, without searching or shrinking. Add print statements or a debugger, and you’ll see only the failing case.

The example database does nearly the same automatically: the next run of the test tries the saved failure first. But it then goes on to search and shrink, so you’ll see other test cases too.

Stop on the minimal example in a debugger

A debugger breakpoint in the test stops on every test case, including the hundreds that pass and the many tried while shrinking. Instead, set a breakpoint on before_minimal_test_case, which proptest calls just before the final replay of a shrunk failure (RapidCheck’s rc::beforeMinimalTestCase). When it stops there, set the breakpoints you need in the test, and continue.

$ mojo build -I path/to/proptest -g my_test.mojo -o my_test
$ mojo-lldb my_test
(lldb) breakpoint set -r before_minimal_test_case
(lldb) run
...
* thread #1, stop reason = breakpoint 1.1
    frame #0: my_test`proptest::core::before_minimal_test_case(::String)
(lldb) breakpoint set -f my_test.mojo -l 42
(lldb) continue

The function’s argument is the test’s location, for a conditional breakpoint when a program has several failing tests.

When the test crashes

A test that segfaults or aborts takes the run down with it, before proptest can shrink anything. Run it with Settings(fork=True); see Test code that crashes.

See what the test computed

• Notes: in a given_data test, data.note(...) adds lines to the report, printed only for the final example.
• Labels: data.draw(strategy, "name") names each drawn value in the report.
• Messages: std.testing assertions take a message, and fail(msg) fails with one.

See what proptest is doing

Settings(verbosity=Verbosity.verbose) (or PROPTEST_VERBOSITY=verbose) prints the counts and seed of each run, the run’s statistics, and the reproduce blob. Verbosity.debug also prints every test case (its status and choices), each successful shrink, and how well each shrink pass did. That’s a lot of output, meant for working on strategies or on proptest itself.

Turn off shrinking

If shrinking is slow, or you want to see the input as first found, Settings(phases=Phases(shrink=False, explain=False)) reports the first failure unshrunk.

Read the explain comments

After shrinking, proptest tries varying each argument of the minimal example. Arguments that don’t affect the failure are marked:

Falsifying example (test.mojo:8:14):
    given(
        11,
        '',  # or any other generated value
        0,  # or any other generated value
    )
    # The test always failed when commented parts were varied together.

Here only the first argument matters, which narrows the search for the cause.

Test code that crashes

A test that segfaults, aborts, or trips AddressSanitizer kills the process, and proptest with it: you see the crash, but not the input that caused it, and nothing is shrunk. Code that uses raw pointers fails this way more often than it raises.

fork=True

With Settings(fork=True), each test case runs in a child process. A crash then fails the test case like any other error, and proptest shrinks it:

from proptest import expect_failure, given, lists, integers, fail, Settings

def last(xs: List[Int]) -> Int:
    # BUG: no check for an empty list, which has no buffer
    return xs.unsafe_ptr()[unsafe_offset=len(xs) - 1]

def main() raises:
    def last_is_an_element(xs: List[Int]) raises:
        if last(xs) not in xs:
            fail("last isn't an element")

    def run() raises:
        given(
            lists(integers()),
            last_is_an_element,
            Settings(database=None, fork=True),
        )

    print(expect_failure(run))

Falsifying example (crash.mojo:15:14):
    given([])
Crash: the test case was killed by SIGSEGV (signal 11), in a child process (Settings(fork=True))

Each signal is a distinct failure, as is each exit status, so a test that can both segfault and abort reports both. A test case that exits before it finishes, for example when AddressSanitizer finds a use after free and exits with status 1, fails too. Build the test with --sanitize address to catch memory errors that don’t crash:

mojo build -I . --sanitize address -o my_test my_test.mojo && ./my_test

While searching and shrinking, children’s output is discarded: sanitizer reports, failed debug_assert messages (which go to stdout), and anything the test prints. The final replay of each shrunk failure shows it, so you see one report, for the minimal example.

timeout

Settings(timeout=ms) kills a test case that runs longer than ms milliseconds and fails it with Timeout; it implies fork=True. Unlike deadline, which times a test case that finishes, it catches one that never does, such as an infinite loop in a linked list with a cycle.

What changes in a child process

• The child gets a copy of the parent’s memory, so a test’s side effects (a counter it increments, a global cache it fills) stay in the child.
• Each test case costs a fork(): about 0.2 ms for a built binary, and a few milliseconds under mojo run. Build the test (mojo build) when running many test cases.
• Core dumps are off in the children, and crashes use the default signal handlers rather than Mojo’s, which print a stack trace. To see the trace, replay the shrunk failure in-process: run the test without fork and with Settings(reproduce=...) (see Debug a failing test).
• Code that uses threads may deadlock in the child, where only the thread that called fork() exists.
• POSIX only (Linux and macOS).

PROPTEST_FORK=1 in the environment turns fork on for tests that don’t set it, and PROPTEST_TIMEOUT=ms sets timeout (and so turns fork on too). Use a timeout when a bug may corrupt a linked structure: a cycle makes a walk loop forever, and with fork alone the run waits for it.

Generate NuMojo arrays

NuMojo is Mojo’s NumPy-like array library. proptest’s strategies for it live in a separate package, proptest_numojo, in the repository’s extras/ directory, so that proptest itself doesn’t depend on NuMojo. It’s the counterpart of hypothesis.extra.numpy.

Setup

Put proptest, extras/, and the directory containing numojo on the include path:

mojo run -I path/to/proptest -I path/to/proptest/extras -I path/to/numojo-parent my_test.mojo

proptest_numojo needs a NuMojo that builds with Mojo 1.3. The published NuMojo 0.12 requires an older Mojo; extras/run_tests.sh describes a patched copy that works.

Arrays

from std.testing import assert_true
from numojo.prelude import *
from proptest import given, floats
from proptest_numojo import arrays, array_shapes

def prop(a: NDArray[DType.float64]) raises:
    assert_true(a.ndim >= 1 and a.ndim <= 2)

def main() raises:
    given(arrays[DType.float64](array_shapes(max_dims=2), floats(-1.0, 1.0)), prop)

Broadcasting and indexing

These follow Hypothesis’s functions of the same names (without gufunc signatures). Indices are values of proptest’s own BasicIndex and IndexItem types, since NuMojo has no single index type; apply them to an array as your code would.

Shrinking

Arrays shrink like other proptest values: towards smaller shapes, and towards simple element values (zeros). A failure prints the array as NuMojo writes it.

Run proptest in CI

Property tests run as ordinary Mojo test programs, so a CI job runs them the way it runs any other test. A few settings are worth choosing deliberately for CI.

Disable the example database

The database lets a failure persist between runs on one machine. In CI, nothing is kept between jobs, so the database only adds files. Disable it for every test that uses the default:

export PROPTEST_DATABASE=none

Decide between fresh and repeatable runs

By default, every run uses a new random seed. That’s what you want most of the time: each CI run explores new inputs, and over time the suite tests far more than any single run does. A failure that appears in CI shows its example in the log, and with print_blob=True or verbose output, a blob to reproduce it.

If you need every run to be identical (for a release check, say), Settings(derandomize=True) derives each test’s seed from the test, or PROPTEST_SEED=1234 fixes the seed for every test that doesn’t set one.

Run more examples

CI machines can afford more examples than a developer’s edit-test loop. PROPTEST_MAX_EXAMPLES raises max_examples for every test that leaves it at the default:

PROPTEST_MAX_EXAMPLES=1000 mojo run -I . tests/test_parser.mojo

A nightly job with a much larger number is a cheap way to find rare bugs.

Watch the deadline

The default deadline is 200 ms per example. Shared CI machines can be much slower than a workstation, which makes slow tests fail with DeadlineExceeded or flaky deadline errors. Give slow tests an explicit deadline (or None).

Print what’s needed to reproduce

With PROPTEST_VERBOSITY=verbose, each failure report includes the seed and a reproduce blob, at the cost of more output for passing tests. Settings(print_blob=True) on important tests includes just the blob.

Using proptest from a pixi project

Until proptest is on the modular-community channel, a project can use it from a checkout:

[tasks]
test = "mojo run -I ../proptest tests/test_all.mojo"

or from a built proptest.mojoc (pixi run package in the proptest repository), put on the include path.

How proptest works

proptest’s engine is a port of Hypothesis’s Conjecture engine. This page explains its main ideas: choice sequences, shrinking, the phases of a run, and how distinct bugs are told apart.

Choice sequences

A strategy doesn’t produce values from a random number generator directly. It makes choices through the ConjectureData: draw an integer in this range, a float, a boolean with this probability, a string from these codepoints, a byte string. Each choice is recorded. A test case is the sequence of choices it made, and the values are whatever the strategies built from those choices.

This has a crucial consequence: given the same choice sequence, the strategies rebuild the same values. So a test case can be replayed, saved, and, most importantly, modified. Change a choice and replay, and the strategies build a different but related value.

Choices are grouped into spans, one for each data.draw(strategy), so the engine knows which choices belong to which value: this run of choices is one list element, that one is a dictionary key. Spans are why a custom strategy should draw through data.draw rather than calling another strategy’s do_draw.

Shrinking

Every kind of choice has a simplicity order: smaller integers (nearer the “shrink towards” point) are simpler, False is simpler than True, shorter strings are simpler, and so on. One choice sequence is simpler than another if it’s shorter, or the same length and simpler at the first choice where they differ.

The shrinker takes a failing choice sequence and tries simpler ones, keeping any that still fail. Its passes each try a kind of change:

• replace a span with its simplest form;
• delete runs of choices (which removes list elements, or steps of a program);
• replace a span with one of its descendants (a tree with a subtree);
• reorder spans with the same label, such as list elements;
• simplify each choice: lower an integer, simplify a float towards an integer, shorten a string;
• lower duplicated choices, or pairs of integers, together;
• and the others in Hypothesis’s shrinker, which proptest ports.

Because the shrinker only moves to simpler sequences, it always ends. And because strategies rebuild values from choices, every simpler failing sequence is a simpler failing value, with all the strategies’ invariants intact. This is the main advantage over shrinking values directly, as QuickCheck and Rust’s proptest do: no strategy needs a shrinker of its own, shrinking works through map, flatmap, and filter, and a shrunk value is always one the strategy could have produced.

The phases of a run

A run of given goes through these phases, each of which can be turned off with Phases:

1. explicit: run explicit examples.
2. reuse: replay failures saved in the example database.
3. generate: generate new test cases. The first is the simplest possible input; early test cases are kept small, and later ones explore further. Some test cases mutate earlier ones rather than starting fresh.
4. target: hill-climb on the scores reported with data.target.
5. shrink: shrink each distinct failure.
6. explain: for the shrunk failure, find which arguments can vary without changing the outcome, and mark them in the report.

Generation is guided by a tree of the choice sequences tried so far, so proptest doesn’t run an identical test case twice, and knows when the search space is exhausted.

Distinct failures

A run can find several bugs. proptest tells them apart by their origin: the location of the error. The std.testing assertions and fail() put an At file:line:col: prefix on their errors, and failures at different locations are treated as different bugs, each shrunk separately and reported together (with report_multiple_bugs=True, the default):

proptest found 2 distinct failures.

--- Failure 1 of 2 ---
Falsifying example (...):
...

Without this, shrinking one bug can slip into another: the shrinker happily keeps a simpler input that fails for a different reason, and you end up with a minimal example of the wrong bug. Errors without a location prefix all count as one origin.

The example database

The database maps each test to the choice sequences of its failures. It stores choices, not values, so saved examples replay through the test’s current strategies. It’s a directory of small text files, one per example, one choice per line.

Further reading

• How many times will proptest run my test?
• David R. MacIver and Alastair F. Donaldson, “Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer”, ECOOP 2020.
• The engine’s source is in proptest/internal/; the README maps each file to its Hypothesis original.

How many times will proptest run my test?

The short answer is “max_examples times”, 100 by default. The long answer has exceptions:

• fewer, if proptest exhausts the search space early;
• more, if some test cases are rejected (by assume or filter) or too large, since those don’t count;
• more, under check_coverage, until the coverage requirements are settled;
• fewer or more, if proptest finds a failure.

Search space exhaustion

proptest never runs an identical test case twice, and it knows when there are no more to try:

from proptest import given, integers

def main() raises:
    var calls = 0

    def prop(n: Int) raises {mut calls}:
        calls += 1

    given(integers(0, 19), prop)
    print(calls)   # 20

There are only 20 integers to try, so the test runs 20 times. The same thing shows up less obviously in the statistics: after the empty list has been tried once, lists(...) never generates it again.

Rejected test cases

A test case that fails an assume, a filter (after three tries), or returns Outcome.discard() is invalid, and doesn’t count towards max_examples:

from std.testing import assert_true, assert_equal
from proptest import *
def prop(n: Int) raises:
    assume(n % 2 == 0)

def main() raises:
    given(integers(), prop, Settings(database=None))

runs about 200 times to get 100 valid examples. If most test cases are invalid, the filter_too_much health check fails the test.

Test cases that are too large

There’s a limit on the number of choices in a test case (8,192). A test case that hits it is overrun: abandoned, and not counted. Early in a run, proptest also keeps test cases deliberately small, so that simple bugs are found with simple inputs, and abandons those that grow too large. Many overruns fail the data_too_large health check.

Coverage checks

With Settings(check_coverage=Confidence()), proptest keeps generating past max_examples until every cover requirement is known to hold or fail, up to 100,000 examples.

Failing test cases

When proptest finds a failure, it stops generating. It then runs the test many more times while shrinking, and while explaining the result. Finally it runs the minimal example once more, to collect its report and check that the failure is reproducible.

Domain and distribution

A strategy has two properties that are easy to confuse:

• its domain: the set of values it can produce;
• its distribution: how likely each of those values is.

integers(0, 100) has the domain 0 to 100. Its distribution isn’t uniform: proptest generates 0, 100, and other boundary values more often than chance would, along with “nasty” values that tend to find bugs.

Choose the domain to match the property

The domain is the part you control, and the part that matters. A test should generate every input for which the property is supposed to hold. If my_sort should work for any list of integers, test it with lists(integers()), not lists(integers(0, 100), max_size=10). A narrower domain only tests a narrower claim.

Narrow the domain when the property genuinely doesn’t apply outside it: floats(allow_nan=False) for code that’s documented not to accept NaN. The constraint types (Positive[T], NonEmpty[T]) are a way of writing the domain into the test’s signature.

Why you don’t control the distribution

proptest doesn’t offer settings for the probabilities of particular values, for the same reasons as Hypothesis:

• The best distribution for finding bugs isn’t a natural one. Bugs cluster at boundaries, at special values, and in unusual combinations, so the engine deliberately over-represents those.
• The distribution changes during a run: proptest starts with small, simple inputs, mutates inputs it has seen, and steers towards new behaviour. A fixed distribution would fight this.
• Shrinking doesn’t depend on the distribution, so there’s no need to bias towards small values to get small counterexamples.

There are two exceptions, both from other libraries: one_of and sampled_from accept weights, for when one alternative really should appear more often; and cover lets you check the distribution where it matters, rather than control it. See Check the distribution of inputs.

What the distribution is

It’s an implementation detail, and it changes between versions. Roughly:

• each choice is sometimes forced to a special value (a bound, zero, a “nasty” float such as NaN or the smallest subnormal) and otherwise drawn at random;
• collections continue with a probability chosen to give a moderate average size;
• after the first few test cases, many are mutations of earlier ones, and later ones are guided towards unexplored choice sequences.

To see what a particular strategy produces, use example, or record statistics with tabulate and Settings(show_statistics=True).

Why the API looks the way it does

proptest’s API follows Hypothesis’s names and ideas, but it’s shaped by Mojo, a statically typed, compiled language without decorators, global variables, or run-time reflection on functions. This page explains the main differences in shape.

given is a function, not a decorator

Hypothesis writes @given(st.integers()) above a test. Mojo has no user decorators, so given(integers(), prop) is a call inside the test, with the property as a nested function. The compiler checks that the property’s parameter types match the strategies’ value types.

There are separate overloads of given for one to six strategies, because Mojo can’t yet express “a function whose parameters are the value types of these strategies” for any number of strategies.

Combinators are free functions

Hypothesis writes integers().map(f). In proptest it’s map(integers(), f). A method on the Strategy trait that’s generic over a closure of Self.Value hits a compiler limitation, so map, filter, flatmap and the rest are free functions with the strategy first.

Strategies have types

Every strategy is a struct with a type: integers() returns an Integers, lists(integers()) a Lists[Integers], and map(s, f) a Mapped[S, R, F], where F is the type of the function. These types let the compiler check and specialize every test, so drawing a value calls the strategies’ code directly, with no dynamic dispatch. The cost is that a function returning a strategy has to spell its type; boxed(s) erases it, at the cost of an indirect call.

one_of follows the same pattern: one_of(s1, s2, s3) stores its strategies in a tuple, with no boxing, and a list of BoxedStrategy is the dynamic alternative.

Inferring strategies from types happens at compile time

Hypothesis’s from_type looks at a type at run time. proptest’s from_type[T]() chooses the strategy at compile time: from an Arbitrary implementation, from the standard types’ built-in strategies, or by reflecting on a struct’s fields. check(prop) doesn’t reflect on the property’s signature (Mojo can’t); overload resolution infers its parameter types, and each is drawn with from_type.

Settings are a struct

Hypothesis’s settings are a decorator with named profiles. proptest’s are a Settings struct of keyword arguments. Mojo has no global variables, so there’s no global profile; PROPTEST_* environment variables take its place.

State machines number their rules

Hypothesis finds a state machine’s rules by looking for methods decorated with @rule. A proptest StateMachine numbers its rules and dispatches on the number. TypedStateMachine and commands avoid numbers by making operations into values and structs.

The “interesting origin” is a location prefix

Hypothesis tells bugs apart by the exception’s type and the line it was raised on. Mojo errors don’t have types or tracebacks, so proptest uses the At file:line:col: prefix that std.testing assertions and fail() put on their messages. Errors raised without one count as a single bug.

Integers are 128-bit

Hypothesis’s integers are unbounded, like Python’s. proptest’s choices are 128-bit integers, which covers every Mojo integer type.

The differences document lists every difference from Hypothesis, with the reasons.

Influences and differences

proptest started as a port of Hypothesis, and its engine still is one. Its API also borrows from other property-testing libraries, especially where their designs suit a statically typed language better than Hypothesis’s dynamic one. This page says what came from where.

Hypothesis

From Hypothesis, proptest has:

• the Conjecture engine: choice sequences, spans, the shrinker and its passes, the data tree, mutation, targeting, the Pareto front, and the explain phase;
• the strategies: numbers, text, collections, one_of, map, filter, flatmap, composite, recursive, shared, functions, from_regex with Unicode categories, and from_type;
• the example database, health checks, deadlines, settings, phases, verbosity, @reproduce_failure (as Settings(reproduce=...)), and run statistics;
• rule-based state machines, with bundles, preconditions, invariants, initialize rules, and swarm testing;
• NuMojo strategies, the counterpart of hypothesis.extra.numpy.

The differences document lists every difference from Hypothesis and why. The main ones are described in Why the API looks the way it does. Not ported: alternative backends, observability output, the date, time, email, and IP address strategies, and Hypothesis’s tooling (the pytest plugin, the ghostwriter).

Rust’s quickcheck

• check(prop): strategies inferred from the property’s parameter types, like quickcheck’s quickcheck(prop) and its Testable trait.
• Outcome: a property can pass, fail with a message, or discard its input (quickcheck’s TestResult).

Haskell’s QuickCheck

• Constraint types: Positive[T], NonNegative[T], NonZero[T], NonEmpty[T], Sorted[T], and Blind[T], from QuickCheck’s modifiers.
• Coverage: cover, tabulate, and check_coverage with its statistical test (checkCoverage).
• expect_failure (expectFailure), and run_property (quickCheckResult).
• PolyA, PolyB, PolyC, the stand-in types for generic code (Test.QuickCheck.Poly).
• Generated functions that print as tables (Fun), alongside Hypothesis’s functions.

Rust’s proptest

• Typed state machines, whose steps are values of a Transition type (proptest-state-machine).
• filter_map, filter(reason=), subsequence, Index, lazy_just, and weighted one_of.

RapidCheck, and Erlang QuickCheck

• Model-based testing with Command structs, the model kept separate from the system under test (rc::state, which follows Erlang QuickCheck’s eqc_statem).
• build[T](field["x"](s)) (gen::build), apply (gen::apply), weighted sampled_from (gen::weightedElement), and before_minimal_test_case (rc::beforeMinimalTestCase).

What wasn’t borrowed

Some ideas from these libraries don’t fit Conjecture:

• Shrinking values directly (QuickCheck’s shrink, Rust proptest’s ValueTree): Conjecture shrinks the choice sequence instead, which needs no per-type code and keeps every invariant.
• A size parameter (QuickCheck’s sized, RapidCheck’s resize): Conjecture controls sizes through average sizes and a choice budget, and a global size would interfere with replay and the database.
• Macros and derive attributes: Mojo has no user macros. check, from_type, composite, and TestSuite discovery cover the same ground.

The repository’s ideas document records each idea considered, with the reasons for adopting or rejecting it.

Tips and limitations

Tips

Start with simple properties

The most useful first property is often “doesn’t crash”: call the code on generated input and check nothing else. It finds a surprising number of bugs, and tells you what input the code actually accepts. Then add round trips (decode(encode(x)) == x), invariants, and comparisons with a simpler implementation.

Generate valid inputs instead of filtering

Construct the inputs you need: draw a list, then an index into it; draw a lower bound, then an upper bound above it. Filtering with filter or assume discards work, and if it discards most of it, the test fails a health check.

Keep test cases small

Large inputs are slow to generate, to run, and to shrink. Pass max_size to collection strategies when the code under test doesn’t need large inputs to show its behaviour; most bugs show up with small ones.

Compare against a model

A slow, obviously correct implementation is a powerful oracle. A Dict can model a hash table, a sorted List a priority queue. Stateful and model-based tests are built around this idea.

Check that the test can fail

A property that can’t fail tests nothing. Plant a bug and run the test with expect_failure, or look at the statistics to see whether the inputs you care about are generated.

Make values readable

Counterexamples are printed with write_to. A short, clear form makes reports easier to read: Interval(0, 5), not every field with its name.

Keep tests deterministic

Draw all randomness through proptest, and don’t let state leak between test cases. See Flaky failures.

Limitations

Property-based testing finds bugs; it doesn’t prove their absence

A passing run means proptest didn’t find a failure in the inputs it tried. Bugs that need very particular inputs (a specific 64-bit value, say) may never be generated. Targeting, explicit examples, and boundary-heavy generation help, but a passing property test isn’t a proof.

Some properties are hard to state

Code whose correct output is hard to describe without reimplementing it is hard to test this way. Partial properties still help: the output has the right length, is sorted, contains only elements of the input.

Tests run many times

A property test runs the code hundreds of times, which is slow if each run is slow. Lower max_examples for expensive tests, and run more examples in CI or nightly.

Mojo-specific limitations

• given and check take at most six arguments; use tuples, a struct, or given_data for more.
• Generated values must be Writable.
• Struct fields of types that can’t be reflected or drawn need an Arbitrary implementation or an explicit strategy.
• from_regex supports the common subset of regular expressions: no backreferences, lookaround, or word boundaries.

Tests and results

Everything here is imported from proptest. Functions that run tests take an optional location keyword argument, which defaults to the caller’s source location. It names the test in reports and keys it in the example database; you only need it when wrapping these functions in your own helpers.

Running tests

given

given(s1, test, settings=Settings())
given(s1, s2, test, settings=Settings())
...                                        # up to six strategies

Runs test(a1, ..., aN) on values drawn from the strategies, max_examples times (see How many times will proptest run my test?). If the test raises, shrinks the failing input and raises an Error whose message is the failure report. The test’s parameter types must be the strategies’ value types. It formats the arguments after the test runs, so generated Functions can print the calls made.

check

check(prop, settings=Settings())

Like given, with each argument drawn by from_type from the property’s parameter types. prop takes one to six arguments and either raises on failure, returns Bool (False fails with check: the property returned False), or returns an Outcome.

given_data

given_data(test, settings=Settings())   # test: def(mut ConjectureData) raises

Runs a test that draws its own values with data.draw(strategy, label) (Hypothesis’s st.data()). Reports list each draw as Draw n (label): value.

check_examples

check_examples(examples: List[V], test)

Runs test on each explicit example (Hypothesis’s @example), raising Falsifying explicit example for the first that fails. Explicit examples are not shrunk.

run_test

run_test(test_fn, settings, name) -> RunReport   # test_fn: def(mut ConjectureData) raises

The engine entry point used by the functions above: generate, shrink, and replay, then return a RunReport without raising for failures. name identifies the test in reports, and its settings.database_key should be set if you use the database.

Inside a test

assume

assume(condition: Bool) raises

Discards the current test case if condition is false. Discarded test cases don’t count towards max_examples; too many fail the filter_too_much health check.

fail

fail(msg: String) raises

Fails the test with msg. Like the std.testing assertions, the error records where it was raised, which is how proptest tells distinct bugs apart.

ConjectureData methods for tests

In given_data tests, composite functions, state machine rules, and Arbitrary.arbitrary:

The low-level methods, for making primitive choices, are in Writing strategies: the low-level API.

Exploring strategies

example

example(strategy, seed: Optional[UInt64] = None) -> S.Value

One random value from strategy, for exploring interactively; not for use in tests.

find

find(strategy, condition, settings=Settings(max_examples=2000, database=None)) -> S.Value

The simplest value satisfying condition (def(S.Value) raises -> Bool), found by searching and then shrinking. Raises NoSuchExample if none is found.

Results

Outcome

A result type for properties passed to check (quickcheck’s TestResult):

is_failure() says whether it’s a failure. Outcome implements the Testable trait (check_result(self) raises), which check accepts as a property’s return type.

run_property

run_property(strategy, test, settings=Settings()) -> PropertyResult[S.Value]

Runs given(strategy, test) and returns what happened instead of raising (QuickCheck’s quickCheckResult). Use tuples(...) for several arguments.

PropertyResult[T]

RunReport

expect_failure

expect_failure(test: def() raises) raises -> String

Runs test, which should fail with a proptest failure (a falsifying example, several distinct failures, or insufficient coverage), and returns its report. Raises if test passes; re-raises any other error (QuickCheck’s expectFailure).

Debugging

before_minimal_test_case

before_minimal_test_case(name: String)

Called just before the final replay of each shrunk failure, and before a reproduce= replay. It does nothing; it’s a place for a debugger breakpoint. name is the test’s location.

Failure messages

Settings

Settings

Settings(
    *,
    max_examples: Int = 100,
    seed: Optional[UInt64] = None,
    derandomize: Bool = False,
    database: Optional[String] = ".proptest/examples",
    database_key: String = "",
    phases: Phases = Phases(),
    verbosity: Verbosity = Verbosity.normal,
    report_multiple_bugs: Bool = True,
    suppress_health_check: List[HealthCheck] = [],
    stateful_step_count: Int = 50,
    max_shrinks: Int = 500,
    print_blob: Bool = False,
    deadline: Optional[Float64] = 200.0,
    reproduce: Optional[String] = None,
    show_statistics: Bool = False,
    check_coverage: Optional[Confidence] = None,
    fork: Bool = False,
    timeout: Optional[Float64] = None,
)

Environment variables

Settings that a test leaves at their defaults can be changed from the environment, like a Hypothesis settings profile. A value set in the code always wins.

settings.with_env_overrides() returns the settings with these applied; the test runners call it for you.

Phases

Phases(*, explicit=True, reuse=True, generate=True, target=True, shrink=True, explain=True)

Verbosity

HealthCheck

See Suppress a health check.

Confidence

Confidence(*, certainty: Float64 = 1e9, tolerance: Float64 = 0.9)

How sure a coverage check must be (QuickCheck’s Confidence). A requirement of p% passes once proptest is confident the true share is at least tolerance × p%, and fails once it is confident the share is below p%. Each conclusion is wrong with probability about 1 / certainty.

Strategies

Every strategy function returns a struct conforming to Strategy, whose type is given after ->. Functions marked raises check their arguments and raise InvalidArgument errors. “Shrinks towards” describes the simplest value.

Numbers

integers

integers(min_value: Optional[Int] = None, max_value: Optional[Int] = None) raises -> Integers

Int values in [min_value, max_value]. Omitted bounds are the limits of Int. Shrinks towards 0, or the bound nearest 0.

integers_of

integers_of[dtype: DType](min_value: Optional[Scalar[dtype]] = None,
                          max_value: Optional[Scalar[dtype]] = None) raises -> ScalarIntegers[dtype]

Integers of any integer DType (UInt8, Int32, UInt64, …), defaulting to the type’s full range.

floats

floats(min_value: Optional[Float64] = None, max_value: Optional[Float64] = None, *,
       allow_nan: Optional[Bool] = None, allow_infinity: Optional[Bool] = None,
       allow_subnormal: Bool = True, exclude_min: Bool = False,
       exclude_max: Bool = False) raises -> Floats

Float64 values in the range. allow_nan defaults to true when there are no bounds; allow_infinity to true when a bound is missing. exclude_min/exclude_max make a bound exclusive. Shrinks towards 0, then towards simple integers and fractions.

floats32

floats32(min_value: Optional[Float64] = None, max_value: Optional[Float64] = None, *,
         allow_nan: Optional[Bool] = None, allow_infinity: Optional[Bool] = None) raises -> Floats32

Float32 values (Hypothesis’s floats(width=32)).

booleans

booleans() -> Booleans

True or False, shrinking towards False.

Text

text

text(alphabet: Optional[String] = None, *, min_size: Int = 0,
     max_size: Optional[Int] = None) raises -> Text
text(alphabet: Characters, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Text

Strings whose length in codepoints is in [min_size, max_size], made of the characters of alphabet: a string of allowed characters, or a characters(...) strategy. By default, any codepoint except surrogates (which UTF-8 can’t encode). Shrinks towards shorter strings, and towards '0'.

characters

characters(*, min_codepoint: UInt32 = 0, max_codepoint: UInt32 = 0x10FFFF,
           categories: List[String] = [], exclude_categories: List[String] = [],
           include_characters: String = "", exclude_characters: String = "",
           codec: Optional[String] = None) raises -> Characters

Single characters, as one-character Strings. categories are Unicode general categories ("Lu", "Nd", or a major class like "L"), from Unicode 17.0. codec is "ascii", "latin-1", or "utf-8".

from_regex

from_regex(pattern: String, *, fullmatch: Bool = False) raises -> Regex

Strings that contain a match of pattern, or, with fullmatch=True, that match it entirely. It supports the common subset of Python’s syntax:

• literals and escapes (\n, \xHH, \uHHHH, …);
• ., classes ([abc], [a-z], [^...]), and \d \D \w \W \s \S, which are Unicode-aware as in Python;
• groups ( ), (?: ), (?P<name> ), and alternation |;
• the quantifiers * + ? {n} {n,} {n,m} {,m}, with lazy and possessive forms;
• the anchors ^ $ \A \Z, and the flags (?i) and (?s) at the start.

Backreferences, lookaround, word boundaries, conditionals, and other flags raise InvalidArgument.

binary

binary(*, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Binary

Byte strings (List[UInt8]).

Collections

lists

lists(elements: S, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Lists[S]

List[S.Value] with length in [min_size, max_size]. Shrinks by deleting elements, then by shrinking the rest.

unique_lists, unique_lists_by

unique_lists(elements: S, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> UniqueValues[S]
unique_lists_by(elements: S, key: F, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> UniqueLists[S, K, F]

Lists of distinct values (S.Value must be KeyElement & Copyable), or of values with distinct key(x) (Hypothesis’s lists(unique=True) and lists(unique_by=key)).

sets

sets(elements: S, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Sets[S]

Set[S.Value]; the values must be KeyElement & Copyable.

dictionaries

dictionaries(keys: KS, values: VS, *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Dictionaries[KS, VS]

Dict[KS.Value, VS.Value]; keys must be KeyElement & Copyable.

tuples

tuples(s1, s2) -> Tuples2[S1, S2]
...                                      # up to six: Tuples6

Tuple of a value from each strategy.

optionals

optionals(strategy: S) -> Optionals[S]

None or a value from strategy, shrinking towards None.

Choosing

just, lazy_just

just(value: T) -> Just[T]                 # T: Copyable
lazy_just(f: def() raises -> T) -> LazyJust[T, F]

Always value; or f(), called afresh for each test case, for values that can’t or shouldn’t be copied. Neither makes any choices.

sampled_from

sampled_from(elements: List[T]) raises -> SampledFrom[T]
sampled_from(elements: List[T], *, weights: List[Int]) raises -> SampledFrom[T]

One of elements, shrinking towards the first. weights (positive, one per element) make each element’s probability proportional to its weight.

one_of

one_of(s1, s2) -> Alternatives[S1, S2]
one_of(s1, s2, *, weights: List[Int]) raises -> Alternatives[S1, S2]
...                                      # up to six strategies
one_of(strategies: List[BoxedStrategy[T]]) raises -> OneOf[T]
one_of(strategies: List[BoxedStrategy[T]], *, weights: List[Int]) raises -> OneOf[T]

A value from one of the strategies, which must all produce the same type; shrinks towards the first. The fixed-arity forms store the strategies unboxed. The weights only bias generation; they don’t change shrinking.

permutations

permutations(values: List[T]) -> Permutations[T]

Reorderings of values, shrinking towards the original order.

subsequence

subsequence(values: List[T], *, min_size: Int = 0, max_size: Optional[Int] = None) raises -> Subsequences[T]

Sublists of values that keep their order (Rust proptest’s sample::subsequence), shrinking towards dropping elements.

Transforming

map

map(strategy: S, f: def(S.Value) raises -> R) -> Mapped[S, R, F]

f(x) for x from strategy (Hypothesis’s strategy.map(f)).

apply

apply(s1, s2, f: def(S1.Value, S2.Value) raises -> R) -> Applied2[S1, S2, R, F]
...                                      # up to six strategies: Applied6

f(a1, ..., aN) with each argument from its strategy (RapidCheck’s gen::apply, Hypothesis’s builds with a function). The function comes last.

filter

filter(strategy: S, predicate: def(S.Value) raises -> Bool, *, reason: String = "") -> Filtered[S, F]

Values for which predicate holds. Each test case tries three times before it’s rejected. reason names the condition in the filter_too_much health check.

filter_map

filter_map(strategy: S, f: def(S.Value) raises -> Optional[R], *, reason: String = "") -> FilterMapped[S, R, F]

f(x) where it isn’t None (Rust proptest’s prop_filter_map).

flatmap

flatmap(strategy: S, f: def(S.Value) raises -> S2) -> FlatMapped[S, S2, F]

Draw x from strategy, then a value from the strategy f(x).

composite

composite(f: def(mut ConjectureData) raises -> T) -> Composite[T, F]

A strategy from a function that draws with data.draw(...) (Hypothesis’s @composite).

recursive

recursive(base: S, extend: def(BoxedStrategy[T]) raises -> BoxedStrategy[T], *,
          max_leaves: Int = 100) raises -> Recursive[T]

Recursive data: values from base, or from extend(s), where s is the recursive strategy itself, up to about max_leaves base values per example.

shared

shared(base: S, key: Optional[String] = None) -> Shared[S]

One value per test case: every draw from a shared strategy with the same key returns the same value. Without a key, draws from the same shared(...) call (and copies of it) share; separate calls don’t. Hypothesis shares by object identity instead.

boxed

boxed(strategy: S) -> BoxedStrategy[S.Value]      # S: Copyable

The same values, with the strategy’s type erased. Useful for lists of strategies, recursion, and functions that return strategies.

Statistics

cover

cover(strategy: S, percent: Float64, label: String, condition: def(S.Value) raises -> Bool) -> Covered[S, F]

Values from strategy, requiring that condition holds for at least percent% of test cases (QuickCheck’s cover).

tabulate

tabulate(strategy: S, table: String, key: def(S.Value) raises -> String) -> Tabulated[S, F]

Values from strategy, recording key(value) in the statistics table table (QuickCheck’s tabulate).

Types

from_type

from_type[T: Drawable]() -> FromType[T]

Values of T, with the strategy chosen at compile time. See Types.

build, field

build[T](field["name"](strategy), ...) -> Built[T, *Fs]

A struct built field by field, with the named fields drawn from the given strategies. See Types.

functions

functions[A](returns: S) -> Functions[A, R]

Memoized functions from A to values of returns. See Generate functions.

commands

commands[*Cs: Command](model, *, max_commands: Int = 50) -> CommandSequences[*Cs]
commands[*Cs: Command](model, *, weights: List[Int], max_commands: Int = 50) raises -> CommandSequences[*Cs]

Programs of commands. See Stateful and model-based testing.

NuMojo arrays

In the separate proptest_numojo package: arrays, array_shapes, from_dtype, broadcastable_shapes, mutually_broadcastable_shapes, basic_indices, and integer_array_indices. See Generate NuMojo arrays.

Types

from_type

from_type[T]() chooses a strategy for T at compile time, in this order:

1. If T implements Arbitrary, its arbitrary(data) method.

2. If T is a standard type, its built-in strategy:

   Type	Strategy
   Int, UInt, Int8 … Int128, UInt8 … UInt128	integers_of over the type’s range
   Float64, Float32	floats(), floats32()
   Bool	booleans()
   String	text()
   List[T]	lists(from_type[T]())
   Optional[T]	optionals(from_type[T]())
   Set[T]	sets(from_type[T]())
   Dict[K, V]	dictionaries(from_type[K](), from_type[V]())
   Tuple[...] (one to six elements)	tuples(...)

3. Otherwise, if T is a struct, each field drawn with from_type, in declaration order, each in its own span. The struct’s __init__ is not called.

A type that matches none of these is a compile error.

draw_from_type

draw_from_type[T](mut data: ConjectureData) raises -> T

The function behind from_type, for drawing a value of a type inside a strategy or test.

Arbitrary

trait Arbitrary:
    @staticmethod
    def arbitrary(mut data: ConjectureData) raises -> Self: ...

A type’s own strategy, used by from_type, check, and struct fields of the type.

build and field

build[T: Drawable](*fields: FieldBinding & Copyable) -> Built[T, *Fs]
field[name: StaticString](strategy: S) -> Field[name, S]

T built field by field, as in step 3 above, with each field named by a field binding drawn from its strategy instead (RapidCheck’s gen::build). Compile errors, each naming the field, for:

• a name that isn’t a field of T;
• a field bound twice;
• a strategy whose value type isn’t the field’s type.

build always works field by field, even if T implements Arbitrary.

Constraint types

Each implements Arbitrary, holds its value in .value, and prints as the value alone. All are Copyable when the value type is.

Constraint types can be nested where the types allow it, such as NonEmpty[List[Positive[Int]]].

Test types

PolyA, PolyB, PolyC, Poly[tag]

Opaque stand-in types for testing generic code (QuickCheck’s Poly). Each wraps an Int (.value), and supports only equality, ordering, hashing, and printing: PolyA prints as A(3). Poly[tag] makes more, with any StaticString tag.

Index

A position in a collection whose length isn’t known when the index is drawn (Rust proptest’s sample::Index). index.get(size) returns a position in [0, size) and raises if size <= 0. Shrinks towards the first position. Prints as a fraction of the way through the collection, such as Index(0.25).

Function[A, R]

A generated function from functions[A](returns). Call it as f(x) (which raises after its test case has ended). It’s memoized, and prints as the table of calls made: {1->1, 2->0}. A must be KeyElement, Copyable, and Writable.

Stateful and model-based testing

StateMachine

trait StateMachine(Deinitable, Movable):
    def __init__(out self)
    def rule_count(self) -> Int
    def rule_name(self, rule: Int) -> String                       # default "rule<n>"
    def precondition(self, rule: Int) -> Bool                      # default True
    def run_rule(mut self, rule: Int, mut data: ConjectureData) raises
    def check_invariants(self) raises                              # default: nothing
    def initialize_count(self) -> Int                              # default 0
    def initialize_name(self, rule: Int) -> String                 # default "initialize<n>"
    def run_initialize(mut self, rule: Int, mut data: ConjectureData) raises
    def teardown(mut self) raises                                  # default: nothing

A rule-based state machine (Hypothesis’s RuleBasedStateMachine). Rules are numbered from 0. Each program:

1. creates the machine with __init__ and checks the invariants;
2. runs each initialize rule once, in a random order;
3. runs up to stateful_step_count steps, each choosing a rule whose precondition holds (from a random subset of the rules: swarm testing), running it, and checking the invariants;
4. calls teardown, even if a step failed.

Rule arguments are the labeled draws a rule makes; a failure prints each step as state.<rule_name>(<label>=<value>, ...).

run_state_machine_as_test

run_state_machine_as_test[M: StateMachine](settings=Settings())

Runs programs against fresh machines and raises with the shrunk failing program. It suppresses the data_too_large and large_base_example health checks and the explain phase.

run_state_machine

run_state_machine[M: StateMachine](mut data: ConjectureData, max_steps: Int, deadline_ns: Int = -1)

Runs one program inside a test, for use with given_data or run_test.

Bundle[T]

Bundle[T](name: String)
bundle.add(value)
bundle.draw(data) -> T          # shrinks towards the most recently added
bundle.consume(data) -> T       # also removes the value
len(bundle)

Values produced by earlier steps for later steps (Hypothesis’s Bundle). draw and consume need a non-empty bundle; check it in the rule’s precondition. T must be Copyable.

TypedStateMachine

trait TypedStateMachine(Deinitable, Movable):
    comptime Transition: Drawable
    def __init__(out self)
    def transition(self, mut data: ConjectureData) raises -> Self.Transition
    def precondition(self, t: Self.Transition) -> Bool             # default True
    def apply(mut self, t: Self.Transition) raises
    def check_invariants(self) raises                              # default: nothing
    def teardown(mut self) raises                                  # default: nothing

A state machine whose steps are values (Rust’s proptest-state-machine). Each step draws a transition from the current state and applies it. A transition that fails its precondition is redrawn; after three rejections in a row, the program ends at that step. Failures print as state.apply(<transition>). No swarm testing.

run_typed_state_machine_as_test, run_typed_state_machine

run_typed_state_machine_as_test[M: TypedStateMachine](settings=Settings())
run_typed_state_machine[M: TypedStateMachine](mut data: ConjectureData, max_steps: Int, deadline_ns: Int = -1)

As for StateMachine.

Command

trait Command(Copyable, Deinitable, Writable):
    comptime Model: Copyable & Deinitable
    comptime Sut: Deinitable

    @staticmethod
    def generate(model: Self.Model, mut data: ConjectureData) raises -> Self
    def precondition(self, model: Self.Model) raises -> Bool       # default True
    def next_state(self, mut model: Self.Model) raises             # default: nothing
    def run(self, model: Self.Model, mut sut: Self.Sut) raises     # default: nothing

One operation in a model-based test (RapidCheck’s rc::state::Command). run receives the model’s state before the command. All the commands of a program must have the same Model and Sut; this is checked at compile time.

Commands[*Cs]

A program: a sequence of commands of the types Cs, generated from a model state.

Prints as [Put(0, 0), Get(0)].

commands

commands[*Cs: Command](model, *, max_commands: Int = 50) -> CommandSequences[*Cs]
commands[*Cs: Command](model, *, weights: List[Int], max_commands: Int = 50) raises -> CommandSequences[*Cs]

A strategy for programs of up to max_commands commands, valid from model. Shrinks towards shorter programs, and towards the first command type. weights biases the choice of command type.

check_commands

check_commands[*Cs: Command](model, settings=Settings(), *, max_commands: Int = 50)

Runs programs on a fresh, default-constructed Sut (which must be Defaultable) for each test case.

run_commands

run_commands[*Cs: Command](model, mut sut, mut data, *, max_commands: Int = 50)

Draws a program and runs it on sut, inside a given_data test (RapidCheck’s rc::state::check).

Writing strategies: the low-level API

Most strategies are built from other strategies, with combinators, composite, or a struct whose do_draw calls data.draw. This page covers the layer beneath: the Strategy trait, the primitive choices a ConjectureData offers, and the tools for making collections that shrink well.

Strategy

trait Strategy(Deinitable, Movable):
    comptime Value: Drawable
    def do_draw(self, mut data: ConjectureData) raises -> Self.Value
    def label(self) -> UInt64      # default: derived from the type's name

do_draw produces one value. Callers use data.draw(strategy) (or the free function draw(data, strategy)), which wraps the call in a span labeled strategy.label(). The shrinker treats spans with the same label as interchangeable, so it can, for example, swap two list elements. Give a strategy a label of its own (with calc_label_from_name("..."), from proptest.internal.data) when its default, the type’s name, would make unrelated draws look alike.

Drawable

comptime Drawable = Movable & Writable & Deinitable

What a strategy’s values must be: movable, printable for reports, and destructible. Not necessarily Copyable.

Primitive choices

All generation comes down to these ConjectureData methods. Each records one choice, which the shrinker can then simplify.

forced= makes the choice take a given value while still recording it, which keeps the choice sequence’s shape the same whether or not a value is forced.

Some rules for strategies that make primitive choices:

• Make the simplest choice give the simplest value. The shrinker moves each choice towards its simplest form (0, False, the empty string), so arrange that this produces the value you’d want in a minimal example.
• Keep generation deterministic. The same choices must produce the same value, and make the same further choices. Don’t consult the clock, a separate random generator, or captured mutable state.
• Prefer drawing over filtering. Draw values in a form that’s always valid instead of rejecting invalid ones.

Spans

data.start_span(label: UInt64)
data.stop_span(discard: Bool = False)

Group the choices between them into a span. data.draw does this for you. Use them directly for structure inside a strategy, such as one span per element. discard=True marks the span’s choices as not contributing to the value, as for a rejected draw.

Collections: Many

Many decides when a collection should stop growing, in a way that shrinks well (Hypothesis’s many). Each element is preceded by a boolean “keep going” choice, inside a span with the element, so deleting the span deletes the element:

from proptest import Strategy, ConjectureData, Many, integers, example

struct EvenLists(Copyable, Strategy):
    comptime Value = List[Int]

    def __init__(out self):
        pass

    def do_draw(self, mut data: ConjectureData) raises -> List[Int]:
        var out = List[Int]()
        var elements = Many(0, 10)                # min_size, max_size
        while elements.more(data):
            var x = data.draw(integers(0, 100))
            if x % 2 != 0:
                elements.reject(data)             # doesn't count; may stop early
                continue
            out.append(x)
        return out^

def main() raises:
    print(example(EvenLists()))

Many(min_size, max_size, avg_size=) takes an optional average size. reject drops the current element; after too many rejections, Many stops the collection, or rejects the test case if it’s below min_size.

Rejecting a test case

data.mark_invalid(why: String = "")

Abandons the test case as invalid (what assume(False) and filters do). The why is counted in the filter_too_much health check’s report.

Type erasure: BoxedStrategy

BoxedStrategy[T] holds any Copyable strategy with values of type T, behind a pointer and a few function pointers. boxed(s) makes one. Use it for collections of strategies (one_of with a list), recursion, and return types that would otherwise be long. A draw through a box costs an indirect call.

Running the engine directly

run_test(test_fn, settings, name) runs a def(mut ConjectureData) raises function under the full engine and returns a RunReport. It’s what given, given_data, and the state machine runners are built on.

Glossary

Choice. A single primitive decision made while generating a test case: an integer, float, boolean, byte string, or string, drawn under constraints such as a range.

Choice sequence. The choices a test case made, in order. Strategies build values from it, so replaying the sequence rebuilds the values. The example database, reproduce blobs, and the shrinker all work on choice sequences.

Command. In model-based testing, a struct representing one operation: it generates itself from the model, updates the model, and runs on the system under test.

Constraint type. A wrapper type such as Positive[T] or NonEmpty[T] that puts a constraint on generated values in the type.

Coverage requirement. A declaration, with cover, that some share of test cases should satisfy a condition.

Distinct failure. A failure with its own origin, the location its error was raised. Distinct failures are shrunk and reported separately.

Example database. The directory where proptest saves the choice sequences of failing test cases, to replay them in later runs.

Explain phase. After shrinking, the phase that finds which arguments of the minimal example can vary without changing the failure.

Explicit example. An input given by hand to check_examples, always tested, never shrunk.

Health check. A check that the test can be tested well: that its strategies don’t reject too much, or generate data too large or too slow.

Invalid test case. A test case rejected by assume, a filter, or Outcome.discard(). Invalid test cases don’t count towards max_examples.

Minimal example. The failing input proptest reports: the result of shrinking.

Model. A simple value describing the state a system under test should be in, used to check the system’s behaviour.

Overrun. A test case abandoned because it made too many choices.

Property. A statement that should hold for every input in a domain, written as a test function.

Shrinking. Searching for a simpler failing test case by simplifying the choice sequence of a failing one.

Span. A run of choices that together make one value, recorded by data.draw. The shrinker uses spans to delete, reorder, and simplify values.

State machine. A stateful test, defined as rules or transitions that are run in random sequences against a system.

Strategy. A description of the values a test should be given: a struct conforming to Strategy, which draws a value from a ConjectureData.

SUT. System under test.

Swarm testing. Disabling a random subset of a state machine’s rules in each test case, to make lopsided programs more likely.

Targeting. Steering the search towards inputs with high scores, reported with data.target.

Test case. One run of the test function on one generated input.