diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md new file mode 100644 index 00000000..bb049849 --- /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 and its mode} 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/.github/workflows/formal-full.yaml b/.github/workflows/formal-full.yaml index 5f752d1b..51a6103e 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 @@ -13,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: @@ -51,7 +66,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 +110,33 @@ 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 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' || 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' + 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 +209,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 +372,7 @@ jobs: # the matrix grows. go-mutations: needs: generate + if: inputs.mode != 'replay' runs-on: ubuntu-latest strategy: fail-fast: false @@ -391,6 +435,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 +577,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 +593,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 f0430743..80af0c54 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,53 +1,259 @@ # 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 -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 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, 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 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 | +| 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. +- **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, 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`), + 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. +- **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, 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)); + 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 the tier's run again. 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 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` + 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 + `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 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. ## Critical behavior @@ -67,63 +273,40 @@ 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). -- 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, 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. + +## 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/DEVELOPMENT_PROCESS.md b/DEVELOPMENT_PROCESS.md new file mode 100644 index 00000000..262c6988 --- /dev/null +++ b/DEVELOPMENT_PROCESS.md @@ -0,0 +1,243 @@ +# 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 the formal tier
the type needs"] + 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 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 + +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`. +- **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 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 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 +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 | 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 | Replay | +| Docs | Correcting a default in a guide | 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 | +| 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 port source or the replay code that +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 + +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 formal tier + G-->>A: PR CI and the tier 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 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) | +| 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) | +| 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/design/README.md b/design/README.md new file mode 100644 index 00000000..5b74f6fc --- /dev/null +++ b/design/README.md @@ -0,0 +1,133 @@ +# 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, 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 + 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 pull + request description, which becomes the squash commit's 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 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 +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 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. 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 + +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 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 + 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`, 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 + 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..2b78abd3 --- /dev/null +++ b/design/TEMPLATE.md @@ -0,0 +1,70 @@ + + +# {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. 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 + +{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. 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 +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/docs/maintainers.md b/docs/maintainers.md index 6c4a1d74..63f8b180 100644 --- a/docs/maintainers.md +++ b/docs/maintainers.md @@ -43,10 +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 +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` 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. diff --git a/formal/catalogs/README.md b/formal/catalogs/README.md index 8c6d5127..c0ecc4b8 100644 --- a/formal/catalogs/README.md +++ b/formal/catalogs/README.md @@ -32,3 +32,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, five catalogs (`semantic-cases`, `execution`, `feature-coverage`, + `coverage-witnesses` and `profiles`) and the source audit's dispositions, not + its bytes, so a prose-only edit never reaches it. +- 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`.** Re-key each reviewed file by name: + `node formal/tools/check-source-audit.mjs --refresh ...`. It recomputes + the hash and the heading or test inventory and carries each disposition to + the entry with the same title; a new or renamed entry stays empty until a + reviewer fills it ([TEST-AUDIT.md](../guides/TEST-AUDIT.md#keeping-the-audit-current)). +4. **`feature-coverage.json`.** Update a reviewed test's `sha256` by hand, then + run `node formal/tools/check-feature-coverage.mjs`. +5. **`go-parity.json`, last.** Run `node formal/tools/check-go-parity.mjs --refresh-inputs` + to re-pin the catalog digests, the audit dispositions and the vector + artifacts. The `typescript/src/` and bound Go file hashes are re-pinned by + hand with their mapping review; a new documentation page or ordinary test + file needs a Go applicability row, and a new `typescript/src/` file needs a + source inventory row ([GO-PARITY.md](../guides/GO-PARITY.md)). + +`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/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index 9ea9b436..4021eb1d 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -217,7 +217,7 @@ }, { "path": "docs/maintainers.md", - "sha256": "836a026530b6773e06aa461a29891fe8c6d2578360f5678702e8d7374d2deb09", + "sha256": "23c819b75f1ef6399e60e0918daa67b78986117b51139cff484a4121a60fad17", "entries": [ {"title":"Maintainer guide","contracts":["B01"]}, {"title":"Validation","contracts":["B01"]}, @@ -1102,7 +1102,7 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "46ea31d30b5cfebfa6163dfad1ad33b770148bf147329bb5c0a93271d4806962", + "sha256": "97e42e308d046dd1021d8adfd643e50a94d00c28a5552a25693eafff68da7394", "entries": [ {"title":"Reading and extending the DialCache models"}, {"title":"Reading a model"}, @@ -1689,7 +1689,7 @@ }, { "path": "formal/guides/VALIDATION.md", - "sha256": "20132bd3ea23510eef25022fec91482fd09bf24f0a285f72aa018d69a69bd154", + "sha256": "db335e1c3bc6981d33f136afa5dce31ac0ed4ea08b2593248a3962e88bb920c2", "entries": [ {"title":"Validation and evidence"}, {"title":"Choosing a run"}, diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index d8b93cf7..3b961669 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -244,7 +244,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 a9be8907..c4e6ff14 100644 --- a/formal/guides/VALIDATION.md +++ b/formal/guides/VALIDATION.md @@ -21,7 +21,8 @@ at the revisions they were made, are in [HISTORY.md](./HISTORY.md). `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/`; @@ -66,14 +67,30 @@ 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` 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/scripts/check-docs.mjs b/scripts/check-docs.mjs index d26a79e5..20da4b44 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 -// 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, 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', '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, ''); diff --git a/scripts/check-docs.test.mjs b/scripts/check-docs.test.mjs index 8f35c1f1..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 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 }); @@ -101,4 +101,15 @@ 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/); + 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/); }); diff --git a/typescript/test/formal-validation.test.ts b/typescript/test/formal-validation.test.ts index 5fb643de..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()); @@ -616,6 +616,51 @@ 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 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.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")!; + // 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. 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 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 () => { 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 } };