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/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/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]) 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 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/solve.clj b/src/writ/solve.clj new file mode 100644 index 0000000..9df8f6e --- /dev/null +++ b/src/writ/solve.clj @@ -0,0 +1,136 @@ +(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 + "The value of integer term t in model m." + [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/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]))) diff --git a/src/writ/solve/search.clj b/src/writ/solve/search.clj new file mode 100644 index 0000000..7c2f686 --- /dev/null +++ b/src/writ/solve/search.clj @@ -0,0 +1,146 @@ +(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- 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: [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 + "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) from)] + (vswap! st assoc-in [:theory lits] r) + r))) + +(declare node) + +(defn- split + "Try l, then its negation." + [st assign cuts l tab] + (budget! st) + (let [neg (negate l) + 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 [neg] tab)] + (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 tab] + (budget! st) + (let [l (cert/cut assign terms) + 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)} + :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 fresh tab] + (let [clauses (:clauses @st) + [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 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)) 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 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 [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 new file mode 100644 index 0000000..45fab03 --- /dev/null +++ b/src/writ/solve/simplex.clj @@ -0,0 +1,185 @@ +(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- 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- 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 :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 {} (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 + 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)))) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index ec09337..c767a39 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." @@ -1419,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 @@ -1433,25 +1525,41 @@ (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) - (= (count ok) (inc (- (peek ok) (first ok)))) - (gen/choose (first ok) (peek ok)) - :else (gen/elements ok))) - (gen/such-that pred (type->gen base (assoc tenv ::bias (::bias-of-refine 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))) + ;; 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))) (such-that-opts name))))) (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 +1590,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 +1660,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 +1678,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 +1713,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 +1759,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 +1788,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 +1866,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 +1900,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 +1922,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 +1944,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 +1979,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 +2016,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 +2036,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 +2048,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 +2069,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 +2077,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..1ab715c 100644 --- a/test/writ/graph_test.clj +++ b/test/writ/graph_test.clj @@ -82,3 +82,33 @@ "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]")))) + +(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/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/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/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_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)))) 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 b136593..3370300 100644 --- a/test/writ/test_runner.clj +++ b/test/writ/test_runner.clj @@ -8,10 +8,14 @@ writ.spec-test writ.prove-test writ.evidence-test - writ.graph-test)) + writ.graph-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.check-test writ.book-test writ.gaps-test writ.spec-test writ.prove-test writ.evidence-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)]