1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; pbt.lisp — property-based testing with shrinking, and a dual
;; sample -> exhaust mode. Pure Lisp, zero interpreter changes, same
;; library pattern as fsm.lisp / testkit.lisp / symreg.lisp.
;;
;; A PROPERTY is a 1-argument boolean predicate over generated inputs.
;; A GENERATOR is a 0-argument function that draws one value from the
;; shared seeded PRNG (reseed with (pbt-seed! n) for reproducible runs).
;;
;; TWO modes, with DELIBERATELY different verdicts so the claim can't be
;; overstated:
;;
;; (pbt-check prop gen n) — SAMPLE mode. Draw n seeded cases; on the
;; first failure, delta-debug SHRINK it to a minimal counterexample and
;; return it as data. Verdict on success is 'passed — the honest claim
;; is "no counterexample in n seeded draws", NEVER 'verified. Absence in
;; a sample is not absence.
;;
;; (pbt-verify prop domain) — EXHAUST mode. Hand the property to
;; check-exhaustive over an EXPLICIT finite input set: it runs the
;; property on every element, so success is 'verified (a real proof over
;; the declared domain, per the bounded-verification rule) and failure
;; still shrinks the first counterexample to minimal. This is the Rusty
;; angle — on a small finite domain a property test UPGRADES from a
;; sample into a proof, reusing the same shrinker for the witness.
;;
;; Shrinking is type-directed and generic (numbers toward 0, lists by
;; deleting elements then shrinking them), greedy first-failing, so the
;; minimal counterexample is a deterministic function of the failing input
;; — same seed => same original => same minimal (pinned in the golden).
;; "Minimal" is minimal under the declared size metric (pbt-size): it is a
;; local minimum of the greedy search, not a global one.
;;
;; Claim discipline: 'verified means "ran everywhere on the DECLARED finite
;; domain", 'passed means "no counterexample sampled" — never "correct" or
;; "safe". A raise from a property counts as NOT holding (boolean-strict,
;; like check-exhaustive since 0.62.1: only #t holds).
;; ── Seeded PRNG (same LCG as symreg.lisp) ────────────────────────────────
; int in 0..n-1
;; ── Generators: each is a thunk drawing one value from the PRNG ──────────
;; ── Does the property hold on v? Boolean-strict: only #t holds; a #f,
;; a non-boolean, or a raise all count as a FAILURE (a counterexample). ───
;; ── Size metric — what "minimal" is minimised against ────────────────────
;; ── Shrink candidates: strictly-smaller values, most-aggressive first ────
;; All lists obtained by deleting exactly one element (each is shorter).
;; All lists obtained by shrinking exactly one element in place (recurses
;; into nested structure via pbt-shrinks).
;; ── Greedy delta-debugging shrink. Precondition: (prop v) fails. Take the
;; first still-failing candidate, adopt it, restart — until none fail. ────
;; ── SAMPLE mode: draw n cases; first failure shrinks to a minimal CE ─────
;; ── EXHAUST mode: prove over an explicit finite input set ────────────────
;; check-exhaustive runs prop on every element of `domain`; success is a
;; real proof over that declared set. On failure the first counterexample
;; is shrunk to minimal, reusing the sampler's shrinker.
;; Multi-argument exhaust passthrough: prop takes k args, `domains` is a
;; list of k finite domains — the raw cartesian-product proof/counterexamples.
;; ── Domain builder: every list over `alphabet` of length 0..max-len ──────