Evaluator cache, prover speed, flaky pong spec, parallel CI

.github/workflows/ci.yml

@@ -2,18 +2,48 @@ 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
+    timeout-minutes: 30
     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
+          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
-      - 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 -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

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,20 @@
 (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)]
+;; 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))]
+            (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))))

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))))))

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

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)

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)]

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

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)))

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)))

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)))]
@@ -783,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)
@@ -797,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)) '...)

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)))))

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)}) {}))))))