diff --git a/docs/maintainers.md b/docs/maintainers.md index 6c4a1d74..23cc628b 100644 --- a/docs/maintainers.md +++ b/docs/maintainers.md @@ -38,7 +38,7 @@ on a port's replay report. Each port's mutation catalog defines its measured sco `make ci NODE22_BIN=/path/to/node22/bin/node` runs the complete pipeline, including integrations, mutations and the exact Node 22.15.0 package floor. See the repository's -[formal guide](https://github.com/lan17/DialCache/blob/main/formal/README.md#generating-and-replaying-behavior) +[formal guide](https://github.com/lan17/DialCache/blob/main/formal/README.md#run-it) for setup, reports and single-history reproduction. Pull requests run fast native/smoke checks and real integrations. Changes to diff --git a/formal/README.md b/formal/README.md index f445cb1a..6bf6b772 100644 --- a/formal/README.md +++ b/formal/README.md @@ -1,21 +1,29 @@ # Executable DialCache specification -Quint defines the portable contracts that TypeScript, Go, Rust and future ports -must preserve. TypeScript is the executable reference those contracts formalize; a -disagreement between the two is settled by a distinguishing [regression](./guides/GLOSSARY.md#corpus-history-regression-exported-run-and-public-only-run) and a -recorded decision, not by editing the easier side. Native [drivers](./guides/GLOSSARY.md#driver) execute -external commands against the real libraries; generated expectations stay in -the test [coordinator](./guides/GLOSSARY.md#coordinator). +DialCache's portable behavior is defined once, in Quint, and every language port +is held to the same generated histories. TypeScript is the executable reference +the models formalize; when the two disagree, the resolution is a distinguishing +[regression](./guides/GLOSSARY.md#corpus-history-regression-exported-run-and-public-only-run) +and a recorded decision, never an edit to whichever side is easier. Native +[drivers](./guides/GLOSSARY.md#driver) execute external commands against the +real libraries, and the expectations stay in the shared +[coordinator](./guides/GLOSSARY.md#coordinator), so no port can pass by +consulting its own predictions. + +This page explains the setup from the models down to the CI lanes, then lists +where everything lives. [guides/README.md](./guides/README.md) indexes the prose +by kind and [GLOSSARY.md](./guides/GLOSSARY.md) defines the terms. ## Start with your task | Task | Read first | | --- | --- | -| Understand system behavior | [SPEC.md](./guides/SPEC.md), then the relevant model below | -| Follow one rule into all three implementations | [WALKTHROUGH.md](./guides/WALKTHROUGH.md) | +| See how the pieces fit together | [The setup, top to bottom](#the-setup-top-to-bottom), then [WALKTHROUGH.md](./guides/WALKTHROUGH.md) | +| Understand system behavior | [SPEC.md](./guides/SPEC.md), then the relevant model in [models/README.md](./models/README.md) | +| Follow one rule into every implementation | [WALKTHROUGH.md](./guides/WALKTHROUGH.md) | | Change a behavior or extend coverage | [AUTHORING.md](./guides/AUTHORING.md) | | Implement another language | [PORTING.md](./guides/PORTING.md) and [PROTOCOL.md](./guides/PROTOCOL.md) | -| Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and the commands below | +| Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and [Run it](#run-it) | | See where one contract is stated, tested, challenged and mapped, or read one challenge or mutant in full | `node formal/tools/where.mjs C45` (or `C45.recheck-after-decode`, `B01.registration-and-policy-snapshot`, `recovery-inclusive-maximum`, `M01`) | | Interpret validation results | [VALIDATION.md](./guides/VALIDATION.md) | | Look up a term | [GLOSSARY.md](./guides/GLOSSARY.md) | @@ -25,6 +33,245 @@ and generated artifacts; a reader should not need to open them to learn a rule. [CONTRACTS.md](./guides/CONTRACTS.md) gives stable obligation IDs and [FEATURE-COVERAGE.md](./guides/FEATURE-COVERAGE.md) organizes their boundary cases. +## The setup, top to bottom + +Six stages turn a rule into evidence. Each stage below names its directory, its +tool, what it produces and where to read more. The diagram summarizes the same +flow: yellow boxes are written by hand, blue boxes are the tools, green boxes +are what they produce, and the numbers are the stages below. + +```mermaid +flowchart LR + M["Quint models
models/"]:::hand + X["Manifests and catalogs
catalogs/"]:::hand + D["Native drivers
typescript/ go/ rust/ python/"]:::hand + RM["2. Check
run-models.mjs"]:::tool + GA["3. Generate
generate-artifacts.mjs, witnesses.mjs"]:::tool + CO["4. Replay
replay/coordinator.mjs"]:::tool + CK["5. Account, 6. Gate
measure-*.mjs, check-*.mjs"]:::tool + CP["Corpus and regressions
.formal-traces/"]:::out + GF["Committed artifacts
generated/"]:::out + RP["Completion, witness
and mutation reports"]:::out + M --> RM --> CP --> CO + M --> GA --> GF --> CO + X --> RM + X --> GA + CO <--> D + CO --> RP --> CK + X --> CK + classDef hand fill:#fff7d6,stroke:#b59b00,color:#1f2328 + classDef tool fill:#e3f0ff,stroke:#2b6cb0,color:#1f2328 + classDef out fill:#e8f7ea,stroke:#2f855a,color:#1f2328 +``` + +### 1. State the rule in Quint + +[cache-rules.qnt](./models/cache-rules.qnt) holds the shared +[judgments](./guides/GLOSSARY.md#judgment-judged-once-and-applied-from-a-judgment) +every model imports: age, expiry, deadline and fence. The +[kernel library](./models/kernel/README.md) states the portable rules as pure +transitions over named shapes, one concern per module. A composed +[profile](./guides/GLOSSARY.md#profile-conformance-profile) assigns state only +through those transitions, exposes its external commands as public actions, and +records each step's command and choices in an explicit input, so replay never +infers a command from changed cache state. Sixteen of the seventeen conformance +profiles compose the kernel; the introductory core profile predates it. Beside +them sit the sum-typed verification models that are model-checked, the +connection models that hold a profile's history against +[cache-contract.qnt](./models/cache-contract.qnt), and the wire models that each +generate one vector file. Properties stay independent: an assertion never calls +the helper it challenges, and each named `Test` run is a public-action +regression that pins one boundary. Protocol classifiers use the same fence +judgment as the generated byte vectors and the behavioral remote reads. + +Read more: [SPEC.md](./guides/SPEC.md) for the behavior, +[models/README.md](./models/README.md) for the file groups, +[kernel/README.md](./models/kernel/README.md) for the composition rules, +[AUTHORING.md](./guides/AUTHORING.md) to change a model. + +### 2. Check the models + +[execution.json](./catalogs/execution.json) schedules every model: its +invariants, bounds, trace paths and exported runs. `node +formal/tools/run-models.mjs check` typechecks each scheduled model, runs it with +the Rust evaluator and exports every public-only run of a profile model as a +regression; runs are discovered from the Quint source, never listed separately, +and a private state-patching run stays model-only unless it is rewritten as a +public action. `check-model-properties.mjs` runs the +[challenge](./guides/GLOSSARY.md#challenge-fault-mutant-and-reproducer) catalog +in the same manifest: for every scheduled model, at least one compiling +single-site fault that a named invariant must detect, with a deterministic +reproducer that fails only under the fault. `lint-profiles.mjs` ratchets the +composition and witness-isolation lint. Those three form the Quint evidence +[lane](./guides/GLOSSARY.md#lane), `make formal-check`. Two separate targets +read the models from another angle: `make model-check` verifies the finite +boundary rules in +[dialcache-rule-checks.qnt](./models/dialcache-rule-checks.qnt) symbolically +with Apalache, and the [differential](./guides/GLOSSARY.md#differential) replays +each composed profile's corpus against the merge base with `origin/main` in both +directions, so a change in observable behavior must be declared by bumping the +profile's `behaviorVersion`. A new profile has no previous text; it establishes +its behavior through independent properties, consequential witnesses and replay +in every port. + +Read more: [VALIDATION.md](./guides/VALIDATION.md) for what each run proves, +[CHALLENGES.md](./generated/CHALLENGES.md) for the challenge index, +[AUTHORING.md](./guides/AUTHORING.md#mapping-every-challenge-to-native-mutants) +for writing one. + +### 3. Generate the corpus and the committed artifacts + +`make formal-generate` writes the sampled corpus and the exported regressions +under `.formal-traces/`, which is never committed, then evaluates the required +[witness](./guides/GLOSSARY.md#witness-label-and-classifier) labels from +[coverage-witnesses.json](./catalogs/coverage-witnesses.json) over the complete +corpus with `witnesses.mjs`. That language-neutral step is the sole producer of +the witness evidence every port lane reads, and it fails generation when a +gated label's sampled hits fall below +[witness-baseline.json](./catalogs/witness-baseline.json). The committed +artifacts under [generated/](./generated/README.md) are rebuilt by +`node formal/tools/generate-artifacts.mjs --write`: one +[smoke](./guides/GLOSSARY.md#smoke) trace per profile from the recipes in +[fixture-recipes.json](./catalogs/fixture-recipes.json), the lock that pins the +input hashes of every model, recipe and generator beside the output hashes, the +four wire vector files, and the witness fixtures under +`typescript/test/fixtures/`. `make fixtures-check` recomputes them all with +pinned Quint and fails on any difference. The read views +[PROFILES.md](./generated/PROFILES.md), [CHALLENGES.md](./generated/CHALLENGES.md) +and [MUTANTS.md](./generated/MUTANTS.md) are rendered from the replay +descriptors and the catalogs by `generate-catalog-docs.mjs --write` and need no +Quint. + +Read more: [generated/README.md](./generated/README.md), +[catalogs/README.md](./catalogs/README.md), +[PORTING.md](./guides/PORTING.md#witness-evidence) for the witness evidence +fields. + +### 4. Replay every history in every port + +Each history is an [ITF](./guides/GLOSSARY.md#itf-informal-trace-format) +trace, the JSON trace format Quint writes. The +[coordinator](./replay/coordinator.mjs) runs it against a driver over the wire +protocol typed by +[protocol.schema.json](./replay/protocol.schema.json). It hands the driver the +fixture and each step's recorded external command, never the predicted +observation. The driver calls the real library, controls the external gates and +clocks, and reports actual results and effects. The coordinator validates each +observation, rejecting a malformed one as an infrastructure error before any +comparison, and asserts it against the model's prediction step by step. Profile +descriptors ([core.mjs](./replay/core.mjs), [effects.mjs](./replay/effects.mjs), +[features.mjs](./replay/features.mjs), +[local-clock.mjs](./replay/local-clock.mjs) and [profiles/](./replay/profiles/)) +decode each profile's integer choices into driver commands; +[PROFILES.md](./generated/PROFILES.md) is their rendered view and +[profiles.json](./catalogs/profiles.json) is the profile registry. The drivers +are [behavior-driver.ts](../typescript/test/formal/behavior-driver.ts), +[behavior_driver_test.go](../go/behavior_driver_test.go), +[driver.rs](../rust/tests/formal/driver.rs) and +[driver.py](../python/tests/formal/driver.py). `make smoke` replays the +committed traces in all four ports; `make formal-ts`, `make formal-go`, `make +formal-rust` and `make formal-python` replay the complete generated corpus and +write a completion report. + +Read more: [WALKTHROUGH.md](./guides/WALKTHROUGH.md) follows one history through +the ports, [PORTING.md](./guides/PORTING.md) is the driver contract with its +[observation contract](./guides/PORTING.md#observation-contract), +[replay/README.md](./replay/README.md) lists the modules, +[CONFORMANCE.md](./guides/CONFORMANCE.md) describes the core profile's trace +format and trust boundary. + +### 5. Account for the evidence + +`node formal/tools/conformance.mjs check` accepts a completion report only when +every scheduled case passed exactly once against the exact corpus and sources it +names. Witness coverage is required across the union of the named regressions +and the sampled corpus, so a corpus that stops reaching a corner is visible even +while the regressions keep the gate green. The mutation campaigns then challenge +the assertions themselves. [mutations.json](./catalogs/mutations.json) and +[rust-mutations.json](./catalogs/rust-mutations.json) catalog compiling semantic +faults in each port; `make mutations-ts`, `make mutations-go` and `make +mutations-rust` measure that the generated histories, the real-Redis +invalidation vectors and the shared witnesses detect every mapped mutant. Each +model challenge maps to the native mutant that injects the same wrong behavior, +and a mapped fault must violate its original property, fail the declared +expectation in a deterministic Quint run, and reach the same public assertion in +the completed TypeScript and Go recordings. Fixed corpora complement the +generated ones: [protocol-vectors.json](./catalogs/protocol-vectors.json), +[invalidation-vectors.json](./catalogs/invalidation-vectors.json) and +[behavioral-scenarios.json](./catalogs/behavioral-scenarios.json) carry +handwritten expectations, and their evidence mappings do not mechanically prove +that each fixed assertion agrees with Quint. +[semantic-cases.json](./catalogs/semantic-cases.json) and +[feature-coverage.json](./catalogs/feature-coverage.json) index every semantic +case and native feature family to its evidence; `where.mjs` answers from them. + +Read more: [SEMANTIC-COVERAGE.md](./guides/SEMANTIC-COVERAGE.md) for the +evidence inventory and the mutation comparison, +[FEATURE-COVERAGE.md](./guides/FEATURE-COVERAGE.md), +[TEST-MAP.md](./guides/TEST-MAP.md), [CONTRACTS.md](./guides/CONTRACTS.md) for +the obligation IDs, [MUTANTS.md](./generated/MUTANTS.md) for the mutant index. + +### 6. Gate a change + +The ledgers in [catalogs/](./catalogs/README.md) make review state checkable. +[source-audit.json](./catalogs/source-audit.json) keys every reviewed guide and +ordinary test by its headings and contract dispositions, so a text edit is +followed by `node formal/tools/check-source-audit.mjs --refresh `. +[go-parity.json](./catalogs/go-parity.json) pins the catalogs, sources and +dispositions the Go parity claim rests on and is re-pinned with +`node formal/tools/check-go-parity.mjs --refresh-inputs`. The lint, witness and +style baselines ratchet. `make audit` runs those checks together with the +semantic and feature coverage inventories, the generated-fixture and read-view +freshness checks and the Quint style caps. The pipelines below run it on every +change, and the full workflow runs everything above. + +Read more: [TEST-AUDIT.md](./guides/TEST-AUDIT.md) for keeping the ledger +current, [GO-PARITY.md](./guides/GO-PARITY.md), +[tools/README.md](./tools/README.md) for every script behind a target. + +## Pipelines + +Three GitHub Actions workflows run the same Make targets as local work. The +diagram is the full workflow's job graph; the pull request lanes, which have no +dependencies between their jobs, are listed below it. + +```mermaid +flowchart LR + CM["check-models
make formal-check"] + GE["generate
make formal-generate"] + SY["symbolic
make model-check"] + EX["exploration
make explore"] + GE --> TP["typescript-parity"] & GP["go-parity"] & RP["rust-parity"] & PP["python-parity"] + GE --> TM["typescript-mutations, 6 shards"] & GM["go-mutations, 10 shards"] & RMU["rust-mutations, 3 shards"] + CM & SY & EX & TP & GP & RP & PP & TM & GM & RMU --> AG["formal-full aggregate"] +``` + +- **CI** ([ci.yaml](../.github/workflows/ci.yaml)) runs each language's native + checks and real-server integration, the cross-language wire suite and the + package floor. Its aggregate `test` job is the required check on `main`. A + docs-only change clears it in a few minutes. +- **Formal smoke** ([formal.yaml](../.github/workflows/formal.yaml)) runs `make + audit smoke`: the ledgers and inventories, then the committed traces in all + four ports. When [fixture-scope.mjs](../.github/scripts/fixture-scope.mjs) + detects a changed Quint input, the job also recomputes every committed + artifact with pinned Quint, and on a pull request four `differential` shards + replay the composed profiles against the merge base. Any edit to a Quint + source counts, including a comment. The shards are migration evidence, not a + completion claim, and take up to about half an hour. +- **Full formal verification** + ([formal-full.yaml](../.github/workflows/formal-full.yaml)) runs weekly on + `main` and on demand for any branch. `check-models` and `generate` run side by + side; the four parity lanes and the three sharded mutation campaigns wait only + for `generate`; the symbolic lane and, when scheduled or requested, the + exploration lane run beside them. The `formal-full` aggregate requires every + lane and keeps a summary artifact for 90 days. The scheduled run takes about + two and a half hours. + +The pull request lanes are fast checks. A behavior, model or replay change +requires the full workflow on its branch before merge, and the PR body records +which run. [VALIDATION.md](./guides/VALIDATION.md) explains how to choose a run +and how to read the reports. + ## Where things are | Directory | Holds | Index | @@ -36,110 +283,12 @@ and generated artifacts; a reader should not need to open them to learn a rule. | [catalogs/](./catalogs/) | Hand-maintained manifests, evidence catalogs, ledgers, baselines and the fixed vector corpora | [catalogs/README.md](./catalogs/README.md) | | [generated/](./generated/) | Smoke traces, the fixtures lock, generated vectors and the generated read views ([PROFILES.md](./generated/PROFILES.md), the [CHALLENGES.md](./generated/CHALLENGES.md) and [MUTANTS.md](./generated/MUTANTS.md) indexes); regenerated, never edited | [generated/README.md](./generated/README.md) | -## How the specification connects to code - -Canonical Quint rules define shared acceptance conditions. Focused models -compose those rules with ownership, policy capture and environment transitions. -Independent properties check the resulting histories; [conformance profiles](./guides/GLOSSARY.md#profile-conformance-profile) -expose commands that the native implementations can execute. - -The shared replay boundary separates three responsibilities: - -- **Quint:** permitted transitions, expected results/effects, and semantic properties. -- **Replay coordination:** decode explicit inputs, map observations, check assertions, - classify reached boundaries, and account for every required result. -- **Native drivers:** call the library, control external gates/clocks, and report - actual results and effects without consulting expectations. - -The important links are executable. Shared helpers prevent repeated transition -[judgments](./guides/GLOSSARY.md#judgment-judged-once-and-applied-from-a-judgment) from drifting; profile connection checks establish selected -correspondences with the contract. Independent assertions deliberately avoid -calling the helper they are meant to challenge. - -## Models and composition profiles - -Read [cache-rules.qnt](./models/cache-rules.qnt) and -[cache-contract.qnt](./models/cache-contract.qnt) for shared judgments and acquired -ownership records. [SPEC.md](./guides/SPEC.md#definition-ownership-and-executable-connections) -maps them to the four checked profile connections. -[dialcache-rule-checks.qnt](./models/dialcache-rule-checks.qnt) supplies the finite -symbolic boundary checks. - -The [verification models](./guides/GLOSSARY.md#verification-model) emphasize individual ownership or safety boundaries: - -| Model | Starting point | -| --- | --- | -| [dialcache-core.qnt](./models/dialcache-core.qnt) | Enabled scopes, traversal and publication | -| [dialcache-runtime-policy.qnt](./models/dialcache-runtime-policy.qnt) | Sparse overlays and captured policy | -| [dialcache-tracked-invalidation.qnt](./models/dialcache-tracked-invalidation.qnt) | Acquired snapshots, watermarks and delayed writes | -| [dialcache-stale-recovery.qnt](./models/dialcache-stale-recovery.qnt) | Retained bytes, age checks and recovery authority | -| [dialcache-redis-protocol.qnt](./models/dialcache-redis-protocol.qnt) | Frame/fence validation order | - -Conformance profiles expose external commands that every language driver replays: - -| Profile | Behavior and interactions | -| --- | --- | -| [core](./models/dialcache-conformance.qnt) | Enabled traversal, hits, misses, publication and invalidation | -| [effects](./models/dialcache-effects-conformance.qnt) | Pending reads, sources and serialization; deadlines, refill authority and late effects | -| [scope](./models/dialcache-scope-conformance.qnt) | Nested enablement, request memoization, shared work and scope closure | -| [recovery](./models/dialcache-recovery-conformance.qnt) | Retained stale bytes, classifier policy, age checks and request-only recovery publication | -| [policy](./models/dialcache-policy-conformance.qnt) | Runtime overlays, captured policy, cache lifetime, capacity and coalescing changes | -| [shadow](./models/dialcache-shadow-conformance.qnt) | Dark reads, source comparison, confirmation, conditional fills and diagnostic outcomes | -| [admission](./models/dialcache-admission-conformance.qnt) | Served-hit shadow admission, deduplication, deadlines and capacity held by unfinished work | -| [layers](./models/dialcache-layers-conformance.qnt) | Request/local/remote composition, instance and key isolation, publication and invalidation | -| [independent](./models/dialcache-independent-conformance.qnt) | Uncoalesced callers, independent budgets, acquired snapshots and per-call refill authority | -| [recovery-read](./models/dialcache-recovery-read-conformance.qnt) | Held reads/decode, compressed recovery, logical versus physical age, marker lifetime and publication | -| [local-failure](./models/dialcache-local-failure-conformance.qnt) | Local storage faults, preserved source outcomes and request publication | -| [runtime-boundaries](./models/dialcache-runtime-boundaries-conformance.qnt) | Omitted/invalid policy leaves, defaults, exact rollout cohorts and policy capture | -| [shadow-layers](./models/dialcache-shadow-layers-conformance.qnt) | Dark fills and local/request reuse; independent sources and mixed served/dark capacity | -| [local-clock](./models/dialcache-local-clock-conformance.qnt) | Fractional environment time and the shared whole-millisecond process-local expiry grid | -| [source-budgets](./models/dialcache-source-budgets-conformance.qnt) | Default/unbounded/finite source deadlines, held policy, followers, outside calls and key failures | -| [dark-layers](./models/dialcache-dark-layers-conformance.qnt) | Held dark work across request/local reuse, source deadlines, instance isolation, captured fill policy, tracked fences and clock rollback | -| [shadow-read-deadlines](./models/dialcache-shadow-read-deadlines-conformance.qnt) | Separate C0/C1 read deadlines, raw capacity ownership, cancellation, captured read policy and whole-job ordering | - -These profiles deliberately bound callers, keys, contexts, capacities, payloads -and time. Their introduction does not imply that every product of those domains -is explored. [profiles.json](./catalogs/profiles.json) records profile versions, input -encodings, [smoke](./guides/GLOSSARY.md#smoke) traces and implementation declarations. - -The [kernel library](./models/kernel/README.md) states shared portable rules as pure -transitions; a composed profile assigns state only through them. Every profile -except core composes this library. The corpus [differential](./guides/GLOSSARY.md#differential) checks that changes -preserve existing profiles' observable behavior; a new profile establishes its -behavior through independent properties, consequential [witnesses](./guides/GLOSSARY.md#witness-label-and-classifier) and replay in -every supported implementation. - -## Generating and replaying behavior - -Use Node 24, pnpm 10.33.0, Go 1.27.1 and Rust/cargo 1.98.1 to match CI. -Install dependencies with `corepack pnpm install --frozen-lockfile`; rustup reads -the native Rust toolchain pin from `rust/rust-toolchain.toml`. -Model work requires Quint 0.32.0 and its Rust evaluator 0.6.0 -(`npm install --global @informalsystems/quint@0.32.0`). The evaluator is separate -from the native Rust port's compiler toolchain. -`make formal` and `make explore` use the Rust evaluator and do not need Java. -The separate `make model-check` target needs Java 21 and `tar`. Its standalone -Apalache 0.56.1 runner downloads the versioned release, verifies the SHA-256 in -[execution.json](./catalogs/execution.json), and extracts those verified bytes afresh. -The archive is cached under `~/.cache/dialcache/apalache/0.56.1/`; for offline -use, supply `APALACHE_ARCHIVE=/absolute/path/to/apalache-0.56.1.tgz`. Supplied -archives must pass the same checksum check. - -Real-server tests and TypeScript/Go mutation campaigns require Docker. Each -TypeScript/Go mutation shard starts a private Redis 6.2 server, replays all -generated invalidation vectors against the production Lua, and removes its own -container afterward. The Rust mutation campaign uses its separate native fault -catalog without Docker. The package floor requires exact Node 22.15.0 -provided through `NODE22_BIN`. `make help` lists targets and prerequisites. -`make model-check` and `make ci` additionally require Java 21 and `tar`, because -the pinned Apalache distribution is unpacked from a checksummed tarball; both -tools are probed before any step runs, and a missing one fails with a setup -message instead of a mid-run extraction error. Only the symbolic runner -downloads its pinned solver archive. +## Run it ```sh make help # Targets and prerequisites. make check # Native checks, package, docs and inventories. +make audit # Ledgers, inventories, generated views and the Quint style caps. make smoke # Committed Quint-derived histories in every port. make formal # Quint model checks, full corpus and every port's completion. make differential # Replay composed profiles' reference corpus through the working tree. @@ -150,89 +299,13 @@ make explore # Fresh recorded seed in an isolated source snapshot. make ci NODE22_BIN=/absolute/path/to/node22/bin/node ``` -`make formal-check` is the Quint evidence [lane](./guides/GLOSSARY.md#lane): it typechecks and runs every -scheduled model with the Rust evaluator, the public regressions and the model -mutation [challenges](./guides/GLOSSARY.md#challenge-fault-mutant-and-reproducer). Its first command, `node formal/tools/run-models.mjs check`, -runs only the unmodified model checks and regressions; the next step runs the -complete pinned fault campaign. `make formal` and `make ci` require both steps. -`make explore` retains the model checks, generation and all port replays but -omits that identical pinned campaign; its result remains non-acceptance evidence. -`make formal-generate` runs generation, fixture -recomputation and the shared witness evaluation; `make formal-ts`, -`make formal-go` and `make formal-rust` then complete each port's replay against -that exact corpus. `make mutations-ts`, `make mutations-go` and -`make mutations-rust` split the fault campaigns. The parity and mutation lanes -depend only on the generated corpus and shared witness evidence, so hosted CI -runs all six in parallel and none of them waits for the -model check, which runs beside generation; the aggregate requires every lane. -`make fixtures-check` recomputes committed artifacts; after an intentional model -edit, update them with `node formal/tools/generate-artifacts.mjs --write` first. -`make ci` includes the separate symbolic checks after `make formal`, as well as -the other local lanes. - -`make differential` checks the lint baseline, regenerates each composed -profile's corpus from the merge base with `origin/main` and from the working -tree, and replays each corpus through the other text (see kernel/README.md). - -Pinned acceptance clears inherited trace selectors and `QUINT_SEED`. Exploration -keeps a separate source snapshot, seed, corpus and diagnostic replay evidence. See -[VALIDATION.md](./guides/VALIDATION.md) for CI policy and report interpretation. - -Scheduled named public-action Quint regressions exercise their declared -boundaries independently of sampling. Every port replays those histories and the -complete sampled corpus; required witness coverage is checked across their -union. `execution.json` schedules the models; the tools discover their runs -from the Quint source and export every public-only run of a profile model. -Do not maintain a separate regression list in the manifest. Private state-patch -checks stay model-only unless rewritten as public actions. - -The replay protocol schema types every observation, fixture [sentinel](./guides/GLOSSARY.md#encodings-and-sentinels) and the -wall epoch, and the coordinator rejects a malformed observation as an -infrastructure error before any comparison; see the -[observation contract](./guides/PORTING.md#observation-contract). - -`execution.json` also carries the challenge catalog: for every scheduled model, -at least one compiling single-site fault that a named invariant must detect. -`node formal/tools/check-model-properties.mjs --only=` measures one entry locally; -only the complete run is evidence. - -Replay one failing feature history in TypeScript or Go: +Pinned toolchain versions, the Docker and Java requirements and the environment +variables are in [VALIDATION.md](./guides/VALIDATION.md#prerequisites). After an +intentional model edit, run `node formal/tools/generate-artifacts.mjs --write` +before `make fixtures-check`. To replay one failing history, see +[Reproducing one history](./guides/VALIDATION.md#reproducing-one-history) and +the walkthrough's [run this example](./guides/WALKTHROUGH.md#run-this-example). -```sh -DIALCACHE_FEATURE_TRACE_FILE=.formal-traces/regressions/shadow/confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest.itf.json \ - corepack pnpm --dir typescript exec vitest run test/formal-features.test.ts --coverage.enabled=false -DIALCACHE_FEATURE_TRACE_FILE="$PWD/.formal-traces/regressions/shadow/confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest.itf.json" \ - go -C go test -race -count=1 -run '^TestFeatureConformance$' ./... -``` - -Core/effects use `DIALCACHE_MBT_TRACE_FILE` or `DIALCACHE_EFFECTS_TRACE_FILE` -and their corresponding tests. Local-clock uses feature selectors with -`typescript/test/formal-local-clock.test.ts` and the Go local-clock replay. -The [walkthrough](./guides/WALKTHROUGH.md#run-this-example) shows one history replayed -in all three languages, including Rust's feature-history selectors. - -## Shared verification and replay rules - -The verification models and portable profiles share transition judgments for -local expiry, coalescing defaults, remote [retention](./guides/GLOSSARY.md#frame-stamp-retention-and-freshness), tracked publication, -recovery acquisition and [watermark](./guides/GLOSSARY.md#fence-watermark-and-marker) reads. Their primary invariants remain -independently stated. Each mapped fault must violate its original property, -fail the declared expectation in a deterministic Quint run, and reach the same -public assertion in completed TypeScript and Go recordings. - -The fractional local-clock profile retains the raw insertion instant beside -its expiry. This lets its portable history distinguish a precise-clock TTL -from the required whole-millisecond TTL while also detecting a hit that renews -expiry. Protocol classifiers use the same fence judgment as generated byte -vectors and behavioral remote reads; vector recordings select the exact -reviewed row for each language binding. - -## Evidence and scope - -[execution.json](./catalogs/execution.json) schedules model properties, exports and -bounds; every run a scheduled model declares is one of its regressions. -[profiles.json](./catalogs/profiles.json) declares the replay profiles. -[SEMANTIC-COVERAGE.md](./guides/SEMANTIC-COVERAGE.md) explains witness and mutation evidence. Query the inventories instead of copying changing totals between documents: ```sh @@ -242,13 +315,19 @@ node formal/tools/check-feature-coverage.mjs node formal/tools/run-models.mjs check --dry-run ``` -The suite combines model properties, generated conformance histories, -independently computed wire vectors, complementary fixed examples and native -integration tests. Fixed scenarios have handwritten expectations and are not -Quint-generated. Their evidence mappings do not mechanically prove each fixed -assertion agrees with Quint. - -The specification and tests use declared finite domains. Environmental -assumptions, allowed races and the limits of conformance claims are centralized -in [SPEC.md](./guides/SPEC.md#assumptions-evidence-and-claims); wire/binding obligations -are in [PROTOCOL.md](./guides/PROTOCOL.md) and [GO-PARITY.md](./guides/GO-PARITY.md). +## Reference + +Every part of the system, one line per group, for reading further. + +- **Contract guides:** [SPEC.md](./guides/SPEC.md), [CONTRACTS.md](./guides/CONTRACTS.md), [PROTOCOL.md](./guides/PROTOCOL.md), [CONFORMANCE.md](./guides/CONFORMANCE.md), [BEHAVIOR.md](./guides/BEHAVIOR.md). +- **Tooling guides:** [WALKTHROUGH.md](./guides/WALKTHROUGH.md), [AUTHORING.md](./guides/AUTHORING.md), [PORTING.md](./guides/PORTING.md), [VALIDATION.md](./guides/VALIDATION.md), [GO-PARITY.md](./guides/GO-PARITY.md), [GLOSSARY.md](./guides/GLOSSARY.md). +- **Coverage guides:** [SEMANTIC-COVERAGE.md](./guides/SEMANTIC-COVERAGE.md), [FEATURE-COVERAGE.md](./guides/FEATURE-COVERAGE.md), [TEST-MAP.md](./guides/TEST-MAP.md), [TEST-AUDIT.md](./guides/TEST-AUDIT.md); measurements at the revisions they were made in [HISTORY.md](./guides/HISTORY.md). +- **Generated views:** [PROFILES.md](./generated/PROFILES.md), [CHALLENGES.md](./generated/CHALLENGES.md), [MUTANTS.md](./generated/MUTANTS.md). +- **Shared Quint helpers:** [cache-rules.qnt](./models/cache-rules.qnt), [cache-contract.qnt](./models/cache-contract.qnt), [cohort-boundaries.qnt](./models/cohort-boundaries.qnt), [conformance-observations.qnt](./models/conformance-observations.qnt), [wire-text.qnt](./models/wire-text.qnt); the [kernel library](./models/kernel/README.md) and its [fixtures](./models/fixtures/kernel/). +- **Verification models:** [core](./models/dialcache-core.qnt), [runtime-policy](./models/dialcache-runtime-policy.qnt), [tracked-invalidation](./models/dialcache-tracked-invalidation.qnt), [stale-recovery](./models/dialcache-stale-recovery.qnt), [redis-protocol](./models/dialcache-redis-protocol.qnt), [rule-checks](./models/dialcache-rule-checks.qnt). +- **Conformance profiles:** [core](./models/dialcache-conformance.qnt), [effects](./models/dialcache-effects-conformance.qnt), [scope](./models/dialcache-scope-conformance.qnt), [recovery](./models/dialcache-recovery-conformance.qnt), [policy](./models/dialcache-policy-conformance.qnt), [shadow](./models/dialcache-shadow-conformance.qnt), [admission](./models/dialcache-admission-conformance.qnt), [layers](./models/dialcache-layers-conformance.qnt), [independent](./models/dialcache-independent-conformance.qnt), [recovery-read](./models/dialcache-recovery-read-conformance.qnt), [local-failure](./models/dialcache-local-failure-conformance.qnt), [runtime-boundaries](./models/dialcache-runtime-boundaries-conformance.qnt), [shadow-layers](./models/dialcache-shadow-layers-conformance.qnt), [local-clock](./models/dialcache-local-clock-conformance.qnt), [source-budgets](./models/dialcache-source-budgets-conformance.qnt), [dark-layers](./models/dialcache-dark-layers-conformance.qnt), [shadow-read-deadlines](./models/dialcache-shadow-read-deadlines-conformance.qnt); one line each in [models/README.md](./models/README.md), decodings in [PROFILES.md](./generated/PROFILES.md). +- **Connection and wire models:** [source](./models/dialcache-source-connection.qnt), [recovery](./models/dialcache-recovery-connection.qnt), [recovery-read](./models/dialcache-recovery-read-connection.qnt), [independent](./models/dialcache-independent-connection.qnt), [shadow-layers](./models/dialcache-shadow-layers-connection.qnt); [key-protocol](./models/dialcache-key-protocol.qnt), [frame-vectors](./models/dialcache-frame-vectors.qnt), [envelope-vectors](./models/dialcache-envelope-vectors.qnt), [invalidation-transition](./models/dialcache-invalidation-transition.qnt). +- **Manifests and catalogs:** [execution.json](./catalogs/execution.json), [profiles.json](./catalogs/profiles.json), [semantic-cases.json](./catalogs/semantic-cases.json), [coverage-witnesses.json](./catalogs/coverage-witnesses.json), [feature-coverage.json](./catalogs/feature-coverage.json), [mutations.json](./catalogs/mutations.json), [rust-mutations.json](./catalogs/rust-mutations.json), [fixture-recipes.json](./catalogs/fixture-recipes.json), [behavioral-scenarios.json](./catalogs/behavioral-scenarios.json); the ledgers and baselines [source-audit.json](./catalogs/source-audit.json), [go-parity.json](./catalogs/go-parity.json), [profile-lint-baseline.json](./catalogs/profile-lint-baseline.json), [witness-baseline.json](./catalogs/witness-baseline.json), [style-allowlist.json](./catalogs/style-allowlist.json); the fixed corpora [protocol-vectors.json](./catalogs/protocol-vectors.json), [invalidation-vectors.json](./catalogs/invalidation-vectors.json). +- **Replay:** [coordinator.mjs](./replay/coordinator.mjs), [bindings.mjs](./replay/bindings.mjs), [settlement.mjs](./replay/settlement.mjs), [protocol.schema.json](./replay/protocol.schema.json), the descriptors in [profiles/](./replay/profiles/) and the classifiers in [witnesses/](./replay/witnesses/). +- **Tools:** [validation.mjs](./tools/validation.mjs) dispatches every target; [execution.mjs](./tools/execution.mjs), [where.mjs](./tools/where.mjs), [run-models.mjs](./tools/run-models.mjs), [generate-artifacts.mjs](./tools/generate-artifacts.mjs), [witnesses.mjs](./tools/witnesses.mjs), [differential.mjs](./tools/differential.mjs), [explore.mjs](./tools/explore.mjs), [check-source-audit.mjs](./tools/check-source-audit.mjs), [check-go-parity.mjs](./tools/check-go-parity.mjs), [check-style.mjs](./tools/check-style.mjs); the rest in [tools/README.md](./tools/README.md). +- **Scope and claims:** the specification and tests use declared finite domains, and the profiles deliberately bound callers, keys, contexts, capacities, payloads and time without claiming that every product of those domains is explored. Environmental assumptions, allowed races and the limits of conformance claims are centralized in [SPEC.md](./guides/SPEC.md#assumptions-evidence-and-claims); the wire and binding obligations are in [PROTOCOL.md](./guides/PROTOCOL.md) and [GO-PARITY.md](./guides/GO-PARITY.md). diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index 9ea9b436..cbeb53df 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -217,7 +217,7 @@ }, { "path": "docs/maintainers.md", - "sha256": "836a026530b6773e06aa461a29891fe8c6d2578360f5678702e8d7374d2deb09", + "sha256": "51b0808c1983de972421a15994bf1090bd20ca3a832a28d1a88dfc5ccc29951d", "entries": [ {"title":"Maintainer guide","contracts":["B01"]}, {"title":"Validation","contracts":["B01"]}, @@ -1084,16 +1084,21 @@ "reviewedGuides": [ { "path": "formal/README.md", - "sha256": "f03253dbdc8b87c8b272b16a0b0898413efddf9cb97a144b261810eff09633bc", + "sha256": "d37b38c1cdf72dbbf26eef1702136076354309bb4d1c497ddc39569b9b9b1578", "entries": [ {"title":"Executable DialCache specification"}, {"title":"Start with your task"}, + {"title":"The setup, top to bottom"}, + {"title":"1. State the rule in Quint"}, + {"title":"2. Check the models"}, + {"title":"3. Generate the corpus and the committed artifacts"}, + {"title":"4. Replay every history in every port"}, + {"title":"5. Account for the evidence"}, + {"title":"6. Gate a change"}, + {"title":"Pipelines"}, {"title":"Where things are"}, - {"title":"How the specification connects to code"}, - {"title":"Models and composition profiles"}, - {"title":"Generating and replaying behavior"}, - {"title":"Shared verification and replay rules"}, - {"title":"Evidence and scope"} + {"title":"Run it"}, + {"title":"Reference"} ], "review": { "kind": "tooling-guide", @@ -1102,7 +1107,7 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "46ea31d30b5cfebfa6163dfad1ad33b770148bf147329bb5c0a93271d4806962", + "sha256": "baca2abd313c0bcccce5e95d384d1cce7d60982a12fe192fee7680f143acd7a7", "entries": [ {"title":"Reading and extending the DialCache models"}, {"title":"Reading a model"}, @@ -1124,7 +1129,7 @@ }, { "path": "formal/guides/BEHAVIOR.md", - "sha256": "7adc2ad8756d8df060b09c6d6c83c6d084e612c7b21afe2107029cb3c2ea2e99", + "sha256": "5d6cb8d7e779cb99e6a60f6ea553b524d49c7a42b79a74f912a90ff44c5bafe8", "entries": [ {"title":"Portable behavioral scenarios and generated profiles"}, {"title":"Scenario format"}, @@ -1220,7 +1225,7 @@ }, { "path": "formal/guides/CONFORMANCE.md", - "sha256": "fb1edc1c05e51a8b647fcb1fe91fd5c75f48f6aae4920892ae479884af67adc7", + "sha256": "3bc580b0ea32bd21e53f54ec78523afb59ebaf40f8396b7884b51d4a7b8ec898", "entries": [ {"title":"Core behavioral conformance profile"}, {"title":"Trace format and trust boundary"}, @@ -1370,7 +1375,7 @@ }, { "path": "formal/guides/GLOSSARY.md", - "sha256": "2e1ae3a35f4b2c525a144e9cd7f079994bd3ebffb3a737c5dd770bd7f5e39fe8", + "sha256": "3737909010fb573669e59ee574b1fabd37131021b9faec5b36ca02d81a590f82", "entries": [ {"title":"Glossary"}, {"title":"Specification and replay"}, @@ -1381,6 +1386,7 @@ {"title":"Connection model"}, {"title":"Smoke"}, {"title":"Lane"}, + {"title":"ITF (Informal Trace Format)"}, {"title":"Corpus, history, regression, exported run and public-only run"}, {"title":"Differential"}, {"title":"Bytes per state"}, @@ -1429,7 +1435,7 @@ }, { "path": "formal/guides/GO-PARITY.md", - "sha256": "1af6d885ef3490badfe7bc05f215bc20c3fad84bd9a2786ac4b62c00ce35e8c7", + "sha256": "956b12eabff3716bac5f4c57d14315c792dc89524c224a261fd15508992ff63f", "entries": [ {"title":"Go parity acceptance"}, {"title":"Required evidence"}, @@ -1475,7 +1481,7 @@ }, { "path": "formal/guides/PORTING.md", - "sha256": "22d0c0dc6ad513ee29f7008a83d8152ea77d1fff5a72c8393a643e0e71d5fe06", + "sha256": "342cfd680eeba31a57c7cc790693fb21d56e358e20ce105a6a6ce28a9e511a7e", "entries": [ {"title":"Implementing another DialCache port"}, {"title":"What a port supplies"}, @@ -1550,7 +1556,7 @@ }, { "path": "formal/guides/SEMANTIC-COVERAGE.md", - "sha256": "2834da3082acbcb70afffb4b4c18e5547209c47129f1ba681a598ac614d41539", + "sha256": "aaa54bdb961436a615dd4a0c1e29270c0c6ebe69adb24a41f97a0f26698e8282", "entries": [ {"title":"Measuring semantic coverage"}, {"title":"Evidence inventory"}, @@ -1673,7 +1679,7 @@ }, { "path": "formal/guides/TEST-MAP.md", - "sha256": "a32e4513667d38236aeb4df0b8c872912e725f1ae1605a6a91c07cb2970dc4d5", + "sha256": "66593388b326cd3c6b5378a1f98dc0cad28a2f39b387cc9b5efa032a28b0ec26", "entries": [ {"title":"Formal contract and implementation evidence map"}, {"title":"Behavioral map"}, @@ -1689,11 +1695,13 @@ }, { "path": "formal/guides/VALIDATION.md", - "sha256": "20132bd3ea23510eef25022fec91482fd09bf24f0a285f72aa018d69a69bd154", + "sha256": "f0dd128820f79d911cd086f9cbb523f7c3016304d9d3e9364e458aa62ca4fa2c", "entries": [ {"title":"Validation and evidence"}, + {"title":"Prerequisites"}, {"title":"Choosing a run"}, {"title":"Reading a completion report"}, + {"title":"Reproducing one history"}, {"title":"Mutation evidence"}, {"title":"Exploratory runs"}, {"title":"A retained sampling regression"} @@ -1705,7 +1713,7 @@ }, { "path": "formal/guides/WALKTHROUGH.md", - "sha256": "c7d3bdb1e65f3672f94c61c5a5cccaf9f2bfd061f5de3f226dfa93973f4fab59", + "sha256": "17eb27c78c4be73e47cec8e08a8f33cf07d8f33116ab0e531f19f0f59f082174", "entries": [ {"title":"Follow one behavior from Quint to every port"}, {"title":"Read the named run first"}, @@ -1720,7 +1728,7 @@ }, { "path": "go/README.md", - "sha256": "97ceca7d13bc270a4e53341ce1d33b0a8f3906d4b4f26b7d2d30a8747f59f0f1", + "sha256": "fa465c2a7e53b4fe3ea2045708510c81ea5304e62533f99726d9bcdf1ba9c079", "entries": [ {"title":"DialCache for Go"}, {"title":"Use"}, diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index d8b93cf7..bf631bbd 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -27,7 +27,7 @@ ownership records. [Verification models](./GLOSSARY.md#verification-model) and [ definitions. [Connection models](./GLOSSARY.md#connection-model) check selected profile histories against the acquired contracts. Conformance profiles also expose external actions that a language [driver](./GLOSSARY.md#driver) can replay. The -[model inventory](../README.md#models-and-composition-profiles) and [profile registry](../catalogs/profiles.json) +[model inventory](../models/README.md) and [profile registry](../catalogs/profiles.json) identify the relevant starting point. The words the models and guides share (driver, profile, flight, source, judgment, variant, witness and the rest) are defined in [GLOSSARY.md](./GLOSSARY.md), each with the file that owns it. @@ -394,7 +394,7 @@ source expression moves or changes; its failure must never count as detection. For a model refactor, run the scheduled model checks/regressions, generation, implementation replay, evidence validation, and relevant mutation gates using -the [documented commands](../README.md#generating-and-replaying-behavior). Keep the +the [documented commands](../README.md#run-it). Keep the committed [smoke](./GLOSSARY.md#smoke) expectations unchanged. Compare pre/post generated action and state histories when preserving a fixed seed and schedule is intended, and investigate differences rather than replacing expectations to obtain a pass. diff --git a/formal/guides/BEHAVIOR.md b/formal/guides/BEHAVIOR.md index 575c6c52..d953c7ab 100644 --- a/formal/guides/BEHAVIOR.md +++ b/formal/guides/BEHAVIOR.md @@ -12,7 +12,7 @@ required witnesses in both languages. Fast PR checks use committed smoke, fixed supplements and freshness audits without claiming full parity; model/generator changes additionally recompute committed artifacts. Full validation remains required for behavior/model changes before merge and for -release/new-port acceptance. See the [Make targets](../README.md#generating-and-replaying-behavior). +release/new-port acceptance. See the [Make targets](../README.md#run-it). ## Scenario format @@ -113,7 +113,7 @@ profile leaves to others, and how to replay a generated trace. ### Trace contract -Each ITF state carries the authoritative `input.name` and `input.choice` beside the +Each [ITF](./GLOSSARY.md#itf-informal-trace-format) state carries the authoritative `input.name` and `input.choice` beside the expected state `s`. The choice is a nonnegative ITF integer on actions that have choices and `-1` otherwise; optional `mbt::actionTaken` and `mbt::nondetPicks.choice` annotations must agree with it, and raw regression exports carry no annotations diff --git a/formal/guides/CONFORMANCE.md b/formal/guides/CONFORMANCE.md index b8c04045..645ebeb1 100644 --- a/formal/guides/CONFORMANCE.md +++ b/formal/guides/CONFORMANCE.md @@ -4,7 +4,7 @@ This document specifies the bounded `core` profile implemented by the TypeScript ## Trace format and trust boundary -Inputs use Quint 0.32.0's ITF JSON format. Each entry in `states` has: +Inputs are Quint 0.32.0 [ITF](./GLOSSARY.md#itf-informal-trace-format) traces (the Informal Trace Format, JSON). Each entry in `states` has: - `input`: the authoritative public action, encoded as `{"name":"init","choice":{"#bigint":"-1"}}`. The first action is `init`; every core action uses `choice: -1` because it has no external arguments. - `s`: the expected model state after that action. Integers are encoded as `{"#bigint":"123"}`; booleans are JSON booleans. diff --git a/formal/guides/GLOSSARY.md b/formal/guides/GLOSSARY.md index 67564bfa..eaa9b268 100644 --- a/formal/guides/GLOSSARY.md +++ b/formal/guides/GLOSSARY.md @@ -39,9 +39,13 @@ One committed named history per conformance profile, `formal/generated/ One validation pipeline run as its own make target and hosted CI job: the Quint evidence lane (`formal-check`), generation (`formal-generate`), the per-port parity lanes (`formal-ts`, `formal-go`, `formal-rust`, `formal-python`), the mutation lanes, and the differential, symbolic, exploration, smoke, audit and integration lanes. Parity and mutation lanes depend only on the generated corpus and witness evidence, so they run in parallel; the aggregate requires every lane. Owner: [VALIDATION.md](./VALIDATION.md) +### ITF (Informal Trace Format) + +The JSON trace format Quint and Apalache write, defined by Informal Systems in [ADR-015](https://apalache-mc.org/docs/adr/015adr-trace.html) and produced by `quint run --out-itf` ([Quint CLI](https://quint.sh/docs/quint)). A trace is one object: a `#meta` header, the `vars` list and a `states` array holding one record of every variable per step. Integers are decimal strings inside `{"#bigint":"…"}` so no value loses precision; sets, tuples and maps use `#set`, `#tup` and `#map` wrappers. Every history here is one ITF file (`.itf.json`): the committed smoke traces, the sampled corpus and the exported regressions, each carrying the `mbt::actionTaken` and `mbt::nondetPicks` annotations the simulator adds beside the authoritative `input` record. The coordinator reads them through [itf.mjs](../replay/itf.mjs), which rejects an integer that would not survive as a JavaScript number. Owner: [itf.mjs](../replay/itf.mjs) + ### Corpus, history, regression, exported run and public-only run -A history is one ITF trace: an initial state then public actions, each recording its command in `input`. The corpus is everything a port replays: the sampled histories generation emits per profile plus the exported regressions. A regression is any `run ...Test` a scheduled model declares; a profile's public-only runs, whose every transition records a command, are exported for replay, while state-patching runs stay model-only. Owner: [AUTHORING.md](./AUTHORING.md), [execution.mjs](../tools/execution.mjs) +A history is one [ITF](#itf-informal-trace-format) trace: an initial state then public actions, each recording its command in `input`. The corpus is everything a port replays: the sampled histories generation emits per profile plus the exported regressions. A regression is any `run ...Test` a scheduled model declares; a profile's public-only runs, whose every transition records a command, are exported for replay, while state-patching runs stay model-only. Owner: [AUTHORING.md](./AUTHORING.md), [execution.mjs](../tools/execution.mjs) ### Differential diff --git a/formal/guides/GO-PARITY.md b/formal/guides/GO-PARITY.md index 0bcb2b10..4d01bbb9 100644 --- a/formal/guides/GO-PARITY.md +++ b/formal/guides/GO-PARITY.md @@ -29,7 +29,7 @@ artifact generation and prepared TS/Go replay. Run `make model-check` for the separate finite symbolic checks, then `make mutations` and `make integration` for their fault and real-server evidence. `make ci NODE22_BIN=/path/to/node22/bin/node` runs all local lanes in order, -including symbolic checks and the exact Node 22.15.0 package floor; see the [Make target guide](../README.md#generating-and-replaying-behavior) +including symbolic checks and the exact Node 22.15.0 package floor; see the [Make target guide](../README.md#run-it) for pinned prerequisites and individual targets. Hosted PR checks run native/race tests, committed smoke, audits and real diff --git a/formal/guides/PORTING.md b/formal/guides/PORTING.md index 18d17402..2c23f34a 100644 --- a/formal/guides/PORTING.md +++ b/formal/guides/PORTING.md @@ -95,7 +95,8 @@ of the Go cache library. ## Trace and observation contract -Quint exports ITF JSON. A trace contains a nonempty `states` array with an +Quint exports [ITF](./GLOSSARY.md#itf-informal-trace-format) JSON, the Informal +Trace Format. A trace contains a nonempty `states` array with an initial state followed by public actions. Reject unknown profiles/versions, unknown actions, malformed or out-of-domain choices, missing observations, misplaced initialization, and empty histories. @@ -329,7 +330,7 @@ harness; those corruptions receive no positive conformance credit. ## Complete corpus and reusable acceptance checks -Use the [shared Make targets and pinned prerequisites](../README.md#generating-and-replaying-behavior) +Use the [shared Make targets and pinned prerequisites](../README.md#run-it) from the repository root: ```sh diff --git a/formal/guides/SEMANTIC-COVERAGE.md b/formal/guides/SEMANTIC-COVERAGE.md index 60096b08..8b9b3cd9 100644 --- a/formal/guides/SEMANTIC-COVERAGE.md +++ b/formal/guides/SEMANTIC-COVERAGE.md @@ -85,7 +85,7 @@ histories against those records. | Exported boundary regressions | The exact public command sequence is checked in Quint and against both implementations | `make model-check` runs the symbolic checks declared in `execution.json` through -checksummed standalone Apalache; see the [tool prerequisites](../README.md#generating-and-replaying-behavior). +checksummed standalone Apalache; see the [tool prerequisites](./VALIDATION.md#prerequisites). This lane is separate from `make formal` and included in `make ci`. The model-property challenge catalog is the `challenges` array of [execution.json](../catalogs/execution.json). It runs once at the end of the scheduled @@ -158,7 +158,7 @@ results; fresh measurements belong with their exact source and corpus artifacts. ## Reproduction and CI -Use the [shared Make targets and pinned prerequisites](../README.md#generating-and-replaying-behavior): +Use the [shared Make targets and pinned prerequisites](../README.md#run-it): ```sh make formal # Regenerate and complete prepared TS, Go and Rust replay. diff --git a/formal/guides/TEST-MAP.md b/formal/guides/TEST-MAP.md index 10c0c5de..816d8755 100644 --- a/formal/guides/TEST-MAP.md +++ b/formal/guides/TEST-MAP.md @@ -107,7 +107,7 @@ small compression caps exercise wrapper decisions without allocating the real ## Evidence and measurement -Run the commands in [README.md](../README.md#generating-and-replaying-behavior) +Run the commands in [README.md](../README.md#run-it) and inspect `node formal/tools/check-semantic-coverage.mjs` for current accounting. Checking a model, reaching a witness and replaying its observations are separate requirements. Both implementation completion gates derive the exact sampled diff --git a/formal/guides/VALIDATION.md b/formal/guides/VALIDATION.md index a9be8907..e94be531 100644 --- a/formal/guides/VALIDATION.md +++ b/formal/guides/VALIDATION.md @@ -1,16 +1,50 @@ # Validation and evidence Run validation from the repository root. The Make targets are shared by local -work and GitHub Actions; [README.md](../README.md#generating-and-replaying-behavior) -lists tool prerequisites and focused reproduction commands. Past measurements, -at the revisions they were made, are in [HISTORY.md](./HISTORY.md). +work and GitHub Actions; [README.md](../README.md#the-setup-top-to-bottom) +explains how the lanes fit together, and the prerequisites and focused +reproduction commands are below. Past measurements, at the revisions they were +made, are in [HISTORY.md](./HISTORY.md). + +## Prerequisites + +Use Node 24, pnpm 10.33.0, Go 1.27.1, Rust/cargo 1.98.1 and Python 3.11 or +later to match CI. Install dependencies with +`corepack pnpm install --frozen-lockfile`; rustup reads the native Rust +toolchain pin from `rust/rust-toolchain.toml`; create `python/.venv` and install +`./python[test,redis]` into it, or point `PYTHON` at another prepared +interpreter. Model work requires Quint 0.32.0 and its Rust evaluator 0.6.0 +(`npm install --global @informalsystems/quint@0.32.0`); the evaluator is +separate from the native Rust port's compiler toolchain. `make formal` and +`make explore` use the Rust evaluator and do not need Java. + +The separate `make model-check` target needs Java 21 and `tar`. Its standalone +Apalache 0.56.1 runner downloads the versioned release, verifies the SHA-256 in +[execution.json](../catalogs/execution.json), and extracts those verified bytes +afresh. The archive is cached under `~/.cache/dialcache/apalache/0.56.1/`; for +offline use, supply `APALACHE_ARCHIVE=/absolute/path/to/apalache-0.56.1.tgz`. +Supplied archives must pass the same checksum check. `make ci` requires the same +two tools; both are probed before any step runs, and a missing one fails with a +setup message instead of a mid-run extraction error. Only the symbolic runner +downloads its pinned solver archive. + +Real-server tests and the TypeScript and Go mutation campaigns require Docker. +Each TypeScript or Go mutation shard starts a private Redis 6.2 server, replays +all generated invalidation vectors against the production Lua, and removes its +own container afterward. The Rust mutation campaign uses its separate native +fault catalog without Docker. The package floor requires exact Node 22.15.0 +provided through `NODE22_BIN`. `make help` lists targets and prerequisites. + +Pinned acceptance clears inherited trace selectors and `QUINT_SEED`. +Exploration keeps a separate source snapshot, seed, corpus and diagnostic +replay evidence. ## Choosing a run | Task | Command | Evidence | | --- | --- | --- | | Routine implementation checks | `make check` | Native tests, coverage, package, docs and source audits | -| Full portable acceptance | `make formal` | Quint model checks with the Rust evaluator, generated histories, shared witness evaluation, TypeScript/Go/Rust replay, exact completion inventories; no Java | +| Full portable acceptance | `make formal` | Quint model checks with the Rust evaluator, generated histories, shared witness evaluation, TypeScript, Go, Rust and Python replay, exact completion inventories; no Java | | Finite symbolic rules | `make model-check` | Scheduled bounded checks with checksummed standalone Apalache; requires Java 21, `tar` and pinned Quint | | Challenge implementation assertions | `make mutations` | Compiling semantic faults tested against every completed port | | Real server behavior | `make integration` | Redis, Valkey, Cluster and cross-language interoperability | @@ -94,6 +128,24 @@ Copying a report to another revision does not revalidate that revision. Scope and environmental assumptions are defined once in [SPEC.md](./SPEC.md#assumptions-evidence-and-claims). +## Reproducing one history + +Replay one failing feature history in TypeScript or Go: + +```sh +DIALCACHE_FEATURE_TRACE_FILE=.formal-traces/regressions/shadow/confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest.itf.json \ + corepack pnpm --dir typescript exec vitest run test/formal-features.test.ts --coverage.enabled=false +DIALCACHE_FEATURE_TRACE_FILE="$PWD/.formal-traces/regressions/shadow/confirmationPastFreshnessKeepsOriginalPayloadAndAgeTest.itf.json" \ + go -C go test -race -count=1 -run '^TestFeatureConformance$' ./... +``` + +Core and effects histories use `DIALCACHE_MBT_TRACE_FILE` or +`DIALCACHE_EFFECTS_TRACE_FILE` with their corresponding tests. Local-clock uses +feature selectors with `typescript/test/formal-local-clock.test.ts` and the Go +local-clock replay. The [walkthrough](./WALKTHROUGH.md#run-this-example) shows +one history replayed in TypeScript, Go and Rust, including Rust's +feature-history selectors. + ## Mutation evidence Each TypeScript or Go mutation report includes a `boundary` entry for every mapped diff --git a/formal/guides/WALKTHROUGH.md b/formal/guides/WALKTHROUGH.md index 368a8bdc..9491c031 100644 --- a/formal/guides/WALKTHROUGH.md +++ b/formal/guides/WALKTHROUGH.md @@ -127,7 +127,7 @@ records native tests and explicit adaptations. ## Run this example -Use the [pinned prerequisites](../README.md#generating-and-replaying-behavior) +Use the [pinned prerequisites](./VALIDATION.md#prerequisites) from the repository root. This focused command runs the named Quint regression and writes its history into a separate exploration directory: diff --git a/formal/models/README.md b/formal/models/README.md index c99e759c..0d8c142c 100644 --- a/formal/models/README.md +++ b/formal/models/README.md @@ -42,7 +42,7 @@ profile for the behavior you care about; - [dialcache-local-failure-conformance.qnt](./dialcache-local-failure-conformance.qnt): local-failure; local storage faults and preserved source outcomes. - [dialcache-runtime-boundaries-conformance.qnt](./dialcache-runtime-boundaries-conformance.qnt): runtime-boundaries; omitted and invalid policy leaves, defaults, exact cohorts. - [dialcache-shadow-layers-conformance.qnt](./dialcache-shadow-layers-conformance.qnt): shadow-layers; dark fills with local and request reuse, mixed capacity. -- [dialcache-local-clock-conformance.qnt](./dialcache-local-clock-conformance.qnt): local-clock; fractional time on the whole-millisecond expiry grid. +- [dialcache-local-clock-conformance.qnt](./dialcache-local-clock-conformance.qnt): local-clock; fractional time on the whole-millisecond expiry grid, keeping the raw insertion instant beside the expiry so a history tells a precise-clock TTL from the required whole-millisecond TTL and still detects a hit that renews expiry. - [dialcache-source-budgets-conformance.qnt](./dialcache-source-budgets-conformance.qnt): source-budgets; default, unbounded and finite source deadlines, held policy. - [dialcache-dark-layers-conformance.qnt](./dialcache-dark-layers-conformance.qnt): dark-layers; held dark work across request and local reuse, fences, clock rollback. - [dialcache-shadow-read-deadlines-conformance.qnt](./dialcache-shadow-read-deadlines-conformance.qnt): shadow-read-deadlines; separate C0 and C1 read deadlines, raw capacity ownership. diff --git a/go/README.md b/go/README.md index a7a06200..e2807029 100644 --- a/go/README.md +++ b/go/README.md @@ -200,7 +200,7 @@ Apalache; integration needs Docker. Go conformance tests use the shared Node replay coordinator for command mappings and assertions. The cache library itself has no Node dependency. Follow the -[shared prerequisite guide](../formal/README.md#generating-and-replaying-behavior) +[shared prerequisite guide](../formal/guides/VALIDATION.md#prerequisites) once, then: ```sh