git » blacktide.git » commit dfe76d5

diff --git a/README.md b/README.md
index b7d98b8..4db2cb0 100644
--- a/README.md
+++ b/README.md
@@ -61,10 +61,16 @@ clojure -T:build jar         # target/blacktide-0.1.0-SNAPSHOT.jar
 ```
 
 Select a JDK with `JAVA_CMD=/path/to/jdk/bin/java bin/check`. Development targets
-JDK 25/27; 17/21 are compatibility targets. Generators use deterministic seeds,
-independent models and shrinking; failures report their seed and source.
+JDK 25/27; 17/21 are compatibility targets. Generators use `test.check`, fixed
+seeds and independent models; failures report their seed and shrunk input.
+Shrinking preserves lexical scope and iteration bounds. Focused regressions
+remain ordinary `clojure.test` examples.
 Forgejo CI tests all four JDKs, checks pass types on 25/27, and builds the JAR.
 
+Pass test namespace names to `clojure -M:test` for a targeted run. At a test REPL,
+call a `defspec` function with a trial count and `:seed` to explore or reproduce
+another run, for example `(generated-nested-loops 1000 :seed 161803)`.
+
 See the [compiler architecture](doc/compiler.md) and [nanopass guide](doc/nanopass.md)
 for implementation contracts and extension guidance.
 
diff --git a/deps.edn b/deps.edn
index c18a050..bb54034 100644
--- a/deps.edn
+++ b/deps.edn
@@ -6,9 +6,11 @@
  {:build {:deps {io.github.clojure/tools.build {:mvn/version "0.10.14"}}
           :ns-default build}
   :test {:extra-paths ["test" "examples"]
+         :extra-deps {org.clojure/test.check {:mvn/version "1.1.3"}}
          :jvm-opts ["-Xmx768m"]
          :main-opts ["-m" "com.tailrecursion.test-runner"]}
   :check {:extra-paths ["test" "test-resources"]
-          :extra-deps {org.typedclojure/typed.clj.checker {:mvn/version "1.3.0"}}
+          :extra-deps {org.typedclojure/typed.clj.checker {:mvn/version "1.3.0"}
+                       org.clojure/test.check {:mvn/version "1.1.3"}}
           :jvm-opts ["-Xmx768m"]
           :main-opts ["-m" "com.tailrecursion.check-runner"]}}}
diff --git a/test/com/tailrecursion/blacktide/algorithms_test.clj b/test/com/tailrecursion/blacktide/algorithms_test.clj
index abdbb7f..75d450e 100644
--- a/test/com/tailrecursion/blacktide/algorithms_test.clj
+++ b/test/com/tailrecursion/blacktide/algorithms_test.clj
@@ -2,6 +2,9 @@
   "Partitioning and small parsers compared with independent collection/regex
   models. These programs are also used in the public examples."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole label goto setq]]
             [blacktide.algorithms :refer [tokens partition! decimal-prefix]]))
 
@@ -43,17 +46,17 @@
     (let [a (long-array xs)]
       (is (= (partition-reference xs) (when (seq xs) [(partition! a) (vec a)]))))))
 
-(deftest deterministic-parser-and-mutation-differentials
-  (let [seed 424242 rng (java.util.Random. seed)]
-    (dotimes [index 300]
-      (let [xs (vec (repeatedly (.nextInt rng 35) #(- (.nextInt rng 31) 15))) a (long-array xs)
-            number (str (nth ["" "-" "+"] (.nextInt rng 3))
-                        (apply str (repeatedly (.nextInt rng 25) #(char (+ (int \0) (.nextInt rng 10)))))
-                        (nth ["" "x" " 3"] (.nextInt rng 3)))
-            text (apply str (repeatedly (.nextInt rng 40) #(nth [\a \b \space \tab \newline \u2003 \u00a0] (.nextInt rng 7))))
-            states (vec (repeatedly (.nextInt rng 35) #(nth [:flip :hold :hold :bad] (.nextInt rng 4))))
-            context (str "seed=" seed " index=" index)]
-        (is (= (partition-reference xs) (when (seq xs) [(partition! a) (vec a)])) context)
-        (is (= (decimal-reference number) (decimal-prefix number)) context)
-        (is (= (token-reference text) (tokens text)) context)
-        (is (= (and (every? #{:flip :hold} states) (even? (count (filter #{:flip} states)))) (even-flips? states)) context)))))
+(defspec deterministic-parser-and-mutation-differentials {:num-tests 300 :seed 424242}
+  (prop/for-all [xs (gen/vector (gen/choose -15 15) 0 34)
+                 number (gen/let [sign (gen/elements ["" "-" "+"])
+                                   digits (gen/vector (gen/elements (vec "0123456789")) 0 24)
+                                   suffix (gen/elements ["" "x" " 3"])]
+                          (str sign (apply str digits) suffix))
+                 text (gen/fmap #(apply str %) (gen/vector (gen/elements [\a \b \space \tab \newline \u2003 \u00a0]) 0 39))
+                 states (gen/vector (gen/elements [:flip :hold :hold :bad]) 0 34)]
+    (let [a (long-array xs)]
+      (and (= (partition-reference xs) (when (seq xs) [(partition! a) (vec a)]))
+           (= (decimal-reference number) (decimal-prefix number))
+           (= (token-reference text) (tokens text))
+           (= (and (every? #{:flip :hold} states) (even? (count (filter #{:flip} states))))
+              (even-flips? states))))))
diff --git a/test/com/tailrecursion/blacktide/assignment_test.clj b/test/com/tailrecursion/blacktide/assignment_test.clj
index b40ee92..484b2ab 100644
--- a/test/com/tailrecursion/blacktide/assignment_test.clj
+++ b/test/com/tailrecursion/blacktide/assignment_test.clj
@@ -1,6 +1,8 @@
 (ns com.tailrecursion.blacktide.assignment-test
   "Assignment semantics, saved operands, and independent interpreter comparisons."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check :as tc]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :as lh :refer [loophole setq psetq]]
             [com.tailrecursion.blacktide.source-test :as source]
             [com.tailrecursion.nanopass.assignment-test :as oracle]))
@@ -83,21 +85,14 @@
       (catch Throwable e {:compiler-error (class e) :message (ex-message e)}))))
 
 (deftest generated-assignment-programs
-  ;; Reuse the library client's independently interpreted source semantics, not
-  ;; its lowering or output evaluator. Both the compiler and its IR are separate.
-  (doseq [seed [712381 314159]]
-    (let [random (java.util.Random. seed)]
-      (dotimes [trial 100]
-        (let [node (oracle/expression random 3)]
-          (doseq [[x y] [[0 0] [1 2] [-7 5] [10 -3]]]
-            (let [expected (oracle/execute node {'x x 'y y}) actual (execute node x y)]
-              (is (= expected actual)
-                  (when (not= expected actual)
-                    (pr-str {:seed seed :trial trial :input [x y]
-                             :source (oracle/minimize node
-                                       #(let [candidate (execute % x y)]
-                                          (and (= (boolean (:compiler-error actual)) (boolean (:compiler-error candidate)))
-                                               (not= (oracle/execute % {'x x 'y y}) candidate))))}))))))))))
+  ;; Reuse only the independent source interpreter, not its lowering algorithm.
+  (let [property (prop/for-all [node (oracle/expression 3)]
+                   (every? true?
+                     (for [[x y] [[0 0] [1 2] [-7 5] [10 -3]]]
+                       (= (oracle/execute node {'x x 'y y}) (execute node x y)))))]
+    (doseq [seed [712381 314159]]
+      (let [result (tc/quick-check 100 property :seed seed)]
+        (is (:pass? result) (pr-str result))))))
 
 (deftest invocation-arity-boundaries-preserve-operator-and-argument-snapshots
   (doseq [n [19 20 21 40]]
diff --git a/test/com/tailrecursion/blacktide/backend_test.clj b/test/com/tailrecursion/blacktide/backend_test.clj
index 66ed081..b24281b 100644
--- a/test/com/tailrecursion/blacktide/backend_test.clj
+++ b/test/com/tailrecursion/blacktide/backend_test.clj
@@ -1,6 +1,9 @@
 (ns com.tailrecursion.blacktide.backend-test
   "Backend decisions, primitive storage, reference identity and conversion order."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check :as tc]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.compiler.backend :as backend]
             [com.tailrecursion.blacktide.compiler.emit :as emit]
@@ -81,24 +84,26 @@
                   (mapcat #(tree-seq coll? seq %) @graphs)))))
 
 (deftest integer-conversion-overloads-are-not-interchangeable
-  (let [random (java.util.Random. 173205)
-        outcome (fn [f x] (try (let [v (f x)] [v (class v)])
-                              (catch Throwable e [(class e) (ex-message e)])))
+  (let [outcome (fn [f x] (try (let [v (f x)] [v (class v)])
+                             (catch Throwable e [(class e) (ex-message e)])))
         reference (fn [x] (int (identity x)))]
     (doseq [[cast values]
-            [['long (concat [Long/MIN_VALUE (dec (long Integer/MIN_VALUE)) Integer/MIN_VALUE
-                             -1 0 1 Integer/MAX_VALUE (inc (long Integer/MAX_VALUE)) Long/MAX_VALUE]
-                            (repeatedly 64 #(.nextLong random)))]
+            [['long [Long/MIN_VALUE (dec (long Integer/MIN_VALUE)) Integer/MIN_VALUE
+                      -1 0 1 Integer/MAX_VALUE (inc (long Integer/MAX_VALUE)) Long/MAX_VALUE]]
              ['double [Double/NaN Double/POSITIVE_INFINITY Double/NEGATIVE_INFINITY
                        -0.0 0.0 1.5 -1.5 2147483647.5 -2147483648.9
                        (double Long/MIN_VALUE) (double Long/MAX_VALUE)]]]
             mode [:default :dispatcher]
             :let [form (list 'fn '[input] (list 'loophole ['x (list cast 'input)] '(int x)))
-                  compiled ((compile-program form mode) (atom []))]
-            value values]
-      (let [value (if (= cast 'long) (long value) (double value))]
-        (is (= (outcome reference value) (outcome compiled value))
-            (pr-str [173205 cast mode value]))))))
+                  compiled ((compile-program form mode) (atom []))]]
+      (doseq [value values :let [value (if (= cast 'long) (long value) (double value))]]
+        (is (= (outcome reference value) (outcome compiled value)) (pr-str [cast mode value])))
+      (when (= cast 'long)
+        (let [result (tc/quick-check 64
+                       (prop/for-all [value gen/large-integer]
+                         (= (outcome reference value) (outcome compiled value)))
+                       :seed 173205)]
+          (is (:pass? result) (pr-str [mode result])))))))
 
 (deftest cached-long-origins-retain-value-class-and-identity
   ;; Compiler.NumberExpr initializes constants with Long.valueOf, including
diff --git a/test/com/tailrecursion/blacktide/case_test.clj b/test/com/tailrecursion/blacktide/case_test.clj
index bb77319..c8ee1da 100644
--- a/test/com/tailrecursion/blacktide/case_test.clj
+++ b/test/com/tailrecursion/blacktide/case_test.clj
@@ -2,6 +2,9 @@
   "Compare native case dispatch, then attack unique arms, lexical joins and
   pending evaluation. Constants are deliberately not interpreted with ordinary =."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [clojure.walk :as walk]
             [com.tailrecursion.blacktide :refer [loophole setq psetq label goto]]
             [com.tailrecursion.blacktide.jvm-test :as jvm]
@@ -199,27 +202,11 @@
   (try {:value (source/run-form (wrap (command-program config)))}
        (catch Throwable error {:error (class error) :message (ex-message error)})))
 
-(defn minimize-command [config wrap]
-  (let [failure (:error (command-outcome config wrap))]
-   (loop [config config]
-    (let [smaller (concat
-                    (for [index (range (count (:tokens config)))]
-                      (update config :tokens #(into (subvec % 0 index) (subvec % (inc index)))))
-                    (for [key [:a :b :weight :width] value (distinct [0 (quot (get config key) 2)])
-                          :when (not= value (get config key))] (assoc config key value)))]
-      (if-let [candidate (first (filter #(let [actual (command-outcome % wrap)]
-                                          (and (= failure (:error actual)) (not= {:value (command-model %)} actual))) smaller))]
-        (recur candidate) config)))))
-
-(deftest generated-case-loop-jump-programs
-  (let [seed 173205 random (java.util.Random. seed) alphabet [:swap \s :add "Aa" "BB" :stop :skip nil :other]]
-    (dotimes [index 120]
-      (let [config {:tokens (vec (repeatedly (.nextInt random 25) #(nth alphabet (.nextInt random (count alphabet)))))
-                    :a (- (.nextInt random 21) 10) :b (- (.nextInt random 21) 10)
-                    :weight (- (.nextInt random 7) 3) :width (.nextInt random 6)}
-            expected {:value (command-model config)}]
-        (doseq [wrap [identity #(list 'do (walk/postwalk-replace '{m left n right scan again finished done snapshot saved} %))]]
-          (let [actual (command-outcome config wrap)]
-            (is (= expected actual)
-                (pr-str {:seed seed :index index :config config :expected expected :actual actual
-                         :minimal (when-not (= expected actual) (command-program (minimize-command config wrap)))}))))))))
+(defspec generated-case-loop-jump-programs {:num-tests 120 :seed 173205}
+  (prop/for-all [config (gen/hash-map
+                         :tokens (gen/vector (gen/elements [:swap \s :add "Aa" "BB" :stop :skip nil :other]) 0 24)
+                         :a (gen/choose -10 10) :b (gen/choose -10 10)
+                         :weight (gen/choose -3 3) :width (gen/choose 0 5))]
+    (every? true?
+      (for [wrap [identity #(list 'do (walk/postwalk-replace '{m left n right scan again finished done snapshot saved} %))]]
+        (= {:value (command-model config)} (command-outcome config wrap))))))
diff --git a/test/com/tailrecursion/blacktide/collections_test.clj b/test/com/tailrecursion/blacktide/collections_test.clj
index 67b4392..ac55e22 100644
--- a/test/com/tailrecursion/blacktide/collections_test.clj
+++ b/test/com/tailrecursion/blacktide/collections_test.clj
@@ -1,6 +1,9 @@
 (ns com.tailrecursion.blacktide.collections-test
   "Compare native collection construction, metadata, errors and observable order."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole]]
             [com.tailrecursion.blacktide.compiler.backend :as backend]
             [com.tailrecursion.blacktide.compiler.emit :as emit]))
@@ -115,21 +118,19 @@
                 observation (fn [f] [(class (first (f))) (first (f))])]
             (is (= (observation plain) (observation compiled)) (pr-str [mode size value]))))))))
 
-(deftest deterministic-construction-differentials
-  (let [seed 314159 random (java.util.Random. seed)
-        value (fn [tag] (let [v (.nextInt random 8)]
-                          (case (.nextInt random 3)
-                            0 v
-                            1 (list 'record! 'events tag v)
-                            (list 'let ['x v] (list 'record! 'events tag 'x)))))]
-    (dotimes [trial 150]
-      (let [n (.nextInt random 13)
-            values (mapv #(value (keyword (str "item" %))) (range (* 2 n)))
-            body (case (.nextInt random 3)
-                   0 values
-                   1 (into {} (map vec (partition 2 values)))
-                   (set values))
-            body (if (.nextBoolean random) (with-meta body {:note '(record! events :metadata :ready)}) body)
-            wrap (fn [body] (list 'let ['out body] ['out '(meta out)]))]
-        (is (= (observe (wrap body)) (observe (wrap (list 'loophole [] body))))
-            (str "seed " seed ", trial " trial ": " (pr-str body)))))))
+(def collection-form
+  (gen/let [items (gen/vector (gen/tuple (gen/choose 0 7) (gen/elements [:literal :event :let])) 0 24)
+            kind (gen/elements [:vector :map :set]) metadata? gen/boolean]
+    (let [values (map-indexed (fn [i [v kind]]
+                               (let [tag (keyword (str "item" i))]
+                                 (case kind
+                                   :literal v
+                                   :event (list 'record! 'events tag v)
+                                   :let (list 'let ['x v] (list 'record! 'events tag 'x))))) items)
+          body (case kind :vector (vec values) :map (into {} (map vec (partition 2 values))) :set (set values))]
+      (if metadata? (with-meta body {:note '(record! events :metadata :ready)}) body))))
+
+(defspec deterministic-construction-differentials {:num-tests 150 :seed 314159}
+  (prop/for-all [body collection-form]
+    (let [wrap (fn [body] (list 'let ['out body] ['out '(meta out)]))]
+      (= (observe (wrap body)) (observe (wrap (list 'loophole [] body)))))))
diff --git a/test/com/tailrecursion/blacktide/control_test.clj b/test/com/tailrecursion/blacktide/control_test.clj
index c6d0829..7e48d70 100644
--- a/test/com/tailrecursion/blacktide/control_test.clj
+++ b/test/com/tailrecursion/blacktide/control_test.clj
@@ -1,6 +1,9 @@
 (ns com.tailrecursion.blacktide.control-test
   "Source control flow and live values across state-machine transitions."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole setq psetq]]
             [com.tailrecursion.blacktide.source-test :as source]
             [com.tailrecursion.blacktide.assignment-test :as assignment]
@@ -62,19 +65,12 @@
     (is (= (if (= 'if (first form)) :invalid-if :invalid-throw)
            (:kind (source/rejection (list 'loophole [] form)))))))
 
-(deftest generated-effectful-conditions
-  (let [seed 20261104 random (java.util.Random. seed)]
-    (dotimes [trial 100]
-      (let [test (case (.nextInt random 3)
-                   0 (oracle/batch :psetq 'x (oracle/read-var 'y) 'y (oracle/read-var 'x))
-                   1 (oracle/batch :setq 'x (oracle/lit 0))
-                   (oracle/read-var 'x))
-            node {:op :if :test (oracle/event :test test)
-                  :then (oracle/expression random 2) :else (oracle/expression random 2)}]
-        (doseq [[x y] [[0 0] [1 2] [-7 5] [10 -3]]]
-          (let [expected (oracle/execute node {'x x 'y y}) actual (assignment/execute node x y)]
-            (is (= expected actual)
-                (when (not= expected actual)
-                  (pr-str {:seed seed :trial trial :input [x y]
-                           :source (oracle/minimize node
-                                     #(not= (oracle/execute % {'x x 'y y}) (assignment/execute % x y)))})))))))))
+(defspec generated-effectful-conditions {:num-tests 100 :seed 20261104}
+  (prop/for-all [test (gen/elements [(oracle/batch :psetq 'x (oracle/read-var 'y) 'y (oracle/read-var 'x))
+                                    (oracle/batch :setq 'x (oracle/lit 0))
+                                    (oracle/read-var 'x)])
+                 then (oracle/expression 2) else (oracle/expression 2)]
+    (let [node {:op :if :test (oracle/event :test test) :then then :else else}]
+      (every? true?
+        (for [[x y] [[0 0] [1 2] [-7 5] [10 -3]]]
+          (= (oracle/execute node {'x x 'y y}) (assignment/execute node x y)))))))
diff --git a/test/com/tailrecursion/blacktide/generated_test.clj b/test/com/tailrecursion/blacktide/generated_test.clj
index b92ce7c..7327ae6 100644
--- a/test/com/tailrecursion/blacktide/generated_test.clj
+++ b/test/com/tailrecursion/blacktide/generated_test.clj
@@ -2,6 +2,9 @@
   "Bounded source generation with a separate state model, two backends, alpha
   variants and validity-preserving shrinking. Coverage includes fallback code."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check :as tc]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [clojure.walk :as walk]
             [com.tailrecursion.blacktide :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.backend-test :as backend]
@@ -89,21 +92,18 @@
   (try (backend/execution (program config control renamed?) mode)
        (catch Throwable error {:compile-error (class error) :message (ex-message error)})))
 
-(defn minimize [config control renamed? mode]
-  (loop [config config]
-    (let [smaller (concat
-                    (for [index (range (count (:steps config)))]
-                      (update config :steps #(vec (concat (subvec % 0 index) (subvec % (inc index))))))
-                    (for [key [:limit :cut :x :y] value (distinct [0 (quot (get config key) 2)])
-                          :when (not= value (get config key))] (assoc config key value))
-                    (for [index (range (count (:steps config)))
-                          :when (not (zero? (get-in config [:steps index 1])))]
-                      (assoc-in config [:steps index 1] 0)))]
-      (if-let [next (first (filter #(not= (model %) (outcome % control renamed? mode)) smaller))]
-        (recur next) config))))
+(def configuration
+  (gen/let [representation (gen/elements [:boxed :primitive :hinted :literal])
+            scalar? gen/boolean native-result? gen/boolean
+            limit (gen/choose 0 6) cut (gen/choose 0 8)
+            x (gen/choose -15 15) y (gen/choose -15 15)
+            steps (gen/vector (gen/tuple (gen/elements operations) (gen/choose -4 4)) 0 5)]
+    {:numeric? (not= :boxed representation) :hinted? (= :hinted representation)
+     :literal-init? (= :literal representation) :scalar? scalar? :native-result? native-result?
+     :limit limit :cut cut :x x :y y :steps steps}))
 
 (deftest generated-backend-equivalence
-  (let [seed 618033 random (java.util.Random. seed) coverage (atom {}) recover structure/recover
+  (let [seed 618033 coverage (atom {}) recover structure/recover
         choose storage/select-storage]
     (with-redefs [structure/recover (fn [analysis]
                                     (let [out (recover analysis)]
@@ -121,25 +121,18 @@
                                                          (tree-seq coll? seq (:body out)))
                                                (swap! coverage update :primitive-returns (fnil inc 0)))
                                              out))]
-      (dotimes [index 80]
-        (let [config {:numeric? (odd? index) :hinted? (= 1 (mod index 4)) :scalar? (zero? (mod index 3))
-                      :native-result? (zero? (mod index 5))
-                      :literal-init? (= 3 (mod index 4))
-                      :limit (.nextInt random 7) :cut (.nextInt random 9)
-                      :x (- (.nextInt random 31) 15) :y (- (.nextInt random 31) 15)
-                      :steps (vec (repeatedly (inc (.nextInt random 5))
-                                             #(vector (nth operations (.nextInt random (count operations)))
-                                                      (- (.nextInt random 9) 4))))}
-              expected (model config)]
-          (doseq [control [:linear :goto :recur :nested] renamed? [false true] mode [:default :dispatcher]]
-            (let [actual (outcome config control renamed? mode)]
-              (is (= expected actual)
-                  (when-not (= expected actual)
-                    (pr-str {:seed seed :index index :control control :mode mode :expected expected :actual actual
-                             :minimal (program (minimize config control renamed? mode) control renamed?)}))))))))
+      (let [result (tc/quick-check 80
+                     (prop/for-all [config configuration]
+                       (let [expected (model config)]
+                         (every? true?
+                           (for [control [:linear :goto :recur :nested]
+                                 renamed? [false true] mode [:default :dispatcher]]
+                             (= expected (outcome config control renamed? mode))))))
+                     :seed seed)]
+        (is (:pass? result) (pr-str result))))
     (is (pos? (get @coverage :structured 0)) (str @coverage))
     (is (pos? (get @coverage :acyclic 0)) (str @coverage))
     (is (pos? (get @coverage :cycles 0)) (str @coverage))
     (is (pos? (get @coverage :primitive-loops 0)) (str @coverage))
     (is (pos? (get @coverage :primitive-returns 0)) (str @coverage))
-    (println "Control generator: seed=" seed "source variants=640 executions=1280 coverage=" @coverage)))
+    (println "Control generator:" {:seed seed :coverage @coverage})))
diff --git a/test/com/tailrecursion/blacktide/graph_test.clj b/test/com/tailrecursion/blacktide/graph_test.clj
index afcaf56..f0d93b5 100644
--- a/test/com/tailrecursion/blacktide/graph_test.clj
+++ b/test/com/tailrecursion/blacktide/graph_test.clj
@@ -1,6 +1,9 @@
 (ns com.tailrecursion.blacktide.graph-test
   "Graph invariants and executable allocation, independent of source lowering."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide.compiler.graph :as graph]
             [com.tailrecursion.blacktide.machine-test :as m]))
 
@@ -97,13 +100,11 @@
                                     :branch (-> term (update :yes rename) (update :no rename))
                                     term)))])) (:blocks program))}))
 
-(deftest deterministic-backedges-and-metamorphisms
-  (let [seed 8675309 random (java.util.Random. seed)]
-    (dotimes [trial 75]
-      (let [initial (- (.nextInt random 200) 100) n (.nextInt random 30)
-            expected (+ initial (reduce + 0 (map #(if (odd? %) % (- %)) (range 1 (inc n)))))
-            program (counting-graph initial n)]
-        (doseq [variant [program (rename-blocks program)
-                         (assoc-in program [:blocks 99] (m/block [] (result (m/local 'uninitialized))))]]
-          (is (= expected (m/run-machine (graph/analyze variant)))
-              (str "seed " seed ", trial " trial ", input " [initial n])))))))
+(defspec deterministic-backedges-and-metamorphisms {:num-tests 75 :seed 8675309}
+  (prop/for-all [initial (gen/choose -100 99) n (gen/choose 0 29)]
+    (let [expected (+ initial (reduce + 0 (map #(if (odd? %) % (- %)) (range 1 (inc n)))))
+          program (counting-graph initial n)]
+      (every? true?
+        (for [variant [program (rename-blocks program)
+                       (assoc-in program [:blocks 99] (m/block [] (result (m/local 'uninitialized))))]]
+          (= expected (m/run-machine (graph/analyze variant))))))))
diff --git a/test/com/tailrecursion/blacktide/jumps_test.clj b/test/com/tailrecursion/blacktide/jumps_test.clj
index fedcb7d..c751675 100644
--- a/test/com/tailrecursion/blacktide/jumps_test.clj
+++ b/test/com/tailrecursion/blacktide/jumps_test.clj
@@ -1,6 +1,9 @@
 (ns com.tailrecursion.blacktide.jumps-test
   "Statement transfers, outer labels, scope reentry and bounded control graphs."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.source-test :as source]))
 
@@ -63,12 +66,12 @@
 (defn reference-fibonacci [n]
   (loop [n n a 0 b 1] (if (zero? n) a (recur (dec n) b (+' a b)))))
 
-(deftest bounded-algorithm-differentials
-  (let [seed 424242 random (java.util.Random. seed)]
-    (dotimes [trial 300]
-      (let [n (.nextInt random 50)]
-        (is (= (reduce +' 0 (range 1 (inc n))) (sum-through n)) (str "sum seed " seed ", trial " trial))
-        (is (= (reference-fibonacci n) (fibonacci n)) (str "fibonacci seed " seed ", trial " trial)))))
+(defspec bounded-algorithm-differentials {:num-tests 300 :seed 424242}
+  (prop/for-all [n (gen/choose 0 49)]
+    (and (= (reduce +' 0 (range 1 (inc n))) (sum-through n))
+         (= (reference-fibonacci n) (fibonacci n)))))
+
+(deftest large-sum
   (is (= 5000050000 (sum-through 100000))))
 
 (defn reference-machine [table budget value]
@@ -98,19 +101,11 @@
     (try (eval (machine-form table budget value labels wrapped?))
          (catch Throwable e {:compiler-error (ex-message e)}))))
 
-(deftest generated-bounded-control-graphs
-  (let [seed 8675309 random (java.util.Random. seed)]
-    (dotimes [trial 60]
-      (let [table (vec (repeatedly 3 #(hash-map :delta (- (.nextInt random 9) 4)
-                                              :yes (.nextInt random 3) :no (.nextInt random 3))))
-            budget (.nextInt random 14) value (- (.nextInt random 41) 20)
-            expected (reference-machine table budget value)]
-        (doseq [[labels wrapped?] [['[end b c] false] ['[renamed-a renamed-b renamed-c] true]]]
-          (let [actual (execute-machine table budget value labels wrapped?)]
-            (is (= expected actual)
-                (when (not= expected actual)
-                  ;; Shrink the execution budget while retaining a mismatch.
-                  (let [small (first (filter #(not= (reference-machine table % value)
-                                                    (execute-machine table % value labels wrapped?)) (range (inc budget))))]
-                    (pr-str {:seed seed :trial trial :table table :budget small :value value
-                             :program (machine-form table small value labels wrapped?)}))))))))))
+(defspec generated-bounded-control-graphs {:num-tests 60 :seed 8675309}
+  (prop/for-all [table (gen/vector (gen/hash-map :delta (gen/choose -4 4)
+                                                :yes (gen/choose 0 2) :no (gen/choose 0 2)) 3)
+                 budget (gen/choose 0 13) value (gen/choose -20 20)]
+    (let [expected (reference-machine table budget value)]
+      (every? true?
+        (for [[labels wrapped?] [['[end b c] false] ['[renamed-a renamed-b renamed-c] true]]]
+          (= expected (execute-machine table budget value labels wrapped?)))))))
diff --git a/test/com/tailrecursion/blacktide/jvm_test.clj b/test/com/tailrecursion/blacktide/jvm_test.clj
index 390faa3..dfa2bdc 100644
--- a/test/com/tailrecursion/blacktide/jvm_test.clj
+++ b/test/com/tailrecursion/blacktide/jvm_test.clj
@@ -2,7 +2,9 @@
   "Native Clojure is the dispatch oracle; event traces test receivers, pending
   operands and assignment effects that result-only comparisons cannot observe."
   (:require [clojure.test :refer [deftest is]]
-            [com.tailrecursion.blacktide.source-test :as source]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide.jvm-fixture]
             [com.tailrecursion.blacktide :refer [loophole setq psetq label goto]]))
 
@@ -103,40 +105,29 @@
     (binding [*unchecked-math* unchecked]
       (is (= (outcome form) (outcome (list 'loophole [] form))) (pr-str [unchecked form])))))
 
-(defn numeric-expression [^java.util.Random random depth locals]
-  (let [pick #(.nextInt random %) child #(numeric-expression random (dec depth) locals)]
-    (if (zero? depth)
-      (if (and (seq locals) (zero? (pick 2))) (nth locals (pick (count locals)))
-          (nth [-13 -1 0 1 7 2.5 1/2] (pick 7)))
-      (case (pick 8)
-        0 (list '+ (child) (child))
-        1 (list 'if (list 'neg? (child)) (child) (child))
-        2 (let [name (nth '[x y] (pick 2))]
-            (list 'let [name (child)] (numeric-expression random (dec depth) (conj locals name))))
-        3 (list '.length (list 'StringBuilder. (list 'str (child))))
-        4 (list 'Math/max (list 'double (child)) (list 'double (child)))
-        5 (list 'aget (list 'long-array [(child) (child)]) (list 'int 1))
-        6 (list 'alength (list 'char-array (list 'str (child))))
-        (list 'do (child) (child))))))
-
-(defn minimize-host [form]
-  (loop [form form]
-    (if-let [smaller (first (filter #(and (not= form %)
-                                         (contains? (outcome %) :value)
-                                         (not= (outcome %) (outcome (list 'loophole [] %))))
-                                   (source/smaller form)))]
-      (recur smaller) form)))
-
-(deftest generated-host-and-inline-expressions
-  (let [seed 112358 random (java.util.Random. seed)]
-    (dotimes [trial 180]
-      (let [form (numeric-expression random 3 []) expected (outcome form)]
-        (doseq [variant [form (list 'do form) (list 'let ['unused nil] form)]]
-          (let [actual (outcome (list 'loophole [] variant))]
-            (is (= expected actual)
-                (when (not= expected actual)
-                  (pr-str {:seed seed :trial trial :form (minimize-host variant)
-                           :expected expected :actual actual})))))))))
+(defn numeric-expression [depth locals]
+  (let [leaf (gen/elements (into [-13 -1 0 1 7 2.5 1/2] locals))]
+    (if (zero? depth) leaf
+      (let [child (numeric-expression (dec depth) locals)]
+        (gen/one-of
+          [leaf
+           (gen/let [a child b child] (list '+ a b))
+           (gen/let [test child a child b child] (list 'if (list 'neg? test) a b))
+           (gen/let [name (gen/elements '[x y]) init child
+                     body (numeric-expression (dec depth) (conj locals name))]
+             (list 'let [name init] body))
+           (gen/fmap #(list '.length (list 'StringBuilder. (list 'str %))) child)
+           (gen/let [a child b child] (list 'Math/max (list 'double a) (list 'double b)))
+           (gen/let [a child b child] (list 'aget (list 'long-array [a b]) (list 'int 1)))
+           (gen/fmap #(list 'alength (list 'char-array (list 'str %))) child)
+           (gen/let [a child b child] (list 'do a b))])))))
+
+(defspec generated-host-and-inline-expressions {:num-tests 180 :seed 112358}
+  (prop/for-all [form (numeric-expression 3 [])]
+    (let [expected (outcome form)]
+      (every? true?
+        (for [variant [form (list 'do form) (list 'let ['unused nil] form)]]
+          (= expected (outcome (list 'loophole [] variant))))))))
 
 (defn failure-trace [form]
   (binding [*ns* (the-ns 'com.tailrecursion.blacktide.jvm-test)]
diff --git a/test/com/tailrecursion/blacktide/loops_test.clj b/test/com/tailrecursion/blacktide/loops_test.clj
index 9c77a66..7291329 100644
--- a/test/com/tailrecursion/blacktide/loops_test.clj
+++ b/test/com/tailrecursion/blacktide/loops_test.clj
@@ -2,6 +2,9 @@
   "Original recur targets, native loop inference, and bounded independent loop
   models. Iteration budgets are structural, so shrinking cannot create hangs."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.source-test :as source]
             [com.tailrecursion.blacktide.jvm-test :as jvm]))
@@ -161,27 +164,13 @@
   (try {:value (source/run-form (wrap (loop-program config)))}
        (catch Throwable error {:error (class error) :message (ex-message error)})))
 
-(defn minimize-loop [config wrap]
-  (loop [config config]
-    (if-let [smaller (first (for [key [:limit :cut :width :a :b :weight]
-                                 value (distinct [0 (quot (get config key) 2)])
-                                 :when (not= value (get config key))
-                                 :let [candidate (assoc config key value)]
-                                 :when (not= {:value (loop-model candidate)} (loop-outcome candidate wrap))]
-                             candidate))]
-      (recur smaller) config)))
-
-(deftest generated-nested-loops
-  (let [seed 161803 random (java.util.Random. seed)]
-    (dotimes [index 240]
-      (let [config {:limit (.nextInt random 12) :cut (.nextInt random 15) :width (.nextInt random 6)
-                    :a (- (.nextInt random 21) 10) :b (- (.nextInt random 21) 10) :weight (- (.nextInt random 7) 3)}
-            expected {:value (loop-model config)}]
-        (doseq [wrap [identity #(list 'let ['unused 1] (list 'do %))]]
-          (let [actual (loop-outcome config wrap)]
-            (is (= expected actual)
-                (pr-str {:seed seed :index index :config config :expected expected :actual actual
-                         :minimal (when-not (= expected actual) (loop-program (minimize-loop config wrap)))}))))))))
+(defspec generated-nested-loops {:num-tests 240 :seed 161803}
+  (prop/for-all [config (gen/hash-map :limit (gen/choose 0 11) :cut (gen/choose 0 14)
+                                    :width (gen/choose 0 5) :a (gen/choose -10 10)
+                                    :b (gen/choose -10 10) :weight (gen/choose -3 3))]
+    (every? true?
+      (for [wrap [identity #(list 'let ['unused 1] (list 'do %))]]
+        (= {:value (loop-model config)} (loop-outcome config wrap))))))
 
 (defn insertion-sort! [^longs values]
   (loophole [writes 0]
@@ -209,12 +198,11 @@
     (loop [a (abs a) b (abs b)]
       (if (zero? b) a (do (setq steps (inc steps)) (recur b (rem a b)))))))
 
-(deftest algorithms-against-independent-references
-  (let [seed 577215 random (java.util.Random. seed)]
-    (dotimes [index 180]
-      (let [input (vec (repeatedly (.nextInt random 25) #(- (.nextInt random 15) 7)))
-            values (long-array input) a (- (.nextInt random 1001) 500) b (- (.nextInt random 1001) 500)]
-        (insertion-sort! values)
-        (is (= (vec (sort input)) (vec values)) (pr-str {:seed seed :index index :input input}))
-        (is (= (or (first (keep-indexed #(when (neg? %2) %1) input)) -1) (first-negative (long-array input))))
-        (is (= (.longValue (.gcd (biginteger a) (biginteger b))) (gcd a b)))))))
+(defspec algorithms-against-independent-references {:num-tests 180 :seed 577215}
+  (prop/for-all [input (gen/vector (gen/choose -7 7) 0 24)
+                 a (gen/choose -500 500) b (gen/choose -500 500)]
+    (let [values (long-array input)]
+      (insertion-sort! values)
+      (and (= (vec (sort input)) (vec values))
+           (= (or (first (keep-indexed #(when (neg? %2) %1) input)) -1) (first-negative (long-array input)))
+           (= (.longValue (.gcd (biginteger a) (biginteger b))) (gcd a b))))))
diff --git a/test/com/tailrecursion/blacktide/native_sites_test.clj b/test/com/tailrecursion/blacktide/native_sites_test.clj
index 8b98233..94d2526 100644
--- a/test/com/tailrecursion/blacktide/native_sites_test.clj
+++ b/test/com/tailrecursion/blacktide/native_sites_test.clj
@@ -2,6 +2,9 @@
   "Control recovery retains Java function construction and cached lookup sites.
   Generated loops preserve bound references without promising literal pooling."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide.backend-test :as backend]
             [com.tailrecursion.blacktide :refer [loophole setq label goto]]
             [com.tailrecursion.blacktide.invocation-test]
@@ -70,32 +73,29 @@
       (is (every? true? (map (fn [flag input] (identical? input (f flag input))) flags inputs))
           (pr-str [real-backedge? context mode])))))
 
-(defn selection-tree [^java.util.Random random depth path]
+(defn selection-tree [depth path]
   (if (zero? depth)
-    (list 'do (list 'swap! 'events 'conj [:leaf path])
-          (list 'quote (nth [nil false 1000 1.5 :selected "text"] (.nextInt random 6))))
-    (let [test (list 'do (list 'swap! 'events 'conj [:test path])
-                     (list 'mod (list '+ 'input (.nextInt random 5)) 3))
-          arm (fn [index] (selection-tree random (dec depth) (conj path index)))]
-      (if (.nextBoolean random)
-        (list 'if (list 'zero? test) (arm 0) (arm 1))
-        (list 'let ['choice test]
-              (list 'case 'choice 0 (arm 0) 1 (arm 1) (arm 2)))))))
+    (gen/fmap #(list 'do (list 'swap! 'events 'conj [:leaf path]) (list 'quote %))
+              (gen/elements [nil false 1000 1.5 :selected "text"]))
+    (let [test (gen/fmap #(list 'do (list 'swap! 'events 'conj [:test path])
+                              (list 'mod (list '+ 'input %) 3)) (gen/choose 0 4))
+          arm #(selection-tree (dec depth) (conj path %))]
+      (gen/one-of
+        [(gen/let [test test a (arm 0) b (arm 1)] (list 'if (list 'zero? test) a b))
+         (gen/let [test test a (arm 0) b (arm 1) c (arm 2)]
+           (list 'let ['choice test] (list 'case 'choice 0 a 1 b c)))]))))
 
-(deftest nested-joins-preserve-one-continuation
+(defspec nested-joins-preserve-one-continuation {:num-tests 32 :seed 331662}
   ;; Java method values after a join retain one class construction site.
-  (let [seed 331662 random (java.util.Random. seed)]
-    (doseq [trial (range 32)]
-      (let [tree (selection-tree random (+ 1 (.nextInt random 3)) [])
-            body (list 'let ['picked tree] '(swap! events conj :joined) '[picked String/.length])
-            form (list 'loophole [] body)
-            source (fn [body] (list 'fn '[input] body))
-            observe (fn [body mode]
-                      (let [events (atom []) f ((backend/compile-program (source body) mode) events)
-                            values (mapv f (range 6))]
-                        [(mapv (fn [[picked f]] [picked (f "abc")]) values)
-                         (identity-pattern (mapv (comp class second) values)) @events]))
-            expected (observe body :default)]
-        (is (= :structured (:op (backend/selection (source form)))) (pr-str [seed trial tree]))
-        (doseq [mode [:default :dispatcher]]
-          (is (= expected (observe form mode)) (pr-str [seed trial mode tree])))))))
+  (prop/for-all [tree (gen/bind (gen/choose 1 3) #(selection-tree % []))]
+    (let [body (list 'let ['picked tree] '(swap! events conj :joined) '[picked String/.length])
+          form (list 'loophole [] body)
+          source (fn [body] (list 'fn '[input] body))
+          observe (fn [body mode]
+                    (let [events (atom []) f ((backend/compile-program (source body) mode) events)
+                          values (mapv f (range 6))]
+                      [(mapv (fn [[picked f]] [picked (f "abc")]) values)
+                       (identity-pattern (mapv (comp class second) values)) @events]))
+          expected (observe body :default)]
+      (and (= :structured (:op (backend/selection (source form))))
+           (every? #(= expected (observe form %)) [:default :dispatcher])))))
diff --git a/test/com/tailrecursion/blacktide/source_loops_test.clj b/test/com/tailrecursion/blacktide/source_loops_test.clj
index d7e20a3..4a88103 100644
--- a/test/com/tailrecursion/blacktide/source_loops_test.clj
+++ b/test/com/tailrecursion/blacktide/source_loops_test.clj
@@ -1,12 +1,16 @@
 (ns com.tailrecursion.blacktide.source-loops-test
   "Compare ordinary numeric loops with both backends, including source boxing,
   recur inference, evaluation traces and bounded generated alpha variants."
-  (:require [com.tailrecursion.blacktide :refer [loophole]]
+  (:require [clojure.test :as t]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
+            [clojure.walk :as walk]
+            [com.tailrecursion.blacktide :refer [loophole]]
             [com.tailrecursion.blacktide.compiler.backend :as backend]
             [com.tailrecursion.blacktide.compiler.emit :as emit]
-            [com.tailrecursion.blacktide.jvm-test :as jvm]
-            [clojure.walk :as walk]
-            [clojure.test :as t]))
+            [com.tailrecursion.blacktide.jvm-test :as jvm]))
+
 (defn root-error [e] (if-let [cause (ex-cause e)] (recur cause) e))
 (defn canonical [value]
   (cond
@@ -198,44 +202,21 @@
                                                            step when bias amount snapshot saved} % %) (meta %)) %) body))
       body)))
 
-(defn config-outcome [config renamed? mode n]
-  (let [form (generated-body config renamed?)]
-    (outcome (compile-body form mode) (:input config) n)))
-
-(defn minimize [config renamed? mode n]
-  (loop [config config]
-    (let [candidates (concat
-                       (for [index (range (count (:steps config)))]
-                         (update config :steps #(into (subvec % 0 index) (subvec % (inc index)))))
-                       (for [key [:typed? :narrow? :alias? :shadow? :scalar? :forward? :literal?]
-                             :when (get config key)] (assoc config key false))
-                       (when (not= 0 (:input config)) [(assoc config :input 0)])
-                       (when (not= 0 (:k config)) [(assoc config :k 0)]))]
-      (if-let [smaller (first (filter #(not= (config-outcome % false :ordinary n)
-                                            (config-outcome % renamed? mode n)) candidates))]
-        (recur smaller) config))))
+(def configuration
+  (gen/let [double? gen/boolean typed? gen/boolean narrow? gen/boolean
+            alias? gen/boolean shadow? gen/boolean scalar? gen/boolean
+            forward? gen/boolean literal? gen/boolean k (gen/choose -3 3)
+            input (gen/elements (if double? [-0.0 1.5 Double/NaN Double/POSITIVE_INFINITY Double/MIN_VALUE]
+                                    [0 1000 Long/MIN_VALUE Long/MAX_VALUE 2M 1/3 nil]))
+            steps (gen/vector (gen/tuple (gen/elements [:add :increment :negate :scale :branch :flip])
+                                        (gen/choose -3 3)) 0 4)]
+    {:double? double? :typed? typed? :narrow? narrow? :alias? alias? :shadow? shadow?
+     :scalar? scalar? :forward? forward? :literal? literal? :k k :input input :steps steps}))
 
-(t/deftest generated-source-loop-equivalence
-  (let [seed 141421 random (java.util.Random. seed)
-        choose #(nth % (.nextInt random (count %)))]
-    (dotimes [index 128]
-      (let [double? (odd? index)
-            config {:double? double? :typed? (.nextBoolean random) :narrow? (.nextBoolean random)
-                    :alias? (.nextBoolean random) :shadow? (.nextBoolean random)
-                    :scalar? (.nextBoolean random) :forward? (.nextBoolean random)
-                    :literal? (.nextBoolean random) :k (- (.nextInt random 7) 3)
-                    :input (choose (if double? [-0.0 1.5 Double/NaN Double/POSITIVE_INFINITY Double/MIN_VALUE]
-                                             [0 1000 Long/MIN_VALUE Long/MAX_VALUE 2M 1/3 nil]))
-                    :steps (vec (repeatedly (inc (.nextInt random 4))
-                                           #(vector (choose [:add :increment :negate :scale :branch :flip])
-                                                    (- (.nextInt random 7) 3))))}
-            reference (compile-body (generated-body config false) :ordinary)]
-        (doseq [renamed? [false true] mode [:default :dispatcher]
-                :let [compiled (compile-body (generated-body config renamed?) mode)] n [0 1 4]]
-          (let [expected (outcome reference (:input config) n) actual (outcome compiled (:input config) n)]
-            (t/is (= expected actual)
-                  (when (not= expected actual)
-                    (let [small (minimize config renamed? mode n)]
-                      (pr-str {:seed seed :index index :mode mode :renamed? renamed? :n n
-                               :input (:input small) :form (generated-body small renamed?)}))))))))
-    (println "Source loop generator:" {:seed seed :configs 128 :comparisons 1536})))
+(defspec generated-source-loop-equivalence {:num-tests 128 :seed 141421}
+  (prop/for-all [config configuration]
+    (let [reference (compile-body (generated-body config false) :ordinary)]
+      (every? true?
+        (for [renamed? [false true] mode [:default :dispatcher]
+              :let [compiled (compile-body (generated-body config renamed?) mode)] n [0 1 4]]
+          (= (outcome reference (:input config) n) (outcome compiled (:input config) n)))))))
diff --git a/test/com/tailrecursion/blacktide/source_test.clj b/test/com/tailrecursion/blacktide/source_test.clj
index 5869e03..8dd4ab5 100644
--- a/test/com/tailrecursion/blacktide/source_test.clj
+++ b/test/com/tailrecursion/blacktide/source_test.clj
@@ -2,6 +2,9 @@
   "Source binding and expansion compared with ordinary Clojure, including
   generated lexical programs."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.blacktide :as lh :refer [loophole label goto setq psetq]]
             [com.tailrecursion.blacktide.source-fixture :as fixture]))
 
@@ -116,55 +119,26 @@
     (is (= {:file "example.clj" :line 31 :column 9 :form bad :kind :invalid-quote}
            data))))
 
-(defn expression [^java.util.Random random depth locals]
-  (let [pick #(.nextInt random %)]
-    (if (zero? depth)
-      (if (and (seq locals) (zero? (pick 2))) (nth locals (pick (count locals))) (- (pick 31) 15))
-      (case (pick 5)
-        0 (list 'sum (expression random (dec depth) locals) (expression random (dec depth) locals))
-        1 (let [name (nth '[x y z] (pick 3))]
-            (list 'let [name (expression random (dec depth) locals)]
-                  (expression random (dec depth) (conj locals name))))
-        2 (list 'do (expression random (dec depth) locals) (expression random (dec depth) locals))
-        3 (list 'identity (expression random (dec depth) locals))
-        (expression random 0 locals)))))
+(defn expression [depth locals]
+  (let [leaf (gen/one-of [(gen/choose -15 15) (gen/elements locals)])]
+    (if (zero? depth) leaf
+      (let [child (expression (dec depth) locals)]
+        (gen/one-of
+          [leaf
+           (gen/let [a child b child] (list 'sum a b))
+           ;; Regenerate the body in the new scope when the name shrinks.
+           (gen/let [name (gen/elements '[x y z]) init child
+                     body (expression (dec depth) (conj locals name))]
+             (list 'let [name init] body))
+           (gen/let [a child b child] (list 'do a b))
+           (gen/fmap #(list 'identity %) child)])))))
 
-(defn smaller [form]
-  (when (seq? form)
-    (let [[op & args] form]
-      (concat [0]
-              (if (= op 'let)
-                [(last args) (list 'let [(first (first args)) 0] (last args))]
-                args)
-              (for [i (range (count args)) child (smaller (nth args i))]
-                (list* op (assoc (vec args) i child)))))))
-
-(defn difference [body]
-  ;; Invalid shrinks are discarded by the independent Clojure oracle.
-  (try
+(defspec deterministic-lexical-programs {:num-tests 150 :seed 20261103}
+  (prop/for-all [body (expression 3 '[x])]
     (let [expected (run-form (list 'let '[x 7] body))]
-      (try (let [actual (run-form (list 'loophole '[x 7] body))]
-             (when-not (= expected actual) :value))
-           (catch Throwable _ :compilation-or-execution)))
-    (catch Throwable _ nil)))
-
-(defn minimize [body kind]
-  (loop [body body]
-    (if-let [small (first (filter #(and (not= body %) (= kind (difference %))) (smaller body)))]
-      (recur small) body)))
-
-(deftest deterministic-lexical-programs
-  (let [seed 20261103 random (java.util.Random. seed)]
-    (dotimes [trial 150]
-      (let [body (expression random 3 '[x])
-            expected (run-form (list 'let '[x 7] body))]
-        (doseq [variant [body (list 'do body) (list 'let ['unused 99] body)]]
-          (let [actual (try [:value (run-form (list 'loophole '[x 7] variant))]
-                            (catch Throwable e [:error (ex-message e)]))]
-            (is (= [:value expected] actual)
-                (when (not= [:value expected] actual)
-                  (str "seed " seed ", trial " trial ": "
-                       (pr-str (if-let [kind (difference variant)] (minimize variant kind) variant)))))))))))
+      (every? true?
+        (for [variant [body (list 'do body) (list 'let ['unused 99] body)]]
+          (= expected (run-form (list 'loophole '[x 7] variant))))))))
 
 (deftest diagnostic-context-survives-expansion-and-native-boundaries
   (doseq [body '[(case)]
diff --git a/test/com/tailrecursion/nanopass/assignment_test.clj b/test/com/tailrecursion/nanopass/assignment_test.clj
index e7d4ab1..e33d91f 100644
--- a/test/com/tailrecursion/nanopass/assignment_test.clj
+++ b/test/com/tailrecursion/nanopass/assignment_test.clj
@@ -2,6 +2,9 @@
   "Execute both grammars against explicit traces and deterministic generated inputs.
   The interpreter is test instrumentation; the compiler pass only constructs data."
   (:require [clojure.test :refer [deftest is testing]]
+            [clojure.test.check :as tc]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.nanopass.clients.assignment :as lower]))
 
 (defn lit [value] {:op :const :value value})
@@ -105,65 +108,29 @@
         (is (= expected (execute source {'x 1 'y 2})))
         (is (= expected (execute (lower/lower source) {'x 1 'y 2})))))))
 
-(defn expression [^java.util.Random rng depth]
-  (let [pick #(.nextInt rng %)
-        child #(expression rng (dec depth))
-        writes #(vec (repeatedly (pick 4) (fn [] [(nth '[x y] (pick 2)) (child)])))]
-    (if (zero? depth)
-      (if (zero? (pick 2)) (lit (- (pick 11) 5)) (read-var (nth '[x y] (pick 2))))
-      (case (pick 7)
-        0 (child)
-        1 {:op :add :left (child) :right (child)}
-        2 (sequence-of (child) (child))
-        3 {:op :if :test (lit (zero? (pick 2))) :then (child) :else (child)}
-        4 (event (nth [:a :b :c] (pick 3)) (child))
-        5 (sequence-of {:op :setq :writes (writes)} (read-var 'x))
-        6 (sequence-of {:op :psetq :writes (writes)} (read-var 'y))))))
-
-(defn child-paths [node]
-  (case (:op node)
-    :add [[:left] [:right]]
-    :if [[:test] [:then] [:else]]
-    :event [[:value]]
-    :do (mapv #(vector :forms %) (range (count (:forms node))))
-    (:setq :psetq) (mapv #(vector :writes % 1) (range (count (:writes node))))
-    []))
-
-(defn paths [node]
-  (cons [] (mapcat (fn [path] (map #(into path %) (paths (get-in node path)))) (child-paths node))))
-
-(defn minimize [source fails?]
-  (loop [source source]
-    (if-let [smaller (some (fn [path]
-                            (let [candidate (if (seq path) (assoc-in source path (lit 0)) (lit 0))]
-                              (when (and (not= candidate source) (fails? candidate)) candidate)))
-                          (paths source))]
-      (recur smaller) source)))
+(defn expression [depth]
+  (let [leaf (gen/one-of [(gen/fmap lit (gen/choose -5 5))
+                          (gen/fmap read-var (gen/elements '[x y]))])]
+    (if (zero? depth) leaf
+      (let [child (expression (dec depth))
+            writes (gen/vector (gen/tuple (gen/elements '[x y]) child) 0 3)]
+        (gen/one-of
+          [leaf
+           (gen/let [a child b child] {:op :add :left a :right b})
+           (gen/let [a child b child] (sequence-of a b))
+           (gen/let [test gen/boolean then child else child]
+             {:op :if :test (lit test) :then then :else else})
+           (gen/let [tag (gen/elements [:a :b :c]) value child] (event tag value))
+           (gen/let [writes writes] (sequence-of {:op :setq :writes writes} (read-var 'x)))
+           (gen/let [writes writes] (sequence-of {:op :psetq :writes writes} (read-var 'y)))])))))
 
 (deftest generated-assignment-combinations
-  (doseq [seed [712381 314159]]
-    (let [rng (java.util.Random. seed)]
-      (dotimes [index 200]
-        (let [source (expression rng 4) lowered (lower/lower source)]
-          (doseq [[x y] [[0 0] [1 2] [-7 5] [10 -3]]]
-            (let [vars {'x x 'y y}
-                  expected (execute source vars)
-                  actual (execute lowered vars)
-                  fails? (fn [program]
-                           (let [expected (execute program vars)
-                                 actual (execute (lower/lower program) vars)]
-                             (and (= :return (:status expected) (:status actual)) (not= expected actual))))]
-              (is (= expected actual)
-                  (pr-str {:seed seed :index index :input [x y]
-                           :source (if (= expected actual) source (minimize source fails?))})))))))))
-
-(deftest shrinking-preserves-semantic-failure
-  (let [source (batch :psetq 'x (sequence-of (lit 8) (read-var 'y)) 'y (read-var 'x))
-        fails? (fn [node]
-                 (when (= :psetq (:op node))
-                   (not= (execute node {'x 1 'y 2})
-                         (execute (lower/lower (sequence-of (assoc node :op :setq) (lit nil))) {'x 1 'y 2}))))
-        smaller (minimize source fails?)]
-    (is (fails? smaller))
-    (is (< (count (paths smaller)) (count (paths source))))
-    (is (= [[]] (vec (paths (lit {:op :setq :writes :opaque})))))))
+  (let [property (prop/for-all [source (expression 4)]
+                   (let [lowered (lower/lower source)]
+                     (every? true?
+                       (for [[x y] [[0 0] [1 2] [-7 5] [10 -3]]
+                             :let [vars {'x x 'y y}]]
+                         (= (execute source vars) (execute lowered vars))))))]
+    (doseq [seed [712381 314159]]
+      (let [result (tc/quick-check 200 property :seed seed)]
+        (is (:pass? result) (pr-str result))))))
diff --git a/test/com/tailrecursion/nanopass/flow_test.clj b/test/com/tailrecursion/nanopass/flow_test.clj
index dc44246..d5ca22a 100644
--- a/test/com/tailrecursion/nanopass/flow_test.clj
+++ b/test/com/tailrecursion/nanopass/flow_test.clj
@@ -2,6 +2,9 @@
   "Execute a client's graphs against independent arithmetic and scope results.
   This bounded VM is test instrumentation, not a library or Loophole backend."
   (:require [clojure.test :refer [deftest is]]
+            [clojure.test.check.clojure-test :refer [defspec]]
+            [clojure.test.check.generators :as gen]
+            [clojure.test.check.properties :as prop]
             [com.tailrecursion.nanopass.clients.flow :as flow]))
 
 (defn number-node [n] {:op :int :value n :note '{:op :read :name opaque}})
@@ -87,15 +90,13 @@
                (set-node 'n (plus (read-node 'n) (number-node -1))))}
        (read-node 'a)))))
 
-(deftest generated-scope-and-control-combinations
-  (let [seed 271828 rng (java.util.Random. seed)]
-    (dotimes [index 250]
-      (let [n (.nextInt rng 13) initial (- (.nextInt rng 11) 5)
-            pivot (.nextInt rng 16) bias (- (.nextInt rng 7) 3) offset (- (.nextInt rng 7) 3)
-            source (inconvenient-program n initial pivot bias offset)
-            expected (loop [i n result initial]
-                       (if (zero? i) result
-                           (recur (dec i) (if (= i pivot) (+ result result bias) (+ result i offset)))))]
-        (doseq [variant [source (forms source) (let-node 'unused (number-node 999) source)]]
-          (is (= expected (execute (flow/compile-program variant)))
-              (pr-str {:seed seed :index index :input [n initial pivot bias offset]})))))))
+(defspec generated-scope-and-control-combinations {:num-tests 250 :seed 271828}
+  (prop/for-all [n (gen/choose 0 12) initial (gen/choose -5 5)
+                 pivot (gen/choose 0 15) bias (gen/choose -3 3) offset (gen/choose -3 3)]
+    (let [source (inconvenient-program n initial pivot bias offset)
+          expected (loop [i n result initial]
+                     (if (zero? i) result
+                       (recur (dec i) (if (= i pivot) (+ result result bias) (+ result i offset)))))]
+      (every? true?
+        (for [variant [source (forms source) (let-node 'unused (number-node 999) source)]]
+          (= expected (execute (flow/compile-program variant))))))))