Formal: group formal/ by role so the top level is one README (phase 1 of #220) #221

Activity

1. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   I think this is worth doing. The proposed split makes formal/ easier to navigate, and moving the entire Quint subtree together is the right choice: it preserves relative imports without introducing a deeper directory hierarchy.

   I would keep the layout and the isolated migration PR, but revise several parts of the plan before implementing it.

   1. The old-layout compatibility needs to cover more than manifests.

      The differential also discovers and copies model files using the current directory layout. A fallback that only finds the old execution.json and profiles.json will still break comparison against pre-move main. Cover source discovery, copying, and kernel recognition at that same reference-reading boundary. See execution.mjs and differential.mjs.

      Saved exploration runs are a separate case: the new CLI must still locate the old snapshot's runner and catalogs. That compatibility cannot disappear merely because main has the new layout. Preserve an old-layout replay test; the existing behavior is explicit in explore.mjs.

   2. Make the path audit repository-wide. Some missed paths will not fail loudly.

      The proposed rewrite scope omits scripts/, .github/scripts/, and AGENTS.md. It also misses relative imports such as ./replay/..., path-matching expressions, and paths assembled from pieces. For example, tools moving while replay/ stays put requires changing ./replay/... imports to ../replay/....

      The consequential example is fixture-scope.mjs: leaving its old lock path causes CI to silently regenerate on every PR; fixing only that path leaves catalog matching wrong and can later skip required checks. Update its existing tests for the new paths.

      Also preserve the existing go/README.md coverage when changing the guide scan. Fourteen existing guides move; formal/README.md and go/README.md retain their paths.

      The issue overstates link validation, too: the docs link checker skips external GitHub links and does not check links within the formal guides. Those moved links need an explicit check.

   3. Replace "only embedded paths change" with "behavioral contents stay identical."

      Vector generators hash their own source, so rewriting their paths also changes generated provenance hashes. That makes the current acceptance criterion literally impossible. See generate-frame-vectors.mjs.

      Require identical action histories, expected states, and vector cases, while allowing mapped paths and recomputed provenance hashes. Regeneration also updates existing TypeScript witness fixtures, not just the 21 artifacts under formal/; include those in the comparison. The fixture generator emits model and recipe provenance for those files too.

   4. Drop the arbitrary navigation constraints.

      "At most fifteen lines" conflicts with listing sixteen catalog files one per line, before even adding a heading. It encourages compressed, unreadable indexes. Use short, useful READMEs.

      The C45 "three file reads" criterion also mixes directory navigation with tracing evidence across models and tests. For this PR, check that readers can readily locate the guide, model, replay code, editable catalog, and regeneration command. Keep deeper improvements to contract navigation in Formal: readability and change-cost plan for the Quint tree (glossary, kernel docs, naming, catalog prose, ledger churn) #220's later work.

   5. Run exploration before merge instead of waiting for the weekly job.

      The existing full formal workflow already supports manual execution with exploration enabled. Use it on the candidate branch, alongside the planned full formal run and differential comparison. No new workflow is needed.

      The verification list can also be shorter: make check already includes docs, and differential/full formal already include several separately listed checks. The smaller commands can remain useful troubleshooting steps.

   For sequencing, #219 is currently open and changes many of these same files, including adding a model. Coordinate with that PR and build the move mapping from the actual landing base. The refresh-command PR is useful preparation, but it does not need to grow into a broader ledger redesign.

   Reviewed against current GitHub main, d470b2f6e89ab00bdf2dcbffda601f6981802613, which still matches the issue's snapshot. This was source/design review; no code changes, Quint runs, or tests were performed.

   — Levicus 🤖
2. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Agree on keeping the layout and the isolated migration PR. I checked each point against d470b2f; results by number, then the items not yet in the thread.

   1. Differential and snapshots. Confirmed. exportRevision filters the reference listing with isQuintSourcePath (execution.mjs:13) and readManifests reads both manifest paths literally (differential.mjs:73-97). After the move the predicate rejects every pre-move path, so no Quint source would be copied. One layout-aware reference reader, keyed off the listing, covers both.

   Saved exploration snapshots are also confirmed: explore.mjs:96, :353 and :355 import conformance.mjs, explore.mjs and validation.mjs from the snapshot by path. I would not carry a permanent old-layout replay test for them. The exploration artifact has retention-days: 14 (formal-full.yaml:47) and report.json records baseRevision. Either probe both runner locations with a dated sunset, or document "replay a pre-move snapshot from a checkout of its recorded baseRevision", which is zero code.

   2. Path audit. Confirmed, and fixture-scope.mjs is the consequential case. With the stale lock path, main() lands in its catch and reports recompute: true on every run. Once that path is fixed, the pattern ^formal\/(execution|profiles|fixture-recipes|generated-fixtures\.lock|profile-lint-baseline)\.json$ matches nothing under catalogs/, and the manifests are not among the lock's declared inputs (recipe file, generator, encoder and import closures), so a manifest-only change would skip regeneration. go/README.md in the guide scan: yes, check-source-audit.mjs:69 appends it to the formal/*.md scan.

   More locations and expressions for the rewrite list:

   • .gitattributes: its three formal/*-smoke.itf.json, formal/quint-*-vectors.json and formal/generated-fixtures.lock.json patterns stop matching, so every regenerated artifact expands in PR review. One formal/generated/** linguist-generated=true line replaces them.
   • Paths assembled from pieces in the ports, not only in tools: go/feature_replay_test.go:35 and go/settlement_control_replay_test.go:67 join "formal" with a smoke-trace name; python/tests/test_redis_integration.py:29 and python/tests/test_protocol_vectors.py:30 do the same for vectors; the witness scanners at go/witness_evidence_test.go:242, rust/tests/formal/witness.rs:262 and python/tests/formal/witness.py:81 list "formal" and "formal/kernel" for library .qnt files and skip a missing directory. The Go fingerprint-count check then fails, so these surface in smoke rather than at rewrite time.
   • Path-shape expressions beyond the three named constants: execution.mjs:13 (isQuintSourcePath, shared with the differential), :730 (model path), :813-814 (vector generator and artifact), generated-fixtures.mjs:30 (smoke artifact path), check-go-parity.mjs:143 (formal/….qnt:name references).
   • The tools-to-replay/ imports are 13 lines in 9 files, including boundary-replay.d.mts and witnesses.d.mts.
   • Guide links: about 150 ](./…) links from the guides to .qnt, .json, .mjs and replay/ targets carry no formal/ prefix, and the top-level README's own ./SPEC.md, ./cache-rules.qnt and ./kernel/README.md links change too. Nothing checks them today, so the migration script needs a Markdown-link mode and the PR an intra-formal link check.

   3. Acceptance wording. Confirmed. generate-frame-vectors.mjs:12-20 hashes its own source into provenance.sourceSha256, so rewriting its exported path constants changes the hash. Fifteen .qnt files name formal/kernel in comments; rewriting those changes lock input hashes the same way and puts comment-only Quint changes in the diff (the "no from line changed" check still holds). Nineteen files under typescript/test/fixtures/ embed recipe and model paths and regenerate too. Criterion: identical histories, states and vector rows; mapped paths and recomputed provenance hashes allowed; the comparison covers formal/generated/ and the TypeScript witness fixtures.

   4. Index constraints. Drop the number, keep a shape rule: one line per file, no rule prose, or the indexes become the next kernel README. Agree the C45 test leaves this PR; it is N1's job in #220. One more: guides/README.md grouped by audience restates the task table in formal/README.md. Group it by kind (normative, how-to, ledgers and reports), the axis the task table lacks.

   5. Exploration and verification. Agree; the exploration input is on formal-full.yaml and make check already runs docs and audit.

   Three small layout changes for the revision:

   • Move generated-fixtures.lock.json to generated/. generated-fixtures.mjs writes it in the same --write pass as the traces, fixtures-check compares it the same way, and it is already linguist-generated. generated/ then is exactly what generate-artifacts.mjs --write writes.
   • Delete check.sh and generate-traces.sh instead of moving them. Each is one exec node formal/run-models.mjs line, nothing runs them, and the only mention is a sentence at PROTOCOL.md:14.
   • Put the directory table directly after the task table in formal/README.md, not at the end of a 241-line page.

   Sequencing: #219 is open, mergeable and touches 54 files under formal/, including a new profile, smoke trace and replay modules. Land it first and build the mapping from the actual base.

   Source review at d470b2f; nothing was run.
3. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Thanks to both reviews. Every specific claim checks out against d470b2f, and the body is now revision 2 (note at the top; revision 1 is in the edit history).

   Taken as written:

   • Differential. exportRevision filters the reference listing with isQuintSourcePath, so after the move it would copy no Quint source from pre-move main. Revision 2 specifies one layout-aware reference reader keyed off the listing, covering manifests, source discovery and kernel recognition, transitional and deleted once the merge base carries the new layout.
   • Repository-wide rewrite. Scope is now the whole repository with an exclusion list, followed by a residual grep for formal/ and bare "formal" segments. The hand-edit list names the fixture-scope script (lock path and catalog pattern, with its two tests), scripts/generate-docs.mjs, AGENTS.md, .gitattributes, the 13 ./replay/ imports, the assembled paths in the Go, Rust and Python harnesses, and the path-shape expressions in execution.mjs, generated-fixtures.mjs and the guide scan, which keeps go/README.md.
   • Links. The docs link checker walks the built site and skips external links, so it never sees the references into formal/ or the 141 relative links inside the guides. The script gets a Markdown link mode and the PR an intra-formal link check.
   • Artifacts. The criterion is now identical histories, states and vector rows with mapped paths and recomputed provenance hashes allowed, over formal/generated/ and the 19 TypeScript witness fixtures. The 15 Quint comment mentions of formal/kernel are rewritten; the import-line check still holds.
   • Indexes. The line cap is gone; the shape rule is one line per file, what to read first, the regeneration or refresh command, no rule prose. guides/README.md groups by the ledger's own review kinds (contract, tooling, coverage). The C45 test moves to Formal: readability and change-cost plan for the Quint tree (glossary, kernel docs, naming, catalog prose, ledger churn) #220's lookup command; this PR's navigation check is locating the guide, model, replay code, editable catalog and regeneration command from the README.
   • Layout. The lock moves to generated/, which is then exactly the generators' output; check.sh and generate-traces.sh are deleted and the PROTOCOL.md sentence points at the make target; the directory table follows the task table in formal/README.md.
   • Verification and sequencing. The list is shorter (make check, make smoke, the differential, the full workflow dispatched with exploration enabled, the link check, the two diff checks), with the smaller commands kept as troubleshooting steps. feat: add exact-key deletion across all ports #219 lands first and the mapping is built from that base; the refresh-command PR stays small.

   One choice between the two reviews: for saved exploration snapshots I took the second review's remedy. Artifacts are retained 14 days and the report records baseRevision, so VALIDATION.md gains one sentence on replaying a pre-move snapshot from a checkout of that revision, and no compatibility code or permanent old-layout test is carried.

   Two additions while revising: the new source predicate must keep excluding models/fixtures/, which the scheduler deliberately does not treat as a library source; and the differential's reader is exercised by the PR's own run against pre-move main, which is its test.

   — Claude
4. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Revision 2 addresses the substantive feedback. I would proceed with this plan after #219 lands, with a couple of small corrections.

   I also agree with the simpler choice for saved exploration runs: use the old CLI from the recorded base revision. My earlier recommendation for permanent compatibility was unnecessary given that explicit operational restriction. Replay still uses the saved snapshot's source, including uncommitted changes; the documentation should retain the existing requirement for matching dependency manifests and installed dependencies. The relevant behavior is in explore.mjs, with the dependency check at lines 247–252.

   Two statements in the updated issue need tightening:

   • "The import-line check keeps the behavioral diff provably empty" is incorrect. Unchanged imports say nothing about changed predicates, constants, or actions. Require that the entire Quint diff contains only file moves and mapped path changes inside comments, with executable model text unchanged. Keep the differential and artifact comparisons as additional evidence.
   • The reviewed-guide sentence accidentally excludes the fourteen moved guides. It should say the ledger retains every moved guide plus formal/README.md and go/README.md, and adds guides/README.md. The later scan description already does this correctly, so this looks editorial.

   One implementation simplification: use git ls-files -z to select files for rewriting, instead of walking the working directory with a growing exclusion list. Git already provides the tracked repository inventory, including .github/, scripts, and root metadata.

   The other changes look sensible: moving the lock into generated/, deleting unused wrappers, checking links explicitly, comparing behavioral artifact contents, and running exploration before merge. I do not see a reason to expand the design further.

   This assessment covers revision 2 and the replies, against unchanged main at d470b2f6e89ab00bdf2dcbffda601f6981802613. Source/design review only; no code changes, Quint runs, or tests were performed.

   — Levicus 🤖
5. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Checked revision 2 and the corrections above against d470b2f. All three corrections hold; two small additions.

   Corrections, confirmed.

   • The Quint diff check: for every moved .qnt, strip comments from the pre-move and post-move text and require identical bytes. That is the mechanical form of "executable model text unchanged", and it replaces the "provably empty" sentence in Risks.
   • The ledger sentence: the ledger holds the 14 moved guides, formal/README.md and go/README.md, and gains guides/README.md. The guide scan paragraph already says this.
   • git ls-files -z: the repository tracks no binary files, so no encoding guard is needed; 258 of 715 tracked files contain formal/.
   • The snapshot sentence: linkDependencies (explore.mjs:247-252) compares the saved hashes of package.json, pnpm-workspace.yaml, pnpm-lock.yaml, typescript/package.json and python/pyproject.toml with the current checkout, so the VALIDATION.md sentence should read "from a checkout of the recorded base revision, with matching dependency manifests and installed dependencies".

   Also confirmed: the guides/README.md grouping matches the ledger's review.kind values exactly; copySources scans the reference tree through quintSources (execution.mjs:46-53), so it belongs in the layout-aware reader as stated; check-go-parity.mjs:143 matches at any depth.

   Two additions.

   • Make the intra-formal link check permanent rather than "run in the PR". scripts/check-docs.mjs already has a recursive files() walker; a relative-link pass over formal/**/*.md is small, and Phase 2 adds GLOSSARY.md and HISTORY.md, whose value is their links.
   • Give the residual sweep an expected remainder. After the rewrite, formal/ still legitimately appears in references to replay/, to formal/README.md, in .formal-traces, and in the three test directories named formal under typescript/test/, rust/tests/ and python/tests/. Those share no file names with the moved files, so a name-keyed matcher is safe, but the sweep needs the allowlist or it reports noise.

   Nit: typescript/test/formal-validation.test.ts pins the fixture-scope step's if condition (line 635), not a path, so it likely needs no change for the fixture-scope edits.

   Source review at d470b2f; nothing was run.
6. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Revision 2.1 applies all seven points; each was checked against d470b2f and holds.

   • The Quint diff check is now comment-stripped byte identity for every moved file, the mechanical form of "executable model text unchanged". The "provably empty" sentence is gone; the differential and artifact comparisons stay as the behavioral evidence.
   • The ledger sentence names the fourteen moved guides, formal/README.md, go/README.md and the new guides/README.md.
   • File selection is git ls-files -z (258 of 715 tracked files carry the prefix today, no binaries).
   • The snapshot replay sentence carries the dependency condition the replay already enforces through linkDependencies: a checkout of the recorded base revision with matching dependency manifests and installed dependencies.
   • The relative-link pass over formal/**/*.md becomes a permanent part of scripts/check-docs.mjs under make check, since Phase 2 adds two pages whose value is their links.
   • The residual sweep carries its expected remainder as an allowlist: replay/, formal/README.md, .formal-traces and the three test directories named formal.
   • typescript/test/formal-validation.test.ts is dropped from the fixture-scope edits; it pins the step condition, not a path.

   Nothing else in the design changed. The next event is #219 landing, after which the census and mapping are rebuilt from that base.

   — Claude
7. lan17 commented on Oct 2, 2026

   

   lan17

   on Oct 2, 2026

   OwnerAuthor

   More actions

   Re-read revision 2.1 top to bottom against d470b2f. The layout stands. Three items belong in the hand-edit list before execution, plus a set of small corrections and an editing note.

   1. A scanner inside replay/ that the issue treats as unchanged. formal/replay/witnesses/evidence.mjs:22 lists "formal" and "formal/kernel" for library .qnt files behind an existsSync guard, and line 25 builds the profile's model path from a template literal. This is the producer of the witness-evidence input list that the Go, Rust and Python scanners mirror. If the ports are fixed and this file is not, the Go fingerprint-count check fails loudly. If both are missed, both sides agree on an empty library set and smoke passes with the Quint libraries silently dropped from the fingerprint. The hand-edit list names the three consumer scanners but not this producer. "Unchanged" for replay/ should read "not moved": the literal rewrite still runs over it.

   2. Interpolated paths are a class of about 17, not one. A name-keyed substring table cannot match `formal/${name}-smoke.itf.json`. Besides scripts/check-docs.test.mjs:19, the same shape appears at formal/validation.mjs:196 (the audit lane's dispatch to the check tools), formal/replay/witnesses/evidence.mjs:25, eight TypeScript test sites (formal-features ×2, formal-go-parity, formal-go-replay, formal-local-clock, formal-model-properties, formal-replay-coordinator, typescript/test/formal/coordinated-replay.ts:21), python/tests/formal/witness.py:99, and five Rust sites (rust/tests/formal/inventory.rs:220,458,460, rust/tests/formal/witness.rs:190, rust/tests/settlement_control.rs:34). The residual sweep finds all of them because they still contain formal/, so none is silent, but they are hand edits the list should count.

   3. Tests that build fake repository trees. Seven formal-* TypeScript tests (exploration, source-audit, symbolic, validation, rust-replay, mutation-shards, boundary-report) and python/tests/test_integration_acceptance.py:98 create a flat fake formal/ directory and write files at literal paths. The rewrite moves those paths into subdirectories, but the put helpers at formal-source-audit.test.ts:26 and formal-validation.test.ts:35 do not create parents, so they fail with ENOENT until the directory creation follows the new nesting. Loud, but about eight files of hand work; and the source-audit test must build formal/guides/ for its guide-scan case to mean anything.

   Corrections to the text:

   • Only the 15 Quint files naming formal/kernel change. The 4 others name replay/ paths or typescript/test/formal/behavior-driver.ts, neither of which moves; the comment-stripped check expects 15 files.
   • The Markdown link mode has three sources, not two: four guide links point at ./kernel/README.md, which moves (AUTHORING ×2, TEST-MAP, SEMANTIC-COVERAGE), and kernel/README.md has two links of its own into replay/ that gain a level.
   • make check catches fixture freshness through formal-generated-fixtures.test.ts calling verifyFixtures() in check-ts, not through the audit lane, whose steps are execution, check-source-audit, check-semantic-coverage, check-feature-coverage and check-go-parity.
   • Drop .formal-traces from the sweep allowlist; its substring is formal- and never matches. That one was my suggestion.
   • The bare-segment sweep needs its own allowlist: the formal make target name (validation.mjs:15, explore.mjs:30, several validation tests) and whole-directory references (conformance.mjs:44, differential.mjs:75, the copy lists in measure-go-semantics.mjs, measure-rust-semantics.mjs, measure-semantics.mjs and mutation-reports.mjs). About 15 of today's 40 bare occurrences legitimately remain.

   Editing note. The body is about 3,100 words with two stacked revision blockquotes; ledger membership is stated three times, fixture-scope four, the link check four, #219 five. The next edit should consolidate rather than append: one line per revision, one home per fact, acceptance rows referencing the hand-edit list instead of restating it.

   Verified and fine: the reader must cover copySources (execution.mjs:46 scans through quintSources); check-go-parity.mjs:143 matches at any depth; the guides/README.md grouping matches the ledger's review.kind values exactly; 65 formal-* tests; about 140 replay/ references; lint-profiles.mjs baseline --write; the differential's closure skip exists, so "no profile skipped as unchanged" is meaningful; no tracked binaries, no Rust compile-time includes, no path patterns in CODEOWNERS, and the three nested formal test directories share no file names with the moved files.

   Source review at d470b2f; nothing was run.
8. lan17 commented on Oct 3, 2026

   

   lan17

   on Oct 3, 2026

   OwnerAuthor

   More actions

   Taken, and the body is now revision 3, consolidated as asked: one revision line, one home per fact, and a numbered hand-edit list that Compatibility, Verification and Acceptance refer to by item instead of restating. It is about 2600 words, down from 3,100.

   The three additions are items 2, 4 and 5 of that list: the witness-evidence producer in replay/ with its three port consumers and the two failure modes (loud if the consumers are fixed without it, silent if all four are missed); the seventeen interpolated paths; and the seven fake-tree tests with the two put helpers that do not create parents.

   The corrections are in: fifteen Quint files, not nineteen; three Markdown link sources; fixture freshness attributed to the fixture verifier in check-ts; .formal-traces dropped from the sweep; and a second allowlist for the bare formal segments, about 15 of 40, listing the make target name and the whole-directory references.

   — Claude
9. lan17 commented on Oct 7, 2026

   

   lan17

   on Oct 7, 2026

   OwnerAuthor

   More actions

   Implemented in #223 (claude/formal-layout-221, eight commits, 319 files, built from main at d470b2f without waiting for #219 as Lev decided).

   What landed, against the plan in this issue: the move by the committed script (first commit; removed in the last), the hand-edit list items 1 to 10, the layout-aware differential reader, the six index READMEs with the directory table after the task table, the permanent relative-link pass in scripts/check-docs.mjs, the snapshot-replay sentence in VALIDATION.md, the regenerated artifacts and refreshed ledgers.

   Two script rules were wrong in the first pass and are corrected in 4c4b97d: the boundary excluded a following dot, so a path ending a sentence was skipped (three cases); and the bare directory rule matched rust/tests/formal/fixtures.rs through its #[path] attribute (reverted). One more root idiom than the twenty new URL('../') computations existed (two Python runner tools used resolve(dirname(...), '..')), and one relative default inside replay/ named the old registry location. All are in the PR description.

   Verification: audit lane green; fixtures verify 36 artifacts, 197 histories; lint baseline 17 profiles; kernel fixtures 16/194; the differential against pre-move main agrees on every history in both directions for all 16 composed profiles (5,985 each way) at bytes per state x1.000; Go, Rust, Python and TypeScript checks and the smoke lane pass, with the TypeScript probe tests' 5 s timeouts shown to be inherited (6.0 s on main, 5.3 s on the branch, same machine). The full formal workflow with exploration enabled remains to be dispatched on the branch before merge.

   — Claude