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
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; pcheck.lisp — Phase D: PARALLEL check-exhaustive over the proc-pmap builtin.
;;
;; check-exhaustive proves a property on EVERY point of a finite domain product
;; — real proof, not sampling. It is also embarrassingly parallel: the points
;; are independent. The Rusty core is Rc-based single-threaded on purpose, so
;; the ONE honest way to reach many cores is many PROCESSES. pcheck-exhaustive
;; shards the sweep across child `rusty` processes (proc-pmap) and merges their
;; verdicts.
;;
;; DETERMINISM (the whole point): check-exhaustive iterates the FIRST domain
;; OUTERMOST (slowest-varying). Split that first domain into CONTIGUOUS chunks
;; and give shard i chunk i x the other domains; concatenating the shards'
;; counterexamples in shard order reproduces the serial odometer order EXACTLY.
;; So the result is bit-identical regardless of shard count or worker count —
;; workers change the SPEED, never the ANSWER. That equivalence is the claim,
;; and pcheck-test.lisp pins it: (equal? (pcheck-exhaustive ...) serial-result).
;;
;; HONEST SCOPE (the caveat is the crack):
;; - A child that errors / times out / crashes is NOT "verified". It surfaces
;; as (pcheck-incomplete shard proc-result). Absence of a counterexample from
;; a shard that never finished is not evidence of its absence — never a false
;; 'verified.
;; - The property must be a BOOLEAN predicate. check-exhaustive's counterexample
;; reason is then uniformly "false", which is exactly what lets the merge
;; rebuild the serial result bit-for-bit. A property that RAISES on some input
;; is outside that contract: the shard child detects the non-"false" reason
;; and fails loudly (its proc-result becomes an error → pcheck-incomplete),
;; rather than mislabel a raised input as an ordinary counterexample.
;; - Per-child interpreter STARTUP is real overhead, so shards must be COARSE
;; enough that compute >> startup. Below that crossover serial check-exhaustive
;; wins — use it. See benchmarks/pcheck_bench.lisp for the measured crossover.
;; - The property and its helpers cross to a fresh child, so anything the
;; property references beyond builtins/std must be supplied as the `preamble`
;; source string. Domain values must be numbers/symbols (they round-trip
;; through the child's printed output; strings/quotes would not).
;; - proc-pmap drains a child's stdout AFTER it exits (like proc-eval). A shard
;; that emits enough counterexamples to fill the OS pipe buffer (~64 KB)
;; before it exits would block and be reported (timeout) -> pcheck-incomplete
;; rather than returning them. It fails SAFE (never a false 'verified), and
;; the target use — a mostly-PASSING safety property — never approaches it;
;; concurrent pipe draining is deferred.
;; ── datum -> source text ────────────────────────────────────────────────────
;; A property crosses to a child as TEXT, so render a datum back to source.
;; Strings are re-quoted so the round-trip is lossless (unlike print/display,
;; which drop the quotes).
;; ── sharding ────────────────────────────────────────────────────────────────
;; Split a list into at most n CONTIGUOUS chunks (ceil-sized; the last chunk
;; takes the remainder). Order-preserving and gap-free, which is what makes the
;; merge reproduce the serial sweep. n larger than the list just yields fewer,
;; smaller shards; never an empty one. One TAIL-RECURSIVE pass — std's `take`
;; is not tail-recursive and overflows the stack on the large domains this is
;; meant for, so we accumulate by hand instead.
;; ── child code ──────────────────────────────────────────────────────────────
;; Each shard child runs check-exhaustive on its sub-domain and prints a
;; PARSE-FREE protocol the parent can reconstruct losslessly:
;; "V" -> this shard verified (no counterexamples)
;; "C(args)\n" -> one counterexample; (args) is the printed argument list
;; A counterexample whose reason is not "false" (the property RAISED) is out of
;; contract: the child raises, so the shard reports incomplete rather than lie.
;; ── parsing one shard's result ──────────────────────────────────────────────
;; Reconstruct a counterexample line "C(1 -4 4)" back to data ((1 -4 4) "false").
;; The args round-trip via the quote trick; the reason is reattached as the
;; literal string "false" so the result is `equal?` to serial check-exhaustive's.
;; proc-result (one element of proc-pmap's output) -> 'verified | (ce...) |
;; (pcheck-incomplete proc-result). Anything but a clean (ok ...) is incomplete.
;; ── merge ───────────────────────────────────────────────────────────────────
;; parsed shards IN ORDER -> the SAME value serial check-exhaustive returns:
;; 'verified iff every shard verified,
;; else the shards' counterexamples concatenated in shard order.
;; An incomplete shard poisons the whole verdict (honest: we did not prove it).
;; ── the driver ──────────────────────────────────────────────────────────────
;; (pcheck-exhaustive prop-src domains n-shards [timeout [preamble]])
;; prop-src : a QUOTED lambda expression, e.g. '(lambda (x) (< x 100))
;; domains : list of finite domain lists, like check-exhaustive's 2nd arg
;; n-shards : how many child processes to split the FIRST domain across
;; timeout : per-child wall-clock seconds (default 30)
;; preamble : extra source the property needs in the child (default "")
;; Returns exactly what (check-exhaustive <prop> domains) returns.