diff --git a/formal/README.md b/formal/README.md index d44548f7..5b4b9711 100644 --- a/formal/README.md +++ b/formal/README.md @@ -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 @@ -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 | @@ -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. @@ -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. @@ -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 diff --git a/formal/catalogs/go-parity.json b/formal/catalogs/go-parity.json index d9761888..2a04320c 100644 --- a/formal/catalogs/go-parity.json +++ b/formal/catalogs/go-parity.json @@ -10,7 +10,7 @@ "inputs": { "semanticCasesSha256": "f5f7ee357201b343eb00f8f9c783c92af0d722709137edc0f55e0a52b3cdec0a", "executionSha256": "29a412f87329347840f000ea44a6e95332464c0b01b92b4e41c615af3c9157cd", - "sourceAuditSha256": "0c810137c44654d5e8ef9b2580ad125709d961846e7628387aa16226cdd8c584", + "sourceAuditSha256": "f895772a73b4810ce6489cdb1ff3c6296b543a6e739c5abb02802f018b4c7f4d", "featureCoverageSha256": "2d4e47ec18688c911ce4d6bda780edc8ee654069aa5704e15a39cbae35655ba7", "coverageWitnessesSha256": "2b2d5d57daacba3ecd3637f5a917d58b0b63fcc88893e651cd602cdba1ef4244", "profilesSha256": "9df8285820e4fff65f6a7753885bbb192c09f3f476eac8f9c98d130454ae1a28" diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index c474a120..db01f4e5 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -1084,7 +1084,7 @@ "reviewedGuides": [ { "path": "formal/README.md", - "sha256": "7ad4d77aa162e93e8def416fb545c29586532138ffd2d2c68c6213a1bab7a23f", + "sha256": "9cc60b22aa7bea2e65d79ecb98befa48829c636547144ac1a70d846988f2f505", "entries": [ {"line":1,"title":"Executable DialCache specification"}, {"line":10,"title":"Start with your task"}, @@ -1092,8 +1092,8 @@ {"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", @@ -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", @@ -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"}, @@ -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"}, @@ -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"}, @@ -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"}, @@ -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", @@ -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"}, @@ -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"}, @@ -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"}, @@ -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"}, @@ -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", @@ -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", diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index c42acaa8..7681f47d 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -4,8 +4,8 @@ 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 @@ -13,7 +13,8 @@ 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. @@ -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 @@ -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 diff --git a/formal/guides/BEHAVIOR.md b/formal/guides/BEHAVIOR.md index 3d0b36bf..526877d5 100644 --- a/formal/guides/BEHAVIOR.md +++ b/formal/guides/BEHAVIOR.md @@ -1,6 +1,6 @@ # Portable behavioral scenarios and generated feature profiles -[`behavioral-scenarios.json`](../catalogs/behavioral-scenarios.json) specifies deterministic feature scenarios independently of TypeScript. [`dialcache-effects-conformance.qnt`](../models/dialcache-effects-conformance.qnt) generates additional races using the same driver operations. Together with the [core profile](./CONFORMANCE.md) and [protocol vectors](../catalogs/protocol-vectors.json), these are executable contracts for implementation tests and language ports. The core profile is the introductory one and stays uncomposed from the kernel library: its drivers read the model's private state fields as their observation, so composing it is a driver-contract change in both ports. +[`behavioral-scenarios.json`](../catalogs/behavioral-scenarios.json) specifies deterministic feature scenarios independently of TypeScript. [`dialcache-effects-conformance.qnt`](../models/dialcache-effects-conformance.qnt) generates additional races using the same driver operations. Together with the [core profile](./CONFORMANCE.md) and [protocol vectors](../catalogs/protocol-vectors.json), these are executable contracts for implementation tests and language ports. The core profile is the introductory one and stays uncomposed from the kernel library: its drivers read the model's private state fields as their observation, so composing it is a driver-contract change in every port. The deterministic corpus currently contains 244 scenarios across 12 behavior families. It includes request-scope lifetime, coalescing, both read and fallback deadlines, local TTL/LRU, runtime snapshots, layer precedence, cache failures, tracked invalidation, frame age/retention, stale recovery, and shadow validation. These scenarios are test-derived contracts, **not Quint-generated traces**. The effects model generates interleavings of calls, loader settlement, clock observations, native writes, and invalidation. Recovery, policy, and shadow models generate further feature schedules through the same driver; their bounds and action mappings appear below. Keeping these complementary forms avoids a single model containing every feature combination. The [feature map](./FEATURE-COVERAGE.md) relates the scenarios to the full reviewed behavioral, protocol, and native inventory. @@ -8,7 +8,7 @@ The corpus includes interaction regressions for scope closure during recovery, r Full validation below means `make formal` locally or the manual/weekly full workflow. It regenerates and replays every scheduled history and checks the -required witnesses in both languages. Fast PR checks use committed smoke, +required witnesses in every port. 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 @@ -198,7 +198,7 @@ After every step, replay compares actual caller outcomes, loader/read/write/inva Full validation exports 512 traces from 4,096 samples, up to 60 transitions, and requires all actions plus 95 witnesses covering abandoned source/read settlement, independent budgets, late settlement guards, application-owned phases, acquired snapshots across invalidation, failure-specific publication, clock rollback at the second fence check, and observer failure isolation. Scheduled deterministic regressions anchor their declared boundaries; [execution.json](../catalogs/execution.json) distinguishes model checks from exported replays. Sampling favors the narrow rollback-during-publication boundary as well as unrestricted clock changes; it does not restrict that behavior to the favored schedule. -Full validation runs all profiles in `execution.json` through TypeScript and Go. PR checks run the committed subset alongside ordinary tests. Committed ITF smokes run without Quint. Failure diagnostics include trace, step, action, and both observations. The effects choice/state schema and scope/policy value choices changed with this specification revision; ports must select a matching revision and reject unsupported actions or choices. Behavioral scenario schema 2 is unchanged. +Full validation runs all profiles in `execution.json` through TypeScript, Go, Rust and Python. PR checks run the committed subset alongside ordinary tests. Committed ITF smokes run without Quint. Failure diagnostics include trace, step, action, and both observations. The effects choice/state schema and scope/policy value choices changed with this specification revision; ports must select a matching revision and reject unsupported actions or choices. Behavioral scenario schema 2 is unchanged. The queued adapter choices are: 1 null, 2 primitive, 3 legacy watermark shape, 4 kindless metadata, 5 missing miss reason, 6 unknown reason, 7 unknown reason with valid future fence, 8 fenced reason without fence, 9 negative fence, 10 fractional fence, 11 unsafe fence, 12 absent reason with future fence, 13 expired reason with zero fence, 14 miss with stray frame fields, 15 valid frame with stray miss metadata, and 16 fenced reason with valid future fence. Future fences are the input wall clock plus 20 ms. Successful raw completion consumes the reply even when DialCache has abandoned that read; adapter failure leaves it queued. Ports with strongly typed replies may normalize these encodings at their input boundary, but must preserve the resulting miss/refill behavior. @@ -226,7 +226,7 @@ Call observations encode pending as 0, fixture values 1/2 as 1/2, source errors Dark-layers inputs use explicit effect ordinals and source indices. `beginCall` choices 0..9 encode key modulo two and context divided by two; `resolveLoader` choices 1..24 encode source index and value 1/2. Policy choices 0..8 select request/local layers, coalescing and dark-shadow admission, with remote serving always off. Seeds 0..11 select two keys and six frame classes; invalidation 0..3 selects a key and a 0/20 ms future buffer. `advance` accepts 1, 10 or 60000 ms, `rollbackWall` shifts wall time back 1000 ms, and each read/load/dump/write fault toggles 0/1. Version 2 adds `inspect` choices 0/1 for public process snapshots of either instance and `s.d.inspections`. The snapshot records instance, leader/follower counts, and oldest monotonic leader age; the model uses -1 for an idle age and the native projection uses null. Five exported histories require live counts, request/process follower separation, oldest-leader replacement, instance isolation, wall rollback independence, cleanup on success/error/timeout, and exclusion of unfinished shadow or abandoned raw work. Served shadow work and the caller's own held write beside its held read remain outside this profile. -The dark-layers native replay settled one diagnostics rule against the TypeScript reference: an active local layer attributes its failed source to `local` even inside a request memo; without a shared layer, a transient request attributes it to `request_local`. Named public histories pin both cases in TypeScript and Go. +The dark-layers native replay settled one diagnostics rule against the TypeScript reference: an active local layer attributes its failed source to `local` even inside a request memo; without a shared layer, a transient request attributes it to `request_local`. Named public histories pin both cases in every port. Recovery opens contexts 0 and 1 in every fixture. New calls use open contexts; the separate scope profile covers detached calls after closure. Request misses may join the same process flight, after which each attached open context memoizes its result. A same-request follower records request coalescing; a new request records process coalescing. Recovered values have no shared-cache publication. Closing a context clears its memo and prevents late recovery from populating it. Four required witnesses include a recovered memo hit, later probes of both requests after shared recovery, a new read after closed-scope recovery, and request followers sharing recovery work. Three deterministic regressions anchor these cases. @@ -422,4 +422,4 @@ The committed `admission-smoke.itf.json` retains actions, choices, and observati 4. Replay the same core, pending-effect, scope, recovery, policy, shadow, admission, layers, and independent ITF corpora used by TypeScript. 5. Report passing behavior families, specification revision, seed, bounds, and tool versions. -Passing covers the supplied observations and scenarios. It does not establish every feature interaction, fairness/liveness, arbitrary resource limits, or all external failures. The Go driver executes this same feature interface and generated corpus. Its native concurrency gates and source-ownership monitor use actual callbacks and contexts, while expected model state remains assertion-only. See [`TEST-MAP.md`](./TEST-MAP.md) for the remaining boundaries. +Passing covers the supplied observations and scenarios. It does not establish every feature interaction, fairness/liveness, arbitrary resource limits, or all external failures. The Go, Rust and Python drivers execute this same feature interface and generated corpus. Go's native concurrency gates and source-ownership monitor use actual callbacks and contexts, while expected model state remains assertion-only. See [`TEST-MAP.md`](./TEST-MAP.md) for the remaining boundaries. diff --git a/formal/guides/CONFORMANCE.md b/formal/guides/CONFORMANCE.md index b8c04045..8b339a71 100644 --- a/formal/guides/CONFORMANCE.md +++ b/formal/guides/CONFORMANCE.md @@ -1,6 +1,6 @@ # Core behavioral conformance profile -This document specifies the bounded `core` profile implemented by the TypeScript and Go replay drivers. Its model is `dialcache-conformance.qnt`; the full port target also requires the other profiles registered in [execution.json](../catalogs/execution.json). +This document specifies the bounded `core` profile implemented by the TypeScript, Go, Rust and Python replay drivers. Its model is `dialcache-conformance.qnt`; the full port target also requires the other profiles registered in [execution.json](../catalogs/execution.json). ## Trace format and trust boundary diff --git a/formal/guides/CONTRACTS.md b/formal/guides/CONTRACTS.md index ce102866..16b097d3 100644 --- a/formal/guides/CONTRACTS.md +++ b/formal/guides/CONTRACTS.md @@ -188,4 +188,4 @@ Each row identifies where the source's semantic rules land. Repeated tests in di When adding or changing a rule, place it in this inventory, name its implementation-test/doc evidence, and add the relevant portable scenario/vector/model or explain its binding/assumption/exclusion boundary. Do not copy expected model state into execution or call a host-specific test a portable trace. The three-state callback outcomes deliberately avoid building a second callback language. -The inventory accounts for the 12 reviewed feature families and the currently identified corners, not exhaustive state-space coverage. Metadata gates require every positive fixed scenario and protocol/invalidation vector to be assigned to a named case; native cases retain exact tests, adaptations, and explicit gaps. The remaining assurance work is broader multi-key/multi-instance and request-scope combinations, larger mixed dark/served capacity schedules, larger generated interaction domains, and additional optional integration profiles. Go now executes every generated profile in `execution.json`, all fixed scenarios and protocol groups, plus real Redis/Valkey/Cluster interoperability. Generated coverage includes core, effects, request scopes, recovery, policy/storage, dark shadow validation, served-hit admission, layer composition, and independent callers; passing these plus the fixed corpus does not certify arbitrary interleavings, all malformed host values, fairness, performance, or every external fault. No percentage of behavioral completeness or universal certification is claimed. Measured code execution coverage is reported separately in `TEST-MAP.md`. +The inventory accounts for the 12 reviewed feature families and the currently identified corners, not exhaustive state-space coverage. Metadata gates require every positive fixed scenario and protocol/invalidation vector to be assigned to a named case; native cases retain exact tests, adaptations, and explicit gaps. The remaining assurance work is broader multi-key/multi-instance and request-scope combinations, larger mixed dark/served capacity schedules, larger generated interaction domains, and additional optional integration profiles. Go, Rust and Python now execute every generated profile in `execution.json`, all fixed scenarios and protocol groups, plus real Redis/Valkey/Cluster interoperability. Generated coverage includes core, effects, request scopes, recovery, policy/storage, dark shadow validation, served-hit admission, layer composition, and independent callers; passing these plus the fixed corpus does not certify arbitrary interleavings, all malformed host values, fairness, performance, or every external fault. No percentage of behavioral completeness or universal certification is claimed. Measured code execution coverage is reported separately in `TEST-MAP.md`. diff --git a/formal/guides/FEATURE-COVERAGE.md b/formal/guides/FEATURE-COVERAGE.md index ab8f3128..d0626323 100644 --- a/formal/guides/FEATURE-COVERAGE.md +++ b/formal/guides/FEATURE-COVERAGE.md @@ -8,7 +8,7 @@ input or combination of features. Quint defines the portable state transitions and their independently checked properties. Generated histories exercise those transitions through the real -TypeScript and Go implementations. Fixed scenarios preserve narrow examples; +TypeScript, Go, Rust and Python implementations. Fixed scenarios preserve narrow examples; wire vectors and native tests cover boundaries that need different evidence. Use [CONTRACTS.md](./CONTRACTS.md) for the obligations and [AUTHORING.md](./AUTHORING.md) to read or extend their models. @@ -163,7 +163,7 @@ only after that raw effect settles. Shadow-read-deadlines separately exercises C0/C1 read expiry, cancellation and raw-capacity retention, including both read/job deadline orderings. Confirmation keeps its admitted read budget after a runtime change and starts that budget at its own dispatch. These histories -replay in both ports; a whole-job timeout alone does not establish a read deadline. +replay in every port; a whole-job timeout alone does not establish a read deadline. Those additions do not enumerate arbitrary request trees, operation/key/instance sets, capacities or simultaneous failures. The short shadow job budget limits diff --git a/formal/guides/PORTING.md b/formal/guides/PORTING.md index 18d17402..093df597 100644 --- a/formal/guides/PORTING.md +++ b/formal/guides/PORTING.md @@ -8,7 +8,8 @@ The specification is experimental and versioned in [profiles.json](../catalogs/p Pin a repository commit and corpus when developing a port. Start with the [worked walkthrough](./WALKTHROUGH.md) to follow one source -deadline contract from a Quint regression to its TypeScript, Go and Rust assertions. +deadline contract from a Quint regression to its TypeScript, Go, Rust and Python +assertions. Then use this guide to implement the remaining profiles and completion reports. ## What a port supplies @@ -17,12 +18,13 @@ Supply a native implementation, a controlled test environment, a driver for the shared commands, and assertion results in the completion format below. The shared [replay coordinator](../replay/coordinator.mjs) owns profile parsing, action mappings and observation assertions. TypeScript imports those same -modules; Go and Rust use a persistent Node process over JSON lines. A new port can +modules; Go, Rust and Python use a persistent Node process over JSON lines. A new port can reuse that protocol instead of translating every profile's tables. Existing implementations are examples: [the TypeScript driver](../../typescript/test/formal/behavior-driver.ts), -[the Go driver](../../go/behavior_driver_test.go) and -[the Rust driver](../../rust/tests/formal/driver.rs). A port need not copy their public +[the Go driver](../../go/behavior_driver_test.go), +[the Rust driver](../../rust/tests/formal/driver.rs) and +[the Python driver](../../python/tests/formal/driver.py). A port need not copy their public API names, threading model, internal storage, or scheduling implementation. | Driver operation | Required behavior | @@ -34,7 +36,7 @@ API names, threading model, internal storage, or scheduling implementation. | External effects | Hold/release actual policy, Redis read/write, serialization, and decoding operations by their invocation IDs. A held operation cannot finish until its external release or specified failure. | | Clock control | Control wall time and elapsed time separately. Advance or shift only the specified clock; follow the profile's timer-delivery rule. Preserve fractional units in the local-clock profile. | | Storage inputs | Seed the specified bytes/value/TTL or execute invalidation. The adapter must expose the requested atomic primary snapshot and maintenance result. | -| Settle | After every command, bring the implementation to quiescence under the `causally-ready-v1` contract: every task spawned by the implementation or the driver has finished or is blocked on a driver-owned gate, a driver-owned timer that is not yet due, or a driver-owned scope gate, and nothing is runnable. This obligation falls on the library as well as the test: it must expose its detached scheduling to the test executor (Go's `Defer` hook drained under `synctest.Wait`, the Node fake-timer microtask queue drained by `advanceTimersByTimeAsync(0)`) so the driver reaches quiescence without guessing turn counts or advancing deadline time. The coordinator checks this contract by name on every behavior `observe` through the driver's settlement receipt, rules R1 to R5 in the [trace and observation contract](#trace-and-observation-contract); a failed rule is a `Settlement violation`, an infrastructure error that earns no comparison credit. Both ports include a no-settle control: [formal-settlement-control.test.ts](../../typescript/test/formal-settlement-control.test.ts) skips the TypeScript drain, and [settlement_control_replay_test.go](../../go/settlement_control_replay_test.go) reports the Go observation held before the drain; each must fail with a settlement violation, never an observation mismatch, on the smoke history of every behavior-driver profile. A further port carries an equivalent control against its own driver. | +| Settle | After every command, bring the implementation to quiescence under the `causally-ready-v1` contract: every task spawned by the implementation or the driver has finished or is blocked on a driver-owned gate, a driver-owned timer that is not yet due, or a driver-owned scope gate, and nothing is runnable. This obligation falls on the library as well as the test: it must expose its detached scheduling to the test executor (Go's `Defer` hook drained under `synctest.Wait`, the Node fake-timer microtask queue drained by `advanceTimersByTimeAsync(0)`) so the driver reaches quiescence without guessing turn counts or advancing deadline time. The coordinator checks this contract by name on every behavior `observe` through the driver's settlement receipt, rules R1 to R5 in the [trace and observation contract](#trace-and-observation-contract); a failed rule is a `Settlement violation`, an infrastructure error that earns no comparison credit. Every port includes a no-settle control: [formal-settlement-control.test.ts](../../typescript/test/formal-settlement-control.test.ts) skips the TypeScript drain, [settlement_control_replay_test.go](../../go/settlement_control_replay_test.go) reports the Go observation held before the drain, [settlement_control.rs](../../rust/tests/settlement_control.rs) skips the Rust drain, and `test_no_settle_control` in [test_conformance.py](../../python/tests/test_conformance.py) skips the Python settlement; each must fail with a settlement violation, never an observation mismatch, on the smoke history of every behavior-driver profile. A further port carries an equivalent control against its own driver. | | Observe | Read actual caller outcomes, source/effect counts, event order, timestamps, values and error categories after the step. Collect observations independently of expected model state. | | Cleanup | Drain or release test-owned work, restore clock/fault hooks, and isolate the next history. Unfinished work must not silently leak into another history. | @@ -334,7 +336,7 @@ from the repository root: ```sh make check # Fast native checks and committed smoke; not full acceptance. -make formal # Quint model/corpus checks, then prepared TS, Go and Rust replay. +make formal # Quint model/corpus checks, then prepared TS, Go, Rust and Python replay. make model-check # Separate finite symbolic checks; requires Java 21 and tar. make mutations # Measures every fault catalog over the generated corpus. make integration # Real-server interoperability; requires Docker. @@ -345,8 +347,9 @@ including symbolic checks and the exact Node 22.15.0 package floor. `make formal-check` runs the Quint evidence lane (every scheduled model, its public regressions and the model mutation challenges); the aggregate requires it, but the port lanes do not wait for it. `make formal-generate` produces the -full corpus and the shared witness evidence; `make formal-ts`, `make formal-go` -and `make formal-rust` each prepare and complete one port's run against them. The +full corpus and the shared witness evidence; `make formal-ts`, `make formal-go`, +`make formal-rust` and `make formal-python` each prepare and complete one port's +run against them. The parity and mutation lanes depend only on the generated corpus and shared witness evidence and run in parallel in hosted CI, whose aggregate requires all of them. These are the same entry points used by hosted CI. @@ -359,7 +362,7 @@ complete inventory. A green smoke lane supplies no full-parity claim. Print the current required IDs with `node formal/tools/conformance.mjs inventory`. The commands below describe the lower-level completion API for implementers of another port; the Make -targets already orchestrate it for TypeScript, Go and Rust. +targets already orchestrate it for TypeScript, Go, Rust and Python. The shared inventory contains stable language-neutral IDs: @@ -376,7 +379,7 @@ the exact inventory; a passing smoke test cannot substitute for a scheduled history. Witness gates establish reachability across the corpus and are separate from implementation assertions. `make formal-generate` evaluates them once with the shared `node formal/tools/witnesses.mjs evaluate` command described under -[Witness evidence](#witness-evidence). Go and Rust consume that evidence after +[Witness evidence](#witness-evidence). Go, Rust and Python consume that evidence after checking its exact corpus and definition hashes; TypeScript checks the same witness gate. Each port independently executes and asserts every history. @@ -387,6 +390,7 @@ Then prepare a separate context before each port's native tests: node formal/tools/conformance.mjs prepare typescript .formal-traces/ts-context.json node formal/tools/conformance.mjs prepare go .formal-traces/go-context.json node formal/tools/conformance.mjs prepare rust .formal-traces/rust-context.json +node formal/tools/conformance.mjs prepare python .formal-traces/python-context.json ``` Each port can prepare, replay and validate independently once those shared @@ -395,7 +399,7 @@ corpus and witness evidence unchanged between preparation and completion. Hosted CI runs the lanes in separate jobs; a local checkout must also keep their output paths distinct and avoid regenerating shared inputs while replays are running. -TypeScript, Go and Rust have built-in default source inventories. For another +TypeScript, Go, Rust and Python have built-in default source inventories. For another language, supply a JSON array containing every repository-relative implementation, driver, adapter, dependency-lock and test-configuration file that affects execution: @@ -408,22 +412,25 @@ These commands do not run the implementation. They record a unique run ID, preparation time, specification/source fingerprints, the exact corpus bytes, and the required case inventory. A port's source manifest is a reviewed input declaration; the checker cannot discover an omitted native dependency itself. -The Go and Rust default inputs also include the shared source/fixture -definitions and the evaluated witness JSON under -`.formal-traces/go-parity-witnesses/`. Another port that consumes auxiliary +The Go, Rust and Python default inputs include the evaluated witness JSON under +`.formal-traces/go-parity-witnesses/`; the Go and Rust inputs also include the +shared source/fixture definitions. Another port that consumes auxiliary evidence must include those files in its input manifest. Run native tests with complete trace directory selectors. Preserve the original assertion report and its timestamps. The supplied report adapters accept -Vitest JSON, `go test -json` and the Rust harness's JSON-lines report: +Vitest JSON, `go test -json` and the Rust harness's and Python runner's JSON-lines +reports: ```sh node formal/tools/conformance-adapters.mjs typescript .formal-traces/ts-replay.json .formal-traces/ts-context.json > .formal-traces/ts-completion.json node formal/tools/conformance-adapters.mjs go .formal-traces/go-replay.jsonl .formal-traces/go-context.json > .formal-traces/go-completion.json node formal/tools/conformance-adapters.mjs rust .formal-traces/rust-replay.jsonl .formal-traces/rust-context.json > .formal-traces/rust-completion.json +node formal/tools/conformance-adapters.mjs python .formal-traces/python-replay.jsonl .formal-traces/python-context.json > .formal-traces/python-completion.json node formal/tools/conformance.mjs check .formal-traces/ts-completion.json .formal-traces/ts-context.json node formal/tools/conformance.mjs check .formal-traces/go-completion.json .formal-traces/go-context.json node formal/tools/conformance.mjs check .formal-traces/rust-completion.json .formal-traces/rust-context.json +node formal/tools/conformance.mjs check .formal-traces/python-completion.json .formal-traces/python-context.json ``` Another language emits the same JSON completion schema: `schemaVersion: 1`, diff --git a/formal/guides/SEMANTIC-COVERAGE.md b/formal/guides/SEMANTIC-COVERAGE.md index 0c78220f..8e8da0a7 100644 --- a/formal/guides/SEMANTIC-COVERAGE.md +++ b/formal/guides/SEMANTIC-COVERAGE.md @@ -19,7 +19,7 @@ The checker reports these distinct categories: | Model | A cited invariant scheduled in [execution.json](../catalogs/execution.json) or a run declared by a scheduled model | | Portable | Fixed scenarios, witnesses, exported Quint regressions or wire vectors | | Generated witness | A required consequential history in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) | -| Quint regression replay | A named public-action regression exported and replayed in both ports | +| Quint regression replay | A named public-action regression exported and replayed in every port | | Quint vector replay | Expected primitive outputs exported from a scheduled Quint model | | Quint-driven | The union of the preceding three Quint execution categories | @@ -38,7 +38,7 @@ check is scheduled and that a cited definition is an action, def or val of a scheduled model or library rather than a scheduled property; it cannot automate the semantic judgment in the scope text. Generated witness reachability and implementation replay are recorded separately: a citation alone does not -establish that a witness was reached or that both implementations passed. Weak +establish that a witness was reached or that every implementation passed. Weak accounting checks such as policy `hitsSkipSource` (loaders <= callers), recovery `singleReadPerFlight` (reads <= callers) and age-sample counts are not treated as proofs of hit traversal, single execution or sample time. No general @@ -82,7 +82,7 @@ histories against those records. | Finite symbolic rule checks | Every decision in the declared finite domain satisfies the independently stated property | | Sampled connection checks | Explored profile histories preserve the selected snapshot, timing and ownership contracts | | Compiling model mutations | The named property detects that deliberate semantic change to a transition | -| Exported boundary regressions | The exact public command sequence is checked in Quint and against both implementations | +| Exported boundary regressions | The exact public command sequence is checked in Quint and against every implementation | `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). @@ -101,7 +101,7 @@ invariant rejects that one deliberate change under the manifest bounds. Model receipts preserve the timestamp, captured policy and owner at acceptance. Every challenge is pinned by its `reproducer` to one deterministic history that passes clean and fails under the fault at a declared expectation, either -an exported public regression both ports replay or a documented model-only +an exported public regression every port replays or a documented model-only run. Missing reproducers fail validation. See the [authoring rules](./AUTHORING.md#challenging-every-model). Each challenge also carries a `nativeMutants` entry naming the TypeScript and @@ -114,7 +114,7 @@ explanation fails validation. See [mapping every challenge to native mutants](./AUTHORING.md#mapping-every-challenge-to-native-mutants). Ownership receipts, failed-read state, closed-scope memo cleanup and initial recovery retention have exact model checkpoints. The closed-scope and recovery -histories also use public inputs replayed by both ports, but their additional +histories also use public inputs replayed by every port, but their additional private-state assertions remain model evidence; they do not create native mutation coverage where later native checks hide the same internal fault. Boundary properties can challenge an eligibility helper by stating the @@ -161,14 +161,14 @@ results; fresh measurements belong with their exact source and corpus artifacts. Use the [shared Make targets and pinned prerequisites](../README.md#generating-and-replaying-behavior): ```sh -make formal # Regenerate and complete prepared TS, Go and Rust replay. +make formal # Regenerate and complete prepared TS, Go, Rust and Python replay. make mutations # Measure every fault catalog over the generated corpus. ``` `make mutations-ts`, `make mutations-go` and `make mutations-rust` depend only on the corpus produced by `make formal-generate` and its shared witness evidence, not on any port's completion report. Hosted CI runs the three -mutation lanes in parallel with the three parity lanes off one generation job; +mutation lanes in parallel with the four parity lanes off one generation job; the aggregate requires all of them. Each report records the source, corpus and witness fingerprints it measured. Raw measurement programs remain `measure-semantics.mjs`, `measure-go-semantics.mjs` and @@ -241,9 +241,9 @@ with source fingerprints, tools and bounds, and fingerprints `execution.json` as `catalogSha256` in its report. This measures the specification separately from implementation mutation detection. -Every effects replay also runs `assertEffectsHistory` over actual external source starts/settlements and public fallback/write observations. Its C23/C25/C26 checks cover source-relative budget/duration, strict deadline acceptance, and a preceding accepted success before publication. It consumes no expected model phases and permits pending prefixes. An additional causal monitor in both drivers ties writes to their actual invocation/source callback and rejects publication after that source settled too late; negative tests distinguish property failures from malformed monitor inputs. This is a bounded connection for selected properties, not full model refinement or liveness proof. +Every effects replay also runs `assertEffectsHistory` over actual external source starts/settlements and public fallback/write observations. Its C23/C25/C26 checks cover source-relative budget/duration, strict deadline acceptance, and a preceding accepted success before publication. It consumes no expected model phases and permits pending prefixes. An additional causal monitor in the TypeScript, Go and Rust drivers ties writes to their actual invocation/source callback and rejects publication after that source settled too late; negative tests distinguish property failures from malformed monitor inputs. This is a bounded connection for selected properties, not full model refinement or liveness proof. -The Go driver executes the same generated corpus through its own cache implementation. Its value-domain and API adaptations appear in [`go/README.md`](../../go/README.md). `measure-go-semantics.mjs` independently measures the Go fault catalog; TypeScript mutation results are never credited to Go. The Go race detector covers only exercised schedules. +The Go driver executes the same generated corpus through its own cache implementation. Its value-domain and API adaptations appear in [`go/README.md`](../../go/README.md). `measure-go-semantics.mjs` independently measures the Go fault catalog; TypeScript mutation results are never credited to Go. The Go race detector covers only exercised schedules. The Rust and Python drivers execute the same corpus through their own implementations; Rust's mutation campaign uses its separate catalog, and Python has none. Generated invalidation vectors also run inside both standard native mutation diff --git a/formal/guides/SPEC.md b/formal/guides/SPEC.md index 6a3ffe3e..926c2ba6 100644 --- a/formal/guides/SPEC.md +++ b/formal/guides/SPEC.md @@ -78,7 +78,7 @@ wire transforms; fixed vectors and native tests retain the remaining boundaries. For a portable behavior change, update Quint first, retain an independent property and a consequential witness or exported public-action regression, then replay the same histories in -TypeScript and Go. Prose and implementation must follow that reviewed contract. +TypeScript, Go, Rust and Python. Prose and implementation must follow that reviewed contract. A discovered disagreement is resolved explicitly in Quint with a distinguishing regression; existing implementation behavior is evidence to investigate, not an alternative oracle. Case-ledger gaps remain visible until their behavior has @@ -280,7 +280,7 @@ and binding responsibilities. A report identifies specification revision, implementation revision, supported profiles and vector groups, tool versions, seed, bounds, and exact corpus. It must list unsupported features. [`profiles.json`](../catalogs/profiles.json) registers the -profile formats and both implementations' declared coverage. Both ports must check every registered +profile formats and each implementation's declared coverage. Every port must check every registered profile, sampled history, exported regression and wire artifact, with separate real Redis/Valkey/Cluster interoperability evidence. A claim requires those current-revision checks; passing one profile does not imply the others. @@ -288,10 +288,10 @@ passing one profile does not imply the others. The source-deadline verification model and the actual-effects history monitor check selected C23/C25/C26 properties: source-relative duration and full budget, strictly pre-deadline success acceptance, and publication requiring a preceding -accepted success. A second monitor in both drivers associates each dispatched -write with its actual source callback and invocation context, then requires -that exact source to have succeeded before its own deadline. It reads no -expected model state. Negative checks distinguish a late source, another +accepted success. A second monitor in the TypeScript, Go and Rust drivers +associates each dispatched write with its actual source callback and invocation +context, then requires that exact source to have succeeded before its own +deadline. It reads no expected model state. Negative checks distinguish a late source, another invocation's source, and valid publication after an accepted source's deadline. This necessary condition does not prove payload provenance, refill fences, or all publication authority; those have their own replay observations. Pending prefixes diff --git a/formal/guides/TEST-AUDIT.md b/formal/guides/TEST-AUDIT.md index a54b0242..9406734a 100644 --- a/formal/guides/TEST-AUDIT.md +++ b/formal/guides/TEST-AUDIT.md @@ -65,6 +65,6 @@ binds these guide reviews without counting them as additional Go tests. All inventoried sources have an explicit disposition. This does **not** mean all Vitest assertions are formalized or every implementation branch is exercised by portable replay. Local storage failure consequences now have Quint-driven replay in the `local-failure` profile, using native storage/clock fault seams to observe caller results and later publication. The seam is a driver capability, not a new public library API. Exporter schemas/registries, exact JSON logging truncation, compression implementation/resource ceilings, transport/connection lifecycle, and TypeScript API/type/Promise details still use the documented B/E/X boundaries. Porting those integrations requires their own checks. -Within the portable scope, the inventory now names 60 behavioral and nine protocol obligations with executable evidence. Remaining assurance work includes larger mixed-feature histories, broader generated exploration, and more combinations of source/codec/adapter faults. The Go implementation now replays every profile in `execution.json`, fixed scenarios and protocol groups, with separate real interoperability tests. No finite source inventory or sampled trace count proves semantic completeness. +Within the portable scope, the inventory now names 60 behavioral and nine protocol obligations with executable evidence. Remaining assurance work includes larger mixed-feature histories, broader generated exploration, and more combinations of source/codec/adapter faults. The Go, Rust and Python implementations now replay every profile in `execution.json`, fixed scenarios and protocol groups, with separate real interoperability tests. No finite source inventory or sampled trace count proves semantic completeness. The [semantic coverage measurement](./SEMANTIC-COVERAGE.md) refines those broad obligations into named cases and checks explicit evidence links. Its isolated mutation comparison challenges actual assertions and reports ordinary/generated/portable detection separately. Full disposition of source declarations must not be confused with universal generated coverage: the finer inventory records each case's checked scope and remaining finite limits. The [historical baseline](./VALIDATION.md#historical-results) preserves the completed mutation measurements and survivors. [Current validation](./VALIDATION.md) describes how to produce fresh evidence. diff --git a/formal/guides/TEST-MAP.md b/formal/guides/TEST-MAP.md index 10c0c5de..7198112b 100644 --- a/formal/guides/TEST-MAP.md +++ b/formal/guides/TEST-MAP.md @@ -18,7 +18,7 @@ validation workflow and report requirements. ## Behavioral map The verification models emphasize individual rules. Conformance profiles expose -public inputs that both implementations replay. Their current versions, bounds, +public inputs that every implementation replays. Their current versions, bounds, sampled trace counts and exported regressions live in [profiles.json](../catalogs/profiles.json) and [execution.json](../catalogs/execution.json). @@ -60,7 +60,7 @@ Six focused profiles close gaps without turning one model into the whole cache: | `source-budgets` | Held policy time does not spend the source budget; default, finite and unbounded calls, followers and disabled/key-error paths preserve their distinct deadlines | Each exportable regression invokes actual public model actions. Explicit -`input: { name, choice }` survives Quint test export and drives both ports. +`input: { name, choice }` survives Quint test export and drives every port. Expected state supplies assertions only. Native local-failure and local-clock seams control the environment while exercising real cache behavior; they do not add production fault APIs or redefine the model's expected outcome. @@ -126,6 +126,6 @@ from parser, classifier and deliberately broken-driver controls. measurements; historical run results live in PR summaries and workflow artifacts. When behavior disagrees, review the intended contract, change Quint with an -independent regression, replay it in both ports, and update explanatory docs and +independent regression, replay it in every port, and update explanatory docs and case mappings. A formal model is authoritative only within its declared scope; its notation does not remove the need to review the actual consequence. diff --git a/formal/guides/VALIDATION.md b/formal/guides/VALIDATION.md index 1b810869..9fd0ca2b 100644 --- a/formal/guides/VALIDATION.md +++ b/formal/guides/VALIDATION.md @@ -9,9 +9,9 @@ lists tool prerequisites and focused reproduction commands. | 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/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 | +| Challenge implementation assertions | `make mutations` | Compiling semantic faults tested against the TypeScript, Go and Rust suites; Python has no mutation campaign | | Real server behavior | `make integration` | Redis, Valkey, Cluster and cross-language interoperability | | Explore another schedule sample | `make explore` | Separate source snapshot, recorded random seed, every port's replay | | Check composed profiles against their previous text | `make differential` | Lint baseline, then both-direction replay against the merge base with `origin/main`; fails on any disagreement or trace growth above the model's bound | @@ -25,8 +25,8 @@ It produces nothing the port lanes consume, so the hosted workflow runs it as a immediately after generation, before any port replays. That shared, language-neutral step is the sole producer of `.formal-traces/go-parity-witnesses/`; the TypeScript suite only checks the same gate. `make formal-ts`, `make formal-go`, -`make formal-rust`, `make mutations-ts`, `make mutations-go` and -`make mutations-rust` depend only on the generated corpus +`make formal-rust`, `make formal-python`, `make mutations-ts`, `make mutations-go` +and `make mutations-rust` depend only on the generated corpus and that witness evidence, so the hosted workflow runs them in parallel and the aggregate requires all of them. @@ -189,7 +189,8 @@ Its separate catalog and evidence scope are described in report for authoring; it is never complete evidence. The workflow's `formal-full` aggregate job retains a small `formal-summary` artifact for 90 -days: every port's completion and context reports, the Go replay summary, the model +days: every port's completion and context reports, the Go, Rust and Python replay +summaries, the model properties `report.json` from the `check-models` job, the symbolic `report.json` and, on scheduled or exploration runs, each exploration `report.json`. Trace corpora, model check counterexamples and mutation evidence keep the 14-day @@ -220,8 +221,8 @@ The weekly full workflow runs this lane alongside pinned validation. Exploration does not produce an acceptance completion: its separate report distinguishes native replay failures, witness-check failures and other infrastructure failures. A witness-check failure can mean an unreached boundary or invalid witness -evidence; inspect the native report before attributing it to sampling. Go replay -still runs after a TypeScript witness-check failure. The exploration report +evidence; inspect the native report before attributing it to sampling. The Go, Rust and +Python replays still run after a TypeScript witness-check failure. The exploration report keeps that seed's witness report under `witnesses`. The witness step itself is tolerated so every port replays, but its baseline gate decides the outcome afterwards: when every required label is present and all ports pass yet a diff --git a/formal/guides/WALKTHROUGH.md b/formal/guides/WALKTHROUGH.md index 368a8bdc..60517a1c 100644 --- a/formal/guides/WALKTHROUGH.md +++ b/formal/guides/WALKTHROUGH.md @@ -65,7 +65,7 @@ other allowed choices. Each transition records its external command in flowchart LR Q[Quint history] --> I[Recorded external input] Q --> P[Predicted observation] - I --> D[TypeScript, Go or Rust driver] + I --> D[TypeScript, Go, Rust or Python driver] D --> C[Real DialCache API] C --> O[Actual results and effects] P --> A[Compare observations] @@ -84,10 +84,12 @@ using the published mapping, rather than supplying the predicted call result. | TS real API execution | [behavior-driver.ts](../../typescript/test/formal/behavior-driver.ts), `BehaviorDriver.apply` and `snapshot` | | Go real API execution | [behavior_driver_test.go](../../go/behavior_driver_test.go), `behaviorDriver.apply` and `observation` | | Rust real API execution | [driver.rs](../../rust/tests/formal/driver.rs), `Driver::apply` and `Driver::observation` | +| Python real API execution | [driver.py](../../python/tests/formal/driver.py), `BehaviorDriver.apply` and `observe` | | Shared projection and per-step assertion | [features.mjs](../replay/features.mjs), `projectObservation` and `assertFeatureObservation` | | TS replay | [formal-features.test.ts](../../typescript/test/formal-features.test.ts), `replay` | | Go replay transport | [feature_replay_test.go](../../go/feature_replay_test.go), `TestFeatureConformance`, and [replay_coordinator_test.go](../../go/replay_coordinator_test.go) | | Rust replay transport | [conformance.rs](../../rust/tests/conformance.rs), `Run::replay_behavior`, and [transport.rs](../../rust/tests/formal/transport.rs), `Coordinator::execute` | +| Python replay transport | [run_conformance.py](../../python/tests/run_conformance.py), `_replay_case`, and [coordinator.py](../../python/tests/formal/coordinator.py), `Coordinator.replay` | The shared fixture installs a real cache with a local TTL and a held runtime-policy provider. Source loaders, policy replies and time are controlled at their @@ -157,11 +159,16 @@ DIALCACHE_FEATURE_TRACE_FILE="$PWD/.formal-traces/walkthrough/source-budgets/hel DIALCACHE_FEATURE_TRACE_FILE="$PWD/../.formal-traces/walkthrough/source-budgets/heldPolicyDoesNotSpendSourceBudgetTest.itf.json" \ cargo test --locked --all-features --test conformance ) + +node formal/tools/run-python-replay.mjs --profile=source-budgets \ + --trace=.formal-traces/walkthrough/source-budgets/heldPolicyDoesNotSpendSourceBudgetTest.itf.json ``` The Rust command selects this history for feature replay and skips fixed scenarios; its harness also runs the core/effects smoke histories and protocol -vectors. Keep Node 24 on `PATH` for the shared replay coordinator. +vectors. The Python runner replays only the selected history; it uses +`python/.venv` unless `PYTHON` names another prepared interpreter. +Keep Node 24 on `PATH` for the shared replay coordinator. These are focused debugging checks. They do not produce full acceptance or satisfy the complete witness inventory. After changing the rule or its driver,