git:20260930.f36b86d to git:20261001.2964f6e

---

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/invariant/question/ann/data/law/assume/calls/flow/

machine/plan/elicit/obligations/attest) -- or its proof namespace

(proof-of/lemma/hint), or the plain Clojure implementation it

constrains, or when reading a writ.spec report or any

"Writ:" error (purity, termination, ordering, arity, types, tagged data,

failing, unproved, vacuous or gapped laws, graph rules, call graph

mismatches). Also for the annotated writ.defn surface (w/defn, ^:many,

w/match, w/law, w/proof).

---

# writ

writ checks plain Clojure against a spec of what the code is for. A spec

namespace is the problem statement in checkable form: it signs the public

fns and states laws about what their results mean. The implementation never

mentions writ. `(writ.spec/check 'my.spec)` runs Bend's static rules over

the implementation's source using those types, runs the laws, and then

checks that the laws actually pin the code down. It returns a report that

names what is wrong. writ runs on jolt; writ.spec uses test.check.

## Who owns what

- The spec (`spec`, `ann`, `data`, `law`) is the contract. A person or an

agent may write it; once written, it is the contract. Do not weaken a

law, loosen an `ann`, lower a `:require`, or delete any of them to get a

check to pass. If the spec looks wrong, say so and ask. Do not answer or

downgrade a blocking `question` yourself. `(spec/attest record 'my.spec)`

compares a recorded check with the spec now and names every way it got

weaker.

- The implementation is yours. Change it until `check` reports `:ok`.

- If you are asked to write the spec, write the intent: see

[What a spec should say](#what-a-spec-should-say).

- A report that fails is the next thing to fix. Read the whole message: it

names the rule or law, the input, and the values.

## Writing a spec, in order

1. `(spec my.ns {:require :proved})` -- the namespace it constrains; ask

for proof.

2. The state graph: the problem's states as types, refinements most

often, and the fns that step between them. Every spec has one; write

it before the laws. See [The state graph](#the-state-graph).

3. `ann` for each public fn. 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. Record anything the problem statement

leaves open as `(question id "...")`; add `{:blocking true}` when the

next piece of work depends on the answer. Never invent the answer.

6. Ask what the problem statement leaves to chance (see

[What to ask](#what-to-ask)), then show the plan: `(spec/plan 'my.spec)`

prints states, steps, signatures, laws and wiring from the spec alone,

and ends with the questions its types raise. 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.

## What to ask

Code decides every case one way or another; a spec should say which way

someone chose. Before the plan is confirmed, go through these with the

spec's owner, and turn each answer into a law, a state or a step, or a

`(question ...)` when nobody knows yet. Never pick an answer yourself.

- The core method: what the result is, stated so two people would compute

the same thing.

- Units and precision: what a number counts, how exact it must be, how it

rounds.

- Order and ties: which comes first when two are equal, and whether order

matters at all.

- Thresholds: whether a boundary value is in or out (`<` or `<=`).

- Empty and edge inputs: an empty collection or string, zero, a negative

number, nil, the largest value that can arrive.

- Missing values: what an absent optional key or value means.

- Surplus and shortfall: too much, too little, not enough to go round.

- Scope: what the code is not responsible for, and who is.

- The whole life: whether what happens can be undone, cancelled,

repeated, paused, or expire.

`(spec/elicit 'my.spec)` lists the kinds its types raise, with the fns or

graphs each is about; `plan` prints them last. Those are prompts, not

failures: a law over every input may already answer one.

## The state graph

```clojure

(refine Green [l (Tuple Keyword Nat)] (and (= :Green (first l)) (<= (second l) GREEN)))

(refine Yellow [l (Tuple Keyword Nat)] (and (= :Yellow (first l)) (<= (second l) YELLOW)))

(refine Red [l (Tuple Keyword Nat)] (and (= :Red (first l)) (<= (second l) RED)))

(graph signal

{:start [:green [:Green 0]] ; a state, or [state value]

:states {:green Green, :yellow Yellow, :red Red}

:edges {:green {[tick] #{:green :yellow}} ; [fn ArgType ...] -> targets

:yellow {[tick] #{:yellow :red}}

:red {[tick] #{:red :green}}}

:before [[:yellow :red]]}) ; also :never [[a b]], :final [s]

```

- 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

- 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, 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.

- An edge argument written `'name` is not a type but the spec's own value

of that name, passed as is: `[scan (Vec Pattern) 'yes Nat]` hands

`scan` the spec's `yes` guard, since a fn cannot be generated.

- `:tested {state "why"}` lets the edges out of a state off proof, as

`{:require :tested :because "why"}` does for a law. A report says so when

such an edge gets proved after all, so the marker can go.

- `: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 state reached from the start with no

edges out must be listed in `:final`.

- `(invariant g :state [v] pred)`: what every value of the state holds,

whichever edge it came by. Each edge landing there carries it, plain

states included, and a `[state value]` start must satisfy it. Each edge

out of the state may assume it, so an invariant kept by induction is

kept; with a keyword `:start`, edges out of the start state assume

nothing, since it may begin at any value. One the refinement already

implies is vacuous and fails.

- A guarded edge: `{[withdraw Nat] {:to #{:open} :when (fn [a amt] (<= amt

(second a))) :else :keep}}`. The `:when` fn takes the edge fn's own

arguments, in the fn's order. The edge law and steps hold under the

test; `g:s:f:refused` says a refused step keeps the state (`:keep`, the

default) or lands in the `:else` state; `g:s:f:when` says some value

passes the guard; for an `and` test, `g:s:f:when.N` says clause N fails

while the others hold. Guard what the problem refuses, rather than

folding the refusal into the targets.

- Who may act: `:actors {:type User :role :role}` on the graph names the

argument that acts and the key holding its role, and `:by #{:owner}` on

an edge the roles that may take it. It is a guard, joined after the

edge's own `:when`, so a step by anyone else must be refused and keep

the state; `plan` lists who may do what.

- A frame, on a record state: `{[award Nat] {:to #{:active} :changes

[:points]}}`. `g:s:f:frame` says the step changes only those keys and

keeps every other one, named by the record or not, as it was. It can go

- `:runs N` (with `:depth D`, default 20) walks N seeded runs from a

`[state value]` start through the real fns: every landing must be in an

allowed state and hold its invariants, and every final state the graph

## A spec

```clojure

(ns my.sort-spec

(:require [writ.spec :refer [spec data ann law graph refine]]))

(spec my.sort {:require :proved}) ; the namespace it constrains

(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

(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-adds (forall [x Nat, xs (List Nat)]

(= (occurrences x (insert x xs)) (inc (occurrences x xs)))))

```

- `(spec ns)` comes first; `(spec ns {:require :proved})` makes every law

need a proof, not just passing tests. Prefer it for new specs.

- `(ann f [A B -> R])`: the parameter count must match the fn, which has a

single arity. `(ann f [A B -> R] {:requires (fn [a b] test) :ensures

(fn [a b r] test)})` adds what the arguments must meet and what the

result meets given them; `:ensures` becomes the law `f:ensures`, and

both are checked on every call while laws run. A private helper that recurses over a collection needs an

`ann` too, or writ cannot tell the collection is finite.

- `(data Tree Leaf (Node Tree Nat Tree))`, or `(data Box [a] (Wrap a))`

with type parameters.

- Types: `Nat Int Bool String Char Keyword Symbol Float Double Unit Any`,

`(List T) (Vec T) (Set T) (Map K V) (Tuple T ...) (Opt T)`, `(-> A R)`,

records such as `{:id Nat, :nick (Opt String)}`, `(Index :id Member

:unique [:email])` (a map of records keyed by their :id, no two sharing

an email, nil counting as one), and declared data. A fn type takes at

most eight arguments.

`(List T)` is any seq: list, vector, lazy seq or nil. `(Opt T)` is a T

or nil.

A generated `String` is mostly letters and digits, sometimes printable

ASCII with whitespace. A generated `Int` stays within -50..50 and a `Nat` within 0..50 (the

default `:max-size`), so a quantified law never reaches a value like

`-127`. Anchor such values with a law that names them. A quarter of the

time a `Keyword`, `Int`, `Nat` or `Any` is instead one of the literals the

target's code mentions (with each integer's neighbours), and an `Any` is

sometimes a vector tagged with one of its keywords, so a branch on

`(= :normal reason)` or `(case (first ret) :reply ...)` is reached.

- A law is built from:

- `(= a b)`

- `(and P ...)`

- `(forall [x T, y U] P)`

- `(throws? e)`: evaluating `e` throws, lazy seqs in its value

realised. A signature broken by the law itself is rethrown, not

counted. Refer it from `writ.spec`.

- 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. A spec helper may not share a name with

a target public fn: the check fails and says to rename the helper.

A law may quantify over fn types: `(forall [p (-> Nat Bool)] ...)`

draws pure fns, each answering the same arguments the same way, and a

counterexample prints one as the calls it answered.

- `(calls f [g str/join])`: `f`'s direct calls are exactly this set.

Multi-arity fns and macros are read too: a macro calls what it calls as

it expands and what its expansion names. Name another namespace's fns

in full (`ensemble.signal/on-signal`) when that namespace is not written

yet, so the spec loads, and `plan` runs, before the code exists. 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. `(calls f {:through [g] :not [h]})` states reach

instead: `f` reaches `g` through any chain of calls, into the project

namespaces `f`'s namespace requires as well (not clojure.* or jolt.*),

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).

## Assumptions

When the code calls something writ does not check (`clojure.string`, a

library, another namespace), say what the spec takes as given:

```clojure

(assume str/trim [String -> String]) ; a signature, via the spec's alias

(assume trim-is-idempotent ; a law about such fns only

(forall [s String] (= (str/trim (str/trim s)) (str/trim s))))

```

A signature types the calls statically and is checked where the fn

returns while laws run, on the code's calls and the laws', not writ's

own or the dependency's calls to itself. A law is tested

against the real fns every check and cited by the prover like a lemma,

without proof. An assumption may not call the target's fns, directly or

through a spec helper. Every report lists what is assumed, and

`attest` counts a new assumption as weakening the spec, so assume what the

dependency documents, not whatever closes a proof.

- ``assumption `x` does not hold of the code it is about`` - the claim

about the dependency is false; fix the claim, not the code.

- ``assumption `x` calls `f`, a fn of target`` - state what the target

does as a law instead.

- A law left tested as "outside the prover: `frequencies`" can rest on an

assumption about it: `(assume clojure.core/frequencies [...])` and a

law about it, which the prover then cites. The signature types every

plain `frequencies` call in the code, unless the namespace excludes it

from core or refers another fn by that name.

- ``assumes a signature for `ns/f`, which does not resolve`` - require

the namespace in the spec and name the fn through its alias.

## The proof namespace

When a law holds but isn't proved, add what the prover needs in

`my/sort_proof.clj` (found by name for `my.sort-spec`), not in the spec:

```clojure

(ns my.sort-proof

(:require [writ.spec :refer [proof-of lemma hint]]))

(proof-of my.sort-spec)

(lemma insert-keeps-sorted ; a law about the code; must be proved

(forall [x Nat, xs (List Nat)]

(=> (my.sort-spec/ascending? xs) (my.sort-spec/ascending? (insert x xs)))))

(hint sorted {:induct xs :use [insert-keeps-sorted]})

```

- A lemma must hold and be proved, or the check fails; it then helps

prove the spec's laws. It never counts as one of them, and never

judges a stand-in, so it can't strengthen a weak spec.

- A lemma may be about clojure.core alone, and its hypothesis may name a

variable its conclusion doesn't: the prover takes it from the goal's

facts. `defn` helpers (an invariant such as `bst?`) may live in the

proof namespace too.

- A hint: `:induct` a variable first, `:vary [acc]` to let the induction

hypothesis hold at any acc (a fold's accumulator), `:use` only these

lemmas and laws, `:strategy` `:symbolic` / `:induction` / `:rewriting`,

`:fuel` more rewrites. It only steers the search.

- The prover reads the target and the project namespaces it requires, so a

pure core split over several namespaces is proved as one. A value of

type `Any` is modelled as an integer, a constant, a boolean, nil, or an

opaque value that can only be passed along and compared. A numeric test

or a lookup on an opaque value is some boolean or some value the solver

may choose, which only adds models; arithmetic on one is left to

testing. A vector literal is known to be a vector and a `list`, `cons`,

`map` or `rest` result known not to be, so `vector?`, `sequential?` and

`get` on them are decided. A constant's kind (keyword, symbol, string,

char) is known, so `keyword?` and `symbol?` are decided too.

- Maps are modelled: literals, `assoc`, `dissoc`, `merge`, `get`, `(:k m)`,

`(m k)`, `contains?`, `count` and equality by entries, keys symbolic or

not; `keys` and `vals` are unordered, so `every?` over them works and an

order-sensitive use gives up. A map of unknown size (a `(Map K V)`

variable) is outside.

- A recursive definition is unfolded, exactly, while a literal drives it --

a pattern walked to its end, a vector of known length -- up to a depth

and a count; past them the law is left to testing.

- A branch that gives up is dropped when the solver shows its path cannot

be taken under the law's hypothesis, so `(=> (not (vector? x)) ...)`

proves even though the code's vector branch walks elements the prover

cannot see. An unknown answer (`vector?` of an opaque value, its `first`)

is the same each time it is asked of the same value.

- The usual reasons a law isn't proved: recursion that needs a lemma about

a helper (write the lemma), a law about a recursive fn stated over its

whole output where a pointwise statement would do, or a form outside

the prover (the report names it; restate the law if you can).

## Machines

`(machine name {:step f :start s :transitions {s {e s'}} :final [..]

:never [[a b]] :before [[a b]]})` states that `f` steps a state machine by

the table. Use it when the code's meaning is a table: screens, protocol

states, lifecycles. `f` is run on every state x event (from its `ann` when

those are data with field-less constructors, or `:states`/`:events`); an

unlisted pair must keep the state. The table must reach every state from

`:start`, reach a `:final` state from every state, never lead from `a` to

`b` (`:never`), and reach `b` only through `a` (`:before`).

- ``(f s e) is x, but the table says y`` - the code is wrong for that

pair; fix the code. If the table is what's wrong, say so.

- ``from s no final state can be reached``, ``a must never lead to b, but

it does: ...``, ``b must be reached only through a, but ... avoids it``

- the table breaks its own rules; that is the spec's owner's to fix.

- `(spec/mermaid 'my.spec {:machine 'name})` draws it.

## The call graph

Laws say what the code computes; `calls` says how it is put together.

Use it where the structure is part of the intent: a handler goes through

the layer that owns a rule (`respond` decides validity, so `handle` must

call `respond`, not `valid?`), a helper is reused rather than inlined, a

pure core never reaches an IO namespace. An implementation that inlines

or bypasses passes every law and still fails `calls`.

- Start from the code's actual graph: `(spec/call-graph 'my.ns)` returns

`{f #{g ...}}` for any namespace, effect code included. It reads the

source and checks nothing.

- `(spec/mermaid 'my.ns)` renders it as a mermaid flowchart;

`(spec/mermaid 'my.spec)` draws the target with the spec's `calls`

over it, marking unlisted calls `not in spec` and absent ones `missing`.

- The static rules use the graph whether or not a spec has `calls`:

definitions refer only to those above them, so there are no cycles but

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

input. It is not a set of examples (that is a test) and not a description

of the algorithm (that is the code).

- **Characterise the result.** For a sort: the output is ordered and is a

permutation of the input. Nothing else satisfies both.

- **Compare with a model.** Where a simple reference exists, say the code

agrees with it: `(= (to-list (build xs)) (sort (distinct xs)))`. The

model may be slow; it only runs in the check.

- **Relate operations.** Round trips (`decode` after `encode`), inverses

(`pop` after `push`), and exact effects (`insert` adds one `x`).

- **Keep invariants.** Say what every operation preserves.

- **Measure with the spec's own helpers.** Never use the implementation's

fns to judge its results. A law that checks the code with the code is

circular.

writ rejects a spec that does not do this:

- A law is `:vacuous`, and fails, when it calls no fn of the target or

when writ.norm proves it without the code. `(= (isort xs) (isort xs))`

and `(= (+ n 0) n)` are vacuous. Rewrite it to say what the code does.

- A **gap** is reported when every law holds but a trivial stand-in for a

signed public fn would also satisfy them all. The stand-ins are a

constant, an argument passed through, the real result reversed,

missing its first element, plus one, or swapped for another value of the

return type, and, when every law fixes an argument to literals, one that

agrees with the real fn on those literals and differs everywhere else.

The fix is a law that the

stand-in breaks, and that states intent: add `permutation` so that

"always returns ()" fails. Never special-case the stand-in in the code.

Rejecting every stand-in is necessary, not sufficient. Still ask whether

the laws say everything the problem statement says.

## The implementation

Plain Clojure, with no writ require and no annotations. writ rejects:

- Effects and interop: I/O, atoms and refs, futures, `eval`, `throw`,

`new`, `.method`, `reify`, static members such as `System/getenv` or

`Math/abs` (use `abs`), reflection.

- Top-level forms other than `ns`, `comment`, `def` and `defn`: no

`defmulti`, `defrecord`, `defmacro`, `declare` or bare expressions.

Each fn has one arity.

- A reference to a definition further down. There is no mutual recursion,

so put helpers first.

- Recursion that does not provably descend. Each recursive call or `recur`

must pass a strict part of one parameter, under a test on it:

- `(rest xs)` or `(next xs)` under `(seq xs)` or `(empty? xs)`, and only

on a collection typed finite, which the `ann` provides

- `(dec n)` under `(pos? n)`, or `(zero? n)` on a `Nat`; a chain

`(dec (dec n))` needs each depth guarded

- `(- n k)`, `k` a literal, under a comparison proving `n >= k`, such

as `(if (< n k) base (f (- n k)))`

- fields from destructuring or `first`/`nth` under a non-nil test,

including a `case` on `(first t)`

- a field of a field, `(rest (rest xs))` or a nested `match`, with each

read guarded at its own depth; a test on a deeper read guards the

reads above it

- `[:Tag f1 f2]` rebuilt from a matched field's own fields, each at its

own index, which is no larger than that field

A test inside `and` counts in the then branch, and each test of an `or`

is false in its else branch. Recursion with no structural measure

(`(quot n 62)`) takes a fuel parameter first: `(loop [fuel 11, n n] (if

(and (pos? fuel) (pos? n)) (recur (dec fuel) (quot n 62)) ...))`.

Parameters before the shrinking one pass through unchanged, so

accumulators go after it, in the parameters and in `loop` bindings.

`doseq` and `for` expand to such loops; their collection needs a type

too.

- Calls with the wrong arity, and calls to non-fns.

- Arguments that do not fit a callee's `ann`, or a body that does not fit

the fn's own return type.

### Data values

A spec data value is a vector headed by its constructor keyword. Build it

as a literal and take it apart with `case` on the tag:

```clojure

(defn insert [x t]

(case (first t)

:Leaf [:Node [:Leaf] x [:Leaf]]

:Node (let [[_ l v r] t]

(cond (< x v) [:Node (insert x l) v r]

(> x v) [:Node l v (insert x r)]

:else t))))

```

The `case` must list every constructor, or carry a default, and name no

others. A clause destructures only its constructor's fields. A literal

`[:Node ...]` carries exactly the declared fields, of fitting types. Read

the tag with `case (first t)` only: `first`, `second` or `nth` of a data

value anywhere else is rejected.

### Records

A map with keyword keys is a record type: `{:id Nat, :email String, :nick

(Opt String)}` is a map with those keys, each value of its key's type. An

`(Opt T)` key may be absent or nil; every other key must be there. Keys it

does not name may be there too. Name a record with a refinement, and

carve states out of it the same way:

```clojure

(refine Member [m {:id Nat, :email String, :points Nat, :nick (Opt String)}] true)

(refine Fresh [m Member] (zero? (:points m)))

```

The code builds and reads records as plain maps: literals, `(:k m)`, `get`,

`assoc`, `dissoc` and `{:keys [...]}` destructuring. The static check reads

them by key: a literal must carry every required key with a value of its

type, a read must name a key the record has, and an `(Opt T)` key read

may be nil, so it is not a `T`, default or not: `(:nick m "")` is nil when

the key holds nil; write `(or (:nick m) "")`. The prover works through

`get`, `assoc`, `dissoc` and `contains?` on literal keys, and symbolic

evaluation runs on records, so an edge over a record state is proved

never to throw.

## Running the check

```clojure

(require '[writ.spec :as spec])

(spec/check 'my.sort-spec) ; report map

(spec/check 'my.sort-spec {:seed 42}) ; replay a failure

(spec/check 'my.sort-spec {:target 'my.sort2}) ; same spec, other impl

(spec/check! 'my.sort-spec) ; throws with the message

(spec/sample '(List Nat) {} 5) ; what a type generates

(spec/scan 'my.ns) ; which fns a spec could cover

(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

(spec/obligations 'my.spec) ; every obligation, with ids, from the spec alone

(spec/check 'my.spec {:record "rec.edn"}) ; write a record of the check

(spec/attest "rec.edn" 'my.spec) ; how the spec got weaker since the record

```

`(spec my.sort)` defines `writ-check`, a clojure.test test that runs the

check, so the test runner checks the spec namespace with no wrapper

(a runner that picks namespaces by name must match `-spec` too).

`{:test {:seed 42}}` passes check options; `{:test false}` drops it.

By hand: `(let [r (spec/check 'my.sort-spec)] (is (:ok r) (:message r)))`.

`:max-size`, the largest generated size (default 50), and

`:adequacy false`, which skips the gap check while a spec is being drafted.

## Reading a report

`:static` fails first. A static failure is a single `Writ:` message, and no

law runs until it is fixed. After that, each law has a `:status`:

- `:vacuous`: true of any implementation; the spec must change.

- `:proved`: passed its tests, and the prover derived it from the code for

every input, and the proof checker replayed the derivation. `:proof`

says how; `:lemmas` names the other laws it cited. Proved laws are

lemmas for each other, in any order, so a spec whose laws build on each

other (`insert-keeps-sorted`, then `sorted`) gets more of them proved.

- `:evaluated`: a law with no quantifiers, run once.

- `:tested`: passed test.check's trials. This is evidence, not proof.

`:unproved` says why the prover did not prove it: a form outside its

model (`conj` onto a non-vector, `frequencies`, most string fns), the

proof checker rejecting the

proof (a writ bug; report it), or no proof found. That is not a failure.

A law written with modelled forms and the spec's own helpers is more

likely to be proved.

- `:witnessed`: an `exists` law, and a value was found.

- A failure "found by the solver, when no test did" is a real

counterexample: the solver found values that break the law, and running

the code on them confirmed it. Fix the code at those values.

- `graph `g`: ... ` lines: edges proved, 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`.

- `:unproved`: the spec (`(spec ns {:require :proved})`) or the law

(`{:require :proved}`) requires proof, and the law is only tested. Get

it proved: restate it with forms the prover models, or add the lemma it

needs as its own law. Only if it truly cannot be proved yet, mark the

law `{:require :tested :because "why"}`; the reason shows in every

report.

- `:failed`: see the message.

Each law also has `:evidence`, `:proof` (proved, evaluated, witnessed) or

`:test`, and the report's `:proof` counts them:

`{:require :tested :proved 6 :general 4 :tested 1 :laws 7}`. `:general`

is how many of the proved laws are `forall` laws, true for every input;

the rest hold on particular values (a closed law, an `exists` witness), and

the summary line says so: `6 of 7 laws proved (4 for every input, 2 on

particular values)`. A spec whose proofs are mostly particular values says

little beyond its examples, however many laws it proves.

A passing report lists, per signed fn, how many laws call it and how many

stand-ins of each kind they rejected:

`` `classify-read`: 5 laws, 3 impostors rejected (2 constant, 1 perturbed) ``.

Only constants rejected, or no fn laws at all, means the spec barely

touches that fn even though it passed.

```

law `permutation` fails for

x = 9

xs = [9 9]

(occurrences x (isort xs)) => 1

(occurrences x xs) => 2

(shrunk from {x 9, xs [0 6 13 ...]}, failing on test 20)

(replay with {:seed 42})

```

The counterexample is already shrunk. Work out why the implementation

gives the left-hand value for that input: here, a duplicate is dropped.

Each line under a predicate law shows what one argument evaluated to. A

vector in `xs` means the input was a vector: the code must accept any seq.

While laws run, the target's fns are instrumented, so a line like

`` `insert` returns (List Nat), but returned ... `` points at the fn that

produced a badly typed value. After a fix, rerun with the same `:seed` to

confirm it, then without one.

## Fixing rejections

### Spec and law failures

- ``law `x` is vacuous: it calls no fn of ns`` / ``writ.norm proves it

without looking at the implementation`` - the law is true of any code.

Restate it as a claim about what the target's fns return.

- ``the spec does not pin down `f`: every law still holds when it ...`` -

the named stand-in satisfies the spec. Add a law about `f`'s meaning

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, 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.

- ``law `x` fails for ...`` - the implementation is wrong for that input;

see [Reading a report](#reading-a-report).

- ``the hypothesis never held in N trials`` - no generated input satisfied

- ``no witness among N generated values`` - the `exists` law found no

value. Either the implementation is wrong, or the witness is too rare to

generate.

- ``cannot generate values of type `T` `` - the law quantifies over a

function type or an undeclared name.

- ``the spec gives `f` a signature, but `ns` defines no fn `f` `` - define

`f`, or check its spelling. The spec names the API.

- ``` `ann f` gives N parameter type(s) but `f` takes M ``` - match the

signature. The spec is the contract.

- ``` `f` is multi-arity; `ann` gives a single signature ``` - write one

arity.

- ``` `f` argument N (x) expects T, got v ``` / ``` `f` returns T, but

returned v ``` - an instrumented call saw a value outside the signature.

- ``cannot find the source of `ns` on the classpath`` - the target file is

not under a source path.

- ``is not a spec namespace`` - the namespace has no `(spec target)` form.

- ``graph `g` breaks on its runs`` - a run from the start, through the

real fns, left the graph, broke an invariant, or never reached a final

state. The path and seed replay it. Fix the code at that value; if no

run reaches a final state only because runs are short, raise `:depth`.

- ``invariant `g :s` is vacuous`` - the state's refinement already says

it; state what a landing must keep that the type does not.

- ``law `g:s:f:refused` fails`` - where the guard fails, the code changed

the state; a refused step must leave it as it was (or go to `:else`).

- ``the guard of f from s never holds`` / ``clause ... never fails on its

own`` - the guard is wrong or has a clause that says nothing; that is

the spec's owner's to fix.

- ``the spec is not finished: open question `q` blocks ...`` - ask the

spec's owner; write the answer in as laws or states, then remove the

question.

- ``laws `a` and `b` cannot both hold`` - no code satisfies both; the

solver shows it. Do not change the code: ask which law is meant.

- ``writ bug: law `x` was proved (...) but a test refutes it`` - the

prover is wrong, not your code. Report it with the seed, and rerun with

`{:prove false}` meanwhile.

### Tagged data

- ``the `case` on `t` (Tree) does not handle :Leaf`` - add the clause, or a

default.

- ``:Nod is not a constructor of Tree (Leaf, Node)`` - fix the keyword.

- ``Node takes 3 field(s) but is built with 2`` - build `[:Node l v r]`.

- ``field N of Node expects T but is given U`` - that field has the wrong

value. Check the field order in the `data` declaration.

- ``field N of C expects a, which field M made T, but is given U`` - a type

parameter was given two different types.

- ``Node has 3 field(s), but `t` is read at position 4`` - destructure at

most the tag plus the fields.

- ``has data type Tree; take it apart with `(case (first t) ...)` `` - read

a data value only through a `case` on its tag.

### Records

- ``` `m` is a record with keys :email, :id, and has no key :point``` -

a misspelt key, or one the type should name. Add it to the record, as

`(Opt T)` if it may be absent.

- ``returns {...} but its body has type {...}: the body leaves out :points``

- build the map with every key the record requires.

- ``:points is Nat, but the body gives String`` - that key's value has the

wrong type.

- ``returns String but its body has type (Opt String): it may be nil`` -

an optional key was read, and it may hold nil even with a default.

Write `(or (:nick m) "")`, or branch on it.

### Structural rules (plain and annotated code)

- ``` `declare`/`defonce`/`defmulti`/`defrecord`/... is not supported in a book ``` -

a book checks def, defn, data, law and proof forms only; rewrite the value

as a plain def or defn.

- ``` `require`/`println`/... is not supported in a book ``` - unknown

top-level forms are rejected, not skipped: a name used only there would

escape the ordering rule. Only `ns`, `comment`, `def`, `defn`, `data`,

`law` and `proof` belong at book top level.

- ``` `def` inside a body is not supported ``` - a book defines names at the

top level only, in book order; hoist the definition.

- ``` duplicate case test constant ``` - a constant may match in only one

clause (or one group); Clojure rejects duplicates at compile time, and a

book is never compiled, so writ checks it.

- ``` `.` / `.foo` is host interop or effect code ``` - pure

data-and-functions code only; rewrite without interop.

- ``` `set!` mutates a var ``` - writ checks pure code. Rewrite without

mutation.

- ``` `recur` in `f` must be in tail position ``` - recur only compiles in

tail position; move it to the tail or use a named self-call.

- ``` `recur` in `f` rebinds N value(s) but is passed M ``` - the frame

contract, checked before quantities and the descend marking, so a

wrong-arity recur is never masked by an affinity error. recur rebinds

exactly its frame: the loop's slots or the defn's parameters. Match the count.

- ``` `throw`/`new`/`.foo` is host interop or effect code ``` - writ checks

pure data-and-functions code only; no host calls, no mutation, no effects.

- ``` duplicate parameter in `f` ``` - parameters are binders: rename one, or

use `_` for a parameter you ignore (it may repeat).

- ``` def `x` must carry a value ``` - a book is never evaluated, so a def

without a value would smuggle an unbound name into scope; write `(def x nil)`

if you mean nil.

- ``` case test must be a compile-time constant ``` - quote the symbol

(`(quote foo)`) to compare against it; bare symbols read like binders but

are constants.

- ``` `Just`/`MaybeInt` is declared more than once ``` - a data type and its

constructors are book-level names and may not collide with a def or defn.

- ``` `map` is used in `f` but is defined later ``` - the book defines its own

`map`, so the core one no longer resolves: move the definition earlier or

rename it.

- ``` `recur` in `f` cannot cross a `try` ``` - move the `loop` inside the

`try`; recur compiles only inside the try's own loop.

- ``` a rest parameter must be followed by exactly one rest name ``` - `[x &]`,

`[& a b]` and `[& &]` are malformed; write `[x & xs]`.

- ``` `f` takes 2 argument(s) but is passed 1 ``` - a book is never evaluated,

so writ checks call arity itself; match the fn's (or constructor's) fixed

arity, or its variadic minimum.

- ``` `f` takes at least 1 argument(s) but is passed 0 ``` - a variadic fn

still requires its fixed parameters.

- ``` a keyword or set is called with no arguments ``` - the collection to

read is missing; write `(:k m)` (a default is optional).

- ``` `a` and `b` are mutually recursive ``` - Bend's defs reference earlier

names only, so no descent can be checked across a cycle of local fns;

break the cycle or make each side self-recursive with descent.

- ``` a catch clause must be `(catch Class binder body*)` ``` - the catch

clause needs a class symbol, a simple binder symbol and a body; a

destructuring binder like `[x]` is not accepted.

- ``` the `finally` clause must be last in a `try` ``` - nothing may follow

finally; catch clauses come before it.

- ``` only catch or finally clauses can follow a catch in a `try` ``` - a

plain body form after a catch is not valid try syntax.

- ``` a `letfn` spec must be `(name [params] body*)` ``` - each spec needs a

name, a params vector, and its body; ``` `letfn` requires a vector of fn

specs ``` - the specs form itself must be a vector.

- ``` Wrong number of args to if, had: N ``` - `if` takes exactly a test,

a then, and optionally an else; a fourth branch is not extra data.

- ``` Wrong number of args to var, had: N ``` / ``` The argument to `var`

must be a symbol ``` - `var` takes exactly one symbol.

- ``` Bad binding form: `x` ``` - a binder (parameter, let/loop local,

catch binder, letfn name) must be a simple symbol: no namespace, no

dots.

- ``` First argument to def must be a symbol ``` / ``` Cannot def

namespace qualified symbol ``` / ``` Too many arguments to def ``` - a

def carries a name, an optional docstring, and one value.

- ``` requires a vector of parameters ``` - write `[x y]`, not `x` or

`(x y)`; a list of arity vectors is the multi-arity error instead.

- ``` `g` takes 2 argument(s) but is passed 1 ``` / ``` takes at least 1

argument(s) ``` - a call to a local fn (letfn, let-bound, anonymous)

does not match its parameter vector; the same rule the book-fn arity

gate enforces.

- ``` an anonymous fn takes 2 argument(s) but is passed 1 ``` - the fn

literal in call position; give it its arguments.

- ``` `let` requires a vector for its bindings ``` / ``` `loop` requires

a vector for its bindings ``` - write `(let [x 1] ...)`, not a bare

form.

- ``` `case` requires at least one clause or a default ``` / ``` Wrong

number of args to case, had: 0 ``` - a case with nothing to match can

only ever throw.

- ``` First argument to defn must be a symbol ``` / ``` Cannot defn

namespace qualified symbol ``` - a book is one namespace; defn names

follow the same rules as def names.

- ``` a collection or symbol is called with no arguments ``` - a vector,

map, set or quoted symbol is a lookup fn; give it the collection to

read. ``` a lookup call ... takes at most the collection and a

default ``` - two arguments is the maximum.

- ``` Unsupported special form: unquote ``` / ``` Unsupported special

form: unquote-splicing ``` - an unquote that survives reading is always

an error (syntax-quote consumes the legal ones at read time; the host

throws the same message).

- ``` def `x` reads itself through a call in its own value ``` - the

name is unbound during its own init, so using it as a call argument

throws at load on the host. Unforced storage (`(def v [1 v])`) is

legal, and a self-reference inside a fn body is recursion.

- ``` a type parameter in `P` must be a simple symbol ``` - `(data P

[a] ...)` binds type parameters; like any binder they are simple

symbols, so [1 2], [foo/bar] and [a.b] are rejected.

- ``` Wrong number of args to quote, had: N ``` - quote takes exactly

one form; jolt evaluates (quote a b) without complaint but the JVM

compiler rejects it, so writ enforces the JVM contract.

- ``` cond requires an even number of forms ``` - cond (and cond-> /

cond->>) takes test/expr pairs; a dangling test with no expr is a

shape error.

- ``` `1` in `f` is not a function ``` - numbers, strings, characters,

booleans and nil can never be called.

- ``` `x` in `g` is not a function; a constant defined in this book

cannot be called ``` - a def bound to a constant (a number, string,

docstring-as-value, nil, collection, or a quoted fn form) is not

callable at any arity. Wrap

the fn in an actual fn value, or call something else.

- ``` `get` takes between 2 and 3 argument(s) but is passed 1 ``` /

``` `map` takes at least 1 argument(s) but is passed 0 ``` - the call

does not match any arity of the clojure.core fn; the table comes from

core's own :arglists, and a book def of the same name wins over it.

- ``does not descend: no argument is a structurally smaller part of its own

parameter`` - recurse on a part destructured from that parameter, or on

`dec`/`rest`/`next` of it. A computed value, the bare parameter, or a part

of a DIFFERENT parameter does not count.

- ``shrinks `x` without a guard`` - test the column first: `(if (zero? x) ..)`

on a Nat, `(pos? x)`, `(seq xs)`, `(empty? xs)`, or a truthiness test.

``must be a finite collection`` means `x` has no finite type: sign the fn

with `ann` in the spec.

- ``refers to itself as a value`` - a self-reference must be a call head.

- ``argument N before the shrinking one must be passed unchanged; put `xs`

first in the parameters`` (or ``the `loop` bindings``) - do what it says:

the accumulator rides after the shrinking one.

- ``a macro's loop in `f`, such as a `doseq`, does not descend`` - the loop

is the macro's, not yours; the message names the collection it walks.

Usually that collection needs a finite type from `ann`.

- ``is not supported: in the code a spec covers, writ checks def and defn

forms only`` - `defrecord`, `defmacro`, `defmulti` and the like cannot sit

in the target; `scan` lists them. Move them out, or leave that namespace

unspecified.

- ``takes N type argument(s), got M`` - fix the type's arity.

- ``expects T for argument N but is passed U`` / ``returns T but its body has

type U`` / ``has type T, which is not a function`` - the code disagrees

with the types in its `ann` (or annotation). Fix the code, not the `ann`.

- ``is defined later or is not a known name`` - move the def earlier, or

qualify the name.

### Annotated surface only (writ.defn)

These come from `w/defn`, `w/match`, `w/law` and `w/proof`, which the

example books use.

- `` `f` is recursive: mark it ^{:writ/descend true} `` - add the attr map, or

rewrite without recursion.

- ``` a match arm must be `(pattern result)` ``` - each arm is exactly

a pattern and its result; a bare symbol, a 1-element or 3-element arm

is a shape error, as is a `match` with no arms at all.

- ``` `:-` in `f` must be followed by a return type ``` / ``` `:-` in `f`

must be followed by a type ``` - a dangling annotation arrow; the type

after `:-` is missing, so the annotation would silently vanish.

- ``is used more than once but is declared affine`` - add `^:many` to that

binder. It may be a parameter, a local, or a pattern binder.

- ``is used once but is declared erased`` - drop `^:zero`, or stop using the

binder.

- ``is used once but is declared erased`` on a `^:zero` local's init or an

argument to a `^:zero` param - Clojure evaluates dead code, so those uses

count (Bend erases them; writ cannot).

- ``shadows a parameter`` / ``duplicate binder`` - rename the local.

- ``the scrutinee of a `match` must be a parameter or a pattern binder`` -

match a bound name, not the computed value.

- ``is reusable (^:many) but its type is not Data`` - drop `^:many`, or

instantiate the type at Data arguments.

- ``is reusable (^:many) but has no type`` / ``no type writ can infer`` -

annotate the binder with a Data type (`:- Nat`, `^Nat`).

- ``is captured by a fn passed to `map`, which may be called more than once``

- mark the captured binder `^:many`, or pass it as an argument.

- ``destructured into overlapping binders`` - read each key once, or make the

source `^:many`.

- ``law `x` is not filled: no proof discharges it`` - add the proof.

- ``discharges no law`` - the proof names a law that is not declared.

- ``re-proves law`` - delete the duplicate proof, a law is discharged once.

- ``cites law `x` before it is proved`` - move that proof after `x`'s own

proof.

- ``duplicate law name`` - rename one of them.

## The annotated surface

`writ.defn` puts the annotations in the code and adds Bend's full

discipline on top of the rules above. Its `w/law` forms need a `w/proof`

gate that proves only identities, like `(= (status req s) (status req s))`;

a spec namespace rejects those as vacuous. Don't copy them into a spec.

- `(w/defn f [a :- Nat, ^:many b :- Nat] :- Nat body)`: `:-` gives types.

An unmarked binder is affine: used at most once, with zero allowed.

`^:many` makes it reusable, which requires a Data type. `^:zero` makes it

erased, never used. Quantities cover every binder, locals and pattern

binders included. Branches join, and sequential uses add.

- Recursion needs `^{:writ/descend true}` on the defn.

- Type variables go in the attr-map: `{:writ/forall [a, b :- Data]}`.

- `w/data` values are `:Nil` or `[:Cons h t]`, and only `w/match` takes

them apart. It is exhaustive; a trailing lowercase arm catches the rest.

The scrutinee must be a parameter or pattern binder. It also matches

`Nat`, `Bool` and `(List T)`.

- Every `(w/law name prop)` needs exactly one `(w/proof name law term)`.

The terms are `refl`, `(pair ..)`, `(fn [x] ..)` and `(witness t pf)`.

`refl` needs both sides convertible under writ.norm, which has no

induction and does not unfold your own fns. It can only prove identities;

checking behaviour is what writ.spec is for.

## In this repo

```sh

rm -rf ~/.jolt/aot-cache .jolt # the AOT cache can serve stale namespaces

jolt -M:test # engine suite

cd examples && jolt -M:test # the example programs and their specs

```

When a test run disagrees with a direct `jolt -e` of the same code, clear the

AOT cache before debugging. That is a known jolt issue, not a writ bug.

`test/writ/spec_demo/` holds worked specs, a sort and a tree, each with

broken implementations and the reports they produce. `examples/` has four

programs on real libraries (raylib pong and life, a ring-chez URL

shortener, an http-client fetcher), each a pure core, a spec, an effect

shell and broken cores; its README walks through what each report says.

Model a new spec on those.

## Source map

- `writ.spec` spec namespaces, law checking with test.check, instrument

- `writ.prove` proofs of laws from the code: `.term` the value model,

`.rewrite` the rules (checked against the runtime), `.translate` Clojure

to terms

- `writ.book` runs every rule over a namespace's forms

- `writ.check` quantities, termination, ordering, effects, arity

- `writ.types` types and tagged data, `writ.kind` well-kindedness

- `writ.lower` the AST, `writ.uses` occurrence analysis

- `writ.match` `w/match`, `writ.norm` conversion behind `refl`,

`writ.law` propositions and the proof gate

- `writ.defn` the annotated macros, `writ.core` its entry points