feat(formal): measure Quint style and enforce two caps

formal/catalogs/README.md

@@ -26,6 +26,7 @@ output lives in [../generated/](../generated/README.md), never here.
 - [go-parity.json](./go-parity.json): the Go parity ledger over the catalogs, sources and audit; `check-go-parity.mjs`; its catalog, audit-dispositions and vector artifact digests re-pinned with `check-go-parity.mjs --refresh-inputs`, its mapping hashes by hand with the review.
 - [profile-lint-baseline.json](./profile-lint-baseline.json): the composition lint ratchet per profile; `node formal/tools/lint-profiles.mjs baseline --check`; `--write` after a reviewed fall.
 - [witness-baseline.json](./witness-baseline.json): the recorded witness hit counts the exploration gate compares against; `witnesses.mjs`; `baseline --write`.
+- [style-allowlist.json](./style-allowlist.json): the Quint files exempt from a style cap (line length, header length) because they broke it when the cap landed; `check-style.mjs`; a stale entry fails, so the list shrinks by deleting a file's entry once it is clean, and grows only as a reviewed exception.
 
 ## Fixed vector corpora
 

formal/catalogs/source-audit.json

@@ -1102,7 +1102,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "75ad1133cd6df5c50f9d4602022a92fb06281ea152b3dae43a60886a4b721489",
+      "sha256": "7f3aee31a1f311f27420550960f1ceed757ecae1f1616bea01436a9635cd12f6",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},

formal/catalogs/style-allowlist.json

@@ -0,0 +1,68 @@
+{
+  "lineLength": [
+    "formal/models/dialcache-admission-conformance.qnt",
+    "formal/models/dialcache-core.qnt",
+    "formal/models/dialcache-dark-layers-conformance.qnt",
+    "formal/models/dialcache-effects-conformance.qnt",
+    "formal/models/dialcache-envelope-vectors.qnt",
+    "formal/models/dialcache-frame-vectors.qnt",
+    "formal/models/dialcache-independent-conformance.qnt",
+    "formal/models/dialcache-independent-connection.qnt",
+    "formal/models/dialcache-invalidation-transition.qnt",
+    "formal/models/dialcache-key-protocol.qnt",
+    "formal/models/dialcache-layers-conformance.qnt",
+    "formal/models/dialcache-local-clock-conformance.qnt",
+    "formal/models/dialcache-local-failure-conformance.qnt",
+    "formal/models/dialcache-policy-conformance.qnt",
+    "formal/models/dialcache-recovery-conformance.qnt",
+    "formal/models/dialcache-recovery-connection.qnt",
+    "formal/models/dialcache-recovery-read-conformance.qnt",
+    "formal/models/dialcache-recovery-read-connection.qnt",
+    "formal/models/dialcache-runtime-boundaries-conformance.qnt",
+    "formal/models/dialcache-runtime-policy.qnt",
+    "formal/models/dialcache-scope-conformance.qnt",
+    "formal/models/dialcache-shadow-conformance.qnt",
+    "formal/models/dialcache-shadow-layers-conformance.qnt",
+    "formal/models/dialcache-shadow-read-deadlines-conformance.qnt",
+    "formal/models/dialcache-source-budgets-conformance.qnt",
+    "formal/models/dialcache-stale-recovery.qnt",
+    "formal/models/fixtures/kernel/budgeted-local.qnt",
+    "formal/models/fixtures/kernel/fractional-clock.qnt",
+    "formal/models/fixtures/kernel/frame-clocks.qnt",
+    "formal/models/fixtures/kernel/frames-and-faults.qnt",
+    "formal/models/fixtures/kernel/held-dark-shadow.qnt",
+    "formal/models/fixtures/kernel/held-diagnostics.qnt",
+    "formal/models/fixtures/kernel/held-remote.qnt",
+    "formal/models/fixtures/kernel/held-replies.qnt",
+    "formal/models/fixtures/kernel/held-shadow.qnt",
+    "formal/models/fixtures/kernel/held-writes.qnt",
+    "formal/models/fixtures/kernel/local-faults.qnt",
+    "formal/models/fixtures/kernel/local-projection.qnt",
+    "formal/models/fixtures/kernel/markers.qnt",
+    "formal/models/fixtures/kernel/payload-classes.qnt",
+    "formal/models/fixtures/kernel/request-only.qnt",
+    "formal/models/fixtures/kernel/shadow-jobs.qnt",
+    "formal/models/kernel/adapter-replies.qnt",
+    "formal/models/kernel/compression.qnt",
+    "formal/models/kernel/deadlines.qnt",
+    "formal/models/kernel/diagnostics.qnt",
+    "formal/models/kernel/flights.qnt",
+    "formal/models/kernel/local-faults.qnt",
+    "formal/models/kernel/local-grid.qnt",
+    "formal/models/kernel/local-storage.qnt",
+    "formal/models/kernel/metrics.qnt",
+    "formal/models/kernel/payloads.qnt",
+    "formal/models/kernel/receipts.qnt",
+    "formal/models/kernel/recovery.qnt",
+    "formal/models/kernel/remote-frames.qnt",
+    "formal/models/kernel/remote-io.qnt",
+    "formal/models/kernel/remote-writes.qnt",
+    "formal/models/kernel/serving.qnt",
+    "formal/models/kernel/shadow-reads.qnt",
+    "formal/models/kernel/shadow.qnt"
+  ],
+  "headerLength": [
+    "formal/models/fixtures/kernel/held-remote.qnt",
+    "formal/models/fixtures/kernel/payload-classes.qnt"
+  ]
+}

formal/guides/AUTHORING.md

@@ -78,7 +78,18 @@ scrolling. Keep a genuinely short action compact. Prefer a descriptive
 intermediate state such as `published` or `completed` over a chain of `x`, `y`,
 and `z`. Comments should explain ownership, ordering, assumptions, or a boundary
 case, rather than narrate the syntax. Quint 0.32.0 has no CLI formatting command;
-these are reviewed authoring conventions.
+these are reviewed authoring conventions, with two of them enforced.
+`node formal/tools/check-style.mjs`, a step of `make audit`, fails a Quint line over
+120 characters and a module header over 25 comment lines in any `.qnt` file under
+`formal/models` not named for that rule in
+[style-allowlist.json](../catalogs/style-allowlist.json). The header is the `//`
+comment block beside the `module` line, written before it or after it, up to the
+first import or definition. The allowlist names the files that broke a cap when it
+landed and may only shrink: once a file is clean, delete its entry, or the check
+fails on the stale entry; adding an entry is a reviewed exception. `--report`
+prints the readability measurements so progress is reproducible: long lines,
+header lengths, comment and guide sentence lengths, parameter widths and the
+free-text exclusion reasons. Those are reported, not enforced.
 
 A kernel module under `formal/models/kernel/` opens with one header of at most
 25 comment lines, each within 100 columns, in a fixed shape: one sentence of

formal/tools/README.md

@@ -13,12 +13,16 @@ which scripts a target runs.
 - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites.
 - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory.
 
-## Checks (the `audit` lane runs `execution.mjs` and the first four)
+## Checks
+
+The `audit` lane runs `execution.mjs`, the first five checks below and the
+generated-fixture verification; `validation.mjs` is the list of record.
 
 - [check-source-audit.mjs](./check-source-audit.mjs): the docs and test review ledger against the current files; `--refresh <path>...` re-keys the named files after their review.
 - [check-semantic-coverage.mjs](./check-semantic-coverage.mjs): every semantic case cites scheduled checks, scenarios, vectors and witnesses.
 - [check-feature-coverage.mjs](./check-feature-coverage.mjs): the native feature inventory and its evidence references.
 - [check-go-parity.mjs](./check-go-parity.mjs): the Go parity ledger against the catalogs and both source trees; `--refresh-inputs` re-pins its catalog, audit-dispositions and vector artifact digests.
+- [check-style.mjs](./check-style.mjs): the two Quint style caps (lines at most 120 characters, module headers at most 25 comment lines) over files not in the style allowlist; `--report` prints the readability measurements.
 - [check-model-properties.mjs](./check-model-properties.mjs): the model-fault challenge catalog; `--only=<id>` measures one.
 - [check-kernel-fixtures.mjs](./check-kernel-fixtures.mjs): typechecks and runs the kernel fixtures (`make kernel-fixtures`).
 - [check-symbolic-models.mjs](./check-symbolic-models.mjs): the finite symbolic checks with Apalache (`make model-check`).

formal/tools/check-style.mjs

@@ -0,0 +1,175 @@
+// Style measurements and two mechanical caps for the Quint sources.
+//
+// `--report` prints the measurement table lan17/DialCache#220 tracks, so
+// progress is reproducible: lines over 120 characters, module header
+// lengths, comment and guide sentence lengths, parameter widths and the
+// free-text exclusion reasons. Those are reported only; the editorial
+// guidance for them is AUTHORING.md "Writing conventions".
+//
+// Without arguments two rules are enforced, because guidance alone did not
+// hold for them: a Quint line is at most 120 characters and a module header
+// is at most 25 comment lines. The header is the `//` comment block beside
+// the `module` line: the contiguous comment lines directly above it plus the
+// comment lines below it up to the first import or definition (blank lines
+// between them allowed), so a header written before `module`, as the kernel
+// fixtures do, counts the same as one written after. Enforcement is over the
+// `.qnt` files under formal/models not named in
+// formal/catalogs/style-allowlist.json. The allowlist names today's
+// offenders per rule and carries no counts; a file that becomes clean must be
+// deleted from it (a stale entry fails the check), so the list may only
+// shrink, and adding an entry is a reviewed exception.
+//
+// Measurement definitions, so the report is reproducible: a comment sentence
+// is a run of full-line `//` comments joined by spaces, with banner lines
+// (dashes only, or a title between dashes) removed, split before a capital
+// letter, backtick, bracket or parenthesis that follows sentence punctuation;
+// a guide sentence is the same split over a paragraph outside headings, tables
+// and code fences; a definition is a `def`, `pure def` or `action` with its
+// parameter list scanned to the matching parenthesis.
+import { readFileSync, readdirSync } from 'node:fs';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+export const root = fileURLToPath(new URL('../../', import.meta.url));
+export const allowlistPath = 'formal/catalogs/style-allowlist.json';
+export const caps = { lineLength: 120, headerLength: 25 };
+const read = (path, directory) => readFileSync(resolve(directory, path), 'utf8');
+
+export function quintFiles(directory = root) {
+  const walk = relative => readdirSync(resolve(directory, relative), { withFileTypes: true }).flatMap(entry =>
+    entry.isDirectory() ? walk(`${relative}/${entry.name}`) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []);
+  return walk('formal/models').sort();
+}
+
+// The header: comment lines after the `module` line, up to the first line
+// that is neither blank nor a comment.
+export function headerLines(lines) {
+  const start = lines.findIndex(line => /^\s*module\s+\w+/.test(line));
+  if (start < 0) return 0;
+  let count = 0;
+  for (let index = start - 1; index >= 0; index--) {
+    const trimmed = lines[index].trim();
+    if (trimmed.startsWith('//')) count++;
+    else if (trimmed !== '') break;
+  }
+  for (const line of lines.slice(start + 1)) {
+    const trimmed = line.trim();
+    if (trimmed.startsWith('//')) count++;
+    else if (trimmed !== '') break;
+  }
+  return count;
+}
+
+const isBanner = text => /^-{3,}/.test(text) || /^-{2,}\s.*\s-{2,}$/.test(text);
+
+// Every def, pure def and action with its parameters, the list scanned to the
+// matching parenthesis so an operator-typed parameter is one parameter.
+export function definitions(text) {
+  const found = [];
+  for (const match of text.matchAll(/\b(?:pure\s+)?(?:def|action)\s+(\w+)\s*\(/g)) {
+    let depth = 1, index = match.index + match[0].length, start = index;
+    const params = [];
+    for (; index < text.length && depth > 0; index++) {
+      const char = text[index];
+      if (char === '(' || char === '[') depth++;
+      else if (char === ')' || char === ']') { depth--; if (depth === 0) break; }
+      else if (char === ',' && depth === 1) { params.push(text.slice(start, index)); start = index + 1; }
+    }
+    const last = text.slice(start, index).trim();
+    if (last) params.push(last);
+    found.push({ name: match[1], params: params.map(param => param.trim()).filter(Boolean) });
+  }
+  return found;
+}
+
+const sentences = text => text.split(/(?<=[.!?])\s+(?=[A-Z`\[(])/).map(s => s.split(/\s+/).filter(Boolean).length).filter(Boolean);
+const area = path => path.includes('/fixtures/') ? 'fixtures' : path.includes('/kernel/') ? 'kernel' : 'models';
+
+export function measure(directory = root) {
+  const files = quintFiles(directory);
+  const areas = { models: 0, kernel: 0, fixtures: 0 };
+  const wide = { models: 0, kernel: 0, fixtures: 0 };
+  let longLines = 0, headerTotal = 0, headerMax = 0, headersOver = 0, definitionCount = 0;
+  const twoBooleans = [];
+  const commentWords = [];
+  for (const path of files) {
+    const text = read(path, directory);
+    const lines = text.split('\n');
+    const over = lines.filter(line => line.length > caps.lineLength).length;
+    longLines += over;
+    areas[area(path)] += over;
+    const header = headerLines(lines);
+    headerTotal += header; headerMax = Math.max(headerMax, header); headersOver += header > caps.headerLength;
+    const comments = lines.filter(line => line.trim().startsWith('//')).map(line => line.trim().replace(/^\/\/\s?/, '')).filter(line => !isBanner(line));
+    commentWords.push(...sentences(comments.join(' ')));
+    for (const definition of definitions(text)) {
+      definitionCount++;
+      if (definition.params.length >= 6) wide[area(path)]++;
+      const booleans = definition.params.filter(param => param.split(':').at(-1).trim() === 'bool').length;
+      if (booleans >= 2) twoBooleans.push(`${path.replace(/^formal\/models\//, '')}:${definition.name}`);
+    }
+  }
+  const guideWords = [];
+  for (const path of [...readdirSync(resolve(directory, 'formal/guides')).filter(p => p.endsWith('.md')).map(p => `formal/guides/${p}`), 'formal/README.md']) {
+    const text = read(path, directory).replace(/```[\s\S]*?```/g, '');
+    for (const paragraph of text.split(/\n\s*\n/)) {
+      if (/^\s*[#|]/.test(paragraph)) continue;
+      guideWords.push(...sentences(paragraph.split('\n').map(line => line.trim()).join(' ')));
+    }
+  }
+  const execution = JSON.parse(read('formal/catalogs/execution.json', directory));
+  const exclusionReasons = (execution.challenges ?? []).reduce((count, challenge) => count + Object.values(challenge.reproducer?.exclusions ?? {}).filter(value => typeof value === 'string').length, 0);
+  const average = values => values.length ? Math.round(values.reduce((a, b) => a + b, 0) / values.length * 10) / 10 : 0;
+  const distribution = values => ({ count: values.length, over40: values.filter(w => w > 40).length, over60: values.filter(w => w > 60).length, over100: values.filter(w => w > 100).length, longest: Math.max(0, ...values), averageWords: average(values) });
+  return {
+    files: files.length,
+    linesOver: { total: longLines, ...areas },
+    headers: { total: headerTotal, longest: headerMax, overCap: headersOver },
+    commentSentences: distribution(commentWords),
+    guideSentences: distribution(guideWords),
+    definitions: { count: definitionCount, sixOrMoreParameters: wide, twoBooleanParameters: twoBooleans },
+    exclusionReasons,
+  };
+}
+
+export function renderReport(m) {
+  return [
+    '| Measure | Value |', '| --- | --- |',
+    `| Quint files under formal/models | ${m.files} |`,
+    `| Lines over ${caps.lineLength} characters (models / kernel / fixtures) | ${m.linesOver.total} (${m.linesOver.models} / ${m.linesOver.kernel} / ${m.linesOver.fixtures}) |`,
+    `| Module header comment lines, total / longest / over ${caps.headerLength} | ${m.headers.total} / ${m.headers.longest} / ${m.headers.overCap} |`,
+    `| Quint comment sentences, count / over 40 / over 60 / over 100 words / longest / average | ${m.commentSentences.count} / ${m.commentSentences.over40} / ${m.commentSentences.over60} / ${m.commentSentences.over100} / ${m.commentSentences.longest} / ${m.commentSentences.averageWords} |`,
+    `| Guide sentences, count / over 40 / over 60 / over 100 words / longest / average | ${m.guideSentences.count} / ${m.guideSentences.over40} / ${m.guideSentences.over60} / ${m.guideSentences.over100} / ${m.guideSentences.longest} / ${m.guideSentences.averageWords} |`,
+    `| Definitions, count / six or more parameters (models / kernel / fixtures) | ${m.definitions.count} / ${m.definitions.sixOrMoreParameters.models + m.definitions.sixOrMoreParameters.kernel + m.definitions.sixOrMoreParameters.fixtures} (${m.definitions.sixOrMoreParameters.models} / ${m.definitions.sixOrMoreParameters.kernel} / ${m.definitions.sixOrMoreParameters.fixtures}) |`,
+    `| Definitions taking two or more boolean parameters | ${m.definitions.twoBooleanParameters.length} (${m.definitions.twoBooleanParameters.join(', ') || 'none'}) |`,
+    `| Free-text exclusion reasons in execution.json | ${m.exclusionReasons} |`,
+  ].join('\n') + '\n';
+}
+
+// The two caps over every file not allowlisted for that rule; an allowlisted
+// file that is clean is reported too, so the list only ever shrinks.
+export function checkStyle({ directory = root, allowlist = JSON.parse(read(allowlistPath, directory)) } = {}) {
+  const failures = [];
+  const listed = { lineLength: new Set(allowlist.lineLength ?? []), headerLength: new Set(allowlist.headerLength ?? []) };
+  const files = quintFiles(directory);
+  for (const rule of Object.keys(listed)) for (const path of listed[rule]) if (!files.includes(path)) failures.push(`${allowlistPath}: ${rule} names a file that is not a Quint source under formal/models: ${path}`);
+  let checked = 0;
+  for (const path of files) {
+    const lines = read(path, directory).split('\n');
+    const long = lines.map((line, index) => line.length > caps.lineLength ? index + 1 : 0).filter(Boolean);
+    const header = headerLines(lines);
+    if (listed.lineLength.has(path)) { if (!long.length) failures.push(`${allowlistPath}: ${path} has no line over ${caps.lineLength}; delete its lineLength entry`); }
+    else { checked++; for (const line of long) failures.push(`${path}:${line}: line over ${caps.lineLength} characters`); }
+    if (listed.headerLength.has(path)) { if (header <= caps.headerLength) failures.push(`${allowlistPath}: ${path} has a header within ${caps.headerLength} lines; delete its headerLength entry`); }
+    else if (header > caps.headerLength) failures.push(`${path}: module header has ${header} comment lines (cap ${caps.headerLength})`);
+  }
+  if (failures.length) throw new Error(failures.join('\n'));
+  return { files: files.length, lineLengthChecked: checked, allowlisted: listed.lineLength.size + listed.headerLength.size };
+}
+
+if (process.argv[1] === fileURLToPath(import.meta.url)) {
+  const [flag] = process.argv.slice(2);
+  if (flag === '--report') process.stdout.write(renderReport(measure()));
+  else if (flag === undefined) console.log(checkStyle());
+  else { console.error('Usage: node formal/tools/check-style.mjs [--report]'); process.exitCode = 2; }
+}