From 461b20dd590f7f0587a0686d5e54634a948742d0 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 10:50:19 -0400
Subject: [PATCH 01/10] Key the law evaluator's cache by the printed term

'(a b) and '[a b] are = in Clojure, so a law quoting a list ran the fn
compiled for an earlier law quoting the same elements as a vector, and
failed or passed depending on which law came first.
---
 src/writ/spec.clj       | 3 ++-
 test/writ/spec_test.clj | 9 +++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/writ/spec.clj b/src/writ/spec.clj
index df71ce7..7d5e6e7 100644
--- a/src/writ/spec.clj
+++ b/src/writ/spec.clj
@@ -683,9 +683,10 @@
   "Compile and cache term fns: (ev vars term env) runs `term` with the
   variables bound from env."
   [spec-ns]
+  ;; keyed by the printed term: '(a b) and '[a b] are =, but not the same term
   (let [cache (atom {})]
     (fn [vars term env]
-      (let [k [vars term]
+      (let [k (pr-str [vars term])
             f (or (get @cache k)
                   (let [f (binding [*ns* (the-ns spec-ns)]
                             (eval (list 'fn (vec vars) term)))]
diff --git a/test/writ/spec_test.clj b/test/writ/spec_test.clj
index 9480ca7..b8ab82f 100644
--- a/test/writ/spec_test.clj
+++ b/test/writ/spec_test.clj
@@ -601,3 +601,12 @@
   (let [r (spec/check 'writ.spec-demo.flow-spec {:seed 42})]
     (is (= '[insert] (:off-graph r)))
     (is (str/includes? (:message r) "not a step of any graph or machine: insert"))))
+
+(deftest a-quoted-list-and-vector-are-different-terms
+  ;; '(a b) and '[a b] are = in Clojure, so a cache keyed on the term alone
+  ;; ran a law about the list with the fn compiled for the vector
+  (let [ev (@#'spec/evaluator 'writ.spec-test)]
+    (is (true? (ev [] '(vector? (quote [a b])) {})))
+    (is (false? (ev [] '(vector? (quote (a b))) {})))
+    (is (= {:k [1]} (ev [] '(quote {:k [1]}) {})))
+    (is (list? (:k (ev [] '(quote {:k (1)}) {}))))))

From 279b34724270436900d4da33defddec445b40f37 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 12:19:16 -0400
Subject: [PATCH 02/10] Run each example as its own CI job, with timeouts

The examples ran one after another in a single job, 30-40 minutes, and a
hang sat until the 6 hour limit. The runner now takes the namespaces to
run, and rejects names it doesn't know so a typo can't pass.
---
 .github/workflows/ci.yml          | 22 ++++++++++++++++++++--
 examples/test/examples_runner.clj | 11 ++++++++---
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 932c263..8354e1b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -5,6 +5,7 @@ on: push
 jobs:
   test:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@v4
       - name: Install jolt
@@ -15,5 +16,22 @@ jobs:
           echo "$HOME/.local/bin" >> "$GITHUB_PATH"
       - name: writ tests
         run: jolt -M:test
-      - name: examples tests
-        run: cd examples && jolt -M:test
+
+  # one job per example, so they run side by side
+  examples:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    strategy:
+      fail-fast: false
+      matrix:
+        example: [fetch, life, pong, screens, shortener]
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install jolt
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y liblz4-1 zlib1g libtinfo6
+          curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+      - name: ${{ matrix.example }}
+        run: cd examples && jolt -M:test ${{ matrix.example }}.core-test
diff --git a/examples/test/examples_runner.clj b/examples/test/examples_runner.clj
index c279ef5..952ea4e 100644
--- a/examples/test/examples_runner.clj
+++ b/examples/test/examples_runner.clj
@@ -1,5 +1,6 @@
 (ns examples-runner
-  "`jolt -M:test` runs every example's checks and exits non-zero on a failure."
+  "`jolt -M:test` runs every example's checks and exits non-zero on a failure.
+  `jolt -M:test pong.core-test` runs only the namespaces named."
   (:require [clojure.test :as t]
             fetch.core-test
             life.core-test
@@ -10,6 +11,10 @@
 (def test-namespaces
   '[pong.core-test life.core-test screens.core-test shortener.core-test fetch.core-test])
 
-(defn -main [& _]
-  (let [{:keys [fail error]} (apply t/run-tests test-namespaces)]
+(defn -main [& args]
+  (let [nses (if (seq args) (map symbol args) test-namespaces)
+        _ (when-let [bad (seq (remove (set test-namespaces) nses))]
+            (println "not an example test namespace:" (vec bad))
+            (System/exit 1))
+        {:keys [fail error]} (apply t/run-tests nses)]
     (System/exit (if (zero? (+ (or fail 0) (or error 0))) 0 1))))

From 28756e57cbb778d8bda687f79dad3a6de7f6e1f2 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 12:20:43 -0400
Subject: [PATCH 03/10] CI: pin jolt, so parallel installs don't hit the API
 rate limit

---
 .github/workflows/ci.yml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8354e1b..2593c5d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -2,6 +2,11 @@ name: ci
 
 on: push
 
+# pinned: "latest" is looked up on the GitHub API, which rate-limits the
+# parallel jobs, and a new release would change what CI runs on
+env:
+  JOLT_VERSION: v0.8.12
+
 jobs:
   test:
     runs-on: ubuntu-latest
@@ -12,7 +17,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install -y liblz4-1 zlib1g libtinfo6
-          curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash
+          curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash -s -- --version "$JOLT_VERSION"
           echo "$HOME/.local/bin" >> "$GITHUB_PATH"
       - name: writ tests
         run: jolt -M:test
@@ -31,7 +36,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install -y liblz4-1 zlib1g libtinfo6
-          curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash
+          curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash -s -- --version "$JOLT_VERSION"
           echo "$HOME/.local/bin" >> "$GITHUB_PATH"
       - name: ${{ matrix.example }}
         run: cd examples && jolt -M:test ${{ matrix.example }}.core-test

From 81f1aa77d1c4acacf7afe5985ae7c23034f1460f Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 13:22:35 -0400
Subject: [PATCH 04/10] Examples runner: print each test as it starts and ends

A CI job ran for an hour with no output, so a slow check and a hang
looked the same. Give pong, which proves every edge of its graph, a
longer timeout.
---
 .github/workflows/ci.yml          |  4 +++-
 examples/test/examples_runner.clj | 10 ++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2593c5d..9c9b1af 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,7 +25,9 @@ jobs:
   # one job per example, so they run side by side
   examples:
     runs-on: ubuntu-latest
-    timeout-minutes: 60
+    # pong's checks prove every edge of its graph from the code, the slowest
+    # thing the suite does
+    timeout-minutes: ${{ matrix.example == 'pong' && 180 || 60 }}
     strategy:
       fail-fast: false
       matrix:
diff --git a/examples/test/examples_runner.clj b/examples/test/examples_runner.clj
index 952ea4e..a8c1d73 100644
--- a/examples/test/examples_runner.clj
+++ b/examples/test/examples_runner.clj
@@ -11,6 +11,16 @@
 (def test-namespaces
   '[pong.core-test life.core-test screens.core-test shortener.core-test fetch.core-test])
 
+;; a check can run for minutes, so say which test is running and how long
+;; each took, rather than print nothing until the end
+(defmethod t/report :begin-test-var [m]
+  (println "  " (-> m :var meta :name) "...")
+  (flush))
+
+(defmethod t/report :end-test-var [m]
+  (println "  " (-> m :var meta :name) "done")
+  (flush))
+
 (defn -main [& args]
   (let [nses (if (seq args) (map symbol args) test-namespaces)
         _ (when-let [bad (seq (remove (set test-namespaces) nses))]

From d4e50ce2d2a32539ca7086653d70d782f549dfd2 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 14:57:08 -0400
Subject: [PATCH 05/10] CI: keep the examples' proof cache between runs

Pong's checks spend most of their time proving its graph edges. writ
already takes a cached proof only when its own source, the spec and the
code are unchanged, so restoring an older cache is safe.
---
 .github/workflows/ci.yml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 9c9b1af..06a8beb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -40,5 +40,12 @@ jobs:
           sudo apt-get install -y liblz4-1 zlib1g libtinfo6
           curl -sL https://raw.githubusercontent.com/jolt-lang/jolt/main/install | bash -s -- --version "$JOLT_VERSION"
           echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+      # proofs found before; writ takes one only when writ, the spec and the
+      # code are all unchanged, so an older cache is safe to start from
+      - uses: actions/cache@v4
+        with:
+          path: examples/.writ-cache
+          key: writ-cache-${{ matrix.example }}-${{ hashFiles('src/**', 'examples/src/**', 'examples/test/**') }}
+          restore-keys: writ-cache-${{ matrix.example }}-
       - name: ${{ matrix.example }}
         run: cd examples && jolt -M:test ${{ matrix.example }}.core-test

From 80335d49778137e3889dc9d9ccfe3a95717061ac Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 19:06:53 -0400
Subject: [PATCH 06/10] Prover: print each term once when sorting by its
 printed form

sort-by with pr-str prints both sides of every comparison, so a sorted
set of facts was printed about 2 log n times per fact.
---
 src/writ/prove/rewrite.clj   | 6 +++---
 src/writ/prove/smt.clj       | 2 +-
 src/writ/prove/term.clj      | 7 +++++++
 src/writ/prove/translate.clj | 6 +++---
 4 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/writ/prove/rewrite.clj b/src/writ/prove/rewrite.clj
index d9197eb..ab4c457 100644
--- a/src/writ/prove/rewrite.clj
+++ b/src/writ/prove/rewrite.clj
@@ -251,7 +251,7 @@
 (defn- lin* [k a] {:c (* k (:c a)) :m (into {} (map (fn [[x v]] [x (* k v)])) (:m a))})
 
 (defn lin->term [{:keys [c m]}]
-  (let [pairs (vec (sort-by (comp pr-str first) (remove (comp zero? second) m)))]
+  (let [pairs (vec (t/sort-printed first (remove (comp zero? second) m)))]
     (cond (empty? pairs) [:lit c]
           (and (zero? c) (= 1 (count pairs)) (= 1 (second (first pairs)))) (ffirst pairs)
           :else [:lin c pairs])))
@@ -635,7 +635,7 @@
   "The term for a plain value: a literal, a sequential or a set of them."
   [v]
   (cond (sequential? v) (let [ts (map value-term v)] (when (every? some? ts) (t/seq-term ts)))
-        (set? v) (let [ts (map value-term (sort-by pr-str v))] (when (every? some? ts) (into [:call 'hash-set] ts)))
+        (set? v) (let [ts (map value-term (t/sort-printed v))] (when (every? some? ts) (into [:call 'hash-set] ts)))
         (or (map? v) (fn? v)) nil
         :else (t/lit v)))
 
@@ -938,7 +938,7 @@
   [ctx hyp vars m]
   (let [unbound? (fn [m c] (some #(and (contains? vars %) (not (contains? m %))) (t/vars c)))
         [plain arith] ((juxt remove filter) #(contains? #{:le :ieq} (head %)) (conjuncts hyp))
-        facts (sort-by pr-str (for [[f v] (:facts ctx) :when (true? v)] f))]
+        facts (t/sort-printed (for [[f v] (:facts ctx) :when (true? v)] f))]
     (letfn [(go [m cs]
               (if-let [c (first cs)]
                 (if (unbound? m c)
diff --git a/src/writ/prove/smt.clj b/src/writ/prove/smt.clj
index 69510fc..c92a64f 100644
--- a/src/writ/prove/smt.clj
+++ b/src/writ/prove/smt.clj
@@ -69,7 +69,7 @@
   "{:formula :decls} saying the facts of ctx imply goal n is truthy."
   [ctx n]
   (let [atoms (atom {:names {} :decls {}})
-        facts (vec (for [[c v] (sort-by (comp pr-str key) (:facts ctx))
+        facts (vec (for [[c v] (t/sort-printed key (:facts ctx))
                          :when (boolean? v)]
                      (let [f (truth ctx atoms c)] (if v f [:not f]))))
         g (truth ctx atoms n)]
diff --git a/src/writ/prove/term.clj b/src/writ/prove/term.clj
index 7984769..068c83f 100644
--- a/src/writ/prove/term.clj
+++ b/src/writ/prove/term.clj
@@ -53,6 +53,13 @@
     (sequential? v) (seq-term (map value->term v))
     :else [:lit v]))
 
+(defn sort-printed
+  "xs in the order they print, or (kf x) prints: terms have no order of
+  their own, and this one is the same on every run.  Each is printed once;
+  sort-by with pr-str prints both sides of every comparison."
+  ([xs] (sort-printed identity xs))
+  ([kf xs] (map peek (sort-by first (map (fn [x] [(pr-str (kf x)) x]) xs)))))
+
 (defn var? [t] (symbol? t))
 
 (defn vars
diff --git a/src/writ/prove/translate.clj b/src/writ/prove/translate.clj
index 6d6c570..e74727c 100644
--- a/src/writ/prove/translate.clj
+++ b/src/writ/prove/translate.clj
@@ -112,7 +112,7 @@
            (cond (nil? v) t/tnil
                  (and (seq? v) (empty? v)) [:sq t/enil]
                  (sequential? v) (t/value->term v)
-                 (and (set? v) (every? scalar? v)) (into [:call 'hash-set] (map t/lit (sort-by pr-str v)))
+                 (and (set? v) (every? scalar? v)) (into [:call 'hash-set] (map t/lit (t/sort-printed v)))
                  (coll? v) (outside! (str "the literal " (pr-str v)))
                  :else [:lit v]))
     :ref (let [s (:name ast)]
@@ -126,7 +126,7 @@
                  (outside! (str "`" s "` passed as a value"))
                  :else (if-let [[x] (constant ctx s)]
                          (if (set? x)
-                           (into [:call 'hash-set] (map t/lit (sort-by pr-str x)))
+                           (into [:call 'hash-set] (map t/lit (t/sort-printed x)))
                            (t/value->term x))
                          (outside! (str "the name `" s "`")))))
     :if [:if (term-of ctx env (:test ast)) (term-of ctx env (:then ast)) (term-of ctx env (:else ast))]
@@ -172,7 +172,7 @@
                 ;; an order fixed by the values so a term is always the same
                 (let [x (term-of ctx env (second (:args ast)))]
                   (reduce (fn [else m] [:if [:call '= x (t/lit m)] [:lit true] else])
-                          [:lit false] (reverse (sort-by pr-str members))))
+                          [:lit false] (reverse (t/sort-printed members))))
                 (invoke-term ctx env f (mapv #(term-of ctx env %) (:args ast)))))
 
     :vec (t/seq-term (mapv #(term-of ctx env %) (:items ast)))

From 5697ea296ec2002764e3c69790e093a614fee36b Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 19:06:53 -0400
Subject: [PATCH 07/10] Prover: summarise a proof trace in one walk that skips
 shared subtrees

A trace shares its subterms, and summary walked it seven times with
tree-seq, which expands the sharing: pong's traces have 16k distinct
nodes walked as 325k. The prover's own pr-str sorts move to
t/sort-printed too. The summary no longer says "with the solver" twice
when a proof both evaluated symbolically and called the solver.
---
 src/writ/prove.clj       | 53 +++++++++++++++++++++-------------------
 test/writ/prove_test.clj | 13 ++++++++++
 2 files changed, 41 insertions(+), 25 deletions(-)

diff --git a/src/writ/prove.clj b/src/writ/prove.clj
index c6df90a..2eb297e 100644
--- a/src/writ/prove.clj
+++ b/src/writ/prove.clj
@@ -45,7 +45,7 @@
   ([n ctx]
    (first (filter #(contains? #{:le :ieq} (head %))
                   (concat (rw/open-conditions n)
-                          (for [[f v] (sort-by (comp pr-str key) (:facts ctx))
+                          (for [[f v] (t/sort-printed key (:facts ctx))
                                 :when (and (true? v) (= :if (head f)))
                                 c (rw/open-conditions f)
                                 :when (not (contains? (:facts ctx) c))]
@@ -62,7 +62,7 @@
   computes."
   [ctx n]
   (first
-    (for [x (sort-by pr-str (distinct (t/subterms n)))
+    (for [x (t/sort-printed (distinct (t/subterms n)))
           :when (and (= :call (head x))
                      (not (contains? '#{= not not= < <= > >= + - * inc dec zero? pos? neg?} (second x))))
           v (drop 2 x)
@@ -93,7 +93,7 @@
   "A variable of a data type the goal or a fact takes apart, as (first v)
   or (= v ...): splitting it into its constructors reveals the tag."
   [opts n ctx]
-  (first (for [x (sort-by pr-str (distinct (mapcat t/subterms (cons n (keys (:facts ctx))))))
+  (first (for [x (t/sort-printed (distinct (mapcat t/subterms (cons n (keys (:facts ctx))))))
                :when (and (= :call (head x)) (contains? '#{first =} (second x)))
                v (drop 2 x)
                :when (and (symbol? v) (sc/data-cases opts v))]
@@ -332,37 +332,40 @@
              :trace {:by :accumulator :call call :c-acc c-acc :acc acc :law-vars (vec law-vars)
                      :on (t/show call) :integer p1 :adds p2}}))))))
 
-(defn- case-vars [trace]
-  (distinct (keep (fn [x] (when (and (map? x) (= :list-cases (:by x))) (:on x)))
-                  (tree-seq coll? seq trace))))
-
-(defn- conditions [trace]
-  (distinct (keep (fn [x] (when (and (map? x) (= :split (:by x))) (:on x)))
-                  (tree-seq coll? seq trace))))
+(defn- trace-steps
+  "The steps of a proof trace, the maps that say :by, in the order a
+  preorder walk meets them.  A trace shares its subterms, so a subtree seen
+  once is not walked again: tree-seq would expand the sharing, twenty times
+  the distinct nodes in pong's traces."
+  [trace]
+  (let [seen (volatile! #{})
+        out (volatile! [])]
+    (letfn [(walk [x]
+              (when (and (coll? x) (not (contains? @seen x)))
+                (vswap! seen conj x)
+                (when (and (map? x) (contains? x :by)) (vswap! out conj x))
+                (doseq [c (seq x)] (walk c))))]
+      (walk trace))
+    @out))
 
 (defn summary
   "A proof trace in one line."
   [trace]
-  (let [on (->> (tree-seq coll? seq trace)
-                (keep #(when (and (map? %) (= :induction (:by %))) (:on %)))
-                first)
-        cs (map (comp pr-str t/show) (conditions trace))]
+  (let [steps (trace-steps trace)
+        ons (fn [by] (distinct (keep #(when (= by (:by %)) (:on %)) steps)))
+        by? (fn [by] (some #(= by (:by %)) steps))
+        on (first (ons :induction))
+        cs (map (comp pr-str t/show) (ons :split))]
     (str (cond on (str "by induction on " on)
-               (some #(and (map? %) (= :symbolic (:by %))) (tree-seq coll? seq trace)) "by symbolic evaluation"
+               (by? :symbolic) "by symbolic evaluation"
                :else "by rewriting")
          (when (seq cs) (str ", splitting on " (str/join " and " cs)))
-         (when (some #(and (map? %) (= :solver (:by %))) (tree-seq coll? seq trace))
-           ", with the solver")
-         (when (some #(and (map? %) (= :symbolic (:by %))) (tree-seq coll? seq trace)) ", with the solver")
-         (when-let [vs (seq (case-vars trace))]
+         (when (or (by? :solver) (by? :symbolic)) ", with the solver")
+         (when-let [vs (seq (ons :list-cases))]
            (str ", with cases on " (str/join " and " vs)))
-         (when-let [gs (seq (distinct (keep (fn [x] (when (and (map? x) (= :generalizing (:by x)))
-                                                       (:on x)))
-                                           (tree-seq coll? seq trace))))]
+         (when-let [gs (seq (ons :generalizing))]
            (str ", generalising " (str/join " and " (map pr-str gs))))
-         (when-let [as (seq (distinct (keep (fn [x] (when (and (map? x) (= :accumulator (:by x)))
-                                                       (:on x)))
-                                           (tree-seq coll? seq trace))))]
+         (when-let [as (seq (ons :accumulator))]
            (str ", generalising the accumulator of " (str/join " and " (map pr-str as)))))))
 
 (defn- recompose
diff --git a/test/writ/prove_test.clj b/test/writ/prove_test.clj
index c63df2a..2ab6b96 100644
--- a/test/writ/prove_test.clj
+++ b/test/writ/prove_test.clj
@@ -546,3 +546,16 @@
       (is (if (pos? k) (<= 0 (mod n k) j) (<= (- j) (mod n k) 0)) [n k])
       (is (<= (- j) (rem n k) j) [n k])
       (is (<= (- j) (- n (* k (quot n k))) j) [n k]))))
+
+(deftest terms-sort-in-the-order-they-print
+  (let [xs ['b [:lit 2] 'a [:lit 10] [:call 'f 'x] "s" :k]]
+    (is (= (sort-by pr-str xs) (t/sort-printed xs)))
+    (is (= (sort-by (comp pr-str key) {'b 1 'a 2 [:lit 1] 3})
+           (t/sort-printed key {'b 1 'a 2 [:lit 1] 3})))))
+
+(deftest a-summary-reads-a-shared-trace-once
+  (let [split {:by :split :on [:le [:lin 0 [['x 1]]]] :proofs []}
+        shared {:by :cases :proofs [split split]}
+        trace {:by :symbolic :proofs [shared shared {:by :solver} {:by :list-cases :on 'xs}]}]
+    (is (= "by symbolic evaluation, splitting on (<= 0 x), with the solver, with cases on xs"
+           (prover/summary trace)))))

From bf3d861769d6e73e363f9158041c867c8021b002 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 19:06:54 -0400
Subject: [PATCH 08/10] Solver search: bind first-pass with an if, not (nil?
 queue)

A jolt release with the new loop-local check rejects the loop otherwise,
and writ would stop loading.
---
 src/writ/solve/search.clj | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/writ/solve/search.clj b/src/writ/solve/search.clj
index 7c2f686..8490e5d 100644
--- a/src/writ/solve/search.clj
+++ b/src/writ/solve/search.clj
@@ -52,7 +52,7 @@
                                      [(conj assign (second r)) (conj units [(second r) i]) (conj q (second r))])
                              [assign units q])))
                        [assign units []] is))]
-    (loop [assign assign, units [], queue (if (nil? queue) nil (vec queue)), first-pass (nil? queue)]
+    (loop [assign assign, units [], queue (if (nil? queue) nil (vec queue)), first-pass (if (nil? queue) true false)]
       (let [is (if first-pass
                  (range (count clauses))
                  (distinct (mapcat #(get occ (negate %)) queue)))

From 253ab062cc96f8f1145e508cad32924431288a76 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 19:06:54 -0400
Subject: [PATCH 09/10] Look for an exists witness among at least 1000 values

The search stops at the first witness, so this costs time only when one
is rare. Pong's playing -> won step needs a game a point from won with
the ball past the paddle, and 100 values sometimes had none, failing the
spec at random.

With that step found, the adequacy check ran for seeds it had been
skipped on, and showed no law pinned new-game down; pong's spec now says
what a new game is.
---
 examples/test/pong/core_spec.clj |  9 +++++++++
 src/writ/spec.clj                | 13 ++++++++++---
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/examples/test/pong/core_spec.clj b/examples/test/pong/core_spec.clj
index 028b27a..dcf75d8 100644
--- a/examples/test/pong/core_spec.clj
+++ b/examples/test/pong/core_spec.clj
@@ -142,6 +142,15 @@
 
 (law a-game-starts-level (= [0 0] (scores (new-game))))
 
+;; ...and with a serve: counting down, the ball on its way right, the paddles
+;; centred. Without it, a new-game that returned any level game passed, since
+;; the one other law naming it compares step's call of it with itself
+(law a-game-starts-with-a-serve
+  (let [[phase ball ly ry] (new-game)]
+    (and (= :Serving (first phase)) (pos? (second phase))
+         (= ball (serve [:Right]))
+         (= ly (quot (- H PH) 2)) (= ry (quot (- H PH) 2)))))
+
 (defn one-point-at-most? [before after]
   (let [[a b] before [a2 b2] after]
     (and (<= a a2) (<= b b2) (<= (+ a2 b2) (inc (+ a b))))))
diff --git a/src/writ/spec.clj b/src/writ/spec.clj
index 7d5e6e7..1f31b3d 100644
--- a/src/writ/spec.clj
+++ b/src/writ/spec.clj
@@ -784,6 +784,8 @@
       (let [[_ [x t] body] p] (recur body (conj bs [x t])))
       [bs p])))
 
+(def ^:private witness-trials 1000)
+
 (defn- test-law
   [ctx {:keys [name prop]} {:keys [trials seed max-size]}]
   (let [[bs body] (leading-foralls prop)
@@ -798,13 +800,18 @@
            :detail (or (:detail r) [[body "the hypothesis does not hold"]])}))
 
       ;; existential: a witness is a counterexample to its negation, so
-      ;; test.check finds it and shrinks it to the simplest one
+      ;; test.check finds it and shrinks it to the simplest one.  The search
+      ;; stops at the first, so a rare one -- a pong game a point from won,
+      ;; with the ball past the paddle -- is looked for harder than a law
+      ;; is tested: at least witness-trials values
       (and (empty? bs) (head? body "exists"))
       (let [[ebs inner] (leading-exists body)
             xs (mapv first ebs)
             ctx* (assoc ctx :vars xs)
-            res (qc (prop/for-all* (mapv #(type->gen (second %) (:tenv ctx)) ebs)
-                                   (fn [& vs] (not= :pass (:result (holds ctx* inner (zipmap xs vs)))))))]
+            res (tc/quick-check (max trials witness-trials)
+                  (prop/for-all* (mapv #(type->gen (second %) (:tenv ctx)) ebs)
+                                   (fn [& vs] (not= :pass (:result (holds ctx* inner (zipmap xs vs))))))
+                  :seed seed :max-size max-size)]
         (if (:pass? res)
           {:law name :status :failed :counterexample {} :seed (:seed res)
            :detail [[(list 'exists (vec (apply concat ebs)) '...)

From d78c894bb67e3a50f7b17dfba7d7b4ecfc84dcb3 Mon Sep 17 00:00:00 2001
From: Yogthos <yogthos@gmail.com>
Date: Fri, 25 Sep 2026 19:11:37 -0400
Subject: [PATCH 10/10] CI: pong back to the examples' 60 minute timeout

It finishes in under four minutes now.
---
 .github/workflows/ci.yml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 06a8beb..daea8b1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,9 +25,7 @@ jobs:
   # one job per example, so they run side by side
   examples:
     runs-on: ubuntu-latest
-    # pong's checks prove every edge of its graph from the code, the slowest
-    # thing the suite does
-    timeout-minutes: ${{ matrix.example == 'pong' && 180 || 60 }}
+    timeout-minutes: 60
     strategy:
       fail-fast: false
       matrix: