From 3364344031145c5116c925c7d51c8cc004dcdf4e Mon Sep 17 00:00:00 2001 From: Yogthos Date: Thu, 24 Sep 2026 12:43:40 -0400 Subject: [PATCH] Check that the code is wired as the graph plans A review from the agent's side found ways a wrong implementation, or a spec that says less than it seems to, got through: - a spec helper named like a target fn was replaced by the target's, so a law judged the code with the code and was "proved"; that is now an error naming the helper to rename - edges only bounded the code: a signal stuck on green kept every edge. Each target of an edge is now also a law that some value takes the step - two states of one plain type told nothing apart, so the sort's :unsorted -> :sorted edge checked only a list type; that fails now, and the edge into a refinement is the law. An edge mixing a plain target with refined ones fails for the same reason - a public fn with no ann passed unchecked; it fails now, and the report lists signed public fns no graph, machine or flow names New forms: `flow` states the path data takes through a fn and is checked by following values through its lowered source; `calls` takes {:through [..] :not [..]} for reach on the transitive graph; both accept a fn of another namespace, so an effect shell's wiring can be stated. An edge may place its state with `_` and take a state out of a tuple with first/second/last. `spec/plan` prints the spec as a plan a person can confirm before code exists, and `mermaid` draws a graph. Edge laws are written as the target's predicate of the call, and when "never throws" can't be proved for a recursive fn the landing is proved anyway and the report says totality was tested. A law that says the same as a proved one is proved by it when no proof from the code is found. --- README.md | 242 ++++++- examples/README.md | 13 + examples/test/fetch/core_spec.clj | 16 +- examples/test/life/core_spec.clj | 5 +- examples/test/pong/core_spec.clj | 16 +- examples/test/shortener/core_spec.clj | 40 +- skills/writ/SKILL.md | 136 +++- src/writ/spec.clj | 724 ++++++++++++++++--- test/writ/evidence_test.clj | 7 +- test/writ/flow_test.clj | 94 +++ test/writ/graph_test.clj | 89 ++- test/writ/proof_test.clj | 3 +- test/writ/spec_demo/flow_plain_spec.clj | 21 + test/writ/spec_demo/flow_spec.clj | 16 +- test/writ/spec_demo/flow_unknown_spec.clj | 18 + test/writ/spec_demo/links.clj | 6 + test/writ/spec_demo/links_bad_spec.clj | 23 + test/writ/spec_demo/links_spec.clj | 23 + test/writ/spec_demo/nat_chain_spec.clj | 4 +- test/writ/spec_demo/pipeline_layers_spec.clj | 28 + test/writ/spec_demo/pipeline_many.clj | 23 + test/writ/spec_demo/pipeline_spec.clj | 15 +- test/writ/spec_demo/pipeline_swapped.clj | 17 + test/writ/spec_demo/pipeline_upper.clj | 16 + test/writ/spec_demo/readme_sort_spec.clj | 34 + test/writ/spec_demo/shadow.clj | 8 + test/writ/spec_demo/shadow_spec.clj | 19 + test/writ/spec_demo/shell.clj | 12 + test/writ/spec_demo/shell_spec.clj | 30 + test/writ/spec_demo/signal_mixed_spec.clj | 20 + test/writ/spec_demo/signal_stuck.clj | 15 + test/writ/spec_demo/sort_every_spec.clj | 8 +- test/writ/spec_demo/sort_extra.clj | 16 + test/writ/spec_demo/sort_lemma_spec.clj | 11 +- test/writ/spec_demo/sort_let_spec.clj | 8 +- test/writ/spec_demo/sort_pairs_spec.clj | 8 +- test/writ/spec_demo/sort_proved_spec.clj | 14 +- test/writ/spec_demo/sort_spec.clj | 16 +- test/writ/spec_demo/sort_unproved_spec.clj | 14 +- test/writ/spec_demo/sort_vacuous_spec.clj | 8 +- test/writ/spec_demo/sort_weak_spec.clj | 8 +- test/writ/spec_demo/total_spec.clj | 4 +- test/writ/spec_demo/tree_spec.clj | 5 +- test/writ/spec_test.clj | 33 +- test/writ/test_runner.clj | 5 +- 45 files changed, 1650 insertions(+), 241 deletions(-) create mode 100644 test/writ/flow_test.clj create mode 100644 test/writ/spec_demo/flow_plain_spec.clj create mode 100644 test/writ/spec_demo/flow_unknown_spec.clj create mode 100644 test/writ/spec_demo/links.clj create mode 100644 test/writ/spec_demo/links_bad_spec.clj create mode 100644 test/writ/spec_demo/links_spec.clj create mode 100644 test/writ/spec_demo/pipeline_layers_spec.clj create mode 100644 test/writ/spec_demo/pipeline_many.clj create mode 100644 test/writ/spec_demo/pipeline_swapped.clj create mode 100644 test/writ/spec_demo/pipeline_upper.clj create mode 100644 test/writ/spec_demo/readme_sort_spec.clj create mode 100644 test/writ/spec_demo/shadow.clj create mode 100644 test/writ/spec_demo/shadow_spec.clj create mode 100644 test/writ/spec_demo/shell.clj create mode 100644 test/writ/spec_demo/shell_spec.clj create mode 100644 test/writ/spec_demo/signal_mixed_spec.clj create mode 100644 test/writ/spec_demo/signal_stuck.clj create mode 100644 test/writ/spec_demo/sort_extra.clj diff --git a/README.md b/README.md index 61a39e4..3f04560 100644 --- a/README.md +++ b/README.md @@ -44,14 +44,20 @@ test/my/sort_test.clj runs the check 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 + It is the first thing a spec says. writ proves each of its edges, and + checks that the code takes every step the graph names. +2. Say how the steps are wired: `flow` for the path data takes through a + fn, `calls` for the layers it goes through. +3. 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 +4. Read the plan back: `(spec/plan 'my.sort-spec)` prints the states, + steps, signatures, laws and wiring from the spec alone, for a person + to confirm before any code is written. +5. Write the implementation as ordinary Clojure. +6. 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. +7. 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. @@ -93,34 +99,35 @@ The spec: ```clojure (ns my.sort-spec - (:require [writ.spec :refer [spec ann law graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (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))) +;; what makes a list sorted +(refine Sorted [xs (List Nat)] (ascending? xs)) + +;; the problem's states: a list goes in, a sorted list comes out, and +;; inserting into a sorted list keeps it sorted (`_` is where the state goes) +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}} + :sorted {[insert Nat _] #{:sorted}}}}) + (defn occurrences [x xs] (count (filter #(= x %) xs))) -;; a sort puts its input in order... -(law sorted (forall [xs (List Nat)] (ascending? (isort xs)))) - -;; ...and keeps every element, duplicates included +;; the graph already says a sort puts its input in order; it also +;; keeps every element, duplicates included (law permutation (forall [x Nat, xs (List Nat)] (= (occurrences x (isort xs)) (occurrences x xs)))) -;; insert keeps an ordered list ordered, and adds exactly one x -(law insert-keeps-sorted (forall [x Nat, xs (List Nat)] - (=> (ascending? xs) (ascending? (insert x xs))))) +;; and insert adds exactly one x (law insert-adds (forall [x Nat, xs (List Nat)] (= (occurrences x (insert x xs)) (inc (occurrences x xs))))) ``` @@ -137,7 +144,11 @@ The check: (is (:ok r) (:message r)))) ``` -If `insert` dropped a value equal to the head, the report would read: +The graph's edges are laws: `sorting:unsorted:isort` says every list +`isort` returns is `Sorted`, and `sorting:sorted:insert` that `insert` +keeps a sorted list sorted. Each step the graph names must also be taken, +by some input. If `insert` dropped a value equal to the head, the report +would read: ``` writ.spec: my.sort-spec against my.sort: FAILED @@ -229,23 +240,35 @@ sufficient. ## Writing a spec -A spec namespace requires `writ.spec` and uses six forms. +A spec namespace requires `writ.spec` and uses these forms. - `(spec target.ns)` names the namespace it constrains. It comes first. - `(ann f [A B -> R])` gives fn `f` its parameter and return types. Every - public fn should have one; the report lists the ones that don't. A - private helper that recurses over a collection needs one too, because - writ has to know the collection is finite to accept the recursion. + public fn needs one: a public fn with no `ann` fails the check, since + nothing would check it. Sign it if the plan has it, or make it private + with `defn-` if it is a helper. A private helper that recurses over a + collection needs an `ann` too, because writ has to know the collection + is finite to accept the recursion. +- `(refine Name [x Base] pred)` is a type: the values of `Base` where + `pred` holds. See [Refinements](#refinements). +- `(graph name {...})` is the problem's states and the steps between them. + See [The state graph](#the-state-graph). - `(data Name Ctor (Ctor2 FieldType ...) ...)` declares a datatype the target's values use. `(data Box [a] (Wrap a))` takes type parameters. - `(law name proposition)` states a law. -- `(calls f [g ...])` states exactly which fns `f` calls. See +- `(calls f [g ...])` states exactly which fns `f` calls, and + `(calls f {:through [g] :not [h]})` what it reaches. See [The call graph](#the-call-graph). +- `(flow f [param ...] [link link ...] ...)` states the path data takes + through `f`. See [Flows](#flows). - `(machine name {...})` states that a fn steps a state machine by a transition table. See [Machines](#machines). A spec may define its own helper fns, like `ascending?` above. They run -only when laws run. +only when laws run. A helper may not share a name with a public fn of the +target: a law's free name is read as the target's fn first, so the helper +would silently be replaced by the code it is meant to judge. writ rejects +the spec instead, and says which name to rename. ### Types @@ -326,7 +349,23 @@ rule. Every law still holds. `calls` states the structure: ``` `(calls f [g ...])` means `f`'s direct calls are exactly that set, no -more and no fewer. The call graph is read from `f`'s source: +more and no fewer. A plan often knows the layers but not every helper, so +the map form states reach instead: + +```clojure +(calls handle {:through [normalize respond] :not [str/upper-case]}) +``` + +`:through` names fns `handle` must reach, directly or through any chain +of the namespace's own fns; `:not` names fns it must never reach. A +reach that breaks the rule is reported with its path: + +``` +the call graph of `handle` is not the one the spec gives + `handle` reaches `clojure.string/upper-case`, which the spec says it never does: handle -> normalize -> clojure.string/upper-case +``` + +The call graph is read from `f`'s source: - A simple name is one of the target's own fns. A qualified name is a fn of another namespace, resolved through the spec's aliases, so @@ -357,6 +396,12 @@ doesn't look at the store. Its call set names the stray call: list``. [examples/](examples/README.md#shortener) has this case, run against a real server. +`f` may be a fn of another namespace, named through the spec's aliases. +That is how a spec reaches the effect shell, which writ doesn't check but +which is where the core gets called: `(calls server/app {:through +[core/handle]})` fails if the shell answers requests some other way. In +such a form, a simple name is a fn of that namespace. + `(spec/call-graph 'my.ns)` returns the graph of any namespace as `{f #{g ...}}`. It reads the source without loading or checking it, so it works on effect code too, and it's the quickest way to write a first @@ -421,29 +466,59 @@ its edges are the fns that step between them: :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: +An edge's key is the fn and the types of its other arguments. The state +is the first argument unless `_` marks where it goes: `[move-paddle Key]` +is `(move-paddle state key)` for every `Key`, and `[insert Nat _]` is +`(insert n state)`. An edge out of a tuple state may take a part of it +with `first`, `second` or `last`, which is how a fn that returns the next +state with something else leads back round: `{:result {[first] +#{:links}}}`. writ checks the graph four 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: + the states it names, and it never throws. The law is the target's + predicate applied to the call, `(Sorted? (isort xs))` read as + `(ascending? (isort xs))`, so it is proved the way the spec's own laws + are. 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 ``` +- **Each step is taken.** An edge only bounds the code, and code that + never leaves its state keeps every bound. So each target of an edge is + also a law, `signal:green:tick->yellow`: some value of the state, and + some arguments, land there. A signal stuck on green fails it: + + ``` + law `signal:green:tick->yellow` fails + the graph says a tick can take green to yellow, but no generated green does + ``` - **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. + to b passes a. + +What that adds up to: with every edge proved, `:never` and `:before` +hold for every run of the code, since a run only takes edges the graph +has. Reachability and `:final` are about the steps, each of which some +value of its state takes; they do not promise that a run from the start +gets there. + +States must say what sets them apart. Two states of the same plain type, +like `:unsorted (List Nat)` and `:sorted (List Nat)`, fail the check: a +value of one is a value of the other, so an edge between them checks the +type and nothing else, and the names say more than the graph does. Make +the state that means something a refinement, `(refine Sorted [xs (List +Nat)] (ascending? xs))`, and the edge into it is the law. For the same +reason an edge may not list a plain state beside refined ones: every +result is in the plain one. Define a refinement with the same helpers the +laws use, so the prover sees one vocabulary. 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, @@ -452,6 +527,10 @@ 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. +`(spec/mermaid 'my.spec {:graph 'signal})` draws a graph as a mermaid +`stateDiagram-v2`, and `(spec/plan 'my.spec)` prints it with the rest of +the plan; see [Other entry points](#other-entry-points). + ### Machines Some code is a state machine: a screen flow, a protocol, an order's @@ -510,6 +589,55 @@ The table also takes part in the adequacy check as a law would, so a machine alone pins its step fn down. `(spec/mermaid 'my.spec {:machine 'screens})` draws the table as a mermaid `stateDiagram-v2`. +A machine and a graph differ where it matters. A machine's states and +events are values, `:start` is a value, and its table is exact: every +pair is run, and a pair the table doesn't list must keep the state. A +graph's states are types, `:start` is a state's name (or `[state +value]`), and an edge says where a step may go and that it can: pairs +the graph doesn't list are unconstrained. Use a machine when the +meaning is a finite table, and a graph when the states are sets of +values. + +### Flows + +`calls` says which fns are called. It doesn't say what they are given: a +fn can call every layer the spec names and still hand the second one the +raw input, throwing the first one's work away. `flow` states the path the +data takes: + +```clojure +(flow handle [req] + [req normalize respond :result] + [normalize :result]) +``` + +The vector after the fn names its parameters, by position, so the spec +never depends on what the code calls them. Each chain after it is a path, +and every link must reach the next: + +- `a` reaches fn `b` when some call the fn makes to `b` is passed a value + that comes from `a`: from the parameter `a`, or from what a call to fn + `a` returned, directly or through other calls. +- `a` reaches `:result` when what the fn returns comes from `a`. A + branch's test counts, so a check that decides the answer reaches it. +- A lambda passed to a fn, as in `(map (fn [x] (step x)) xs)`, is given + that call's other arguments, and so is a fn passed by name. A loop's + bindings carry what each `recur` passes. + +The check reads the fn's source. A flow that the code breaks names the +link: + +``` +the flow of `handle` is not the one the spec gives + `respond` is never given anything that comes from `normalize` + what `handle` returns does not come from `normalize` +``` + +A flow names only parameters and fns; a name that is neither, or a +parameter count that doesn't match, fails the check. Like `calls`, a flow +may be about a fn of another namespace, such as an effect shell. A fn a +flow names is a step of the plan, like a graph's edge fns. + ## Running the check `(writ.spec/check 'my.sort-spec)` returns a report map: @@ -525,8 +653,11 @@ machine alone pins its step fn down. `(spec/mermaid 'my.spec {:machine :gaps [] ; fns the laws don't pin down :rejected [{:fn isort ...}] ; per fn: its laws and the stand-ins they rejected :calls [{:fn handle :calls [normalize respond] :status :ok} ...] + :flows [{:fn handle :chains ["req -> normalize -> respond -> result"] :status :ok} ...] + :graphs [{:graph sorting :status :ok :states 2 :edges 2} ...] :machines [{:machine screens :status :ok :states 6 :events 7} ...] - :unspecified [] ; public fns with no ann + :unspecified [] ; public fns with no ann: each fails the check + :off-graph [] ; signed public fns no graph, machine or flow names :message "writ.spec: my.sort-spec against my.sort: ok\n `insert`: ..."} ``` @@ -534,7 +665,9 @@ It works in three stages, and each runs only if the one before passed. 1. **Static.** writ reads the target's source from the classpath, puts the `ann` types on its `defn`s and checks it (see below). If this fails, - `:static` carries the error and no law runs. + `:static` carries the error and no law runs. Nor does one run when a + helper of the spec shares a name with a public fn of the target; + `:ambiguous` names it. 2. **Laws.** Each law gets a `:status`: - `:vacuous`: it holds whatever the code does, so it fails; see [What a spec should say](#what-a-spec-should-say). @@ -570,7 +703,11 @@ It works in three stages, and each runs only if the one before passed. The `calls` forms are checked once the static stage passes, beside the laws, and each gets an entry in `:calls` with `:status` `:ok` or -`:failed`, plus `:missing` and `:extra` when it failed. Each `machine` +`:failed`, plus `:missing` and `:extra` when it failed (`:unreached` and +`:reached` for the map form). Each `flow` gets an entry in `:flows`, with +`:errors` when it failed. A passing report lists the signed public fns +that no graph, machine or flow names, as `not a step of any graph or +machine`: a public helper is fine, but a reader should see it. Each `machine` gets an entry in `:machines`; a failed one carries `:mismatches`, one `{:state :event :expected :actual}` per pair the code gets wrong, and `:errors` for the table's own rules. @@ -887,7 +1024,38 @@ The report map has the same in `:forms`, one entry per form with argument and return checks for use at the REPL, and `unstrument` removes them. `(spec/sample '(List Nat) {} 5)` shows what a type generates. `(spec/call-graph 'my.ns)` and `(spec/mermaid 'my.ns)` read a namespace's -call graph; see [The call graph](#the-call-graph). +call graph; see [The call graph](#the-call-graph). `(spec/flow-facts 'my.ns +'f)` shows what `flow` reads: each call `f` makes, with where each +argument's value comes from, and where its result comes from. + +`(spec/plan 'my.spec)` prints the spec as a plan for a person to read and +confirm, from the spec alone, so it works before the code exists: each +graph's states, with a refinement's predicate spelled out, and its steps +and rules; each signed fn with its signature, the laws that name it, its +flows and its call set; and the wiring the spec gives fns outside the +target, such as a shell's. + +``` +plan: my.pipeline-spec for my.pipeline + +graph `request` + states + :raw String + :clean Clean, a String where (= s (cleaned s)) + :response (Tuple Keyword String) + steps + :raw -[normalize]-> :clean + :clean -[respond]-> :response + +fns + handle [String -> (Tuple Keyword String)] + laws: handle-answers-with-the-cleaned-input, ok-exactly-when-short + flow: s -> normalize -> respond -> result + calls exactly: normalize, respond +``` + +`(spec/mermaid 'my.spec {:graph 'g})` draws graph `g` as a mermaid +`stateDiagram-v2`. ## What the static check enforces diff --git a/examples/README.md b/examples/README.md index 79dab66..984e1ac 100644 --- a/examples/README.md +++ b/examples/README.md @@ -336,6 +336,19 @@ What writ catches: Writ: `println` in `shorten` is effect code (...); writ checks pure data-and-functions code only ``` +The spec also says how the data moves. `flow` forms state that `handle` +passes the path to `route` and on to `follow`, and the body to `shorten`, +and that `shorten` validates the normalized URL, not the raw body. The +same forms reach into the server, which writ doesn't check: `app` must +answer each request with `shortener.core/handle`, through +`shortener.store/transact!`, and build its response from `handle`'s +reply. The server's source is read for this, never loaded: + +```clojure +(calls shortener.server/app {:through [shortener.core/handle shortener.store/transact!]}) +(flow shortener.server/app [req] [req shortener.core/handle response :result]) +``` + `scan` reads the server namespace, which writ can't check, and follows the effect up the call graph: diff --git a/examples/test/fetch/core_spec.clj b/examples/test/fetch/core_spec.clj index 1e3a14c..f0b0f21 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 refine graph law]])) + [writ.spec :refer [spec data ann refine graph flow law]])) (spec fetch.core) @@ -27,14 +27,26 @@ ;; a wait is never shorter than the base or longer than the cap (refine Delay [ms Nat] (<= base-ms ms cap-ms)) +;; an HTTP status, or 0 when no response came back +(refine Status [n Nat] (<= n 599)) + (graph retry - {:states {:status Nat, :class Class, :attempt Nat, :delay Delay, + {:states {:status Status, :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}}}}) +;; next-action is the steps above put together: the status is classified, +;; a retry waits by the backoff for its attempt, and only a repeatable +;; request is retried +(flow next-action [method status attempt] + [status classify :result] + [attempt backoff-ms :result] + [method repeatable? :result] + [status repeatable?]) + (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/life/core_spec.clj b/examples/test/life/core_spec.clj index 2d9a179..0df0b12 100644 --- a/examples/test/life/core_spec.clj +++ b/examples/test/life/core_spec.clj @@ -12,7 +12,7 @@ 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]])) + (:require [writ.spec :refer [spec ann refine graph flow law]])) (spec life.core {:require :proved}) @@ -28,6 +28,9 @@ :edges {:cell {[neighbours] #{:around}} :world {[step] #{:world}}}}) +;; a step looks at the live cells and the cells around them +(flow step [world] [world neighbours :result]) + ;; --- the rule, cell by cell ------------------------------------------------------ (def offsets [[-1 -1] [0 -1] [1 -1] [-1 0] [1 0] [-1 1] [0 1] [1 1]]) diff --git a/examples/test/pong/core_spec.clj b/examples/test/pong/core_spec.clj index 25d6130..028b27a 100644 --- a/examples/test/pong/core_spec.clj +++ b/examples/test/pong/core_spec.clj @@ -8,7 +8,7 @@ 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 refine graph law]])) + [writ.spec :refer [spec data ann refine graph flow law]])) (spec pong.core {:require :proved}) @@ -60,6 +60,20 @@ :won {[step Key] #{:won :serving}}} :before [[:playing :won]]}) +;; a tick of play: the key moves the left paddle, the ball draws the +;; right one, and the ball moves against both +(flow play [ball ly ry ls rs key] + [key move-paddle advance :result] + [ball track advance] + [ball advance :result]) + +;; step hands the game and the key to play, and moves the paddle while +;; a serve counts down +(flow step [game key] + [game play :result] + [key play] + [key move-paddle :result]) + ;; --- paddles ------------------------------------------------------------------- (law a-paddle-never-leaves-the-court diff --git a/examples/test/shortener/core_spec.clj b/examples/test/shortener/core_spec.clj index a6ecc1a..9fd49bc 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 refine graph law calls]])) + [writ.spec :refer [spec data ann refine graph flow law calls]])) (spec shortener.core) @@ -36,18 +36,24 @@ ;; 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))) +;; a URL as it is stored: no surrounding space +(refine Trimmed [s String] (= s (str/trim s))) + (graph shortener - {:states {:id Nat, :code Code, :text String, :url String, :verdict Bool, + {:states {:id Nat, :code Code, :text String, :url Trimmed, :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}} + :code {[decode-id] #{:id}} + :text {[normalize-url] #{:url}, [valid-code?] #{:verdict}} + :url {[valid-url?] #{:verdict}} :method {[route String] #{:route}} :links {[shorten String] #{:result} [follow String] #{:reply} - [handle Keyword String String] #{:result}}}}) + [handle Keyword String String] #{:result}} + ;; the links after a request are the links for the next one + :result {[first] #{:links}}}}) ;; --- the call graph ------------------------------------------------------------ @@ -60,6 +66,30 @@ (calls encode-id []) (calls normalize-url [str/trim]) +;; --- the data flow ----------------------------------------------------------------- + +;; handle routes the request, and the route decides the reply: a new link +;; is made from the body, a code from the path is followed in the links +(flow handle [links method path body] + [method route :result] + [path route follow :result] + [body shorten :result] + [links shorten] + [links follow]) + +;; the shell, which writ does not check, still answers every request +;; with handle, run against the store, and turns handle's reply into the +;; response. Its source is read, never loaded. +(calls shortener.server/app {:through [shortener.core/handle shortener.store/transact!]}) +(flow shortener.server/app [req] [req shortener.core/handle response :result]) + +;; the body is normalized, the normalized URL is what is validated and +;; stored, and a new code comes from the store's size +(flow shorten [links body] + [body normalize-url valid-url? :result] + [normalize-url :result] + [links encode-id :result]) + ;; --- vocabulary ------------------------------------------------------------------- (defn big diff --git a/skills/writ/SKILL.md b/skills/writ/SKILL.md index 2465e23..a91f404 100644 --- a/skills/writ/SKILL.md +++ b/skills/writ/SKILL.md @@ -3,7 +3,7 @@ name: writ description: >- 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 + spec/graph/refine/ann/data/law/calls/flow/machine/plan) -- 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, @@ -41,9 +41,16 @@ names what is wrong. writ runs on jolt; writ.spec uses test.check. 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 +3. `ann` for each public fn. A public fn with no `ann` fails the check; + a helper the plan doesn't name should be private (`defn-`). +4. The wiring: `flow` for the path data takes through each fn that + composes steps, `calls` for the layers it must (or must not) reach. + See [Flows](#flows) and [The call graph](#the-call-graph). +5. Laws for what each step means. +6. Show the plan: `(spec/plan 'my.spec)` prints states, steps, signatures, + laws and wiring from the spec alone. When a person asked for the + feature, show it to them and have them confirm it before writing code. +7. 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. @@ -63,44 +70,61 @@ names what is wrong. writ runs on jolt; writ.spec uses test.check. :before [[:yellow :red]]}) ; also :never [[a b]], :final [s] ``` +- The state is the fn's first argument, unless `_` marks it: + `[insert Nat _]` is `(insert n state)`. `[first]`, `[second]` or + `[last]` takes a state out of a tuple state, so a fn that returns + `[next-state reply]` can lead back: `{:result {[first] #{:links}}}`. - `(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. +- Each edge's fn must fit by its `ann`: the state's param (first, or at + `_`) = the state's base type, the others 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. + throws. It is tested and proved like any law, and reads as the target's + predicate of the call, `(ascending? (isort xs))`. +- Each target of such an edge is also a law, `graph:state:fn->target`: + some value of the state lands there. A step the code never takes fails, + so don't list targets "just in case"; list the steps the problem has. +- Two states of the same plain type fail the check (`:unsorted` and + `:sorted` both `(List Nat)` say nothing apart). Make the meaningful one + a refinement, defined with the helpers the laws use: + `(refine Sorted [xs (List Nat)] (ascending? xs))`, and the edge into it + is the sort's law. An edge may not list a plain state beside refined + ones either. +- An edge into plain types of their own 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, `:never` and `:before` hold for every run of the + code. Reachability and `:final` say each step can happen, not that a + run from the start gets there. ## A spec ```clojure (ns my.sort-spec - (:require [writ.spec :refer [spec data ann law graph]])) + (:require [writ.spec :refer [spec data ann law graph refine]])) (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)]) (defn ascending? [xs] (or (empty? xs) (apply <= xs))) ; the spec's own (defn occurrences [x xs] (count (filter #(= x %) xs))) ; vocabulary -(law sorted (forall [xs (List Nat)] (ascending? (isort xs)))) +(refine Sorted [xs (List Nat)] (ascending? xs)) + +(graph sorting ; its edges are the laws + {:states {:unsorted (List Nat), :sorted Sorted} ; "isort sorts" and + :edges {:unsorted {[isort] #{:sorted}} ; "insert keeps it sorted" + :sorted {[insert Nat _] #{:sorted}}}}) + (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))))) ``` @@ -127,13 +151,19 @@ names what is wrong. writ runs on jolt; writ.spec uses test.check. - any expression, which holds when it is truthy A free name refers first to the target's public fns, then to the spec's - helpers, then to clojure.core. Laws cannot quantify over fn types, - because no generator exists for them. + helpers, then to clojure.core. A spec helper may not share a name with + a target public fn: the check fails and says to rename the helper. + Laws cannot quantify over fn types, because no generator exists for + them. - `(calls f [g str/join])`: `f`'s direct calls are exactly this set. A simple name is a target fn; a qualified one is a fn of another namespace, through the spec's aliases. Called or passed as a value both count. clojure.core, host members, self-recursion and locals that - shadow a fn do not. See [The call graph](#the-call-graph). + shadow a fn do not. `(calls f {:through [g] :not [h]})` states reach + instead: `f` reaches `g` through any chain of its namespace's fns, and + never reaches `h`. See [The call graph](#the-call-graph). +- `(flow f [param ...] [link link ...] ...)`: the path data takes through + `f`. See [Flows](#flows). ## The proof namespace @@ -207,6 +237,29 @@ or bypasses passes every law and still fails `calls`. self-recursion, and `scan` reports every caller of a fn writ cannot check ("it uses `f`, which writ cannot check"). +## Flows + +```clojure +(flow handle [req] ; handle's params, by position + [req normalize respond :result] ; req goes to normalize, its result to respond, + [normalize :result]) ; respond's to the result; the answer uses normalize +``` + +A link is a parameter, a fn (what it returns) or, last, `:result`. `a` +reaches fn `b` when some call to `b` is passed a value that comes from +`a`, directly or through other calls; `a` reaches `:result` when the +return value comes from it, a branch's test included. Lambdas passed to a +fn get the call's other arguments, as do fns passed by name; loops carry +what `recur` passes. `calls` says which fns are called; `flow` says what +they are given, which catches a fn that calls every layer but hands one +the raw input. + +Write a flow for each fn that composes steps: a handler, a `step` that +dispatches, a policy built from smaller rules. `f` may be a fn of another +namespace, such as the effect shell (`(flow server/app [req] [req +core/handle :result])`); there, simple names are that namespace's fns. +`(spec/flow-facts 'my.ns 'f)` shows what the check reads. + ## What a spec should say A spec says what makes an answer right, in the problem's terms, for every @@ -313,6 +366,9 @@ value anywhere else is rejected. (spec/call-graph 'my.ns) ; {f #{g ...}}, read from source (spec/mermaid 'my.spec) ; the graph, with the spec's calls (spec/mermaid 'my.spec {:machine 'm}) ; a machine's table as a state diagram +(spec/mermaid 'my.spec {:graph 'g}) ; a state graph as a state diagram +(spec/plan 'my.spec) ; the plan, for a person to confirm +(spec/flow-facts 'my.ns 'f) ; what `flow` reads from f (spec/instrument 'my.sort-spec) ; runtime arg/return checks ``` @@ -343,10 +399,13 @@ law runs until it is fixed. After that, each law has a `:status`: - 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. +- `graph `g`: ... ` lines: edges proved, each of their steps taken, 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. +- `not a step of any graph or machine: f` on a passing report: a signed + public fn the plan doesn't place. Fine for a helper laws need to name; + otherwise it belongs on the graph or in a flow. - ``declares no state graph``: add the graph first. - `:lemmas` in the report: the proof namespace's lemmas; each must be `:proved`. @@ -399,9 +458,26 @@ confirm it, then without one. that the stand-in breaks. If you own only the implementation, report the gap to the spec's owner; the code is not at fault. - ``the call graph of `f` is not the one the spec gives`` - `f` calls a - fn the spec does not list, or does not call one it lists. Route the - call through the named fn (don't inline it, don't skip a layer). If the - graph in the spec is wrong, say so; don't edit `calls` to match. + fn the spec does not list, or does not call one it lists, or (map form) + does not reach a `:through` fn or reaches a `:not` one, with the path. + Route the call through the named fn (don't inline it, don't skip a + layer). If the graph in the spec is wrong, say so; don't edit `calls` + to match. +- ``the flow of `f` is not the one the spec gives`` - ``` `b` is never + given anything that comes from `a` ``` means pass `b` what `a` + returns (or the parameter `a`), not something else; ``` `f` never calls + `b` ``` means the step is missing; ``what `f` returns does not come from + `a` `` means `a`'s result is computed and dropped. Fix the wiring. +- ``law `g:s:f->t` fails ... the graph says a f can take s to t, but no + generated s does`` - the code never takes that step. Usually the code + is stuck (a missing transition); if the step truly cannot happen, the + graph is wrong: say so. +- ``graph `g`: :a and :b are both T, so nothing tells them apart`` - make + one (or both) a refinement that says what it means. +- ``` `x` is defined by the spec and by ns ``` - rename the spec's helper; + a law would otherwise judge the code with the code. +- ``` `f` is public, but the spec gives it no signature ``` - sign it if + the plan has it; make it private (`defn-`) if it is a helper. - ``the spec says `f` calls `g`, but ns defines no fn `g` `` / ``the spec gives `f` a call set, but ns defines no fn `f` `` - define it or fix the spelling; the spec names the structure. diff --git a/src/writ/spec.clj b/src/writ/spec.clj index 115f11c..df71ce7 100644 --- a/src/writ/spec.clj +++ b/src/writ/spec.clj @@ -100,6 +100,7 @@ :graph (update e :graphs (fnil conj []) v) :data (update e :data conj v) :calls (update e :calls (fnil conj []) v) + :flow (update e :flows (fnil conj []) v) :machine (update e :machines (fnil conj []) v) :ann (assoc-in e [:anns (first v)] (second v)) :law (update e :laws conj v)))) @@ -156,17 +157,60 @@ g)) (defmacro calls - "State exactly which fns `f` calls: (calls f [g str/join]). A simple - name is a fn of the target; a qualified one is a fn of another + "State how `f` calls: + + (calls f [g str/join]) ; exactly these, directly + (calls f {:through [g h] :not [io/x]}) ; reaches g and h, never io/x + + A simple name is a fn of the target; a qualified one is a fn of another namespace, through the spec's own aliases. clojure.core and host members are not part of the call graph, and neither is `f` calling - itself." + itself. The map form is read on the transitive graph: `f` reaches `g` + through any chain of the namespace's own fns. `f` itself may be + qualified, a fn of another namespace such as an effect shell; its + simple names are then that namespace's own fns." [f gs] - (when-not (simple-sym? f) - (fail! "`calls` needs a simple fn name, had: `" (pr-str f) "`")) - (when-not (and (vector? gs) (every? symbol? gs)) - (fail! "`calls " f "` needs a vector of fn names, had: " (pr-str gs))) - `(-register! '~(ns-name *ns*) :calls '~[f (mapv resolve-callee gs)])) + (when-not (symbol? f) + (fail! "`calls` needs a fn name, had: `" (pr-str f) "`")) + (let [names? #(and (vector? %) (every? symbol? %))] + (when-not (or (names? gs) + (and (map? gs) (seq gs) (every? #{:through :not} (keys gs)) (every? names? (vals gs)))) + (fail! "`calls " f "` needs a vector of fn names, or {:through [fn ...] :not [fn ...]}, had: " + (pr-str gs))) + `(-register! '~(ns-name *ns*) :calls + '~[(resolve-callee f) + (if (map? gs) (update-vals gs #(mapv resolve-callee %)) (mapv resolve-callee gs))]))) + +(defmacro flow + "State how data moves through fn `f`: + + (flow handle [req] + [req normalize respond :result]) + + The vector after `f` names its parameters, by position, for the chains + that follow. Each chain is a path the data takes: every link reaches + the next. A link is a parameter, a fn (what it returns), or, last, + `:result`, what `f` returns. `a` reaches fn `b` when some call `f` + makes to `b` is passed a value that comes from `a`, directly or through + other calls; it reaches `:result` when what `f` returns comes from it. + A branch's test counts: a value that decides the answer reaches it." + [f params & chains] + (let [where (str "`flow " f "`")] + (when-not (and (symbol? f) (vector? params) (every? simple-sym? params)) + (fail! where " is (flow f [param ...] [link link ...] ...), had: " + (pr-str (list* 'flow f params chains)))) + (when (empty? chains) + (fail! where " needs at least one chain: [link link ...]")) + (doseq [c chains] + (when-not (and (vector? c) (<= 2 (count c))) + (fail! where ": a chain needs at least two links, had " (pr-str c))) + (doseq [l c] + (when-not (or (symbol? l) (= :result l)) + (fail! where ": a link is a parameter, a fn or :result, had " (pr-str l)))) + (when (some #{:result} (butlast c)) + (fail! where ": `:result` can only end a chain, had " (pr-str c)))) + `(-register! '~(ns-name *ns*) :flow + '~[(resolve-callee f) params (mapv (fn [c] (mapv #(if (symbol? %) (resolve-callee %) %) c)) chains)]))) (defmacro machine "State that a target fn steps a state machine by a transition table: @@ -214,6 +258,11 @@ (def ^:private graph-keys #{:states :edges :start :never :before :final}) +(def ^:private projections + "clojure.core fns an edge may use to take a state out of a tuple state: + the tuple element's position, from its arity." + {'first (constantly 0), 'second (constantly 1), 'last dec}) + (defmacro graph "The problem's state graph. Its states are types, most often refinements; its edges are fns, each from a state to the states its @@ -253,6 +302,11 @@ (doseq [[k tos] es] (when-not (and (vector? k) (simple-sym? (first k))) (fail! where ": an edge from " (pr-str from) " is keyed [fn ArgType ...], had " (pr-str k))) + (when (< 1 (count (filter #{'_} (rest k)))) + (fail! where ": the edge " (pr-str from) " " (pr-str k) " marks the state with `_` more than once")) + (when (and (contains? projections (first k)) (next k)) + (fail! where ": the edge " (pr-str from) " " (pr-str k) " -- `" (first k) + "` takes the state alone, a " (pr-str (get (:states m) from)))) (when-not (and (coll? tos) (seq tos)) (fail! where ": the edge " (pr-str from) " " (pr-str k) " needs a set of target states")) (doseq [t tos] @@ -723,6 +777,12 @@ (let [[_ [x t] body] p] (recur body (conj bs [x t]))) [bs p]))) +(defn- leading-exists [p] + (loop [p p, bs []] + (if (head? p "exists") + (let [[_ [x t] body] p] (recur body (conj bs [x t]))) + [bs p]))) + (defn- test-law [ctx {:keys [name prop]} {:keys [trials seed max-size]}] (let [[bs body] (leading-foralls prop) @@ -739,15 +799,17 @@ ;; existential: a witness is a counterexample to its negation, so ;; test.check finds it and shrinks it to the simplest one (and (empty? bs) (head? body "exists")) - (let [[_ [x t] inner] body - ctx* (assoc ctx :vars [x]) - res (qc (prop/for-all* [(type->gen t (:tenv ctx))] - (fn [v] (not= :pass (:result (holds ctx* inner {x v}))))))] + (let [[ebs inner] (leading-exists body) + xs (mapv first ebs) + ctx* (assoc ctx :vars xs) + res (qc (prop/for-all* (mapv #(type->gen (second %) (:tenv ctx)) ebs) + (fn [& vs] (not= :pass (:result (holds ctx* inner (zipmap xs vs)))))))] (if (:pass? res) {:law name :status :failed :counterexample {} :seed (:seed res) - :detail [[body (str "no witness among " (:num-tests res) " generated values")]]} + :detail [[(list 'exists (vec (apply concat ebs)) '...) + (str "no witness among " (:num-tests res) " generated values")]]} {:law name :status :witnessed :seed (:seed res) - :witness {x (first (get-in res [:shrunk :smallest]))}})) + :witness (zipmap xs (get-in res [:shrunk :smallest]))})) :else (let [vars (mapv first bs) @@ -1129,6 +1191,180 @@ [nm (disj (into #{} (keep #(callee % own names)) (body-refs params body own)) nm)])))) +(defn- home + "Where a `calls` or `flow` form's fn lives: [its namespace, its simple + name]. A simple name is the target's." + [target f] + (if (namespace f) [(symbol (namespace f)) (symbol (name f))] [target f])) + +(defn- reach-path + "The shortest chain of calls from `f` to `g` in `graph`, through the + namespace's own fns, as [f ... g]; nil when `f` never reaches `g`." + [graph f g] + (loop [frontier [[f]], seen #{f}] + (when (seq frontier) + (let [nexts (for [path frontier, h (get graph (peek path)) :when (not (contains? seen h))] + (conj path h))] + (or (first (filter #(= g (peek %)) nexts)) + (recur (vec (filter #(contains? graph (peek %)) nexts)) + (into seen (map peek nexts)))))))) + +(defn- ns-context + "The names a namespace's source brings in, and its defns by name." + [forms] + (let [nsf (first (filter #(head? % "ns") forms)) + defns (keep #(when (ck/defn-form? %) (defn-parts %)) forms)] + {:names (assoc-in (ns-names nsf) [:aliases :self] (second nsf)) + :defns (into {} (map (juxt :name identity)) defns) + :own (set (map :name defns))})) + +(defn- dataflow + "Where each value in a fn comes from. `ast` is the fn, lowered and + uniquified. A source is [:param i], the fn's i-th parameter, or + [:call g], what a call to g returns. Returns {:calls [{:g g :args + [sources ...]}] :result sources}: each call the fn makes to a named fn, + with the sources of each argument, and the sources of its result. + A branch's test flows into its value. A lambda passed to a fn is given + that call's other arguments, and so is a fn passed by name." + [ast self own names] + (let [calls (atom #{}) + un (fn [xs] (reduce into #{} xs)) + named (fn [a] (when (= :ref (:op a)) (callee (:name a) own names)))] + (letfn [(src [a env sink] + (case (:op a) + :ref (or (get env (:name a)) + (when-let [g (named a)] (when (not= g self) #{[:call g]})) + #{}) + :lit #{} + :if (un [(src (:test a) env sink) (src (:then a) env sink) (src (:else a) env sink)]) + :do (src (:ret a) env sink) + :let (src (:body a) + (reduce (fn [e [b init]] + (let [v (src init e sink)] + (reduce #(assoc %1 %2 v) e (l/binding-names b)))) + env (:bindings a)) + sink) + :loop (frame (map (comp first) (:bindings a)) + (mapv #(src (second %) env sink) (:bindings a)) + (:body a) env) + :recur (do (swap! sink conj (mapv #(src % env sink) (:args a))) #{}) + :fn (lambda a env #{}) + :case (un (concat [(src (:scrut a) env sink)] + (map #(src (:body %) env sink) (:clauses a)) + (when (:default a) [(src (:default a) env sink)]))) + (:vec :set) (un (map #(src % env sink) (:items a))) + :map (un (map #(src % env sink) (concat (:keys a) (:vals a)))) + :invoke (invoke a env sink) + #{})) + ;; a loop, or the fn itself: its binders take their inits and + ;; whatever each recur passes, until nothing new arrives + (frame [names inits body env] + (loop [ins inits, n 0] + (let [sink (atom []) + v (src body (merge env (zipmap names ins)) sink) + ins2 (reduce (fn [acc args] (mapv into acc (concat args (repeat #{})))) + ins @sink)] + (if (or (= ins2 ins) (< 8 n)) v (recur ins2 (inc n)))))) + (lambda [a env given] + (let [sink (atom [])] + (src (:body a) (merge env (zipmap (:params a) (repeat given))) sink))) + (invoke [a env sink] + (let [fa (:fn a), args (:args a) + g (named fa) + plain (remove #(or (= :fn (:op %)) (named %)) args) + given (un (map #(src % env sink) plain)) + arg-src (fn [x] (cond (= :fn (:op x)) (lambda x env given) + :else (src x env sink)))] + (cond + (= :fn (:op fa)) + (let [s (atom [])] + (src (:body fa) (merge env (zipmap (:params fa) (map #(src % env sink) args))) s)) + + (= g self) + (do (swap! sink conj (mapv #(src % env sink) args)) + (un (map #(src % env sink) args))) + + :else + (let [srcs (mapv arg-src args)] + ;; a fn passed by name is called on the other arguments + (doseq [x args :let [h (named x)] :when (and h (not= h self))] + (swap! calls conj {:g h :args [given]})) + (when g (swap! calls conj {:g g :args srcs})) + (un (concat srcs [(src fa env sink)] + (when g [#{[:call g]}])))))))] + (let [ps (:params ast) + v (frame ps (mapv (fn [i] #{[:param i]}) (range (count ps))) (:body ast) {})] + {:calls (vec @calls) :result v})))) + +(defn- flow-facts* + [ctx f] + (when-let [{params :params body :body} (get (:defns ctx) f)] + (let [ast (binding [l/*locals* (:own ctx)] + (l/uniquify (l/lower (list* 'fn params body))))] + (assoc (dataflow ast f (:own ctx) (:names ctx)) :arity (count params))))) + +(defn flow-facts + "How data moves through fn `f` of namespace `ns-sym`, read from source: + {:calls [{:g g :args [sources ...]}] :result sources :arity n}. A + source is [:param i] or [:call g]. Nothing is checked." + [ns-sym f] + (flow-facts* (ns-context (book/read-forms (source-url ns-sym))) f)) + +(defn- check-flows + "Each `flow` form against the source of the namespace its fn is in." + [{:keys [target flows]} forms forms-of] + (vec (for [[qf ps chains] flows] + (let [[hns f] (home target qf) + ctx (ns-context (if (= hns target) forms (forms-of hns))) + target hns + facts (try (flow-facts* ctx f) + (catch Throwable ex {:unreadable (or (ex-message ex) (str ex))})) + pos (zipmap ps (range)) + tok #(if (contains? pos %) [:param (pos %)] [:call %]) + show #(if (= :result %) "result" (str %)) + unknown (distinct (for [c chains, l c + :when (and (symbol? l) (not (contains? pos l)) + (nil? (namespace l)) (not (contains? (:own ctx) l)))] + l)) + errors + (cond + (nil? facts) + [(str "the spec gives `" f "` a flow, but " target " defines no fn `" f "`")] + + (:unreadable facts) + [(str "writ cannot follow the data through `" f "`: " (:unreadable facts))] + + (or (seq unknown) (not= (count ps) (:arity facts))) + (concat + (for [l unknown] + (str "the flow of `" f "` names `" l "`, which is neither a parameter of `" f + "` nor a fn of " target)) + (when (not= (count ps) (:arity facts)) + [(str "the flow of `" f "` names " (count ps) " parameter(s), but `" f "` takes " + (:arity facts))])) + + :else + (distinct + (for [c chains, [a b] (partition 2 1 c) + :let [t (tok a) + from (if (contains? pos a) (str "`" a "`") (str "`" a "`"))] + err [(cond + (= :result b) + (when-not (contains? (:result facts) t) + (str "what `" f "` returns does not come from " from)) + + (not-any? #(= b (:g %)) (:calls facts)) + (str "`" f "` never calls `" b "`") + + (not-any? #(and (= b (:g %)) (some (fn [x] (contains? x t)) (:args %))) + (:calls facts)) + (str "`" b "` is never given anything that comes from " from))] + :when err] + err)))] + (cond-> {:fn qf :chains (mapv #(str/join " -> " (map show %)) chains) + :status (if (seq errors) :failed :ok)} + (seq errors) (assoc :errors (vec errors))))))) + (defn call-graph "The call graph of a namespace, read from its source without loading it: {f #{g ...}} for each of its defns. A callee is one of its own fns @@ -1139,29 +1375,39 @@ (graph-of (book/read-forms (source-url ns-sym)))) (defn- check-calls - "Each `calls` form against the target's call graph." - [{:keys [target calls]} forms] - (let [graph (graph-of forms)] - (vec (for [[f gs] (sort-by (comp str first) calls)] - (let [actual (get graph f) - unknown (first (filter #(and (nil? (namespace %)) (not (contains? graph %))) gs))] - (cond - (nil? actual) - {:fn f :calls gs :status :failed - :error (str "the spec gives `" f "` a call set, but " target " defines no fn `" f "`")} - - unknown - {:fn f :calls gs :status :failed - :error (str "the spec says `" f "` calls `" unknown "`, but " target - " defines no fn `" unknown "`")} - - :else - (let [declared (set gs) - missing (vec (sort-by str (remove actual declared))) - extra (vec (sort-by str (remove declared actual)))] - (if (and (empty? missing) (empty? extra)) - {:fn f :calls gs :status :ok} - {:fn f :calls gs :status :failed :missing missing :extra extra})))))))) + "Each `calls` form against the call graph of the namespace its fn is in: + the target's, read from `forms`, or another's, read by `forms-of`." + [{:keys [target calls]} forms forms-of] + (vec (for [[qf gs] (sort-by (comp str first) calls)] + (let [[hns f] (home target qf) + graph (graph-of (if (= hns target) forms (forms-of hns))) + actual (get graph f) + names (if (map? gs) (apply concat (vals gs)) gs) + unknown (first (filter #(and (nil? (namespace %)) (not (contains? graph %))) names))] + (cond + (nil? actual) + {:fn qf :calls gs :status :failed + :error (str "the spec gives `" qf "` a call set, but " hns " defines no fn `" f "`")} + + unknown + {:fn qf :calls gs :status :failed + :error (str "the spec says `" qf "` calls `" unknown "`, but " hns + " defines no fn `" unknown "`")} + + (map? gs) + (let [missing (vec (remove #(reach-path graph f %) (:through gs))) + reached (vec (keep #(reach-path graph f %) (:not gs)))] + (if (and (empty? missing) (empty? reached)) + {:fn qf :calls gs :status :ok} + {:fn qf :calls gs :status :failed :unreached missing :reached reached})) + + :else + (let [declared (set gs) + missing (vec (sort-by str (remove actual declared))) + extra (vec (sort-by str (remove declared actual)))] + (if (and (empty? missing) (empty? extra)) + {:fn qf :calls gs :status :ok} + {:fn qf :calls gs :status :failed :missing missing :extra extra}))))))) ;; --- machines ---------------------------------------------------------------------- @@ -1281,61 +1527,138 @@ ;; --- graphs ----------------------------------------------------------------------- (defn- graph-edges - "Each edge of a graph as {:from :f :args :tos}, its targets in the order - the graph lists its states." + "Each edge of a graph as {:from :f :args :pos :key :tos}: the types of the + arguments beside the state, the state's position among the fn's + parameters (where `_` marks it, else first), the edge's key as written, + and its targets in the order the graph lists its states." [[_ m]] - (for [[from es] (:edges m), [[f & args] tos] es] - {:from from :f f :args (vec args) + (for [[from es] (:edges m), [[f & args :as k] tos] es] + {:from from :f f :args (vec (remove #{'_} args)) :key k + :pos (or (first (keep-indexed #(when (= '_ %2) %1) args)) 0) :tos (filterv (set tos) (keys (:states m)))})) +(defn- insert-at [v i x] (vec (concat (take i v) [x] (drop i v)))) + +(defn- subst-var + "`form` with free occurrences of symbol `x` replaced by `e`. A binder + of `x` in a let, fn, loop or quantifier stops it." + [form x e] + (letfn [(binds? [bs] (some #{x} (mapcat l/binding-names (take-nth 2 bs)))) + (walk [f] + (cond + (= x f) e + (and (seq? f) (= 'quote (first f))) f + (and (seq? f) (contains? '#{let let* loop loop* forall exists} (first f)) + (vector? (second f)) (binds? (second f))) + f + (and (seq? f) (contains? '#{fn fn*} (first f)) + (some #(and (vector? %) (some #{x} (mapcat l/binding-names %))) (take 3 f))) + f + (seq? f) (apply list (map walk f)) + (vector? f) (mapv walk f) + (map? f) (into {} (map (fn [[k v]] [(walk k) (walk v)])) f) + (set? f) (into #{} (map walk) f) + :else f))] + (walk form))) + (defn- arg-var [t i taken] (let [base (if (symbol? t) (str/lower-case (name t)) (str "arg" i)) v (symbol base)] (if (contains? taken v) (symbol (str base i)) v))) (defn- graph-obligations - "A law per edge whose targets are refinements: every value of its state - goes, by the edge's fn, to a value of one of its targets. An edge into - plain types needs no law; the signatures and the static check keep it." + "Laws for each edge whose targets are refinements. One says every value + of its state goes, by the edge's fn, to a value of one of its targets. + One per target says the step is taken: some value of the state, and + some arguments, land there. Without those the graph only bounds the + code, and code that never leaves its state keeps every bound. An edge + into plain types needs no law; the signatures and the static check keep + it." [[gname m :as g] refs] - (vec (for [{:keys [from f args tos]} (graph-edges g) + (vec (for [{:keys [from f args tos pos]} (graph-edges g) :let [ty #(get (:states m) %) 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))))) - [] (map-indexed vector args)) - nxt (if (= 'next v) 'next-state 'next)] - {:name (symbol (str gname ":" (name from) ":" f)) - :prop (list 'forall (vec (concat [v (ty from)] (interleave avs args))) - (list 'let [nxt (apply list f v avs)] - (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 - :total true})))) + :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))))) + [] (map-indexed vector args)) + binders (vec (concat [v (ty from)] (interleave avs args))) + call (apply list f (insert-at avs pos v)) + ;; each target's predicate, of the call itself: the law + ;; reads as the spec would write it, (ascending? (isort xs)), + ;; the shape the prover takes apart + in (fn [t] (let [r (ref-of t)] (subst-var (:pred r) (:var r) call))) + lands (fn [ts] (if (next ts) (cons 'or (map in ts)) (in (first ts))))] + law (cons {:name (symbol (str gname ":" (name from) ":" f)) + :prop (list 'forall binders (lands tos)) + :explain (str "a " f " from " (name from) " must land in " + (str/join " or " (map name tos))) + :graph gname + :total true} + (for [t tos] + {:name (symbol (str gname ":" (name from) ":" f "->" (name t))) + :prop (list 'exists binders (lands [t])) + :explain (str "the graph says a " f " can take " (name from) " to " + (name t) ", but no generated " (name from) " does") + :step-of gname}))] + law))) (defn- fits? "Does a value of type `a` fit where type `b` is expected?" [a b] (or (= a b) (and (= 'Nat a) (= 'Int b)) (= 'Any b))) +(defn- same-type-errors + "States of one plain type: a value of one is a value of the other, so an + edge between them checks the type and nothing else, and the names say + more than the graph does." + [[gname m] refs] + (let [refined? #(let [t (plain %)] (and (symbol? t) (contains? refs t)))] + (for [[t ss] (group-by val (:states m)) + :when (and (next ss) (not (refined? t))) + :let [ss (map key ss)]] + (str "graph `" gname "`: " (str/join " and " (map pr-str ss)) " are both " (pr-str t) + ", so nothing tells them apart and a step between them checks only the type;" + " make each a refinement that says what sets it apart")))) + (defn- graph-flow-errors "Each edge's fn must take its state's type, and return its targets'." [[gname m :as g] anns refs] (let [base #(plain (erase % refs)) ty #(get (:states m) %)] - (vec (for [{:keys [from f args tos]} (graph-edges g) - :let [sig (get anns f) - edge (str "the edge " (pr-str from) " -" (pr-str (into [f] args)) "->") - ps (mapv base (:params sig))] + (vec (concat (same-type-errors g refs) + (for [{:keys [from f args tos pos key]} (graph-edges g) + :let [proj (get projections f) + tup (let [t (base (ty from))] (when (and (seq? t) (= 'Tuple (first t))) (vec (rest t)))) + sig (if proj + (when tup {:params [(base (ty from))] :ret (get tup (proj (count tup)))}) + (get anns f)) + edge (str "the edge " (pr-str from) " -" (pr-str key) "->") + ps (let [ps (mapv base (:params sig))] + (if (< pos (count ps)) + (into [(nth ps pos)] (concat (take pos ps) (drop (inc pos) ps))) + ps))] err (cond + (and proj (nil? tup)) + [(str edge " takes `" f "` of " (pr-str from) ", which is a " (pr-str (ty from)) + ", not a Tuple")] + proj + (for [t tos :when (not (fits? (base (:ret sig)) (base (ty t))))] + (str edge " " (pr-str t) " expects a " (pr-str (base (ty t))) ", but `" f "` of " + (pr-str from) " gives a " (pr-str (base (:ret sig))))) (nil? sig) [(str edge " uses `" f "`, which has no ann")] (not= (count ps) (inc (count args))) [(str edge " calls `" f "` with " (inc (count args)) " argument(s), but its ann takes " (count ps))] :else (concat + (let [refined? #(let [t (plain (ty %))] (and (symbol? t) (contains? refs t)))] + (when (some refined? tos) + (for [t tos :when (not (refined? t))] + (str edge " lands in " (pr-str t) ", a plain " (pr-str (ty t)) + ", beside refined states, so every result is in it and the edge" + " says nothing about where `" f "` goes; make " (pr-str t) + " a refinement")))) (when-not (fits? (base (ty from)) (first ps)) [(str edge " passes `" f "` a " (pr-str (base (ty from))) ", but its ann takes " (pr-str (first ps)))]) @@ -1344,14 +1667,14 @@ (for [t tos :when (not (fits? (base (:ret sig)) (base (ty t))))] (str edge " " (pr-str t) " expects a " (pr-str (base (ty t))) ", but `" f "` returns " (pr-str (base (:ret sig))) " by its ann"))))] - (str "graph `" gname "`: " err))))) + (str "graph `" gname "`: " err)))))) (defn- graph-rule-errors "The graph's own rules, over its edges: reachability from :start, a :final state from every state reached, :never and :before." [[_ m :as g]] - (let [edges (vec (for [{:keys [from f args tos]} (graph-edges g), t tos] - [from (into [f] args) t])) + (let [edges (vec (for [{:keys [from key tos]} (graph-edges g), t tos] + [from key t])) st (:start m) start (if (vector? st) (first st) st) from-start (when start (reachable edges start))] @@ -1400,6 +1723,18 @@ (str "\n " (state-id s) " --> " (state-id t) " : " (state-id ev)))) (apply str (for [s final] (str "\n " (state-id s) " --> [*]"))))) +(defn- graph-diagram [[_ m :as g]] + (let [st (:start m) + start (if (vector? st) (first st) st)] + (str "stateDiagram-v2" + (apply str (for [[s t] (:states m)] + (str "\n " (state-id s) " : " (name s) ", a " (pr-str t)))) + (when start (str "\n [*] --> " (state-id start))) + (apply str (for [{:keys [from key tos]} (graph-edges g), t tos] + (str "\n " (state-id from) " --> " (state-id t) " : " + (str/join " " (map str key))))) + (apply str (for [s (:final m)] (str "\n " (state-id s) " --> [*]")))))) + (defn- mermaid-id [s] (let [id (-> (str s) (str/replace "?" "_Q") (str/replace "!" "_B") (str/replace #"[^A-Za-z0-9_]" "_"))] @@ -1410,14 +1745,23 @@ graph. Given a spec namespace, its target's (or opts :target's), with the spec's `calls` laid over it: a call the spec does not list is a dotted edge marked `not in spec`, and a call it lists that the code does - not make is an edge marked `missing`." + not make is an edge marked `missing`. opts :graph or :machine draws + that graph or machine of the spec as a mermaid stateDiagram-v2." ([ns-sym] (mermaid ns-sym {})) ([ns-sym opts] (require ns-sym) - (if-let [m (:machine opts)] - (let [[_ spec-m] (or (first (filter #(= m (first %)) (:machines (get @registry ns-sym)))) + (cond + (:graph opts) + (graph-diagram (or (first (filter #(= (:graph opts) (first %)) (:graphs (get @registry ns-sym)))) + (fail! "`" ns-sym "` has no graph `" (:graph opts) "`"))) + + (:machine opts) + (let [m (:machine opts) + [_ spec-m] (or (first (filter #(= m (first %)) (:machines (get @registry ns-sym)))) (fail! "`" ns-sym "` has no machine `" m "`"))] (state-diagram spec-m)) + + :else (let [e (get @registry ns-sym) target (if e (or (:target opts) (:target e)) ns-sym) graph (call-graph target) @@ -1454,6 +1798,81 @@ (map? t) (into {} (map (fn [[k v]] [k (erase v refines)])) t) :else t)) +(defn- sig-str [{:keys [params ret]}] + (str "[" (str/join " " (map pr-str params)) (when (seq params) " ") "-> " (pr-str ret) "]")) + +(defn- calls-str [gs] + (cond + (map? gs) (str (when (seq (:through gs)) (str "\n goes through: " (str/join ", " (:through gs)))) + (when (seq (:not gs)) (str "\n never reaches: " (str/join ", " (:not gs))))) + (seq gs) (str "\n calls exactly: " (str/join ", " gs)) + :else "\n calls nothing outside clojure.core")) + +(defn plan + "The spec as a plan a person can read and confirm, from the spec alone: + each graph's states and steps, each signed fn with the laws that name + it, its flows and its call set, and each machine. Nothing is checked, + and the target need not exist yet." + [spec-ns] + (require spec-ns) + (let [e (or (get @registry spec-ns) (fail! "`" spec-ns "` is not a spec namespace")) + refs (refines-of e) + show-type (fn [t] (if-let [r (get refs (plain t))] + (str (pr-str t) ", a " (pr-str (:base r)) " where " (pr-str (:pred r))) + (pr-str t))) + names-in (fn [p] (set (filter symbol? (tree-seq coll? seq p)))) + laws-of (fn [f] (for [{:keys [name prop]} (:laws e) :when (contains? (names-in prop) f)] name)) + flows (group-by first (:flows e)) + calls (into {} (:calls e))] + (str "plan: " spec-ns " for " (:target e) + (when (= :proved (:require e)) " (every law must be proved)") + (apply str + (for [[gname m :as g] (:graphs e) + :let [w (+ 2 (apply max 0 (map (comp count str) (keys (:states m)))))]] + (str "\n\ngraph `" gname "`" + (when-let [st (:start m)] (str "\n start: " (pr-str st))) + "\n states" + (apply str (for [[s t] (:states m)] + (str "\n " (format (str "%-" w "s") (str s)) (show-type t)))) + "\n steps" + (apply str (for [{:keys [from key tos]} (graph-edges g)] + (str "\n " from " -" key "-> " + (str/join " or " (map str tos))))) + (apply str (for [[k label] [[:never "never"] [:before "only through"]] + [a b] (get m k)] + (if (= k :never) + (str "\n " a " never leads to " b) + (str "\n " b " is reached only through " a)))) + (when (seq (:final m)) + (str "\n final: " (str/join ", " (map str (:final m)))))))) + (when (seq (:anns e)) + (str "\n\nfns" + (apply str + (for [[f sig] (sort-by (comp str key) (:anns e)) + :let [ls (laws-of f)]] + (str "\n " f " " (sig-str sig) + (if (seq ls) + (str "\n laws: " (str/join ", " ls)) + "\n laws: none") + (apply str (for [[_ ps chains] (get flows f), c chains] + (str "\n flow: " + (str/join " -> " (map #(if (= :result %) "result" (str %)) c))))) + (when-let [gs (get calls f)] (calls-str gs))))))) + (let [outside (sort-by str (remove (set (keys (:anns e))) + (distinct (concat (keys calls) (keys flows)))))] + (when (seq outside) + (str "\n\nwiring outside the signed fns" + (apply str (for [f outside] + (str "\n " f + (apply str (for [[_ ps chains] (get flows f), c chains] + (str "\n flow: " + (str/join " -> " (map #(if (= :result %) "result" (str %)) c))))) + (when-let [gs (get calls f)] (calls-str gs)))))))) + (apply str (for [[mname m] (:machines e)] + (str "\n\nmachine `" mname "`: " (:step m) " steps it from " (pr-str (:start m)) + (apply str (for [[st evs] (:transitions m), [ev to] evs] + (str "\n " (pr-str st) " -" (pr-str ev) "-> " (pr-str to)))))))))) + (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." @@ -1703,7 +2122,9 @@ (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 graph-missing lemmas]}] + [{:keys [ok target spec static laws gaps unspecified rejected calls flows machines proof graphs graph-missing + lemmas off-graph] + ambiguous ::ambiguous}] (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" @@ -1726,23 +2147,40 @@ (when ok (apply str (for [{f :fn gs :calls} calls] (str "\n `" f "` " - (if (seq gs) - (str "calls exactly " (str/join ", " gs)) - "calls nothing outside clojure.core"))))) + (cond + (map? gs) (str/join "; " (concat + (when (seq (:through gs)) + [(str "goes through " (str/join ", " (:through gs)))]) + (when (seq (:not gs)) + [(str "never reaches " (str/join ", " (:not gs)))]))) + (seq gs) (str "calls exactly " (str/join ", " gs)) + :else "calls nothing outside clojure.core"))))) + (when ok + (apply str (for [{f :fn cs :chains} flows, c cs] + (str "\n flow of `" f "`: " c)))) (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 m ::obligations} graphs :when (= :ok st) - :let [m (or m 0) u (or u 0) + (apply str (for [{g :graph n :edges st :status u ::unproved m ::obligations k ::steps} graphs + :when (= :ok st) + :let [m (or m 0) u (or u 0) k (or k 0) edges (fn [k] (str k (if (= 1 k) " edge" " edges"))) flow (- n m)]] (str "\n graph `" g "`: " (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 (pos? k) + (str ", each of " (if (= 1 m) "its " "their ") k (if (= 1 k) " step" " steps") + " taken")) (when (and (pos? m) (pos? flow)) (str ", " flow " more checked against the signatures"))))) (when-not (:ok static) (str "\n\n" (:error static))) + (apply str (for [{n :name :keys [where whose]} ambiguous] + (str "\n\n`" n "` is defined by " where " and by " target + ", so a law cannot tell which one it means." + "\n A law judges the code with the spec's own helpers, never the code's:" + "\n rename " whose " `" n "`."))) (when graph-missing (str "\n\n`" spec "` declares no state graph. A spec starts from the problem's states" " and the steps between them:" @@ -1763,10 +2201,22 @@ (when (seq errors) (str "\n\nmachine `" m "`: the table breaks its own constraints" (apply str (map #(str "\n " %) errors))))))) - (apply str (for [{f :fn gs :calls :keys [error missing extra]} calls - :when (or error (seq missing) (seq extra))] - (if error + (apply str (for [{f :fn gs :calls :keys [error missing extra unreached reached]} calls + :when (or error (seq missing) (seq extra) (seq unreached) (seq reached))] + (cond + error (str "\n\n" error) + + (map? gs) + (str "\n\nthe call graph of `" f "` is not the one the spec gives" + (apply str (for [g unreached] + (str "\n `" f "` does not reach `" g "`, which the spec says it goes through"))) + (apply str (for [p reached] + (str "\n `" f "` reaches `" (peek p) "`, which the spec says it never does: " + (str/join " -> " (cons f (rest p)))))) + "\n Call through the layers the spec names instead of around them.") + + :else (str "\n\nthe call graph of `" f "` is not the one the spec gives" (apply str (for [g missing] (str "\n `" f "` does not call `" g @@ -1777,6 +2227,11 @@ "\n the spec says `" f "` calls " (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 (for [{f :fn :keys [errors]} flows :when (seq errors)] + (str "\n\nthe flow of `" f "` is not the one the spec gives" + (apply str (map #(str "\n " %) errors)) + "\n Pass each step what the step before it returns; the spec names the path" + " the data takes."))) (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 `") @@ -1804,8 +2259,12 @@ (apply str (map #(str "\n or when it " %) more))) "\n State what `" f "` must do, so that a law rejects this.")) gaps)) - (when (seq unspecified) - (str "\n\nnot in the spec (no signature): " (str/join ", " unspecified))))) + (when (and ok (seq off-graph)) + (str "\n not a step of any graph or machine: " (str/join ", " off-graph))) + (apply str (for [f unspecified] + (str "\n\n`" f "` is public, but the spec gives it no signature, so nothing" + " checks it.\n Sign it with `ann` if the plan has it; if it is a helper," + " make it private with defn-."))))) (def ^:private writ-sources "The sources a proof depends on, beside the code and the spec: writ's @@ -1881,6 +2340,19 @@ (defn- thrown? [r] (or (:error r) (some (fn [[_ v]] (str/starts-with? (str v) "threw:")) (:detail r)))) +(defn- alpha= + "Do two laws say the same, up to the names of their leading `forall` + binders?" + [p q] + (let [canon (fn [p] + (loop [p p, bs [], i 0] + (if (head? p "forall") + (let [[_ [x t] body] p + y (symbol (str "_" i))] + (recur (subst-var body x y) (conj bs t) (inc i))) + [bs p])))] + (= (canon p) (canon q)))) + (defn- prove-laws "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 @@ -1907,11 +2379,6 @@ ;; 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")) @@ -1926,7 +2393,7 @@ ;; 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)) @@ -1941,6 +2408,19 @@ (plain (:ret sig))]))})) (catch Throwable e {:proved false :reason (str "the prover failed: " (ex-message e))}))) + ;; that a step never throws is proved only by running it + ;; symbolically, which a recursive fn defeats; its landing is + ;; then proved by any strategy, and the report says the rest + ;; was tested + attempt* (fn [r lemmas] + (let [pr (attempt** r lemmas)] + (if (or (:proved pr) (not (:total r))) + pr + (let [pr2 (attempt** (dissoc r :total) lemmas)] + (if (:proved pr2) + (update pr2 :summary str + ", and it threw on no test (that it never throws is not proved)") + pr))))) 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)) @@ -1958,7 +2438,18 @@ (fn [[out lemmas] r] (if-not (open? r) [(conj out r) lemmas] - (let [pr (attempt r lemmas)] + ;; a proved law that says the same is no proof of this one + ;; from the code, so it is left out of the search; when + ;; the search fails, that law is the proof + (let [same? #(alpha= (:prop %) (:prop r)) + same (first (filter same? lemmas)) + pr (attempt r (vec (remove same? lemmas))) + pr (if (or (:proved pr) (not same)) + pr + {:proved true + :summary (str "as law `" (:name same) "`, which says the same" + (when (:total r) + ", and it threw on no test (that it never throws is not proved)"))})] (cond (and (:proved pr) (= :tested (:status r))) [(conj out (cond-> (-> r (dissoc :unproved) @@ -2014,6 +2505,27 @@ :tested (count (filter #(= :test (:evidence %)) results)) :laws (count results)}) +(defn- step-fns + "The fns a spec's graphs and machines name as steps." + [e] + (-> (set (map :step (map second (:machines e)))) + (into (mapcat #(map :f (graph-edges %)) (:graphs e))) + (into (for [[f _ chains] (:flows e), x (cons f (apply concat chains)) :when (symbol? x)] x)))) + +(defn- ambiguous-names + "Names a law could read two ways: a public of the target that the spec, + or its proof namespace, also defines. A law's free name resolves to + the target first, so the spec's helper would silently be replaced by + the code it is meant to judge." + [e spec-ns] + (let [target (:target e) + publics (set (keys (ns-publics (the-ns target)))) + by (fn [where whose nss] + (for [n (sort (filter publics nss))] {:name n :where where :whose whose}))] + (vec (concat (by "the spec" "the spec's" (keys (ns-interns (the-ns spec-ns)))) + (when-let [p (:ns (::proof e))] + (by (str "the proof namespace " p) "the proof namespace's" (keys (proof-own p)))))))) + (defn check "Check a spec namespace against its target (or opts :target). Returns a report map; :ok says whether everything held and :message explains any @@ -2033,13 +2545,15 @@ ;; 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) - :unspecified (vec (sort (for [[nm private?] (:defns static) - :when (and (not private?) (not (contains? anns nm)))] - nm)))}] - (if-not (:ok static) - (let [r (assoc base :ok false :laws [] :gaps [] :calls [] :machines [] :graphs [])] + ambiguous (when (:ok static) (ambiguous-names e spec-ns)) + base (cond-> {:spec spec-ns :target target + :static (if (:ok static) {:ok true} static) + :unspecified (vec (sort (for [[nm private?] (:defns static) + :when (and (not private?) (not (contains? anns nm)))] + nm)))} + (seq ambiguous) (assoc :ambiguous (mapv :name ambiguous) ::ambiguous ambiguous))] + (if (or (not (:ok static)) (seq ambiguous)) + (let [r (assoc base :ok false :laws [] :gaps [] :calls [] :flows [] :machines [] :graphs [])] (assoc r :message (format-report r))) (let [refs (refines-of e) tenv (type-env-of e spec-ns) @@ -2058,7 +2572,7 @@ ;; caller's own instrument stays in place wrapped (wrap! e) results (try - (vec (for [{:keys [name prop explain graph total lemma]} laws + (vec (for [{:keys [name prop explain graph total lemma step-of]} laws :let [p (desugar prop)]] (try (lw/check-prop-shape! p) @@ -2082,6 +2596,7 @@ :prop qp) explain (assoc :explain explain) graph (assoc :graph graph) + step-of (assoc :step-of step-of) total (assoc :total true) lemma (assoc :lemma true)))) ;; a law that cannot be run (a malformed @@ -2114,7 +2629,9 @@ per-fn (if (and sound? (not= false (:adequacy opts))) (adequacy ctx target (sort (filter #(contains? publics %) (keys anns))) - anns (concat (keep :prop (remove :lemma results)) + ;; a step's witness is found by search, so a stand-in + ;; that misses it may only be unlucky: it pins nothing + anns (concat (keep :prop (remove #(or (:lemma %) (:step-of %)) results)) (for [m (:machines e)] (qualify (machine-prop m e) #{} publics interns target spec-ns))) @@ -2125,7 +2642,10 @@ 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))) + target-forms (book/read-forms (source-url target)) + forms-of (memoize #(book/read-forms (source-url %))) + call-results (check-calls e target-forms forms-of) + flow-results (check-flows e target-forms forms-of) machine-results (mapv #(check-machine % e target) (:machines e)) graph-results (mapv (fn [g] (let [errs (vec (concat (graph-flow-errors g anns refs) @@ -2138,22 +2658,28 @@ :edges (count (graph-edges g)) :status (if (and (empty? errs) (empty? rules)) :ok :failed) ::obligations (count obls) + ::steps (count (filter #(and (= (first g) (:step-of %)) + (= :witnessed (:status %))) + results)) ::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 + r (assoc base :laws results :gaps gaps :calls call-results :flows flow-results :lemmas lemma-results :graph-missing graphless - :graphs (mapv #(dissoc % ::unproved ::obligations) graph-results) + :graphs (mapv #(dissoc % ::unproved ::obligations ::steps) 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) + :off-graph (vec (sort-by str (remove (step-fns e) + (filter #(contains? publics %) (keys anns))))) + :ok (and sound? (empty? gaps) (empty? (:unspecified base)) (not-any? #(= :unproved (:status %)) results) (every? #(= :proved (:status %)) lemma-results) (every? #(= :ok (:status %)) call-results) + (every? #(= :ok (:status %)) flow-results) (every? #(= :ok (:status %)) machine-results) (every? #(= :ok (:status %)) graph-results) (not graphless)))] diff --git a/test/writ/evidence_test.clj b/test/writ/evidence_test.clj index 140b0ed..d067143 100644 --- a/test/writ/evidence_test.clj +++ b/test/writ/evidence_test.clj @@ -24,8 +24,9 @@ (testing "a law that only ran on generated inputs is tested" (is (= :test (:evidence (law-result r 'smallest-first))))) (testing "the report counts them" - (is (= {:require :tested :proved 6 :tested 1 :laws 7} (:proof r))) - (is (str/includes? (:message r) "6 of 7 laws proved")) + ;; seven laws, the graph's two edges and a witness for each step + (is (= {:require :tested :proved 10 :tested 1 :laws 11} (:proof r))) + (is (str/includes? (:message r) "10 of 11 laws proved")) (is (str/includes? (:message r) "tested, not proved: smallest-first"))))) (deftest a-check-can-demand-proof @@ -55,7 +56,7 @@ (is (= :unproved (:status (law-result r 'smallest-first)))) (is (str/includes? (:message r) "law `smallest-first` is tested, not proved, and the law requires proof")) (testing "the other laws keep the spec's level: tested is enough for them" - (is (= :tested (:status (law-result r 'sorted)))) + (is (not= :unproved (:status (law-result r 'sorted)))) (is (= :proved (:status (law-result r 'permutation))))))) (deftest proof-options-are-checked-when-the-spec-loads diff --git a/test/writ/flow_test.clj b/test/writ/flow_test.clj new file mode 100644 index 0000000..37abdd3 --- /dev/null +++ b/test/writ/flow_test.clj @@ -0,0 +1,94 @@ +(ns writ.flow-test + "`flow`: how data moves through a fn. Each chain says a value reaches a + step: a parameter, or what a step returns, is passed (maybe through + other calls) to the next step, and the last may be the fn's result. + The check reads the fn's source, so code that calls every layer the + spec names but wires them wrong is caught." + (:require [clojure.test :refer [deftest is testing]] + [clojure.string :as str] + [writ.spec :as spec])) + +(defn- expansion-error [form] + (try (macroexpand-1 form) nil + (catch Throwable e (ex-message e)))) + +(defn- flow-of [r f] (first (filter #(= f (:fn %)) (:flows r)))) + +(deftest a-fn-wired-as-planned-passes + (let [r (spec/check 'writ.spec-demo.pipeline-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (= :ok (:status (flow-of r 'handle)))) + (is (str/includes? (:message r) "flow of `handle`: s -> normalize -> respond -> result")))) + +(deftest a-step-given-the-wrong-value-fails + (let [r (spec/check 'writ.spec-demo.pipeline-spec + {:seed 42 :target 'writ.spec-demo.pipeline-swapped}) + fl (flow-of r 'handle)] + (is (not (:ok r))) + (is (= :ok (:status (first (filter #(= 'handle (:fn %)) (:calls r))))) + "the call set is right...") + (is (= :failed (:status fl)) "...but the data goes the wrong way") + (is (str/includes? (:message r) "the flow of `handle` is not the one the spec gives")) + (is (str/includes? (:message r) "`respond` is never given anything that comes from `normalize`")) + (is (= ["`respond` is never given anything that comes from `normalize`" + "what `handle` returns does not come from `normalize`"] + (:errors fl)) + "respond's answer is still handle's; only the links that break are named"))) + +(deftest a-step-the-fn-never-calls-fails + (let [r (spec/check 'writ.spec-demo.pipeline-spec + {:seed 42 :target 'writ.spec-demo.pipeline-bypass})] + (is (not (:ok r))) + (is (str/includes? (:message r) "`handle` never calls `respond`")))) + +(deftest data-is-followed-through-lambdas-fns-by-name-and-loops + (let [fl (spec/flow-facts 'writ.spec-demo.pipeline-many 'handle-all)] + (is (some #(and (= 'normalize (:g %)) (some (fn [a] (contains? a [:param 0])) (:args %))) + (:calls fl)) + "a lambda passed to map is given the collection's values") + (is (some #(and (= 'respond (:g %)) (some (fn [a] (contains? a [:call 'normalize])) (:args %))) + (:calls fl)) + "a fn passed by name is given the other arguments") + (is (contains? (:result fl) [:call 'respond]))) + (let [fl (spec/flow-facts 'writ.spec-demo.pipeline-many 'count-ok)] + (is (contains? (:result fl) [:call 'respond]) "a loop's result carries what its recur passed") + (is (some #(and (= 'respond (:g %)) (some (fn [a] (contains? a [:param 0])) (:args %))) + (:calls fl))))) + +(deftest a-flow-form-is-checked-when-it-is-read + (is (str/includes? (expansion-error '(writ.spec/flow handle [s] [s])) + "a chain needs at least two links")) + (is (str/includes? (expansion-error '(writ.spec/flow handle [s] [:result s])) + "`:result` can only end a chain")) + (is (str/includes? (expansion-error '(writ.spec/flow handle s [s normalize])) + "(flow f [param ...] [link link ...] ...)"))) + +(deftest a-flow-names-only-params-and-fns + (let [r (spec/check 'writ.spec-demo.flow-unknown-spec {:seed 42})] + (is (not (:ok r))) + (is (str/includes? (:message r) + "flow of `handle` names `sanitize`, which is neither a parameter of `handle` nor a fn of writ.spec-demo.pipeline")) + (is (str/includes? (:message r) + "flow of `handle` names 2 parameter(s), but `handle` takes 1")))) + +(deftest calls-can-state-reach-instead-of-an-exact-set + (let [r (spec/check 'writ.spec-demo.pipeline-layers-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (str/includes? (:message r) "`handle` goes through normalize, respond, valid?; never reaches clojure.string/upper-case"))) + (let [r (spec/check 'writ.spec-demo.pipeline-layers-spec + {:seed 42 :target 'writ.spec-demo.pipeline-inline})] + (is (str/includes? (:message r) "`handle` does not reach `normalize`")) + (is (not (str/includes? (:message r) "does not reach `respond`")))) + (let [r (spec/check 'writ.spec-demo.pipeline-layers-spec + {:seed 42 :target 'writ.spec-demo.pipeline-upper})] + (is (not (:ok r))) + (is (str/includes? (:message r) + "`handle` reaches `clojure.string/upper-case`, which the spec says it never does: handle -> normalize -> clojure.string/upper-case")))) + +(deftest a-shell-is-held-to-its-wiring + (let [r (spec/check 'writ.spec-demo.shell-spec {:seed 42})] + (is (not (:ok r))) + (is (= :ok (:status (first (filter #(= 'writ.spec-demo.shell/serve (:fn %)) (:calls r)))))) + (is (= :ok (:status (flow-of r 'writ.spec-demo.shell/serve)))) + (is (str/includes? (:message r) + "`writ.spec-demo.shell/serve-raw` does not reach `writ.spec-demo.pipeline/handle`")))) diff --git a/test/writ/graph_test.clj b/test/writ/graph_test.clj index 1ab715c..6890f26 100644 --- a/test/writ/graph_test.clj +++ b/test/writ/graph_test.clj @@ -48,7 +48,25 @@ (testing "a law over a refined type" (is (= :proved (:status (law-result r 'a-light-counts-up-while-it-shows))))) (is (= [{:graph 'signal :status :ok :states 3 :edges 3}] (:graphs r))) - (is (str/includes? (:message r) "graph `signal`: 3 edges proved")))) + (is (str/includes? (:message r) "graph `signal`: 3 edges proved, each of their 6 steps taken")))) + +(deftest every-step-of-the-graph-is-taken + (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42})] + (doseq [nm '[signal:green:tick->green signal:green:tick->yellow + signal:yellow:tick->yellow signal:yellow:tick->red + signal:red:tick->red signal:red:tick->green]] + (is (= :witnessed (:status (law-result r nm))) (str nm ": " (pr-str (law-result r nm))))) + (testing "the witness is the state, and any args, that takes the step" + (is (= '{l [:Green 30]} (:witness (law-result r 'signal:green:tick->yellow))))))) + +(deftest a-step-the-code-never-takes-fails + (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42 :target 'writ.spec-demo.signal-stuck})] + (is (not (:ok r))) + (is (= :proved (:status (law-result r 'signal:green:tick))) "the light stays in its states...") + (is (= :failed (:status (law-result r 'signal:green:tick->yellow))) "...but never turns yellow") + (is (str/includes? (:message r) "law `signal:green:tick->yellow` fails")) + (is (str/includes? (:message r) + "the graph says a tick can take green to yellow, but no generated green does")))) (deftest code-that-leaves-the-graph-fails-its-edge (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42 :target 'writ.spec-demo.signal-skip}) @@ -89,11 +107,19 @@ (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) +(deftest a-refined-state-makes-its-edge-a-law (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))))) + (is (= [{:graph 'sorting :status :ok :states 2 :edges 1}] (:graphs r))) + (is (= :witnessed (:status (law-result r 'sorting:unsorted:isort->sorted)))) + (is (contains? #{:proved :tested} (:status (law-result r 'sorting:unsorted:isort)))))) + +(deftest states-of-one-plain-type-cannot-be-told-apart + (let [r (spec/check 'writ.spec-demo.flow-plain-spec {:seed 42})] + (is (not (:ok r))) + (is (str/includes? (:message r) + "graph `sorting`: :unsorted and :sorted are both (List Nat), so nothing tells them apart")) + (is (str/includes? (:message r) "make each a refinement that says what sets it apart")))) (deftest a-graph-step-is-proved-never-to-throw (let [r (spec/check 'writ.spec-demo.signal-spec {:seed 42}) @@ -112,3 +138,58 @@ (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))))) + +(deftest an-edge-into-a-plain-state-beside-refined-ones-fails + (let [r (spec/check 'writ.spec-demo.signal-mixed-spec {:seed 42})] + (is (not (:ok r))) + (is (some? (law-result r 'signal:green:tick)) "an edge into refinements only is still a law") + (is (str/includes? (:message r) + "graph `signal`: the edge :yellow -[tick]-> lands in :red, a plain (Tuple Keyword Nat)")) + (is (str/includes? (:message r) "make :red a refinement")))) + +(deftest an-edge-can-take-its-state-at-any-parameter + (let [r (spec/check 'writ.spec-demo.sort-spec {:seed 42})] + (is (:ok r) (:message r)) + (testing "`_` marks the state: insert keeps a sorted list sorted" + (is (contains? #{:proved :tested} (:status (law-result r 'sorting:sorted:insert))))))) + +(deftest a-state-can-be-taken-out-of-a-result + (let [r (spec/check 'writ.spec-demo.links-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (= [{:graph 'store :status :ok :states 2 :edges 2}] (:graphs r))))) + +(deftest an-edge-marks-its-state-once + (is (str/includes? (expansion-error '(writ.spec/graph g {:states {:a Nat} :edges {:a {[f _ _] #{:a}}}})) + "marks the state with `_` more than once")) + (is (str/includes? (expansion-error '(writ.spec/graph g {:states {:a Nat} :edges {:a {[first Nat] #{:a}}}})) + "`first` takes the state alone"))) + +(deftest a-projection-must-fit-its-state + (let [r (spec/check 'writ.spec-demo.links-bad-spec {:seed 42})] + (is (not (:ok r))) + (is (str/includes? (:message r) + "graph `store`: the edge :added -[second]-> :links expects a (Map String String), but `second` of :added gives a String")))) + +(deftest a-graph-draws-as-a-state-diagram + (let [m (spec/mermaid 'writ.spec-demo.signal-spec {:graph 'signal})] + (is (str/starts-with? m "stateDiagram-v2")) + (is (str/includes? m "[*] --> green")) + (is (str/includes? m "green --> yellow : tick")) + (is (str/includes? m "green : green, a Green")))) + +(deftest the-plan-reads-from-the-spec-alone + (let [p (spec/plan 'writ.spec-demo.pipeline-spec)] + (is (str/includes? p "plan: writ.spec-demo.pipeline-spec for writ.spec-demo.pipeline")) + (is (str/includes? p "graph `request`")) + (is (str/includes? p ":clean Clean, a String where (= s (cleaned s))")) + (is (str/includes? p ":raw -[normalize]-> :clean")) + (is (str/includes? p "handle [String -> (Tuple Keyword String)]")) + (is (str/includes? p "laws: handle-answers-with-the-cleaned-input, ok-exactly-when-short")) + (is (str/includes? p "flow: s -> normalize -> respond -> result")) + (is (str/includes? p "calls exactly: normalize, respond")))) + +(deftest the-readmes-sort-spec-is-proved + (let [r (spec/check 'writ.spec-demo.readme-sort-spec {:seed 42})] + (is (:ok r) (:message r)) + (is (= :proved (:status (law-result r 'sorting:unsorted:isort)))) + (is (= :proved (:status (law-result r 'sorting:sorted:insert)))))) diff --git a/test/writ/proof_test.clj b/test/writ/proof_test.clj index 418cdc3..007d704 100644 --- a/test/writ/proof_test.clj +++ b/test/writ/proof_test.clj @@ -23,7 +23,8 @@ (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)))) + ;; three laws, the graph's edge and the witness for its step + (is (= 5 (:laws (:proof r)))) (is (str/includes? (:message r) "lemma `insert-keeps-sorted` proved"))))) (deftest a-false-lemma-fails-the-check diff --git a/test/writ/spec_demo/flow_plain_spec.clj b/test/writ/spec_demo/flow_plain_spec.clj new file mode 100644 index 0000000..a042e46 --- /dev/null +++ b/test/writ/spec_demo/flow_plain_spec.clj @@ -0,0 +1,21 @@ +(ns writ.spec-demo.flow-plain-spec + "A graph whose two states are the same plain type: nothing tells a + sorted list from an unsorted one." + (: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/flow_spec.clj b/test/writ/spec_demo/flow_spec.clj index 8da7acb..06edb24 100644 --- a/test/writ/spec_demo/flow_spec.clj +++ b/test/writ/spec_demo/flow_spec.clj @@ -1,20 +1,22 @@ (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]])) + "A graph from a plain type into a refinement: the sorted state says what + makes a list sorted, so the edge into it is the sort's law." + (:require [writ.spec :refer [spec ann law graph refine]])) (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)))) +(refine Sorted [xs (List Nat)] (ascending? xs)) + +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}}}}) + (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/flow_unknown_spec.clj b/test/writ/spec_demo/flow_unknown_spec.clj new file mode 100644 index 0000000..e43f542 --- /dev/null +++ b/test/writ/spec_demo/flow_unknown_spec.clj @@ -0,0 +1,18 @@ +(ns writ.spec-demo.flow-unknown-spec + "Flows that name what the target does not have." + (:require [writ.spec :refer [spec ann law flow graph refine]])) + +(spec writ.spec-demo.pipeline) + +(ann normalize [String -> String]) +(ann respond [String -> (Tuple Keyword String)]) +(ann handle [String -> (Tuple Keyword String)]) + +(graph request + {:states {:raw String, :response (Tuple Keyword String)} + :edges {:raw {[handle] #{:response}}}}) + +(flow handle [s] [s sanitize respond]) +(flow handle [s t] [s normalize]) + +(law answers (forall [s String] (keyword? (first (handle s))))) diff --git a/test/writ/spec_demo/links.clj b/test/writ/spec_demo/links.clj new file mode 100644 index 0000000..bce6f99 --- /dev/null +++ b/test/writ/spec_demo/links.clj @@ -0,0 +1,6 @@ +(ns writ.spec-demo.links + "A link store: adding a url hands back the grown store and the url's code.") + +(defn add [links url] + (let [code (str (count links))] + [(assoc links code url) code])) diff --git a/test/writ/spec_demo/links_bad_spec.clj b/test/writ/spec_demo/links_bad_spec.clj new file mode 100644 index 0000000..80efeef --- /dev/null +++ b/test/writ/spec_demo/links_bad_spec.clj @@ -0,0 +1,23 @@ +(ns writ.spec-demo.links-bad-spec + "The store goes around a loop: `add` returns the store with a code, and + the store is taken back out of that result for the next add." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.links) + +(ann add [(Map String String) String -> (Tuple (Map String String) String)]) + +(graph store + {:start [:links {}] + :states {:links (Map String String), :added (Tuple (Map String String) String)} + :edges {:links {[add String] #{:added}} + :added {[second] #{:links}}}}) + +(law add-keeps-the-url + (forall [links (Map String String), url String] + (let [[links2 code] (add links url)] (= url (get links2 code))))) + +(law add-grows-the-store-by-one + (forall [links (Map String String), url String] + (=> (not (contains? links (str (count links)))) + (= (inc (count links)) (count (first (add links url))))))) diff --git a/test/writ/spec_demo/links_spec.clj b/test/writ/spec_demo/links_spec.clj new file mode 100644 index 0000000..ecfeb92 --- /dev/null +++ b/test/writ/spec_demo/links_spec.clj @@ -0,0 +1,23 @@ +(ns writ.spec-demo.links-spec + "The store goes around a loop: `add` returns the store with a code, and + the store is taken back out of that result for the next add." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.links) + +(ann add [(Map String String) String -> (Tuple (Map String String) String)]) + +(graph store + {:start [:links {}] + :states {:links (Map String String), :added (Tuple (Map String String) String)} + :edges {:links {[add String] #{:added}} + :added {[first] #{:links}}}}) + +(law add-keeps-the-url + (forall [links (Map String String), url String] + (let [[links2 code] (add links url)] (= url (get links2 code))))) + +(law add-grows-the-store-by-one + (forall [links (Map String String), url String] + (=> (not (contains? links (str (count links)))) + (= (inc (count links)) (count (first (add links url))))))) diff --git a/test/writ/spec_demo/nat_chain_spec.clj b/test/writ/spec_demo/nat_chain_spec.clj index cda1a5c..ed079c9 100644 --- a/test/writ/spec_demo/nat_chain_spec.clj +++ b/test/writ/spec_demo/nat_chain_spec.clj @@ -9,8 +9,8 @@ (ann thirds [Nat -> Nat]) (graph dividing - {:states {:n Nat, :part Nat} - :edges {:n {[half] #{:part}, [parity] #{:part}, [half-by-two] #{:part}, [thirds] #{:part}}}}) + {:states {:n Nat} + :edges {:n {[half] #{:n}, [parity] #{:n}, [half-by-two] #{:n}, [thirds] #{:n}}}}) (law half-halves (forall [n Nat] (= (half n) (quot n 2)))) (law parity-is-mod-2 (forall [n Nat] (= (parity n) (mod n 2)))) diff --git a/test/writ/spec_demo/pipeline_layers_spec.clj b/test/writ/spec_demo/pipeline_layers_spec.clj new file mode 100644 index 0000000..e6fb2b7 --- /dev/null +++ b/test/writ/spec_demo/pipeline_layers_spec.clj @@ -0,0 +1,28 @@ +(ns writ.spec-demo.pipeline-layers-spec + "The pipeline's layers stated as reach, not as exact call sets: `handle` + goes through `respond`, which decides validity, and nothing it reaches + upper-cases a request." + (:require [clojure.string :as str] + [writ.spec :refer [spec ann law calls graph]])) + +(spec writ.spec-demo.pipeline) + +(ann normalize [String -> String]) +(ann valid? [String -> Bool]) +(ann respond [String -> (Tuple Keyword String)]) +(ann handle [String -> (Tuple Keyword String)]) + +(graph request + {:states {:raw String, :response (Tuple Keyword String)} + :edges {:raw {[handle] #{:response}}}}) + +(calls handle {:through [normalize respond valid?] :not [str/upper-case]}) + +(defn cleaned [s] (str/lower-case (str/trim s))) + +(law handle-answers-with-the-cleaned-input + (forall [s String] (= (second (handle s)) (cleaned s)))) + +(law ok-exactly-when-short + (forall [s String] + (= (= :ok (first (handle s))) (<= 1 (count (cleaned s)) 8)))) diff --git a/test/writ/spec_demo/pipeline_many.clj b/test/writ/spec_demo/pipeline_many.clj new file mode 100644 index 0000000..2ef0348 --- /dev/null +++ b/test/writ/spec_demo/pipeline_many.clj @@ -0,0 +1,23 @@ +(ns writ.spec-demo.pipeline-many + "Requests handled in bulk: data reaches each layer through a lambda, a + fn passed by name, a loop and a let." + (:require [clojure.string :as str])) + +(defn normalize [s] + (str/lower-case (str/trim s))) + +(defn valid? [s] + (<= 1 (count s) 8)) + +(defn respond [s] + (if (valid? s) [:ok s] [:error s])) + +(defn handle-all [ss] + (map respond (map (fn [s] (normalize s)) ss))) + +(defn count-ok [ss] + (loop [xs ss, n 0] + (if (seq xs) + (let [r (respond (first xs))] + (recur (rest xs) (if (= :ok (first r)) (inc n) n))) + n))) diff --git a/test/writ/spec_demo/pipeline_spec.clj b/test/writ/spec_demo/pipeline_spec.clj index fc568e7..a9fcd97 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 graph]])) + [writ.spec :refer [spec ann law calls graph flow refine]])) (spec writ.spec-demo.pipeline) @@ -11,8 +11,13 @@ (ann respond [String -> (Tuple Keyword String)]) (ann handle [String -> (Tuple Keyword String)]) +(defn cleaned [s] (str/lower-case (str/trim s))) + +;; what normalize hands on: trimmed and lower case already +(refine Clean [s String] (= s (cleaned s))) + (graph request - {:states {:raw String, :clean String, :valid Bool, :response (Tuple Keyword String)} + {:states {:raw String, :clean Clean, :valid Bool, :response (Tuple Keyword String)} :edges {:raw {[normalize] #{:clean}, [handle] #{:response}} :clean {[valid?] #{:valid}, [respond] #{:response}}}}) @@ -21,7 +26,11 @@ (calls respond [valid?]) (calls handle [normalize respond]) -(defn cleaned [s] (str/lower-case (str/trim s))) +;; the request is normalized, the normalized request is what respond +;; answers, and its answer is handle's +(flow handle [s] + [s normalize respond :result] + [normalize :result]) (law handle-answers-with-the-cleaned-input (forall [s String] (= (second (handle s)) (cleaned s)))) diff --git a/test/writ/spec_demo/pipeline_swapped.clj b/test/writ/spec_demo/pipeline_swapped.clj new file mode 100644 index 0000000..00bde25 --- /dev/null +++ b/test/writ/spec_demo/pipeline_swapped.clj @@ -0,0 +1,17 @@ +(ns writ.spec-demo.pipeline-swapped + "`handle` calls both layers, as the spec's `calls` says, but hands + `respond` the raw input and throws the normalized one away." + (:require [clojure.string :as str])) + +(defn normalize [s] + (str/lower-case (str/trim s))) + +(defn valid? [s] + (<= 1 (count s) 8)) + +(defn respond [s] + (if (valid? s) [:ok s] [:error s])) + +(defn handle [s] + (let [n (normalize s)] + (respond s))) diff --git a/test/writ/spec_demo/pipeline_upper.clj b/test/writ/spec_demo/pipeline_upper.clj new file mode 100644 index 0000000..715f452 --- /dev/null +++ b/test/writ/spec_demo/pipeline_upper.clj @@ -0,0 +1,16 @@ +(ns writ.spec-demo.pipeline-upper + "`normalize` shouts: it upper-cases, which the spec says no request + handling may do." + (:require [clojure.string :as str])) + +(defn normalize [s] + (str/upper-case (str/trim s))) + +(defn valid? [s] + (<= 1 (count s) 8)) + +(defn respond [s] + (if (valid? s) [:ok s] [:error s])) + +(defn handle [s] + (respond (normalize s))) diff --git a/test/writ/spec_demo/readme_sort_spec.clj b/test/writ/spec_demo/readme_sort_spec.clj new file mode 100644 index 0000000..34ff839 --- /dev/null +++ b/test/writ/spec_demo/readme_sort_spec.clj @@ -0,0 +1,34 @@ +(ns writ.spec-demo.readme-sort-spec + "The README's sort spec, word for word but for the target: the graph's + edges carry `sorted` and `insert-keeps-sorted`, and both are proved." + (:require [writ.spec :refer [spec ann law graph refine]])) + +(spec writ.spec-demo.sort {:require :proved}) + +(ann insert [Nat (List Nat) -> (List Nat)]) +(ann isort [(List Nat) -> (List Nat)]) + +(defn ascending? [xs] + (or (empty? xs) (apply <= xs))) + +;; what makes a list sorted +(refine Sorted [xs (List Nat)] (ascending? xs)) + +;; the problem's states: a list goes in, a sorted list comes out, and +;; inserting into a sorted list keeps it sorted (`_` is where the state goes) +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}} + :sorted {[insert Nat _] #{:sorted}}}}) + +(defn occurrences [x xs] + (count (filter #(= x %) xs))) + +;; the graph already says a sort puts its input in order; it also +;; keeps every element, duplicates included +(law permutation (forall [x Nat, xs (List Nat)] + (= (occurrences x (isort xs)) (occurrences x xs)))) + +;; and insert adds exactly one x +(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/shadow.clj b/test/writ/spec_demo/shadow.clj new file mode 100644 index 0000000..c75093b --- /dev/null +++ b/test/writ/spec_demo/shadow.clj @@ -0,0 +1,8 @@ +(ns writ.spec-demo.shadow + "An insertion sort's name for its own order test, the same name as the + spec's helper. `isort` here only rotates its input.") + +(defn ascending? [xs] true) + +(defn isort [xs] + (if (seq xs) (concat (rest xs) (list (first xs))) ())) diff --git a/test/writ/spec_demo/shadow_spec.clj b/test/writ/spec_demo/shadow_spec.clj new file mode 100644 index 0000000..25cb2cd --- /dev/null +++ b/test/writ/spec_demo/shadow_spec.clj @@ -0,0 +1,19 @@ +(ns writ.spec-demo.shadow-spec + "A sort spec whose helper `ascending?` shares its name with a fn of the + target. A law must judge the code with the spec's helper, never the + target's, so writ rejects the ambiguity instead of picking one." + (:require [writ.spec :refer [spec ann law graph]])) + +(spec writ.spec-demo.shadow) + +(graph sorting {:states {:unsorted (List Nat), :sorted (List Nat)} + :edges {:unsorted {[isort] #{:sorted}}}}) + +(ann isort [(List Nat) -> (List Nat)]) + +(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)))) diff --git a/test/writ/spec_demo/shell.clj b/test/writ/spec_demo/shell.clj new file mode 100644 index 0000000..c4f00dd --- /dev/null +++ b/test/writ/spec_demo/shell.clj @@ -0,0 +1,12 @@ +(ns writ.spec-demo.shell + "An effect shell over the pipeline: it prints, so writ does not check + its code, but a spec can still say how it is wired." + (:require [writ.spec-demo.pipeline :as p])) + +(defn- show [r] (println (pr-str r)) r) + +(defn serve [line] + (show (p/handle line))) + +(defn serve-raw [line] + (show (p/respond line))) diff --git a/test/writ/spec_demo/shell_spec.clj b/test/writ/spec_demo/shell_spec.clj new file mode 100644 index 0000000..75b825f --- /dev/null +++ b/test/writ/spec_demo/shell_spec.clj @@ -0,0 +1,30 @@ +(ns writ.spec-demo.shell-spec + "The pipeline's spec, with the shell's wiring: `serve` hands each line + to the pipeline's `handle`, and never answers it with `respond` alone." + (:require [writ.spec-demo.shell :as shell] + [writ.spec-demo.pipeline :as p] + [writ.spec :refer [spec ann law calls graph flow]])) + +(spec writ.spec-demo.pipeline) + +(ann normalize [String -> String]) +(ann valid? [String -> Bool]) +(ann respond [String -> (Tuple Keyword String)]) +(ann handle [String -> (Tuple Keyword String)]) + +(graph request + {:states {:raw String, :response (Tuple Keyword String)} + :edges {:raw {[handle] #{:response}}}}) + +(calls shell/serve {:through [p/handle]}) +(calls shell/serve-raw {:through [p/handle]}) +(flow shell/serve [line] [line p/handle show :result]) + +(law answers (forall [s String] (keyword? (first (handle s))))) +(law ok-exactly-when-short + (forall [s String] + (= (= :ok (first (handle s))) + (<= 1 (count (clojure.string/lower-case (clojure.string/trim s))) 8)))) +(law keeps-the-cleaned-input + (forall [s String] + (= (second (handle s)) (clojure.string/lower-case (clojure.string/trim s))))) diff --git a/test/writ/spec_demo/signal_mixed_spec.clj b/test/writ/spec_demo/signal_mixed_spec.clj new file mode 100644 index 0000000..032fe86 --- /dev/null +++ b/test/writ/spec_demo/signal_mixed_spec.clj @@ -0,0 +1,20 @@ +(ns writ.spec-demo.signal-mixed-spec + "The signal with red left a plain tuple. An edge into yellow or red then + says nothing about where a tick from yellow goes: every tuple is in red." + (:require [writ.spec-demo.signal :refer [GREEN YELLOW]] + [writ.spec :refer [spec ann refine graph law]])) + +(spec writ.spec-demo.signal) + +(ann tick [(Tuple Keyword Nat) -> (Tuple Keyword Nat)]) + +(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))) + +(graph signal + {:states {:green Green, :yellow Yellow, :red (Tuple Keyword Nat)} + :edges {:green {[tick] #{:green :yellow}} + :yellow {[tick] #{:yellow :red}}}}) + +(law a-light-counts-up-while-it-shows + (forall [l Green] (=> (< (second l) GREEN) (= (tick l) [:Green (inc (second l))])))) diff --git a/test/writ/spec_demo/signal_stuck.clj b/test/writ/spec_demo/signal_stuck.clj new file mode 100644 index 0000000..b7db201 --- /dev/null +++ b/test/writ/spec_demo/signal_stuck.clj @@ -0,0 +1,15 @@ +(ns writ.spec-demo.signal-stuck + "A signal that counts up and then stays put: it never changes colour. + Every tick keeps a light in its own phase, so each edge's law holds, + but the graph's steps to the next phase are never taken.") + +(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)] light) + :Yellow (if (< t YELLOW) [:Yellow (inc t)] light) + :Red (if (< t RED) [:Red (inc t)] light)))) diff --git a/test/writ/spec_demo/sort_every_spec.clj b/test/writ/spec_demo/sort_every_spec.clj index f3bcc9a..2fc7b0e 100644 --- a/test/writ/spec_demo/sort_every_spec.clj +++ b/test/writ/spec_demo/sort_every_spec.clj @@ -1,16 +1,18 @@ (ns writ.spec-demo.sort-every-spec "A law that passes a fn literal to every?." - (:require [writ.spec :refer [spec ann law graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(refine Sorted [xs (List Nat)] (or (empty? xs) (apply <= xs))) + (graph sorting - {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :edges {:unsorted {[isort] #{:sorted}} - :item {[insert (List Nat)] #{:sorted}}}}) + :sorted {[insert Nat _] #{:sorted}}}}) (law every-prefix-starts-low (forall [xs (List Nat)] diff --git a/test/writ/spec_demo/sort_extra.clj b/test/writ/spec_demo/sort_extra.clj new file mode 100644 index 0000000..ac01a79 --- /dev/null +++ b/test/writ/spec_demo/sort_extra.clj @@ -0,0 +1,16 @@ +(ns writ.spec-demo.sort-extra + "The insertion sort with a public fn the spec never planned.") + +(defn insert [x xs] + (if (seq xs) + (if (<= x (first xs)) + (cons x xs) + (cons (first xs) (insert x (rest xs)))) + (list x))) + +(defn isort [xs] + (if (seq xs) + (insert (first xs) (isort (rest xs))) + ())) + +(defn largest [xs] (last (isort xs))) diff --git a/test/writ/spec_demo/sort_lemma_spec.clj b/test/writ/spec_demo/sort_lemma_spec.clj index 34f74cb..d66c9ec 100644 --- a/test/writ/spec_demo/sort_lemma_spec.clj +++ b/test/writ/spec_demo/sort_lemma_spec.clj @@ -2,18 +2,21 @@ "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]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort {:require :proved}) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(defn ascending? [xs] (or (empty? xs) (apply <= xs))) + +;; no edge for insert: what it keeps is the proof namespace's lemma +(refine Sorted [xs (List Nat)] (ascending? xs)) + (graph sorting - {:states {:unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :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)))) diff --git a/test/writ/spec_demo/sort_let_spec.clj b/test/writ/spec_demo/sort_let_spec.clj index 437696f..a6d593a 100644 --- a/test/writ/spec_demo/sort_let_spec.clj +++ b/test/writ/spec_demo/sort_let_spec.clj @@ -1,16 +1,18 @@ (ns writ.spec-demo.sort-let-spec "A law whose predicate binds a local with `let`." - (:require [writ.spec :refer [spec ann law graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(refine Sorted [xs (List Nat)] (or (empty? xs) (apply <= xs))) + (graph sorting - {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :edges {:unsorted {[isort] #{:sorted}} - :item {[insert (List Nat)] #{:sorted}}}}) + :sorted {[insert Nat _] #{:sorted}}}}) (law smallest-first (forall [xs (List Nat)] diff --git a/test/writ/spec_demo/sort_pairs_spec.clj b/test/writ/spec_demo/sort_pairs_spec.clj index 47fc45f..1efbd20 100644 --- a/test/writ/spec_demo/sort_pairs_spec.clj +++ b/test/writ/spec_demo/sort_pairs_spec.clj @@ -1,17 +1,19 @@ (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 graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(refine Sorted [xs (List Nat)] (or (empty? xs) (apply <= xs))) + (graph sorting - {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :edges {:unsorted {[isort] #{:sorted}} - :item {[insert (List Nat)] #{:sorted}}}}) + :sorted {[insert Nat _] #{:sorted}}}}) (defn in-order? [xs] (every? (fn [[a b]] (<= a b)) (partition 2 1 xs))) diff --git a/test/writ/spec_demo/sort_proved_spec.clj b/test/writ/spec_demo/sort_proved_spec.clj index 3b2967f..d73b8f9 100644 --- a/test/writ/spec_demo/sort_proved_spec.clj +++ b/test/writ/spec_demo/sort_proved_spec.clj @@ -1,21 +1,23 @@ (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 graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (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))) +(refine Sorted [xs (List Nat)] (ascending? xs)) + +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}} + :sorted {[insert Nat _] #{:sorted}}}}) + (defn occurrences [x xs] (count (filter #(= x %) xs))) diff --git a/test/writ/spec_demo/sort_spec.clj b/test/writ/spec_demo/sort_spec.clj index a7a0399..c2ad950 100644 --- a/test/writ/spec_demo/sort_spec.clj +++ b/test/writ/spec_demo/sort_spec.clj @@ -5,21 +5,25 @@ 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 graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (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))) +;; a list goes in, a sorted one comes out +(refine Sorted [xs (List Nat)] (ascending? xs)) + +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}} + ;; `_` is where the state goes: (insert x sorted-list) + :sorted {[insert Nat _] #{:sorted}}}}) + (defn occurrences [x xs] (count (filter #(= x %) xs))) diff --git a/test/writ/spec_demo/sort_unproved_spec.clj b/test/writ/spec_demo/sort_unproved_spec.clj index 62aafa2..1701308 100644 --- a/test/writ/spec_demo/sort_unproved_spec.clj +++ b/test/writ/spec_demo/sort_unproved_spec.clj @@ -1,21 +1,23 @@ (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 graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (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))) +(refine Sorted [xs (List Nat)] (ascending? xs)) + +(graph sorting + {:states {:unsorted (List Nat), :sorted Sorted} + :edges {:unsorted {[isort] #{:sorted}} + :sorted {[insert Nat _] #{:sorted}}}}) + (defn occurrences [x xs] (count (filter #(= x %) xs))) diff --git a/test/writ/spec_demo/sort_vacuous_spec.clj b/test/writ/spec_demo/sort_vacuous_spec.clj index aee8e18..1b4c3d4 100644 --- a/test/writ/spec_demo/sort_vacuous_spec.clj +++ b/test/writ/spec_demo/sort_vacuous_spec.clj @@ -1,16 +1,18 @@ (ns writ.spec-demo.sort-vacuous-spec "A spec whose laws are true of any implementation." - (:require [writ.spec :refer [spec ann law graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(refine Sorted [xs (List Nat)] (or (empty? xs) (apply <= xs))) + (graph sorting - {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :edges {:unsorted {[isort] #{:sorted}} - :item {[insert (List Nat)] #{:sorted}}}}) + :sorted {[insert 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 87705c3..93e34f2 100644 --- a/test/writ/spec_demo/sort_weak_spec.clj +++ b/test/writ/spec_demo/sort_weak_spec.clj @@ -1,15 +1,17 @@ (ns writ.spec-demo.sort-weak-spec "A spec that states only that the output is ordered." - (:require [writ.spec :refer [spec ann law graph]])) + (:require [writ.spec :refer [spec ann law graph refine]])) (spec writ.spec-demo.sort) (ann insert [Nat (List Nat) -> (List Nat)]) (ann isort [(List Nat) -> (List Nat)]) +(refine Sorted [xs (List Nat)] (or (empty? xs) (apply <= xs))) + (graph sorting - {:states {:item Nat, :unsorted (List Nat), :sorted (List Nat)} + {:states {:unsorted (List Nat), :sorted Sorted} :edges {:unsorted {[isort] #{:sorted}} - :item {[insert (List Nat)] #{:sorted}}}}) + :sorted {[insert 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 ad9ab6c..b33a85d 100644 --- a/test/writ/spec_demo/total_spec.clj +++ b/test/writ/spec_demo/total_spec.clj @@ -8,8 +8,8 @@ (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}}}}) + {:states {:items (List Nat), :number Nat} + :edges {:items {[total] #{:number}, [total-by-reduce] #{:number}, [size] #{:number}}}}) (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)))) diff --git a/test/writ/spec_demo/tree_spec.clj b/test/writ/spec_demo/tree_spec.clj index 014f5e2..9497670 100644 --- a/test/writ/spec_demo/tree_spec.clj +++ b/test/writ/spec_demo/tree_spec.clj @@ -15,9 +15,8 @@ (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}}}}) + {:states {:tree Tree, :listed (List Nat), :size Nat} + :edges {:tree {[insert Nat _] #{:tree}, [to-list] #{:listed}, [size] #{:size}}}}) (defn strictly-ascending? [xs] (or (empty? xs) (apply < xs))) diff --git a/test/writ/spec_test.clj b/test/writ/spec_test.clj index 2fb14e0..9480ca7 100644 --- a/test/writ/spec_test.clj +++ b/test/writ/spec_test.clj @@ -297,7 +297,7 @@ (deftest a-spec-that-does-not-pin-a-fn-down-has-gaps (let [r (spec/check 'writ.spec-demo.sort-weak-spec {:seed 42}) gap-fns (set (map :fn (:gaps r)))] - (is (every? #(contains? #{:tested :proved} (:status %)) (:laws r)) "every law holds") + (is (every? #(contains? #{:tested :proved :witnessed} (:status %)) (:laws r)) "every law holds") (is (not (:ok r)) "but the spec is too weak to mean anything") (is (contains? gap-fns 'isort)) (testing "the report names the impostor that satisfied every law" @@ -346,7 +346,7 @@ (deftest laws-that-fix-an-argument-leave-the-rest-unspecified (let [r (spec/check 'writ.spec-demo.classify-weak-spec {:seed 42})] - (is (every? #(contains? #{:tested :proved} (:status %)) (:laws r)) "every law holds") + (is (every? #(contains? #{:tested :proved :witnessed} (:status %)) (:laws r)) "every law holds") (is (not (:ok r))) (is (= ['classify-read] (map :fn (:gaps r)))) (is (re-find #"when it returns a different value whenever `n` is not one of -127, -2, -1, 0" @@ -572,3 +572,32 @@ (is (str/includes? m "[*] --> Locked")) (is (str/includes? m "Locked --> Unlocked : Coin")) (is (str/includes? m "Locked --> [*]")))) + +;; --- a law judges the code with the spec's own helpers ------------------------ + +(deftest a-helper-named-like-a-target-fn-is-rejected + (let [r (spec/check 'writ.spec-demo.shadow-spec {:seed 42})] + (is (not (:ok r))) + (is (= '[ascending?] (:ambiguous r))) + (is (empty? (:laws r)) "no law runs while a name means two things") + (is (str/includes? (:message r) + "`ascending?` is defined by the spec and by writ.spec-demo.shadow")) + (is (str/includes? (:message r) "rename the spec's `ascending?`")))) + +;; --- the spec bounds the code's public fns -------------------------------------- + +(deftest a-public-fn-the-spec-does-not-sign-fails + (let [r (spec/check spec-ns {:target 'writ.spec-demo.sort-extra :seed 42})] + (is (not (:ok r))) + (is (= '[largest] (:unspecified r))) + (is (str/includes? (:message r) + "`largest` is public, but the spec gives it no signature")) + (is (str/includes? (:message r) "make it private with defn-")))) + +(deftest the-report-names-public-fns-off-the-graph + (let [r (spec/check spec-ns {:seed 42})] + (is (:ok r) (:message r)) + (is (= [] (:off-graph r)) "insert is a step: it keeps a sorted list sorted")) + (let [r (spec/check 'writ.spec-demo.flow-spec {:seed 42})] + (is (= '[insert] (:off-graph r))) + (is (str/includes? (:message r) "not a step of any graph or machine: insert")))) diff --git a/test/writ/test_runner.clj b/test/writ/test_runner.clj index 3370300..277bc75 100644 --- a/test/writ/test_runner.clj +++ b/test/writ/test_runner.clj @@ -11,11 +11,12 @@ writ.graph-test writ.solve-test writ.symbolic-test - writ.proof-test)) + writ.proof-test + writ.flow-test)) (def test-namespaces '[writ.check-test writ.book-test writ.gaps-test writ.spec-test writ.prove-test writ.evidence-test - writ.graph-test writ.solve-test writ.symbolic-test writ.proof-test]) + writ.graph-test writ.solve-test writ.symbolic-test writ.proof-test writ.flow-test]) (defn -main [& _] (let [{:keys [fail error]} (apply t/run-tests test-namespaces)]