diff --git a/.claude/skills/VENDORED.md b/.claude/skills/VENDORED.md new file mode 100644 index 000000000..fb5cfd725 --- /dev/null +++ b/.claude/skills/VENDORED.md @@ -0,0 +1,11 @@ +# Vendored skills + +`quint-lang/` and `quint-modeling/` are copied unchanged from the Quint LLM Kit, so every session uses the same pinned version. + +- Source: https://github.com/quint-co/quint-llm-kit, directory `quint-llm-kit-plugin/skills/` +- Commit: `cc75369f741af7d490936f82002c2d28e3b3d78d` (copied 2026-10-26) +- Licence: Apache-2.0, copied into each skill directory as `LICENSE` + +To update, copy both directories from a newer commit, keep the `LICENSE` files, update the commit above, and rerun `specs/quint/check.sh all`. +Put Proxy-specific rules in `proxy-quint/`, not in the vendored files. +The kit's third skill, `quint-execute-spec`, is not vendored, so `quint-modeling`'s pointers to it lead nowhere here. diff --git a/.claude/skills/proxy-quint/SKILL.md b/.claude/skills/proxy-quint/SKILL.md new file mode 100644 index 000000000..9d04f08a1 --- /dev/null +++ b/.claude/skills/proxy-quint/SKILL.md @@ -0,0 +1,45 @@ +--- +name: proxy-quint +description: Proxy's rules for its Quint models in specs/quint. Use when adding, changing or reviewing a .qnt model, check.sh or a recorded finding, or when changing Proxy's statement routing, Parse/Bind lifecycle, settings protocol or schema reload. +--- + +# Quint models in Proxy + +Read `specs/quint/README.md`, then the model's `requirements.md` and `verification.md`. +For Quint syntax and the CLI, use the `quint-lang` skill. +For modelling discipline and the spec review checklist, use the `quint-modeling` skill. +This skill holds only what is specific to Proxy, and wins where it differs from those two. + +## Running the checks + +- Iterate with `./check.sh` from `specs/quint`: typecheck, scenario tests, and simulation with every witness required to be reached. +- Before pushing a model change, run `./check.sh all` in the background (about 11 minutes) and wait for exit 0. TLC is part of Proxy's checks, unlike the kit's sampled-only workflow. +- Record the new state counts, timings and witness counts in `verification.md` in the same change. +- When you run `quint` yourself, use the pinned CLI (`npx --no-install quint` in `specs/quint`, or bare `quint` under mise) and pass `--backend typescript` to `run` and `test`: the default Rust backend downloads through the GitHub API, which cloud sessions block. + +## Changing a model + +1. Classify the change. A requirements change updates `requirements.md` and the model together, and the pull request description names each property it changes, for the reviewer to approve. +2. For an implementation change, the properties are fixed: a failing check means the model is wrong or Proxy has a finding. Fix the model, or record the finding. +3. When modelling a code path, follow every call from the handler that can refuse, rewrite or forward the message, through `Context` (every `begin_*`, `prepare_*` and `finish_*` hook) and `SettingsProtocol`, until it returns. The trace is done when every such function has a row in the model's source-file correspondence table. Add rows for new elements, and keep the file list in the `AGENTS.md` pointer in step with the table. Finding F3 was a false alarm because a hand trace stopped at the handler. +4. For a new rule in the model, add a mutation to `check.sh` that removes it, and confirm TLC catches it. `mutate` checks only the `asBuilt` instance and replaces the first match, so pick a pattern that occurs once, and extend `mutate` with an instance argument for a rule only another instance exercises. +5. For a new action, name it and call it directly from `step` (Quint Connect needs named actions), and add a witness that only that action can make true to the `simulate` list in `check.sh`. + +## Findings + +Record a counterexample as an unconfirmed finding, in four places: +- an entry under Findings in `requirements.md` +- an expected violation in `check.sh tlc` +- a row in `verification.md` +- a scenario test in the model's `*_test.qnt` that replays the trace + +It stays unconfirmed until a failing test against Proxy and PostgreSQL reproduces it. +Fix Proxy in a separate pull request, test first. + +## Changing Proxy's Rust code + +When a change touches a function in a model's source-file correspondence table, update the model and rerun `./check.sh all` in the same change, or say in the pull request why the model is unaffected. + +## Public repository + +The model files are public, so refer to other work in them by GitHub pull request number. diff --git a/.claude/skills/quint-lang/LICENSE b/.claude/skills/quint-lang/LICENSE new file mode 100644 index 000000000..08f754199 --- /dev/null +++ b/.claude/skills/quint-lang/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2026 Informal Systems Inc. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/.claude/skills/quint-lang/SKILL.md b/.claude/skills/quint-lang/SKILL.md new file mode 100644 index 000000000..792255e73 --- /dev/null +++ b/.claude/skills/quint-lang/SKILL.md @@ -0,0 +1,563 @@ +--- +name: quint-lang +description: > + Quint language and CLI reference — the expert on Quint syntax, operators, types, `basicSpells`, + the toolchain (typecheck/run/test/verify), and how to read simulation and counterexample output. + Use when writing or debugging the contents of a `.qnt` file, fixing a typecheck/parse error, + looking up an operator or idiom, analyzing an invariant violation or counterexample trace, or + optimizing state-space exploration. This is for working IN Quint at the language level — not for + analyzing or running TLA+/TLC itself. For building a NEW model end-to-end from some source — + including translating a TLA+ spec into Quint, or modeling code/requirements/an idea — use the + quint-modeling skill, which owns that workflow and consults this reference for syntax. Keywords: + quint, syntax, operators, typecheck, model checking, counterexample, basicSpells, CLI, + specification language. +--- +# Quint Language Reference + +Quint is an executable specification language for complex systems, developed by Informal Systems. It compiles to TLA+ and supports simulation and model checking. + +## Module structure + +```quint +module MyProtocol { + // type aliases, constants, state, actions, properties +} +``` + +Modules can import others: +```quint +import Voting.* // all definitions +import Voting(quorum) // specific definition +import Voting as V // namespace alias +``` + +--- + +## Types + +| Type | Description | Example | +|---|---|---| +| `int` | Integers | `-1, 0, 42` | +| `bool` | Booleans | `true, false` | +| `str` | Strings | `"hello"` | +| `Set[T]` | Finite set | `Set(1, 2, 3)` | +| `List[T]` | Ordered sequence | `List(1, 2, 3)` | +| `K -> V` | Key-value map (type is `K -> V`, **not** `Map[K, V]`) | value: `Map("a" -> 1)` | +| `(T1, T2)` | Tuple | `(1, "x")` | +| `{ f: T, g: U }` | Record | `{ x: 1, ok: true }` | +| `T \| U` | Sum (variant) | (use type alias) | + +Type aliases: +```quint +type NodeId = int +type Phase = Idle | Propose | Vote | Commit // enum — prefer over string literals +``` + +--- + +## Definitions + +```quint +// Module parameter — fixed at instantiation, not a state variable +const N: int +const Nodes: Set[str] + +// Pure function — no state access, usable anywhere +pure def max(a: int, b: int): int = if (a > b) a else b + +// Stateful operator — can read vars, takes arguments (unlike val) +def isActive(n: str): bool = active.contains(n) + +// State-reading value — can read vars, no arguments +val quorum: bool = votes.size() * 2 > nodes.size() + +// Compile-time constant +pure val N: int = 4 +val threshold: int = N / 2 + 1 +``` + +`const` vs `pure val`: `const` is a module parameter bound at instantiation (`import A(N = 3)`); `pure val` is a fixed expression computed once. `def` vs `val`: `def` takes arguments; `val` does not. + +--- + +## State variables + +```quint +type LocalState = { + leader: int, + phase: Phase, // enum (see Type aliases) — prefer over a bare str + votes: Set[int], + log: List[str], +} + +var localState: LocalState // cohesive local protocol state +var peers: int -> str // independent concern (peer metadata) +``` + +State variables can only be read in `val` definitions and actions; they cannot be read in `pure def`. + +--- + +## Actions + +Actions describe state transitions. They return `bool` — `true` if the action fires. + +```quint +action init: bool = all { + leader' = 0, + phase' = Idle, + votes' = Set(), + log' = List(), + state' = Map(), +} + +action propose(node: int): bool = all { + phase == Idle, + node > 0, + leader' = node, + phase' = Propose, + votes' = votes, + log' = log, + state' = state, +} +``` + +Key rules: +- Every `var` must be assigned in every action (use `x' = x` to leave unchanged). +- `all { ... }` — all sub-expressions must hold (conjunction). Guards are plain boolean expressions inside `all { }`. +- `any { ... }` — at least one must hold (disjunction); the REPL picks non-deterministically. + +--- + +## Non-determinism + +```quint +action step: bool = any { + propose(1), + propose(2), + vote, + timeout, +} + +// Non-deterministic choice from a set +action deliverMessage: bool = { + nondet msg = pending.oneOf() + all { + pending.size() > 0, + delivered' = delivered.union(Set(msg)), + pending' = pending.exclude(Set(msg)), + // ... other vars unchanged + } +} +``` + +--- + +## Set operators + +```quint +Set(1, 2, 3).contains(2) // true +Set(1, 2).union(Set(2, 3)) // Set(1, 2, 3) +Set(1, 2, 3).intersect(Set(2, 3)) // Set(2, 3) +Set(1, 2, 3).exclude(Set(2)) // Set(1, 3) +Set(1, 2, 3).filter(x => x > 1) // Set(2, 3) +Set(1, 2, 3).map(x => x * 2) // Set(2, 4, 6) +Set(1, 2, 3).fold(0, (acc, x) => acc + x) // 6 +Set(1, 2, 3).size() // 3 +Set(1, 2, 3).forall(x => x > 0) // true +Set(1, 2, 3).exists(x => x > 2) // true +1.to(5) // Set(1, 2, 3, 4, 5) +nondet x = Set(1, 2, 3).oneOf() // non-deterministic pick — only valid in nondet bindings +``` + +--- + +## List operators + +```quint +List(1, 2, 3).head() // 1 +List(1, 2, 3).tail() // List(2, 3) +List(1, 2, 3).length() // 3 +List(1, 2, 3).nth(1) // 2 (0-indexed) +List(1, 2, 3).append(4) // List(1, 2, 3, 4) +List(1, 2).concat(List(3, 4)) // List(1, 2, 3, 4) +List(1, 2, 3).foldl(0, (acc, x) => acc + x) // 6 +List(1, 2, 3).select(x => x > 1) // List(2, 3) +``` + +--- + +## Map operators + +```quint +Map("a" -> 1, "b" -> 2).get("a") // 1 +Map("a" -> 1).put("b", 2) // Map("a" -> 1, "b" -> 2) +Map("a" -> 1, "b" -> 2).keys() // Set("a", "b") +Set(1, 2, 3).mapBy(k => k * 2) // Map(1 -> 2, 2 -> 4, 3 -> 6) — set of keys → map +``` + +--- + +## Records + +Records group related fields into a named type. They are the primary tool for modelling structured state in Quint. + +### Type aliases for records + +```quint +type NodeState = { + phase: Phase, // enum: Idle | Propose | Vote | Commit + voted: bool, + log: List[int], +} + +type Message = { + from: int, + to: int, + round: int, + payload: str, +} +``` + +### Creating and accessing + +```quint +val n: NodeState = { phase: Idle, voted: false, log: List() } +n.phase // Idle +n.voted // false +``` + +### Updating (immutable — returns a new record) + +```quint +{ ...n, phase: Propose } // ✅ preferred — idiomatic, handles multiple fields +{ ...n, voted: true, phase: Vote } // ✅ multiple fields at once + +n.with("phase", Propose) // ⚠️ valid but non-idiomatic — field name is a string literal +``` + +### Records as state — when to group variables + +TLA+ specs typically flatten all state into independent top-level variables. Quint's type system lets you group them. **When fields describe one cohesive local state, make a record type and use a single state variable of that type.** + +**Group into a record when:** +- They represent the local state of a single actor (e.g. one node's phase + log + vote) +- They are always passed together as function arguments +- An invariant relates multiple fields of the same conceptual entity + +**Keep flat when:** +- The variables represent distinct concerns that change independently +- The component is simple and grouping adds no clarity +- The variables are intentionally in different ownership/lifecycle domains + +### Example: preferred grouped local state vs. anti-pattern + +**Preferred (cohesive local state):** +```quint +type LocalState = { + id: int, + phase: Phase, + est1: int, + est2: Option[int], // Option is from basicSpells, not built in — see Basic spells below + round: int, + crashed: bool, + leader: int, + received_messages: Set[Message], +} + +var localState: LocalState +``` + +**Avoid for cohesive local state:** +```quint +var id: int +var phase: Phase +var est1: int +var est2: Option[int] +var round: int +var crashed: bool +var leader: int +var received_messages: Set[Message] +``` + +**For N actors, use a map of grouped records:** +```quint +type LocalState = { phase: Phase, votedFor: int, log: List[int] } + +var nodes: int -> LocalState + +action commit(id: int): bool = { + val node = nodes.get(id) + all { + node.phase == Vote, + nodes' = nodes.put(id, {...node, phase: Commit}), + } +} +``` + +### Nested records + +```quint +type ClusterState = { + nodes: int -> NodeState, + leader: int, + epoch: int, +} + +var cluster: ClusterState + +// Read nested field: +cluster.nodes.get(1).phase + +// Update nested field (must rebuild from the inside out): +val updated = {...cluster.nodes.get(1), phase: Commit} +cluster' = {...cluster, nodes: cluster.nodes.put(1, updated)} +``` + +### Records in sets (messages, events) + +```quint +var inFlight: Set[Message] + +action send(src: int, dst: int, r: int, p: str): bool = all { + inFlight' = inFlight.union(Set({ from: src, to: dst, round: r, payload: p })), + // ... +} + +// Filter by field: +inFlight.filter(m => m.to == nodeId) +inFlight.exists(m => m.round == currentRound and m.payload == "vote") +``` + +--- + +## Sum types + +Sum types (variants) represent a value that can be one of several distinct cases. + +```quint +type Action = + | Propose({ value: int, proposer: int }) + | Vote({ value: int, voter: int }) + | Decide({ value: int }) +``` + +Each variant has a named constructor and carries one payload. A constructor takes exactly one argument — wrap multiple fields in a record (as above) or a tuple. + +Construct a value by calling the constructor: +```quint +val a: Action = Propose({ value: 1, proposer: 2 }) +``` + +Pattern-match with `match`, binding the payload: +```quint +pure def describeAction(a: Action): str = + match a { + | Propose(p) => "proposal" + | Vote(v) => "vote" + | Decide(d) => "decision" + } +``` + +Use `_` to ignore the payload when you only care which variant it is: +```quint +match a { + | Propose(_) => "proposal" + | _ => "other" +} +``` + +Use sum types when a message, event, or state can take structurally different forms — not just different values of the same type. + +--- + +## Enum types +Enum types are a special case of sum types where each case has no additional data. + +```quint +type Phase = Idle | Propose | Vote | Commit +var phase: Phase + +if (phase == Propose) { ... } +``` + +--- + +## Variable grouping — decision guide + +Before writing `var` declarations, answer these questions for each candidate group: + +| Question | Group → record if... | Keep flat if... | +|---|---|---| +| Do these vars always change together? | Yes, in most actions | No, they're independent | +| Do they describe the same entity? | Same node / same message / same round | Different concerns | +| Is there one instance or N instances? | Either one or N (group if cohesive; for N use `Id -> RecordType`) | Flat only when concerns are truly independent | +| Do invariants relate them? | Invariant spans multiple fields of one entity | Invariant uses vars independently | + +--- + +## Boolean operators + +```quint +not(p) // negation — Quint has no ! operator +p and q // conjunction +p or q // disjunction +p implies q // p => q (not(p) or q) +p iff q // p == q for booleans + +and { p1, p2, p3 } // block form — equivalent to p1 and p2 and p3 +or { p1, p2, p3 } // block form — at least one must hold +``` + +`and { }` and `or { }` are the same operators as `all { }` and `any { }` in actions — use whichever reads more naturally in context. + +--- + +## Invariants and temporal properties + +```quint +// Safety invariant — must hold in every reachable state +// @invariant +val noDuplicateLeader: bool = + leaders.size() <= 1 + +// Temporal property — evaluated over traces +// @temporal +temporal eventualProgress: bool = + eventually(committed.size() > 0) + +// Temporal operators +eventually(p) // p holds in some future state +always(p) // p holds in all future states +p.implies(q) // p => q +``` + +--- + +## Assume + +```quint +assume nodeCountPositive = N > 0 +assume quorumMajority = 2 * quorum > N +``` + +An `assume` states a premise about constants, but it is **not enforced** — a violated `assume` +is silently ignored by `quint typecheck`, `quint run`, and `quint verify` (none of them flags +it). It is documentation, not a checked constraint. To actually *check* a condition on +constants, write a `run` test that asserts it (it executes and fails when the condition is +false): + +```quint +run quorumAssumptionTest = all { + 2 * quorum > N, + N > 0, +} +``` + +Run it with `quint test`; the test fails (reporting which conjunct broke) if a constant +assignment violates the condition. + +--- + +## Conditional and let + +```quint +if (x > 0) "positive" else "non-positive" + +val result = { + val doubled = x * 2 + doubled + 1 +} +``` + + +--- + +## REPL usage + +Prefer CLI commands (`quint typecheck`, `quint run`, `quint test`, `quint verify`) for all validation and execution tasks. Open the REPL (`quint` or `quint -r spec.qnt::ModuleName`) only when you need expression-level interaction the CLI does not provide. + +Type inspection: +``` +>>> :type myExpression +``` + +--- + +## File layout + +Split specs across two files: + +``` +.qnt # main module — step, init, vars, invariants +_test.qnt # test module — run tests and scenario witnesses (imports main) +``` + +### Module responsibilities + +**Main module** (`.qnt`): +- Declares all state variables, `init`, actions, and safety invariants +- **`step` must live in the main module** — it is the entry point for `quint run` simulation +- The module name matches the file stem: `module myProtocol` in `myProtocol.qnt` + +**Test module** (`_test.qnt`): +- Imports the main module (`import myProtocol.*`) +- Contains `run` tests and scenario witnesses invoked via `quint test` or `quint run` +- Inherits `step` from the main module through the import + +### Which `--main` to pass for `quint run` + +`quint run` must receive the module that **owns the property** being checked: + +| Property location | Correct `--main` | +|---|---| +| Invariant defined in main module | main module name | +| Witness / `run` test defined in test module | test module name (it imports `step` from main) | + +The primitive's `module_name` field (set during indexing) always holds the correct value. Use it directly — do not derive from the filename. + +--- + +--- + +## Basic spells + +Many useful operators are not built into Quint but are available in `basicSpells.qnt`, a standard library shipped with most Quint projects. Import it with: + +```quint +import basicSpells.* from "./basicSpells" +``` + +Key definitions it provides: + +| Definition | What it does | +|---|---| +| `type Option[a] = Some(a) \| None` | The option type — Quint has **no** built-in `Option`. Any spec field typed `Option[T]` depends on this import. | +| `unwrap(o)` | The value inside `Some`; undefined on `None` | +| `require(cond)` | Blocks the action if `cond` is false (cleaner than bare `all { cond, ... }`) | +| `values(m)` | Set of all values in map `m` | +| `transformValues(m, f)` | New map with `f` applied to every value | +| `has(m, key)` | True if `key` is bound in `m` | +| `getOrElse(m, key, default)` | `m.get(key)` if present, otherwise `default` | +| `mapRemove(m, key)` / `mapRemoveAll(m, ks)` | Copy of `m` without `key` (or without the set of keys `ks`) | +| `setRemove(s, e)` / `setAdd(s, e)` | Copy of set `s` without / with element `e` | +| `find(s, f)` / `findFirst(l, f)` | First element of set / list satisfying `f`, as `Option` | +| `max(i, j)` / `min(i, j)` / `abs(i)` | Max / min of two integers; absolute value | + +When you see a spec using `Option`, `require`, `values`, or `transformValues` without an import, it is relying on basicSpells — check whether the project includes it. (Less common operators live in a sibling `rareSpells.qnt`.) + +--- + +## Guidelines + +Detailed references — read these when you need more than the quick reference above: + +| File | Contents | +| --- | --- | +| `guidelines/operators.md` | Complete operator reference: extended set/list/map operators, `run`/`then`/`expect`/`reps` for tests and witnesses, temporal fairness, `q::debug` | +| `guidelines/simulations.md` | Witnesses vs invariants, result interpretation, progressive increase protocol, trace analysis, coverage standard | +| `guidelines/constraints.md` | Hard language limitations: no string ops, no nested match, no destructuring, no loops, no early returns | +| `guidelines/cli.md` | Full CLI reference: `quint run`, `quint test`, `quint verify` flags, verbosity guide, reading output | +| `guidelines/patterns.md` | 14 core patterns: State Type, Pure Functions, Thin Actions, Map Pre-population, Syntax Rules, Undefined Behavior, Witnesses, Nondeterministic Testing, Separate Test Files, REPL-First Debugging, Separate Concerns First, Extract System Model, Types-First Scaffolding, Logic Stubs | +| `guidelines/tests.md` | Writing and debugging tests: `run`/`then`/`expect`/`reps`/`fail`, nondeterministic tests, error location ≠ failure point, frame counting, REPL-first debugging | +| `guidelines/choreo.md` | Choreo framework for distributed protocols: two-file split, `choreo::cue` pattern, `.with_cue().perform()` testing, witness-based test discovery | diff --git a/.claude/skills/quint-lang/guidelines/choreo.md b/.claude/skills/quint-lang/guidelines/choreo.md new file mode 100644 index 000000000..9df76b392 --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/choreo.md @@ -0,0 +1,267 @@ +# Choreo Framework + +Choreo is a structured framework for writing distributed protocol specs in Quint. Instead of a blank file, it gives you pre-built abstractions for message passing, state management, and Byzantine fault tolerance. + +**Use Choreo when:** consensus protocols (Raft, Paxos, Tendermint, HotStuff), BFT protocols, multi-phase commit, any message-passing protocol with N processes. + +## Contents + +- [1. Two-File Split](#1-two-file-split) +- [2. The `choreo::cue` Pattern](#2-the-choreocue-pattern) +- [3. Testing with Cues](#3-testing-with-cues) +- [4. Witness-Based Test Discovery](#4-witness-based-test-discovery) + +**Import:** +```quint +import choreo(processes = NODES) as choreo from "./choreo" +``` + +--- + +## 1. Two-File Split + +Choreo specs split into two files: + +``` +algorithm.qnt — pure consensus logic (no distributed state) +consensus.qnt — distributed system: N processes, message buffer, actions +``` + +```quint +// algorithm.qnt — pure logic only +module algorithm { + type LocalState = { + currentRound: int, + votes: Set[Vote], + decisions: Set[Decision], + } + + type Result = { + output: Set[ConsensusOutput], + post: LocalState, + } + + pure def processInput(state: LocalState, input: Input, id: ID): Result = { + // All business logic here — no global state access + } +} + +// consensus.qnt — distributed wrapper +module consensus { + import algorithm.* from "./algorithm" + + type Environment = { + processes: ID -> LocalState, + messageBuffer: Set[Message], + } + + const correctProcesses: Set[ID] + const byzantineProcesses: Set[ID] + + // Actions call algorithm.* pure functions +} +``` + +**Why**: Pure functions in `algorithm.qnt` can be tested directly in the REPL with any state. The distributed wrapper in `consensus.qnt` handles network, faults, and nondeterminism. + +--- + +## 2. The `choreo::cue` Pattern + +The core abstraction: separates **when** (listen) from **what** (act). + +```quint +choreo::cue(context, listen_operator, act_operator) +``` + +- `listen_operator`: returns a `Set[Params]` — the messages/events that match current state +- `act_operator`: takes one `Params` value and returns a `Transition` +- If the set is empty, no transition fires + +### Example: Tendermint proposal handling + +```quint +// 1. Listen: filter proposals relevant to current state +pure def listen_proposal_in_propose(ctx: LocalContext): Set[ProposeMsg] = { + val s = ctx.state + val proposals = ctx.messages.get_proposals() + proposals.filter(p => and { + s.stage == ProposeStage, + p.valid_round == -1, + p.src == PROPOSER.get(s.round), + }) +} + +// 2. Act: produce a transition for a matching proposal +pure def broadcast_prevote_for_proposal(ctx: LocalContext, p: ProposeMsg): Transition = { + val s = ctx.state + val effects = if (valid(p.proposal) and s.locked_round == -1) + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: Some(id(p.proposal)) }))) + else + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: None }))) + { post_state: { ...s, stage: PreVoteStage }, effects: effects } +} + +// 3. Wire together in main_listener +pure def main_listener(ctx: LocalContext): Set[Transition] = + Set( + choreo::cue(ctx, listen_proposal_in_propose, broadcast_prevote_for_proposal), + choreo::cue(ctx, listen_quorum_prevotes_any, trigger_prevote_timeout), + choreo::cue(ctx, listen_quorum_precommits_any, trigger_precommit_timeout), + on_propose_timeout(ctx), // non-cue transitions mix in freely + on_prevote_timeout(ctx), + on_precommit_timeout(ctx), + ).flatten() +``` + +The `main_listener` is a protocol at-a-glance — good names make it read like the paper. + +### `Transition` type + +```quint +{ + post_state: LocalState, // new local state after transition + effects: Set[choreo::Effect] // messages to broadcast, custom effects +} +``` + +Built-in effects: `choreo::Broadcast(msg)`. Custom effects via `choreo::CustomEffect(...)`. + +--- + +## 3. Testing with Cues + +The cue pattern enables **controlled, non-cheating** tests. `.with_cue()` verifies the listen condition is met before executing. + +```quint +module protocolTest { + import protocol.* from "./protocol" + + // Happy path: inject a proposal, verify stage transition + run proposalHandlingTest = { + val proposal = { proposal: "v0", round: 0, src: "p1", valid_round: -1 } + init + .then("p1".with_cue(listen_proposal_in_propose, proposal).perform(broadcast_prevote_for_proposal)) + .expect(s.system.get("p1").stage == PreVoteStage) + .then("p2".with_cue(listen_proposal_in_propose, proposal).perform(broadcast_prevote_for_proposal)) + } + + // Timeout test + run timeoutTest = { + init + .then("p1".step_with(on_propose_timeout)) + .then("p2".step_with(on_propose_timeout)) + .expect(NODES.forall(n => s.system.get(n).round == 1)) + } + + // Message injection: manually add messages to the buffer + run messageInjectionTest = { + val msg1 = { src: "p1", round: 2, value: "v0" } + init + .then( + "p3".step_with_messages( + (ctx) => listen_prevote(ctx).filter(m => m.round == 2), + (msgs) => msgs.setAdd(PreVote(msg1)) + ) + ) + .expect(s.system.get("p3").votes.size() == 1) + } +} +``` + +### Testing operators + +| Operator | Signature | Effect | +|---|---|---| +| `"node".with_cue(listen, params).perform(act)` | — | Assert listen returns params, then call act | +| `"node".step_with(listener)` | — | Execute a timeout or special listener | +| `"node".step_with_messages(listener_fn, msg_fn)` | — | Inject messages, then run listener | + +### Anti-patterns + +```quint +// ❌ Wrong syntax +.then("p1", with_cue(listen, params), perform(act)) + +// ✅ Methods chain on the string +.then("p1".with_cue(listen, params).perform(act)) + +// ❌ Wrong order +.then(step_with("p1", listener)) + +// ✅ Node comes first +.then("p1".step_with(listener)) + +// ❌ Messages are Sets, not arrays +val msg = s.messages.get("p1")[0] + +// ✅ Use find + unwrap +val msg = s.messages.get("p1").get_votes().find(m => m.round == 0).unwrap() +``` + +--- + +## 4. Witness-Based Test Discovery + +For complex actions requiring deep state setup, use witnesses to find reachable traces, then convert them to deterministic tests. + +### Step 1: Add a logging custom effect + +```quint +// Add to your action +choreo::CustomEffect(Log(BroadcastedPrecommit(ctx.state.process_id, params))) + +// Handle it +def apply_custom_effect(env: GlobalContext, effect: CustomEffects): GlobalContext = + match effect { + | Log(logType) => { ...env, extensions: { ...env.extensions, log: logType } } + | _ => env + } +``` + +### Step 2: Write a witness + +```quint +val canBroadcastPrecommit: bool = + match choreo::s.extensions.log { + | BroadcastedPrecommit(_) => false + | _ => true + } +``` + +### Step 3: Find a counterexample + +```bash +# Here we want the actual PATH, so use the negated-invariant form (not --witnesses): +# canBroadcastPrecommit is written not(target); a reported violation is a trace reaching it. +quint run spec.qnt --main myProtocol --invariant canBroadcastPrecommit \ + --max-steps 50 --init init_displayer +``` + +If still satisfied, increase `--max-steps` until violated. Then minimize: + +```bash +# Minimize: decrease until you can't find violation +quint run spec.qnt --main myProtocol --invariant canBroadcastPrecommit --max-steps 19 +``` + +### Step 4: Convert counterexample to a `run` + +Read the trace's `log` field. Each log entry maps to a `with_cue().perform()` call: + +``` +Log: BroadcastedPrecommit("p1", { round: 2, value: "v0" }) +→ "p1".with_cue(listen_precommit, { round: 2, value: "v0" }).perform(broadcast_precommit) +``` + +```quint +run canBroadcastPrecommitTest = + init + .then("p1".with_cue(listen_proposal_in_propose, v0_proposal).perform(broadcast_prevote_for_proposal)) + .then("p2".with_cue(listen_proposal_in_propose, v0_proposal).perform(broadcast_prevote_for_proposal)) + .then("p1".with_cue(listen_quorum_prevotes, v0_proposal).perform(broadcast_precommit)) +``` + +### Step 5: Clean up + +Remove all `Log(...)` effects, the `log` field from `Extensions`, and the `apply_custom_effect` instrumentation. Keep only the tests. diff --git a/.claude/skills/quint-lang/guidelines/cli.md b/.claude/skills/quint-lang/guidelines/cli.md new file mode 100644 index 000000000..91da081bd --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/cli.md @@ -0,0 +1,248 @@ +# Quint CLI Reference + +## Contents + +- [Installation](#installation) +- [Commands Overview](#commands-overview) +- [`quint run` — Simulation](#quint-run--simulation) +- [`quint test` — Deterministic Tests](#quint-test--deterministic-tests) +- [`quint verify` — Model Checking](#quint-verify--model-checking) +- [`quint typecheck`](#quint-typecheck) +- [Reading Output](#reading-output) +- [Verbosity Guide](#verbosity-guide) + +## Installation + +```bash +npm i @informalsystems/quint -g +``` + +--- + +## Commands Overview + +| Command | Purpose | +|---|---| +| `quint` | Start REPL | +| `quint run` | Random simulation — find invariant violations fast | +| `quint test` | Run deterministic `run` tests | +| `quint verify` | Exhaustive verification via Apalache (bounded model checking) | +| `quint typecheck` | Type-check without running | +| `quint parse` | Parse and resolve imports only | +| `quint compile` | Compile to TLA+ or JSON IR | + +--- + +## `quint run` — Simulation + +Randomly walks the state space. Finds obvious violations in seconds. + +```bash +quint run spec.qnt \ + --main MyModule \ + --invariant myInvariant \ + --max-steps 100 + # --max-samples defaults to 10000; lower it only for quick debugging, not to confirm a property +``` + +### Key flags + +| Flag | Default | Effect | +|---|---|---| +| `--main` | filename | Module to use | +| `--invariant` | `true` | Invariant name or expression to check | +| `--invariants` | `[]` | Space-separated list of invariant names (all checked with AND) | +| `--witnesses` | `[]` | Space-separated list of witnesses to report on | +| `--max-steps` | 20 | Max steps per trace | +| `--init` | `init` | Name of the init action in the module | +| `--step` | `step` | Name of the step action in the module | +| `--max-samples` | 10000 | Max number of runs before giving up | +| `--seed` | random | Seed for reproducibility | +| `--verbosity` | 2 | Output detail, **0–5**: 0=silent, 1=pass/fail, 2=example trace, 3=+`nondet` picks, 4–5=+evaluator internals | +| `--hide` | `[]` | Variable names to hide from terminal output | +| `--out-itf` | — | Write traces in Informal Trace Format (for ITF Viewer) | +| `--mbt` | false | Emit `mbt::actionTaken` and `mbt::nondetPicks` metadata for MBT | + +### Reading output + +| Output | Meaning | +|---|---| +| `"An example execution"` | Invariant violated — counterexample found | +| `"No violation found"` | Invariant held across all sampled traces | +| `" was witnessed in N trace(s) … (P%)"` (with `--witnesses`) | Witness `` reachable in N traces; **0 traces** ⚠️ = unreachable in this sampling | + +### Verbosity guide + +| Level | Shows | When to use | +|---|---|---| +| 0 | Nothing (silent) | Scripted/bulk runs where you only check the exit code | +| 1 | Pass/fail line only | Bulk runs | +| 2 (default) | Example trace (states) | Quick trace understanding | +| 3 | + `nondet` picks / state changes | Debugging failures | +| 4–5 | + evaluator internals | Deep debugging of the tool itself | + +### Notifying the user about non-default actions + +After calling `quint run` or `quint verify`, if a +non-default `init` or `step` was passed, always include a brief confirmation in your +reply, for example: + +> Ran with `--init customInit --step myStep`. + +If both are omitted (using Quint defaults), no confirmation line is needed. + +### Reproducing a run + +```bash +# Capture the seed from a violation, then replay +quint run spec.qnt --invariant myInv --seed 12345 --verbosity 3 +``` + +--- + +## `quint test` — Deterministic Tests + +Runs all `run` definitions in the spec (or a filtered subset). + +```bash +quint test spec.qnt --main MyModule --match testName +``` + +### Key flags + +| Flag | Default | Effect | +|---|---|---| +| `--main` | filename | Module to use | +| `--match` | all | String or regex to filter test names | +| `--max-samples` | 10000 | Max runs for randomized tests | +| `--seed` | random | Seed for reproducibility | +| `--verbosity` | 2 | Output detail level | + +### Reading output + +``` +[PASS] basicTest +[FAIL] transferTest +``` + +A `[FAIL]` shows which `.expect()` failed and the state at failure. + +--- + +## `quint verify` — Apalache (Exhaustive) + +Checks invariants across **all** reachable states up to `--max-steps`. Requires Java (OpenJDK). + +```bash +quint verify spec.qnt \ + --main MyModule \ + --invariant myInvariant \ + --max-steps 10 +``` + +Quint automatically downloads and starts Apalache. To use a running Apalache server: + +```bash +apalache-mc server # start Apalache server +quint verify spec.qnt --server-endpoint localhost:8822 --invariant myInv +``` + +### Key flags + +| Flag | Default | Effect | +|---|---|---| +| `--main` | filename | Module to use | +| `--invariant` | — | Invariants to check (comma-separated) | +| `--init` | `init` | Name of the init action in the module | +| `--step` | `step` | Name of the step action in the module | +| `--inductive-invariant` | — | Inductive invariant (checked in 2–3 Apalache calls) | +| `--temporal` | — | Temporal properties to check | +| `--max-steps` | 10 | Bound on trace length | +| `--random-transitions` | false | Symbolic simulation instead of full exploration | +| `--out-itf` | — | Write counterexample trace to ITF file | + +### When to use verify vs run + +| Tool | Coverage | Cost | Use when | +|---|---|---|---| +| `quint run` | Sampled | Seconds | Early design, quick sanity check | +| `quint verify` | All states up to bound | Minutes–hours | Final confirmation, critical invariants | + +--- + +## REPL + +```bash +quint # start blank REPL +quint -r spec.qnt::ModuleName # load file and import module +``` + +To drive the REPL **non-interactively** (piping commands from a script/agent), add +`--backend=typescript` — the default Rust backend evaluates nothing on piped stdin +(`ERR_USE_AFTER_CLOSE: readline was closed`). Interactive TTY use works on either backend. + +```bash +printf 'init\nstep\nbalances\n' | quint -r spec.qnt::ModuleName --backend=typescript +``` + +### REPL commands + +| Command | Effect | +|---|---| +| `.load spec.qnt` | Load (or reload) a file | +| `.clear` | Reset all session state | +| `.save kettle.qnt` | Save session to file | +| `.seed[=]` | Set (or get) the random seed — makes `nondet`/`oneOf` picks reproducible: same seed, same trace | +| `.exit` | Exit REPL | +| `:type expr` | Show inferred type of expression | + +### REPL workflow + +``` +>>> init // apply init action (returns true if succeeded) +>>> step // take one random step +>>> myInvariant // evaluate an invariant in the current state +>>> myPureFunc(arg) // call any pure def +>>> :type balances // inspect type +``` + +Force a specific state with an anonymous action: + +```quint +>>> all { balances' = Set("alice").mapBy(_ => 999), phase' = "ready" } +true +>>> balances +Map("alice" -> 999) +``` + +--- + +## Common Patterns + +### Check a witness (reachability) + +```bash +# Positive predicate; expect a non-zero trace count (0 traces = unreachable) +quint run spec.qnt --witnesses canDecide --max-steps 100 +``` + +### Check a safety invariant + +```bash +# Invariant should be SATISFIED — violation means a bug. +# Keep --max-samples at its 10000 default (or higher) when confirming a property; +# don't lower it to go faster. See simulations.md "Choosing --max-samples and --max-steps". +quint run spec.qnt --invariant noNegativeBalances --max-steps 100 +``` + +### Run a specific test + +```bash +quint test specTest.qnt --main specTest --match happyPath +``` + +### Generate an ITF trace for the viewer + +```bash +quint run spec.qnt --invariant myWitness --out-itf trace_{seq}.itf.json +``` diff --git a/.claude/skills/quint-lang/guidelines/constraints.md b/.claude/skills/quint-lang/guidelines/constraints.md new file mode 100644 index 000000000..d7eb3a372 --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/constraints.md @@ -0,0 +1,172 @@ +# Quint Language Constraints + +**CRITICAL**: These are fundamental limitations of the Quint language. Violating these constraints will result in compilation errors that cannot be worked around. + +## Contents + +- [1. No String Manipulation](#1-no-string-manipulation) +- [2. No Nested Pattern Matching](#2-no-nested-pattern-matching) +- [3. Destructuring — bindings and lambdas only](#3-destructuring--bindings-and-lambdas-only) +- [4. No Mutable Local Variables](#4-no-mutable-local-variables) +- [5. No Loops](#5-no-loops) +- [6. No Early Returns](#6-no-early-returns) +- [7. Type Inference Limitations](#7-type-inference-limitations) +- [Debugging Workflow](#debugging-workflow) + +--- + +## 1. No String Manipulation + +Quint treats strings as **opaque values** — equality comparison only. + +```quint +// ❌ NOT allowed +"hello" + "world" // concatenation +"value: ${x}" // interpolation +str[0] // indexing +str.length() // methods +toString(42) // conversion + +// ✅ Allowed +name == "Alice" // equality comparison +Map("a" -> 1) // strings as map keys +Set("alice", "bob") // strings in sets +``` + +When you need composite identifiers, use records or sum types instead: + +```quint +// Instead of string concatenation, use structured data +type MessageId = { sender: str, round: int } +``` + +--- + +## 2. No Nested Pattern Matching + +`match` works on **one level only**. Nested patterns cause a compile error. + +```quint +// ❌ NOT allowed — nested patterns +match msg + | Request(Prepare(n, v)) => ... + +// ✅ Allowed — sequential matches +match msg + | Request(inner) => + match inner + | Prepare(n, v) => ... + | Promise(n, r) => ... +``` + +**Rule**: Match one layer at a time. Use intermediate `val` bindings between match levels. + +--- + +## 3. Destructuring — bindings and lambdas only + +Destructuring (unpacking a tuple or record into named parts) works in **`val`/let bindings** +and in **lambda parameters**, but **not** in `def`/operator parameter lists or `match` arms. + +```quint +// ✅ Allowed — val/let binding (tuple and record) +val (x, y) = get_pair() // x = pair._1, y = pair._2 +val { name, age } = person // name = person.name, age = person.age + +// ✅ Allowed — tuple destructuring in a lambda (note the DOUBLE parens) +mySet.map(((a, b)) => a + b) // ((a, b)) => … unpacks one tuple argument +// contrast: (a, b) => … is a TWO-argument lambda, not destructuring + +// ❌ NOT allowed — destructuring in a def/operator parameter list +def f((a, b)) = a + b // use a single param + ._1/._2 instead: +def f(p) = p._1 + p._2 + +// ❌ NOT allowed — destructuring a tuple inside a match arm +match msg { | Foo((a, b)) => ... } // bind, then access: +match msg { | Foo(hr) => hr._1 + hr._2 } +``` + +The `((x, y)) => e` lambda form is sugar for `t => { val x = t._1 val y = t._2 e }`. + +--- + +## 4. No Mutable Local Variables + +`val` bindings are immutable. You cannot reassign within a definition. + +```quint +// ❌ NOT allowed +val x = 1 +val x = 2 // redeclaration error + +// ✅ Use state variables (with ') for mutable state across transitions +// ✅ Use if-then-else or match for conditional values +``` + +--- + +## 5. No Loops + +Quint has no `for` or `while`. Use set/list/map operators instead. + +```quint +// ❌ NOT a thing in Quint +for x in S: x + 1 + +// ✅ Use functional operators +S.map(x => x + 1) +S.fold(0, (acc, x) => acc + x) +S.filter(x => x > 0) +``` + +--- + +## 6. No Early Returns + +Definitions must have a **single expression** as their body. + +```quint +// ❌ NOT allowed +pure def f(x: int): int = { + if (x < 0) return -1 // no return keyword + x + 1 +} + +// ✅ Use if-then-else +pure def f(x: int): int = + if (x < 0) -1 else x + 1 + +// ✅ Use match for multiple cases +pure def classify(x: int): str = + if (x < 0) "negative" + else if (x == 0) "zero" + else "positive" +``` + +--- + +## 7. Type Inference Limitations + +Quint infers types well, but needs help with empty collections and polymorphic operators. + +```quint +// ❌ Ambiguous — type of empty set unknown +val s = Set() + +// ✅ Provide context +val s: Set[int] = Set() +// or just start with elements +val s = Set(1, 2, 3) +``` + +--- + +## Debugging Workflow + +When you hit a compilation error: + +1. **Check constraints first** — most errors come from the seven rules above +2. **Read the error message** — the type checker is precise about location and cause +3. **Break complex expressions into `val` steps** — simplifies type inference and debugging +4. **Match one level at a time** — never nest patterns +5. **Use explicit field access** — `.field`, `._1`, `._2` instead of destructuring diff --git a/.claude/skills/quint-lang/guidelines/operators.md b/.claude/skills/quint-lang/guidelines/operators.md new file mode 100644 index 000000000..573307adb --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/operators.md @@ -0,0 +1,164 @@ +# Quint Operator Reference — Complete + +This file covers operators missing from SKILL.md's quick reference. Read this when you need the full operator surface. + +## Contents + +- [Set operators (extended)](#set-operators-extended) +- [List operators (extended)](#list-operators-extended) +- [Map operators (extended)](#map-operators-extended) +- [Run tests and witnesses](#run-tests-and-witnesses) +- [Temporal operators (extended)](#temporal-operators-extended) +- [Debug output](#debug-output) + +--- + +## Set operators (extended) + +```quint +// Membership +1.in(Set(1, 2, 3)) // true (reverse of contains) +Set(1, 2).subseteq(Set(1, 2, 3)) // true + +// Structure +Set(1, 2).powerset() + // Set(Set(), Set(1), Set(2), Set(1, 2)) +Set(Set(1, 2), Set(3, 4)).flatten() // Set(1, 2, 3, 4) + +// Selection +Set(5).getOnlyElement() // 5 — deterministic; undefined if size != 1 +nondet x = Set(1, 2, 3).oneOf() // nondeterministic pick — use in actions only +``` + +**Picking an element**: use `getOnlyElement()` when the set has exactly one element (deterministic), or `oneOf()` inside a `nondet` binding in an action for a nondeterministic pick. `oneOf` outside a `nondet` binding causes a type/effect error. + +> Quint also has a `chooseSome` operator in its type signatures, but the simulator and verifier **do not implement it** — calling it raises a runtime error (`QNT501: Runtime does not support the built-in operator 'chooseSome'`). Do not use it in executable specs. + +--- + +## List operators (extended) + +```quint +List(1, 2, 3).indices() // Set(0, 1, 2) +List(1, 2, 3).replaceAt(1, 9) // List(1, 9, 3) +List(1, 2, 3, 4, 5).slice(1, 3) // List(2, 3) — i inclusive, j exclusive +range(1, 4) // List(1, 2, 3) — i inclusive, j exclusive +``` + +**`range` vs `to`**: `range(i, j)` returns a `List[int]` (ordered, j exclusive). `i.to(j)` returns a `Set[int]` (unordered, j inclusive). + +--- + +## Map operators (extended) + +```quint +// set vs put — critical distinction +Map(1 -> "a", 2 -> "b").set(2, "x") // Map(1 -> "a", 2 -> "x") — update EXISTING key only +Map(1 -> "a", 2 -> "b").put(3, "c") // Map(1 -> "a", 2 -> "b", 3 -> "c") — add or update + +// Functional update +Map(1 -> 10, 2 -> 20).setBy(2, x => x + 5) // Map(1 -> 10, 2 -> 25) + +// Building maps +Set((1, true), (2, false)).setToMap() // Map(1 -> true, 2 -> false) +Set(1, 2).setOfMaps(Set(true, false)) + // all possible maps from {1,2} to {true,false} +``` + +**`set` vs `put`**: `set(k, v)` has undefined behavior when `k` is not already a key. Use `put` when you might be inserting a new key; use `set` (or `setBy`) when you know the key exists. In practice, `put` is almost always what you want for state updates. + +--- + +## Run tests and witnesses + +`run` definitions define concrete execution scenarios. They are the primary way to write witnesses (reachability checks) and deterministic tests. + +```quint +// Basic pattern: chain actions with .then(), assert state with .expect() +run happyPath = init.then(vote(1)).then(vote(2)).then(decide).expect(decided == true) + +// Repeat an action N times +run threeVotes = init.then(3.reps(i => vote(i))).expect(votes.size() == 3) + +// Negative test — assert an action fails +run cannotDoubleVote = init.then(vote(1)).then(vote(1).fail()) + +// Assert mid-trace. An `assert` must ride inside an `all { }` that also assigns +// the state variables — a bare `.then(assert(...))` step assigns nothing and +// fails to typecheck (effect mismatch with the rest of the trace). Use `.expect` +// for an after-the-fact check. +run checkAfterVote = + init + .then(all { vote(1), assert(votes.size() == 0) }) // assert BEFORE vote executes + .expect(votes.size() == 1) // assert AFTER (no extra step needed) +``` + +### Operators + +| Operator | Signature | Meaning | +| --- | --- | --- | +| `a.then(b)` | `(bool, bool) => bool` | Execute `a`, then `b` from the resulting state | +| `a.expect(p)` | `(bool, bool) => bool` | Execute `a`, fail if `p` is false in resulting state | +| `n.reps(i => A)` | `(int, (int) => bool) => bool` | Execute action `A` n times; iteration index passed as `i` | +| `a.fail()` | `(bool) => bool` | True when `a` evaluates to false | +| `assert(p)` | `(bool) => bool` | Does not change state; fails if `p` is false | + +### Using run as a witness + +A witness is a `run` that demonstrates a state is reachable. The spec verifier checks that the `run` completes without failure: + +```quint +// @witness +run decisionIsReachable = + init + .then(3.reps(i => vote(i))) + .expect(decided == true) +``` + +This `run`-style witness documents a *known* reachable path and is checked with `quint test` (it passes when the path completes). For exploratory reachability, write the target as a predicate and use `quint run --witnesses ` instead — a non-zero trace count means reachable. See `guidelines/simulations.md` for the full witnesses treatment. + +--- + +## Temporal operators (extended) + +```quint +// Logical equivalence +p.iff(q) // true when p and q have the same truth value + +// Stuttering — `vars` is a Set of state variables: Set(x), Set(x, y), ... +a.orKeep(vars) // a is true, OR all vars in vars are unchanged +a.mustChange(vars) // a is true AND at least one var in vars changed + +// Action enablement +enabled(a) // true when action a's preconditions are satisfiable + +// Fairness +a.weakFair(vars) // if a is eventually always enabled, it eventually fires +a.strongFair(vars) // if a is infinitely often enabled, it eventually fires +``` + +The `vars` argument is a **`Set` of state variables**, so every variable in it must have the **same type** (e.g. `Set(votes, committed)` where both are `Set[int]`). To cover differently-typed variables, group cohesive state into one record variable and pass `Set(localState)`, or pass `Set(theOneVar)`. The official examples use a single variable: `Next.weakFair(Set(x))`. + +### Fairness in practice + +Fairness conditions are needed to rule out trivially non-terminating behaviours in liveness proofs. Add `weakFair` for actions that should eventually fire when continuously enabled (e.g. message delivery). Add `strongFair` for actions that may be intermittently enabled but must eventually fire. + +```quint +// @temporal — pass same-typed vars; here both are sets +temporal liveness: bool = + step.weakFair(Set(votes, delivered)).implies(eventually(decided)) +``` + +--- + +## Debug output + +```quint +// Print a label and value; returns the value unchanged +q::debug("votes after round", votes) + +// Self-labelling form — prints the expression text and its value +q::debug(votes.size()) +``` + +`q::debug` is a `pure def` — it can appear anywhere including inside expressions. It prints to stdout during REPL evaluation and simulation. Remove before formal verification with Apalache. diff --git a/.claude/skills/quint-lang/guidelines/patterns.md b/.claude/skills/quint-lang/guidelines/patterns.md new file mode 100644 index 000000000..c49937728 --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/patterns.md @@ -0,0 +1,408 @@ +# Quint Specification Patterns + +Core patterns for writing correct, testable Quint specifications. + +## Contents + +- [1. State Type Pattern](#1-state-type-pattern) +- [2. Pure Functions Pattern](#2-pure-functions-pattern) +- [3. Thin Actions Pattern](#3-thin-actions-pattern) +- [4. Map Pre-population Pattern](#4-map-pre-population-pattern) +- [5. Syntax Rules](#5-syntax-rules) +- [6. Undefined Behavior — What to Guard Against](#6-undefined-behavior--what-to-guard-against) +- [7. Action Witnesses Pattern](#7-action-witnesses-pattern) +- [8. Nondeterministic Testing Pattern](#8-nondeterministic-testing-pattern) +- [9. Separate Test Files Pattern](#9-separate-test-files-pattern) +- [10. REPL-First Debugging](#10-repl-first-debugging) +- [11. Separate Concerns First](#11-separate-concerns-first) +- [12. Extract the System Model](#12-extract-the-system-model) +- [13. Types-First Scaffolding](#13-types-first-scaffolding) +- [14. Logic Stubs Pattern](#14-logic-stubs-pattern) + +--- + +## 1. State Type Pattern + +Encapsulate all state in a single `State` record. This is the fundamental structure for most Quint specs. + +```quint +module System { + // 1. Types — State record encapsulates everything + type State = { + field1: Type1, + field2: str -> int, // map type syntax: KeyType -> ValueType + } + + // 2. Constants + pure val INITIAL_USERS: Set[str] = Set("alice", "bob") + + // 3. Pure functions — ALL business logic here, split into a guard and a next-state function + pure def canDoOperation(state: State, param: Type1): bool = precondition(state, param) + pure def applyOperation(state: State, param: Type1): State = {...state, field1: newValue} + + // 4. State variable — keep cohesive state grouped + var state: State + + // 5. Invariants + val noNegativeBalances: bool = INITIAL_USERS.forall(u => state.field2.get(u) >= 0) + + // 6. Actions — guarded: the guard gates whether the action fires, then assign the next state + action doOperation(param: Type1): bool = all { + canDoOperation(state, param), + state' = applyOperation(state, param), + } + + // 7. Initialization — pre-populate ALL maps + action init: bool = all { + state' = { + field1: initialValue, + field2: INITIAL_USERS.mapBy(u => 0), + }, + } + + // 8. Step action — nondeterministic exploration + action step: bool = { + nondet user = INITIAL_USERS.oneOf() + any { + doOperation(user), + } + } +} +``` + +**Section order matters** — the type checker requires definitions before use: Types → Constants → Pure Functions → State Variables → Invariants → Actions → Init → Step. + +--- + +## 2. Pure Functions Pattern + +All business logic goes in pure functions. Split each operation into two pure defs: a **guard** +(can it happen?) and a **next-state** function (what does it produce, assuming the guard holds). +The action (Pattern 3) lifts the guard so it is *disabled* when the operation can't happen — no +success flag, no no-op branch. + +```quint +// Note: a pure def and an action cannot share a name in the same module (QNT101), +// so the action is `transfer` and the next-state function is `applyTransfer`. +pure def canTransfer(state: State, sender: str, recipient: str, amount: int): bool = and { + state.balances.get(sender) >= amount, + amount > 0, + sender != recipient, +} +pure def applyTransfer(state: State, sender: str, recipient: str, amount: int): State = { + val newBalances = state.balances + .setBy(sender, b => b - amount) + .setBy(recipient, b => b + amount) + {...state, balances: newBalances} +} +``` + +**Why**: Pure functions can be tested directly in the REPL with any state. Logic in actions can only be tested by running the full state machine. + +> `to` is a built-in operator (`i.to(j)`), so it cannot be used as a parameter name — that is why the parameters here are `sender`/`recipient` rather than `from`/`to`. + +--- + +## 3. Guarded Actions Pattern + +An action puts the guard and the next-state assignment together in one `all { ... }`: the guard +gates whether the action fires, then it assigns the next state. When the guard is false the action +is simply **disabled** (it does not fire and changes nothing) — no success flag, no `unchanged_all` +fallback. A disabled action is the faithful model of "this can't happen now," and it's what lets the +simulator surface dead ends; a blanket no-op fallback fabricates a transition the system doesn't have. + +```quint +action transfer(sender: str, recipient: str, amount: int): bool = all { + canTransfer(state, sender, recipient, amount), + state' = applyTransfer(state, sender, recipient, amount), +} +``` + +The action `transfer` uses the pure `canTransfer`/`applyTransfer` — distinct names, since a +`pure def` and an `action` cannot share a name. No conditional logic in the action beyond the guard. + +For cohesive local state, avoid decomposing one concept into many top-level vars (`var id`, `var phase`, `var round`, ...). Prefer a `type LocalState` record and one `var localState: LocalState`. + +--- + +## 4. Map Pre-population Pattern + +Always pre-populate maps in `init` using `mapBy`. Never start with an empty map if you'll call `.get()` on it. + +```quint +// ❌ Wrong — get("alice") is undefined if alice not in map +action init = all { balances' = Map() } + +// ✅ Correct — all keys pre-populated +action init = all { + balances' = USERS.mapBy(u => 0) +} +``` + +Map type syntax is `KeyType -> ValueType`, not `Map[KeyType, ValueType]`: + +```quint +var balances: str -> int // ✅ correct +var balances: Map[str, int] // ❌ wrong +``` + +--- + +## 5. Syntax Rules + +Common gotchas: + +```quint +// 1. Parameterless pure def — omit parentheses +pure def name = ... // ✅ +pure def name() = ... // ❌ + +// 2. Map type syntax +var m: str -> int // ✅ +var m: Map[str, int] // ❌ + +// 3. Record update — spread syntax is idiomatic +{...state, field: newValue} // ✅ preferred +state.with("field", newValue) // ⚠️ valid, but non-idiomatic (field name is a string literal) + +// 4. Variant constructors take one argument — use tuples for multiple values +TimeoutInput((height, round)) // ✅ +TimeoutInput(height, round) // ❌ + +// 5. Tuple destructuring in match — bind first, then access +| TimeoutInput(hr) => ... hr._1 ... hr._2 // ✅ +| TimeoutInput((height, round)) => ... // ❌ + +// 6. oneOf is a method on collections +collection.oneOf() // ✅ +oneOf(collection) // ❌ + +// 7. Reserved keywords cannot be identifiers or record field names +type T = { value: int } // ✅ +type T = { val: int } // ❌ — `val` is a keyword (also `def`, `to`, `from`, `import`, …) +def f(sender: int) = ... // ✅ +def f(to: int) = ... // ❌ — `to` is the built-in i.to(j) operator +``` + +--- + +## 6. Undefined Behavior — What to Guard Against + +These operations have undefined behavior if preconditions aren't met: + +| Operation | Unsafe when | Safe alternative | +| --- | --- | --- | +| `map.get(key)` | key not in map | Pre-populate with `mapBy`, or check `map.keys().contains(key)` | +| `set.getOnlyElement()` | set size ≠ 1 | `oneOf()` inside a `nondet` binding (nondeterministic), or guard the size to 1 first | +| `list.head()` / `list.tail()` | list is empty | Check `list.length() > 0` first | +| `list.nth(i)` | i < 0 or i ≥ length | Check `i >= 0 and i < list.length()` | +| `range(i, j)` / `i.to(j)` | i > j | Ensure `i <= j` | +| `map.set(k, v)` | key not already in map | Use `put(k, v)` instead | + +--- + +## 7. Action Witnesses Pattern + +A witness names a target state, written **positively**, and is checked with `quint run --witnesses`, +which reports how many sampled traces reached it. + +```quint +// state-evidence: a withdrawal pushed someone's balance below the initial value +val withdrawalHappened = users.exists(u => balances.get(u) < INITIAL_BALANCE) + +// multi-condition target +val fullCycleReached = and { + delegations.size() == 0, + users.forall(u => rewards.get(u) == 0), + users.exists(u => balances.get(u) > INITIAL_BALANCE), +} + +// quint run --witnesses withdrawalHappened fullCycleReached spec.qnt +// → withdrawalHappened was witnessed in N trace(s) … (P%) +// N > 0 = reachable; 0 = dead action (over-constrained precondition or bug) +``` + +Add one witness per major action; a witness reached in 0 traces means the action is dead. + +**Make the target a state only an action can produce.** A witness is satisfied by *any* state that +matches, including the initial state — so a predicate that already holds at `init` (e.g. a balance +that starts unequal) is "reached" in 100% of traces at step 0, telling you nothing about the action. +Phrase the target so only the action you care about can make it true (e.g. a balance *below* the +initial value requires a withdraw to have fired), and a non-zero count then genuinely witnesses the +action. + +**Distinguishing *which* action fired (rare).** When several actions can produce the same target +state and you must confirm a *specific* one ran, add a dedicated per-action boolean `var` set in that +action's body and read it in the witness: + +```quint +var lastWasWithdraw: bool // declared; set in EVERY action (false elsewhere) +// ... withdraw sets lastWasWithdraw' = true; other actions set it false ... +val withdrawFired = lastWasWithdraw and withdrawalHappened +``` + +This costs an assignment in every action (Quint requires every `var` set in every action), so reach +for it only when a plain state-evidence target genuinely can't distinguish the case — usually it can. + +When you want an actual *trace* that reaches the state rather than a count, write the negation as an +invariant (`val w = not(target)`) and run `--invariant w` — the reported "violation" is a reaching +execution. + +--- + +## 8. Nondeterministic Testing Pattern + +Use `nondet` with `.oneOf()` for broad coverage with random value selection. + +```quint +run nondetTest = { + nondet amount = 50.to(300).oneOf() + nondet user = USERS.oneOf() + init + .then(transfer(user, "treasury", amount)) + .expect(balances.get(user) >= 0) +} +``` + +Multiple `nondet` bindings explore combinations. The simulator picks values pseudo-randomly; use `--seed` to reproduce a specific run. + +--- + +## 9. Separate Test Files Pattern + +Main spec has no `run` definitions. Tests live in a separate file that imports the spec. + +```quint +// system.qnt — main spec, no tests +module system { + // ... spec only ... +} + +// systemTest.qnt — tests only +module systemTest { + import system.* from "./system" + + run basicTest = { + init + .then(transfer("alice", "bob", 50)) + .expect(balances.get("alice") == INITIAL_BALANCE - 50) + } +} +``` + +Run tests with: +```bash +quint test systemTest.qnt --main systemTest --match basicTest +``` + +--- + +## 10. REPL-First Debugging + +Test pure functions and action sequences in the REPL before writing formal tests. If REPL output surprises you, the spec has a bug. + +```bash +# Test a pure function with a hand-crafted state +echo 'val s = {balances: Set("alice").mapBy(_ => 100)} +transfer(s, "alice", "bob", 50)' | quint repl -r system.qnt::system + +# Test an action sequence +echo 'init +transfer("alice", "bob", 50) +balances' | quint repl -r system.qnt::system +``` + +Anonymous actions are also useful for forcing specific state in the REPL: + +```quint +>>> all { balances' = Set("alice").mapBy(_ => 999), owner' = "alice" } +true +>>> balances +Map("alice" -> 999) +``` + +--- + +## 11. Separate Concerns First + +Before writing any Quint, partition the protocol into three buckets: + +- **State machine** — variables, initialization, transitions +- **Functional logic** — pure computations: quorum checks, message filtering, state updates +- **Properties** — invariants, witnesses, temporal properties + +This partition maps directly to Quint: state machine → `var` + actions, functional logic → `pure def`, properties → `val` invariants + witnesses. Trying to translate everything at once produces specs where logic ends up in the wrong layer. + +--- + +## 12. Extract the System Model + +Before writing `var` declarations, identify the protocol's assumptions explicitly — they're easy to miss when implicit in prose or TLA+. Each becomes a `const` declaration; to actually *check* a condition on those consts, write a `run` test (an `assume` only documents the premise and is not enforced — see the `## Assume` section). + +| Concern | Questions to answer | +| --- | --- | +| **Communication** | Reliable or lossy? Ordered or unordered? Broadcast or point-to-point? | +| **Failures** | Crash-stop? Crash-recovery? Byzantine? What fraction `f` of `n`? | +| **Time** | Synchronous? Asynchronous? Partial synchrony? Are timeouts modelled? | +| **Participants** | Fixed membership or dynamic? How many processes? | + +```quint +pure val N: int = 4 // total processes +pure val F: int = 1 // max faulty + +// Check the assumption — a `run` test actually evaluates it. (`assume` would only document +// it; it is not enforced. Name ends in `Test` so `quint test` picks it up — see tests.md.) +run quorumMajorityTest = { all { 2 * F < N } } +``` + +If an assumption is wrong, every invariant built on top of it is wrong. Surface them before building anything else. + +--- + +## 13. Types-First Scaffolding + +Define all types and run `quint typecheck` before writing any logic. A spec that compiles with only types and `var` declarations is a solid foundation. A spec with correct logic but misaligned types is hard to untangle. + +```quint +// Step 1: define all types +// (Option is not built in — it comes from basicSpells; import it or define +// `type Option[a] = Some(a) | None` yourself.) +type Entry = { term: int, value: str } +type NodeState = { log: List[Entry], votedFor: Option[int], currentTerm: int } +type Message = + | VoteRequest({ term: int, src: int }) + | VoteResponse({ term: int, src: int, granted: bool }) + +// Step 2: declare vars — no logic yet +var nodes: int -> NodeState +var messages: Set[Message] + +// Step 3: quint typecheck — must pass before proceeding +``` + +Use the full type system: records for structured state, sum types for messages with distinct shapes, `NodeId -> LocalState` maps for per-process state, `Set[Message]` for the message soup. + +**Iterate with the user at this step.** Show the type sketch and get explicit approval before writing any functions or actions. + +--- + +## 14. Logic Stubs Pattern + +Write correct `pure def` signatures with placeholder bodies that compile. Fill in real logic one function at a time, testing each in the REPL before moving to the next. + +```quint +// ✅ Stub — correct signature, placeholder body, compiles +pure def isQuorum(voters: Set[int], allNodes: Set[int]): bool = + false // TODO + +pure def applyEntry(state: NodeState, entry: Entry): NodeState = + state // TODO + +// Later — fill in one at a time and test in REPL +pure def isQuorum(voters: Set[int], allNodes: Set[int]): bool = + voters.size() * 2 > allNodes.size() +``` + +**Why stubs first**: type mismatches surface at the signature level before logic exists, when they're cheap to fix. A full stub pass also forces you to think through every function's inputs and outputs before committing to an implementation. + +Only move to the state machine (actions, `init`, `step`) after all stubs compile and all logic is tested. diff --git a/.claude/skills/quint-lang/guidelines/simulations.md b/.claude/skills/quint-lang/guidelines/simulations.md new file mode 100644 index 000000000..7bbc74a69 --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/simulations.md @@ -0,0 +1,308 @@ +# Verification — Witnesses, Invariants, and Test Interpretation + +## Contents + +- [Critical Distinction](#critical-distinction) +- [Before you can run: instantiate the consts](#before-you-can-run-instantiate-the-consts) +- [Witnesses (Liveness — Protocol Makes Progress)](#witnesses-liveness--protocol-makes-progress) +- [Invariants (Safety — Properties Hold)](#invariants-safety--properties-hold) +- [Trace Analysis](#trace-analysis) +- [Result Classification](#result-classification) + +For the full `quint run` / `verify` / `test` flag reference, see `guidelines/cli.md`. This file +is about *running and interpreting* checks. + +## Critical Distinction + +Witnesses and invariants ask **opposite** questions — one wants the state reached, the other wants +it never violated: + +| Check (how to run it) | Good result | Bad result | +|---|---|---| +| **Witness** (`--witnesses`, positive predicate) | ✅ reached in > 0 traces — the state is reachable | ⚠️ 0 traces — unreachable: over-constrained or a bug | +| **Invariant** (`--invariant`) | ⚪ no counterexample in the sampled traces — *not* a proof | ❌ violated — a real bug (one trace disproves it) | + +Never confuse the two. With `--witnesses`, a witness reached in > 0 traces is success; an invariant +violation is a bug. Note the asymmetry: a single trace settles a witness (reached) or refutes an +invariant (violated), but an invariant with *no* counterexample only reflects the traces sampled in +this run — report it that way (see "Simulation is … not a proof" below), never as "safety holds". + +--- + +## Before you can run: instantiate the consts + +`quint run` / `verify` / `test` execute a **concrete** module — every `const` must have a value. +A spec module that declares `const N: int` (or `const Nodes: Set[str]`) cannot be run directly: +it fails with `QNT500: Uninitialized const N`. Giving the const a value via `assume` does **not** +fix this — `assume` states a premise, it does not bind the parameter. + +Instead, write a small concrete **instance module** that imports the spec with the consts bound, +and run *that* module (`--main`): + +```quint +module spec { + const N: int + const Nodes: Set[str] + // ... vars, actions, invariants, witnesses ... +} + +// concrete instance — this is what you run +module spec_3 { + import spec(N = 3, Nodes = Set("n1", "n2", "n3")).* +} +``` + +```bash +quint run spec.qnt --main spec_3 --invariants inv1 inv2 --max-steps 100 +``` + +By convention the instance module is named `Analysis` (e.g. `PaxosAnalysis`) and holds the +concrete `init`/`step` and the witnesses; pass `--main Analysis`, not the parameterized spec +module. (This is the same executability rule the quint-modeling skill enforces while building.) + +--- + +## Witnesses (Liveness — Protocol Makes Progress) + +### Syntax + +Write a witness as the **target state, stated positively** (no negation), and pass it to +`quint run --witnesses`. Quint reports how many sampled traces reached it. + +```quint +// State-change evidence: a deposit raised someone's balance above the initial value +val depositHappened: bool = + users.exists(u => balances.get(u) > INITIAL_BALANCE) + +// State-change evidence: a transfer pushed alice's balance below the initial value +val transferHappened: bool = + balances.get("alice") < INITIAL_BALANCE + +// Multi-condition target +val fullCycleReached: bool = and { + delegations.size() == 0, + users.forall(u => rewards.get(u) == 0), + users.exists(u => balances.get(u) > INITIAL_BALANCE), +} +``` + +Add one witness per major action. A witness reached in **0 traces** means the action is dead — an +over-constrained precondition or a bug. + +Phrase the target so **only an action can make it true** — a predicate that already holds at `init` +is "reached" at step 0 and witnesses nothing about the action. (If several actions can reach the same +state and you must confirm a *specific* one fired, use a per-action flag `var`; see `patterns.md` §7.) + +### Running witnesses + +Pass witnesses (space-separated) to `--witnesses`; they run alongside invariants in one pass: + +```bash +quint run spec.qnt \ + --main MyModule \ + --invariant noNegativeBalances \ + --witnesses withdrawalHappened transferSucceeded \ + --max-steps 100 \ + --max-samples 1000 +``` + +### Result interpretation + +Each witness is reported as a trace count: + +``` +withdrawalHappened was witnessed in 90 trace(s) out of 100 explored (90.00%) +transferSucceeded was witnessed in 0 trace(s) out of 100 explored (0.00%) +``` + +| Count | Meaning | Action | +|---|---|---| +| > 0 traces | ✅ the target state is reachable | done — non-zero coverage confirms it | +| 0 traces | ⚠️ never reached in this sampling | try more steps — see progressive increase below | + +### Progressive increase for 0-trace witnesses + +Do not conclude a state is unreachable after one run. Increase steps first: + +```bash +quint run spec.qnt --witnesses myWitness --max-steps 100 +quint run spec.qnt --witnesses myWitness --max-steps 200 +quint run spec.qnt --witnesses myWitness --max-steps 500 +``` + +If still 0 traces after 500 steps, run with `--verbosity 3` to inspect execution, then diagnose: + +| Symptom | Root cause | Fix | +|---|---|---| +| No actions execute | Protocol stuck at init | Fix `init` or witness precondition | +| Same action loops | Liveness bug or over-constrained guard | Relax action guard | +| Actions run but never reach witness | Witness condition too strong | Weaken the witness | +| Actions run, witness never reached | Real reachability bug in spec | Investigate spec logic | + +### When you want the actual reaching trace + +`--witnesses` gives a count, not an example. When you need the simulator to hand you a concrete +trace that *reaches* the state, write the negation as an invariant — `val w = not(target)` — and run +`--invariant w`; the "violation" it reports is an execution that reaches `target`. The two forms are +complementary, not old-vs-new: use `--witnesses` for the routine reachability + coverage check, and +the negated-invariant form when you specifically want the reaching trace (to understand or document +how the state is reached, or to debug a witness that fires unexpectedly). + +### Witness as a `run` (alternative form) + +```quint +// @witness +run decisionIsReachable = + init + .then(3.reps(i => vote(i))) + .expect(decided == true) +``` + +Use invariant-style witnesses for nondeterministic exploration; run-style witnesses for documenting known reachable paths. + +--- + +## Invariants (Safety — Properties Hold) + +### Running invariants + +```bash +quint run spec.qnt \ + --main MyModule \ + --invariant noNegativeBalances \ + --max-steps 200 + # --max-samples left at its 10000 default — see "Choosing parameters" below; + # don't lower it when confirming a safety invariant +``` + +### Choosing `--max-samples` and `--max-steps` + +These control *how many* traces and *how deep*. Choose them by **what you're doing**, not by habit: + +**`--max-samples` — by purpose.** +- **Debugging / shaking out runtime errors / a first run** — a small sample (e.g. + `--max-samples 50`) is fine. You just want to see the spec execute, catch a crash, or eyeball a + trace; fast feedback beats coverage. +- **Confirming a safety invariant holds** — keep `--max-samples` at its **`10000` default or + higher; never lower it** to go faster. "No counterexample" is only as strong as the number of + traces behind it, and the result is already non-exhaustive — cutting samples directly weakens the + evidence. For an actual guarantee up to a bound, use `quint verify`. + +**`--max-steps` — match it to the protocol's branching, not just its action count.** The default +(`20`) is often too short to reach interesting states. The trap is counting only the named actions +in `step`: a *single* action can expand into many concrete transitions through the `nondet` choices +inside it. A lone `sendMessage` over 3 nodes × 2 message types is **6 distinct transitions per +step**, so a random walk needs well more than 6 steps to exercise meaningful *combinations* — e.g. +to see all 6 (node, kind) pairs sent takes ~12–20 steps, not 1. So estimate the **branching factor** +(number of actions × the `nondet` fan-out inside them), then set `--max-steps` several times higher +than "fire each action once" — enough for the walk to reach a full cycle, a decision, a drained +queue, the state your invariants and witnesses are actually about. Too short and you only ever +witness shallow prefixes. (A small deterministic spec needs few steps; a single action with wide +internal nondet across many participants needs many.) + +### Checking several invariants at once + +When a spec has more than one invariant, **prefer a single run with `--invariants` (plural, a +space-separated list) over spawning one `quint run` per invariant.** They are checked together +(conjoined with AND), so one run covers them all — the same sampled traces exercise every +invariant, it's far cheaper than N separate runs, and any single violation still names the +invariant it broke. + +```bash +quint run spec.qnt --main MyModule \ + --invariants noNegativeBalances totalConserved holderIsMember \ + --max-steps 200 # --max-samples at the 10000 default for a confirmation run +``` + +Use a single `--invariant` (singular) only when you specifically want to isolate one property +(e.g. to focus a counterexample search or reproduce a seed against just that invariant). + +### Result interpretation + +| Output | Meaning | Action | +|---|---|---| +| `"No violation found"` | No counterexample in **this run** | Report as a sampling result, not a proof — see below | +| `"An example execution"` | VIOLATED ❌ | Bug — capture seed and analyze trace | + +> **Simulation is bounded random sampling, not a proof.** "No violation found" means no +> counterexample turned up in the traces that were sampled — it does **not** establish that the +> invariant holds in every reachable state. When reporting to the user, say "no counterexample +> found across N sampled runs (max-steps M, seed S)" and state the coverage as plain facts; do +> not call the property "proven", "verified", "safe", or "correct", and do not judge whether the +> sample size was "enough" — that is the user's call. For an actual exhaustive guarantee over a +> bounded horizon, use `quint verify` (bounded model checking), and even then scope the claim to +> that bound. Always offer next steps (more samples / a different seed / `quint verify` / tighten +> the property) and frame them as the user's decision. + +### Bug protocol: invariant violated + +**Step 1 — Capture details** +```bash +# Re-run with the seed from the violation output +quint run spec.qnt --invariant myInv --seed --verbosity 3 --main MyModule +``` + +**Step 2 — Analyze trace** +- Find the step N where the invariant became false +- Find the action that caused the transition to step N +- Extract the relevant state snapshot: which variables changed, what values + +**Step 3 — Determine root cause** + +| Scenario | Root cause | Fix | +|---|---|---| +| Invariant violated at step 0 | `init` produces invalid state | Fix `init` | +| Invariant holds at init, fails after action X | Action X has wrong guard or wrong update | Fix action X | +| Invariant seems too strict | Invariant itself is wrong | Weaken invariant | + + +## Trace Analysis + +Use `--verbosity 3` whenever you need to understand a failure or a never-violated witness. + +```bash +quint run spec.qnt --invariant myInv --seed --verbosity 3 --max-steps 50 +``` + +### Verbosity levels + +`--verbosity 3` is the one to reach for when diagnosing — it adds `nondet` picks and state changes on +top of the default example trace. The full 0–5 range is in `cli.md`'s verbosity guide. + +### `--mbt` — see *which* action fired at each step + +`--verbosity 3` shows state changes and picks, but not always *which named action* produced each +step. Add `--mbt` to surface that: each state in the trace carries `mbt::actionTaken` (the action +name) and `mbt::nondetPicks` (the values chosen inside it). + +```bash +quint run spec.qnt --invariant myInv --seed --verbosity 3 --mbt --max-steps 50 +``` + +Reach for it when a trace reaches the critical state but it's unclear which action drove the +transition — e.g. several actions could produce the same state, or a witness fires unexpectedly and +you need to name the culprit. (For *confirming* a specific action fired as a property rather than +reading it off a trace, the per-action flag `var` in `patterns.md` §7 is the structural alternative.) + +### Analysis steps + +1. Scan for repeated actions — signal of a stuck loop +2. Find the critical transition: step where invariant violated or witness should have fired +3. Read state before and after that step — what changed? +4. Trace backwards: which actions led here, what nondeterministic picks were made + +--- + +## Result Classification + +After running all checks. These classify **what the sampled runs showed** — they describe the +run, not a verdict on the spec's correctness (sampling is not a proof; see the note above). + +| Run outcome | Condition | How to report it | +|---|---|---| +| Clean run | Every witness reached in > 0 traces, all invariants without counterexample, all tests pass | "No counterexamples across the sampled runs; all target states reached. Not exhaustive." | +| Liveness concern | One or more witnesses reached in 0 traces after 500+ steps | "Target state not reached in sampling — possibly over-constrained, or sampling missed it." | +| Safety concern | Any invariant violated | "Counterexample found — this IS a bug (one trace is enough to disprove). Capture seed, analyze." | + +Note the asymmetry: a violation is conclusive (a single counterexample disproves a safety +property), but the absence of one is not — it only summarizes the traces that were sampled. diff --git a/.claude/skills/quint-lang/guidelines/tests.md b/.claude/skills/quint-lang/guidelines/tests.md new file mode 100644 index 000000000..eb5d319a0 --- /dev/null +++ b/.claude/skills/quint-lang/guidelines/tests.md @@ -0,0 +1,308 @@ +# Writing and Debugging Tests + +## Contents + +- [File Structure](#file-structure) +- [Writing Tests](#writing-tests) +- [Running Tests](#running-tests) +- [Debugging Failures](#debugging-failures) +- [REPL-First Debugging](#repl-first-debugging) + +## File Structure + +Tests live in a separate file that imports the main spec. The main spec has no `run` definitions. + +```quint +// system.qnt — spec only, no tests +module system { + // ... vars, actions, invariants ... +} + +// systemTest.qnt — tests only +module systemTest { + import system.* from "./system" + + run basicTest = { + init + .then(transfer("alice", "bob", 50)) + .expect(balances.get("alice") == INITIAL_BALANCE - 50) + } +} +``` + +Run with: +```bash +quint test systemTest.qnt --main systemTest --match basicTest +``` + +> **Naming gotcha:** by default `quint test` runs only `run` definitions whose name **ends in +> `Test`** (e.g. `basicTest`). A `run` named otherwise (`happyPath`, `testBasic`, `checkQuorum`) is +> **silently skipped** — no error, no output, exit 0 — which reads as "passed." Either suffix the +> name with `Test`, or select it explicitly with `--match ` (or `--match '.*'` for all). + +--- + +## Writing Tests + +### Basic pattern + +```quint +run happyPath = + init + .then(action1(args)) + .expect(condition1) + .then(action2(args)) + .expect(condition2) +``` + +### Operators + +| Operator | Meaning | +|---|---| +| `a.then(b)` | Execute `a`, then execute `b` from resulting state | +| `a.expect(p)` | Execute `a`, fail if `p` is false in resulting state | +| `n.reps(i => A)` | Execute action `A` n times; iteration index passed as `i` | +| `a.fail()` | Asserts `a` evaluates to false (action should be blocked) | +| `assert(p)` | Does not change state; fails if `p` is false | + +### Repeat an action N times + +```quint +run threeVotes = + init + .then(3.reps(i => vote(i))) + .expect(votes.size() == 3) +``` + +### Negative test — assert an action is blocked + +```quint +run cannotDoubleVote = + init + .then(vote("alice")) + .then(vote("alice").fail()) // second vote must fail +``` + +### Assert mid-trace + +An `assert` must sit inside an `all { }` block that also assigns the state +variables. A standalone `.then(assert(...))` step assigns nothing, so its effect +cannot unify with the rest of the trace and the test fails to typecheck. For an +after-the-fact check, use `.expect(...)` instead of a trailing assert step. + +```quint +run checkTiming = + init + .then(all { vote(1), assert(votes.size() == 0) }) // assert BEFORE vote executes + .expect(votes.size() == 1) // assert AFTER +``` + +### Nondeterministic tests + +```quint +run nondetTest = { + nondet amount = 50.to(300).oneOf() + nondet user = USERS.oneOf() + init + .then(transfer(user, "treasury", amount)) + .expect(balances.get(user) >= 0) +} +``` + +Multiple `nondet` bindings explore combinations. Use `--seed` to reproduce a specific run. + +### Conditional expectations — one test covering several branches + +When the *correct* outcome depends on how the random inputs relate to each other, don't write one +fixed assertion (it can't be right for every draw) and don't split into many hardcoded tests. +Instead branch the `.expect()` on the inputs and assert the outcome that's correct **for that +branch** — a single `run` then exercises the whole decision surface. + +```quint +// withdrawCapped is always enabled; it takes the whole balance if asked for more. +run withdrawTest = { + nondet amount = 50.to(150).oneOf() + init // balance starts at 100 + .then(withdrawCapped(amount)) + .expect(if (amount > 100) + balance == 0 // asked for more than held → capped to the balance + else + balance == 100 - amount) // normal deduction +} +``` + +The branch condition uses the `nondet` values; each arm asserts the result appropriate to that +relationship (under/at/over a threshold, full/partial, etc.). + +**Caveat — this only works while the action stays *enabled* across all branches.** A `.then(act)` +on a **disabled** action (its guard is false) cannot proceed: the test stops with `Cannot continue +to "expect"` before the `.expect` is ever evaluated — so you **cannot** write an `if`-arm meaning +"in this case the action was blocked, assert nothing changed." Conditional `.expect()` is for an +always-enabled action whose *result* differs by input. To test that an action is correctly +**blocked** for some inputs, use a separate `.then(act.fail())` step instead (the spec uses +disabled actions, not a `success` boolean — see `patterns.md`). + +### Variable scope inside `.expect(...)` + +A `val` bound inside an `and { ... }` is **not** in scope for sibling conditions or an `if` guard in +the same block — you get an "unresolved name" error: + +```quint +// ❌ actualReward is not visible to the `if` below it +.expect(and { + val actualReward = reward - commission + balance == initial + actualReward, + if (actualReward > 0) balance > initial else true, // ERROR: actualReward not in scope +}) +``` + +Wrap the conditions in an `all { }` so the shared `val`s scope over all of them — and remember +`all { }` separates conditions with **commas**, not `and`: + +```quint +// ✅ shared vals scope over the whole all-block +.expect( + val actualReward = reward - commission + all { + balance == initial + actualReward, + if (actualReward > 0) balance > initial else true, + }) +``` + +--- + +## Running Tests + +```bash +# Run a specific test +quint test systemTest.qnt --main systemTest --match basicTest + +# Run all tests matching a pattern +quint test systemTest.qnt --main systemTest --match ".*" + +# Run with detailed trace output +quint test systemTest.qnt --main systemTest --match basicTest --verbosity 3 + +# Reproduce a failure with a seed +quint test systemTest.qnt --main systemTest --match basicTest --seed 0x1a2b3c +``` + +--- + +## Debugging Failures + +### `quint test` output is sparse — it does NOT show the state + +On a failure, `quint test` prints only the error code, the offending `run`, and a seed — **no +state, no trace, at any `--verbosity`** (even `--verbosity 5` adds nothing for a test). The two +failure modes read differently, and the error text is your only clue which one you hit: + +``` +Error [QNT508]: Expect condition does not hold true ← an .expect(...) evaluated to false +Error [QNT508]: Cannot continue to "expect" ← a .then(action) was DISABLED (its guard + was false), so the trace couldn't proceed +``` + +Both underline the **whole `run` expression**, not the specific `.expect` or action that failed, and +neither tells you the actual values. To debug, you must recover the state yourself — two reliable +ways below. + +### Recover the state — Option A: replay in the REPL (best for exploring) + +Feed `init` then each action of the failing trace into the REPL and query whatever the `.expect` +checked. Each action prints `true` and the state transition (`old => new`); then evaluate any +expression at the current state: + +```bash +printf 'init\ntransfer("alice","bob",50)\nstate.balances.get("alice")\n' \ + | quint -r system.qnt::system --backend=typescript +# >>> true +# { state: { balances: Map("alice" -> 100 => 50, "bob" -> 100 => 150) } } +# >>> 50 ← the value your .expect compared; here 50, so `== 999` is obviously false +``` + +**`--backend=typescript` is required for piped/non-interactive REPL input.** The default Rust +backend closes its readline on EOF and evaluates nothing (`ERR_USE_AFTER_CLOSE: readline was +closed`) — so without the flag this recipe silently produces no output. (Interactive TTY use works +on either backend; it's specifically piped stdin that needs `typescript`.) + +For nondeterministic stepping, set a seed so the run is reproducible: `.seed=` in the REPL +(or `--seed` on the CLI) makes every `nondet`/`oneOf` pick deterministic — same seed, same trace. +Capture the seed `quint test`/`quint run` prints on a failure and replay it to reproduce exactly. + +### Recover the state — Option B: dump the trace with `--out-itf` (scriptable) + +`quint test --out-itf` writes the full state trace of every test (passing *and* failing) to a JSON +file — useful in scripts or when you want the machine-readable trace: + +```bash +quint test systemTest.qnt --match myTest --out-itf "out_{test}_{seq}.itf.json" +# then read the states from out_myTest_0.itf.json (the last state is where it stopped) +``` + +### Then map the trace to the test code and classify the bug + +| Symptom | Type | Fix | +|---|---|---| +| Action doesn't update the field being checked | Spec bug | Fix the action's state update | +| `.expect()` checks a field before the action that sets it | Test bug | Move the `.expect()` later in the chain | +| `.expect()` uses wrong value | Test bug | Correct the expected value | +| Action sets a wrong value | Spec bug | Fix the pure function logic | + +### Common mistakes + +```quint +// ❌ Checking state before it's set +run bad = + init + .then(all { action1, assert(result == 42) }) // assert runs BEFORE action1 updates state + +// ✅ Check after +run good = + init + .then(action1) + .expect(result == 42) + +// ❌ Forgetting action order matters +run bad = + init + .then(approve(100)) + .expect(balance == INITIAL - 100) // approve doesn't deduct — transfer does + +// ✅ Complete the sequence +run good = + init + .then(approve(100)) + .then(transfer(100)) + .expect(balance == INITIAL - 100) +``` + +--- + +## REPL-First Debugging + +Before writing a failing test, isolate the problem in the REPL: + +```bash +# Interactive (TTY): either backend works +quint -r system.qnt::system + +# Force a specific state with an anonymous action, then step and query +>>> all { balances' = Set("alice").mapBy(_ => 100), phase' = "ready" } +true +>>> transfer("alice", "bob", 50) +true +>>> balances.get("alice") +50 +``` + +When driving the REPL **non-interactively** (piping commands, e.g. from a script or an agent), add +`--backend=typescript` — the default Rust backend evaluates nothing on piped stdin (see Option A +above): + +```bash +printf 'init\ntransfer("alice","bob",50)\nbalances.get("alice")\n' \ + | quint -r system.qnt::system --backend=typescript +``` + +If the REPL shows wrong output, the spec has a bug. If the REPL shows the right output but the test fails, the test chain has a sequencing error. diff --git a/.claude/skills/quint-modeling/LICENSE b/.claude/skills/quint-modeling/LICENSE new file mode 100644 index 000000000..08f754199 --- /dev/null +++ b/.claude/skills/quint-modeling/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2026 Informal Systems Inc. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/.claude/skills/quint-modeling/SKILL.md b/.claude/skills/quint-modeling/SKILL.md new file mode 100644 index 000000000..85172898a --- /dev/null +++ b/.claude/skills/quint-modeling/SKILL.md @@ -0,0 +1,466 @@ +--- +name: quint-modeling +description: > + Build a Quint model of a system, protocol, or algorithm. Use this whenever the user wants to + model, spec out, formally describe, model-check, or verify a system in Quint — e.g. "model this + protocol in Quint", "spec out this design", "translate this TLA+", "formally check this Rust + code" — even if they never say the word "specification." When the goal is to verify or + model-check a design or implementation and no Quint model exists yet, writing the model is the + required first step, so start here. It generates the spec from whatever the user has — an idea + developed interactively, natural-language or functional requirements, source code (Rust, Go, + TypeScript, etc.), or an existing TLA+ specification — and walks the modelling flow (state, + actions, invariants), adapting to the source type. Also use this to **review or audit an + existing Quint spec** — "review my .qnt", "audit this spec before I ship it", "is this model + any good" — it carries the structural + runtime review checklist. Do NOT use this for + implementing code against a spec that already exists (that's quint-execute-spec) or for pure + Quint syntax/CLI/debugging questions (quint-lang). For Quint language syntax and the CLI, see the + quint-lang reference. +--- + +# Quint Modelling + +Produce a Quint specification from whatever the user starts with. This skill owns the +**shared modelling discipline** (below) and **routes** to a flow-specific guideline for the +intake — the part that turns a particular kind of input into the understanding the shared +steps build on. + +For language syntax, operators, the CLI, and `basicSpells`, defer to the **quint-lang** +reference. This skill is about *how to model*, not Quint syntax. + +--- + +## Pick the flow + +Identify what the user is starting from, then read the matching guideline. The guideline +handles **intake** — extracting the system's state, operations, and assumptions from that +source. After intake, everyone converges on the **Shared modelling spine** below. + +| Starting point | Flow | Guideline | +|---|---|---| +| Only an idea / informal proposal, built interactively with the user | **from nothing** | `guidelines/from-nothing.md` | +| A written requirements / functional-spec document | **from requirements** | `guidelines/from-requirements.md` | +| Source code (Rust, Go, TypeScript, …) | **from code** | `guidelines/from-code.md` | +| An existing TLA+ specification | **from TLA+** | `guidelines/from-tlaplus.md` | +| A **finished `.qnt` spec to audit**, not build | **review** | `guidelines/review.md` | + +The first four are **build** flows: intake → the Shared modelling spine below. The **review** +flow is different — there is no new model to produce; you audit an existing spec against a +checklist and report findings. It does not use the spine; read `guidelines/review.md` and follow +it directly. + +If the starting point is ambiguous (e.g. "a design doc with some pseudocode"), ask the user +which source is authoritative before picking — the intake differs materially. + +--- + +## Shared modelling spine + +Every flow lands here. Intake (flow-specific) produces an **understanding** of the system: +its entities, the operations they perform, the state each operation reads and writes, and the +system-model assumptions (communication, failures, time, participants). The spine turns that +understanding into a verified Quint spec. + +Two principles hold throughout: + +- **Executable from the first line.** Quint specs run immediately — you validate design + decisions as you make them, not at the end. Never build more than one step without + verifying the previous one: `quint typecheck`, **then `quint run`**. Typecheck is not + enough — a spec can typecheck and still fail to *execute*, which defeats the whole point of + an executable spec. The trap to watch for: a **`const` not given a value** typechecks but + cannot run — `quint run` fails with `Uninitialized const`. To make the spec runnable, + **instantiate the const in a concrete instance module** — + `module spec_3 { import spec(C = Set(1,2,3)).* }` — and run *that* module. (`assume` documents a + premise; it does not supply a value — see Step 1 and quint-lang's `guidelines/simulations.md`.) + After each addition, actually run it — if you can't `quint run` the module, it isn't done. + **Use `quint run` only — never `quint verify`.** This holds for the whole skill: building, + iterating, reviewing, sanity-checking invariants — every step uses sampled `quint run`, not once + `quint verify`, not even as a final pass. `verify` is exhaustive bounded model checking + (Apalache): far slower (minutes to hours) and not part of the modeling workflow. It is a + *model-checking* tool, documented in quint-lang (`guidelines/cli.md`, `guidelines/simulations.md`) + — reach for it **only when the user explicitly asks to model-check** the spec, never on your own. +- **What, not how.** Model observable state transitions and their effects. Abstract away + implementation detail (serialization, memory management, retry plumbing). If a detail + doesn't affect an invariant you care about, it doesn't belong in the spec. + +#### Reference examples + +Two complete, runnable specs are bundled in `examples/`, one for each of the **two ways +components coordinate** — by **passing messages** or by **sharing state**. Almost any system maps +onto one of them; pick by *that* question, not by domain label, and read the closer match as a +worked instance of the spine patterns (Step 2 state-shaping, Step 4 guarded actions, Step 5 +witnesses + invariants) — to see how the pieces compose into a whole spec. (They are canonical +shapes to learn from, not the only valid ones.) + +| Example | Coordinates by… | Read it when modelling… | +|---|---|---| +| `examples/tendermint/` | **message passing** (`choreo::` broadcast/send; real BFT consensus) | **any distributed protocol where parties exchange messages** — consensus, BFT, replication, atomic commit, leader election, reliable broadcast/gossip, request/response, a mempool. This is the **default** reference for distributed systems. Shows: grouped `Id -> LocalState` (Step 2), guarded transitions (Step 4), `choreo::cue` listen/act split, safety invariants (`agreement`/`validity`) + an accountability/liveness angle + a counterexample demo (Step 5), `const`-instantiation, and test separation. Its banner has a "quick read" path so you needn't read all ~760 lines. See also Step 2's "When to use Choreo" and `../quint-lang/guidelines/choreo.md`. | +| `examples/ewd426.qnt` | **shared state** (no messages) | systems whose parts coordinate through **common state** rather than messages — mutexes/locks, token rings, shared registers, self-stabilization, anything where a process reads its neighbours/the environment directly. Shows: grouped-map state (Step 2), guarded `step` (Step 4), `const`-instantiation, and `temporal` **liveness** properties (Step 5). | + +If a system has both (e.g. message-passing nodes that also touch a shared ledger), start from +**tendermint** (the message-passing structure dominates) and add shared state as its own `var`, +per Step 2. Plain message *soup* (`Set[Msg]`) without the Choreo framework isn't a separate file — +Choreo's broadcast is soup underneath, so `tendermint/` is also the reference for that shape (read +the state decls + a guarded transition; the `choreo::` wrapper is the only added layer). + +### Step 1 — Separate concerns + +Partition the understanding into three layers. Keeping them apart is what makes a spec +testable; mixing them is the most common source of untestable specs. + +- **State machine** — variables, initialization, transitions → `var`, `init`, actions +- **Functional logic** — pure computations: guards, quorum checks, state updates → `pure def` +- **Properties** — what must always hold, what must be reachable, what must *eventually* happen → + `val` invariants + witnesses, plus `temporal` properties for liveness (Step 5; quint-lang has the detail) + +Also pin down the **system-model assumptions** — they shape every invariant built on top. +Encode them as **`const` declarations**. To actually *check* an assumption (e.g. a quorum +condition like `2 * f < n`), write a **`run` test** that asserts it — the `assume` keyword +*documents* a premise but is not enforced, so don't rely on it as a check (see quint-lang's +`## Assume` for why and the `run`-test pattern). Each flow's intake fills this in from its own +source (interview, requirements doc, code, or TLA+); the checklist is the same regardless: + +| Concern | Questions to answer | +|---|---| +| **Communication** | **How do the actors communicate — messages or shared state? If messages: reliable or lossy? ordered or unordered? broadcast or point-to-point?** (The other shaping question — answer it right after actors; it picks the message medium in Step 2 and, with the actor count, settles the Choreo decision.) | +| **Failures** | Crash-stop? Crash-recovery? Byzantine? What fraction `f` of `n`? | +| **Time** | Synchronous? Asynchronous? Partial synchrony? Are timeouts modelled? | +| **Actors / Participants** | **Who are the actors and roles, and what local state does each hold?** (This is the most concrete intake question — answer it first; it feeds Step 2's `Id -> LocalState` shaping directly.) Fixed membership or dynamic? How many processes? | + +If an assumption is wrong, every property built on it is wrong — surface them before building. + +### Step 2 — Shape the state + +**Start from the two questions you answered in Step 1 — *who the actors are* and *how they +communicate*. Together they drive every structural decision this step makes.** They are not just +background; they pick the shape, the message medium, and the framework: + +- **How many actors → the state shape.** One actor → a single `var s: Record`. N actors of the + same kind → one `Id -> LocalState` map (the record describes *one* actor; see "Scaling to N" + below). Distinct roles → either a field on `LocalState` (e.g. `role: Coordinator | Participant`) + or separate maps. Get the actor count/roles right and the shape falls out. +- **How actors communicate → the message medium.** Messages → a separate `var` for the medium, + *not* crammed into `LocalState`: unordered `Set[Message]` soup (the default), or `... -> + List[Message]` ordered per-pair queues only when delivery order is load-bearing. No messages, + coordination through common state → shared memory (no medium var; see `examples/ewd426.qnt`). + This is the "Communication shapes" choice detailed just below. +- **Actors + communication → Choreo or not.** Multiple actors coordinating by **exchanging + messages** → default to Choreo (see "Default to Choreo" below). A single actor, or actors + coordinating through **shared state** → plain Quint. So answer "who, how many, and how do they + talk?" first, and all three decisions below are mostly settled before you write a type. + +**Group cohesive state into a record** and let the functional layer operate on that record — this is +the recommended shape, because most of the time the variables that describe one entity *are* +cohesive, and grouping keeps the functional layer clean and the invariants readable. Keeping +variables flat is the deliberate exception, not a co-equal default: + +- **Group into a record when** the fields are the local state of one entity (a node's phase + log + + vote), are always passed together, or an invariant relates several of them. This is the usual case. +- **Keep flat (separate `var`s) only when** the variables are genuinely independent concerns that + change on their own, or the spec is small enough that grouping adds no clarity. (Some canonical + examples, e.g. `ewd840`, keep per-field maps flat because the fields don't form an obvious unit.) + +**The cohesive case — one unit:** + +```quint +type State = { + phase: str, + balances: NodeId -> int, + members: Set[NodeId], +} + +var state: State +``` + +The `apply…` pure functions take and return `State`; actions assign the next-state record directly +(`state' = applyTransfer(state, …)`). No per-field reassembly. + +**Scaling to N instances** — when there are N actors, the record describes **one** actor's +local state, and the variable becomes a map keyed by actor id. The pure functions are +**unchanged** — they still operate on a single `LocalState`; only the wiring around them +changes: + +```quint +type NodeId = int +type LocalState = { phase: str, balance: int, voted: bool } + +var nodes: NodeId -> LocalState // per-actor cohesive state +var messages: Set[Message] // genuinely global concern → its OWN var, not inside LocalState +``` + +| | One instance | N instances | +|---|---|---| +| state var | `var state: State` | `var nodes: NodeId -> LocalState` | +| pure fns | `can…(State, …): bool` + `apply…(State, …): State` | `can…(LocalState, …): bool` + `apply…(LocalState, …): LocalState` — same shape | +| action read | reads `state` | `nodes.get(id)` | +| action write | `state' = applyOp(state, …)` | `nodes' = nodes.set(id, applyOp(nodes.get(id), …))` | +| `init` | one record literal | `NODES.mapBy(_ => )` | + +The guideline, stated once: **group cohesive state into a record (one var for one unit, an +`Id -> LocalState` map for N), and keep genuinely independent concerns — the message soup, a shared +registry — as their own separate vars**, never crammed into the per-instance record. Reach for flat +per-field vars only when the fields don't cohere into a unit. + +**Communication shapes** (decide alongside the state shape): +- **Message soup** — `var network: Set[Message]`, processes receive any in-flight message. The + default for asynchronous protocols; use it unless ordering genuinely matters. +- **Shared memory** — no message medium; processes read/write common state directly. See the + bundled **`examples/ewd426.qnt`** (a token ring where each node reads its neighbours). +- **Ordered per-pair queues** — `... -> List[Message]` with head/tail ops. Use **only when + delivery order is semantically required** (e.g. logical-clock causality); it is more expensive + to model-check than soup. The corpus spec `LamportMutex` is the canonical example — prefer + soup unless you can name why ordering is load-bearing. + +#### Default to Choreo for distributed protocols + +For **any distributed, message-passing protocol with N processes** (consensus, BFT, replication, +multi-phase commit, broadcast/gossip, leader election), **default to the Choreo framework** — and +make a deliberate, justified decision if you are *not* going to. This isn't a stylistic toss-up: +Choreo's listen → react structure and its clean split between local-state updates and network +effects (the `choreo::cue` pattern) actively push you toward a better-organized, more reviewable +spec than a hand-rolled `NodeId -> LocalState` + message-soup `step`. The default expectation is +Choreo; plain Quint for a message-passing protocol is the thing that needs a reason. + +**The one legitimate reason to decline:** on a *small* protocol, Choreo's scaffolding (the type +boilerplate — `LocalContext`/`Transition`/effects — and framework wiring) can add more ceremony +than the spec's structure is worth, making it materially more verbose for little gain. That's a +real judgment call — but it is the **only** routine exception, and even then lean toward Choreo. +Two structural cases also fall outside Choreo: a **single actor** (no inter-process messaging to +choreograph) and **shared-memory coordination** (no message medium at all → plain Quint, see +`examples/ewd426.qnt`). + +Not a reason: *"still exploring the design."* You can explore *in* Choreo, and switching frameworks +later is expensive — so don't defer the decision on those grounds. + +**This is a structural fork — decide it before writing logic.** If you intend to go plain Quint for +a protocol that would otherwise be a Choreo candidate, **say so to the user, name the +verbosity/benefit tradeoff, and get agreement** (fold this into the type-sketch sign-off below). + +When Choreo fits, the per-process state still follows the grouping rule above — Choreo just +supplies the messaging and handler scaffolding around it. See +`../quint-lang/guidelines/choreo.md` for the framework's API and patterns, and +**`examples/tendermint/`** for a complete, runnable Choreo spec — real BFT consensus +demonstrating the `choreo::cue` listen/act split, `agreement`/`validity`/`accountability` +invariants, and `with_cue`-based tests in a separate `tendermintTest.qnt` (run via +`--main=valid`). + +Decide grouping (and Choreo-or-not) with the user and **get explicit approval on the type +sketch before writing any logic** (Step 3). Typecheck the types + `var` declarations first; +this is the highest-leverage review point — a wrong shape is expensive to unwind later. + +### Step 3 — Write the functional logic (pure functions) + +Implement each operation's logic as `pure def`s — they take the state record and arguments and +return plain values, so you can exercise them in the REPL with hand-built states. Split the two +distinct questions a transition answers: + +- **Can it happen?** — a `pure def … : bool` guard (the precondition). +- **What's the resulting state?** — a `pure def … : State` that computes the next state, *assuming* + the guard holds. + +```quint +pure def canTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): bool = + amount > 0 and from != recipient and s.balances.get(from) >= amount + +pure def applyTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): State = + { ...s, balances: s.balances.setBy(from, b => b - amount) + .setBy(recipient, b => b + amount) } +``` + +Write signatures first (stub the bodies), typecheck, then fill in one function at a time and +exercise each in the REPL with a hand-built state before moving on. If the output surprises +you, the function has a bug — fix it before wiring it into the state machine. + +> Keep the guard separate from the update because they are separate facts about the operation: one +> says *when* it is allowed, the other says *what it does*. The action (Step 4) uses the guard to +> decide whether it fires at all. A single `pure def` returning `{ success, newState }` — handing +> back the unchanged state when the guard fails — fuses the two and pushes the action toward a no-op +> branch; prefer the split. (If a *failed* operation is itself something the system observes and +> reacts to, model that failure as its own guarded action, not as a fallback.) + +### Step 4 — Wire the state machine (guarded actions) + +An action puts the guard and the update together in one `all { ... }`: the guard gates whether the +action fires, the update sets the next state. When the guard is false the action is **disabled** — +it does not fire and does not change anything. No `success` flag, no no-op branch. + +```quint +action init: bool = all { + state' = { phase: "idle", + balances: NODES.mapBy(_ => INITIAL_BALANCE), // pre-populate every map + members: NODES }, +} + +action transferAction(from: NodeId, recipient: NodeId, amount: int): bool = all { + canTransfer(state, from, recipient, amount), // guard — disables the action when false + state' = applyTransfer(state, from, recipient, amount), +} +``` + +A disabled action is the faithful model of "this cannot happen in this state." Resist adding a +blanket `else` / `unchanged_all` fallback to keep things moving — that puts a transition in the +model that the real system can't take, which is a modeling inaccuracy regardless of what you do +with the spec afterward. + +An action and a `pure def` cannot share a name. Pre-populate every map in `init` — `.get()` on an +absent key is undefined behavior. See quint-lang for the full list of such gotchas. + +### Step 5 — Properties: witnesses first, then invariants + +**Witnesses first.** A witness names a target state and asks whether it is *reachable* — write the +predicate **positively** (the state you hope to reach) and pass it to `quint run --witnesses`, which +reports **how many sampled traces reached it**. Add one per major action: a witness reached in 0 +traces means the action is dead (its precondition can never hold), so fix that before spending +effort on safety. + +```quint +// the state you want to be reachable — written plainly, no negation +val someBalanceChanged: bool = + state.members.exists(n => state.balances.get(n) != INITIAL_BALANCE) +``` + +``` +quint run spec.qnt --witnesses someBalanceChanged --max-steps 10 + → someBalanceChanged was witnessed in 90 trace(s) out of 100 explored (90.00%) +``` + +A non-zero count means the state is reachable; **0% means it never happened** — investigate. + +There is a second, complementary form: write the *negation* as an invariant — `val w = not(target)` +— so a reported "violation" is an execution that *reaches* the state. It can't batch with the other +invariants and you read a "violation" as success, but it gives you something `--witnesses` cannot: an +**actual trace** that reaches the state. Pick by what you need — `--witnesses` for the routine +reachability + coverage check, the negated-invariant form when you want to *see the path* (to +understand or document how the state is reached, or to debug a witness that fires unexpectedly). + +**Then invariants** — the safety properties that must hold in every reachable state: + +```quint +val noNegativeBalances: bool = + state.members.forall(n => state.balances.get(n) >= 0) +``` + +Invariants and witnesses run together in one pass: `quint run --invariant noNegativeBalances +--witnesses someBalanceChanged`. + +When a source yields *many* candidate properties and you need to prioritize verification effort, +the from-requirements flow describes a High/Medium/Low impact-scoring aid (`guidelines/from-requirements.md`); +it applies wherever you're modelling against stated requirements. + +(Witness vs invariant interpretation, fairness, and temporal properties are detailed in quint-lang's +`guidelines/simulations.md`. `someBalanceChanged` is *state* evidence — phrase such a target so only +an action can make it true, since a predicate that already holds at `init` is "reached" at step 0 and +witnesses nothing. To confirm a *specific* action fired when several could reach the same state, use a +per-action flag `var` — quint-lang's `guidelines/patterns.md` §7 covers it and how to debug a witness +that never fires.) + +### Step 6 — Compose `step` and simulate + +Compose the actions in `any { ... }` and stress the model with random walks. + +```quint +action step: bool = { + nondet from = NODES.oneOf() + nondet dst = NODES.oneOf() // `dst`, not `to` (a built-in) — see quint-lang + any { + transferAction(from, dst, 10), + // other actions… + } +} +``` + +- Check **witnesses** with `quint run --witnesses` — expect a non-zero trace count (reachable); + 0% means a dead action. +- Check **invariants** with `quint run` (sampled) — expect no violation; read counterexample + traces step by step when one appears. Use `quint run` for this, not `quint verify` (see the + "Executable from the first line" principle — `verify` is only for when the user explicitly asks + to model-check). + +#### A guarded model can reach a state where nothing is enabled + +Because actions are guarded (Step 4), the model can reach a state with **no enabled action**. The +trap during a build: **`quint run` does not detect deadlocks** — it stops early and prints `[ok] No +violation found` with a trace shorter than `--max-steps`. A short trace is the only hint, and the +run reads as success, so watch trace length when you expect the protocol to keep going. (For the +record, `quint verify` reports a deadlock outright — `Found a deadlock` — but that's a +model-checking step, only in play if the user explicitly asks for it; don't switch to `verify` just +to chase a suspected deadlock mid-build — inspect the short trace with `quint run` instead.) + +Whether reaching such a state is correct depends on the system: one that should keep serving must +never get stuck, while one that genuinely finishes (everyone committed, nothing left to do) is +*supposed* to end in a terminal state. The tool can't tell these apart — only you know which you +intended. (This is the other reason Step 4 avoids the no-op fallback: a blanket `unchanged_all` +lets every trace extend forever, so the model can never reach — or reveal — such a state.) + +**A note on bounding.** `--max-steps` (how deep a run explores) is not a modeling decision — it's +always there. Whether the *model itself* has a bounded state space is: some protocols are +**terminating by construction** (a one-shot commit reaches a final state and stops), and modeling +them that way is correct — reaching a terminal state is the design, not a deadlock. You may also +bound an otherwise-unbounded model deliberately to shrink the state space, but never with a no-op +escape hatch (Step 4) — bound it by modeling the real terminal states, not by a fake step. + +Tests (`run` definitions) go in a **separate `*_test.qnt` file** that imports the spec — keep +the main module free of test scenarios. Build incrementally: typecheck after every addition, +simulate after every action. + +### Step 7 — Self-review, then hand off the spec + +Before writing the handoff record, do a quick pass over your own spec against the same bar a +reviewer would apply — catching these now is cheaper than having them bounce back. Most you've +already followed while building; this is the closing check that they all hold together: + +- **Guarded actions** — no business logic in an action beyond the guard and assignments; it lives + in `pure def`s, and the guard is lifted into the action so it's disabled when it can't fire (Step 4). +- **Witness per major action** — every action in `step` has a witness, and each one is reached in + > 0 traces under `quint run --witnesses`, not dead at 0 traces (Step 5). +- **At least one protocol-level invariant** — a real safety property (no two leaders, conservation, + agreement), not just a type/bounds check; and every invariant references a `var`. +- **`init` assigns every `var`** and every action assigns every `var` (a missing `x' = x` is a + silent stutter bug); every map is pre-populated (Step 4). +- **Right abstraction** — IDs are opaque (no string manipulation), messages are a `Set` unless + ordering is the property, no serialization/retry/memory detail leaked in. + +If a spec is large or being handed to someone else, run the full audit in `guidelines/review.md` +(the C1–C6 / R1–R2 checklist with a report) — reach for it when a self-pass isn't enough. + +A finished spec needs a short record so the next reader knows its scope and can trust it. +Produce one (as a comment block, a `README.md`, or whatever the flow prefers) covering: + +- **What it covers** — which modules/protocols are modelled, which assumptions (`const` + declarations, with `run`-test checks for the ones that must hold) are encoded, which + properties are verified. +- **What it does NOT cover** — implementation detail left out on purpose, edge cases excluded + (and why), properties still to add. This honesty note is what stops the spec from being + over-trusted. +- **When to update it** — for a spec that grounds an artifact (code, a TLA+ source), update + the spec and re-verify *before* changing the artifact. + +**The spec is the ground truth. Never edit the spec to match broken code.** If the spec is +wrong, stop and discuss with the user — that is the highest-leverage review point. + +Each flow adds its own format detail (source-file correspondence for code, a translation +README with recorded `quint run` output for TLA+, a comment block for an interactive build). + +--- + +## Conventions + +- `NodeId` / `LocalState` for per-actor state, and `NODES` for the participant set (the `Set[NodeId]` + the model ranges over); descriptive type names after the protocol (`VoteRequest`, `PrepareMsg`) not + `Msg1`, `Msg2`. +- Small domains: `N = 3` actors (or `N = 2` for first exploration) and value ranges like + `0..10` are enough for most safety properties and keep simulation cheap. Use **symbolic IDs** + (`int` or `str`) for participants. +- Message soup: store sent messages in one `Set` and don't model delivery order unless + ordering is what you're verifying. +- Abstract time: when the protocol has a notion of time or progress, model it as an integer + **round/epoch counter** (`round: int`), not wall-clock time or timer mechanics — a timeout is + just the round advancing. Exception: model timing explicitly only when the timing bound + itself is what you're verifying. +- Start with **one action**: get `init` + one action + one witness working before adding the + rest. For N actors, model **one actor first, verify, then generalize** to the map — never + wire up all N at once. +- Test pure functions in **isolation** in the REPL with hand-built states; that catches logic + bugs before they get tangled into the state machine. + +For everything syntactic — operators, undefined-behavior rules, `basicSpells`, the CLI flags — +consult the **quint-lang** reference rather than reproducing it here. diff --git a/.claude/skills/quint-modeling/examples/README.md b/.claude/skills/quint-modeling/examples/README.md new file mode 100644 index 000000000..9f8c5623f --- /dev/null +++ b/.claude/skills/quint-modeling/examples/README.md @@ -0,0 +1,60 @@ +# Reference examples + +Two fully-runnable Quint specs, bundled so an agent can read a *complete* model end-to-end — +not just the inline snippets in `SKILL.md`. They are chosen to contrast on the axis that drives +a model's whole shape: **how processes communicate**. + +Pick by **how the parts coordinate** — passing messages or sharing state — not by domain label. +Almost any system maps onto one; read the closer match as a worked instance of the spine patterns. + +| Example | Coordinates by… | Read it when modelling… | Illustrates (spine patterns) | +|---|---|---|---| +| [`tendermint/`](tendermint/tendermint.qnt) | **message passing** (`choreo::`; real BFT consensus) | **any distributed protocol where parties exchange messages** — consensus, BFT, replication, atomic commit, leader election, reliable broadcast/gossip, request/response, mempool. The **default** distributed-systems reference. | grouped `Id -> LocalState` (Step 2), guarded transitions (Step 4), `choreo::cue` listen/act split, `agreement`/`validity`/`accountability` invariants + counterexample demo (Step 5), `const`-instantiation, test separation | +| [`ewd426.qnt`](ewd426.qnt) | **shared state** (no messages) | parts coordinate through **common state** — mutexes/locks, token rings, shared registers, self-stabilization, reading neighbours/environment directly | grouped-map state (Step 2), guarded `step` (Step 4), `const`-instantiation, `temporal` **liveness** (Step 5) | + +Both message *soup* (plain `Set[Msg]`, no framework) and hybrid systems (message-passing + a +shared ledger) route through **tendermint** — Choreo's broadcast is soup underneath, and when a +system has both, the message-passing structure dominates (add shared state as its own `var`, per +Step 2). + +`tendermint/` is large (~760 lines — a real protocol is large); its banner has a **"quick read"** +path so you can learn the `cue` pattern without reading the whole spec, and the per-read token +cost is paid only when an agent actually opens it. + +Justified-*exception* shapes (ordered per-pair queues, flat variables, the contract Result-record +pattern) are intentionally left to prose in `SKILL.md` / the guidelines, not bundled — a bundled +example exerts a "copy me" pull we don't want pointing at exceptions. + +## Maintenance contract + +These are **owned copies**, snapshotted from the official corpus +(`mcp-servers/kb/kb/examples/`). They must be kept `quint`-clean across Quint upgrades. + +| File(s) | Upstream source | +|---|---| +| `ewd426.qnt` | `classic/distributed/ewd426/ewd426.qnt` | +| `tendermint/{tendermint,tendermintTest,choreo}.qnt`, `tendermint/spells/basicSpells.qnt` | `advanced/tendermint/` | + +For most files only a top-of-file teaching banner was added; the spec bodies are otherwise +byte-for-byte upstream, so re-syncing is a near-clean diff. **Exception — `tendermint/`:** upstream +ships a single `tendermint.qnt` with its `run` tests inline. We split it per the test-separation +guideline (`quint-lang/guidelines/tests.md`): the spec stays in `tendermint.qnt` (no `run`s), and +the `valid` + `no_agreement` instance/test modules moved to `tendermintTest.qnt` — the only body +change being a `from "./tendermint"` clause added to each `import tendermint(...)`. (We drop +upstream's `tendermintMicro.qnt`, `test_witness.sh`, `witness_bench.py`, and `spells/rareSpells.qnt`, +none of which this example needs.) + +- **Pinned Quint version:** 0.32.0 (last verified). + +### Re-verify (run from this directory after any Quint upgrade) + +```sh +quint typecheck ewd426.qnt +quint run ewd426.qnt --main=ewd426 --max-steps 15 + +cd tendermint +quint typecheck tendermint.qnt # spec alone — no runs +quint run tendermintTest.qnt --main=valid --invariant="agreement and validity and accountability" --max-steps 12 +quint test tendermintTest.qnt --main=valid # line28Test must pass +quint test tendermintTest.qnt --main=no_agreement # disagreementTest must pass +``` diff --git a/.claude/skills/quint-modeling/examples/ewd426.qnt b/.claude/skills/quint-modeling/examples/ewd426.qnt new file mode 100644 index 000000000..4ee7fb571 --- /dev/null +++ b/.claude/skills/quint-modeling/examples/ewd426.qnt @@ -0,0 +1,110 @@ +/** + * ewd426's Stabilizing Token Ring (EWD426) + * K state machine + * This implementation ensures that from some time on, + * exactly one token circulates in a set of nodes, + * + * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025 + */ + +/* ============================================================================= + * quint-modeling REFERENCE EXAMPLE — communication model: SHARED MEMORY + * ----------------------------------------------------------------------------- + * Why this is bundled: it is the canonical *shared-memory* shape — there is NO + * message medium. Processes coordinate by reading common state: each node's + * `state_transition` reads its left/right neighbours in `var system: int -> State`. + * Contrast with the Choreo example (tendermint/), which is message-passing. + * + * Demonstrates, against the quint-modeling guidelines: + * - Grouped-map state `var system: int -> State` (one entry per node). + * - Guarded action `step` picks a node that *can* move; no no-op fallback. + * - Logic in pure defs `has_token`, `state_transition`, `count_tokens`. + * - const-instantiation the parametric `self_stabilization` module is run via + * the concrete `ewd426` instance (N = 5, K = 7). This is + * the pattern the skill's spine teaches: a `const` cannot + * run until instantiated. Run with `--main=ewd426`. + * - temporal LIVENESS `convergence` / `closure` / `persistence` — the system + * self-stabilizes to exactly one token. (The only bundled + * example with temporal properties.) + * + * The `broken_ewd426` instance (N = 3, K = 2) is a deliberately-broken config kept for + * contrast — useful to show what a property *failing* looks like. + * + * Verified clean on Quint 0.32.0. See ../examples/README.md for re-verification commands. + * ============================================================================= */ +module self_stabilization { + // Number of nodes in the ring + const N: int + const K: int + + /// Ensures the state space is larger than the number of nodes + assume _ = K >= N + + val bottom = 0 + val top = N + + /// Mapping of node indices to their states + var system: int -> int + + /// Check if a node has the token + pure def has_token(nodes: int -> int, index: int): bool = + if (index == bottom) + nodes.get(bottom) == nodes.get(top) + else + not(nodes.get(index) == nodes.get(index - 1)) + + /// Update the state of a specific node + pure def state_transition(nodes: int -> int, index: int): int = + if (not(has_token(nodes, index))) + nodes.get(index) + else if (index == bottom) + (nodes.get(bottom) + 1) % K + else + nodes.get(index - 1) + + /// Initialize all nodes with non-deterministic states + action init = all { + nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf() + system' = initial + } + + /// Pick a single active node non-deterministically and update its state + action step = { + nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf() + system' = system.set(node, state_transition(system, node)) + } + + /// Pick several active nodes non-deterministically and update their state. + /// Closer to the distributed demon is discussed in EWD 391. We are not + /// considering interleaving in the execution of state_transition here + action distributed_step = { + nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf() + system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x))) + } + + // Pure function to count how many tokens exist + pure def count_tokens(nodes: int -> int): int = { + 0.to(N).filter(i => has_token(nodes, i)).size() + } + + // Temporal properties + temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1) + temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1)) + temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1)) + + // Invariant + def tokenInv = count_tokens(system) > 0 + + /// to better see the token in the repl + pure def show_token(nodes: int -> int): int -> bool = + nodes.keys().mapBy(i => has_token(nodes, i)) +} + +module ewd426 { + import self_stabilization(N = 5, K = 7).* +} + +module broken_ewd426 { + // This should break the assumption of K >= N. See #1182. + import self_stabilization(N = 3, K = 2).* +} diff --git a/.claude/skills/quint-modeling/examples/tendermint/choreo.qnt b/.claude/skills/quint-modeling/examples/tendermint/choreo.qnt new file mode 100644 index 000000000..4845ffbb3 --- /dev/null +++ b/.claude/skills/quint-modeling/examples/tendermint/choreo.qnt @@ -0,0 +1,295 @@ +/** + * Choreo: Choreograph distributed protocols in Quint + * + * Read the documentation: TODO LINK + * + * Gabriela Moreira, Josef Widder and Yassine Boukhari, + * Informal Systems, 2025 + */ + +module choreo { + import basicSpells.* from "spells/basicSpells" + + // TODO: try moving process id to local context + type LocalState[process_id, ext] = { + process_id: process_id + | ext + } + + type Transition[p, s, m, e, ce] = { + post_state: LocalState[p, s], + effects: Set[Effect[p, m, e, ce]], + } + + type GlobalContext[p, s, m, e, ext] = { + system: p -> LocalState[p, s], + messages: p -> Set[m], + events: p -> Set[e], + extensions: ext + } + + type LocalContext[p, s, m, e, ext] = { + state: LocalState[p, s], + messages: Set[m], + events: Set[e], + extensions: ext + } + + // This is the message routing to the # handler + type Listener[p, s, m, e, ce, ext] = + (LocalContext[p, s, m, e, ext]) => Set[Transition[p, s, m, e, ce]] + + type DeterministicListener[p, s, m, e, ce, ext] = + (LocalContext[p, s, m, e, ext]) => Transition[p, s, m, e, ce] + + // Only needed for micro_step + type Input[m, e] = Message(m) | Event(e) + + // Only needed for micro_step + type MicroListener[p, s, m, e, ce, ext] = + (LocalContext[p, s, m, e, ext], Input[m, e]) => Set[Transition[p, s, m, e, ce]] + + type EffectProcessor[p, s, m, e, ce, ext] = + (GlobalContext[p, s, m, e, ext], ce) => GlobalContext[p, s, m, e, ext] + + + type Effect[p, m, e, ce] = + | Broadcast(m) + | Send({ to: p, message: m }) + | TriggerEvent(e) + | CustomEffect(ce) + + /// A displayer is a function that takes a global context and returns a displayable representation of it. + /// This is used to visualize the state of the system for debugging or monitoring purposes. + /// After type instantiation, it should have the following signature: + /// ``` + /// (Environment) => Display + /// ``` + /// The display type can be anything. + type Displayer[p, s, m, e, ext, d] = (GlobalContext[p, s, m, e, ext]) => d + + pure def apply_effect( + env: GlobalContext[p, s, m, e, ext], + v: p, + tr: Transition[p, s, m, e, ce], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, ext] + ): GlobalContext[p, s, m, e, ext] = { + val env1 = { ...env, system: env.system.setBy(v, s => tr.post_state) } + + tr.effects.fold(env1, (e, effect) => { + match effect { + | Broadcast(m) => { + { ...e, messages: e.messages.transformValues(b => b.setAdd(m)) } + } + | Send(r) => { + { ...e, messages: e.messages.setBy(r.to, b => b.setAdd(r.message)) } + } + | TriggerEvent(ev) => { + { ...e, events: e.events.setBy(v, b => b.setAdd(ev)) } + } + | CustomEffect(ex) => { + apply_custom_effect(e, ex) + } + } + }) + } + + const processes: Set[p] + var s: GlobalContext[p, s, m, e, ext] + var display: d + + pure def initialize(x: a, f: Option[(a) => Set[b]]): Set[b] = { + match f { + | Some(fun) => fun(x) + | None => Set() + } + } + + pure def convert_context( + env: GlobalContext[p, s, m, e, ext], + v: p + ): LocalContext[p, s, m, e, ext] = { + { + state: env.system.get(v), + messages: env.messages.get(v), + events: env.events.get(v), + extensions: env.extensions + } + } + + action process_transitions( + v: p, + transitions: Set[Transition[p, s, m, e, ce]], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions], + ): bool = + // FIXME: Quint was supposed to detect determinism alone + if (transitions.size() == 1) { + val transition = transitions.getOnlyElement() + val post_env = apply_effect(s, v, transition, apply_custom_effect) + s' = post_env + } else { + nondet transition = oneOf(transitions) + val post_env = apply_effect(s, v, transition, apply_custom_effect) + s' = post_env + } + + action process_transitions_with_displayer( + v: p, + transitions: Set[Transition[p, s, m, e, ce]], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions], + displayer: Displayer[p, s, m, e, extensions, d], + ): bool = + // FIXME: Quint was supposed to detect determinism alone + if (transitions.size() == 1) { + val transition = transitions.getOnlyElement() + val post_env = apply_effect(s, v, transition, apply_custom_effect) + all { + s' = post_env, + display' = displayer(post_env), + } + } else { + nondet transition = oneOf(transitions) + val post_env = apply_effect(s, v, transition, apply_custom_effect) + all { + s' = post_env, + display' = displayer(post_env), + } + } + + action init(ctx: GlobalContext[p, s, m , e, ext]): bool = { + s' = ctx + } + + action init_with_displayer( + ctx: GlobalContext[p, s, m , e, ext], + displayer: Displayer[p, s, m, e, extensions, d], + ): bool = all { + s' = ctx, + display' = displayer(ctx) + } + + action step( + listener: Listener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions] + ): bool = { + nondet v = oneOf(processes) + val input = convert_context(s, v) + val transitions = listener(input).filter(t => t.effects.size() > 0 or t.post_state != input.state) + process_transitions(v, transitions, apply_custom_effect) + } + + action step_with_displayer( + listener: Listener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions], + displayer: Displayer[p, s, m, e, extensions, d] + ): bool = { + nondet v = oneOf(processes) + val input = convert_context(s, v) + val transitions = listener(input).filter(t => t.effects.size() > 0 or t.post_state != input.state) + process_transitions_with_displayer(v, transitions, apply_custom_effect, displayer) + } + + action micro_step( + listener: MicroListener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions] + ): bool = { + nondet process = processes.oneOf() + val ctx = convert_context(s, process) + any { + nondet msg = s.messages.get(process).oneOf() + val transitions = listener(ctx, Message(msg)) + process_transitions(process, transitions, apply_custom_effect), + + nondet event = s.events.get(process).oneOf() + val transitions = listener(ctx, Event(event)) + process_transitions(process, transitions, apply_custom_effect), + } + } + + action step_with( + v: p, + listener: Listener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions] + ): bool = { + val input = convert_context(s, v) + val transitions = listener(input).filter(t => t.effects.size() > 0 or t.post_state != input.state) + process_transitions(v, transitions, apply_custom_effect) + } + + action step_deterministic( + v: p, + listener: DeterministicListener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions] + ): bool = { + val input = convert_context(s, v) + val transitions = Set(listener(input)).filter(t => t.effects.size() > 0 or t.post_state != input.state) + process_transitions(v, transitions, apply_custom_effect) + } + + action step_with_filter( + v: p, + listener: Listener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions], + f: (Transition[p, s, m, e, ce]) => bool + ): bool = { + val input = convert_context(s, v) + val transitions = listener(input).filter(t => t.effects.size() > 0 or t.post_state != input.state).filter(f) + process_transitions(v, transitions, apply_custom_effect) + } + + action step_with_messages( + v: p, + listener: Listener[p, s, m, e, ce, extensions], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, extensions], + f: Set[m] => Set[m] + ): bool = { + val input = convert_context(s, v) + val input1 = { ...input, messages: f(input.messages) } + val transitions = listener(input1).filter(t => t.effects.size() > 0 or t.post_state != input.state) + process_transitions(v, transitions, apply_custom_effect) + } + + action lose_messages(v: p, f: Set[m] => Set[m]): bool = { + val msgs = s.messages.get(v) + val new_msgs = msgs.exclude(f(msgs)) + all { + s' = { ...s, messages: s.messages.set(v, new_msgs) } + } + } + + pure def cue( + ctx: LocalContext[p, s, m, e, ext], + listen_fn: (LocalContext[p, s, m, e, ext]) => Set[r], + upon_fn: (LocalContext[p, s, m, e, ext], r) => Transition[p, s, m, e, ce] + ): Set[Transition[p, s, m, e, ce]] = { + val params = listen_fn(ctx) + params.map(param => upon_fn(ctx, param)) + } + + type CueResult[p, s, m, e, ext, r] = CueOk({ ctx: LocalContext[p, s, m, e, ext], params: r }) | NoCue + + def with_cue( + process: p, + listen_fn: (LocalContext[p, s, m, e, ext]) => Set[r], + params: r + ): CueResult[p, s, m, e, ext, r] = { + val ctx = convert_context(s, process) + val valid_params = listen_fn(ctx) + val is_valid = valid_params.contains(params) + if (is_valid) + CueOk({ ctx: ctx, params: params }) + else + NoCue + } + + action perform( + cue_result: CueResult[p, s, m, e, ext, r], + upon_fn: (LocalContext[p, s, m, e, ext], r) => Transition[p, s, m, e, ce], + apply_custom_effect: EffectProcessor[p, s, m, e, ce, ext], + ): bool = { + match cue_result { + | CueOk(cue) => process_transitions(cue.ctx.state.process_id, Set(upon_fn(cue.ctx, cue.params)), apply_custom_effect) + | NoCue => all { false, s' = s } + } + } +} diff --git a/.claude/skills/quint-modeling/examples/tendermint/spells/basicSpells.qnt b/.claude/skills/quint-modeling/examples/tendermint/spells/basicSpells.qnt new file mode 100644 index 000000000..6c75bcbe7 --- /dev/null +++ b/.claude/skills/quint-modeling/examples/tendermint/spells/basicSpells.qnt @@ -0,0 +1,388 @@ +/** + * This module collects definitions that are ubiquitous. + * One day they will become the standard library of Quint. + */ +module basicSpells { + /// Option type, which may hold some value or none + type Option[a] = Some(a) | None + + /// An annotation for writing preconditions. + /// - @param cond condition to check + /// - @returns true if and only if cond evaluates to true + pure def require(cond: bool): bool = cond + + run requireTest = all { + assert(require(4 > 3)), + assert(not(require(false))), + } + + /// A convenience operator that returns a string error code, + /// if the condition does not hold true. + /// + /// - @param cond condition to check + /// - @param error a non-empty error message + /// - @returns "", when cond holds true; otherwise error + pure def requires(cond: bool, error: str): str = { + if (cond) "" else error + } + + run requiresTest = all { + assert(requires(4 > 3, "4 > 3") == ""), + assert(requires(4 < 3, "false: 4 < 3") == "false: 4 < 3"), + } + + + /// Compute the maximum of two integers. + /// + /// - @param i first integer + /// - @param j second integer + /// - @returns the maximum of i and j + pure def max(i: int, j: int): int = { + if (i > j) i else j + } + + run maxTest = all { + assert(max(3, 4) == 4), + assert(max(6, 3) == 6), + assert(max(10, 10) == 10), + assert(max(-3, -5) == -3), + assert(max(-5, -3) == -3), + } + + /// Compute the minimum of two integers. + /// + /// - @param i first integer + /// - @param j second integer + /// - @returns the minimum of i and j + pure def min(i: int, j: int): int = { + if (i < j) i else j + } + + run minTest = all { + assert(min(3, 4) == 3), + assert(min(6, 3) == 3), + assert(min(10, 10) == 10), + assert(min(-3, -5) == -5), + assert(min(-5, -3) == -5), + } + + /// Compute the absolute value of an integer + /// + /// - @param i : an integer whose absolute value we are interested in + /// - @returns |i|, the absolute value of i + pure def abs(i: int): int = { + if (i < 0) -i else i + } + + run absTest = all { + assert(abs(3) == 3), + assert(abs(-3) == 3), + assert(abs(0) == 0), + } + + /// Remove a set element. + /// + /// - @param s a set to remove an element from + /// - @param elem an element to remove + /// - @returns a new set that contains all elements of set but elem + pure def setRemove(s: Set[a], elem: a): Set[a] = { + s.exclude(Set(elem)) + } + + run setRemoveTest = all { + assert(Set(2, 4) == Set(2, 3, 4).setRemove(3)), + assert(Set() == Set().setRemove(3)), + } + + /// Adds an element to a set. + /// + /// - @param s a set to add an element to + /// - @param elem an element to add + /// - @returns a new set that contains all elements of set and elem + pure def setAdd(s: Set[a], elem: a): Set[a] = { + s.union(Set(elem)) + } + + run setAddTest = all{ + assert(Set(2, 3, 4) == Set(2, 4).setAdd(3)), + assert(Set(3) == Set().setAdd(3)), + assert(Set(2,4) == Set(2,4).setAdd(4)), + } + + /// Test whether a key is present in a map + /// + /// - @param m a map to query + /// - @param key the key to look for + /// - @returns true if and only map has an entry associated with key + pure def has(m: a -> b, key: a): bool = { + m.keys().contains(key) + } + + run hasTest = all { + assert(Map(2 -> 3, 4 -> 5).has(2)), + assert(not(Map(2 -> 3, 4 -> 5).has(6))), + } + + /// Get the map value associated with a key, or the default, + /// if the key is not present. + /// + /// - @param m the map to query + /// - @param key the key to search for + /// - @returns the value associated with the key, if key is + /// present in the map, and default otherwise + pure def getOrElse(m: a -> b, key: a, default: b): b = { + if (m.has(key)) { + m.get(key) + } else { + default + } + } + + run getOrElseTest = all { + assert(Map(2 -> 3, 4 -> 5).getOrElse(2, 0) == 3), + assert(Map(2 -> 3, 4 -> 5).getOrElse(7, 11) == 11), + } + + /// Remove a map entry. + /// + /// - @param m a map to remove an entry from + /// - @param key the key of an entry to remove + /// - @returns a new map that contains all entries of map + /// that do not have the key key + pure def mapRemove(m: a -> b, key: a): a -> b = { + m.keys().setRemove(key).mapBy(k => m.get(k)) + } + + run mapRemoveTest = all { + assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)), + assert(Map() == Map().mapRemove(3)), + } + + /// Removes a set of map entries. + /// + /// - @param m a map to remove entries from + /// - @param ks a set of keys for entries to remove from the map + /// - @returns a new map that contains all entries of map + /// that do not have a key in keys + pure def mapRemoveAll(m: a -> b, ks: Set[a]): a -> b = { + m.keys().exclude(ks).mapBy(k => m.get(k)) + } + + run mapRemoveAllTest = + val m = Map(3 -> 4, 5 -> 6, 7 -> 8) + all { + assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)), + assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)), + } + + /// Get the set of values of a map. + /// + /// - @param map a map from type a to type b + /// - @returns the set of all values in the map + pure def values(m: a -> b): Set[b] = { + m.keys().map(k => m.get(k)) + } + + run valuesTest = all { + assert(values(Map()) == Set()), + assert(values(Map(1 -> 2, 2 -> 3)) == Set(2, 3)), + assert(values(Map(1 -> 2, 2 -> 3, 3 -> 2)) == Set(2, 3)), + } + + /// Whether a set is empty + /// + /// - @param s a set of any type + /// - @returns true iff the set is the empty set + pure def empty(s: Set[a]): bool = s == Set() + + run emptyTest = all { + assert(empty(Set()) == true), + assert(empty(Set(1, 2)) == false), + assert(empty(Set(Set())) == false), + } + + /// Sort a list, given the ordering operator. + /// + /// - @param list a list to sort + /// - @param lt a definition of "less than" + /// - @returns the sorted version of list + pure def sortList(list: List[a], lt: (a, a) => bool): List[a] = { + pure def insertInOrder(sortedList: List[a], num: a): List[a] = { + match range(0, sortedList.length()).findFirst(i => not(lt(sortedList[i], num))) { + | None => sortedList.append(num) + | Some(index) => sortedList.slice(0, index).append(num).concat(sortedList.slice(index, sortedList.length())) + } + } + + list.foldl([], (sortedList, num) => insertInOrder(sortedList, num)) + } + + run listSortedTest = all { + assert([ 1, 3, 5 ] == sortList([ 5, 1, 3 ], (x, y) => x < y)), + assert([ 1, 1, 3, 5, 5 ] == sortList([ 5, 1, 3, 1, 5 ], (x, y) => x < y)), + } + + /// Apply an operator to all values of a map + /// + /// - @param m: a map of any type + /// - @param f: an operator with one argument with the same type as the map's values + /// - @returns a map with same keys as m and f applied to the values + pure def transformValues(m: a -> b, f: (b) => c): a -> c = { + m.keys().mapBy(k => f(m.get(k))) + } + + run transformValuesTest = { + pure val m = Map("a" -> 1, "b" -> 2) + assert(m.transformValues(x => x + 1) == Map("a" -> 2, "b" -> 3)) + } + + /// map a function over a list + /// + /// - @param l: a list of any type + /// - @param f: a function to apply to each element of the list + /// - @returns a list of the results of applying f to each element of l + pure def listMap(l: List[a], f: (a) => b): List[b] = { + range(0, l.length()).foldl([], (acc, i) => { + acc.append(f(l[i])) + }) + } + + run listMapTest = all { + assert(listMap([1, 2, 3], x => x + 1) == [2, 3, 4]), + assert(listMap([1, 2, 3], x => x > 1) == [false, true, true]), + } + + /// The last element of a list + /// + /// - @param v: a list of any type + /// - @returns the last element of the list + pure def last(v: List[a]): a = { + v[v.length() - 1] + } + + run lastTest = all { + assert(last([1, 2, 3]) == 3), + assert(last([1]) == 1), + } + + /// `decreasingRange(i, j)` is the list of integers between `j` and `i` + /// both `i` and `j` are inclusive. + /// The behavior is undefined if `i < j`. + /// + /// - @param start: the first integer in the range + /// - @param end: the last integer in the range + pure def decreasingRange(start: int, end: int): List[int] = { + range(end, start + 1).foldl([], (acc, i) => { + List(i).concat(acc) + }) + } + + run decreasingRangeTest = all { + assert(decreasingRange(5, 1) == [5, 4, 3, 2, 1]), + } + + /// `takeWhile(l, cond)` is the longest prefix of `l` such that all elements + /// satisfy the condition `cond`. + /// + /// - @param l: a list of any type + /// - @param cond: a function that takes an element of the list and returns a boolean + /// - @returns the longest prefix of `l` such that all elements satisfy `cond` + pure def takeWhile(l: List[a], cond: (a) => bool): List[a] = { + pure val result = l.foldl(([], true), (acc, e) => { + if (acc._2 and cond(e)) { + (acc._1.append(e), true) + } else { + (acc._1, false) + } + }) + + result._1 + } + + run takeWhileTest = all { + assert(takeWhile([1, 5, 4, 3], (x) => x % 2 == 1) == [1, 5]), + } + + /// `isPrefixOf(l1, l2)` is true iff `l1` is a prefix of `l2`. + /// + /// - @param l1: a list of any type + /// - @param l2: a list of same type as `l1` + /// - @returns true iff `l1` is a prefix of `l2` + pure def isPrefixOf(l1: List[a], l2: List[a]): bool = { + if (l1.length() > l2.length()) { + false + } else { + l1.indices().forall(i => l1[i] == l2[i]) + } + } + + run isPrefixOfTest = all { + assert(isPrefixOf([1, 2], [1, 2, 3])), + assert(not(isPrefixOf([1, 2], [1, 3, 2]))), + assert(not(isPrefixOf([1, 2], [1]))), + assert(isPrefixOf([], [1, 2])), + assert(isPrefixOf([], [])), + } + + /// `find(s, f)` is an element of `s` that satisfies the predicate `f`, or None + /// if no such element exists. + /// + /// - @param s: a set of any type + /// - @param f: a function that takes an element of the set and returns a boolean + /// - @returns an element of `s` that satisfies `f`, or None + pure def find(s, f) = s.fold(None, (a, i) => if (f(i)) Some(i) else a) + + run findTest = all { + assert(find(Set(1, 2, 3), x => x == 2) == Some(2)), + assert(find(Set(1, 2, 3), x => x == 4) == None), + } + + /// `findFirst(l, f)` is the first element of `l` that satisfies the predicate `f`, or None + /// if no such element exists. + /// + /// - @param l: a list of any type + /// - @param f: a function that takes an element of the list and returns a boolean + /// - @returns the first element of `l` that satisfies `f`, or None + pure def findFirst(l, f) = l.foldl(None, (a, i) => if (a == None and f(i)) Some(i) else a) + + run findFirstTest = all { + assert(findFirst([1, 2, 3], x => x > 1) == Some(2)), + assert(findFirst([1, 2, 3], x => x == 4) == None), + } + + /// `setByWithDefault(m, k, op, default)` is a map that is the same as `m` except that + /// the value associated with `k` is `op(m[k])` if `k` is present in `m`, and `op(default)` otherwise. + /// + /// - @param m: a map from type `a` to type `b` + /// - @param k: a key of type `a` + /// - @param op: a function to transform the value of the key + /// - @param default: the value to use if the key is not present in the map + /// - @returns a new map with the updated key. + pure def setByWithDefault(m: a -> b, k: a, op: (b) => b, default: b): a -> b = { + if (m.has(k)) + m.setBy(k, op) + else + m.put(k, default).setBy(k, op) + } + + run setByWithDefaultTest = all { + assert(setByWithDefault(Map(1 -> 2, 2 -> 3), 1, x => x + 1, 0) == Map(1 -> 3, 2 -> 3)), + assert(setByWithDefault(Map(1 -> 2, 2 -> 3), 3, x => x + 1, 0) == Map(1 -> 2, 2 -> 3, 3 -> 1)), + } + + pure def unwrap(value: Option[a]): a = { + match value { + | None => Map().get(value) + | Some(x) => x + } + } + + pure def filterMap(s: Set[a], f: (a) => Option[b]): Set[b] = { + s.fold(Set(), (acc, e) => { + match f(e) { + | Some(x) => acc.union(Set(x)) + | None => acc + } + }) + } +} diff --git a/.claude/skills/quint-modeling/examples/tendermint/tendermint.qnt b/.claude/skills/quint-modeling/examples/tendermint/tendermint.qnt new file mode 100644 index 000000000..26dfde0f6 --- /dev/null +++ b/.claude/skills/quint-modeling/examples/tendermint/tendermint.qnt @@ -0,0 +1,800 @@ +/* ============================================================================= + * quint-modeling REFERENCE EXAMPLE — communication model: MESSAGE-PASSING (Choreo) + * ----------------------------------------------------------------------------- + * Why this is bundled: it is the canonical *Choreo framework* spec — a real BFT + * consensus engine (Tendermint), and the source of the examples in + * ../../../quint-lang/guidelines/choreo.md. Choreo is a different programming model + * from plain Quint (its own `choreo::` API), so it cannot be inferred — you have to + * see one. Contrast with the shared-memory example (../ewd426.qnt). + * + * READ THIS when modelling ANY distributed protocol where parties exchange messages — + * consensus/BFT, replication, atomic commit, leader election, reliable broadcast/gossip, + * request/response, a mempool. It is the default reference for message-passing systems + * (not just consensus); the patterns below transfer. Use ../ewd426.qnt instead only when + * parts coordinate through SHARED STATE rather than messages. + * + * Demonstrates the `choreo::cue` PATTERN — separate *when* from *what*: + * - `listen_*(ctx): Set[Params]` — the messages/conditions that match (Set[()] for + * state/quorum-only triggers). + * - `broadcast_*` / `act_*(ctx, p): Transition` — the reaction for each match. + * - `main_listener` wires them with `choreo::cue(ctx, listen, act)` (x7) — reads + * like the protocol at a glance. + * Plus: real `agreement` / `validity` / `accountability` invariants. + * + * QUICK READ (to learn the pattern without reading all ~760 lines — anchored to + * names so it survives upstream re-sync): read `listen_proposal_in_propose` + + * `broadcast_prevote_for_proposal` (one cue pair), then `main_listener` (the wiring), + * then the `agreement` / `validity` / `accountability` invariants. The rest is full + * protocol depth. + * + * TESTS: in the sibling `tendermintTest.qnt` (this spec has no `run`s, per the + * test-separation guideline — quint-lang/guidelines/tests.md). That file also holds + * the concrete instances; the spec here is parametric (const F/CORRECT/FAULTY/...), + * so it cannot run on its own — run an instance: + * quint run tendermintTest.qnt --main=valid --invariant="agreement and validity and accountability" + * The `no_agreement` instance there is a deliberate agreement-violation demo. + * + * Dependencies (bundled alongside): ./choreo.qnt, ./spells/basicSpells.qnt. + * Verified clean on Quint 0.32.0. See ../README.md for re-verification commands. + * ============================================================================= */ +module tendermint { + import basicSpells.* from "./spells/basicSpells" + import choreo(processes = NODES) as choreo from "./choreo" + + type Round = int + type Stage = ProposeStage | PreVoteStage | PreCommitStage | DecidedStage + type Value = str + + type Bookkeeping = { + evidence_propose: Set[ProposeMsg], + evidence_prevote: Set[PreVoteMsg], + evidence_precommit: Set[PreVoteMsg], + } + + type TimeoutKind = ProposeTimeout | PreVoteTimeout | PreCommitTimeout + type TimeoutEvent = { kind: TimeoutKind, round: Round } + + /// The ID of a value. In the implementation, this would be a hash of the value. + /// Here, we wrap it in a record and don't convert it back into a value. + /// This keeps the property that v1.id() == v2.id() iff v1 == v2. + type ValueId = { hashed: Value } + type Node = str + + type StateFields = { + round: Round, + stage: Stage, + decision: Option[Value], + locked_value: Option[Value], + locked_round: Round, + valid_value: Option[Value], + valid_round: Round, + after_prevote_for_first_time: bool, + precommit_quorum: bool, + } + + type ProposeMsg = { + src: Node, + round: Round, + proposal: Value, + valid_round: Round, + } + + type PreVoteMsg = { + src: Node, + round: Round, + id: Option[ValueId], + } + + type Message = + | Propose(ProposeMsg) + | PreVote(PreVoteMsg) + | PreCommit(PreVoteMsg) + + type CustomEffects = CollectEvidence(Message) + type Event = TimeoutEvent + type Extensions = Bookkeeping + + /* Boilerplate */ + type LocalState = choreo::LocalState[Node, StateFields] + type LocalContext = choreo::LocalContext[Node, StateFields, Message, Event, Extensions] + type Transition = choreo::Transition[Node, StateFields, Message, Event, CustomEffects] + type GlobalContext = choreo::GlobalContext[ + Node, + StateFields, + Message, + Event, + Extensions + ] + /* End of boilerplate */ + + pure def get_proposals(messages: Set[Message]): Set[ProposeMsg] = + messages.filterMap(m => { + match m { + | Propose(p) => Some(p) + | _ => None + } + }) + + pure def get_pre_votes(messages: Set[Message]): Set[PreVoteMsg] = + messages.filterMap(m => { + match m { + | PreVote(p) => Some(p) + | _ => None + } + }) + + pure def get_pre_commits(messages: Set[Message]): Set[PreVoteMsg] = + messages.filterMap(m => { + match m { + | PreCommit(p) => Some(p) + | _ => None + } + }) + + pure def source(message: Message): Node = + match message { + | Propose(p) => p.src + | PreVote(p) => p.src + | PreCommit(p) => p.src + } + + pure def valid(v: Value): bool = { + VALID_VALUES.contains(v) + } + + pure def id(v: Value): ValueId = { hashed: v } + + pure def start_round(ctx: LocalContext, round: Round): Transition = { + val s = ctx.state + + pure val effect = + if (s.process_id == PROPOSER.get(round)) { + pure val proposal = + if (s.valid_value != None) + s.valid_value.unwrap() + else + VALUES.get(round) + + choreo::Broadcast( + Propose({ src: s.process_id, round: round, proposal: proposal, valid_round: s.valid_round }) + ) + } else { + choreo::TriggerEvent({ kind: ProposeTimeout, round: s.round }) + } + { + effects: Set(effect), + post_state: { + ...s, + round: round, + stage: ProposeStage, + precommit_quorum: false, + } + } + } + + pure def listen_proposal_in_propose(ctx: LocalContext): Set[ProposeMsg] = { + val s = ctx.state + val messages = ctx.messages + + val state_guard = and { + s.stage == ProposeStage + } + + // Message guards: predicates on the messages that can use the state as context + def message_guard = (p) => and { + p.valid_round == -1, + p.src == PROPOSER.get(s.round), + } + + // Apply Guards + val proposals = messages.get_proposals() + proposals.filter(p => and { + message_guard(p), + state_guard + }) + } + + pure def broadcast_prevote_for_proposal(ctx: LocalContext, p: ProposeMsg): Transition = { + val s = ctx.state + + // Broadcast the PreVote message for the proposal + pure val effects = if (valid(p.proposal) and (s.locked_round == -1 or s.locked_value == Some(p.proposal))) { + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: Some(id(p.proposal)) }))) + } else { + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: None }))) + } + + // TODO -> add timeout and logging effects + { + post_state: { ...s, stage: PreVoteStage }, + effects: effects.setAdd(choreo::CustomEffect(CollectEvidence(Propose(p)))) + } + } + + pure def listen_proposal_in_propose_prevote(ctx: LocalContext): Set[ProposeMsg] = { + val s = ctx.state + val messages = ctx.messages + + val state_guard = and { + s.stage == ProposeStage, + } + + def message_guard = (p) => and { + p.src == PROPOSER.get(s.round), + p.valid_round >= 0, + p.valid_round < s.round + } + + val proposals = messages.get_proposals().filter(p => and { + message_guard(p), + state_guard, + }) + + val pre_votes = messages.get_pre_votes() + proposals.filter(p => and { + pre_votes.filter(q => q.id == Some(p.proposal.id()) and q.round == p.valid_round).size() >= 2 * F + 1 // quorum size is F + 1 + }) + } + + pure def broadcast_prevote_with_validation(ctx: LocalContext, p: ProposeMsg): Transition = { + val s = ctx.state + val messages = ctx.messages + + // Collect evidence for prevotes that contributed to this decision + val contributing_prevotes = messages.get_pre_votes().filter(pv => + pv.round == p.valid_round and pv.id == Some(id(p.proposal)) + ) + val prevote_evidence = contributing_prevotes.map(pv => choreo::CustomEffect(CollectEvidence(PreVote(pv)))) + val evidence = Set(choreo::CustomEffect(CollectEvidence(Propose(p)))).union(prevote_evidence) + + // Broadcast the PreVote message for the proposal + val effects = if (valid(p.proposal) and (s.locked_round <= p.valid_round or s.locked_value == Some(p.proposal))) { + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: Some(id(p.proposal))}))) + } else { + Set(choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: None }))) + } + + { + post_state: { ...s, stage: PreVoteStage }, + effects: effects.union(evidence) + } + } + + + pure def listen_quorum_prevotes_any(ctx: LocalContext): Set[()] = { + val s = ctx.state + val messages = ctx.messages + + // Do we have a quorum of PreVotes in the current round + def message_guard = (pv) => (pv.round == s.round) + val quorum = messages.get_pre_votes().filter(pv => and { + message_guard(pv), + }).size() >= 2 * F + 1 // quorum size is F + 1 + + if (quorum) { + Set(()) + } else { + Set() + } + } + + pure def trigger_prevote_timeout(ctx: LocalContext, _params: ()): Transition = { + val s = ctx.state + + // If we have a quorum, we can move to precommit stage + { + post_state: s, + effects: Set(choreo::TriggerEvent({ kind: PreVoteTimeout, round: s.round })) + } + } + + pure def listen_quorum_nil_prevotes(ctx: LocalContext): Set[()] = { + val s = ctx.state + val messages = ctx.messages + + val state_guard = and { + s.stage == PreVoteStage, + } + + // Do we have a quorum of PreVotes in the current round + def message_guard = (pv) => (pv.round == s.round and pv.id == None) + val prevotes = messages.get_pre_votes().filter(pv => message_guard(pv)) + val quorum = prevotes.map(m => m.src).size() >= 2 * F + 1 + + if (quorum and state_guard) { + Set(()) + } else { + Set() + } + } + + pure def broadcast_nil_precommit(ctx: LocalContext, _params: ()): Transition = { + val s = ctx.state + val messages = ctx.messages + + // Collect evidence for all nil prevotes that enabled this decision + val nil_prevotes = messages.get_pre_votes().filter(pv => + pv.round == s.round and pv.id == None + ) + val prevote_evidence = nil_prevotes.map(pv => choreo::CustomEffect(CollectEvidence(PreVote(pv)))) + + // If we have a quorum, we can move to precommit stage + { + post_state: { ...s, stage: PreCommitStage }, + effects: Set( + choreo::Broadcast(PreCommit({ src: s.process_id, round: s.round, id: None })) + ).union(prevote_evidence) + } + } + + pure def listen_quorum_precommits_any(ctx: LocalContext): Set[()] = { + val s = ctx.state + val messages = ctx.messages + + // Do we have a quorum of PreCommits in the current round + def message_guard = (pc) => (pc.round == s.round) + val quorum = messages.get_pre_commits().filter(pc => and { + message_guard(pc), + }).map(m => m.src).size() >= 2 * F + 1 // quorum size is F + 1 + + if (quorum) { + Set(()) + } else { + Set() + } + } + + pure def trigger_precommit_timeout(ctx: LocalContext, _params: ()): Transition = { + val s = ctx.state + + // If we have a quorum, we can move to decided stage + { + post_state: s, + effects: Set(choreo::TriggerEvent({ kind: PreCommitTimeout, round: s.round })) + } + } + + pure def listen_proposal_in_prevote_commit(ctx: LocalContext): Set[ProposeMsg] = { + val s = ctx.state + val messages = ctx.messages + + val state_guard = and { + s.stage.in(Set(PreVoteStage, PreCommitStage)) + } + + def message_guard = (p) => and { + p.src == PROPOSER.get(s.round), + p.round == s.round + } + + val proposals = messages.get_proposals() + val pre_votes = messages.get_pre_votes() + + proposals.filter(p => and { + message_guard(p), + state_guard, + // Check for quorum of prevotes for this proposal in current round + pre_votes.filter(pv => and { + pv.round == s.round, + pv.id == Some(id(p.proposal)) + }).map(pv => pv.src).size() >= 2 * F + 1 + }) + } + + pure def lock_value_and_precommit(ctx: LocalContext, p: ProposeMsg): Transition = { + val s = ctx.state + val messages = ctx.messages + + // Collect evidence for prevotes that enabled this decision + val enabling_prevotes = messages.get_pre_votes().filter(pv => + pv.round == s.round and pv.id == Some(id(p.proposal)) + ) + val prevote_evidence = enabling_prevotes.map(pv => choreo::CustomEffect(CollectEvidence(PreVote(pv)))) + + if (s.stage == PreVoteStage) { + // If in prevote stage, broadcast precommit and move to precommit stage + { + // Move to precommit stage and update values + post_state: { + ...s, + stage: PreCommitStage, + valid_value: Some(p.proposal), + valid_round: s.round, + locked_value: Some(p.proposal), + locked_round: s.round + }, + effects: Set( + choreo::Broadcast(PreCommit({ src: s.process_id, round: s.round, id: Some(id(p.proposal)) })), + choreo::CustomEffect(CollectEvidence(Propose(p))) + ).union(prevote_evidence) + } + } else { + // Just update valid value if already in precommit + { + post_state: { + ...s, + valid_value: Some(p.proposal), + valid_round: s.round + }, + effects: Set(choreo::CustomEffect(CollectEvidence(Propose(p)))).union(prevote_evidence) + } + } + } + + pure def listen_proposal_in_precommit_no_decision(ctx: LocalContext): Set[ProposeMsg] = { + val s = ctx.state + val messages = ctx.messages + + val state_guard = and { + s.decision == None + } + + def message_guard = (p) => and { + p.src == PROPOSER.get(p.round), + p.round <= s.round // Can decide on current or past rounds + } + + val proposals = messages.get_proposals() + val pre_commits = messages.get_pre_commits() + + proposals.filter(p => and { + message_guard(p), + state_guard, + // Check for quorum of precommits for this proposal + pre_commits.filter(pc => and { + pc.round == p.round, + pc.id == Some(id(p.proposal)) + }).map(pc => pc.src).size() >= 2 * F + 1 + }) + } + + pure def decide_on_proposal(ctx: LocalContext, p: ProposeMsg): Transition = { + val s = ctx.state + val messages = ctx.messages + + // Collect evidence for precommits that enabled this decision + val enabling_precommits = messages.get_pre_commits().filter(pc => + pc.round == p.round and pc.id == Some(id(p.proposal)) + ) + val precommit_evidence = enabling_precommits.map(pc => choreo::CustomEffect(CollectEvidence(PreCommit(pc)))) + + // Make decision and move to decided stage + { + post_state: { + ...s, + decision: Some(p.proposal), + stage: DecidedStage + }, + effects: Set(choreo::CustomEffect(CollectEvidence(Propose(p)))).union(precommit_evidence) + } + } + + pure def on_propose_timeout(ctx: LocalContext): Set[Transition] = { + val s = ctx.state + + val candidates = ctx.events.filter(t => t.round >= s.round and t.kind == ProposeTimeout) + val guard = and { + candidates.size() > 0, + s.stage == ProposeStage, + } + + if (guard) + Set({ + post_state: { ...s, stage: PreVoteStage }, + effects: Set( + choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: None })), + choreo::TriggerEvent({ kind: PreVoteTimeout, round: s.round }) + ), + }) + else + Set() + } + + pure def on_prevote_timeout(ctx: LocalContext): Set[Transition] = { + val s = ctx.state + + val candidates = ctx.events.filter(t => t.round >= s.round and t.kind == PreVoteTimeout) + val guard = and { + candidates.size() > 0, + s.stage == PreVoteStage, + } + + if (guard) + Set({ + post_state: { ...s, stage: PreCommitStage }, + effects: Set( + choreo::Broadcast(PreVote({ src: s.process_id, round: s.round, id: None })), + choreo::TriggerEvent({ kind: PreCommitTimeout, round: s.round }) + ), + }) + else + Set() + } + + pure def on_precommit_timeout(ctx: LocalContext): Set[Transition] = { + val s = ctx.state + + val candidates = ctx.events.filter(t => t.round >= s.round and t.kind == PreCommitTimeout) + val guard = and { + candidates.size() > 0, + s.stage == PreCommitStage, + } + + if (guard) + Set(start_round(ctx, s.round + 1)) + else + Set() + } + + pure def main_listener(ctx: LocalContext): Set[Transition] = + Set( + choreo::cue(ctx, listen_proposal_in_propose, broadcast_prevote_for_proposal), + choreo::cue(ctx, listen_proposal_in_propose_prevote, broadcast_prevote_with_validation), + choreo::cue(ctx, listen_proposal_in_precommit_no_decision, decide_on_proposal), + choreo::cue(ctx, listen_proposal_in_prevote_commit, lock_value_and_precommit), + choreo::cue(ctx, listen_quorum_prevotes_any, trigger_prevote_timeout), + choreo::cue(ctx, listen_quorum_nil_prevotes, broadcast_nil_precommit), + choreo::cue(ctx, listen_quorum_precommits_any, trigger_precommit_timeout), + on_propose_timeout(ctx), + on_prevote_timeout(ctx), + on_precommit_timeout(ctx) + ).flatten() + + pure val initial_message = + Propose({ src: PROPOSER.get(0), round: 0, proposal: VALUES.get(0), valid_round: -1 }) + + pure val initial_bookkeeping = { + evidence_propose: Set(), + evidence_prevote: Set(), + evidence_precommit: Set(), + } + + def initialize_process(n: Node): LocalState = { + { + process_id: n, + round: 0, + stage: ProposeStage, + decision: None, + locked_value: None, + locked_round: -1, + valid_value: None, + valid_round: -1, + after_prevote_for_first_time: false, + precommit_quorum: false, + } + } + + // Card(powset) = 4096 + val byzantine_messages_1 = { + val rounds = Set(0) + val byzantine_proposals = rounds.map(r => { + tuples(FAULTY, Set("v0","v1","v2"), rounds.setAdd(-1)).map(((f, v, vr)) => { + Propose({ src: f, round: r, proposal: v, valid_round: vr }) + }) + }).flatten() + + val byzantine_prevotes = rounds.map(r => { + tuples(FAULTY, Set("v0","v1","v2")).map(((f, v)) => { + PreVote({ src: f, round: r, id: Some(v.id()) }) + }) + }).flatten() + + val byzantine_precommits = rounds.map(r => { + tuples(FAULTY, Set("v0","v1","v2")).map(((f, v)) => { + PreCommit({ src: f, round: r, id: Some(v.id()) }) + }) + }).flatten() + + // Reintegrate byzantine proposals + Set(byzantine_prevotes, byzantine_precommits, byzantine_proposals).flatten() + } + + // TODO (Gabriela): I don't understand this + val byzantine_messages = { + // We can have at most 2^F faulty nodes, so we take the powerset of the byzantine messages + // to simulate all possible combinations of byzantine messages. + + // 10 dummy prevotes for future rounds + val dummy_prevotes = 1000.to(1025).map(r => { + PreVote({ src: "p4", round: r, id: None }) + }) + dummy_prevotes + //Set() + } + + action init = choreo::init({ + system: NODES.mapBy(n => initialize_process(n)), + messages: NODES.mapBy(n => Set(initial_message).union(byzantine_messages_1)), + events: NODES.mapBy(n => Set()), + extensions: initial_bookkeeping + }) + + def apply_custom_effect(env: GlobalContext, effect: CustomEffects): GlobalContext = { + match effect { + | CollectEvidence(msg) => { + pure val updated_bookkeeping = match msg { + | Propose(p) => { ...env.extensions, evidence_propose: env.extensions.evidence_propose.setAdd(p) } + | PreVote(p) => { ...env.extensions, evidence_prevote: env.extensions.evidence_prevote.setAdd(p) } + | PreCommit(p) => { ...env.extensions, evidence_precommit: env.extensions.evidence_precommit.setAdd(p) } + } + { ...env, extensions: updated_bookkeeping } + } + } + } + + action step = choreo::step( + main_listener, + apply_custom_effect + ) + + + // -------------------------------- semantic symmetry utilities -------------------------------- + // TODO: Update these functions to work with choreo library + /* + type StateFingerprint = { + round: Round, + stage: Stage, + decision: Option[Value], + locked_value: Option[Value], + locked_round: Round, + valid_value: Option[Value], + valid_round: Round, + after_prevote_for_first_time: bool, + precommit_quorum: bool, + is_proposer: bool, + } + + pure def select_representatives(s: GlobalState): Set[Node] = { + val states = s.system.values() + val unique = group_by_fingerprint(states) + unique.setByAll((k, group) => group.filter(n =>(n.in(CORRECT))).takeOne()). + values().filter(n => n != None).map(n => n.unwrap()) + } + + def group_by_fingerprint(s: Set[LocalState]): StateFingerprint -> Set[Node] = { + val init = Map() + s.fold(init, (acc, state) => { + val key = { + round: state.round, + stage: state.stage, + decision: state.decision, + locked_value: state.locked_value, + locked_round: state.locked_round, + valid_value: state.valid_value, + valid_round: state.valid_round, + after_prevote_for_first_time: state.after_prevote_for_first_time, + precommit_quorum: state.precommit_quorum, + is_proposer: state.process_id == PROPOSER.get(state.round) + } + acc.setByWithDefault(key, (e) => e.setAdd(state.process_id),Set()) + }) + } + */ + // -------------------------------- semantic symmetry utilities -------------------------------- + + val correct_nodes = s.system.values().filter(s => s.process_id.in(CORRECT)) + val agreement = tuples(correct_nodes, correct_nodes).forall(((p1, p2)) => { + p1.decision == None or p2.decision == None or p1.decision == p2.decision + }) + + val one_decided = + not(s.system.values().forall(v => v.decision == None)) + + val all_decided = + not(correct_nodes.exists(v => v.decision == None)) + + // Witness for a to find a case where a node is in the decided stage while another is prevote + // state + val stages = + and { + s.system.values().map(v => v.stage).contains(ProposeStage), + s.system.values().map(v => v.stage).contains(PreVoteStage), + s.system.values().map(v => v.stage).contains(PreCommitStage), + s.system.values().map(v => v.stage).contains(DecidedStage) + } + + // Evidence-based properties + + pure def equivocation_in(n: Node, evidence: Set[{ src: Node, round: Round | other }]): bool = { + tuples(evidence, evidence).exists(((e1, e2)) => { + e1 != e2 and e1.src == n and e2.src == n and e1.round == e2.round + }) + } + + /// Equivocation by a node n + def equivocation_by(n: Node): bool = { + or { + n.equivocation_in(s.extensions.evidence_propose), + n.equivocation_in(s.extensions.evidence_prevote), + n.equivocation_in(s.extensions.evidence_precommit), + } + } + + /// Amnesic behavior by a node n + def amnesia_by(n: Node): bool = { + tuples(ROUNDS, ROUNDS).exists(((r1, r2)) => { + r1 < r2 and tuples(VALID_VALUES, VALID_VALUES).exists(((v1, v2)) => { + and { + v1 != v2, + s.extensions.evidence_propose.contains({ + src: n, round: r1, proposal: v1, valid_round: r1 + }), + s.extensions.evidence_propose.contains({ + src: n, round: r2, proposal: v2, valid_round: r2 + }), + ROUNDS.filter(r => r1 <= r and r < r2).forall(r => { + s.extensions.evidence_prevote.filter(m => { + m.round == r and m.id == Some(id(v2)) + }).size() >= 2 * F + 1 + }), + } + }) + }) + } + + /// Validity: the decided block satisfies the predefined predicate valid(). + val validity = correct_nodes.forall(s => s.decision.in(VALID_VALUES.map(v => Some(v)).setAdd(None))) + + /// The protocol safety. Two cases are possible: + /// 1. There is no fork, that is, Agreement holds true. + /// 2. A subset of faulty processes demonstrates equivocation or amnesia. + val accountability = or { + agreement, + FAULTY.powerset().exists(f => and { + f.size() >= F + 1, + f.forall(n => equivocation_by(n) or amnesia_by(n)), + }) + } + + const F: int + /// The set of correct processes + const CORRECT: Set[Node] + /// The set of faulty processes + const FAULTY: Set[Node] + /// Which node is the proposer in each round + const PROPOSER: Round -> Node + /// Which value is proposed in each round. + /// Values from rounds with correct nodes (in PROPOSER) are considered valid values. + const VALUES: Round -> Value + const MAX_ROUND: Round + + /// The set of all nodes + pure val NODES = CORRECT.union(FAULTY) + /// The set of all rounds (prepared by the constants) + pure val ROUNDS = VALUES.keys() + + /// The set of all correct values (prepared by the constants) + //pure val VALID_VALUES = ROUNDS.filter(k => PROPOSER.get(k).in(CORRECT)).map(k => VALUES.get(k)) + pure val VALID_VALUES = Set("v0", "v1", "v2") + + action step_with(v: Node, listener: LocalContext => Set[Transition]): bool = + choreo::step_with(v, listener, apply_custom_effect) + + action step_deterministic(v: Node, listener: LocalContext => Transition): bool = + choreo::step_deterministic(v, listener, apply_custom_effect) + + def with_cue(process, listen_fn, params) = + choreo::with_cue(process, listen_fn, params) + + action perform(cue_ctx, upon_fn) = + choreo::perform(cue_ctx, upon_fn, apply_custom_effect) + + action step_with_filter( + v: Node, + listener: LocalContext => Set[Transition], + f: Transition => bool + ): bool = + choreo::step_with_filter(v, listener, apply_custom_effect, f) + + action step_with_messages( + v: Node, + listener: LocalContext => Set[Transition], + f: Set[Message] => Set[Message] + ): bool = + choreo::step_with_messages(v, listener, apply_custom_effect, f) + + action lose_messages = choreo::lose_messages + + val s = choreo::s +} + diff --git a/.claude/skills/quint-modeling/examples/tendermint/tendermintTest.qnt b/.claude/skills/quint-modeling/examples/tendermint/tendermintTest.qnt new file mode 100644 index 000000000..8d0cc8a2d --- /dev/null +++ b/.claude/skills/quint-modeling/examples/tendermint/tendermintTest.qnt @@ -0,0 +1,98 @@ +/* ============================================================================= + * Tests for the Tendermint Choreo reference example. + * + * Per the test-separation guideline (quint-lang/guidelines/tests.md), `run` tests + * live in this file, NOT in the spec — `tendermint.qnt` has no `run` definitions. + * Each module here instantiates the parametric `tendermint` spec with concrete + * consts (the const-instantiation pattern) and drives a scenario: + * - `valid` — a run where consensus succeeds; `line28Test` exercises the + * proposal/prevote/precommit cue chain across a round change. + * - `no_agreement` — a faulty proposer equivocates; `disagreementTest` shows the + * `agreement` invariant being violated (a counterexample demo). + * + * Run / test (from this directory): + * quint run tendermintTest.qnt --main=valid --invariant="agreement and validity and accountability" + * quint test tendermintTest.qnt --main=valid + * quint run tendermintTest.qnt --main=no_agreement --invariant=accountability + * quint test tendermintTest.qnt --main=no_agreement + * ============================================================================= */ +module valid { + // quint run tendermintTest.qnt --main valid --invariant="agreement and validity and accountability" + // quint test tendermintTest.qnt --main valid + + import basicSpells.* from "./spells/basicSpells" + + import tendermint( + F = 1, + CORRECT = Set("p1","p2", "p3"), + FAULTY = Set("p4"), + PROPOSER = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4"), + VALUES = Map(0 -> "v0", 1 -> "v1", 2 -> "v2", 3 -> "v3"), + MAX_ROUND = 4 + ).* from "./tendermint" + + run line28Test = { + val v0_proposal = { proposal: "v0", round: 0, src: "p1", valid_round: -1 } + + init + .then("p1".with_cue(listen_proposal_in_propose, v0_proposal).perform(broadcast_prevote_for_proposal)) + .then("p2".with_cue(listen_proposal_in_propose, v0_proposal).perform(broadcast_prevote_for_proposal)) + + .then("p1".with_cue(listen_proposal_in_prevote_commit, v0_proposal).perform(lock_value_and_precommit)) + .then("p2".with_cue(listen_proposal_in_prevote_commit, v0_proposal).perform(lock_value_and_precommit)) + + .then("p2".with_cue(listen_quorum_precommits_any, ()).perform(trigger_precommit_timeout)) + + .then(step_with("p2", on_precommit_timeout)) + // p2 starts a new round + .expect(s.system.get("p2").round == 1) + + // since p2 is the proposer in the new round, it will propose the stored valid value + .expect(and { + s.system.get("p2").stage == ProposeStage, + s.messages.values().forall(ms => { + ms.contains(Propose({ src: "p2", round: 1, proposal: "v0", valid_round: 0 })) + }) + }) + + // Which enables line 28 to be called by p2, as it is in propose stage and can receive + // the new proposal with valid_round 0. + .then("p2" + .with_cue(listen_proposal_in_propose_prevote, { proposal: "v0", round: 1, src: "p2", valid_round: 0 }) + .perform(broadcast_prevote_with_validation) + ) + } +} + +module no_agreement { + // Should fail: + // quint run tendermintTest.qnt --main no_agreement --invariants=agreement validity accountability + // + // Should succeed (accountability should still hold): + // quint run tendermintTest.qnt --main no_agreement --invariant=accountability + // quint test tendermintTest.qnt --main no_agreement + + import tendermint( + F = 1, + CORRECT = Set("p1", "p2"), + FAULTY = Set("p3","p4"), + // a faulty node is the proposer in the first round + PROPOSER = Map(0 -> "p3", 1 -> "p2", 2 -> "p3", 3 -> "p4"), + VALUES = Map(0 -> "v0", 1 -> "v1", 2 -> "v2", 3 -> "v3"), + MAX_ROUND = 4 + ).* from "./tendermint" + + run disagreementTest = { + val v0_proposal = { proposal: "v0", round: 0, src: "p3", valid_round: -1 } + val v1_proposal = { proposal: "v1", round: 0, src: "p3", valid_round: -1 } + + init + .then("p1".with_cue(listen_proposal_in_propose, v0_proposal).perform(broadcast_prevote_for_proposal)) + .then("p2".with_cue(listen_proposal_in_propose, v1_proposal).perform(broadcast_prevote_for_proposal)) + .then("p1".with_cue(listen_proposal_in_prevote_commit, v0_proposal).perform(lock_value_and_precommit)) + .then("p2".with_cue(listen_proposal_in_prevote_commit, v1_proposal).perform(lock_value_and_precommit)) + .then("p1".with_cue(listen_proposal_in_precommit_no_decision, v0_proposal).perform(decide_on_proposal)) + .then("p2".with_cue(listen_proposal_in_precommit_no_decision, v1_proposal).perform(decide_on_proposal)) + .expect(not(agreement)) + } +} diff --git a/.claude/skills/quint-modeling/guidelines/from-code.md b/.claude/skills/quint-modeling/guidelines/from-code.md new file mode 100644 index 000000000..5d5da0e43 --- /dev/null +++ b/.claude/skills/quint-modeling/guidelines/from-code.md @@ -0,0 +1,182 @@ +# From code — intake for generating a Quint spec from source + +This is the **code-intake flow**: extract a system's structure from source code (Rust, Go, +TypeScript, …). It carries only the code-specific intake; **after intake, follow the shared +spine (Steps 1–7) in `../SKILL.md`.** + +## Contents + +- **Why a spec from code** — the spec as a persistent grounding artifact +- **Phase 0: Research (compact)** — catalog the codebase before deep reading +- **Phase 1: Understand the code** — Steps 1.1–1.4 (domain, operations, state vars, system model) +- **The source-construct → Quint mapping** — the construct translation table +- **Set scope and abstraction level** — modules in/out, atomic granularity, details to hide (confirm with the user) +- **After intake** — hand off to the shared spine +- **Handoff** — spine Step 7 plus a source-file correspondence map + +## Why a spec from code + +**The spec is a persistent grounding artifact, not throwaway output** — the machine-checked source +of truth for what the system *is supposed to do*, used to verify every future change against. Code +stays primary: the spec *verifies* code, it does not generate it. A 50–200 line model captures what +1000 lines of code can't, and reviewing at the spec stage — then re-verifying it whenever the code +changes — is the highest-leverage check you get. + +## Phase 0: Research (compact) + +Before reading code in detail, catalog the codebase to keep the main context window lean +(target: under 400 lines of catalog). Skip this for simple single-file cases with a clear +entry point and no concurrency. + +> Explore `[path]`. Find and catalog: +> 1. The top-level entry points and their signatures +> 2. The state-carrying data structures (structs, maps, enums) +> 3. The concurrency primitives (mutexes, channels, goroutines, async tasks) +> 4. The message types and their payload shapes +> 5. Any existing tests that reveal expected behavior +> +> Output a compact summary — file paths, key types, key operations. Do not read every file. +> Prioritize what is most relevant to concurrent/distributed behavior. + +If the catalog missed something critical, do a targeted follow-up read — do not re-read the +whole codebase from scratch. + +## Phase 1: Understand the code + +Using the research output, answer in English. + +### Step 1.1 — Identify the problem domain + +1. **Overall purpose?** (e.g. "distributed leader election", "token transfer protocol") +2. **What entities exist?** (nodes, validators, clients, coordinators) +3. **What resources are shared or contested?** (leader slot, token balances, lock ownership) + +### Step 1.2 — Catalog operations and their purpose + +| Operation | Purpose | State it reads | State it writes | Concurrency notes | +|---|---|---|---|---| +| `functionName` | What it does | Which vars | Which vars | Atomic? Per-node? | + +**Focus on:** public API / entry points, state-modifying operations, message send/receive +points, timeout/timer triggers. + +**Skip:** side-effect-free getters, logging, metrics, serialization, retry plumbing (unless +retry is what you're verifying). + +### Step 1.3 — Identify state variables + +| Variable | Type | Purpose | Scope | +|---|---|---|---| +| `varName` | int / enum / record | What it tracks | Global / per-node | + +**Look for:** state-machine enums, per-node bookkeeping, shared global state, message buffers. + +### Step 1.4 — Extract system-model assumptions + +Read these off the code — concurrency primitives reveal the time model, error/recovery paths +reveal the failure model, transport reveals communication. **Fill in the spine's system-model +assumptions checklist (Step 1)** from what the code shows. + +## The source-construct → Quint mapping + +This is the heart of code intake: translate each language construct into its Quint counterpart. + +| Source | Quint | +|---|---| +| State enum | Sum type `\| State1 \| State2`, or `str` constant | +| Struct / record | `type T = { field1: Type1, field2: Type2 }` | +| `Vec` / array | `List[T]` | +| `HashSet` | `Set[T]` | +| `HashMap` | `K -> V` (map type) | +| Thread / process | Element of `NODES`; per-actor `NodeId -> LocalState` | +| Atomic CAS | Guarded action (atomicity is implicit) | +| Message queue | `Set[Message]` — message soup, no ordering unless ordering is what you verify | + +**Sum types use named constructors**, not inline tagged records: + +```quint +type Message = + | VoteRequest({ term: int, candidateId: int }) + | VoteResponse({ term: int, voterId: int, granted: bool }) +``` + +## Set scope and abstraction level — propose, then confirm + +You now understand what the code does. **Before** handing off to the spine, pin down three +decisions that the code itself cannot answer — they depend on *what you intend to verify*, and +getting them wrong is expensive to unwind once types and logic exist. Code is the flow where this +matters most: a codebase offers far more detail than a spec should reproduce. + +First, **infer** as much as you can from what the user already told you — the request usually +states (or strongly implies) the target property, which modules matter, and how faithful the +model must be. Don't re-ask what's already answered. Draft the three decisions from that, then +**present them as a proposal and ask the user to confirm the parts you inferred** — especially +anything you had to guess. This is the same propose-then-approve gate as the spine's type sketch, +just one step earlier. + +**1. Scope — which modules/components.** From the Phase 0 catalog, decide which modules/files are +*in* the spec and which are out, and what an out-of-scope component is replaced by (an abstract +map, an assumption). "Model the consensus core in `raft.rs`/`log.rs`; treat storage as an abstract +`Key -> Value` map; exclude the gRPC transport." Model what the target invariants depend on; leave +the rest out. **Only stop to confirm scope with the user when the boundary is genuinely +ambiguous** — if the request already makes it clear (names the component, the property, the entry +point), just state your inferred scope in one line and move on. Don't turn an obvious boundary into +a question. + +**2. Granularity — how many implementation steps become one atomic transition.** Real code does +one logical operation in many small steps (lock → read → check → mutate → unlock → ack). In the +model, decide the **atomic grain**: which sequences collapse into a single action. +- **Fuse into one atomic action** when the intermediate states are not observable to other actors, + or cannot interleave in a way that affects an invariant you care about. +- **Keep the steps separate** when the concurrent interleaving *between* sub-steps is exactly what + you are verifying — a check-then-act race (TOCTOU), a partial-write window, a torn read. + + This is the choice that most determines whether the spec can *find* a concurrency bug versus + silently *assume it away*, so make it deliberately and state it. (Atomicity is implicit in + Quint — an action either fires whole or not at all — so fusing is the default; splitting is the + decision that costs you nothing in syntax but buys interleaving coverage.) For **distributed + protocols specifically, lean toward splitting at message boundaries** — a process's local update + and another process observing its message are not simultaneous, so fusing them assumes away the + interleavings where most real bugs live. (This is also what Choreo structures for you.) + +**3. Implementation details — which mechanism to hide.** Source code is full of plumbing a spec +should *assume away*, not reproduce. For each concern the code surfaces, state model-it vs. +hide-it and why: + +| Detail in the code | Default in the spec | Model it only when… | +|---|---|---| +| Locks / mutexes / atomics | hide — steps are atomic (see decision 2) | lock-acquisition order is the property | +| Serialization / wire format | hide — pass structured values | a (de)serialization bug is the target | +| Retry / backoff / timeout plumbing | hide — model the outcome (success/failure) | retry semantics are the property | +| **Bounded channels / queues** | hide — unbounded `Set[Msg]` message soup, delivery is an action firing | back-pressure / blocking-on-full / capacity is the property | +| Network transport (sockets, framing) | hide — message soup; no delivery order | loss or ordering is what you verify | +| Error-propagation boilerplate | hide — a failed op is a guarded action that doesn't fire; *but if the error value itself is observable state you assert on (revert reason, error code), return it from a `pure def` as `{error, state}` instead* | error handling itself is the property | +| Concrete data structures (ring buffers, trees) | hide — `List` / `Set` / `Map` | the structure's own invariant is the target | +| Identifiers (node/request/txn IDs) | abstract — a small symbolic set (`NodeId = int`, opaque) | identity arithmetic/ordering is the property | +| Unbounded counters / sequence numbers | abstract — a small capped int or round counter | the bound itself is the property | + +The governing rule is the spine's "what, not how": if a detail doesn't affect an invariant you +care about, it doesn't belong in the spec. These choices become the `const` declarations and +system-model assumptions the spine's Step 1 will encode — you are deciding them here as one +coherent set, with the user's sign-off, rather than discovering them ad hoc while writing. + +## After intake + +With scope, granularity, and abstraction level agreed, hand the understanding (entities, the +operations table, the state variables, the filled-in assumptions checklist) to the **shared spine, +Steps 1–7** in `../SKILL.md`. The spine shapes the state, writes the pure functions, wires thin +actions, proposes witnesses-then-invariants, composes `step`, and simulates. Do not duplicate that +work here. + +## Handoff (spine Step 7, with a code-specific addition) + +Follow the spine's Step 7 handoff (covers / does NOT cover / when to update / ground truth), +and add a **source-file correspondence map** so each module is traceable back to the code it +grounds. When those files change, update the spec first and re-verify before touching the code. + +``` +Raft.qnt ↔ src/consensus/raft.rs, src/consensus/log.rs +Membership.qnt ↔ src/cluster/membership.go +``` + +To implement changes against this spec, use the `quint-execute-spec` skill. diff --git a/.claude/skills/quint-modeling/guidelines/from-nothing.md b/.claude/skills/quint-modeling/guidelines/from-nothing.md new file mode 100644 index 000000000..ce36b9bc3 --- /dev/null +++ b/.claude/skills/quint-modeling/guidelines/from-nothing.md @@ -0,0 +1,64 @@ +# From nothing — interactive build + +The user arrives with only an idea (or an informal proposal doc) and no written spec, code, or +TLA+ to translate. Intake here is a **guided interview**: you elicit the model one layer at a +time, and the user supplies the domain knowledge. After the interview, follow the shared spine +(Steps 1–7) in `../SKILL.md` to turn the elicited model into a verified spec. + +Unlike the other flows, there is no source artifact to read — so the risk is *modelling the +wrong thing*. The interview exists to surface the system's real shape before any code is +written, and to catch forks early. + +## The interview + +Walk these in order. Ask one focused question per layer; do not move on until the answer is +concrete. Each answer feeds a specific part of the spine. + +1. **Entities & types** — "What are the core entities, and what does each remember?" Get the + nouns (users, nodes, accounts, messages) and the data each carries. → feeds the spine's + Step 2 state record(s). + +2. **System model** — "How many participants? Can they fail? Is communication reliable/ordered? + Is time relevant?" Fill in the spine's **system-model assumptions checklist** (Step 1). Do + this early — it decides whether you need one actor or `NodeId -> LocalState`, a message soup, + a fault model. + +3. **Operations** — "What can happen? For each operation: who triggers it, what must be true + first (precondition), and what changes?" → feeds the spine's Step 3 pure functions. List them + in English first; no code yet. + +4. **Properties** — "What must *always* hold? (safety) What must be *reachable*? (liveness)" + Capture safety conditions (no negative balance, at most one leader, conservation laws) and the + key reachable states. → feeds the spine's Step 5 witnesses and invariants. + +5. **Initial state** — "How does the system start? What are the initial values?" → feeds `init` + in the spine's Step 4 (remember to pre-populate every map). + +6. **Exploration surface** — "Which operations should the simulator be free to fire, over what + parameter ranges?" → feeds the spine's Step 6 `step`. + +## Surface forks, don't bury them + +The interview's main value is catching ambiguity. **If two plausible readings of an answer imply +different state shapes or different action semantics, stop and ask** — describe the fork and its +consequence, and let the user choose. Never resolve a behavior-changing ambiguity by guessing a +default. Common forks: single actor vs. N actors; synchronous vs. asynchronous; whether a failed +operation is a no-op or an error state. + +## Pace and checkpoints + +- Build incrementally, exactly as the spine prescribes — one type, one pure function, one action + at a time, verifying each before the next. Do not dump a full spec from the interview. +- The type sketch (spine Step 2) is the **highest-leverage checkpoint**: present the types and + `var` declarations, typecheck them, and get explicit approval before writing any logic. +- **Stop before tests.** When the main spec is complete and simulates cleanly, say so and review + it with the user *before* writing any `*_test.qnt` file. Tests come after the main spec is + agreed, not alongside it. + +## Handoff + +Produce the spine's Step 7 handoff as a short comment block at the top of the spec (or a brief +note): what it models, what it deliberately leaves out, and which design forks were resolved and +how. For an interactive build there is no source artifact to map back to — the "what it does NOT +cover" note is the important part, since the scope was decided in conversation and is easy to +lose. diff --git a/.claude/skills/quint-modeling/guidelines/from-requirements.md b/.claude/skills/quint-modeling/guidelines/from-requirements.md new file mode 100644 index 000000000..fa07ca021 --- /dev/null +++ b/.claude/skills/quint-modeling/guidelines/from-requirements.md @@ -0,0 +1,85 @@ +# From requirements — written specification + +The user has a written requirements or functional-spec document (prose, user stories, a design +doc) and wants it modelled in Quint. Intake here is **reading and structuring**: you extract the +model from the document rather than interviewing for it. After intake, follow the shared spine +(Steps 1–7) in `../SKILL.md`. + +This is the non-interactive sibling of `from-nothing`: the same target understanding (entities, +operations, properties, system model), but sourced from a document instead of a conversation. +The interaction is *targeted* — you ask the user only where the document is silent or ambiguous +on something that changes the spec. + +## Extract from the document + +Read the document and produce, in English, the same understanding the spine builds on: + +1. **Entities & state** — what the system tracks and what each entity remembers. → spine Step 2. +2. **System model** — fill the spine's **assumptions checklist** (Step 1): participants, failure + model, communication, time. Requirements docs frequently leave these *implicit* — list what + the document states explicitly and flag what it omits (see below). +3. **Operations** — every operation the document describes, with its precondition and effect. + → spine Step 3 pure functions. +4. **Properties** — the document's stated guarantees become invariants; "the system can reach X" + statements become witnesses. → spine Step 5. When the document yields **many** candidate + properties, score each by how directly it validates what the user asked for, so verification + effort goes to what matters first: + - **High** — directly validates the requested change / the document's core guarantee. + - **Medium** — validates a supporting path or edge condition. + - **Low** — a broad safety check not specific to this request. + + Give each a one-line rationale citing the requirement it comes from. This is a triage aid for + ordering work and presenting results — not a Quint construct; skip it when there are only a + couple of obvious properties. + +A table is often the cleanest intake artifact: + +| Requirement (quote/§) | Entity / operation / property | Maps to | +|---|---|---| +| "a transfer must not overdraw" | invariant: no negative balance | spine Step 5 | +| "any node may propose" | operation `propose(node)` | spine Step 3 | + +Linking each modelling decision back to a line in the document keeps the spec traceable and makes +the handoff's "what it covers" trivial to write. + +## Resolve gaps before modelling, not by guessing + +Requirements docs are written for humans and routinely omit what a formal model must pin down — +exact failure semantics, ordering, what happens on a precondition violation, how many +participants. **Where the document is silent on something that changes state shape or action +semantics, ask one targeted question** rather than inventing a default. Record the answer (and +that it was a gap) so the handoff can note it. Where the document is silent on something +*immaterial* to any property you care about, omit it — that's the "what, not how" rule from the +spine. + +## Set scope and granularity (confirm before modelling) + +A requirements doc usually describes more than one spec should cover, and states *what* happens +without fixing the *grain* at which to model it. Before the spine, settle two choices — infer them +from the doc and the user's ask, then confirm the parts you inferred (same targeted-question +discipline as the gaps above): + +- **Scope — which requirements are in.** Docs carry future phases, explicitly out-of-scope + sections, and features irrelevant to the property you're after. State which requirements this + spec models and which it leaves out, tied to what's being verified. Decide this **now**, before + writing types — the spec you build should be shaped by the scope, not have a scope justified + after the fact. (The handoff later just records what you agreed here.) +- **Granularity — the atomic grain of each operation.** A requirement like "a customer confirms a + booking" may be one atomic action, or may decompose into steps (reserve → pay → confirm) whose + *interleaving* matters. Model an operation as a single action when its intermediate states can't + be observed or interleaved in a way that affects an invariant; split it into separate actions + when concurrent interleaving between the steps is part of what you're checking. The doc rarely + states this — it is a modelling decision, so make it deliberately. + +## Then follow the spine + +With the understanding extracted, proceed through the spine: separate concerns, shape the state, +write pure functions, wire thin actions, add witnesses then invariants, compose `step`, simulate. +Build incrementally and get approval on the type sketch (spine Step 2) before writing logic. + +## Handoff + +The spine's Step 7 handoff, with a requirements-specific addition: a **coverage map** linking each +modelled operation/property back to the requirement it came from, and the **scope you agreed +up front** — the requirements left out (and why) — recorded as the "what it does NOT cover" list. +The gaps you had to ask about belong in that same assumptions note. diff --git a/.claude/skills/quint-modeling/guidelines/from-tlaplus.md b/.claude/skills/quint-modeling/guidelines/from-tlaplus.md new file mode 100644 index 000000000..6a6b6fba2 --- /dev/null +++ b/.claude/skills/quint-modeling/guidelines/from-tlaplus.md @@ -0,0 +1,295 @@ +# From TLA+: translation intake + +This is the intake flow for translating an existing TLA+ specification into Quint. Do the TLA+-specific intake and design decisions below, then follow the shared modelling spine (Steps 1–7) in `quint-modeling/SKILL.md`. + +## Contents + +- **Philosophy: fidelity** — what the translation must preserve +- **The "Maintain" rules** — CONSTANT/ASSUME, abstract sets, sentinel constants, EXTENDS +- **The "Change" rules** — where idiomatic Quint diverges (local state, thin actions, message soup → Choreo, listen/send naming) +- **Phase 1: TLA+ intake** — Steps 1.1–1.4 (domain, EXTENDS, CHOOSE, variables, actions, system model) +- **TLA+-specific output format** — editor mode line, `NameAnalysis` module, `README.md` +- **TLA+-specific pitfalls** — the gotcha table + +## Philosophy: fidelity + +TLA+ specs have precise semantics that must be maintained. Most TLA+ specs translate close to one-to-one, but Quint offers modern syntax that reads better. The goal is a readable Quint spec **where the TLA+↔Quint mapping is obvious**. + +Concretely: + +- **Maintain names** — of variables, functions, and operators. +- **Infer TLA+ types.** If a type is genuinely in doubt, ask the user rather than guessing. +- **Translate every TLA+ invariant faithfully.** Each TLA+ invariant operator (`Inv`, `TypeOK`, `VotesSafe`, etc.) becomes a `val` in Quint with the **same name**, the **same conjunct order**, and inline comments that cite the TLA+ formula. Do **not** add invariants that have no TLA+ counterpart, do not split a TLA+ invariant into helper `val`s, and do not introduce safety properties beyond what the TLA+ spec defines. + +## The "Maintain" rules + +These preserve the TLA+ structure. Keep the concrete forms below — they are the value of this flow. + +### Modularity: CONSTANT and ASSUME + +- **CONSTANT → separate parametric modules.** If a TLA+ spec uses `CONSTANT` and separate TLA+ files instantiate those constants, do the same in Quint: a parametric module with `const` declarations, plus an instantiation module. +- **ASSUME → a `run` test in the same parametric module as the `const`** — *not* in the instantiation module, and *not* via Quint's `assume` keyword (do not use `assume`). + +```quint +run quorumAssumptionTest = { + all { + Quorum.forall(Q => Q.subseteq(Acceptor)), + Quorum.forall(Q1 => Quorum.forall(Q2 => Q1.intersect(Q2) != Set())), + } +} +``` + +Run it via `quint test --main `. The test passes when all conditions hold; it fails (reporting which step failed) otherwise. + +### Abstract TLA+ sets → const + parametric types + +`CONSTANT Value, Acceptor` become `const`s with **descriptive lowercase type variables** (e.g. `acceptorType`, `valueType`). Use distinct variables when the sets have independent element types. Any type that mentions them must be made **parametric**. The `var` and function signatures use the module-level type variables directly; the instantiation module infers concrete types from the const values, so no explicit type arguments are needed: + +```quint +const Acceptor : Set[acceptorType] +const Value : Set[valueType] +const Quorum : Set[Set[acceptorType]] +type Vote[v] = { bal : int, value : v } +type AcceptorState[v] = { votes : Set[Vote[v]], maxBal : int } +var acceptors : acceptorType -> AcceptorState[valueType] +// function sigs can omit the type param when Quint can infer it: +// (state : AcceptorState, acc : acceptorType, v : valueType, ...) + +// Instance: types inferred as acceptorType=int, valueType=int +import Voting(Acceptor = Set(1,2,3), Value = Set(0,1), Quorum = ...).* +``` + +### TLA+ sentinel constants → variants of a shared sum type + +TLA+ sentinel constants (`CONSTANT any, none` with `any \notin Values \union {none}`) should be translated as explicit variants of a **shared sum type** defined in a **separate module** — not as an abstract `const`. Define the type in its own file (e.g. `PaxosValues.qnt`) imported by all modules that need it: + +```quint +// PaxosValues.qnt +module PaxosValues { + type AllValues[v] = Any | NoVal | Val(v) + // Val(v) — a real protocol value + // Any — TLA+ `any` sentinel + // NoVal — TLA+ `none` sentinel +} +``` + +The assume test can then faithfully check both exclusions: + +```quint +not(Values.contains(Any)), // any \notin Values \union {none} +not(Values.contains(NoVal)), // none \notin Values \union {any} +``` + +The type **must** live in a separate module (see the parametric-type cycle in Pitfalls). + +## The "Change" rules + +These are the places where idiomatic Quint diverges from the TLA+ structure. + +- **Distributed local state.** In TLA+ local variables are often multiple flat maps from process IDs to values. In Quint, encode a `LocalState` record capturing one process's local variables, and store the system state as a map from process ID to `LocalState`. (The spine's Step 2 covers the general mechanics of this map-of-records shape.) + +- **Truly thin action layer.** All guards and state computation belong in `pure def`s; actions are single assignments that call the pure def and set the next state. When a TLA+ guard that would *disable* an action is instead absorbed into a pure def's `if-else` (returning the old state on failure), this introduces stuttering — document it on the action with a note and a hint for how to remove it: + + ```quint + // Note: applyFoo returns st unchanged when fails — stuttering vs TLA+. + // To remove stuttering add: , + action foo(acc : acceptorID, bal : int) : bool = all { + acceptors' = acceptors.set(acc, applyFoo(acceptors, acc, bal)), + } + ``` + + Returning-old-state-on-failure is acceptable as a **transient step** during translation (it lets + you get the spec running before every guard is lifted out), but it is not the end state: a + blanket no-op fabricates a transition the protocol doesn't have. Before handoff, lift the guards + out so the action is properly disabled when its precondition fails — see the spine's Step 6 + ("Model transitions faithfully: guard actions, don't fake no-ops") for the reasoning. + +- **Message soup → consider Choreo.** A TLA+ message soup (a `msgs` variable, a `Send(m)` helper, or any `\cup {m}` pattern on a message set) is a strong signal the protocol is genuinely message-passing — **raise Choreo in design before writing any code, unless the protocol is single-actor or simple enough that plain Quint is clearer** (see the spine's "When to use Choreo"). When it fits, use Choreo (`../quint-lang/guidelines/choreo.md`) and ask the user to confirm the node/role decomposition (which processes send/receive which message types, whether to introduce an explicit leader). The TLA+ soup is monotone (messages are never deleted) — decide whether Choreo inboxes should consume messages or leave them in place. + +- **Choreo `listen_*` / `send_*` naming.** `listen_X` is named after what it watches for (the triggering condition or incoming message type); `send_X` is named after the message type it produces (= the TLA+ operator name). E.g., TLA+ `Phase2b(a,b,v)` is triggered by a Phase2a message → `listen_phase2a` / `send_phase2b`. For an initial step with no incoming message, use a descriptive name like `listen_start` or `listen_phase1b_quorum`. The `main_listener` then reads as a direct transliteration of the TLA+ `Next` definition. + +### TLA+ `EXTENDS` → `import M(...) as m` + `export m` + +Quint has no `EXTENDS` keyword. The closest equivalent is a namespaced import where the extending module re-declares the shared `const`s, passes them through, and re-exports the namespace: + +```quint +// FastPaxos.qnt — mirrors TLA+ EXTENDS Paxos +const Replicas : Set[acceptorType] // re-declare shared consts +const Ballots : Set[int] +// ... + +import Paxos( + Replicas = Replicas, // pass through to base module + Ballots = Ballots, + // ... +) as paxos from "Paxos" +export paxos // re-export so analysis modules can call paxos::f +``` + +The analysis module then calls `paxos::listen_p2a_value`, `paxos::upon_classic_decide`, etc. without duplication. + +**Constraint — higher-order const bindings (verify locally).** In some cross-module setups (observed +passing `paxos::f` to `choreo::cue`), a function whose body references module-level `const`s loses +the const binding when used as a higher-order argument across the boundary, failing at runtime with +"Uninitialized const". This is **not** a reliable general rule — a plain higher-order const closure +across a normal `import` runs fine on current Quint — so treat it as a setup-specific gotcha to check +against your own version, not a law. If you do hit it, the fix is to rewrite the body to use only the +type structure: `Values.contains(r.value)` → `r.value != Any and r.value != NoVal` (equivalent when +`Values` only contains `Val(v)` elements, which the assume test guarantees). + +**Constraint — cross-module `val` invariants.** The governing insight: a `pure def`'s arguments are +evaluated at the **call site**, so consts passed in refer to the *caller's* (bound) consts; a `val` +is evaluated in **its own defining module's** const environment, which is not propagated across an +import boundary. So referencing `paxos::TypeOKInvariant` (a `val`) from the extending module fails at +runtime with "Uninitialized const". Fix: extract the invariant body into a `pure def` that takes the +consts as explicit parameters, then call it from both the base `val` and the extending module's +invariant. + +```quint +// Paxos.qnt — base module +pure def checkPaxosTypeOK( + values: Set[AllValues], + ballots: Set[int], + decision: AllValues, + replicaStates: Set[StateFields] // pass s.system.get(a).state for each replica +): bool = + (values.contains(decision) or decision == NoVal) + and replicaStates.forall(sf => + match sf { + | AcceptorState(acc) => + ballots.contains(acc.maxBallot) + and ballots.contains(acc.maxVBallot) + and (values.contains(acc.maxValue) or acc.maxValue == NoVal) + | CoordState(_) => false + } + ) + +val PaxosTypeOK: bool = + checkPaxosTypeOK(Values, Ballots, coordState.decision, + Replicas.map(a => s.system.get(a).state)) + +// FastPaxos.qnt — extending module +// paxos::checkPaxosTypeOK works because it takes consts as explicit parameters. +// paxos::PaxosTypeOK would fail — val references do not propagate const bindings. +val FastTypeOK: bool = + paxos::checkPaxosTypeOK(Values, Ballots, coordState.decision, + Replicas.map(a => s.system.get(a).state)) + and (Values.contains(coordState.cValue) or coordState.cValue == NoVal) +``` + +(In the example above, `checkPaxosTypeOK` works from FastPaxos because `Values`/`Ballots` are +evaluated at the call site against FastPaxos's bound consts.) + +When the operator genuinely differs between base and extending module (e.g. `ClassicDecide` iterates `ClassicBallots` in FastPaxos but `Ballots` in Paxos), define the function locally in the extending module. This is semantically correct, not a workaround. + +**File length check — ask before combining `EXTENDS` modules.** When the TLA+ source uses `EXTENDS AnotherFile`, check the total line count of both files. If keeping them combined would make the Quint file noticeably longer than its TLA+ counterpart, present the user with a choice: + +- **One file** — simpler imports for the analysis module, but potentially long. +- **Two files mirroring TLA+** — each Quint file stays close in length to its TLA+ source; base module content is duplicated (~15–20 lines) since Quint parametric modules cannot be cross-imported cleanly. + +Ask the user which they prefer before writing any code. A Quint file should not be substantially longer than the TLA+ spec it translates. + +## Phase 1: TLA+ intake + +### Step 1.1: Identify the problem domain + +Read the spec and answer in English: + +1. **What is the overall purpose?** (e.g. "distributed leader election", "two-phase commit") +2. **What entities exist?** (e.g. nodes, validators, clients, coordinators) +3. **What resources are shared or contested?** (e.g. leader slot, token balances, lock ownership) + +### Step 1.1b: Analyze TLA+ `EXTENDS` imports + +Before translating any spec that uses `EXTENDS AnotherFile`, read `AnotherFile` and list **precisely** which operators/definitions the extending spec actually uses. This determines the Quint module structure. Example: + +| Used from Paxos | How used in FastPaxos | +|---|---| +| `PaxosAccepted` | `ClassicAccepted == UNCHANGED<> /\ PaxosAccepted` | +| `PaxosInit` | `FastInit == PaxosInit /\ cValue = none` | +| `PaxosTypeOK` | `FastTypeOK == PaxosTypeOK /\ cValue \in Values \union {none}` | +| `Ballots`, `Quorums`, `Replicas`, `Values` | shared constants, inherited | + +Operators **not** used (e.g. Phase1a/1b, Phase2a, PaxosNext) can be dropped from scope. This analysis drives the module-structure decision before any code is written. + +### Step 1.1c: Flag TLA+ `CHOOSE` operators + +Scan the TLA+ spec for any use of `CHOOSE` (e.g. `CHOOSE x \in S : P(x)`). Quint has no direct `CHOOSE` equivalent. For **each** occurrence: + +1. Quote the TLA+ expression to the user. +2. Explain what it does in context (picks an arbitrary element satisfying a predicate, defines a canonical representative, etc.). +3. Ask the user how to handle it. Common options: + - **Nondeterministic choice** — replace with `nondet x = S.filter(e => P(e)).oneOf()` in an action (only valid in an action context). + - **Deterministic selection** — replace with a deterministic helper (e.g. `S.filter(P).fold(...)`) if the choice is semantically irrelevant. + - **Constant / abstract value** — introduce a `const` or `pure val` if the chosen value is fixed for a run. +4. **Do not translate any `CHOOSE` occurrence until the user has approved an approach for it.** + +### Step 1.2: Analyze the variables + +1. **What is local state?** Read and written only by one entity (e.g. round number, decision value). Often a map from entity to variable. +2. **What is global state?** Read and written by more entities (shared variables, message soup). +3. **What is the type of each variable?** +4. **Is there state that fits neither?** Ask the user for advice. + +### Step 1.3: Analyze the actions in `Next` + +1. **Init.** +2. **What are the actions that constitute `Next`?** Separate entity actions from environment actions. What are their effects on local and global state? + +### Step 1.4: System-model assumptions + +Fill in the spine's system-model assumptions checklist (Step 1 of `quint-modeling/SKILL.md`) from the TLA+ spec — communication, failures, time, participants. These become the `const` declarations and the `run` test that checks the translated `ASSUME` (Maintain rules above). + +--- + +After this intake and the TLA+-specific design decisions above, follow the shared spine (Steps 1–7) in `quint-modeling/SKILL.md`. For Quint syntax, operators, and the CLI, defer to **quint-lang**. + +## TLA+-specific output format + +This flow's deliverables differ from the other flows in three ways: + +### 1. Spec module — editor mode line + +The spec module's **first line must be `// -*- mode: Bluespec; -*-`** — before any other content, including the module header comment. The spec module is the faithful TLA+ translation: same names, same structure, same properties, same conjunct order, a pure functional layer for all guards and state computation, and Choreo for any message soup. No witnesses, runs, or concrete instances live here — those go in the analysis module. + +### 2. `NameAnalysis` module — appended to the same `.qnt` file + +A second module written at the bottom of the same `.qnt` file (no separate file). It holds the concrete instantiation of the spec module (e.g. 3 nodes, specific constant values), happy-path runs showing how the protocol works, and the witnesses. The module name follows the pattern `Analysis`, e.g. `PaxosAnalysis`. Run with `--main NameAnalysis` (not the spec module name), because the analysis module holds the concrete `init` and `step`. + +```quint +module PaxosAnalysis { + import Paxos( + Acceptor = Set(1, 2, 3), + // ... other constants + ).* + + // happy-path run + run happyPathTest = { ... } + + // Witness: not in TLA+, inferred for reachability checking + val canPhase1aSent: bool = ... +} +``` + +### 3. `README.md` next to the `.qnt` file + +This is the spine's Step 7 handoff, in TLA+-translation form. It documents the translation and records simulation results: + +- **Purpose** — one paragraph: Quint translation of which TLA+ spec, link to the TLA+ source, brief description of what the protocol does. +- **Invariants** — for each `val` invariant: its name, the TLA+ operator it translates, a one-line description. Note that invariants are taken directly from the TLA+ spec, not invented. +- **Witnesses** — table: name, what it confirms is reachable. State explicitly that witnesses are not in the TLA+ spec and were added for simulation coverage. +- **Experiments** — the executed `quint run` arguments and an output summary (the `[ok]` line, trace-length statistics, witness counts), plus a one-sentence interpretation. Record the **date** of each run. When parameters change (e.g. higher `--max-steps`), add a new dated run block rather than overwriting the old one. + +## TLA+-specific pitfalls + +| Pitfall | Solution | +|---|---| +| `val` is a keyword | TLA+ specs often have a `val` field; it cannot be a record field name in Quint. Use `value` instead | +| `ASSUME` → `assume` | Do not use Quint's `assume` keyword. Translate TLA+ `ASSUME` as a `run` test in the same parametric module as the `const` (see Maintain rules) | +| `msgs` / message soup → plain `Set[Message]` | Consider Choreo instead — a soup is a strong Choreo signal; raise it in design unless the protocol is single-actor/simple (see the spine) | +| TLA+ `EXTENDS` → duplicating all functions | Use `import M(...) as m` + `export m`. The extending module re-declares shared `const`s and passes them through. Functions with no `const` refs in their body are safely reusable as `m::f` | +| `type T[v] = ...` in same module as `const X: Set[T]`, instantiated with `X = Set(Constructor(v))` | Quint detects a self-referential cycle: `Constructor` is defined by `T`, defined in the module being instantiated. Fix: extract `type T[v]` to a separate shared module imported by both base and extending modules | +| `m::f` fails at runtime with "Uninitialized const" when passed as a higher-order argument *(setup-specific — verify; a plain cross-module higher-order const closure runs fine on current Quint)* | If you hit it: rewrite `f` to avoid const references — use the type structure (e.g. `x != SentinelA and x != SentinelB` rather than `Values.contains(x)`) | +| `paxos::TypeOKInvariant` (a `val`) fails at runtime with "Uninitialized const" | Quint does not propagate `const` bindings when a `val` is accessed across module boundaries, even without higher-order calls. Fix: extract the invariant body into a `pure def` taking the consts as explicit parameters, then call it from both the base `val` and the extending module (see EXTENDS section) | +| TLA+ `CHOOSE` | No direct Quint equivalent. Flag each occurrence to the user (Step 1.1c) and get an approved approach — nondet, deterministic helper, or const — before translating | +| Parenthetical insertions with em-dashes in README or Quint comments | In *generated output* (the spec, its comments, the README) — not this guideline's own prose — do not write sentences that insert a clause between em-dashes ("X — which does Y — Z"). Use separate sentences or plain parentheses instead | diff --git a/.claude/skills/quint-modeling/guidelines/review.md b/.claude/skills/quint-modeling/guidelines/review.md new file mode 100644 index 000000000..e6634b64f --- /dev/null +++ b/.claude/skills/quint-modeling/guidelines/review.md @@ -0,0 +1,102 @@ +# Review — auditing an existing Quint spec + +This is the **review flow**: the input is a *finished* `.qnt` spec and the job is to audit it, not +build it. There is no new model to produce — the deliverable is a **report** of pass / warn / fail +findings plus fixes. You reach it two ways: directly ("review/audit this spec", a collaborator's or +your own), or as the deeper pass Step 7 escalates to when a quick self-review isn't enough. Either +way the procedure below is the same. + +Review does not introduce a new rulebook. **It checks a finished spec against the same discipline +this skill teaches for building one** (the spine, Steps 1–7, and the Conventions). So the +structural pass below is mostly "did the spec follow the rules already stated above?" — this file +points back to them rather than restating them. The genuinely review-only part is the **runtime +checks** (you have to *run* the spec) and the **report format**. + +For language/operator questions that come up while reviewing, defer to **quint-lang** as usual. + +## Preparation + +1. Read the spec. Catalogue: `var` declarations, `pure def`s, `action`s, `val` invariants and + witnesses, `temporal` properties, `assume` axioms. +2. For the runtime checks, drive the spec: `quint -r ::` then run `init`, + or use `quint run`. +3. Run **all** checks, record **pass / warn / fail** for each, print the report only at the end. + +## Structural checks — does the spec follow the build discipline? + +Each row is a rule from the spine; the spec passes if it followed it, warns/fails if not. Re-read +the referenced step if you need the rationale — don't reinvent it here. + +| Check | Rule (where it's taught) | Fail / warn when | +|---|---|---| +| **Guarded actions** | Step 4 — logic in `pure def`s, guard lifted into the action | an action carries business logic beyond the guard + assignments, or uses a no-op fallback instead of being disabled | +| **Enums over strings** | Conventions — sum types / typed constants for roles & phases | raw string literals like `"leader"`, `"propose"` in state or guards | +| **Record grouping** | Step 2 — group cohesive state into a record | several `var`s describe one entity but aren't grouped | +| **Witnesses present & per-action** | Step 5 — one witness per major action, checked with `--witnesses` (reached in > 0 traces) | no witnesses, or a major `step` action has none, or a witness reaches 0 traces (dead) | +| **Right abstraction** | "What, not how" + Conventions — opaque IDs, message soup | string manipulation, messages in an ordered `List` (when order isn't the property), serialization/retry/memory detail | +| **Non-trivial invariants** | Step 5 — at least one real protocol property | every invariant is a type/bounds check, or an invariant references no `var` (a tautology) | + +Anything that **fails** here is a correctness or value problem; a **warn** is a judgement call to +raise with the user. + +## Runtime checks — these need you to *run* the spec (review-only) + +- **C-init — `init` assigns every `var`.** Run `init`; every declared `var` must be assigned. + - Fail: `init` returns `false` / errors (quote it), or a `var` is unassigned. +- **C-step — every `var` updated in every action.** A missing `var' = ...` is a silent stutter + bug. Warn per gap: "Did you mean `' = `?" +- **C-step-complete — a `step` using `any { ... }` exists and includes all major actions.** + Warn if missing, or if an action exists but isn't in `step`. +- **R1 — invariants hold at `init`.** Evaluate each invariant after `init`. + - Fail: invariant `` is `false` at init — either `init` is wrong or the invariant is too + strong. +- **R2 — no counterexample after each action.** Fire each action reachable from init, re-check all + invariants. + - Fail: invariant `` violated after `` — show the state at violation. + +> R1/R2 are bounded checks driven from `init`, not a proof. A *violation* is conclusive (the spec +> does break the property); the *absence* of one across what you ran is **not** — report it as "no +> counterexample observed in the runs executed," never "the invariant holds." Stay with `quint +> run` for the review — do **not** reach for `quint verify`; exhaustive model checking is a separate +> activity, only when the user explicitly asks for it (see quint-lang's `guidelines/simulations.md` +> and `guidelines/cli.md`). See `guidelines/simulations.md` for the full result-language discipline. + +## Report format + +Print after all checks complete: + +``` +── Spec review: ────────────────────────────────── + +Structural (vs the build discipline) + thin actions [✓ / ⚠ list actions with logic] + enums over strings [✓ / ⚠ list raw string literals] + record grouping [✓ / ⚠ list ungrouped vars] + witnesses present & per-action[✓ / ✗ none / ⚠ uncovered or dead] + right abstraction [✓ / ⚠ describe what leaked] + non-trivial invariants [✓ / ✗ all structural / ⚠ tautologies] + +Runtime + init assigns all vars [✓ / ✗ error] + var assignment per action [✓ / ⚠ list gaps] + step exists & complete [✓ / ⚠ missing or incomplete] + invariants hold at init [✓ / ✗ list violations] + no counterexample after acts [✓ / ✗ broke ] + +── Top issues ───────────────────────────────────────────── + 1. + 2. + 3. + +── Suggested next steps ─────────────────────────────────── + 1. Fix the fails above + 2. Stress-test flagged scenarios with `quint run` / the REPL + 3. `quint run --invariant ` to sample (offer `quint verify` only if the user wants + exhaustive model checking — it is not part of the review itself) +``` + +## After the report + +Fix any **fail** immediately without asking — those are correctness problems. For **warn** +items, present the list and ask which to address (offer "All" and "None — leave as-is"); address +only what the user selects. diff --git a/AGENTS.md b/AGENTS.md index f1d7fc622..f617f34ce 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -9,6 +9,14 @@ Before exploring or changing package code, read `CONTEXT-MAP.md` and the applicable package `CONTEXT.md`. Treat those files as the source of truth for architecture, domain boundaries, request flow, and vocabulary. +## Formal models + +Before changing `specs/quint/`, or Proxy's statement routing, Parse/Bind +lifecycle, settings protocol or schema reload (`frontend.rs`, +`context/{lifecycle,mod,settings_protocol}.rs` and +`schema/{middleware,manager}.rs` in `packages/cipherstash-proxy/src/`, and +`packages/eql-mapper/src/eql_mapper.rs`), use the `proxy-quint` skill. + ## Development workflow Before setting up a local environment; starting or stopping Proxy or diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index ad644368b..3fb4cf545 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -479,6 +479,25 @@ To run language-specific integration tests, call: - `mise run test:integration:lang:golang` - `mise run test:integration:lang:python` +#### Quint specifications + +`specs/quint/` holds design-level Quint models of Proxy behaviour; see `specs/quint/README.md` for what each check shows. +They need Node 22 and Java 21. + +```shell +# install the pinned Quint CLI +mise run quint:install + +# typecheck, scenario tests and simulation (about 20 s) +mise run quint:check + +# everything, including exhaustive TLC checks (about 10 min) +mise run quint:check all +``` + +mise puts `specs/quint/node_modules/.bin` on `PATH`, so tools that call `quint` directly, such as Quint Connect model-based tests, use the pinned version. +Quint's default Rust simulator backend downloads a binary through the GitHub API on first use; where that API is blocked, as in Claude Code cloud sessions, pass `--backend typescript`. + ### Working with Encrypt Query Language (EQL) diff --git a/mise.toml b/mise.toml index f1cdb3146..8dcbf6c4c 100644 --- a/mise.toml +++ b/mise.toml @@ -36,6 +36,10 @@ DOCKER_CLI_HINTS = "false" # Please don't show us What's Next. CS_EQL_VERSION = "eql-3.0.4" +# The Quint CLI pinned in specs/quint/package-lock.json, for tools that call +# `quint` from PATH, such as Quint Connect model-based tests. +_.path = ["{{config_root}}/specs/quint/node_modules/.bin"] + [tools] "cargo:cargo-binstall" = "1.17.3" @@ -151,6 +155,17 @@ mise run test:format mise run test:clippy """ +[tasks."quint:install"] +description = "Install the pinned Quint CLI into specs/quint" +dir = "{{config_root}}/specs/quint" +run = "npm ci --ignore-scripts" + +[tasks."quint:check"] +description = "Run the Quint model checks (stage: basic, tlc, mutations or all)" +dir = "{{config_root}}/specs/quint" +usage = 'arg "[stage]" default="basic" { choices "basic" "tlc" "mutations" "all" }' +run = './check.sh "${usage_stage}"' + [tasks."reset"] alias = 'r' description = "Reset database"