From 465fe5658b4b3e9cb5f719ee7a3306aaea98466e Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 14:04:25 -0400 Subject: [PATCH 1/8] writ.solve: clauses of linear literals, and a certificate checker writ.solve.pre brings a formula over integers to clauses of integer inequalities and booleans: mod, quot, abs, max, min and ite name fresh variables with their defining cases, uninterpreted fns and predicates are Ackermann-expanded, and the rest goes through Tseitin. writ.solve.cert rebuilds those clauses and checks a proof tree over them: splits, clauses false on a branch, Chvatal-Gomory cuts and Farkas sums. It searches for nothing. --- src/writ/solve/cert.clj | 111 +++++++++++++++ src/writ/solve/pre.clj | 296 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 407 insertions(+) create mode 100644 src/writ/solve/cert.clj create mode 100644 src/writ/solve/pre.clj diff --git a/src/writ/solve/cert.clj b/src/writ/solve/cert.clj new file mode 100644 index 0000000..2f844f3 --- /dev/null +++ b/src/writ/solve/cert.clj @@ -0,0 +1,111 @@ +(ns writ.solve.cert + "The checker for the solver's unsat certificates. It searches for + nothing: it rebuilds the clauses itself, with writ.solve.pre, and walks + the proof tree the search recorded. + + A certificate is {:claim :unsat|:valid, :proof p}. A :valid claim is + about a formula's negation. A proof is a tree: + + {:split l :yes p :no q} l is true in p's branch, its negation in q's + {:clause i} clause i has every literal false on the branch + {:cut [[l k] ...] :then p} + the inequalities l hold on the branch, and + their sum weighted by rationals k >= 0, + a.x <= c, has integer coefficients a; then + a.x <= floor(c) holds in p's branch too + {:farkas [[l k] ...]} the inequalities l hold on the branch, and + their sum weighted by rationals k >= 0 is + 0 <= c for a constant c < 0 + + Each is plainly sound. A split covers every integer assignment, since + over the integers a.x <= c or -a.x <= -c - 1, and a boolean is true or + false. A clause false everywhere on a branch leaves the branch without + a model. A cut is Chvatal and Gomory's: with integer coefficients the + left side is an integer, so it is at most the bound rounded down. And + a nonnegative sum of true inequalities is true, so one + that says 0 is at most a negative number cannot be. So a tree whose + every leaf checks shows the clauses, and with them the formula, have no + model. What must be trusted is this namespace and writ.solve.pre." + (:require [writ.solve.pre :as pre])) + +(defn- reject! [& msg] + (throw (ex-info (apply str msg) {:writ.solve/rejected true}))) + +(defn- literal! + "A split may be on any literal with integer coefficients and bound." + [l] + (let [ok (and (vector? l) (= 3 (count l)) + (case (first l) + :le (let [[_ a c] l] + (and (map? a) (every? integer? (vals a)) (integer? c))) + :bool (boolean? (nth l 2)) + false))] + (when-not ok (reject! "not a literal: " (pr-str l))) + l)) + +(defn combine + "The sum of the inequalities l weighted by k, [:le a c], a without zeros. + Each must be true on the branch path." + [path terms] + (when-not (and (sequential? terms) (seq terms)) + (reject! "an empty combination of inequalities")) + (doseq [t terms] + (let [[l k] (when (and (vector? t) (= 2 (count t))) t)] + (when-not (and (rational? k) (not (neg? k))) + (reject! "a multiplier is not a nonnegative rational: " (pr-str t))) + (when-not (= :le (first l)) + (reject! "a combined term is not an inequality: " (pr-str l))) + (when-not (contains? path l) + (reject! "a combined inequality is not true on its branch: " (pr-str l))))) + (let [sum (reduce (fn [m [[_ a _] k]] (merge-with + m (into {} (map (fn [[x c]] [x (* k c)])) a))) + {} terms)] + [:le (into {} (remove (comp zero? val)) sum) + (reduce + (map (fn [[[_ _ c] k]] (* k c)) terms))])) + +(defn cut + "The literal a cut with multipliers terms derives on branch path." + [path terms] + (let [[_ a c] (combine path terms)] + (when-not (every? integer? (vals a)) + (reject! "a cut's sum has a fractional coefficient: " (pr-str a))) + [:le a (if (integer? c) c (let [n (numerator c) d (denominator c)] (quot (- n (mod n d)) d)))])) + +(defn- farkas! + "The weighted inequalities, all true on the branch, sum to 0 <= negative." + [path terms] + (let [[_ a c] (combine path terms)] + (when (seq a) + (reject! "the Farkas sum leaves variables: " (pr-str a))) + (when-not (neg? c) + (reject! "the Farkas sum is 0 <= " c ", which holds")))) + +(defn- check! + "Every branch of proof p closes, the literals in path being true." + [clauses path p] + (cond + (not (map? p)) (reject! "not a proof: " (pr-str p)) + (contains? p :split) + (let [l (literal! (:split p))] + (check! clauses (conj path l) (:yes p)) + (check! clauses (conj path (pre/negate l)) (:no p))) + (contains? p :clause) + (let [i (:clause p) + c (when (and (integer? i) (< -1 i (count clauses))) (clauses i))] + (when-not c (reject! "no clause " (pr-str i))) + (doseq [l c] + (when-not (contains? path (pre/negate l)) + (reject! "clause " i " is not false on its branch: " (pr-str l))))) + (contains? p :cut) (check! clauses (conj path (cut path (:cut p))) (:then p)) + (contains? p :farkas) (farkas! path (:farkas p)) + :else (reject! "not a proof step: " (pr-str p)))) + +(defn verify + "True when certificate c proves its claim of formula f under decls; + otherwise throws, saying which step is wrong." + [f decls c] + (let [target (case (:claim c) + :unsat f + :valid [:not f] + (reject! "a certificate claims :unsat or :valid, not " (pr-str (:claim c))))] + (check! (:clauses (pre/preprocess target decls)) #{} (:proof c)) + true)) diff --git a/src/writ/solve/pre.clj b/src/writ/solve/pre.clj new file mode 100644 index 0000000..c0b10e0 --- /dev/null +++ b/src/writ/solve/pre.clj @@ -0,0 +1,296 @@ +(ns writ.solve.pre + "The solver's formulas brought to clauses of linear literals. + + A formula over integers is rewritten, deterministically, into a set of + clauses whose literals are of two kinds: + + [:le {x a, y b ...} c] a*x + b*y + ... <= c, integers throughout + [:bool v true|false] a boolean variable, or its negation + + Every term is first made linear, a map of variables to coefficients and + a constant. The rest are named by fresh variables, defined by side + constraints that are conjoined with the formula: + + * (mod t k) and (quot t k) name a quotient q and remainder r with + t = k*q + r, and r bounded as clojure.core has it: mod takes the sign + of the divisor, quot truncates toward zero + * abs, max, min and ite name their value, with one case per branch + * each distinct application of an uninterpreted fn or predicate, its + arguments made linear, is a fresh variable; for each pair of + applications of the same fn, equal arguments imply equal results + (Ackermann's reduction) + + Each fresh variable is defined as a total function of the others, so any + model of the formula extends to one of the result: when the clauses have + no model, neither has the formula. A literal's negation is again a + literal, since over the integers not (a.x <= c) is (-a).x <= -c - 1, and + an inequality is divided through by its coefficients' gcd, rounding the + bound down, which is exact over the integers. + + The boolean structure goes to clauses by Tseitin's encoding in the + one-directional form of Plaisted and Greenbaum, again adding only + definitions. Both the search and the certificate checker run this + namespace, so a certificate is always checked against the clauses the + checker made itself.") + +(defn unsupported! [msg t] + (throw (ex-info msg {:writ.solve/unsupported t}))) + +;; --- linear terms: [{var coeff} constant] ------------------------------------- + +(defn- lin-add [[a c] [b d]] + [(reduce-kv (fn [m x k] (let [s (+ (get m x 0) k)] (if (zero? s) (dissoc m x) (assoc m x s)))) + a b) + (+ c d)]) + +(defn- lin-scale [k [a c]] + (if (zero? k) [{} 0] [(into {} (map (fn [[x v]] [x (* k v)])) a) (* k c)])) + +(defn- lin-sub [l m] (lin-add l (lin-scale -1 m))) + +(defn- constant? [[a _]] (empty? a)) + +(defn lin-value + "The value of a linear term under an assignment of its variables." + [[a c] value-of] + (reduce-kv (fn [s x k] (+ s (* k (value-of x)))) c a)) + +;; --- literals ------------------------------------------------------------------ + +(defn- gcd [a b] (if (zero? b) (abs a) (recur b (rem a b)))) + +(defn- floor-div [a g] (quot (- a (mod a g)) g)) + +(defn le + "The literal for l <= 0, or true or false when l is a constant." + [[a c]] + (if (empty? a) + (<= c 0) + (let [g (reduce gcd 0 (vals a))] + [:le (into {} (map (fn [[x k]] [x (quot k g)])) a) (floor-div (- c) g)]))) + +(defn negate + "A literal's negation." + [[kind x y]] + (case kind + :le [:le (into {} (map (fn [[v k]] [v (- k)])) x) (- (- y) 1)] + :bool [:bool x (not y)])) + +(defn literal? [f] (contains? #{:le :bool} (and (vector? f) (first f)))) + +;; --- formulas in negation normal form: true, false, literals, :and, :or ---------- + +(defn- conj* [fs] + (let [fs (mapcat (fn [f] (if (and (vector? f) (= :and (first f))) (rest f) [f])) fs)] + (cond (some false? fs) false + :else (let [fs (vec (distinct (remove true? fs)))] + (case (count fs) 0 true 1 (first fs) (into [:and] fs)))))) + +(defn- disj* [fs] + (let [fs (mapcat (fn [f] (if (and (vector? f) (= :or (first f))) (rest f) [f])) fs)] + (cond (some true? fs) true + :else (let [fs (vec (distinct (remove false? fs)))] + (case (count fs) 0 false 1 (first fs) (into [:or] fs)))))) + +(defn- negf [f] + (cond (true? f) false + (false? f) true + (literal? f) (negate f) + (= :and (first f)) (disj* (map negf (rest f))) + :else (conj* (map negf (rest f))))) + +(defn- le* [l m] (le (lin-sub l m))) +(defn- lt* [l m] (le (lin-add (lin-sub l m) [{} 1]))) +(defn- eq* [l m] (conj* [(le* l m) (le* m l)])) + +;; --- translation --------------------------------------------------------------- + +(defn- fresh! + "The fresh variable memoised under key, defining it by (side v) when new." + [st key side] + (or (get-in @st [:memo key]) + (let [v [:% (:n @st)]] + (vswap! st #(-> % (update :n inc) (assoc-in [:memo key] v))) + (vswap! st update :sides conj (side v)) + v))) + +(defn- fresh-app! + "The variable for the application of f to linear args ls." + [st kind f ls] + (or (get-in @st [:memo [kind f ls]]) + (let [v [:% (:n @st)]] + (vswap! st #(-> % (update :n inc) (assoc-in [:memo [kind f ls]] v) + (update :apps conj {:kind kind :f f :args ls :var v}))) + v))) + +(defn- check-arity [decls f kind n t] + (when-let [d (get decls f)] + (when-not (and (vector? d) (= kind (first d)) (= n (second d))) + (unsupported! (str "`" f "` is declared " (pr-str d)) t)))) + +(declare formula) + +(defn- term + "The linear form of an integer term." + [st decls t] + (let [tm #(term st decls %) + v [{} 0]] + (cond + (integer? t) [{} t] + (symbol? t) (if (= :bool (get decls t)) + (unsupported! (str "`" t "` is a boolean, not an integer") t) + [{t 1} 0]) + (not (vector? t)) (unsupported! (str "not an integer term: " (pr-str t)) t) + :else + (let [[op & args] t] + (case op + :+ (reduce lin-add v (map tm args)) + :- (if (= 1 (count args)) + (lin-scale -1 (tm (first args))) + (reduce lin-sub (map tm args))) + :neg (lin-scale -1 (tm (first args))) + :* (let [ls (map tm args) + vs (remove constant? ls)] + (when (next vs) (unsupported! "a product of variables is not linear" t)) + (lin-scale (reduce * 1 (map second (filter constant? ls))) + (or (first vs) [{} 1]))) + (:mod :quot) + (let [[x k] args + l (tm x)] + (when-not (and (integer? k) (not (zero? k))) + (unsupported! "a divisor must be a nonzero integer literal" t)) + (if (constant? l) + [{} ((if (= op :mod) mod quot) (second l) k)] + (let [q (fresh! st [:q op l k] (fn [_] true)) + r (fresh! st [op l k] + (fn [r] + (let [q [{q 1} 0] r [{r 1} 0] m (dec (abs k))] + (conj* [(eq* l (lin-add (lin-scale k q) r)) + (le* r [{} m]) (le* [{} (- m)] r) + (if (= op :mod) + (if (pos? k) (le* [{} 0] r) (le* r [{} 0])) + (conj* [(disj* [(lt* l [{} 0]) (le* [{} 0] r)]) + (disj* [(le* [{} 0] l) (le* r [{} 0])])]))]))))] + [{(if (= op :mod) r q) 1} 0]))) + :abs (let [l (tm (first args))] + (if (constant? l) + [{} (abs (second l))] + [{(fresh! st [:abs l] + (fn [a] (let [a [{a 1} 0]] + (conj* [(disj* [(lt* l [{} 0]) (eq* a l)]) + (disj* [(le* [{} 0] l) (eq* a (lin-scale -1 l))])])))) + 1} 0])) + (:max :min) + (let [[l m] (map tm args) + pick (if (= op :max) max min)] + (when-not (= 2 (count args)) (unsupported! "max and min take two terms" t)) + (if (and (constant? l) (constant? m)) + [{} (pick (second l) (second m))] + ;; max is l when m <= l; min is l when l <= m + (let [l-wins (if (= op :max) (le* m l) (le* l m))] + [{(fresh! st [op l m] + (fn [a] (let [a [{a 1} 0]] + (conj* [(disj* [(negf l-wins) (eq* a l)]) + (disj* [l-wins (eq* a m)])])))) + 1} 0]))) + :ite (let [[b x y] args + c (formula st decls b) + l (tm x) + m (tm y)] + (cond (true? c) l + (false? c) m + (= l m) l + :else [{(fresh! st [:ite c l m] + (fn [a] (let [a [{a 1} 0]] + (conj* [(disj* [(negf c) (eq* a l)]) + (disj* [c (eq* a m)])])))) + 1} 0])) + :app (let [[f & xs] args] + (check-arity decls f :fn (count xs) t) + [{(fresh-app! st :fn f (mapv tm xs)) 1} 0]) + (unsupported! (str "not an integer term: " (pr-str t)) t)))))) + +(defn- chain + "A comparison of each adjacent pair of terms, as clojure.core's are." + [st decls rel ts] + (let [ls (map #(term st decls %) ts)] + (conj* (map rel ls (rest ls))))) + +(defn- formula + "The negation normal form of a formula." + [st decls f] + (let [fm #(formula st decls %)] + (cond + (boolean? f) f + (symbol? f) (if (contains? #{nil :bool} (get decls f)) + [:bool f true] + (unsupported! (str "`" f "` is not a boolean") f)) + (not (vector? f)) (unsupported! (str "not a formula: " (pr-str f)) f) + :else + (let [[op & args] f] + (case op + :and (conj* (map fm args)) + :or (disj* (map fm args)) + :not (negf (fm (first args))) + :=> (disj* [(negf (fm (first args))) (fm (second args))]) + :iff (let [[p q] (map fm args)] + (conj* [(disj* [(negf p) q]) (disj* [p (negf q)])])) + := (chain st decls eq* args) + :< (chain st decls lt* args) + :<= (chain st decls le* args) + :> (chain st decls #(lt* %2 %1) args) + :>= (chain st decls #(le* %2 %1) args) + :distinct (let [ls (vec (map #(term st decls %) args))] + (conj* (for [i (range (count ls)) j (range (inc i) (count ls))] + (negf (eq* (ls i) (ls j)))))) + :papp (let [[p & xs] args] + (check-arity decls p :pred (count xs) f) + [:bool (fresh-app! st :pred p (mapv #(term st decls %) xs)) true]) + (unsupported! (str "not a formula: " (pr-str f)) f)))))) + +(defn- ackermann + "For each pair of applications of one fn: equal arguments, equal results." + [apps] + (conj* (for [[i a] (map-indexed vector apps) + b (drop (inc i) apps) + :when (and (= (:kind a) (:kind b)) (= (:f a) (:f b)))] + (disj* (concat (map (comp negf eq*) (:args a) (:args b)) + [(if (= :fn (:kind a)) + (eq* [{(:var a) 1} 0] [{(:var b) 1} 0]) + (let [p [:bool (:var a) true] q [:bool (:var b) true]] + (conj* [(disj* [(negate p) q]) (disj* [p (negate q)])])))]))))) + +;; --- clauses ------------------------------------------------------------------- + +(defn- name-of! + "A literal standing for f: f itself, or a fresh variable implying it." + [st f] + (if (literal? f) + f + (let [p [:bool [:t (:n @st)] true]] + (vswap! st update :n inc) + (let [names (mapv #(name-of! st %) (rest f))] + (vswap! st update :clauses into + (if (= :and (first f)) + (map (fn [g] [(negate p) g]) names) + [(into [(negate p)] names)]))) + p))) + +(defn- clausify! [st f] + (cond + (true? f) nil + (false? f) (vswap! st update :clauses conj []) + (literal? f) (vswap! st update :clauses conj [f]) + (= :and (first f)) (doseq [g (rest f)] (clausify! st g)) + :else (let [c (mapv #(name-of! st %) (rest f))] + (vswap! st update :clauses conj c)))) + +(defn preprocess + "The clauses of formula under decls, with the applications they name: + {:clauses [[lit ...] ...] :apps [{:kind :f :args :var} ...]}." + [f decls] + (let [st (volatile! {:n 0 :memo {} :sides [] :apps [] :clauses []}) + main (formula st decls f) + whole (conj* (concat [main] (:sides @st) [(ackermann (:apps @st))]))] + (clausify! st whole) + (select-keys @st [:clauses :apps]))) From 66347c08e44cd23a47c247b9866bfe598670a51c Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 14:04:25 -0400 Subject: [PATCH 2/8] writ.solve: simplex with Farkas certificates, and DPLL over it A from-scratch Dutertre-de Moura simplex over ratios explains an infeasible bound set as a Farkas sum. DPLL with unit propagation calls it at each node, closes integrality with Gomory cuts and then branch-and-bound, and records the search tree as the proof, dropping any split whose subtree never used its literal. --- src/writ/solve/search.clj | 120 +++++++++++++++++++++++++++++ src/writ/solve/simplex.clj | 153 +++++++++++++++++++++++++++++++++++++ 2 files changed, 273 insertions(+) create mode 100644 src/writ/solve/search.clj create mode 100644 src/writ/solve/simplex.clj diff --git a/src/writ/solve/search.clj b/src/writ/solve/search.clj new file mode 100644 index 0000000..29ed7e4 --- /dev/null +++ b/src/writ/solve/search.clj @@ -0,0 +1,120 @@ +(ns writ.solve.search + "The search for a model of a set of clauses over linear literals: DPLL + with unit propagation, the simplex as its theory solver, and + branch-and-bound for integrality. None of it is trusted: an unsat + answer comes with a proof that writ.solve.cert checks on its own. + + The proof is the search tree. Each node splits on a literal, one that + was decided, propagated, or a branch-and-bound cut x <= k, or adds a + Gomory cut, which is a Chvatal-Gomory combination of literals on the + branch; each leaf + names what closes its branch: a clause every literal of which is false + there, or a Farkas combination of the inequalities that hold there. + A subtree that never used its branch's literal proves its goal without + it, and replaces the split: backjumping, and a smaller proof." + (:require [writ.solve.pre :refer [negate]] + [writ.solve.simplex :as simplex] + [writ.solve.cert :as cert])) + +(def max-cuts + "The most Gomory cuts on one branch before branch-and-bound takes over." + 12) + +(defn- budget! [st] + (vswap! st update :decisions inc) + (when (> (:decisions @st) (:budget @st)) + (throw (ex-info (str "the budget of " (:budget @st) " decisions is exhausted") {::budget true})))) + +(defn- propagate + "Unit propagation from the true literals in assign: [assign units + conflict], units being [literal clause-index] in order." + [clauses assign] + (loop [assign assign units []] + (let [step (reduce (fn [_ i] + (let [c (clauses i)] + (when-not (some assign c) + (let [open (remove #(assign (negate %)) c)] + (cond (empty? open) (reduced [:conflict i]) + (empty? (rest open)) (reduced [:unit (first open) i])))))) + nil (range (count clauses)))] + (case (first step) + :conflict [assign units (second step)] + :unit (recur (conj assign (second step)) (conj units (vec (rest step)))) + [assign units nil])))) + +(defn- theory [st lits] + (or (get-in @st [:theory lits]) + (let [r (simplex/check lits (:max-pivots @st))] + (vswap! st assoc-in [:theory lits] r) + r))) + +(declare node) + +(defn- split + "Try l, then its negation." + [st assign cuts l] + (budget! st) + (let [neg (negate l) + a (node st (conj assign l) cuts)] + (cond + (:sat a) a + (not ((:used a) l)) a + :else (let [b (node st (conj assign neg) cuts)] + (cond + (:sat b) b + (not ((:used b) neg)) b + :else {:proof {:split l :yes (:proof a) :no (:proof b)} + :used (into (disj (:used a) l) (disj (:used b) neg))}))))) + +(defn- add-cut + "Go on with the literal the cut terms derive." + [st assign cuts terms] + (budget! st) + (let [l (cert/cut assign terms) + r (node st (conj assign l) (inc cuts))] + (if (or (:sat r) (not ((:used r) l))) + r + {:proof {:cut terms :then (:proof r)} + :used (into (disj (:used r) l) (map first terms))}))) + +(defn- wrap-units + "Put the propagated literals back into the proof, as splits whose other + branch the propagating clause closes." + [st units r] + (let [clauses (:clauses @st)] + (reduce (fn [r [l i]] + (if (or (:sat r) (not ((:used r) l))) + r + {:proof {:split l :yes (:proof r) :no {:clause i}} + :used (into (disj (:used r) l) + (disj (set (map negate (clauses i))) (negate l)))})) + r (reverse units)))) + +(defn- node [st assign cuts] + (let [clauses (:clauses @st) + [assign units conflict] (propagate clauses assign)] + (wrap-units + st units + (if conflict + {:proof {:clause conflict} :used (set (map negate (clauses conflict)))} + (let [lits (set (filter #(= :le (first %)) assign)) + t (theory st lits)] + (if-let [fk (:conflict t)] + (let [fk (vec (remove #(zero? (second %)) fk))] + {:proof {:farkas fk} :used (set (map first fk))}) + (if-let [c (first (remove #(some assign %) clauses))] + (split st assign cuts (first (remove #(assign (negate %)) c))) + (if-let [[x v] (first (remove #(integer? (val %)) (sort-by (comp str key) (:sat t))))] + (let [terms (when (< cuts max-cuts) (simplex/gomory (:tableau t)))] + (if (and terms (not (assign (cert/cut assign terms)))) + (add-cut st assign cuts terms) + (split st assign cuts [:le {x 1} (simplex/floor-value v)]))) + {:sat true :assign assign :values (:sat t)})))))))) + +(defn solve + "Search clauses for a model. {:sat true :assign #{literal} :values + {var int}} or {:proof p}; throws ::budget when out of decisions." + [clauses {:keys [budget max-pivots]}] + (let [st (volatile! {:clauses clauses :budget budget :max-pivots max-pivots + :decisions 0 :theory {}})] + (node st #{} 0))) diff --git a/src/writ/solve/simplex.clj b/src/writ/solve/simplex.clj new file mode 100644 index 0000000..67f7079 --- /dev/null +++ b/src/writ/solve/simplex.clj @@ -0,0 +1,153 @@ +(ns writ.solve.simplex + "Feasibility of linear inequalities over the rationals, by the general + simplex of Dutertre and de Moura. + + Each inequality a.x <= c bounds a variable: x itself when a is a single + unit coefficient, otherwise a slack s = a.x, one per distinct form up to + sign. The tableau keeps the basic variables as linear combinations of + the nonbasic ones; nonbasic variables always sit within their bounds, + and a basic variable out of its bounds is pivoted back, choosing + variables by Bland's rule so the search ends. + + When a basic variable cannot be brought back, its row names the bounds + that stop it, and those bounds, weighted by the row's coefficients, sum + to 0 <= a negative constant: a Farkas certificate over the literals the + bounds came from. Everything is exact: Clojure's ratios.") + +(defn- floor-rat [v] + (if (integer? v) v (let [n (numerator v) d (denominator v)] (quot (- n (mod n d)) d)))) + +(defn floor-value [v] (floor-rat v)) + +(defn- neg-form [a] (into {} (map (fn [[x k]] [x (- k)])) a)) + +(defn- bound-of + "The variable a literal bounds, the side, and the bound's value." + [slacks [_ a c]] + (if (and (= 1 (count a)) (#{1 -1} (val (first a)))) + (let [[x k] (first a)] (if (= 1 k) [x :hi c] [x :lo (- c)])) + (if (contains? slacks (neg-form a)) + [[:slack (neg-form a)] :lo (- c)] + [[:slack a] :hi c]))) + +(defn- tighter? [side v old] (or (nil? old) (if (= side :hi) (< v (first old)) (> v (first old))))) + +(defn- setup + "Bounds, rows and the variables in Bland's order, for literals lits." + [lits] + (reduce (fn [st [_ a _ :as l]] + (let [slacks (:slacks st) + multi (not (and (= 1 (count a)) (#{1 -1} (val (first a))))) + st (if (and multi (not (contains? slacks a)) (not (contains? slacks (neg-form a)))) + (-> st (update :slacks conj a) (assoc-in [:rows [:slack a]] a)) + st) + [x side v] (bound-of (:slacks st) l) + st (reduce (fn [st y] (if (contains? (:idx st) y) st + (assoc-in st [:idx y] (count (:idx st))))) + st (concat (keys a) [x]))] + (if (tighter? side v (get-in st [:bounds x side])) + (assoc-in st [:bounds x side] [v l]) + st))) + {:slacks #{} :rows {} :bounds {} :idx {}} + lits)) + +(defn- value [st x] (get-in st [:val x] 0)) + +(defn- violation [st x] + (let [v (value st x) lo (get-in st [:bounds x :lo]) hi (get-in st [:bounds x :hi])] + (cond (and lo (< v (first lo))) :lo + (and hi (> v (first hi))) :hi))) + +(defn- pivot-and-update + "Set basic xi to v by moving nonbasic xj, then swap their roles." + [st xi xj v] + (let [rows (:rows st) + row (rows xi) + a (row xj) + theta (/ (- v (value st xi)) a) + vals (reduce-kv (fn [m k r] (if-let [c (r xj)] (assoc m k (+ (get m k 0) (* c theta))) m)) + (:val st) (dissoc rows xi)) + vals (-> vals (assoc xi v) (assoc xj (+ (value st xj) theta))) + new-row (reduce-kv (fn [m k c] (if (= k xj) m (assoc m k (- (/ c a))))) {xi (/ 1 a)} row) + subst (fn [r] (if-let [c (r xj)] + (reduce-kv (fn [m k d] (let [s (+ (get m k 0) (* c d))] + (if (zero? s) (dissoc m k) (assoc m k s)))) + (dissoc r xj) new-row) + r)) + rows (-> (into {} (map (fn [[k r]] [k (subst r)])) (dissoc rows xi)) + (assoc xj new-row))] + (assoc st :rows rows :val vals))) + +(defn- explain + "The Farkas multipliers for basic x stuck below (side :lo) or above its bound." + [st x side] + (let [other {:lo :hi :hi :lo} + lit (fn [y s] (second (get-in st [:bounds y s])))] + (into [[(lit x side) 1]] + (for [[y a] (get-in st [:rows x])] + (if (pos? a) + [(lit y (other side)) a] + [(lit y side) (- a)]))))) + +(defn check + "Are the literals [:le a c] satisfiable over the rationals? {:sat + values} or {:conflict [[literal multiplier] ...]}. Throws ::budget after + max-pivots pivots." + [lits max-pivots] + (let [st (setup lits) + clash (some (fn [[x {:keys [lo hi]}]] (when (and lo hi (> (first lo) (first hi))) x)) + (:bounds st))] + (if clash + {:conflict [[(second (get-in st [:bounds clash :lo])) 1] + [(second (get-in st [:bounds clash :hi])) 1]]} + (let [order #(get-in st [:idx %]) + ;; nonbasic variables start at 0, or the nearest bound + vals (into {} (for [x (keys (:idx st)) :when (not (contains? (:rows st) x))] + (let [{:keys [lo hi]} (get-in st [:bounds x])] + [x (cond (and lo (< 0 (first lo))) (first lo) + (and hi (> 0 (first hi))) (first hi) + :else 0)]))) + vals (reduce-kv (fn [m s row] (assoc m s (reduce-kv (fn [t x k] (+ t (* k (vals x)))) 0 row))) + vals (:rows st))] + (loop [st (assoc st :val vals) n 0] + (when (> n max-pivots) + (throw (ex-info "simplex pivot budget exhausted" {::budget true}))) + (let [bad (first (sort-by order (filter #(violation st %) (keys (:rows st)))))] + (if-not bad + {:sat (into {} (remove (fn [[x _]] (and (vector? x) (= :slack (first x))))) (:val st)) + :tableau (select-keys st [:rows :bounds :val :idx])} + (let [side (violation st bad) + target (first (get-in st [:bounds bad side])) + ;; below its lower bound it must rise, above its upper it must fall + can? (fn [[y a]] + (let [up (if (= side :lo) (pos? a) (neg? a)) + b (get-in st [:bounds y (if up :hi :lo)])] + (or (nil? b) (if up (< (value st y) (first b)) (> (value st y) (first b)))))) + y (first (sort-by order (map first (filter can? (get-in st [:rows bad])))))] + (if y + (recur (pivot-and-update st bad y target) (inc n)) + {:conflict (explain st bad side)}))))))))) + +(defn gomory + "A Gomory cut for a satisfied tableau whose basic variable x has a + fractional value and a row of nonbasic variables all at a bound, as the + Chvatal-Gomory multipliers [[literal k] ...] that derive it, or nil. + + Write each nonbasic y as its bound plus or minus a slack s >= 0, so + x = v + sum a's; the literals saying s >= 0, weighted by the fractional + parts of a', sum to an inequality with integer coefficients that the + current point violates once its bound is rounded down." + [{:keys [rows bounds val idx]}] + (let [value #(get val % 0) + frac #(- % (floor-rat %))] + (first + (for [[x row] (sort-by (comp idx key) rows) + :when (not (integer? (value x))) + :let [terms (for [[y a] row] + (let [{:keys [lo hi]} (get bounds y)] + (cond (and lo (= (value y) (first lo))) [(second lo) (frac a)] + (and hi (= (value y) (first hi))) [(second hi) (frac (- a))])))] + :when (every? some? terms) + :let [terms (vec (remove (comp zero? second) terms))] + :when (seq terms)] + terms)))) From 5a37696e642205bf0aacc4d261b915355700a45a Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 14:04:25 -0400 Subject: [PATCH 3/8] writ.solve: check, valid?, verify and eval-formula The API over the search and the checker, with tests: known sat and unsat cases, mod and quot against clojure.core, integer-only infeasibility, min monotonicity, EUF, a Game of Life shift, budgets, tampered certificates, and random formulas against brute force. --- src/writ/solve.clj | 134 ++++++++++++++++++ test/writ/solve_test.clj | 290 ++++++++++++++++++++++++++++++++++++++ test/writ/test_runner.clj | 5 +- 3 files changed, 427 insertions(+), 2 deletions(-) create mode 100644 src/writ/solve.clj create mode 100644 test/writ/solve_test.clj diff --git a/src/writ/solve.clj b/src/writ/solve.clj new file mode 100644 index 0000000..b11a9df --- /dev/null +++ b/src/writ/solve.clj @@ -0,0 +1,134 @@ +(ns writ.solve + "A certifying solver for linear integer arithmetic with uninterpreted + functions, quantifier free. + + A formula is plain data: + + terms integers, symbols, [:+ t ...] [:- t u ...] [:neg t] + [:* k t] (k an integer), [:mod t k] [:quot t k] (as in + clojure.core, k a nonzero integer), [:abs t] [:max t u] + [:min t u] [:ite p t u], [:app f t ...] + formulas true false, boolean symbols, [:and p ...] [:or p ...] + [:not p] [:=> p q] [:iff p q], [:= t u ...] [:distinct t ...] + [:< t u ...] [:<= t u ...] [:> t u ...] [:>= t u ...], + [:papp p t ...] + + with declarations {x :int, b :bool, f [:fn 2], p [:pred 1]}; an + undeclared symbol is an integer in a term and a boolean in a formula. + + `check` answers :sat with a model, :unsat with a certificate, or + :unknown when its budget runs out. The search that finds either is + not trusted: `verify` checks a certificate without it, with only + writ.solve.pre and writ.solve.cert, and a model is checked by `eval-formula`." + (:require [writ.solve.pre :as pre] + [writ.solve.search :as search] + [writ.solve.simplex :as simplex] + [writ.solve.cert :as cert])) + +(def default-budget 20000) + +(defn- model + "The values of the formula's own variables, and a finite map with a + default for each of its fns and predicates." + [f decls apps {:keys [assign values]}] + (let [value-of #(get values % 0) + empty-fn (fn [kind] {:map {} :default (if (= :fn kind) 0 false)}) + declared (into {} (for [[g d] decls :when (vector? d)] [g (empty-fn (first d))])) + fns (reduce (fn [m {:keys [kind f args var]}] + (update m f (fn [i] (assoc-in (or i (empty-fn kind)) + [:map (mapv #(pre/lin-value % value-of) args)] + (if (= :fn kind) + (value-of var) + (contains? assign [:bool var true])))))) + declared apps) + bool? (fn [x] (or (= :bool (get decls x)) + (contains? assign [:bool x true]) (contains? assign [:bool x false])))] + (into fns + (for [x (into #{} (filter symbol?) (tree-seq vector? seq f)) + :when (not (contains? fns x))] + [x (if (bool? x) (contains? assign [:bool x true]) (value-of x))])))) + +(defn check + "Is formula f satisfiable? {:result :sat :model m}, {:result :unsat + :certificate c} or {:result :unknown :reason s}. opts: :budget, the + most decisions and branch-and-bound splits to make." + [f decls opts] + (let [{:keys [clauses apps]} (pre/preprocess f decls) + budget (or (:budget opts) default-budget)] + (try + (let [r (search/solve clauses {:budget budget :max-pivots (* 100 (max budget 100))})] + (if (:sat r) + {:result :sat :model (model f decls apps r)} + {:result :unsat :certificate {:claim :unsat :proof (:proof r)}})) + (catch clojure.lang.ExceptionInfo e + (if (or (::search/budget (ex-data e)) (::simplex/budget (ex-data e))) + {:result :unknown :reason (ex-message e)} + (throw e)))))) + +(defn valid? + "Is formula f true in every model? {:result :valid :certificate c}, + {:result :invalid :model m} (a counter-model) or {:result :unknown}." + [f decls opts] + (let [r (check [:not f] decls opts)] + (case (:result r) + :unsat {:result :valid :certificate (assoc (:certificate r) :claim :valid)} + :sat {:result :invalid :model (:model r)} + r))) + +(defn verify + "True when certificate c proves what it claims of f: that f is + unsatisfiable, or valid. Throws ex-info naming the wrong step + otherwise. It runs no search." + [f decls c] + (cert/verify f decls c)) + +;; --- evaluation ---------------------------------------------------------------- + +(declare eval-formula) + +(defn- eval-term [t m] + (let [ev #(eval-term % m)] + (cond + (integer? t) t + (symbol? t) (let [v (get m t 0)] (if (integer? v) v 0)) + :else + (let [[op & args] t] + (case op + :+ (reduce + 0 (map ev args)) + :- (apply - (map ev args)) + :neg (- (ev (first args))) + :* (reduce * 1 (map ev args)) + :mod (mod (ev (first args)) (second args)) + :quot (quot (ev (first args)) (second args)) + :abs (abs (ev (first args))) + :max (max (ev (first args)) (ev (second args))) + :min (min (ev (first args)) (ev (second args))) + :ite (if (eval-formula (first args) m) (ev (second args)) (ev (nth args 2))) + :app (let [{fm :map d :default} (get m (first args))] + (get fm (mapv ev (rest args)) (or d 0)))))))) + +(defn eval-formula + "The truth of formula f in model m: a map of variables to values, and + of fns and predicates to {:map {args value} :default value}." + [f m] + (let [ev #(eval-formula % m) + terms #(map (fn [t] (eval-term t m)) %)] + (cond + (boolean? f) f + (symbol? f) (true? (get m f)) + :else + (let [[op & args] f] + (case op + :and (every? ev args) + :or (boolean (some ev args)) + :not (not (ev (first args))) + :=> (or (not (ev (first args))) (ev (second args))) + :iff (= (ev (first args)) (ev (second args))) + := (apply = (terms args)) + :distinct (apply distinct? (terms args)) + :< (apply < (terms args)) + :<= (apply <= (terms args)) + :> (apply > (terms args)) + :>= (apply >= (terms args)) + :papp (let [{pm :map d :default} (get m (first args))] + (true? (get pm (vec (terms (rest args))) (boolean d))))))))) diff --git a/test/writ/solve_test.clj b/test/writ/solve_test.clj new file mode 100644 index 0000000..37c0319 --- /dev/null +++ b/test/writ/solve_test.clj @@ -0,0 +1,290 @@ +(ns writ.solve-test + "The solver: its answers on known formulas, its agreement with brute + force on random ones, and the checker's refusal of a tampered proof." + (:require [clojure.test :refer [deftest is testing]] + [clojure.walk :as walk] + [clojure.test.check :as tc] + [clojure.test.check.generators :as gen] + [clojure.test.check.properties :as prop] + [writ.solve :as s])) + +(defn- unsat? [f & [decls]] + (let [r (s/check f (or decls {}) {})] + (and (= :unsat (:result r)) (s/verify f (or decls {}) (:certificate r))))) + +(defn- sat-model [f & [decls]] + (let [r (s/check f (or decls {}) {})] + (when (= :sat (:result r)) + (when (s/eval-formula f (:model r)) (:model r))))) + +(defn- valid? [f & [decls]] + (let [r (s/valid? f (or decls {}) {})] + (and (= :valid (:result r)) (s/verify f (or decls {}) (:certificate r))))) + +(defn- invalid-model [f & [decls]] + (let [r (s/valid? f (or decls {}) {})] + (when (= :invalid (:result r)) + (when-not (s/eval-formula f (:model r)) (:model r))))) + +;; --- simple cases ------------------------------------------------------------ + +(deftest constants + (is (sat-model true)) + (is (unsat? false)) + (is (unsat? [:< 1 0])) + (is (sat-model [:<= 0 0]))) + +(deftest linear-sat-and-unsat + (is (sat-model [:and [:< 'x 'y] [:< 'y 3] [:> 'x 0]])) + (is (unsat? [:and [:< 'x 'y] [:< 'y 'z] [:< 'z 'x]])) + (is (unsat? [:and [:<= [:+ 'x 'y] 3] [:>= 'x 2] [:>= 'y 2]])) + (is (= {'x 1 'y 2} (select-keys (sat-model [:and [:= 'x 1] [:= [:+ 'x 'y] 3]]) '[x y]))) + (is (unsat? [:and [:= 'x 1] [:distinct 'x 'y] [:= 'y 1]])) + (is (sat-model [:distinct 'x 'y 'z])) + (is (unsat? [:and [:distinct 'x 'y 'z] [:<= 0 'x 1] [:<= 0 'y 1] [:<= 0 'z 1]] + {}) + "three distinct values in {0,1} is impossible")) + +(deftest boolean-structure + (is (unsat? [:and 'p [:not 'p]] {'p :bool})) + (is (valid? [:or 'p [:not 'p]] {'p :bool})) + (is (valid? [:iff [:=> 'p 'q] [:or [:not 'p] 'q]] {'p :bool 'q :bool})) + (is (invalid-model [:=> 'p 'q] {'p :bool 'q :bool})) + (is (valid? [:=> [:and [:< 'x 5] [:or [:= 'x 1] [:= 'x 7]]] [:= 'x 1]]))) + +(deftest nonlinear-products-are-rejected + (is (thrown? clojure.lang.ExceptionInfo (s/check [:= [:* 'x 'y] 1] {} {}))) + (is (= :writ.solve/unsupported + (try (s/check [:= [:* 'x 'y] 1] {} {}) nil + (catch clojure.lang.ExceptionInfo e + (some #{:writ.solve/unsupported} (keys (ex-data e)))))))) + +(deftest products-with-a-literal-either-side + (is (valid? [:= [:* 2 'x] [:* 'x 2]])) + (is (valid? [:= [:* 3 [:+ 'x 1]] [:+ [:* 3 'x] 3]]))) + +;; --- mod and quot follow clojure.core ---------------------------------------- + +(deftest mod-bounds + (is (unsat? [:and [:<= 0 'x] [:< 'x 10] [:= 'y [:mod [:+ 'x 3] 10]] + [:not [:and [:<= 0 'y] [:< 'y 10]]]])) + (is (valid? [:and [:<= 0 [:mod 'x 7]] [:< [:mod 'x 7] 7]])) + (is (valid? [:and [:< -7 [:mod 'x -7]] [:<= [:mod 'x -7] 0]]))) + +(deftest mod-and-quot-agree-with-clojure-core + (doseq [a (range -9 10) k [-4 -3 -1 1 2 5]] + (is (valid? [:= [:mod a k] (mod a k)]) (str "(mod " a " " k ")")) + (is (valid? [:= [:quot a k] (quot a k)]) (str "(quot " a " " k ")")) + (is (valid? [:=> [:= 'x a] [:and [:= [:mod 'x k] (mod a k)] [:= [:quot 'x k] (quot a k)]]]) + (str "symbolic " a " " k)))) + +(deftest quot-truncates + (is (valid? [:=> [:<= 0 'x] [:<= 0 [:quot 'x 3]]])) + (is (valid? [:=> [:<= 'x 0] [:<= [:quot 'x 3] 0]])) + (is (valid? [:=> [:<= 'x 0] [:>= [:quot 'x -3] 0]])) + (is (valid? [:=> [:<= 0 'x] [:= 'x [:+ [:* 4 [:quot 'x 4]] [:mod 'x 4]]]])) + (is (invalid-model [:= 'x [:+ [:* 4 [:quot 'x 4]] [:mod 'x 4]]]))) + +;; --- integers, not rationals -------------------------------------------------- + +(deftest integer-infeasibility + (is (unsat? [:= [:* 2 'x] 1])) + (is (unsat? [:and [:<= 3 [:* 2 'x]] [:<= [:* 2 'x] 3]])) + (is (unsat? [:and [:<= 1 [:- [:* 3 'x] [:* 3 'y]]] [:<= [:- [:* 3 'x] [:* 3 'y]] 2]])) + ;; x = 3, y = 5/3 is a rational point; there is no integer one + (is (unsat? [:and [:= [:- [:* 2 'x] [:* 3 'y]] 1] [:<= 3 'x 4]])) + (is (sat-model [:and [:= [:+ [:* 2 'x] [:* 3 'y]] 1] [:<= 0 'x 10]]))) + +;; --- abs, max, min, ite --------------------------------------------------------- + +(deftest abs-max-min-ite + (is (valid? [:>= [:abs 'x] 0])) + (is (valid? [:>= [:abs 'x] 'x])) + (is (valid? [:= [:max 'x 'y] [:neg [:min [:neg 'x] [:neg 'y]]]])) + (is (valid? [:= [:ite [:< 'x 0] [:neg 'x] 'x] [:abs 'x]])) + (is (invalid-model [:= [:abs 'x] 'x]))) + +(deftest min-is-monotone + (is (valid? [:=> [:<= 'a 'b] [:<= [:min 'cap [:* 2 'a]] [:min 'cap [:* 2 'b]]]])) + (is (invalid-model [:=> [:<= 'a 'b] [:< [:min 'cap [:* 2 'a]] [:min 'cap [:* 2 'b]]]]))) + +(deftest doubling-until-cap + ;; one step of x := min(cap, 2x) keeps 0 < x <= cap and never shrinks x + (let [step [:min 'cap [:* 2 'x]]] + (is (valid? [:=> [:and [:< 0 'x] [:<= 'x 'cap]] + [:and [:< 0 step] [:<= step 'cap] [:<= 'x step]]])) + (is (valid? [:=> [:and [:< 0 'x] [:<= 'x 'cap] [:= step 'x]] [:= 'x 'cap]])) + (is (invalid-model [:=> [:<= 'x 'cap] [:<= 'x step]])))) + +;; --- uninterpreted functions ------------------------------------------------------ + +(deftest euf + (let [d {'f [:fn 1] 'g [:fn 2] 'p [:pred 1]}] + (is (valid? [:=> [:= 'x 'y] [:= [:app 'f 'x] [:app 'f 'y]]] d)) + (is (valid? [:=> [:= 'x [:+ 'y 1]] [:= [:app 'f 'x] [:app 'f [:+ 1 'y]]]] d)) + (is (valid? [:=> [:and [:= 'x 'y] [:papp 'p 'x]] [:papp 'p 'y]] d)) + (is (valid? [:=> [:and [:= 'a 'b] [:= 'c 'd]] [:= [:app 'g 'a 'c] [:app 'g 'b 'd]]] d)) + (is (valid? [:=> [:= 'x 'y] [:= [:app 'f [:app 'f 'x]] [:app 'f [:app 'f 'y]]]] d)) + (let [m (invalid-model [:=> [:= [:app 'f 'x] [:app 'f 'y]] [:= 'x 'y]] d)] + (is m) + (is (map? (get-in m ['f :map]))) + (is (not= (m 'x) (m 'y)))) + (is (invalid-model [:=> [:papp 'p 'x] [:papp 'p 'y]] d)))) + +(deftest game-of-life-shift + ;; the live neighbours of (x-dx, y-dy) in world w are the live neighbours + ;; of (x, y) in w shifted by (dx, dy): w'(a, b) = w(a - dx, b - dy) + (let [d {'w [:pred 2]} + offsets (for [i [-1 0 1] j [-1 0 1] :when (not= [i j] [0 0])] [i j]) + live (fn [a b] [:ite [:papp 'w a b] 1 0]) + in-w (into [:+] (for [[i j] offsets] + (live [:+ [:- 'x 'dx] i] [:+ [:- 'y 'dy] j]))) + in-w' (into [:+] (for [[i j] offsets] + (live [:- [:+ 'x i] 'dx] [:- [:+ 'y j] 'dy])))] + (is (valid? [:= in-w in-w'] d)) + (is (valid? [:and [:<= 0 in-w] [:<= in-w 8]] d)) + (is (valid? [:=> [:= in-w 3] [:iff [:= in-w' 3] true]] d)) + (is (invalid-model [:= in-w 3] d)))) + +;; --- budget --------------------------------------------------------------------- + +(deftest a-tiny-budget-gives-unknown + (let [f [:and [:= [:+ [:* 3 'x] [:* 5 'y]] [:+ [:* 7 'z] 1]] [:> 'x 100] [:> 'y 100] + [:distinct 'x 'y 'z 1 2 3]] + r (s/check f {} {:budget 1})] + (is (= :unknown (:result r))) + (is (string? (:reason r))))) + +(deftest budget-never-gives-a-wrong-answer + (doseq [b [1 2 3 5 8 20]] + (let [f [:and [:= [:- [:* 2 'x] [:* 3 'y]] 1] [:<= 3 'x 4]] + r (s/check f {} {:budget b})] + (is (contains? #{:unsat :unknown} (:result r))) + (when (= :unsat (:result r)) (is (s/verify f {} (:certificate r))))))) + +;; --- certificates --------------------------------------------------------------- + +(defn- farkas-leaves [c] + (let [acc (volatile! [])] + (walk/postwalk (fn [x] (when (and (map? x) (:farkas x)) (vswap! acc conj x)) x) c) + @acc)) + +(defn- perturb-multiplier + "The certificate with the first Farkas multiplier increased by one." + [c] + (let [done (volatile! false)] + (walk/prewalk (fn [x] + (if (and (not @done) (map? x) (seq (:farkas x))) + (do (vreset! done true) + (update-in x [:farkas 0 1] + 1)) + x)) + c))) + +(defn- drop-branch + "The certificate with its first split replaced by the split's yes branch." + [c] + (let [done (volatile! false)] + (walk/prewalk (fn [x] + (if (and (not @done) (map? x) (:split x)) + (do (vreset! done true) (:yes x)) + x)) + c))) + +(defn- has-split? [c] + (let [found (volatile! false)] + (walk/postwalk (fn [x] (when (and (map? x) (:split x)) (vreset! found true)) x) c) + @found)) + +(defn- rejected? [f decls c] + (try (s/verify f decls c) false + (catch clojure.lang.ExceptionInfo _ true))) + +(deftest a-tampered-certificate-is-rejected + (let [f [:and [:< 'x 'y] [:< 'y 'z] [:< 'z 'x]] + c (:certificate (s/check f {} {}))] + (is (s/verify f {} c)) + (is (seq (farkas-leaves c))) + (is (rejected? f {} (perturb-multiplier c))) + (is (rejected? [:and [:< 'x 'y] [:< 'y 'z]] {} c) "a certificate for another formula")) + (let [f [:and [:or [:< 'x 0] [:> 'x 5]] [:<= 0 'x 5]] + c (:certificate (s/check f {} {}))] + (is (s/verify f {} c)) + (is (rejected? f {} (drop-branch c)))) + (let [f [:= [:* 2 'x] 1] + c (:certificate (s/check f {} {}))] + (is (rejected? f {} (assoc c :proof {:farkas []}))) + (is (rejected? f {} (assoc c :proof {:clause 99}))))) + +(deftest a-validity-certificate-says-so + (let [f [:>= [:abs 'x] 0] + r (s/valid? f {} {}) + c (:certificate r)] + (is (= :valid (:claim c))) + (is (s/verify f {} c)) + (is (rejected? [:< [:abs 'x] 0] {} c)))) + +;; --- random formulas against brute force ------------------------------------------ + +(def ^:private vars '[x y z]) + +(def ^:private gen-term + (gen/recursive-gen + (fn [inner] + (gen/one-of + [(gen/fmap (fn [[a b]] [:+ a b]) (gen/tuple inner inner)) + (gen/fmap (fn [[a b]] [:- a b]) (gen/tuple inner inner)) + (gen/fmap (fn [[k a]] [:* k a]) (gen/tuple (gen/choose -3 3) inner)) + (gen/fmap (fn [[a k]] [:mod a k]) (gen/tuple inner (gen/elements [-3 -2 2 3]))) + (gen/fmap (fn [[a k]] [:quot a k]) (gen/tuple inner (gen/elements [-3 -2 2 3]))) + (gen/fmap (fn [a] [:abs a]) inner) + (gen/fmap (fn [[a b]] [:max a b]) (gen/tuple inner inner)) + (gen/fmap (fn [[a b]] [:min a b]) (gen/tuple inner inner)) + (gen/fmap (fn [[a b c]] [:ite [:< a 0] b c]) (gen/tuple inner inner inner))])) + (gen/one-of [(gen/choose -4 4) (gen/elements vars)]))) + +(def ^:private gen-atom + (gen/fmap (fn [[op a b]] [op a b]) + (gen/tuple (gen/elements [:< :<= :> :>= := :distinct]) gen-term gen-term))) + +(def ^:private gen-formula + (gen/recursive-gen + (fn [inner] + (gen/one-of + [(gen/fmap (fn [ps] (into [:and] ps)) (gen/vector inner 1 3)) + (gen/fmap (fn [ps] (into [:or] ps)) (gen/vector inner 1 3)) + (gen/fmap (fn [p] [:not p]) inner) + (gen/fmap (fn [[p q]] [:=> p q]) (gen/tuple inner inner)) + (gen/fmap (fn [[p q]] [:iff p q]) (gen/tuple inner inner))])) + gen-atom)) + +(defn- brute-force + "A model in the box [-6,6]^3, or nil." + [f] + (first (for [x (range -6 7) y (range -6 7) z (range -6 7) + :let [m {'x x 'y y 'z z}] + :when (s/eval-formula f m)] + m))) + +(defn- agrees-with-brute-force [f] + (let [r (s/check f {} {:budget 2000}) + bf (brute-force f)] + (case (:result r) + :sat (s/eval-formula f (:model r)) + :unsat (and (nil? bf) + (s/verify f {} (:certificate r)) + (let [c (:certificate r)] + (and (or (empty? (farkas-leaves c)) (rejected? f {} (perturb-multiplier c))) + (or (not (has-split? c)) (rejected? f {} (drop-branch c)))))) + :unknown true))) + +(deftest random-formulas-agree-with-brute-force + (let [r (tc/quick-check 400 (prop/for-all [f gen-formula] (agrees-with-brute-force f)) + :seed 20260923 :max-size 12)] + (is (:pass? r) (pr-str (select-keys r [:shrunk :fail]))))) + +(deftest random-conjunctions-agree-with-brute-force + ;; conjunctions of atoms are unsat often, so certificates get exercised + (let [r (tc/quick-check 400 (prop/for-all [ps (gen/vector gen-atom 2 5)] + (agrees-with-brute-force (into [:and] ps))) + :seed 7 :max-size 8)] + (is (:pass? r) (pr-str (select-keys r [:shrunk :fail]))))) diff --git a/test/writ/test_runner.clj b/test/writ/test_runner.clj index 7c68822..02e4b75 100644 --- a/test/writ/test_runner.clj +++ b/test/writ/test_runner.clj @@ -7,10 +7,11 @@ writ.gaps-test writ.spec-test writ.prove-test - writ.evidence-test)) + writ.evidence-test + writ.solve-test)) (def test-namespaces - '[writ.check-test writ.book-test writ.gaps-test writ.spec-test writ.prove-test writ.evidence-test]) + '[writ.check-test writ.book-test writ.gaps-test writ.spec-test writ.prove-test writ.evidence-test writ.solve-test]) (defn -main [& _] (let [{:keys [fail error]} (apply t/run-tests test-namespaces)] From 31ffa92b8a42096e3d5cee7fb4fb8fb3fba8b55c Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 20:12:36 -0400 Subject: [PATCH 4/8] writ.solve: incremental simplex, and propagation by occurrence A search node now starts the simplex from its parent's tableau and only repairs the bounds it adds, and unit propagation looks only at the clauses holding the negation of a literal just made true. The slowest query from the pong spec went from 38s to 2.5s. Certificates are unchanged, so the checker is too. --- src/writ/solve.clj | 4 +- src/writ/solve/search.clj | 88 ++++++++++++++++++---------- src/writ/solve/simplex.clj | 114 ++++++++++++++++++++++++------------- 3 files changed, 133 insertions(+), 73 deletions(-) diff --git a/src/writ/solve.clj b/src/writ/solve.clj index b11a9df..9df8f6e 100644 --- a/src/writ/solve.clj +++ b/src/writ/solve.clj @@ -86,7 +86,9 @@ (declare eval-formula) -(defn- eval-term [t m] +(defn eval-term + "The value of integer term t in model m." + [t m] (let [ev #(eval-term % m)] (cond (integer? t) t diff --git a/src/writ/solve/search.clj b/src/writ/solve/search.clj index 29ed7e4..7c2f686 100644 --- a/src/writ/solve/search.clj +++ b/src/writ/solve/search.clj @@ -25,26 +25,49 @@ (when (> (:decisions @st) (:budget @st)) (throw (ex-info (str "the budget of " (:budget @st) " decisions is exhausted") {::budget true})))) +(defn- clause-state + "What clause c says under assign: :sat, [:conflict], [:unit l] or nil." + [c assign] + (when-not (some assign c) + (let [open (remove #(assign (negate %)) c)] + (cond (empty? open) [:conflict] + (empty? (rest open)) [:unit (first open)])))) + (defn- propagate - "Unit propagation from the true literals in assign: [assign units - conflict], units being [literal clause-index] in order." - [clauses assign] - (loop [assign assign units []] - (let [step (reduce (fn [_ i] - (let [c (clauses i)] - (when-not (some assign c) - (let [open (remove #(assign (negate %)) c)] - (cond (empty? open) (reduced [:conflict i]) - (empty? (rest open)) (reduced [:unit (first open) i])))))) - nil (range (count clauses)))] - (case (first step) - :conflict [assign units (second step)] - :unit (recur (conj assign (second step)) (conj units (vec (rest step)))) - [assign units nil])))) + "Unit propagation: [assign units conflict], units being [literal + clause-index] in order. Only the clauses that hold the negation of a + literal just made true can have become unit or false, so those are the + ones looked at: queue holds the literals made true since the last + fixpoint, or is nil to look at every clause." + [st assign queue] + (let [clauses (:clauses @st) + occ (:occ @st) + look (fn [assign units is] + (reduce (fn [[assign units q] i] + (let [r (clause-state (clauses i) assign)] + (case (first r) + :conflict (reduced [assign units q i]) + :unit (if (assign (second r)) + [assign units q] + [(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)] + (let [is (if first-pass + (range (count clauses)) + (distinct (mapcat #(get occ (negate %)) queue))) + [assign units q conflict] (look assign units is)] + (cond + conflict [assign units conflict] + (seq q) (recur assign units q false) + :else [assign units nil]))))) -(defn- theory [st lits] +(defn- theory + "The simplex on lits, started from the tableau the parent node ended + with: a child adds a bound or two, so few pivots repair it." + [st lits from] (or (get-in @st [:theory lits]) - (let [r (simplex/check lits (:max-pivots @st))] + (let [r (simplex/check lits (:max-pivots @st) from)] (vswap! st assoc-in [:theory lits] r) r))) @@ -52,14 +75,14 @@ (defn- split "Try l, then its negation." - [st assign cuts l] + [st assign cuts l tab] (budget! st) (let [neg (negate l) - a (node st (conj assign l) cuts)] + a (node st (conj assign l) cuts [l] tab)] (cond (:sat a) a (not ((:used a) l)) a - :else (let [b (node st (conj assign neg) cuts)] + :else (let [b (node st (conj assign neg) cuts [neg] tab)] (cond (:sat b) b (not ((:used b) neg)) b @@ -68,10 +91,10 @@ (defn- add-cut "Go on with the literal the cut terms derive." - [st assign cuts terms] + [st assign cuts terms tab] (budget! st) (let [l (cert/cut assign terms) - r (node st (conj assign l) (inc cuts))] + r (node st (conj assign l) (inc cuts) [l] tab)] (if (or (:sat r) (not ((:used r) l))) r {:proof {:cut terms :then (:proof r)} @@ -90,31 +113,34 @@ (disj (set (map negate (clauses i))) (negate l)))})) r (reverse units)))) -(defn- node [st assign cuts] +(defn- node [st assign cuts fresh tab] (let [clauses (:clauses @st) - [assign units conflict] (propagate clauses assign)] + [assign units conflict] (propagate st assign fresh)] (wrap-units st units (if conflict {:proof {:clause conflict} :used (set (map negate (clauses conflict)))} (let [lits (set (filter #(= :le (first %)) assign)) - t (theory st lits)] + t (theory st lits tab) + tab (or (:tableau t) tab)] (if-let [fk (:conflict t)] (let [fk (vec (remove #(zero? (second %)) fk))] {:proof {:farkas fk} :used (set (map first fk))}) (if-let [c (first (remove #(some assign %) clauses))] - (split st assign cuts (first (remove #(assign (negate %)) c))) + (split st assign cuts (first (remove #(assign (negate %)) c)) tab) (if-let [[x v] (first (remove #(integer? (val %)) (sort-by (comp str key) (:sat t))))] (let [terms (when (< cuts max-cuts) (simplex/gomory (:tableau t)))] (if (and terms (not (assign (cert/cut assign terms)))) - (add-cut st assign cuts terms) - (split st assign cuts [:le {x 1} (simplex/floor-value v)]))) + (add-cut st assign cuts terms tab) + (split st assign cuts [:le {x 1} (simplex/floor-value v)] tab))) {:sat true :assign assign :values (:sat t)})))))))) (defn solve "Search clauses for a model. {:sat true :assign #{literal} :values {var int}} or {:proof p}; throws ::budget when out of decisions." [clauses {:keys [budget max-pivots]}] - (let [st (volatile! {:clauses clauses :budget budget :max-pivots max-pivots - :decisions 0 :theory {}})] - (node st #{} 0))) + (let [occ (reduce (fn [m [i c]] (reduce (fn [m l] (update m l (fnil conj []) i)) m c)) + {} (map-indexed vector clauses)) + st (volatile! {:clauses clauses :budget budget :max-pivots max-pivots + :decisions 0 :theory {} :occ occ})] + (node st #{} 0 nil nil))) diff --git a/src/writ/solve/simplex.clj b/src/writ/solve/simplex.clj index 67f7079..45fab03 100644 --- a/src/writ/solve/simplex.clj +++ b/src/writ/solve/simplex.clj @@ -32,25 +32,6 @@ (defn- tighter? [side v old] (or (nil? old) (if (= side :hi) (< v (first old)) (> v (first old))))) -(defn- setup - "Bounds, rows and the variables in Bland's order, for literals lits." - [lits] - (reduce (fn [st [_ a _ :as l]] - (let [slacks (:slacks st) - multi (not (and (= 1 (count a)) (#{1 -1} (val (first a))))) - st (if (and multi (not (contains? slacks a)) (not (contains? slacks (neg-form a)))) - (-> st (update :slacks conj a) (assoc-in [:rows [:slack a]] a)) - st) - [x side v] (bound-of (:slacks st) l) - st (reduce (fn [st y] (if (contains? (:idx st) y) st - (assoc-in st [:idx y] (count (:idx st))))) - st (concat (keys a) [x]))] - (if (tighter? side v (get-in st [:bounds x side])) - (assoc-in st [:bounds x side] [v l]) - st))) - {:slacks #{} :rows {} :bounds {} :idx {}} - lits)) - (defn- value [st x] (get-in st [:val x] 0)) (defn- violation [st x] @@ -89,33 +70,84 @@ [(lit y (other side)) a] [(lit y side) (- a)]))))) +(defn- register [st x] + (if (contains? (:idx st) x) st (assoc-in st [:idx x] (count (:idx st))))) + +(defn- row-of + "Linear form a written over the nonbasic variables of the tableau." + [st a] + (reduce-kv (fn [m y k] + (if-let [r (get-in st [:rows y])] + (reduce-kv (fn [m z d] (let [v (+ (get m z 0) (* k d))] (if (zero? v) (dissoc m z) (assoc m z v)))) + m r) + (let [v (+ (get m y 0) k)] (if (zero? v) (dissoc m y) (assoc m y v))))) + {} a)) + +(defn- assert-lit + "The tableau with literal l's bound added: a new variable is nonbasic at + 0, a new slack a basic row over the nonbasic variables." + [st [_ a _ :as l]] + (let [multi (not (and (= 1 (count a)) (#{1 -1} (val (first a))))) + st (reduce register st (keys a)) + st (if (and multi (not (contains? (:slacks st) a)) (not (contains? (:slacks st) (neg-form a)))) + (let [sx [:slack a] + row (row-of st a)] + (-> st (update :slacks conj a) (assoc-in [:rows sx] row) + (register sx) + (assoc-in [:val sx] (reduce-kv (fn [t x k] (+ t (* k (get-in st [:val x] 0)))) 0 row)))) + st) + [x side v] (bound-of (:slacks st) l) + st (register st x)] + (if (tighter? side v (get-in st [:bounds x side])) + (assoc-in st [:bounds x side] [v l]) + st))) + +(defn- repair-nonbasic + "Move each nonbasic variable out of bounds to the bound it breaks, and + the basic variables with it." + [st] + (reduce (fn [st x] + (if (contains? (:rows st) x) + st + (let [v (value st x) + {:keys [lo hi]} (get-in st [:bounds x]) + target (cond (and lo (< v (first lo))) (first lo) + (and hi (> v (first hi))) (first hi))] + (if (nil? target) + st + (let [d (- target v)] + (reduce-kv (fn [st b r] (if-let [c (r x)] (update-in st [:val b] (fnil + 0) (* c d)) st)) + (assoc-in st [:val x] target) (:rows st))))))) + st (keys (:idx st)))) + +(defn empty-tableau [] + {:slacks #{} :rows {} :bounds {} :idx {} :val {}}) + (defn check "Are the literals [:le a c] satisfiable over the rationals? {:sat - values} or {:conflict [[literal multiplier] ...]}. Throws ::budget after - max-pivots pivots." - [lits max-pivots] - (let [st (setup lits) - clash (some (fn [[x {:keys [lo hi]}]] (when (and lo hi (> (first lo) (first hi))) x)) - (:bounds st))] - (if clash - {:conflict [[(second (get-in st [:bounds clash :lo])) 1] - [(second (get-in st [:bounds clash :hi])) 1]]} - (let [order #(get-in st [:idx %]) - ;; nonbasic variables start at 0, or the nearest bound - vals (into {} (for [x (keys (:idx st)) :when (not (contains? (:rows st) x))] - (let [{:keys [lo hi]} (get-in st [:bounds x])] - [x (cond (and lo (< 0 (first lo))) (first lo) - (and hi (> 0 (first hi))) (first hi) - :else 0)]))) - vals (reduce-kv (fn [m s row] (assoc m s (reduce-kv (fn [t x k] (+ t (* k (vals x)))) 0 row))) - vals (:rows st))] - (loop [st (assoc st :val vals) n 0] + values :tableau t} or {:conflict [[literal multiplier] ...]}. Throws + ::budget after max-pivots pivots. Given a tableau a check of fewer of + the literals ended with, it starts from there: only the new bounds need + repairing." + ([lits max-pivots] (check lits max-pivots nil)) + ([lits max-pivots from] + (let [base (or from (empty-tableau)) + st (reduce assert-lit base (remove (or (:asserted base) #{}) lits)) + st (assoc st :asserted (into (or (:asserted base) #{}) lits)) + clash (some (fn [[x {:keys [lo hi]}]] (when (and lo hi (> (first lo) (first hi))) x)) + (:bounds st))] + (if clash + {:conflict [[(second (get-in st [:bounds clash :lo])) 1] + [(second (get-in st [:bounds clash :hi])) 1]]} + (let [order #(get-in st [:idx %])] + (loop [st (repair-nonbasic st) n 0] (when (> n max-pivots) (throw (ex-info "simplex pivot budget exhausted" {::budget true}))) (let [bad (first (sort-by order (filter #(violation st %) (keys (:rows st)))))] (if-not bad - {:sat (into {} (remove (fn [[x _]] (and (vector? x) (= :slack (first x))))) (:val st)) - :tableau (select-keys st [:rows :bounds :val :idx])} + {:sat (into {} (for [x (keys (:idx st)) :when (not (and (vector? x) (= :slack (first x))))] + [x (value st x)])) + :tableau st} (let [side (violation st bad) target (first (get-in st [:bounds bad side])) ;; below its lower bound it must rise, above its upper it must fall @@ -126,7 +158,7 @@ y (first (sort-by order (map first (filter can? (get-in st [:rows bad])))))] (if y (recur (pivot-and-update st bad y target) (inc n)) - {:conflict (explain st bad side)}))))))))) + {:conflict (explain st bad side)})))))))))) (defn gomory "A Gomory cut for a satisfied tableau whose basic variable x has a From f2d1f70a69c74b7ea080f67716e74fa4d21bf026 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 20:12:36 -0400 Subject: [PATCH 5/8] Prove over every input: state graphs, symbolic evaluation, proof namespace Every spec now declares its state graph. An edge into refinements is an obligation that the step lands in the states it names and never throws; a spec with no graph fails the check. The prover runs non-recursive code on symbolic values, Rosette style: branches merge, data values whose constructor depends on a branch are unions, sets of unknown size are predicates and equal by extensionality. The formula goes to writ.solve, and the checker verifies its certificate. Data variables are split by constructor first, bounded integers are enumerated, and open linear goals go to the solver too. A counter-model from the solver becomes a counterexample, run on the code before it is reported, so bugs no test samples are still found. A proof namespace (proof-of, lemma, hint) holds what the prover needs and the spec should not say; lemmas must be proved and never count as laws. Proof results are cached against the exact sources they came from. Also fixed: a graph state of a compound type crashed the check, an `and` hypothesis was not taken apart, and integer refinements were sampled uniformly, missing the edges of their range. --- .gitignore | 3 + src/writ/prove.clj | 246 ++++- src/writ/prove/check.clj | 49 +- src/writ/prove/rewrite.clj | 88 +- src/writ/prove/scheme.clj | 30 +- src/writ/prove/smt.clj | 100 ++ src/writ/prove/symbolic.clj | 896 ++++++++++++++++++ src/writ/prove/term.clj | 9 +- src/writ/prove/translate.clj | 27 +- src/writ/spec.clj | 327 ++++++- test/writ/graph_test.clj | 26 + test/writ/proof_test.clj | 60 ++ test/writ/prove_test.clj | 24 + test/writ/spec_demo/cells.clj | 21 + test/writ/spec_demo/cells_origin.clj | 21 + test/writ/spec_demo/cells_spec.clj | 41 + test/writ/spec_demo/classify_spec.clj | 6 +- test/writ/spec_demo/classify_weak_spec.clj | 6 +- test/writ/spec_demo/court_spec.clj | 8 +- test/writ/spec_demo/flow_spec.clj | 20 + test/writ/spec_demo/light_spec.clj | 6 +- test/writ/spec_demo/nat_chain_spec.clj | 6 +- test/writ/spec_demo/no_graph_spec.clj | 9 + test/writ/spec_demo/pipeline_spec.clj | 7 +- test/writ/spec_demo/pipeline_unknown_spec.clj | 6 +- test/writ/spec_demo/shapes.clj | 30 + test/writ/spec_demo/signal_throw.clj | 14 + test/writ/spec_demo/sort_every_spec.clj | 7 +- .../writ/spec_demo/sort_false_lemma_proof.clj | 8 + test/writ/spec_demo/sort_lemma_proof.clj | 13 + test/writ/spec_demo/sort_lemma_spec.clj | 21 + test/writ/spec_demo/sort_let_spec.clj | 7 +- test/writ/spec_demo/sort_pairs_spec.clj | 7 +- test/writ/spec_demo/sort_proved_spec.clj | 7 +- test/writ/spec_demo/sort_spec.clj | 7 +- test/writ/spec_demo/sort_unproved_spec.clj | 7 +- test/writ/spec_demo/sort_vacuous_spec.clj | 7 +- test/writ/spec_demo/sort_weak_spec.clj | 7 +- test/writ/spec_demo/total_spec.clj | 6 +- test/writ/spec_demo/tree_spec.clj | 7 +- test/writ/symbolic_test.clj | 113 +++ test/writ/test_runner.clj | 6 +- 42 files changed, 2201 insertions(+), 115 deletions(-) create mode 100644 src/writ/prove/smt.clj create mode 100644 src/writ/prove/symbolic.clj create mode 100644 test/writ/proof_test.clj create mode 100644 test/writ/spec_demo/cells.clj create mode 100644 test/writ/spec_demo/cells_origin.clj create mode 100644 test/writ/spec_demo/cells_spec.clj create mode 100644 test/writ/spec_demo/flow_spec.clj create mode 100644 test/writ/spec_demo/no_graph_spec.clj create mode 100644 test/writ/spec_demo/shapes.clj create mode 100644 test/writ/spec_demo/signal_throw.clj create mode 100644 test/writ/spec_demo/sort_false_lemma_proof.clj create mode 100644 test/writ/spec_demo/sort_lemma_proof.clj create mode 100644 test/writ/spec_demo/sort_lemma_spec.clj create mode 100644 test/writ/symbolic_test.clj diff --git a/.gitignore b/.gitignore index d522e3e..b572bc3 100644 --- a/.gitignore +++ b/.gitignore @@ -29,3 +29,6 @@ .claude/ AGENTS.md CLAUDE.md + +# writ proof cache +.writ-cache/ diff --git a/src/writ/prove.clj b/src/writ/prove.clj index b19ea55..045886e 100644 --- a/src/writ/prove.clj +++ b/src/writ/prove.clj @@ -15,21 +15,94 @@ a term throws. A proof that never unfolds one of the target's own definitions says nothing about the code, and is not reported." (:require [clojure.string :as str] + [clojure.test.check.generators :as gen] [writ.prove.term :as t :refer [head]] [writ.prove.rewrite :as rw] [writ.prove.translate :as tr] [writ.prove.check :as check] + [writ.prove.smt :as smt] + [writ.prove.symbolic :as sym] [writ.prove.scheme :as sc :refer [split-foralls goal plain cases truthy? falsy? solve-eq assume-hyp subst-all instance ih-for useful-ih replace-term lemma-rules]])) ;; --- proving a goal --------------------------------------------------------------------- + +(declare prove-goal) ;; Every step records what the checker needs to replay it: writ.prove.check ;; follows the trace with writ.prove.scheme and the rewriter, and searches ;; for nothing. -(defn- split-candidate [n] - (first (filter #(contains? #{:le :ieq} (head %)) (rw/open-conditions n)))) +(defn- split-candidate + "An open integer comparison to split on: in the goal, or in a fact that + is still an if, such as a disjunction taken as a hypothesis." + ([n] (split-candidate n nil)) + ([n ctx] + (first (filter #(contains? #{:le :ieq} (head %)) + (concat (rw/open-conditions n) + (for [[f v] (sort-by (comp pr-str key) (:facts ctx)) + :when (and (true? v) (= :if (head f))) + c (rw/open-conditions f) + :when (not (contains? (:facts ctx) c))] + c)))))) + +(def ^:private enum-limit + "The most values a bounded integer is split into, one case each." + 16) + +(defn- enum-candidate + "An integer variable that an unmodelled call takes, such as + (bit-shift-left 1 k), whose facts bound it to a few values, as [k lo + hi]. A case per value puts a literal in the call, which the rewriter + computes." + [ctx n] + (first + (for [x (sort-by pr-str (distinct (t/subterms n))) + :when (and (= :call (head x)) + (not (contains? '#{= not not= < <= > >= + - * inc dec zero? pos? neg?} (second x)))) + v (drop 2 x) + :when (and (symbol? v) (rw/int-term? ctx v)) + :let [bound (fn [sign] + (first (for [[f tv] (:facts ctx) + :when (and (true? tv) (= :le (head f))) + :let [d (second f)] + :when (and (= :lin (head d)) (= [[v sign]] (nth d 2)))] + (* (- sign) (second d))))) + lo (or (bound 1) (when (= 'Nat (get-in ctx [:types v])) 0)) + hi (bound -1)] + :when (and lo hi (<= 1 (- hi lo) enum-limit))] + [v lo hi]))) + +(defn- by-enumeration + "Prove g by one case per value of v from lo to hi, which the facts + bound it to: each case puts the value in for v." + [opts g hyps depth [v lo hi]] + (let [ps (mapv (fn [k] + (let [[o g* hs] (subst-all opts g hyps {v [:lit k]})] + (prove-goal o g* hs (dec depth)))) + (range lo (inc hi)))] + (when (every? some? ps) + {:by :enumeration :on v :from lo :to hi :cases ps}))) + +(defn- data-var + "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)))))) + :when (and (= :call (head x)) (contains? '#{first =} (second x))) + v (drop 2 x) + :when (and (symbol? v) (sc/data-cases opts v))] + v))) + +(defn- by-data-cases + "Prove g by splitting data variable v into one case per constructor." + [opts g hyps depth v] + (let [ps (mapv (fn [[value types]] + (let [[o g* hs] (subst-all (update opts :types merge types) g hyps {v value})] + (prove-goal o g* hs (dec depth)))) + (sc/data-cases opts v))] + (when (every? some? ps) + {:by :data-cases :on v :cases ps}))) (def ^:dynamic *stuck* "When bound to an atom, collects the goals a search could not close, as @@ -42,8 +115,6 @@ [opts n] (first (filter #(map? (get-in opts [:types %])) (sort-by str (t/vars n))))) -(declare prove-goal) - (defn- by-list-cases "Prove g by splitting element-list variable v into empty and a head and a tail. Not induction: the tail gets no hypothesis of its own." @@ -58,28 +129,45 @@ {:by :list-cases :on v :empty empty :cons more}))) (defn- prove-goal - "Prove boolean term g under hyps, splitting on open integer comparisons, - and on the shape of an unknown list of elements. Returns a trace or nil." + "Prove boolean term g under hyps. In order: a data value's tag is split + into its constructors; integer arithmetic through and through goes to + the solver whole; an open integer comparison is split into its two + outcomes; a bounded integer an unmodelled call takes is split into its + values; an unknown list of elements into its two shapes; and whatever + is left open goes to the solver. Returns a trace or nil." [opts g hyps depth] - (let [[ctx vacuous n] (sc/case-context opts g hyps)] + (let [[ctx vacuous n] (sc/case-context opts g hyps) + split (delay (split-candidate n ctx)) + solve (delay (smt/prove ctx n)) + solved (fn [] (when-let [c @solve] {:by :solver :certificate c}))] (swap! (:unfolded opts) into @(:unfolded ctx)) - (when (and *stuck* (not vacuous) (not (truthy? n)) (or (zero? depth) (nil? (split-candidate n)))) + (when (and *stuck* (not vacuous) (not (truthy? n)) (or (zero? depth) (nil? @split))) (swap! *stuck* conj {:goal n :facts (:facts ctx)})) (cond vacuous {:by :hypothesis-false} (truthy? n) {:by :rewriting} - (zero? depth) nil - (nil? (split-candidate n)) - (when-let [v (elems-var opts n)] - (by-list-cases opts g hyps depth v)) + (zero? depth) (solved) :else - (when-let [c (split-candidate n)] - (let [yes (if-let [[x v] (and (= :ieq (head c)) (solve-eq (second c)))] - (let [[o g* hs] (subst-all opts g hyps {x v})] - (prove-goal o g* hs (dec depth))) - (prove-goal opts g (conj hyps c) (dec depth))) - no (prove-goal opts g (conj hyps [:call 'not c]) (dec depth))] - (when (and yes no) {:by :split :on c :then yes :else no})))))) + (if-let [v (data-var opts n ctx)] + (by-data-cases opts g hyps depth v) + (or ;; each data case, once its tags are known: the code run + ;; symbolically, one small formula for the solver + (when-not (:symbolic-tried opts) + (when-let [[c used] (sym/prove opts hyps g)] + (swap! (:unfolded opts) into used) + {:by :symbolic :certificate c})) + (when (smt/pure? ctx n) (solved)) + (if-let [c @split] + (let [opts (assoc opts :symbolic-tried true) + yes (if-let [[x v] (and (= :ieq (head c)) (solve-eq (second c)))] + (let [[o g* hs] (subst-all opts g hyps {x v})] + (prove-goal o g* hs (dec depth))) + (prove-goal opts g (conj hyps c) (dec depth))) + no (when yes (prove-goal opts g (conj hyps [:call 'not c]) (dec depth)))] + (when (and yes no) {:by :split :on c :then yes :else no})) + (or (when-let [e (enum-candidate ctx n)] (by-enumeration opts g hyps depth e)) + (when-let [v (elems-var opts n)] (by-list-cases opts g hyps depth v)) + (solved)))))))) (defn- prove-all "Prove every goal (under the hyps) in one context of opts." @@ -89,6 +177,33 @@ (declare by-induction) +(defn- sample-gen + "A generator for values of a prover type, or nil." + [ty] + (cond + (= 'Nat ty) gen/nat + (= 'Int ty) gen/small-integer + (= 'Bool ty) gen/boolean + (and (map? ty) (:elems ty)) (some-> (sample-gen (:elems ty)) gen/list) + (and (seq? ty) (contains? '#{List Vec} (first ty))) (some-> (sample-gen (second ty)) gen/list) + :else nil)) + +(defn- plausible? + "Does goal gi survive a few random values of its variables? A + generalisation can make a goal false; testing it first, as ACL2s does, + saves searching for a proof that is not there. Only a value that makes + the hypotheses true and a goal false counts; a throw is no evidence." + [opts gi] + (let [vs (vec (sort-by str (reduce into #{} (map t/vars (concat (:hyps gi) (:goals gi)))))) + gens (mapv #(sample-gen (get-in opts [:types %])) vs)] + (or (some nil? gens) + (not-any? (fn [i] + (let [env (zipmap vs (map #(gen/generate % (mod i 20) i) gens))] + (try (and (every? #(t/evaluate % env) (:hyps gi)) + (not-every? #(t/evaluate % env) (:goals gi))) + (catch Throwable _ false)))) + (range 30))))) + (defn- by-generalizing "Prove an induction case by using an equality hypothesis the other way round, then generalising the recursive call it brought in to a fresh @@ -113,7 +228,8 @@ ty (get-in opts [:rets (second call)]) g* (sc/generalization opts gi ih call ys) opts* (-> opts (assoc :generalized? true :ih []) (update :types assoc ys ty)) - p (when g* (or (prove-all opts* g*) (by-induction opts* g* ys ty)))] + p (when (and g* (plausible? opts* g*)) + (or (prove-all opts* g*) (by-induction opts* g* ys ty)))] :when p] {:by :generalizing :ih i :call call :as ys :ty ty :on (t/show call) :proof p})))) @@ -214,8 +330,13 @@ (keep #(when (and (map? %) (= :induction (:by %))) (:on %))) first) cs (map (comp pr-str t/show) (conditions trace))] - (str (if on (str "by induction on " on) "by rewriting") + (str (cond on (str "by induction on " on) + (some #(and (map? %) (= :symbolic (:by %))) (tree-seq coll? seq trace)) "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))] (str ", with cases on " (str/join " and " vs))) (when-let [gs (seq (distinct (keep (fn [x] (when (and (map? x) (= :generalizing (:by x))) @@ -227,6 +348,16 @@ (tree-seq coll? seq trace))))] (str ", generalising the accumulator of " (str/join " and " (map pr-str as))))))) +(defn- recompose + "A counterexample over the expanded binders, as values of the law's own: + a Tuple binder's value is the vector of its components'." + [bs0 cex] + (letfn [(value [x ty] + (if (and (seq? ty) (= 'Tuple (first ty))) + (vec (map-indexed (fn [i cty] (value (symbol (str x "-" i)) (plain cty))) (rest ty))) + (get cex x)))] + (into {} (for [[x ty] bs0] [x (value x (plain ty))])))) + (defn- expand-tuples "Each binder of a Tuple type as a vector of fresh variables, one per component, with the component's type: a value of (Tuple A B) is exactly @@ -242,12 +373,49 @@ (recur (rest todo) (conj out [x ty]) g)) [out g]))) +(defn- symbolic-cases + "Prove goal g under hyps by splitting each data variable into its + constructors, and running every case symbolically: small formulas, one + per combination of tags, where one formula for all of them would make + the solver search the tags too. The same trace a case split on data + and a symbolic leaf make, so the checker replays it as those." + [opts hyps g] + (if-let [v (first (filter #(sc/data-cases opts %) + (sort-by str (reduce into (t/vars g) (map t/vars hyps)))))] + (let [ps (mapv (fn [[value types]] + (let [[o g* hs] (subst-all (update opts :types merge types) g hyps {v value})] + (symbolic-cases o hs g*))) + (sc/data-cases opts v))] + (when (every? some? ps) + {:by :data-cases :on v :cases ps})) + (when-let [[c used] (sym/prove opts hyps g)] + (swap! (:unfolded opts) into used) + {:by :symbolic :certificate c}))) + +(defn- by-symbolic-cases + "Every goal by symbolic-cases, when the code runs symbolically at all." + [opts {:keys [hyps goals]}] + (when (every? #(sym/formula opts hyps %) goals) + (let [ps (mapv #(symbolic-cases opts hyps %) goals)] + (when (every? some? ps) + {:by :cases :proofs ps})))) + +(defn- by-symbolic + "Prove every goal by running it on symbolic values and handing the one + formula to the solver: no case splits, so a step fn with many + conditions is one query." + [opts {:keys [hyps goals]}] + (let [rs (mapv #(sym/prove opts hyps %) goals)] + (when (every? some? rs) + (swap! (:unfolded opts) into (mapcat second rs)) + {:by :symbolic :certificates (mapv first rs)}))) + (defn prove-law "Try to prove a law. prop is the desugared law, its names qualified; defs are the translated definitions; target the implementation's ns; lemmas are the laws proved before it, as {:name :prop}. Returns {:proved true :trace :summary :lemmas} or {:proved false :reason}." - [{:keys [prop defs tenv target own fuel lemmas rets]}] + [{:keys [prop defs tenv target own fuel lemmas rets total hint]}] (try (let [[bs0 body] (split-foralls prop) tctx (tr/context own) @@ -256,18 +424,39 @@ unfolded (atom #{}) lemmas-used (atom #{}) opts {:defs defs :tenv tenv :types (into {} (map (fn [[x ty]] [x (plain ty)])) bs) + :total total :unfolded unfolded :fuel (or fuel 20000) :lemmas-used lemmas-used :rets (or rets {}) - :lemmas (vec (mapcat #(lemma-rules % defs tenv own) lemmas))} + :lemmas (vec (mapcat #(lemma-rules % defs tenv own) + (if-let [use (:use hint)] + (filter #(contains? (set use) (:name %)) lemmas) + lemmas)))} ;; an attempt that runs out of fuel fails on its own; the others ;; still get their turn + ran-out (atom false) attempt (fn [f] (reset! unfolded #{}) (reset! lemmas-used #{}) (let [r (try (f) (catch clojure.lang.ExceptionInfo e - (if (:writ.prove.rewrite/fuel (ex-data e)) nil (throw e))))] + (if (:writ.prove.rewrite/fuel (ex-data e)) + (do (reset! ran-out true) nil) + (throw e))))] [r @unfolded])) - tries (concat [#(some->> (prove-all opts g) (hash-map :by :cases :proofs))] - (for [[v ty] bs] #(by-induction opts g v ty))) + symbolic [#(by-symbolic-cases opts g) #(by-symbolic opts g)] + rewriting [#(some->> (prove-all opts g) (hash-map :by :cases :proofs))] + ;; a hint's variable first + bs-order (if-let [v (:induct hint)] + (concat (filter #(= v (first %)) bs) (remove #(= v (first %)) bs)) + bs) + induction (for [[v ty] bs-order] #(by-induction opts g v ty)) + tries (cond + ;; that nothing throws is known only from running the code + ;; symbolically, where every throw is noted + total symbolic + (= :symbolic (:strategy hint)) symbolic + (= :rewriting (:strategy hint)) rewriting + (= :induction (:strategy hint)) induction + (:induct hint) (concat induction symbolic rewriting) + :else (concat [(first symbolic)] rewriting [(second symbolic)] induction)) [trace used] (or (first (filter first (map attempt tries))) [nil #{}]) ;; a fold into an accumulator: prove it adds, then try again with that [trace used] (if trace @@ -292,13 +481,16 @@ checked (when (and trace (seq target-used)) (check/check-proof (dissoc opts :lemmas-used :unfolded) g trace))] (cond - (nil? trace) {:proved false :reason "no proof found"} + (nil? trace) (cond-> {:proved false :reason (if @ran-out "the search ran out of fuel" "no proof found")} + (seq bs) (merge (when-let [cex (first (keep #(sym/counterexample opts (:hyps g) %) (:goals g)))] + {:counterexample (recompose bs0 cex)}))) (empty? target-used) {:proved false :reason "the proof does not use the code"} (not (:ok checked)) {:proved false :reason (str "the proof checker rejected the proof: " (:reason checked))} :else (let [cited (sort (remove synthetic-lemmas @lemmas-used))] {:proved true :trace trace :summary (str (summary trace) + (when total ", and it never throws") (when (seq cited) (str ", citing " (str/join ", " cited)))) :lemmas (vec cited)}))) (catch clojure.lang.ExceptionInfo e diff --git a/src/writ/prove/check.clj b/src/writ/prove/check.clj index 98bd1dd..f86aa53 100644 --- a/src/writ/prove/check.clj +++ b/src/writ/prove/check.clj @@ -22,7 +22,9 @@ this namespace: not the search, its heuristics or its bookkeeping." (:require [writ.prove.term :as t :refer [head]] [writ.prove.rewrite :as rw] - [writ.prove.scheme :as sc])) + [writ.prove.scheme :as sc] + [writ.prove.smt :as smt] + [writ.prove.symbolic :as sym])) (defn- reject! [& msg] (throw (ex-info (apply str msg) {::rejected true}))) @@ -30,13 +32,22 @@ (declare check-goal check-cases check-induction) (defn- check-goal - "Replay the proof of boolean goal g under hyps." + "Replay the proof of boolean goal g under hyps. The goal is normalised + only for the steps that read it: a case split on data and a symbolic + leaf do not, and normalising a large goal is where time goes." [opts g hyps p] - (let [[_ vacuous n] (sc/case-context opts g hyps)] + (let [cc (delay (sc/case-context opts g hyps)) + vacuous (delay (second @cc)) + n (delay (nth @cc 2))] (case (:by p) - :hypothesis-false (when-not vacuous (reject! "a hypothesis said to be false is not")) - :rewriting (when-not (or vacuous (sc/truthy? n)) - (reject! "the goal does not rewrite to true: " (pr-str (t/show n)))) + :hypothesis-false (when-not @vacuous (reject! "a hypothesis said to be false is not")) + :symbolic (when-not (sym/verify opts hyps g (:certificate p)) + (reject! "the solver's certificate does not prove " (pr-str (t/show g)))) + :solver (let [[ctx _ n] (sc/case-context opts g hyps)] + (when-not (or @vacuous (smt/verify ctx n (:certificate p))) + (reject! "the solver's certificate does not prove " (pr-str (t/show n))))) + :rewriting (when-not (or @vacuous (sc/truthy? @n)) + (reject! "the goal does not rewrite to true: " (pr-str (t/show @n)))) :split (let [c (:on p)] (if-let [[x v] (and (= :ieq (head c)) (sc/solve-eq (second c)))] (let [[o g* hs] (sc/subst-all opts g hyps {x v})] @@ -49,6 +60,25 @@ (doseq [[[value types] sub] (map vector (sc/list-cases opts v) [(:empty p) (:cons p)])] (let [[o g* hs] (sc/subst-all (update opts :types merge types) g hyps {v value})] (check-goal o g* hs sub)))) + :enumeration (let [{v :on lo :from hi :to cs :cases} p + [ctx] (sc/case-context opts g hyps) + holds? #(= [:lit true] (rw/normalize ctx %))] + (when-not (and (symbol? v) (integer? lo) (integer? hi) (<= lo hi) + (holds? [:call '<= [:lit lo] v]) (holds? [:call '<= v [:lit hi]])) + (reject! "the facts do not bound `" v "` to " lo ".." hi)) + (when-not (= (count cs) (inc (- hi lo))) + (reject! "the cases on `" v "` are not one per value")) + (doseq [[k sub] (map vector (range lo (inc hi)) cs)] + (let [[o g* hs] (sc/subst-all opts g hyps {v [:lit k]})] + (check-goal o g* hs sub)))) + :data-cases (let [v (:on p) + cs (or (sc/data-cases opts v) + (reject! "`" v "` is not of a data type"))] + (when-not (= (count cs) (count (:cases p))) + (reject! "the cases on `" v "` are not one per constructor")) + (doseq [[[value types] sub] (map vector cs (:cases p))] + (let [[o g* hs] (sc/subst-all (update opts :types merge types) g hyps {v value})] + (check-goal o g* hs sub)))) (reject! "a goal cannot be proved " (pr-str (:by p)))))) (defn- check-all @@ -119,6 +149,13 @@ (case (:by trace) :cases (check-all opts g (:proofs trace)) :induction (check-induction opts g trace) + :symbolic (let [{:keys [hyps goals]} g + cs (:certificates trace)] + (when-not (= (count cs) (count goals)) + (reject! "a certificate for each goal is missing")) + (doseq [[gl c] (map vector goals cs)] + (when-not (sym/verify opts hyps gl c) + (reject! "the solver's certificate does not prove " (pr-str (t/show gl)))))) :with (let [rules (check-accumulator opts (:lemma trace)) opts* (update opts :lemmas into rules) inner (:proof trace)] diff --git a/src/writ/prove/rewrite.clj b/src/writ/prove/rewrite.clj index c45a0c6..cbe1260 100644 --- a/src/writ/prove/rewrite.clj +++ b/src/writ/prove/rewrite.clj @@ -207,6 +207,15 @@ (= :sq (head c)) (elems-ok? (second c)) :else false))) +(declare int-term?) + +(defn- division? + "quot, mod or rem of an integer by a nonzero integer literal: an integer." + [ctx t] + (and (= :call (head t)) (contains? '#{quot mod rem} (second t)) (= 4 (count t)) + (t/int-lit? (nth t 3)) (not (zero? (second (nth t 3)))) + (int-term? ctx (nth t 2)))) + (defn int-term? "Is t known to be an integer? Literals, linear forms, counts, variables typed Nat or Int, and a term a fact, hypothesis or proved lemma says is @@ -218,6 +227,7 @@ (and (= :call (head t)) (= 'count (second t))) (and (= :call (head t)) (= 'apply (second t)) (= [:cfn '+] (nth t 2 nil)) (int-elems? ctx (nth t 3 nil))) + (division? ctx t) (and (contains? #{:app :call} (head t)) (proved-integer? ctx t)))) (defn- nat-atom? [ctx a] @@ -288,6 +298,22 @@ (recur (concat rest combined) budget)) false))))) +(defn- division-bounds + "What is known of a division atom, as constraints c + sum k*x >= 0. + With |k| - 1 = j: (mod n k) is 0..j for k > 0 and -j..0 for k < 0; + (rem n k) is -j..j; and n - k*(quot n k), the remainder, is -j..j." + [ctx a] + (when (division? ctx a) + (let [[_ f n [_ k]] a + j (dec (abs k)) + between (fn [lf lo hi] [(lin+ lf {:c (- lo) :m {}}) (lin+ (lin* -1 lf) {:c hi :m {}})]) + self {:c 0 :m {a 1}}] + (case f + mod (if (pos? k) (between self 0 j) (between self (- j) 0)) + rem (between self (- j) j) + quot (when-let [ln (lin-of ctx n)] + (between (lin+ ln (lin* (- k) self)) (- j) j)))))) + (defn- known-constraints "The integer facts in ctx, as constraints c + sum k*x >= 0, with each Nat atom they or `extra` mention known to be at least 0." @@ -300,7 +326,9 @@ nil)] lf) atoms (distinct (mapcat (comp keys :m) (concat facts extra)))] - (concat facts (for [a atoms :when (nat-atom? ctx a)] {:c 0 :m {a 1}})))) + (concat facts + (for [a atoms :when (nat-atom? ctx a)] {:c 0 :m {a 1}}) + (mapcat #(division-bounds ctx %) atoms)))) (defn decide-le "true / false / nil for 0 <= d, from its form, Nat atoms and the facts." @@ -357,7 +385,7 @@ (case (head c) :nil false :lit (not (false? (second c))) - (:sq :fn :cfn) true + (:sq :fn :cfn :dfn) true :if (let [a (truthiness ctx (nth c 2)) b (truthiness ctx (nth c 3))] (when (and (some? a) (= a b)) a)) :call (if (contains? seq-makers (second c)) @@ -514,12 +542,57 @@ (= :elems (head e)) [:call 'reduce f init (second e)] :else nil))) +(def ^:private pure-fns + "clojure.core fns that compute a value from plain data and nothing else, + so a call of one on closed values is its value." + '#{sort distinct reverse hash-set set sort-by count vec str name keyword + subs frequencies max min abs quot mod rem inc dec + - * nth first second + last rest butlast take drop concat interpose}) + +(defn- closed-value + "The Clojure value of a closed term built from literals, or ::none." + [x] + (case (head x) + :lit (second x) + :nil nil + :sq (let [vs (loop [e (second x), out []] + (case (head e) + :enil out + :econs (let [v (closed-value (nth e 1))] (if (= ::none v) nil (recur (nth e 2) (conj out v)))) + nil))] + (if (nil? vs) ::none (apply list vs))) + :call (if (= 'hash-set (second x)) + (let [vs (map closed-value (drop 2 x))] (if (some #{::none} vs) ::none (set vs))) + ::none) + ::none)) + +(defn- value-term + "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))) + (or (map? v) (fn? v)) nil + :else (t/lit v))) + +(defn- ground-call + "A pure core fn applied to closed values, computed: the code is pure, + so running it is its meaning. nil when it is not closed or throws." + [x] + (when (and (= :call (head x)) (contains? pure-fns (second x))) + (let [vs (map closed-value (drop 2 x))] + (when (not-any? #{::none} vs) + (try (value-term (let [r (apply @(resolve (symbol "clojure.core" (name (second x)))) vs)] + (if (seq? r) (doall r) r))) + (catch Throwable _ nil)))))) + (defn- computed "The computed rules: a rewrite of t, or nil." [ctx x] (case (head x) :call - (let [[_ f & args] x + (or + (when-not (= 'hash-set (second x)) (ground-call x)) + (let [[_ f & args] x n (count args) [a b] args] (case f @@ -568,6 +641,10 @@ [:sq (reduce (fn [e v] [:eapp [:elems v] e]) [:elems (last args)] (reverse (butlast args)))]) identity (when (= 1 n) a) + (bit-shift-left bit-shift-right) + (when (and (= 2 n) (t/int-lit? a) (t/int-lit? b) (<= 0 (second b) 62)) + [:lit ((case f bit-shift-left bit-shift-left bit-shift-right bit-shift-right) + (second a) (second b))]) (quot mod rem) (when (and (= 2 n) (all-num-lits? args) (integer? (second a)) (integer? (second b)) (not (zero? (second b)))) [:lit ((case f quot quot mod mod rem rem) (second a) (second b))]) @@ -579,14 +656,15 @@ reduce (when (= 3 n) (reduce-rule ctx a b (nth args 2))) nth (when (and (<= 2 n 3) (t/int-lit? b)) (nth-rule a (second b) (if (= 3 n) (nth args 2) ::none))) - nil)) + nil))) :ap (let [[_ f & args] x] (cond (and (= :fn (head f)) (= (count (second f)) (count args))) (t/subst (nth f 2) (zipmap (second f) args)) - ;; a core fn value applied is a call of it + ;; a core fn value applied is a call of it, and a defn's an app (= :cfn (head f)) (into [:call (second f)] args) + (= :dfn (head f)) (into [:app (second f)] args) :else nil)) :le (let [d (decide ctx x)] (when (some? d) [:lit d])) diff --git a/src/writ/prove/scheme.clj b/src/writ/prove/scheme.clj index 9da04eb..bd027ef 100644 --- a/src/writ/prove/scheme.clj +++ b/src/writ/prove/scheme.clj @@ -105,13 +105,14 @@ (defn assume-hyp "[ctx vacuous?] with hypothesis h, already normalised, taken as true. - (if c a false) holds when c and a do, and (if c false b) when c does not - and b does, so each part becomes a fact of its own." + (if c a false) holds when c and a do, as does (if c a c), the shape + `and` lowers to; (if c false b) holds when c does not and b does. So + each part becomes a fact of its own." [ctx h] (cond (truthy? h) [ctx false] (falsy? h) [ctx true] - (and (= :if (head h)) (falsy? (nth h 3))) + (and (= :if (head h)) (or (falsy? (nth h 3)) (= (nth h 1) (nth h 3)))) (let [[c1 v1] (assume-hyp ctx (nth h 1))] (if v1 [c1 true] (assume-hyp c1 (rw/normalize c1 (nth h 2))))) (and (= :if (head h)) (falsy? (nth h 2))) @@ -211,13 +212,30 @@ under them, and the goal g normalised there. vacuous? when a hypothesis is false, and then there is nothing to prove." [opts g hyps] - (let [[ctx vacuous] (reduce (fn [[c vac] h] - (if vac [c vac] (assume-hyp c (rw/normalize c h)))) - [(rw/context (dissoc opts :ih)) false] hyps) + (let [take-all (fn [ctx0 hs] + (reduce (fn [[c vac] h] + (if vac [c vac] (assume-hyp c (rw/normalize c h)))) + [ctx0 false] hs)) + [ctx vacuous] (take-all (rw/context (dissoc opts :ih)) hyps) + ;; a hypothesis read before a later one decided its test (an or + ;; whose first case a split ruled out) is read again under all of + ;; them + [ctx vacuous] (if vacuous [ctx vacuous] (take-all ctx hyps)) ctx (assoc ctx :ih (mapv (fn [i] (update i :lhs #(rw/normalize ctx %))) (:ih opts))) ctx (assoc ctx :memo (atom {}) :stuck (atom #{}) :int-memo (atom {}))] [ctx vacuous (when-not vacuous (rw/normalize ctx g))])) +(defn data-cases + "One case per constructor of v's data type, as [[value types] ...]; nil + when v is not of a data type. A case split, not induction: no case + gets a hypothesis." + [opts v] + (let [ty (get-in opts [:types v]) + h (if (seq? ty) (first ty) ty) + d (when (symbol? h) (get-in opts [:tenv h]))] + (when (and d (:ctors d) (not (:tvar d))) + (mapv (juxt :value :types) (cases v ty (:tenv opts)))))) + (defn list-cases "The two shapes of an unknown list of elements v: empty, and a head and a tail, as [[value types] [value types]]." diff --git a/src/writ/prove/smt.clj b/src/writ/prove/smt.clj new file mode 100644 index 0000000..69510fc --- /dev/null +++ b/src/writ/prove/smt.clj @@ -0,0 +1,100 @@ +(ns writ.prove.smt + "A goal the rewriter leaves open, handed to writ.solve. + + The goal and the facts it is under become one formula: facts imply that + the goal is truthy. Integer terms -- literals, linear forms, integer + variables, quot and mod by a literal -- are the solver's terms, and + comparisons of them its atoms. Any other term is an atom of its own: + an integer the solver knows nothing about, or the truth of a test, the + same term always the same atom. So the formula is weaker than the goal, + never stronger, and when the solver finds it valid the goal holds. + + The formula is built the same way every time from the same goal and + facts, and the solver's certificate is checked by writ.solve/verify, so + the proof checker replays this step without searching." + (:require [writ.prove.term :as t :refer [head]] + [writ.prove.rewrite :as rw] + [writ.solve :as solve])) + +(def budget + "Decisions the solver may make on one goal; past it, the goal stays open." + 3000) + +(defn- atom-of + "The symbol standing for term x, the next free one the first time." + [atoms kind x] + (or (get-in @atoms [:names x]) + (let [n (symbol (str "%" (name kind) (count (:names @atoms))))] + (swap! atoms #(-> % (assoc-in [:names x] n) (assoc-in [:decls n] kind))) + n))) + +(declare truth) + +(defn- int-of [ctx atoms x] + (cond + (t/int-lit? x) (second x) + (= :lin (head x)) (into [:+ (second x)] + (for [[a k] (nth x 2)] [:* k (int-of ctx atoms a)])) + (and (symbol? x) (rw/int-term? ctx x)) (atom-of atoms :int x) + (and (= :call (head x)) (contains? '#{quot mod} (second x)) (= 4 (count x)) + (t/int-lit? (nth x 3)) (not (zero? (second (nth x 3)))) (rw/int-term? ctx (nth x 2))) + [(keyword (name (second x))) (int-of ctx atoms (nth x 2)) (second (nth x 3))] + (rw/int-term? ctx x) (atom-of atoms :int x) + :else nil)) + +(defn- ints [ctx atoms xs] + (let [vs (mapv #(int-of ctx atoms %) xs)] + (when (every? some? vs) vs))) + +(defn truth + "The formula for 'x is truthy'." + [ctx atoms x] + (case (head x) + :lit (not (false? (second x))) + :nil false + (:sq :fn :cfn) true + :le (if-let [d (int-of ctx atoms (second x))] [:<= 0 d] (atom-of atoms :bool x)) + :ieq (if-let [d (int-of ctx atoms (second x))] [:= 0 d] (atom-of atoms :bool x)) + :if [:or [:and (truth ctx atoms (nth x 1)) (truth ctx atoms (nth x 2))] + [:and [:not (truth ctx atoms (nth x 1))] (truth ctx atoms (nth x 3))]] + :call (let [[_ f & args] x] + (cond + (and (= 'not f) (= 1 (count args))) [:not (truth ctx atoms (first args))] + (and (contains? '#{= < <= > >=} f) (= 2 (count args)) (ints ctx atoms args)) + (into [(keyword (name f))] (ints ctx atoms args)) + :else (atom-of atoms :bool x))) + (atom-of atoms :bool x))) + +(defn goal-formula + "{: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)) + :when (boolean? v)] + (let [f (truth ctx atoms c)] (if v f [:not f])))) + g (truth ctx atoms n)] + {:formula [:=> (into [:and true] facts) g] + :decls (:decls @atoms)})) + +(defn pure? + "Is the goal, under its facts, integer arithmetic through and through: + no atom but integers? Then the solver decides it whole." + [ctx n] + (every? #(= :int %) (vals (:decls (goal-formula ctx n))))) + +(defn prove + "A certificate that goal n holds under the facts of ctx, or nil." + [ctx n] + (let [{:keys [formula decls]} (goal-formula ctx n)] + (when (some #(= :int %) (vals decls)) + (let [r (try (solve/valid? formula decls {:budget budget}) + (catch clojure.lang.ExceptionInfo _ nil))] + (when (= :valid (:result r)) + (:certificate r)))))) + +(defn verify + "Does certificate c prove goal n under the facts of ctx?" + [ctx n c] + (let [{:keys [formula decls]} (goal-formula ctx n)] + (try (solve/verify formula decls c) + (catch clojure.lang.ExceptionInfo _ false)))) diff --git a/src/writ/prove/symbolic.clj b/src/writ/prove/symbolic.clj new file mode 100644 index 0000000..09c3f43 --- /dev/null +++ b/src/writ/prove/symbolic.clj @@ -0,0 +1,896 @@ +(ns writ.prove.symbolic + "Symbolic evaluation of a goal into one formula for writ.solve. + + Rewriting a goal splits it at every if, and a step fn with a dozen + conditions makes thousands of cases. Here the goal is run once, on + symbolic values, the way Rosette runs a program: the two branches of an + if are both run, and their values are merged under the test. Merging + keeps the result small -- two integers merge into one, defined once as + an if of the two, two vectors of one length merge element by element -- + and only values of different shapes, a data value whose constructor + depends on the branch, are kept apart, as a union of guarded values. + + A value is one of + + {:int t} an integer, t a solver term + {:bool f} true or false, f a solver formula + {:const t} a keyword, string, char or symbol, t its code + {:nil} + {:vec [v ...]} a sequential value of known length + {:set {...}} a set, or a seq drawn from one: :mem gives the + formula for 'x is in it'; :elems, when it is + finite, its elements as [guard v]; :elem a value + shaped like its elements + {:fn f} a fn value: f takes a vector of values + {:union [[g v] ...]} v where formula g holds; the gs are disjoint + :bottom a throw + + A set of unknown size -- a variable of type (Set T) -- is a predicate + the solver knows nothing about: x is in it when the predicate holds of + x. The image of such a set under a translation, a fn adding a fixed + offset to each part of an element, is the predicate at x minus the + offset. Two sets are equal when an element the solver may choose + freely is in both or in neither: extensionality, read the same way in a + goal or a hypothesis. + + A constant's code is fixed per distinct literal; a variable of a type + of constants is an integer the solver may give any value, so it may + equal any literal, or none. That can only add models, never remove + one, so a formula found valid holds of the code. + + What is outside -- recursion, collections of unknown length, fns as + values -- makes the evaluation give up, and the goal is left to the + rest of the prover. Proofs are for every input on which the terms + return: a branch that throws is never taken, so merging it with a value + is that value. + + `formula` is deterministic, so the proof checker rebuilds it and checks + the solver's certificate for it." + (:require [writ.prove.term :as t :refer [head]] + [writ.solve :as solve])) + +(def ^:dynamic *why* + "When bound to an atom, collects why evaluations gave up, for debugging." + nil) + +(defn- give-up! [why] + (throw (ex-info (str "outside symbolic evaluation: " why) {::outside why}))) + +;; --- state: fresh names, definitions and constant codes ------------------------- + +(defn- state [] + (atom {:n 0 :defs [] :decls {} :codes {} :memo {} :path [] :throws []})) + +(defn- fresh! [st kind] + (let [n (:n @st) + s (symbol (str "%" (name kind) n))] + (swap! st #(-> % (update :n inc) (assoc-in [:decls s] kind))) + s)) + +(defn- define! + "A fresh variable standing for integer term or formula e." + [st kind e] + (if (or (symbol? e) (integer? e) (boolean? e)) + e + (let [v (fresh! st kind)] + (swap! st #(-> % (update :defs conj (if (= :int kind) [:= v e] [:iff v e])) + (assoc-in [:def-of v] e))) + v))) + +(defn- interval + "[lo hi] an integer term lies in, nil for no bound on that side: from + its literals, the bounds its variables are known to have, and the + definitions of the variables merging introduced." + [st t] + (let [iv #(interval st %) + add (fn [[a b] [c d]] [(when (and a c) (+ a c)) (when (and b d) (+ b d))]) + neg (fn [[a b]] [(when b (- b)) (when a (- a))]) + lo-of (fn [xs] (when (every? some? xs) (apply min xs))) + hi-of (fn [xs] (when (every? some? xs) (apply max xs)))] + (cond + (integer? t) [t t] + (symbol? t) (if-let [d (get-in @st [:def-of t])] + (iv d) + (get-in @st [:bounds t] [nil nil])) + (vector? t) + (let [[op & xs] t] + (case op + :+ (reduce add [0 0] (map iv xs)) + :- (if (next xs) (reduce add (iv (first xs)) (map (comp neg iv) (rest xs))) (neg (iv (first xs)))) + :neg (neg (iv (first xs))) + :* (let [[k u] xs [a b] (iv u)] + (if (integer? k) + (if (neg? k) [(when b (* k b)) (when a (* k a))] [(when a (* k a)) (when b (* k b))]) + [nil nil])) + :ite (let [[a b] (iv (nth xs 1)) [c d] (iv (nth xs 2))] [(lo-of [a c]) (hi-of [b d])]) + :min (let [[a b] (iv (first xs)) [c d] (iv (second xs))] [(lo-of [a c]) (cond (and b d) (min b d) b b :else d)]) + :max (let [[a b] (iv (first xs)) [c d] (iv (second xs))] [(cond (and a c) (max a c) a a :else c) (hi-of [b d])]) + :mod (let [k (second xs)] (if (pos? k) [0 (dec k)] [(inc k) 0])) + [nil nil])) + :else [nil nil]))) + +(defn- code! + "The integer code of a constant literal: distinct literals, distinct codes." + [st c] + (or (get-in @st [:codes c]) + (let [k (- -1000000 (count (:codes @st)))] + (swap! st assoc-in [:codes c] k) + k))) + +;; --- values --------------------------------------------------------------------- + +(defn- const? [x] (or (keyword? x) (string? x) (char? x) (symbol? x))) + +(defn- lit-value [st x] + (cond + (nil? x) {:nil true} + (boolean? x) {:bool x} + (integer? x) {:int x} + (const? x) {:const (code! st x)} + :else (give-up! (str "the literal " (pr-str x))))) + +(defn- alts + "A value as guarded alternatives." + [v] + (cond (= :bottom v) [] + (:union v) (:union v) + :else [[true v]])) + +(defn- conj-f [a b] + (cond (true? a) b (true? b) a (or (false? a) (false? b)) false :else [:and a b])) + +(defn- shape [v] + (cond (:int v) :int (contains? v :int) :int + (contains? v :bool) :bool + (contains? v :const) :const + (:nil v) :nil + (:vec v) [:vec (count (:vec v))] + (:set v) :set + (:fn v) :fn + :else (give-up! "a value of no known shape"))) + +(declare merge-values) + +(defn- merge-same + "Merge two values of one shape under formula c." + [st c a b] + (case (shape a) + :int {:int (define! st :int [:ite c (:int a) (:int b)])} + :const {:const (define! st :int [:ite c (:const a) (:const b)])} + :bool {:bool (define! st :bool [:or [:and c (:bool a)] [:and [:not c] (:bool b)]])} + :nil a + :set (let [sa (:set a) sb (:set b)] + {:set {:mem (fn [x] [:or [:and c ((:mem sa) x)] [:and [:not c] ((:mem sb) x)]]) + :elems (when (and (:elems sa) (:elems sb)) + (vec (concat (for [[g v] (:elems sa)] [(conj-f c g) v]) + (for [[g v] (:elems sb)] [(conj-f [:not c] g) v])))) + :distinct (and (:distinct sa) (:distinct sb)) + :elem (or (:elem sa) (:elem sb))}}) + :fn (give-up! "a fn value chosen by a test") + {:vec (mapv #(merge-values st c %1 %2) (:vec a) (:vec b))})) + +(defn- union-of + "A value from guarded alternatives, alternatives of one shape merged." + [st gvs] + (let [gvs (for [[g v] gvs + [g2 v2] (alts v) + :let [g* (conj-f g g2)] + :when (not (false? g*))] + [g* v2])] + (cond + (empty? gvs) :bottom + (= 1 (count gvs)) (second (first gvs)) + :else + (let [groups (vals (group-by (comp shape second) gvs)) + merged (for [g groups] + (reduce (fn [[ga va] [gb vb]] + [[:or ga gb] (merge-same st ga va vb)]) + g))] + (if (= 1 (count merged)) + (second (first merged)) + {:union (vec merged)}))))) + +(defn merge-values + "The value that is a when c holds and b otherwise." + [st c a b] + (cond + (true? c) a + (false? c) b + (= :bottom a) b + (= :bottom b) a + (and (not (:union a)) (not (:union b)) (= (shape a) (shape b))) (merge-same st c a b) + :else (union-of st (concat (for [[g v] (alts a)] [(conj-f c g) v]) + (for [[g v] (alts b)] [(conj-f [:not c] g) v]))))) + +(defn- throws! + "Clojure throws here: arithmetic on nil, first of a number." + [] + (throw (ex-info "throws" {::throws true}))) + +(defn- record-throw! + "Note that evaluation throws when formula g holds on the current path." + [st g] + (when-not (false? g) + (swap! st update :throws conj (reduce conj-f g (:path @st))))) + +(defn- on-path + "(f), with formula c added to the path the evaluation is on." + [st c f] + (swap! st update :path conj c) + (try (f) (finally (swap! st update :path pop)))) + +(defn- guarded + "(f x), or :bottom where Clojure would throw, noting that it does." + [st f x] + (try (f x) + (catch clojure.lang.ExceptionInfo e + (if (::throws (ex-data e)) + (do (record-throw! st true) :bottom) + (throw e))))) + +(defn- lift + "Apply f to each alternative of v, merging the results; an alternative + on which Clojure throws is never taken, and the throw is noted." + [st f v] + (if (:union v) + (union-of st (vec (for [[g x] (:union v)] [g (on-path st g #(guarded st f x))]))) + (if (= :bottom v) :bottom (guarded st f v)))) + +(defn- lift2 [st f a b] + (lift st (fn [x] (lift st (fn [y] (f x y)) b)) a)) + +(defn truth + "The formula for 'v is truthy'." + [v] + (cond + (= :bottom v) true + (:union v) (into [:or] (for [[g x] (:union v)] (conj-f g (truth x)))) + (contains? v :bool) (:bool v) + (:nil v) false + :else true)) + +(defn- int-of + "The integer of v; arithmetic on anything else throws in Clojure." + [v] + (if (contains? v :int) (:int v) (throws!))) + +(declare equal) + +(defn- fresh-like + "A value shaped like v, of fresh variables the solver may choose." + [st v] + (case (shape v) + :int {:int (fresh! st :int)} + :const {:const (fresh! st :int)} + :bool {:bool (fresh! st :bool)} + :nil v + :set (give-up! "a set of sets") + :fn (give-up! "a set of fns") + {:vec (mapv #(fresh-like st %) (:vec v))})) + +(defn- flat + "The solver terms of an element, part by part, or nil when it has a + part no predicate can take." + [v] + (cond (contains? v :int) [(:int v)] + (contains? v :const) [(:const v)] + (:vec v) (let [ps (map flat (:vec v))] (when (every? some? ps) (vec (apply concat ps)))) + :else nil)) + +(defn- member-of + "The formula for 'x is one of these guarded elements'." + [st elems x] + (into [:or false] (for [[g v] elems] (conj-f g (truth (lift2 st (fn [p q] {:bool (equal st p q)}) x v)))))) + +(defn- finite-set + "A set of guarded elements; distinct when it is a set, not a seq drawn + from one, so equal elements count once." + [st elems distinct] + {:set {:mem (fn [x] (member-of st elems x)) + :elems (vec elems) + :distinct distinct + :elem (second (first elems))}}) + +(defn- equal + "The formula for (= a b)." + [st a b] + (let [sa (shape a) sb (shape b)] + (cond + (not= sa sb) false + (= :int sa) [:= (:int a) (:int b)] + (= :const sa) [:= (:const a) (:const b)] + (= :bool sa) [:iff (:bool a) (:bool b)] + (= :nil sa) true + (= :set sa) (let [tmpl (or (:elem (:set a)) (:elem (:set b)))] + (if (nil? tmpl) + true + (let [x (fresh-like st tmpl)] + [:iff ((:mem (:set a)) x) ((:mem (:set b)) x)]))) + (= :fn sa) (give-up! "equality of fns") + :else (reduce conj-f true (map (fn [x y] (truth (lift2 st (fn [p q] {:bool (equal st p q)}) x y))) + (:vec a) (:vec b)))))) + +;; --- evaluating terms ------------------------------------------------------------- + +(declare ev app apply-fn image core* finite-set) + +(defn- var-value + "The value of a variable of type ty: fresh solver variables, and the + facts its type gives, such as a Nat at least 0." + [st facts ty tenv v] + (let [ty (if (seq? ty) (apply list (map #(if (symbol? %) (symbol (name %)) %) ty)) + (if (symbol? ty) (symbol (name ty)) ty))] + (cond + (= 'Int ty) {:int (fresh! st :int)} + (= 'Nat ty) (let [x (fresh! st :int)] + (swap! facts conj [:<= 0 x]) + (swap! st assoc-in [:bounds x] [0 nil]) + {:int x}) + (= 'Bool ty) {:bool (fresh! st :bool)} + (contains? '#{Keyword String Char Symbol} ty) {:const (fresh! st :int)} + (and (seq? ty) (= 'Tuple (first ty))) + {:vec (mapv #(var-value st facts % tenv v) (rest ty))} + (and (seq? ty) (= 'Set (first ty))) + (let [tmpl (var-value st (atom []) (second ty) tenv v) + n (count (or (flat tmpl) (give-up! (str "a set of " (pr-str (second ty)))))) + p (fresh! st :pred)] + (swap! st assoc-in [:decls p] [:pred n]) + {:set {:pred p + :mem (fn [x] (if-let [ts (flat x)] + (if (= n (count ts)) (into [:papp p] ts) false) + false)) + :elem tmpl}}) + (and (symbol? ty) (get-in tenv [ty :ctors]) (empty? (:params (get tenv ty)))) + (let [ctors (sort-by str (keys (get-in tenv [ty :ctors]))) + tag (fresh! st :int)] + (when (some (fn [c] (some #(= ty (if (symbol? %) (symbol (name %)) %)) + (get-in tenv [ty :ctors c :fields]))) + ctors) + (give-up! (str "the recursive data type " ty))) + (swap! facts conj [:<= 0 tag (dec (count ctors))]) + (union-of st (map-indexed + (fn [i c] + [[:= tag i] + {:vec (into [{:const (code! st (keyword (str c)))}] + (map #(var-value st facts % tenv v) + (get-in tenv [ty :ctors c :fields])))}]) + ctors))) + :else (give-up! (str "a variable `" v "` of type " (pr-str ty)))))) + +(defn- elems + "The values of an element list, or give up when its length is unknown." + [st env e] + (case (head e) + :enil [] + :econs (into [(ev st env (nth e 1))] (elems st env (nth e 2))) + :eapp (into (elems st env (nth e 1)) (elems st env (nth e 2))) + :elems (let [v (ev st env (second e))] + (cond (:vec v) (:vec v) + (:nil v) [] + :else (give-up! "the elements of a value of unknown length"))) + (give-up! "an element list of unknown length"))) + +(defn- seq-of + "The elements of a seqable value, as a vector of values; nil has none, + and a number, keyword or boolean is not seqable, so Clojure throws." + [v] + (cond (:vec v) (:vec v) + (:nil v) [] + (:set v) (give-up! "the order of a set's elements") + (:fn v) (throws!) + :else (throws!))) + +(defn- compare-int [op a b] + [op (int-of a) (int-of b)]) + +(defn- fold + "An integer term with its literal parts computed: [:+ 1 2] is 3." + [t] + (if (vector? t) + (let [[op & xs] t + xs (map #(if (keyword? %) % (fold %)) xs)] + (if (and (contains? #{:+ :- :* :neg :quot :mod :abs :max :min} op) (every? integer? xs)) + (case op + :+ (apply + xs) :- (apply - xs) :* (apply * xs) :neg (- (first xs)) + :quot (quot (first xs) (second xs)) :mod (mod (first xs) (second xs)) + :abs (abs (first xs)) :max (apply max xs) :min (apply min xs)) + (into [op] xs))) + t)) + +(defn- concrete + "The Clojure value of a symbolic value made only of literals, or ::none." + [st v] + (let [by-code (into {} (map (fn [[c k]] [k c])) (:codes @st))] + ((fn walk [v] + (cond + (and (contains? v :int) (integer? (:int v))) (:int v) + (and (contains? v :bool) (boolean? (:bool v))) (:bool v) + (and (contains? v :const) (contains? by-code (:const v))) (by-code (:const v)) + (:nil v) nil + (:vec v) (let [xs (mapv walk (:vec v))] (if (some #{::none} xs) ::none (apply list xs))) + (and (:set v) (:elems (:set v)) (every? (comp true? first) (:elems (:set v)))) + (let [xs (mapv (comp walk second) (:elems (:set v)))] (if (some #{::none} xs) ::none (set xs))) + :else ::none)) + v))) + +(defn- from-concrete + "The symbolic value of a plain Clojure value, or nil." + [st x] + (cond (sequential? x) (let [vs (map #(from-concrete st %) x)] (when (every? some? vs) {:vec (vec vs)})) + (set? x) (let [vs (map #(from-concrete st %) x)] + (when (every? some? vs) (finite-set st (map (fn [v] [true v]) vs) true))) + (or (map? x) (fn? x)) nil + :else (try (lit-value st x) (catch clojure.lang.ExceptionInfo _ nil)))) + +(def ^:private pure-fns + '#{sort distinct reverse sort-by str name keyword subs frequencies last butlast take drop count}) + +(defn- core + "A clojure.core fn applied to values." + [st f args] + (if-let [v (and (contains? pure-fns f) + (let [xs (map #(concrete st %) args)] + (when (not-any? #{::none} xs) + (try (let [r (apply @(resolve (symbol "clojure.core" (name f))) xs)] + (from-concrete st (if (seq? r) (doall r) r))) + (catch Throwable _ nil)))))] + v + (core* st f args))) + +(defn- core* + "A clojure.core fn applied to values." + [st f args] + (let [[a b c] args + n (count args) + num (fn [g] (lift st (fn [x] {:int (g (int-of x))}) a)) + num2 (fn [g] (lift2 st (fn [x y] {:int (g (int-of x) (int-of y))}) a b))] + (case f + + (reduce (fn [acc x] (lift2 st (fn [p q] {:int [:+ (int-of p) (int-of q)]}) acc x)) {:int 0} args) + - (if (= 1 n) + (num (fn [x] [:neg x])) + (reduce (fn [acc x] (lift2 st (fn [p q] {:int [:- (int-of p) (int-of q)]}) acc x)) a (rest args))) + * (reduce (fn [acc x] + (lift2 st (fn [p q] + (let [s (fold (int-of p)) u (fold (int-of q))] + (cond (integer? s) {:int [:* s u]} + (integer? u) {:int [:* u s]} + :else (give-up! "a product of two unknowns")))) + acc x)) + {:int 1} args) + inc (num (fn [x] [:+ x 1])) + dec (num (fn [x] [:- x 1])) + (quot mod rem) (lift2 st (fn [x y] + (let [k (int-of y)] + (when-not (and (integer? k) (not (zero? k))) + (give-up! (str f " by a value that is not a literal"))) + {:int (case f + quot [:quot (int-of x) k] + mod [:mod (int-of x) k] + rem [:- (int-of x) [:* k [:quot (int-of x) k]]])})) + a b) + abs (num (fn [x] [:abs x])) + bit-shift-left + (lift2 st (fn [x k] + (let [xv (fold (int-of x)) kv (fold (int-of k))] + (cond + (and (integer? xv) (integer? kv) (<= 0 kv 62)) {:int (bit-shift-left xv kv)} + :else + ;; x times 2^k for each k a shift can be; anything else + ;; is a value the solver may choose, which proves less + (let [other (fresh! st :int) + [lo hi] (interval st kv) + js (range (max 0 (or lo 0)) (inc (min 62 (or hi 62))))] + {:int (reduce (fn [acc j] [:ite (define! st :bool [:= kv j]) [:* (bit-shift-left 1 j) xv] acc]) + other (reverse js))})))) + a b) + max (reduce (fn [acc x] (lift2 st (fn [p q] {:int [:max (int-of p) (int-of q)]}) acc x)) a (rest args)) + min (reduce (fn [acc x] (lift2 st (fn [p q] {:int [:min (int-of p) (int-of q)]}) acc x)) a (rest args)) + (< <= > >=) (if (= 1 n) + {:bool true} + {:bool (reduce conj-f true + (map (fn [x y] (truth (lift2 st (fn [p q] {:bool (compare-int (keyword (name f)) p q)}) x y))) + args (rest args)))}) + = (if (= 1 n) + {:bool true} + {:bool (reduce conj-f true + (map (fn [x y] (truth (lift2 st (fn [p q] {:bool (equal st p q)}) x y))) + args (rest args)))}) + not= {:bool [:not (truth (core st '= args))]} + not {:bool [:not (truth a)]} + boolean {:bool (truth a)} + zero? (lift st (fn [x] {:bool [:= (int-of x) 0]}) a) + pos? (lift st (fn [x] {:bool [:> (int-of x) 0]}) a) + neg? (lift st (fn [x] {:bool [:< (int-of x) 0]}) a) + identity a + hash-set (finite-set st (map (fn [x] [true x]) args) true) + set (lift st (fn [x] (cond (:set x) {:set (assoc (:set x) :distinct true)} + :else (finite-set st (map (fn [e] [true e]) (seq-of x)) true))) + a) + contains? (lift2 st (fn [sv x] + (if (:set sv) {:bool ((:mem (:set sv)) x)} (give-up! "contains? on a value that is not a set"))) + a b) + into (lift2 st (fn [x y] + (when-not (:set x) (give-up! "into a value that is not a set")) + (let [sy (if (:set y) (:set y) (:set (finite-set st (map (fn [e] [true e]) (seq-of y)) false))) + sx (:set x)] + {:set {:mem (fn [e] [:or ((:mem sx) e) ((:mem sy) e)]) + :elems (when (and (:elems sx) (:elems sy)) (into (:elems sx) (:elems sy))) + :distinct true + :elem (or (:elem sx) (:elem sy))}})) + a b) + filter (lift st (fn [xs] + (let [keep? (fn [e] (truth (apply-fn st a [e]))) + sx (cond (:set xs) (:set xs) + ;; a seq of known length, filtered: which + ;; elements stay depends on the tests + (:vec xs) (:set (finite-set st (map (fn [e] [true e]) (:vec xs)) false)) + :else (seq-of xs))] + {:set {:mem (fn [e] [:and ((:mem sx) e) (keep? e)]) + :elems (when (:elems sx) (vec (for [[g v] (:elems sx)] [(conj-f g (keep? v)) v]))) + :distinct (:distinct sx) + :elem (:elem sx)}})) + b) + (map mapcat) (lift st (fn [xs] + (cond + (:vec xs) (if (= 'map f) + {:vec (mapv #(apply-fn st a [%]) (:vec xs))} + {:vec (vec (mapcat #(seq-of (apply-fn st a [%])) (:vec xs)))}) + (:set xs) (image st f a (:set xs)) + :else (seq-of xs))) + b) + (list vector) {:vec (vec args)} + vec (lift st (fn [x] {:vec (seq-of x)}) a) + first (lift st (fn [x] (or (first (seq-of x)) {:nil true})) a) + second (lift st (fn [x] (or (second (seq-of x)) {:nil true})) a) + rest (lift st (fn [x] {:vec (vec (rest (seq-of x)))}) a) + next (lift st (fn [x] (let [r (vec (rest (seq-of x)))] (if (seq r) {:vec r} {:nil true}))) a) + seq (lift st (fn [x] (if (seq (seq-of x)) {:vec (seq-of x)} {:nil true})) a) + empty? (lift st (fn [x] + (if (:set x) + (let [es (or (:elems (:set x)) (give-up! "whether a set of unknown size is empty"))] + {:bool [:not (into [:or false] (map first es))]}) + {:bool (empty? (seq-of x))})) + a) + count (lift st (fn [x] + (if (:set x) + (let [{:keys [elems distinct]} (:set x)] + (when-not elems (give-up! "the count of a set of unknown size")) + {:int (into [:+ 0] + (map-indexed + (fn [i [g v]] + [:ite (if distinct + (conj-f g [:not (member-of st (take i elems) v)]) + g) + 1 0]) + elems))}) + {:int (count (seq-of x))})) + a) + cons (lift2 st (fn [x ys] {:vec (into [x] (seq-of ys))}) a b) + concat {:vec (vec (mapcat (fn [x] (let [v (lift st identity x)] (seq-of v))) args))} + nth (lift2 st (fn [x i] + (let [k (int-of i) + xs (seq-of x) + past (if (= 3 n) c :bottom)] + (if (integer? k) + (cond (< -1 k (count xs)) (nth xs k) + (= 3 n) c + :else (throws!)) + ;; an unknown index: each position, under k = j + (do (when-not (= 3 n) + (record-throw! st [:not (into [:or false] (for [j (range (count xs))] [:= k j]))])) + (reduce (fn [acc j] (merge-values st (define! st :bool [:= k j]) (nth xs j) acc)) + past (reverse (range (count xs)))))))) + a b) + (give-up! (str "`" f "`"))))) + +(defn- folded + "v with each integer term in it folded." + [v] + (cond (= :bottom v) v + (:union v) {:union (mapv (fn [[g x]] [g (folded x)]) (:union v))} + (contains? v :int) {:int (fold (:int v))} + (:vec v) {:vec (mapv folded (:vec v))} + :else v)) + +(defn- app + "A defn of the target or the spec applied to values: its body, run on + them. Recursion is outside." + [st f vs] + (let [d (get-in @st [:defs-of f])] + (when (or (nil? d) (:recursive? d) (:outside d)) + (give-up! (str "the call of `" f "`"))) + (swap! st update :used (fnil conj #{}) f) + (let [k [f vs] + [r tau] (or (get-in @st [:memo k]) + ;; the body on a path of its own: what it throws on is + ;; noted once, and at each call under the call's path + (let [{:keys [path throws]} @st + _ (swap! st assoc :path [] :throws []) + r (ev st (zipmap (:params d) vs) (:body d)) + tau (let [ts (:throws @st)] (if (seq ts) (into [:or false] ts) false))] + (swap! st assoc :path path :throws throws) + (swap! st assoc-in [:memo k] [r tau]) + [r tau]))] + (record-throw! st tau) + r))) + +(defn- apply-fn [st fv vs] + (if (:fn fv) + ((:fn fv) vs) + (give-up! "applying a value that is not a fn"))) + +;; --- images of sets -------------------------------------------------------------- + +(defn- lin + "{:c n :m {atom k}} for a linear solver term, or nil." + [t] + (cond + (integer? t) {:c t :m {}} + (symbol? t) {:c 0 :m {t 1}} + (and (vector? t) (= :+ (first t))) (reduce (fn [a b] (when (and a b) {:c (+ (:c a) (:c b)) :m (merge-with + (:m a) (:m b))})) + {:c 0 :m {}} (map lin (rest t))) + (and (vector? t) (= :- (first t))) + (let [[x & ys] (map lin (rest t))] + (when (and x (every? some? ys)) + (if (empty? ys) + {:c (- (:c x)) :m (into {} (map (fn [[k v]] [k (- v)])) (:m x))} + (reduce (fn [a b] {:c (- (:c a) (:c b)) :m (merge-with + (:m a) (into {} (map (fn [[k v]] [k (- v)])) (:m b)))}) + x ys)))) + (and (vector? t) (= :neg (first t))) (when-let [x (lin (second t))] + {:c (- (:c x)) :m (into {} (map (fn [[k v]] [k (- v)])) (:m x))}) + (and (vector? t) (= :* (first t)) (integer? (second t))) + (when-let [x (lin (nth t 2))] + (let [k (second t)] {:c (* k (:c x)) :m (into {} (map (fn [[a v]] [a (* k v)])) (:m x))})) + :else {:c 0 :m {t 1}})) + +(defn- mentions? [t syms] + (boolean (some syms (tree-seq coll? seq t)))) + +(defn- offset + "Term r is e plus a term free of the element's variables es: that term, + or nil." + [r e es] + (when-let [{:keys [c m]} (lin r)] + (when (and (= 1 (get m e)) (not-any? #(mentions? % es) (keys (dissoc m e)))) + (into [:+ c] (for [[a k] (dissoc m e) :when (not (zero? k))] [:* k a]))))) + +(defn- rebuild + "A value shaped like v whose parts are the terms ts, in order." + [v ts] + (let [ts (atom ts) + take! (fn [] (let [t (first @ts)] (swap! ts rest) t))] + ((fn walk [x] + (cond (contains? x :int) {:int (take!)} + (contains? x :const) {:const (take!)} + (:vec x) {:vec (mapv walk (:vec x))} + :else x)) + v))) + +(defn- substitute + "Formula f with symbols replaced by terms, as m says." + [f m] + (cond (symbol? f) (get m f f) + (vector? f) (mapv #(substitute % m) f) + :else f)) + +(defn- image + "The image of a set of unknown size under fn value f (map), or the + union of f's results (mapcat). f is run once on an element of fresh + variables; each result must be that element plus fixed offsets, so an + x is in the image when x minus an offset is in the set." + [st kind fv sx] + (if (:elems sx) + (let [out (for [[g v] (:elems sx) + :let [r (apply-fn st fv [v])] + [h w] (if (= 'map kind) [[true r]] (or (:elems (:set r)) (map (fn [e] [true e]) (seq-of r))))] + [(conj-f g h) w])] + (finite-set st out false)) + (let [e (fresh-like st (or (:elem sx) (give-up! "the image of a set of no known elements"))) + es (set (flat e)) + ndefs (count (:defs @st)) + r (apply-fn st fv [e]) + parts (if (= 'map kind) [[true r]] (or (:elems (:set r)) (map (fn [x] [true x]) (seq-of r)))) + _ (when (not= ndefs (count (:defs @st))) + (give-up! "an image under a fn with tests")) + inverses (vec (for [[g w] parts] + (let [ws (flat w) ecs (flat e)] + (when-not (and ws (= (count ws) (count ecs))) + (give-up! "an image that is not the element moved")) + (let [offs (mapv #(or (offset %1 %2 es) (give-up! "an image that is not a translation")) + ws ecs)] + [g offs]))))] + {:set {:mem (fn [x] + (if-let [xs (flat x)] + (into [:or false] + (for [[g offs] inverses + :let [pre (mapv (fn [xi o] [:- xi o]) xs offs) + sub (zipmap (flat e) pre) + back (rebuild e pre)]] + (conj-f (substitute g sub) ((:mem sx) back)))) + false)) + :distinct false + :elem e}}))) + +(defn ev + "The value of term x under env, symbol -> value." + [st env x] + (cond + (symbol? x) (or (get env x) (give-up! (str "the unbound `" x "`"))) + :else + (case (head x) + :nil {:nil true} + :lit (lit-value st (second x)) + :sq {:vec (elems st env (second x))} + :if (let [c (truth (ev st env (nth x 1))) + c (if (or (boolean? c) (symbol? c)) c (define! st :bool c))] + (cond + ;; a test known either way: only its branch runs, as in Clojure + (true? c) (ev st env (nth x 2)) + (false? c) (ev st env (nth x 3)) + ;; each branch is evaluated on its own path, so a throw in it + ;; counts only when the test takes it there + :else (merge-values st c + (on-path st c #(ev st env (nth x 2))) + (on-path st [:not c] #(ev st env (nth x 3)))))) + :call (folded (core st (second x) (mapv #(ev st env %) (drop 2 x)))) + :app (let [[_ f & args] x] (app st f (mapv #(ev st env %) args))) + :fn (let [[_ ps body] x] + {:fn (fn [vs] (ev st (merge env (zipmap ps vs)) body))}) + :cfn (let [f (second x)] {:fn (fn [vs] (folded (core st f vs)))}) + :dfn (let [f (second x)] {:fn (fn [vs] (app st f vs))}) + :ap (let [[_ f & args] x] + (apply-fn st (ev st env f) (mapv #(ev st env %) args))) + :lin (folded {:int (into [:+ (second x)] (for [[a k] (nth x 2)] [:* k (int-of (ev st env a))]))}) + :le {:bool [:<= 0 (int-of (ev st env (second x)))]} + :ieq {:bool [:= 0 (int-of (ev st env (second x)))]} + :bottom (do (record-throw! st true) :bottom) + (give-up! (str "the term " (pr-str (t/show x))))))) + +;; --- goals ------------------------------------------------------------------------ + +(defn formula + "{:formula :decls} saying that under hyps, goal g is truthy, for every + value of the typed variables -- and, when opts has :total, that its + evaluation never throws; nil when some part is outside." + [{:keys [types defs tenv total]} hyps g] + (try + (let [st (state) + facts (atom []) + _ (swap! st assoc :defs-of defs) + occurs (reduce into (t/vars g) (map t/vars hyps)) + env (into {} (for [v (sort-by str (keys types)) :when (contains? occurs v)] + [v (var-value st facts (get types v) tenv v)])) + hs (mapv #(truth (ev st env %)) hyps) + ;; only what the goal throws on counts: a hypothesis that throws + ;; is one the law does not assume + _ (swap! st assoc :throws []) + goal (truth (ev st env g)) + throws (into [:or false] (:throws @st)) + goal (if total [:and [:not throws] goal] goal)] + {:formula [:=> (into [:and true] (concat @facts (:defs @st) hs)) goal] + :decls (:decls @st) + :used (or (:used @st) #{}) + :env env + :codes (:codes @st) + :throws throws}) + (catch clojure.lang.ExceptionInfo e + (cond + (::outside (ex-data e)) (do (when *why* (swap! *why* conj (ex-message e))) nil) + ;; a throw outside any alternative: give the goal back + (::throws (ex-data e)) nil + :else (throw e))))) + +(defn- pin + "The formula saying symbolic value v is the concrete value x." + [st v x] + (cond + (= :bottom v) false + (:union v) (into [:or] (for [[g a] (:union v)] (conj-f g (pin st a x)))) + (contains? v :int) (if (integer? x) [:= (:int v) x] false) + (contains? v :bool) (if (boolean? x) (if x (:bool v) [:not (:bool v)]) false) + (contains? v :const) (if (const? x) [:= (:const v) (code! st x)] false) + (:nil v) (nil? x) + (:vec v) (if (and (sequential? x) (= (count x) (count (:vec v)))) + (reduce conj-f true (map #(pin st %1 %2) (:vec v) x)) + false) + :else false)) + +(defn agrees? + "Does the formula for term g agree with running it, at the concrete + values of its variables in env? For testing the evaluator: with the + variables pinned to those values, the formula must say g is truthy + exactly when it is. :outside when the evaluation gives up." + [{:keys [types defs tenv]} g env] + (try + (let [st (state) + facts (atom []) + _ (swap! st assoc :defs-of defs) + vals (into {} (for [v (sort-by str (keys types))] + [v (var-value st facts (get types v) tenv v)])) + goal (truth (ev st vals g)) + actual (try (boolean (t/evaluate g env)) (catch Throwable _ ::threw)) + pins (reduce conj-f true (for [[v x] env] (pin st (get vals v) x))) + f [:=> (into [:and true pins] (concat @facts (:defs @st))) + (if (= ::threw actual) true [:iff goal actual])]] + (= :valid (:result (solve/valid? f (:decls @st) {:budget 20000})))) + (catch clojure.lang.ExceptionInfo e + (if (::outside (ex-data e)) :outside (throw e))))) + +(defn throws-agree? + "Does the throw condition for term g agree with running it, at the + concrete values in env? For testing the evaluator, like agrees?." + [{:keys [types defs tenv]} g env] + (try + (let [st (state) + facts (atom []) + _ (swap! st assoc :defs-of defs) + vals (into {} (for [v (sort-by str (keys types))] + [v (var-value st facts (get types v) tenv v)])) + _ (ev st vals g) + throws (into [:or false] (:throws @st)) + threw (try (t/evaluate g env) false (catch Throwable _ true)) + pins (reduce conj-f true (for [[v x] env] (pin st (get vals v) x))) + f [:=> (into [:and true pins] (concat @facts (:defs @st))) [:iff throws threw]]] + (= :valid (:result (solve/valid? f (:decls @st) {:budget 20000})))) + (catch clojure.lang.ExceptionInfo e + (if (::outside (ex-data e)) :outside (throw e))))) + +(def budget + "Decisions the solver may make on a goal evaluated whole." + 20000) + +(defn- decode + "The Clojure value symbolic value v takes in the solver's model, or + ::none when it has none there (a throw, a set with no end)." + [v model decoded-code] + (let [dec #(decode % model decoded-code) + int-at (fn [t] (if (integer? t) t (solve/eval-term t model)))] + (cond + (= :bottom v) ::none + (:union v) (if-let [[_ x] (first (filter #(solve/eval-formula (first %) model) (:union v)))] + (dec x) + ::none) + (contains? v :int) (int-at (:int v)) + (contains? v :bool) (let [b (:bool v)] (if (boolean? b) b (solve/eval-formula b model))) + (contains? v :const) (decoded-code (int-at (:const v))) + (:nil v) nil + (:vec v) (let [xs (mapv dec (:vec v))] (if (some #{::none} xs) ::none xs)) + (:set v) (let [{:keys [pred elem]} (:set v) + {m :map d :default} (get model pred)] + (if (or (nil? pred) d) + ::none + (set (for [[args in?] m :when in?] + (dec (rebuild elem args)))))) + :else ::none))) + +(defn counterexample + "Values of the variables for which hyps hold and goal g does not, from + the solver's counter-model, or nil." + [opts hyps g] + (when-let [{:keys [formula decls env codes]} (formula opts hyps g)] + (let [r (try (solve/valid? formula decls {:budget budget}) + (catch clojure.lang.ExceptionInfo _ nil))] + (when (= :invalid (:result r)) + (let [by-code (into {} (map (fn [[c k]] [k c])) codes) + decoded-code (fn [k] (get by-code k (keyword (str "k" (abs k))))) + values (into {} (for [[v sv] env] [v (decode sv (:model r) decoded-code)]))] + (when-not (some #{::none} (vals values)) + values)))))) + +(defn prove + "[certificate fns-it-unfolded] proving goal g holds under hyps, or nil." + [opts hyps g] + (when-let [{:keys [formula decls used]} (formula opts hyps g)] + (let [r (try (solve/valid? formula decls {:budget budget}) + (catch clojure.lang.ExceptionInfo _ nil))] + (when (and *why* (not= :valid (:result r))) + (swap! *why* conj (str "solver: " (:result r) " " (pr-str (select-keys r [:reason :model]))))) + (when (= :valid (:result r)) [(:certificate r) used])))) + +(defn verify + "Does certificate c prove goal g under hyps?" + [opts hyps g c] + (if-let [{:keys [formula decls]} (formula opts hyps g)] + (try (solve/verify formula decls c) + (catch clojure.lang.ExceptionInfo _ false)) + false)) diff --git a/src/writ/prove/term.clj b/src/writ/prove/term.clj index e76e9d4..7984769 100644 --- a/src/writ/prove/term.clj +++ b/src/writ/prove/term.clj @@ -18,6 +18,7 @@ [:app f a ...] a fn of the target or the spec applied [:fn [p ...] body] a fn value [:cfn f] the clojure.core fn f, as a value + [:dfn f] the target's or the spec's fn f, as a value [:ap f a ...] a fn value applied [:if c a b] Clojure's if: b when c is nil or false [:lin c [[t k] ...]] the integer c + k*t + ... @@ -62,7 +63,7 @@ (not (vector? t)) #{} (= :fn (head t)) (let [[_ ps body] t] (apply disj (vars body) ps)) (= :lin (head t)) (into #{} (mapcat (fn [[a _]] (vars a))) (nth t 2)) - (contains? #{:lit :cfn} (head t)) #{} + (contains? #{:lit :cfn :dfn} (head t)) #{} ;; a call's head is the name of a fn, not a variable (contains? #{:call :app} (head t)) (into #{} (mapcat vars) (drop 2 t)) :else (into #{} (mapcat vars) (rest t)))) @@ -76,7 +77,7 @@ (cond (symbol? t) (get m t t) (not (vector? t)) t - (contains? #{:lit :nil :enil :bottom :cfn} (head t)) t + (contains? #{:lit :nil :enil :bottom :cfn :dfn} (head t)) t (= :fn (head t)) (let [[_ ps body] t m* (apply dissoc m ps) free (into #{} (comp (filter #(contains? (vars body) (key %))) @@ -92,7 +93,7 @@ :else (into [(first t)] (map #(subst % m)) (rest t)))) (defn subterms [t] - (tree-seq (fn [x] (and (vector? x) (not (lit? x)) (not= :cfn (head x)))) + (tree-seq (fn [x] (and (vector? x) (not (lit? x)) (not (contains? #{:cfn :dfn} (head x))))) (fn [x] (case (head x) :lin (map first (nth x 2)) (:call :app) (drop 2 x) @@ -133,6 +134,7 @@ :fn (let [[_ ps body] t] (fn [& args] (evaluate body (merge env (zipmap ps args)) res))) :cfn @(resolve (symbol "clojure.core" (name (second t)))) + :dfn @(res (second t)) :ap (apply (ev (second t)) (map ev (drop 2 t))) :if (if (ev (nth t 1)) (ev (nth t 2)) (ev (nth t 3))) :lin (reduce + (second t) (map (fn [[a k]] (* k (ev a))) (nth t 2))) @@ -177,6 +179,7 @@ :app (apply list (symbol (name (second t))) (map show (drop 2 t))) :fn (list 'fn (nth t 1) (show (nth t 2))) :cfn (second t) + :dfn (symbol (name (second t))) :ap (apply list (show (second t)) (map show (drop 2 t))) :if (list 'if (show (nth t 1)) (show (nth t 2)) (show (nth t 3))) :lin (let [[p n] (show-lin (second t) (nth t 2))] diff --git a/src/writ/prove/translate.clj b/src/writ/prove/translate.clj index c59d70a..6d6c570 100644 --- a/src/writ/prove/translate.clj +++ b/src/writ/prove/translate.clj @@ -15,7 +15,9 @@ "The clojure.core fns the prover models." '#{seq first rest next second empty? count cons list vector vec concat filter map not = not= < <= > >= + - * inc dec zero? pos? neg? nth identity apply - reduce integer? max min abs every? some quot mod rem contains? boolean}) + reduce integer? max min abs every? some quot mod rem contains? boolean + bit-shift-left bit-shift-right set hash-set into mapcat + sort distinct reverse last butlast take drop str name keyword}) (def value-fns "The clojure.core fns that may be passed as values: the modelled ones, @@ -32,9 +34,16 @@ (defn- scalar? [x] (or (nil? x) (number? x) (string? x) (keyword? x) (char? x) (boolean? x))) +(defn- plain-data? + "A scalar, or a sequential of plain data, or a set of scalars." + [x] + (or (scalar? x) + (and (sequential? x) (every? plain-data? x)) + (and (set? x) (every? scalar? x)))) + (defn- constant "The value of a def the name refers to, when it is plain data the prover - can hold: a scalar, or a sequential or set of them. Code is pure, so a + can hold: a scalar, a sequential of plain data, or a set of scalars. Code is pure, so a def's value is fixed once its namespace is loaded; nil otherwise." [ctx s] (let [v (try (if (namespace s) @@ -43,8 +52,7 @@ (catch Throwable _ nil))] (when (and (var? v) (bound? v) (not (:dynamic (meta v)))) (let [x @v] - (when (or (scalar? x) - (and (or (sequential? x) (set? x)) (every? scalar? x))) + (when (plain-data? x) [x]))))) (defn- member-set @@ -91,9 +99,7 @@ (case k :local (into [:ap v] args) :own (into [:app v] args) - :core (if (= 'contains? v) - (outside! "contains? on anything but a set of literals") - (into [:call v] args)) + :core (into [:call v] args) (outside! (str "`" (:name f) "`")))) :fn (into [:ap (term-of ctx env f)] args) (outside! "calling a computed value"))) @@ -106,6 +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))) (coll? v) (outside! (str "the literal " (pr-str v))) :else [:lit v])) :ref (let [s (:name ast)] @@ -114,11 +121,12 @@ (contains? #{nil "clojure.core"} (namespace s)) (contains? value-fns (symbol (name s)))) [:cfn (symbol (name s))] - (or (contains? (:own ctx) s) (call-head ctx env s)) + (contains? (:own ctx) s) [:dfn (get (:own ctx) s)] + (call-head ctx env s) (outside! (str "`" s "` passed as a value")) :else (if-let [[x] (constant ctx s)] (if (set? x) - (outside! (str "the set `" s "` outside contains?")) + (into [:call 'hash-set] (map t/lit (sort-by pr-str 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))] @@ -168,6 +176,7 @@ (invoke-term ctx env f (mapv #(term-of ctx env %) (:args ast))))) :vec (t/seq-term (mapv #(term-of ctx env %) (:items ast))) + :set (into [:call 'hash-set] (map #(term-of ctx env %) (:items ast))) :case (case-term ctx env ast) (outside! (str "`" (name (:op ast)) "`")))) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index ec09337..107b515 100644 --- a/src/writ/spec.clj +++ b/src/writ/spec.clj @@ -38,7 +38,9 @@ `instrument` wraps the target's fns with the signatures' runtime checks, and `scan` says which of a namespace's fns writ could check at all." - (:require [clojure.java.io :as io] + (:require [clojure.edn :as edn] + [clojure.java.io :as io] + [clojure.set :as set] [clojure.string :as str] [writ.book :as book] [writ.check :as ck] @@ -76,6 +78,18 @@ (fail! "`ann " nm "` must end in `-> ReturnType`, had: " (pr-str sig))) {:params (vec ps) :ret (first rs)})) +(def proofs + "proof ns name -> {:proves spec-ns :lemmas [lemma] :hints {law hint}}" + (atom {})) + +(defn -register-proof! [proof-ns k v] + (swap! proofs update proof-ns + (fn [e] (case k + :proves {:proves v :lemmas [] :hints {}} + :lemma (update e :lemmas conj v) + :hint (assoc-in e [:hints (first v)] (second v))))) + nil) + (defn -register! [spec-ns k v] (swap! registry update spec-ns (fn [e] (case k @@ -250,6 +264,60 @@ (doseq [f (:final m)] (known! ":final" f))) `(-register! '~(ns-name *ns*) :graph '~[nm m]))) +(def ^:private strategies #{:symbolic :induction :rewriting}) + +(defmacro proof-of + "Name the spec this namespace proves. A proof namespace holds what the + prover needs and the spec should not say: lemmas and hints. The agent + writes it; the spec stays the contract. writ finds it by name, my.sort-proof + for my.sort-spec, or by check's :proof option." + [spec-ns] + (when-not (simple-sym? spec-ns) + (fail! "`proof-of` names a spec namespace symbol, had: `" (pr-str spec-ns) "`")) + `(-register-proof! '~(ns-name *ns*) :proves '~spec-ns)) + +(defmacro lemma + "A law about the code that helps prove the spec's laws: + + (lemma insert-keeps-sorted + (forall [x Nat, xs (List Nat)] (=> (ascending? xs) (ascending? (insert x xs))))) + + It is tested and must be proved, like a law the spec demands proof of; + once proved, the spec's laws may cite it. It is not part of the spec: + it counts toward no law, and no stand-in is judged by it." + [nm prop] + (when-not (simple-sym? nm) + (fail! "a `lemma` name must be a simple symbol: `" (pr-str nm) "`")) + `(-register-proof! '~(ns-name *ns*) :lemma '~{:name nm :prop prop})) + +(defmacro hint + "Tell the prover how to prove one of the spec's laws (or a lemma): + + (hint sorted {:induct xs :use [insert-keeps-sorted]}) + + :induct, the variable to try induction on first; :use, the only lemmas + and laws the proof may cite; :strategy, one of :symbolic (run the code + on symbolic values), :induction or :rewriting; :fuel, the rewrites one + attempt may make. A hint only steers the search: a proof it finds is + checked like any other." + [law-name m] + (let [where (str "`hint " law-name "`")] + (when-not (simple-sym? law-name) + (fail! "a `hint` names a law by its simple symbol, had: `" (pr-str law-name) "`")) + (when-not (map? m) + (fail! where " takes a map: {:induct x :use [lemma ...] :strategy :symbolic :fuel n}")) + (when-let [bad (seq (remove #{:induct :use :strategy :fuel} (keys m)))] + (fail! where " has unknown keys: " (pr-str bad) "; it takes :induct :use :strategy :fuel")) + (when (and (contains? m :strategy) (not (contains? strategies (:strategy m)))) + (fail! where ": :strategy must be one of " (pr-str (sort strategies)) ", had " (pr-str (:strategy m)))) + (when (and (contains? m :induct) (not (simple-sym? (:induct m)))) + (fail! where ": :induct names a variable of the law")) + (when (and (contains? m :use) (not (and (vector? (:use m)) (every? simple-sym? (:use m))))) + (fail! where ": :use is a vector of lemma and law names")) + (when (and (contains? m :fuel) (not (pos-int? (:fuel m)))) + (fail! where ": :fuel is a positive integer")) + `(-register-proof! '~(ns-name *ns*) :hint '~[law-name m]))) + (defn- law-opts! "Check a law's options: :require sets the evidence it needs, and :require :tested needs :because, the reason it cannot be proved yet." @@ -876,7 +944,7 @@ (when doc [doc]) (when attrs [attrs]) [params*] body)))))) -(declare erase refines-of) +(declare erase erase-data refines-of) (defn- static-check "Run writ's rules over the target's source with the spec's types, each @@ -893,7 +961,7 @@ missing (remove #(contains? defns %) (sort (keys anns))) refs (refines-of e) anns (into {} (map (fn [[k sig]] [k (erase sig refs)])) anns) - data (mapv #(erase % refs) data)] + data (mapv #(erase-data % refs) data)] (when (seq missing) (fail! "the spec gives `" (first missing) "` a signature, but `" target "` defines no fn `" (first missing) "`")) @@ -1213,7 +1281,7 @@ [[gname m :as g] refs] (vec (for [{:keys [from f args tos]} (graph-edges g) :let [ty #(get (:states m) %) - ref-of #(get refs (symbol (name (plain (ty %)))))] + ref-of #(let [t (plain (ty %))] (when (symbol? t) (get refs t)))] :when (every? ref-of tos)] (let [v (or (:var (ref-of from)) 's) avs (reduce (fn [acc [i t]] (conj acc (arg-var t i (set (conj acc v))))) @@ -1225,7 +1293,8 @@ (cons 'or (map #(list (:pred-name (ref-of %)) nxt) tos)))) :explain (str "a " f " from " (name from) " must land in " (str/join " or " (map name tos))) - :graph gname})))) + :graph gname + :total true})))) (defn- fits? "Does a value of type `a` fit where type `b` is expected?" @@ -1285,10 +1354,11 @@ (defn- graph-start-errors "A [state value] start: the value, run once, must be in its state." - [[gname m] spec-ns tenv] + [[gname m] spec-ns tenv qualify-form] (let [st (:start m)] (when (vector? st) (let [[s expr] st + expr (qualify-form expr) t (get (:states m) s) v (try {:ok (binding [*ns* (the-ns spec-ns)] (eval expr))} (catch Throwable ex {:thrown (ex-message ex)}))] @@ -1365,6 +1435,16 @@ (map? t) (into {} (map (fn [[k v]] [k (erase v refines)])) t) :else t)) +(defn- erase-data + "A data form with refinements in its field types erased; the type's and + constructors' own names are left as they are." + [f refs] + (let [[h nm & more] f + [params ctors] (if (vector? (first more)) [(first more) (rest more)] [nil more])] + (apply list (concat [h nm] (when params [params]) + (for [c ctors] + (if (seq? c) (apply list (first c) (map #(erase % refs) (rest c))) c)))))) + (defn- guard "The form saying value `x` meets the refinements inside type `t`, or nil when `t` has none." @@ -1434,24 +1514,40 @@ (fail! "refinement `" name "` has no value between " (- int-window) " and " int-window) (or (= (first ok) (- int-window)) (= (peek ok) int-window)) (gen/such-that pred (type->gen b tenv) 200) - (= (count ok) (inc (- (peek ok) (first ok)))) - (gen/choose (first ok) (peek ok)) - :else (gen/elements ok))) + :else + (let [lo (first ok) hi (peek ok) + spread (if (= (count ok) (inc (- hi lo))) + ;; near either bound first, as test.check's sizes + ;; grow: the edges of a range are where code breaks + (gen/sized (fn [size] + (gen/one-of [(gen/choose lo (min hi (+ lo size))) + (gen/choose (max lo (- hi size)) hi)]))) + (gen/elements ok)) + ;; the bounds, and the spec's own numbers, where the code + ;; decides things: a wall, a paddle's column, a cap + ok-set (set ok) + edges (vec (sort (filter ok-set (concat [(first ok) (peek ok)] + (get-in tenv [::spec-ints] [])))))] + (gen/frequency [[3 spread] [1 (gen/elements edges)]])))) (gen/such-that pred (type->gen base (assoc tenv ::bias (::bias-of-refine tenv))) 200)))) (defn- type-env-of "The data types and refinements of a spec entry. Refinements sit under ::refines, apart from the data the prover and the static check read." - [{:keys [data refines]} spec-ns] + [{:keys [data refines laws]} spec-ns] (let [bodies (delay (into {} (for [f (book/read-forms (source-url spec-ns)) :when (and (seq? f) (contains? '#{defn defn-} (first f)))] - [(second f) f])))] + [(second f) f]))) + spec-ints (delay (let [ns (filter integer? (literals (concat (map :prop laws) (map :pred refines) + (vals @bodies)) + spec-ns @bodies))] + (vec (sort (distinct (mapcat (fn [n] [(dec n) n (inc n)]) ns))))))] (reduce (fn [tenv {:keys [name pred-name] :as r}] (let [pred (deref (ns-resolve (the-ns spec-ns) pred-name)) tenv (assoc-in tenv [::refines name] (assoc r :pred pred)) bias (bias-of (literals (:pred r) spec-ns @bodies))] (assoc-in tenv [::refines name :gen] - (refine-gen r pred (assoc tenv ::bias-of-refine bias))))) + (refine-gen r pred (assoc tenv ::bias-of-refine bias ::spec-ints @spec-ints))))) (tenv-of data) refines))) @@ -1482,14 +1578,39 @@ " for arguments " (pr-str (vec args)))) r))) -(defn- entry [spec-ns target] - (require spec-ns) - (let [e (get @registry spec-ns)] - (when-not e - (fail! "`" spec-ns "` is not a spec namespace: it has no `(spec target-ns)` form")) - (let [e (assoc (if target (assoc e :target target) e) ::ns spec-ns)] - (require (:target e)) - e))) +(defn- default-proof-ns [spec-ns] + (let [n (name spec-ns)] + (symbol (if (str/ends-with? n "-spec") + (str (subs n 0 (- (count n) 5)) "-proof") + (str n "-proof"))))) + +(defn- ns-resource [ns-sym] + (let [base (-> (name ns-sym) (str/replace "-" "_") (str/replace "." "/"))] + (or (io/resource (str base ".clj")) (io/resource (str base ".cljc"))))) + +(defn- proof-entry + "The proof namespace of a spec: opts :proof names it (false for none), + or it is found by name; nil when there is none." + [spec-ns proof] + (let [p (if (some? proof) proof (default-proof-ns spec-ns))] + (when (and p (or (some? proof) (ns-resource p))) + (require p) + (let [pe (or (get @proofs p) + (fail! "`" p "` is not a proof namespace: it has no `(proof-of " spec-ns ")` form"))] + (when-not (= spec-ns (:proves pe)) + (fail! "`" p "` proves `" (:proves pe) "`, not `" spec-ns "`")) + (assoc pe :ns p))))) + +(defn- entry + ([spec-ns target] (entry spec-ns target nil)) + ([spec-ns target proof] + (require spec-ns) + (let [e (get @registry spec-ns)] + (when-not e + (fail! "`" spec-ns "` is not a spec namespace: it has no `(spec target-ns)` form")) + (let [e (assoc (if target (assoc e :target target) e) ::ns spec-ns)] + (require (:target e)) + (assoc e ::proof (proof-entry spec-ns proof)))))) (defn- wrap! "Wrap the signed fns not already wrapped; returns the vars it wrapped." @@ -1527,7 +1648,7 @@ ;; --- check --------------------------------------------------------------------- -(defn- format-failure [{:keys [law counterexample detail original trial seed error prover-bug proof explain]}] +(defn- format-failure [{:keys [law counterexample detail original trial seed error prover-bug proof explain found-by]}] (let [pad (apply max 0 (map (comp count str) (keys counterexample)))] (str (when prover-bug (str "writ bug: law `" law "` was proved (" proof ") but a test refutes it; " @@ -1545,17 +1666,21 @@ (when error (str " " error)) (when (and original (not= original counterexample)) (str "\n (shrunk from " (pr-str original) ", failing on test " trial ")")) - (when seed (str "\n (replay with {:seed " seed "})"))))) + (if (= :solver found-by) + "\n (found by the solver, when no test did, and confirmed by running the code)" + (when seed (str "\n (replay with {:seed " seed "})")))))) (defn format-report "The report as text for an agent or a person: what failed and why." - [{:keys [ok target spec static laws gaps unspecified rejected calls machines proof graphs]}] + [{:keys [ok target spec static laws gaps unspecified rejected calls machines proof graphs graph-missing lemmas]}] (str "writ.spec: " spec " against " target (if ok ": ok" ": FAILED") (when (and proof (pos? (:laws proof))) (str "\n " (:proved proof) " of " (:laws proof) " laws proved" (when (= :proved (:require proof)) " (the spec requires proof)") (when-let [ts (seq (filter #(= :test (:evidence %)) laws))] (str "; tested, not proved: " (str/join ", " (map :law ts)))))) + (apply str (for [{l :lemma p :proof st :status} lemmas :when (= :proved st)] + (str "\n lemma `" l "` proved " p))) (apply str (for [{l :law p :proof st :status} laws :when (= :proved st)] (str "\n law `" l "` proved " p))) (apply str (for [{l :law b :because} laws :when b] @@ -1576,10 +1701,24 @@ (when ok (apply str (for [{m :machine n :states k :events} machines] (str "\n machine `" m "`: " (* n k) " transitions checked")))) - (apply str (for [{g :graph n :edges st :status u ::unproved} graphs :when (= :ok st)] + (apply str (for [{g :graph n :edges st :status u ::unproved m ::obligations} graphs :when (= :ok st) + :let [m (or m 0) u (or u 0) + edges (fn [k] (str k (if (= 1 k) " edge" " edges"))) + flow (- n m)]] (str "\n graph `" g "`: " - (if (zero? u) (str n " edges proved") (str (- n u) " of " n " edges proved"))))) + (cond (zero? m) (str (edges n) ", data flow checked against the signatures") + (zero? u) (str (edges m) " proved") + :else (str (- m u) " of " (edges m) " proved")) + (when (and (pos? m) (pos? flow)) + (str ", " flow " more checked against the signatures"))))) (when-not (:ok static) (str "\n\n" (:error static))) + (when graph-missing + (str "\n\n`" spec "` declares no state graph. A spec starts from the problem's states" + " and the steps between them:" + "\n (graph name {:states {state Type ...} :edges {state {[fn ArgType ...] #{state ...}}}})" + "\n Its states are types, refinements most often; each edge is a fn, proved to take" + "\n its state into one of the states it names. A transition table can be a" + "\n `machine` instead.")) (apply str (for [{g :graph :keys [errors rules]} graphs] (str (apply str (map #(str "\n\n" %) errors)) (when (seq rules) @@ -1608,6 +1747,14 @@ (if (seq gs) (str "exactly " (str/join ", " gs)) "nothing outside clojure.core") ". Call through the layers the spec names instead of around them.")))) (apply str (map #(str "\n\n" (format-failure %)) (filter #(= :failed (:status %)) laws))) + (apply str (for [{l :lemma :as lr} lemmas :when (= :failed (:status lr))] + (str "\n\n" (str/replace-first (format-failure (assoc lr :law l)) "law `" "lemma `") + "\n A lemma must hold: it is a law about the code, written to help prove the spec."))) + (apply str (for [{l :lemma why :unproved st :status} lemmas :when (#{:unproved :tested} st)] + (str "\n\nlemma `" l "` holds in its tests but is not proved" + "\n the prover: " (or why "no proof found") + "\n A lemma must be proved before a law may cite it: give it a hint," + "\n or a lemma of its own."))) (apply str (for [{l :law why :unproved st :status need :require} laws :when (= :unproved st)] (str "\n\nlaw `" l "` is tested, not proved, and the " (if need "law" "spec") " requires proof" @@ -1629,6 +1776,57 @@ (when (seq unspecified) (str "\n\nnot in the spec (no signature): " (str/join ", " unspecified))))) +(def ^:private writ-sources + "The sources a proof depends on, beside the code and the spec: writ's + own translation, prover and solver." + ["writ/lower.clj" "writ/types.clj" "writ/norm.clj" "writ/data.clj" "writ/spec.clj" + "writ/prove.clj" "writ/prove/term.clj" "writ/prove/rewrite.clj" "writ/prove/translate.clj" + "writ/prove/scheme.clj" "writ/prove/check.clj" "writ/prove/smt.clj" "writ/prove/symbolic.clj" + "writ/solve.clj" "writ/solve/pre.clj" "writ/solve/search.clj" "writ/solve/simplex.clj" + "writ/solve/cert.clj"]) + +(def ^:private writ-version + (delay (apply str (map #(or (some-> (io/resource %) slurp) "") writ-sources)))) + +(defn- cache-file + "One file per spec and target: a spec checked against several + implementations keeps a cache for each." + [dir [spec-ns target]] + (io/file dir (str spec-ns "--" target ".edn"))) + +(defn- load-proofs + "The proof results cached for a spec and target, when they were found + from exactly these sources; {} otherwise. The sources are kept whole, not hashed, so a + cached proof is never taken for a different law or different code." + [dir spec-ns sources] + (or (try (let [f (cache-file dir spec-ns)] + (when (.exists f) + (let [c (edn/read-string (slurp f))] + (when (= sources (:sources c)) (:proofs c))))) + (catch Throwable _ nil)) + {})) + +(defn- save-proofs! [dir spec-ns sources proofs] + (try (.mkdirs (io/file dir)) + (spit (cache-file dir spec-ns) (pr-str {:sources sources :proofs proofs})) + (catch Throwable _ nil))) + +(defn- refuted + "The law's failure at the counterexample the solver found, confirmed by + running the law there; nil when there is none, or running it holds." + [ctx r cex] + (when cex + (let [[bs body] (leading-foralls (:prop r)) + vars (mapv first bs)] + (when (every? #(contains? cex %) vars) + (let [res (try (holds (assoc ctx :vars vars) body cex) + (catch Throwable _ nil))] + (when (= :fail (:result res)) + (-> r + (dissoc :unproved :trials :discarded) + (assoc :status :failed :counterexample (select-keys cex vars) + :detail (:detail res) :found-by :solver)))))))) + (defn- refine->defn "A refine form read as the defn of its predicate, which it defines." [f] @@ -1656,21 +1854,33 @@ "Try to prove each law that ran. A tested law the prover proves becomes :proved; a law it cannot prove keeps :tested with the reason. A law that is proved yet refuted by a value (not a throw) is a writ bug." - [results opts target spec-ns tenv anns refs] + [results opts target spec-ns tenv anns refs ctx] (if (= false (:prove opts)) results (let [defs (delay (prover/definitions [[target (book/read-forms (source-url target))] [spec-ns (mapv refine->defn (book/read-forms (source-url spec-ns)))]])) - anns (into {} (map (fn [[k sig]] [k (erase sig refs)])) anns)] + anns (into {} (map (fn [[k sig]] [k (erase sig refs)])) anns) + ;; a proof found before, from the same law, lemmas, code, spec, + ;; proof namespace and writ, is the same proof + cache-dir (when-not (= false (:cache opts)) (or (:cache-dir opts) ".writ-cache")) + sources (delay (pr-str [@writ-version + (book/read-forms (source-url target)) + (book/read-forms (source-url spec-ns)) + (some-> (::proof-ns opts) source-url book/read-forms)])) + cached (atom (if cache-dir (load-proofs cache-dir [spec-ns target] @sources) {})) + fresh (atom false)] ;; a law proved here is a lemma for any law proved after it; one that ;; is only tested, or that a test refutes, never is. Passes repeat ;; while they prove something new, so a law may cite one that comes ;; later in the spec, and no proof can lean on itself: each cites ;; only laws whose proofs were finished before it began - (let [attempt (fn [r lemmas] + (let [attempt* (fn [r lemmas] (try (let [[ds own] @defs] (prover/prove-law {:prop (erase-law (:prop r) refs spec-ns) + :hint (get (::hints opts) (:law r)) + :fuel (or (:fuel (get (::hints opts) (:law r))) (:fuel opts)) + :total (:total r) :defs ds :tenv tenv :target target :own own :lemmas lemmas :rets (into {} (for [[nm sig] anns] @@ -1678,6 +1888,16 @@ (plain (:ret sig))]))})) (catch Throwable e {:proved false :reason (str "the prover failed: " (ex-message e))}))) + attempt (fn [r lemmas] + (let [k (pr-str [(:prop r) (get (::hints opts) (:law r)) (:total r) lemmas (:fuel opts)])] + (or (when-let [pr (get @cached k)] (assoc pr :cached true)) + ;; a search that failed is kept too: it can only + ;; say "not proved", and a counterexample in it is + ;; run on the code again before it is believed + (let [pr (attempt* r lemmas)] + (swap! cached assoc k (select-keys pr [:proved :summary :lemmas :reason :counterexample])) + (reset! fresh true) + pr)))) open? (fn [r] (and (:prop r) (contains? #{:tested :failed} (:status r)) (not (:proof r)) (not (:unproved-final r)))) pass (fn [[rs lemmas]] @@ -1690,12 +1910,16 @@ (and (:proved pr) (= :tested (:status r))) [(conj out (cond-> (-> r (dissoc :unproved) (assoc :status :proved :proof (:summary pr))) + (:cached pr) (assoc :cached true) (seq (:lemmas pr)) (assoc :lemmas (:lemmas pr)))) (conj lemmas {:name (:law r) :prop (:prop r)})] (and (:proved pr) (not (thrown? r))) [(conj out (assoc r :prover-bug true :proof (:summary pr))) lemmas] + (and (= :tested (:status r)) (refuted ctx r (:counterexample pr))) + [(conj out (refuted ctx r (:counterexample pr))) lemmas] + (= :tested (:status r)) [(conj out (cond-> (assoc r :unproved (:reason pr)) ;; outside the model: no lemma changes that @@ -1708,7 +1932,8 @@ (loop [[rs lemmas] (pass [results []])] (let [[rs2 lemmas2] (pass [rs lemmas])] (if (= (count lemmas2) (count lemmas)) - (mapv #(dissoc % :unproved-final) rs2) + (do (when (and cache-dir @fresh) (save-proofs! cache-dir [spec-ns target] @sources @cached)) + (mapv #(dissoc % :unproved-final) rs2)) (recur [rs2 lemmas2])))))))) (def ^:private evidence-of @@ -1742,13 +1967,18 @@ failure. opts: :target, :trials (test.check runs per law, default 100), :seed (default random; each law's report carries the one it used) and :max-size (the largest generated size, default 50), :adequacy (false - skips the gap check), :prove (false skips the prover) and :require + skips the gap check), :prove (false skips the prover), :fuel (the + rewrites the prover may make on one attempt, default 20000) and :require (:proved or :tested, in place of the spec's own)." ([spec-ns] (check spec-ns {})) ([spec-ns opts] (let [{:keys [trials seed max-size] :or {trials 100 max-size 50}} opts - e (entry spec-ns (:target opts)) + e (entry spec-ns (:target opts) (:proof opts)) {:keys [target anns data laws]} e + proof-e (::proof e) + lemma-names (set (map :name (:lemmas proof-e))) + ;; lemmas first, so a law proved after them may cite them + laws (into (mapv #(assoc % :lemma true) (:lemmas proof-e)) laws) static (static-check e) base {:spec spec-ns :target target :static (if (:ok static) {:ok true} static) @@ -1774,7 +2004,7 @@ ;; caller's own instrument stays in place wrapped (wrap! e) results (try - (vec (for [{:keys [name prop explain graph]} laws + (vec (for [{:keys [name prop explain graph total lemma]} laws :let [p (desugar prop)]] (try (lw/check-prop-shape! p) @@ -1794,7 +2024,9 @@ {:trials trials :seed seed :max-size max-size}) :prop qp) explain (assoc :explain explain) - graph (assoc :graph graph)))) + graph (assoc :graph graph) + total (assoc :total true) + lemma (assoc :lemma true)))) ;; a law that cannot be run (a malformed ;; proposition, a type with no generator) ;; fails with the reason, not the whole check @@ -1804,8 +2036,13 @@ (finally (unwrap! wrapped))) level (or (:require opts) (:require e) :tested) _ (check-level! "`check`" level) - results (-> (prove-laws results opts target spec-ns data-tenv anns refs) - (require-evidence laws level)) + results (mapv #(cond-> % (contains? lemma-names (:law %)) (assoc :lemma true)) results) + results (-> (prove-laws results (assoc opts ::hints (:hints proof-e) ::proof-ns (:ns proof-e)) + target spec-ns data-tenv anns refs ctx) + (require-evidence + ;; a lemma is there to be cited, so it must be proved + (mapv #(if (:lemma %) (assoc-in % [:opts :require] :proved) %) laws) + level)) unq (fn unq [f] (cond (and (symbol? f) (contains? #{(name target) (name spec-ns)} (namespace f))) (symbol (name f)) @@ -1820,7 +2057,7 @@ per-fn (if (and sound? (not= false (:adequacy opts))) (adequacy ctx target (sort (filter #(contains? publics %) (keys anns))) - anns (concat (keep :prop results) + anns (concat (keep :prop (remove :lemma results)) (for [m (:machines e)] (qualify (machine-prop m e) #{} publics interns target spec-ns))) @@ -1828,31 +2065,41 @@ []) gaps (vec (for [{f :fn s :survivors} per-fn :when (seq s)] {:fn f :survivors s})) - results (mapv #(dissoc % :prop) results) + lemma-results (mapv #(-> % (dissoc :prop :lemma) (set/rename-keys {:law :lemma})) + (filter :lemma results)) + results (mapv #(dissoc % :prop) (remove :lemma results)) call-results (check-calls e (book/read-forms (source-url target))) machine-results (mapv #(check-machine % e target) (:machines e)) graph-results (mapv (fn [g] (let [errs (vec (concat (graph-flow-errors g anns refs) - (graph-start-errors g spec-ns tenv))) + (graph-start-errors + g spec-ns tenv + #(qualify % #{} publics interns target spec-ns)))) rules (graph-rule-errors g) obls (filter #(= (first g) (:graph %)) results)] (cond-> {:graph (first g) :states (count (:states (second g))) :edges (count (graph-edges g)) :status (if (and (empty? errs) (empty? rules)) :ok :failed) + ::obligations (count obls) ::unproved (count (remove #(= :proof (:evidence %)) obls))} (seq errs) (assoc :errors errs) (seq rules) (assoc :rules rules)))) (:graphs e)) + graphless (and (empty? (:graphs e)) (empty? (:machines e))) r (assoc base :laws results :gaps gaps :calls call-results - :graphs (mapv #(dissoc % ::unproved) graph-results) + :lemmas lemma-results + :graph-missing graphless + :graphs (mapv #(dissoc % ::unproved ::obligations) graph-results) :proof (proof-coverage results level) :machines (mapv #(dissoc % :shown :step) machine-results) :rejected (mapv #(select-keys % [:fn :laws :rejected]) per-fn) :ok (and sound? (empty? gaps) (not-any? #(= :unproved (:status %)) results) + (every? #(= :proved (:status %)) lemma-results) (every? #(= :ok (:status %)) call-results) (every? #(= :ok (:status %)) machine-results) - (every? #(= :ok (:status %)) graph-results)))] + (every? #(= :ok (:status %)) graph-results) + (not graphless)))] (assoc r :message (format-report (assoc r :machines machine-results :graphs graph-results)))))))) diff --git a/test/writ/graph_test.clj b/test/writ/graph_test.clj index 8ad6ad1..cda9c71 100644 --- a/test/writ/graph_test.clj +++ b/test/writ/graph_test.clj @@ -82,3 +82,29 @@ "unknown keys")) (is (str/includes? (expansion-error '(writ.spec/refine Row [y] (pos? y))) "(refine Name [x BaseType] predicate)"))) + +(deftest a-spec-must-declare-its-graph + (let [r (spec/check 'writ.spec-demo.no-graph-spec {:seed 42})] + (is (not (:ok r))) + (is (str/includes? (:message r) "`writ.spec-demo.no-graph-spec` declares no state graph")) + (is (str/includes? (:message r) "(graph name {:states {state Type ...} :edges {state {[fn ArgType ...] #{state ...}}}})")))) + +(deftest a-graph-over-plain-compound-types-is-data-flow + (require 'writ.spec-demo.flow-spec) + (let [r (spec/check 'writ.spec-demo.flow-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (= [{:graph 'sorting :status :ok :states 2 :edges 1}] (:graphs r))))) + +(deftest a-graph-step-is-proved-never-to-throw + (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42}) + l (law-result r 'signal:yellow:tick)] + (is (= :proved (:status l))) + (is (true? (:total l))) + (is (str/includes? (:proof l) "and it never throws")))) + +(deftest a-step-that-throws-is-caught + (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42 :target 'writ.spec-demo.signal-throw}) + l (law-result r 'signal:yellow:tick)] + (is (not (:ok r))) + (is (= :failed (:status l)) (pr-str l)) + (is (str/includes? (:message r) "l = [:Yellow 5]")))) diff --git a/test/writ/proof_test.clj b/test/writ/proof_test.clj new file mode 100644 index 0000000..b08f5d4 --- /dev/null +++ b/test/writ/proof_test.clj @@ -0,0 +1,60 @@ +(ns writ.proof-test + "The proof namespace: lemmas and hints the agent writes to get a spec's + laws proved, kept apart from the spec, which is the contract. A lemma + is a law about the code like any other, so it must hold and be proved; + it helps prove the spec's laws, but never counts as one of them." + (:require [clojure.test :refer [deftest is testing]] + [clojure.string :as str] + [writ.spec :as spec])) + +(defn- law-result [report nm] + (first (filter #(= nm (:law %)) (:laws report)))) + +(deftest without-its-lemma-a-law-stays-unproved + (let [r (spec/check 'writ.spec-demo.sort-lemma-spec {:seed 42 :proof false})] + (is (not (:ok r))) + (is (= :unproved (:status (law-result r 'sorted)))))) + +(deftest a-lemma-from-the-proof-namespace-gets-it-proved + (let [r (spec/check 'writ.spec-demo.sort-lemma-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (= :proved (:status (law-result r 'sorted)))) + (is (= ['insert-keeps-sorted] (:lemmas (law-result r 'sorted)))) + (testing "the lemma is reported apart, and does not count as a law of the spec" + (is (= [{:lemma 'insert-keeps-sorted :status :proved}] + (mapv #(select-keys % [:lemma :status]) (:lemmas r)))) + (is (= 3 (:laws (:proof r)))) + (is (str/includes? (:message r) "lemma `insert-keeps-sorted` proved"))))) + +(deftest a-false-lemma-fails-the-check + (let [r (spec/check 'writ.spec-demo.sort-lemma-spec + {:seed 42 :proof 'writ.spec-demo.sort-false-lemma-proof})] + (is (not (:ok r))) + (is (= :failed (:status (first (:lemmas r))))) + (is (str/includes? (:message r) "lemma `insert-keeps-length` fails for")))) + +(deftest proof-forms-are-checked-when-they-load + (let [err (fn [form] (try (macroexpand-1 form) nil (catch Throwable e (ex-message e))))] + (is (str/includes? (err '(writ.spec/hint sorted [:induct xs])) + "`hint sorted` takes a map")) + (is (str/includes? (err '(writ.spec/hint sorted {:strategy :magic})) + ":strategy must be one of")) + (is (str/includes? (err '(writ.spec/hint sorted {:color :red})) + "unknown keys")))) + +(deftest a-proof-found-once-is-reused + (let [dir (str ".target/writ-cache-test-" (System/currentTimeMillis)) + first-run (spec/check 'writ.spec-demo.court-spec {:seed 42 :cache-dir dir}) + again (spec/check 'writ.spec-demo.court-spec {:seed 42 :cache-dir dir}) + proved (fn [r] (set (map :law (filter #(= :proved (:status %)) (:laws r)))))] + (is (:ok again) (:message again)) + (is (seq (proved first-run))) + (is (= (proved first-run) (proved again))) + (testing "the second check finds its proofs in the cache" + (is (every? :cached (filter #(= :proved (:status %)) (:laws again)))) + (is (not-any? :cached (:laws first-run)))) + (testing "another target has a cache of its own" + (let [other (spec/check 'writ.spec-demo.court-spec {:seed 42 :cache-dir dir :target 'writ.spec-demo.court-open})] + (is (not-any? :cached (:laws other))))) + (testing "without the cache, every proof is found again" + (is (not-any? :cached (:laws (spec/check 'writ.spec-demo.court-spec {:seed 42 :cache false}))))))) diff --git a/test/writ/prove_test.clj b/test/writ/prove_test.clj index 82c71d7..5933879 100644 --- a/test/writ/prove_test.clj +++ b/test/writ/prove_test.clj @@ -361,3 +361,27 @@ (is (= [:lit -3] (norm [:call 'rem [:lit -3] [:lit 5]]))) (testing "a division by zero is left alone, not folded" (is (= [:call 'quot [:lit 1] [:lit 0]] (norm [:call 'quot [:lit 1] [:lit 0]]))))) + +(deftest division-by-a-literal-is-bounded + (let [ctx (rw/context {:types {'n 'Int}}) + holds? (fn [x] (= [:lit true] (rw/normalize ctx x)))] + (testing "mod by a positive k is 0 to k-1, by a negative k is k+1 to 0" + (is (holds? [:call '<= [:lit 0] [:call 'mod 'n [:lit 7]]])) + (is (holds? [:call '<= [:call 'mod 'n [:lit 7]] [:lit 6]])) + (is (holds? [:call '<= [:call 'mod 'n [:lit -7]] [:lit 0]])) + (is (holds? [:call '<= [:lit -6] [:call 'mod 'n [:lit -7]]]))) + (testing "quot by k is within |k|-1 of n/k, rem within |k|-1 of 0" + (is (holds? [:call '<= [:call '* [:lit 7] [:call 'quot 'n [:lit 7]]] [:call '+ 'n [:lit 6]]])) + (is (holds? [:call '<= [:call '- 'n [:lit 6]] [:call '* [:lit 7] [:call 'quot 'n [:lit 7]]]])) + (is (holds? [:call '<= [:call 'rem 'n [:lit 7]] [:lit 6]]))) + (testing "nothing more: mod is not always 0" + (is (not (holds? [:call '= [:call 'mod 'n [:lit 7]] [:lit 0]])))) + (testing "an untyped operand is not an integer" + (is (not (holds? [:call '<= [:lit 0] [:call 'mod 'x [:lit 7]]])))))) + +(deftest division-bounds-agree-with-the-runtime + (doseq [n (range -40 41), k (remove zero? (range -9 10))] + (let [j (dec (abs k))] + (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])))) diff --git a/test/writ/spec_demo/cells.clj b/test/writ/spec_demo/cells.clj new file mode 100644 index 0000000..4189d54 --- /dev/null +++ b/test/writ/spec_demo/cells.clj @@ -0,0 +1,21 @@ +(ns writ.spec-demo.cells + "Conway's rule on an unbounded plane, as a set of live cells.") + +(defn neighbours [cell] + (let [[x y] cell] + #{[(dec x) (dec y)] [x (dec y)] [(inc x) (dec y)] + [(dec x) y] [(inc x) y] + [(dec x) (inc y)] [x (inc y)] [(inc x) (inc y)]})) + +(defn- live-neighbours [world cell] + (count (filter #(contains? world %) (neighbours cell)))) + +(defn- alive-next? [world cell] + (let [n (live-neighbours world cell)] + (if (contains? world cell) + (or (= n 2) (= n 3)) + (= n 3)))) + +(defn step [world] + (set (filter #(alive-next? world %) + (into world (mapcat neighbours world))))) diff --git a/test/writ/spec_demo/cells_origin.clj b/test/writ/spec_demo/cells_origin.clj new file mode 100644 index 0000000..b26355d --- /dev/null +++ b/test/writ/spec_demo/cells_origin.clj @@ -0,0 +1,21 @@ +(ns writ.spec-demo.cells-origin + "cells with a favoured place: a live cell at the origin never dies.") + +(defn neighbours [cell] + (let [[x y] cell] + #{[(dec x) (dec y)] [x (dec y)] [(inc x) (dec y)] + [(dec x) y] [(inc x) y] + [(dec x) (inc y)] [x (inc y)] [(inc x) (inc y)]})) + +(defn- live-neighbours [world cell] + (count (filter #(contains? world %) (neighbours cell)))) + +(defn- alive-next? [world cell] + (let [n (live-neighbours world cell)] + (if (contains? world cell) + (or (= n 2) (= n 3) (= cell [0 0])) + (= n 3)))) + +(defn step [world] + (set (filter #(alive-next? world %) + (into world (mapcat neighbours world))))) diff --git a/test/writ/spec_demo/cells_spec.clj b/test/writ/spec_demo/cells_spec.clj new file mode 100644 index 0000000..fe7e35c --- /dev/null +++ b/test/writ/spec_demo/cells_spec.clj @@ -0,0 +1,41 @@ +(ns writ.spec-demo.cells-spec + "The rule, cell by cell, and the plane's symmetry: proved for every + world, however large." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.cells {:require :proved}) + +(ann neighbours [(Tuple Int Int) -> (Set (Tuple Int Int))]) +(ann step [(Set (Tuple Int Int)) -> (Set (Tuple Int Int))]) + +(graph life + {:states {:cell (Tuple Int Int), :world (Set (Tuple Int Int))} + :edges {:cell {[neighbours] #{:world}} + :world {[step] #{:world}}}}) + +(def offsets [[-1 -1] [0 -1] [1 -1] [-1 0] [1 0] [-1 1] [0 1] [1 1]]) + +(defn around [cell] + (let [[x y] cell] (map (fn [o] [(+ x (first o)) (+ y (second o))]) offsets))) + +(defn touching [world cell] (count (filter (fn [c] (contains? world c)) (around cell)))) + +(defn alive-by-the-rule? [world cell] + (let [n (touching world cell)] + (if (contains? world cell) (or (= n 2) (= n 3)) (= n 3)))) + +(defn shifted [dx dy world] + (set (map (fn [c] [(+ (first c) dx) (+ (second c) dy)]) world))) + +(law neighbours-are-the-eight-cells-around + (forall [x Int, y Int] (= (neighbours [x y]) (set (around [x y]))))) + +(law a-cell-lives-by-the-rule + (forall [w (Set (Tuple Int Int)), x Int, y Int] + (= (contains? (step w) [x y]) (alive-by-the-rule? w [x y])))) + +(law the-plane-has-no-favoured-place + (forall [w (Set (Tuple Int Int)), dx Int, dy Int] + (= (step (shifted dx dy w)) (shifted dx dy (step w))))) + +(law a-blinker-turns (= #{[1 0] [1 1] [1 2]} (step #{[0 1] [1 1] [2 1]}))) diff --git a/test/writ/spec_demo/classify_spec.clj b/test/writ/spec_demo/classify_spec.clj index 03c07a0..2126778 100644 --- a/test/writ/spec_demo/classify_spec.clj +++ b/test/writ/spec_demo/classify_spec.clj @@ -2,12 +2,16 @@ "The contract for writ.spec-demo.classify. The sentinels are pinned by closed laws because a generated Int never reaches -127, and one quantified law says what every other count means." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.classify) (ann classify-read [Int Bool -> Keyword]) +(graph reading + {:states {:count Int, :status Keyword} + :edges {:count {[classify-read Bool] #{:status}}}}) + (law zero-is-decided-by-the-eof-flag (forall [e Bool] (= (classify-read 0 e) (if e :eof :idle)))) diff --git a/test/writ/spec_demo/classify_weak_spec.clj b/test/writ/spec_demo/classify_weak_spec.clj index f38e96c..676207c 100644 --- a/test/writ/spec_demo/classify_weak_spec.clj +++ b/test/writ/spec_demo/classify_weak_spec.clj @@ -2,12 +2,16 @@ "classify-spec without its one quantified law over n. Every law still holds, but they only ever call classify-read with n = 0, -1, -2 or -127, so nothing says what 5 or -50 means." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.classify) (ann classify-read [Int Bool -> Keyword]) +(graph reading + {:states {:count Int, :status Keyword} + :edges {:count {[classify-read Bool] #{:status}}}}) + (law zero-is-decided-by-the-eof-flag (forall [e Bool] (= (classify-read 0 e) (if e :eof :idle)))) diff --git a/test/writ/spec_demo/court_spec.clj b/test/writ/spec_demo/court_spec.clj index fc9b4f5..3a086d3 100644 --- a/test/writ/spec_demo/court_spec.clj +++ b/test/writ/spec_demo/court_spec.clj @@ -3,7 +3,7 @@ constants, max and min, abs, not=, every? and some, a comparison of three, and contains? on a set of keywords." (:require [writ.spec-demo.court :refer [H PH]] - [writ.spec :refer [spec data ann law refine]])) + [writ.spec :refer [spec data ann law refine graph]])) (spec writ.spec-demo.court {:require :proved}) @@ -13,6 +13,12 @@ (ann safe? [Keyword -> Bool]) (ann distance [Int Int -> Nat]) +(graph court + {:states {:paddle Int, :gap Nat, :method Keyword, :verdict Bool} + :edges {:paddle {[move Key] #{:paddle} + [distance Int] #{:gap}} + :method {[safe?] #{:verdict}}}}) + (def top (- H PH)) (law a-paddle-stays-on-the-court diff --git a/test/writ/spec_demo/flow_spec.clj b/test/writ/spec_demo/flow_spec.clj new file mode 100644 index 0000000..8da7acb --- /dev/null +++ b/test/writ/spec_demo/flow_spec.clj @@ -0,0 +1,20 @@ +(ns writ.spec-demo.flow-spec + "A graph whose states are plain compound types: data flow only." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.sort) + +(ann insert [Nat (List Nat) -> (List Nat)]) +(ann isort [(List Nat) -> (List Nat)]) + +(graph sorting + {:states {:unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}}}}) + +(defn occurrences [x xs] (count (filter #(= x %) xs))) +(defn ascending? [xs] (or (empty? xs) (apply <= xs))) + +(law sorted (forall [xs (List Nat)] (ascending? (isort xs)))) +(law permutation (forall [x Nat, xs (List Nat)] (= (occurrences x (isort xs)) (occurrences x xs)))) +(law insert-keeps-sorted (forall [x Nat, xs (List Nat)] (=> (ascending? xs) (ascending? (insert x xs))))) +(law insert-adds (forall [x Nat, xs (List Nat)] (= (occurrences x (insert x xs)) (inc (occurrences x xs))))) diff --git a/test/writ/spec_demo/light_spec.clj b/test/writ/spec_demo/light_spec.clj index 6008183..2c9963f 100644 --- a/test/writ/spec_demo/light_spec.clj +++ b/test/writ/spec_demo/light_spec.clj @@ -1,5 +1,5 @@ (ns writ.spec-demo.light-spec - (:require [writ.spec :refer [spec data ann law]])) + (:require [writ.spec :refer [spec data ann law graph]])) (spec writ.spec-demo.light) @@ -7,5 +7,9 @@ (ann tick [(Tuple Light Nat) -> (Tuple Light Nat)]) +(graph light + {:states {:showing (Tuple Light Nat)} + :edges {:showing {[tick] #{:showing}}}}) + (law a-light-holds-for-three-ticks (forall [n Nat] (= [[:Red] (inc n)] (tick [[:Red] n])))) diff --git a/test/writ/spec_demo/nat_chain_spec.clj b/test/writ/spec_demo/nat_chain_spec.clj index f3826c3..cda1a5c 100644 --- a/test/writ/spec_demo/nat_chain_spec.clj +++ b/test/writ/spec_demo/nat_chain_spec.clj @@ -1,5 +1,5 @@ (ns writ.spec-demo.nat-chain-spec - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.nat-chain) @@ -8,6 +8,10 @@ (ann half-by-two [Nat -> Nat]) (ann thirds [Nat -> Nat]) +(graph dividing + {:states {:n Nat, :part Nat} + :edges {:n {[half] #{:part}, [parity] #{:part}, [half-by-two] #{:part}, [thirds] #{:part}}}}) + (law half-halves (forall [n Nat] (= (half n) (quot n 2)))) (law parity-is-mod-2 (forall [n Nat] (= (parity n) (mod n 2)))) (law half-by-two-halves (forall [n Nat] (= (half-by-two n) (quot n 2)))) diff --git a/test/writ/spec_demo/no_graph_spec.clj b/test/writ/spec_demo/no_graph_spec.clj new file mode 100644 index 0000000..77e724a --- /dev/null +++ b/test/writ/spec_demo/no_graph_spec.clj @@ -0,0 +1,9 @@ +(ns writ.spec-demo.no-graph-spec + "A spec that states laws but no state graph." + (:require [writ.spec :refer [spec ann law]])) + +(spec writ.spec-demo.signal) + +(ann tick [(Tuple Keyword Nat) -> (Tuple Keyword Nat)]) + +(law a-green-light-counts-up (= [:Green 1] (tick [:Green 0]))) diff --git a/test/writ/spec_demo/pipeline_spec.clj b/test/writ/spec_demo/pipeline_spec.clj index a734aac..fc568e7 100644 --- a/test/writ/spec_demo/pipeline_spec.clj +++ b/test/writ/spec_demo/pipeline_spec.clj @@ -2,7 +2,7 @@ "The contract for writ.spec-demo.pipeline. The laws say what a request gets back; the `calls` forms say how the layers fit together." (:require [clojure.string :as str] - [writ.spec :refer [spec ann law calls]])) + [writ.spec :refer [spec ann law calls graph]])) (spec writ.spec-demo.pipeline) @@ -11,6 +11,11 @@ (ann respond [String -> (Tuple Keyword String)]) (ann handle [String -> (Tuple Keyword String)]) +(graph request + {:states {:raw String, :clean String, :valid Bool, :response (Tuple Keyword String)} + :edges {:raw {[normalize] #{:clean}, [handle] #{:response}} + :clean {[valid?] #{:valid}, [respond] #{:response}}}}) + (calls normalize [str/lower-case str/trim]) (calls valid? []) (calls respond [valid?]) diff --git a/test/writ/spec_demo/pipeline_unknown_spec.clj b/test/writ/spec_demo/pipeline_unknown_spec.clj index a61fd59..e4a0eca 100644 --- a/test/writ/spec_demo/pipeline_unknown_spec.clj +++ b/test/writ/spec_demo/pipeline_unknown_spec.clj @@ -1,11 +1,15 @@ (ns writ.spec-demo.pipeline-unknown-spec "A `calls` form naming fns the target does not define." - (:require [writ.spec :refer [spec ann law calls]])) + (:require [writ.spec :refer [spec ann law calls graph]])) (spec writ.spec-demo.pipeline) (ann handle [String -> (Tuple Keyword String)]) +(graph request + {:states {:raw String, :response (Tuple Keyword String)} + :edges {:raw {[handle] #{:response}}}}) + (calls handle [normalise respond]) (calls render [respond]) diff --git a/test/writ/spec_demo/shapes.clj b/test/writ/spec_demo/shapes.clj new file mode 100644 index 0000000..ff2d17a --- /dev/null +++ b/test/writ/spec_demo/shapes.clj @@ -0,0 +1,30 @@ +(ns writ.spec-demo.shapes + "Plain code for testing symbolic evaluation: tagged data with fields, + destructuring with defaults, a branch that throws, and division.") + +(defn perimeter [shape] + (case (first shape) + :Square (let [[_ s] shape] (* 4 s)) + :Rect (let [[_ w h] shape] (* 2 (+ w h))) + :Dot 0)) + +(defn area [shape] + (case (first shape) + :Square (let [[_ s] shape] (* s s)) + :Rect (let [[_ w h] shape] (* w h)) + :Dot 0)) + +(defn grow [shape] + (let [[tag a b] shape] + (case tag + :Square [:Square (inc a)] + :Rect [:Rect (inc a) (max b (quot a 2))] + :Dot [:Square 1]))) + +(defn bucket [n] + (cond (neg? n) [:low (abs n)] + (< n 10) [:mid (mod n 3)] + :else [:high (quot n 10)])) + +(defn pick [xs i] + (nth xs i :none)) diff --git a/test/writ/spec_demo/signal_throw.clj b/test/writ/spec_demo/signal_throw.clj new file mode 100644 index 0000000..ef1eb6f --- /dev/null +++ b/test/writ/spec_demo/signal_throw.clj @@ -0,0 +1,14 @@ +(ns writ.spec-demo.signal-throw + "signal, but a yellow light that has run its time looks past the end of + a vector: tick throws there.") + +(def GREEN 30) +(def YELLOW 5) +(def RED 30) + +(defn tick [light] + (let [[phase t] light] + (case phase + :Green (if (< t GREEN) [:Green (inc t)] [:Yellow 0]) + :Yellow (if (< t YELLOW) [:Yellow (inc t)] (nth [[:Red 0]] (- t YELLOW -1))) + :Red (if (< t RED) [:Red (inc t)] [:Green 0])))) diff --git a/test/writ/spec_demo/sort_every_spec.clj b/test/writ/spec_demo/sort_every_spec.clj index 4130352..f3bcc9a 100644 --- a/test/writ/spec_demo/sort_every_spec.clj +++ b/test/writ/spec_demo/sort_every_spec.clj @@ -1,12 +1,17 @@ (ns writ.spec-demo.sort-every-spec "A law that passes a fn literal to every?." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (law every-prefix-starts-low (forall [xs (List Nat)] (every? #(<= (first (isort xs)) %) xs))) diff --git a/test/writ/spec_demo/sort_false_lemma_proof.clj b/test/writ/spec_demo/sort_false_lemma_proof.clj new file mode 100644 index 0000000..edba6fe --- /dev/null +++ b/test/writ/spec_demo/sort_false_lemma_proof.clj @@ -0,0 +1,8 @@ +(ns writ.spec-demo.sort-false-lemma-proof + "A proof namespace with a lemma that is false of the code." + (:require [writ.spec :refer [proof-of lemma]])) + +(proof-of writ.spec-demo.sort-lemma-spec) + +(lemma insert-keeps-length + (forall [x Nat, xs (List Nat)] (= (count (insert x xs)) (count xs)))) diff --git a/test/writ/spec_demo/sort_lemma_proof.clj b/test/writ/spec_demo/sort_lemma_proof.clj new file mode 100644 index 0000000..4366a21 --- /dev/null +++ b/test/writ/spec_demo/sort_lemma_proof.clj @@ -0,0 +1,13 @@ +(ns writ.spec-demo.sort-lemma-proof + "How writ.spec-demo.sort-lemma-spec is proved: the lemma its `sorted` + law needs, and a hint where to look." + (:require [writ.spec :refer [proof-of lemma hint]])) + +(proof-of writ.spec-demo.sort-lemma-spec) + +(lemma insert-keeps-sorted + (forall [x Nat, xs (List Nat)] + (=> (writ.spec-demo.sort-lemma-spec/ascending? xs) + (writ.spec-demo.sort-lemma-spec/ascending? (insert x xs))))) + +(hint sorted {:induct xs :use [insert-keeps-sorted]}) diff --git a/test/writ/spec_demo/sort_lemma_spec.clj b/test/writ/spec_demo/sort_lemma_spec.clj new file mode 100644 index 0000000..34f74cb --- /dev/null +++ b/test/writ/spec_demo/sort_lemma_spec.clj @@ -0,0 +1,21 @@ +(ns writ.spec-demo.sort-lemma-spec + "The sort's contract, demanding proof, without the lemma about insert + that the proof of `sorted` needs: that lemma is the prover's business, + kept in writ.spec-demo.sort-lemma-proof." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.sort {:require :proved}) + +(ann insert [Nat (List Nat) -> (List Nat)]) +(ann isort [(List Nat) -> (List Nat)]) + +(graph sorting + {:states {:unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}}}}) + +(defn ascending? [xs] (or (empty? xs) (apply <= xs))) +(defn occurrences [x xs] (count (filter #(= x %) xs))) + +(law sorted (forall [xs (List Nat)] (ascending? (isort xs)))) +(law permutation (forall [x Nat, xs (List Nat)] (= (occurrences x (isort xs)) (occurrences x xs)))) +(law insert-adds (forall [x Nat, xs (List Nat)] (= (occurrences x (insert x xs)) (inc (occurrences x xs))))) diff --git a/test/writ/spec_demo/sort_let_spec.clj b/test/writ/spec_demo/sort_let_spec.clj index 51b151a..437696f 100644 --- a/test/writ/spec_demo/sort_let_spec.clj +++ b/test/writ/spec_demo/sort_let_spec.clj @@ -1,12 +1,17 @@ (ns writ.spec-demo.sort-let-spec "A law whose predicate binds a local with `let`." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (law smallest-first (forall [xs (List Nat)] (=> (seq xs) diff --git a/test/writ/spec_demo/sort_pairs_spec.clj b/test/writ/spec_demo/sort_pairs_spec.clj index 1dd35e1..47fc45f 100644 --- a/test/writ/spec_demo/sort_pairs_spec.clj +++ b/test/writ/spec_demo/sort_pairs_spec.clj @@ -1,13 +1,18 @@ (ns writ.spec-demo.sort-pairs-spec "A spec whose helper destructures in a fn literal, which the prover cannot read." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (defn in-order? [xs] (every? (fn [[a b]] (<= a b)) (partition 2 1 xs))) (law sorted (forall [xs (List Nat)] (in-order? (isort xs)))) diff --git a/test/writ/spec_demo/sort_proved_spec.clj b/test/writ/spec_demo/sort_proved_spec.clj index 940ec89..3b2967f 100644 --- a/test/writ/spec_demo/sort_proved_spec.clj +++ b/test/writ/spec_demo/sort_proved_spec.clj @@ -1,13 +1,18 @@ (ns writ.spec-demo.sort-proved-spec "The sort's contract, demanding proof: every law must be proved, not only tested, unless it says why it cannot be yet." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort {:require :proved}) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (defn ascending? [xs] (or (empty? xs) (apply <= xs))) diff --git a/test/writ/spec_demo/sort_spec.clj b/test/writ/spec_demo/sort_spec.clj index 075989c..a7a0399 100644 --- a/test/writ/spec_demo/sort_spec.clj +++ b/test/writ/spec_demo/sort_spec.clj @@ -5,13 +5,18 @@ element. The laws say that and nothing about how it is done, and they measure the result with the spec's own vocabulary (`ascending?`, `occurrences`), never with the implementation's." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (defn ascending? [xs] (or (empty? xs) (apply <= xs))) diff --git a/test/writ/spec_demo/sort_unproved_spec.clj b/test/writ/spec_demo/sort_unproved_spec.clj index 90fa617..62aafa2 100644 --- a/test/writ/spec_demo/sort_unproved_spec.clj +++ b/test/writ/spec_demo/sort_unproved_spec.clj @@ -1,13 +1,18 @@ (ns writ.spec-demo.sort-unproved-spec "The sort's contract at the default level, with one law that demands proof the prover cannot give." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (defn ascending? [xs] (or (empty? xs) (apply <= xs))) diff --git a/test/writ/spec_demo/sort_vacuous_spec.clj b/test/writ/spec_demo/sort_vacuous_spec.clj index c283db2..aee8e18 100644 --- a/test/writ/spec_demo/sort_vacuous_spec.clj +++ b/test/writ/spec_demo/sort_vacuous_spec.clj @@ -1,12 +1,17 @@ (ns writ.spec-demo.sort-vacuous-spec "A spec whose laws are true of any implementation." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + ;; restates itself: true whatever isort does (law sort-refl (forall [xs (List Nat)] (= (isort xs) (isort xs)))) diff --git a/test/writ/spec_demo/sort_weak_spec.clj b/test/writ/spec_demo/sort_weak_spec.clj index 21ecd1c..87705c3 100644 --- a/test/writ/spec_demo/sort_weak_spec.clj +++ b/test/writ/spec_demo/sort_weak_spec.clj @@ -1,10 +1,15 @@ (ns writ.spec-demo.sort-weak-spec "A spec that states only that the output is ordered." - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(graph sorting + {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}} + :item {[insert (List Nat)] #{:sorted}}}}) + (law sorted (forall [xs (List Nat)] (apply <= 0 (isort xs)))) diff --git a/test/writ/spec_demo/total_spec.clj b/test/writ/spec_demo/total_spec.clj index 62e4807..ad9ab6c 100644 --- a/test/writ/spec_demo/total_spec.clj +++ b/test/writ/spec_demo/total_spec.clj @@ -1,5 +1,5 @@ (ns writ.spec-demo.total-spec - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) (spec writ.spec-demo.total) @@ -7,6 +7,10 @@ (ann size [(List Nat) -> Nat]) (ann total-by-reduce [(List Nat) -> Nat]) +(graph summing + {:states {:items (List Nat), :sum Nat, :count Nat} + :edges {:items {[total] #{:sum}, [total-by-reduce] #{:sum}, [size] #{:count}}}}) + (law total-of-two (forall [a Nat, b Nat] (= (+ a b) (total (list a b))))) (law total-sums (forall [xs (List Nat)] (= (total xs) (apply + xs)))) (law size-counts (forall [xs (List Nat)] (= (size xs) (count xs)))) diff --git a/test/writ/spec_demo/tree_spec.clj b/test/writ/spec_demo/tree_spec.clj index bf65e7c..014f5e2 100644 --- a/test/writ/spec_demo/tree_spec.clj +++ b/test/writ/spec_demo/tree_spec.clj @@ -4,7 +4,7 @@ The problem: a set of nats that keeps its elements in order. The central law says exactly that -- a tree built by inserting xs lists the distinct elements of xs in ascending order -- against clojure.core as the model." - (:require [writ.spec :refer [spec data ann law]])) + (:require [writ.spec :refer [spec data ann law graph]])) (spec writ.spec-demo.tree) @@ -14,6 +14,11 @@ (ann to-list [Tree -> (List Nat)]) (ann insert [Nat Tree -> Tree]) +(graph tree + {:states {:item Nat, :tree Tree, :listed (List Nat), :size Nat} + :edges {:item {[insert Tree] #{:tree}} + :tree {[to-list] #{:listed}, [size] #{:size}}}}) + (defn strictly-ascending? [xs] (or (empty? xs) (apply < xs))) diff --git a/test/writ/symbolic_test.clj b/test/writ/symbolic_test.clj new file mode 100644 index 0000000..33d2d1d --- /dev/null +++ b/test/writ/symbolic_test.clj @@ -0,0 +1,113 @@ +(ns writ.symbolic-test + "Symbolic evaluation agrees with running the code: for concrete inputs, + the formula for (= (f x) out) holds exactly when f returns out." + (:require [clojure.test :refer [deftest is testing]] + [clojure.java.io] + [writ.book] + [writ.prove :as prover] + [writ.prove.symbolic :as sym] + [writ.spec :as spec])) + +(require 'writ.spec-demo.shapes 'writ.spec-demo.signal 'writ.spec-demo.court) + +(defn- defs-of [ns-sym file] + (first (prover/definitions [[ns-sym (writ.book/read-forms (clojure.java.io/resource file))]]))) + +(def ^:private tenv + {'Shape {:arity 0 :params [] :ctors {'Square {:fields ['Int]} + 'Rect {:fields ['Int 'Int]} + 'Dot {:fields []}}} + 'Key {:arity 0 :params [] :ctors {'Idle {:fields []} 'Up {:fields []} 'Down {:fields []}}}}) + +(defn- term-of + "The term for a value: a literal, a list or a set of them." + [v] + (cond (sequential? v) [:sq (reduce (fn [e x] [:econs (term-of x) e]) [:enil] (reverse v))] + (set? v) (into [:call 'hash-set] (map term-of v)) + :else [:lit v])) + +(defn- check [defs types f args envs] + (doseq [env envs] + (let [opts {:types types :defs defs :tenv tenv} + actual (try (apply (resolve f) (map env args)) (catch Throwable _ ::threw)) + call (into [:app f] args)] + (when-not (= ::threw actual) + (is (true? (sym/agrees? opts [:call '= call (term-of actual)] env)) + (str f " at " env " is " (pr-str actual)))) + (is (true? (sym/agrees? opts [:call '= call [:lit :not-a-result]] env)) + (str f " at " env " is not :not-a-result"))))) + +(deftest data-with-fields-and-defaults + (let [defs (defs-of 'writ.spec-demo.shapes "writ/spec_demo/shapes.clj") + shapes (for [a [-3 0 2 7] b [-1 5]] [[:Square a] [:Rect a b] [:Dot]])] + (check defs '{s Shape} 'writ.spec-demo.shapes/perimeter '[s] + (for [s (distinct (apply concat shapes))] {'s s})) + (check defs '{s Shape} 'writ.spec-demo.shapes/grow '[s] + (for [s (distinct (apply concat shapes))] {'s s})))) + +(deftest branches-and-division + (let [defs (defs-of 'writ.spec-demo.shapes "writ/spec_demo/shapes.clj")] + (check defs '{n Int} 'writ.spec-demo.shapes/bucket '[n] + (for [n [-17 -1 0 1 5 9 10 11 99 -100]] {'n n})))) + +(deftest nth-with-a-default-on-a-tuple + (let [defs (defs-of 'writ.spec-demo.shapes "writ/spec_demo/shapes.clj")] + (check defs '{xs (Tuple Int Keyword Int) i Int} 'writ.spec-demo.shapes/pick '[xs i] + (for [i [-1 0 1 2 3 7]] {'xs [4 :k -2] 'i i})))) + +(deftest the-demos-agree + (let [defs (defs-of 'writ.spec-demo.signal "writ/spec_demo/signal.clj")] + (check defs '{l (Tuple Keyword Nat)} 'writ.spec-demo.signal/tick '[l] + (for [p [:Green :Yellow :Red :Blue] t [0 4 5 29 30 31]] {'l [p t]}))) + (let [defs (defs-of 'writ.spec-demo.court "writ/spec_demo/court.clj")] + (check defs '{y Int k Key} 'writ.spec-demo.court/move '[y k] + (for [y [-9 0 1 36 37 38 99] k [[:Up] [:Down] [:Idle]]] {'y y 'k k})))) + +(deftest outside-is-said-not-guessed + (testing "a product of two unknowns is not linear" + (let [defs (defs-of 'writ.spec-demo.shapes "writ/spec_demo/shapes.clj")] + (is (= :outside (sym/agrees? {:types '{s Shape} :defs defs :tenv tenv} + [:call '= [:app 'writ.spec-demo.shapes/area 's] [:lit 9]] + {'s [:Square 3]}))))) + (let [defs (defs-of 'writ.spec-demo.sort "writ/spec_demo/sort.clj")] + (require 'writ.spec-demo.sort) + (is (= :outside (sym/agrees? {:types '{xs (List Nat)} :defs defs :tenv {}} + [:app 'writ.spec-demo.sort/isort 'xs] {'xs [3 1]}))))) + +(deftest sets-agree + (require 'writ.spec-demo.cells) + (let [defs (defs-of 'writ.spec-demo.cells "writ/spec_demo/cells.clj") + worlds [#{} #{[0 0]} #{[0 1] [1 1] [2 1]} #{[0 0] [1 0] [0 1] [1 1]} #{[5 5] [-3 2]}]] + (check defs '{c (Tuple Int Int)} 'writ.spec-demo.cells/neighbours '[c] + (for [c [[0 0] [-4 9]]] {'c c})) + (testing "membership in a stepped world of unknown size" + (doseq [w worlds, cell [[0 0] [1 1] [1 0] [4 4]]] + (let [opts {:types '{w (Set (Tuple Int Int)) cell (Tuple Int Int)} :defs defs :tenv {}} + g [:call 'contains? [:app 'writ.spec-demo.cells/step 'w] 'cell]] + ;; w is a predicate the solver may choose; pinning a finite set + ;; to it is outside, so only the cell is pinned, and the check + ;; is that the formula is not refuted at the real value + (is (not= false (sym/agrees? opts g {'cell cell})))))))) + +(deftest a-symmetric-rule-is-proved-for-every-world + (let [r (spec/check 'writ.spec-demo.cells-spec {:seed 42}) + law (fn [nm] (first (filter #(= nm (:law %)) (:laws r))))] + (is (:ok r) (:message r)) + (doseq [nm '[neighbours-are-the-eight-cells-around a-cell-lives-by-the-rule + the-plane-has-no-favoured-place]] + (is (= :proved (:status (law nm))) (str nm))) + (testing "a favoured place is refuted, and never proved" + (let [r (spec/check 'writ.spec-demo.cells-spec {:seed 42 :target 'writ.spec-demo.cells-origin})] + (is (not (:ok r))) + (is (not= :proved (:status (first (filter #(= 'the-plane-has-no-favoured-place (:law %)) (:laws r)))))) + (is (not= :proved (:status (first (filter #(= 'a-cell-lives-by-the-rule (:law %)) (:laws r)))))) + (is (not-any? :prover-bug (:laws r))))))) + +(deftest throws-agree + (let [defs (defs-of 'writ.spec-demo.shapes "writ/spec_demo/shapes.clj") + opts {:types '{xs (Tuple Int Keyword Int) i Int} :defs defs :tenv tenv}] + (doseq [i [-1 0 2 3 9]] + (is (true? (sym/throws-agree? opts [:call 'nth 'xs 'i] {'xs [4 :k -2] 'i i})) (str i))) + (doseq [n [-3 0 12]] + (is (true? (sym/throws-agree? {:types '{n Int} :defs defs :tenv tenv} + [:app 'writ.spec-demo.shapes/bucket 'n] {'n n})))))) diff --git a/test/writ/test_runner.clj b/test/writ/test_runner.clj index 98de4e7..3370300 100644 --- a/test/writ/test_runner.clj +++ b/test/writ/test_runner.clj @@ -9,11 +9,13 @@ writ.prove-test writ.evidence-test writ.graph-test - writ.solve-test)) + writ.solve-test + writ.symbolic-test + writ.proof-test)) (def test-namespaces '[writ.check-test writ.book-test writ.gaps-test writ.spec-test writ.prove-test writ.evidence-test - writ.graph-test writ.solve-test]) + writ.graph-test writ.solve-test writ.symbolic-test writ.proof-test]) (defn -main [& _] (let [{:keys [fail error]} (apply t/run-tests test-namespaces)] From 7dc17bd32a65936008af6100d0edb1a0a2d0a692 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 20:12:37 -0400 Subject: [PATCH 6/8] examples: specs as state graphs, proved end to end pong, life and fetch now prove every universal law and every graph edge. life's the-plane-has-no-favoured-place holds for every world, not packed 6x6 samples. pong's tunnel bug is found by the solver where no test finds it. life.fast counts with frequencies, outside the prover, so it is checked with :require :tested. --- examples/test/fetch/core_spec.clj | 15 ++- examples/test/fetch/examples_spec.clj | 6 +- examples/test/life/broken/origin.clj | 21 +++ examples/test/life/core_spec.clj | 89 +++++++----- examples/test/life/core_test.clj | 19 ++- examples/test/pong/ball_draft_spec.clj | 7 +- examples/test/pong/core_spec.clj | 180 ++++++++++++------------- examples/test/pong/core_test.clj | 12 +- examples/test/shortener/core_spec.clj | 20 ++- 9 files changed, 233 insertions(+), 136 deletions(-) create mode 100644 examples/test/life/broken/origin.clj diff --git a/examples/test/fetch/core_spec.clj b/examples/test/fetch/core_spec.clj index 81a75be..1e3a14c 100644 --- a/examples/test/fetch/core_spec.clj +++ b/examples/test/fetch/core_spec.clj @@ -10,7 +10,7 @@ generated offset, like (+ 400 (mod n 100)), and name the statuses that carry meaning one by one." (:require [fetch.core :refer [base-ms cap-ms max-attempts]] - [writ.spec :refer [spec data ann law]])) + [writ.spec :refer [spec data ann refine graph law]])) (spec fetch.core) @@ -22,6 +22,19 @@ (ann repeatable? [Keyword Nat -> Bool]) (ann next-action [Keyword Nat Nat -> Action]) +;; --- the flow of a request --------------------------------------------------------- + +;; a wait is never shorter than the base or longer than the cap +(refine Delay [ms Nat] (<= base-ms ms cap-ms)) + +(graph retry + {:states {:status Nat, :class Class, :attempt Nat, :delay Delay, + :method Keyword, :safe Bool, :action Action} + :edges {:status {[classify] #{:class}} + :attempt {[backoff-ms] #{:delay}} + :method {[repeatable? Nat] #{:safe} + [next-action Nat Nat] #{:action}}}}) + (def redirects #{301 302 303 307 308}) (def transient #{0 408 425 429 500 502 503 504}) (def server-refused #{408 429 503}) diff --git a/examples/test/fetch/examples_spec.clj b/examples/test/fetch/examples_spec.clj index f16e608..3665b5f 100644 --- a/examples/test/fetch/examples_spec.clj +++ b/examples/test/fetch/examples_spec.clj @@ -5,7 +5,7 @@ any other status, and writ reports that: a `classify` that agrees on these statuses and answers anything at all elsewhere satisfies it. core_spec.clj states the bands instead." - (:require [writ.spec :refer [spec data ann law]])) + (:require [writ.spec :refer [spec data ann graph law]])) (spec fetch.core) @@ -13,6 +13,10 @@ (ann classify [Nat -> Class]) +(graph statuses + {:states {:status Nat, :class Class} + :edges {:status {[classify] #{:class}}}}) + (law ok-is-done (= [:Done] (classify 200))) (law moved-is-a-redirect (= [:Redirect] (classify 301))) (law throttled-is-transient (= [:Transient] (classify 429))) diff --git a/examples/test/life/broken/origin.clj b/examples/test/life/broken/origin.clj new file mode 100644 index 0000000..acf83c7 --- /dev/null +++ b/examples/test/life/broken/origin.clj @@ -0,0 +1,21 @@ +(ns life.broken.origin + "life.core with a favoured place: a cell at the origin never dies.") + +(defn neighbours [cell] + (let [[x y] cell] + #{[(dec x) (dec y)] [x (dec y)] [(inc x) (dec y)] + [(dec x) y] [(inc x) y] + [(dec x) (inc y)] [x (inc y)] [(inc x) (inc y)]})) + +(defn- live-neighbours [world cell] + (count (filter #(contains? world %) (neighbours cell)))) + +(defn- alive-next? [world cell] + (let [n (live-neighbours world cell)] + (if (contains? world cell) + (or (= n 2) (= n 3) (= cell [0 0])) + (= n 3)))) + +(defn step [world] + (set (filter #(alive-next? world %) + (into world (mapcat neighbours world))))) diff --git a/examples/test/life/core_spec.clj b/examples/test/life/core_spec.clj index 98c5cf8..2d9a179 100644 --- a/examples/test/life/core_spec.clj +++ b/examples/test/life/core_spec.clj @@ -1,28 +1,67 @@ (ns life.core-spec "The contract for the Game of Life, for any implementation of it. - The rule is stated once, cell by cell, in `next-generation`: a model that - scans every cell of the box around the world. It is slow and plain, and - it only runs here. The laws say the code agrees with it, and they add - what the rule implies: the plane has no favoured place, and the famous - patterns behave as they should. + The rule is stated cell by cell: a cell is alive after a step exactly + when it has three live neighbours, or two and was alive. That is the + whole meaning of `step`, for every world and every cell, and it is + proved from the code. So is what the rule implies: the plane has no + favoured place, and a world shifted and stepped is the world stepped + and shifted. Random worlds are sparse, and a sparse world hardly ever has a cell with - three live neighbours. `packed` folds any generated world into a 6x6 - box, so every trial is crowded enough to exercise the rule." - (:require [writ.spec :refer [spec ann law]])) + three live neighbours. `packed` folds a generated world into a 6x6 box, + and one law, tested on crowded worlds, compares whole generations with + a model of the rule, so a broken rule is caught with a small world." + (:require [writ.spec :refer [spec ann refine graph law]])) -(spec life.core) +(spec life.core {:require :proved}) (ann neighbours [(Tuple Int Int) -> (Set (Tuple Int Int))]) (ann step [(Set (Tuple Int Int)) -> (Set (Tuple Int Int))]) -;; --- the rule, cell by cell -------------------------------------------------------- +;; --- the states: a world, and the cells around a cell ------------------------------ -(defn touching [world x y] - (count (for [dx [-1 0 1] dy [-1 0 1] - :when (and (not= 0 dx dy) (contains? world [(+ x dx) (+ y dy)]))] - 1))) +(refine Neighbourhood [cells (Set (Tuple Int Int))] (= 8 (count cells))) + +(graph life + {:states {:cell (Tuple Int Int), :around Neighbourhood, :world (Set (Tuple Int Int))} + :edges {:cell {[neighbours] #{:around}} + :world {[step] #{:world}}}}) + +;; --- the rule, cell by cell ------------------------------------------------------ + +(def offsets [[-1 -1] [0 -1] [1 -1] [-1 0] [1 0] [-1 1] [0 1] [1 1]]) + +(defn around [cell] + (let [[x y] cell] + (map (fn [o] [(+ x (first o)) (+ y (second o))]) offsets))) + +(defn touching [world cell] + (count (filter (fn [c] (contains? world c)) (around cell)))) + +(defn alive-by-the-rule? [world cell] + (let [n (touching world cell)] + (if (contains? world cell) (or (= n 2) (= n 3)) (= n 3)))) + +(law neighbours-are-the-eight-cells-around + (forall [x Int, y Int] (= (neighbours [x y]) (set (around [x y]))))) + +(law neighbours-names-each-once + (forall [x Int, y Int] (= 8 (count (neighbours [x y]))))) + +(law a-cell-lives-by-the-rule + (forall [w (Set (Tuple Int Int)), x Int, y Int] + (= (contains? (step w) [x y]) (alive-by-the-rule? w [x y])))) + +(defn shifted [dx dy world] + (set (map (fn [c] [(+ (first c) dx) (+ (second c) dy)]) world))) + +(law the-plane-has-no-favoured-place + (forall [w (Set (Tuple Int Int)), dx Int, dy Int] + (= (step (shifted dx dy w)) + (shifted dx dy (step w))))) + +;; --- whole generations, on crowded worlds ----------------------------------------- (defn next-generation [world] (if (empty? world) @@ -30,37 +69,23 @@ (let [xs (map first world) ys (map second world)] (set (for [x (range (dec (apply min xs)) (+ 2 (apply max xs))) y (range (dec (apply min ys)) (+ 2 (apply max ys))) - :let [n (touching world x y)] - :when (if (contains? world [x y]) (<= 2 n 3) (= n 3))] + :when (alive-by-the-rule? world [x y])] [x y]))))) (defn packed [world] (set (map (fn [[x y]] [(mod x 6) (mod y 6)]) world))) -(defn shifted [dx dy world] (set (map (fn [[x y]] [(+ x dx) (+ y dy)]) world))) - -;; --- laws ------------------------------------------------------------------------ - -(law neighbours-are-the-eight-cells-around - (forall [x Int, y Int] - (= (neighbours [x y]) - (set (for [dx [-1 0 1] dy [-1 0 1] :when (not= 0 dx dy)] [(+ x dx) (+ y dy)]))))) - -(law neighbours-names-each-once - (forall [x Int, y Int] (= 8 (count (neighbours [x y]))))) - (defn follows-the-rule? "`world` stepped to `next`, and the rule says it steps to `by-rule`." [world next by-rule] (= next by-rule)) (law a-generation-follows-the-rule + {:require :tested + :because "it samples crowded worlds so its tests reach births and deaths; the rule itself is proved cell by cell in a-cell-lives-by-the-rule"} (forall [w (Set (Tuple Int Int))] (follows-the-rule? (packed w) (step (packed w)) (next-generation (packed w))))) -(law the-plane-has-no-favoured-place - (forall [w (Set (Tuple Int Int)), dx Int, dy Int] - (= (step (shifted dx dy (packed w))) - (shifted dx dy (step (packed w)))))) +;; --- the famous patterns ---------------------------------------------------------- (def block #{[0 0] [1 0] [0 1] [1 1]}) (def blinker #{[0 1] [1 1] [2 1]}) diff --git a/examples/test/life/core_test.clj b/examples/test/life/core_test.clj index beb137a..c38c848 100644 --- a/examples/test/life/core_test.clj +++ b/examples/test/life/core_test.clj @@ -13,10 +13,23 @@ (let [r (spec/check 'life.core-spec)] (is (:ok r) (:message r)))) +(deftest the-readable-life-is-proved + (let [r (spec/check 'life.core-spec {:seed 42}) + status (fn [l] (:status (first (filter #(= l (:law %)) (:laws r)))))] + (doseq [l '[neighbours-are-the-eight-cells-around neighbours-names-each-once + a-cell-lives-by-the-rule the-plane-has-no-favoured-place]] + (is (= :proved (status l)) (str l))))) + (deftest the-fast-life-meets-the-same-spec - (let [r (spec/check 'life.core-spec {:target 'life.fast})] - (is (:ok r) (:message r)) - (is (= 'life.fast (:target r))))) + (testing "it counts with frequencies, outside the prover, so it is tested, not proved" + (let [r (spec/check 'life.core-spec {:target 'life.fast :require :tested})] + (is (:ok r) (:message r)) + (is (= 'life.fast (:target r)))))) + +(deftest a-favoured-place-is-refuted + (let [r (check 'life.broken.origin)] + (is (not (:ok r))) + (is (str/includes? (:message r) "law `the-plane-has-no-favoured-place` fails for")))) (deftest highlife-is-not-life (let [r (check 'life.broken.highlife)] diff --git a/examples/test/pong/ball_draft_spec.clj b/examples/test/pong/ball_draft_spec.clj index dea1c95..a926ca2 100644 --- a/examples/test/pong/ball_draft_spec.clj +++ b/examples/test/pong/ball_draft_spec.clj @@ -5,12 +5,17 @@ adequacy check tries exactly that stand-in and reports the gap. core_spec.clj closes it with `in-open-court-the-ball-travels-at-its-velocity`." (:require [pong.core :refer [W H PH LEFT-X]] - [writ.spec :refer [spec ann law]])) + [writ.spec :refer [spec ann graph law]])) (spec pong.core) (ann advance [(Tuple Int Int Int Int) Int Int -> (Tuple Int Int Int Int)]) +;; a draft: the ball goes on being a ball, and nothing more is said here +(graph ball + {:states {:ball (Tuple Int Int Int Int)} + :edges {:ball {[advance Int Int] #{:ball}}}}) + (defn court-paddle [y] (mod y (inc (- H PH)))) (defn court-ball [x y dx dy] diff --git a/examples/test/pong/core_spec.clj b/examples/test/pong/core_spec.clj index 5cfc184..25d6130 100644 --- a/examples/test/pong/core_spec.clj +++ b/examples/test/pong/core_spec.clj @@ -1,20 +1,31 @@ (ns pong.core-spec - "The contract for pong.core: what pong is, stated for every position on - the court rather than for a few rallies. - - Generated Ints fall anywhere, so the laws build their games through - `court-ball`, `court-paddle` and `game-of`, which fold any Int onto the - court. Every trial is then a position the game can really be in, and no - `=>` premise starves for lack of inputs." + "The contract for pong.core: its state graph, and what each step means. + + A game is [phase ball left-y right-y left-score right-score]. Its parts + are refinements -- a Paddle is a row a paddle can be on, a Ball one on + the court at a pace it can have -- so every generated game is one the + game can be in, and the prover assumes as much. The graph's states are + the four phases of a game; each edge is proved from the code, so every + run of `step` stays inside the graph and keeps its rules." (:require [pong.core :refer [W H PH LEFT-X RIGHT-X WIN]] - [writ.spec :refer [spec data ann law]])) + [writ.spec :refer [spec data ann refine graph law]])) -(spec pong.core) +(spec pong.core {:require :proved}) (data Side Left Right) (data Phase (Serving Nat) Playing Paused (Won Side)) (data Key Idle Up Down Pause) +;; --- the parts of a game --------------------------------------------------------- + +(refine Paddle [y Int] (<= 0 y (- H PH))) +(refine Row [y Int] (<= 0 y (dec H))) +(refine Column [x Int] (<= 0 x (dec W))) +(refine Pace [dx Int] (<= 1 (abs dx) 3)) +(refine Spin [dy Int] (<= -2 dy 2)) +(refine Ball [b (Tuple Column Row Pace Spin)] true) +(refine Score [s Nat] (< s WIN)) + (ann move-paddle [Int Key -> Int]) (ann track [Int Int -> Int]) (ann advance [(Tuple Int Int Int Int) Int Int -> (Tuple Int Int Int Int)]) @@ -25,140 +36,121 @@ (ann step [(Tuple Phase (Tuple Int Int Int Int) Int Int Nat Nat) Key -> (Tuple Phase (Tuple Int Int Int Int) Int Int Nat Nat)]) -;; --- the court, in the spec's own terms -------------------------------------- - -(defn court-paddle [y] (mod y (inc (- H PH)))) +;; --- the game's states ----------------------------------------------------------- -(defn court-ball - "A ball on the court: across by 1 to 3 cells a tick, up or down by at most 2." - [x y dx dy] - (let [s (inc (mod (abs dx) 3))] - [(mod x W) (mod y H) (if (neg? dx) (- s) s) (- (mod dy 5) 2)])) - -(defn game-of [phase x y dx dy ly ry ls rs] - [phase (court-ball x y dx dy) (court-paddle ly) (court-paddle ry) (mod ls WIN) (mod rs WIN)]) - -(defn paddle-ok? [y] (<= 0 y (- H PH))) +(defn phase-of [game] (first (first game))) -(defn under? [paddle-y y] (and (<= paddle-y y) (< y (+ paddle-y PH)))) +(defn scores [game] (let [[_ _ _ _ ls rs] game] [ls rs])) -(defn on-court? [[x y dx dy]] - (and (<= 0 x (dec W)) (<= 0 y (dec H)) (<= 1 (abs dx) 3) (<= (abs dy) 2))) +(refine Live [g (Tuple Phase Ball Paddle Paddle Score Score)] (not= :Won (phase-of g))) -(defn valid-game? [[phase ball ly ry ls rs]] - (and (paddle-ok? ly) (paddle-ok? ry) (<= ls WIN) (<= rs WIN) - (or (= :Won (first phase)) (on-court? ball)))) +(refine Serving [g Live] (= :Serving (phase-of g))) +(refine Playing [g Live] (= :Playing (phase-of g))) +(refine Paused [g Live] (= :Paused (phase-of g))) +(refine Won [g (Tuple Phase (Tuple Int Int Int Int) Paddle Paddle Nat Nat)] + (let [[phase _ _ _ ls rs] g] + (and (= :Won (first phase)) (<= ls WIN) (<= rs WIN) (or (= ls WIN) (= rs WIN))))) -(defn phase-of [game] (first (first game))) -(defn scores [game] (drop 4 game)) +(graph pong + {:start [:serving (new-game)] + :states {:serving Serving, :playing Playing, :paused Paused, :won Won} + :edges {:serving {[step Key] #{:serving :playing :paused}} + :playing {[step Key] #{:playing :paused :serving :won}} + :paused {[step Key] #{:paused :playing}} + :won {[step Key] #{:won :serving}}} + :before [[:playing :won]]}) ;; --- paddles ------------------------------------------------------------------- (law a-paddle-never-leaves-the-court - (forall [y Int, k Key] (paddle-ok? (move-paddle y k)))) + (forall [y Int, k Key] (Paddle? (move-paddle y k)))) (law up-and-down-move-two-rows-to-the-wall - (forall [y Int] - (and (= (move-paddle (court-paddle y) [:Up]) (max 0 (- (court-paddle y) 2))) - (= (move-paddle (court-paddle y) [:Down]) (min (- H PH) (+ (court-paddle y) 2))) - (= (move-paddle (court-paddle y) [:Idle]) (court-paddle y))))) + (forall [y Paddle] + (and (= (move-paddle y [:Up]) (max 0 (- y 2))) + (= (move-paddle y [:Down]) (min (- H PH) (+ y 2))) + (= (move-paddle y [:Idle]) y)))) + +(defn gap [p ball-y] (abs (- (+ p (quot PH 2)) ball-y))) (defn closer-by-one? [p p2 ball-y] - (let [gap (fn [q] (abs (- (+ q (quot PH 2)) ball-y)))] - (and (paddle-ok? p2) (<= (abs (- p2 p)) 1) - (<= (gap p2) (gap p)) - (or (zero? (gap p)) (not (< 0 p (- H PH))) (< (gap p2) (gap p)))))) + (and (Paddle? p2) (<= (abs (- p2 p)) 1) + (<= (gap p2 ball-y) (gap p ball-y)) + (or (zero? (gap p ball-y)) (not (< 0 p (- H PH))) (< (gap p2 ball-y) (gap p ball-y))))) (law the-cpu-paddle-closes-on-the-ball - (forall [y Int, by Int] - (closer-by-one? (court-paddle y) (track (court-paddle y) (mod by H)) (mod by H)))) + (forall [y Paddle, by Row] (closer-by-one? y (track y by) by))) ;; --- the ball -------------------------------------------------------------------- -(defn pace-kept? [[_ _ dx _] [_ y2 dx2 dy2]] - (and (= (abs dx) (abs dx2)) (<= (abs dy2) 2) (<= 0 y2 (dec H)))) +(defn pace-kept? [b b2] + (let [[_ _ dx _] b + [_ y2 dx2 dy2] b2] + (and (= (abs dx) (abs dx2)) (Spin? dy2) (Row? y2)))) (law the-ball-stays-between-the-walls-at-its-pace - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int] - (pace-kept? (court-ball x y dx dy) - (advance (court-ball x y dx dy) (court-paddle ly) (court-paddle ry))))) + (forall [b Ball, ly Paddle, ry Paddle] (pace-kept? b (advance b ly ry)))) -(defn open-court? [[x y dx dy]] - (and (< (+ LEFT-X 3) x (- RIGHT-X 3)) (< 2 y (- H 3)))) +(defn open-court? [b] + (let [[x y _ _] b] + (and (< (+ LEFT-X 3) x (- RIGHT-X 3)) (< 2 y (- H 3))))) (law in-open-court-the-ball-travels-at-its-velocity - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int] - (=> (open-court? (court-ball x y dx dy)) - (= (advance (court-ball x y dx dy) (court-paddle ly) (court-paddle ry)) - (let [[x y dx dy] (court-ball x y dx dy)] [(+ x dx) (+ y dy) dx dy]))))) + (forall [b Ball, ly Paddle, ry Paddle] + (=> (open-court? b) + (= (advance b ly ry) + (let [[x y dx dy] b] [(+ x dx) (+ y dy) dx dy]))))) + +(defn under? [paddle-y y] (and (<= paddle-y y) (< y (+ paddle-y PH)))) ;; A paddle is a wall on its own rows: a ball in front of it is still in ;; front after a tick, unless it went by on a row the paddle does not cover. ;; However fast the ball, it cannot jump the paddle. -(defn held-by-left? [paddle-y _before [x2 y2]] - (or (> x2 LEFT-X) (not (under? paddle-y y2)))) +(defn held-by-left? [paddle-y b2] + (let [[x2 y2] b2] (or (> x2 LEFT-X) (not (under? paddle-y y2))))) (law the-left-paddle-stops-the-ball - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int] - (=> (> (first (court-ball x y dx dy)) LEFT-X) - (held-by-left? (court-paddle ly) (court-ball x y dx dy) - (advance (court-ball x y dx dy) (court-paddle ly) (court-paddle ry)))))) + (forall [b Ball, ly Paddle, ry Paddle] + (=> (> (first b) LEFT-X) (held-by-left? ly (advance b ly ry))))) -(defn held-by-right? [paddle-y _before [x2 y2]] - (or (< x2 RIGHT-X) (not (under? paddle-y y2)))) +(defn held-by-right? [paddle-y b2] + (let [[x2 y2] b2] (or (< x2 RIGHT-X) (not (under? paddle-y y2))))) (law the-right-paddle-stops-the-ball - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int] - (=> (< (first (court-ball x y dx dy)) RIGHT-X) - (held-by-right? (court-paddle ry) (court-ball x y dx dy) - (advance (court-ball x y dx dy) (court-paddle ly) (court-paddle ry)))))) + (forall [b Ball, ly Paddle, ry Paddle] + (=> (< (first b) RIGHT-X) (held-by-right? ry (advance b ly ry))))) (law a-serve-goes-to-the-side-named (and (neg? (nth (serve [:Left]) 2)) (pos? (nth (serve [:Right]) 2)) - (on-court? (serve [:Left])) (on-court? (serve [:Right])))) + (Ball? (serve [:Left])) (Ball? (serve [:Right])))) ;; --- the game -------------------------------------------------------------------- -(law a-game-starts-level-and-serving - (and (= [0 0] (scores (new-game))) (= :Serving (phase-of (new-game))) - (valid-game? (new-game)))) - -(law every-tick-leaves-a-game-that-can-be - (forall [p Phase, x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat, k Key] - (valid-game? (step (game-of p x y dx dy ly ry ls rs) k)))) +(law a-game-starts-level (= [0 0] (scores (new-game)))) -(defn one-point-at-most? [[a b] [a2 b2]] - (and (<= a a2) (<= b b2) (<= (+ a2 b2) (inc (+ a b))))) +(defn one-point-at-most? [before after] + (let [[a b] before [a2 b2] after] + (and (<= a a2) (<= b b2) (<= (+ a2 b2) (inc (+ a b)))))) (law a-tick-scores-at-most-one-point - (forall [p Phase, x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat, k Key] - (=> (not= :Won (first p)) - (one-point-at-most? (scores (game-of p x y dx dy ly ry ls rs)) - (scores (step (game-of p x y dx dy ly ry ls rs) k)))))) + (forall [g Live, k Key] (one-point-at-most? (scores g) (scores (step g k))))) (law the-game-is-won-exactly-at-WIN - (forall [p Phase, x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat, k Key] - (=> (not= :Won (first p)) - (= (= :Won (phase-of (step (game-of p x y dx dy ly ry ls rs) k))) - (boolean (some #(>= % WIN) (scores (step (game-of p x y dx dy ly ry ls rs) k)))))))) + (forall [g Live, k Key] + (= (= :Won (phase-of (step g k))) + (let [[ls rs] (scores (step g k))] (or (= ls WIN) (= rs WIN)))))) (law pausing-twice-changes-nothing - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat] - (= (step (step (game-of [:Playing] x y dx dy ly ry ls rs) [:Pause]) [:Pause]) - (game-of [:Playing] x y dx dy ly ry ls rs)))) + (forall [g Playing] (= (step (step g [:Pause]) [:Pause]) g))) (law a-paused-game-stands-still - (forall [x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat, k Key] - (=> (not= :Pause (first k)) - (= (step (game-of [:Paused] x y dx dy ly ry ls rs) k) - (game-of [:Paused] x y dx dy ly ry ls rs))))) + (forall [g Paused, k Key] (=> (not= :Pause (first k)) (= (step g k) g)))) (law a-serve-counts-down - (forall [n Nat, x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat, k Key] + (forall [g Serving, k Key] (=> (not= :Pause (first k)) - (= (phase-of (step (game-of [:Serving n] x y dx dy ly ry ls rs) k)) - (if (pos? n) :Serving :Playing))))) + (= (phase-of (step g k)) + (if (pos? (second (first g))) :Serving :Playing))))) (law pause-after-a-win-starts-over - (forall [s Side, x Int, y Int, dx Int, dy Int, ly Int, ry Int, ls Nat, rs Nat] - (= (step (game-of [:Won s] x y dx dy ly ry ls rs) [:Pause]) (new-game)))) + (forall [g Won] (= (step g [:Pause]) (new-game)))) diff --git a/examples/test/pong/core_test.clj b/examples/test/pong/core_test.clj index 5749d5f..881cb92 100644 --- a/examples/test/pong/core_test.clj +++ b/examples/test/pong/core_test.clj @@ -22,13 +22,19 @@ "the spec does not pin down `advance`: every law still holds when it returns its argument `ball` unchanged") "...and still the spec is too weak"))) +(deftest pong-is-proved + (let [r (spec/check 'pong.core-spec {:seed 42 :adequacy false})] + (is (= (:laws (:proof r)) (+ (:proved (:proof r)))) (:message r)) + (is (str/includes? (:message r) "graph `pong`: 4 edges proved")))) + (deftest a-fast-ball-cannot-jump-the-paddle (let [r (check 'pong.broken.tunnel)] (is (not (:ok r))) (is (str/includes? (:message r) "law `the-left-paddle-stops-the-ball` fails for")) - (testing "the counterexample is shrunk to a ball two cells from the paddle" - (is (str/includes? (:message r) "(court-ball x y dx dy) => [3 44 -2 -2]")) - (is (str/includes? (:message r) "=> [1 42 -2 -2]"))))) + (testing "no test finds it; the solver does, with a ball two cells from the paddle" + (is (str/includes? (:message r) "b = [3 3 -2 0]")) + (is (str/includes? (:message r) "(advance b ly ry) => [1 3 -2 0]")) + (is (str/includes? (:message r) "found by the solver"))))) (deftest a-phase-step-forgets-is-caught-before-anything-runs (let [r (check 'pong.broken.forgot-pause)] diff --git a/examples/test/shortener/core_spec.clj b/examples/test/shortener/core_spec.clj index 929079d..a6ecc1a 100644 --- a/examples/test/shortener/core_spec.clj +++ b/examples/test/shortener/core_spec.clj @@ -13,7 +13,7 @@ `store-of` shortens a generated list of URLs into an empty store." (:require [clojure.string :as str] [shortener.core :refer [handle]] - [writ.spec :refer [spec data ann law calls]])) + [writ.spec :refer [spec data ann refine graph law calls]])) (spec shortener.core) @@ -31,6 +31,24 @@ (ann handle [(Map String String) Keyword String String -> (Tuple (Map String String) Reply)]) +;; --- the state graph --------------------------------------------------------------- + +;; what encode-id hands out: one to eleven letters and digits +(refine Code [s String] (boolean (re-matches #"[0-9a-zA-Z]{1,11}" s))) + +(graph shortener + {:states {:id Nat, :code Code, :text String, :url String, :verdict Bool, + :method Keyword, :route Route, + :links (Map String String), :reply Reply, + :result (Tuple (Map String String) Reply)} + :edges {:id {[encode-id] #{:code}} + :text {[decode-id] #{:id}, [valid-code?] #{:verdict}} + :url {[normalize-url] #{:url}, [valid-url?] #{:verdict}} + :method {[route String] #{:route}} + :links {[shorten String] #{:result} + [follow String] #{:reply} + [handle Keyword String String] #{:result}}}}) + ;; --- the call graph ------------------------------------------------------------ (calls handle [route shorten follow]) From cac66280c1eebfe47a39c602dba12df3289ec9a5 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 20:12:37 -0400 Subject: [PATCH 7/8] Document graphs, refinements, the solver and the proof namespace --- README.md | 210 +++++++++++++++++++++++++++++++++++++++---- skills/writ/SKILL.md | 103 +++++++++++++++++++-- 2 files changed, 287 insertions(+), 26 deletions(-) diff --git a/README.md b/README.md index 4a4ee1a..f1c1dd3 100644 --- a/README.md +++ b/README.md @@ -5,11 +5,12 @@ is the problem statement written so a machine can check it: signatures for the public functions, and laws that say what their results mean. It lives in its own namespace, and the code never mentions writ. -It is built for code an LLM writes. A person writes the spec, which is the -intent. The agent writes the implementation. writ is the gate between -them. Its report says what to fix: the rule that was broken, or the law -that failed, the smallest input that fails it, and the value each side -produced. +It is built for code an LLM writes. The spec is the intent: the problem's +states, the steps between them, and what each step means. An agent, or a +person, writes it first; then the implementation. writ is the gate +between them. Its report says what to fix: the rule that was broken, or +the law that failed, the smallest input that fails it, and the value each +side produced. A spec is not a test suite. Tests pin down examples: this input gives that output. A spec states what must hold for every input: the output is @@ -20,9 +21,15 @@ laws don't pin down, naming a trivial stand-in that would pass. The static rules come from [Bend](https://github.com/HigherOrderCO/Bend): pure code only, recursion that provably terminates, definitions in order, -types that fit. Behaviour is checked by running the laws, through -[test.check](https://github.com/clojure/test.check), against inputs -generated from the spec's types. +types that fit. Behaviour is checked two ways. The laws run, through +[test.check](https://github.com/clojure/test.check), on inputs generated +from the spec's types. And writ proves them from the code: by rewriting +and induction, or by running the code on symbolic values and handing the +result to a solver. A proof holds for every input, not the ones a test +happened to try. Every proof is replayed by a small checker before it is +reported, and the solver's answers come with certificates that checker +verifies, so the search is never trusted. The report says which laws are +proved and which are only tested, and a spec can demand proof. writ runs on [jolt](https://github.com/jolt-lang/jolt). @@ -30,15 +37,21 @@ writ runs on [jolt](https://github.com/jolt-lang/jolt). ``` src/my/sort.clj the implementation: plain Clojure, no writ -test/my/sort_spec.clj the contract: spec, data, ann, law +test/my/sort_spec.clj the contract: spec, graph, refine, ann, law +test/my/sort_proof.clj optional: lemmas and hints that help the prover test/my/sort_test.clj runs the check ``` -1. Write the spec. It names the namespace it constrains, signs the public - fns and states what they mean. This is the part a person owns. -2. The agent writes the implementation as ordinary Clojure. -3. Run the check. If it fails, hand the report back to the agent and repeat. -4. Keep the check in the test suite, so it gates every change. +1. Declare the state graph. Every spec has one: the problem's states, as + types -- refinements most often -- and the fns that step between them. + It is the first thing a spec says, and writ proves each of its edges. +2. State what each step means, as laws, and ask for proof with + `(spec my.sort {:require :proved})`. +3. Write the implementation as ordinary Clojure. +4. Run the check. If it fails, the report says what to fix. If a law holds + but is not proved, help the prover with a lemma or a hint in the proof + namespace; don't weaken the law. +5. Keep the check in the test suite, so it gates every change. writ is a test dependency. The spec and the check live on the test classpath, so production code never loads writ. @@ -80,13 +93,18 @@ The spec: ```clojure (ns my.sort-spec - (:require [writ.spec :refer [spec ann law]])) + (:require [writ.spec :refer [spec ann law graph]])) -(spec my.sort) +(spec my.sort {:require :proved}) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +;; the problem's data flow: a list goes in, a sorted list comes out +(graph sorting + {:states {:unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}}}}) + (defn ascending? [xs] (or (empty? xs) (apply <= xs))) @@ -370,6 +388,70 @@ spec has `calls` forms: with "it uses `f`, which writ cannot check", so one effect deep in a call chain shows up at every caller above it. +### Refinements + +A refinement is a type and a predicate: + +```clojure +(refine Paddle [y Int] (<= 0 y (- H PH))) +(refine Ball [b (Tuple Column Row Pace Spin)] true) +(refine Green [l (Tuple Keyword Nat)] (and (= :Green (first l)) (<= (second l) GREEN))) +``` + +It goes wherever a type goes: in an `ann`, a `forall`, a graph's states, +another refinement. Its values are generated to satisfy it -- an integer +range is found once and sampled near its bounds and the spec's own +numbers, where code tends to break -- so a law never folds random inputs +into shape. The prover takes the predicate as a hypothesis, and the +static check sees the base type. `refine` also defines the predicate, as +`Paddle?`, for laws to use. + +### The state graph + +Every spec declares its graph, and it comes first. Its states are types; +its edges are the fns that step between them: + +```clojure +(graph signal + {:start [:green [:Green 0]] + :states {:green Green, :yellow Yellow, :red Red} + :edges {:green {[tick] #{:green :yellow}} + :yellow {[tick] #{:yellow :red}} + :red {[tick] #{:red :green}}} + :before [[:yellow :red]]}) +``` + +An edge's key is the fn and the types of the arguments after the state: +`[move-paddle Key]` is `(move-paddle state key)` for every `Key`. writ +checks the graph three ways: + +- **Data flow.** Each edge's fn must take its state's type and return its + targets' type, by its `ann`. +- **Each edge is a law.** An edge into refinements is an obligation named + for the graph, the state and the fn, `signal:yellow:tick`, run and + proved like any law: the fn takes every value of its state into one of + the states it names, and it never throws. A step that breaks it is + reported with the state it breaks on: + + ``` + law `signal:yellow:tick` fails for + l = [:Yellow 5] + a tick from yellow must land in yellow or red + ``` +- **The graph's own rules.** `:start` names a state, or `[state value]` + with a value in it; every state must be reachable from it; `:final` + states must be reachable from every state; `:never [a b]` says no path + leads from a to b, and `:before [a b]` that every path from the start + to b passes a. With every edge proved, these hold for every run of the + code, not only for the table. + +A spec for plain functions has a graph too: its states are the data the +problem moves through, and an edge into plain types is data flow only, +checked against the signatures. pong's graph has four states, one per +phase of a game, each a refinement of the game's tuple; its four edges +are proved from the code, so no sequence of key presses ever takes a +game out of them. + ### Machines Some code is a state machine: a screen flow, a protocol, an order's @@ -499,7 +581,16 @@ replays a run (default random, reported per law), and `:max-size` is the largest generated size (default 50). `:adequacy false` skips the third stage, for example while a spec is still being written, and `:prove false` skips the prover. `:require` sets the evidence every law -needs, in place of the spec's own. +needs, in place of the spec's own. `:proof` names the proof namespace +(`false` for none), and `:fuel` gives the prover more rewrites per +attempt. + +Proofs are cached in `.writ-cache/`, one file per spec. A cached proof is +used only when the law, its hint and lemmas, and the source of the code, +the spec, the proof namespace and writ itself are all exactly as they +were when it was found and checked, so a check that changes nothing +proves nothing again. `:cache false` turns it off; `:cache-dir` puts it +elsewhere. Add `.writ-cache/` to `.gitignore`. ### Requiring proof @@ -538,6 +629,37 @@ A closed law that evaluates to true, and an `exists` law with a witness, count as proved: running pure, terminating code on fixed inputs decides them. +### The proof namespace + +When a law holds but the prover can't find its proof, it needs a lemma or +a hint, and those don't belong in the spec: the spec is the contract, and +lemmas are how it is proved. They go in the proof namespace, found by +name (`my.sort-proof` for `my.sort-spec`) or given as check's `:proof`: + +```clojure +(ns my.sort-proof + (:require [writ.spec :refer [proof-of lemma hint]])) + +(proof-of my.sort-spec) + +(lemma insert-keeps-sorted + (forall [x Nat, xs (List Nat)] + (=> (my.sort-spec/ascending? xs) (my.sort-spec/ascending? (insert x xs))))) + +(hint sorted {:induct xs :use [insert-keeps-sorted]}) +``` + +A lemma is a law about the code: it is tested, and it must be proved, or +the check fails. Once proved, the spec's laws may cite it. It is reported +apart, it counts toward no law of the spec, and the adequacy check never +judges a stand-in by it, so a lemma can't make a weak spec look strong. + +A hint steers the search and nothing more: `:induct` the variable to try +induction on first, `:use` the only lemmas and laws a proof may cite, +`:strategy` one of `:symbolic`, `:induction` or `:rewriting`, and `:fuel` +the rewrites one attempt may make. A proof a hint leads to is checked +like any other. + ### Proofs After a `forall` law passes its tests, writ tries to prove it from the @@ -639,7 +761,51 @@ The prover covers: `defn`s Anything else leaves the law tested, with `:unproved` saying why, for -example "outside the prover: the name `min`". +example "outside the prover: `frequencies`". + +### Symbolic evaluation and the solver + +Rewriting splits a goal at every `if`, and a step fn with a dozen +conditions makes thousands of cases. So writ also runs the code once, on +symbolic values, the way [Rosette](https://emina.github.io/rosette/) +does: both branches of an `if` run, and their values merge under its +test. Integers merge into one value defined once, vectors of one length +merge element by element, and a data value whose constructor depends on +the branch is kept as a union of guarded values. Data values are split +into their constructors first, so each case is a small formula. What +comes out is one formula: the law holds, and, for a graph's edges, the +code never throws. + +That formula goes to `writ.solve`, a solver written for writ in plain +Clojure: linear integer arithmetic (with `mod` and `quot` by a constant), +uninterpreted functions, and sets of unknown size as predicates. Two sets +are equal when an element the solver may choose is in both or neither, so +a law about every world of the Game of Life is one query: +`the-plane-has-no-favoured-place` is proved for every world, however +large, not sampled. The solver's search is not trusted. An unsatisfiable +formula comes with a certificate -- case splits down to Farkas +combinations, whose sums a few lines of arithmetic check -- and +`writ.solve.cert` verifies it, as the proof checker does for every step. + +When the solver finds the formula invalid, its model is a counterexample. +writ turns it back into Clojure values and runs the law on them; if the +law fails there, that is the report, even when no test found it: + +``` +law `the-left-paddle-stops-the-ball` fails for + b = [3 3 -2 0] + ly = 0 + ry = 4 + (held-by-left? ly (advance b ly ry)) => false + (advance b ly ry) => [1 3 -2 0] + (found by the solver, when no test did, and confirmed by running the code) +``` + +Symbolic evaluation covers the non-recursive code: arithmetic, `if`, +`case`, `let`, destructuring, vectors of known length, data values, sets +built from literals and sets of unknown size filtered, mapped by a +translation, or tested for membership, and calls of pure core fns on +literal data. Recursion is left to rewriting and induction. ### Which fns qualify @@ -778,7 +944,13 @@ of forms, and `writ.book/check-files` checks source files as one book. - `writ.prove`: the proof search; `writ.prove.term`, `writ.prove.rewrite` and `writ.prove.translate` hold the terms, the rewrite rules and the translation from Clojure; `writ.prove.scheme` the steps a proof is made - of, and `writ.prove.check` the checker that replays every proof + of, and `writ.prove.check` the checker that replays every proof; + `writ.prove.symbolic` runs code on symbolic values, and + `writ.prove.smt` hands open goals to the solver +- `writ.solve`: the certifying solver for linear integer arithmetic and + uninterpreted functions; `writ.solve.pre` turns formulas into clauses, + `writ.solve.search` and `writ.solve.simplex` search, and + `writ.solve.cert` checks certificates without searching - `writ.book`: runs every rule over a namespace's forms - `writ.check`: quantities, termination, ordering, effects, arity - `writ.types`: type checking and tagged data diff --git a/skills/writ/SKILL.md b/skills/writ/SKILL.md index ad99757..786916a 100644 --- a/skills/writ/SKILL.md +++ b/skills/writ/SKILL.md @@ -1,13 +1,15 @@ --- name: writ description: >- - Use when writing a writ spec -- the problem statement as checkable laws - about what code means and how it calls (writ.spec: - spec/ann/data/law/calls/machine) -- or the plain Clojure implementation it + Use when writing a writ spec -- the problem statement as a state graph + and checkable laws about what code means and how it calls (writ.spec: + spec/graph/refine/ann/data/law/calls/machine) -- or its proof namespace + (proof-of/lemma/hint), or the plain Clojure implementation it constrains, or when reading a writ.spec report or any "Writ:" error (purity, termination, ordering, arity, types, tagged data, - failing, vacuous or gapped laws, call graph mismatches). Also for the - annotated writ.defn surface (w/defn, ^:many, w/match, w/law, w/proof). + failing, unproved, vacuous or gapped laws, graph rules, call graph + mismatches). Also for the annotated writ.defn surface (w/defn, ^:many, + w/match, w/law, w/proof). --- # writ @@ -32,13 +34,61 @@ names what is wrong. writ runs on jolt; writ.spec uses test.check. - A report that fails is the next thing to fix. Read the whole message: it names the rule or law, the input, and the values. +## Writing a spec, in order + +1. `(spec my.ns {:require :proved})` -- the namespace it constrains; ask + for proof. +2. The state graph: the problem's states as types, refinements most + often, and the fns that step between them. Every spec has one; write + it before the laws. See [The state graph](#the-state-graph). +3. `ann` for each public fn. +4. Laws for what each step means. +5. Then the implementation. If a law holds but isn't proved, write a + lemma or hint in the proof namespace (see + [The proof namespace](#the-proof-namespace)); never weaken the law. + +## The state graph + +```clojure +(refine Green [l (Tuple Keyword Nat)] (and (= :Green (first l)) (<= (second l) GREEN))) +(refine Yellow [l (Tuple Keyword Nat)] (and (= :Yellow (first l)) (<= (second l) YELLOW))) +(refine Red [l (Tuple Keyword Nat)] (and (= :Red (first l)) (<= (second l) RED))) + +(graph signal + {:start [:green [:Green 0]] ; a state, or [state value] + :states {:green Green, :yellow Yellow, :red Red} + :edges {:green {[tick] #{:green :yellow}} ; [fn ArgType ...] -> targets + :yellow {[tick] #{:yellow :red}} + :red {[tick] #{:red :green}}} + :before [[:yellow :red]]}) ; also :never [[a b]], :final [s] +``` + +- `(refine Name [x Base] pred)` is a type: values of Base where pred + holds. Use it in `ann`, `forall`, states, other refinements. It defines + `Name?`. Refine the parts (a Paddle, a Ball) rather than folding random + Ints into range inside laws. +- Each edge's fn must fit by its `ann`: first param = the state's base + type, then the arg types; the return type = the targets' base type. +- An edge into refinements is a law named `graph:state:fn`: every value + of the state goes, by the fn, into one of the targets, and the fn never + throws. It is tested and proved like any law. +- An edge into plain types, like `{:unsorted {[isort] #{:sorted}}}` over + `(List Nat)`, is data flow only, checked against the signatures. A spec + of plain functions still has a graph: the data the problem moves + through. +- `:start`, `:final`, `:never`, `:before` are rules of the graph itself; + with every edge proved they hold for every run of the code. + ## A spec ```clojure (ns my.sort-spec - (:require [writ.spec :refer [spec data ann law]])) + (:require [writ.spec :refer [spec data ann law graph]])) -(spec my.sort) ; the namespace it constrains +(spec my.sort {:require :proved}) ; the namespace it constrains + +(graph sorting {:states {:unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}}}}) (ann insert [Nat (List Nat) -> (List Nat)]) ; one per public fn (ann isort [(List Nat) -> (List Nat)]) @@ -85,6 +135,35 @@ names what is wrong. writ runs on jolt; writ.spec uses test.check. count. clojure.core, host members, self-recursion and locals that shadow a fn do not. See [The call graph](#the-call-graph). +## The proof namespace + +When a law holds but isn't proved, add what the prover needs in +`my/sort_proof.clj` (found by name for `my.sort-spec`), not in the spec: + +```clojure +(ns my.sort-proof + (:require [writ.spec :refer [proof-of lemma hint]])) + +(proof-of my.sort-spec) + +(lemma insert-keeps-sorted ; a law about the code; must be proved + (forall [x Nat, xs (List Nat)] + (=> (my.sort-spec/ascending? xs) (my.sort-spec/ascending? (insert x xs))))) + +(hint sorted {:induct xs :use [insert-keeps-sorted]}) +``` + +- A lemma must hold and be proved, or the check fails; it then helps + prove the spec's laws. It never counts as one of them, and never + judges a stand-in, so it can't strengthen a weak spec. +- A hint: `:induct` a variable first, `:use` only these lemmas and laws, + `:strategy` `:symbolic` / `:induction` / `:rewriting`, `:fuel` more + rewrites. It only steers the search. +- The usual reasons a law isn't proved: recursion that needs a lemma about + a helper (write the lemma), a law about a recursive fn stated over its + whole output where a pointwise statement would do, or a form outside + the prover (the report names it; restate the law if you can). + ## Machines `(machine name {:step f :start s :transitions {s {e s'}} :final [..] @@ -256,6 +335,16 @@ law runs until it is fixed. After that, each law has a `:status`: A law written with modelled forms and the spec's own helpers is more likely to be proved. - `:witnessed`: an `exists` law, and a value was found. +- A failure "found by the solver, when no test did" is a real + counterexample: the solver found values that break the law, and running + the code on them confirmed it. Fix the code at those values. +- `graph `g`: ... ` lines: edges proved, and edges checked as data flow; + `graph `g` breaks its own rules` is the graph's own `:never`, `:before`, + `:final` or reachability failing; fix the graph or the code, whichever + is wrong, and say which. +- ``declares no state graph``: add the graph first. +- `:lemmas` in the report: the proof namespace's lemmas; each must be + `:proved`. - `:unproved`: the spec (`(spec ns {:require :proved})`) or the law (`{:require :proved}`) requires proof, and the law is only tested. Get it proved: restate it with forms the prover models, or add the lemma it From 6af2cd8460a1cbb466be06270fc2278765dc991e Mon Sep 17 00:00:00 2001 From: Yogthos Date: Wed, 23 Sep 2026 20:16:03 -0400 Subject: [PATCH 8/8] writ.spec: look harder for a rare refinement's values A won pong game needs its tag and an exact score together, and 200 tries sometimes found none, failing a law at random. Generation now tries 5000 times, and says which refinement starved if it still can't. --- src/writ/spec.clj | 16 ++++++++++++++-- test/writ/graph_test.clj | 4 ++++ test/writ/spec_demo/signal_spec.clj | 3 +++ 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index 107b515..c767a39 100644 --- a/src/writ/spec.clj +++ b/src/writ/spec.clj @@ -1499,6 +1499,18 @@ 'Keyword (set (filter keyword? lits)) 'String (set (filter string? lits))})) +(defn- such-that-opts + "How hard to look for a value of a refinement. A value can be rare -- + a tag and an exact score together -- so it tries many times, and says + which refinement starved if it still finds none." + [nm] + {:max-tries 5000 + :ex-fn (fn [_] (ex-info (str "writ could not generate a value of refinement `" nm + "`: its predicate rejected 5000 candidates. Refine its parts" + " (a refined field, a narrower base type) so values are built" + " to fit rather than filtered.") + {:writ/error true}))}) + (defn- refine-gen "Values of a refinement. An integer one is found once across a window and generated in its range, so a narrow range is never starved; any @@ -1513,7 +1525,7 @@ (empty? ok) (fail! "refinement `" name "` has no value between " (- int-window) " and " int-window) (or (= (first ok) (- int-window)) (= (peek ok) int-window)) - (gen/such-that pred (type->gen b tenv) 200) + (gen/such-that pred (type->gen b tenv) (such-that-opts name)) :else (let [lo (first ok) hi (peek ok) spread (if (= (count ok) (inc (- hi lo))) @@ -1529,7 +1541,7 @@ edges (vec (sort (filter ok-set (concat [(first ok) (peek ok)] (get-in tenv [::spec-ints] [])))))] (gen/frequency [[3 spread] [1 (gen/elements edges)]])))) - (gen/such-that pred (type->gen base (assoc tenv ::bias (::bias-of-refine tenv))) 200)))) + (gen/such-that pred (type->gen base (assoc tenv ::bias (::bias-of-refine tenv))) (such-that-opts name))))) (defn- type-env-of "The data types and refinements of a spec entry. Refinements sit under diff --git a/test/writ/graph_test.clj b/test/writ/graph_test.clj index cda9c71..1ab715c 100644 --- a/test/writ/graph_test.clj +++ b/test/writ/graph_test.clj @@ -108,3 +108,7 @@ (is (not (:ok r))) (is (= :failed (:status l)) (pr-str l)) (is (str/includes? (:message r) "l = [:Yellow 5]")))) + +(deftest a-rare-refinement-is-still-generated + (let [tenv (spec/type-env 'writ.spec-demo.signal-spec)] + (is (every? #(= [:Red 30] %) (spec/sample 'Stopped tenv 1000))))) diff --git a/test/writ/spec_demo/signal_spec.clj b/test/writ/spec_demo/signal_spec.clj index 8ac9a18..47691ab 100644 --- a/test/writ/spec_demo/signal_spec.clj +++ b/test/writ/spec_demo/signal_spec.clj @@ -24,3 +24,6 @@ (law a-light-counts-up-while-it-shows (forall [l Green] (=> (< (second l) GREEN) (= (tick l) [:Green (inc (second l))])))) + +;; a rare value: one tag and an exact count together, generated reliably +(refine Stopped [l (Tuple Keyword Nat)] (and (= :Red (first l)) (= RED (second l))))