refactor(formal): group the formal tree by role

[lan17]

Closes #221. Phase 1 of #220.

What this does

Groups formal/ by role so the top level is one README and six directories, each with an index. Nothing about the models, the driver contract, the catalogs' content or the checks changes; the Quint tree moves down one level as a unit, so no import changes.

formal/
  README.md      the task table, then a directory table
  guides/        the 14 reviewed guides (+ guides/README.md, grouped by the ledger's review kinds)
  models/        37 .qnt files, flat; kernel/ and fixtures/kernel/ beneath
  replay/        not moved
  tools/         44 .mjs and 5 .d.mts; the two one-line shell wrappers are deleted
  catalogs/      15 hand-maintained JSON files, including the two fixed vector corpora
  generated/     17 smoke traces, the fixtures lock and the 4 generated vector files

How to review it

The move is one script, formal/tools/migrate-layout.mjs, committed in the first commit (96eb885) and removed in the last. Review the mapping in that file rather than the 3,500 rewritten paths: it maps every formal/<name> string by kind (directory, smoke-trace and vector name shapes, then extension), so synthetic test paths follow the layout and the rewrite is idempotent. A dry run on the merged tree reports zero moves and 11 literal edits, all in scripts/check-docs.test.mjs, whose fixtures use pre-move paths on purpose (one of them is the deliberately broken formal/SPEC.md link that asserts a failure); the script is gone, so nothing acts on them.

Everything the script could not see is in the hand-edit commits, following the list in #221:

Commit	Content
96eb885	The move: 183 renames, 2 deletions, 217 Markdown links and about 3,500 literal paths rewritten; 15 kernel comments are the only Quint edits
a46911b	Tools: the scheduler's source predicate, scan directories and path-shape checks; fixture generator and guide scan; 20 repository-root computations; 13 replay/ imports; the witness-evidence producer; fixture-scope's lock path and catalog pattern; .gitattributes
bb34fa5	Docs: the directory table, six index READMEs, a permanent relative-link pass in scripts/check-docs.mjs, four pre-existing broken links in typescript/README.md, the snapshot-replay sentence in VALIDATION.md, AGENTS.md
271df31	Regenerated artifacts and refreshed ledgers (see below)
4c4b97d	Two corrections to the script's rules found during the series (sentence-final paths; the ports' own formal/ test modules) and the layout-legacy marker
87a01d5	Go, Rust and Python harnesses: assembled smoke, model and corpus paths; the three witness scanners mirror the producer; two Python runner tools' repository root
e1d7fbc	TypeScript tests: interpolated paths, escaped regex expectations, fake repository trees, synthetic manifest paths; the fixture-scope and docs tests
1caf7f2	Removes the migration script
6bea358	Review fixes: absolute GitHub links in the TypeScript README (npm resolves relative README links against the repository URL, and the package declares no directory), two corrected sentences in the tools index, the guide-scan sentence in TEST-AUDIT.md

Compatibility. The differential reads its reference revision through the layout that revision's own listing shows (layouts in execution.mjs): manifests, source discovery and kernel recognition together. That reader is transitional and goes once the merge base with main carries the new layout. Saved exploration runs from before the move are replayed from a checkout of their recorded base revision; VALIDATION.md says so.

Artifact and ledger changes

#221 step 1 had the refresh-commands PR from #220 landing first; it did not, so the ledgers were re-keyed with a session script built on the exported snapshot functions, and that PR (E1) becomes the first item of #220 Phase 2.

node formal/tools/generate-artifacts.mjs --write regenerated everything: the 17 smoke traces and 19 witness fixtures came back byte-identical to the path-rewritten files, so their histories and states are unchanged by construction; the four vector files change only in the generator's own source digest (one line each); the lock records the new input and artifact hashes. The source audit is re-keyed for the moved guides and gains the guides index; feature-coverage and go-parity pins follow the files the move touched.

Verification

• make audit lane: manifest, source audit, semantic coverage, feature coverage, go-parity: green. Fixture verify: 36 artifacts, 197 histories.
• Lint baseline --check: matches 17 profiles. Kernel fixtures: 16 fixtures, 194 runs pass.
• Go: go vet and go test ./... pass. Rust: cargo fmt --check, cargo clippy -D warnings and cargo test --all-features pass (1,738 conformance cases). Python: 2,229 passed, 342 skipped for the absent Redis.
• Docs sources and the new formal link pass: 27 pages, no broken links.
• Differential against pre-move main (d470b2f) through the layout-aware reader: all 16 composed profiles agree on every history in both directions, 5,985 reference histories forward and 5,985 candidate histories reverse (5,380 sampled plus 605 exported regressions each way), bytes per state x1.000 for every profile, generation wall within x0.97 to x1.02.
• TypeScript: typecheck, build and the packed-package check pass. The unit suite passes 3,506 tests; in a full make check-ts run on a saturated machine (load 26 to 34 alongside the differential) 20 tests hit their 5 s timeouts, all of them tests that spawn fake tool processes for the prerequisite probes or the receipt replays, and every one of those files passes when run on its own. The slowest of them, the Rust prerequisite probe, takes 6.0 s on pre-move main and 5.3 s on this branch on the same machine back to back, so the sensitivity is inherited, not introduced. Smoke: make smoke green in all four ports (1,821 TypeScript replay assertions, then Go, Rust and Python).
• Not run locally: the mutation lanes and the full formal workflow; both are unaffected by a path move beyond what the audit and smoke lanes check, and the full workflow should be dispatched on this branch with exploration enabled before merge, as Formal: group formal/ by role so the top level is one README (phase 1 of #220) #221 asks.

Not in this PR

Splitting models/ by kind or tools/ by verb (the indexes carry the grouping), permanent old-layout compatibility, and everything in #220 Phase 2 and 3. #219 is open and touches 54 files under formal/; the script can be re-run on that branch from the first commit (git show 96eb885:formal/tools/migrate-layout.mjs) with rows added for its new files.

🤖 Generated with Claude Code

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.73%. Comparing base (d470b2f) to head (6bea358).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #223   +/-   ##
=======================================
  Coverage   93.73%   93.73%           
=======================================
  Files          78       78           
  Lines       11357    11357           
  Branches      656      656           
=======================================
+ Hits        10645    10646    +1     
+ Misses        642      641    -1     
  Partials       70       70           

Flag	Coverage Δ
go	91.17% <ø> (+0.05%)	⬆️
python	92.08% <ø> (ø)
rust	94.29% <ø> (ø)
typescript	96.56% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[lan17]

Reviewed at 1caf7f2 against main d470b2f. The move is mechanically sound: I re-derived the #221 acceptance checks on the branch rather than reading the 3,500 rewritten paths, and they all hold. One gate still has to run and there are four small text fixes; nothing structural.

Before merge

1. Dispatch the full formal workflow on this branch with exploration enabled. No run exists for it yet. It is the only lane that exercises the witness-evidence producer (formal/replay/witnesses/evidence.mjs:22) against the three port scanners: without the full-replay environment those tests return before checking anything, so make check and make smoke cannot see a mismatch. I read all four and they agree on formal/models and formal/models/kernel, so I expect green, but this is the gate the PR body names.
2. typescript/README.md:141 may trade a GitHub break for an npm break. The four links went from go/README.md to ../go/README.md, which is right when GitHub renders the file in place. npmjs.com rewrites relative README links against the repository URL, and typescript/package.json declares no repository.directory, so ../go/README.md would resolve above the repository root while the old form resolved correctly there. Worth checking the rendered package page; absolute GitHub URLs work in both renderers, which is what the same table already does for the docs-site links.
3. Two sentences in formal/tools/README.md are wrong. "the audit lane runs the first five" of the Checks list: audit runs execution.mjs plus the first four, and check-model-properties.mjs is the formal-check lane's fault campaign. "writes generated output only under ../generated/": generated-fixtures.mjs also writes the witness fixtures under typescript/test/fixtures/, as generated/README.md itself says.
4. formal/guides/TEST-AUDIT.md:43 still describes the old layout. "every top-level formal/*.md guide" was a glob the script could not see; the scan is now formal/guides/*.md plus formal/README.md and go/README.md. It is a reviewed guide, so the edit carries a ledger re-key.

Two accuracy notes for the description: the dry run on the merged tree is not zero edits. It reports 11 literal edits, all in scripts/check-docs.test.mjs, whose fixtures use pre-move paths on purpose, including the deliberately broken formal/SPEC.md link that asserts a failure. Harmless since the script is gone, but say so. And #221 step 1 had the #220 refresh-commands PR landing first; the branch's check-source-audit.mjs has no refresh mode, so the ledgers were refreshed another way. Not a defect here, just a dangling step in both issues.

Verified

• Shape. ls formal is README.md and six directories; 37 models, 29 kernel modules, 16 fixtures, 49 tools, 15 catalogs, 22 generated files.
• Quint. Zero import lines changed. Comment-stripped text is byte-identical for all 82 .qnt files against main: 67 untouched, 15 comment-only, 0 with executable differences.
• Artifacts. The 17 traces and 19 witness fixtures are absent from the regeneration commit, so they came back identical to the rewritten files; the four vector files differ only in the generator's own source digest; the lock and three ledgers are the rest of 271df31.
• Residual sweep. After the allowlist (replay/, the formal README, the three nested formal test directories), the only formal/<name> hits are two deliberate test fixtures, and the bare "formal" segments are the make target and whole-directory references. Every prefix-less relative file reference under formal/ resolves to an existing file.
• Compatibility. layoutOfListing and layoutOfDirectory agree; copySources follows the layout through quintSources; a scratch tree with no manifests defaults to the current layout, which is what the candidate tree needs. The four differential shards ran this reader against pre-move main.
• Guards. fixture-scope.mjs and its tests pin the PR-lane row (a manifest-only change regenerates, a docs-only change does not). checkFormalLinks is permanent through docs:check under docs:build under make check; locally it reports 27 pages clean, the 12 node tests in scripts/check-docs.test.mjs and fixture-scope.test.mjs pass, and node formal/tools/execution.mjs validates the manifest.
• Indexes. Every file in every directory is named in its index (the .d.mts siblings by prose). The guides grouping matches the ledger's review.kind values exactly; the ledger has 17 entries including guides/README.md; the corpus schema versions are right; .gitattributes is one line; VALIDATION.md's snapshot sentence carries the dependency condition; the AGENTS.md tree is updated.
• Script. Directory rules first, then name shapes, then extensions, with an end lookahead that handles sentence-final paths and .jsonl. The one real hazard, the ports' own formal/ test modules, was caught in 4c4b97d, and the final tree has no mangled module paths.

Ran locally on a checkout of the branch: the migration script dry run, the formal link pass, the two node test files and the manifest validator. Did not run make check or the formal lanes; CI covers the PR lanes and item 1 covers the rest.

[lan17]

Thanks, all four points taken in 6bea358, and the gate is running.

1. Full formal workflow with exploration enabled: dispatched on 6bea358, run 37848048336. No earlier run existed for the branch.
2. typescript/README.md: the four repository links are absolute GitHub URLs now. You are right about npm: the package declares no repository.directory, so the parent-relative form resolved above the repository root there, and the old form was the one broken on GitHub. The same table already used absolute links for the docs site.
3. formal/tools/README.md: "runs execution.mjs and the first four", and generators write under generated/ and, for the witness fixtures, typescript/test/fixtures/.
4. formal/guides/TEST-AUDIT.md: the scan is described as formal/guides/*.md plus formal/README.md and go/README.md; its ledger entry is re-keyed.

Both accuracy notes are in the description now: the dry run on the merged tree reports 11 literal edits, all of them pre-move paths that scripts/check-docs.test.mjs uses on purpose (including the deliberately broken formal/SPEC.md link that asserts a failure), and the refresh-commands PR from #220 did not land first, so the ledgers were re-keyed with a session script on the exported snapshot functions. #220 is updated: that PR (E1) moves to the front of Phase 2.

The commit message of 1caf7f2 still says the dry run reported no edits; that was true at 4c4b97d, before the docs test gained its fixtures, and the PR description carries the correction.

— Claude