From 76481d8b29500a87c3de729f2d0bf0d4463038d9 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 21:41:46 +0300 Subject: [PATCH 1/3] mcp: an assistant can author models with no docs pasted in MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The MCP server could run a model someone else wrote but not teach a client to write one: tools took only paths (a chat client cannot write to the server's disk), no instructions were set, and errors were prose. This implements the feature request in mcp_advanced.md, R1-R8: - inline sources beside every path argument, served as `inline:NAME.writ`, a name no (load …) can reach, so pinned claims stay pinned; model_name keeps revision history per inline model; claims_source is refused under --claims-dir; - writ_guide: index, syntax.model/claims/rules, semantics, idioms, five worked examples (failing check, fix, compare) and one topic per error code, as markdown in tooling/mcp/guide embedded at build time; also writ://guide resources and a writ_model_system prompt; server instructions; a complete example in writ_check's description; - writ_validate: parse and type-check without building the space, with a summary and the situation bound; a misspelt name in claims, which check would answer n/a, is an error here, and check adds a `why n/a` line; - coded errors (code, position, found, expected, hint, corrected line, guide pointer), as prose or JSON; - max_situations / timeout_ms, and a cut-off search that reports how far it got and which cells grew, deciding nothing; - writ_compare names properties still failing in both models. Breaking: a transition clause other than when/do is an error; a bare (set …) outside (do …) was silently dropped. No model in the writ repositories has one. test_mcp_authoring re-runs every guide example against its printed output and every error code's wrong and right example. A cold-start agent given only the tools passed the request's six acceptance scenarios; its findings and a code review are folded in. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 28 + core/syntax/parser.ml | 16 + docs/interrogator.md | 2 +- docs/mcp.md | 57 +- runtime/space.ml | 81 +- tests/unit/dune | 9 + tests/unit/test_mcp_authoring.ml | 902 ++++++++++++++++++++ tooling/mcp/gen/dune | 4 + tooling/mcp/gen/embed.ml | 27 + tooling/mcp/guide/examples.commit.md | 126 +++ tooling/mcp/guide/examples.consumer.md | 132 +++ tooling/mcp/guide/examples.handoff.md | 146 ++++ tooling/mcp/guide/examples.mutex.md | 96 +++ tooling/mcp/guide/examples.webhooks.md | 128 +++ tooling/mcp/guide/idioms.md | 84 ++ tooling/mcp/guide/index.md | 40 + tooling/mcp/guide/semantics.md | 74 ++ tooling/mcp/guide/syntax.claims.md | 65 ++ tooling/mcp/guide/syntax.model.md | 99 +++ tooling/mcp/guide/syntax.rules.md | 59 ++ tooling/mcp/lib/diagnose.ml | 1081 ++++++++++++++++++++++++ tooling/mcp/lib/dune | 11 + tooling/mcp/lib/fault.ml | 48 ++ tooling/mcp/lib/guide.ml | 93 ++ tooling/mcp/lib/server.ml | 687 ++++++++++++--- tooling/mcp/lib/tools.ml | 645 ++++++++++++-- 26 files changed, 4554 insertions(+), 186 deletions(-) create mode 100644 tests/unit/test_mcp_authoring.ml create mode 100644 tooling/mcp/gen/dune create mode 100644 tooling/mcp/gen/embed.ml create mode 100644 tooling/mcp/guide/examples.commit.md create mode 100644 tooling/mcp/guide/examples.consumer.md create mode 100644 tooling/mcp/guide/examples.handoff.md create mode 100644 tooling/mcp/guide/examples.mutex.md create mode 100644 tooling/mcp/guide/examples.webhooks.md create mode 100644 tooling/mcp/guide/idioms.md create mode 100644 tooling/mcp/guide/index.md create mode 100644 tooling/mcp/guide/semantics.md create mode 100644 tooling/mcp/guide/syntax.claims.md create mode 100644 tooling/mcp/guide/syntax.model.md create mode 100644 tooling/mcp/guide/syntax.rules.md create mode 100644 tooling/mcp/lib/diagnose.ml create mode 100644 tooling/mcp/lib/fault.ml create mode 100644 tooling/mcp/lib/guide.ml diff --git a/CHANGELOG.md b/CHANGELOG.md index deb7e6d..1a3d1dd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3,6 +3,34 @@ 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/` 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. + ## 0.4.0 — 2026-10-03 **Upgrading:** `writ check` now exits 1 when a property is `n/a`. A pipeline diff --git a/core/syntax/parser.ml b/core/syntax/parser.ml index fedffca..ba9b13b 100644 --- a/core/syntax/parser.ml +++ b/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 diff --git a/docs/interrogator.md b/docs/interrogator.md index 82a7c6a..94625ee 100644 --- a/docs/interrogator.md +++ b/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 ``` diff --git a/docs/mcp.md b/docs/mcp.md index f1ef712..8c6f85e 100644 --- a/docs/mcp.md +++ b/docs/mcp.md @@ -94,18 +94,71 @@ 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. 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.`. The + same topics are MCP resources, `writ://guide/`, 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. diff --git a/runtime/space.ml b/runtime/space.ml index c3a83ee..b811191 100644 --- a/runtime/space.ml +++ b/runtime/space.ml @@ -25,12 +25,48 @@ type t = { let cap = 200_000 +(* Why a bounded search stopped short: how far it got, and, per mutable cell, + how many distinct values it had seen, most first, the cells driving the + growth. *) +type cutoff = { + reason : [ `Cap of int | `Timeout of float ]; + explored : int; + edges_seen : int; + spread : (string * int * int) list; (* cell, values seen, domain size *) +} + +(* The most situations the mutable cells allow: the product of their domains. + A float, since it overflows an int long before it is interesting. *) +let bound (lay : State.layout) : float = + Array.fold_left + (fun acc d -> acc *. float_of_int (max 1 (Array.length d))) + 1.0 lay.State.domains + +let show_bound f = + if f < 1e9 then Printf.sprintf "%.0f" f else Printf.sprintf "%.2g" f + +let spread_of (ctx : State.ctx) (states : State.t list) = + let lay = ctx.State.layout in + let n = Array.length lay.State.cells in + let seen = Array.init n (fun _ -> Hashtbl.create 8) in + List.iter + (fun (s : State.t) -> + Array.iteri (fun i v -> Hashtbl.replace seen.(i) v ()) s) + states; + List.init n (fun i -> + let cr = lay.State.cells.(i) in + ( cr.Instance.src ^ "." ^ cr.Instance.arrow, + Hashtbl.length seen.(i), + Array.length lay.State.domains.(i) )) + |> List.stable_sort (fun (_, a, _) (_, b, _) -> compare b a) + (* Breadth-first search from the initial state, firing every enabled - transition. Unnamed transitions get a positional label [#i]. Overflowing - [cap] is an error. *) -let build (m : Model.t) : (t, string) result = + transition. Unnamed transitions get a positional label [#i]. The search + stops at [max] situations or after [timeout] seconds of CPU time. *) +let explore ?(max = cap) ?timeout (m : Model.t) : + (t, [ `Model of string | `Cutoff of cutoff ]) result = match State.build_ctx m.schema m.initial with - | Error e -> Error e + | Error e -> Error (`Model e) | Ok (ctx, init) -> let index = ref State.M.empty in let dist = ref State.M.empty in @@ -50,8 +86,20 @@ let build (m : Model.t) : (t, string) result = incr count; Queue.add s queue in + let started = Sys.time () in + let timed_out = ref None in + (* The clock is read every 256 situations expanded, not added: adding + can stall while the queue drains. *) + let popped = ref 0 in add_state init 0; - while (not (Queue.is_empty queue)) && not !overflow do + while + (not (Queue.is_empty queue)) && (not !overflow) && !timed_out = None + do + incr popped; + (match timeout with + | Some t when !popped land 255 = 0 && Sys.time () -. started > t -> + timed_out := Some t + | _ -> ()); let s = Queue.pop queue in let d = State.M.find s !dist in List.iteri @@ -69,12 +117,23 @@ let build (m : Model.t) : (t, string) result = | `Next s' -> edges := { src = s; via; dst = `To s' } :: !edges; if not (State.M.mem s' !index) then - if !count >= cap then overflow := true + if !count >= max then overflow := true else add_state ~from:(s, via) s' (d + 1) end) m.transitions done; - if !overflow then Error "state space exceeds cap (200000)" + let cutoff reason = + Error + (`Cutoff + { + reason; + explored = !count; + edges_seen = List.length !edges; + spread = spread_of ctx !states; + }) + in + if !overflow then cutoff (`Cap max) + else if !timed_out <> None then cutoff (`Timeout (Option.get !timed_out)) else Ok { @@ -88,6 +147,14 @@ let build (m : Model.t) : (t, string) result = transitions = m.transitions; } +(* The unbounded-by-choice search the CLI uses: [cap] situations, no clock. *) +let build (m : Model.t) : (t, string) result = + match explore m with + | Ok t -> Ok t + | Error (`Model e) -> Error e + | Error (`Cutoff _) -> + Error ("state space exceeds cap (" ^ string_of_int cap ^ ")") + let same (a : State.t) (b : State.t) : bool = Value.compare_cells a b = 0 (* A fewest-moves path from the initial state to [target], as [via] labels: diff --git a/tests/unit/dune b/tests/unit/dune index f17355c..ec8ef2c 100644 --- a/tests/unit/dune +++ b/tests/unit/dune @@ -83,3 +83,12 @@ (test (name test_mcp) (libraries writ_data writ_syntax writ_runtime writ_mcp writ_json)) + +; Authoring through MCP: inline sources, the guide, errors, limits. Reads the +; stdlib from disk, so it depends on it. + +(test + (name test_mcp_authoring) + (deps + (glob_files %{workspace_root}/core/stdlib/*.{writ,rules})) + (libraries writ_data writ_syntax writ_runtime writ_mcp writ_json)) diff --git a/tests/unit/test_mcp_authoring.ml b/tests/unit/test_mcp_authoring.ml new file mode 100644 index 0000000..b82e4ee --- /dev/null +++ b/tests/unit/test_mcp_authoring.ml @@ -0,0 +1,902 @@ +(* Copyright (C) 2026 Alex Kunich *) +(* SPDX-License-Identifier: AGPL-3.0-or-later *) + +(* Authoring through MCP: a client that knows nothing of Writ and cannot write + to the server's filesystem must be able to learn the language (writ_guide, + instructions, the example in writ_check), send sources inline, fix its + errors from the error alone, and be told when a model is too big. + + Also the guide's own promises: every example in it still produces the + output it shows, every error code's wrong example raises that code and its + right example validates, and no topic outgrows its budget. *) + +open Writ_data + +let passed = ref 0 + +let check name cond = + if cond then incr passed + else ( + print_string ("FAIL: " ^ name ^ "\n"); + exit 1) + +let contains ~sub s = + let ls = String.length s and n = String.length sub in + let rec go i = i + n <= ls && (String.sub s i n = sub || go (i + 1)) in + go 0 + +(* dune runs tests from _build/default/tests/unit, so walk up to the root. *) +let repo_root () = + let rec up dir n = + if Sys.file_exists (Filename.concat dir "core/stdlib/stdlib.writ") then dir + else if n = 0 then dir + else up (Filename.dirname dir) (n - 1) + in + up (Sys.getcwd ()) 8 + +let read_file p = + match open_in_bin p with + | exception Sys_error _ -> None + | ic -> + let s = really_input_string ic (in_channel_length ic) in + close_in ic; + Some s + +(* Only the standard library is on disk: everything else must come inline. *) +let resolve _base name : (string, Errors.t) result = + match read_file (Filename.concat (repo_root ()) ("core/stdlib/" ^ name)) with + | Some s -> Ok s + | None -> Error { Errors.pos = None; msg = "cannot resolve load: " ^ name } + +let memory : Writ_mcp.Tools.memory = Hashtbl.create 4 + +let handle ?(pinned = None) msg = + Writ_mcp.Server.handle ~resolve ~pinned ~memory ~version:"test" msg + +let req ?(id = 1) m params = + Json.Assoc + ([ + ("jsonrpc", Json.String "2.0"); + ("id", Json.Int id); + ("method", Json.String m); + ] + @ match params with None -> [] | Some p -> [ ("params", p) ]) + +let result = function Some j -> Json.member "result" j | None -> None +let s x = Json.String x + +(* A tool call: (is-error, text). *) +let tool ?pinned name args = + let r = + result + (handle ?pinned + (req "tools/call" + (Some + (Json.Assoc [ ("name", s name); ("arguments", Json.Assoc args) ])))) + in + let text = + match Option.bind r (Json.member "content") with + | Some (Json.List (c :: _)) -> + Option.value + (Option.bind (Json.member "text" c) Json.to_string_opt) + ~default:"" + | _ -> "" + in + let err = + match Option.bind r (Json.member "isError") with + | Some (Json.Bool b) -> b + | _ -> false + in + (err, text) + +let lines t = String.split_on_char '\n' t + +(* ── initialize: instructions ───────────────────────────────────────────── *) + +let () = + let r = result (handle (req "initialize" None)) in + let ins = + Option.bind (Option.bind r (Json.member "instructions")) Json.to_string_opt + in + check "initialize: sets instructions" (ins <> None); + let ins = Option.value ins ~default:"" in + check "instructions: under 1500 characters" (String.length ins < 1500); + check "instructions: send the client to writ_guide index first" + (contains ~sub:"call writ_guide with [\"index\"]" ins); + check "instructions: give the workflow" + (contains ~sub:"writ_validate" ins + && contains ~sub:"writ_compare" ins + && contains ~sub:"writ_show" ins); + check "instructions: n/a is a failure" (contains ~sub:"n/a is a FAILURE" ins); + check "initialize: declares resources and prompts" + (match Option.bind r (Json.member "capabilities") with + | Some c -> + Json.member "resources" c <> None && Json.member "prompts" c <> None + | None -> false) + +(* ── tools/list ─────────────────────────────────────────────────────────── *) + +let tools = + match + Option.bind (result (handle (req "tools/list" None))) (Json.member "tools") + with + | Some (Json.List xs) -> xs + | _ -> [] + +let tool_named n = + List.find_opt + (fun t -> Option.bind (Json.member "name" t) Json.to_string_opt = Some n) + tools + +let description n = + Option.value + (Option.bind + (Option.bind (tool_named n) (Json.member "description")) + Json.to_string_opt) + ~default:"" + +let () = + check "tools/list: writ_guide and writ_validate are listed" + (tool_named "writ_guide" <> None && tool_named "writ_validate" <> None); + check "tools/list: every tool is marked read-only" + (List.for_all + (fun t -> + match + Option.bind + (Json.member "annotations" t) + (Json.member "readOnlyHint") + with + | Some (Json.Bool true) -> true + | _ -> false) + tools); + check "writ_guide: its description says to call it first" + (contains ~sub:"BEFORE" (description "writ_guide")); + check "writ_check: documents the default limits" + (contains ~sub:"200000" (description "writ_check") + && contains ~sub:"60000" (description "writ_check")) + +(* ── R4: the example in writ_check's description runs as described ──────── *) + +let model = Writ_mcp.Server.example_model +let claims = Writ_mcp.Server.example_claims + +let () = + let d = description "writ_check" in + check "writ_check: carries the example model and claims" + (contains ~sub:model d && contains ~sub:claims d); + let n t = + List.length (List.filter (fun l -> String.trim l <> "") (lines t)) + in + check "the example is at most 25 lines" (n model + n claims <= 25); + let err, out = + tool "writ_check" [ ("model_source", s model); ("claims_source", s claims) ] + in + check "the example checks inline" (not err); + check "the example: can-open holds" (contains ~sub:"holds can-open" out); + check "the example: never-trapped fails" + (contains ~sub:"fails never-trapped" out); + check "the example: never-lost fails" (contains ~sub:"fails never-lost" out); + check "the example: the law is broken" + (contains ~sub:"equation locked-means-held" out) + +(* ── R1: inline sources ─────────────────────────────────────────────────── *) + +let base = Writ_mcp.Diagnose.base + +let () = + let _, out = + tool "writ_check" [ ("model_source", s model); ("claims_source", s claims) ] + in + (* every index a witness names resolves through writ_show, same source *) + let idx = + List.filter_map + (fun l -> + match String.index_opt l '#' with + | Some i -> + let j = ref (i + 1) in + while !j < String.length l && l.[!j] >= '0' && l.[!j] <= '9' do + incr j + done; + int_of_string_opt (String.sub l (i + 1) (!j - i - 1)) + | None -> None) + (lines out) + in + check "witnesses name indices" (idx <> []); + List.iter + (fun i -> + let err, shown = + tool "writ_show" + [ ("model_source", s model); ("at", Json.List [ Json.Int i ]) ] + in + check + ("writ_show resolves witness index " ^ string_of_int i) + ((not err) + && contains ~sub:("situation " ^ string_of_int i ^ " of") shown)) + idx; + let err, out = + tool "writ_check" [ ("model", s "x.writ"); ("model_source", s base) ] + in + check "path and source together: E_ARG_CONFLICT" + (err && contains ~sub:"E_ARG_CONFLICT" out); + let err, out = tool "writ_check" [] in + check "neither path nor source: E_ARG_CONFLICT" + (err && contains ~sub:"E_ARG_CONFLICT" out); + let err, out = + tool "writ_check" [ ("model_source", s (String.make (300 * 1024) ' ')) ] + in + check "an oversized source: E_SOURCE_TOO_LARGE" + (err && contains ~sub:"E_SOURCE_TOO_LARGE" out); + let err, out = + tool ~pinned:(Some "humans") "writ_check" + [ + ("model_source", s base); + ("claims_source", s "(property p \"x\" (possible (is a.stage done)))"); + ] + in + check "pinned claims refuse inline claims: E_CLAIMS_PINNED" + (err && contains ~sub:"E_CLAIMS_PINNED" out); + let err, out = + tool "writ_check" [ ("model_source", s base); ("model_name", s "../x") ] + in + check "a model_name with a path in it is refused" + (err && contains ~sub:"E_ARG_INVALID" out); + let err, out = + tool "writ_query" + [ + ("model_source", s base); + ("claims_source", s "(query where (where (j job)) (is j.stage queued))"); + ("name", s "where"); + ] + in + check "writ_query: inline claims" ((not err) && contains ~sub:"j = a" out); + let err, out = + tool "writ_derive" + [ + ("model_source", s base); + ( "rules_source", + s + "(relation done 1)\n\ + (rule (done S) (situation S) (holds S (is a.stage done)))\n" ); + ("relation", s "done"); + ] + in + check "writ_derive: inline rules" + ((not err) && contains ~sub:"done (1 row)" out) + +(* ── revision history per model_name ────────────────────────────────────── *) + +let () = + (* finish can never fire: a stays running *) + let stuck = + Writ_mcp.Diagnose.replace base + [ + ( "(transition finish (when (is a.stage running))", + "(transition finish (when (is a.stage done))" ); + ] + in + let cl = + "(property finishes \"it can finish\" (possible (is a.stage done)))\n" + in + let run ?name m = + tool "writ_check" + ([ ("model_source", s m); ("claims_source", s cl) ] + @ match name with Some n -> [ ("model_name", s n) ] | None -> []) + in + Hashtbl.reset memory; + let _, first = run ~name:"shop" base in + check "revision: first named check has none" + (not (contains ~sub:"revision:" first)); + let _, second = run ~name:"shop" stuck in + check "revision: the second named check reports the LOST guarantee" + (contains ~sub:"a guarantee was LOST" second + && contains ~sub:"finishes" second); + let _, _ = run base in + let _, unnamed = run stuck in + check "revision: unnamed inline models keep no history" + (not (contains ~sub:"revision:" unnamed)) + +(* ── compare inline: the handoff regression ─────────────────────────────── *) + +let guide_topic n = + List.assoc_opt n (Writ_mcp.Guide.topics ()) |> Option.value ~default:"" + +(* The fenced blocks of a topic: (info string, body). *) +let blocks body = + let rec go acc cur = function + | [] -> List.rev acc + | l :: rest -> ( + match cur with + | None -> + if String.length l >= 3 && String.sub l 0 3 = "```" then + go acc + (Some (String.trim (String.sub l 3 (String.length l - 3)), [])) + rest + else go acc None rest + | Some (info, ls) -> + if String.trim l = "```" then + go + ((info, String.concat "\n" (List.rev ls) ^ "\n") :: acc) + None rest + else go acc (Some (info, l :: ls)) rest) + in + go [] None (lines body) + +let words s = List.filter (( <> ) "") (String.split_on_char ' ' s) + +let kv info k = + List.find_map + (fun w -> + let p = k ^ "=" in + let n = String.length p in + if String.length w > n && String.sub w 0 n = p then + Some (String.sub w n (String.length w - n)) + else None) + (words info) + +let strip_cert t = + String.concat "\n" + (List.filter (fun l -> not (contains ~sub:"certified" l)) (lines t)) + |> String.trim + +(* ── the guide's examples still do what the guide says ──────────────────── *) + +let () = + let examples = + List.filter + (fun n -> String.length n > 9 && String.sub n 0 9 = "examples.") + (Writ_mcp.Guide.names ()) + in + check "the guide has 4-6 examples" + (List.length examples >= 4 && List.length examples <= 6); + List.iter + (fun ex -> + let bs = blocks (guide_topic ex) in + let files = + List.filter_map + (fun (info, b) -> Option.map (fun f -> (f, b)) (kv info "file")) + bs + in + let src f = + match List.assoc_opt f files with + | Some b -> s b + | None -> + check (ex ^ ": names a file it defines: " ^ f) false; + s "" + in + let outputs = + List.filter + (fun (info, _) -> + String.length info > 5 && String.sub info 0 5 = "text ") + bs + in + check (ex ^ ": shows tool output") (outputs <> []); + List.iter + (fun (info, expected) -> + let get k = Option.value (kv info k) ~default:"" in + let _, actual = + match words info with + | _ :: "writ_check" :: _ -> + tool "writ_check" + [ + ("model_source", src (get "model")); + ("claims_source", src (get "claims")); + ] + | _ :: "writ_compare" :: _ -> + tool "writ_compare" + [ + ("old_model_source", src (get "old")); + ("new_model_source", src (get "new")); + ("claims_source", src (get "claims")); + ] + | _ -> (true, "unknown tool in " ^ info) + in + let ok = strip_cert actual = strip_cert expected in + if not ok then + print_string + ("--- expected\n" ^ expected ^ "--- actual\n" ^ actual ^ "\n"); + check (ex ^ ": " ^ info ^ " matches the guide") ok) + outputs) + examples; + (* syntax topics: their whole model, claims and rules validate together *) + let first_lisp n = + List.find_map + (fun (info, b) -> if info = "lisp" then Some b else None) + (blocks (guide_topic n)) + in + match + ( first_lisp "syntax.model", + first_lisp "syntax.claims", + first_lisp "syntax.rules" ) + with + | Some m, Some c, Some r -> + let law = + Writ_mcp.Diagnose.replace m + [ + ( "(arrow uses (to machine) fixed)))", + "(arrow uses (to machine) fixed))\n\ + \ (equation one-holder (not (and (is job.stage running) (not \ + (defined job.uses.held-by))))))" ); + ] + in + let err, out = + tool "writ_validate" + [ + ("model_source", s law); + ("claims_source", s c); + ("rules_source", s r); + ] + in + if err then print_string out; + check "syntax.*: the topics' examples validate together" (not err) + | _ -> check "syntax.*: each topic has a lisp example" false + +(* ── R6: every code's wrong example raises it; its right one validates ──── *) + +let validate_example (ex : Writ_mcp.Diagnose.example) = + match ex with + | Writ_mcp.Diagnose.Model m -> + Some (tool "writ_validate" [ ("model_source", s m) ]) + | Writ_mcp.Diagnose.Claims c -> + Some + (tool "writ_validate" + [ ("model_source", s base); ("claims_source", s c) ]) + | Writ_mcp.Diagnose.Rules r -> + Some + (tool "writ_validate" + [ ("model_source", s base); ("rules_source", s r) ]) + | Writ_mcp.Diagnose.Call _ -> None + +let () = + List.iter + (fun (e : Writ_mcp.Diagnose.entry) -> + (match validate_example e.wrong with + | Some (err, out) -> + if not (err && contains ~sub:("error " ^ e.code ^ " ") out) then + print_string out; + check + (e.code ^ ": its wrong example raises it") + (err && contains ~sub:("error " ^ e.code ^ " ") out) + | None -> ()); + match validate_example e.right with + | Some (err, out) -> + if err then print_string out; + check (e.code ^ ": its right example validates") (not err) + | None -> ()) + Writ_mcp.Diagnose.codes; + (* the Call examples, driven directly *) + let err, out = + tool "writ_show" + [ ("model_source", s base); ("at", Json.List [ Json.Int 99 ]) ] + in + check "E_NO_SITUATION: an index out of range" + (err && contains ~sub:"E_NO_SITUATION" out); + let err, out = tool "writ_query" [ ("model_source", s base) ] in + check "E_ARG_INVALID: a missing name" + (err && contains ~sub:"E_ARG_INVALID" out); + let err, out = + tool "writ_check" + [ ("model_source", s base); ("max_situations", Json.Int 0) ] + in + check "E_ARG_INVALID: a limit out of range" + (err && contains ~sub:"E_ARG_INVALID" out); + (* every code has its guide topic *) + List.iter + (fun (e : Writ_mcp.Diagnose.entry) -> + check + ("errors." ^ e.code ^ " is a guide topic") + (guide_topic ("errors." ^ e.code) <> "")) + Writ_mcp.Diagnose.codes + +(* ── R6: the acceptance case: a misspelt name, fixed from the error alone ── *) + +let () = + let typo = + Writ_mcp.Diagnose.replace base + [ ("(set a.stage running)", "(set a.stage runing)") ] + in + let err, out = + tool "writ_validate" [ ("model_source", s typo); ("json", Json.Bool true) ] + in + check "typo: an error" err; + let d = + match Json_parse.parse out with + | Ok j -> ( + match Json.member "errors" j with + | Some (Json.List (d :: _)) -> Some d + | _ -> None) + | Error _ -> None + in + let field k = + Option.bind (Option.bind d (Json.member k)) Json.to_string_opt + in + let int_field k = + Option.bind (Option.bind d (Json.member k)) Json.to_int_opt + in + check "typo: E_UNKNOWN_VALUE" (field "code" = Some "E_UNKNOWN_VALUE"); + check "typo: names the source" (field "source" = Some "model"); + check "typo: found the misspelling" (field "found" = Some "runing"); + check "typo: line and column" + (int_field "line" = Some 8 && int_field "col" <> None); + check "typo: expected lists the value meant" + (match Option.bind d (Json.member "expected") with + | Some (Json.List (Json.String "running" :: _)) -> true + | _ -> false); + check "typo: see points at the guide" + (field "see" = Some "writ_guide errors.E_UNKNOWN_VALUE"); + match field "fix" with + | None -> check "typo: carries a fix" false + | Some fix -> + let broken = List.nth (lines typo) 7 in + let fixed = + String.concat "\n" + (List.mapi (fun i l -> if i = 7 then fix else l) (lines typo)) + in + check "typo: the fix replaces the offending line" + (String.trim broken <> fix); + let err, _ = tool "writ_validate" [ ("model_source", s fixed) ] in + check "typo: applying the fix validates" (not err) + +(* ── a modality from another logic gets its Writ spelling ──────────────── *) + +let () = + let _, out = + tool "writ_validate" + [ + ("model_source", s base); + ("claims_source", s "(property p \"x\" (always (is a.stage done)))"); + ] + in + check "always: the hint gives (never (not P))" + (contains ~sub:"(never (not P))" out) + +(* ── review and acceptance fixes ──────────────────────────────────────── *) + +let () = + (* a typo in claims is an error at validate, with the name meant *) + let err, out = + tool "writ_validate" + [ + ("model_source", s base); + ( "claims_source", + s "(property done \"x\"\n (possible (is a.stage don)))\n" ); + ] + in + check "claims typo: validate reports it" + (err && contains ~sub:"E_UNKNOWN_VALUE in claims" out); + check "claims typo: positioned on the name" + (contains ~sub:"inline:model.claims:2:" out); + check "claims typo: with the fix" + (contains ~sub:"fix: (possible (is a.stage done)))" out); + (* and writ_check says why the property is n/a *) + let _, out = + tool "writ_check" + [ + ("model_source", s base); + ("claims_source", s "(property done \"x\" (possible (is a.stage don)))"); + ] + in + check "n/a: check says why, with the name meant" + (contains + ~sub: + "why n/a done: value don not in codomain stage-t — did you mean \ + `done`?" + out); + (* inline models have no sibling claims *) + let err, out = + tool "writ_compare" + [ ("old_model_source", s base); ("new_model_source", s base) ] + in + check "compare: inline old model needs claims" + (err && contains ~sub:"pass `claims` or `claims_source`" out); + let err, out = + tool "writ_query" [ ("model_source", s base); ("name", s "q") ] + in + check "query: inline model needs claims" + (err && contains ~sub:"E_ARG_INVALID" out); + (* an inline model is never what a (load …) reads *) + let err, out = + tool "writ_validate" + [ + ("model_source", s base); + ( "claims_source", + s "(load \"model.writ\")\n(load \"inline:model.writ\")\n" ); + ] + in + check "overlay: a load does not read the inline model" + (err && contains ~sub:"E_LOAD" out); + (* arithmetic gets the no-numbers hint, naming what is unknown *) + let plus = + Writ_mcp.Diagnose.replace base + [ + ( "(use shop)", + "(form (bump J) (transition (when (is J.stage queued)) (do (+ \ + J.stage 1))))\n\ + (use shop)" ); + ] + in + let _, out = tool "writ_validate" [ ("model_source", s plus) ] in + if not (contains ~sub:"no numbers" out) then print_string out; + check "arithmetic: the hint says there are no numbers" + (contains ~sub:"no numbers or arithmetic" out); + (* bad `at` is refused, not read as 0 *) + let err, _ = + tool "writ_show" [ ("model_source", s base); ("at", Json.List [ s "3" ]) ] + in + check "at: a string index is refused" err; + (* an instance error has no invented position *) + let unset = + Writ_mcp.Diagnose.replace base [ ("(job a) (stage (a queued))", "(job a)") ] + in + let _, js = + tool "writ_validate" [ ("model_source", s unset); ("json", Json.Bool true) ] + in + check "instance error: no made-up line" (not (contains ~sub:"\"line\"" js)); + (* history is per model_name *) + Hashtbl.reset memory; + let cl = + "(property finishes \"it can finish\" (possible (is a.stage done)))\n" + in + let stuck = + Writ_mcp.Diagnose.replace base + [ + ( "(transition finish (when (is a.stage running))", + "(transition finish (when (is a.stage done))" ); + ] + in + let _ = + tool "writ_check" + [ + ("model_source", s base); + ("claims_source", s cl); + ("model_name", s "one"); + ] + in + let _, out = + tool "writ_check" + [ + ("model_source", s stuck); + ("claims_source", s cl); + ("model_name", s "two"); + ] + in + check "history: another name starts fresh" + (not (contains ~sub:"revision:" out)); + (* the budget warning *) + let wide = + Writ_mcp.Diagnose.replace base + [ + ( "(type stage-t (queued running done))", + "(type stage-t (queued running done s3 s4 s5 s6 s7 s8 s9))" ); + ( "(type job (arrow stage (to stage-t))))", + "(type job (arrow stage (to stage-t)) (arrow b (to stage-t)) (arrow \ + c (to stage-t)) (arrow d (to stage-t)) (arrow e (to stage-t)) \ + (arrow f (to stage-t))))" ); + ( "(stage (a queued))", + "(stage (a queued)) (b (a queued)) (c (a queued)) (d (a queued)) (e \ + (a queued)) (f (a queued))" ); + ] + in + let _, out = tool "writ_validate" [ ("model_source", s wide) ] in + check "validate: warns when the bound is over budget" + (contains ~sub:"warning: the bound is over" out); + (* a timeout cuts a big search short *) + let spin = + Writ_mcp.Diagnose.replace wide + [ + ( "(transition begin", + String.concat "\n" + (List.concat_map + (fun c -> + List.map + (fun v -> + Printf.sprintf + "(transition (when (is a.%s a.%s)) (do (set a.%s %s)))" c + c c v) + [ + "queued"; + "running"; + "done"; + "s3"; + "s4"; + "s5"; + "s6"; + "s7"; + "s8"; + "s9"; + ]) + [ "b"; "c"; "d"; "e"; "f" ]) + ^ "\n(transition begin" ); + ] + in + let err, out = + tool "writ_check" + [ + ("model_source", s spin); + ("max_situations", Json.Int 2000000); + ("timeout_ms", Json.Int 1); + ] + in + if not (contains ~sub:"timeout" out) then print_string out; + check "timeout: a long search stops at the clock" + (err && contains ~sub:"stopped at timeout" out) + +(* ── a bare (set …) outside (do …) is an error, not a silent no-op ───────── *) + +let () = + let bare = + Writ_mcp.Diagnose.replace base + [ ("(do (set a.stage done))", "(set a.stage done)") ] + in + let err, out = tool "writ_validate" [ ("model_source", s bare) ] in + check "a transition clause outside when/do is refused" + (err + && contains ~sub:"unknown transition clause" out + && contains ~sub:"E_UNKNOWN_DECL" out) + +(* ── writ_validate: the summary ─────────────────────────────────────────── *) + +let () = + let err, out = + tool "writ_validate" + [ ("model_source", s model); ("claims_source", s claims) ] + in + check "validate: ok" ((not err) && contains ~sub:"ok: model, claims parse" out); + check "validate: lists types with values" + (contains ~sub:"type pos values: shut open locked" out); + check "validate: lists arrows" (contains ~sub:"arrow at -> pos" out); + check "validate: lists laws and moves" + (contains ~sub:"laws: locked-means-held" out + && contains ~sub:"moves (4): open, close, lock, drop-key" out); + check "validate: bounds the space" (contains ~sub:"at most 6 situations" out); + check "validate: property kinds" (contains ~sub:"never-trapped (live)" out); + let _, js = + tool "writ_validate" [ ("model_source", s model); ("json", Json.Bool true) ] + in + check "validate: json" + (match Json_parse.parse js with + | Ok j -> + Json.member "ok" j = Some (Json.Bool true) + && Json.member "cells" j = Some (Json.Int 2) + | Error _ -> false); + (* claims and rules errors are reported together, one per file *) + let err, out = + tool "writ_validate" + [ + ("model_source", s base); + ("claims_source", s "(property p \"x\" (always (is a.stage done)))"); + ("rules_source", s "(rule (nope S) (situation S))"); + ] + in + check "validate: one error per file" + (err && contains ~sub:"in claims" out && contains ~sub:"in rules" out) + +(* ── R7: limits ─────────────────────────────────────────────────────────── *) + +let () = + let err, out = + tool "writ_check" + [ + ("model_source", s model); + ("claims_source", s claims); + ("max_situations", Json.Int 3); + ] + in + check "limit: E_STATE_LIMIT, as an error" + (err && contains ~sub:"limit E_STATE_LIMIT" out); + check "limit: says how far it got" + (contains ~sub:"explored: 3 situations" out); + check "limit: names every property undecided" + (contains ~sub:"undecided: can-open, never-trapped, never-lost" out); + check "limit: ranks the cells driving growth" (contains ~sub:"d.at" out); + check "limit: points at idioms" (contains ~sub:"writ_guide idioms" out); + let _, js = + tool "writ_check" + [ + ("model_source", s model); + ("max_situations", Json.Int 3); + ("json", Json.Bool true); + ] + in + check "limit: json" + (match Json_parse.parse js with + | Ok j -> ( + match Json.member "limit" j with + | Some l -> Json.member "explored" l = Some (Json.Int 3) + | None -> false) + | Error _ -> false); + let err, _ = + tool "writ_check" + [ ("model_source", s model); ("max_situations", Json.Int 6) ] + in + check "limit: a space exactly at the limit is not cut off" (not err) + +(* ── R2: the guide ──────────────────────────────────────────────────────── *) + +(* ~4 bytes per token for this prose; the budgets have headroom below it. *) +let () = + let topics = Writ_mcp.Guide.topics () in + List.iter + (fun t -> check ("guide: has " ^ t) (List.mem_assoc t topics)) + [ + "index"; + "syntax.model"; + "syntax.claims"; + "syntax.rules"; + "semantics"; + "idioms"; + "errors"; + ]; + check "guide: index under 1000 tokens" + (String.length (guide_topic "index") <= 4000); + List.iter + (fun (n, b) -> + check ("guide: " ^ n ^ " under 6000 tokens") (String.length b <= 20000)) + topics; + let g = Writ_mcp.Guide.get [ "index"; "semantics" ] in + check "guide: one section per topic, in order" + (contains ~sub:"# topic.index" g && contains ~sub:"# topic.semantics" g); + let g = Writ_mcp.Guide.get [ "nonesuch" ] in + check "guide: an unknown topic lists the valid ones" + (contains ~sub:"unknown topic" g && contains ~sub:"syntax.model" g); + let err, out = + tool "writ_guide" [ ("items", Json.List [ s "errors.E_PAREN" ]) ] + in + check "writ_guide: the tool serves topics" + ((not err) && contains ~sub:"**Wrong:**" out) + +(* ── R8: resources and the prompt ───────────────────────────────────────── *) + +let () = + let r = result (handle (req "resources/list" None)) in + let n = + match Option.bind r (Json.member "resources") with + | Some (Json.List xs) -> List.length xs + | _ -> 0 + in + check "resources: one per guide topic" + (n = List.length (Writ_mcp.Guide.topics ())); + let r = + result + (handle + (req "resources/read" + (Some (Json.Assoc [ ("uri", s "writ://guide/semantics") ])))) + in + check "resources: read a topic" + (match Option.bind r (Json.member "contents") with + | Some (Json.List (c :: _)) -> + Option.bind (Json.member "text" c) Json.to_string_opt + = Some (guide_topic "semantics") + | _ -> false); + let j = + handle + (req "resources/read" + (Some (Json.Assoc [ ("uri", s "writ://guide/none") ]))) + in + check "resources: an unknown uri is a protocol error" + (Option.bind j (Json.member "error") <> None); + let r = + result + (handle + (req "prompts/get" + (Some + (Json.Assoc + [ + ("name", s "writ_model_system"); + ( "arguments", + Json.Assoc [ ("description", s "a door that locks") ] ); + ])))) + in + check "prompt: writ_model_system carries the description and the workflow" + (match Option.bind r (Json.member "messages") with + | Some (Json.List (m :: _)) -> ( + match Option.bind (Json.member "content" m) (Json.member "text") with + | Some (Json.String t) -> + contains ~sub:"a door that locks" t + && contains ~sub:"writ_validate" t + && contains ~sub:"writ_compare" t + | _ -> false) + | _ -> false) + +let () = + print_string + ("mcp authoring tests: " ^ string_of_int !passed ^ " checks passed\n") diff --git a/tooling/mcp/gen/dune b/tooling/mcp/gen/dune new file mode 100644 index 0000000..08e0d4e --- /dev/null +++ b/tooling/mcp/gen/dune @@ -0,0 +1,4 @@ +; Embeds the guide topics at build time (see embed.ml). + +(executable + (name embed)) diff --git a/tooling/mcp/gen/embed.ml b/tooling/mcp/gen/embed.ml new file mode 100644 index 0000000..1d28554 --- /dev/null +++ b/tooling/mcp/gen/embed.ml @@ -0,0 +1,27 @@ +(* Copyright (C) 2026 Alex Kunich *) +(* SPDX-License-Identifier: AGPL-3.0-or-later *) + +(* Build step: embed the guide's markdown topics (tooling/mcp/guide/*.md) as an + OCaml list, so writ-mcp serves them with no files to install. A topic is + named by its file: syntax.model.md is `syntax.model`. *) + +let read path = + let ic = open_in_bin path in + let s = really_input_string ic (in_channel_length ic) in + close_in ic; + s + +let () = + let files = + Array.to_list Sys.argv |> List.tl + |> List.filter (fun f -> Filename.check_suffix f ".md") + |> List.sort compare + in + print_string "let topics = [\n"; + List.iter + (fun f -> + Printf.printf " (%S, %S);\n" + (Filename.remove_extension (Filename.basename f)) + (read f)) + files; + print_string "]\n" diff --git a/tooling/mcp/guide/examples.commit.md b/tooling/mcp/guide/examples.commit.md new file mode 100644 index 0000000..befebee --- /dev/null +++ b/tooling/mcp/guide/examples.commit.md @@ -0,0 +1,126 @@ +Two-phase commit with two participants. Each votes yes or no (two moves each: the choice is nondeterministic, so writ tries both); the coordinator decides; each participant applies the decision. The coordinator here commits as soon as *some* participant is ready. + +```lisp file=commit.writ +(load "stdlib.writ") +(schema tpc + (type vote-t (yes no)) + (type outcome-t (commit abort)) + (type state-t (working committed aborted)) + (type part (maybe vote vote-t) (arrow state (to state-t))) + (type coord (maybe decision outcome-t))) +(instance start tpc + (part p1 (state working)) + (part p2 (state working)) + (coord c)) +(use tpc) +(initial start) + +(form (participant P YES NO APPLY-COMMIT APPLY-ABORT) + (transition YES (when (not (defined P.vote))) (do (set P.vote yes))) + (transition NO (when (not (defined P.vote))) (do (set P.vote no))) + (transition APPLY-COMMIT (when (and (is c.decision commit) (is P.state working))) + (do (set P.state committed))) + (transition APPLY-ABORT (when (and (is c.decision abort) (is P.state working))) + (do (set P.state aborted)))) +(participant p1 p1-yes p1-no p1-commit p1-abort) +(participant p2 p2-yes p2-no p2-commit p2-abort) + +; Commit as soon as one participant is ready. +(transition decide-commit + (when (and (not (defined c.decision)) (some (p part) (is p.vote yes)))) + (do (set c.decision commit))) +(transition decide-abort + (when (and (not (defined c.decision)) (some (p part) (is p.vote no)))) + (do (set c.decision abort))) +``` + +```lisp file=commit.claims +(load "stdlib.writ") +(property atomic "no participant commits while another voted no" + (never (and (some (x part) (is x.state committed)) + (some (y part) (is y.vote no))))) +(property terminates "every run ends with every participant decided" + (inevitable (all (x part) (not (is x.state working))))) +``` + +```text writ_check model=commit.writ claims=commit.claims +states: 49 edges: 94 +regime: committing — no move can be undone +gaps: none +dead ends: 6 + reached by: p1-yes, p2-yes, decide-commit, p1-commit, p2-commit + reached by: p1-yes, p2-no, decide-commit, p1-commit, p2-commit + reached by: p1-yes, p2-no, decide-abort, p1-abort, p2-abort + reached by: p1-no, p2-yes, decide-commit, p1-commit, p2-commit + reached by: p1-no, p2-yes, decide-abort, p1-abort, p2-abort + reached by: p1-no, p2-no, decide-abort, p1-abort, p2-abort +fails atomic + "no participant commits while another voted no" + witness: 1. p1-yes → #1 p1.vote: ∅ → yes + 2. p2-no → #6 p2.vote: ∅ → no + 3. decide-commit → #14 c.decision: ∅ → commit + 4. p1-commit → #29 p1.state: working → committed +holds terminates + "every run ends with every participant decided" +``` + +`atomic` fails: `p1` votes yes, `p2` votes no, the coordinator commits, `p1` commits. `terminates` holds, and the six dead ends are the designed endings (every participant has applied a decision), which is what `inevitable` confirms. + +**The fix.** Commit only when every participant voted yes: `all` from the standard library. + +```lisp file=commit-fixed.writ +(load "stdlib.writ") +(schema tpc + (type vote-t (yes no)) + (type outcome-t (commit abort)) + (type state-t (working committed aborted)) + (type part (maybe vote vote-t) (arrow state (to state-t))) + (type coord (maybe decision outcome-t))) +(instance start tpc + (part p1 (state working)) + (part p2 (state working)) + (coord c)) +(use tpc) +(initial start) + +(form (participant P YES NO APPLY-COMMIT APPLY-ABORT) + (transition YES (when (not (defined P.vote))) (do (set P.vote yes))) + (transition NO (when (not (defined P.vote))) (do (set P.vote no))) + (transition APPLY-COMMIT (when (and (is c.decision commit) (is P.state working))) + (do (set P.state committed))) + (transition APPLY-ABORT (when (and (is c.decision abort) (is P.state working))) + (do (set P.state aborted)))) +(participant p1 p1-yes p1-no p1-commit p1-abort) +(participant p2 p2-yes p2-no p2-commit p2-abort) + +; Commit only when every participant voted yes. +(transition decide-commit + (when (and (not (defined c.decision)) (all (p part) (is p.vote yes)))) + (do (set c.decision commit))) +(transition decide-abort + (when (and (not (defined c.decision)) (some (p part) (is p.vote no)))) + (do (set c.decision abort))) +``` + +```text writ_check model=commit-fixed.writ claims=commit.claims +states: 33 edges: 58 +regime: committing — no move can be undone +gaps: none +dead ends: 4 + reached by: p1-yes, p2-yes, decide-commit, p1-commit, p2-commit + reached by: p1-yes, p2-no, decide-abort, p1-abort, p2-abort + reached by: p1-no, p2-yes, decide-abort, p1-abort, p2-abort + reached by: p1-no, p2-no, decide-abort, p1-abort, p2-abort +holds atomic + "no participant commits while another voted no" +holds terminates + "every run ends with every participant decided" +``` + +```text writ_compare old=commit.writ new=commit-fixed.writ claims=commit.claims +equations: +properties: atomic gained + terminates preserved +``` + +`some` and `all` range over a type's entities; their variable heads chains (`p.vote`) and cannot stand alone as a value. diff --git a/tooling/mcp/guide/examples.consumer.md b/tooling/mcp/guide/examples.consumer.md new file mode 100644 index 0000000..f64fb19 --- /dev/null +++ b/tooling/mcp/guide/examples.consumer.md @@ -0,0 +1,132 @@ +A consumer charges a customer for a message, then acks it. The ack can be lost, in which case the broker times out and redelivers. Charges are counted on a ladder `c0 → c1 → c2` (`idioms`, Counters), so "never charged twice" is `(never (is acct.charges c2))`. Termination is asked twice: plainly, and assuming an offered `ack` is not refused for ever. + +```lisp file=consumer.writ +(load "stdlib.writ") +(schema billing + (type stage-t (queued delivered processed acked)) + (type count (arrow next (to count) fixed vacatable)) ; a ladder, not a number + (type message (arrow stage (to stage-t))) + (type account (arrow charges (to count)))) +(instance start billing + (count c0 c1 c2) + (next (c0 c1) (c1 c2) (c2 vacant)) + (message m (stage queued)) + (account acct (charges c0))) +(use billing) +(initial start) + +(transition deliver (when (is m.stage queued)) (do (set m.stage delivered))) +(transition process (when (is m.stage delivered)) + (do (set acct.charges acct.charges.next) (set m.stage processed))) +(transition ack (when (is m.stage processed)) (do (set m.stage acked))) +; The ack can be lost: the broker times out and redelivers. +(transition timeout (when (is m.stage processed)) (do (set m.stage queued))) +``` + +```lisp file=consumer.claims +(property charged-once "the customer is never charged twice" + (never (is acct.charges c2))) +(property finishes "every run acks the message" + (inevitable (is m.stage acked))) +(property finishes-fairly "it does, if an offered ack is not refused for ever" + (inevitable (is m.stage acked) (fair ack))) +``` + +```text writ_check model=consumer.writ claims=consumer.claims +states: 10 edges: 9 +regime: committing — no move can be undone +gaps: none +dead ends: 3 + reached by: deliver, process, ack + reached by: deliver, process, timeout, deliver, process, ack + reached by: deliver, process, timeout, deliver, process, timeout, deliver +fails charged-once + "the customer is never charged twice" + witness: 1. deliver → #1 m.stage: queued → delivered + 2. process → #2 m.stage: delivered → processed, acct.charges: c0 → c1 + 3. timeout → #4 m.stage: processed → queued + 4. deliver → #5 m.stage: queued → delivered + 5. process → #6 m.stage: delivered → processed, acct.charges: c1 → c2 +fails finishes + "every run acks the message" + stuck at: #9 (m.stage=delivered acct.charges=c2) + witness: 1. deliver → #1 m.stage: queued → delivered + 2. process → #2 m.stage: delivered → processed, acct.charges: c0 → c1 + 3. timeout → #4 m.stage: processed → queued + 4. deliver → #5 m.stage: queued → delivered + 5. process → #6 m.stage: delivered → processed, acct.charges: c1 → c2 + 6. timeout → #8 m.stage: processed → queued + 7. deliver → #9 m.stage: queued → delivered +fails finishes-fairly + "it does, if an offered ack is not refused for ever" + assuming fair: ack + stuck at: #9 (m.stage=delivered acct.charges=c2) + witness: 1. deliver → #1 m.stage: queued → delivered + 2. process → #2 m.stage: delivered → processed, acct.charges: c0 → c1 + 3. timeout → #4 m.stage: processed → queued + 4. deliver → #5 m.stage: queued → delivered + 5. process → #6 m.stage: delivered → processed, acct.charges: c1 → c2 + 6. timeout → #8 m.stage: processed → queued + 7. deliver → #9 m.stage: queued → delivered +``` + +`charged-once` fails: process, lose the ack, redeliver, process again. Both termination properties fail too, stuck at `#9`, where the message is delivered but `process` cannot fire because the ladder has ended (`acct.charges.next` has no answer). That dead end is the **bound**, not the system: the ladder only counts to `c2`. Read it as such. + +**The fix.** An idempotency key: the first processing sets `m.key-seen` and charges; any later one only marks the message processed. + +```lisp file=consumer-fixed.writ +(load "stdlib.writ") +(schema billing + (type stage-t (queued delivered processed acked)) + (type count (arrow next (to count) fixed vacatable)) ; a ladder, not a number + (type yes-no (no yes)) + (type message (arrow stage (to stage-t)) (arrow key-seen (to yes-no))) + (type account (arrow charges (to count)))) +(instance start billing + (count c0 c1 c2) + (next (c0 c1) (c1 c2) (c2 vacant)) + (message m (stage queued) (key-seen no)) + (account acct (charges c0))) +(use billing) +(initial start) + +(transition deliver (when (is m.stage queued)) (do (set m.stage delivered))) +; The idempotency key: charge only the first time this message is processed. +(transition process (when (and (is m.stage delivered) (is m.key-seen no))) + (do (set acct.charges acct.charges.next) (set m.key-seen yes) + (set m.stage processed))) +(transition process-again (when (and (is m.stage delivered) (is m.key-seen yes))) + (do (set m.stage processed))) +(transition ack (when (is m.stage processed)) (do (set m.stage acked))) +; The ack can be lost: the broker times out and redelivers. +(transition timeout (when (is m.stage processed)) (do (set m.stage queued))) +``` + +```text writ_check model=consumer-fixed.writ claims=consumer.claims +states: 6 edges: 6 +regime: reversible — 3 of 6 situations lie on cycles +gaps: none +dead ends: 1 + reached by: deliver, process, ack +holds charged-once + "the customer is never charged twice" +fails finishes + "every run acks the message" + stuck at: #2 (m.stage=processed m.key-seen=yes acct.charges=c1) + witness: 1. deliver → #1 m.stage: queued → delivered + 2. process → #2 m.stage: delivered → processed, m.key-seen: no → yes, acct.charges: c0 → c1 +holds finishes-fairly + "it does, if an offered ack is not refused for ever" + assuming fair: ack +``` + +Now `charged-once` holds. `finishes` still fails, correctly: a run can lose the ack for ever (`timeout` again and again). `finishes-fairly` holds: if `ack` is not refused for ever, every run acks. That is `inevitable` with `(fair …)` doing its job, and the honest statement of what this protocol guarantees. + +```text writ_compare old=consumer.writ new=consumer-fixed.writ claims=consumer.claims +equations: +properties: charged-once gained + finishes-fairly gained +still failing in both models: finishes +``` + +`finishes` fails in both models, so it is no row of the comparison; the last line names it, so a fix that fixed nothing cannot pass for one. diff --git a/tooling/mcp/guide/examples.handoff.md b/tooling/mcp/guide/examples.handoff.md new file mode 100644 index 0000000..503a278 --- /dev/null +++ b/tooling/mcp/guide/examples.handoff.md @@ -0,0 +1,146 @@ +Leader `a` hands leadership to `b`. In this version `b` acknowledges only once `a` has stepped down, and `a` steps down only once `b` has acknowledged. + +```lisp file=handoff.writ +(load "stdlib.writ") +(schema cluster + (type role-t (leader follower)) + (type yes-no (no yes)) + (type server (arrow role (to role-t)) + (arrow offered (to yes-no)) + (arrow acked (to yes-no)))) +(instance start cluster + (server a (role leader) (offered no) (acked no)) + (server b (role follower) (offered no) (acked no))) +(use cluster) +(initial start) + +(transition offer (when (and (is a.role leader) (is a.offered no))) + (do (set a.offered yes))) +; b acknowledges only once a has stepped down... +(transition b-ack (when (and (is a.offered yes) (is a.role follower) (is b.acked no))) + (do (set b.acked yes))) +; ...and a steps down only once b has acknowledged. +(transition a-release (when (and (is b.acked yes) (is a.role leader))) + (do (set a.role follower))) +(transition b-take (when (and (is b.acked yes) (is a.role follower) (is b.role follower))) + (do (set b.role leader))) +``` + +```lisp file=handoff.claims +(property one-leader "never two leaders at once" + (never (and (is a.role leader) (is b.role leader)))) +(property hands-off "the handoff can always still complete" + (live (is b.role leader))) +``` + +```text writ_check model=handoff.writ claims=handoff.claims +states: 2 edges: 1 +regime: committing — no move can be undone +gaps: none +dead ends: 1 + reached by: offer +holds one-leader + "never two leaders at once" +fails hands-off + "the handoff can always still complete" + stuck at: #0 (a.role=leader b.role=follower a.offered=no b.offered=no a.acked=no b.acked=no) +``` + +`hands-off` fails, stuck at `#0`: no run can ever complete the handoff, because after `offer` each side waits for the other. The one dead end, after `offer`, is that deadlock, not a designed ending. `one-leader` holds only because nothing happens. + +**A first fix**, which looks right: let `b` acknowledge the offer itself and take over once it has. + +```lisp file=handoff-v2.writ +(load "stdlib.writ") +(schema cluster + (type role-t (leader follower)) + (type yes-no (no yes)) + (type server (arrow role (to role-t)) + (arrow offered (to yes-no)) + (arrow acked (to yes-no)))) +(instance start cluster + (server a (role leader) (offered no) (acked no)) + (server b (role follower) (offered no) (acked no))) +(use cluster) +(initial start) + +(transition offer (when (and (is a.role leader) (is a.offered no))) + (do (set a.offered yes))) +; b acknowledges the offer itself. +(transition b-ack (when (and (is a.offered yes) (is b.acked no))) + (do (set b.acked yes))) +(transition a-release (when (and (is b.acked yes) (is a.role leader))) + (do (set a.role follower))) +(transition b-take (when (and (is b.acked yes) (is b.role follower))) + (do (set b.role leader))) +``` + +```text writ_check model=handoff-v2.writ claims=handoff.claims +states: 6 edges: 6 +regime: committing — no move can be undone +gaps: none +dead ends: 1 + reached by: offer, b-ack, a-release, b-take +fails one-leader + "never two leaders at once" + witness: 1. offer → #1 a.offered: no → yes + 2. b-ack → #2 b.acked: no → yes + 3. b-take → #4 b.role: follower → leader +holds hands-off + "the handoff can always still complete" +``` + +The deadlock is gone, but compare the edit before calling it done: + +```text writ_compare old=handoff.writ new=handoff-v2.writ claims=handoff.claims +equations: +properties: one-leader LOST witness: 1. offer 2. b-ack 3. b-take + hands-off gained +``` + +`one-leader` is LOST, and the row carries the route: `b` takes over before `a` has released. This is the regression loop (`idioms`): an edit that makes one property pass by losing another is not a fix. + +**The real fix.** `b` takes over only once `a` is a follower. + +```lisp file=handoff-v3.writ +(load "stdlib.writ") +(schema cluster + (type role-t (leader follower)) + (type yes-no (no yes)) + (type server (arrow role (to role-t)) + (arrow offered (to yes-no)) + (arrow acked (to yes-no)))) +(instance start cluster + (server a (role leader) (offered no) (acked no)) + (server b (role follower) (offered no) (acked no))) +(use cluster) +(initial start) + +(transition offer (when (and (is a.role leader) (is a.offered no))) + (do (set a.offered yes))) +; b acknowledges the offer itself. +(transition b-ack (when (and (is a.offered yes) (is b.acked no))) + (do (set b.acked yes))) +(transition a-release (when (and (is b.acked yes) (is a.role leader))) + (do (set a.role follower))) +(transition b-take (when (and (is b.acked yes) (is a.role follower) (is b.role follower))) + (do (set b.role leader))) +``` + +```text writ_check model=handoff-v3.writ claims=handoff.claims +states: 5 edges: 4 +regime: committing — no move can be undone +gaps: none +dead ends: 1 + reached by: offer, b-ack, a-release, b-take +holds one-leader + "never two leaders at once" +holds hands-off + "the handoff can always still complete" +``` + +```text writ_compare old=handoff.writ new=handoff-v3.writ claims=handoff.claims +equations: +properties: one-leader preserved + hands-off gained +``` diff --git a/tooling/mcp/guide/examples.mutex.md b/tooling/mcp/guide/examples.mutex.md new file mode 100644 index 0000000..b8d8aa8 --- /dev/null +++ b/tooling/mcp/guide/examples.mutex.md @@ -0,0 +1,96 @@ +Two processes share a lock. Each checks that the lock is free, then takes it: two moves, so the other process can run in between. The question is the safety property every mutex owes: never both inside. + +```lisp file=mutex.writ +(load "stdlib.writ") +(schema mutex + (type pc-t (idle saw-free critical)) + (type proc (arrow pc (to pc-t))) + (type lock (maybe holder proc))) +(instance start mutex + (proc p (pc idle)) + (proc q (pc idle)) + (lock l)) +(use mutex) +(initial start) + +; Check, then take: two moves, so both processes can see the lock free. +(form (process P LOOK TAKE LEAVE) + (transition LOOK (when (and (is P.pc idle) (not (defined l.holder)))) + (do (set P.pc saw-free))) + (transition TAKE (when (is P.pc saw-free)) + (do (set l.holder P) (set P.pc critical))) + (transition LEAVE (when (is P.pc critical)) + (do (vacate l.holder) (set P.pc idle)))) +(process p p-look p-take p-leave) +(process q q-look q-take q-leave) +``` + +```lisp file=mutex.claims +(property exclusive "never both in the critical section" + (never (and (is p.pc critical) (is q.pc critical)))) +(property p-can-enter "p can always still get in" + (live (is p.pc critical))) +``` + +```text writ_check model=mutex.writ claims=mutex.claims +states: 14 edges: 26 +regime: reversible — 14 of 14 situations lie on cycles +gaps: none +dead ends: none +fails exclusive + "never both in the critical section" + witness: 1. p-look → #1 p.pc: idle → saw-free + 2. q-look → #4 q.pc: idle → saw-free + 3. p-take → #6 p.pc: saw-free → critical, l.holder: ∅ → p + 4. q-take → #8 q.pc: saw-free → critical, l.holder: p → q +holds p-can-enter + "p can always still get in" +``` + +`exclusive` fails, and the witness is the race: both look while the lock is free (steps 1 and 2), then both take it. The second take overwrites `l.holder` (`p → q`), which a real lock would refuse. `p-can-enter` holds: there is no deadlock, only a safety bug. + +**The fix.** Make seeing the lock free and taking it one move, a test-and-set. `saw-free` disappears. + +```lisp file=mutex-fixed.writ +(load "stdlib.writ") +(schema mutex + (type pc-t (idle critical)) + (type proc (arrow pc (to pc-t))) + (type lock (maybe holder proc))) +(instance start mutex + (proc p (pc idle)) + (proc q (pc idle)) + (lock l)) +(use mutex) +(initial start) + +; Test-and-set: seeing the lock free and taking it are one move. +(form (process P TAKE LEAVE) + (transition TAKE (when (and (is P.pc idle) (not (defined l.holder)))) + (do (set l.holder P) (set P.pc critical))) + (transition LEAVE (when (is P.pc critical)) + (do (vacate l.holder) (set P.pc idle)))) +(process p p-take p-leave) +(process q q-take q-leave) +``` + +```text writ_check model=mutex-fixed.writ claims=mutex.claims +states: 3 edges: 4 +regime: reversible — 3 of 3 situations lie on cycles +gaps: none +dead ends: none +holds exclusive + "never both in the critical section" +holds p-can-enter + "p can always still get in" +``` + +Then price the edit against the old model: + +```text writ_compare old=mutex.writ new=mutex-fixed.writ claims=mutex.claims +equations: +properties: exclusive gained + p-can-enter preserved +``` + +`exclusive` was gained and nothing was lost. The lesson is in `idioms` (Concurrency): whatever the real system does in two steps must be two moves, or the model cannot show the race. diff --git a/tooling/mcp/guide/examples.webhooks.md b/tooling/mcp/guide/examples.webhooks.md new file mode 100644 index 0000000..394ec13 --- /dev/null +++ b/tooling/mcp/guide/examples.webhooks.md @@ -0,0 +1,128 @@ +An order is authorized and can then be captured or voided. A payment gateway sends `capture` and `void` webhooks; delivery is at-least-once, so a handled webhook can arrive again, and two workers consume them concurrently. The requirement: a voided order is never captured. That mentions order (*after* voided), so the model keeps a history cell, `o.was-voided`, set by the void handler (`idioms`, History). + +```lisp file=webhooks.writ +(load "stdlib.writ") +(schema shop + (type status-t (authorized captured voided)) + (type yes-no (no yes)) + (type order (arrow status (to status-t)) (arrow was-voided (to yes-no))) + (type kind-t (capture void)) + (type stage-t (queued working done)) + (type hook (arrow kind (to kind-t) fixed) (arrow stage (to stage-t))) + (type worker (maybe job hook))) +(instance start shop + (order o (status authorized) (was-voided no)) + (hook cap (kind capture) (stage queued)) + (hook vd (kind void) (stage queued)) + (worker w1) + (worker w2)) +(use shop) +(initial start) + +; At-least-once delivery: a handled webhook can arrive again. +(transition redeliver-capture (when (is cap.stage done)) (do (set cap.stage queued))) +(transition redeliver-void (when (is vd.stage done)) (do (set vd.stage queued))) + +(form (consumer W TAKE-CAP TAKE-VOID CAPTURE VOID SKIP-VOID) + (transition TAKE-CAP (when (and (is cap.stage queued) (not (defined W.job)))) + (do (set W.job cap) (set cap.stage working))) + (transition TAKE-VOID (when (and (is vd.stage queued) (not (defined W.job)))) + (do (set W.job vd) (set vd.stage working))) + ; "Skip duplicates": capture unless already captured. + (transition CAPTURE (when (and (is W.job.kind capture) (not (is o.status captured)))) + (do (set o.status captured) (set W.job.stage done) (vacate W.job))) + (transition VOID (when (and (is W.job.kind void) (is o.status authorized))) + (do (set o.status voided) (set o.was-voided yes) + (set W.job.stage done) (vacate W.job))) + (transition SKIP-VOID (when (and (is W.job.kind void) (not (is o.status authorized)))) + (do (set W.job.stage done) (vacate W.job)))) +(consumer w1 w1-take-capture w1-take-void w1-capture w1-void w1-skip-void) +(consumer w2 w2-take-capture w2-take-void w2-capture w2-void w2-skip-void) +``` + +```lisp file=webhooks.claims +(property no-capture-after-void "a voided order is never captured" + (never (and (is o.was-voided yes) (is o.status captured)))) +(property can-settle "the order can always still be settled" + (live (not (is o.status authorized)))) +``` + +```text writ_check model=webhooks.writ claims=webhooks.claims +states: 45 edges: 91 +regime: reversible — 38 of 45 situations lie on cycles +gaps: none +dead ends: none +fails no-capture-after-void + "a voided order is never captured" + witness: 1. w1-take-capture → #1 cap.stage: queued → working, w1.job: ∅ → cap + 2. w2-take-void → #6 vd.stage: queued → working, w2.job: ∅ → vd + 3. w2-void → #12 o.status: authorized → voided, o.was-voided: no → yes, vd.stage: working → done, w2.job: vd → ∅ + 4. w1-capture → #21 o.status: voided → captured, cap.stage: working → done, w1.job: cap → ∅ +holds can-settle + "the order can always still be settled" +``` + +`no-capture-after-void` fails. The witness: `w1` takes the capture webhook, `w2` takes the void and voids the order, then `w1` captures it, because the capture handler's guard only skips orders that are *already captured*. Duplicates are not even needed: the two workers are enough. `can-settle` holds: the order can always leave `authorized`. + +**The fix.** Capture only an order that is still `authorized`, and acknowledge any other capture webhook without effect (a new `SKIP-CAP` move per worker). + +```lisp file=webhooks-fixed.writ +(load "stdlib.writ") +(schema shop + (type status-t (authorized captured voided)) + (type yes-no (no yes)) + (type order (arrow status (to status-t)) (arrow was-voided (to yes-no))) + (type kind-t (capture void)) + (type stage-t (queued working done)) + (type hook (arrow kind (to kind-t) fixed) (arrow stage (to stage-t))) + (type worker (maybe job hook))) +(instance start shop + (order o (status authorized) (was-voided no)) + (hook cap (kind capture) (stage queued)) + (hook vd (kind void) (stage queued)) + (worker w1) + (worker w2)) +(use shop) +(initial start) + +; At-least-once delivery: a handled webhook can arrive again. +(transition redeliver-capture (when (is cap.stage done)) (do (set cap.stage queued))) +(transition redeliver-void (when (is vd.stage done)) (do (set vd.stage queued))) + +(form (consumer W TAKE-CAP TAKE-VOID CAPTURE SKIP-CAP VOID SKIP-VOID) + (transition TAKE-CAP (when (and (is cap.stage queued) (not (defined W.job)))) + (do (set W.job cap) (set cap.stage working))) + (transition TAKE-VOID (when (and (is vd.stage queued) (not (defined W.job)))) + (do (set W.job vd) (set vd.stage working))) + ; Capture only what is still authorized; ack anything else. + (transition CAPTURE (when (and (is W.job.kind capture) (is o.status authorized))) + (do (set o.status captured) (set W.job.stage done) (vacate W.job))) + (transition SKIP-CAP (when (and (is W.job.kind capture) (not (is o.status authorized)))) + (do (set W.job.stage done) (vacate W.job))) + (transition VOID (when (and (is W.job.kind void) (is o.status authorized))) + (do (set o.status voided) (set o.was-voided yes) + (set W.job.stage done) (vacate W.job))) + (transition SKIP-VOID (when (and (is W.job.kind void) (not (is o.status authorized)))) + (do (set W.job.stage done) (vacate W.job)))) +(consumer w1 w1-take-capture w1-take-void w1-capture w1-skip-capture w1-void w1-skip-void) +(consumer w2 w2-take-capture w2-take-void w2-capture w2-skip-capture w2-void w2-skip-void) +``` + +```text writ_check model=webhooks-fixed.writ claims=webhooks.claims +states: 35 edges: 80 +regime: reversible — 28 of 35 situations lie on cycles +gaps: none +dead ends: none +holds no-capture-after-void + "a voided order is never captured" +holds can-settle + "the order can always still be settled" +``` + +```text writ_compare old=webhooks.writ new=webhooks-fixed.writ claims=webhooks.claims +equations: +properties: no-capture-after-void gained + can-settle preserved +``` + +The guard on the current state, not on "have I seen this before", is what makes the handler safe against duplicates and reordering alike. diff --git a/tooling/mcp/guide/idioms.md b/tooling/mcp/guide/idioms.md new file mode 100644 index 0000000..5e6f0ab --- /dev/null +++ b/tooling/mcp/guide/idioms.md @@ -0,0 +1,84 @@ +Modelling patterns. A model that parses can still ask the wrong question; most mistakes are here, not in the syntax. + +## Concurrency + +- **One move is one atomic step.** Whatever a real system does indivisibly (a test-and-set, a transaction) is one move; whatever it does in separate steps (read, then write) must be separate moves, or the model hides the race. `examples.mutex` is exactly this. +- **N identical workers**: write one form taking the worker and its move names, and call it once per worker (`examples.webhooks`). Interleaving is automatic: every enabled move of every worker is explored at every step. +- **Use the fewest workers that show the behaviour.** Two exhibit any race or mutual-exclusion bug; a third rarely adds one. Identical workers multiply the space by symmetric copies (w1 holds the job, or w2 does) and writ does not merge them. +- **Guard every move on the state it changes.** A move that can fire again after doing its job is a self-loop that doubles edges and hides dead ends: `(when (and (is b.acked yes) (is a.role leader)))`, not `(when (is b.acked yes))`. + +## Messaging + +Give each message its own stage cell; a consumer takes any queued one, so every delivery order is explored. These are small patterns, combine them: + +```lisp +; duplicate delivery (at-least-once): a handled message can arrive again +(transition redeliver (when (is m.stage done)) (do (set m.stage queued))) +; loss: a sent message can vanish +(transition lose (when (is m.stage sent)) (do (set m.stage lost))) +; bounded retries: m.tries walks a ladder r0 -> r1 -> r2; at the end the +; retry is absent and only giving up is left +(transition retry (when (is m.stage lost)) + (do (set m.stage sent) (set m.tries m.tries.next))) +(transition give-up (when (and (is m.stage lost) (not (defined m.tries.next)))) + (do (set m.stage failed))) +``` + +- **Reordering** is free with one cell per message. To model a FIFO channel, guard taking `m2` on `m1` already taken. +- **An idempotency key** is a cell the handler sets the first time and tests after (`examples.consumer`). + +## Time + +There are no clocks. A timeout, an expiry or a crash is a move that is enabled whenever it could happen, so writ explores it firing at every possible moment: + +```lisp +(transition timeout (when (is req.stage waiting)) (do (set req.stage expired))) +(transition lease-expires (when (defined l.holder)) (do (vacate l.holder))) +``` + +Add a ladder of ticks only when the order of two deadlines matters. + +## Counters + +A count is a ladder of entities walked by a fixed vacatable arrow, never a number: + +```lisp +(type count (arrow next (to count) fixed vacatable)) +(instance … (count c0 c1 c2) (next (c0 c1) (c1 c2) (c2 vacant)) …) +(transition charge (when …) (do (set acct.charges acct.charges.next))) +``` + +At the top of the ladder `acct.charges.next` has no answer, so `charge` is absent: the counter saturates by blocking. That block is the bound, not the system, and it shows up as a dead end or a stuck run. Make the ladder one step longer than the question needs (to ask "never charged twice", count to `c2`) and read a dead end at the top as the bound. For a cheap counter, prefer a small enum `(none one many)`. + +## History + +A property that mentions order ("never captured *after* voided") needs a cell that remembers: set a flag when the first event happens and test it with the second, as in `(never (and (is o.was-voided yes) (is o.status captured)))`. A history cell multiplies the space by its domain, so keep it two-valued. + +## Abstraction and size + +- The space is at most the product of every mutable cell's domain (plus one for vacatable cells). `writ_validate` prints the bound. Keep it under about 100000 for a check in seconds; the hard default is 200000 situations. +- Leave out everything no property reads: amounts become buckets (`(small large)`), identifiers become one entity per role, and payloads disappear. +- Model one instance of the thing at risk (one order, one message) and two of the things that race over it. +- Make wiring `fixed`: a fixed arrow costs nothing. +- When writ reports `E_STATE_LIMIT`, read its growth list: the cells that took the most values are the ones to shrink. + +## Asking the right question + +| requirement | property | +| --- | --- | +| "X must never happen" | `(never X)` | +| "P always holds" | `(never (not P))` | +| "it is possible to X"; "find a schedule" | `(possible X)` (the witness is the schedule) | +| "it can always recover"; "no trap"; "can always still finish" | `(live X)` | +| "it eventually finishes"; "it terminates" | `(inevitable X)` | +| "it finishes provided the retry is not refused for ever" | `(inevitable X (fair retry))` | +| "every ending is a good one" | `(inevitable GOOD-ENDING)` | + +`live` and `inevitable` part company exactly where a system can loop for ever without being stuck: the retry that is always possible but need never succeed. Ask `live` for a capability that must not be lost and `inevitable` for an outcome that must be delivered. If `inevitable` fails only through a loop of retries, the honest fix is often the fairness assumption, stated, not a change to the model. + +## The regression loop + +1. Check the model; keep the claims fixed. +2. Edit the model to fix a failure. +3. `writ_compare` the old model against the new (or re-check with the same `model_name`). A LOST row is a guarantee the edit broke, with its route; an edit that fixes one property by losing another is not a fix (`examples.handoff`). +4. Never edit a claim to make it pass, and never delete what a claim asks about: `n/a` counts as LOST. diff --git a/tooling/mcp/guide/index.md b/tooling/mcp/guide/index.md new file mode 100644 index 0000000..53364fe --- /dev/null +++ b/tooling/mcp/guide/index.md @@ -0,0 +1,40 @@ +Writ is an explicit-state model checker for finite discrete systems. You write a world down — the kinds of thing in it, the typed arrows between them, one starting configuration, and guarded moves — and writ enumerates **every** reachable situation, then answers your questions by exhaustion: `holds` with the shortest witness route, `fails` with the shortest counterexample. There are no numbers and nothing unbounded; that is what makes `never` a census rather than a search that gave up. + +## Workflow + +1. Read `syntax.model`, `syntax.claims` and `semantics`; read `idioms` before modelling anything concurrent, retried or timed. +2. Write the model (`model_source`) and the questions (`claims_source`) as two separate texts. +3. `writ_validate`: parse and type-check without building anything. Repeat until `ok`, and read its summary: does the model declare what you meant? Is the situation bound small? +4. `writ_check`: build the space and answer every property. +5. `writ_show` on every `#N` a witness or a `stuck at:` line names; explain the route in the system's own terms. +6. After every edit, `writ_compare` the old model against the new one, or give `writ_check` the same `model_name` each time: either reports any guarantee the edit LOST. + +## Topics + +| topic | what it holds | +| --- | --- | +| `syntax.model` | the `.writ` grammar: every keyword, types, arrows, instance, moves, laws, forms, the standard library | +| `syntax.claims` | the `.claims` grammar: the four property kinds, fairness, queries, `accept` | +| `syntax.rules` | the `.rules` grammar: relations and rules over the space, for `writ_derive` | +| `semantics` | what each construct means: situations, moves, property kinds, `n/a`, witnesses, indices, compare | +| `idioms` | concurrency, messaging, time, counters, abstraction and size, choosing the property kind, the regression loop | +| `examples.mutex` | a check-then-act race; `never` | +| `examples.webhooks` | two workers, duplicated and reordered webhooks; a history cell; `never` and `live` | +| `examples.consumer` | retries and an idempotency key; a counter ladder; `inevitable` with fairness | +| `examples.commit` | two-phase commit; `some` and `all` | +| `examples.handoff` | a deadlock found by `live`; a fix that LOSES a guarantee, caught by `writ_compare` | +| `errors` | every error code; `errors.` gives a wrong and a right example | + +## Limits + +- The search stops at `max_situations` (default 200000, at most 2000000) or `timeout_ms` of CPU time (default 60000, at most 600000) and returns `E_STATE_LIMIT`; nothing is decided then. Edges are not limited separately. +- The space is at most the product of every mutable cell's domain: three jobs with a three-valued stage each is 27 situations, ten such cells 59049. `writ_validate` prints this bound; keep it under about 100000. +- Inline sources are at most 256 KB each. + +## Five rules that save a retry + +1. Start with `(load "stdlib.writ")` if you use `all`, `differ`, `=` or `maybe`; there is no implicit prelude. Loading it reserves the type names `node`, `edge`, `ob`, `hom` and `eqn`. +2. Effects go inside `(do …)`. A property needs a description string; a query has none. +3. A law, `(equation NAME GUARD)`, is reported, not enforced; enforce a rule with a move's `when`. +4. There is no `always` (write `(never (not P))`) and there are no numbers (a counter is a ladder; see `idioms`). +5. A property reported `n/a` is a FAILURE: it names something the model lacks. diff --git a/tooling/mcp/guide/semantics.md b/tooling/mcp/guide/semantics.md new file mode 100644 index 0000000..2fd1932 --- /dev/null +++ b/tooling/mcp/guide/semantics.md @@ -0,0 +1,74 @@ +What each construct means, precisely. Read this before choosing a property kind. + +## 1. Situations + +A **situation** is one assignment of a value to every mutable cell (every entity × non-`fixed` arrow), a vacatable cell possibly `vacant`. Two situations are equal when every mutable cell holds the same value. Fixed cells (the wiring) are the same in all of them and are not part of a situation. The set of possible situations is the product of the cells' domains; the space writ builds is the part reachable from the initial one. + +## 2. The initial situation + +There is exactly one: the instance named by `(initial …)`. It is index `0`. + +## 3. Moves + +- A move is **enabled** in a situation when its `when` guard is true there. A guard is evaluated in that one situation; `is` is false when either side has no answer. +- Firing a move applies all of its effects at once, each reading the situation the move started from. The result is the next situation, or, if a `gap` fires, no situation: a **gap edge** out of the model. +- A `set` whose target or right side has no answer makes the move **absent** there: no edge at all. +- One step fires exactly one enabled move. Several enabled moves are nondeterministic alternatives, and writ explores every one: concurrency is interleaving, and there is no synchronous step and no built-in scheduler. +- A move whose effects change nothing is an edge back to the same situation. + +## 4. The property kinds + +Let R be the reachable situations and F the formula. A **run** is a maximal path: it goes on for ever, or it stops at a situation with no enabled move, or at one whose only moves are gaps. + +| kind | meaning | sort | +| --- | --- | --- | +| `(possible F)` | some s in R satisfies F | reachability | +| `(never F)` | no s in R satisfies F | safety (an invariant is `(never (not P))`) | +| `(live F)` | for every s in R, some situation reachable from s satisfies F | recoverability: no trap | +| `(inevitable F)` | from every s in R, every run reaches F | liveness: termination, must-happen | +| `(inevitable F (fair M…))` | the same, ignoring runs in which a named move is enabled infinitely often and never taken | liveness under strong fairness | + +There is no fairness unless you write `(fair …)`, and it only ever names moves. A run that stops is never unfair, so fairness cannot rescue a deadlock. `inevitable` implies `live` and `live` implies `possible` (from the initial situation); the gap between `live` and `inevitable` is a world that can always still reach F and need never do it. + +## 5. Laws and properties + +A law, `(equation NAME GUARD)` in the schema, is checked in every reachable situation but never restricts a move. `writ_check` reports, per law, the moves that **can break it** (a conservative analysis: any move that writes a cell the law reads), the reachable situations that **violate** it, and the shortest route to one. "A law can be broken" means a reachable situation violates it. To make a rule hold, put it in the moves' `when` guards; to ask whether it holds, write a `never` property. In claims, `(accept MOVE LAW)` records a known breaker; an unacknowledged breaker is reported `unadmitted` and fails the check. + +## 6. Gaps and dead ends + +A **gap** is a declared silence, `(gap "MSG")`: the model says its rules do not cover what happens next. A **dead end** is a reachable situation with no enabled move (a gap does not count as a move). Neither is an error: the report counts dead ends with a route to each, because only you know whether an ending is the goal or a deadlock. Say which with `(inevitable GOAL)`: an ending that is not GOAL then fails with a route. + +## 7. n/a + +A property is `n/a` when it cannot be asked of this model. It is a **failure**: the check fails as it does for `fails`, and `writ_check` adds a `why n/a` line naming what is missing. Causes: + +- its formula names an arrow the type lacks: `(is a.colour red)` when `job` has no `colour`; +- it compares with a value outside the type: `(is a.stage finished)` when `stage-t` has no `finished`; +- it names a type the schema lacks in `some` or `all`; +- its `(fair M)` names a move the model lacks. + +After an edit, a property that became `n/a` counts as LOST. Never make a check pass by deleting what a question asks about. + +## 8. Witnesses + +The space is built breadth-first, so every route printed is a shortest one (fewest moves). Among equally short routes, writ reports the first found: moves are tried in the order they are declared, situations in index order. A `fails` for `never` shows the route to the violating situation; for `live` and `inevitable` it shows `stuck at:` the nearest situation from which F is unreachable (`live`) or avoidable for ever (`inevitable`), with the route *to* it. That route is empty when the stuck situation is `#0`, and it does not show the loop that avoids F: `writ_show` the stuck situation and follow its moves, or ask `.rules` (`recurrent` in `ct.rules`). A holding `possible` shows the route to the nearest F situation: that route is the answer to "is there a way". + +## 9. Indices + +Situation `#N` is the N-th situation discovered breadth-first. The search is deterministic, so the same source gives the same numbering on every run, and `writ_show` re-enumerates to resolve an index. Almost any edit renumbers: a new or reordered move, a new value, a changed guard. Never carry an index from one version of a model to another: re-run `writ_check` on the new source and take its indices. + +## 10. Rules + +A `.rules` program is evaluated to its least fixpoint over the finite space, stratum by stratum; negation must be stratified (no recursion through `not`), so every answer is exact. `writ_derive` with `why: true` returns a derivation tree: the rule used at each step, down to built-in facts about situations, edges and cells. It proves the fact is derivable; it does not prove that nothing else is. + +## 11. writ_compare + +Both models are built. The old model's claims are put to both, and properties are matched **by name**. Each row is: + +- `preserved`: passes in both; +- `LOST`: passes in the old and fails or is `n/a` in the new; the row carries the route through the new model that breaks it; +- `gained`: fails in the old, passes in the new. + +A property that fails in both is no row; a closing `still failing in both models:` line names it, so an edit that fixed nothing does not look clean. + +Laws (equations) are matched by name and meaning: a law deleted or rewritten is LOST. `writ_check` given the same claims path, or the same `model_name` with inline sources, prints the same comparison against the previous check as a `revision:` block. That history lives in the server process: it is lost when the server restarts, and a client that starts a server per call never sees it; use `writ_compare` then. diff --git a/tooling/mcp/guide/syntax.claims.md b/tooling/mcp/guide/syntax.claims.md new file mode 100644 index 0000000..9a5a078 --- /dev/null +++ b/tooling/mcp/guide/syntax.claims.md @@ -0,0 +1,65 @@ +A `.claims` file holds the questions about one model, kept apart from it so an edit to the model cannot quietly change what is asked. It is read against the model: its chains are typed by the model's schema. Same lexical rules as `syntax.model`. + +## Grammar + +``` +claims ::= (load-d | form-d | property-d | query-d | accept-d)… + +property-d ::= (property NAME "DESCRIPTION" (MODALITY guard [fair-d]) [show-d]) +MODALITY ::= possible | never | live | inevitable +fair-d ::= (fair MOVE…) ; only after an inevitable formula +show-d ::= (show QUERY…) ; queries of this file, answered where the verdict points + +query-d ::= (query NAME (where (VAR TYPE)…) guard) ; no description string +accept-d ::= (accept MOVE LAW…) ; this move is known to be able to break these laws +``` + +The guard is the model's guard language (`syntax.model`), including forms; load `stdlib.writ` here too if you use `all`, `differ` or `=`. + +## The four property kinds + +| kind | holds when | a failure shows | +| --- | --- | --- | +| `(possible F)` | some reachable situation satisfies F | nothing exists to show; a hold carries the route to F | +| `(never F)` | no reachable situation satisfies F | the shortest route to an F situation | +| `(live F)` | from every reachable situation, some F situation is still reachable | `stuck at:` a situation from which F is gone for good, and its route | +| `(inevitable F)` | no run avoids F for ever (every run reaches F) | `stuck at:` where a run can avoid F, and its route | +| `(inevitable F (fair M…))` | the same, ignoring runs in which a named move is offered again and again and never taken | as above | + +There is no `always`, `eventually` or `exists`. Translate: + +| you mean | write | +| --- | --- | +| P always holds; P is an invariant | `(never (not P))` | +| X can never happen | `(never X)` | +| X can happen; there is a schedule that does X | `(possible X)` (its witness is the schedule) | +| X can always still happen; no trap; can always recover | `(live X)` | +| X eventually happens; it terminates; it cannot be put off for ever | `(inevitable X)` | +| …provided the network/scheduler does not starve move M | `(inevitable X (fair M))` | + +## Example + +```lisp +(load "stdlib.writ") +(property finishes "the job can finish" + (possible (is a.stage done))) +(property never-stuck "from anywhere it can still finish" + (live (is a.stage done))) +(property must-finish "no run goes on for ever without finishing" + (inevitable (is a.stage done) (fair a-finish)) + (show holder)) +(property exclusive "the machine never has two jobs running" + (never (and (is a.stage running) (is b.stage running)))) +(query holder (where (m machine)) (defined m.held-by)) +(accept a-finish one-holder) +``` + +## Rules + +- A property needs its description string; a query must not have one. Either mistake rejects the whole file (`E_MALFORMED`). +- F may use `some` and `all` (stdlib); its variables head chains, as in the model. +- `(fair …)` names **moves** (transitions), so name your moves. Naming a move the model lacks makes the property `n/a`. +- `(show Q…)` answers the named queries at the situation the verdict singles out: the stuck situation of a failing `live` or `inevitable`, the violating one of a failing `never`, the satisfying one of a holding `possible`. +- A query answers the set of bindings that satisfy its guard, at the initial situation (or at `at` in `writ_query`). Its guard can test a cell (`(defined m.held-by)`, `(is j.stage done)`) but a bare variable cannot be a value: to ask *what a cell holds*, use `.rules` (`syntax.rules`). +- `accept` acknowledges that a move can break a law. A move that can break a law without an `accept` is reported `unadmitted`; an `accept` for a move that cannot is `stale`. Both make `writ_check` fail, as a failing property does. Violations are still reported. +- A property that names an arrow, value, type or move the model lacks is `n/a`: a failure, never a pass. diff --git a/tooling/mcp/guide/syntax.model.md b/tooling/mcp/guide/syntax.model.md new file mode 100644 index 0000000..0b31f4c --- /dev/null +++ b/tooling/mcp/guide/syntax.model.md @@ -0,0 +1,99 @@ +A `.writ` file is s-expressions. `;` starts a comment to end of line. Atoms are case-sensitive; a quoted atom `"…"` may hold spaces (escapes `\n \t \r \" \\`). An atom containing `.` is a **chain**: `a.uses.held-by` follows the arrow `uses` from `a`, then `held-by`. ALL-CAPS atoms are blanks inside a form, and variables in a rules file; avoid them for names. + +## Grammar + +``` +model ::= library-datum… use-d initial-d transition-d… +library-datum ::= load-d | schema-d | instance-d | form-d + +load-d ::= (load "FILE") ; e.g. (load "stdlib.writ"); no implicit prelude +use-d ::= (use SCHEMA) ; exactly one +initial-d ::= (initial INSTANCE) ; exactly one + +schema-d ::= (schema NAME type-d… equation-d…) +type-d ::= (type NAME) ; open: entities are listed by the instance + | (type NAME (VALUE…)) ; enumerated: these values and no others + | (type NAME arrow-d…) ; open, with arrows out of it +arrow-d ::= (arrow NAME (to TYPE) flag…) +flag ::= fixed ; wiring: set in the instance, no move may change it + | vacatable ; may be empty (vacant) +equation-d ::= (equation NAME guard) ; a law; chains start at a TYPE name (see below) + +instance-d ::= (instance NAME SCHEMA clause…) +clause ::= (TYPE ENTITY…) ; declare entities of an open type + | (TYPE ENTITY slot…) ; one entity with its slots + | (ARROW (ENTITY value)…) ; one arrow's value for several entities +slot ::= (ARROW value) +value ::= VALUE | ENTITY | vacant + +transition-d::= (transition NAME (when guard) (do effect…)) ; NAME optional but always give one +guard ::= (and guard…) | (or guard…) | (not guard) + | (is CHAIN rhs) ; the chain's answer is rhs; false if it has none + | (defined CHAIN) ; the chain has an answer + | (some (VAR TYPE) guard) ; some entity of TYPE; VAR may only head chains + | NAME | (NAME arg…) ; a form +rhs ::= VALUE | ENTITY | CHAIN +effect ::= (set CHAIN rhs) | (vacate CHAIN) | (gap "MESSAGE") + +form-d ::= (form (NAME BLANK… [&rest BLANK]) TEMPLATE…) + | (form NAME DATUM) ; nullary, used as the bare atom NAME +``` + +The 26 kernel words: `load use initial schema type arrow to fixed vacatable equation instance vacant transition when do set vacate gap and or not is defined some form &rest`. + +## A whole model + +```lisp +(load "stdlib.writ") +(schema shop + (type stage-t (queued running done)) ; enumerated + (type machine (maybe held-by job)) ; maybe = stdlib for a vacatable arrow + (type job + (arrow stage (to stage-t)) + (arrow uses (to machine) fixed))) ; wiring +(instance start shop + (machine m1) + (job a (stage queued) (uses m1)) + (job b (stage queued) (uses m1))) ; m1.held-by is vacatable, so it starts vacant +(use shop) +(initial start) +(form (job-moves J BEGIN FINISH) + (transition BEGIN + (when (and (is J.stage queued) (not (defined J.uses.held-by)))) + (do (set J.uses.held-by J) (set J.stage running))) + (transition FINISH (when (is J.stage running)) + (do (set J.stage done) (vacate J.uses.held-by)))) +(job-moves a a-begin a-finish) +(job-moves b b-begin b-finish) +``` + +## Rules of each construct + +**Types.** An enumerated type's values are atoms; an open type's entities come from the instance. Every type, entity, form and law shares one namespace with everything loaded; arrow names are scoped to their type. + +**Arrows and cells.** Each (entity, arrow) pair is a cell. A `fixed` cell is wiring: given once in the instance, never written, not part of a situation. Every other cell is mutable and is part of the situation. In the instance, every non-vacatable cell needs a value; a vacatable mutable cell left out starts `vacant`; a fixed cell must be given even when vacatable (write `(c2 vacant)` at the end of a ladder). + +**Chains.** `x.a.b` follows `a` from `x`, then `b`. If any step has no answer, the chain has none: `is` is then false, `defined` false, and a `set` whose target or right side has no answer makes the whole move absent in that situation. + +**Moves.** `when` decides where the move exists; there is no failure and no rollback. All effects of one move read the situation it started from and apply together, so `(do (set a.x b.y) (set b.y a.x))` swaps. `set` cannot write `vacant`; use `vacate`, and only on a vacatable arrow. `(gap "MSG")` declares the rules silent here: the move leads out of the model. Omitting `(do …)` makes a move that changes nothing (a self-loop). + +**Guards.** `(is A B)` is strict: false if either side has no answer, so `(not (is A B))` is true when A is vacant. `some` binds a variable that may head chains, `(some (j job) (is j.stage done))`, but cannot stand alone as a value: `(is x.owner j)` with a bare `j` is an error. A guard can test a cell but cannot bind what it holds for later use; use `.rules` for that. + +**Laws.** `(equation NAME GUARD)` sits inside the schema. Its chains start at a type name, which ranges over every entity of that type: `(equation one-holder (not (and (is job.stage running) (not (defined job.uses.held-by)))))`. A law is observed: `writ_check` reports which moves can break it and the shortest route to a situation that does. It never prunes a move. + +**Forms.** A form renames and pastes, before parsing: blanks (ALL-CAPS) are replaced by what the call wrote; `&rest R` captures the remaining arguments and `@R` pastes them. No recursion, conditionals or loops. A template may mention only kernel words, its own blanks and forms declared earlier; it cannot introduce a bound variable, so pass a `some` variable in as a parameter. A top-level call may expand to several datums (several transitions); inside a list it must expand to exactly one. Pass move names as parameters, as above: unnamed moves print as `#0`, `#1`…, which reads like a situation index. + +## The standard library (`stdlib.writ`) + +| form | means | +| --- | --- | +| `(all (X T) G)` | every X of type T satisfies G | +| `(= A B)` | equal, or either side has no answer | +| `(differ A B)` | `(not (is A B))`: true when either side has no answer | +| `(maybe A T)` | `(arrow A (to T) vacatable)`, inside a type | +| `(toggle P A B)` | two moves flipping P between A and B | +| `(latch P A B)` | one move taking P from A to B, never back | +| `(phase-gated P V G)` | `(and (is P V) G)` | +| `(span R A B)` | a junction type R with fixed arrows `left` to A and `right` to B | + +It also declares the schemas `quiver` (types `node`, `edge`) and `olog` (types `ob`, `hom`, `eqn`): do not name your own types or entities `node`, `edge`, `ob`, `hom` or `eqn`. diff --git a/tooling/mcp/guide/syntax.rules.md b/tooling/mcp/guide/syntax.rules.md new file mode 100644 index 0000000..8c2f134 --- /dev/null +++ b/tooling/mcp/guide/syntax.rules.md @@ -0,0 +1,59 @@ +A `.rules` file holds Datalog-style relations over a model's enumerated space, asked with `writ_derive`. Use it for what claims cannot say: *what* a cell holds where (a claims guard can only test it), closures such as "reports to, transitively", and custom modalities. Rules never add a situation, edge or cell. Same lexical rules as `syntax.model`. + +## Grammar + +``` +rules ::= (load-d | form-d | relation-d | rule-d)… + +relation-d ::= (relation NAME ARITY) ; columns typed by use + | (relation NAME (SORT…)) ; or typed explicitly +SORT ::= Situation | Edge | TYPE ; TYPE: a schema type +rule-d ::= (rule (NAME term…) literal…) ; head, then body (a conjunction) +term ::= VAR | CONSTANT ; VAR is ALL-CAPS; anything else a constant +literal ::= (NAME term…) ; a declared relation + | (not (NAME term…)) ; negation of a declared relation + | builtin + | kernel guard over constants and variables ; (is X.arrow V), (is X.a Y.b), (defined X.arrow), … +``` + +## Built-in relations + +| relation | holds when | +| --- | --- | +| `(situation S)` | S is a reachable situation | +| `(init S)` | S is the initial situation | +| `(edge E S1 S2)` | the move named E leads from S1 to S2 | +| `(holds S G)` | guard G (a guard datum, not a variable) is true in S; G's variables are the rule's | +| `(gap-edge E S)` | move E fires at S with no successor (a `gap`) | +| `(phase S P)` | S belongs to phase P: a class of mutually reachable situations, named by its least index | +| `(phase-step P Q)` | some move leads out of phase P into a different phase Q | + +These names are reserved. `(load "ct.rules")` adds `reach`, `mutual`, `recurrent`, `before`, `phase-before`, `one-way`, `escapes`, `final-phase`, `moves` and `dead-end`. + +## Example + +```lisp +(relation holder (Situation machine job)) +(rule (holder S M J) (situation S) (holds S (is M.held-by J))) + +(relation can-finish 1) +(rule (can-finish S) (situation S) (holds S (is a.stage done))) +(rule (can-finish S) (edge E S T) (can-finish T)) + +(relation trapped 1) +(rule (trapped S) (situation S) (not (can-finish S))) + +(relation sharing (job job)) +(rule (sharing J K) (is J.uses M) (is K.uses M) (is J.uses K.uses)) +``` + +`writ_derive` with relation `holder` and args `[null, "m1", null]` lists every situation index and the job holding `m1` there; with `why: true` and every argument given it returns the derivation tree. A situation is written as its bare index, the one `writ_show` takes. + +## Rules + +- A variable is an ALL-CAPS atom; a model name spelled in capitals would read as a variable and is rejected. +- A body joins in written order. Relations, built-ins and a top-level `(is PATH V)` bind variables; `not` and tests may only use variables bound before them. +- `(is PATH V)` with a variable V binds V to what the path holds. `(is PATH PATH)` compares two paths: it only tests, so both roots must be bound before it, and two paths landing in different types are refused. To bind a value two paths share, use one variable: `(is C.approver P) (is C.preparer P)`. +- Recursion is allowed; recursion through `not` is rejected (`E_RULES`). The answer is the least fixpoint, computed stratum by stratum. +- `holds` does not bind its situation: put `(situation S)` (or `edge`, `init`) before it. It does bind the guard's variables, so `(situation S) (holds S (is X.a Y))` binds Y to what `X.a` holds in S: the thing a claims query cannot do. +- `reach` and `before` are quadratic in the number of situations; prefer a backward relation like `can-finish` above, which is linear. diff --git a/tooling/mcp/lib/diagnose.ml b/tooling/mcp/lib/diagnose.ml new file mode 100644 index 0000000..f1c735a --- /dev/null +++ b/tooling/mcp/lib/diagnose.ml @@ -0,0 +1,1081 @@ +(* Copyright (C) 2026 Alex Kunich *) +(* SPDX-License-Identifier: AGPL-3.0-or-later *) + +(* A failure, made actionable: a stable code, where, what was found and what + could have been meant, one imperative hint, and a corrected line when the + mistake is a misspelt name. + + The engine's diagnostics are prose with a position. Codes are assigned + here, by message, rather than at the ~160 places that raise them: the + table below is the one place to look, and test_mcp runs every code's + wrong example to prove the message still maps to it. *) + +open Writ_data +open Writ_syntax + +(* ── the codes ───────────────────────────────────────────────────────────── *) + +(* What an example is written against: a whole model, claims or rules for + [base], or a tool call. *) +type example = + | Model of string + | Claims of string + | Rules of string + | Call of string + +type entry = { + code : string; + cause : string; + hint : string; + wrong : example; + right : example; +} + +(* Every example below is checked by test_mcp: [wrong] must produce [code], + [right] must validate. *) +let base = + "(load \"stdlib.writ\")\n\ + (schema shop\n\ + \ (type stage-t (queued running done))\n\ + \ (type job (arrow stage (to stage-t))))\n\ + (instance start shop (job a) (stage (a queued)))\n\ + (use shop)\n\ + (initial start)\n\ + (transition begin (when (is a.stage queued)) (do (set a.stage running)))\n\ + (transition finish (when (is a.stage running)) (do (set a.stage done)))\n" + +(* [src] with each [from] replaced by its [into], once. *) +let replace (src : string) (edits : (string * string) list) = + List.fold_left + (fun src (from, into) -> + let n = String.length from and l = String.length src in + let rec at i = + if i + n > l then invalid_arg ("Diagnose.replace: " ^ from) + else if String.sub src i n = from then i + else at (i + 1) + in + let i = at 0 in + String.sub src 0 i ^ into ^ String.sub src (i + n) (l - i - n)) + src edits + +let edit ~from ~into = replace base [ (from, into) ] + +(* [base] with a second enumerated type, for a mismatch to have two sides. *) +let flagged = + replace base + [ + ( "(type job (arrow stage (to stage-t))))", + "(type flag (no yes))\n\ + \ (type job (arrow stage (to stage-t)) (arrow urgent (to flag))))" ); + ("(stage (a queued))", "(stage (a queued)) (urgent (a no))"); + ] + +let begin_ = + "(transition begin (when (is a.stage queued)) (do (set a.stage running)))" + +let codes : entry list = + [ + { + code = "E_PAREN"; + cause = "A list is never closed, or a `)` closes nothing."; + hint = "Balance the parentheses of the form at the position given."; + wrong = + Model + (edit ~from:begin_ + ~into:(String.sub begin_ 0 (String.length begin_ - 1))); + right = Model base; + }; + { + code = "E_LOAD"; + cause = + "A `(load \"FILE\")` names a file that cannot be found, loads itself, \ + or loads a file that is not a library (it holds use, initial or \ + transition)."; + hint = + "Load `stdlib.writ` by that exact name; a library may hold \ + declarations only."; + wrong = Model (edit ~from:"stdlib.writ" ~into:"stdlb.writ"); + right = Model base; + }; + { + code = "E_UNKNOWN_FORM"; + cause = + "A guard's head is neither a kernel word (and or not is defined some) \ + nor a declared form. There is no implicit prelude: `all`, `differ` \ + and the rest come from `(load \"stdlib.writ\")`."; + hint = "Use a kernel guard word, or load or declare the form first."; + wrong = + Model + (edit ~from:"(when (is a.stage queued))" + ~into:"(when (equals a.stage queued))"); + right = Model base; + }; + { + code = "E_UNKNOWN_ARROW"; + cause = + "A chain follows an arrow the type at that point does not declare."; + hint = "Use an arrow declared on the type the chain has reached."; + wrong = + Model + (edit ~from:"(when (is a.stage queued))" + ~into:"(when (is a.stauts queued))"); + right = Model base; + }; + { + code = "E_UNKNOWN_ENTITY"; + cause = + "A chain starts at a name that is not an entity of the instance or a \ + variable bound by `some`/`all`/`where`."; + hint = "Start the chain at an entity the instance declares."; + wrong = + Model + (edit ~from:"(when (is a.stage queued))" + ~into:"(when (is b.stage queued))"); + right = Model base; + }; + { + code = "E_UNKNOWN_VALUE"; + cause = + "A value is not in the type the arrow points to (a misspelt enum \ + value, or an entity of the wrong type)."; + hint = "Use a value of the arrow's codomain type."; + wrong = + Model (edit ~from:"(set a.stage running)" ~into:"(set a.stage runing)"); + right = Model base; + }; + { + code = "E_UNKNOWN_TYPE"; + cause = + "A type name is used that the schema does not declare: an arrow's `(to \ + TYPE)`, an instance clause, or a binder."; + hint = "Use a type the schema declares, or declare it."; + wrong = Model (edit ~from:"(to stage-t)" ~into:"(to stage)"); + right = Model base; + }; + { + code = "E_UNKNOWN_DECL"; + cause = + "A top-level datum or a clause inside one is not a word of its file \ + type. A model has load schema instance form use initial transition; a \ + claims file property query accept load form; a rules file relation \ + rule load form."; + hint = "Spell the declaration as the grammar for this file type has it."; + wrong = Model (edit ~from:"(transition finish" ~into:"(transtion finish"); + right = Model base; + }; + { + code = "E_UNKNOWN_MODALITY"; + cause = + "A property's formula is not headed by possible, never, live or \ + inevitable. There is no `always`: always P is `(never (not P))`."; + hint = "Head the formula with possible, never, live or inevitable."; + wrong = + Claims "(property ok \"never stuck\" (always (is a.stage done)))\n"; + right = + Claims "(property ok \"always done\" (never (not (is a.stage done))))\n"; + }; + { + code = "E_UNKNOWN_NAME"; + cause = + "`(use …)` or `(initial …)` names a schema or instance that is not \ + declared."; + hint = + "Name the schema in (use …) and the instance in (initial …) exactly."; + wrong = Model (edit ~from:"(use shop)" ~into:"(use shp)"); + right = Model base; + }; + { + code = "E_UNKNOWN_QUERY"; + cause = + "A `(show …)` clause or a writ_query call names a query the claims \ + file lacks."; + hint = "Name a query declared in the same claims file."; + wrong = + Claims + "(query where (where (j job)) (is j.stage done))\n\ + (property ok \"it can finish\" (possible (is a.stage done)) (show \ + wher))\n"; + right = + Claims + "(query where (where (j job)) (is j.stage done))\n\ + (property ok \"it can finish\" (possible (is a.stage done)) (show \ + where))\n"; + }; + { + code = "E_UNKNOWN_RELATION"; + cause = + "A rule uses a relation that is neither declared with (relation …) nor \ + built in."; + hint = "Declare the relation with (relation NAME ARITY) before using it."; + wrong = + Rules + "(relation done 1)\n\ + (rule (done S) (situation S) (holds S (is a.stage done)) (finished \ + S))\n"; + right = + Rules + "(relation done 1)\n\ + (rule (done S) (situation S) (holds S (is a.stage done)))\n"; + }; + { + code = "E_UNKNOWN_MOVE"; + cause = + "A `(fair …)` names a move the model does not have. Fairness names \ + transitions, so every move it names needs a name in the model."; + hint = "Name a transition the model declares (writ_validate lists them)."; + wrong = + Claims + "(property done \"it finishes\" (inevitable (is a.stage done) (fair \ + finsh)))\n"; + right = + Claims + "(property done \"it finishes\" (inevitable (is a.stage done) (fair \ + finish)))\n"; + }; + { + code = "E_DUPLICATE"; + cause = + "A name is declared twice where it must be fresh: a transition, a \ + type, a value, a form."; + hint = "Rename one of the two declarations."; + wrong = Model (edit ~from:"(transition finish" ~into:"(transition begin"); + right = Model base; + }; + { + code = "E_MISSING"; + cause = + "A required part is absent: a model needs exactly one (use SCHEMA) and \ + one (initial INSTANCE); a transition needs one (when GUARD)."; + hint = "Add the missing declaration."; + wrong = Model (edit ~from:"(initial start)\n" ~into:""); + right = Model base; + }; + { + code = "E_FIXED"; + cause = + "A move writes an arrow declared `fixed` (wiring, which no move may \ + change)."; + hint = "Drop `fixed` from the arrow, or stop writing it."; + wrong = + Model + (edit ~from:"(arrow stage (to stage-t))" + ~into:"(arrow stage (to stage-t) fixed)"); + right = Model base; + }; + { + code = "E_NOT_VACATABLE"; + cause = + "A move vacates an arrow not declared `vacatable`; only those may be \ + empty."; + hint = "Declare the arrow `vacatable`, or set it to a value instead."; + wrong = + Model + (edit ~from:"(do (set a.stage done))" ~into:"(do (vacate a.stage))"); + right = + Model + (replace base + [ + ( "(arrow stage (to stage-t))", + "(arrow stage (to stage-t) vacatable)" ); + ("(do (set a.stage done))", "(do (vacate a.stage))"); + ]); + }; + { + code = "E_UNSET_CELL"; + cause = + "The instance leaves a cell without a value: a fixed arrow, or a \ + mutable arrow that is not vacatable."; + hint = + "Give every entity a value for every non-vacatable arrow in the \ + instance."; + wrong = Model (edit ~from:"(job a) (stage (a queued))" ~into:"(job a)"); + right = Model base; + }; + { + code = "E_TYPE_MISMATCH"; + cause = + "The two sides of a comparison or assignment land in different types."; + hint = "Compare or assign a value of the type the chain lands in."; + wrong = + Model + (replace flagged + [ ("(set a.stage running)", "(set a.stage a.urgent)") ]); + right = Model flagged; + }; + { + code = "E_FORM"; + cause = + "A form is invoked with the wrong number of arguments, recurses, or \ + its template mentions a name that is not a blank (a form cannot \ + introduce a bound variable)."; + hint = + "Match the form's pattern exactly, and pass binders in as parameters."; + wrong = + Model + (replace base + [ + ("(use shop)", "(form (at J S) (is J.stage S))\n(use shop)"); + ("(when (is a.stage queued))", "(when (at a))"); + ]); + right = Model base; + }; + { + code = "E_RULES"; + cause = + "A rules program cannot be evaluated: recursion through negation, a \ + negated built-in, or a variable not bound by a positive literal."; + hint = + "Negate only declared relations, and never on a cycle back to the head."; + wrong = Rules "(relation p 1)\n(rule (p S) (situation S) (not (p S)))\n"; + right = + Rules + "(relation p 1)\n\ + (rule (p S) (situation S) (holds S (is a.stage done)))\n"; + }; + { + code = "E_MALFORMED"; + cause = + "A declaration has the wrong shape. A property needs a description \ + string: (property NAME \"TEXT\" FORMULA); a query has none: (query \ + NAME (where (x TYPE)…) GUARD)."; + hint = + "Rewrite the datum in the shape syntax.model / syntax.claims gives."; + wrong = Claims "(property ok (possible (is a.stage done)))\n"; + right = + Claims "(property ok \"it can finish\" (possible (is a.stage done)))\n"; + }; + { + code = "E_STATE_LIMIT"; + cause = + "The space grew past max_situations (or timeout_ms) before the search \ + finished. Nothing is decided on a partial space."; + hint = + "Shrink the model: fewer entities, smaller enums, a short ladder for \ + any counter, and no cell the questions do not read."; + wrong = Call "writ_check({model_source: …, max_situations: 2})"; + right = Call "writ_check({model_source: …})"; + }; + { + code = "E_NO_SITUATION"; + cause = + "An index is out of range. Indices are positions in this model's space \ + only."; + hint = "Use an index the last writ_check of this exact source printed."; + wrong = Call "writ_show({model_source: …, at: [99]})"; + right = Call "writ_show({model_source: …, at: [1]})"; + }; + { + code = "E_ARG_CONFLICT"; + cause = + "An argument was given both as a path and as inline source, or as \ + neither."; + hint = + "Pass exactly one of `model` or `model_source` (likewise claims, \ + rules)."; + wrong = Call "writ_check({model: \"m.writ\", model_source: \"…\"})"; + right = Call "writ_check({model_source: \"…\"})"; + }; + { + code = "E_ARG_INVALID"; + cause = + "A required argument is missing, has the wrong type, or is out of \ + range."; + hint = + "Pass the arguments the tool's input schema lists, with their types."; + wrong = Call "writ_query({model_source: \"…\"})"; + right = + Call + "writ_query({model_source: \"…\", claims_source: \"…\", name: \ + \"where\"})"; + }; + { + code = "E_SOURCE_TOO_LARGE"; + cause = "An inline source is over 256 KB."; + hint = + "Shrink the source or pass a path; a model that large will not check \ + in time anyway."; + wrong = Call "writ_check({model_source: <300 KB>})"; + right = Call "writ_check({model: \"big.writ\"})"; + }; + { + code = "E_CLAIMS_PINNED"; + cause = + "The server pins claims (--claims-dir), so inline claims are refused: \ + the questions are the human's, not the agent's."; + hint = "Pass `claims` as a path; its basename picks the pinned file."; + wrong = Call "writ_check({model_source: \"…\", claims_source: \"…\"})"; + right = Call "writ_check({model_source: \"…\", claims: \"shop.claims\"})"; + }; + { + code = "E_OTHER"; + cause = + "A failure no other code describes; the message is the engine's own."; + hint = "Read the message; it names the construct and the rule it breaks."; + wrong = Call "—"; + right = Call "—"; + }; + ] + +let entry code = List.find_opt (fun e -> e.code = code) codes + +(* ── classification ──────────────────────────────────────────────────────── *) + +let contains ~sub s = + let ls = String.length s and n = String.length sub in + let rec go i = i + n <= ls && (String.sub s i n = sub || go (i + 1)) in + go 0 + +(* First match wins, so the specific patterns come before the general. *) +let table = + [ + ("E_LOAD", [ "cannot resolve load"; "load cycle"; "declarations only" ]); + ( "E_PAREN", + [ "parenthes"; "unterminated"; "unexpected `)`"; "unexpected )" ] ); + ("E_UNKNOWN_MODALITY", [ "unknown modality" ]); + ( "E_UNKNOWN_FORM", + [ "unknown guard"; "a form not yet declared"; "nullary form" ] ); + ("E_UNKNOWN_ARROW", [ "has no arrow" ]); + ("E_UNKNOWN_ENTITY", [ "unknown entity or variable"; "names no entity" ]); + ( "E_UNKNOWN_VALUE", + [ "not in codomain"; "value out of domain"; "is not a value" ] ); + ( "E_UNKNOWN_NAME", + [ + "names unknown schema"; + "names unknown instance"; + "refers to unknown schema"; + ] ); + ("E_UNKNOWN_QUERY", [ "names no query"; "no query named" ]); + ("E_UNKNOWN_MOVE", [ "no move named" ]); + ( "E_UNKNOWN_RELATION", + [ + "is not a declared relation"; + "no relation named"; + "not a declared relation"; + ] ); + ( "E_UNKNOWN_TYPE", + [ + "undeclared type"; + "is not a declared type"; + "not a type the schema declares"; + "not a type or arrow of the schema"; + ] ); + ( "E_UNKNOWN_DECL", + [ + "unknown top-level declaration"; + "unknown schema clause"; + "unknown claims declaration"; + "unknown rules declaration"; + "unknown arrow clause"; + "unknown transition clause"; + ] ); + ( "E_DUPLICATE", + [ + "already declared"; + "declared twice"; + "is already a value"; + "collides with"; + ] ); + ("E_FIXED", [ "is fixed, so" ]); + ("E_NOT_VACATABLE", [ "is not vacatable, so" ]); + ("E_UNSET_CELL", [ "has no value"; " unset" ]); + ( "E_TYPE_MISMATCH", + [ + "lands in `"; + "comparing two chains"; + "but is used with"; + "ranges over two types"; + "is not an equality test"; + ] ); + ( "E_FORM", + [ + "form invocation"; + "recurses"; + "expansion exceeded"; + "&rest"; + "form pattern"; + "template of"; + "expands to several"; + "does not match the invocation"; + "structural form"; + ] ); + ( "E_RULES", + [ + "stratified"; + "negation cycle"; + "cannot be negated"; + "built-in relation"; + "built in and a rule"; + "is not bound"; + "unsafe"; + ] ); + ("E_MISSING", [ "needs one"; "needs a ("; "needs at least" ]); + ("E_NO_SITUATION", [ "no situation " ]); + ("E_MALFORMED", [ "malformed"; "expected "; "exactly one"; "empty " ]); + ] + +let classify (f : Fault.t) : string = + match f.code with + | Some c -> c + | None -> ( + let msg = f.err.Errors.msg in + match + List.find_opt + (fun (_, subs) -> List.exists (fun sub -> contains ~sub msg) subs) + table + with + | Some (c, _) -> c + | None -> "E_OTHER") + +(* ── what the sources declare, read lexically ──────────────────────────── + Lexical so it works when the parse failed: the names a did-you-mean can + offer. A form call inside a type body, (maybe held-by job), is read as + declaring its second atom as an arrow, which is what stdlib's do. *) + +type symbols = { + mutable types : string list; + mutable arrows : (string * string) list; (** type, arrow *) + mutable values : (string * string) list; (** enumerated type, value *) + mutable entities : (string * string) list; (** open type, entity *) + mutable forms : string list; + mutable moves : string list; + mutable schemas : string list; + mutable instances : string list; + mutable queries : string list; + mutable relations : string list; +} + +let harvest ~(read : string -> string option) (files : string list) : symbols = + let s = + { + types = []; + arrows = []; + values = []; + entities = []; + forms = []; + moves = []; + schemas = []; + instances = []; + queries = []; + relations = []; + } + in + let seen = Hashtbl.create 8 in + let atom = function Reader.Atom (a, _) -> Some a | _ -> None in + (* A type body: (v1 v2 …) enumerates values, (arrow A …) declares an + arrow, and a form call (F A …) — stdlib's (maybe A T) — declares A. *) + let type_body ty items = + List.iter + (function + | Reader.List (Reader.Atom ("arrow", _) :: Reader.Atom (a, _) :: _, _) + -> + s.arrows <- (ty, a) :: s.arrows + | Reader.List (Reader.Atom (f, _) :: Reader.Atom (a, _) :: _, _) + when List.mem f s.forms -> + s.arrows <- (ty, a) :: s.arrows + | Reader.List (vs, _) when List.for_all (fun d -> atom d <> None) vs -> + List.iter + (fun v -> + Option.iter (fun v -> s.values <- (ty, v) :: s.values) (atom v)) + vs + | _ -> ()) + items + in + let rec walk file = + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + match Option.map (Reader.read_string ~file) (read file) with + | Some (Ok ds) -> List.iter top ds + | _ -> () + end + and top d = + match d with + | Reader.List (Reader.Atom ("load", p) :: Reader.Atom (f, _) :: _, _) -> + (* relative to the including file, as the loader searches *) + let dir = + match p.Errors.file with + | Some inc -> Filename.dirname inc + | None -> "." + in + walk (if dir = "." then f else Filename.concat dir f) + | Reader.List (Reader.Atom ("schema", _) :: Reader.Atom (n, _) :: items, _) + -> + s.schemas <- n :: s.schemas; + List.iter top items + | Reader.List (Reader.Atom ("type", _) :: Reader.Atom (n, _) :: items, _) -> + s.types <- n :: s.types; + type_body n items + | Reader.List + (Reader.Atom ("instance", _) :: Reader.Atom (n, _) :: _ :: clauses, _) + -> + s.instances <- n :: s.instances; + List.iter + (function + | Reader.List (Reader.Atom (ty, _) :: items, _) -> + List.iter + (function + | Reader.Atom (e, _) -> s.entities <- (ty, e) :: s.entities + | _ -> ()) + items + | _ -> ()) + clauses + | Reader.List + ( Reader.Atom ("form", _) + :: Reader.List (Reader.Atom (n, _) :: _, _) + :: _, + _ ) + | Reader.List (Reader.Atom ("form", _) :: Reader.Atom (n, _) :: _, _) -> + s.forms <- n :: s.forms + | Reader.List (Reader.Atom ("transition", _) :: Reader.Atom (n, _) :: _, _) + -> + s.moves <- n :: s.moves + | Reader.List (Reader.Atom ("query", _) :: Reader.Atom (n, _) :: _, _) -> + s.queries <- n :: s.queries + | Reader.List (Reader.Atom ("relation", _) :: Reader.Atom (n, _) :: _, _) -> + s.relations <- n :: s.relations + | _ -> () + in + List.iter walk files; + s + +(* ── did you mean ────────────────────────────────────────────────────────── *) + +let distance a b = + let la = String.length a and lb = String.length b in + let d = Array.make_matrix (la + 1) (lb + 1) 0 in + for i = 0 to la do + d.(i).(0) <- i + done; + for j = 0 to lb do + d.(0).(j) <- j + done; + for i = 1 to la do + for j = 1 to lb do + let c = if a.[i - 1] = b.[j - 1] then 0 else 1 in + d.(i).(j) <- + min (min (d.(i - 1).(j) + 1) (d.(i).(j - 1) + 1)) (d.(i - 1).(j - 1) + c); + if i > 1 && j > 1 && a.[i - 1] = b.[j - 2] && a.[i - 2] = b.[j - 1] then + d.(i).(j) <- min d.(i).(j) (d.(i - 2).(j - 2) + 1) + done + done; + d.(la).(lb) + +let uniq xs = List.sort_uniq compare xs + +(* Candidates nearest first; [best] only when it is plausibly a typo. *) +let rank found cands = + let cands = uniq (List.filter (fun c -> c <> found) cands) in + let scored = List.map (fun c -> (distance found c, c)) cands in + let sorted = List.stable_sort (fun (a, _) (b, _) -> compare a b) scored in + let best = + match sorted with + | (d, c) :: _ when d <= max 1 (min 3 (String.length found / 3)) -> Some c + | _ -> None + in + (List.map snd sorted, best) + +let backticked msg = + let rec go i acc = + match String.index_from_opt msg i '`' with + | None -> List.rev acc + | Some a -> ( + match String.index_from_opt msg (a + 1) '`' with + | None -> List.rev acc + | Some b -> go (b + 1) (String.sub msg (a + 1) (b - a - 1) :: acc)) + in + go 0 [] + +let words msg = String.split_on_char ' ' msg |> List.filter (( <> ) "") + +let rec after w = function + | x :: y :: _ when x = w -> Some y + | _ :: rest -> after w rest + | [] -> None + +(* What a modality from another logic is in Writ's four. *) +let synonyms = + [ + ( "always", + "There is no `always`: write `(never (not P))` for \"P always holds\"." ); + ( "globally", + "There is no `globally`: write `(never (not P))` for \"P always holds\"." + ); + ("invariant", "There is no `invariant`: write `(never (not P))`."); + ( "eventually", + "There is no `eventually`: write `(inevitable P)` for \"every run \ + reaches P\", or `(possible P)` for \"some run can\"." ); + ( "finally", + "There is no `finally`: write `(inevitable P)` for \"every run reaches \ + P\"." ); + ( "exists", + "There is no `exists`: write `(possible P)` for \"some reachable \ + situation has P\"." ); + ("reachable", "Write `(possible P)` for \"P is reachable\"."); + ("recoverable", "Write `(live P)` for \"P can always still be reached\"."); + ] + +let arithmetic = + [ + "+"; + "-"; + "*"; + "/"; + "<"; + ">"; + "<="; + ">="; + "inc"; + "dec"; + "succ"; + "add"; + "sum"; + "count"; + "int"; + "integer"; + "nat"; + "number"; + ] + +let kernel_guards = [ "and"; "or"; "not"; "is"; "defined"; "some" ] +let modalities = [ "possible"; "never"; "live"; "inevitable" ] + +let decl_words = function + | Fault.Model -> + [ + "load"; + "schema"; + "instance"; + "form"; + "use"; + "initial"; + "transition"; + "when"; + "do"; + "type"; + "arrow"; + "equation"; + ] + | Fault.Claims -> [ "load"; "form"; "property"; "query"; "accept" ] + | Fault.Rules -> [ "load"; "form"; "relation"; "rule" ] + | Fault.Args -> [] + +(* found, and every name that would have been legal there. *) +let found_and_expected (sym : symbols) (f : Fault.t) code : + (string * string list) option = + let msg = f.err.Errors.msg in + let bt = backticked msg in + let first = match bt with x :: _ -> Some x | [] -> None in + let of_type ty = + List.filter_map (fun (t, v) -> if t = ty then Some v else None) + in + let values_of ty = of_type ty sym.values @ of_type ty sym.entities in + let with_ found cands = Option.map (fun x -> (x, cands)) found in + match code with + | "E_UNKNOWN_ARROW" -> ( + match bt with + | [ ty; a ] -> + let own = + List.filter_map + (fun (t, x) -> if t = ty then Some x else None) + sym.arrows + in + Some (a, if own <> [] then own else List.map snd sym.arrows) + | _ -> None) + | "E_UNKNOWN_ENTITY" -> with_ first (List.map snd sym.entities) + | "E_UNKNOWN_VALUE" -> ( + let ws = words msg in + match (after "value" ws, after "codomain" ws) with + | Some v, Some ty -> Some (v, values_of ty) + | _ -> None) + | "E_UNKNOWN_TYPE" -> + let found = + match bt with + | [ _; t ] when contains ~sub:"undeclared type" msg -> Some t + | x :: _ -> Some x + | [] -> None + in + with_ found + (if contains ~sub:"or arrow" msg then + sym.types @ List.map snd sym.arrows + else sym.types) + | "E_UNKNOWN_FORM" -> + (* "template of `F` mentions `X`": X is what is unknown *) + let found = + match bt with + | [ _; x ] when contains ~sub:"mentions" msg -> Some x + | _ -> first + in + with_ found (kernel_guards @ sym.forms) + | "E_UNKNOWN_MOVE" -> with_ first sym.moves + | "E_UNKNOWN_MODALITY" -> with_ first modalities + | "E_UNKNOWN_DECL" -> with_ first (decl_words f.source) + | "E_UNKNOWN_NAME" -> + with_ first + (if contains ~sub:"instance" msg then sym.instances else sym.schemas) + | "E_UNKNOWN_QUERY" -> + (* "(show wher) names no query in this file": the name is not ticked *) + let found = + match first with + | Some x -> Some x + | None -> ( + match words msg with + | "(show" :: n :: _ -> + Some (String.concat "" (String.split_on_char ')' n)) + | _ -> None) + in + with_ found sym.queries + | "E_UNKNOWN_RELATION" -> with_ first sym.relations + | _ -> None + +(* The source line at [line] with [found] replaced, nearest [col] first. *) +let is_name c = + match c with + | 'a' .. 'z' + | 'A' .. 'Z' + | '0' .. '9' + | '-' | '_' | '?' | '!' | '*' | '+' | '<' | '>' | '=' | '/' -> + true + | _ -> false + +let fix_line ~(read : string -> string option) (pos : Errors.pos) found best = + match Option.bind pos.Errors.file read with + | None -> None + | Some src -> ( + match + List.nth_opt (String.split_on_char '\n' src) (pos.Errors.line - 1) + with + | None -> None + | Some line -> + let n = String.length found and l = String.length line in + let whole i = + (i = 0 || not (is_name line.[i - 1])) + && (i + n = l || not (is_name line.[i + n])) + && String.sub line i n = found + in + let rec from i = + if i + n > l then None else if whole i then Some i else from (i + 1) + in + let at = + match from (max 0 (pos.Errors.col - 1)) with + | Some i -> Some i + | None -> from 0 + in + Option.map + (fun i -> + String.trim + (String.sub line 0 i ^ best + ^ String.sub line (i + n) (l - i - n))) + at) + +(* ── one diagnostic ──────────────────────────────────────────────────────── *) + +type t = { + code : string; + source : Fault.source; + file : string option; + line : int option; + col : int option; + message : string; + found : string option; + expected : string list; + hint : string; + fix : string option; +} + +let max_expected = 12 + +let of_fault ~read ~files (f : Fault.t) : t = + let code = classify f in + let generic = match entry code with Some e -> e.hint | None -> "" in + let fe = + match f.Fault.meant with + | Some m -> Some m + | None -> + if String.length code > 10 && String.sub code 0 10 = "E_UNKNOWN_" then + found_and_expected (harvest ~read files) f code + else None + in + let found, expected, best = + match fe with + | None -> (None, [], None) + | Some (x, cands) -> + let ranked, best = rank x cands in + (* `+` is one edit from `=`, which is no help: there are no numbers *) + let best = if List.mem x arithmetic then None else best in + (Some x, List.filteri (fun i _ -> i < max_expected) ranked, best) + in + let pos = f.err.Errors.pos in + let fix = + match (pos, found, best) with + | Some p, Some x, Some b -> fix_line ~read p x b + | _ -> None + in + let hint = + match (found, best) with + | Some x, Some b -> "Write `" ^ b ^ "` for `" ^ x ^ "`. " ^ generic + | Some x, None when code = "E_UNKNOWN_MODALITY" && List.mem_assoc x synonyms + -> + List.assoc x synonyms + | Some x, None when List.mem x arithmetic -> + "Writ has no numbers or arithmetic: a count is a ladder of entities or \ + a small enum (writ_guide idioms, Counters), and an order is a fixed \ + arrow such as `next`." + | _ -> generic + in + { + code; + source = f.source; + file = Option.bind pos (fun p -> p.Errors.file); + line = Option.map (fun p -> p.Errors.line) pos; + col = Option.map (fun p -> p.Errors.col) pos; + message = f.err.Errors.msg; + found; + expected; + hint; + fix; + } + +let see code = "writ_guide errors." ^ code + +let to_text (d : t) = + let b = Buffer.create 256 in + let line k v = + Buffer.add_string b (Printf.sprintf " %-9s %s\n" (k ^ ":") v) + in + let where = + match (d.file, d.line, d.col) with + | Some f, Some l, Some c -> Printf.sprintf "%s:%d:%d" f l c + | None, Some l, Some c -> Printf.sprintf "%d:%d" l c + | Some f, _, _ -> f + | _ -> "" + in + Buffer.add_string b + (Printf.sprintf "error %s in %s%s\n" d.code + (Fault.source_name d.source) + (if where = "" then "" else " at " ^ where)); + Buffer.add_string b (" " ^ d.message ^ "\n"); + Option.iter (line "found") d.found; + if d.expected <> [] then + line "expected" ("one of " ^ String.concat ", " d.expected); + if d.hint <> "" then line "hint" d.hint; + Option.iter (line "fix") d.fix; + line "see" (see d.code); + Buffer.contents b + +let to_json (d : t) = + let opt k = function Some v -> [ (k, Json.String v) ] | None -> [] in + let opti k = function Some v -> [ (k, Json.Int v) ] | None -> [] in + Json.Assoc + ([ + ("code", Json.String d.code); + ("source", Json.String (Fault.source_name d.source)); + ] + @ opt "file" d.file @ opti "line" d.line @ opti "col" d.col + @ [ ("message", Json.String d.message) ] + @ opt "found" d.found + @ (if d.expected = [] then [] + else + [ + ("expected", Json.List (List.map (fun s -> Json.String s) d.expected)); + ]) + @ [ ("hint", Json.String d.hint) ] + @ opt "fix" d.fix + @ [ ("see", Json.String (see d.code)) ]) + +(* ── a search cut short ──────────────────────────────────────────────────── *) + +let bound (spread : (string * int * int) list) = + List.fold_left + (fun acc (_, _, dom) -> acc *. float_of_int (max 1 dom)) + 1.0 spread + +let show_bound = Writ_runtime.Space.show_bound + +let limit_text (l : Fault.limit) = + let c = l.Fault.cutoff in + let b = Buffer.create 512 in + let add = Buffer.add_string b in + (match c.Writ_runtime.Space.reason with + | `Cap n -> + add + (Printf.sprintf "limit E_STATE_LIMIT: stopped at max_situations = %d\n" + n) + | `Timeout t -> + add + (Printf.sprintf "limit E_STATE_LIMIT: stopped at timeout = %.0f ms\n" + (t *. 1000.))); + add + (Printf.sprintf " explored: %d situations, %d edges, not finished\n" + c.explored c.edges_seen); + add + (Printf.sprintf + " bound: at most %s situations (the product of every mutable \ + cell's domain)\n" + (show_bound (bound c.spread))); + if l.undecided <> [] then + add + (" undecided: " + ^ String.concat ", " l.undecided + ^ " (nothing is decided on a partial space)\n"); + add " growth, by distinct values seen per cell (of its domain):\n"; + List.iteri + (fun i (cell, seen, dom) -> + if i < 8 then add (Printf.sprintf " %-24s %d of %d\n" cell seen dom)) + c.spread; + (match entry "E_STATE_LIMIT" with + | Some e -> add (" hint: " ^ e.hint ^ "\n") + | None -> ()); + add " see: writ_guide idioms (Abstraction), errors.E_STATE_LIMIT\n"; + Buffer.contents b + +let limit_json (l : Fault.limit) = + let c = l.Fault.cutoff in + let reason, value = + match c.Writ_runtime.Space.reason with + | `Cap n -> ("max_situations", Json.Int n) + | `Timeout t -> ("timeout_ms", Json.Int (int_of_float (t *. 1000.))) + in + Json.Assoc + [ + ("ok", Json.Bool false); + ( "limit", + Json.Assoc + [ + ("code", Json.String "E_STATE_LIMIT"); + ("reason", Json.String reason); + ("value", value); + ("explored", Json.Int c.explored); + ("edges", Json.Int c.edges_seen); + ("bound", Json.String (show_bound (bound c.spread))); + ( "undecided", + Json.List (List.map (fun s -> Json.String s) l.undecided) ); + ( "growth", + Json.List + (List.map + (fun (cell, seen, dom) -> + Json.Assoc + [ + ("cell", Json.String cell); + ("seen", Json.Int seen); + ("domain", Json.Int dom); + ]) + c.spread) ); + ("see", Json.String "writ_guide idioms"); + ] ); + ] + +(* ── the reply ───────────────────────────────────────────────────────────── *) + +let render ~json ~read ~files (f : Fault.failure) = + match f with + | Fault.Limit l -> + if json then Json.to_string (limit_json l) else limit_text l + | Fault.Bad faults -> + let ds = List.map (of_fault ~read ~files) faults in + if json then + Json.to_string + (Json.Assoc + [ + ("ok", Json.Bool false); + ("errors", Json.List (List.map to_json ds)); + ]) + else String.concat "\n" (List.map to_text ds) diff --git a/tooling/mcp/lib/dune b/tooling/mcp/lib/dune index c34f662..e7c058a 100644 --- a/tooling/mcp/lib/dune +++ b/tooling/mcp/lib/dune @@ -15,3 +15,14 @@ version.ml (echo "let v =\n let raw = \"%{version:writ}\" in\n if String.length raw > 1 && raw.[0] = 'v' && raw.[1] >= '0' && raw.[1] <= '9'\n then String.sub raw 1 (String.length raw - 1)\n else raw\n")))) + +; The writ_guide topics, from ../guide/*.md (tooling/mcp/gen/embed.ml). + +(rule + (targets guide_data.ml) + (deps + (glob_files ../guide/*.md)) + (action + (with-stdout-to + guide_data.ml + (run ../gen/embed.exe %{deps})))) diff --git a/tooling/mcp/lib/fault.ml b/tooling/mcp/lib/fault.ml new file mode 100644 index 0000000..b3e1d4d --- /dev/null +++ b/tooling/mcp/lib/fault.ml @@ -0,0 +1,48 @@ +(* Copyright (C) 2026 Alex Kunich *) +(* SPDX-License-Identifier: AGPL-3.0-or-later *) + +(* Why a tool call produced no answer. Kept as data, not a string, so the + server can render it as prose or JSON and attach a code, a suggestion and + a fix (Diagnose). *) + +open Writ_data + +type source = Model | Claims | Rules | Args + +let source_name = function + | Model -> "model" + | Claims -> "claims" + | Rules -> "rules" + | Args -> "arguments" + +(* [code] is set where the tool knows it; otherwise Diagnose classifies the + engine's message. [meant] is (found, legal alternatives) when the tool + knows them; otherwise Diagnose reads the sources for them. *) +type t = { + source : source; + code : string option; + err : Errors.t; + meant : (string * string list) option; +} + +(* A search stopped by a limit: not wrong, only unfinished. *) +type limit = { + cutoff : Writ_runtime.Space.cutoff; + undecided : string list; (** properties the claims ask, none decided *) +} + +(* [Bad] holds one error per file at most: each front end stops at its first. *) +type failure = Bad of t list | Limit of limit + +let bad ?code ?meant source err = Bad [ { source; code; err; meant } ] + +let arg code msg = + Bad + [ + { + source = Args; + code = Some code; + err = { pos = None; msg }; + meant = None; + }; + ] diff --git a/tooling/mcp/lib/guide.ml b/tooling/mcp/lib/guide.ml new file mode 100644 index 0000000..d6b44ef --- /dev/null +++ b/tooling/mcp/lib/guide.ml @@ -0,0 +1,93 @@ +(* Copyright (C) 2026 Alex Kunich *) +(* SPDX-License-Identifier: AGPL-3.0-or-later *) + +(* The writ_guide topics: the language as an LLM client needs it to write a + model unaided. Written topics are ../guide/*.md, embedded at build time + (Guide_data); `errors` and `errors.` are generated from Diagnose's + table, so a code cannot exist without its topic. test_mcp checks every + example in them still behaves as the text says. *) + +let example_block = function + | Diagnose.Model s -> "```lisp\n; model (model_source)\n" ^ s ^ "```\n" + | Diagnose.Claims s -> + "```lisp\n; claims (claims_source), against the model below\n" ^ s + ^ "```\n" + | Diagnose.Rules s -> + "```lisp\n; rules (rules_source), against the model below\n" ^ s ^ "```\n" + | Diagnose.Call s -> "```\n" ^ s ^ "\n```\n" + +let needs_base = function + | Diagnose.Claims _ | Diagnose.Rules _ -> true + | _ -> false + +let error_topic (e : Diagnose.entry) = + "**Cause.** " ^ e.cause ^ "\n\n**Fix.** " ^ e.hint ^ "\n\n**Wrong:**\n\n" + ^ example_block e.wrong ^ "\n**Right:**\n\n" ^ example_block e.right + ^ + if needs_base e.wrong then + "\nThe model they are checked against:\n\n```lisp\n" ^ Diagnose.base + ^ "```\n" + else "" + +let errors_index () = + "Every error a writ tool returns carries one of these codes, with `found`, \ + `expected`, `hint` and, for a misspelt name, a corrected `fix` line. Ask \ + for `errors.` for a wrong and a right example.\n\n" + ^ String.concat "\n" + (List.map + (fun (e : Diagnose.entry) -> "- `" ^ e.code ^ "`: " ^ e.cause) + Diagnose.codes) + ^ "\n" + +let topics () : (string * string) list = + Guide_data.topics + @ [ ("errors", errors_index ()) ] + @ List.map + (fun (e : Diagnose.entry) -> ("errors." ^ e.code, error_topic e)) + Diagnose.codes + +let names () = List.map fst (topics ()) + +(* A topic's one-line summary: its first non-blank line. *) +let summary body = + match + List.find_opt + (fun l -> String.trim l <> "") + (String.split_on_char '\n' body) + with + | Some l -> String.trim l + | None -> "" + +let unknown_listing bad = + "# unknown topic" + ^ (if List.length bad > 1 then "s" else "") + ^ ": " ^ String.concat ", " bad ^ "\n\nValid topics:\n\n" + ^ String.concat "\n" + (List.filter_map + (fun (n, _) -> + if String.length n > 7 && String.sub n 0 7 = "errors." then None + else Some ("- `" ^ n ^ "`")) + (topics ())) + ^ "\n- `errors.`, one per code listed in `errors`\n" + +(* One `# topic.` section per item, in the order asked; unknown names + get the valid list rather than an error. A trailing `topic.` is accepted, + since clients echo the heading back. *) +let get (items : string list) : string = + let all = topics () in + let strip n = + if String.length n > 6 && String.sub n 0 6 = "topic." then + String.sub n 6 (String.length n - 6) + else n + in + let items = List.map (fun n -> strip (String.trim n)) items in + let items = if items = [] then [ "index" ] else items in + let found, bad = + List.partition_map + (fun n -> + match List.assoc_opt n all with + | Some body -> Left ("# topic." ^ n ^ "\n\n" ^ body) + | None -> Right n) + items + in + String.concat "\n\n" (found @ if bad = [] then [] else [ unknown_listing bad ]) diff --git a/tooling/mcp/lib/server.ml b/tooling/mcp/lib/server.ml index be54ce8..0fd8fde 100644 --- a/tooling/mcp/lib/server.ml +++ b/tooling/mcp/lib/server.ml @@ -2,13 +2,20 @@ (* SPDX-License-Identifier: AGPL-3.0-or-later *) (* The Model Context Protocol (JSON-RPC 2.0) as a pure function: one message - in, at most one out, so it can be unit-tested without a process. A tools-only - server: [initialize], [tools/list], [tools/call], [ping], and notifications. + in, at most one out, so it can be unit-tested without a process. Methods: + [initialize] (with [instructions]), [tools/*], [resources/*] (the guide, + as writ://guide/), [prompts/*] (one authoring prompt), [ping], and + notifications. A tool that fails (a parse error, an undeclared relation) returns a successful result with [isError: true], so the agent sees the message and can fix its input; a JSON-RPC error would go only to the client. Protocol faults - such as an unknown method or tool stay JSON-RPC errors. *) + such as an unknown method or tool stay JSON-RPC errors. + + Every model, claims and rules argument is a path OR inline source. Inline + source is served from memory under a virtual file name (NAME.writ, + NAME.claims, NAME.rules) by layering it over the injected resolver, so a + client that cannot write to the server's filesystem can still author. *) let protocol_version = "2024-11-05" @@ -42,7 +49,6 @@ let text ?(is_error = false) s = ] let str j k = Option.bind (Json.member k j) Json.to_string_opt -let int_ j k = Option.bind (Json.member k j) Json.to_int_opt let bool_ j k = match Json.member k j with Some (Json.Bool b) -> Some b | _ -> None @@ -54,6 +60,39 @@ let args_of j k = Some (List.map (function Json.String s -> Some s | _ -> None) xs) | _ -> None +(* ── limits ──────────────────────────────────────────────────────────────── *) + +let max_source = 256 * 1024 +let default_max = Writ_runtime.Space.cap +let ceiling_max = 2_000_000 +let default_timeout_ms = 60_000 +let ceiling_timeout_ms = 600_000 + +(* ── the R4 example: one whole model and its claims ──────────────────────── *) + +let example_model = + "(load \"stdlib.writ\")\n\ + (schema house\n\ + \ (type pos (shut open locked))\n\ + \ (type holder (nobody guest))\n\ + \ (type door (arrow at (to pos)) (arrow key (to holder)))\n\ + \ (equation locked-means-held (not (and (is door.at locked) (is door.key \ + nobody)))))\n\ + (instance start house (door d (at shut) (key guest)))\n\ + (use house)\n\ + (initial start)\n\ + (transition open (when (is d.at shut)) (do (set d.at open)))\n\ + (transition close (when (is d.at open)) (do (set d.at shut)))\n\ + (transition lock (when (is d.at shut)) (do (set d.at locked)))\n\ + (transition drop-key (when (is d.key guest)) (do (set d.key nobody)))\n" + +let example_claims = + "(property can-open \"the door can be opened\" (possible (is d.at open)))\n\ + (property never-trapped \"it can always be opened again\" (live (is d.at \ + open)))\n\ + (property never-lost \"the key is never lost while locked\" (never (and (is \ + d.at locked) (is d.key nobody))))\n" + (* ── the tools ───────────────────────────────────────────────────────────── *) let obj props required = @@ -69,82 +108,179 @@ let p name ty desc = Json.Assoc [ ("type", Json.String ty); ("description", Json.String desc) ] ) +let src_p name what = + ( name, + Json.Assoc + [ + ("type", Json.String "string"); + ("maxLength", Json.Int max_source); + ( "description", + Json.String + ("The " ^ what + ^ " as inline source text, instead of a path (exactly one of the \ + two). At most 256 KB.") ); + ] ) + let json_p = p "json" "boolean" "Answer as the JSON object `writ … --json` prints (docs/json.md) instead \ - of prose: witnesses carry the situation each move lands in." + of prose: witnesses carry the situation each move lands in; errors are \ + objects with code, line, col, found, expected, hint, fix." + +let name_p = + p "model_name" "string" + "A name for an inline model (letters, digits, - and _). Errors cite it as \ + NAME.writ; writ_check keeps revision history per name, so give the same \ + name to every version of one system. History lasts while this server \ + runs. Default: `model`, with no history." + +let model_ps = + [ + p "model" "string" "Path to the .writ model."; + src_p "model_source" ".writ model"; + name_p; + ] + +let claims_ps what = + [ + p "claims" "string" + ("Path to a .claims file" ^ what + ^ ". Under --claims-dir it is read from that directory by basename."); + src_p "claims_source" ".claims file"; + ] + +let limit_ps = + [ + p "max_situations" "integer" + (Printf.sprintf + "Stop exploring after this many situations (default %d, at most %d)." + default_max ceiling_max); + p "timeout_ms" "integer" + (Printf.sprintf "Stop after this much CPU time (default %d, at most %d)." + default_timeout_ms ceiling_timeout_ms); + ] + +let at_list_p = + ( "at", + Json.Assoc + [ + ("type", Json.String "array"); + ("items", Json.Assoc [ ("type", Json.String "integer") ]); + ( "description", + Json.String + "Situation indices to show; omit for the initial situation." ); + ] ) + +let check_description = + "Build a Writ model's situation space and report it: how many situations and \ + edges, the declared gaps, the dead ends, and whether any law can be broken. \ + With claims it also answers every property — `holds` with a shortest \ + witness route, `fails` with the shortest counterexample — and runs every \ + query. This is the verb to reach for first; the witness under a holding \ + `possible` IS a solution. A property reported `n/a` names structure the \ + model lacks: treat it as a FAILURE, never a pass. When the same claims were \ + checked before (same path, or same model_name), the answer ends with a \ + `revision:` block saying which guarantees this model LOST against the \ + previous one.\n\n\ + Pass `model` (a path) or `model_source` (the text); likewise `claims` or \ + `claims_source`. Inline claims are never found as a sibling file: pass \ + claims_source explicitly. Limits: the search stops at max_situations \ + (default 200000) or timeout_ms (default 60000) and returns E_STATE_LIMIT \ + with the cells driving the growth; nothing is decided then.\n\n\ + A complete model (model_source):\n\n" ^ example_model + ^ "\nand its claims (claims_source):\n\n" ^ example_claims + ^ "\n\ + It reports can-open holds (witness: open), never-trapped fails (stuck at \ + the locked door: no move unlocks it), and never-lost fails (lock, \ + drop-key). More: writ_guide." let descriptors = [ - ( "writ_check", - "Build a Writ model's situation space and report it: how many situations \ - and edges, the declared gaps, the dead ends, and whether any law can be \ - broken. With a .claims file it also answers every property — `holds` \ - with a shortest witness route, `fails` with the shortest counterexample \ - — and runs every query. This is the verb to reach for first; the \ - witness under a holding `possible` IS a solution. A property reported \ - `n/a` names structure the model lacks: treat it as a FAILURE, never a \ - pass. When the same claims file was checked before, the answer ends \ - with a `revision:` block saying which guarantees this model LOST \ - against the previous one — an edit that makes one property pass by \ - losing another is reported in the same reply.", + ( "writ_guide", + "Writ language guide. Call writ_guide({items:[\"index\"]}) BEFORE \ + writing any .writ, .claims or .rules source. Several topics per call is \ + fine: syntax.model, syntax.claims, syntax.rules, semantics, idioms, \ + examples., errors..", obj [ - p "model" "string" "Path to the .writ model."; - p "claims" "string" - "Optional path to a .claims file of properties and queries to \ - answer. If the server was started with --claims-dir, the file is \ - read from that directory by its basename, whatever path is given."; - json_p; - ] - [ "model" ] ); - ( "writ_show", - "Print what a situation IS, by the index a witness step, a derived row \ - or a `stuck at:` line names: its cells, the fewest moves to it, and \ - every move out. Follow a witness with this rather than guessing what \ - `#17` holds.", - obj - [ - p "model" "string" "Path to the .writ model."; - ( "at", + ( "items", Json.Assoc [ ("type", Json.String "array"); - ("items", Json.Assoc [ ("type", Json.String "integer") ]); + ("items", Json.Assoc [ ("type", Json.String "string") ]); ( "description", Json.String - "Situation indices to show; omit for the initial situation." - ); + "Topic names, e.g. index, syntax.model, syntax.claims, \ + syntax.rules, semantics, idioms, examples., \ + errors." ); ] ); - json_p; ] - [ "model" ] ); + [ "items" ] ); + ( "writ_validate", + "Parse and type-check a model and, optionally, its claims and rules, \ + WITHOUT building the space: fast, for any size. On success, what the \ + sources declare (types with their values or entities, arrows, laws, \ + moves, the mutable cells and the most situations they allow, properties \ + with their kinds, queries, relations with arity), so you can confirm \ + the model means what you intended. On failure, the first error of each \ + file with a code, position, found/expected, a hint and, for a misspelt \ + name, the corrected line. Call it before writ_check.", + obj + (model_ps @ claims_ps " to type-check" + @ [ + p "rules" "string" "Path to a .rules file to type-check."; + src_p "rules_source" ".rules file"; + json_p; + ]) + [] ); + ( "writ_check", + check_description, + obj + (model_ps + @ claims_ps " of properties and queries to answer" + @ limit_ps @ [ json_p ]) + [] ); + ( "writ_show", + "Print what a situation IS, by the index a witness step, a derived row \ + or a `stuck at:` line names: its cells, the fewest moves to it, and \ + every move out. Follow a witness with this rather than guessing what \ + `#17` holds. Indices are stable for the same source (the search is \ + deterministic) but NOT across edits: pass the exact source the index \ + came from.", + obj (model_ps @ [ at_list_p ] @ limit_ps @ [ json_p ]) [] ); ( "writ_compare", - "Which guarantees an edit kept, LOST and gained: the old model's sibling \ - .claims put to both models. Price your own edit with this before \ - calling it done — a LOST row carries the route through the new model \ - that breaks the guarantee.", + "Which guarantees an edit kept, LOST and gained: the old model's claims \ + put to both models, matched by property name. A LOST row (passes \ + before; fails or is n/a after) carries the route through the new model \ + that breaks the guarantee. Price every edit with this before calling it \ + done.", obj - [ - p "old_model" "string" "Path to the model before the edit."; - p "new_model" "string" "Path to the model after it."; - json_p; - ] - [ "old_model"; "new_model" ] ); + ([ + p "old_model" "string" "Path to the model before the edit."; + src_p "old_model_source" "model before the edit"; + p "new_model" "string" "Path to the model after it."; + src_p "new_model_source" "model after the edit"; + ] + @ claims_ps + " to put to both (default: the old model's sibling .claims; for an \ + inline old model, pass claims or claims_source)" + @ limit_ps @ [ json_p ]) + [] ); ( "writ_query", - "Run ONE named query from the model's sibling .claims file, optionally \ - at a situation other than the initial one. Use when writ_check's full \ - report is more than you need.", + "Run ONE named query from the claims, optionally at a situation other \ + than the initial one. Use when writ_check's full report is more than \ + you need.", obj - [ - p "model" "string" "Path to the .writ model."; - p "name" "string" "The query's name, as written in the .claims file."; - p "at" "integer" - "Optional index into the enumerated space; defaults to the initial \ - situation (0)."; - json_p; - ] - [ "model"; "name" ] ); + (model_ps + @ claims_ps " holding the query (default: the model's sibling .claims)" + @ [ + p "name" "string" "The query's name, as written in the claims."; + p "at" "integer" + "Optional index into the enumerated space; defaults to the \ + initial situation (0)."; + ] + @ limit_ps @ [ json_p ]) + [ "name" ] ); ( "writ_derive", "Answer a relation from a .rules file over the model's space. Leave an \ argument null to ask for every value it can take. With why=true you get \ @@ -152,24 +288,25 @@ let descriptors = fact, down to the model facts it rests on — which needs every argument \ given.", obj - [ - p "model" "string" "Path to the .writ model."; - p "rules" "string" "Path to the .rules file."; - p "relation" "string" "The relation to ask about."; - ( "args", - Json.Assoc - [ - ("type", Json.String "array"); - ("items", Json.Assoc [ ("type", Json.String "string") ]); - ( "description", - Json.String - "One entry per column; null leaves that column open. Omit \ - to leave all of them open." ); - ] ); - p "why" "boolean" "Return the derivation tree instead of the rows."; - json_p; - ] - [ "model"; "rules"; "relation" ] ); + (model_ps + @ [ + p "rules" "string" "Path to the .rules file."; + src_p "rules_source" ".rules file"; + p "relation" "string" "The relation to ask about."; + ( "args", + Json.Assoc + [ + ("type", Json.String "array"); + ("items", Json.Assoc [ ("type", Json.String "string") ]); + ( "description", + Json.String + "One entry per column; null leaves that column open. \ + Omit to leave all of them open." ); + ] ); + p "why" "boolean" "Return the derivation tree instead of the rows."; + ] + @ limit_ps @ [ json_p ]) + [ "relation" ] ); ] let tool_list = @@ -184,77 +321,397 @@ let tool_list = ("name", Json.String n); ("description", Json.String d); ("inputSchema", schema); + ( "annotations", + Json.Assoc [ ("readOnlyHint", Json.Bool true) ] ); ]) descriptors) ); ] -(* ── dispatch ────────────────────────────────────────────────────────────── *) +(* ── instructions, resources, prompt ─────────────────────────────────────── *) + +let instructions = + "Writ is an explicit-state model checker for finite discrete systems: it \ + enumerates every reachable situation of a rule-governed world and answers \ + with a concrete route as evidence.\n\n\ + Before writing any Writ source, call writ_guide with [\"index\"].\n\n\ + Workflow: writ_validate (parse and type-check, instant) -> writ_check \ + (build the space, answer the claims) -> writ_show on any index a witness \ + names -> writ_compare after every edit, old model against new. Sources go \ + inline (model_source, claims_source, rules_source) or as paths.\n\n\ + A property reported n/a is a FAILURE, never a pass: it names structure the \ + model lacks. Do not make a check green by making its question unaskable." + +let guide_uri n = "writ://guide/" ^ n + +let resource_list () = + Json.Assoc + [ + ( "resources", + Json.List + (List.map + (fun (n, body) -> + Json.Assoc + [ + ("uri", Json.String (guide_uri n)); + ("name", Json.String ("writ guide: " ^ n)); + ("description", Json.String (Guide.summary body)); + ("mimeType", Json.String "text/markdown"); + ]) + (Guide.topics ())) ); + ] + +let prompt_name = "writ_model_system" + +let prompt_list = + Json.Assoc + [ + ( "prompts", + Json.List + [ + Json.Assoc + [ + ("name", Json.String prompt_name); + ( "description", + Json.String + "Model a system described in plain language and check it \ + with writ." ); + ( "arguments", + Json.List + [ + Json.Assoc + [ + ("name", Json.String "description"); + ( "description", + Json.String "The system and what must hold of it." + ); + ("required", Json.Bool true); + ]; + ] ); + ]; + ] ); + ] + +let prompt_text description = + "Model this system in Writ and check it:\n\n" ^ description + ^ "\n\n\ + 1. Call writ_guide with [\"index\", \"semantics\", \"idioms\"] and read \ + them.\n\ + 2. List the requirements in plain words. For each, choose the property \ + kind from semantics: never (it must not happen), possible (it can \ + happen), live (it can always still happen), inevitable (it must happen).\n\ + 3. Draft the model (model_source) and the claims (claims_source). Keep \ + the space small: estimate the product of every mutable cell's domain.\n\ + 4. Call writ_validate until it answers ok; check its summary says what \ + you meant.\n\ + 5. Call writ_check. For each failing property, writ_show the stuck or \ + last situation and explain the counterexample in the system's own terms.\n\ + 6. After any fix, call writ_compare (old model against new) and report \ + anything LOST." + +(* ── arguments ───────────────────────────────────────────────────────────── *) + +let ( let* ) = Result.bind + +(* One path-or-source argument: [Ok None] when neither is given and it is + optional. Inline text is added to [overlay] under [virtual_]. *) +let source_arg a ~path ~src ~virtual_ ~required overlay = + match (str a path, str a src) with + | Some _, Some _ -> + Error + (Fault.arg "E_ARG_CONFLICT" + ("pass `" ^ path ^ "` or `" ^ src ^ "`, not both")) + | None, None -> + if required then + Error + (Fault.arg "E_ARG_CONFLICT" + ("pass `" ^ path ^ "` (a path) or `" ^ src ^ "` (the text)")) + else Ok None + | Some f, None -> Ok (Some f) + | None, Some text -> + if String.length text > max_source then + Error + (Fault.arg "E_SOURCE_TOO_LARGE" + (Printf.sprintf "`%s` is %d bytes; the limit is %d" src + (String.length text) max_source)) + else ( + overlay := (virtual_, text) :: !overlay; + Ok (Some virtual_)) + +(* Inline text is served under this prefix, which no (load …) names: so an + inline model can never stand in for a library a pinned claims file loads. *) +let virtual_prefix = "inline:" + +let valid_name n = + n <> "" && n <> "stdlib" + && String.for_all + (function + | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '-' | '_' -> true | _ -> false) + n + +let int_arg a k ~default ~ceiling = + match Json.member k a with + | None | Some Json.Null -> Ok default + | Some (Json.Int n) when n >= 1 && n <= ceiling -> Ok n + | Some _ -> + Error + (Fault.arg "E_ARG_INVALID" + (Printf.sprintf "`%s` must be an integer from 1 to %d" k ceiling)) + +let limits_of a = + let* max = + int_arg a "max_situations" ~default:default_max ~ceiling:ceiling_max + in + let* ms = + int_arg a "timeout_ms" ~default:default_timeout_ms + ~ceiling:ceiling_timeout_ms + in + Ok { Tools.max; timeout = Some (float_of_int ms /. 1000.) } (* [writ_show] indices: a list, or a single integer. *) let ints_of j k = match Json.member k j with - | Some (Json.List xs) -> List.filter_map Json.to_int_opt xs - | Some (Json.Int i) -> [ i ] - | _ -> [] + | Some (Json.List xs) -> + let is = List.filter_map Json.to_int_opt xs in + if List.length is = List.length xs then Ok is + else Error (Fault.arg "E_ARG_INVALID" ("`" ^ k ^ "` must be integers")) + | Some (Json.Int i) -> Ok [ i ] + | None | Some Json.Null -> Ok [] + | Some _ -> Error (Fault.arg "E_ARG_INVALID" ("`" ^ k ^ "` must be integers")) + +let need a k = + match str a k with + | Some s -> Ok s + | None -> Error (Fault.arg "E_ARG_INVALID" ("missing `" ^ k ^ "`")) + +(* ── dispatch ────────────────────────────────────────────────────────────── *) let call ?certify ?(version = "") ~resolve ?(pinned = None) ?(memory = Tools.remember) name (a : Json.t) = - let need k = - match str a k with Some s -> Ok s | None -> Error ("missing `" ^ k ^ "`") - in let json = Option.value (bool_ a "json") ~default:false in - let ( let* ) = Result.bind in - match name with - | "writ_check" -> - let* model = need "model" in - Tools.check ~json ~pinned ~memory ?certify ~version ~resolve ~model - ~claims:(str a "claims") () - | "writ_show" -> - let* model = need "model" in - Tools.show ~json ~resolve ~model ~at:(ints_of a "at") () - | "writ_compare" -> - let* old_model = need "old_model" in - let* new_model = need "new_model" in - Tools.compare ~json ~pinned ~resolve ~old_model ~new_model () - | "writ_query" -> - let* model = need "model" in - let* n = need "name" in - Tools.query ~json ~pinned ~resolve ~model ~name:n ~at:(int_ a "at") () - | "writ_derive" -> - let* model = need "model" in - let* rules = need "rules" in - let* relation = need "relation" in - Tools.derive ~json ~resolve ~model ~rules ~relation - ~args:(args_of a "args") - ~why:(Option.value (bool_ a "why") ~default:false) - () - (* Unreachable: [handle] rejects unknown names first. *) - | _ -> Error ("no such tool: " ^ name) + let overlay = ref [] in + (* Inline text first, by basename, then whatever [resolve] finds. *) + let resolve' base = + let r = resolve base in + fun n -> match List.assoc_opt n !overlay with Some s -> Ok s | None -> r n + in + let read f = + match (resolve' f) (Filename.basename f) with + | Ok s -> Some s + | Error _ -> None + in + let files = ref [] in + let note = function Some f -> files := f :: !files | None -> () in + let result = + let* mname = + match str a "model_name" with + | None -> Ok None + | Some n when valid_name n -> Ok (Some n) + | Some n -> + Error + (Fault.arg "E_ARG_INVALID" + ("`model_name` `" ^ n + ^ "` must be letters, digits, - and _ (and not `stdlib`)")) + in + let stem = Option.value mname ~default:"model" in + let src ?(stem = stem) ?(required = false) path src ext = + let* f = + source_arg a ~path ~src + ~virtual_:(virtual_prefix ^ stem ^ ext) + ~required overlay + in + note f; + Ok f + in + let model () = + let* m = src ~required:true "model" "model_source" ".writ" in + Ok (Option.get m) + in + (* Inline claims would let the agent write its own questions. *) + let claims () = + if pinned <> None && str a "claims_source" <> None then + Error + (Fault.arg "E_CLAIMS_PINNED" + "this server pins claims (--claims-dir): pass `claims` as a path, \ + not `claims_source`") + else src "claims" "claims_source" ".claims" + in + let inline s = str a s <> None in + (* An unnamed inline model or claims keeps no history: unrelated drafts + would otherwise be compared with each other. History is per name. *) + let memory = + if (inline "model_source" || inline "claims_source") && mname = None then + Hashtbl.create 1 + else memory + in + (* Inline sources have no sibling .claims to fall back on. *) + let claims_needed f = + let* c = claims () in + if c = None && inline f then + Error + (Fault.arg "E_ARG_INVALID" + ("an inline `" ^ f + ^ "` has no sibling .claims file: pass `claims` or `claims_source`" + )) + else Ok c + in + match name with + | "writ_guide" -> + let items = + match Json.member "items" a with + | Some (Json.List xs) -> List.filter_map Json.to_string_opt xs + | Some (Json.String s) -> [ s ] + | _ -> [] + in + Ok (Guide.get items) + | "writ_validate" -> + let* model = model () in + let* claims = claims () in + let* rules = src "rules" "rules_source" ".rules" in + Tools.validate ~json ~pinned ~resolve:resolve' ~model ~claims ~rules () + | "writ_check" -> + let* model = model () in + let* claims = claims () in + let* limits = limits_of a in + Tools.check ~json ~pinned ~memory ?memory_key:mname ?certify ~version + ~limits ~resolve:resolve' ~model ~claims () + | "writ_show" -> + let* model = model () in + let* limits = limits_of a in + let* at = ints_of a "at" in + Tools.show ~json ~limits ~resolve:resolve' ~model ~at () + | "writ_compare" -> + let* old_model = + src ~stem:(stem ^ "-old") ~required:true "old_model" + "old_model_source" ".writ" + in + let* new_model = + src ~stem:(stem ^ "-new") ~required:true "new_model" + "new_model_source" ".writ" + in + let* claims = claims_needed "old_model_source" in + let* limits = limits_of a in + Tools.compare ~json ~pinned ~limits ?claims ~resolve:resolve' + ~old_model:(Option.get old_model) ~new_model:(Option.get new_model) () + | "writ_query" -> + let* model = model () in + let* claims = claims_needed "model_source" in + let* n = need a "name" in + let* limits = limits_of a in + let* at = + match Json.member "at" a with + | None | Some Json.Null -> Ok None + | Some (Json.Int i) -> Ok (Some i) + | Some _ -> + Error (Fault.arg "E_ARG_INVALID" "`at` must be an integer") + in + Tools.query ~json ~pinned ~limits ?claims ~resolve:resolve' ~model + ~name:n ~at () + | "writ_derive" -> + let* model = model () in + let* rules = src ~required:true "rules" "rules_source" ".rules" in + let* relation = need a "relation" in + let* limits = limits_of a in + Tools.derive ~json ~limits ~resolve:resolve' ~model + ~rules:(Option.get rules) ~relation ~args:(args_of a "args") + ~why:(Option.value (bool_ a "why") ~default:false) + () + (* Unreachable: [handle] rejects unknown names first. *) + | _ -> Error (Fault.arg "E_OTHER" ("no such tool: " ^ name)) + in + Result.map_error (Diagnose.render ~json ~read ~files:(List.rev !files)) result (* [certify] runs writ-cert and, like [resolve], is injected by the binary because it is I/O. Without it, checks are not certified. *) let handle ~resolve ?(pinned = None) ?(memory = Tools.remember) ?certify ~version (msg : Json.t) : Json.t option = let id = Option.value (Json.member "id" msg) ~default:Json.Null in + let params = Option.value (Json.member "params" msg) ~default:Json.Null in match str msg "method" with | Some "initialize" -> ok id (Json.Assoc [ ("protocolVersion", Json.String protocol_version); - ("capabilities", Json.Assoc [ ("tools", Json.Assoc []) ]); + ( "capabilities", + Json.Assoc + [ + ("tools", Json.Assoc []); + ("resources", Json.Assoc []); + ("prompts", Json.Assoc []); + ] ); ( "serverInfo", Json.Assoc [ ("name", Json.String "writ"); ("version", Json.String version); ] ); + ("instructions", Json.String instructions); ]) (* Notifications expect no reply. *) | Some "notifications/initialized" | Some "notifications/cancelled" -> None | Some "ping" -> ok id (Json.Assoc []) | Some "tools/list" -> ok id tool_list + | Some "resources/list" -> ok id (resource_list ()) + | Some "resources/templates/list" -> + ok id (Json.Assoc [ ("resourceTemplates", Json.List []) ]) + | Some "resources/read" -> ( + let prefix = guide_uri "" in + let lp = String.length prefix in + match str params "uri" with + | Some u when String.length u > lp && String.sub u 0 lp = prefix -> ( + let n = String.sub u lp (String.length u - lp) in + match List.assoc_opt n (Guide.topics ()) with + | Some body -> + ok id + (Json.Assoc + [ + ( "contents", + Json.List + [ + Json.Assoc + [ + ("uri", Json.String u); + ("mimeType", Json.String "text/markdown"); + ("text", Json.String body); + ]; + ] ); + ]) + | None -> error id (-32002) ("no such resource: " ^ u)) + | Some u -> error id (-32002) ("no such resource: " ^ u) + | None -> error id (-32602) "resources/read needs a `uri`") + | Some "prompts/list" -> ok id prompt_list + | Some "prompts/get" -> ( + match str params "name" with + | Some n when n = prompt_name -> + let args = + Option.value (Json.member "arguments" params) ~default:Json.Null + in + let d = + Option.value (str args "description") + ~default:"(describe the system here)" + in + ok id + (Json.Assoc + [ + ( "description", + Json.String "Model a system in Writ and check it." ); + ( "messages", + Json.List + [ + Json.Assoc + [ + ("role", Json.String "user"); + ( "content", + Json.Assoc + [ + ("type", Json.String "text"); + ("text", Json.String (prompt_text d)); + ] ); + ]; + ] ); + ]) + | Some n -> error id (-32602) ("no such prompt: " ^ n) + | None -> error id (-32602) "prompts/get needs a `name`") | Some "tools/call" -> ( - let params = Option.value (Json.member "params" msg) ~default:Json.Null in match str params "name" with | None -> error id (-32602) "tools/call needs a `name`" (* An unknown tool is a protocol fault (see the header). *) diff --git a/tooling/mcp/lib/tools.ml b/tooling/mcp/lib/tools.ml index 2a40973..f2e8654 100644 --- a/tooling/mcp/lib/tools.ml +++ b/tooling/mcp/lib/tools.ml @@ -2,7 +2,8 @@ (* SPDX-License-Identifier: AGPL-3.0-or-later *) (* The writ verbs as tool calls. Each returns a [result] instead of exiting as - [Cli_io] does, so the agent gets the error message and can fix its input. + [Cli_io] does, so the agent gets the error and can fix its input; a failure + is a [Fault.failure], which [Diagnose] turns into a coded diagnostic. Loading, checking and reporting are the same engine code `writ check` uses. [resolve] maps the file being read to its resolver, since loads search the @@ -14,13 +15,208 @@ open Writ_runtime let ( let* ) = Result.bind +(* How far a search may go before it is cut off ([Fault.Limit]). *) +type limits = { max : int; timeout : float option } + +let default_limits = { max = Space.cap; timeout = None } + let load resolve path = - Loader.read_model (resolve path) path |> Result.map_error Errors.to_string + Loader.read_model (resolve path) path + |> Result.map_error (fun e -> Fault.bad Fault.Model e) -let build path m = Space.build m |> Result.map_error (fun e -> path ^ ": " ^ e) +(* An instance that breaks its own schema surfaces here, not at parse, and + carries no position: the message names the cell instead. *) +let model_fault path e = + Fault.bad Fault.Model { Errors.pos = None; msg = path ^ ": " ^ e } + +let build ?(limits = default_limits) ?(undecided = []) path m = + match Space.explore ~max:limits.max ?timeout:limits.timeout m with + | Ok sp -> Ok sp + | Error (`Model e) -> Error (model_fault path e) + | Error (`Cutoff cutoff) -> Error (Fault.Limit { cutoff; undecided }) let read_claims resolve m path = - Loader.read_claims (resolve path) m path |> Result.map_error Errors.to_string + Loader.read_claims (resolve path) m path + |> Result.map_error (fun e -> Fault.bad Fault.Claims e) + +(* The rules as read (for their declarations) and as checked (to run). *) +let read_rules resolve m path = + Result.bind + (Loader.read_rules (resolve path) m path) + (fun t -> Result.map (fun prog -> (t, prog)) (Rules_check.check m t)) + |> Result.map_error (fun e -> Fault.bad Fault.Rules e) + +let no_situation i n = + Fault.arg "E_NO_SITUATION" + ("no situation " ^ string_of_int i ^ ": this model has " ^ string_of_int n + ^ " (indices 0 to " + ^ string_of_int (n - 1) + ^ ")") + +let prop_names (cl : Claims.t) = + List.map (fun (p : Claims.property) -> p.Claims.name) cl.Claims.props + +(* ── why a property is n/a ────────────────────────────────────────────────── + The checker answers n/a when a property names structure the model lacks, + and says no more. Here is the first such name, with what it could have + been: (code, message, found, alternatives). *) + +let entities (ctx : State.ctx) = + List.concat_map + (fun (r : Instance.roster) -> r.Instance.entities) + ctx.State.rosters + +let members (ctx : State.ctx) ty = + match Schema.type_of ctx.State.schema ty with + | Some { Schema.flavor = Schema.Enumerated vs; _ } -> vs + | _ -> + List.concat_map + (fun (r : Instance.roster) -> + if r.Instance.ty = ty then r.Instance.entities else []) + ctx.State.rosters + +let arrows_from (ctx : State.ctx) ty = + List.filter_map + (fun (a : Schema.arrow) -> + if a.Schema.dom = ty then Some a.Schema.name else None) + ctx.State.schema.Schema.arrows + +let rec missing_in (ctx : State.ctx) env (g : Model.guard) = + let path (p : Value.path) = + match Checker.root_type ctx env p.Value.root with + | None -> + Some + ( "E_UNKNOWN_ENTITY", + "unknown entity or variable `" ^ p.Value.root ^ "`", + p.Value.root, + List.map fst env @ entities ctx ) + | Some ty -> + let rec walk cur = function + | [] -> None + | step :: rest -> ( + match Schema.arrow_in ctx.State.schema ~dom:cur step with + | Some a -> walk a.Schema.cod rest + | None -> + Some + ( "E_UNKNOWN_ARROW", + "`" ^ cur ^ "` has no arrow `" ^ step ^ "`", + step, + arrows_from ctx cur )) + in + walk ty p.Value.steps + in + let ( |? ) a b = match a with Some _ -> a | None -> Lazy.force b in + match g with + | Model.And gs | Model.Or gs -> List.find_map (missing_in ctx env) gs + | Model.Not g -> missing_in ctx env g + | Model.Defined p -> path p + | Model.Is (p, Model.Lit v) -> + path p + |? lazy + (match Checker.path_cod ctx env p with + | Some ty when not (Checker.value_in_type ctx ty v) -> + Some + ( "E_UNKNOWN_VALUE", + "value " ^ v ^ " not in codomain " ^ ty, + v, + members ctx ty ) + | _ -> None) + | Model.Is (p, Model.Chain q) -> + path p + |? lazy (path q) + |? lazy + (match (Checker.path_cod ctx env p, Checker.path_cod ctx env q) with + | Some a, Some b when a <> b -> + Some + ( "E_TYPE_MISMATCH", + "one side lands in `" ^ a ^ "`, the other in `" ^ b ^ "`", + b, + [] ) + | _ -> None) + | Model.Some_ (x, ty, g) -> ( + match Schema.type_of ctx.State.schema ty with + | None -> + Some + ( "E_UNKNOWN_TYPE", + "`" ^ ty ^ "` is not a declared type", + ty, + List.map + (fun (t : Schema.ty) -> t.Schema.name) + ctx.State.schema.Schema.types ) + | Some _ -> missing_in ctx ((x, ty) :: env) g) + +let move_names (m : Model.t) = + List.filter_map + (fun (t : Model.transition) -> t.Model.name) + m.Model.transitions + +let missing (ctx : State.ctx) (m : Model.t) (p : Claims.property) = + match missing_in ctx [] p.Claims.formula with + | Some r -> Some r + | None -> ( + match p.Claims.modality with + | Claims.Inevitable fair -> ( + match + List.find_opt (fun mv -> not (List.mem mv (move_names m))) fair + with + | Some mv -> + Some + ( "E_UNKNOWN_MOVE", + "no move named `" ^ mv ^ "`", + mv, + move_names m ) + | None -> None) + | _ -> None) + +(* Where [token] first stands as a whole word in [text], at or after the line + holding [after]: the claims datum is not positioned once parsed. *) +let locate ~file ~after ~token text : Errors.pos option = + let ls = String.split_on_char '\n' text in + let start = + let rec go k = function + | [] -> 0 + | l :: rest -> + if Diagnose.contains ~sub:after l then k else go (k + 1) rest + in + go 0 ls + in + let word l i = + let n = String.length token and len = String.length l in + let name c = Diagnose.is_name c in + String.sub l i n = token + && (i = 0 || not (name l.[i - 1])) + && (i + n = len || not (name l.[i + n])) + in + List.find_map + (fun (k, l) -> + if k < start then None + else + let n = String.length token in + let rec go i = + if i + n > String.length l then None + else if word l i then Some i + else go (i + 1) + in + Option.map + (fun i -> { Errors.file = Some file; line = k + 1; col = i + 1 }) + (go 0)) + (List.mapi (fun k l -> (k, l)) ls) + +(* One line per n/a property of a check: what it names that the model lacks. *) +let na_notes ctx m (props : (Claims.property * Checker.outcome) list) = + List.filter_map + (fun ((p : Claims.property), o) -> + match (o, missing ctx m p) with + | Checker.Not_applicable _, Some (code, msg, found, alts) -> + let _, best = Diagnose.rank found alts in + Some + ("why n/a " ^ p.Claims.name ^ ": " ^ msg + ^ (match best with + | Some b -> " — did you mean `" ^ b ^ "`?" + | None -> "") + ^ " (" ^ code ^ "; n/a is a failure)") + | _ -> None) + props (* Appends a line, skipping the empty sections [Report] returns as "". *) let adder b s = @@ -47,12 +243,17 @@ type memory = (string, Space.t) Hashtbl.t let remember : memory = Hashtbl.create 8 +(* A space can be large, so only this many are kept; past it the memory + starts over rather than grow without bound. *) +let memory_cap = 16 + (* The §17 comparison against the remembered space, or [None] the first time. As in `writ compare`, a property that became n/a counts as LOST. *) -let revision ~(memory : memory) ~(cpath : string) (cl : Claims.t) (sp : Space.t) - : (string * Json.t) option = +let revision ~(memory : memory) ?(key = "") ~(cpath : string) (cl : Claims.t) + (sp : Space.t) : (string * Json.t) option = + let key = key ^ "|" ^ cpath in let result = - match Hashtbl.find_opt memory cpath with + match Hashtbl.find_opt memory key with | None -> None | Some old_sp -> let equations = Compare.equation_rows [] old_sp sp in @@ -74,21 +275,29 @@ let revision ~(memory : memory) ~(cpath : string) (cl : Claims.t) (sp : Space.t) in Some (head ^ "\n" ^ text, json) in - Hashtbl.replace memory cpath sp; + if Hashtbl.length memory >= memory_cap && not (Hashtbl.mem memory key) then + Hashtbl.reset memory; + Hashtbl.replace memory key sp; result (* ── check ───────────────────────────────────────────────────────────────── Same output as `writ check` (or `writ check --json`). *) -let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify - ?(version = "") ~resolve ~model ~claims () = +let check ?(json = false) ?(pinned = None) ?(memory = remember) ?memory_key + ?certify ?(version = "") ?limits ~resolve ~model ~claims () = let* m = load resolve model in - let* sp = build model m in let claims = Option.map (pin ~pinned) claims in - let* parts = + (* Claims are typed against the model alone, so they are read before the + search: a cut-off search can then name what it left undecided. *) + let* cl = match claims with | None -> Ok None - | Some c -> - let* cl = read_claims resolve m c in + | Some c -> Result.map (fun cl -> Some (c, cl)) (read_claims resolve m c) + in + let undecided = match cl with Some (_, cl) -> prop_names cl | None -> [] in + let* sp = build ?limits ~undecided model m in + let parts = + Option.map + (fun (c, cl) -> let unadmitted = Observe.unadmitted sp cl and stale = Observe.stale sp cl in let props = @@ -101,7 +310,8 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify (fun (q : Claims.query) -> (q, 0, Query.run sp q ())) cl.Claims.queries in - Ok (Some (c, cl, unadmitted, stale, props, queries)) + (c, cl, unadmitted, stale, props, queries)) + cl in let failed = List.exists @@ -112,7 +322,11 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify | Some (_, _, u, s, props, _) -> u <> [] || s <> [] || List.exists - (fun (_, o) -> match o with Checker.Fails _ -> true | _ -> false) + (fun (_, o) -> + (* n/a is a finding, as in `writ check` *) + match o with + | Checker.Holds _ -> false + | _ -> true) props | None -> false in @@ -145,7 +359,8 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify let exit = if failed then 1 else 0 in let rev = match parts with - | Some (c, cl, _, _, _, _) -> revision ~memory ~cpath:c cl sp + | Some (c, cl, _, _, _, _) -> + revision ~memory ?key:memory_key ~cpath:c cl sp | None -> None in if json then @@ -166,7 +381,22 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify Json.Assoc (kvs @ [ ("claims", Json.String c) ]) | j, _, _ -> j in - Ok (Json.to_string with_pin) + let notes = + match parts with + | Some (_, _, _, _, props, _) -> na_notes sp.Space.ctx m props + | None -> [] + in + let with_notes = + match (with_pin, notes) with + | Json.Assoc kvs, _ :: _ -> + Json.Assoc + (kvs + @ [ + ("why_na", Json.List (List.map (fun n -> Json.String n) notes)); + ]) + | j, _ -> j + in + Ok (Json.to_string with_notes) else begin let b = Buffer.create 1024 in let add = adder b in @@ -179,7 +409,8 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify List.iter (fun (p, o) -> add (Report.outcome ~queries:cl.Claims.queries sp p o)) props; - List.iter (fun (q, i, rows) -> add (Report.query_rows q i rows)) queries); + List.iter (fun (q, i, rows) -> add (Report.query_rows q i rows)) queries; + List.iter add (na_notes sp.Space.ctx m props)); (match rev with Some (text, _) -> add text | None -> ()); Option.iter (fun v -> add (Certify_json.verdict_line v)) certified; Ok (Buffer.contents b) @@ -187,19 +418,16 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?certify (* ── show ────────────────────────────────────────────────────────────────── The situations at the given indices; the initial one if none. *) -let show ?(json = false) ~resolve ~model ~at () = +let show ?(json = false) ?limits ~resolve ~model ~at () = let* m = load resolve model in - let* sp = build model m in + let* sp = build ?limits model m in let n = Array.length sp.Space.states in let* idxs = match at with | [] -> Ok [ 0 ] | is -> ( match List.find_opt (fun i -> i < 0 || i >= n) is with - | Some i -> - Error - ("no situation " ^ string_of_int i ^ ": this model has " - ^ string_of_int n) + | Some i -> Error (no_situation i n) | None -> Ok is) in if json then Ok (Json.to_string (Report_json.show sp idxs)) @@ -207,17 +435,23 @@ let show ?(json = false) ~resolve ~model ~at () = (* ── compare ─────────────────────────────────────────────────────────────── OLD's claims put to both models: guarantees kept, lost and gained. *) -let compare ?(json = false) ?(pinned = None) ~resolve ~old_model ~new_model () = +let compare ?(json = false) ?(pinned = None) ?limits ?claims ~resolve ~old_model + ~new_model () = let* old_m = load resolve old_model in - let* old_sp = build old_model old_m in let* new_m = load resolve new_model in - let* new_sp = build new_model new_m in - let cpath = sibling_claims ~pinned old_model in + (* The old model's claims: the ones named, else its sibling, else none. A + named file that does not read is an error; a missing sibling is not. *) let* cl = - match read_claims resolve old_m cpath with - | Ok cl -> Ok cl - | Error _ -> Ok { Claims.props = []; queries = []; accepts = [] } + match claims with + | Some c -> read_claims resolve old_m (pin ~pinned c) + | None -> ( + match read_claims resolve old_m (sibling_claims ~pinned old_model) with + | Ok cl -> Ok cl + | Error _ -> Ok { Claims.props = []; queries = []; accepts = [] }) in + let undecided = prop_names cl in + let* old_sp = build ?limits ~undecided old_model old_m in + let* new_sp = build ?limits ~undecided new_model new_m in let equations = Compare.equation_rows [] old_sp new_sp in let properties = Compare.property_rows [] old_sp new_sp cl in let any_lost = @@ -232,16 +466,37 @@ let compare ?(json = false) ?(pinned = None) ~resolve ~old_model ~new_model () = ~exit:(if any_lost then 1 else 0))) else let text, _ = Compare.run old_sp new_sp cl [] in - Ok text + (* Compare lists what changed; a property failing in both is silent + there, which reads as "nothing wrong". *) + let failing sp (p : Claims.property) = + match Checker.check sp p with Checker.Holds _ -> false | _ -> true + in + let still = + List.filter_map + (fun (p : Claims.property) -> + if failing old_sp p && failing new_sp p then Some p.Claims.name + else None) + cl.Claims.props + in + Ok + (if still = [] then text + else + String.trim text ^ "\nstill failing in both models: " + ^ String.concat ", " still ^ "\n") (* ── query ───────────────────────────────────────────────────────────────── One named query from the sibling .claims. An out-of-range [at] is an error, not an empty answer. *) -let query ?(json = false) ?(pinned = None) ~resolve ~model ~name ~at () = +let query ?(json = false) ?(pinned = None) ?limits ?claims ~resolve ~model ~name + ~at () = let* m = load resolve model in - let* sp = build model m in - let cpath = sibling_claims ~pinned model in + let cpath = + match claims with + | Some c -> pin ~pinned c + | None -> sibling_claims ~pinned model + in let* cl = read_claims resolve m cpath in + let* sp = build ?limits model m in let* q = match List.find_opt @@ -249,41 +504,59 @@ let query ?(json = false) ?(pinned = None) ~resolve ~model ~name ~at () = cl.Claims.queries with | Some q -> Ok q - | None -> Error ("no query named `" ^ name ^ "` in " ^ cpath) + | None -> + Error + (Fault.Bad + [ + { + Fault.source = Fault.Claims; + code = Some "E_UNKNOWN_QUERY"; + err = + { + Errors.pos = None; + msg = "no query named `" ^ name ^ "` in " ^ cpath; + }; + meant = + Some + ( name, + List.map + (fun (q : Claims.query) -> q.Claims.name) + cl.Claims.queries ); + }; + ]) in let* idx, st = match at with | None -> Ok (0, sp.Space.initial) | Some i when i >= 0 && i < Array.length sp.Space.states -> Ok (i, sp.Space.states.(i)) - | Some i -> - Error - ("no situation " ^ string_of_int i ^ ": this model has " - ^ string_of_int (Array.length sp.Space.states)) + | Some i -> Error (no_situation i (Array.length sp.Space.states)) in let rows = Query.run sp q ~at:st () in if json then Ok (Json.to_string (Report_json.query_rows q idx rows)) else Ok (Report.query_rows q idx rows) +let no_relation relation rules = + Fault.bad ~code:"E_UNKNOWN_RELATION" Fault.Rules + { + Errors.pos = None; + msg = "no relation named `" ^ relation ^ "` in " ^ rules; + } + (* ── derive ──────────────────────────────────────────────────────────────── A relation from a .rules file, with arguments as a JSON list (null = unbound). [why] returns the derivation tree and needs every argument. *) -let derive ?(json = false) ~resolve ~model ~rules ~relation ~args ~why () = +let derive ?(json = false) ?limits ~resolve ~model ~rules ~relation ~args ~why + () = let* m = load resolve model in - let* sp = build model m in - let* prog = - let* t = - Loader.read_rules (resolve rules) m rules - |> Result.map_error Errors.to_string - in - Rules_check.check m t |> Result.map_error Errors.to_string - in + let* _, prog = read_rules resolve m rules in + let* sp = build ?limits model m in (* Compute only the relation asked for, as [Cmd_derive] does. *) let t = Derive.run ~only:relation sp prog in let* sorts = match Derive_answers.sorts_of t relation with | Some ss -> Ok ss - | None -> Error ("no relation named `" ^ relation ^ "` in " ^ rules) + | None -> Error (no_relation relation rules) in let arity = List.length sorts in let args = @@ -293,8 +566,9 @@ let derive ?(json = false) ~resolve ~model ~rules ~relation ~args ~why () = if List.length args = arity then Ok () else Error - (relation ^ " takes " ^ string_of_int arity ^ " arguments, not " - ^ string_of_int (List.length args)) + (Fault.arg "E_ARG_INVALID" + (relation ^ " takes " ^ string_of_int arity ^ " arguments, not " + ^ string_of_int (List.length args))) in if why then let* ground = @@ -302,8 +576,9 @@ let derive ?(json = false) ~resolve ~model ~rules ~relation ~args ~why () = Ok (List.map (Option.value ~default:"") args) else Error - ("`why` needs every argument of `" ^ relation - ^ "` given, not left open") + (Fault.arg "E_ARG_INVALID" + ("`why` needs every argument of `" ^ relation + ^ "` given, not left open")) in if json then Ok (Json.to_string (Report_json.derive_why t relation ground)) else Ok (Report_derive.why t relation ground) @@ -316,9 +591,257 @@ let derive ?(json = false) ~resolve ~model ~rules ~relation ~args ~why () = (* Wrong-sort constant: the .rules parser's wording. *) | Some (Error (i, srt)) -> Error - ("`" - ^ Option.value ~default:"?" (List.nth args i) - ^ "` is not " ^ Rules_terms.sort_name srt ^ ", which is what column " - ^ string_of_int (i + 1) - ^ " of `" ^ relation ^ "` takes") - | None -> Error ("no relation named `" ^ relation ^ "` in " ^ rules) + (Fault.arg "E_ARG_INVALID" + ("`" + ^ Option.value ~default:"?" (List.nth args i) + ^ "` is not " ^ Rules_terms.sort_name srt + ^ ", which is what column " + ^ string_of_int (i + 1) + ^ " of `" ^ relation ^ "` takes")) + | None -> Error (no_relation relation rules) + +(* ── validate ────────────────────────────────────────────────────────────── + Parse and type-check without enumerating: every file's first error, or + what the sources declare, so the agent can see the model means what it + intended. Claims and rules are typed against the model, so a broken model + is the only error reported. *) + +let modality_name = function + | Claims.Possible -> "possible" + | Claims.Never -> "never" + | Claims.Live -> "live" + | Claims.Inevitable [] -> "inevitable" + | Claims.Inevitable fair -> "inevitable (fair " ^ String.concat " " fair ^ ")" + +let arity (r : Rules.relation) = + match r.Rules.cols with Rules.Arity n -> n | Rules.Sorts l -> List.length l + +let validate ?(json = false) ?(pinned = None) ~resolve ~model ~claims ~rules () + = + let* m = load resolve model in + let* ctx, _ = + State.build_ctx m.Model.schema m.Model.initial + |> Result.map_error (model_fault model) + in + let claims = Option.map (pin ~pinned) claims in + let cl = Option.map (read_claims resolve m) claims in + let rl = + Option.map (fun r -> Result.map fst (read_rules resolve m r)) rules + in + let errs = + List.concat_map + (function Some (Error (Fault.Bad fs)) -> fs | _ -> []) + [ Option.map (Result.map ignore) cl; Option.map (Result.map ignore) rl ] + in + (* Claims are typed against the model, but a name the model lacks parses + and only answers n/a: almost always a typo in new claims, so here it is + an error with the name meant. *) + let errs = + match (cl, claims) with + | Some (Ok cl), Some cpath -> + let text = + match resolve cpath (Filename.basename cpath) with + | Ok t -> t + | Error _ -> "" + in + errs + @ List.filter_map + (fun (p : Claims.property) -> + Option.map + (fun (code, msg, found, alts) -> + { + Fault.source = Fault.Claims; + code = Some code; + err = + { + Errors.pos = + locate ~file:cpath + ~after:("property " ^ p.Claims.name) + ~token:found text; + msg = + "property `" ^ p.Claims.name ^ "` would be n/a: " + ^ msg; + }; + meant = Some (found, alts); + }) + (missing ctx m p)) + cl.Claims.props + | _ -> errs + in + if errs <> [] then Error (Fault.Bad errs) + else + let cl = Option.map Result.get_ok cl and rl = Option.map Result.get_ok rl in + let schema = m.Model.schema and inst = m.Model.initial in + let lay = ctx.State.layout in + let cells = Array.length lay.State.cells in + let bound = Space.bound lay and show_bound = Space.show_bound in + let members (ty : Schema.ty) = + match ty.Schema.flavor with + | Schema.Enumerated vs -> ("values", vs) + | Schema.Open -> + ("entities", Instance.entities_of_type inst ty.Schema.name) + in + let arrows_of (ty : Schema.ty) = + List.filter + (fun (a : Schema.arrow) -> a.Schema.dom = ty.Schema.name) + schema.Schema.arrows + in + let moves = + List.mapi + (fun i (t : Model.transition) -> + match t.Model.name with Some n -> n | None -> "#" ^ string_of_int i) + m.Model.transitions + in + let laws = + List.map + (fun (e : Schema.equation) -> e.Schema.name) + schema.Schema.equations + in + if json then + let strs l = Json.List (List.map (fun s -> Json.String s) l) in + let types = + List.map + (fun (ty : Schema.ty) -> + let k, vs = members ty in + Json.Assoc + [ + ("name", Json.String ty.Schema.name); + (k, strs vs); + ( "arrows", + Json.List + (List.map + (fun (a : Schema.arrow) -> + Json.Assoc + [ + ("name", Json.String a.Schema.name); + ("to", Json.String a.Schema.cod); + ("fixed", Json.Bool a.Schema.fixed); + ("vacatable", Json.Bool a.Schema.vacatable); + ]) + (arrows_of ty)) ); + ]) + schema.Schema.types + in + let claims_j = + match cl with + | None -> [] + | Some cl -> + [ + ( "properties", + Json.List + (List.map + (fun (p : Claims.property) -> + Json.Assoc + [ + ("name", Json.String p.Claims.name); + ( "modality", + Json.String (modality_name p.Claims.modality) ); + ]) + cl.Claims.props) ); + ( "queries", + strs + (List.map + (fun (q : Claims.query) -> q.Claims.name) + cl.Claims.queries) ); + ] + in + let rules_j = + match rl with + | None -> [] + | Some (t : Rules_parser.t) -> + [ + ( "relations", + Json.List + (List.map + (fun (r : Rules.relation) -> + Json.Assoc + [ + ("name", Json.String r.Rules.rel_name); + ("arity", Json.Int (arity r)); + ]) + t.Rules_parser.relations) ); + ] + in + Ok + (Json.to_string + (Json.Assoc + ([ + ("ok", Json.Bool true); + ("schema", Json.String schema.Schema.name); + ("instance", Json.String inst.Instance.name); + ("types", Json.List types); + ("laws", strs laws); + ("moves", strs moves); + ("cells", Json.Int cells); + ("bound", Json.String (show_bound bound)); + ] + @ claims_j @ rules_j))) + else + let b = Buffer.create 1024 in + let add = adder b in + add + ("ok: " + ^ String.concat ", " + (("model" :: (if cl <> None then [ "claims" ] else [])) + @ if rl <> None then [ "rules" ] else []) + ^ " parse and type-check (nothing was enumerated)"); + add ("schema " ^ schema.Schema.name ^ ", instance " ^ inst.Instance.name); + List.iter + (fun (ty : Schema.ty) -> + let k, vs = members ty in + add + (" type " ^ ty.Schema.name ^ " " ^ k ^ ": " + ^ if vs = [] then "(none)" else String.concat " " vs); + List.iter + (fun (a : Schema.arrow) -> + add + (" arrow " ^ a.Schema.name ^ " -> " ^ a.Schema.cod + ^ (if a.Schema.fixed then " fixed" else "") + ^ if a.Schema.vacatable then " vacatable" else "")) + (arrows_of ty)) + schema.Schema.types; + if laws <> [] then add ("laws: " ^ String.concat ", " laws); + add + ("moves (" + ^ string_of_int (List.length moves) + ^ "): " ^ String.concat ", " moves); + add + ("cells: " ^ string_of_int cells ^ " mutable; at most " + ^ show_bound bound + ^ " situations (the product of their domains; check budget " + ^ string_of_int Space.cap ^ ")"); + if bound > float_of_int Space.cap then + add + "warning: the bound is over the check budget; writ_check may stop \ + with E_STATE_LIMIT. Shrink domains and drop unread cells \ + (writ_guide idioms, Abstraction and size)."; + Option.iter + (fun (cl : Claims.t) -> + add + ("properties: " + ^ String.concat ", " + (List.map + (fun (p : Claims.property) -> + p.Claims.name ^ " (" + ^ modality_name p.Claims.modality + ^ ")") + cl.Claims.props)); + if cl.Claims.queries <> [] then + add + ("queries: " + ^ String.concat ", " + (List.map + (fun (q : Claims.query) -> q.Claims.name) + cl.Claims.queries))) + cl; + Option.iter + (fun (t : Rules_parser.t) -> + add + ("relations: " + ^ String.concat ", " + (List.map + (fun (r : Rules.relation) -> + r.Rules.rel_name ^ "/" ^ string_of_int (arity r)) + t.Rules_parser.relations))) + rl; + Ok (Buffer.contents b) From e1427b52a4f1c645f2090081bbf328b748a282db Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 21:45:49 +0300 Subject: [PATCH 2/3] report: how a failing inevitable avoids its goal; shorter dead-end lists MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The cold-start acceptance run found that a failing inevitable said only `stuck at: #N` — not how a run avoids the goal from there — and that dead-end routes of hundreds of moves flooded a reply. - inevitable: `avoids: the run stops at #N`, or `loop:` a shortest cycle back to the stuck situation outside F; under (fair …), where one cycle could starve a fair move, `loops among:` the region a fair run circles in. Space.avoidance exposes the region escapes_f already computed. - dead ends: a route over 24 moves keeps its ends and counts the middle; past 20 dead ends the rest are counted. - Prose only; --json and certificates are unchanged (certified as before). - plugin skill: mention writ_guide/writ_validate when the server lists them, so it reads true against the pinned 0.4.0 image and later ones. - docs/mcp.md: an inline model's (load …) searches the working directory first, as a path model's does. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 8 +++ docs/kernel-spec.md | 6 ++ docs/mcp.md | 4 +- plugins/writ/skills/writ/SKILL.md | 5 ++ runtime/report.ml | 78 +++++++++++++++++++++++-- runtime/space.ml | 81 ++++++++++++++++++++++++-- tests/unit/test_mcp_authoring.ml | 44 ++++++++++++++ tooling/mcp/guide/examples.consumer.md | 3 + tooling/mcp/guide/semantics.md | 2 +- 9 files changed, 219 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1a3d1dd..20ff899 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,6 +31,14 @@ error: a bare `(set …)` outside `(do …)` used to be dropped silently, leavin 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. + ## 0.4.0 — 2026-10-03 **Upgrading:** `writ check` now exits 1 when a property is `n/a`. A pipeline diff --git a/docs/kernel-spec.md b/docs/kernel-spec.md index a86cd16..db26820 100644 --- a/docs/kernel-spec.md +++ b/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 diff --git a/docs/mcp.md b/docs/mcp.md index 8c6f85e..2357cc3 100644 --- a/docs/mcp.md +++ b/docs/mcp.md @@ -112,7 +112,9 @@ Every file argument is a path **or** inline text: `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. Under +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 diff --git a/plugins/writ/skills/writ/SKILL.md b/plugins/writ/skills/writ/SKILL.md index 7ee9167..7db1d12 100644 --- a/plugins/writ/skills/writ/SKILL.md +++ b/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, diff --git a/runtime/report.ml b/runtime/report.ml index deca7e1..be1ac0a 100644 --- a/runtime/report.ml +++ b/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 ------------------------------------------------------------ *) diff --git a/runtime/space.ml b/runtime/space.ml index b811191..4f17ff2 100644 --- a/runtime/space.ml +++ b/runtime/space.ml @@ -358,7 +358,18 @@ let enabled_names (t : t) : string list array = takes it is removed, repeatedly (Emerson–Lei). Stops are unaffected. Not closed backward: the closure gives the same verdict but its shortest witness would usually be the empty route. *) -let escapes_f ?(fair = []) (t : t) (sat : State.t -> bool) : bool array = +(* The region a run can stay in for ever without F: the non-F situations on + a cycle that survives the fairness deletions, plus the non-F dead ends. + [escape.(i)] marks them; [comp] numbers the surviving cycles' components, + so a reader can be shown the loop itself. *) +type avoidance = { + escape : bool array; + alive : bool array; + comp : int array; + stopped : bool array; +} + +let avoidance ?(fair = []) (t : t) (sat : State.t -> bool) : avoidance = let n = Array.length t.states in let f = Array.init n (fun i -> sat t.states.(i)) in let all = succs t in @@ -436,11 +447,69 @@ let escapes_f ?(fair = []) (t : t) (sat : State.t -> bool) : bool array = Array.iteri (fun i k -> if alive.(i) && k >= 0 then size.(k) <- size.(k) + 1) c; - Array.init n (fun i -> - (not f.(i)) - && ((* stopped: no real move out of the model at all *) - all.(i) = [] - || (alive.(i) && (size.(c.(i)) > 1 || List.mem i sub.(i))))) + let cyclic i = alive.(i) && (size.(c.(i)) > 1 || List.mem i sub.(i)) in + (* stopped: no real move out of the model at all *) + let stopped = Array.init n (fun i -> (not f.(i)) && all.(i) = []) in + { + escape = Array.init n (fun i -> stopped.(i) || ((not f.(i)) && cyclic i)); + alive = Array.init n cyclic; + comp = c; + stopped; + } + +let escapes_f ?fair (t : t) (sat : State.t -> bool) : bool array = + (avoidance ?fair t sat).escape + +(* The situations of [i]'s avoiding cycle, and a shortest loop from [i] back + to itself inside it: (move, landing index) steps. [None] for a dead end. *) +let avoid_loop (a : avoidance) (t : t) (i : int) : + (int list * (string * int) list) option = + if (not a.alive.(i)) || a.stopped.(i) then None + else + let k = a.comp.(i) in + let inside j = a.alive.(j) && a.comp.(j) = k in + let members = + List.filter inside (List.init (Array.length t.states) Fun.id) + in + let out = Array.make (Array.length t.states) [] in + List.iter + (fun e -> + match e.dst with + | `To s' -> ( + match + (State.M.find_opt e.src t.index, State.M.find_opt s' t.index) + with + | Some si, Some di when inside si && inside di -> + out.(si) <- (e.via, di) :: out.(si) + | _ -> ()) + | `Gap _ -> ()) + t.edges; + Array.iteri (fun j l -> out.(j) <- List.rev l) out; + (* BFS from i until an edge leads back into i. [parent] maps a reached + situation to the move and situation it was first reached from. *) + let parent = Hashtbl.create 16 in + let q = Queue.create () in + Queue.add i q; + let rec path_to d acc = + if d = i then acc + else + let via, from = Hashtbl.find parent d in + path_to from ((via, d) :: acc) + in + let found = ref None in + while !found = None && not (Queue.is_empty q) do + let u = Queue.pop q in + List.iter + (fun (via, d) -> + if !found = None then + if d = i then found := Some (path_to u [] @ [ (via, i) ]) + else if not (Hashtbl.mem parent d) then begin + Hashtbl.replace parent d (via, u); + Queue.add d q + end) + out.(u) + done; + Option.map (fun loop -> (members, loop)) !found (* The edges out of a state, gap edges included — so a gap-firing state is not a dead end (§15: a gap is a declared boundary, listed separately). *) diff --git a/tests/unit/test_mcp_authoring.ml b/tests/unit/test_mcp_authoring.ml index b82e4ee..3b687f4 100644 --- a/tests/unit/test_mcp_authoring.ml +++ b/tests/unit/test_mcp_authoring.ml @@ -720,6 +720,50 @@ let () = check "timeout: a long search stops at the clock" (err && contains ~sub:"stopped at timeout" out) +(* ── how an inevitable failure avoids F; long dead-end routes ──────────── *) + +let () = + let consumer = + List.assoc "consumer-fixed.writ" + (List.filter_map + (fun (info, b) -> Option.map (fun f -> (f, b)) (kv info "file")) + (blocks (guide_topic "examples.consumer"))) + in + let _, out = + tool "writ_check" + [ + ("model_source", s consumer); + ( "claims_source", + s "(property f \"x\" (inevitable (is m.stage acked) (fair deliver)))" + ); + ] + in + check "fair inevitable: names the region a fair run circles in" + (contains ~sub:"loops among: #2 #4 #5, taking every fair move offered there" + out); + (* a 40-step ladder: its dead end's route is shortened in the middle *) + let n = 40 in + let steps = List.init n (fun i -> "t" ^ string_of_int i) in + let ladder = + "(schema l (type tick (arrow next (to tick) fixed vacatable)) (type c \ + (arrow at (to tick))))\n\ + (instance i l (tick " ^ String.concat " " steps ^ ") (next " + ^ String.concat " " + (List.mapi + (fun i t -> + if i = n - 1 then "(" ^ t ^ " vacant)" + else "(" ^ t ^ " t" ^ string_of_int (i + 1) ^ ")") + steps) + ^ ") (c k (at t0)))\n\ + (use l)\n\ + (initial i)\n\ + (transition step (when (defined k.at.next)) (do (set k.at k.at.next)))\n" + in + let err, out = tool "writ_check" [ ("model_source", s ladder) ] in + if err then print_string out; + check "dead ends: a long route is shortened" + (contains ~sub:"… 19 more moves …" out) + (* ── a bare (set …) outside (do …) is an error, not a silent no-op ───────── *) let () = diff --git a/tooling/mcp/guide/examples.consumer.md b/tooling/mcp/guide/examples.consumer.md index f64fb19..c0c886c 100644 --- a/tooling/mcp/guide/examples.consumer.md +++ b/tooling/mcp/guide/examples.consumer.md @@ -57,6 +57,7 @@ fails finishes 5. process → #6 m.stage: delivered → processed, acct.charges: c1 → c2 6. timeout → #8 m.stage: processed → queued 7. deliver → #9 m.stage: queued → delivered + avoids: the run stops at #9: no move is left fails finishes-fairly "it does, if an offered ack is not refused for ever" assuming fair: ack @@ -68,6 +69,7 @@ fails finishes-fairly 5. process → #6 m.stage: delivered → processed, acct.charges: c1 → c2 6. timeout → #8 m.stage: processed → queued 7. deliver → #9 m.stage: queued → delivered + avoids: the run stops at #9: no move is left ``` `charged-once` fails: process, lose the ack, redeliver, process again. Both termination properties fail too, stuck at `#9`, where the message is delivered but `process` cannot fire because the ladder has ended (`acct.charges.next` has no answer). That dead end is the **bound**, not the system: the ladder only counts to `c2`. Read it as such. @@ -115,6 +117,7 @@ fails finishes stuck at: #2 (m.stage=processed m.key-seen=yes acct.charges=c1) witness: 1. deliver → #1 m.stage: queued → delivered 2. process → #2 m.stage: delivered → processed, m.key-seen: no → yes, acct.charges: c0 → c1 + loop: 1. timeout → #4 2. deliver → #5 3. process-again → #2 (and again, for ever) holds finishes-fairly "it does, if an offered ack is not refused for ever" assuming fair: ack diff --git a/tooling/mcp/guide/semantics.md b/tooling/mcp/guide/semantics.md index 2fd1932..48e7e29 100644 --- a/tooling/mcp/guide/semantics.md +++ b/tooling/mcp/guide/semantics.md @@ -51,7 +51,7 @@ After an edit, a property that became `n/a` counts as LOST. Never make a check p ## 8. Witnesses -The space is built breadth-first, so every route printed is a shortest one (fewest moves). Among equally short routes, writ reports the first found: moves are tried in the order they are declared, situations in index order. A `fails` for `never` shows the route to the violating situation; for `live` and `inevitable` it shows `stuck at:` the nearest situation from which F is unreachable (`live`) or avoidable for ever (`inevitable`), with the route *to* it. That route is empty when the stuck situation is `#0`, and it does not show the loop that avoids F: `writ_show` the stuck situation and follow its moves, or ask `.rules` (`recurrent` in `ct.rules`). A holding `possible` shows the route to the nearest F situation: that route is the answer to "is there a way". +The space is built breadth-first, so every route printed is a shortest one (fewest moves). Among equally short routes, writ reports the first found: moves are tried in the order they are declared, situations in index order. A `fails` for `never` shows the route to the violating situation; for `live` and `inevitable` it shows `stuck at:` the nearest situation from which F is unreachable (`live`) or avoidable for ever (`inevitable`), with the route *to* it. That route is empty when the stuck situation is `#0`. A failing `inevitable` then says how a run avoids F from there: `avoids: the run stops at #N` (no move left), `loop:` a shortest cycle back to it, or, under `(fair …)`, `loops among:` the situations a fair run circles in. A holding `possible` shows the route to the nearest F situation: that route is the answer to "is there a way". ## 9. Indices From 8db022e0bd1e348f7300e6802becf744ec912dbc Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 21:47:47 +0300 Subject: [PATCH 3/3] certified: say so when every property is n/a MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With every property n/a and no query, writ-cert re-derives only the situation count, yet the last line read "every answer re-derived". It now reads `certified: the situation count only — every property is n/a, so no claim was checked`, in `writ check` and `writ_check` alike (one renderer, Certify_json.verdict_line). The certification JSON field and the certificate format are unchanged, so writ-cert needs nothing. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 6 ++++++ docs/certificates.md | 5 +++-- tests/unit/test_report_json.ml | 27 +++++++++++++++++++++++++++ tooling/cli/cmd_check.ml | 9 ++++++++- tooling/mcp/lib/tools.ml | 11 ++++++++++- tooling/report_json/certify_json.ml | 13 ++++++++++++- 6 files changed, 66 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 20ff899..b2eff78 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -39,6 +39,12 @@ 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 diff --git a/docs/certificates.md b/docs/certificates.md index c0b3304..7336947 100644 --- a/docs/certificates.md +++ b/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: diff --git a/tests/unit/test_report_json.ml b/tests/unit/test_report_json.ml index c377990..730d1b1 100644 --- a/tests/unit/test_report_json.ml +++ b/tests/unit/test_report_json.ml @@ -333,6 +333,33 @@ let () = check "certificate: the report rides along" (int (get "states" (get "report" j)) = n) +(* All n/a and no query: the certified line must not claim the claims. *) +let () = + let na = Checker.Not_applicable "x" and held = Checker.Holds [] in + let line nothing_decided = + Certify_json.verdict_line ~nothing_decided Certify_json.Certified + in + let has sub s = + let n = String.length sub in + let rec go i = + i + n <= String.length s && (String.sub s i n = sub || go (i + 1)) + in + go 0 + in + check "nothing decided: all n/a, no query" + (Certify_json.nothing_decided [ na; na ] ~queries:0); + check "decided: one property held" + (not (Certify_json.nothing_decided [ na; held ] ~queries:0)); + check "decided: a query was answered" + (not (Certify_json.nothing_decided [ na ] ~queries:1)); + check "decided: no claims at all is not all-n/a" + (not (Certify_json.nothing_decided [] ~queries:0)); + check "certified line says n/a when nothing was decided" + (has "every property is n/a" (line true)); + check "certified line unchanged otherwise" + (line false + = "certified: every answer re-derived from the model (writ-cert)") + let () = print_string ("test_report_json: " ^ string_of_int !passed ^ " checks passed\n") diff --git a/tooling/cli/cmd_check.ml b/tooling/cli/cmd_check.ml index 0fee4c7..0cbf0cf 100644 --- a/tooling/cli/cmd_check.ml +++ b/tooling/cli/cmd_check.ml @@ -198,7 +198,14 @@ let run ?(json = false) ?(fibers = []) ?(certificate = Off) ?(version = "") List.iter say (Report.fiber_lines sp fs)) props; List.iter (fun (q, i, rows) -> say (Report.query_rows q i rows)) a.queries; - Option.iter (fun v -> say (Certify_json.verdict_line v)) certified + let nothing_decided = + Certify_json.nothing_decided + (List.map (fun (_, o, _) -> o) props) + ~queries:(List.length a.queries) + in + Option.iter + (fun v -> say (Certify_json.verdict_line ~nothing_decided v)) + certified end; flush stdout; exit exit_code diff --git a/tooling/mcp/lib/tools.ml b/tooling/mcp/lib/tools.ml index f2e8654..9bc5d49 100644 --- a/tooling/mcp/lib/tools.ml +++ b/tooling/mcp/lib/tools.ml @@ -412,7 +412,16 @@ let check ?(json = false) ?(pinned = None) ?(memory = remember) ?memory_key List.iter (fun (q, i, rows) -> add (Report.query_rows q i rows)) queries; List.iter add (na_notes sp.Space.ctx m props)); (match rev with Some (text, _) -> add text | None -> ()); - Option.iter (fun v -> add (Certify_json.verdict_line v)) certified; + let nothing_decided = + match parts with + | Some (_, _, _, _, props, queries) -> + Certify_json.nothing_decided (List.map snd props) + ~queries:(List.length queries) + | None -> false + in + Option.iter + (fun v -> add (Certify_json.verdict_line ~nothing_decided v)) + certified; Ok (Buffer.contents b) end diff --git a/tooling/report_json/certify_json.ml b/tooling/report_json/certify_json.ml index add46ea..44e9a3c 100644 --- a/tooling/report_json/certify_json.ml +++ b/tooling/report_json/certify_json.ml @@ -178,7 +178,18 @@ let verdict_of_run ~(code : int) ~(output : string list) : verdict = | 126 | 127 -> Absent | _ -> Failed (String.concat " " (List.filter (( <> ) "") output)) -let verdict_line : verdict -> string = function +(* Every property n/a and no query: writ-cert re-derived only the count, so + the line must not read as if the claims were checked. *) +let nothing_decided (outcomes : Checker.outcome list) ~(queries : int) = + queries = 0 && outcomes <> [] + && List.for_all + (function Checker.Not_applicable _ -> true | _ -> false) + outcomes + +let verdict_line ?(nothing_decided = false) : verdict -> string = function + | Certified when nothing_decided -> + "certified: the situation count only — every property is n/a, so no \ + claim was checked (writ-cert)" | Certified -> "certified: every answer re-derived from the model (writ-cert)" | Disagrees ls -> String.concat "\n"