diff --git a/README.md b/README.md index 61a39e4..24f3895 100644 --- a/README.md +++ b/README.md @@ -589,7 +589,10 @@ 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 +proves nothing again. The contracts proved for the code are cached +apart, in one file per implementation, keyed on the code, its signatures +and data and writ, so editing a law or the proof namespace keeps them. +`:cache false` turns it off; `:cache-dir` puts it elsewhere. Add `.writ-cache/` to `.gitignore`. ### Requiring proof @@ -739,7 +742,9 @@ 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 +own type. An `Int` return is proved an integer, and a `Nat` return is then +proved not negative, so `(size t)` is an integer term the arithmetic +works with, known to be at least 0. 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 2465e23..a21d783 100644 --- a/skills/writ/SKILL.md +++ b/skills/writ/SKILL.md @@ -265,6 +265,11 @@ Plain Clojure, with no writ require and no annotations. writ rejects: as `(if (< n k) base (f (- n k)))` - fields from destructuring or `first`/`nth` under a non-nil test, including a `case` on `(first t)` + - a field of a field, `(rest (rest xs))` or a nested `match`, with each + read guarded at its own depth; a test on a deeper read guards the + reads above it + - `[:Tag f1 f2]` rebuilt from a matched field's own fields, each at its + own index, which is no larger than that field A test inside `and` counts in the then branch, and each test of an `or` is false in its else branch. Recursion with no structural measure diff --git a/src/writ/check.clj b/src/writ/check.clj index aeb0991..b8a20d5 100644 --- a/src/writ/check.clj +++ b/src/writ/check.clj @@ -300,14 +300,26 @@ (not (contains? (:bound info) s))) (symbol (name s)))))) +;; A place is a column and the path of structural reads below it, each +;; read a template like (nth % 2) or (rest %). A fact about a place also +;; holds of every place above it: a read of nil or () is nil or (), so a +;; value below that is non-nil or non-empty leaves the ones above it +;; non-empty. + (defn- shrink-step - "[step operand]: step is :dec, :inc or a set of structural needs. A - lookup with a default is not a step: the default can hand the value back." + "[step operand read]: step is :dec, :inc or a set of structural needs; + read is the structural read as a template over %, nil when an argument + other than the operand is not a literal. A lookup with a default is not + a step: the default can hand the value back." [t info] (let [h (core-head t info) args (:args t) n (count args) - [a b] args] + [a b] args + lit? (fn [x] (= :lit (:op x))) + hole? (fn [x] (= '% x)) + read (fn [& xs] (when (every? (fn [x] (or (hole? x) (lit? x))) xs) + (apply list h (map (fn [x] (if (hole? x) x (lit-val x))) xs))))] (case h dec (when (= n 1) [:dec a]) inc (when (= n 1) [:inc a]) @@ -318,35 +330,65 @@ (and (= n 2) (= 1 (lit-val a))) [:inc b] :else nil) (rest pop next nnext butlast first second last peek ffirst) - (when (= n 1) [(get shrink-needs h) a]) + (when (= n 1) [(get shrink-needs h) a (read '%)]) ;; a literal nil default cannot hand the column back: the read is ;; an element or nil, both below a non-nil column - (nth get) (when (or (= n 2) (and (= n 3) (= :lit (:op (nth args 2))) + (nth get) (when (or (= n 2) (and (= n 3) (lit? (nth args 2)) (nil? (lit-val (nth args 2))))) - [#{:nil} a]) - drop (when (and (= n 2) (pos-int-lit? a)) [#{:empty :finite} b]) - nthrest (when (and (= n 2) (pos-int-lit? b)) [#{:empty :finite} a]) - nthnext (when (and (= n 2) (pos-int-lit? b)) [#{:nil :finite} a]) - subvec (when (and (<= 2 n 3) (pos-int-lit? b)) [#{:empty :finite} a]) + [#{:nil} a (read '% b)]) + drop (when (and (= n 2) (pos-int-lit? a)) [#{:empty :finite} b (read a '%)]) + nthrest (when (and (= n 2) (pos-int-lit? b)) [#{:empty :finite} a (read '% b)]) + nthnext (when (and (= n 2) (pos-int-lit? b)) [#{:nil :finite} a (read '% b)]) + subvec (when (and (<= 2 n 3) (pos-int-lit? b)) + [#{:empty :finite} a (apply read '% (rest args))]) nil))) -(defn- numeric-only? [o] (every? vector? (:needs o))) +(def ^:private finite-reads + "Reads that keep a finite collection finite." + '#{rest pop next nnext butlast drop nthrest nthnext subvec}) + +(declare origin) + +(defn- num-need? [need] (and (vector? need) (= :num (first need)))) + +(defn- numeric-only? [o] (every? num-need? (:needs o))) + +(defn- rebuild-origin + "A tagged vector, [:Tag f1 .. fn], whose fields are the fields of one + place, each read back at its own index, rebuilds that place: it is no + larger than it. The rebuilt value is always non-nil, so it never feeds + a fact, and nothing is read below it." + [t info stop] + (let [items (when (and (= :vec (:op t)) (keyword? (lit-val (first (:items t))))) + (rest (:items t))) + os (map #(origin % info stop) items) + at (fn [i o] (when (and o (:exact? o) (zero? (:net o 0)) + (= (list 'nth '% (inc i)) (peek (:path o)))) + [(:col o) (pop (:path o))])) + places (map-indexed at os)] + (when (and (seq items) (every? some? places) (apply = places)) + (let [[c p] (first places)] + {:col c :net 0 :path p :strict? (boolean (seq p)) :exact? false + :rebuilt? true :needs (into #{} (mapcat :needs) os)})))) (defn- origin "Where `t` comes from, relative to the column names in `stop`: - {:col c :net 0 :strict? false} for an unchanged copy of column c; - {:col c :strict? true :needs #{..}} for a strict subterm, where needs - are what each step requires of the column; for a dec/inc chain, :net is - how far below c the value sits and each dec at depth k needs [:num k] - (c minus k proven positive). Copies, (seq x), let chains, destructure - and match temporaries are followed; a loop binder outside `stop` is - opaque (recur rebinds it)." + {:col c :net 0 :strict? false :path []} for an unchanged copy of column + c; {:col c :strict? true :path p :needs #{..}} for a strict subterm at + the place [c p], where needs are what each read requires of the place + it reads (a bare need is on the column, [:at q need] on the place + [c q]); for a dec/inc chain, :net is how far below c the value sits and + each dec at depth k needs [:num k] (c minus k proven positive). :exact? + is false when the value is at or below its place, not exactly there; + nothing is read below such a value. Copies, (seq x), let chains, + destructure and match temporaries are followed; a loop binder outside + `stop` is opaque (recur rebinds it)." [t info stop] (cond (ref? t) (let [n (:name t)] (cond - (contains? stop n) {:col n :net 0 :strict? false :needs #{}} + (contains? stop n) {:col n :net 0 :strict? false :needs #{} :path [] :exact? true} (contains? (:loops info) n) nil (contains? (:binds info) n) (origin (get (:binds info) n) info stop) :else nil)) @@ -359,42 +401,57 @@ coercion? (contains? '#{seq? vector? map?} (core-head (:test t) info))] (cond (and a b (= (:col a) (:col b)) (= (:net a 0) (:net b 0))) - {:col (:col a) :net (:net a 0) :strict? (and (:strict? a) (:strict? b)) - :needs (into (:needs a) (:needs b))} + (let [pa (:path a) pb (:path b) + common (vec (map first (take-while (fn [[x y]] (= x y)) (map vector pa pb))))] + {:col (:col a) :net (:net a 0) :strict? (and (:strict? a) (:strict? b)) + :needs (into (:needs a) (:needs b)) :path common + :exact? (and (:exact? a) (:exact? b) (= pa pb)) + :rebuilt? (or (:rebuilt? a) (:rebuilt? b))}) (and coercion? (or a b) (not (and a b))) (assoc (or a b) :strict? false :needs #{} :net 0) :else nil)) (= :invoke (:op t)) - (if-let [[step x] (shrink-step t info)] + (if-let [[step x read] (shrink-step t info)] (when-let [o (origin x info stop)] (case (if (vector? step) (first step) step) :dec (when (numeric-only? o) (let [k (:net o 0)] - {:col (:col o) :net (inc k) :strict? true - :needs (conj (:needs o) [:num k])})) + (assoc o :net (inc k) :strict? true + :needs (conj (:needs o) [:num k])))) :sub (when (numeric-only? o) (let [k (:net o 0) d (second step)] - {:col (:col o) :net (+ k d) :strict? true - :needs (into (:needs o) (for [j (range d)] [:num (+ k j)]))})) + (assoc o :net (+ k d) :strict? true + :needs (into (:needs o) (for [j (range d)] [:num (+ k j)]))))) ;; inc undoes a dec; back at (or past) the column is not smaller :inc (when (and (numeric-only? o) (pos? (:net o 0))) (let [k (dec (:net o 0))] (assoc o :net k :strict? (pos? k)))) - (when (and (numeric-only? o) (zero? (:net o 0)) (empty? (:needs o))) - {:col (:col o) :net 0 :strict? true :needs (into (:needs o) step)}) - )) + ;; a structural read, at any depth of reads before it + (when (and (zero? (:net o 0)) (:exact? o) (not-any? num-need? (:needs o))) + (let [p (:path o)] + {:col (:col o) :net 0 :strict? true :path (if read (conj p read) p) + :exact? (some? read) + :needs (into (:needs o) (map #(if (empty? p) % [:at p %])) step)})))) (when (and (= 'seq (core-head t info)) (= 1 (count (:args t)))) (origin (first (:args t)) info stop))) + (= :vec (:op t)) (rebuild-origin t info stop) + :else nil)) +(defn- place-of + "The place a fact about `o`'s value is about: its column, or [c path]." + [o] + (when (and o (not (:rebuilt? o))) + (if (empty? (:path o)) (:col o) [(:col o) (:path o)]))) + (defn- test-facts "[then else]: the facts a branch test proves about columns, as sets of [:pos c k] / [:nonzero c k] (c minus k is positive / nonzero), - [:nonempty c], [:nonnil c] and [:eq c v]." + [:nonempty place], [:nonnil place] and [:eq c v]." [test info stop] - (let [col (fn [e] (:col (origin e info stop))) + (let [col (fn [e] (place-of (origin e info stop))) num (fn [e] (let [o (origin e info stop)] (when (and o (numeric-only? o)) [(:col o) (:net o 0)]))) num-fact (fn [f e] (if-let [[c k] (num e)] #{[f c k]} #{})) @@ -471,31 +528,44 @@ (defn- case-clause-facts "Facts a `case` clause proves: when its test constants are all non-nil, - the scrutinee is non-nil there, and so is the column an element read - like (first x) took it from -- (first nil) is nil." + the scrutinee is non-nil there, and so is every place above it -- (first + nil) is nil." [ast clause info stop] (let [test (:test clause) consts (if (seq? test) test [test]) - scrut (:scrut ast) - col (fn [e] (:col (origin e info stop)))] - (if (and (seq consts) (every? some? consts)) - (into #{} - (comp (remove nil?) (map (fn [c] [:nonnil c]))) - [(col scrut) - (when (contains? '#{first second last peek nth get ffirst} - (core-head scrut info)) - (col (first (:args scrut))))]) + place (place-of (origin (:scrut ast) info stop))] + (if (and place (seq consts) (every? some? consts)) + #{[:nonnil place]} #{}))) +(defn- split-place [place] (if (vector? place) place [place []])) + +(defn- prefix? [p q] + (and (<= (count p) (count q)) (= (seq p) (seq (take (count p) q))))) + +(defn- place-proven? + "A fact of one of `kinds` at the place [c p], or any fact strictly below + it: whatever is below a nil or empty place is nil or empty too." + [kinds c p facts] + (some (fn [[k place]] + (when (contains? #{:nonnil :nonempty} k) + (let [[fc fp] (split-place place)] + (and (= fc c) (prefix? p fp) + (or (> (count fp) (count p)) (contains? kinds k)))))) + facts)) + (defn- proven? [need c facts info] - (if (vector? need) + (if (num-need? need) (let [k (second need)] (or (contains? facts [:pos c k]) (and (contains? (:nat info) c) (contains? facts [:nonzero c k])))) - (case need - :empty (contains? facts [:nonempty c]) - :nil (or (contains? facts [:nonnil c]) (contains? facts [:nonempty c])) - :finite (contains? (:finite info) c)))) + (let [[p need] (if (vector? need) [(second need) (nth need 2)] [[] need])] + (case need + :empty (place-proven? #{:nonempty} c p facts) + :nil (place-proven? #{:nonnil :nonempty} c p facts) + ;; below the column, only reads that keep a collection finite + :finite (and (contains? (:finite info) c) + (every? #(contains? finite-reads (first %)) p)))))) (defn- literal-smaller? [a c facts] (let [v (lit-val a)] @@ -503,13 +573,20 @@ (some (fn [f] (and (= :eq (first f)) (= c (second f)) (< v (nth f 2)))) facts)))) +(defn- place-text + "The place [c p] as the Clojure form that reads it." + [c p] + (reduce (fn [e read] (map (fn [x] (if (= '% x) e x)) read)) (display c) p)) + (defn- need-text [need c] - (let [c (display c)] - (if (vector? need) - (let [k (second need) - v (if (zero? k) (str "`" c "`") (str "`" c "` minus " k))] - (str "`" c "` must first be tested so that " v " is positive (a `pos?` " - "test), or nonzero (a `zero?` test) when `" c "` is a Nat")) + (if (num-need? need) + (let [c (display c) + k (second need) + v (if (zero? k) (str "`" c "`") (str "`" c "` minus " k))] + (str "`" c "` must first be tested so that " v " is positive (a `pos?` " + "test), or nonzero (a `zero?` test) when `" c "` is a Nat")) + (let [[p need] (if (vector? need) [(second need) (nth need 2)] [[] need]) + c (pr-str (place-text c p))] (case need :empty (str "`" c "` must first be tested non-empty (a `seq` or `empty?` test)") :nil (str "`" c "` must first be tested non-nil (a truthiness, `some?` or `seq` test)") diff --git a/src/writ/prove.clj b/src/writ/prove.clj index c6df90a..81ac6fd 100644 --- a/src/writ/prove.clj +++ b/src/writ/prove.clj @@ -534,31 +534,46 @@ (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." + type has a recognizer to say so. An Int return is (integer? call); a + Nat return is that and then (<= 0 call), proved once the call is known + to be an integer. 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. + Callees go first, so a fn may lean on the contracts of the fns it + calls; one that fails is tried again only once a fn its code reaches + has a new contract. 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)) + goal (fn [f ps types nm check & [after]] + (let [call (into [:app f] ps) + pat (into [:app f] (map #(symbol (str "?" %)) ps))] + [[f nm] {:types types :ps ps :after after + :g {:hyps [] :goals [(t/subst check {'%x call})]} + :rule {:name (symbol (str (name f) nm)) + :vars (set (map #(symbol (str "?" %)) ps)) + :types (into {} (map (fn [p] [(symbol (str "?" p)) (types p)])) ps) + :lhs (t/subst check {'%x pat}) + :rhs [:lit true]}}])) 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))) + ret (plain ret) + c (get-in recs [:checks ret])] + :when (and (:params d) (= (count params) (count (:params d)))) :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]}}])) + types (zipmap ps (map plain params))] + g (cond + (and (vector? c) (= :app (head c))) + [(goal f ps types "%contract" c)] + (contains? '#{Int Nat} ret) + (cond-> [(goal f ps types "%contract" [:call 'integer? '%x])] + (= 'Nat ret) + (conj (goal f ps types "%nonneg%contract" + [:call '<= [:lit 0] '%x] [f "%contract"]))) + :else [])] + g)) 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) @@ -567,12 +582,42 @@ #(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) + trace))) + ;; the fns each fn's code calls, itself and transitively + callees (fn [f] (set (keep #(when (= :app (head %)) (second %)) + (some-> (get defs f) :body t/subterms)))) + reach (memoize (fn [f] (loop [seen #{f} todo [f]] + (if-let [x (first todo)] + (let [new (remove seen (callees x))] + (recur (into seen new) (into (subvec todo 1) new))) + seen)))) + ;; callees first, so a proof can lean on what it calls in the + ;; same pass; a Nat's bound after its integer contract + order (vec (sort-by (fn [[f nm]] [(count (reach f)) (str f) (= nm "%nonneg%contract")]) + (keys goals))) + ;; the contracts proved so far that f's code can use + usable (fn [f proved] (set (filter (fn [[g]] (contains? (reach f) g)) proved)))] + ;; a goal that failed is tried again only once a fn its code reaches + ;; has a new contract: nothing else changes what it can prove + (loop [rules [] proved #{} tried {} todo order] + (let [[rules proved tried] + (reduce (fn [[rules proved tried] [f :as k]] + (let [x (get goals k) + have (usable f proved)] + (if (or (and (:after x) (not (contains? proved (:after x)))) + (= have (get tried k))) + [rules proved tried] + (if (attempt rules x) + [(conj rules (:rule x)) (conj proved k) tried] + [rules proved (assoc tried k have)])))) + [rules proved tried] todo) + left (vec (remove proved todo))] + (if (or (= (count left) (count todo)) + (not-any? (fn [[f :as k]] + (not= (get tried k) (usable f proved))) + left)) rules - (recur (into rules (vals done)) (apply dissoc todo (keys done)))))))) + (recur rules proved tried left)))))) (defn definitions "Translate the defns of the target and the spec: [defs own]. pairs is diff --git a/src/writ/prove/rewrite.clj b/src/writ/prove/rewrite.clj index d9197eb..4e7e05f 100644 --- a/src/writ/prove/rewrite.clj +++ b/src/writ/prove/rewrite.clj @@ -234,9 +234,12 @@ (division? ctx t) (and (contains? #{:app :call} (head t)) (proved-integer? ctx t)))) +(declare proved-nat?) + (defn- nat-atom? [ctx a] (or (and (symbol? a) (= 'Nat (get-in ctx [:types a]))) - (and (= :call (head a)) (= 'count (second a))))) + (and (= :call (head a)) (= 'count (second a))) + (and (= :app (head a)) (proved-nat? ctx a)))) (defn- lin-of "{:c const :m {atom coef}} for an integer term, else nil." @@ -920,6 +923,29 @@ (some-> memo (swap! assoc t r)) r)))) +(defn- proved-nat? + "Does a proved contract say (<= 0 t)? A contract's rule is kept as + written, (<= 0 (f ?x)) to true, so it is read here, where t is an atom + of a linear form, not by rewriting." + [ctx t] + (let [memo (:int-memo ctx) + k [:nat t] + hit (some-> memo deref (get k))] + (if (some? hit) + hit + (let [_ (some-> memo (swap! assoc k false)) + r (boolean + (some (fn [{:keys [vars hyp lhs rhs name types]}] + (when (and (nil? hyp) (= [:lit true] rhs) (= :call (head lhs)) + (= '<= (second lhs)) (= [:lit 0] (nth lhs 2 nil)) (= 4 (count lhs))) + (when-let [m (match-term (nth lhs 3) t vars)] + (when (typed? ctx types m) + (swap! (:lemmas-used ctx) conj name) + true)))) + (:lemmas ctx)))] + (some-> memo (swap! assoc k r)) + r)))) + (defn- conjuncts "The parts of a normalised conjunction: (if a b false) and (if a b a), the shapes `and` lowers to." diff --git a/src/writ/prove/scheme.clj b/src/writ/prove/scheme.clj index e6db34a..e65db66 100644 --- a/src/writ/prove/scheme.clj +++ b/src/writ/prove/scheme.clj @@ -345,6 +345,15 @@ ;; 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))) + ;; an unconditional hypothesis that is a linear comparison is a + ;; fact too: the arithmetic reads facts, and a rewrite of the + ;; comparison itself never meets 0 <= h + (f t) with 0 <= (f t) + ctx (reduce (fn [c {:keys [hyp lhs rhs vars]}] + (if (and (nil? hyp) (empty? vars) (= [:lit true] rhs) + (contains? #{:le :ieq} (t/head lhs))) + (rw/assume c lhs true) + c)) + ctx (:ih ctx)) ctx (assoc ctx :memo (atom {}) :stuck (atom #{}) :int-memo (atom {}))] [ctx vacuous (when-not vacuous (rw/normalize ctx g))])) diff --git a/src/writ/spec.clj b/src/writ/spec.clj index 115f11c..79a02c0 100644 --- a/src/writ/spec.clj +++ b/src/writ/spec.clj @@ -1842,6 +1842,28 @@ (spit (cache-file dir spec-ns) (pr-str {:sources sources :proofs proofs})) (catch Throwable _ nil))) +(defn- cached-contracts + "The contracts proved for target, from the cache when they were proved + from the same writ, code, signatures and data; they depend on nothing + else, so a change to a law or a proof namespace keeps them." + [dir target key prove] + (let [f (when dir (io/file dir (str "contracts--" target ".edn"))) + hit (try (when (and f (.exists f)) + (let [c (edn/read-string (slurp f))] + (when (= key (:key c)) (:rules c)))) + (catch Throwable _ nil))] + (or hit + (let [rules (prove) + data {:key key :rules rules}] + ;; kept only when it reads back as itself + (when f + (try (let [text (pr-str data)] + (when (= data (edn/read-string text)) + (.mkdirs (io/file dir)) + (spit f text))) + (catch Throwable _ nil))) + rules)))) + (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." @@ -1906,15 +1928,13 @@ [(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}))) + cache-dir (when-not (= false (:cache opts)) (or (:cache-dir opts) ".writ-cache")) + contracts (delay (let [[ds] @defs] + (cached-contracts cache-dir target + [@writ-version (book/read-forms (source-url target)) sigs tenv] + #(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")) sources (delay (pr-str [@writ-version (book/read-forms (source-url target)) (book/read-forms (source-url spec-ns)) diff --git a/test/writ/gaps_test.clj b/test/writ/gaps_test.clj index f4313db..ed8c8cf 100644 --- a/test/writ/gaps_test.clj +++ b/test/writ/gaps_test.clj @@ -2570,3 +2570,64 @@ [^:many s :- (List writ.kind/Char)] :- writ.kind/Nat (if (empty? s) 0 (+ (if (= (first s) \{) 1 0) (opens (rest s))))) (writ.defn/defn g [] :- writ.kind/Nat (opens "a{b{"))])))) + +;; --- G119: descent through nested matches on declared datatypes ------------- +;; +;; A field of a field is smaller than the column, as long as each read is +;; guarded at its own depth (the inner match's tag test guards the inner +;; read). Putting a matched node's fields back in their places rebuilds +;; that node, which is no larger than it (Bend: nested_literal_rebuild). + +(deftest descent-through-nested-data-matches + (let [tree '(writ.defn/data NatTree (Leaf) (Node Nat NatTree NatTree)) + nlist '(writ.defn/data NatList (Nil) (Cons Nat NatList))] + (testing "a grandchild" + (is (nil? (book-err [tree '(writ.defn/defn ^{:writ/descend true} lm [t :- NatTree] :- Nat + (writ.defn/match t :- NatTree + (Leaf 0) + ((Node v l r) (writ.defn/match l :- NatTree + (Leaf v) + ((Node w ll lr) (lm ll))))))])))) + (testing "two cells at a time" + (is (nil? (book-err [nlist '(writ.defn/defn ^{:writ/descend true} ev [xs :- NatList] :- Nat + (writ.defn/match xs :- NatList + (Nil 0) + ((Cons h t) (writ.defn/match t :- NatList + (Nil h) + ((Cons h2 t2) (+ h (ev t2)))))))])))) + (testing "a one-layer rebuild of a matched field" + (is (nil? (book-err [nlist '(writ.defn/defn ^{:writ/descend true} ev [xs :- NatList] :- Nat + (writ.defn/match xs :- NatList + (Nil 0) + ((Cons h t) (writ.defn/match t :- NatList + (Nil h) + ((Cons h2 t2) (+ h (ev [:Cons h2 t2])))))))])))) + (testing "rebuilding the column itself is not smaller" + (is (re-find #"does not descend" + (book-err [nlist '(writ.defn/defn ^{:writ/descend true} ev [xs :- NatList] :- Nat + (writ.defn/match xs :- NatList + (Nil 0) + ((Cons h t) (ev [:Cons h t]))))])))) + (testing "a rebuild must put each field back in its place" + (is (re-find #"does not descend" + (book-err [tree '(writ.defn/defn ^{:writ/descend true} sw [t :- NatTree] :- Nat + (writ.defn/match t :- NatTree + (Leaf 0) + ((Node v l r) (writ.defn/match l :- NatTree + (Leaf v) + ((Node w ll lr) (sw [:Node w lr ll]))))))])))))) + +(deftest descent-through-nested-seq-reads + (is (nil? (err-msg '(defn f {:writ/descend true} [^:many ^{:writ/type (List Nat)} xs] + (if (seq xs) (if (seq (rest xs)) (f (rest (rest xs))) 0) 0))))) + (testing "each read is guarded at its own depth" + (is (re-find #"`\(rest xs\)` must first be tested non-empty" + (err-msg '(defn f {:writ/descend true} [^:many ^{:writ/type (List Nat)} xs] + (if (seq xs) (f (rest (rest xs))) 0)))))) + (testing "a deeper test guards the reads above it" + (is (nil? (err-msg '(defn f {:writ/descend true} [^:many ^{:writ/type (List Nat)} xs] + (if (seq (rest xs)) (f (rest (rest xs))) 0)))))) + (testing "a rest below an element read needs the element to be finite" + (is (re-find #"finite" + (err-msg '(defn f {:writ/descend true} [^:many ^{:writ/type (List Nat)} xs] + (if (seq xs) (if (seq (first xs)) (f (rest (first xs))) 0) 0))))))) diff --git a/test/writ/proof_test.clj b/test/writ/proof_test.clj index 418cdc3..d1b9d7c 100644 --- a/test/writ/proof_test.clj +++ b/test/writ/proof_test.clj @@ -4,6 +4,8 @@ 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.edn :as edn] + [clojure.java.io :as io] [clojure.string :as str] [writ.spec :as spec])) @@ -79,6 +81,11 @@ (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 "the contracts are kept apart from the laws, keyed on the code" + (let [f (io/file dir "contracts--writ.spec-demo.court.edn") + c (edn/read-string (slurp f))] + (is (.exists f)) + (is (contains? (set (map :name (:rules c))) 'move%contract)))) (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))))) diff --git a/test/writ/prove_test.clj b/test/writ/prove_test.clj index c63df2a..babfe44 100644 --- a/test/writ/prove_test.clj +++ b/test/writ/prove_test.clj @@ -437,7 +437,37 @@ :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)))))) + (is (= '#{insert%contract to-list%contract size%contract size%nonneg%contract} + (set (map :name rules)))))) + +(deftest nat-and-int-contracts-are-proved-from-the-code + (let [forms '[(ns c.nums) + (defn twice [n] (* 2 n)) + (defn down [n] (- n 1)) + (defn total [xs] (if (seq xs) (+ (first xs) (total (rest xs))) 0)) + (defn half-str [s] (str s))] + [defs] (prover/definitions [['c.nums forms]]) + rules (prover/prove-contracts {:defs defs :tenv {} + :sigs '{c.nums/twice {:params [Int] :ret Int} + c.nums/down {:params [Nat] :ret Nat} + c.nums/total {:params [(List Nat)] :ret Nat} + c.nums/half-str {:params [Int] :ret Int}}}) + names (set (map :name rules))] + (testing "an Int return is an integer" + (is (contains? names 'twice%contract))) + (testing "a Nat return is an integer and not negative" + (is (contains? names 'total%contract)) + (is (contains? names 'total%nonneg%contract))) + (testing "a Nat return that can go negative is only an integer" + (is (contains? names 'down%contract)) + (is (not (contains? names 'down%nonneg%contract)))) + (testing "a signature the code does not keep proves nothing" + (is (not (contains? names 'half-str%contract)))) + (testing "a proved contract makes a call an integer term, and a Nat" + (let [ctx (rw/context {:types '{k Nat xs (List Nat)} :lemmas rules})] + (is (rw/int-term? ctx [:app 'c.nums/twice 'k])) + (is (= [:lit true] (rw/normalize ctx [:call '<= [:lit 0] [:app 'c.nums/total 'xs]]))) + (is (not= [:lit true] (rw/normalize ctx [:call '<= [:lit 0] [:app 'c.nums/down 'k]]))))))) ;; --- rewriting under names, facts and floats --------------------------------------