From a03433c57fec197139c5f3e4bda377381643c765 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Fri, 14 Aug 2026 05:43:39 +0300 Subject: [PATCH] =?UTF-8?q?docs(mgtt):=20work=20the=20reading=20through=20?= =?UTF-8?q?=E2=80=94=20why=20the=20reduction=20is=20lossless?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The verb's reference is in --help; this is the reasoning behind the mapping: why facts stop being numbers without loss, why facts are the only varying cells, why an overriding component needs its own type, why origination moves cannot be omitted, and what is declined. --- README.md | 47 ++++++ docs/mgtt-bridge.md | 338 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 385 insertions(+) create mode 100644 docs/mgtt-bridge.md diff --git a/README.md b/README.md index 6fd789d..1c9f81d 100644 --- a/README.md +++ b/README.md @@ -243,6 +243,7 @@ what it costs. | `writ schema MODEL` | emit the model's schema as an instance of the standard library's `olog` schema | | `writ sql SCHEMA.sql` | read a relational schema as an olog — tables become types, foreign keys arrows, NULL `vacatable`, enums enumerated types, single-row `CHECK`s laws | | `writ sql MODEL.writ` | …and back: emit the model's schema as `CREATE TABLE` | +| `writ mgtt MODEL.json` | read an [mgtt](https://github.com/mgt-tool/mgtt) architecture model — components, dependencies, health — as a model | | `writ derive MODEL RULES.rules R` | answer a `.rules` relation over the model's enumerated universe — every row | | `writ derive MODEL RULES.rules "(R A…)"` | …keeping only the rows that match, ALL-CAPS being a free variable, any position bindable (so the dynamics run backward) | | `writ derive MODEL RULES.rules --why "(R A…)"` | print one fact's derivation tree instead of rows | @@ -341,6 +342,49 @@ normalises spellings on purpose — and the two facts SQL cannot state (whether key is ever `UPDATE`d, whether a plain column is wiring) travel as `-- writ:` pragmas the import reads back. +### Architecture models + +An [mgtt](https://github.com/mgt-tool/mgtt) model describes a system's +components, what each depends on, and what "healthy" means for each of them. +`writ mgtt` reads one — so the architecture somebody already wrote becomes a +model whose every reachable failure configuration can be enumerated. + +```console +$ mgtt model export --json > system.json # in the mgtt repo +$ writ mgtt system.json > system.writ +$ writ check system.writ +``` + +The input is mgtt's *resolved* export rather than its YAML, so nothing here +needs mgtt's provider registry or a credential, and mgtt's own precedence rules +stay on mgtt's side of the seam. + +**Facts stop being numbers, losslessly.** mgtt's expression language has six +comparison operators and no arithmetic, so the constants a model mentions cut +each fact's values into finitely many regions on which every predicate is +constant. A region becomes a member; two values in one region were already +indistinguishable to mgtt's own engine. Regions nothing separates are merged, +so `connection_count < 500` costs two members rather than three. + +**The payoff is a law mgtt cannot state.** A component is healthy exactly when +it is in its default active state — one side derived from its `healthy:` block, +the other from its type's state rules, with nothing keeping the two consistent: + +```console +equation datastore-store-health-matches-state + can be broken by: store-fails-stopped (acknowledge in claims) + violated in 18 reachable situations witness: 1. store-fails-stopped +``` + +Half that system's reachable configurations disagree with themselves about +whether the component is healthy, and one failure reaches the nearest. It is a +property of the model rather than a wrong answer to any one scenario, which is +why testing scenarios does not find it. + +Declined constructs are named on stderr, as with `writ sql`; the emitted model +is kernel-only. The reading is worked through in +[`docs/mgtt-bridge.md`](docs/mgtt-bridge.md). + ## Install `writ` is a real opam package (`writ.opam`, generated from `dune-project`), and it @@ -522,6 +566,9 @@ ships in vocabulary for one subject, e.g. [`tests/models/politics.lib.writ`](tests/models/politics.lib.writ)) is ordinary user code and lives beside the models that load it. +- **The mgtt bridge:** [`docs/mgtt-bridge.md`](docs/mgtt-bridge.md) — how an + architecture model is read: why the fact reduction is lossless, why facts are + the only varying cells, and what is declined. - **The relational extension:** [`docs/interrogator.md`](docs/interrogator.md) — partly built. The `.rules` file, the built-in relations that expose the derived state category, and `writ derive` (§0–§2, §4, §5) ship; `writ solve`, diff --git a/docs/mgtt-bridge.md b/docs/mgtt-bridge.md new file mode 100644 index 0000000..838d891 --- /dev/null +++ b/docs/mgtt-bridge.md @@ -0,0 +1,338 @@ +# The mgtt bridge — an architecture read as a model + +`writ mgtt` reads a model written for [mgtt](https://github.com/mgt-tool/mgtt) +— a tool that makes a system's architecture executable — and emits a writ model +on stdout. It is a **reading**, in the sense `writ sql` is: the output is +kernel-only, a person owns it afterwards, and everything the input says that +the model cannot hold is named on stderr rather than dropped. + +This document is the kitchen. It explains *why* the mapping is shaped the way +it is, which is the part a user of the verb does not need and a person changing +it cannot do without. The verb's own reference is `writ mgtt --help`. + +## 1. Why this domain + +An mgtt model names a system's components, the dependencies between them, what +each component's *facts* are, which *states* those facts put it in, and how a +failing state propagates to whatever depends on it. + +That is [Appendix G](kernel-spec.md#appendix-g--problems-tractable-with-writ)'s +"incident-response runbooks" with the furniture already assembled — down to the +question the appendix asks first: *from every reachable incident state, is +recovery still reachable?* The fit is not a coincidence to be pleased about but +a constraint to be checked, and §G states the terms: finitely many kinds of +piece, rules that read as "only if … then this changes", laws that read as "two +routes must agree", questions about reachability and silence. An mgtt model +meets all four, and the one place it appears not to — its facts are integers — +is §3. + +What the domain supplies that writ's corpus lacks is a model **somebody already +wrote**. Authoring is the cost writ asks a new user to pay before it can say +anything at all; here it is already paid, by someone who paid it for their own +reasons. + +## 2. The seam is JSON, and the input is the resolved model + +`writ mgtt` does not read mgtt's YAML. mgtt emits a resolved document — +`mgtt model export --json` — and this verb reads that. + +Two reasons, and only the first is about effort. Writ is OCaml-stdlib-only by +policy; a YAML parser is a large thing to hand-write and a larger thing to keep +correct, while `tooling/json/` already exists because the LSP and MCP servers +needed it. The second reason is the one that would stand even if YAML were +free: *resolved* means mgtt has already merged each provider's type definitions +into the components using them and applied every component-level override. So +this side never implements mgtt's precedence rules, and cannot drift from them. +A bridge that re-decided whether a component's `healthy:` replaces or extends +its type's would be a second implementation of a rule that already exists. + +The document carries mgtt's own declines too — a component whose type fell back +to mgtt's generic placeholder, say — and they are forwarded rather than +absorbed. Silence about what the *other* side could not do would be the same +failure as silence about what this side could not do. + +## 3. The reduction — how facts stop being numbers + +Writ has no numbers ([§2.4](kernel-spec.md#24-the-language-stops-short-of-computation)), +and that absence is what buys the negative answer: `never` is a census rather +than a search that came back empty. mgtt's facts are `mgtt.int`, `mgtt.float`, +`mgtt.bytes`, `mgtt.duration`. So this section is where the crossing is either +honest or it is nothing. + +It is honest, and for a reason about mgtt rather than a cleverness here. +**mgtt's expression language has six comparison operators and no arithmetic.** +Its grammar is + +``` +or = and ("|" and)* +and = primary ("&" primary)* +primary = cmp | "(" or ")" +cmp = ref cmpop value +``` + +with `cmpop` one of `== != < > <= >=`. There is no `+`. Every predicate in an +mgtt model is therefore a comparison of one fact against a constant, or against +a sibling fact. + +From which the reduction follows. The constants a model mentions cut a fact's +value line into finitely many regions, and **every predicate in that model is +constant on each region**. So a region becomes a member of an enumerated type, +and two concrete values lying in one region were already indistinguishable to +mgtt's own engine. Nothing is approximated. This is the kernel spec's own move +— *counting becomes naming, calculating becomes writing down* — applied to a +fact rather than to a payment. + +### Cutting, then merging + +Cutting alone is not enough, and the reason is a state-space argument rather +than a tidiness one. Cut `connection_count` at 500 and you get three regions: +below it, exactly it, above it. But if `< 500` is the only predicate the model +applies, nothing distinguishes 500 from 501, and carrying three members would +put a distinction in the model that no rule can make — doubling that fact's +contribution to the product to represent a difference the engine could never +observe. + +So the regions are cut by every constant and then **collapsed wherever no +gathered predicate separates two neighbours**. Whether a fact's domain ends up +coarse or fine is decided by what the model asks of it, not by its type. Two +facts from the same worked model, both integers, both compared against zero: + +```lisp +(type gateway-upstream-count (below-0 exactly-0 above-0)) +(type workload-endpoints (below-0 above-0)) +``` + +The gateway's states use both `upstream_count > 0` and `upstream_count == 0`, +and those two predicates disagree about zero, so zero must be a member of its +own. The workload only ever asks `endpoints > 0`, so nothing tells zero apart +from anything else below one, and the two regions merge. Same type, same +constant, different domains — because the models ask different questions. + +### Where it stops + +A fact compared with a *sibling* fact needs a joint domain rather than an +independent one, since the predicate reads the pair: `ready_replicas == +desired_replicas` constrains two cells at once. Those become one cell with +three members, which is exactly what six operators can distinguish about two +values with no arithmetic between them: + +```lisp +(type workload-desired-replicas-vs-ready-replicas (fewer equal more)) +``` + +The pair is named from the alphabetically-first fact, so one pair spells one +way however the author wrote it. + +**A fact compared both with a sibling and against a constant is not carried.** +`ready_replicas == desired_replicas` wants an ordering; `desired_replicas == 0` +wants regions; both constrain the same two cells, and the joint domain over +both is not implemented. The behaviour is sound but lossy — guards needing the +constant are refused, so the moves that would use them are **not emitted** +rather than emitted wrongly — and it is declined by name. It is the one gap +that costs coverage rather than merely reporting less, and it is the first +thing to fix. + +A non-integer constant is refused outright. Writ has no floats to name a member +after and no ordering worth inventing for one, and refusing loudly is what +`writ sql` does with arithmetic in a `CHECK`, for the same reason. + +## 4. What a state is here + +The decision that shapes everything downstream: **facts are the only varying +cells. There is no `state` arrow.** + +The alternative is obvious enough to be worth refuting. mgtt names states — +`live`, `degraded`, `draining` — and an arrow into an enumerated type of those +names would be the direct translation. It fails on the question the bridge +exists to answer. A component's state and its health are *both* predicates over +its facts; carry the state as a cell and their agreement becomes something this +emitter computes and reports, rather than something the model states and writ +decides. A law you evaluate yourself is not a law, it is a lint. + +Carrying the facts and deriving both makes the agreement an `equation` over +real cells — §5 — and it is also what keeps the space small, §7. + +## 5. The law, and why a type per override + +The law is: **a component is healthy exactly when it is in its default active +state.** + +```lisp +;; healthy: available == true & connection_count < 500 +;; active: available == true +(equation datastore-health-matches-state + (iff (and (is datastore.available yes) (is datastore.connection-count below-500)) + (is datastore.available yes))) +``` + +`iff` is generated into the file rather than shipped: a law must be a guard, +mutual implication is two of them, and a form renames and pastes so an error +inside it still points at a line that exists. Every emitted block carries the +mgtt text it came from as a comment, so a finding walks back to a line of YAML. + +Now the constraint that shapes the schema. +[§8.6](kernel-spec.md#86-equation) requires a law's subject to be a **declared +type** — *"chains are written from the type, not an entity"* — so that the law +ranges over every entity of it. But mgtt lets a single component override +`healthy:` while keeping its type, and that override is precisely the case +worth catching: it is where a component's own definition of health drifts from +the state rules it is judged by. + +A law rooted at the shared type could not see it. So the emitter groups +components by **(mgtt type, effective healthy)** and emits one writ type per +group: components agreeing with their type keep its name, and any component +overriding gets a type of its own, named for both. Its law then ranges over +exactly one entity — that component — which is what per-component checking +requires, obtained without adding a construct. + +## 6. The moves + +### Origination, and why it cannot be omitted + +Each component gets one move per non-default state: from healthy into that +state, guarded on being healthy now. + +```lisp +(transition store-fails-stopped + (when (is store.available yes)) + (do (set store.available no))) +``` + +This looks like an addition and is a necessity. Propagation only *relays* a +failure from a dependency; with nothing to originate one, no move is ever +enabled at the initial situation, and the model enumerates exactly one +situation with no edges — every question answering vacuously, every law holding +because nothing can reach a counterexample. That is not a small model, it is a +model that says nothing while appearing to pass. + +mgtt supplies the origin from outside: an injected fact in a scenario, a probe +result at 3am. Its own scenario enumerator supplies it the same way, by taking +each component in turn as the root cause. Measured on the four-component +worked model: **1 situation and 0 edges without these moves, 36 and 138 with.** + +### Propagation, from mgtt's own label protocol + +mgtt declares propagation in two halves: a failing state emits `can_cause` +labels, and a state of a dependent declares `triggered_by` labels it answers +to. One transition per matching (dependency edge × emitted label × triggered +state): + +```lisp +(transition store-stopped-triggers-api-degraded + (when (and (is store.available no) (is api.desired-replicas-vs-ready-replicas equal))) + (do (set api.restart-count above-5) (set api.desired-replicas-vs-ready-replicas more))) +``` + +The effect writes a **representative assignment** of the target state — the +first, in domain-declaration order, that satisfies its guard. First rather than +any, because the choice must be reproducible: two runs of the emitter that +picked differently would produce two models from one input, and `writ compare` +would report a change nobody made. Only the cells that actually differ from the +default state are written, so `can be broken by` stays truthful about what each +move touches. + +Note the guard's second half. A propagation move requires the dependent to be +*healthy now*, which is what keeps the moves monotone — §7 — and keeps a +witness route reading as a chain of distinct events rather than a component +degrading twice. + +Moves are named, always. A witness route prints move names, and an unnamed move +makes the route unreadable, which is most of what a route is for. + +## 7. What an answer costs + +The standing worry about the direct translation is the product: twenty +components at four states each is 4²⁰, and no enumeration survives that. + +It does not form, and the reason is structural rather than lucky. The initial +situation is every component healthy; origination moves lead away from health; +propagation moves lead away from health. **No move restores it.** So the +reachable set is not the product of the state domains but the set of *consistent +failure configurations* — which is the set mgtt's own enumerator walks when it +writes `scenarios.yaml`. + +Measured, on the same four-component model: writ reports 36 situations and 138 +edges; mgtt's enumerator writes 76 chains. The two count different objects — a +chain is a route from a root cause, a situation is a whole-system configuration +— so neither number bounds the other, and the point is not that one is smaller. +The point is that both are in the tens, from a model whose naive product is in +the hundreds. + +[§14](kernel-spec.md#14-conformance) permits an implementation limit no lower +than 200 000 situations. A deployment large enough to exceed it is one whose +answer set was too big to have wanted, which is the README's reading of when a +model is too big, and it applies unchanged here. + +**What would cost.** Adding repair moves — a component recovering — makes +states mutually reachable, the product forms, and the argument above is gone. +That is not an oversight: it is the price of asking whether recovery is always +still reachable, and it should be asked deliberately and scoped, not switched on +by default. + +## 8. What is declined + +Named on stderr, grouped by reason with a count and a first subject, never +dropped. Aggregation is not tidying: forty components resolving to a generic +placeholder would otherwise bury the one decline that mattered. + +| Declined | Why | +|---|---| +| a fact compared with both a sibling and a constant | §3 — the joint domain is not implemented; moves are lost, not faked | +| a non-integer constant | no member name, and no ordering worth inventing | +| a fact no predicate mentions | no regions to name, so no arrow to make | +| a state no assignment satisfies | it is unreachable, which is a finding in itself | +| a model whose dependencies pair no `can_cause` with a `triggered_by` | it has no moves at all, and would report clean | +| mgtt's own declines | forwarded unchanged | + +The last two deserve their standing. A model with dependencies but no +propagation enumerates one situation and reports no findings — the most +misleading answer this bridge could give, and the shape a provider ships when +it declares `can_cause` and omits the other half. And a `state` nothing can +satisfy is the same finding mgtt's own validation reports for a `triggered_by` +label with no producer, arrived at independently. + +Two things are **out of scope by design** rather than declined, and the +distinction is the one writ already draws between a `gap` and a dead end. Probe +cost and ranking stay with mgtt: writ has no numbers, and *can these be told +apart at all* is the question upstream of *which to check first*. TTL and +staleness stay with mgtt: writ has no clock. + +## 9. End to end + +```console +$ mgtt model export --json > system.json +$ writ mgtt system.json > system.writ +$ writ check system.writ +states: 36 edges: 138 +gaps: none +dead ends: 4 + reached by: api-fails-degraded, edge-fails-draining, frontend-fails-degraded, store-fails-stopped +equation datastore-store-health-matches-state + can be broken by: store-fails-stopped (acknowledge in claims) + violated in 18 reachable situations witness: 1. store-fails-stopped +$ echo $? +1 +``` + +That finding is the whole argument in one line. The model's `store` overrides +`healthy:` to check `connection_count` and forget `available`, while its type +derives its state from `available`. Half of the reachable configurations of +that system disagree with themselves about whether the component is healthy, +and one failure is enough to reach the nearest one. It is not a wrong +conclusion about any particular scenario, so no scenario finds it; it is a +property of the model, and properties of the model are what exhaustion is for. + +## 10. Deliberately absent + +- **The other direction.** `writ sql` reads both ways because a relational + schema and an olog are two spellings of one object. An mgtt model is a + description of a system; writing one back from a writ model would be + synthesis, and a different feature. The door is open; the verb is not. +- **Live probing.** The bridge is design-time. `diagnose` is mgtt's. +- **Repair moves**, §7 — until the question that needs them is asked + deliberately. +- **Diagnosability** — whether two distinct root causes produce identical + observable facts, which caps how well any engine can diagnose the system. + It is a rules query over the derived state category + ([interrogator.md §2](interrogator.md)) rather than a change to this reading, + and it is the next thing worth building.