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 { ... } — 少なくとも 1 つが成立する必要があります（論理和）。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 の型システムでは、これらをまとめることができます。フィールドが一貫性のある 1 つのローカル状態を表す場合は、レコード型を作成し、その型の状態変数を 1 つ使用してください。

次の場合はレコードにまとめます：

• 1 つのアクターのローカル状態を表す場合（例：1 つのノードのフェーズ、ログ、投票）
• 関数の引数として常に一緒に渡される場合
• 不変条件が、同じ概念上のエンティティの複数のフィールドに関係する場合

次の場合はフラットなままにします：

• 変数が、独立して変化する別々の関心事を表す場合
• コンポーネントが単純で、まとめても明確さが増さない場合
• 変数が意図的に異なる所有権またはライフサイクルの領域に分かれている場合

例：推奨されるローカル状態のグループ化とアンチパターン

推奨（まとまりのあるローカル状態）：

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

各バリアントには名前付きコンストラクターがあり、1 つのペイロードを持ちます。コンストラクターが受け取る引数はちょうど 1 つです。複数のフィールドを渡す場合は、（上記のように）レコードまたはタプルでラップしてください。

コンストラクターを呼び出して値を作成します：

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 宣言を書く前に、候補となる各グループについて次の質問に答えてください。

質問	グループ化 → 次の場合は記録する	フラットのままにする → 次の場合
これらの変数は常に一緒に変化しますか？	ほとんどのアクションでそうである	互いに独立している
同じエンティティを表していますか？	同じノード／同じメッセージ／同じラウンドである	関心事が異なる
インスタンスは1つですか、それともN個ですか？	1つでもN個でも（まとまりがある場合はグループ化し、N個の場合は Id -> RecordType を使う）	関心事が真に独立している場合に限り、フラットのままにする
不変条件はそれらに関係しますか？	1つのエンティティの複数のフィールドにまたがる不変条件である	不変条件が変数を個別に使う

---

ブール演算子

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

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

---

ファイル構成

仕様を2つのファイルに分割します。

<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 に組み込まれていませんが、ほとんどの Quint プロジェクトに同梱されている標準ライブラリ basicSpells.qnt で利用できます。次のようにインポートします。

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)	key が存在する場合は m.get(key)、存在しない場合は default です。
mapRemove(m, key) / mapRemoveAll(m, ks)	key（またはキーの集合 ks）を除いた m のコピーです。
setRemove(s, e) / setAdd(s, e)	要素 e を除いた／追加した集合 s のコピーです。
find(s, f) / findFirst(l, f)	f を満たす集合／リストの最初の要素を Option として返します。
max(i, j) / min(i, j) / abs(i)	2 つの整数の最大値／最小値、および絶対値です。

インポートせずに Option、require、values、transformValues を使っている仕様を見つけたら、basicSpells に依存している可能性があります。プロジェクトに含まれているか確認してください。（あまり一般的でない演算子は、兄弟ファイルの rareSpells.qnt にあります。）

---

ガイドライン

詳細なリファレンスです。上記のクイックリファレンスだけでは足りない場合に参照してください。

ファイル	内容
guidelines/operators.md	演算子の完全なリファレンス：拡張された集合／リスト／マップ演算子、テストと証人のための run／then／expect／reps、時相公平性、q::debug
guidelines/simulations.md	証人と不変条件、結果の解釈、段階的な増加プロトコル、トレース分析、カバレッジ標準
guidelines/constraints.md	言語の厳格な制限：文字列操作なし、ネストした match なし、分割代入なし、ループなし、早期 return なし
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 フレームワーク：2 ファイルへの分割、choreo::cue パターン、.with_cue().perform() によるテスト、証人ベースのテスト検出