quint-lang

Quint 语言参考

Quint 是一种用于复杂系统的可执行规约语言，由 Informal Systems 开发。它可编译为 TLA+，并支持模拟和模型检查。

模块结构

module MyProtocol {
  // type aliases, constants, state, actions, properties
}

模块可以导入其他模块：

import Voting.*              // all definitions
import Voting(quorum)        // specific definition
import Voting as V           // namespace alias

---

类型

类型	描述	示例
int	整数	-1, 0, 42
bool	布尔值	true, false
str	字符串	"hello"
Set[T]	有限集合	Set(1, 2, 3)
List[T]	有序序列	List(1, 2, 3)
K -> V	键值映射（类型为 K -> V，不是 Map[K, V]）	值：Map("a" -> 1)
(T1, T2)	元组	(1, "x")
{ f: T, g: U }	记录	{ x: 1, ok: true }
T | U	和类型（变体）	（使用类型别名）

类型别名：

type NodeId = int
type Phase = Idle | Propose | Vote | Commit   // enum — prefer over string literals

---

定义

// 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 与 pure val：const 是在实例化时绑定的模块参数（import A(N = 3)）；pure val 是仅计算一次的固定表达式。def 与 val：def 接收参数；val 不接收参数。

---

状态变量

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)

状态变量只能在 val 定义和动作中读取；不能在 pure def 中读取。

---

动作

动作描述状态转换。它们返回 bool——如果动作触发，则返回 true。

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,
}

主要规则：

• 每个 var 都必须在每个动作中赋值（使用 x' = x 可保持不变）。
• all { ... }——所有子表达式都必须成立（合取）。守卫是在 all { } 中的普通布尔表达式。
• any { ... }——至少一个子表达式必须成立（析取）；REPL 会以非确定方式选择。

---

非确定性

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(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(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("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

---

记录

记录将相关字段组合成一个命名类型。它们是 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,
}

创建和访问

val n: NodeState = { phase: Idle, voted: false, log: List() }
n.phase                          // Idle
n.voted                          // false

更新（不可变——返回一条新记录）

{ ...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

将记录用作状态——何时对变量进行分组

TLA+ 规约通常会将所有状态展平为相互独立的顶层变量。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

避免用于内聚的局部状态：

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]

对于 N 个参与者，使用由分组记录构成的映射：

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}),
  }
}

嵌套记录

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)}

集合中的记录（消息、事件）

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")

---

和类型

和类型（变体）表示一个值可以是若干不同情况之一。

type Action =
  | Propose({ value: int, proposer: int })
  | Vote({ value: int, voter: int })
  | Decide({ value: int })

每个变体都有一个命名构造器，并携带一个负载。构造器恰好接收一个参数——多个字段应封装在记录（如上所示）或元组中。

通过调用构造器来构造一个值：

val a: Action = Propose({ value: 1, proposer: 2 })

使用 match 进行模式匹配，并绑定负载：

pure def describeAction(a: Action): str =
  match a {
    | Propose(p) => "proposal"
    | Vote(v)    => "vote"
    | Decide(d)  => "decision"
  }

如果只关心值属于哪个变体，可使用 _ 忽略负载：

match a {
  | Propose(_) => "proposal"
  | _          => "other"
}

当消息、事件或状态可以采用结构不同的形式，而不只是同一类型的不同值时，应使用和类型。

---

枚举类型

枚举类型是和类型的一种特殊情况，其中每个情况都不包含额外数据。

type Phase = Idle | Propose | Vote | Commit
var phase: Phase

if (phase == Propose) { ... }

---

变量分组——决策指南

在编写 var 声明前，请针对每个候选分组回答以下问题：

问题	分组 → 满足以下条件时记录	保持扁平 → 满足以下条件时
这些变量是否总是一起变化？	是，在大多数操作中	否，它们彼此独立
它们是否描述同一个实体？	同一个节点／同一条消息／同一轮	不同的关注点
是一个实例还是 N 个实例？	一个或 N 个（如果内聚则分组；对于 N 个，使用 Id -> RecordType）	只有在关注点确实彼此独立时才保持扁平
不变量是否关联它们？	不变量跨越同一实体的多个字段	不变量分别使用各个变量

---

布尔运算符

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 { } 和 or { } 与操作中的 all { } 和 any { } 是相同的运算符——根据上下文选择读起来更自然的写法。

---

不变量和时序属性

// 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 nodeCountPositive = N > 0
assume quorumMajority = 2 * quorum > N

assume 用于声明有关常量的前提，但它不会强制执行——被违反的 assume 会被 quint typecheck、quint run 和 quint verify 静默忽略（它们都不会对此发出提示）。它只是文档说明，而不是经过检查的约束。若要实际检查常量条件，请编写一个断言该条件的 run 测试（条件为假时，测试会执行并失败）：

run quorumAssumptionTest = all {
  2 * quorum > N,
  N > 0,
}

使用 quint test 运行；如果常量赋值违反该条件，测试就会失败（并报告哪个合取项不成立）。

---

条件语句和 let

if (x > 0) "positive" else "non-positive"

val result = {
  val doubled = x * 2
  doubled + 1
}

---

REPL 用法

所有验证和执行任务都优先使用 CLI 命令（quint typecheck、quint run、quint test、quint verify）。只有在需要 CLI 不支持的表达式级交互时，才打开 REPL（quint 或 quint -r spec.qnt::ModuleName）。

类型检查：

>>> :type myExpression

---

文件布局

将规范拆分到两个文件中：

<protocol-name>.qnt        # main module — step, init, vars, invariants
<protocol-name>_test.qnt   # test module — run tests and scenario witnesses (imports main)

模块职责

主模块（<protocol-name>.qnt）：

• 声明所有状态变量、init、操作和安全不变量
• step 必须位于主模块中——它是 quint run 模拟的入口点
• 模块名称与文件主干名一致：在 myProtocol.qnt 中使用 module myProtocol

测试模块（<protocol-name>_test.qnt）：

• 导入主模块（import myProtocol.*）
• 包含通过 quint test 或 quint run 调用的 run 测试和场景见证
• 通过导入从主模块继承 step

quint run 应传入哪个 --main

quint run 必须接收拥有待检查属性的模块：

属性位置	正确的 --main
在主模块中定义的不变量	主模块名称
在测试模块中定义的见证／run 测试	测试模块名称（它从主模块导入 step）

基元的 module_name 字段（在索引时设置）始终包含正确的值。直接使用它，不要根据文件名推导。

---

---

基础咒语

许多实用运算符并未内置于 Quint，但可在 basicSpells.qnt 中找到。它是大多数 Quint 项目随附的标准库。使用以下方式导入：

import basicSpells.* from "./basicSpells"

它提供的关键定义：

定义	功能
type Option[a] = Some(a) | None	选项类型——Quint 没有内置的 Option。任何类型为 Option[T] 的规范字段都依赖此导入。
unwrap(o)	Some 中的值；对 None 未定义
require(cond)	如果 cond 为 false，则阻止该操作（比直接使用 all { cond, ... } 更简洁）
values(m)	映射 m 中所有值组成的集合
transformValues(m, f)	对每个值应用 f 后生成的新映射
has(m, key)	如果 key 在 m 中有绑定，则为 true
getOrElse(m, key, default)	如果存在，则返回 m.get(key)；否则返回 default
mapRemove(m, key) / mapRemoveAll(m, ks)	删除 key 后的 m 副本（或删除键集合 ks 后的副本）
setRemove(s, e) / setAdd(s, e)	删除元素 e 后的集合 s 副本／添加元素 e 后的集合 s 副本
find(s, f) / findFirst(l, f)	返回集合／列表中第一个满足 f 的元素，类型为 Option
max(i, j) / min(i, j) / abs(i)	两个整数的最大值／最小值；绝对值

如果你看到某个规范使用了 Option、require、values 或 transformValues，却没有导入相关内容，那么它依赖于 basicSpells——请检查项目是否包含它。（较少使用的运算符位于同级文件 rareSpells.qnt 中。）

---

指南

详细参考资料——需要了解超出上述速查内容的信息时，请阅读：

文件	内容
guidelines/operators.md	完整的运算符参考：扩展的集合／列表／映射运算符、测试和见证中的 run/then/expect/reps、时序公平性、q::debug
guidelines/simulations.md	见证与不变量、结果解读、渐进式递增协议、轨迹分析、覆盖率标准
guidelines/constraints.md	语言的硬性限制：不支持字符串操作、嵌套 match、解构、循环和提前返回
guidelines/cli.md	完整的 CLI 参考：quint run、quint test、quint verify 标志、详细程度指南、输出解读
guidelines/patterns.md	14 种核心模式：状态类型、纯函数、精简操作、映射预填充、语法规则、未定义行为、见证、非确定性测试、单独的测试文件、REPL 优先调试、先分离关注点、提取系统模型、类型优先搭建、逻辑桩
guidelines/tests.md	编写和调试测试：run/then/expect/reps/fail、非确定性测试、错误位置 ≠ 失败点、帧计数、REPL 优先调试
guidelines/choreo.md	用于分布式协议的 Choreo 框架：双文件拆分、choreo::cue 模式、.with_cue().perform() 测试、基于见证的测试发现