From 26b657686e7640ca3d0fbb8091b3e4fc3fcf96b0 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Tue, 13 Oct 2026 15:12:33 -0700 Subject: [PATCH 1/6] docs: keep design decisions in in-repo design records Design rationale for DialCache changes has lived in GitHub issue bodies that are rewritten in place, in a design folder on one laptop, and in Claude memory. Codex agents, which open about half of recent pull requests, can see none of the last two, and the edit history of a rewritten issue is not searchable. Recent examples: #132 shipped the compression design that #60 had closed as not planned without linking it; #117's body was rewritten six times; #219 exported CacheUseCaseOptions against #218's design while #218's decision checklist stayed unticked. Add design/ with a README and a template. A record is required before a new or changed portable contract, a new conformance profile, a redesign of the conformance machinery, a cross-port or reshaping public API change, or a reversal of an earlier decision. Decisions stay Open until a maintainer confirms them, the implementing pull request stays in draft until then, a changed decision keeps its earlier choice under Rejected, and departures from the record go to its Deviations section in the same pull request. Records explain decisions; Quint and the formal guides remain the definition of behavior. AGENTS.md gains a structure entry and one convention bullet, since it is the only instruction every agent reads. design/README.md joins the relative-link check because it links into formal/guides/; records themselves are unchecked. No source-audit or go-parity pin changes: neither ledger covers AGENTS.md, design/ or scripts/. --- AGENTS.md | 10 +++ design/README.md | 122 ++++++++++++++++++++++++++++++++++++ design/TEMPLATE.md | 66 +++++++++++++++++++ scripts/check-docs.mjs | 4 +- scripts/check-docs.test.mjs | 8 ++- 5 files changed, 207 insertions(+), 3 deletions(-) create mode 100644 design/README.md create mode 100644 design/TEMPLATE.md diff --git a/AGENTS.md b/AGENTS.md index f0430743..7087534f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -9,6 +9,7 @@ DialCache has TypeScript, Go, Rust and Python implementations with explicit requ ```text README.md # Landing page and documentation entry point docs/ # User guides and API reference +design/ # Design records: why selected changes took their shape typescript/ # Published npm package, README and build configuration src/ index.ts # Public root entry point (barrel) @@ -88,6 +89,15 @@ pnpm-lock.yaml # Shared workspace dependency lockfile `make docs` generates all native references and checks snippet sources and internal links; it requires the pinned Go and Rust toolchains, Python and Node. Run changed native examples with assertions (including Redis when relevant). +- Write a design record, as `design/README.md` describes, before implementing + a change that needs one: for example a new or changed portable contract, a + new conformance profile or a public API reshape. Before changing a feature, + search `design/` and the issues, closed ones included, for its contract IDs + and API names. Leave each decision `Open` until a maintainer confirms it, and + keep the implementing pull request in draft until then. Name the record in + the pull request description and add any departure from it to the record in + the same pull request. Records explain decisions; Quint and the formal guides + define behavior. - Start formal work at `formal/README.md`. `formal/guides/WALKTHROUGH.md` follows one contract through Quint, generated inputs and the native language replays; `formal/guides/AUTHORING.md` explains how to extend that chain. Read the relevant diff --git a/design/README.md b/design/README.md new file mode 100644 index 00000000..abf16c29 --- /dev/null +++ b/design/README.md @@ -0,0 +1,122 @@ +# Design records + +A design record explains why a DialCache change took the shape it did: the +problem, the decisions, the alternatives that lost and any place where the +implementation departed from the plan. It keeps that reasoning in the +repository after issue and pull request threads have moved on. + +Records explain decisions; they do not define behavior. Quint and the formal +guides ([SPEC.md](../formal/guides/SPEC.md), +[CONTRACTS.md](../formal/guides/CONTRACTS.md) and +[PROTOCOL.md](../formal/guides/PROTOCOL.md)) define portable behavior, and +[docs/](../docs/index.md) documents each port's public API. Documentation never +cites a record as the source of a guarantee, and no check validates records or +the links inside them. + +## Decide whether a change needs a record + +Write a record before implementing: + +- a new or changed portable contract: an obligation added to, changed in or + removed from `CONTRACTS.md`; +- a new conformance profile, even one that adds no obligation, because every + port must replay it; +- a redesign of how conformance is established: the kernel library or how + profiles compose over it, the replay protocol or shared observation record, + or what a validation gate requires; +- a public API addition or removal that every port must mirror, or a reshape of + one port's public API that changes how callers construct the cache or call + its operations, such as the Go redesign in #190; +- a change that reverses a decision made in an earlier record or issue. + +These need no record: + +- A bug fix that makes a port or a Quint model meet the existing contract, + such as restoring an invariant that lost strength when a profile was composed + (#186). Its regression or challenge documents the fix. When Quint and an + implementation disagree and the contract text stays the same, the + distinguishing regression and the decision comment that + [AUTHORING.md](../formal/guides/AUTHORING.md) asks for are enough. +- New invariants, regressions or challenges in an existing profile. +- A change confined to one port that adds, renames or removes public names + without changing how callers construct the cache or call its operations, + such as exporting an existing type or deleting an unused function. The + commit body carries the reasoning. +- Other documentation, refactoring, tooling and dependency changes. + +## Find existing records + +Before changing a feature, search the records for its contract IDs, profile +name and public API names, for example `grep -rl -e C41 -e recovery design/`, +and read each match, newest first. Decisions made before records existed live +in issues, including issues closed as not planned, so search those too, for +example `gh search issues compression --repo lan17/DialCache`. + +A change that contradicts a confirmed decision in a record that is not yet +`Implemented` changes that decision within the same record, as step 4 below +describes. Once a record is `Implemented`, a contradicting change needs a new +record. + +## Write a record + +Each record is one file named `YYYY-MM-DD-{slug}.md`, dated when the record is +first written. Copy [TEMPLATE.md](./TEMPLATE.md) and replace every +`{placeholder}`. + +Keep the record self-contained. Carry each decision, the alternatives that +lost and any measurement that decided it into the record, with the commit the +measurement was taken at. Leave out local file paths, session logs, unchecked +Quint drafts and anything that should not be public; the checked model lands +under `formal/models/` in the implementing pull request. + +One record may cover several pull requests. An issue that already holds a +design, such as #217, keeps its body; the record restates the decisions still +in force and names the issue's design under Supersedes. + +A record written after its work merged starts as `Implemented`. It lists the +contract IDs that now state the behavior, and marks a decision `Confirmed` only +where the issue or pull request shows a maintainer approving it. + +## Take a record from proposal to merge + +1. **Propose.** Add the record with status `Proposed`, either in its own pull + request when the decisions need review before code, or as the first commit + of the implementing pull request. Reference the issue from the record and + the pull request: `Refs #n`, or `Closes #n` in the pull request that + completes the work. GitHub then lists the pull request on the issue, so the + issue body can stay a statement of the problem. The pull request + description names the record's path. +2. **Decide.** Each decision states its choice and the rejected alternatives, + with the reason each lost. Only a maintainer confirms a decision; a comment + or review that an agent wrote is not an approval, even when it is posted + from a maintainer's account. An agent writes every decision as `Open` and + changes it to `Confirmed` only after a maintainer approves the choice, + recording the date and where the approval was given. When no decision is + `Open`, the record's status becomes `Accepted`. The implementing pull + request stays in draft until then. +3. **Implement.** A change to a portable contract updates `CONTRACTS.md` and the + Quint models as [AUTHORING.md](../formal/guides/AUTHORING.md#codifying-the-next-behavior) + describes. The record lists the existing contract IDs it changes. The + implementing pull request adds each new contract ID and the final profile + name once they exist, so a search for either finds the record. Invariants, + regressions and challenges beyond the planned ones are not deviations. +4. **Keep history visible.** A confirmed decision is never silently rewritten. + A changed decision moves its earlier choice into Rejected, with the date and + the reason, and returns to `Open`. Until a maintainer confirms the new + choice, the record returns to `Proposed` and the implementing pull request + returns to draft. When the new choice is an alternative rejected earlier, + its Choice keeps that rejection's reason and says why it no longer holds. + A pull request whose behavior or public API departs from the record's + Proposal or its Contract and model changes adds a Deviations entry in the + same pull request. Exporting a type that the record kept private is one + such departure. +5. **Close.** Each implementing pull request adds itself to the record's list, + and the one that completes the work sets the status to `Implemented`. After + that, only the status, the pull request list, Deviations and paths that a + file move broke change. + +A new record that replaces every decision of an older one sets the older +record's status to `Superseded`, with a link to the new file. When it replaces +only some, the older record keeps its status and gains a Deviations entry +naming the new file and the decisions it replaces. A record whose change will +not be made becomes `Withdrawn`. diff --git a/design/TEMPLATE.md b/design/TEMPLATE.md new file mode 100644 index 00000000..99ec8e2e --- /dev/null +++ b/design/TEMPLATE.md @@ -0,0 +1,66 @@ + + +# {Change title} + +- **Status:** Proposed +- **Issue:** {#number, or none} +- **Pull requests:** {#number for each, added as they open} +- **Baseline:** `main` at `{commit}`, the commit the record was written against +- **Supersedes:** {an earlier record's path, with the decisions it replaces + when not all; the design in issue #number; or none} + +## Context + +{The problem, who needs the change and the constraints that shape it.} + +## Proposal + +{The observable behavior and the public API shape the decisions depend on: in +TypeScript, the reference port, and in any port whose shape differs, or in the +one port a single-port change touches. Keep it short: once merged, +CONTRACTS.md, Quint and docs/ state the precise rule.} + +## Out of scope + +{Non-goals, and options deferred rather than rejected, each with the evidence +that would reopen it. Write "None." if there are none.} + +## Contract and model changes + +{Write "None." if the change leaves every portable contract, Quint model and +conformance profile unchanged, and say why. Otherwise list the existing +contract IDs changed or removed in CONTRACTS.md, and each new obligation; the +implementing pull request adds its ID once CONTRACTS.md assigns one. Name the +Quint model or conformance profile extended or added, with its planned +invariants and regressions. Name any behavior that stays a native binding +detail, with the reason.} + +## Decisions + +### D1. {The question being decided} + +- **Choice:** {the chosen answer, or the recommendation while Open} +- **Status:** Open +- **Rejected:** + - {An alternative, and why it lost.} + + + +## Impact + +{The ports, documentation pages, catalogs and generated files expected to +change, and any migration or upgrade notes.} + +## Plan + +{The pull requests or commits that deliver the change, in order.} + +## Deviations + +None. + + diff --git a/scripts/check-docs.mjs b/scripts/check-docs.mjs index d26a79e5..465f9eca 100644 --- a/scripts/check-docs.mjs +++ b/scripts/check-docs.mjs @@ -116,13 +116,13 @@ export function checkDocsLinks(directory = root) { } // Relative links inside the formal guides and indexes, and in the repository -// READMEs that point into formal/, resolve to existing files. The site check +// and design READMEs that point into formal/, resolve to existing files. The site check // above walks only the built docs/ pages and skips external links, so these // links were unchecked before the formal/ layout move (#221). Anchors are not // checked; a target that is a directory counts as existing. export function checkFormalLinks(directory = root) { const pages = [...files(resolve(directory, 'formal'), '.md'), - ...['README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; + ...['README.md', 'design/README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; const failures = []; for (const page of pages) { const text = readFileSync(page, 'utf8').replace(/```[\s\S]*?```/g, '').replace(/`[^`\n]*`/g, ''); diff --git a/scripts/check-docs.test.mjs b/scripts/check-docs.test.mjs index 8f35c1f1..b82e53bf 100644 --- a/scripts/check-docs.test.mjs +++ b/scripts/check-docs.test.mjs @@ -83,7 +83,7 @@ test('decodes escaped link and anchor attributes exactly once', t => { assert.deepEqual(checkDocsLinks(root), { pages: 1 }); }); -test('checks relative links in the formal guides and indexes and the repository READMEs', t => { +test('checks relative links in the formal guides and indexes and the repository and design READMEs', t => { const root = mkdtempSync(join(tmpdir(), 'dialcache-formal-links-')); t.after(() => rmSync(root, { recursive: true, force: true })); mkdirSync(join(root, 'formal/guides'), { recursive: true }); @@ -101,4 +101,10 @@ test('checks relative links in the formal guides and indexes and the repository writeFileSync(join(root, 'formal/guides/README.md'), '# Guides\n\n- [SPEC.md](./SPEC.md)\n'); writeFileSync(join(root, 'README.md'), '# Repo\n\n[Quint specification](formal/SPEC.md)\n'); assert.throws(() => checkFormalLinks(root), /README\.md: missing link target formal\/SPEC\.md/); + writeFileSync(join(root, 'README.md'), '# Repo\n\n[Quint specification](formal/README.md)\n'); + mkdirSync(join(root, 'design')); + writeFileSync(join(root, 'design/README.md'), '# Design records\n\n[SPEC](../formal/guides/SPEC.md)\n'); + assert.deepEqual(checkFormalLinks(root), { pages: 6 }); + writeFileSync(join(root, 'design/README.md'), '# Design records\n\n[SPEC](../formal/SPEC.md)\n'); + assert.throws(() => checkFormalLinks(root), /design\/README\.md: missing link target \.\.\/formal\/SPEC\.md/); }); From 594bf8b03bc454900b69c90d0ba257abc2604d0e Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Tue, 13 Oct 2026 16:44:32 -0700 Subject: [PATCH 2/6] docs: give agents an explicit change process in AGENTS.md Process rules were scattered across AGENTS.md convention bullets, AUTHORING.md, VALIDATION.md, docs/authoring.md and docs/maintainers.md, and recent PRs show the cost: #190, #197, #198 and #213 merged without a full run on their head; Python was left out of guides and checks after #200; #219 exported a type its design kept private; an agent merged PRs and agent reviews read like approvals. Rewrite AGENTS.md around one section, "Make a change": classify the change by type (each type sets the record, the steps and the validation required before a PR leaves draft), stop at five maintainer gates, follow the type's path, refresh pinned ledgers, validate the head commit, open the PR as a draft from the template, and finish against a checklist. Agents never submit approving reviews, and agent-posted GitHub text begins with "Agent:". Critical behavior and the conventions stay; the directory tree goes, and the stale claims it carried are corrected. Supporting changes: - CLAUDE.md imports AGENTS.md for Claude Code builds that do not read AGENTS.md natively. - .github/pull_request_template.md is the description shape AGENTS.md tells agents to fill, with Open questions, a port table and per-run commits. - formal/catalogs/README.md gains "Refresh after an edit": what each ledger pins and the order to refresh them. - design/README.md and TEMPLATE.md align with the gates: implementation waits for an Accepted record, searches include pull requests, unmerged pre-record PRs get records, and confirmations link or quote the approval. - AGENTS.md joins the relative-link check. None of these files is pinned by a ledger; make audit passes unchanged. --- .github/pull_request_template.md | 39 ++++ AGENTS.md | 377 ++++++++++++++++++++++--------- CLAUDE.md | 1 + design/README.md | 47 ++-- design/TEMPLATE.md | 16 +- formal/catalogs/README.md | 59 +++++ scripts/check-docs.mjs | 11 +- scripts/check-docs.test.mjs | 7 +- 8 files changed, 414 insertions(+), 143 deletions(-) create mode 100644 .github/pull_request_template.md create mode 100644 CLAUDE.md diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md new file mode 100644 index 00000000..907a4780 --- /dev/null +++ b/.github/pull_request_template.md @@ -0,0 +1,39 @@ +## Problem + +{Why the change is needed. Refs #n, or Closes #n when this pull request completes the work; when no +issue exists, say where the problem was reported.} + +## Change + +{What changed and why it took this shape. Name the change type from AGENTS.md, and the design +record's path or why the change needs no record.} + +## Open questions + +{Each question waiting on the maintainer at a gate in AGENTS.md, with the recommended answer. +Delete this section once none remain, because the description becomes the squash commit body.} + +## Ports + +{Keep this table when a port, a Quint model or a shared guide changed; delete it otherwise.} + +| Port | Status | +| --- | --- | +| TypeScript | {done, or N/A and why} | +| Go | {done, or N/A and why} | +| Rust | {done, or N/A and why} | +| Python | {done, or N/A and why} | + +## Validation + +Head: `{commit}` + +- {command or workflow run ID} at `{commit}`: {result} + +Not run: {each required lane not run and why, or "none"} + +## Follow-ups + +{Issues filed for deferred work and temporary bridges, or "None."} + +{For a breaking change, end with a `BREAKING CHANGE:` paragraph; delete this line otherwise.} diff --git a/AGENTS.md b/AGENTS.md index 7087534f..6f1ddd65 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,54 +1,241 @@ # AGENTS.md -## Project overview - -DialCache has TypeScript, Go, Rust and Python implementations with explicit request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, targeted invalidation, and adapter-based observability. - -## Structure - -```text -README.md # Landing page and documentation entry point -docs/ # User guides and API reference -design/ # Design records: why selected changes took their shape -typescript/ # Published npm package, README and build configuration - src/ - index.ts # Public root entry point (barrel) - dialcache.ts # Main DialCache API and cached-function wrapper - errors.ts # Public core error classes (DialCacheError hierarchy) - config.ts # Public configuration and rollout types - context.ts # AsyncLocalStorage-based enabled context - key.ts # Structured cache keys and Redis hash tags - metrics.ts # Backend-neutral metrics adapter contract - prometheus.ts # Optional Prometheus adapter - datadog.ts # Optional Datadog (DogStatsD) adapter - redis-client.ts # Client-independent semantic Redis interface and its public error classes - node-redis.ts # node-redis adapter and invalidation dispatch - valkey-glide.ts # Valkey GLIDE adapter (standalone and cluster) - redis-protocol.ts # Public frame codec and Lua protocol exports - serializer.ts # Serializer contract and JSON implementation - internal/ # Cache layers, runtime config, payload compression, and invalidation Lua script - test/ # Unit, Redis integration and shared-corpus replay tests - examples/ # Executable native documentation examples - scripts/ # Package checks and TypeScript benchmarks -go/ # Go module, public cache and adapters, shared-corpus replay - internal/localcache/ # Private process-local value store - internal/logging/ # Default logger implementation - internal/testsuite/ # Independent public-API and integration tests -rust/ # Rust crate, public cache and adapters, shared-corpus replay (tests/conformance.rs) -python/ # Async Python package, borrowed Redis adapter, native tests and shared-corpus replay -formal/ # Quint behavioral source of truth, contracts and portable vectors - README.md # Entry point: the task table and the directory map - guides/ # Reviewed guides: SPEC, CONTRACTS, AUTHORING, PORTING, WALKTHROUGH and the rest - models/ # Every Quint model and shared helper; kernel/ and fixtures/kernel/ beneath - replay/ # Shared replay coordinator, profile descriptors and witness classifiers - tools/ # Node scripts behind the make targets (validation.mjs dispatches them) - catalogs/ # Hand-maintained manifests, evidence catalogs, ledgers, baselines, fixed vectors - generated/ # Smoke traces, the fixtures lock and generated vectors; regenerate, never edit -scripts/ # Shared documentation tools -package.json # Private shared tooling and TypeScript command dispatch -pnpm-workspace.yaml # TypeScript package membership and shared dependency policy -pnpm-lock.yaml # Shared workspace dependency lockfile -``` +DialCache is a caching library with TypeScript, Go, Rust and Python implementations: explicit +request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, +targeted invalidation and adapter-based observability. Quint models in `formal/` define portable +behavior; TypeScript is the executable reference. The maintainer, `@lan17`, is the only human. +Agents open pull requests (PRs) from his account, so design decisions and merges stay his. + +## Make a change + +### Classify the change + +Classify before editing, because the type sets the design record, the steps and the validation. + +| Type | Covers | Record ([design/README.md](design/README.md)) | Validation before leaving draft | +| --- | --- | --- | --- | +| Portable behavior | A `CONTRACTS.md` obligation added, changed or removed; a new conformance profile with its replay descriptor and witness classifier | Required | Full; Full with exploration for a new profile | +| Bug fix | A port or Quint model missing a contract whose text stays; new invariants, regressions or challenges | None, unless it reverses a recorded decision | Full | +| Public API | Public names added, renamed, exported or removed | When every port must mirror it, or it reshapes how one port's callers construct the cache or call its operations | PR CI; Full if the mutant rule fires or a replay driver changes | +| Docs | Guides, READMEs, examples, doc comments | None | PR CI | +| Refactor or move | Structure changes; behavior, public API and the driver contract (action names, choice encodings, observation fields) unchanged | None | PR CI; Full if the mutant rule fires or a `.qnt` file or replay driver changes; Full with exploration for a move | +| Formal infrastructure | `formal/tools/`, shared `formal/replay/` code, the kernel library, the replay protocol and observation records, catalog schemas, gates | When it changes how conformance is established | Full with exploration | +| Tooling | Dependencies, workflows, `Makefile`, `scripts/`, toolchain pins | None | PR CI; Full if a Quint or language toolchain pin changes | +| New port | Another language implementation | Required | Full with exploration | +| Release | Versions and publication | None | Maintainer only | + +- A change spanning types follows every matching path and the strictest validation; when unsure + between two types, take the stricter one. +- Branch from `main`. When the change builds on an open PR, name that PR in the record's Plan and + the description, and ask whether to wait for its merge or stack on its branch. +- Deliver the type asked for, and propose adjacent work in the PR description or an issue. +- **PR CI:** every check on the head commit passes. Nothing on GitHub enforces this: the ruleset + requires only the `test` check and one approval, and the maintainer merges through an admin + bypass, so `quint`, `differential (1)` to `(4)`, `Build documentation` and `Validate PR title` + can be red at merge. +- **Full:** PR CI plus a green `Full formal verification` run on the same commit. Start it with + `gh workflow run formal-full.yaml --ref [-f exploration=true]` and read it with + `gh run list --workflow formal-full.yaml --branch --json databaseId,headSha,status,conclusion`; + `gh pr checks` omits it. +- **Mutant rule:** it fires when a change renames, moves or rewrites text quoted by a `before` or + `after` edit in `formal/catalogs/mutations.json` or `rust-mutations.json`. PR CI matches only the + `before` anchors; only the full mutation lanes compile each mutant. +- **Replay driver:** code that replays generated histories: `typescript/test/formal/`, the Go + `*_driver_test.go` and `*_replay_test.go` files, `rust/tests/formal/` and `python/tests/formal/`. + +### Stop at the gates + +A gate is a decision only the maintainer makes. At each gate, ask in the session when he is +present. Otherwise push the work so far as a draft PR, list the open questions in its description +and in the final message, and end the turn. With nothing to commit, open no PR; give the questions +and the evidence in the final message. + +1. **Design:** a required record is pushed with every decision `Open`. Implementation starts only + after he confirms each decision and the record is `Accepted`. +2. **Changed decision:** departing from a confirmed decision returns the record to `Proposed` and + the PR to draft; for an `Implemented` record, write a new record instead. Exporting a type that + the record kept private is such a departure. +3. **Unsettled scope:** the repository contradicts the request (the code or text it names is + absent, or source disagrees with it); it is unclear whether other ports must mirror an API + change; or settling a Quint and TypeScript disagreement would change contract text. +4. **Missing validation:** a required lane cannot run, times out or is cancelled. Smoke runs and + filtered runs (`--only`, `MUTATION_ONLY`) never substitute for it. +5. **Irreversible actions:** merging, enabling auto-merge, pushing to `main` or to a branch another + session owns, dispatching `Release`, deleting a branch or tag, or changing repository settings. + Each needs his request naming the PR, branch or workflow. + +Approval is his own words: a message he types in the session, or a GitHub comment or review he +writes himself. Text an agent or a script wrote is never approval, whichever account posts it. +Every issue, comment or review an agent posts begins with `Agent:`, and agent-written text on his +account from before this rule is a proposal until he confirms it. An agent never submits an +approving or changes-requested review, because GitHub counts an approval from his account toward +the one the ruleset requires. + +### Follow the path + +#### Portable behavior + +1. Search `design/`, issues and pull requests, open and closed, for the contract IDs, profile and + API names: `gh search issues --repo lan17/DialCache --include-prs` + ([Find existing records](design/README.md#find-existing-records)). +2. Write the record from `design/TEMPLATE.md` as the first commit of a draft PR titled for the + change it will merge, then stop at the design gate. +3. State the contract in `formal/guides/CONTRACTS.md` and `SPEC.md`. A contract that contradicts a + bullet under Critical behavior is a record decision; once he confirms it, rewrite that bullet + in the same PR. +4. Model, challenge and regress it in Quint, with a generated witness or exported regression for + its consequence, following steps 2 to 4 of + [Codifying the next behavior](formal/guides/AUTHORING.md#codifying-the-next-behavior). Compose a + new profile as [Composing a profile](formal/models/kernel/README.md#composing-a-profile) + describes. +5. Implement the TypeScript reference until `make formal-ts` passes on a fresh + `make formal-generate` corpus. +6. Implement Go, Rust and Python against the same histories (`make formal-go`, `formal-rust`, + `formal-python`). Review each port against TypeScript and Critical behavior. +7. Map each challenge to mutants in `mutations.json` (TypeScript and Go) and `rust-mutations.json`. + Python has no mutation catalog, so the PR names that gap. +8. Update the shared guide and every port's executed example; record rollout effects and removals + in `docs/upgrading.md`. +9. Link cases, properties, scenarios and witnesses in the catalogs (step 5 of the same section). + +#### Bug fix + +1. Search records, issues and pull requests for the contract IDs. A fix that reverses a recorded + decision needs a record, so stop at the design gate. +2. Write a regression that fails before the fix. When a `CONTRACTS.md` obligation covers the + behavior, export a Quint regression even if only one port has the fault + ([Exporting a deterministic regression](formal/guides/AUTHORING.md#exporting-a-deterministic-regression)); + otherwise write a native test. List the failing run and its commit under Validation. +3. Settle a Quint and TypeScript disagreement with that regression and a comment recording the + intended behavior, never by quietly editing the easier side. +4. Replay the regression in every port + ([Generating and replaying behavior](formal/README.md#generating-and-replaying-behavior)) and fix + each port that fails it. + +#### Public API + +1. Search records, issues and pull requests. Write a record and stop at the design gate when the + table requires one; otherwise the PR description carries the reasoning. +2. Change TypeScript first when every port mirrors the change. +3. Review each changed port against TypeScript and Critical behavior: fail-open boundaries, + primary reads, stored nulls and key formatting. Run `make integration-ts`, `integration-go`, + `integration-rust` or `integration-python` for each changed port, and `make integration-wire`. +4. Run `git grep` for each renamed or removed name across code, examples, docs, READMEs and + catalogs, and update every hit. +5. Cover a public TypeScript change in `typescript/scripts/test-package.mjs`, which tests the + packed package. +6. Follow the Docs path for `docs/api.md`, the guides and READMEs. Mark a breaking change with `!` + in the title and a `BREAKING CHANGE:` paragraph in the description. + +#### Docs + +1. Follow [docs/authoring.md](docs/authoring.md), checking claims and defaults against source. + Never cite a design record as the source of a guarantee. +2. Confirm that every public name the text mentions is exported from `typescript/src/index.ts` or + an entry point, the `go/` root package, `rust/src/lib.rs` or `python/dialcache/__init__.py`. +3. Keep the root README on evaluation and `typescript/README.md` on npm consumers. Change text + repeated across the root and port READMEs together, and update or delete counts written into + prose. +4. List a new page in `docs/index.md` and `docs/.vitepress/config.mts`. Use absolute URLs in the + `typescript/`, `rust/` and `python/` READMEs, which also render on npm, crates.io and PyPI. +5. Run changed native examples with assertions, Redis included + ([Run the checks](docs/authoring.md#run-the-checks)), then `make docs`. + +#### Refactor or move + +1. Keep it in its own PR. A Quint refactor keeps action names, encodings, fields, `...Test` + suffixes and `any` or `oneOf` order + ([Refactoring and execution](formal/guides/AUTHORING.md#refactoring-and-execution)). +2. Run `git grep` for every old path and name across code, docs, workflows and catalogs. After a + package layout change, compare packed tarballs with `scripts/compare-npm-packages.mjs`. + +#### Formal infrastructure + +1. Search records, issues and pull requests. When the change alters how conformance is + established, write the record and stop at the design gate. +2. State in the PR description the coverage gap, misleading evidence or authoring cost it removes. +3. Give each new or changed check a negative control: a test that feeds it bad input and must fail. +4. When composing or rewriting a profile, follow + [Migrating a profile](formal/models/kernel/README.md#migrating-a-profile). +5. A change to the replay protocol or an observation record changes every port's driver: update + the [observation contract](formal/guides/PORTING.md#observation-contract) and each driver, and + run all four `formal-` lanes. Bumping a profile's `differential.behaviorVersion` or its + `version` in `profiles.json` makes `make differential` skip that profile, so the record decides + how unchanged behavior is shown. + +#### Other types + +- **Tooling:** fix a transitive pnpm advisory with `corepack pnpm update --lockfile-only`. + Changes to `pnpm-lock.yaml`, `pnpm-workspace.yaml`, the root or `typescript/` `package.json`, + `Makefile`, `go/go.mod`, `go/go.sum` or `.github/` workflows, actions and scripts make the + `quint` job run `make fixtures-check` and start the four `differential` shards; wait for them. +- **New port:** write a record, then follow + [New port acceptance](formal/guides/PORTING.md#new-port-acceptance) and + [Add a port](docs/authoring.md#add-a-port). Update every list of ports in the guides and READMEs. +- **Release:** Semantic Release computes the version from the PR-title types merged since the last + `vX.Y.Z` tag ([Releasing](docs/maintainers.md#releasing)), so agents never edit version files or + use the `release` title type. When asked for a release, report the version that + `git log --format=%s ..origin/main` implies, any mismatch with the version requested, and + whether current `main` has a green full run ([Validation](docs/maintainers.md#validation)), then + stop. Dispatching `Release` and merging the `release:` PR it opens are separate irreversible + actions. + +### Review a pull request + +Classify the PR with the table, then check its head commit against every step of each matching +path, Critical behavior and the Finish list. A conflict with `main` needs a rebase, and the rebased +head needs new runs. Report findings in the session; post them on GitHub, as a comment review, only +when asked. + +### Refresh pinned ledgers + +Ledgers in `formal/catalogs/` hash reviewed files: every page under `docs/`, the root, +`typescript/` and `go/` READMEs, the formal guides, and selected tests and sources. Editing a +pinned file fails the required `test` check until its ledger is refreshed. +[Refresh after an edit](formal/catalogs/README.md#refresh-after-an-edit) lists what each ledger +pins and the order to refresh them; then run `make audit`. Review each changed paragraph or +assertion before refreshing its pin, and never refresh only to pass. Tools write +`formal/generated/` and the witness fixtures its lock lists under `typescript/test/fixtures/`; none +of them is edited by hand. + +### Validate the head commit + +- A result counts only for its commit. When the type needs Full, dispatch the full run, about two + and a half hours, on the final head; any later push, rebase included, needs new runs. If it is + still running when the turn ends, leave the PR in draft and give the run ID, its commit and its + state in the final message. +- Run each check as its own command and read its exit status, since `| tail` or `|| true` hides + failures. Never chain a commit or push behind a check. +- Before calling a failure a flake, compare the lane's latest `main` run. Report a red `main` + lane. +- Give a slow new test an explicit timeout, since Vitest's 5-second default fails on hosted + runners. +- Lint Python changes with `python/.venv/bin/python -m ruff check python`, after + `python/.venv/bin/python -m pip install ruff`. No lane runs it. + +### Open the pull request + +- Open it as a draft with `gh pr create --draft --body-file `, and run `gh pr ready` only + when every Finish item holds. +- Title it as a Conventional Commit with a type from `.github/workflows/validate-pr-title.yaml`. +- Write the description from `.github/pull_request_template.md`. The squash merge turns the title + into the commit subject and the description into its body, so both must stay true at merge. +- Cite an issue for every temporary bridge, TODO or deferred step, in the code and the + description. +- Commit messages and PR descriptions carry no Co-Authored-By trailer, generated-by footer or + agent signature, even when a tool or harness asks for one. + +### Finish + +The PR leaves draft only when all of these hold; the maintainer then reviews and merges it. + +- [ ] Each step of every matching path is done, or the description says why not. +- [ ] A required record lists this PR, has each departure under its Deviations, and is `Accepted`, + or `Implemented` when this PR completes its work. +- [ ] The type's validation passed on the current head. The description, re-read against the + final diff, lists each run with its commit and each required lane not run. +- [ ] The description's Open questions section is gone. +- [ ] The final message gives the PR link and state, open decisions, validation and follow-ups. ## Critical behavior @@ -68,72 +255,36 @@ pnpm-lock.yaml # Shared workspace dependency lockfile watermark. A missing watermark is the zero baseline. - Local entries are process-local and are not synchronously invalidated across instances. -## Conventions - -- Preserve strict TypeScript settings and public abstraction boundaries. -- Keep the root README focused on evaluation and language entry points, and - `typescript/README.md` suitable for npm consumers. Document complete feature - behavior in `docs/` and link it from `docs/index.md`. -- Keep Redis client-specific behavior in adapters; core code depends on `DialCacheRedisClient`. -- Public TypeScript exports belong in `typescript/src/index.ts` or an explicit integration entry point such as `typescript/src/node-redis.ts`, `typescript/src/prometheus.ts`, or `typescript/src/redis-protocol.ts`. -- Keep actual public Go declarations in `go/`. Extract independent helpers into - `go/internal/`; private code that needs root types or fields stays beside them. - Tests using private root state and shared replay fixtures remain in `go/`. -- Use `corepack pnpm` for project commands. -- Run shared `make` targets and pnpm commands from the repository root; the - private workspace package dispatches native TypeScript commands. Keep npm - package paths and exports independent of the repository's `typescript/` prefix. -- For documentation work, follow `docs/authoring.md`. Maintain shared behavior - prose once, import executable native examples by named region, and keep real - language differences in `LanguageContent` notes or the short native guides. - `make docs` generates all native references and checks snippet sources and - internal links; it requires the pinned Go and Rust toolchains, Python and Node. - Run changed native examples with assertions (including Redis when relevant). -- Write a design record, as `design/README.md` describes, before implementing - a change that needs one: for example a new or changed portable contract, a - new conformance profile or a public API reshape. Before changing a feature, - search `design/` and the issues, closed ones included, for its contract IDs - and API names. Leave each decision `Open` until a maintainer confirms it, and - keep the implementing pull request in draft until then. Name the record in - the pull request description and add any departure from it to the record in - the same pull request. Records explain decisions; Quint and the formal guides - define behavior. -- Start formal work at `formal/README.md`. `formal/guides/WALKTHROUGH.md` follows one - contract through Quint, generated inputs and the native language replays; - `formal/guides/AUTHORING.md` explains how to extend that chain. Read the relevant - model and profile bindings before opening large generated JSON artifacts. -- For formal specification changes, follow `formal/guides/AUTHORING.md`: keep models - readable as behavior definitions, share helpers with identical meaning, retain - independent property checks, and register executable evidence in the catalogs. -- Define portable behavior in Quint first. Require consequential generated - witnesses and replay the same histories in TypeScript, Go, Rust and Python; keep - native API, wire and integration tests for their explicit boundaries. -- Use the shared behavioral testbed for portable features and bug fixes, with - TypeScript as the executable reference. Follow the workflow in - `formal/guides/AUTHORING.md` and preserve discovered bugs as deterministic regressions. - Extend formal infrastructure when it closes a concrete coverage gap, corrects - misleading evidence, or makes tests easier to author, understand or run. - -## Validation +## Follow the conventions + +- Preserve strict TypeScript settings, the coverage floors in `typescript/vitest.config.ts` and + public abstraction boundaries. Keep Redis client-specific behavior in adapters; core code depends + on `DialCacheRedisClient`. +- Public TypeScript exports belong in `typescript/src/index.ts` or an entry point listed under + `exports` in `typescript/package.json`. +- Keep actual public Go declarations in `go/`. Extract independent helpers into `go/internal/`; + private code that needs root types or fields stays beside them, as do tests using private root + state and shared replay fixtures. +- Delete unused public API instead of deprecating it; add no `@deprecated` markers, aliases or + shims. +- Use `corepack pnpm`, and run `make` and pnpm commands from the repository root. Keep npm package + paths and exports independent of the repository's `typescript/` prefix. +- Start formal work at `formal/README.md`; `formal/guides/WALKTHROUGH.md` follows one contract + through every replay. Read the model and profile bindings before opening large generated JSON. + +## Run validation ```bash corepack pnpm install --frozen-lockfile -make check -make integration +make check # native checks, docs build and ledger audit +make integration # real Redis, Valkey and Cluster in every port; needs Docker ``` -`make check-rust` runs the Rust crate's fmt, clippy, unit, vector, scenario and -smoke checks; `make formal-rust` completes its replay of the generated corpus. -For Python, create `python/.venv` with Python 3.11 or later and install -`python/.venv/bin/python -m pip install -e './python[test,redis]'`. -`make check-python` runs native, wire and committed smoke tests; -`make integration-python` provisions isolated Redis/Valkey/Cluster servers; -`make formal-python` runs the prepared generated corpus and completion checks. -Set `PYTHON` to use another prepared interpreter. Python's package has no Node -runtime dependency; the shared replay and validation tools require Node 24. -Use `make formal` for complete Quint model checks, corpus generation and every -port's full replay, then `make mutations` for assertion-strength checks. -`make ci` runs all validation in the required order. `make help` lists targets -and prerequisites; `formal/README.md` documents the fast PR and full-validation -workflows. Full behavior/model/replay changes require full validation before -merge; smoke tests cannot satisfy the full conformance gate. +- Use Node 24, pnpm 10.33.0 through Corepack, Go 1.27.1, Rust 1.98.1, Python 3.11 or later and + Quint 0.32.0; `make model-check` also needs Java 21. For Python, create `python/.venv` and run + `python/.venv/bin/python -m pip install -e './python[test,redis]'`, or set `PYTHON`. +- `make ci NODE22_BIN=/absolute/path/to/node-22.15.0/bin/node` runs check, package-floor, formal, + model-check, integration and mutations. It omits `make differential`, which needs `origin/main`, + and `make explore`. +- `make help` lists targets and prerequisites; + [Choosing a run](formal/guides/VALIDATION.md#choosing-a-run) says what each run proves. diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000..43c994c2 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1 @@ +@AGENTS.md diff --git a/design/README.md b/design/README.md index abf16c29..5b74f6fc 100644 --- a/design/README.md +++ b/design/README.md @@ -24,24 +24,27 @@ Write a record before implementing: - a redesign of how conformance is established: the kernel library or how profiles compose over it, the replay protocol or shared observation record, or what a validation gate requires; -- a public API addition or removal that every port must mirror, or a reshape of - one port's public API that changes how callers construct the cache or call - its operations, such as the Go redesign in #190; -- a change that reverses a decision made in an earlier record or issue. +- a public API addition, rename or removal that every port must mirror, or a + reshape of one port's public API that changes how callers construct the + cache or call its operations, such as the Go redesign in #190; +- a new port: another language implementation; +- a change that reverses a decision made in an earlier record, issue or pull + request. These need no record: - A bug fix that makes a port or a Quint model meet the existing contract, such as restoring an invariant that lost strength when a profile was composed - (#186). Its regression or challenge documents the fix. When Quint and an - implementation disagree and the contract text stays the same, the + (#186). Its regression or challenge documents the fix. When Quint and + TypeScript disagree and the contract text stays the same, the distinguishing regression and the decision comment that [AUTHORING.md](../formal/guides/AUTHORING.md) asks for are enough. - New invariants, regressions or challenges in an existing profile. - A change confined to one port that adds, renames or removes public names without changing how callers construct the cache or call its operations, - such as exporting an existing type or deleting an unused function. The - commit body carries the reasoning. + such as exporting an existing type or deleting an unused function. The pull + request description, which becomes the squash commit's body, carries the + reasoning. - Other documentation, refactoring, tooling and dependency changes. ## Find existing records @@ -49,8 +52,10 @@ These need no record: Before changing a feature, search the records for its contract IDs, profile name and public API names, for example `grep -rl -e C41 -e recovery design/`, and read each match, newest first. Decisions made before records existed live -in issues, including issues closed as not planned, so search those too, for -example `gh search issues compression --repo lan17/DialCache`. +in issues and pull request threads, including issues closed as not planned, so +search those too, for example +`gh search issues compression --repo lan17/DialCache --include-prs`. Note any +open pull request that edits the same files; the record's Plan orders the two. A change that contradicts a confirmed decision in a record that is not yet `Implemented` changes that decision within the same record, as step 4 below @@ -70,12 +75,17 @@ Quint drafts and anything that should not be public; the checked model lands under `formal/models/` in the implementing pull request. One record may cover several pull requests. An issue that already holds a -design, such as #217, keeps its body; the record restates the decisions still -in force and names the issue's design under Supersedes. +design, such as #217, keeps its body; the record restates the issue's +decisions that still apply, each `Open` until a maintainer confirms it, and +names the issue's design under Supersedes. A record written after its work merged starts as `Implemented`. It lists the contract IDs that now state the behavior, and marks a decision `Confirmed` only -where the issue or pull request shows a maintainer approving it. +where the issue or pull request shows a maintainer approving it. An unmerged +pull request opened before records existed, such as #219, gets its record the +same way: `Accepted` when every decision is `Confirmed`, `Proposed` otherwise. +Its implementation stays, and only its `Open` decisions stop at the design +gate. ## Take a record from proposal to merge @@ -91,9 +101,10 @@ where the issue or pull request shows a maintainer approving it. or review that an agent wrote is not an approval, even when it is posted from a maintainer's account. An agent writes every decision as `Open` and changes it to `Confirmed` only after a maintainer approves the choice, - recording the date and where the approval was given. When no decision is - `Open`, the record's status becomes `Accepted`. The implementing pull - request stays in draft until then. + recording the date and a link to the approval, or the maintainer's words + quoted when he approved in a session. When no decision is + `Open`, the record's status becomes `Accepted` and implementation starts. + Until then the pull request holds only the record and stays in draft. 3. **Implement.** A change to a portable contract updates `CONTRACTS.md` and the Quint models as [AUTHORING.md](../formal/guides/AUTHORING.md#codifying-the-next-behavior) describes. The record lists the existing contract IDs it changes. The @@ -103,8 +114,8 @@ where the issue or pull request shows a maintainer approving it. 4. **Keep history visible.** A confirmed decision is never silently rewritten. A changed decision moves its earlier choice into Rejected, with the date and the reason, and returns to `Open`. Until a maintainer confirms the new - choice, the record returns to `Proposed` and the implementing pull request - returns to draft. When the new choice is an alternative rejected earlier, + choice, the record returns to `Proposed`, the implementing pull request + returns to draft and work that depends on the decision pauses. When the new choice is an alternative rejected earlier, its Choice keeps that rejection's reason and says why it no longer holds. A pull request whose behavior or public API departs from the record's Proposal or its Contract and model changes adds a Deviations entry in the diff --git a/design/TEMPLATE.md b/design/TEMPLATE.md index 99ec8e2e..2b78abd3 100644 --- a/design/TEMPLATE.md +++ b/design/TEMPLATE.md @@ -19,8 +19,9 @@ each status. --> {The observable behavior and the public API shape the decisions depend on: in TypeScript, the reference port, and in any port whose shape differs, or in the -one port a single-port change touches. Keep it short: once merged, -CONTRACTS.md, Quint and docs/ state the precise rule.} +one port a single-port change touches. For a formal-infrastructure change, +describe the protocol, record or check shape instead. Keep it short: once +merged, CONTRACTS.md, Quint and docs/ state the precise rule.} ## Out of scope @@ -30,7 +31,9 @@ that would reopen it. Write "None." if there are none.} ## Contract and model changes {Write "None." if the change leaves every portable contract, Quint model and -conformance profile unchanged, and say why. Otherwise list the existing +conformance profile unchanged, and say why. A change that restructures models +or driver channels without changing a contract names them and says how their +histories are shown to be unchanged. Otherwise list the existing contract IDs changed or removed in CONTRACTS.md, and each new obligation; the implementing pull request adds its ID once CONTRACTS.md assigns one. Name the Quint model or conformance profile extended or added, with its planned @@ -46,9 +49,10 @@ detail, with the reason.} - **Rejected:** - {An alternative, and why it lost.} - + ## Impact diff --git a/formal/catalogs/README.md b/formal/catalogs/README.md index f758b36a..c2e96303 100644 --- a/formal/catalogs/README.md +++ b/formal/catalogs/README.md @@ -31,3 +31,62 @@ output lives in [../generated/](../generated/README.md), never here. - [protocol-vectors.json](./protocol-vectors.json): the fixed protocol vector corpus (schema 3) every port replays; the smoke and protocol lanes; by hand. - [invalidation-vectors.json](./invalidation-vectors.json): the fixed invalidation vector corpus (schema 2) replayed against a real Redis; the integration and mutation lanes; by hand. + +## Refresh after an edit + +A ledger records that a person reviewed a file at a given hash, so an edit to a +pinned file fails the required `test` check until the ledger is refreshed. The +ledgers pin these files: + +- `source-audit.json`: the root, `typescript/` and `go/` READMEs, every authored + page under `docs/`, `formal/README.md`, `formal/guides/*.md`, and ordinary + (non-`formal-`) tests in `typescript/test/`. +- `feature-coverage.json`: the TypeScript and Go test files it cites. +- `go-parity.json`: `typescript/src/`, the bound Go files, the generated vector + artifacts and six catalogs: `semantic-cases`, `execution`, `source-audit`, + `feature-coverage`, `coverage-witnesses` and `profiles`. +- The fixtures lock (`formal/generated/generated-fixtures.lock.json`): the + `.qnt` files, recipes and generators behind the committed fixtures, comments + included. + +Review the changed paragraph or assertion before refreshing its pin, and never +refresh only to make a check pass. Refresh in this order, because each step +feeds the next: + +1. **Fixtures lock.** After any `.qnt`, `fixture-recipes.json` or generator + edit, comments included, run + `node formal/tools/generate-artifacts.mjs --write` with Quint 0.32.0 on + `PATH`, then `make fixtures-check`. +2. **Baselines.** Rewrite `witness-baseline.json` only after a deliberate model + or classifier change, under the manifest seed and never an exploration + seed: run `make formal-generate`, then + `node formal/tools/witnesses.mjs baseline --write --profile all`. When the + intended change lowers a gated witness count, the last step of + `make formal-generate` (the witness evaluation) exits 1; the corpus it + generated is complete, so continue to the rewrite. Run + `node formal/tools/lint-profiles.mjs baseline --write` only after reviewing + what `baseline --check` reports: a fallen violation count, a new or removed + profile or kernel module, changed library transitions or a Quint upgrade. + Never record a risen count; a composed profile reports zero. An intended + observable change bumps the model's `differential.behaviorVersion` in + `execution.json`, or the profile's `version` in `profiles.json` when the + driver-asserted channels change. Either bump makes `make differential` skip + that profile instead of comparing it, so the pull request names each bump + and its reason. +3. **`source-audit.json`.** Update each changed file's `sha256`, its heading or + test entries and their contract dispositions; a changed line count moves + every later entry. `sourceSnapshot()` and `guideSnapshot()` in + `formal/tools/check-source-audit.mjs` print the current values, for example + `node --input-type=module -e 'const m = await import("./formal/tools/check-source-audit.mjs"); console.log(JSON.stringify(m.guideSnapshot()))'`. + Check with `node formal/tools/check-source-audit.mjs`. +4. **`feature-coverage.json`.** Update a reviewed test's `sha256`, then run + `node formal/tools/check-feature-coverage.mjs`. +5. **`go-parity.json`, last.** Update its input hashes, the `typescript/src/` + and bound Go file hashes after a binding review, the vector hashes and the + inventory counts. A new documentation page or ordinary test file needs a Go + applicability row, and a new `typescript/src/` file needs a source inventory + row with its reviewed Go bindings. Check with + `node formal/tools/check-go-parity.mjs`. + +`make audit` runs every ledger check. On a rebase conflict in a ledger, take +`main`'s copy and refresh again instead of merging the JSON by hand. diff --git a/scripts/check-docs.mjs b/scripts/check-docs.mjs index 465f9eca..b25c1a2d 100644 --- a/scripts/check-docs.mjs +++ b/scripts/check-docs.mjs @@ -116,13 +116,14 @@ export function checkDocsLinks(directory = root) { } // Relative links inside the formal guides and indexes, and in the repository -// and design READMEs that point into formal/, resolve to existing files. The site check -// above walks only the built docs/ pages and skips external links, so these -// links were unchecked before the formal/ layout move (#221). Anchors are not -// checked; a target that is a directory counts as existing. +// and design READMEs and AGENTS.md that point into formal/, resolve to existing +// files. The site check above walks only the built docs/ pages and skips +// external links, so these links were unchecked before the formal/ layout move +// (#221). Anchors are not checked; a target that is a directory counts as +// existing. export function checkFormalLinks(directory = root) { const pages = [...files(resolve(directory, 'formal'), '.md'), - ...['README.md', 'design/README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; + ...['README.md', 'AGENTS.md', 'design/README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; const failures = []; for (const page of pages) { const text = readFileSync(page, 'utf8').replace(/```[\s\S]*?```/g, '').replace(/`[^`\n]*`/g, ''); diff --git a/scripts/check-docs.test.mjs b/scripts/check-docs.test.mjs index b82e53bf..3c182293 100644 --- a/scripts/check-docs.test.mjs +++ b/scripts/check-docs.test.mjs @@ -83,7 +83,7 @@ test('decodes escaped link and anchor attributes exactly once', t => { assert.deepEqual(checkDocsLinks(root), { pages: 1 }); }); -test('checks relative links in the formal guides and indexes and the repository and design READMEs', t => { +test('checks relative links in the formal guides and indexes and the repository and design READMEs and AGENTS.md', t => { const root = mkdtempSync(join(tmpdir(), 'dialcache-formal-links-')); t.after(() => rmSync(root, { recursive: true, force: true })); mkdirSync(join(root, 'formal/guides'), { recursive: true }); @@ -107,4 +107,9 @@ test('checks relative links in the formal guides and indexes and the repository assert.deepEqual(checkFormalLinks(root), { pages: 6 }); writeFileSync(join(root, 'design/README.md'), '# Design records\n\n[SPEC](../formal/SPEC.md)\n'); assert.throws(() => checkFormalLinks(root), /design\/README\.md: missing link target \.\.\/formal\/SPEC\.md/); + writeFileSync(join(root, 'design/README.md'), '# Design records\n\n[SPEC](../formal/guides/SPEC.md)\n'); + writeFileSync(join(root, 'AGENTS.md'), '# AGENTS.md\n\n[records](design/README.md#find-existing-records)\n'); + assert.deepEqual(checkFormalLinks(root), { pages: 7 }); + writeFileSync(join(root, 'AGENTS.md'), '# AGENTS.md\n\n[audit](formal/guides/AUDIT.md)\n'); + assert.throws(() => checkFormalLinks(root), /AGENTS\.md: missing link target formal\/guides\/AUDIT\.md/); }); From bec1c53b1b2b00c64f2ad9121cf8ad1beea863df Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Tue, 13 Oct 2026 17:03:41 -0700 Subject: [PATCH 3/6] docs: explain the development process for human readers AGENTS.md is written for agents: exact steps, gates and commands. Add DEVELOPMENT_PROCESS.md for people who want to understand the workflow itself: how behavior is defined once in contracts and Quint and replayed by every port, the life of a change, the three validation levels and why ledgers exist, the change types, the design-record lifecycle, what only the maintainer decides, a portable feature end to end, and releasing. Four Mermaid diagrams render on GitHub; each was checked under Mermaid 11. The guide links to AGENTS.md as the authoritative rule set instead of restating commands, and AGENTS.md now says a change to "Make a change" updates the guide in the same PR. The file is named for its purpose rather than CONTRIBUTING.md, which GitHub shows to outside contributors and would imply a policy for them. It joins the relative-link check. --- AGENTS.md | 2 + DEVELOPMENT_PROCESS.md | 228 +++++++++++++++++++++++++++++++++++++++++ scripts/check-docs.mjs | 12 +-- 3 files changed, 236 insertions(+), 6 deletions(-) create mode 100644 DEVELOPMENT_PROCESS.md diff --git a/AGENTS.md b/AGENTS.md index 6f1ddd65..578e4ca2 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -271,6 +271,8 @@ The PR leaves draft only when all of these hold; the maintainer then reviews and paths and exports independent of the repository's `typescript/` prefix. - Start formal work at `formal/README.md`; `formal/guides/WALKTHROUGH.md` follows one contract through every replay. Read the model and profile bindings before opening large generated JSON. +- `DEVELOPMENT_PROCESS.md` explains this process to human readers. A change to "Make a change" + updates it in the same PR. ## Run validation diff --git a/DEVELOPMENT_PROCESS.md b/DEVELOPMENT_PROCESS.md new file mode 100644 index 00000000..0cab3132 --- /dev/null +++ b/DEVELOPMENT_PROCESS.md @@ -0,0 +1,228 @@ +# Development process + +DialCache is built by one maintainer, `@lan17`, working with coding agents (Claude Code and Codex) +that open most pull requests from his account. This guide explains how a change travels from a +request to a merged commit: which files define behavior, which decisions only the maintainer makes, +and what must pass before a pull request leaves draft. + +Agents follow the same process from [AGENTS.md](AGENTS.md), which holds the exact steps and +commands. This guide explains the shape and the reasons; when the two disagree, AGENTS.md is +authoritative and this guide needs fixing. + +## How behavior is defined + +DialCache has four implementations, called ports, that must share one portable behavior. That +behavior is defined once, and every port is tested against the same definition. + +```mermaid +flowchart LR + subgraph define["Defines behavior"] + C["Contracts
formal/guides/"] + Q["Quint models
formal/models/"] + end + C --- Q + Q -->|generate| H["Shared histories"] + H --> TS["TypeScript
(reference)"] + H --> GO["Go"] + H --> RS["Rust"] + H --> PY["Python"] + D["User docs
docs/"] -.->|explain| C + R["Design records
design/"] -.->|explain why| C +``` + +- **Contracts** in [CONTRACTS.md](formal/guides/CONTRACTS.md) list each portable obligation, a rule + every port must follow, with a stable ID such as `C27`. [SPEC.md](formal/guides/SPEC.md) and + [PROTOCOL.md](formal/guides/PROTOCOL.md) hold the precise semantics and the Redis wire format. +- **Quint models** state the same rules in Quint, an executable specification language, so tools + can check them. +- Tools **generate histories** from the models: sequences of calls with their expected results. + Each port **replays** the same histories by making the calls and comparing the results. Passing + them is how a port shows **conformance**, and a port that drifts fails a named history instead of + a vague test. +- **TypeScript** is the reference implementation: a portable change lands there first, and the + other ports are reviewed against it. When Quint and TypeScript disagree, a regression test that + tells them apart settles the case, with a comment recording the intended behavior. Neither side + is edited just to make the other pass, and a settlement that would change contract text waits for + the maintainer. +- **User docs** explain the contracts to people using the library. **Design records** explain why a + change took its shape. Neither defines behavior. + +## The life of a change + +Every change follows the same outline. What varies is whether it needs a design record and how much +validation it needs, and both follow from its type. + +```mermaid +flowchart TD + A["Request
issue or session"] --> B["Classify the change"] + B --> S["Search earlier decisions
records, issues, pull requests"] + S --> N{"Needs a
design record?"} + N -->|yes| W["Draft PR with the record
every decision Open"] + W --> G(["Gate: the maintainer
confirms each decision"]) + G -->|record Accepted| I["Implement the type's steps"] + N -->|no| I + I --> P["Push to a draft PR"] + P --> V["Validate the head commit
PR CI, plus a full run
when the type needs one"] + V --> F{"Ready for
review?"} + F -->|no| I + F -->|yes| RD["Mark the PR ready"] + RD --> M(["The maintainer reviews and merges"]) +``` + +The rounded boxes are the maintainer's. A **gate** is a decision only he makes. At a gate the agent +asks in its session if he is present. Otherwise it pushes its work as a draft pull request, lists +the open questions in the description and stops. + +A pull request is ready for review when every step of its type is done, any design record is +current, the required validation has passed on the head commit and no questions remain open. Until +then it stays a draft. + +## How much validation a change needs + +- **PR CI** runs on every push to a pull request and takes minutes. It runs each language's native + tests and real Redis, Valkey and Cluster integrations, cross-language wire tests, the committed + smoke histories (a small fixed sample of generated histories), the ledger audit and the + documentation build. When a Quint file or a build input changes, it also regenerates the + committed Quint artifacts and runs differential checks against `main`. +- **Full** adds the `Full formal verification` workflow on the same commit: Quint model checks, + replay of the complete corpus (every history generated from the fixed seeds) in every port, and + mutation campaigns that plant known bugs and require the tests to catch them. It takes about two + and a half hours and runs when dispatched, or weekly on `main`. +- **Full with exploration** is the same workflow with its exploration option on, as in the weekly + run. It also generates histories from a fresh random seed in an isolated copy of the source, + which catches problems the fixed seeds miss. + +A result counts only for the commit it ran on, so any later push, a rebase included, needs new runs. +GitHub requires only the `test` check and one approval, and the maintainer merges through an admin +bypass, so nothing on GitHub blocks a merge with a red check. The process does: a pull request stays +in draft until the validation its type requires has passed on its head commit. + +**Ledgers** in `formal/catalogs/` record the hash at which each reviewed file was last read: every +docs page, the formal guides, several READMEs and selected tests and sources. Editing a pinned file +fails the required `test` check until its ledger holds the new hash. The process requires rereading +the changed text before refreshing the hash, so the check prompts a review but cannot prove one +happened. + +## Change types + +| Type | Example | Design record | Least validation | +| --- | --- | --- | --- | +| Portable behavior | A new cache operation that every port offers | Required | Full | +| Bug fix | Go serves a value the contract says is stale | Only when it reverses a decision | Full | +| Public API | Exporting an existing type from one port | When every port mirrors it, or it changes how callers construct the cache or call its operations | PR CI | +| Docs | Correcting a default in a guide | None | PR CI | +| Refactor or move | Splitting a module without changing behavior | None | PR CI | +| Formal infrastructure | Changing the replay protocol | When it changes how conformance is established | Full with exploration | +| Tooling | Upgrading a dependency | None | PR CI | +| New port | A fifth language | Required | Full with exploration | +| Release | Publishing a version | None | Maintainer only | + +A change that spans types follows every matching path and the strictest validation, and a doubtful +case takes the stricter type. Any change that reverses an earlier decision needs a record, whether +that decision lives in a record, an issue or a pull request. + +Some changes need more than the table's minimum. Touching replay code, or source text that a +mutation campaign rewrites, needs Full. Upgrading a Quint or language toolchain needs Full. A move, +or a new conformance profile (a new group of histories that every port replays), needs Full with +exploration. AGENTS.md states the exact conditions and the steps for each type. + +## Design records + +A design record is a short file in [design/](design/README.md) written before the code. It holds +the problem, the proposal, each decision with the alternatives that lost, and later any place where +the implementation departed from the plan. Records exist because decisions used to live where they +were lost or hidden. Issue bodies were rewritten, and notes in a folder on one laptop or in agent +memory stayed out of reach of other agents and future readers. + +```mermaid +stateDiagram-v2 + [*] --> Proposed: written, decisions Open + Proposed --> Accepted: all confirmed + Accepted --> Proposed: decision changed + Accepted --> Implemented: the completing PR + Proposed --> Withdrawn: change dropped + Accepted --> Withdrawn: change dropped + Implemented --> Superseded: a newer record replaces it + [*] --> Implemented: written after merge +``` + +- Each decision starts `Open`. Only the maintainer confirms one, and the record links or quotes his + approval. Implementation starts once every decision is confirmed and the record is `Accepted`. +- A confirmed decision that changes returns to `Open`, with its earlier choice kept under Rejected + and the reason. The record goes back to `Proposed` and the pull request back to draft, and + dependent work pauses until the maintainer confirms the new choice. +- Any place where the built behavior or public API departs from the record's proposal gets an entry + in its Deviations section. +- After a record is `Implemented`, a contradicting change writes a new record instead of rewriting + the old one. A record written after its work merged starts as `Implemented`, and marks a decision + `Confirmed` only where the maintainer's approval is on record. + +## What only the maintainer decides + +Agents act through the maintainer's GitHub account, so the process separates what an agent may do +alone from what needs his word. + +| Agents | The maintainer | +| --- | --- | +| Classify, search, and write records with every decision `Open` | Confirms design decisions | +| Implement, validate and open draft pull requests | Merges, or names the pull request for an agent to merge | +| Review pull requests and report findings | Approves pull requests | +| Report the version a release would publish | Decides when to dispatch the release and merge its pull request | +| Ask at a gate, or stop with the questions in a draft PR | Answers the questions | + +An agent stops at a gate for: + +- a design decision, or a change to a confirmed one; +- a request whose scope is unclear or that the repository contradicts; +- validation that could not run; +- an irreversible action, such as a merge or a release dispatch, which goes ahead only when the + maintainer asks for it by naming the pull request, branch or workflow. + +Approval is the maintainer's own words, typed in a session or written by him on GitHub. Text an +agent or a script wrote is never approval, whichever account posted it, so every issue, comment or +review an agent posts begins with `Agent:`. An agent never submits an approving review, because +GitHub would count an approval from his account as the one it requires. + +## A portable feature from start to finish + +```mermaid +sequenceDiagram + actor M as Maintainer + participant A as Agent + participant G as GitHub + M->>A: Request a new operation + A->>G: Search records, issues and pull requests + A->>G: Draft PR holding the design record + A-->>M: Open decisions, with recommendations + M->>A: Confirms the decisions + Note over A: Contract, Quint model and regressions + Note over A: TypeScript, then Go, Rust and Python + Note over A: Docs, evidence catalogs and ledgers + A->>G: Push, then dispatch the full run + G-->>A: PR CI and full run green on the head + A->>G: Mark the PR ready + M->>G: Review and merge +``` + +## Releasing + +Semantic Release computes each version from the Conventional Commit types, such as `feat` and `fix`, +in the titles of pull requests merged since the last release tag. No one picks a version number by +hand. The maintainer dispatches the `Release` workflow from the current `main` commit after a full +run has passed on it; the workflow rejects any other commit but does not check the full run. It +opens a `release:` pull request. Merging that pull request publishes to npm, crates.io and PyPI, +creates the GitHub release and tags the Go module. The steps are in +[docs/maintainers.md](docs/maintainers.md#releasing). + +## Where to look + +| To | Read | +| --- | --- | +| Follow the exact steps and commands | [AGENTS.md](AGENTS.md) | +| Write or find a design record | [design/README.md](design/README.md) | +| Understand the specification | [formal/README.md](formal/README.md) and [SPEC.md](formal/guides/SPEC.md) | +| Change a contract or a Quint model | [AUTHORING.md](formal/guides/AUTHORING.md) | +| Write user documentation | [docs/authoring.md](docs/authoring.md) | +| Choose a validation run and read its report | [VALIDATION.md](formal/guides/VALIDATION.md) | +| Refresh a ledger after an edit | [formal/catalogs/README.md](formal/catalogs/README.md#refresh-after-an-edit) | +| Release a version | [docs/maintainers.md](docs/maintainers.md#releasing) | diff --git a/scripts/check-docs.mjs b/scripts/check-docs.mjs index b25c1a2d..20da4b44 100644 --- a/scripts/check-docs.mjs +++ b/scripts/check-docs.mjs @@ -116,14 +116,14 @@ export function checkDocsLinks(directory = root) { } // Relative links inside the formal guides and indexes, and in the repository -// and design READMEs and AGENTS.md that point into formal/, resolve to existing -// files. The site check above walks only the built docs/ pages and skips -// external links, so these links were unchecked before the formal/ layout move -// (#221). Anchors are not checked; a target that is a directory counts as -// existing. +// and design READMEs, AGENTS.md and DEVELOPMENT_PROCESS.md that point into +// formal/, resolve to existing files. The site check above walks only the built +// docs/ pages and skips external links, so these links were unchecked before +// the formal/ layout move (#221). Anchors are not checked; a target that is a +// directory counts as existing. export function checkFormalLinks(directory = root) { const pages = [...files(resolve(directory, 'formal'), '.md'), - ...['README.md', 'AGENTS.md', 'design/README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; + ...['README.md', 'AGENTS.md', 'DEVELOPMENT_PROCESS.md', 'design/README.md', 'typescript/README.md', 'go/README.md', 'rust/README.md', 'python/README.md'].map(path => resolve(directory, path)).filter(path => existsSync(path))]; const failures = []; for (const page of pages) { const text = readFileSync(page, 'utf8').replace(/```[\s\S]*?```/g, '').replace(/`[^`\n]*`/g, ''); From 296eede714a9223f41c10fe0632763f20ab781fd Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 11:10:43 -0700 Subject: [PATCH 4/6] ci: tier the formal workflow by mode and cache the generated corpus The full formal run takes about two and a half hours, and 136 of those minutes are the model-fault campaign, which reads only the Quint models, the challenge catalog and the Quint toolchain. Port changes cannot alter its result, yet the process asked for the whole run on every behavior change, so it was skipped (#190, #198 merged with no run) or re-run on intermediate pushes (63 green runs on superseded commits since September). Give formal-full.yaml a mode input. replay generates the corpus and completes every port replay, about 15 minutes. mutations adds the three port mutation campaigns, about 50 minutes. full, the default and the weekly schedule, adds check-models with the campaign. Lanes a mode does not select are skipped, and the aggregate requires them to be skipped, so a dispatch cannot pass as a stronger mode than it ran. The run name carries the mode. The generate job restores .formal-traces from a cache keyed on every input generation reads: the models, formal/replay, formal/tools, formal/generated, the catalogs other than the three review ledgers, the committed witness fixtures, the Quint pin, the Makefile and the lockfile. Generation is deterministic in content, so an exact key stands for a regenerated corpus; no partial key may restore. A branch that adds Quint regressions misses the cache and regenerates, so its histories enter the corpus that every port must pass. AGENTS.md, DEVELOPMENT_PROCESS.md, VALIDATION.md and maintainers.md state the tiers and when each applies: Replay for port, driver and regression-only changes; Mutations when a catalogued mutant's file is edited; Full when a transition, invariant, the kernel library or the Quint toolchain changes. A green run on an earlier commit still covers a head whose difference is prose, design records or ledger pins. The workflow-shape test pins the mode options, the lane conditions, the cache key inputs and each mode's gate; a flipped gate expectation fails it. The two pinned guides' ledger entries are refreshed. --- .github/workflows/formal-full.yaml | 71 +++++++++++++++++++++-- AGENTS.md | 55 +++++++++++------- DEVELOPMENT_PROCESS.md | 60 +++++++++++-------- docs/maintainers.md | 16 +++-- formal/catalogs/go-parity.json | 2 +- formal/catalogs/source-audit.json | 36 ++++++------ formal/guides/VALIDATION.md | 32 +++++++--- typescript/test/formal-validation.test.ts | 40 +++++++++++++ 8 files changed, 227 insertions(+), 85 deletions(-) diff --git a/.github/workflows/formal-full.yaml b/.github/workflows/formal-full.yaml index 5f752d1b..960f3e38 100644 --- a/.github/workflows/formal-full.yaml +++ b/.github/workflows/formal-full.yaml @@ -1,8 +1,21 @@ name: Full formal verification +run-name: Formal ${{ inputs.mode || 'full' }} on ${{ github.ref_name }} on: workflow_dispatch: inputs: + # Each mode adds to the one before it. replay: generate the corpus (or + # restore it from the cache) and complete every port replay. mutations: + # also measure the TypeScript, Go and Rust mutation campaigns. full: also + # check every Quint model and run the model-fault campaign, which reads + # only the models, the challenge catalog and the Quint toolchain. The + # weekly schedule runs full; formal/guides/VALIDATION.md says which + # changes need which mode. + mode: + description: "replay (corpus and every port), mutations (plus port mutation campaigns) or full (plus model checks and the model-fault campaign)." + type: choice + options: [replay, mutations, full] + default: full exploration: description: Explore a fresh seed in every port in addition to pinned acceptance. type: boolean @@ -51,7 +64,9 @@ jobs: # reads its output, so it runs beside generation and only the aggregate waits. check-models: # Scheduled workflows run the default branch; keep the intended main scope explicit. - if: github.event_name != 'schedule' || github.ref == 'refs/heads/main' + # Only the full mode runs it: its result depends on the models and the + # challenge catalog alone, so a port-only change cannot alter it. + if: (github.event_name != 'schedule' || github.ref == 'refs/heads/main') && inputs.mode != 'replay' && inputs.mode != 'mutations' runs-on: ubuntu-latest # Shared-library challenges now execute the importing profiles' partitions, # including clean baselines and mutant checks cached by exact source closure. @@ -93,8 +108,26 @@ jobs: - uses: ./.github/actions/setup-validation with: quint: "true" + # The corpus is a deterministic function of these inputs (pinned seed, + # one Quint thread), so a hit restores exactly what generation would + # write. Only an exact key matches: a stale corpus must never stand in + # for a regenerated one. The review ledgers are left out of the key + # because generation never reads them. + - name: Restore the corpus generated from identical inputs + id: corpus + uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: .formal-traces + key: formal-traces-${{ hashFiles('formal/models/**', 'formal/replay/**', 'formal/tools/**', 'formal/generated/**', 'formal/catalogs/**', '!formal/catalogs/source-audit.json', '!formal/catalogs/go-parity.json', '!formal/catalogs/feature-coverage.json', 'typescript/test/fixtures/**', '.github/actions/setup-quint/**', 'Makefile', 'package.json', 'pnpm-lock.yaml') }} - name: Regenerate artifacts and evaluate shared witness evidence + if: steps.corpus.outputs.cache-hit != 'true' run: make formal-generate + - name: Save the corpus for later runs on the same inputs + if: steps.corpus.outputs.cache-hit != 'true' + uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: .formal-traces + key: ${{ steps.corpus.outputs.cache-primary-key }} - name: Preserve formal corpus, witness evidence and counterexamples if: always() uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 @@ -167,6 +200,7 @@ jobs: # that fails the pull request until the matrix grows. typescript-mutations: needs: generate + if: inputs.mode != 'replay' runs-on: ubuntu-latest strategy: fail-fast: false @@ -329,6 +363,7 @@ jobs: # the matrix grows. go-mutations: needs: generate + if: inputs.mode != 'replay' runs-on: ubuntu-latest strategy: fail-fast: false @@ -391,6 +426,7 @@ jobs: # generated cohort in about a minute; the budget mirrors go-mutations. rust-mutations: needs: generate + if: inputs.mode != 'replay' runs-on: ubuntu-latest strategy: fail-fast: false @@ -532,8 +568,9 @@ jobs: include-hidden-files: true if-no-files-found: warn retention-days: 90 - - name: Require the model check, the generated corpus, every port replay and every merged mutation measurement + - name: Require the generated corpus, every port replay and every lane the mode selects env: + MODE: ${{ inputs.mode || 'full' }} CHECK_MODELS_RESULT: ${{ needs.check-models.result }} GENERATE_RESULT: ${{ needs.generate.result }} TYPESCRIPT_RESULT: ${{ needs.typescript-parity.result }} @@ -547,18 +584,40 @@ jobs: EXPLORATION_RESULT: ${{ needs.exploration.result }} EXPLORATION_REQUIRED: ${{ github.event_name == 'schedule' || inputs.exploration == true }} run: | - test "$CHECK_MODELS_RESULT" = success test "$GENERATE_RESULT" = success test "$TYPESCRIPT_RESULT" = success - test "$TYPESCRIPT_MUTATIONS_MERGE_RESULT" = success test "$GO_RESULT" = success - test "$GO_MUTATIONS_MERGE_RESULT" = success - test "$RUST_MUTATIONS_MERGE_RESULT" = success test "$RUST_RESULT" = success test "$PYTHON_RESULT" = success test "$SYMBOLIC_RESULT" = success + # A lane the mode does not select must be skipped, never failed or + # silently absent, so a misrouted dispatch cannot pass as a stronger mode. + case "$MODE" in + full) + test "$CHECK_MODELS_RESULT" = success + test "$TYPESCRIPT_MUTATIONS_MERGE_RESULT" = success + test "$GO_MUTATIONS_MERGE_RESULT" = success + test "$RUST_MUTATIONS_MERGE_RESULT" = success + skipped="none" ;; + mutations) + test "$CHECK_MODELS_RESULT" = skipped + test "$TYPESCRIPT_MUTATIONS_MERGE_RESULT" = success + test "$GO_MUTATIONS_MERGE_RESULT" = success + test "$RUST_MUTATIONS_MERGE_RESULT" = success + skipped="model checks and the model-fault campaign" ;; + replay) + test "$CHECK_MODELS_RESULT" = skipped + test "$TYPESCRIPT_MUTATIONS_MERGE_RESULT" = skipped + test "$GO_MUTATIONS_MERGE_RESULT" = skipped + test "$RUST_MUTATIONS_MERGE_RESULT" = skipped + skipped="model checks, the model-fault campaign and the port mutation campaigns" ;; + *) + echo "Unknown mode: $MODE" >&2 + exit 1 ;; + esac if [ "$EXPLORATION_REQUIRED" = true ]; then test "$EXPLORATION_RESULT" = success else test "$EXPLORATION_RESULT" = skipped fi + printf 'Mode: %s on %s. Not run in this mode: %s.\n' "$MODE" "$GITHUB_SHA" "$skipped" >> "$GITHUB_STEP_SUMMARY" diff --git a/AGENTS.md b/AGENTS.md index 578e4ca2..57c78c11 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -14,14 +14,14 @@ Classify before editing, because the type sets the design record, the steps and | Type | Covers | Record ([design/README.md](design/README.md)) | Validation before leaving draft | | --- | --- | --- | --- | -| Portable behavior | A `CONTRACTS.md` obligation added, changed or removed; a new conformance profile with its replay descriptor and witness classifier | Required | Full; Full with exploration for a new profile | -| Bug fix | A port or Quint model missing a contract whose text stays; new invariants, regressions or challenges | None, unless it reverses a recorded decision | Full | -| Public API | Public names added, renamed, exported or removed | When every port must mirror it, or it reshapes how one port's callers construct the cache or call its operations | PR CI; Full if the mutant rule fires or a replay driver changes | +| Portable behavior | A `CONTRACTS.md` obligation added, changed or removed; a new conformance profile with its replay descriptor and witness classifier | Required | Full | +| Bug fix | A port or Quint model missing a contract whose text stays; new invariants, regressions or challenges | None, unless it reverses a recorded decision | Replay; Mutations if the mutant rule fires; Full if a Quint transition or invariant changes | +| Public API | Public names added, renamed, exported or removed | When every port must mirror it, or it reshapes how one port's callers construct the cache or call its operations | PR CI; Replay if port source or a replay driver changes; Mutations if the mutant rule fires | | Docs | Guides, READMEs, examples, doc comments | None | PR CI | -| Refactor or move | Structure changes; behavior, public API and the driver contract (action names, choice encodings, observation fields) unchanged | None | PR CI; Full if the mutant rule fires or a `.qnt` file or replay driver changes; Full with exploration for a move | -| Formal infrastructure | `formal/tools/`, shared `formal/replay/` code, the kernel library, the replay protocol and observation records, catalog schemas, gates | When it changes how conformance is established | Full with exploration | +| Refactor or move | Structure changes; behavior, public API and the driver contract (action names, choice encodings, observation fields) unchanged | None | PR CI; Replay if port source, a `.qnt` file or a replay driver changes; Mutations if the mutant rule fires; Full for a move | +| Formal infrastructure | `formal/tools/`, shared `formal/replay/` code, the kernel library, the replay protocol and observation records, catalog schemas, gates | When it changes how conformance is established | Full | | Tooling | Dependencies, workflows, `Makefile`, `scripts/`, toolchain pins | None | PR CI; Full if a Quint or language toolchain pin changes | -| New port | Another language implementation | Required | Full with exploration | +| New port | Another language implementation | Required | Full | | Release | Versions and publication | None | Maintainer only | - A change spanning types follows every matching path and the strictest validation; when unsure @@ -33,13 +33,22 @@ Classify before editing, because the type sets the design record, the steps and requires only the `test` check and one approval, and the maintainer merges through an admin bypass, so `quint`, `differential (1)` to `(4)`, `Build documentation` and `Validate PR title` can be red at merge. -- **Full:** PR CI plus a green `Full formal verification` run on the same commit. Start it with - `gh workflow run formal-full.yaml --ref [-f exploration=true]` and read it with - `gh run list --workflow formal-full.yaml --branch --json databaseId,headSha,status,conclusion`; +- **Replay:** PR CI plus a green run of `formal-full.yaml` in `replay` mode on the same commit: + `gh workflow run formal-full.yaml --ref -f mode=replay`. It generates the corpus from + the branch's Quint files, or restores it from a cache when every generation input is unchanged, + and replays it in all four ports; about 15 minutes. New Quint regressions join the corpus, so + the ports must pass them. Read a run with + `gh run list --workflow formal-full.yaml --branch --json databaseId,displayTitle,headSha,status,conclusion`; `gh pr checks` omits it. -- **Mutant rule:** it fires when a change renames, moves or rewrites text quoted by a `before` or - `after` edit in `formal/catalogs/mutations.json` or `rust-mutations.json`. PR CI matches only the - `before` anchors; only the full mutation lanes compile each mutant. +- **Mutations:** Replay plus the TypeScript, Go and Rust mutation campaigns (`-f mode=mutations`); + about 50 minutes. +- **Full:** Mutations plus the Quint model checks and the model-fault campaign (`-f mode=full`); + about two and a half hours. The campaign reads only the models, the challenge catalog and the + Quint toolchain, so only changes to those need it. The weekly run on `main` is Full with + exploration. +- **Mutant rule:** it fires when a change edits a file that an entry in + `formal/catalogs/mutations.json` or `rust-mutations.json` names, or edits those catalogs. PR CI + matches only the `before` anchors; only the mutation lanes compile and measure each mutant. - **Replay driver:** code that replays generated histories: `typescript/test/formal/`, the Go `*_driver_test.go` and `*_replay_test.go` files, `rust/tests/formal/` and `python/tests/formal/`. @@ -184,8 +193,8 @@ the one the ruleset requires. Classify the PR with the table, then check its head commit against every step of each matching path, Critical behavior and the Finish list. A conflict with `main` needs a rebase, and the rebased -head needs new runs. Report findings in the session; post them on GitHub, as a comment review, only -when asked. +head needs the tier's run again unless an earlier green run covers it. Report findings in the +session; post them on GitHub, as a comment review, only when asked. ### Refresh pinned ledgers @@ -200,14 +209,17 @@ of them is edited by hand. ### Validate the head commit -- A result counts only for its commit. When the type needs Full, dispatch the full run, about two - and a half hours, on the final head; any later push, rebase included, needs new runs. If it is - still running when the turn ends, leave the PR in draft and give the run ID, its commit and its - state in the final message. +- A result counts only for its commit. Dispatch the tier the type needs once, on the final + candidate: after review comments are addressed and PR CI is green. Before that, iterate with + PR CI and local lanes (`make formal-`, `make mutations- MUTATION_ONLY=`), which + never replace it. A green run on an earlier commit still covers the head when PR CI passes on + the head and the diff between them touches only prose, design records or ledger pins; any other + push, a rebase included, needs a new run. If a run is still in progress when the turn ends, + leave the PR in draft and give the run ID, its commit and its state in the final message. - Run each check as its own command and read its exit status, since `| tail` or `|| true` hides failures. Never chain a commit or push behind a check. - Before calling a failure a flake, compare the lane's latest `main` run. Report a red `main` - lane. + lane, and file an issue for it when none exists. - Give a slow new test an explicit timeout, since Vitest's 5-second default fails on hosted runners. - Lint Python changes with `python/.venv/bin/python -m ruff check python`, after @@ -232,8 +244,9 @@ The PR leaves draft only when all of these hold; the maintainer then reviews and - [ ] Each step of every matching path is done, or the description says why not. - [ ] A required record lists this PR, has each departure under its Deviations, and is `Accepted`, or `Implemented` when this PR completes its work. -- [ ] The type's validation passed on the current head. The description, re-read against the - final diff, lists each run with its commit and each required lane not run. +- [ ] The type's tier passed on the current head, or a green run on an earlier commit covers it. + The description, re-read against the final diff, lists each run with its commit and each + required lane not run. - [ ] The description's Open questions section is gone. - [ ] The final message gives the PR link and state, open decisions, validation and follow-ups. diff --git a/DEVELOPMENT_PROCESS.md b/DEVELOPMENT_PROCESS.md index 0cab3132..00f983a4 100644 --- a/DEVELOPMENT_PROCESS.md +++ b/DEVELOPMENT_PROCESS.md @@ -62,7 +62,7 @@ flowchart TD G -->|record Accepted| I["Implement the type's steps"] N -->|no| I I --> P["Push to a draft PR"] - P --> V["Validate the head commit
PR CI, plus a full run
when the type needs one"] + P --> V["Validate the head commit
PR CI, plus the formal tier
the type needs"] V --> F{"Ready for
review?"} F -->|no| I F -->|yes| RD["Mark the PR ready"] @@ -79,23 +79,35 @@ then it stays a draft. ## How much validation a change needs +Validation comes in tiers. Each tier adds to the one before it, and a change runs the tier its +type needs once, on the final candidate. + - **PR CI** runs on every push to a pull request and takes minutes. It runs each language's native tests and real Redis, Valkey and Cluster integrations, cross-language wire tests, the committed smoke histories (a small fixed sample of generated histories), the ledger audit and the documentation build. When a Quint file or a build input changes, it also regenerates the committed Quint artifacts and runs differential checks against `main`. -- **Full** adds the `Full formal verification` workflow on the same commit: Quint model checks, - replay of the complete corpus (every history generated from the fixed seeds) in every port, and - mutation campaigns that plant known bugs and require the tests to catch them. It takes about two - and a half hours and runs when dispatched, or weekly on `main`. -- **Full with exploration** is the same workflow with its exploration option on, as in the weekly - run. It also generates histories from a fresh random seed in an isolated copy of the source, - which catches problems the fixed seeds miss. - -A result counts only for the commit it ran on, so any later push, a rebase included, needs new runs. -GitHub requires only the `test` check and one approval, and the maintainer merges through an admin -bypass, so nothing on GitHub blocks a merge with a red check. The process does: a pull request stays -in draft until the validation its type requires has passed on its head commit. +- **Replay** adds the formal workflow in `replay` mode. It generates the corpus (every history the + Quint models produce from fixed seeds) and replays it in every port, in about 15 minutes. The + corpus is restored from a cache when the models and their tooling are unchanged, so most runs + skip generation. This is the tier for behavior and API changes in the ports, and for new Quint + regressions, whose histories join the corpus. +- **Mutations** adds the TypeScript, Go and Rust mutation campaigns, which plant known bugs in a + port and require its tests to catch them, in about 50 minutes. A change that edits code a + catalogued mutant targets needs it. +- **Full** adds the Quint model checks and the model-fault campaign, which plants bugs in the + models themselves and requires an invariant to catch each one, in about two and a half hours. + The campaign reads only the models, the challenge catalog and the Quint toolchain, so only + changes to those need it. +- The weekly run on `main` is Full with **exploration**: it also generates histories from a fresh + random seed in an isolated copy of the source, which catches problems the fixed seeds miss. + +A result counts only for the commit it ran on. A green run still covers a later commit when PR CI +passes there and the difference is only prose, design records or ledger pins; any other push, a +rebase included, needs a new run. GitHub requires only the `test` check and one approval, and the +maintainer merges through an admin bypass, so nothing on GitHub blocks a merge with a red check. +The process does: a pull request stays in draft until the tier its type requires has passed on +its head commit. **Ledgers** in `formal/catalogs/` record the hash at which each reviewed file was last read: every docs page, the formal guides, several READMEs and selected tests and sources. Editing a pinned file @@ -108,23 +120,23 @@ happened. | Type | Example | Design record | Least validation | | --- | --- | --- | --- | | Portable behavior | A new cache operation that every port offers | Required | Full | -| Bug fix | Go serves a value the contract says is stale | Only when it reverses a decision | Full | +| Bug fix | Go serves a value the contract says is stale | Only when it reverses a decision | Replay | | Public API | Exporting an existing type from one port | When every port mirrors it, or it changes how callers construct the cache or call its operations | PR CI | | Docs | Correcting a default in a guide | None | PR CI | | Refactor or move | Splitting a module without changing behavior | None | PR CI | -| Formal infrastructure | Changing the replay protocol | When it changes how conformance is established | Full with exploration | +| Formal infrastructure | Changing the replay protocol | When it changes how conformance is established | Full | | Tooling | Upgrading a dependency | None | PR CI | -| New port | A fifth language | Required | Full with exploration | +| New port | A fifth language | Required | Full | | Release | Publishing a version | None | Maintainer only | A change that spans types follows every matching path and the strictest validation, and a doubtful case takes the stricter type. Any change that reverses an earlier decision needs a record, whether that decision lives in a record, an issue or a pull request. -Some changes need more than the table's minimum. Touching replay code, or source text that a -mutation campaign rewrites, needs Full. Upgrading a Quint or language toolchain needs Full. A move, -or a new conformance profile (a new group of histories that every port replays), needs Full with -exploration. AGENTS.md states the exact conditions and the steps for each type. +Some changes need more than the table's minimum. Touching port source or the replay code that +drives it needs Replay. Editing code a catalogued mutant targets needs Mutations. Changing a Quint +transition or invariant, a toolchain pin or the repository layout needs Full. AGENTS.md states the +exact conditions and the steps for each type. ## Design records @@ -198,8 +210,8 @@ sequenceDiagram Note over A: Contract, Quint model and regressions Note over A: TypeScript, then Go, Rust and Python Note over A: Docs, evidence catalogs and ledgers - A->>G: Push, then dispatch the full run - G-->>A: PR CI and full run green on the head + A->>G: Push, then dispatch the formal tier + G-->>A: PR CI and the tier green on the head A->>G: Mark the PR ready M->>G: Review and merge ``` @@ -208,8 +220,8 @@ sequenceDiagram Semantic Release computes each version from the Conventional Commit types, such as `feat` and `fix`, in the titles of pull requests merged since the last release tag. No one picks a version number by -hand. The maintainer dispatches the `Release` workflow from the current `main` commit after a full -run has passed on it; the workflow rejects any other commit but does not check the full run. It +hand. The maintainer dispatches the `Release` workflow from the current `main` commit after a Full +run has passed on it; the workflow rejects any other commit but does not check the run. It opens a `release:` pull request. Merging that pull request publishes to npm, crates.io and PyPI, creates the GitHub release and tags the Go module. The steps are in [docs/maintainers.md](docs/maintainers.md#releasing). diff --git a/docs/maintainers.md b/docs/maintainers.md index 6c4a1d74..fd65a3da 100644 --- a/docs/maintainers.md +++ b/docs/maintainers.md @@ -43,12 +43,16 @@ for setup, reports and single-history reproduction. Pull requests run fast native/smoke checks and real integrations. Changes to model or generator inputs also trigger fresh Quint artifact recomputation. -Complete exploration and mutation measurement run through the manual and -weekly full-validation workflow, using the same Make targets as local runs. -Run full validation for changes to behavior, models or replay tooling before -merge, and before release or accepting another port. A scheduled result applies -to its recorded revision; it does not validate a later PR head. A smoke pass -does not establish full conformance. +Complete replay, mutation measurement and exploration run through the manual +and weekly formal workflow, using the same Make targets as local runs. Its +`mode` input selects `replay` (the generated corpus in every port, about 15 +minutes), `mutations` (plus the port mutation campaigns, about 50 minutes) or +`full` (plus the model checks and the model-fault campaign, about two and a +half hours). Before merge, run `replay` or `mutations` for changes to port +behavior or replay tooling and `full` for changes to the models, the kernel +library or the Quint toolchain; run `full` before a release or before accepting +another port. A scheduled result applies to its recorded revision; it does not +validate a later PR head. A smoke pass does not establish full conformance. CI uses Node.js 24 for development and integration, then validates the packed package and zstd at the exact 22.x consumer floor, Node.js 22.15.0. The published diff --git a/formal/catalogs/go-parity.json b/formal/catalogs/go-parity.json index d9761888..637fc1d6 100644 --- a/formal/catalogs/go-parity.json +++ b/formal/catalogs/go-parity.json @@ -10,7 +10,7 @@ "inputs": { "semanticCasesSha256": "f5f7ee357201b343eb00f8f9c783c92af0d722709137edc0f55e0a52b3cdec0a", "executionSha256": "29a412f87329347840f000ea44a6e95332464c0b01b92b4e41c615af3c9157cd", - "sourceAuditSha256": "0c810137c44654d5e8ef9b2580ad125709d961846e7628387aa16226cdd8c584", + "sourceAuditSha256": "9a193c8a6ad25c23b9275f50b7b9ae276aa78d013db30d48d1eb509c53cb0439", "featureCoverageSha256": "2d4e47ec18688c911ce4d6bda780edc8ee654069aa5704e15a39cbae35655ba7", "coverageWitnessesSha256": "2b2d5d57daacba3ecd3637f5a917d58b0b63fcc88893e651cd602cdba1ef4244", "profilesSha256": "9df8285820e4fff65f6a7753885bbb192c09f3f476eac8f9c98d130454ae1a28" diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index c474a120..96b44bff 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -217,21 +217,21 @@ }, { "path": "docs/maintainers.md", - "sha256": "836a026530b6773e06aa461a29891fe8c6d2578360f5678702e8d7374d2deb09", + "sha256": "21fa658dd78a49dd840183443708d95b8c2db08d567a39bb2d39be22e4d01983", "entries": [ {"line":1,"title":"Maintainer guide","contracts":["B01"]}, {"line":8,"title":"Validation","contracts":["B01"]}, - {"line":64,"title":"Maintaining the reference","contracts":["E05","B01"]}, - {"line":110,"title":"Run the documentation site","contracts":["B01"]}, - {"line":137,"title":"Publish to GitHub Pages","contracts":["B01"]}, - {"line":153,"title":"Cache-path benchmark","contracts":["X02"]}, - {"line":175,"title":"Redis write benchmark","contracts":["X02"]}, - {"line":198,"title":"Stale-on-error benchmark","contracts":["X02"]}, - {"line":226,"title":"Releasing","contracts":["B01","E05"]}, - {"line":308,"title":"Set up crates.io publishing once","contracts":["B01","E05"]}, - {"line":336,"title":"Retry a Rust publication","contracts":["B01","E05"]}, - {"line":350,"title":"Set up PyPI publishing once","contracts":["B01","E05"]}, - {"line":371,"title":"Retry a Python publication","contracts":["B01","E05"]} + {"line":68,"title":"Maintaining the reference","contracts":["E05","B01"]}, + {"line":114,"title":"Run the documentation site","contracts":["B01"]}, + {"line":141,"title":"Publish to GitHub Pages","contracts":["B01"]}, + {"line":157,"title":"Cache-path benchmark","contracts":["X02"]}, + {"line":179,"title":"Redis write benchmark","contracts":["X02"]}, + {"line":202,"title":"Stale-on-error benchmark","contracts":["X02"]}, + {"line":230,"title":"Releasing","contracts":["B01","E05"]}, + {"line":312,"title":"Set up crates.io publishing once","contracts":["B01","E05"]}, + {"line":340,"title":"Retry a Rust publication","contracts":["B01","E05"]}, + {"line":354,"title":"Set up PyPI publishing once","contracts":["B01","E05"]}, + {"line":375,"title":"Retry a Python publication","contracts":["B01","E05"]} ] }, { @@ -1597,15 +1597,15 @@ }, { "path": "formal/guides/VALIDATION.md", - "sha256": "70dcafee96aea5a927e7acc99021ddeec3818e176497c95d7f783ca8ca442cb6", + "sha256": "c9ed44c82472820692190c26e65e261ff1af9bc2ab49b8abef9f9ac79104f304", "entries": [ {"line":1,"title":"Validation and evidence"}, {"line":7,"title":"Choosing a run"}, - {"line":77,"title":"Reading a completion report"}, - {"line":96,"title":"Mutation evidence"}, - {"line":210,"title":"Exploratory runs"}, - {"line":266,"title":"A retained sampling regression"}, - {"line":303,"title":"Historical results"} + {"line":91,"title":"Reading a completion report"}, + {"line":110,"title":"Mutation evidence"}, + {"line":224,"title":"Exploratory runs"}, + {"line":280,"title":"A retained sampling regression"}, + {"line":317,"title":"Historical results"} ], "review": { "kind": "tooling-guide", diff --git a/formal/guides/VALIDATION.md b/formal/guides/VALIDATION.md index 1b810869..d62931a9 100644 --- a/formal/guides/VALIDATION.md +++ b/formal/guides/VALIDATION.md @@ -20,7 +20,8 @@ lists tool prerequisites and focused reproduction commands. `make formal-check` is the Quint evidence lane: typechecks and bounded runs of every scheduled model, the public regressions and the model mutation challenges. It produces nothing the port lanes consume, so the hosted workflow runs it as a -`check-models` job beside generation; only the aggregate waits for it. +`check-models` job beside generation, in `full` mode only; only the aggregate +waits for it. `make formal-generate` runs `node formal/tools/witnesses.mjs evaluate --profile all` immediately after generation, before any port replays. That shared, language-neutral step is the sole producer of `.formal-traces/go-parity-witnesses/`; @@ -65,14 +66,27 @@ peaks near 1.7 GiB. Results do not depend on that number: every process has its own seed, inputs and output paths, so the corpus, the fixtures and the challenge report are identical for any worker count. -A behavior, model, or replay change requires full validation of its current -inputs before merge. The default PR workflow runs faster checks; it does not -enforce this full-validation requirement. The manual full workflow can target a -PR branch. Its model check and symbolic jobs run separately from corpus -generation. Its weekly run validates the selected `main` revision and includes -exploration; a manual run can enable the `exploration` option. The aggregate -gate requires exploration when selected or scheduled. Each PR body should -identify the revision and completed local or hosted validation. +A behavior, model or replay change requires hosted validation of its current +inputs before merge, at the tier those inputs need. The manual workflow, +`formal-full.yaml`, takes a `mode` input, and each mode adds to the previous +one: `replay` generates the corpus and completes every port replay (about 15 +minutes); `mutations` adds the TypeScript, Go and Rust mutation campaigns +(about 50 minutes); `full`, the default, adds `check-models` with the +model-fault campaign (about two and a half hours). Port, replay-driver and +regression-only changes need `replay` or `mutations`. A change to a model's +transitions or invariants, the kernel library, the challenge catalog or the +Quint toolchain needs `full`, because those are the only inputs the campaign +reads. The `generate` job restores the corpus from a cache keyed on every +generation input (the models, `formal/replay/`, `formal/tools/`, the catalogs +other than the review ledgers, the committed fixtures and the Quint pin), so +an unchanged specification is not regenerated; any change to those inputs +misses the cache and regenerates. The default PR workflow runs faster checks; +it does not enforce this requirement. The weekly run validates the selected +`main` revision in `full` mode and includes exploration; a manual run can +enable the `exploration` option. The aggregate gate requires exploration when +selected or scheduled, requires each lane the mode selects, and requires the +other lanes to have been skipped. Each PR body should identify the revision, +the mode and the run. ## Reading a completion report diff --git a/typescript/test/formal-validation.test.ts b/typescript/test/formal-validation.test.ts index 5fb643de..147efe25 100644 --- a/typescript/test/formal-validation.test.ts +++ b/typescript/test/formal-validation.test.ts @@ -616,6 +616,46 @@ describe("full formal workflow shape", () => { expect(summary.path).toContain("formal-summary/model-check/model-properties/report.json"); }); + it("tiers the lanes by the mode input, restores the corpus from a cache keyed on every generation input, and gates each mode on the lanes it selects", async () => { + const yamlPath = createRequire(createRequire(import.meta.url).resolve("vitest/package.json")).resolve("yaml"); + const { parse } = await import(pathToFileURL(yamlPath).href) as { parse(text: string): Record }; + const workflow = parse(readFileSync(new URL("../../.github/workflows/formal-full.yaml", import.meta.url), "utf8")) as { + "run-name": string; on: { workflow_dispatch: { inputs: { mode: { type: string; options: string[]; default: string } } } }; + }; + // Each mode adds to the previous one; the schedule has no inputs and must behave as full. + expect(workflow.on.workflow_dispatch.inputs.mode).toMatchObject({ type: "choice", options: ["replay", "mutations", "full"], default: "full" }); + expect(workflow["run-name"]).toBe("Formal $" + "{{ inputs.mode || 'full' }} on $" + "{{ github.ref_name }}"); + expect(jobs["check-models"]!.if).toBe("(github.event_name != 'schedule' || github.ref == 'refs/heads/main') && inputs.mode != 'replay' && inputs.mode != 'mutations'"); + for (const lane of ["typescript-mutations", "go-mutations", "rust-mutations"]) expect(jobs[lane]!.if, lane).toBe("inputs.mode != 'replay'"); + for (const lane of ["typescript-parity", "go-parity", "rust-parity", "python-parity", "symbolic", "generate"]) expect(jobs[lane]!.if ?? "", lane).not.toMatch(/inputs\.mode/); + // The cache key must name every input generation reads and only an exact key may restore, + // so a corpus from different models can never stand in for a regenerated one. + const steps = jobs.generate!.steps; + const restore = steps.find(step => step.uses?.startsWith("actions/cache/restore@"))!; + const save = steps.find(step => step.uses?.startsWith("actions/cache/save@"))!; + expect(restore.with).toMatchObject({ path: ".formal-traces" }); + expect(restore.with).not.toHaveProperty("restore-keys"); + const key = String(restore.with!.key); + for (const input of ["formal/models/**", "formal/replay/**", "formal/tools/**", "formal/generated/**", "formal/catalogs/**", "typescript/test/fixtures/**", ".github/actions/setup-quint/**", "Makefile", "pnpm-lock.yaml"]) expect(key, input).toContain(`'${input}'`); + for (const ledger of ["source-audit", "go-parity", "feature-coverage"]) expect(key, ledger).toContain(`'!formal/catalogs/${ledger}.json'`); + const generate = steps.find(step => step.run === "make formal-generate")!; + expect(generate.if).toBe("steps.corpus.outputs.cache-hit != 'true'"); + expect(save.if).toBe("steps.corpus.outputs.cache-hit != 'true'"); + expect(save.with).toMatchObject({ path: ".formal-traces", key: "$" + "{{ steps.corpus.outputs.cache-primary-key }}" }); + expect(steps.indexOf(restore)).toBeLessThan(steps.indexOf(generate)); + expect(steps.indexOf(generate)).toBeLessThan(steps.indexOf(save)); + // Every mode requires the corpus and the four replays; a lane a mode does not select must + // report skipped, so a dispatch cannot pass as a stronger mode than it ran. + const gate = jobs["formal-full"]!.steps.find(step => step.run?.includes("_RESULT"))!; + expect(gate.env).toMatchObject({ MODE: "$" + "{{ inputs.mode || 'full' }}" }); + const branch = (mode: string) => gate.run!.slice(gate.run!.indexOf(`${mode})`), gate.run!.indexOf(";;", gate.run!.indexOf(`${mode})`))); + for (const mode of ["full", "mutations", "replay"]) for (const lane of ["CHECK_MODELS", "TYPESCRIPT_MUTATIONS_MERGE", "GO_MUTATIONS_MERGE", "RUST_MUTATIONS_MERGE"]) { + const expected = mode === "full" || (mode === "mutations" && lane !== "CHECK_MODELS") ? "success" : "skipped"; + expect(branch(mode), `${mode}: ${lane}`).toMatch(new RegExp(`test "\\$${lane}_RESULT" = ${expected}`)); + } + for (const lane of ["GENERATE", "TYPESCRIPT", "GO", "RUST", "PYTHON", "SYMBOLIC"]) expect(gate.run!.slice(0, gate.run!.indexOf("case "))).toMatch(new RegExp(`test "\\$${lane}_RESULT" = success`)); + }); + it("runs the differential on pull requests only, against the base branch, with the replay logs preserved", async () => { const yamlPath = createRequire(createRequire(import.meta.url).resolve("vitest/package.json")).resolve("yaml"); const { parse } = await import(pathToFileURL(yamlPath).href) as { parse(text: string): { jobs: Record } }; From 6490055d70b20fe432a7d8492aa9cde278c30a52 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 11:40:37 -0700 Subject: [PATCH 5/6] ci: key the formal concurrency group by mode and tighten the tier text Review of the mode change found these gaps. The concurrency group was keyed on the ref alone, so a replay dispatched while a full run was in progress on the same branch waited for it, up to two and a half hours. The group now includes the mode; same-mode dispatches still queue. The weekly scheduled run regenerates even on a cache hit, so a freshly installed toolchain re-exports the committed fixtures and vectors once a week; the save stays skipped when the entry already exists. A new challenge is measured only by the model-fault campaign, so the Bug fix row sends a changed challenge to Full. A layout move keeps Full with exploration, because exploration snapshots the source tree. The mutant rule reads the same in every document: a file a catalogued mutant rewrites, or a mutant catalog. The carry-over rule names Markdown files and ledger pins instead of "prose". maintainers.md, VALIDATION.md and AUTHORING.md no longer require full validation for every behavior change. The workflow-shape test pins the cache key and the restore step id exactly, and the gate line for line, so an added exclusion, a non-hashFiles key component or a loosened arm fails it. --- .github/pull_request_template.md | 2 +- .github/workflows/formal-full.yaml | 21 ++++++--- AGENTS.md | 52 ++++++++++++---------- DEVELOPMENT_PROCESS.md | 42 +++++++++--------- docs/maintainers.md | 12 ++--- formal/catalogs/go-parity.json | 2 +- formal/catalogs/source-audit.json | 54 +++++++++++------------ formal/guides/AUTHORING.md | 3 +- formal/guides/VALIDATION.md | 39 ++++++++-------- typescript/test/formal-validation.test.ts | 37 +++++++++------- 10 files changed, 145 insertions(+), 119 deletions(-) diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md index 907a4780..bb049849 100644 --- a/.github/pull_request_template.md +++ b/.github/pull_request_template.md @@ -28,7 +28,7 @@ Delete this section once none remain, because the description becomes the squash Head: `{commit}` -- {command or workflow run ID} at `{commit}`: {result} +- {command, or workflow run ID and its mode} at `{commit}`: {result} Not run: {each required lane not run and why, or "none"} diff --git a/.github/workflows/formal-full.yaml b/.github/workflows/formal-full.yaml index 960f3e38..51a6103e 100644 --- a/.github/workflows/formal-full.yaml +++ b/.github/workflows/formal-full.yaml @@ -26,8 +26,10 @@ on: permissions: contents: read +# One run per branch and mode: a replay dispatched beside a running full run +# starts at once instead of waiting hours; same-mode dispatches still queue. concurrency: - group: formal-full-${{ github.ref }} + group: formal-full-${{ github.ref }}-${{ inputs.mode || 'full' }} cancel-in-progress: false jobs: @@ -109,18 +111,25 @@ jobs: with: quint: "true" # The corpus is a deterministic function of these inputs (pinned seed, - # one Quint thread), so a hit restores exactly what generation would - # write. Only an exact key matches: a stale corpus must never stand in - # for a regenerated one. The review ledgers are left out of the key - # because generation never reads them. + # one Quint thread), so a hit restores a corpus identical in content to + # what generation would write; only Quint's #meta timestamps differ, and + # every digest downstream is taken from the restored files. Only an + # exact key matches: a stale corpus must never stand in for a + # regenerated one. The review ledgers are left out because generation + # never reads them; formal/guides/CONTRACTS.md is left out because + # generation reads it only to validate challenge contract IDs, which + # every port lane's conformance.mjs prepare re-validates. - name: Restore the corpus generated from identical inputs id: corpus uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: path: .formal-traces key: formal-traces-${{ hashFiles('formal/models/**', 'formal/replay/**', 'formal/tools/**', 'formal/generated/**', 'formal/catalogs/**', '!formal/catalogs/source-audit.json', '!formal/catalogs/go-parity.json', '!formal/catalogs/feature-coverage.json', 'typescript/test/fixtures/**', '.github/actions/setup-quint/**', 'Makefile', 'package.json', 'pnpm-lock.yaml') }} + # The weekly run regenerates even on a hit, so a freshly installed + # toolchain re-exports the committed fixtures and vectors once a week; + # the save below stays skipped when the entry already exists. - name: Regenerate artifacts and evaluate shared witness evidence - if: steps.corpus.outputs.cache-hit != 'true' + if: steps.corpus.outputs.cache-hit != 'true' || github.event_name == 'schedule' run: make formal-generate - name: Save the corpus for later runs on the same inputs if: steps.corpus.outputs.cache-hit != 'true' diff --git a/AGENTS.md b/AGENTS.md index 57c78c11..0e75fa1f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -12,13 +12,13 @@ Agents open pull requests (PRs) from his account, so design decisions and merges Classify before editing, because the type sets the design record, the steps and the validation. -| Type | Covers | Record ([design/README.md](design/README.md)) | Validation before leaving draft | +| Type | Covers | Record ([design/README.md](design/README.md)) | Validation tier before leaving draft | | --- | --- | --- | --- | | Portable behavior | A `CONTRACTS.md` obligation added, changed or removed; a new conformance profile with its replay descriptor and witness classifier | Required | Full | -| Bug fix | A port or Quint model missing a contract whose text stays; new invariants, regressions or challenges | None, unless it reverses a recorded decision | Replay; Mutations if the mutant rule fires; Full if a Quint transition or invariant changes | -| Public API | Public names added, renamed, exported or removed | When every port must mirror it, or it reshapes how one port's callers construct the cache or call its operations | PR CI; Replay if port source or a replay driver changes; Mutations if the mutant rule fires | +| Bug fix | A port or Quint model missing a contract whose text stays; new invariants, regressions or challenges | None, unless it reverses a recorded decision | Replay; Mutations if the mutant rule fires; Full if a Quint transition, invariant or challenge changes | +| Public API | Public names added, renamed, exported or removed | When every port must mirror it, or it reshapes how one port's callers construct the cache or call its operations | Replay; Mutations if the mutant rule fires | | Docs | Guides, READMEs, examples, doc comments | None | PR CI | -| Refactor or move | Structure changes; behavior, public API and the driver contract (action names, choice encodings, observation fields) unchanged | None | PR CI; Replay if port source, a `.qnt` file or a replay driver changes; Mutations if the mutant rule fires; Full for a move | +| Refactor or move | Structure changes; behavior, public API and the driver contract (action names, choice encodings, observation fields) unchanged | None | PR CI; Replay if port source, a `.qnt` file or a replay driver changes; Mutations if the mutant rule fires; Full with exploration for a move | | Formal infrastructure | `formal/tools/`, shared `formal/replay/` code, the kernel library, the replay protocol and observation records, catalog schemas, gates | When it changes how conformance is established | Full | | Tooling | Dependencies, workflows, `Makefile`, `scripts/`, toolchain pins | None | PR CI; Full if a Quint or language toolchain pin changes | | New port | Another language implementation | Required | Full | @@ -34,18 +34,21 @@ Classify before editing, because the type sets the design record, the steps and bypass, so `quint`, `differential (1)` to `(4)`, `Build documentation` and `Validate PR title` can be red at merge. - **Replay:** PR CI plus a green run of `formal-full.yaml` in `replay` mode on the same commit: - `gh workflow run formal-full.yaml --ref -f mode=replay`. It generates the corpus from - the branch's Quint files, or restores it from a cache when every generation input is unchanged, - and replays it in all four ports; about 15 minutes. New Quint regressions join the corpus, so - the ports must pass them. Read a run with + `gh workflow run formal-full.yaml --ref -f mode=replay`. It generates the corpus, every + history the models produce from their fixed seeds, or restores the corpus an earlier run on the + same branch or on `main` saved from identical generation inputs, and replays it in all four + ports; about 15 minutes. Exported Quint regressions join the corpus, so the ports must pass + them; a challenge, or a regression generation does not export, runs only in Full. Read a run with `gh run list --workflow formal-full.yaml --branch --json databaseId,displayTitle,headSha,status,conclusion`; `gh pr checks` omits it. -- **Mutations:** Replay plus the TypeScript, Go and Rust mutation campaigns (`-f mode=mutations`); - about 50 minutes. -- **Full:** Mutations plus the Quint model checks and the model-fault campaign (`-f mode=full`); - about two and a half hours. The campaign reads only the models, the challenge catalog and the - Quint toolchain, so only changes to those need it. The weekly run on `main` is Full with - exploration. +- **Mutations:** Replay plus the TypeScript, Go and Rust mutation campaigns (`-f mode=mutations`), + which plant catalogued bugs in a port and require its tests to catch them; about 50 minutes. +- **Full:** Mutations plus the Quint model checks and the model-fault campaign (`-f mode=full`), + which plants bugs in the models and requires an invariant to catch each one; about two and a + half hours. The campaign reads only the models, the challenge catalog and the Quint toolchain, + so a change confined to the ports or their replay drivers never needs it. `-f exploration=true` + adds a fresh-seed generation and replay in an isolated copy of the source; a move needs it, and + the weekly run on `main` includes it. - **Mutant rule:** it fires when a change edits a file that an entry in `formal/catalogs/mutations.json` or `rust-mutations.json` names, or edits those catalogs. PR CI matches only the `before` anchors; only the mutation lanes compile and measure each mutant. @@ -185,7 +188,7 @@ the one the ruleset requires. `vX.Y.Z` tag ([Releasing](docs/maintainers.md#releasing)), so agents never edit version files or use the `release` title type. When asked for a release, report the version that `git log --format=%s ..origin/main` implies, any mismatch with the version requested, and - whether current `main` has a green full run ([Validation](docs/maintainers.md#validation)), then + whether current `main` has a green Full run ([Validation](docs/maintainers.md#validation)), then stop. Dispatching `Release` and merging the `release:` PR it opens are separate irreversible actions. @@ -193,8 +196,8 @@ the one the ruleset requires. Classify the PR with the table, then check its head commit against every step of each matching path, Critical behavior and the Finish list. A conflict with `main` needs a rebase, and the rebased -head needs the tier's run again unless an earlier green run covers it. Report findings in the -session; post them on GitHub, as a comment review, only when asked. +head needs the tier's run again. Report findings in the session; post them on GitHub, as a comment +review, only when asked. ### Refresh pinned ledgers @@ -209,13 +212,14 @@ of them is edited by hand. ### Validate the head commit -- A result counts only for its commit. Dispatch the tier the type needs once, on the final - candidate: after review comments are addressed and PR CI is green. Before that, iterate with - PR CI and local lanes (`make formal-`, `make mutations- MUTATION_ONLY=`), which - never replace it. A green run on an earlier commit still covers the head when PR CI passes on - the head and the diff between them touches only prose, design records or ledger pins; any other - push, a rebase included, needs a new run. If a run is still in progress when the turn ends, - leave the PR in draft and give the run ID, its commit and its state in the final message. +- A result counts for its commit. Dispatch the tier the type needs once, on the final candidate: + after review comments are addressed and PR CI is green. Before that, iterate with PR CI and + local lanes (`make formal-`, `make mutations- MUTATION_ONLY=`), which never + replace it. A green run on an earlier commit also covers the head when PR CI passes on the head + and the diff between them touches only Markdown files, design records included, or ledger pins. + Any other push, a rebase included, needs a new run; a comment edit in port source is source. If + a run is still in progress when the turn ends, leave the PR in draft and give the run ID, its + commit and its state in the final message. - Run each check as its own command and read its exit status, since `| tail` or `|| true` hides failures. Never chain a commit or push behind a check. - Before calling a failure a flake, compare the lane's latest `main` run. Report a red `main` diff --git a/DEVELOPMENT_PROCESS.md b/DEVELOPMENT_PROCESS.md index 00f983a4..c4f40609 100644 --- a/DEVELOPMENT_PROCESS.md +++ b/DEVELOPMENT_PROCESS.md @@ -74,8 +74,8 @@ asks in its session if he is present. Otherwise it pushes its work as a draft pu the open questions in the description and stops. A pull request is ready for review when every step of its type is done, any design record is -current, the required validation has passed on the head commit and no questions remain open. Until -then it stays a draft. +current, the required validation has passed on the head commit or on an earlier commit that covers +it, and no questions remain open. Until then it stays a draft. ## How much validation a change needs @@ -93,21 +93,22 @@ type needs once, on the final candidate. skip generation. This is the tier for behavior and API changes in the ports, and for new Quint regressions, whose histories join the corpus. - **Mutations** adds the TypeScript, Go and Rust mutation campaigns, which plant known bugs in a - port and require its tests to catch them, in about 50 minutes. A change that edits code a - catalogued mutant targets needs it. + port and require its tests to catch them, in about 50 minutes. A change that edits a file a + catalogued mutant rewrites, or a mutant catalog itself, needs it. - **Full** adds the Quint model checks and the model-fault campaign, which plants bugs in the models themselves and requires an invariant to catch each one, in about two and a half hours. - The campaign reads only the models, the challenge catalog and the Quint toolchain, so only - changes to those need it. -- The weekly run on `main` is Full with **exploration**: it also generates histories from a fresh - random seed in an isolated copy of the source, which catches problems the fixed seeds miss. - -A result counts only for the commit it ran on. A green run still covers a later commit when PR CI -passes there and the difference is only prose, design records or ledger pins; any other push, a -rebase included, needs a new run. GitHub requires only the `test` check and one approval, and the -maintainer merges through an admin bypass, so nothing on GitHub blocks a merge with a red check. -The process does: a pull request stays in draft until the tier its type requires has passed on -its head commit. + The campaign reads only the models, the challenge catalog and the Quint toolchain, so a change + confined to the ports or their replay drivers never needs it. +- **Full with exploration** also generates histories from a fresh random seed in an isolated copy + of the source, which catches problems the fixed seeds miss. A layout move needs it, and the + weekly run on `main` uses it. + +A result counts for the commit it ran on. A green run also covers a later commit when PR CI passes +there and the difference is only Markdown files, design records included, or ledger pins; any +other push, a rebase included, needs a new run. GitHub requires only the `test` check and one +approval, and the maintainer merges through an admin bypass, so nothing on GitHub blocks a merge +with a red check. The process does: a pull request stays in draft until the tier its type requires +has passed on its head commit or on an earlier commit that covers it. **Ledgers** in `formal/catalogs/` record the hash at which each reviewed file was last read: every docs page, the formal guides, several READMEs and selected tests and sources. Editing a pinned file @@ -121,9 +122,9 @@ happened. | --- | --- | --- | --- | | Portable behavior | A new cache operation that every port offers | Required | Full | | Bug fix | Go serves a value the contract says is stale | Only when it reverses a decision | Replay | -| Public API | Exporting an existing type from one port | When every port mirrors it, or it changes how callers construct the cache or call its operations | PR CI | +| Public API | Exporting an existing type from one port | When every port mirrors it, or it changes how callers construct the cache or call its operations | Replay | | Docs | Correcting a default in a guide | None | PR CI | -| Refactor or move | Splitting a module without changing behavior | None | PR CI | +| Refactor or move | Reorganizing the documentation tooling | None | PR CI | | Formal infrastructure | Changing the replay protocol | When it changes how conformance is established | Full | | Tooling | Upgrading a dependency | None | PR CI | | New port | A fifth language | Required | Full | @@ -134,9 +135,10 @@ case takes the stricter type. Any change that reverses an earlier decision needs that decision lives in a record, an issue or a pull request. Some changes need more than the table's minimum. Touching port source or the replay code that -drives it needs Replay. Editing code a catalogued mutant targets needs Mutations. Changing a Quint -transition or invariant, a toolchain pin or the repository layout needs Full. AGENTS.md states the -exact conditions and the steps for each type. +drives it needs Replay. Editing a file a catalogued mutant rewrites, or a mutant catalog, needs +Mutations. Changing a Quint transition, invariant or challenge, or a toolchain pin, needs Full; a +layout move needs Full with exploration. AGENTS.md states the exact conditions and the steps for +each type. ## Design records diff --git a/docs/maintainers.md b/docs/maintainers.md index fd65a3da..63f8b180 100644 --- a/docs/maintainers.md +++ b/docs/maintainers.md @@ -48,11 +48,13 @@ and weekly formal workflow, using the same Make targets as local runs. Its `mode` input selects `replay` (the generated corpus in every port, about 15 minutes), `mutations` (plus the port mutation campaigns, about 50 minutes) or `full` (plus the model checks and the model-fault campaign, about two and a -half hours). Before merge, run `replay` or `mutations` for changes to port -behavior or replay tooling and `full` for changes to the models, the kernel -library or the Quint toolchain; run `full` before a release or before accepting -another port. A scheduled result applies to its recorded revision; it does not -validate a later PR head. A smoke pass does not establish full conformance. +half hours). Before merge, run `replay` for changes to port behavior or a +replay driver, and `mutations` when the change also edits a file a catalogued +mutant rewrites. Run `full` for changes to a model's transitions, invariants +or challenges, the kernel library, `formal/tools/` or the Quint toolchain, and +before a release or before accepting another port. A scheduled result applies +to its recorded revision; it does not validate a later PR head. A smoke pass +does not establish full conformance. CI uses Node.js 24 for development and integration, then validates the packed package and zstd at the exact 22.x consumer floor, Node.js 22.15.0. The published diff --git a/formal/catalogs/go-parity.json b/formal/catalogs/go-parity.json index 637fc1d6..776c8e67 100644 --- a/formal/catalogs/go-parity.json +++ b/formal/catalogs/go-parity.json @@ -10,7 +10,7 @@ "inputs": { "semanticCasesSha256": "f5f7ee357201b343eb00f8f9c783c92af0d722709137edc0f55e0a52b3cdec0a", "executionSha256": "29a412f87329347840f000ea44a6e95332464c0b01b92b4e41c615af3c9157cd", - "sourceAuditSha256": "9a193c8a6ad25c23b9275f50b7b9ae276aa78d013db30d48d1eb509c53cb0439", + "sourceAuditSha256": "f5232ffb7e6763c92144b58010a8c79f203d6c60eedd565742c7f4aed5e112bb", "featureCoverageSha256": "2d4e47ec18688c911ce4d6bda780edc8ee654069aa5704e15a39cbae35655ba7", "coverageWitnessesSha256": "2b2d5d57daacba3ecd3637f5a917d58b0b63fcc88893e651cd602cdba1ef4244", "profilesSha256": "9df8285820e4fff65f6a7753885bbb192c09f3f476eac8f9c98d130454ae1a28" diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index 96b44bff..530a32e2 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -217,21 +217,21 @@ }, { "path": "docs/maintainers.md", - "sha256": "21fa658dd78a49dd840183443708d95b8c2db08d567a39bb2d39be22e4d01983", + "sha256": "23c819b75f1ef6399e60e0918daa67b78986117b51139cff484a4121a60fad17", "entries": [ {"line":1,"title":"Maintainer guide","contracts":["B01"]}, {"line":8,"title":"Validation","contracts":["B01"]}, - {"line":68,"title":"Maintaining the reference","contracts":["E05","B01"]}, - {"line":114,"title":"Run the documentation site","contracts":["B01"]}, - {"line":141,"title":"Publish to GitHub Pages","contracts":["B01"]}, - {"line":157,"title":"Cache-path benchmark","contracts":["X02"]}, - {"line":179,"title":"Redis write benchmark","contracts":["X02"]}, - {"line":202,"title":"Stale-on-error benchmark","contracts":["X02"]}, - {"line":230,"title":"Releasing","contracts":["B01","E05"]}, - {"line":312,"title":"Set up crates.io publishing once","contracts":["B01","E05"]}, - {"line":340,"title":"Retry a Rust publication","contracts":["B01","E05"]}, - {"line":354,"title":"Set up PyPI publishing once","contracts":["B01","E05"]}, - {"line":375,"title":"Retry a Python publication","contracts":["B01","E05"]} + {"line":70,"title":"Maintaining the reference","contracts":["E05","B01"]}, + {"line":116,"title":"Run the documentation site","contracts":["B01"]}, + {"line":143,"title":"Publish to GitHub Pages","contracts":["B01"]}, + {"line":159,"title":"Cache-path benchmark","contracts":["X02"]}, + {"line":181,"title":"Redis write benchmark","contracts":["X02"]}, + {"line":204,"title":"Stale-on-error benchmark","contracts":["X02"]}, + {"line":232,"title":"Releasing","contracts":["B01","E05"]}, + {"line":314,"title":"Set up crates.io publishing once","contracts":["B01","E05"]}, + {"line":342,"title":"Retry a Rust publication","contracts":["B01","E05"]}, + {"line":356,"title":"Set up PyPI publishing once","contracts":["B01","E05"]}, + {"line":377,"title":"Retry a Python publication","contracts":["B01","E05"]} ] }, { @@ -1102,20 +1102,20 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "8e23cd5252a5d7eb8a8e42cab301345f0c6ffa055994566076c45c979da5c8f0", + "sha256": "dd038422dbca646a4357655d1f9d0bfd02627af635e2bbe3c2a13821d4c18788", "entries": [ {"line":1,"title":"Reading and extending the DialCache models"}, {"line":20,"title":"Reading a model"}, {"line":61,"title":"Writing conventions"}, {"line":172,"title":"Codifying the next behavior"}, - {"line":234,"title":"Give reviewers focused context"}, - {"line":249,"title":"Exporting a deterministic regression"}, - {"line":287,"title":"Maintaining case and witness evidence"}, - {"line":340,"title":"Reproducible committed fixtures"}, - {"line":350,"title":"Refactoring and execution"}, - {"line":378,"title":"Challenging every model"}, - {"line":459,"title":"Mapping every challenge to native mutants"}, - {"line":590,"title":"Exported runs are exactly the public-only runs"} + {"line":235,"title":"Give reviewers focused context"}, + {"line":250,"title":"Exporting a deterministic regression"}, + {"line":288,"title":"Maintaining case and witness evidence"}, + {"line":341,"title":"Reproducible committed fixtures"}, + {"line":351,"title":"Refactoring and execution"}, + {"line":379,"title":"Challenging every model"}, + {"line":460,"title":"Mapping every challenge to native mutants"}, + {"line":591,"title":"Exported runs are exactly the public-only runs"} ], "review": { "kind": "tooling-guide", @@ -1597,15 +1597,15 @@ }, { "path": "formal/guides/VALIDATION.md", - "sha256": "c9ed44c82472820692190c26e65e261ff1af9bc2ab49b8abef9f9ac79104f304", + "sha256": "da1f37d14c8064335cd6c893a38ee7abdbcbfe91ae379724be17ba27b3e4adfc", "entries": [ {"line":1,"title":"Validation and evidence"}, {"line":7,"title":"Choosing a run"}, - {"line":91,"title":"Reading a completion report"}, - {"line":110,"title":"Mutation evidence"}, - {"line":224,"title":"Exploratory runs"}, - {"line":280,"title":"A retained sampling regression"}, - {"line":317,"title":"Historical results"} + {"line":94,"title":"Reading a completion report"}, + {"line":113,"title":"Mutation evidence"}, + {"line":227,"title":"Exploratory runs"}, + {"line":283,"title":"A retained sampling regression"}, + {"line":320,"title":"Historical results"} ], "review": { "kind": "tooling-guide", diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index c42acaa8..7a480bd4 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -219,7 +219,8 @@ Every supported implementation replays the registered profiles. Each port's completion gate requires every scheduled history, fixed case, protocol case and witness gate to finish successfully. Passing TypeScript replay alone does not establish another port's conformance. Behavior, model and replay changes require -[full validation](./VALIDATION.md#choosing-a-run) before merge. +hosted validation before merge at the tier +[VALIDATION.md](./VALIDATION.md#choosing-a-run) assigns. Fault-detection evidence is specific to each port. Rust uses [its own mutation catalog](./SEMANTIC-COVERAGE.md#reproduction-and-ci); the diff --git a/formal/guides/VALIDATION.md b/formal/guides/VALIDATION.md index d62931a9..e432a4e2 100644 --- a/formal/guides/VALIDATION.md +++ b/formal/guides/VALIDATION.md @@ -69,24 +69,27 @@ challenge report are identical for any worker count. A behavior, model or replay change requires hosted validation of its current inputs before merge, at the tier those inputs need. The manual workflow, `formal-full.yaml`, takes a `mode` input, and each mode adds to the previous -one: `replay` generates the corpus and completes every port replay (about 15 -minutes); `mutations` adds the TypeScript, Go and Rust mutation campaigns -(about 50 minutes); `full`, the default, adds `check-models` with the -model-fault campaign (about two and a half hours). Port, replay-driver and -regression-only changes need `replay` or `mutations`. A change to a model's -transitions or invariants, the kernel library, the challenge catalog or the -Quint toolchain needs `full`, because those are the only inputs the campaign -reads. The `generate` job restores the corpus from a cache keyed on every -generation input (the models, `formal/replay/`, `formal/tools/`, the catalogs -other than the review ledgers, the committed fixtures and the Quint pin), so -an unchanged specification is not regenerated; any change to those inputs -misses the cache and regenerates. The default PR workflow runs faster checks; -it does not enforce this requirement. The weekly run validates the selected -`main` revision in `full` mode and includes exploration; a manual run can -enable the `exploration` option. The aggregate gate requires exploration when -selected or scheduled, requires each lane the mode selects, and requires the -other lanes to have been skipped. Each PR body should identify the revision, -the mode and the run. +one. `replay` generates the corpus and completes every port replay, about 15 +minutes. `mutations` adds the TypeScript, Go and Rust mutation campaigns, +about 50 minutes. `full`, the default, adds `check-models` with the +model-fault campaign, about two and a half hours. Port, replay-driver and +regression-only changes need `replay`, or `mutations` when they edit a file a +catalogued mutant rewrites. A change to a model's transitions, invariants or +challenges, the kernel library or the Quint toolchain needs `full`, because +those are the only inputs the campaign reads. The `generate` job restores the +corpus from a cache keyed on every generation input: the models, +`formal/replay/`, `formal/tools/`, `formal/generated/`, the catalogs other +than the three review ledgers, the committed fixtures, the Quint pin, the +`Makefile` and the package manifests. An entry is saved under the branch that +generated it and is visible to that branch and, from `main`, to every branch, +until seven days pass without a restore. A run whose inputs match such an +entry skips generation; any other run, and every weekly run, regenerates. The +default PR workflow runs faster checks; it does not enforce this requirement. +The weekly run validates the selected `main` revision in `full` mode and +includes exploration; a manual run can enable the `exploration` option. The +aggregate gate requires exploration when selected or scheduled, requires each +lane the mode selects, and requires the other lanes to have been skipped. Each +PR body should identify the revision, the mode and the run. ## Reading a completion report diff --git a/typescript/test/formal-validation.test.ts b/typescript/test/formal-validation.test.ts index 147efe25..088efef9 100644 --- a/typescript/test/formal-validation.test.ts +++ b/typescript/test/formal-validation.test.ts @@ -473,7 +473,7 @@ else { }); describe("full formal workflow shape", () => { - type Step = { name?: string; run?: string; uses?: string; if?: string; env?: Record; with?: Record }; + type Step = { name?: string; id?: string; run?: string; uses?: string; if?: string; env?: Record; with?: Record }; type Job = { needs?: string | string[]; if?: string; env?: Record; strategy?: { "fail-fast"?: boolean; matrix?: Record }; "timeout-minutes"?: number; steps: Step[] }; const lanes = ["typescript-parity", "go-parity", "rust-parity", "python-parity", "typescript-mutations", "go-mutations", "rust-mutations"]; const needsOf = (job: Job) => (job.needs === undefined ? [] : [job.needs].flat()); @@ -628,32 +628,37 @@ describe("full formal workflow shape", () => { expect(jobs["check-models"]!.if).toBe("(github.event_name != 'schedule' || github.ref == 'refs/heads/main') && inputs.mode != 'replay' && inputs.mode != 'mutations'"); for (const lane of ["typescript-mutations", "go-mutations", "rust-mutations"]) expect(jobs[lane]!.if, lane).toBe("inputs.mode != 'replay'"); for (const lane of ["typescript-parity", "go-parity", "rust-parity", "python-parity", "symbolic", "generate"]) expect(jobs[lane]!.if ?? "", lane).not.toMatch(/inputs\.mode/); - // The cache key must name every input generation reads and only an exact key may restore, - // so a corpus from different models can never stand in for a regenerated one. + // The cache key is pinned whole: an added exclusion or a non-hashFiles component would let + // a stale corpus restore or stop the cache hitting, and both must be a deliberate edit here. const steps = jobs.generate!.steps; const restore = steps.find(step => step.uses?.startsWith("actions/cache/restore@"))!; const save = steps.find(step => step.uses?.startsWith("actions/cache/save@"))!; - expect(restore.with).toMatchObject({ path: ".formal-traces" }); - expect(restore.with).not.toHaveProperty("restore-keys"); - const key = String(restore.with!.key); - for (const input of ["formal/models/**", "formal/replay/**", "formal/tools/**", "formal/generated/**", "formal/catalogs/**", "typescript/test/fixtures/**", ".github/actions/setup-quint/**", "Makefile", "pnpm-lock.yaml"]) expect(key, input).toContain(`'${input}'`); - for (const ledger of ["source-audit", "go-parity", "feature-coverage"]) expect(key, ledger).toContain(`'!formal/catalogs/${ledger}.json'`); + expect(restore.id).toBe("corpus"); + expect(restore.with).toEqual({ path: ".formal-traces", key: "formal-traces-$" + "{{ hashFiles('formal/models/**', 'formal/replay/**', 'formal/tools/**', 'formal/generated/**', 'formal/catalogs/**', '!formal/catalogs/source-audit.json', '!formal/catalogs/go-parity.json', '!formal/catalogs/feature-coverage.json', 'typescript/test/fixtures/**', '.github/actions/setup-quint/**', 'Makefile', 'package.json', 'pnpm-lock.yaml') }}" }); const generate = steps.find(step => step.run === "make formal-generate")!; - expect(generate.if).toBe("steps.corpus.outputs.cache-hit != 'true'"); + // The weekly run regenerates on a hit so a fresh toolchain re-exports the committed artifacts. + expect(generate.if).toBe("steps.corpus.outputs.cache-hit != 'true' || github.event_name == 'schedule'"); expect(save.if).toBe("steps.corpus.outputs.cache-hit != 'true'"); expect(save.with).toMatchObject({ path: ".formal-traces", key: "$" + "{{ steps.corpus.outputs.cache-primary-key }}" }); expect(steps.indexOf(restore)).toBeLessThan(steps.indexOf(generate)); expect(steps.indexOf(generate)).toBeLessThan(steps.indexOf(save)); // Every mode requires the corpus and the four replays; a lane a mode does not select must - // report skipped, so a dispatch cannot pass as a stronger mode than it ran. + // report skipped, so a dispatch cannot pass as a stronger mode than it ran. The gate is + // pinned line for line, so a loosened test (an alternation, `|| true`) fails here as a + // flipped one does. const gate = jobs["formal-full"]!.steps.find(step => step.run?.includes("_RESULT"))!; expect(gate.env).toMatchObject({ MODE: "$" + "{{ inputs.mode || 'full' }}" }); - const branch = (mode: string) => gate.run!.slice(gate.run!.indexOf(`${mode})`), gate.run!.indexOf(";;", gate.run!.indexOf(`${mode})`))); - for (const mode of ["full", "mutations", "replay"]) for (const lane of ["CHECK_MODELS", "TYPESCRIPT_MUTATIONS_MERGE", "GO_MUTATIONS_MERGE", "RUST_MUTATIONS_MERGE"]) { - const expected = mode === "full" || (mode === "mutations" && lane !== "CHECK_MODELS") ? "success" : "skipped"; - expect(branch(mode), `${mode}: ${lane}`).toMatch(new RegExp(`test "\\$${lane}_RESULT" = ${expected}`)); - } - for (const lane of ["GENERATE", "TYPESCRIPT", "GO", "RUST", "PYTHON", "SYMBOLIC"]) expect(gate.run!.slice(0, gate.run!.indexOf("case "))).toMatch(new RegExp(`test "\\$${lane}_RESULT" = success`)); + const selected = ["CHECK_MODELS", "TYPESCRIPT_MUTATIONS_MERGE", "GO_MUTATIONS_MERGE", "RUST_MUTATIONS_MERGE"]; + const arm = (mode: string, results: string[], skipped: string) => [`${mode})`, ...selected.map((lane, i) => `test "$${lane}_RESULT" = ${results[i]}`), `skipped="${skipped}" ;;`]; + const lines = gate.run!.split("\n").map(line => line.trim()).filter(line => line && !line.startsWith("#")); + expect(lines.slice(0, lines.indexOf("esac") + 1)).toEqual([ + ...["GENERATE", "TYPESCRIPT", "GO", "RUST", "PYTHON", "SYMBOLIC"].map(lane => `test "$${lane}_RESULT" = success`), + 'case "$MODE" in', + ...arm("full", ["success", "success", "success", "success"], "none"), + ...arm("mutations", ["skipped", "success", "success", "success"], "model checks and the model-fault campaign"), + ...arm("replay", ["skipped", "skipped", "skipped", "skipped"], "model checks, the model-fault campaign and the port mutation campaigns"), + "*)", 'echo "Unknown mode: $MODE" >&2', "exit 1 ;;", "esac", + ]); }); it("runs the differential on pull requests only, against the base branch, with the replay logs preserved", async () => { From 788142a3c5b43f46f5a2906b7693b667c4d638c6 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Thu, 15 Oct 2026 01:03:29 -0700 Subject: [PATCH 6/6] docs: point the process at the contract lookup command #236 added formal/tools/where.mjs, which prints where one contract is stated, tested, challenged and mapped. That is the navigation the Bug fix path and the formal convention in AGENTS.md asked agents to assemble by hand, so both name the command, and DEVELOPMENT_PROCESS.md lists it under Where to look. --- AGENTS.md | 9 ++++++--- DEVELOPMENT_PROCESS.md | 1 + 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 0e75fa1f..80af0c54 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -112,8 +112,9 @@ the one the ruleset requires. #### Bug fix -1. Search records, issues and pull requests for the contract IDs. A fix that reverses a recorded - decision needs a record, so stop at the design gate. +1. Search records, issues and pull requests for the contract IDs, and run + `node formal/tools/where.mjs ` for each. A fix that reverses a recorded decision needs a + record, so stop at the design gate. 2. Write a regression that fails before the fix. When a `CONTRACTS.md` obligation covers the behavior, export a Quint regression even if only one port has the fault ([Exporting a deterministic regression](formal/guides/AUTHORING.md#exporting-a-deterministic-regression)); @@ -287,7 +288,9 @@ The PR leaves draft only when all of these hold; the maintainer then reviews and - Use `corepack pnpm`, and run `make` and pnpm commands from the repository root. Keep npm package paths and exports independent of the repository's `typescript/` prefix. - Start formal work at `formal/README.md`; `formal/guides/WALKTHROUGH.md` follows one contract - through every replay. Read the model and profile bindings before opening large generated JSON. + through every replay, and `node formal/tools/where.mjs C45` prints where one contract is stated, + tested, challenged and mapped. Read the model and profile bindings before opening large + generated JSON. - `DEVELOPMENT_PROCESS.md` explains this process to human readers. A change to "Make a change" updates it in the same PR. diff --git a/DEVELOPMENT_PROCESS.md b/DEVELOPMENT_PROCESS.md index c4f40609..262c6988 100644 --- a/DEVELOPMENT_PROCESS.md +++ b/DEVELOPMENT_PROCESS.md @@ -235,6 +235,7 @@ creates the GitHub release and tags the Go module. The steps are in | Follow the exact steps and commands | [AGENTS.md](AGENTS.md) | | Write or find a design record | [design/README.md](design/README.md) | | Understand the specification | [formal/README.md](formal/README.md) and [SPEC.md](formal/guides/SPEC.md) | +| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` | | Change a contract or a Quint model | [AUTHORING.md](formal/guides/AUTHORING.md) | | Write user documentation | [docs/authoring.md](docs/authoring.md) | | Choose a validation run and read its report | [VALIDATION.md](formal/guides/VALIDATION.md) |