MCP: an assistant can author models with no docs pasted in

CHANGELOG.md

@@ -3,6 +3,48 @@
 Versions follow `dune-project`: what opam publishes, `writ --version` prints and
 `make release` names the tarball with.
 
+## Unreleased
+
+**An assistant can author models through MCP with no documentation pasted
+in.** `writ-mcp` now teaches the language and accepts what an assistant
+writes:
+
+- every file argument also takes inline text (`model_source`,
+  `claims_source`, `rules_source`, `old_model_source`, `new_model_source`), so a
+  client that cannot write to the server's disk can author; `model_name` keeps
+  revision history per inline model;
+- `writ_guide` serves the language by topic (syntax, semantics, idioms, five
+  worked examples, every error code), also as `writ://guide/<topic>` resources
+  and a `writ_model_system` prompt; the server sets `instructions`, and
+  `writ_check`'s description carries a complete example;
+- `writ_validate` parses and type-checks without building the space and
+  summarises what the sources declare, including the most situations they
+  allow;
+- every error carries a code (`E_UNKNOWN_ARROW`, `E_STATE_LIMIT`, …), position,
+  found and expected names, a hint, and, for a misspelt name, the corrected
+  line;
+- `max_situations` and `timeout_ms` bound a search, and a cut-off search says
+  how far it got and which cells drove the growth, and decides nothing.
+
+**Breaking:** a transition with a clause other than `when` and `do` is now an
+error: a bare `(set …)` outside `(do …)` used to be dropped silently, leaving a
+move that changed nothing. No model in writ, writ-problems, writ-arch or
+writ-scheduling-verification has one.
+
+**A failing `inevitable` says how a run avoids the goal.** Under the witness,
+`avoids: the run stops at #N` when no move is left, or `loop:` a shortest cycle
+back to the stuck situation; under `(fair …)`, `loops among:` the situations a
+fair run circles in. Prose only: `--json` and certificates are unchanged.
+
+**Long dead-end lists are readable.** A route over 24 moves keeps its first and
+last ten and counts the rest; past 20 dead ends the report says how many more.
+
+**`certified` no longer reads as if n/a claims were checked.** When every
+property is `n/a` and no query was asked, the last line is `certified: the
+situation count only — every property is n/a, so no claim was checked`, in
+`writ check` and `writ_check` alike. The `certification` JSON field is
+unchanged.
+
 ## 0.4.0 — 2026-10-03
 
 **Upgrading:** `writ check` now exits 1 when a property is `n/a`. A pipeline

core/syntax/parser.ml

@@ -86,6 +86,22 @@ let decode_transition ?(origin : Reader.t -> string option = fun _ -> None)
             | _ -> None)
           clauses
       in
+      (* Anything else was silently dropped, so a bare (set …) outside (do …)
+         made a move that changes nothing. *)
+      let* () =
+        match
+          List.find_opt
+            (function
+              | Reader.List (Reader.Atom (("when" | "do"), _) :: _, _) -> false
+              | _ -> true)
+            clauses
+        with
+        | Some c ->
+            Reader.err_at c
+              "unknown transition clause: a transition is (transition [NAME] \
+               (when GUARD) (do EFFECT…)), and effects go inside (do …)"
+        | None -> Ok ()
+      in
       let* gdatum =
         match occurrences "when" with
         | [ ([ g ], _) ] -> Ok g

docs/certificates.md

@@ -15,8 +15,9 @@ certified: every answer re-derived from the model (writ-cert)
 `writ-cert` is looked for in `$WRIT_CERT`, then beside the `writ` executable,
 then on the `PATH`; if missing, the line reads `not certified: writ-cert is not
 installed`. If it refutes the report, the line is `NOT CERTIFIED`, the refuted
-answers follow, and the exit status is 1. With `--json` the result is the
-`certification` field.
+answers follow, and the exit status is 1. When every property is `n/a` and
+there is no query, only the situation count was re-derived, and the line says
+so. With `--json` the result is the `certification` field.
 
 Run by hand, `writ-cert` prints a line-by-line account:
 

docs/interrogator.md

@@ -117,7 +117,7 @@ rule's, so `(holds S (is X.a Y))` finds where a mutable arrow points in S.
 
 ```lisp
 (relation can-reach 1)
-(rule (can-reach S) (holds S F))            ; the goal set itself
+(rule (can-reach S) (situation S) (holds S F))   ; the goal set itself
 (rule (can-reach S) (edge E S T) (can-reach T))   ; and a move into it
 ```
 

docs/kernel-spec.md

@@ -1488,6 +1488,12 @@ forms.
   vacant side). A `stuck at:` line leads with that same index. One numbering
   runs through the whole tool, so a witness can be followed with `writ show
   --at N` without counting.
+- A failing **`inevitable`** also says how a run avoids F from the stuck
+  situation: `avoids: the run stops at #N` when no move is left, or `loop:` a
+  shortest cycle back to it, every situation on it outside F. Under
+  `(fair …)` a single cycle could starve a fair move, so the line is `loops
+  among:` the situations a fair run circles in. The prose report carries this;
+  `--json` does not.
 - A holding **`possible`** also carries a witness: the shortest route to a
   satisfying situation — the example the question asked for (Appendix C's
   solvable river prints its crossing). The other three hold with no single

docs/mcp.md

@@ -94,18 +94,73 @@ assistant's to change; the questions stay yours.
 Describe the system and the question in plain words, and say you want it
 checked with writ. The assistant writes the model and claims, calls the tools,
 and revises the model until your questions hold — or shows you why they cannot.
+It needs no Writ documentation from you: the server teaches the language itself
+(below).
 
 | Tool | Arguments | Answers |
 |---|---|---|
+| `writ_guide` | `items` | the language, by topic: syntax, semantics, idioms, worked examples, every error code |
+| `writ_validate` | `model`, `claims`, `rules` | parse and type-check only, instantly; what the sources declare, or coded errors |
 | `writ_check` | `model`, `claims` | every property `holds` / `fails` with a route; laws, gaps, dead ends; what the edit **LOST**; `certified` |
 | `writ_show` | `model`, `at` | what a situation is — the one a witness names by `#N` |
-| `writ_compare` | `old_model`, `new_model` | which guarantees an edit kept, lost and gained |
-| `writ_query` | `model`, `name`, `at` | a named query's matching rows |
+| `writ_compare` | `old_model`, `new_model`, `claims` | which guarantees an edit kept, lost and gained |
+| `writ_query` | `model`, `claims`, `name`, `at` | a named query's matching rows |
 | `writ_derive` | `model`, `rules`, `relation`, `why` | a relation from a `.rules` file, or its derivation tree |
 
+Every file argument is a path **or** inline text: `model_source`,
+`claims_source`, `rules_source` (and `old_model_source`, `new_model_source`),
+at most 256 KB each, so an assistant in a chat app that cannot write to your
+disk can still author. Give inline models a `model_name` to keep revision
+history per name (for as long as the server runs); errors cite the source
+as `inline:NAME.writ`, a name no `(load …)` can reach. An inline model's own
+`(load …)` is looked up as a path model's is: the server's working directory
+first, then the library path. Under
+`--claims-dir`, inline claims are refused.
+
 Every tool takes `json: true` for the same answer as one JSON object
 ([json.md](json.md)).
 
+### How an assistant learns the language
+
+- **`instructions`** on initialize: what writ is, the workflow
+  (`writ_validate` → `writ_check` → `writ_show` → `writ_compare`), and that
+  `n/a` is a failure. Some clients drop these, so nothing depends on them.
+- **`writ_guide`**: topics `index`, `syntax.model`, `syntax.claims`,
+  `syntax.rules`, `semantics`, `idioms`, five worked examples
+  (`examples.mutex`, `.webhooks`, `.consumer`, `.commit`, `.handoff`, each
+  with the failing check, the fix and the compare), and `errors.<code>`. The
+  same topics are MCP resources, `writ://guide/<topic>`, and the prompt
+  `writ_model_system` walks a description through the workflow. The topics
+  live in `tooling/mcp/guide/` and are compiled into the server; a test re-runs
+  every example and fails if its output drifts.
+- **`writ_check`'s description** carries one complete model and claims, so a
+  client sees working syntax before it calls anything.
+
+### Errors and limits
+
+A failed call answers with one block per file in error:
+
+```
+error E_UNKNOWN_VALUE in model at inline:shop.writ:8:60
+  value runing not in codomain stage-t
+  found:    runing
+  expected: one of running, done, queued
+  hint:     Write `running` for `runing`. Use a value of the arrow's codomain type.
+  fix:      (transition go (when (is a.stage queued)) (do (set a.stage running)))
+  see:      writ_guide errors.E_UNKNOWN_VALUE
+```
+
+With `json: true` the same fields come as objects. `fix` is the corrected line
+when the mistake is a misspelt name. A misspelt name in claims, which `writ_check`
+would answer `n/a`, is an error in `writ_validate`, and `writ_check` adds a
+`why n/a` line naming it.
+
+The search stops at `max_situations` (default 200 000, at most 2 000 000) or
+`timeout_ms` of CPU time (default 60 000, at most 600 000). Then the answer is
+`E_STATE_LIMIT`: how many situations were explored, the bound (the product of
+every mutable cell's domain), each property marked undecided, and the cells
+that took the most values, the ones to shrink.
+
 Read a reply's last lines first. `NOT CERTIFIED` means writ itself got
 something wrong — report it rather than work around it. A `LOST` guarantee or
 an `n/a` property is a failure, even when everything else holds.

plugins/writ/skills/writ/SKILL.md

@@ -96,6 +96,11 @@ Time is a ladder of named ticks walked by an arrow, never a number.
 - **`writ_derive`** — a relation from a `.rules` file; `why: true` returns the
   derivation tree down to the model facts it rests on.
 - Every tool takes `json: true` to answer as the object `writ … --json` prints.
+- **Newer servers** also list `writ_guide` (the language by topic, with worked
+  examples and every error code) and `writ_validate` (parse and type-check,
+  instantly). When `writ_guide` is listed, read its `index` before writing a
+  model; when `writ_validate` is listed, run it before `writ_check`. Every file
+  argument then also takes inline text (`model_source`, `claims_source`).
 
 An index (`#17`, or a rules row's `17`) is not an answer: one numbering runs
 through the whole tool, so follow it with `writ_show` and quote the situation,

runtime/report.ml

@@ -35,16 +35,40 @@ let gaps (sp : Space.t) : string =
       in
       String.concat "\n" (head :: List.map line gs)
 
+(* A long route keeps its ends: the start says how it began, the end what
+   led into the dead end; the middle is counted, not printed. *)
+let route_cap = 24
+
+let elide (r : string list) : string =
+  let n = List.length r in
+  if n <= route_cap then String.concat ", " r
+  else
+    let keep = (route_cap / 2) - 2 in
+    String.concat ", " (List.filteri (fun i _ -> i < keep) r)
+    ^ ", … "
+    ^ string_of_int (n - (2 * keep))
+    ^ " more moves …, "
+    ^ String.concat ", " (List.filteri (fun i _ -> i >= n - keep) r)
+
+(* So many dead ends are a pattern, not a list to read. *)
+let dead_end_cap = 20
+
 let dead_ends (sp : Space.t) : string =
   match Space.dead_ends sp with
   | [] -> "dead ends: none"
   | des ->
-      let head = "dead ends: " ^ string_of_int (List.length des) in
+      let n = List.length des in
+      let head = "dead ends: " ^ string_of_int n in
       let line (_, route) =
-        "  reached by: "
-        ^ match route with [] -> "(initial)" | r -> String.concat ", " r
+        "  reached by: " ^ match route with [] -> "(initial)" | r -> elide r
       in
-      String.concat "\n" (head :: List.map line des)
+      let shown = List.filteri (fun i _ -> i < dead_end_cap) des in
+      String.concat "\n"
+        ((head :: List.map line shown)
+        @
+        if n > dead_end_cap then
+          [ "  … and " ^ string_of_int (n - dead_end_cap) ^ " more" ]
+        else [])
 
 (* Inline numbered route: [1. m1 2. m2 …] on one line. *)
 let inline_route (route : string list) : string =
@@ -112,6 +136,46 @@ let cells_line (sp : Space.t) (s : State.t) : string =
   in
   "(" ^ String.concat " " (Array.to_list (Array.mapi cell cells)) ^ ")"
 
+(* How a run from a failing [inevitable]'s stuck situation avoids F for ever:
+   it stops there, or it loops. Without fairness the loop is a concrete
+   shortest cycle; with it, a cycle may starve a fair move, so the honest
+   answer is the region a fair run circles in. *)
+let avoids (sp : Space.t) (prop : Claims.property) (fair : string list)
+    (s : State.t) : string option =
+  match State.M.find_opt s sp.Space.index with
+  | None -> None
+  | Some i -> (
+      let ctx = sp.Space.ctx in
+      let sat st = Eval.guard_holds ctx st [] prop.formula in
+      let a = Space.avoidance ~fair sp sat in
+      let idx = "#" ^ string_of_int i in
+      if a.Space.stopped.(i) then
+        Some ("  avoids:   the run stops at " ^ idx ^ ": no move is left")
+      else
+        match Space.avoid_loop a sp i with
+        | None -> None
+        | Some (members, loop) ->
+            if fair = [] then
+              Some
+                ("  loop:     "
+                ^ String.concat "   "
+                    (List.mapi
+                       (fun k (via, d) ->
+                         string_of_int (k + 1)
+                         ^ ". " ^ via ^ " → #" ^ string_of_int d)
+                       loop)
+                ^ "   (and again, for ever)")
+            else
+              let n = List.length members in
+              let shown = List.filteri (fun k _ -> k < 12) members in
+              Some
+                ("  loops among: "
+                ^ String.concat " "
+                    (List.map (fun j -> "#" ^ string_of_int j) shown)
+                ^ (if n > 12 then " … (" ^ string_of_int n ^ " situations)"
+                   else "")
+                ^ ", taking every fair move offered there"))
+
 (* The index leads so `writ show --at N` can be run on it directly. *)
 let stuck_line (sp : Space.t) (s : State.t) : string =
   let idx =
@@ -263,6 +327,12 @@ let outcome ?(queries : Claims.query list = []) (sp : Space.t)
       (match route with
       | [] -> ()
       | _ -> parts := witness_block sp route :: !parts);
+      (match (prop.modality, stuck) with
+      | Claims.Inevitable fair, Some s -> (
+          match avoids sp prop fair s with
+          | Some l -> parts := l :: !parts
+          | None -> ())
+      | _ -> ());
       String.concat "\n" (List.rev !parts @ shown)
 
 (* --- §17 fibers ------------------------------------------------------------ *)