Skip to content

docs(formal): describe all four ports in the formal guides #226

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lan17 wants to merge 1 commit into
base: main
Choose a base branch
from
+129 −108
Open

docs(formal): describe all four ports in the formal guides #226

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 13 additions & 9 deletions formal/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# 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
Quint defines the portable contracts that TypeScript, Go, Rust, Python and future
ports must preserve. TypeScript is the executable reference those contracts formalize; a
disagreement between the two is settled by a distinguishing regression and a
recorded decision, not by editing the easier side. Native drivers execute
external commands against the real libraries; generated expectations stay in
Expand All @@ -12,7 +12,7 @@ the test coordinator.
| 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) |
| Follow one rule into all four implementations | [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 |
Expand Down Expand Up @@ -109,9 +109,12 @@ 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.
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`.
the native Rust toolchain pin from `rust/rust-toolchain.toml`. Create
`python/.venv` and run `python/.venv/bin/python -m pip install -e './python[test,redis]'`,
or set `PYTHON` to 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.
Expand Down Expand Up @@ -157,11 +160,11 @@ complete pinned fault campaign. `make formal` and `make ci` require both steps.
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 formal-go`, `make formal-rust` and `make formal-python` 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
runs all seven 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.
Expand Down Expand Up @@ -207,7 +210,8 @@ 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.
in all four languages, including Rust's feature-history selectors and the Python
replay runner.

## Shared verification and replay rules

Expand Down
2 changes: 1 addition & 1 deletion formal/catalogs/go-parity.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
"inputs": {
"semanticCasesSha256": "f5f7ee357201b343eb00f8f9c783c92af0d722709137edc0f55e0a52b3cdec0a",
"executionSha256": "29a412f87329347840f000ea44a6e95332464c0b01b92b4e41c615af3c9157cd",
"sourceAuditSha256": "0c810137c44654d5e8ef9b2580ad125709d961846e7628387aa16226cdd8c584",
"sourceAuditSha256": "f895772a73b4810ce6489cdb1ff3c6296b543a6e739c5abb02802f018b4c7f4d",
"featureCoverageSha256": "2d4e47ec18688c911ce4d6bda780edc8ee654069aa5704e15a39cbae35655ba7",
"coverageWitnessesSha256": "2b2d5d57daacba3ecd3637f5a917d58b0b63fcc88893e651cd602cdba1ef4244",
"profilesSha256": "9df8285820e4fff65f6a7753885bbb192c09f3f476eac8f9c98d130454ae1a28"
Expand Down
80 changes: 40 additions & 40 deletions formal/catalogs/source-audit.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1084,16 +1084,16 @@
"reviewedGuides": [
{
"path": "formal/README.md",
"sha256": "7ad4d77aa162e93e8def416fb545c29586532138ffd2d2c68c6213a1bab7a23f",
"sha256": "9cc60b22aa7bea2e65d79ecb98befa48829c636547144ac1a70d846988f2f505",
"entries": [
{"line":1,"title":"Executable DialCache specification"},
{"line":10,"title":"Start with your task"},
{"line":26,"title":"Where things are"},
{"line":37,"title":"How the specification connects to code"},
{"line":57,"title":"Models and composition profiles"},
{"line":110,"title":"Generating and replaying behavior"},
{"line":212,"title":"Shared verification and replay rules"},
{"line":228,"title":"Evidence and scope"}
{"line":216,"title":"Shared verification and replay rules"},
{"line":232,"title":"Evidence and scope"}
],
"review": {
"kind": "tooling-guide",
Expand All @@ -1102,20 +1102,20 @@
},
{
"path": "formal/guides/AUTHORING.md",
"sha256": "8e23cd5252a5d7eb8a8e42cab301345f0c6ffa055994566076c45c979da5c8f0",
"sha256": "ec456bc370b1f32e1964cc5472838544f6014a5ddbadb85e8892a3185d22241f",
"entries": [
{"line":1,"title":"Reading and extending the DialCache models"},
{"line":20,"title":"Reading a model"},
{"line":61,"title":"Writing conventions"},
{"line":172,"title":"Codifying the next behavior"},
{"line":234,"title":"Give reviewers focused context"},
{"line":249,"title":"Exporting a deterministic regression"},
{"line":287,"title":"Maintaining case and witness evidence"},
{"line":340,"title":"Reproducible committed fixtures"},
{"line":350,"title":"Refactoring and execution"},
{"line":378,"title":"Challenging every model"},
{"line":459,"title":"Mapping every challenge to native mutants"},
{"line":590,"title":"Exported runs are exactly the public-only runs"}
{"line":21,"title":"Reading a model"},
{"line":62,"title":"Writing conventions"},
{"line":173,"title":"Codifying the next behavior"},
{"line":236,"title":"Give reviewers focused context"},
{"line":251,"title":"Exporting a deterministic regression"},
{"line":289,"title":"Maintaining case and witness evidence"},
{"line":342,"title":"Reproducible committed fixtures"},
{"line":352,"title":"Refactoring and execution"},
{"line":380,"title":"Challenging every model"},
{"line":461,"title":"Mapping every challenge to native mutants"},
{"line":592,"title":"Exported runs are exactly the public-only runs"}
],
"review": {
"kind": "tooling-guide",
Expand All @@ -1124,7 +1124,7 @@
},
{
"path": "formal/guides/BEHAVIOR.md",
"sha256": "6c835d7e3aecafce708b9ec7bf4b54d7c2d5daa4fa9c9a02ea71bbd5446b34a6",
"sha256": "8d2ffe0d01ce8ce9bc5d74ca2fe87c7ba410021c5d75a3eadf3a84cbbf507a2a",
"entries": [
{"line":1,"title":"Portable behavioral scenarios and generated feature profiles"},
{"line":17,"title":"Scenario format"},
Expand Down Expand Up @@ -1220,7 +1220,7 @@
},
{
"path": "formal/guides/CONFORMANCE.md",
"sha256": "fb1edc1c05e51a8b647fcb1fe91fd5c75f48f6aae4920892ae479884af67adc7",
"sha256": "c4f33cc4a5a8ed1a0e641c9ab3ddead6adeccddbc436263ce4d9bb597f56890e",
"entries": [
{"line":1,"title":"Core behavioral conformance profile"},
{"line":5,"title":"Trace format and trust boundary"},
Expand Down Expand Up @@ -1251,7 +1251,7 @@
},
{
"path": "formal/guides/CONTRACTS.md",
"sha256": "6b6c3a08412f1ad1da0700dd4777a7e61306b6b7559e3409b83b15dda75ff8c6",
"sha256": "ff09f4b06df9414fcf532c2410630363c367dfce5a95ff19782cf9b45a14b643",
"entries": [
{"line":1,"title":"Portable contract inventory"},
{"line":11,"title":"Where the boundary lies"},
Expand Down Expand Up @@ -1354,7 +1354,7 @@
},
{
"path": "formal/guides/FEATURE-COVERAGE.md",
"sha256": "8368ec455fa600c89821853926ca1c5025ba18bb6dacdc6d6a34794d9ade8afb",
"sha256": "9401068c25e880fc863fb5dde393e77dca0993e72a9b4bbd96d3c48d7da60e2b",
"entries": [
{"line":1,"title":"DialCache features and known behavioral corners"},
{"line":16,"title":"What is accounted for"},
Expand Down Expand Up @@ -1385,18 +1385,18 @@
},
{
"path": "formal/guides/PORTING.md",
"sha256": "22d0c0dc6ad513ee29f7008a83d8152ea77d1fff5a72c8393a643e0e71d5fe06",
"sha256": "10004e16853943b8a17014e97454b16bc31d4709f39dd1ceec6a100a9f263711",
"entries": [
{"line":1,"title":"Implementing another DialCache port"},
{"line":14,"title":"What a port supplies"},
{"line":46,"title":"Shared coordinator protocol"},
{"line":96,"title":"Trace and observation contract"},
{"line":197,"title":"Observation contract"},
{"line":295,"title":"Generated fixtures and fast local tests"},
{"line":330,"title":"Complete corpus and reusable acceptance checks"},
{"line":450,"title":"Witness evidence"},
{"line":540,"title":"Current limitations for a further port"},
{"line":562,"title":"New-port acceptance"}
{"line":15,"title":"What a port supplies"},
{"line":48,"title":"Shared coordinator protocol"},
{"line":98,"title":"Trace and observation contract"},
{"line":199,"title":"Observation contract"},
{"line":297,"title":"Generated fixtures and fast local tests"},
{"line":332,"title":"Complete corpus and reusable acceptance checks"},
{"line":457,"title":"Witness evidence"},
{"line":547,"title":"Current limitations for a further port"},
{"line":569,"title":"New-port acceptance"}
],
"review": {
"kind": "tooling-guide",
Expand Down Expand Up @@ -1458,7 +1458,7 @@
},
{
"path": "formal/guides/SEMANTIC-COVERAGE.md",
"sha256": "fda0d8e33d65d56129a9d38f828500843f01038d03772cba0ec7f9fe33a8bd0c",
"sha256": "22564e0f805c9b9ca2b877f7f3fcb9ad81b42f06102ef6e62c4157bdde2c3cb4",
"entries": [
{"line":1,"title":"Measuring semantic coverage"},
{"line":5,"title":"Evidence inventory"},
Expand All @@ -1476,7 +1476,7 @@
},
{
"path": "formal/guides/SPEC.md",
"sha256": "869de9ced5a70b4bd966c8c0e94ead1b3df0b06a54ca7773e0307e4aa3e7cda4",
"sha256": "efbc80ee6aee75c46f12663bf4189ae95b898f7d6ab0832254685e67a2ea7d6b",
"entries": [
{"line":1,"title":"DialCache behavioral specification"},
{"line":18,"title":"Definition ownership and executable connections"},
Expand Down Expand Up @@ -1567,7 +1567,7 @@
},
{
"path": "formal/guides/TEST-AUDIT.md",
"sha256": "40bfa79ffe73d35813ead894c92b0e776ba97e02b003f85d992df1a5c87bdd6a",
"sha256": "8a0ab751ab354c67944f27f29f9bd45320858238d2f579cf610671ad88b0c8d5",
"entries": [
{"line":1,"title":"Docs and test behavior audit"},
{"line":13,"title":"Keeping the audit current"},
Expand All @@ -1581,7 +1581,7 @@
},
{
"path": "formal/guides/TEST-MAP.md",
"sha256": "a32e4513667d38236aeb4df0b8c872912e725f1ae1605a6a91c07cb2970dc4d5",
"sha256": "d29dfd836a13a86512da0e107ebcdb51e49150e1b92245c114c706bd853c5388",
"entries": [
{"line":1,"title":"Formal contract and implementation evidence map"},
{"line":18,"title":"Behavioral map"},
Expand All @@ -1597,15 +1597,15 @@
},
{
"path": "formal/guides/VALIDATION.md",
"sha256": "70dcafee96aea5a927e7acc99021ddeec3818e176497c95d7f783ca8ca442cb6",
"sha256": "fcef5ccca5ee27308735ea6bd874832c38cc038b262ea804d34b94cb24e4a5c8",
"entries": [
{"line":1,"title":"Validation and evidence"},
{"line":7,"title":"Choosing a run"},
{"line":77,"title":"Reading a completion report"},
{"line":96,"title":"Mutation evidence"},
{"line":210,"title":"Exploratory runs"},
{"line":266,"title":"A retained sampling regression"},
{"line":303,"title":"Historical results"}
{"line":211,"title":"Exploratory runs"},
{"line":267,"title":"A retained sampling regression"},
{"line":304,"title":"Historical results"}
],
"review": {
"kind": "tooling-guide",
Expand All @@ -1614,13 +1614,13 @@
},
{
"path": "formal/guides/WALKTHROUGH.md",
"sha256": "c7d3bdb1e65f3672f94c61c5a5cccaf9f2bfd061f5de3f226dfa93973f4fab59",
"sha256": "304116bc3a815ffb12528c5af298d4e238d1bb57571b6ceb80a6f9aadfc9eade",
"entries": [
{"line":1,"title":"Follow one behavior from Quint to every port"},
{"line":14,"title":"Read the named run first"},
{"line":62,"title":"Follow input and evidence separately"},
{"line":99,"title":"Find the rule's catalog entries"},
{"line":128,"title":"Run this example"}
{"line":101,"title":"Find the rule's catalog entries"},
{"line":130,"title":"Run this example"}
],
"review": {
"kind": "tooling-guide",
Expand Down
14 changes: 8 additions & 6 deletions formal/guides/AUTHORING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,17 @@ The Quint files should let a reader understand a behavior without translating
the TypeScript implementation. Readability is part of the specification's
acceptance criteria. Executable checks then challenge that written behavior.
TypeScript is the executable reference these models formalize; Quint is the
independently reviewed contract that TypeScript, Go, Rust and future ports are held
to. When the two disagree, neither side is edited to match the other quietly:
independently reviewed contract that TypeScript, Go, Rust, Python and future ports
are held to. When the two disagree, neither side is edited to match the other quietly:
the change lands with a regression that distinguishes the two behaviors and a
comment recording the decision about which one is intended. The prose explains
the contract; implementation tests must not become an independent, drifting
definition of the same portable rule.

For a first contribution, start with the [worked walkthrough](./WALKTHROUGH.md).
It follows one existing contract from a named Quint regression through actual
TypeScript, Go and Rust assertions, and identifies the catalog entry each edit owns.
TypeScript, Go, Rust and Python assertions, and identifies the catalog entry each
edit owns.
Then use the checklist below for your rule; it applies the same path to another
behavior.

Expand Down Expand Up @@ -195,7 +196,7 @@ own API and integration tests.
[Mapping every challenge to native mutants](#mapping-every-challenge-to-native-mutants)).
4. **Exercise every supported implementation.** Require a generated witness or exported
Quint regression that exposes the rule's consequence, and replay the same
history in TypeScript, Go and Rust. Preserve a discovered portable bug as a
history in TypeScript, Go, Rust and Python. Preserve a discovered portable bug as a
deterministic exported regression. Fixed scenarios preserve narrow regressions;
protocol vectors and native
tests cover wire and language boundaries. The driver supplies only external inputs and asserts actual public
Expand Down Expand Up @@ -223,8 +224,9 @@ establish another port's conformance. Behavior, model and replay changes require

Fault-detection evidence is specific to each port. Rust uses
[its own mutation catalog](./SEMANTIC-COVERAGE.md#reproduction-and-ci); the
TypeScript/Go mappings above do not establish Rust detection. Add equivalent
native faults where applicable and report remaining gaps explicitly.
TypeScript/Go mappings above do not establish Rust detection. Python has no
native mutation campaign, so nothing yet measures fault detection by its replay.
Add equivalent native faults where applicable and report remaining gaps explicitly.

Extend formal infrastructure when a concrete behavior cannot be expressed or
tested clearly, evidence gives misleading credit, or authoring and execution
Expand Down
Loading
Loading