Formal: readability and change-cost plan for the Quint tree (glossary, kernel docs, naming, catalog prose, ledger churn) #220

Revision 3.2, 2026-10-08. Phase 1 was executed as #223 without the refresh-commands PR landing first (the ledgers were re-keyed with a session script); E1 therefore moves to the front of Phase 2 as PR 3a. Paths in this issue are pre-move; the mapping is in #221 and the file is now at formal/tools/check-source-audit.mjs and so on.

Revision 3.1, 2026-10-02. After the two reviews on #221: Phase 1's navigation criterion is the locate test and the C45 contract-navigation test moves to N1 in Phase 3; the differential fallback covers sources as well as manifests.

Revision 3, 2026-10-02. States the purpose (a specification consumable by humans and LLM agents), adds the directory layout move as Phase 1 (child issue #221), renames the three-PR milestone to Phase 2 and the candidates to Phase 3, and adds per-directory indexes and a navigation test to acceptance. File paths in this issue are today's; after Phase 1 they move per the child issue's mapping (tools/, catalogs/, generated/, guides/, models/).

Revision 2, 2026-09-29. Revised after the review in the first comment. E2 no longer promises per-section hashes (the spans nest), E3 keeps content hashes for test sources, the differential acceptance criterion is stated as what the tool checks, and the plan became a three-PR first milestone with everything else held as candidates. Earlier text is in the edit history.

Summary

The formal tree has the right architecture (cache-rules as the judgment layer, a kernel library that states each rule once, composed profiles guarded by a two-way corpus differential), and its shared rules, verification models and walkthrough read well. What does not read well is the kernel library's commentary and its README, the private vocabulary nobody defines, and the hand-written prose inside the JSON catalogs. What costs the most to change is not Quint but the ledgers around it: a docs-only edit touches two catalog files, and a one-profile fix touches eight files across four catalogs.

The purpose of all of it is a specification that humans and LLM agents can consume. For both readers that means the same things: the directory listing is the map; every fact is stated once, at the definition that implements it, with a contract ID a grep can find; the vocabulary is defined; and the large catalogs have compact indexes a reader can hold in view. Line width is a human concern; header length, sentence length and undefined terms are what cost a model comprehension.

This issue is the implementation plan for fixing presentation and change cost without changing behavior. Nothing here alters what the models permit, what the drivers compare, which properties, challenges and witnesses are checked, or any encoding in the driver contract. It complements #165 (the kernel architecture and what still needs composing) and #166 (the documentation site); it does not move work out of either.

Measured on main at d470b2f (2026-09-28) by static analysis; Quint was not run for these numbers.

Where the tree is today

Goals and non-goals

Goals:

• The directory listing is the map: one README at the top of formal/, role-named directories, each with an index of at most fifteen lines.
• A reader finds what a kernel module does in its first three lines, and the rules under the definitions that implement them, each tagged with its contract ID.
• Every recurring term is defined once and linked from its first use.
• The kernel has a stated dependency layering and reading order.
• A docs edit touches its own file and one ledger entry, nothing else. A changed test assertion still invalidates the Go applicability review.
• Two mechanical style rules, line width and header length, cannot regrow; everything else about style is measured and reviewed, not enforced.

Non-goals, frozen for the whole plan:

• No behavior, observation, encoding or bounds change in any model. For every Quint edit, make differential must report every reference and candidate history agreeing in both directions, and the reviewer confirms the reported bytes-per-state ratio is unchanged. The tool compares driver-asserted channels step by step and fails only above a 1.2 bytes ratio; it does not compare corpus bytes, so "unchanged" is a reviewer's reading of the report.
• The driver contract is untouched: input.name strings, choice encodings, observation fields, integer codes, ...Test names and profile public action names.
• No change to which invariants, challenges, witnesses or mutants are checked.
• Composing the core profile (a driver-contract change in four ports) and folding verification models stay under Formal: converge the Quint specification on one kernel model with profile instances #165. The documentation site stays under Docs: language-neutral behavior pages, generated per-language references, and executed examples #166.

Phase 1: layout

Two PRs were planned; the move landed first as #223, and the refresh-commands PR follows as the first PR of Phase 2.

PR 1. Ledger refresh commands (E1). Add node formal/check-source-audit.mjs --refresh <path>...: recompute the hash and heading inventory for the named files, keep the contract dispositions of headings whose title is unchanged, and leave new headings with an empty disposition so the check fails until a reviewer fills it. Add node formal/check-go-parity.mjs --refresh-inputs for the six input digests. Today both steps are done with scripts outside the repository. Document both in TEST-AUDIT.md. Done when a guide edit is refreshed by the two documented commands and make audit passes. Size S. This lands first because the layout move re-keys every guide ledger entry with these commands.

PR 2. Group formal/ by role: #221. The top level becomes README.md plus guides/, models/ (with kernel/ and fixtures/kernel/ beneath it, so no Quint import changes), replay/, tools/, catalogs/ and generated/, each with an index README. About 3,500 literal path edits, all made by one committed migration script, plus regeneration of the traces that embed their own paths and a transitional fallback in the differential so it can read the reference revision's manifests and Quint sources from the old layout. It goes first so that everything in Phase 2 is written once against the final paths, and because it conflicts with every open branch under formal/, so it lands alone when nothing else is in flight. Size M. The child issue carries the target tree, the grouping rules, the mapping, the verification list and the deferred splits.

Phase 2: ledgers, glossary, kernel documentation

The former three-PR milestone, minus the refresh PR, written against the Phase 1 layout. After it lands, an ordinary contribution (a behavior fix or a coverage addition) is the measurement of what remains painful, and Phase 3 is reassessed against it.

PR 3a. Ledger refresh commands (E1), carried over from Phase 1

As described under Phase 1 PR 1; paths are now formal/tools/check-source-audit.mjs and formal/tools/check-go-parity.mjs. Until it lands, a guide edit is re-keyed with the exported snapshot functions, as the #223 ledger refresh was.

PR 3. Ledger decoupling, narrowly (E2 and E3)

E2, stable heading identity. source-audit.json schema 2 keys each Markdown entry by a heading slug plus an occurrence index instead of line. The whole-file hash stays the review trigger. Effect: an edit changes the file's hash line and no other line of that file's entry list, instead of renumbering every heading below the edit. Revision 1 proposed per-section hashes; those spans nest (an H2 section contains its H3s), so an H3 edit would have changed three hashes. Non-overlapping section hashes remain an option if whole-file review proves too coarse.

E3, go-parity stops depending on Markdown bytes. check-go-parity.mjs re-hashes every audited file today, both the 29 test files and the 21 documentation files, and pins the audit file's bytes in inputs.sourceAuditSha256. Change it so that:

• test sources (.ts) keep their content hash check exactly as today, because a changed assertion can change what Go must mirror;
• documentation sources (.md) are compared by their dispositions (path, heading identity, contracts), not their bytes;
• inputs.sourceAuditSha256 becomes a digest over the audit's schema, the test-source hashes, every disposition and the reviewed-guide review metadata, excluding Markdown byte hashes.

Tests: formal-source-audit.test.ts and formal-go-parity.test.ts gain two cases, a prose-only edit that leaves go-parity clean and a changed test assertion that still fails it. Update TEST-AUDIT.md in the same PR.

Done when a change like #214 touches its Markdown file and one source-audit.json entry, and zero lines of go-parity.json, while a changed test assertion still fails the go-parity check. Size M.

PR 4. Glossary and kernel documentation (A1, A2, A3)

May land as a short series if the header rewrite is split by kernel layer.

A1. guides/GLOSSARY.md. About 45 terms, one paragraph each, naming the file that owns the concept: driver, coordinator, profile, verification model, connection model, kernel library, shape, projection, variant, judgment and "judged once" and "applied from a judgment", seam, receipt, consulted record, pending-only record, opt-in record, held versus immediate reply and effect, atomic path versus held path, lifecycle (budgeted, held, atomic, diagnosed, metered), flight, source and loader and ordinal, effect index, C0 and C1, dark job versus served job, witness and label and classifier, fidelity, challenge and fault and mutant and reproducer, native mutant, exclusion (structural versus measured), corpus and history and regression and exported run and public-only run, smoke, lane, evidence, ledger, differential, bytes per state, settlement and settlement receipt, fence and watermark and marker, frame and stamp and retention and freshness, layout, resolution and reply and TTLs and effective TTLs and gated layers, participating and bypass, scope and context and persistent context and memo slot, identity and slot, encodings and sentinels. Add a "Look up a term" row to the README task table and a pointer in AUTHORING "Reading a model". A new file under guides/ joins the reviewed-guide inventory, so its reviewedGuides entry (kind tooling-guide) lands in the same PR. Link the first use of each term in README, AUTHORING and the kernel README.

A2. Kernel module headers. One template for all 29 modules: one sentence of purpose; "Rules" as bullets of at most two lines, each naming its contract IDs; "Shapes" one line per type alias; "Consumers" naming the profiles that compose the module; a "Ports" trailer holding every pointer into TypeScript and Go source. Cap the header at 25 comment lines. Rule prose that exceeds the cap moves onto the definition that implements the rule: comment the definition, not the module. Order of work, by current header length: shadow 124, remote-io 59, deadlines 57, payloads 50, metrics 49, recovery 41, remote-writes 37, markers 35, remote-frames 35, local-faults 32, serving 31, then the rest. Split sentences over 40 words while there.

A3. Restructure the kernel README.

• Modules table: one sentence of concern plus the entry points per row, at most 40 words per cell. Rules live in the module headers only; the README stops being the fourth restatement of each rule after SPEC, CONTRACTS and the header.
• New "Layering and reading order" section, hand-written from the import graph. Layers by dependency depth as measured today: 0: encodings, calls, clock, layer_policy, config_errors, instances; 1: request_memo, local_storage, payloads, policy_gate, flights, policy_overlay, runtime_policy; 2: remote_frames; 3: recovery, serving; 4: remote_io, receipts, local_faults, local_grid, markers; 5: deadlines, compression; 6: remote_writes, adapter_replies, diagnostics; 7: shadow, metrics; 8: shadow_reads. No freshness check for now; one becomes a candidate if the section drifts.
• Move "Record of the layers rewrite" through "Separate shadow read deadlines" (lines 428 to 700) to guides/HISTORY.md (reviewed-guide kind historical-evidence, with the revisions each record was measured at). Update the AUTHORING pointer to "the record table" for differential.maxBytesPerStateRatio reasons. The VALIDATION "Historical results" section moves to the same file; the pilot measurements stay in Formal: converge the Quint specification on one kernel model with profile instances #165, which HISTORY.md links.
• Keep "Composing a profile" and "Migrating a profile"; split their sentences to 40 words or fewer without changing content.

The kernel README is outside the reviewed-guide inventory (the guide scan covers guides/ and the top-level README after Phase 1), so its rewrite carries no ledger refresh; HISTORY.md under guides/ joins the inventory and needs an entry.

Verification for the Quint comment edits in A2: node formal/tools/execution.mjs (a comment that quotes an anchored expression makes that challenge anchor ambiguous); node formal/tools/generate-artifacts.mjs --write then make fixtures-check (the fixtures lock pins kernel source hashes); make kernel-fixtures; make differential reporting every history agreeing in both directions, with the reviewer confirming the bytes ratio is unchanged. Size M.

Phase 3: candidates

Each of these stays a proposal until an ordinary contribution shows the pain it addresses. Sizes: S under a day, M one to three days, L three to five.

C1. Naming key and targeted renames (M). Write the key into the kernel README. Verbs: admit (a caller enters and its policy call is counted or held), release (the drivers release a held reply or effect by index), settle (an effect completes with the outcome the environment supplies), expire (a deadline is delivered), begin (admission and release in one step for immediate replies), start (a source or loader begins), hold (a pending-only record is created), record (a channel fact is appended). Suffixes: Local and Request are traversal projections; Judged applies a judgment already made; Held is over the held remote lifecycle; Job is a shadow job's own effect; Dark and Served name the job kind. Rename only names that hide meaning; judgeReleaseUnder to judgeReleaseWithLocalFault is the demonstrated case. Other candidates, to confirm one by one:

Frozen: profile action names, input.name strings, ...Test names, encodings. Per rename: update callers in profiles and fixtures; update challenge anchors whose before/after text names the definition (one today, shadow-fill-before-source; the manifest check fails on any broken anchor); grep nativeMutants.text, exclusion reasons and guides for the old name. Gate: the differential as stated above, make kernel-fixtures, the lint baseline check.

B1. Measurements plus two mechanical caps (M). tools/check-style.mjs --report prints the measurement table above so progress is reproducible; sentence length, parameter width and comment sentence length are reported only, and the editorial guidance for them lives in AUTHORING "Writing conventions". Two rules are enforced in the audit lane because guidance alone has not held for them (AUTHORING already asks for lines without horizontal scrolling and the kernel breaks that 658 times): Quint line length at most 120 and module header comment at most 25 lines. Enforcement is over files not named in a static allowlist of today's offenders; the allowlist shrinks by deleting a file's line when A2 cleans it and carries no counts, so nothing is refreshed when a number improves. Target: an empty allowlist when A2 finishes. Quint 0.32.0 has no formatter, so wrapping stays manual.

C2. One record for resolution and TTLs; named flags at four sites (M). Add layer_policy::Reply = { resolution: Resolution, ttls: Ttls }. Across the kernel, profiles and fixtures, 30 signatures take the two together; 20 of them have no read budget (local and request projections, the atomic path), so the budget stays a separate parameter at the 10 held-lifecycle sites and does not enter the record. Replace the two adjacent booleans with named record fields at the four definitions that have them: judgeReleaseUnder (observed, localFailed), authority (read, readOk), startLoader (readOk, visible), newJob (dark, logging). Single booleans such as failed at 25 sites mirror the drivers' fail-or-release split and stay. Constraint: no state field changes shape, because ITF bytes and the fidelity views read private state; parameters are not state, so the reported bytes ratio must be unchanged. Land per kernel layer with the differential per PR.

C3. Shapes listing, on demand (S). node formal/tools/shapes.mjs unfolds every kernel shape alias through the quint parse IR (lint-profiles.mjs already resolves typedefs) and prints the flat field list with the owning module, so a reader can answer "what fields does Metered have" without unfolding five files. No committed file and no checker: Quint's typechecker already rejects a profile State that lacks a field a transition needs, and the lint already rejects incompatible lifecycle combinations.

N1. Contract lookup, on demand (S). node formal/tools/where.mjs C45 prints where a contract is stated (SPEC section, CONTRACTS row), tested (Quint definitions and runs, scenarios, vectors), challenged (challenge IDs) and mapped to native mutants, read from the catalogs the audit already parses. This is the navigation test below as a command, for agents and for reviewers assembling a context packet. No new data, no gate.

D1. Generated read views of the catalogs (S). node formal/tools/generate-catalog-docs.mjs --write produces guides/CHALLENGES.md (per challenge: contract, source and anchor, invariant, native mutant kind and text, reproducer run, failure, profiles, exclusions) and guides/MUTANTS.md (per mutant: case, description, rationale, edits per port, required detections), freshness-checked in audit. The JSON stays the source of truth.

D2. Exclusion vocabulary (M). Reproducer exclusions become { "<profile>": { "reason": "<slug>", "note": "<at most 120 characters, optional>" } } with a controlled slug list mined from the 530 current strings; candidates: no-remote-layer, no-clock, no-frames, no-held-effects, no-shadow-jobs, no-recovery, no-deadlines, immediate-replies-only, untracked-only, request-only-projection, local-projection, bounds-never-reach-boundary, fixture-never-declines-frame. The manifest check validates the slug; the checker's holds measurement remains the evidence, which AUTHORING already states.

D3. Catalog formatting and caps (S). Write execution.json, mutations.json and semantic-cases.json through compact-json.mjs with one record per block and a stable key order so a diff is one entry. Cap new nativeMutants.text at 300 characters, rationale at 400 and scope at 200.

A4. Generate PROFILES.md; shrink BEHAVIOR.md (M). The six "Generated ... profile" sections (6,576 words) restate the descriptors in replay/features.mjs, replay/local-clock.mjs, replay/profiles/*.mjs and profiles.json. Generate guides/PROFILES.md from them (per profile: model, version, fixture choices, each command with its choice decoding into the driver input, observation fields, smoke trace), freshness-checked in audit; BEHAVIOR.md keeps the scenario format, fixture, inputs and completion boundaries, observations, events and port workflow, about 3,000 words.

A5. Demote the core profile (S). Move core to the last row of the README profile table, labelled introductory and uncomposed, with one sentence in CONFORMANCE.md saying its drivers read model state and that composition is tracked in #165. Could ride along with A3.

A6. Guide sentence pass (S). Split sentences over 40 words in AUTHORING (24), PORTING (15), SEMANTIC-COVERAGE (8), VALIDATION (7) and README (3) without changing content.

Verification by change type

Acceptance

Phase 1:

Phase 2:

Phase 3, if adopted:

Risks

• The layout move conflicts with every open branch under formal/ and the differential needs a transitional fallback to read the old layout's manifests; both are handled in the child issue.
• A comment edit can quote an anchored expression and make a challenge anchor ambiguous. The manifest check runs in audit on every PR and catches it.
• E2 keeps whole-file review, so a reviewer still re-confirms every disposition of an edited file; if that proves too coarse, non-overlapping section hashes are the next step.
• E3 changes what the go-parity review pins for documentation; the two new tests (prose-only edit clean, changed assertion red) are the guard against loosening it further than intended.
• Renames invalidate prose that names definitions in challenge text, exclusion reasons and guides. C1 carries a grep step.
• C2 touches every profile and fixture. Land it per kernel layer with the differential per PR, and confirm the reported bytes ratio did not move.
• Each generated document (CHALLENGES, MUTANTS, PROFILES) adds a freshness check; each needs its --write command documented in AUTHORING "Refactoring and execution" before it lands.

Related

#221 is Phase 1 of this plan. #165 owns composing core, folding verification models and the remaining kernel migration. #166 owns the documentation site. #171 and #172 hold the pilot records that HISTORY.md links.