diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 932c263..daea8b1 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/examples/test/examples_runner.clj b/examples/test/examples_runner.clj index c279ef5..a8c1d73 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,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)))) 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/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/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))) 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))) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index df71ce7..1f31b3d 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)))] @@ -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)) '...) 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))))) 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)}) {}))))))