Property Testing Without the Boilerplate

Unit tests pin down known inputs. Property tests explore the *space* of inputs and ask whether an invariant holds across all of them. The gap between them has always been tooling. In Lateralus 0.5+ that tooling lives inside the compiler.

◉ The one-line version

Add #[property] above a function and the compiler synthesizes a shrinking driver for you:

#[property(runs = 500)]
fn reverse_twice_is_identity(xs: [Int]) -> Bool {
    xs |> reverse() |> reverse() == xs
}

That's it. lateralus test finds it. The compiler generates the driver, the RNG wiring, and the shrinker.

◉ How the compiler sees it

The analysis pass (property_check.ltl) walks the AST after type-check, finds every #[property] annotation, and emits a synthetic __prop_<name>() function marked #[test]. Generated code reads:

fn __prop_reverse_twice_is_identity() {
    let rng = std::rand::Rng::from_env()
    let failures = []
    for _ in 0..500 { __prop_one(rng, failures) }
    if len(failures) > 0 {
        panic("property failed after shrinking: {failures[0]}")
    }
}

The driver is a normal test. It shows up in your test runner output. It fails with a shrunk counterexample.

◉ Why a compiler pass and not a macro?

Lateralus has macros, but we chose a pass because:

It sees types

The arbitrary generator for [Int] is wired up by reading the argument type from the AST, not by asking the user to write any::<Vec<i32>>().

It runs after inference

Property functions can return Bool or Result<(), E> and we pick the right assertion shape at codegen time.

It composes with other passes

The observability pass (otel_emit.ltl) wraps property drivers in spans automatically — every property run shows up in your traces.

◉ Attributes you can tune

#[property(runs = 5000, max_shrink = 256, seed = 0xC0FFEE)]
fn sort_is_idempotent(xs: [Int]) -> Bool {
    let a = xs |> sort()
    let b = a  |> sort()
    a == b
}

- runs — how many samples to try (default 100) - max_shrink — shrink-step budget (default 128) - seed — pin an RNG for deterministic CI

◉ What's next

Stateful properties (think QuickCheck state machines) and coverage-guided input generation are both in-flight. Neither needs user-facing syntax changes — they slot into the same pass. Which is the whole point.