- Nix 100%
| Filename | Latest commit message | Latest commit date |
|---|---|---|
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
|
||
| adapters | ||
| examples | ||
| lib | ||
| tests | ||
| default.nix | ||
| flake.lock | ||
| flake.nix | ||
| README.md | ||
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.0evaluates to0, so there is no negative zero to generate.1.0 / 0.0is an evaluation error;infonly arises from overflow (1.0e308 * 10.0) andnanfrominf - inf. Both are outside any finite bounds, so they are opt-in:gen.floatWith { range; allowInfinite = true; allowNaN = true; }. Test fornanwithx != x—nan == nanis false, andbuiltins.toJSONrenders both asnull.builtins.floorandbuiltins.ceilthrow on any float outside theNixIntrange (1.0e100,9.3e18,inf,nan), and that throw is not catchable withbuiltins.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.asciistarts at0x01, not0x00. A Nix string cannot hold a NUL byte at all, and the error saying so is not catchable withbuiltins.tryEval— a generated NUL would abort the whole run instead of failing one case. Everything from0x01to0x7Fis fair game, control characters included.gen.unicodeis 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 thatbuiltins.stringLength— which counts bytes — disagrees with the character count on every single one. Code that slices strings withbuiltins.substringbreaks 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→ aPropertycheck { tests ? 100; seed ? 42; maxShrinks ? 1000; maxSize ? 100; maxDiscards ? tests * 10; replay ? null; } property→ aReportsample { 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 withnameclassify cond name result— tag it only whencondholdscollect value result— tag it with the value itself (a string as-is, anything else viabuiltins.toJSON)cover minPercent name cond result—classify, plus a demand that at leastminPercentof the cases carryname
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-boundsbuiltins.elemAt, division by zero; builtins.floor/builtins.ceilon a float outside theNixIntrange (verified on Nix 2.34),builtins.toJSONof 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.filterretries 100 times per draw, then discards.checkgives up oncediscardedreachesmaxDiscards(defaulttests * 10).- Shrinking stops after
maxShrinkssteps (default1000) 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.intdraws fromhi - lo + 1, so a range spanning more than the wholeNixIntwidth overflows inside the generator.rngis a 32-bit LCG: a run has at most ~4×10⁹ distinct states, andrng.belowis 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 abovenix flake check— runs the nixpkgslibexample 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).