Property-based testing for the Nix language
Find a file
Repository files (latest commit first)
Filename Latest commit message Latest commit date
natsukium 75f8c9c6ad
Document what check cannot catch
The README claimed a type mismatch inside a predicate counts as a failure. It
does not: on Nix 2.34 `builtins.tryEval` catches `throw` and a failed `assert`
and nothing else, so `1 + "s"`, `{ }.a`, `head [ ]`, division by zero, `abort`
and infinite recursion all abort the whole run. Anyone relying on the old
sentence would have read a crashed suite as a broken library.

The same check turned up two more claims that no longer hold. `==` on two
functions is not an error in 2.34, it is `false` — even for `f == f` — so the
reason to keep `gen.anythingWith { functions = ...; }` off by default is that
reflexivity-shaped properties silently fail, not that they crash.

Collect these, the lost error message, the unguarded generator, the
version-bound seeds and the search budgets (filter retries, maxDiscards,
greedy shrinking, the 32-bit LCG) into one Limitations section, so the
failure modes are findable before they are hit rather than after.

Assisted-by: Claude Code:Fable 5.1
2026-09-14 00:25:50 +09:00
adapters Classify test cases with label, classify, collect and cover 2026-09-14 00:00:38 +09:00
examples Add gen.anything and gen.json 2026-09-14 00:21:49 +09:00
lib Document what check cannot catch 2026-09-14 00:25:50 +09:00
tests Add gen.anything and gen.json 2026-09-14 00:21:49 +09:00
default.nix Add gen.anything and gen.json 2026-09-14 00:21:49 +09:00
flake.lock Initial commit: nixcheck, property-based testing for Nix 2026-07-06 14:53:57 +09:00
flake.nix wip 2026-09-12 02:07:28 +09:00
README.md Document what check cannot catch 2026-09-14 00:25:50 +09:00

nixcheck

Property-based testing for the Nix language, with integrated (Hedgehog-style) shrinking. Pure, reproducible, and dependency-free — the core needs neither nixpkgs nor lib.

Instead of writing example-based tests (assert f 2 == 4), you state a property that should hold for all inputs and let nixcheck generate hundreds of cases. When one fails, it automatically shrinks the counterexample to a minimal one.

[ 81 27 60 11 63 96 95 ]   ← first random counterexample
[ 1 0 ]                    ← shrunk: the smallest input that still fails

Why integrated shrinking

Nix has no type classes, so a generator must always be passed explicitly — which is exactly the Hedgehog model. Generators carry their shrink tree with the value, so anything you build by composing map / bind / listOf / record shrinks for free. You never write a separate shrinker.

Quick start

let
  nixcheck = import ./nixcheck;                 # or inputs.nixcheck.lib
  inherit (nixcheck) gen range forAll check;

  # A property: reversing a list twice returns the original.
  prop = forAll
    (gen.listOf (range.linear 0 20) (gen.int (range.linearFrom 0 (-100) 100)))
    (xs: builtins.elemAt [ (lib.reverseList (lib.reverseList xs)) ] 0 == xs);
in
check { tests = 100; seed = 42; } prop
# => { ok = true; testsRun = 100; discarded = 0; labels = { }; }
#    or { ok = false; testsRun = N; discarded = D;
#         failure = { original = ...; shrunk = ...; shrinkSteps = ...;
#                     seed = ...; size = ...; index = ...; }; }

Run the shrinking demo (a deliberately broken sort):

$ nix eval --json -f examples/demo.nix
{ "discarded": 0, "failure": { "original": [21,2], "shrunk": [1,0], "shrinkSteps": 6,
  "seed": 20260706, "size": 25, "index": 25 }, "labels": {}, "ok": false, "testsRun": 26 }

API

Generators (gen.*)

Generator Description
gen.constant v always v, no shrinks
gen.int range integer from a range, shrinks toward its origin
gen.float range float from a range, shrinks toward its origin, with edge values
gen.floatWith { range; allowInfinite ? false; allowNaN ? false; } gen.float with the non-finite values opted in
gen.bool true shrinks to false
gen.elements xs one element of xs, shrinks toward the first
gen.map f g transform values (shrinking preserved)
gen.filter pred g redraw until pred holds; discards if it never does
gen.bind g f dependent generation (shrinking preserved)
gen.oneOf gens uniformly pick one generator, shrinks toward the first
gen.frequency [ [ w g ] ... ] weighted pick, shrinks toward the first
gen.vectorOf n g list of exactly n elements
gen.listOf lenRange g variable-length list (elements are dropped when shrinking)
gen.nonEmptyListOf lenRange g like listOf, but never the empty list
gen.uniqueListOf lenRange g listOf whose elements are pairwise distinct
gen.subsequence xs some elements of xs, in order, shrinks toward [ ]
gen.shuffle xs a permutation of xs, shrinks toward the original order
gen.stringOf lenRange chars string over an alphabet (a character list or a character generator)
gen.string lenRange gen.stringOf over printable ASCII
gen.digit / gen.lower / gen.upper one-character string: 0–9 / a–z / A–Z
gen.alpha / gen.alphaNum one ASCII letter / one letter or digit
gen.printable one printable ASCII character (0x20–0x7E)
gen.ascii one ASCII byte (0x01–0x7F), control characters included
gen.unicode one multibyte code point (accents, CJK, RTL, combining, emoji)
gen.record { k = g; ... } attrset with per-field generators
gen.attrsOf lenRange keyGen valueGen attrset with generated keys and values, sheds keys when shrinking
gen.attrsWith keys valueGen attrset over a subset of keys, shrinks toward { }
gen.optional g null (absent) or { value = v; } (present), shrinks toward absent
gen.recordWith { required; optional; } attrset whose optional fields may be missing
gen.sized f build a generator from the current size
gen.scale f g run g at size f size
gen.small g g at half size
gen.recursive choose leaves nodes recursive generator with size-bounded depth
gen.anything an arbitrary Nix value: null, bool, int, float, string, list, attrset
gen.anythingWith { floats ? true; functions ? false; paths ? false; unicode ? true; } gen.anything with the awkward value kinds toggled
gen.json gen.anything restricted to what builtins.toJSON round-trips
gen.discard / gen.isDiscard the discard sentinel and its test

gen.frequency takes a list of [ weight generator ] pairs (weights must be positive integers) and draws each alternative with probability weight / total. gen.oneOf gens is gen.frequency with weight 1 on every alternative. Both shrink across alternatives: the chosen index is shrunk toward 0 before the value inside it, so a counterexample first migrates to an earlier alternative and is then minimised there.

Floats

gen.float range reads the range's bounds as floats, so an integer-valued range works unchanged and the result is always a float:

gen.float (range.linearFrom 0.0 (-1.5) 2.5)

Shrinking pulls toward the range's origin, in this order: the origin itself, then the nearest whole number on the way to it (so a counterexample that does not depend on the fractional part becomes an integer), then the points halving the remaining distance. Halving stops once the distance is below 1e-9, so an alwaysFails property over range.linearFrom 0.0 (-100.0) 100.0 shrinks to exactly 0.0, while "this value is a whole number" shrinks to a tiny fraction rather than to 0.0.

Edge values. Uniform sampling over a wide range essentially never produces the numbers that actually break callers, so one draw in ten is an edge value: the bounds, the origin, and ±2^53, ±9.3e18, ±1e100 when the range contains them. Edge values carry the ordinary shrink tree, and because gen.frequency shrinks toward its first alternative (the uniform draw), an edge counterexample migrates back to an ordinary value and is then minimised there.

Nix float caveats, all of which this generator is shaped around:

  • -0.0 evaluates to 0, so there is no negative zero to generate.
  • 1.0 / 0.0 is an evaluation error; inf only arises from overflow (1.0e308 * 10.0) and nan from inf - inf. Both are outside any finite bounds, so they are opt-in: gen.floatWith { range; allowInfinite = true; allowNaN = true; }. Test for nan with x != x — nan == nan is false, and builtins.toJSON renders both as null.
  • builtins.floor and builtins.ceil throw on any float outside the NixInt range (1.0e100, 9.3e18, inf, nan), and that throw is not catchable with builtins.tryEval — it aborts the whole run instead of counting as a failing case. This is the main bug class the large edge values target; a predicate that floors a generated float must bound its magnitude itself.

Strings

gen.string lenRange is the everyday one — printable ASCII, length from lenRange:

gen.string (range.linear 0 10)      # "" | "k" | "R7" | "a.q" | …

It is gen.stringOf lenRange over the printable alphabet, and gen.stringOf takes either a list of one-character strings or a character generator, so an alphabet with a deliberate distribution needs no extra combinator:

gen.stringOf (range.linear 0 8) [ "a" "b" ]                 # a list
gen.stringOf (range.linear 0 8) gen.digit                   # a generator
gen.stringOf (range.linear 0 8) (
  gen.frequency [ [ 9 gen.printable ] [ 1 gen.unicode ] ]   # mostly ASCII
)

The single-character generators are gen.digit, gen.lower, gen.upper, gen.alpha, gen.alphaNum, gen.printable, gen.ascii and gen.unicode. Each is gen.elements over a fixed alphabet, so each shrinks toward that alphabet's first entry: the alphabets are ordered simplest-first (letters, then digits, then symbols) rather than in ASCII order, so a counterexample over printable ASCII lands on "a" and not on a space or a backtick.

Strings are lists underneath, so they inherit list shrinking: a counterexample drops the characters it does not need before simplifying the rest. An always-failing property over gen.string (range.linear 0 10) shrinks to "", and "contains no z" shrinks to exactly "z".

Two things worth knowing about the byte-level sets:

  • gen.ascii starts at 0x01, not 0x00. A Nix string cannot hold a NUL byte at all, and the error saying so is not catchable with builtins.tryEval — a generated NUL would abort the whole run instead of failing one case. Everything from 0x01 to 0x7F is fair game, control characters included.
  • gen.unicode is deliberately multibyte. It draws from a curated set of code points (é, ß, CJK ideographs, a Hebrew letter, a right-to-left mark, a combining acute, a zero-width joiner, astral-plane emoji) chosen so that builtins.stringLength — which counts bytes — disagrees with the character count on every single one. Code that slices strings with builtins.substring breaks on these, which is the point.

Lists

gen.listOf lenRange g shrinks a list by removing elements from anywhere in it and then minimising the survivors (tree.interleave, Hedgehog's Shrink.list): first whole halves, then quarters, down to single elements. Removing a chunk and shortening the list is one step, which is what lets [ 5 0 0 0 7 ] reach [ 5 7 ] — a shrinker that could only drop a suffix would have to keep the zeros to keep the 7. Removal stops at the length range's lower bound at the current size, so a range.constant 2 5 list never shrinks below two elements. gen.vectorOf n g has no removals at all: its length is fixed, so only its elements shrink.

gen.nonEmptyListOf clamps the drawn length to at least one, per size, so a range whose upper bound is still 0 at small sizes stays usable; a range that can never reach one element (range.constant 0 0) is an error.

gen.uniqueListOf is gen.filter over a listOf draw: a list containing a duplicate (compared with ==) is redrawn rather than deduplicated, so the drawn length is the resulting length. The price is a discard when the element generator's domain is too small to fill the drawn length — see Filtering and discards.

gen.subsequence xs keeps each element of xs independently, preserving order, and shrinks toward [ ]. gen.shuffle xs always yields a permutation of xs; it draws an index into the remaining elements at each step, and since those indices shrink toward 0, a counterexample shrinks back to the original order.

Attrsets

gen.record fixes the key set. When the keys themselves should vary, use gen.attrsOf lenRange keyGen valueGen: it draws a list of name/value pairs and collapses it with builtins.listToAttrs. A draw whose names collide is rejected and redrawn, so the drawn length is the entry count; a key generator whose domain is too small to fill it discards the case rather than quietly returning a shorter attrset — see Filtering and discards. Being a list underneath, it inherits list shrinking: a counterexample drops the individual keys it does not need, not just the last ones.

gen.attrsWith keys valueGen takes a list of key strings and keeps each key independently, with a value from valueGen. It shrinks toward { }, so a counterexample sheds every key it does not need before its values are minimised.

gen.attrsWith [ "a" "b" "c" ] (gen.int (range.constant 0 9))
# => { } | { b = 4; } | { a = 0; c = 7; } | …

Optional values

gen.optional g generates null for absent and { value = v; } for present. The wrapper is deliberate: null | v would make a generated null — a perfectly ordinary Nix value — indistinguishable from absence. Match on it with if o == null then ... else o.value. Absence is common at small sizes, rarer as the size grows, and "present → absent" is the first shrink step.

gen.recordWith is the usual consumer: optional fields are simply missing from the generated attrset (never wrapped), and a counterexample sheds them before the remaining fields are minimised. A key declared both required and optional is an error.

gen.recordWith {
  required = { name = gen.stringOf (range.linear 1 8) [ "a" "b" ]; };
  optional = { description = gen.constant "…"; priority = gen.int (range.linear 0 9); };
}
# => { name = "ab"; } | { name = "ab"; priority = 3; } | …

Filtering and discards

gen.filter pred g draws from g until the value satisfies pred, advancing the rng and raising the size by one on each retry (so a predicate only larger draws can satisfy still terminates). It also prunes the shrink tree: every shrink candidate satisfies pred too, so a minimised counterexample is still a value your property is defined on.

gen.filter (xs: xs != [ ]) (gen.listOf (range.linear 0 10) gen.bool)

A rejected branch is pruned whole rather than descended into. Its children might satisfy pred, but reaching them would route the shrink through a value the filter excluded, and "smaller" is only meaningful among the values pred admits.

After 100 failed attempts the draw becomes a discard — the sentinel gen.discard, recognised by gen.isDiscard. A discarded case is neither a pass nor a failure: check does not count it toward tests, adds it to discarded, and draws another case. Once discarded reaches maxDiscards (default tests * 10) the run gives up:

check { tests = 100; maxDiscards = 50; } (forAll (gen.filter (_: false) gen.bool) (_: true))
# => { ok = false; testsRun = 0; discarded = 50; gaveUp = true; }

There is no failure in a give-up report: a property that never ran has not been falsified, it has not been tested. Both adapters print the discard count and report a give-up distinctly from a counterexample.

A predicate may discard too, by returning discard — QuickCheck's ==> for conditional properties:

forAll (gen.int (range.linear 0 100)) (x: if x < 10 then discard else f x == g x)

Prefer gen.filter where you can: a filtered generator retries within the draw, while a discarding predicate throws the whole case away, so a narrow condition burns through maxDiscards much faster.

Filtering happens at the level of the whole draw: a discard anywhere inside a composite generator discards the case, never appearing as a component of the generated value. A list element, a vector element, a record field, an attrsOf entry or key, an optional payload — if its draw discards, the whole [ ... ] / { ... } is the sentinel and check drops the case, exactly as in Hedgehog. gen.map and gen.bind pass the sentinel along untouched for the same reason.

Recursive generators

gen.recursive choose leaves nodes builds a self-referential generator. Every recursive occurrence runs at half the current size, so nesting depth is bounded by log2 size and stays under the runner's control: small tests generate flat values, large ones nested ones, and shrinking the size shrinks the depth. choose receives a plain list of generators — use gen.oneOf, or a lambda for weights, e.g. (gens: gen.frequency (map (g: [ 1 g ]) gens)).

# JSON-like nested lists. No depth counter: `let` is lazy and the size guard
# terminates the unfolding.
genNested = gen.recursive gen.oneOf
  [ (gen.int (range.constant 0 9)) ]
  [ (gen.listOf (range.constant 0 2) genNested) ];

Because choose shrinks toward its first alternative and the leaves are listed first, a deeply nested counterexample shrinks all the way back to a leaf.

Arbitrary values

A property whose subject is any Nix value — lib.id x == x, "mapping the identity over an attrset changes nothing", a serialiser round trip — is usually tested against a hand-rolled generator of integers, which proves it for integers. gen.anything generates the whole language instead: null, a bool, an int, a float, a string, or a list or attrset of more of the same.

gen.anything
# => null | true | -3 | 0.5 | "k" | [ ] | [ "" { a = 7; } ] | { qL = [ null ]; } | …

It is gen.recursive underneath, so nesting depth is bounded by the test size and shrinking unwraps it: the leaves are listed simplest-first with null first, so a counterexample climbs out of its nesting and bottoms out at null unless the property needs more than that.

gen.anythingWith toggles the value kinds that not every property can handle:

Option Default Why it is a switch
floats true some subjects are integer-only
functions false == on two functions is false, even for f == f
paths false builtins.toJSON of a path copies it into the store
unicode true a byte-oriented consumer chokes on a wide character

Integers reach ±(2^62 − 1) over an exponential range, so the magnitudes where Nix integer arithmetic overflows are reachable but the orders of magnitude in between still get their share of the draws. Floats stop at ±10^12 on purpose: builtins.floor throws — uncatchably — above 2^63, so a wider default would make ordinary-looking properties abort the run instead of failing a case.

gen.json is gen.anythingWith { unicode = false; }: no functions, no paths, ASCII strings and keys, no inf/nan. Everything it draws survives a JSON round trip, which makes it the generator for anything serialisation-shaped:

forAll gen.json (v: builtins.fromJSON (builtins.toJSON v) == v)

That round trip is exact, which is worth stating because the JSON data model suggests otherwise: Nix renders the float 1.0 as 1.0 rather than 1 and reads it back as a float, so whole-numbered floats need no special casing, and it renders enough digits to restore any float bit-for-bit.

Ranges (range.*)

Range Bounds at size s Shrinks toward
range.constant min max [min, max], size-independent min
range.constantFrom origin min max [min, max], size-independent origin
range.linear min max upper bound grows linearly to max min
range.linearFrom origin min max same origin
range.exponential min max bounds grow geometrically to max min
range.exponentialFrom origin min max both sides grow geometrically away from origin origin

linear* grows the upper bound with the test size (small inputs first). The same constructors serve gen.float: their arithmetic promotes, so range.linearFrom 0.0 (-1.5) 2.5 is a float range and needs no separate constructor.

exponential* interpolates each side from the origin with origin ± ((|bound - origin| + 1) ^ (size / 100) - 1), so the magnitude of the interval — not its width — grows at a constant rate. Over a range as wide as 1 .. 2^62 that is the difference between spending nine sizes in ten above 10^17 and spending them evenly across the orders of magnitude:

(range.exponential 1 4611686018427387904).bounds 50
# => { lo = 1; hi = 2147483648; }   # 2^31, the geometric midpoint

Size 0 yields exactly the origin and size 100 exactly the endpoints, both by construction rather than to within a rounding error. Integer endpoints give integer bounds, rounded toward the origin so the interval never widens past the float; a float endpoint keeps the float, so gen.float gets the same distribution over range.exponentialFrom 0.0 0.0 1.0e100. (Nix has neither pow nor sqrt, so the exponentiation is done by repeated square roots on [1, 2] — see lib/range.nix.)

Running

  • forAll gen predicate → a Property
  • check { tests ? 100; seed ? 42; maxShrinks ? 1000; maxSize ? 100; maxDiscards ? tests * 10; replay ? null; } property → a Report
  • sample { tests ? 100; seed ? 42; maxSize ? 100; } gen → [ value ]
  • sampleTree { ... } gen → [ Tree value ] (the same draws, shrink trees included)

A Report always carries ok, testsRun, discarded and labels (the distribution of the cases that ran, see Classifying test cases). A falsified one adds failure, one that missed a cover demand adds coverage, and one that ran out of discards adds gaveUp = true instead — a run can carry both failure and coverage, but a give-up has neither.

A throw or a failed assert inside the predicate counts as a failure rather than aborting the run (via builtins.tryEval). Other evaluation errors do not — see Limitations. Returning discard instead drops the case; see Filtering and discards.

Classifying test cases

A property that passes tells you nothing about what it was tested on: a generator can drift until every case is trivial and the suite stays green. classify, collect and cover make the distribution part of the report.

Hedgehog does this from inside the generator monad; Nix has none, so these are pure wrappers around the predicate's result. A predicate may return a labelled result — { ok; labels ? [ ]; covers ? [ ]; } — instead of a bool, and the wrappers nest:

  • label name result — tag this case with name
  • classify cond name result — tag it only when cond holds
  • collect value result — tag it with the value itself (a string as-is, anything else via builtins.toJSON)
  • cover minPercent name cond result — classify, plus a demand that at least minPercent of the cases carry name

Report.labels counts, per name, the cases that ran; it is always present and { } when nothing was labelled. Discarded cases did not run, so they count toward nothing.

# How often is an optional value absent?
check { tests = 100; } (
  forAll (gen.optional (gen.int (range.linear 0 100))) (
    o: classify (o == null) "absent" (classify (o != null) "present" true)
  )
)
# => { ok = true; testsRun = 100; discarded = 0;
#      labels = { absent = 7; present = 93; }; }

cover turns a distribution demand into a check. If the run ends below the demanded percentage, ok is false and coverage lists what was missed — even though no counterexample was found:

# gen.float spends one draw in ten on an edge value; demand that we see them.
check { tests = 100; } (
  forAll (gen.float (range.constant 0.0 1.0)) (
    x: cover 5 "an edge value" (x == 0.0 || x == 1.0) (x >= 0.0 && x <= 1.0)
  )
)
# => { ok = true; testsRun = 100; discarded = 0;
#      labels = { "an edge value" = 12; }; }
#    or, had the edges dried up:
#    { ok = false; ...; coverage = [ { name = "an edge value";
#                                      minPercent = 5; actualPercent = 2.0; } ]; }

A counterexample and insufficient coverage are reported side by side: failure and coverage both appear, and failure is the one to look at first. A replay run still collects labels, but skips the coverage check — over a single case every demand would read as 0% or 100%.

Both adapters surface the distribution: flake-check.nix prints one line per label (commonest first) and a COVERAGE: block when a demand was missed, and run-summary.nix reports labels per property and counts a coverage failure as a failure.

Sampling

sample draws values from a generator without running a property — useful for eyeballing a new generator's distribution in nix repl. It shares the case construction with check, so for a given seed the i-th sampled value is exactly the i-th value check feeds the predicate (sizes cycle 0..maxSize the same way).

sample { tests = 5; seed = 42; } (gen.int (range.linear 0 100))
# => [ 0 0 1 2 0 ]

sampleTree returns the Trees instead, so you can inspect the shrink candidates a value would offer.

Both skip discarded draws — exactly the cases check would drop — so a filtered generator may return fewer than tests values.

Reproducing a failure

A failure carries everything needed to run that one case again:

failure = {
  original = ...;      # the first counterexample found
  shrunk = ...;        # the minimal one
  shrinkSteps = ...;
  seed = 20260706;     # the seed passed to `check`
  size = 25;           # the size that case ran at
  index = 25;          # its position in the run
};

check { replay = { seed; index; }; } runs only that case — with the rng state and size it had originally — and shrinks it, so a CI failure reproduces locally in a fraction of a second:

check { replay = { seed = 20260706; index = 25; }; } prop
# => { ok = false; testsRun = 1; failure = { ... }; }

A failure record can be passed verbatim (replay = report.failure). Replay is keyed on seed and index only: size is reported for information, being implied by index and maxSize, so a replay must use the same maxSize as the original run. Replaying a case that passes yields { ok = true; testsRun = 1; }.

Both adapters print the reproduction line on failure, so a nix flake check log says exactly which replay to use.

Limitations

builtins.tryEval catches only throw and assert. check evaluates the predicate under tryEval, so a property that throws (or trips an assert) on some input is falsified by it. Nothing else is caught. All of these abort the entire check instead of failing one case:

  • abort, infinite recursion, stack overflow;
  • type errors (1 + "s", applying a non-function);
  • a missing attribute ({ }.a), builtins.head [ ], an out-of-bounds builtins.elemAt, division by zero;
  • builtins.floor / builtins.ceil on a float outside the NixInt range (verified on Nix 2.34), builtins.toJSON of a function, a string that would contain a NUL byte.

If a property can reach one of those, guard it yourself — (builtins.tryEval …).success converts a catchable error into a bool, and an explicit bound (if magnitude < 4.0e18 then … else true) is the only defence against the rest.

A report never says why. tryEval yields success = false and no message, so a failure tells you which input broke the property and never what the error was. To see it, evaluate the predicate on failure.shrunk by hand, or re-run the single case with check { replay = report.failure; } and read the trace.

The generator is not guarded. Only the predicate runs inside tryEval. A generator that throws — a gen.map over a partial function, say — aborts the run rather than failing a case.

Seeds are not stable across versions. Changing any combinator, any range, or the rng changes the random stream, so a seed/index pair reproduces a failure only against the same build of nixcheck. Keep the shrunk counterexample as a regression test; treat the seed as a same-version convenience.

Floats. -0.0 evaluates to 0, so there is no negative zero to generate. 1.0 / 0.0 is an evaluation error, so inf only arises from overflow and nan from inf - inf; both lie outside any finite bounds and are opt-in via gen.floatWith. See Floats.

Functions compare as unequal, not as an error. (x: x) == (x: x) is false, and so is f == f. Any reflexivity-shaped property therefore fails on a generated lambda, which is why gen.anythingWith keeps functions off.

Budgets that quietly bound the search.

  • gen.filter retries 100 times per draw, then discards.
  • check gives up once discarded reaches maxDiscards (default tests * 10).
  • Shrinking stops after maxShrinks steps (default 1000) and is greedy: it descends into the first failing child at each node, so the reported counterexample is a local minimum, not necessarily the smallest one.
  • gen.int draws from hi - lo + 1, so a range spanning more than the whole NixInt width overflows inside the generator.
  • rng is a 32-bit LCG: a run has at most ~4×10⁹ distinct states, and rng.below is modulo-biased for large bounds.

Performance. A check is a single Nix evaluation — one thread, no cache between runs, memory growing with the cases retained. It draws tests + maxDiscards cases (lazily, so the unused ones cost nothing). One derivation per property under nix flake check is the only parallelism on offer today.

Extending

Everything is a plain function or attrset — no magic. A domain generator is just a composition:

# Generate "MAJOR.MINOR.PATCH" version strings. Shrinking comes for free.
genVersion = gen.map
  ({ major, minor, patch }: "${toString major}.${toString minor}.${toString patch}")
  (gen.record {
    major = gen.int (range.linear 0 9);
    minor = gen.int (range.linear 0 20);
    patch = gen.int (range.linear 0 50);
  });

Architecture

adapters/     nix-unit / flake-check / CLI integration
property.nix  forAll / check / sample        (runner strategy)
gen.nix       int, list, record, anything…  (extension surface)
range.nix     distribution & size scaling   (a peer gen.nix is handed,
                                             not one it imports)
tree.nix      lazy rose tree (map / bind /
              interleave)                   ┐ stable core
rng.nix       splittable PRNG (split / next) ┘

The three conventions everything agrees on:

Gen a    = size: rng: Tree a
Tree a   = { value : a; shrinks : [ Tree a ]; }
Report   = { ok; testsRun; discarded; labels; gaveUp?;
             failure? = { original; shrunk; shrinkSteps; seed; size; index; };
             coverage? = [ { name; minPercent; actualPercent; } ]; }

Flake

  • nixcheck.lib — the API above
  • nix flake check — runs the nixpkgs lib example properties and nixcheck's own dogfooding suite, one derivation per property

Status

v0.1 — the core (splittable RNG, integrated shrinking, generators, runner, labels and coverage) is in place and self-tested. Planned: a nix-unit adapter, a parallel (derivation-per-seed) runner, and reporting the error message behind a failure rather than only the input (see Limitations).