writ mgtt — read an mgtt architecture model as a writ model

[sajonaro]

Adds writ mgtt, a reading of mgtt architecture models, in the tradition of writ sql: a foreign notation read into a model the user then owns, kernel-only output, declines named on stderr, --strict for CI.

Why it works

mgtt's expression language (internal/expr/parser.go) has six comparison operators and no arithmetic. So the constants a model mentions cut each fact's value line into finitely many regions on which every predicate is constant — a region becomes a member, and two values in one region were already indistinguishable to mgtt's own engine. The crossing is lossless rather than approximate.

Regions nothing separates are merged, so connection_count < 500 costs two members, not three.

What it reports

The load-bearing finding is a law: a component is healthy exactly when it is in its default active state. mgtt derives one side from healthy: and the other from the type's state guards, and nothing keeps them consistent. Here it is an equation, so writ check names the move and routes to the violation:

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

Two decisions worth review

Facts are the only varying cells — there is no state arrow. States and healthy are both predicates over facts, so deriving both makes their agreement a real law rather than a check the emitter performs. Because a law's subject must be a declared type (§8.6), a component overriding healthy: gets its own emitted type so its law ranges over it.

Origination moves. Propagation only relays a failure, so without a move letting each component fail on its own the model enumerates one situation and every question answers vacuously. mgtt gets this from a scenario or a probe. Measured on a four-component model: 1 state without them, 36 states / 138 edges with.

Known gap

A fact compared both with a sibling fact and against a constant is not carried — ready_replicas == desired_replicas wants an ordering, desired_replicas == 0 wants regions, and both constrain the same cells. Behaviour is sound but lossy: the guards are refused so the moves are not emitted rather than emitted wrongly, and it is declined by name.

Layout

tooling/mgtt/ depends on writ_json and nothing else — it never builds a model, so a malformed export cannot reach the engine. IO stays in tooling/cli/cmd_mgtt.ml.

make test green; 55 new checks in tests/unit/test_mgtt.ml, including reading the emitted model back through the real front end (asserting on the text would pass just as happily if the text were confidently wrong).