diff --git a/README.md b/README.md index f1c1dd3..61a39e4 100644 --- a/README.md +++ b/README.md @@ -653,12 +653,38 @@ 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 lemma may be about clojure.core alone, such as what a bound on a list +says about a `filter` of it. + +A proof namespace may define helpers for its lemmas with `defn`, such as +an invariant the code keeps. The prover reads them as it reads the +target's, and a helper that refers to the target's fns reads those of +the target under check. + +A lemma's hypothesis may name a variable its conclusion doesn't. The +prover finds that variable's value in the facts of the goal at hand, the +way ACL2 does: + +```clojure +(lemma none-below + (forall [x Nat, v Nat, xs (List Nat)] + (=> (and (every? #(> % v) xs) (<= x v)) (= (filter #(< % x) xs) ())))) +``` + +rewrites `(filter #(< % x) r)` to `()` wherever the facts say every +element of `r` is above some `v` with `x <= v`. 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. +induction on first, `:vary` the other variables the induction hypothesis +holds at every value of (an accumulator a fold passes on), `: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. + +`writ.spec-demo.tree-proof` in the tests proves the tree's +`holds-a-sorted-set` this way: a `bst?` invariant, lemmas that `insert` +keeps it and that listing the tree after an insert is inserting into the +list, and a fold lemma with the tree varying. ### Proofs @@ -688,6 +714,11 @@ When a case still isn't closed, the prover tries two things: replaces the recursive call that brings in with a fresh variable, and proves that more general goal by an induction of its own. `permutation` is proved this way, with `(isort xs-t)` generalised. +- **Sorting.** On a list of integers, `(sort xs)` and + `(sort (distinct xs))` are a fold that inserts each element into the + sorted list so far: the elements below it, it, the elements above it + (at or above, when duplicates stay). `writ.prove.rewrite/model-check` + runs the model against `sort` itself. - **An accumulator.** A fold that grows an accumulator by addition from 0, as a `loop` or a `reduce`, is first proved to give acc plus the fold from 0, from any integer acc, by induction with acc left free in the @@ -695,7 +726,20 @@ When a case still isn't closed, the prover tries two things: A law proved earlier is a lemma for the laws after it: an equality rewrites its left side to its right, anything else rewrites to true, when -its hypotheses hold. The passes repeat until nothing new is proved, so a +its hypotheses hold. + +A lemma holds only at its own types, and the prover's logic is untyped, +as ACL2's is, so a type is a hypothesis like any other. Each term a +lemma's variable takes must be shown to be of the variable's type: a +variable of that type is; an integer term is an Int, and a Nat when it +can't be negative; anything else must satisfy the type's recognizer, +which the prover builds from the spec's `data` and takes values apart +with the way the type's cases do. A signature is only a claim, so before +the laws, the prover proves each signed fn's contract from its code, as +ACL2s's `defunc` does: given arguments of its parameter types, it returns +a value of its return type. Then `(insert x t)` is known to be a `Tree`. +A set, a map or a fn has no recognizer, and takes only a variable of its +own type. Contracts for `Nat` and `Int` returns aren't proved yet. The passes repeat until nothing new is proved, so a law may cite one that comes later in the spec. A law that is only tested is never cited. The report names what each proof used: diff --git a/skills/writ/SKILL.md b/skills/writ/SKILL.md index 786916a..2465e23 100644 --- a/skills/writ/SKILL.md +++ b/skills/writ/SKILL.md @@ -156,9 +156,14 @@ When a law holds but isn't proved, add what the prover needs in - 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. +- A lemma may be about clojure.core alone, and its hypothesis may name a + variable its conclusion doesn't: the prover takes it from the goal's + facts. `defn` helpers (an invariant such as `bst?`) may live in the + proof namespace too. +- A hint: `:induct` a variable first, `:vary [acc]` to let the induction + hypothesis hold at any acc (a fold's accumulator), `: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 diff --git a/src/writ/prove.clj b/src/writ/prove.clj index 045886e..c6df90a 100644 --- a/src/writ/prove.clj +++ b/src/writ/prove.clj @@ -12,8 +12,13 @@ A proof holds for every input on which the law's terms return, as with Typed Clojure; writ still runs every law, which catches the inputs where - a term throws. A proof that never unfolds one of the target's own - definitions says nothing about the code, and is not reported." + a term throws. The logic is untyped, as ACL2's is: a lemma, or a + hypothesis that varies, is used only at terms shown to be of its + variables' types -- by a recognizer, and by each signed fn's contract, + proved from its code before any law. A proof that never unfolds one of the target's own + definitions says nothing about the code, and is not reported -- unless + it proves a lemma of a proof namespace, which may be about clojure.core + alone." (:require [clojure.string :as str] [clojure.test.check.generators :as gen] [writ.prove.term :as t :refer [head]] @@ -233,15 +238,27 @@ :when p] {:by :generalizing :ih i :call call :as ys :ty ty :on (t/show call) :proof p})))) +(defn- varying + "The variables of opts' :vary, but v, with their types: they stay free + in an induction hypothesis on v." + [opts v] + (into {} (for [x (:vary opts) + :let [ty (get-in opts [:types x])] + :when (and ty (not= x v))] + [x ty]))) + (defn- by-induction [opts g v ty] (when-let [cs (cases v ty (:tenv opts))] - (let [steps (for [c cs] + (let [free (varying opts v) + opts (cond-> opts (seq free) (assoc :ih-free free)) + steps (for [c cs] (let [[opts* gi] (sc/induction-case opts g v c)] [c (or (prove-all opts* gi) (by-generalizing (dissoc opts* :ih-free) gi (keys (:types c))))]))] (when (every? (comp some? second) steps) - {:by :induction :on v :ty (plain ty) - :cases (mapv (fn [[c p]] {:case (:desc c) :proof p}) steps)})))) + (cond-> {:by :induction :on v :ty (plain ty) + :cases (mapv (fn [[c p]] {:case (:desc c) :proof p}) steps)} + (seq free) (assoc :vary free)))))) (defn- fuelled "f's result, or nil when it runs out of fuel." @@ -410,12 +427,24 @@ (swap! (:unfolded opts) into (mapcat second rs)) {:by :symbolic :certificates (mapv first rs)}))) +(defn- types-of + "The types a law's variables, its lemmas' and the signatures name." + [bs lemmas sigs] + (distinct (map plain (concat (map second bs) + (mapcat #(map second (first (split-foralls (:prop %)))) lemmas) + (mapcat (fn [[_ {:keys [params ret]}]] (cons ret params)) sigs))))) + +(defn- contract? [nm] (str/ends-with? (name nm) "%contract")) + (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}. + lemmas are the laws proved before it, as {:name :prop}; lemma, true + for a lemma of a proof namespace, which may be about clojure.core alone; + sigs, the target's signatures, {name {:params :ret}}; contracts, the + rules prove-contracts gave for them. Returns {:proved true :trace :summary :lemmas} or {:proved false :reason}." - [{:keys [prop defs tenv target own fuel lemmas rets total hint]}] + [{:keys [prop defs tenv target own fuel lemmas rets total hint lemma sigs contracts]}] (try (let [[bs0 body] (split-foralls prop) tctx (tr/context own) @@ -423,14 +452,17 @@ [bs g] (expand-tuples (map (fn [[x ty]] [x (plain ty)]) bs0) g0) unfolded (atom #{}) lemmas-used (atom #{}) + recs (sc/recognizers tenv (types-of bs lemmas sigs)) + defs (merge defs (:defs recs)) opts {:defs defs :tenv tenv :types (into {} (map (fn [[x ty]] [x (plain ty)])) bs) - :total total + :total total :vary (:vary hint) :recognizers recs :unfolded unfolded :fuel (or fuel 20000) :lemmas-used lemmas-used :rets (or rets {}) - :lemmas (vec (mapcat #(lemma-rules % defs tenv own) - (if-let [use (:use hint)] - (filter #(contains? (set use) (:name %)) lemmas) - lemmas)))} + :lemmas (into (vec (mapcat #(lemma-rules % defs tenv own) + (if-let [use (:use hint)] + (filter #(contains? (set use) (:name %)) lemmas) + lemmas))) + contracts)} ;; an attempt that runs out of fuel fails on its own; the others ;; still get their turn ran-out (atom false) @@ -478,16 +510,16 @@ [nil #{}])) target-used (filter #(= (str target) (namespace %)) used) ;; every proof is replayed by the checker before it is reported - checked (when (and trace (seq target-used)) + checked (when (and trace (or lemma (seq target-used))) (check/check-proof (dissoc opts :lemmas-used :unfolded) g trace))] (cond (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"} + (and (empty? target-used) (not lemma)) {: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))] + :else (let [cited (sort (remove #(or (contains? synthetic-lemmas %) (contract? %)) @lemmas-used))] {:proved true :trace trace :summary (str (summary trace) (when total ", and it never throws") @@ -499,15 +531,61 @@ (:writ.prove.rewrite/fuel (ex-data e)) {:proved false :reason "the search ran out of fuel"} :else (throw e))))) +(defn prove-contracts + "Prove each signed fn's contract, as defunc does: on arguments of its + parameter types, it returns a value of its return type -- where that + type has a recognizer to say so. A signature is only a claim; a + contract proved from the code is a fact, and a lemma's variable may take + a call of the fn as its value once the contract says the call is of the + variable's type. Passes repeat while one proves something new, so a fn + may lean on the contracts of the fns it calls. Each proof is replayed + by the checker. Returns the proved contracts as lemma rules." + [{:keys [defs tenv sigs fuel]}] + (let [recs (sc/recognizers tenv (types-of [] [] sigs)) + defs (merge defs (:defs recs)) + goals (into {} + (for [[f {:keys [params ret]}] (sort-by key sigs) + :let [d (get defs f) + c (get-in recs [:checks (plain ret)])] + :when (and (:params d) (= (count params) (count (:params d))) + (vector? c) (= :app (head c))) + :let [ps (mapv #(symbol (str "c%" %)) (range (count params))) + types (zipmap ps (map plain params)) + call (into [:app f] ps)]] + [f {:types types :ps ps + :g {:hyps [] :goals [(t/subst c {'%x call})]} + :rule {:name (symbol (str (name f) "%contract")) + :vars (set (map #(symbol (str "?" %)) ps)) + :types (into {} (map (fn [p] [(symbol (str "?" p)) (types p)])) ps) + :lhs (t/subst c {'%x (into [:app f] (map #(symbol (str "?" %)) ps))}) + :rhs [:lit true]}}])) + attempt (fn [rules {:keys [types ps g]}] + (let [opts {:defs defs :tenv tenv :types types :recognizers recs + :unfolded (atom #{}) :lemmas-used (atom #{}) :fuel (or fuel 20000) + :lemmas rules :rets {}} + trace (fuelled + #(or (some->> (prove-all opts g) (hash-map :by :cases :proofs)) + (first (keep (fn [p] (by-induction opts g p (types p))) ps))))] + (when (and trace (:ok (check/check-proof (dissoc opts :lemmas-used :unfolded) g trace))) + trace)))] + (loop [rules [] todo goals] + (let [done (into {} (keep (fn [[f x]] (when (attempt rules x) [f (:rule x)]))) todo)] + (if (empty? done) + rules + (recur (into rules (vals done)) (apply dissoc todo (keys done)))))))) + (defn definitions "Translate the defns of the target and the spec: [defs own]. pairs is - [[ns-sym forms] ...]; each ns reads its own plain names first." + [[ns-sym forms] ...] or [[ns-sym forms refers] ...]; each ns reads its + own plain names first, then the plain names in refers, name -> + qualified name." [pairs] - (let [qualified (into {} (for [[k v] (tr/own-names pairs) :when (namespace k)] [k v])) + (let [qualified (into {} (for [[k v] (tr/own-names (map #(take 2 %) pairs)) :when (namespace k)] [k v])) defs (into {} - (for [[ns-sym forms] pairs] - (let [own (merge qualified (into {} (for [[k v] (tr/own-names [[ns-sym forms]]) - :when (nil? (namespace k))] - [k v])))] + (for [[ns-sym forms refers] pairs] + (let [own (merge qualified refers + (into {} (for [[k v] (tr/own-names [[ns-sym forms]]) + :when (nil? (namespace k))] + [k v])))] (tr/defs-of (tr/context own) ns-sym forms))))] [defs qualified])) diff --git a/src/writ/prove/check.clj b/src/writ/prove/check.clj index f86aa53..86356fe 100644 --- a/src/writ/prove/check.clj +++ b/src/writ/prove/check.clj @@ -107,10 +107,16 @@ (reject! "an induction case cannot be proved " (pr-str (:by p)))))) (defn- check-induction - "Replay an induction on v: its cases must be the type's cases." - [opts g {:keys [on ty cases]}] + "Replay an induction on v: its cases must be the type's cases. A + variable that varies in the hypothesis must be one of the goal's, at its + own type." + [opts g {:keys [on ty cases vary]}] (let [cs (or (sc/cases on ty (:tenv opts)) (reject! "`" on "` is not of an inductive type")) - declared (get-in opts [:types on])] + declared (get-in opts [:types on]) + _ (doseq [[x xty] vary] + (when (or (= x on) (not= xty (get-in opts [:types x]))) + (reject! "`" x "` cannot vary in the hypothesis of an induction on `" on "`"))) + opts (cond-> opts (seq vary) (assoc :ih-free vary))] (when-not (= (sc/plain declared) ty) (reject! "induction on `" on "` as " (pr-str ty) " but it is " (pr-str declared))) (when-not (= (map :desc cs) (map :case cases)) diff --git a/src/writ/prove/rewrite.clj b/src/writ/prove/rewrite.clj index cbe1260..d9197eb 100644 --- a/src/writ/prove/rewrite.clj +++ b/src/writ/prove/rewrite.clj @@ -70,6 +70,8 @@ [:sq [:econs ?h [:elems [:call filter ?f [:sq ?E]]]]] [:call filter ?f [:sq ?E]]]] [filter-elems [:call filter ?f [:sq [:elems ?v]]] [:call filter ?f ?v]] + [filter-app [:call filter ?f [:sq [:eapp ?A ?B]]] + [:sq [:eapp [:elems [:call filter ?f [:sq ?A]]] [:elems [:call filter ?f [:sq ?B]]]]]] [map-nil [:call map ?f [:nil]] [:sq [:enil]]] [map-empty [:call map ?f [:sq [:enil]]] [:sq [:enil]]] [map-cons [:call map ?f [:sq [:econs ?h ?E]]] @@ -118,6 +120,8 @@ [every-cons [:call every? ?f [:sq [:econs ?h ?E]]] [:if [:ap ?f ?h] [:call every? ?f [:sq ?E]] [:lit false]]] [every-elems [:call every? ?f [:sq [:elems ?v]]] [:call every? ?f ?v]] + [every-app [:call every? ?f [:sq [:eapp ?A ?B]]] + [:if [:call every? ?f [:sq ?A]] [:call every? ?f [:sq ?B]] [:lit false]]] [some-nil [:call some ?f [:nil]] [:nil]] [some-empty [:call some ?f [:sq [:enil]]] [:nil]] [some-cons [:call some ?f [:sq [:econs ?h ?E]]] @@ -415,24 +419,59 @@ (declare boolean-term?) +(def ^:private selecting-fns + "clojure.core fns whose value is made of parts of their data arguments + and nothing else: no float in, no float out. A fn argument only picks + which parts." + '#{filter remove concat list vector vec cons rest next seq take drop reverse + sort distinct butlast first second last nth}) + (defn float-free? "Can this term's value hold no float? Then two syntactically equal - terms are =; with a NaN inside, Clojure's = says they are not." - [ctx x] - (cond - (int-term? ctx x) true - (boolean-term? x) true - (symbol? x) (float-free-type? ctx (get-in ctx [:types x])) - :else - (case (head x) - :nil true - :lit (not (float? (second x))) - :sq (float-free? ctx (second x)) - :enil true - :econs (and (float-free? ctx (nth x 1)) (float-free? ctx (nth x 2))) - :eapp (and (float-free? ctx (nth x 1)) (float-free? ctx (nth x 2))) - :elems (float-free? ctx (second x)) - false))) + terms are =; with a NaN inside, Clojure's = says they are not. A value + built only by picking and arranging parts of float-free values -- a + filter, a concat, a fold that does no more, a definition that does no + more -- has none either." + ([ctx x] (float-free? ctx x #{} #{})) + ([ctx x env seen] + (let [ff? #(float-free? ctx % env seen)] + (cond + (int-term? ctx x) true + (boolean-term? x) true + (symbol? x) (or (contains? env x) (float-free-type? ctx (get-in ctx [:types x]))) + :else + (case (head x) + :nil true + :bottom true + :lit (not (float? (second x))) + :sq (ff? (second x)) + :enil true + :econs (and (ff? (nth x 1)) (ff? (nth x 2))) + :eapp (and (ff? (nth x 1)) (ff? (nth x 2))) + :elems (ff? (second x)) + :if (and (ff? (nth x 2)) (ff? (nth x 3))) + :call (let [[_ f & args] x] + (cond + (contains? selecting-fns f) + (every? ff? (remove #(contains? #{:fn :cfn :dfn} (head %)) args)) + ;; a fold whose step makes its value of the accumulator's + ;; and the element's parts + (and (= 'reduce f) (= 3 (count args)) (= :fn (head (first args))) + (= 2 (count (second (first args))))) + (let [[[_ ps body] init coll] args] + (and (ff? init) (ff? coll) + (float-free? ctx body (into env ps) seen))) + :else false)) + ;; a definition's value, on float-free arguments, when its body + ;; makes it of their parts; a recursive call is taken to, which + ;; holds of every value the definition returns + :app (let [[_ f & args] x + d (get-in ctx [:defs f])] + (and (:params d) (= (count args) (count (:params d))) + (every? ff? args) + (or (contains? seen f) + (float-free? ctx (:body d) (set (:params d)) (conj seen f))))) + false))))) (defn- exact-scalar? "A value = compares by identity of value: two of them are = exactly when @@ -466,6 +505,10 @@ [:if [:call '= (nth ea 1) (nth eb 1)] [:call '= [:sq (nth ea 2)] [:sq (nth eb 2)]] [:lit false]] + ;; the same float-free elements first: the rest decides + (and (= :eapp (head ea)) (= :eapp (head eb)) (= (nth ea 1) (nth eb 1)) + (float-free? ctx (nth ea 1))) + [:call '= [:sq (nth ea 2)] [:sq (nth eb 2)]] (and (= a b) (float-free? ctx a)) [:lit true] :else nil)) (and (int-term? ctx a) (int-term? ctx b)) @@ -481,6 +524,28 @@ ;; --- computed rules -------------------------------------------------------------- +(defn- insert-sorted + "A fn value inserting x into a sorted list s of integers: the elements + below x, then x, then the elements above it -- or at and above it, when + duplicates are kept." + [above] + [:fn '[s x] [:call 'concat + [:call 'filter [:fn '[y] [:call '< 'y 'x]] 's] + [:call 'list 'x] + [:call 'filter [:fn '[y] [:call above 'y 'x]] 's]]]) + +(defn sort-model + "(sort xs) and (sort (distinct xs)) on a list of integers, as a fold + inserting each element into the sorted list so far. Only on integers: + two equal integers are the same value, so where an equal element goes + does not matter, and < orders them totally. nil when xs is not known + to hold integers." + [ctx a] + (let [dedup? (and (= :call (head a)) (= 'distinct (second a)) (= 3 (count a))) + xs (if dedup? (nth a 2) a)] + (when (int-elems? ctx xs) + [:call 'reduce (insert-sorted (if dedup? '> '>=)) [:sq t/enil] xs]))) + (defn- le [ctx a b] [:le (lin->term (lin+ (lin-of ctx b) (lin* -1 (lin-of ctx a))))]) @@ -654,6 +719,7 @@ (and (t/lit? a) (not (integer? (second a))))) [:lit false] :else nil)) reduce (when (= 3 n) (reduce-rule ctx a b (nth args 2))) + sort (when (= 1 n) (sort-model ctx a)) nth (when (and (<= 2 n 3) (t/int-lit? b)) (nth-rule a (second b) (if (= 3 n) (nth args 2) ::none))) nil))) @@ -708,21 +774,27 @@ when every guard left open is an integer comparison the prover can split on. An open test on the shape of an unknown value (seq xs, first t) means it is too early: the call stays folded until induction - or a split reveals that shape. Only the guards are normalised, never - the branches, so a recursive call inside a branch is not unfolded here." - [ctx body] - (if (= :if (head body)) - (let [c (normalize ctx (nth body 1)) - tr (truthiness ctx c)] - (cond - (true? tr) (settled? ctx (nth body 2)) - (false? tr) (settled? ctx (nth body 3)) - (and (= :call (head c)) (= 'not (second c))) - (settled? ctx [:if (nth c 2) (nth body 3) (nth body 2)]) - (splittable? c) (and (settled? (assume ctx c true) (nth body 2)) - (settled? (assume ctx c false) (nth body 3))) - :else false)) - true)) + or a split reveals that shape. Once a guard has been decided, an open + test of what a definition's call returns -- (and (bst? l) ...) after + the tag is known -- is not a shape: the call stays folded until its + own guards settle. Only the guards are normalised, never the + branches, so a recursive call inside a branch is not unfolded here." + ([ctx body] (settled? ctx body false)) + ([ctx body decided?] + (if (= :if (head body)) + (let [c (normalize ctx (nth body 1)) + tr (truthiness ctx c)] + (cond + (true? tr) (settled? ctx (nth body 2) true) + (false? tr) (settled? ctx (nth body 3) true) + (and (= :call (head c)) (= 'not (second c))) + (settled? ctx [:if (nth c 2) (nth body 3) (nth body 2)] decided?) + (splittable? c) (and (settled? (assume ctx c true) (nth body 2) decided?) + (settled? (assume ctx c false) (nth body 3) decided?)) + (and decided? (some #(= :app (head %)) (t/subterms c))) + (and (settled? ctx (nth body 2) true) (settled? ctx (nth body 3) true)) + :else false)) + true))) (defn- unfold [ctx x] (let [[_ f & args] x @@ -744,20 +816,73 @@ [x y] (and (not= x y) (some #(= x %) (t/subterms y)))) +(defn has-type? + "Is term u known to be of type ty? A variable of that type is; an + integer term is an Int, and a Nat when it is not negative; anything else + is when the type's recognizer, applied to it, rewrites to true. A type + with no recognizer (a set, a map) takes only a variable of its own." + [ctx ty u] + (let [el (fn [t] (when (and (seq? t) (contains? '#{List Vec} (first t))) (second t)))] + (boolean + (or (= ty (get-in ctx [:types u])) + (and (= :sq (head u)) (symbol? (second u)) (el ty) + (= {:elems (el ty)} (get-in ctx [:types (second u)]))) + (case ty + Int (int-term? ctx u) + Nat (and (int-term? ctx u) + (true? (truthiness ctx (normalize ctx [:call '<= [:lit 0] u])))) + (let [c (get-in ctx [:recognizers :checks ty])] + (cond (= :any c) true + (nil? c) false + :else (true? (truthiness ctx (normalize ctx (t/subst c {'%x u}))))))))))) + +(defn- typed? + "Do the terms bindings m give a rule's variables have the variables' + types?" + [ctx types m] + (every? (fn [[v ty]] (or (not (contains? m v)) (has-type? ctx ty (get m v)))) types)) + +(defn- recognizer-rule + "A recognizer on a variable of its type is true. A list recognizer on a + concatenation is its parts'; on the elements of a value, the value's + (nil being the empty list)." + [ctx x] + (when (and (= :app (head x)) (= 3 (count x))) + (let [r (second x) u (nth x 2) + ty (some (fn [[ty n]] (when (= n r) ty)) (get-in ctx [:recognizers :names]))] + (cond + (and ty (or (and (symbol? u) (= ty (get-in ctx [:types u]))) + (and (= :sq (head u)) (symbol? (second u)) (seq? ty) + (contains? '#{List Vec} (first ty)) + (= {:elems (second ty)} (get-in ctx [:types (second u)]))))) + [:lit true] + (and (contains? (get-in ctx [:recognizers :lists]) r) (= :sq (head u))) + (let [e (second u)] + (case (head e) + :eapp [:if [:app r [:sq (nth e 1)]] [:app r [:sq (nth e 2)]] [:lit false]] + :elems [:if [:call '= (second e) t/tnil] [:lit true] [:app r (second e)]] + nil)) + :else nil)))) + (defn- ih-rewrite "Rewrite x by an induction hypothesis. One with free variables (its law quantified over them as well) matches x as a pattern, and holds only for their declared types, which its hypothesis states." [ctx x] - (some (fn [{:keys [hyp lhs rhs vars]}] + (some (fn [{:keys [hyp lhs rhs vars types]}] ;; a hypothesis whose left side is a bare variable would match ;; every term; it has nothing to rewrite (when-let [m (when-not (symbol? lhs) - (if (seq vars) (match-term lhs x vars) (when (= x lhs) {})))] + (if (seq vars) + (let [m (match-term lhs x vars)] (when (and m (typed? ctx types m)) m)) + (when (= x lhs) {})))] (let [hyp (some-> hyp (t/subst m)) y (t/subst rhs m)] - (when (and (or (nil? hyp) (true? (truthiness ctx (normalize ctx hyp)))) - (not (loops? x y))) + ;; a rewrite to x itself changes nothing, and its hypothesis + ;; may hold x: reading it would rewrite x again + (when (and (not= x y) + (not (loops? x y)) + (or (nil? hyp) (true? (truthiness ctx (normalize ctx hyp))))) (swap! (:used-ih ctx) inc) y)))) (:ih ctx))) @@ -795,21 +920,56 @@ (some-> memo (swap! assoc t r)) r)))) +(defn- conjuncts + "The parts of a normalised conjunction: (if a b false) and (if a b a), + the shapes `and` lowers to." + [h] + (if (and (= :if (head h)) (or (= [:lit false] (nth h 3)) (= (nth h 1) (nth h 3)))) + (concat (conjuncts (nth h 1)) (conjuncts (nth h 2))) + [h])) + +(defn- bind-free + "Every extension of bindings m that gives the variables of hyp that the + left side left unbound a value from the facts: a part of hyp that + mentions one is matched against a fact known to be true, the way ACL2 + binds a hypothesis's free variables. Parts that are integer + comparisons go last: their linear form orders terms by name, so they + are checked once bound, not matched." + [ctx hyp vars m] + (let [unbound? (fn [m c] (some #(and (contains? vars %) (not (contains? m %))) (t/vars c))) + [plain arith] ((juxt remove filter) #(contains? #{:le :ieq} (head %)) (conjuncts hyp)) + facts (sort-by pr-str (for [[f v] (:facts ctx) :when (true? v)] f))] + (letfn [(go [m cs] + (if-let [c (first cs)] + (if (unbound? m c) + (mapcat #(some-> (match-term c % vars m) (go (rest cs))) facts) + (go m (rest cs))) + [m]))] + (go m (concat plain arith))))) + (defn- lemma-rewrite "Rewrite x by an earlier proved law: its left side matched against x, - its hypothesis, instantiated, normalised to true here." + its hypothesis, instantiated, normalised to true here. A variable of + the hypothesis the left side does not bind is bound from the facts. + The law holds only at its own types, so each term its variables take + must be shown to be of the variable's type." [ctx x] - (some (fn [{:keys [vars hyp lhs rhs name]}] - (when-let [m (match-term lhs x vars)] - (when (every? #(contains? m %) (t/vars rhs)) - (when (or (nil? hyp) - (let [h (t/subst hyp m)] - (and (every? #(not (contains? vars %)) (t/vars h)) - (true? (truthiness ctx (normalize ctx h)))))) - (let [y (t/subst rhs m)] - (when-not (loops? x y) - (swap! (:lemmas-used ctx) conj name) - y)))))) + (some (fn [{:keys [vars hyp lhs rhs name types]}] + (when-let [m0 (match-term lhs x vars)] + (some (fn [m] + (when (and (every? #(contains? m %) (t/vars rhs)) (typed? ctx types m)) + (let [y (t/subst rhs m)] + (when (and (not= x y) + (not (loops? x y)) + (or (nil? hyp) + (let [h (t/subst hyp m)] + (and (every? #(not (contains? vars %)) (t/vars h)) + (true? (truthiness ctx (normalize ctx h))))))) + (swap! (:lemmas-used ctx) conj name) + y)))) + (if (and hyp (some #(and (contains? vars %) (not (contains? m0 %))) (t/vars hyp))) + (bind-free ctx hyp vars m0) + [m0])))) (:lemmas ctx))) (def ^:private boolean-fns @@ -850,6 +1010,7 @@ [:lit (get (:facts ctx) x)]) (apply-patterns (get @indexed (rule-key x)) x) (computed ctx x) + (recognizer-rule ctx x) (when (= :app (head x)) (unfold ctx x)))) (defn assume @@ -864,6 +1025,23 @@ facts)] (assoc ctx :facts facts :memo (atom {}) :stuck (atom #{}) :int-memo (atom {}))))) +(defn- fn-height + "How deep fn literals nest in t: 0 with none." + [t] + (if (vector? t) + (+ (if (= :fn (head t)) 1 0) (reduce max 0 (map fn-height (rest t)))) + 0)) + +(defn- canonical-params + "A fn literal's parameters, named by their position and by how deep fn + literals nest in its body, so two fns that differ only in the names of + their parameters are one term, and a fact about one is a fact about the + other. An inner fn's parameters are never named like an outer one's: + the outer's height is greater." + [ps body] + (let [h (inc (fn-height body))] + (mapv #(symbol (str "%" h "_" %)) (range (count ps))))) + (defn normalize "Rewrite t to normal form under ctx. An if whose test is open gets its branches normalised under the test assumed true, and false." @@ -896,7 +1074,9 @@ (lin->term (reduce lin+ {:c c :m {}} (map (fn [[a k]] (lin* k (lin-of ctx a))) atoms))) [:lin c (vec atoms)])) - :fn (let [[_ ps body] x] [:fn ps (normalize ctx body)]) + :fn (let [[_ ps body] x + ps* (canonical-params ps body)] + [:fn ps* (normalize ctx (t/subst body (zipmap ps ps*)))]) (into [(head x)] (map #(normalize ctx %)) (rest x)))] (if (= :if (head x)) ;; a boolean law's left side is often an if: an induction @@ -915,8 +1095,9 @@ (defn context "A fresh normalising context. defs: name -> {:params :body :recursive?}; types: variable -> type; tenv: data declarations." - [{:keys [defs types tenv facts ih fuel lemmas lemmas-used]}] + [{:keys [defs types tenv facts ih fuel lemmas lemmas-used recognizers]}] {:defs (or defs {}) :types (or types {}) :tenv (or tenv {}) + :recognizers (or recognizers {}) :facts (or facts {}) :ih (or ih []) :lemmas (or lemmas []) :lemmas-used (or lemmas-used (atom #{})) :memo (atom {}) :stuck (atom #{}) :unfolded (atom #{}) :used-ih (atom 0) :int-memo (atom {}) @@ -1035,3 +1216,22 @@ (if (:pass? res) {:ok true} {:ok false :counterexample (first (get-in res [:shrunk :smallest]))})))) + +;; --- the models of clojure.core fns against the runtime ------------------------- + +(defn model-check + "Run the sort model on random lists of integers -- lists, vectors and + nil, with and without distinct -- against sort itself." + ([] (model-check 300 42)) + ([trials seed] + (let [ctx (context {:types '{xs (List Int)}}) + p (prop/for-all [xs (gen/one-of [(gen/return nil) (gen/list gen-int) (gen/vector gen-int)]) + dedup? gen/boolean] + (let [call (if dedup? [:call 'sort [:call 'distinct 'xs]] [:call 'sort 'xs]) + want (realize (t/evaluate call {'xs xs}))] + (and (= want (realize (t/evaluate (sort-model ctx (nth call 2)) {'xs xs}))) + (= want (realize (t/evaluate (normalize ctx call) {'xs xs})))))) + res (tc/quick-check trials p :seed seed)] + (if (:pass? res) + {:ok true} + {:ok false :counterexample (get-in res [:shrunk :smallest])})))) diff --git a/src/writ/prove/scheme.clj b/src/writ/prove/scheme.clj index bd027ef..e6db34a 100644 --- a/src/writ/prove/scheme.clj +++ b/src/writ/prove/scheme.clj @@ -81,6 +81,128 @@ :else nil))) +;; --- recognizers ------------------------------------------------------------------ +;; A law proved for every value of a type holds at a term only if the term +;; is of that type. The prover's logic is untyped, like ACL2's: a type is +;; a hypothesis, and a recognizer states it. Each recognizer takes a value +;; apart the way the type's cases do, so what it accepts is what a proof +;; over the type covers. + +(def ^:private scalar-checks + '{Bool boolean? String string? Char char? Keyword keyword? Symbol symbol? + Float number? Double number?}) + +(def ^:private rec-var '%x) + +(defn- type-var? [tenv ty] + (or (= 'Any ty) + (and (symbol? ty) (:tvar (get tenv ty))) + (and (symbol? ty) (not (get tenv ty)) (not (contains? scalar-checks ty)) + (not (contains? '#{Nat Int Unit} ty))))) + +(defn- rec-name [ty] + (symbol "writ.prove.types" + (str (-> (pr-str ty) (str/replace #"[\s()]+" "-") (str/replace #"^-|-$" "")) "?"))) + +(defn- conj-terms [cs] + (if (empty? cs) + [:lit true] + (reduce (fn [a c] [:if c a [:lit false]]) (reverse cs)))) + +(defn recognizers + "Recognizers for `types` (and the types their parts have) under tenv: + {:names {type name} :defs {name def} :checks {type template} :lists + #{name}}. A template is a term in `%x` saying a value is of the type: + :any for a type every value is of (a type variable), and no entry for a + type with no recognizer (a set, a map, a fn), which only a variable of + that type is known to be." + [tenv types] + (let [out (atom {:names {} :defs {} :checks {} :lists #{}}) + bad (atom #{})] + (letfn [(check [ty e] + (let [ty (plain ty)] + (cond + (= 'Nat ty) [:if [:call 'integer? e] [:call '<= [:lit 0] e] [:lit false]] + (= 'Int ty) [:call 'integer? e] + (= 'Unit ty) [:call '= e t/tnil] + (contains? scalar-checks ty) [:call (scalar-checks ty) e] + (type-var? tenv ty) [:lit true] + :else (when-let [n (rec ty)] [:app n e])))) + (rec [ty] + (let [known (:names @out)] + (if (contains? known ty) + (get known ty) + (let [n (rec-name ty) + _ (swap! out assoc-in [:names ty] n) + body (body-of ty rec-var)] + (if body + (do (swap! out assoc-in [:defs n] + {:params [rec-var] :body body + :recursive? (boolean (some #(and (= :app (head %)) (= n (second %))) + (t/subterms body)))}) + n) + (do (swap! bad conj n) n)))))) + (body-of [ty x] + (let [[h & args] (if (seq? ty) ty [ty])] + (cond + (contains? '#{List Vec} h) + (when-let [c (check (first args) [:call 'first x])] + (swap! out update :lists conj (rec-name ty)) + [:if [:call 'seq x] + [:if c [:app (rec-name ty) [:call 'rest x]] [:lit false]] + (if (= 'List h) + [:if [:call '= x t/tnil] [:lit true] [:call '= x [:sq t/enil]]] + [:call '= x [:sq t/enil]])]) + + (= 'Tuple h) + (let [cs (map-indexed (fn [i a] (check a [:call 'nth x [:lit i]])) args)] + (when (every? some? cs) + [:if [:call '= [:call 'count x] [:lit (count args)]] (conj-terms cs) [:lit false]])) + + (and (symbol? h) (get tenv h) (:ctors (get tenv h))) + (let [d (get tenv h) + sub (zipmap (:params d) args) + st (fn st [y] (cond (symbol? y) (get sub y y) (seq? y) (apply list (map st y)) :else y)) + arms (for [[c info] (sort-by (comp str key) (:ctors d)) + :let [fs (map st (:fields info)) + cs (map-indexed (fn [i f] (check f [:call 'nth x [:lit (inc i)]])) fs)]] + (when (every? some? cs) + [[:call '= [:call 'first x] [:lit (keyword (str c))]] + [:if [:call '= [:call 'count x] [:lit (inc (count fs))]] (conj-terms cs) [:lit false]]]))] + (when (every? some? arms) + (reduce (fn [e [c b]] [:if c b e]) [:lit false] (reverse arms)))) + + :else nil)))] + (doseq [ty types] (check ty rec-var)) + ;; a recognizer whose type, or a part's, has none is dropped, and so + ;; is every one that calls it + (loop [] + (let [{:keys [defs]} @out + gone (set (for [[n d] defs + :when (or (contains? @bad n) + (some #(and (= :app (head %)) (contains? @bad (second %)) + (not= n (second %))) + (t/subterms (:body d))))] + n))] + (when (seq gone) + (swap! bad into gone) + (swap! out update :defs #(apply dissoc % gone)) + (recur)))) + (let [{:keys [names] :as o} @out + all (into (set types) (keys names))] + (assoc o + :names (into {} (remove (fn [[_ n]] (contains? @bad n))) names) + :lists (set (remove #(contains? @bad %) (:lists o))) + :checks (into {} (for [ty all + :let [ty (plain ty) + c (cond (type-var? tenv ty) :any + (contains? '#{Nat Int} ty) nil + :else (let [c (check ty rec-var)] + (when-not (and (= :app (head c)) (contains? @bad (second c))) + c)))] + :when c] + [ty c]))))))) + ;; --- goals under hypotheses --------------------------------------------------- (defn truthy? [x] @@ -159,7 +281,8 @@ (cond-> (if (and (= :call (head gi)) (= '= (second gi)) (= 4 (count gi))) {:hyp hi :lhs (n (nth gi 2)) :rhs (n (nth gi 3))} {:hyp hi :lhs (n gi) :rhs [:lit true]}) - (seq pvars) (assoc :vars pvars)))))) + (seq pvars) (assoc :vars pvars + :types (into {} (map (fn [[x ty]] [(ren x) (plain ty)])) free))))))) (defn useful-ih "The hypotheses that can rewrite something: not one whose left side @@ -201,7 +324,7 @@ (if (< (calls a) (calls b)) [b a] [a b])) [(n gl) [:lit true]])] :when (not (or (symbol? l) (= :lin (head l))))] - {:name name :vars (set (vals ren)) :hyp hyp :lhs l :rhs r})))) + {:name name :vars (set (vals ren)) :types types :hyp hyp :lhs l :rhs r})))) (catch clojure.lang.ExceptionInfo _ nil))) @@ -289,7 +412,10 @@ (into {} (map (fn [[x v]] [v (if (= x acc) 'Int (get-in opts [:types x]))])) ren)))) n #(rw/normalize ctx %) - hyp [:call 'integer? (ren acc)]] + hyp [:call 'integer? (ren acc)] + types (into {} (keep (fn [[x v]] (when-let [ty (if (= x acc) 'Int (get-in opts [:types x]))] + [v (plain ty)]))) + ren)] (if (= 'integer? (second g)) - {:name nm :vars (set (vals ren)) :hyp hyp :lhs (n g) :rhs [:lit true]} - {:name nm :vars (set (vals ren)) :hyp hyp :lhs (n (nth g 2)) :rhs (n (nth g 3))}))) + {:name nm :vars (set (vals ren)) :types types :hyp hyp :lhs (n g) :rhs [:lit true]} + {:name nm :vars (set (vals ren)) :types types :hyp hyp :lhs (n (nth g 2)) :rhs (n (nth g 3))}))) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index c767a39..115f11c 100644 --- a/src/writ/spec.clj +++ b/src/writ/spec.clj @@ -295,23 +295,29 @@ (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 + :induct, the variable to try induction on first; :vary, the other + variables the induction hypothesis holds at every value of, not just + the goal's -- an accumulator a fold passes on, say; :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")) + (fail! where " takes a map: {:induct x :vary [y] :use [lemma ...] :strategy :symbolic :fuel n}")) + (when-let [bad (seq (remove #{:induct :vary :use :strategy :fuel} (keys m)))] + (fail! where " has unknown keys: " (pr-str bad) "; it takes :induct :vary :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 :vary) (not (and (vector? (:vary m)) (every? simple-sym? (:vary m))))) + (fail! where ": :vary is a vector of variables of the law")) + (when (and (contains? m :vary) (contains? (set (:vary m)) (:induct m))) + (fail! where ": the variable of the induction cannot vary in its own hypothesis")) (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)))) @@ -582,12 +588,17 @@ (defn- qualify "Resolve a law's free names the way the spec reads them: a target public first, then a name the spec ns interns; bound names and anything else - (core, aliases) are left for eval in the spec ns." - [form bound target-publics spec-interns target spec-ns] + (core, aliases) are left for eval in the spec ns. own, name -> + qualified name, comes before both: a lemma reads the defns of its proof + namespace first." + ([form bound target-publics spec-interns target spec-ns] + (qualify form bound target-publics spec-interns target spec-ns {})) + ([form bound target-publics spec-interns target spec-ns own] (letfn [(walk [f bound] (cond (and (symbol? f) (nil? (namespace f)) (not (contains? bound f))) - (cond (contains? target-publics f) (symbol (name target) (name f)) + (cond (contains? own f) (get own f) + (contains? target-publics f) (symbol (name target) (name f)) (contains? spec-interns f) (symbol (name spec-ns) (name f)) :else f) (and (seq? f) (= 'quote (first f))) f @@ -598,7 +609,15 @@ (map? f) (into {} (map (fn [[k v]] [(walk k bound) (walk v bound)])) f) (set? f) (into #{} (map #(walk % bound)) f) :else f))] - (walk form bound))) + (walk form bound)))) + +(defn- proof-own + "name -> qualified name for the defns a proof namespace interns." + [proof-ns] + (if proof-ns + (into {} (for [[k v] (ns-interns (the-ns proof-ns)) :when (fn? @v)] + [k (symbol (name proof-ns) (name k))])) + {})) (defn- calls-target? "Does a qualified law mention any fn of the target namespace?" @@ -1869,10 +1888,30 @@ [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)))]])) + (let [proof-ns (::proof-ns opts) + defs (delay (prover/definitions + (cond-> [[target (book/read-forms (source-url target))] + [spec-ns (mapv refine->defn (book/read-forms (source-url spec-ns)))]] + ;; a proof namespace's own defns, reading the + ;; target's fns it refers by their plain names -- + ;; the fns of the target checked, when a stand-in + ;; is checked in place of the spec's own + proof-ns (conj [proof-ns (book/read-forms (source-url proof-ns)) + (into {} (for [[k v] (ns-refers (the-ns proof-ns)) + :when (contains? #{target (:target (get @registry spec-ns))} + (ns-name (:ns (meta v))))] + [k (symbol (name target) (name k))]))])))) anns (into {} (map (fn [[k sig]] [k (erase sig refs)])) anns) + sigs (into {} (for [[nm sig] anns] + [(symbol (str target) (str nm)) {:params (mapv plain (:params sig)) :ret (plain (:ret sig))}])) + ;; what each signed fn returns, proved from its code once: the + ;; laws' lemmas are instantiated only at terms of their types + contracts (delay (let [[ds] @defs] (prover/prove-contracts {:defs ds :tenv tenv :sigs sigs}))) + sigs (into {} (for [[nm sig] anns] + [(symbol (str target) (str nm)) {:params (mapv plain (:params sig)) :ret (plain (:ret sig))}])) + ;; what each signed fn returns, proved from its code once: the + ;; laws' lemmas are instantiated only at terms of their types + contracts (delay (let [[ds] @defs] (prover/prove-contracts {:defs ds :tenv tenv :sigs sigs}))) ;; 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")) @@ -1893,6 +1932,8 @@ :hint (get (::hints opts) (:law r)) :fuel (or (:fuel (get (::hints opts) (:law r))) (:fuel opts)) :total (:total r) + :lemma (:lemma r) + :sigs sigs :contracts @contracts :defs ds :tenv tenv :target target :own own :lemmas lemmas :rets (into {} (for [[nm sig] anns] @@ -2006,6 +2047,7 @@ laws (into (vec laws) (mapcat #(graph-obligations % refs) (:graphs e))) publics (set (keys (ns-publics (the-ns target)))) interns (set (keys (ns-interns (the-ns spec-ns)))) + proof-own* (proof-own (:ns proof-e)) opaque (into (set publics) interns) numeric-fns (into #{} (keep (fn [[k s]] (when (contains? '#{Nat Int Float Double} (plain (:ret s))) @@ -2020,13 +2062,16 @@ :let [p (desugar prop)]] (try (lw/check-prop-shape! p) - (let [qp (qualify p #{} publics interns target spec-ns)] + (let [qp (qualify p #{} publics interns target spec-ns + (if lemma proof-own* {}))] + ;; a lemma is proof, not contract: one about + ;; clojure.core alone is a fact the proof uses (cond - (not (calls-target? qp target)) + (and (not lemma) (not (calls-target? qp target))) {:law name :status :vacuous :why (str "it calls no fn of " target)} - (try-prove p data-tenv opaque numeric-fns) + (and (not lemma) (try-prove p data-tenv opaque numeric-fns)) {:law name :status :vacuous :why (str "writ.norm proves it without looking at the " "implementation, so any code satisfies it")} diff --git a/test/writ/proof_test.clj b/test/writ/proof_test.clj index b08f5d4..418cdc3 100644 --- a/test/writ/proof_test.clj +++ b/test/writ/proof_test.clj @@ -42,6 +42,32 @@ (is (str/includes? (err '(writ.spec/hint sorted {:color :red})) "unknown keys")))) +(deftest the-tree-holds-a-sorted-set-is-proved-from-its-proof-namespace + (let [r (spec/check 'writ.spec-demo.tree-spec {:seed 42 :cache false}) + l (law-result r 'holds-a-sorted-set)] + (is (:ok r) (:message r)) + (is (= :proved (:status l)) (pr-str l)) + (is (= ['build-lists] (:lemmas l))) + (testing "every lemma is proved, those about clojure.core alone too" + (is (every? #(= :proved (:status %)) (:lemmas r)) (pr-str (:lemmas r))) + (is (= :proved (:status (first (filter #(= 'none-below (:lemma %)) (:lemmas r))))))) + (testing "the fold is proved with its accumulator varying in the hypothesis" + (is (re-find #"by induction on xs" + (:proof (first (filter #(= 'build-lists (:lemma %)) (:lemmas r))))))))) + +(deftest a-broken-tree-is-not-proved-a-sorted-set + (doseq [target '[writ.spec-demo.tree-mirror writ.spec-demo.tree-bad-build]] + (let [r (spec/check 'writ.spec-demo.tree-spec {:seed 42 :cache false :target target})] + (is (not= :proved (:status (law-result r 'holds-a-sorted-set))) (str target)) + (is (not-any? :prover-bug (concat (:laws r) (:lemmas r))) (str target))))) + +(deftest a-vary-hint-is-checked-when-it-loads + (let [err (fn [form] (try (macroexpand-1 form) nil (catch Throwable e (ex-message e))))] + (is (str/includes? (err '(writ.spec/hint fold {:vary acc})) ":vary is a vector")) + (is (str/includes? (err '(writ.spec/hint fold {:induct xs :vary [xs]})) + "cannot vary in its own hypothesis")) + (is (nil? (err '(writ.spec/hint fold {:induct xs :vary [acc]})))))) + (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}) diff --git a/test/writ/prove_test.clj b/test/writ/prove_test.clj index 5933879..c63df2a 100644 --- a/test/writ/prove_test.clj +++ b/test/writ/prove_test.clj @@ -173,6 +173,32 @@ (is (:ok r) (pr-str (:failures r))) (is (<= 10 (:checked r))))) +(deftest sort-and-distinct-are-modelled-on-integer-lists + (testing "the model computes what sort and distinct compute" + (let [r (rw/model-check 300 42)] + (is (:ok r) (pr-str (:counterexample r))))) + (testing "on a list of integers, sorting is inserting each element in turn" + (is (= 'reduce (second (norm {:types '{xs (List Nat)}} [:call 'sort [:call 'distinct 'xs]])))) + (is (= 'reduce (second (norm {:types '{xs (List Int)}} [:call 'sort 'xs]))))) + (testing "on two unknown integers it is the comparison" + (let [x (norm {:types '{a Nat b Nat}} [:call 'sort [:call 'distinct (t/seq-term '[a b])]])] + (doseq [[a b] [[1 2] [2 1] [3 3] [0 7]]] + (is (= (sort (distinct [a b])) (t/evaluate x {'a a 'b b})))))) + (testing "elements that may be floats or strings are left alone" + (is (= [:call 'sort 'xs] (norm {:types '{xs (List Double)}} [:call 'sort 'xs]))) + (is (= [:call 'sort [:call 'distinct 'xs]] (norm [:call 'sort [:call 'distinct 'xs]]))))) + +(deftest filter-and-every-walk-a-concatenation + (let [ctx {:types '{a {:elems Nat} b {:elems Nat}}} + f [:fn '[y] [:call 'odd? 'y]]] + (is (= (norm ctx [:sq [:eapp [:elems [:call 'filter f [:sq 'a]]] [:elems [:call 'filter f [:sq 'b]]]]]) + (norm ctx [:call 'filter f [:sq [:eapp 'a 'b]]]))) + (is (= (norm ctx [:if [:call 'every? f [:sq 'a]] [:call 'every? f [:sq 'b]] [:lit false]]) + (norm ctx [:call 'every? f [:sq [:eapp 'a 'b]]])))) + (let [r (rw/self-test (filter #(re-find #"-app$" (name (first %))) rw/pattern-rules) 200 42)] + (is (:ok r) (pr-str (:failures r))) + (is (= 3 (:checked r))))) + (deftest comparisons-follow-from-chains-of-facts ;; a <= b, b <= c, c <= d gives a <= d, and settles d < a false (let [le (fn [x y] [:le [:lin 0 [[y 1] [x -1]]]]) @@ -327,6 +353,141 @@ (is (:proved r) (str nm)) (is (= {:ok true} (writ.prove.check/check-proof opts goal (:trace r))) (str nm)))))) +;; --- a hypothesis that varies ---------------------------------------------------------- + +(def ^:private fold-prop + '(forall [xs (List Nat)] + (forall [acc (List Nat)] + (= (count (reduce (fn [a v] (cons v a)) acc xs)) (+ (count acc) (count xs)))))) + +(deftest a-varying-hypothesis-is-replayed-by-the-checker + (let [law {:prop fold-prop :defs {} :tenv {} :target 'none :own {} :lemma true + :hint {:induct 'xs :vary '[acc] :strategy :induction}} + r (prover/prove-law law) + [bs body] (writ.prove.scheme/split-foralls fold-prop) + recs (writ.prove.scheme/recognizers {} (map second bs)) + opts {:defs (:defs recs) :tenv {} :types (into {} bs) :fuel 20000 :lemmas [] :recognizers recs} + goal (writ.prove.scheme/goal (writ.prove.translate/context {}) (mapv first bs) body)] + (is (:proved r) (pr-str r)) + (testing "without its recognizers the checker can't show acc's instance is a list" + (is (not (:ok (writ.prove.check/check-proof (dissoc opts :recognizers) goal (:trace r)))))) + (is (= '{acc (List Nat)} (:vary (:trace r)))) + (is (= {:ok true} (writ.prove.check/check-proof opts goal (:trace r)))) + (testing "the fold is not proved with the accumulator held fixed" + (is (not (:proved (prover/prove-law (assoc-in law [:hint :vary] nil)))))) + (testing "the checker rebuilds the hypothesis the trace names, and no other" + (is (not (:ok (writ.prove.check/check-proof opts goal (dissoc (:trace r) :vary))))) + (is (re-find #"cannot vary" + (:reason (writ.prove.check/check-proof opts goal (assoc (:trace r) :vary '{acc (List Int)}))))) + (is (re-find #"cannot vary" + (:reason (writ.prove.check/check-proof opts goal (assoc (:trace r) :vary '{xs (List Nat)})))))))) + +;; --- a lemma holds only at its own types ------------------------------------------ + +(def ^:private tree-tenv + '{Tree {:arity 0 :params [] :ctors {Leaf {:fields []} Node {:fields [Tree Nat Tree]}}}}) + +(defn- run-recognizer + "Evaluate recognizer `nm` of `recs` on value v, as the runtime would." + [recs nm v] + (letfn [(res [q] (delay (fn [x] (let [d (get-in recs [:defs q])] + (t/evaluate (:body d) {(first (:params d)) x} res)))))] + (try (boolean (t/evaluate [:app nm 'v] {'v v} res)) (catch Throwable _ false)))) + +(deftest a-recognizer-accepts-what-the-type-checks + (let [recs (writ.prove.scheme/recognizers tree-tenv '[Tree (List Nat) (Vec Int)]) + vecs (fn vecs [v] (cond (map-entry? v) v (sequential? v) (mapv vecs v) :else v)) + junk [nil [] () [:Leaf] [:Leaf 1] [:Node [:Leaf] 3 [:Leaf]] [:Node [:Leaf] -3 [:Leaf]] + [:Node [:Leaf] 3] '(:Node (:Leaf) 2 (:Leaf)) [1 2] [-1] ["a"] "ab" 5 {:a 1} [nil]]] + (doseq [ty '[Tree (List Nat) (Vec Int)] + :let [nm (get-in recs [:names ty])]] + (is (symbol? nm) (str ty)) + (testing (str "every value of " ty " is recognised") + (doseq [v (spec/sample ty tree-tenv 30)] + (is (run-recognizer recs nm v) (pr-str [ty v])))) + (testing (str "what is recognised as " ty " is one, lists read as vectors") + (doseq [v junk :when (run-recognizer recs nm v)] + (is (spec/conforms? ty (vecs v) tree-tenv) (pr-str [ty v]))))))) + +(deftest a-lemma-instance-must-have-the-lemmas-types + (let [recs (writ.prove.scheme/recognizers tree-tenv '[Tree]) + rule (fn [ty] {:name 'l :vars '#{?a} :types {'?a ty} :lhs [:app 'f '?a] :rhs [:lit 1]}) + rw (fn [ty types x] (rw/normalize (rw/context {:types types :lemmas [(rule ty)] + :defs (:defs recs) :recognizers recs}) + [:app 'f x]))] + (testing "a Nat" + (is (= [:lit 1] (rw 'Nat '{k Nat} 'k))) + (is (= [:lit 1] (rw 'Nat {} [:lit 3]))) + (is (not= [:lit 1] (rw 'Nat '{k Int} 'k))) + (is (not= [:lit 1] (rw 'Nat {} [:lit -1])))) + (testing "a Tree" + (is (= [:lit 1] (rw 'Tree '{t Tree} 't))) + (is (not= [:lit 1] (rw 'Tree {} 'u)) "an unknown value is not known to be a Tree") + (is (= [:lit 1] (rw 'Tree '{n Nat} (t/seq-term [[:lit :Node] (t/seq-term [[:lit :Leaf]]) 'n (t/seq-term [[:lit :Leaf]])])))) + (is (not= [:lit 1] (rw 'Tree {} (t/seq-term [[:lit :Node] (t/seq-term [[:lit :Leaf]]) [:lit -1] (t/seq-term [[:lit :Leaf]])]))))) + (testing "a type with no recognizer takes only a variable of it" + (is (= [:lit 1] (rw '(Set Int) '{s (Set Int)} 's))) + (is (not= [:lit 1] (rw '(Set Int) {} [:call 'hash-set [:lit 1]])))))) + +(deftest a-fns-contract-is-proved-from-its-code + (require 'writ.spec-demo.tree) + (let [[defs] (prover/definitions [['writ.spec-demo.tree + (writ.book/read-forms (clojure.java.io/resource "writ/spec_demo/tree.clj"))]]) + rules (prover/prove-contracts {:defs defs :tenv tree-tenv + :sigs '{writ.spec-demo.tree/insert {:params [Nat Tree] :ret Tree} + writ.spec-demo.tree/to-list {:params [Tree] :ret (List Nat)} + writ.spec-demo.tree/size {:params [Tree] :ret Nat}}})] + (is (= '#{insert%contract to-list%contract} (set (map :name rules)))))) + +;; --- rewriting under names, facts and floats -------------------------------------- + +(deftest fns-that-differ-only-in-parameter-names-are-one-term + (is (= (norm [:fn '[a] [:call 'inc 'a]]) (norm [:fn '[b] [:call 'inc 'b]]))) + (testing "an inner fn's parameters never capture an outer one's" + (let [x (norm [:fn '[a] [:fn '[b] [:call '+ 'a 'b]]])] + (is (= 7 (((t/evaluate x) 3) 4))))) + (testing "a fact about one is a fact about the other" + (let [f (fn [p] [:call 'every? [:fn [p] [:call 'odd? p]] 'xs]) + ctx (rw/assume (rw/context {:types '{xs (List Nat)}}) (rw/normalize (rw/context {}) (f 'a)) true)] + (is (= [:lit true] (rw/normalize ctx (f 'b))))))) + +(deftest what-picks-parts-of-integers-holds-no-float + (let [ctx {:types '{xs (List Nat) ys (List Double)}} + pick (fn [v] [:call 'filter [:fn '[y] [:call 'odd? 'y]] v])] + (is (= [:lit true] (norm ctx [:call '= (pick 'xs) (pick 'xs)]))) + (is (= '= (second (norm ctx [:call '= (pick 'ys) (pick 'ys)]))) "a NaN may be inside") + (testing "and a fold that only arranges them" + (let [fold [:call 'reduce [:fn '[s x] [:call 'cons 'x 's]] [:sq [:enil]] 'xs]] + (is (= [:lit true] (norm ctx [:call '= fold fold]))))) + (testing "a shared first part leaves the rest to compare" + (let [ctx {:types '{a {:elems Nat} b Nat c Nat}}] + (is (= (norm ctx [:call '= 'b 'c]) + (norm ctx [:call '= [:sq [:eapp 'a [:econs 'b [:enil]]]] [:sq [:eapp 'a [:econs 'c [:enil]]]]]))))))) + +(deftest a-lemma-binds-a-free-variable-from-the-facts + ;; (every? #(> % ?v) ?B) and ?x <= ?v: nothing in ?B is below ?x. The + ;; left side binds ?x and ?B; ?v comes from a fact. + (let [above (fn [v b] [:call 'every? [:fn '[y] [:call '> 'y v]] b]) + below (fn [x b] [:call 'filter [:fn '[y] [:call '< 'y x]] b]) + types '{x Nat v Nat xs (List Nat) ?x Nat ?v Nat ?B (List Nat)} + n0 (rw/context {:types types}) + rule {:name 'none-below :vars '#{?x ?v ?B} + :hyp (rw/normalize n0 [:if (above '?v '?B) [:call '<= '?x '?v] [:lit false]]) + :lhs (rw/normalize n0 (below '?x '?B)) :rhs [:sq [:enil]]} + ctx (fn [facts] (reduce (fn [c f] (rw/assume c (rw/normalize n0 f) true)) + (rw/context {:types types :lemmas [rule]}) facts))] + (is (= [:sq [:enil]] (rw/normalize (ctx [(above 'v 'xs) [:call '<= 'x 'v]]) (below 'x 'xs)))) + (testing "without the fact, or with the wrong bound, it stays" + (is (not= [:sq [:enil]] (rw/normalize (ctx [[:call '<= 'x 'v]]) (below 'x 'xs)))) + (is (not= [:sq [:enil]] (rw/normalize (ctx [(above 'v 'xs) [:call '< 'v 'x]]) (below 'x 'xs))))))) + +(deftest a-rewrite-to-itself-is-not-applied + ;; an induction hypothesis at the empty list can read () -> (): applying + ;; it would read its hypothesis, which holds (), again and again + (let [ih {:lhs [:sq [:enil]] :rhs [:sq [:enil]] + :hyp [:call 'every? [:fn '[y] [:call 'odd? 'y]] [:sq [:enil]]]}] + (is (= [:sq [:enil]] (rw/normalize (rw/context {:ih [ih] :fuel 200}) [:call 'rest [:nil]]))))) + ;; --- constants and more of clojure.core ------------------------------------------ (deftest named-constants-and-core-fns-are-proved diff --git a/test/writ/spec_demo/tree_proof.clj b/test/writ/spec_demo/tree_proof.clj new file mode 100644 index 0000000..c8fad57 --- /dev/null +++ b/test/writ/spec_demo/tree_proof.clj @@ -0,0 +1,80 @@ +(ns writ.spec-demo.tree-proof + "How writ.spec-demo.tree-spec's holds-a-sorted-set is proved. + + The prover models (sort (distinct xs)) as a fold inserting each element + into a sorted list: the elements below it, it, the elements above it. + Building the tree is the same kind of fold, inserting into a tree, so + the law follows from one fact about insert -- listing a search tree + after an insert is that list insert -- and the fold lemma it gives." + (:require [writ.spec :refer [proof-of lemma hint]] + [writ.spec-demo.tree :refer [to-list insert]])) + +(proof-of writ.spec-demo.tree-spec) + +;; a search tree: everything left of a value is below it, everything right +;; of it above +(defn bst? [t] + (case (first t) + :Leaf true + :Node (let [[_ l v r] t] + (and (bst? l) (bst? r) + (every? #(< % v) (to-list l)) + (every? #(> % v) (to-list r)))))) + +;; inserting a value below (above) every element keeps them all below (above) +(lemma below-insert + (forall [x Nat, v Nat, t Tree] + (=> (and (every? #(< % v) (to-list t)) (< x v)) + (every? #(< % v) (to-list (insert x t)))))) + +(lemma above-insert + (forall [x Nat, v Nat, t Tree] + (=> (and (every? #(> % v) (to-list t)) (> x v)) + (every? #(> % v) (to-list (insert x t)))))) + +(lemma insert-keeps-bst + (forall [x Nat, t Tree] (=> (bst? t) (bst? (insert x t))))) + +;; what a bound on a list says about the part of it below or above x; +;; (concat xs) is xs as a seq, () for nil, as filter gives +(lemma none-below + (forall [x Nat, v Nat, xs (List Nat)] + (=> (and (every? #(> % v) xs) (<= x v)) (= (filter #(< % x) xs) ())))) + +(lemma all-above + (forall [x Nat, v Nat, xs (List Nat)] + (=> (and (every? #(> % v) xs) (<= x v)) (= (filter #(> % x) xs) (concat xs))))) + +(lemma all-below + (forall [x Nat, v Nat, xs (List Nat)] + (=> (and (every? #(< % v) xs) (>= x v)) (= (filter #(< % x) xs) (concat xs))))) + +(lemma none-above + (forall [x Nat, v Nat, xs (List Nat)] + (=> (and (every? #(< % v) xs) (>= x v)) (= (filter #(> % x) xs) ())))) + +;; listing a search tree after an insert is inserting into its list +(lemma to-list-insert + (forall [x Nat, t Tree] + (=> (bst? t) + (= (to-list (insert x t)) + (concat (filter #(< % x) (to-list t)) [x] (filter #(> % x) (to-list t))))))) + +;; building the tree from any search tree is the fold of that list insert +(lemma build-lists + (forall [xs (List Nat), acc Tree] + (=> (bst? acc) + (= (to-list (reduce (fn [acc v] (insert v acc)) acc xs)) + (reduce (fn [s x] (concat (filter #(< % x) s) [x] (filter #(> % x) s))) + (to-list acc) xs))))) + +(hint below-insert {:induct t}) +(hint above-insert {:induct t}) +(hint insert-keeps-bst {:induct t :use [below-insert above-insert]}) +(hint none-below {:induct xs}) +(hint all-above {:induct xs}) +(hint all-below {:induct xs}) +(hint none-above {:induct xs}) +(hint to-list-insert {:induct t :use [none-below all-above all-below none-above]}) +(hint build-lists {:induct xs :vary [acc] :use [insert-keeps-bst to-list-insert]}) +(hint holds-a-sorted-set {:use [build-lists]}) diff --git a/test/writ/spec_test.clj b/test/writ/spec_test.clj index c621957..2fb14e0 100644 --- a/test/writ/spec_test.clj +++ b/test/writ/spec_test.clj @@ -320,7 +320,7 @@ (let [r (spec/check tree-spec {:seed 42})] (is (:ok r) (:message r)) (is (= [] (:gaps r))) - (is (= :tested (:status (law-result r 'holds-a-sorted-set)))))) + (is (= :proved (:status (law-result r 'holds-a-sorted-set)))))) ;; --- adequacy for keyword results and pinned arguments ---------------------