quint-execute-spec

Quint 仕様の実行

Quint 仕様があり、コードベースに変更を加えたい場合、このスキルを使って作業の基準を仕様に置きます。仕様は参考情報ではありません。システムが何をしなければならないかを定める正式な記述です。すべての変更は仕様を満たす必要があります。まず仕様をレビューし、それからコードに取り組みます。

このスキルを使うタイミング

• リファクタリング：動作を維持しながらコードを再構成する（仕様は固定のまま、コードは引き続き仕様を満たす必要があります）
• 新機能：仕様に記述されている、または仕様に合致する機能を追加する
• ギャップの解消：コードが仕様から逸脱している場合、仕様に適合する状態に戻す
• 仕様先行の変更：まず仕様を更新し、その要件を満たすよう実装する

まだ仕様がない場合は、まず quint-modeling を使って基準となる成果物を作成してください。

---

基本原則：仕様が正解の基準

このスキルはループの仕様策定後の段階です。調査と計画は、文章だけの計画ではなく、既存の .qnt ファイルと簡潔なギャップ分析に基づいて行います。実装は、フェーズ 3～4 の検証ゲート（実質的な編集後の Quint ツール実行）を通過して初めて進めます。自然言語の計画は証明ではありません。証拠となるのはツールの実行結果です。

検証に失敗しても、仕様を変更して通そうとしてはいけません。 仕様を変更する必要がある場合（動作を意図的に変更する場合）は、コードに手を加える前に作業を止め、仕様変更案をユーザーに提示してください。仕様変更は、最も重要なレビューの機会です。

コンテキスト使用率の目標：調査と計画の間は 40～60% です。すべてをメインのコンテキストに読み込むのではなく、コードベースを簡潔に把握してください。

---

ワークフロー

[Quint spec] + [Desired change description]
         ↓
┌────────────────────────────────────────────────────────────┐
│ Phase 0: Orient                                             │
│   → Read the spec: what does it guarantee?                 │
│   → Clarify the change: what new behavior is needed?       │
│   → Decide: is this a spec change or a code change?        │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ Phase 1: Research (compact)                                 │
│   → Map the gap between spec and code                      │
│   → Output: compact gap analysis (target: under 300 lines) │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ Phase 2: Plan                                               │
│   → Precise steps: files to change, expected state delta   │
│   → For each step: how to verify it satisfies the spec     │
│   → Identify which Quint properties to run at each gate    │
│   → Present plan to user before implementing               │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ Phase 3: Implement                                          │
│   → Follow plan phase by phase                             │
│   → After each phase: run Quint tools, verify properties   │
│   → Compact status back into the plan after each phase     │
└────────────────────────────────────────────────────────────┘
         ↓
┌────────────────────────────────────────────────────────────┐
│ Phase 4: Verify                                             │
│   → Run all witnesses (expect VIOLATED)                    │
│   → Run all invariants (expect no violation)               │
│   → If any invariant fails: return to Phase 2, fix plan    │
└────────────────────────────────────────────────────────────┘

---

フェーズ 0：概要の把握

仕様を読み、意図された変更を理解します。

1. 仕様を読む。何をモデル化していますか？どの不変条件を主張していますか？どのようなウィットネスがありますか？
2. 仕様の引き継ぎセクション（存在する場合）を読む。仕様はどのソースファイルに対応していますか？
3. 変更内容を明確にする。ユーザーに次の点を確認します。
   • どのような動作が変わりますか？（リファクタリングの場合は、何も変わらないはずです。機能追加の場合は、何が新しくなりますか？）
   • 仕様を変更しますか。それとも、既存の仕様をコードが満たす必要がありますか？
   • 既存の不変条件が失敗していますか。それとも、今後に向けた変更ですか？

簡易パス（単純な変更では調査を省略）： 変更が小規模（単一の関数、1 つのモジュール、新しい状態なし）であれば、フェーズ 1 を省略し、フェーズ 2 に進みます。

---

フェーズ 1：調査（簡潔に）

複雑な変更では、仕様とコードの簡潔なギャップ分析を作成します。焦点を絞ってください。目的は、コードベース全体を読み込むことではなく、簡潔で正確な要約を作ることです。次の質問に答えてください。

[spec path] の Quint 仕様と、[file list from handoff] のソースファイルを前提として：

1. 仕様内の各状態変数について、ソースコード内でどこが管理しているかを特定する
2. 仕様内の各アクションについて、ソースコード内の対応する関数を特定する
3. 仕様の動作のうち、対応するソースコードがないもの（ギャップ）を特定する
4. 仕様に記述されていない、ソースコードの動作（スコープ外）を特定する
5. [change description] の変更に影響するソースファイルを特定する

簡潔な要約を出力してください。関係のないファイルは読まないでください。目標：300 行未満。

分析で重要な点を見落とした場合は、先に進む前に対象を絞って追加調査してください。

---

フェーズ 2：計画

正確な実装計画を作成します。計画の各ステップでは、次の点を必ず記述してください。

• 変更するファイルと関数
• 期待される状態の差分（システムの動作にどのような変化があるか）
• 検証ゲートとして実行する Quint プロパティ
• 個別に検証できる程度の小ささ

計画の形式

## Change: [one-sentence description]

### Spec impact
- Properties that must continue to hold: [list]
- Properties that will change (if any): [list] — REQUIRES USER APPROVAL BEFORE IMPLEMENTATION

### Implementation steps

#### Step 1: [file] — [what changes]
- Expected behavior change: [description]
- Quint verification gate: `quint run` / `quint verify` — invariant `[name]`

#### Step 2: [file] — [what changes]
...

### Rollback criteria
If invariant `[name]` fails after Step N, stop and return to planning. Do not proceed.

実装を始める前に、計画をユーザーに提示してください。 コードのレビューよりも、人による計画のレビューのほうが効果的です。

計画に仕様の変更が必要な場合は、仕様変更案を明示して、事前に承認を得てください。

フェーズ 3：実装

計画に従います。各ステップの後に、以下を行います。

1. quint typecheck を実行し、報告されたエラーをすべて修正します。
2. ステップの検証ゲート（quint run ／ quint test ／ quint verify）を実行します。
3. ゲートに失敗した場合：停止して原因を特定し、フェーズ 2 に戻ります。仕様を緩めて修正してはいけません。
4. 各ステップの後に、現在の状況を計画ファイルにまとめます。次のステップでコンテキストウィンドウを圧迫しないようにするためです。

コンテキストのまとめ方

各ステップの検証後、進捗をまとめます。

## Status (after Step N)
- Steps 1–N: DONE ✓
- Current: Step N+1
- Blocking issues: [none / description]
- Next verification gate: [invariant name]

これを計画ファイルに書き込みます。複雑な実装では、コンテキストが過負荷になった状態で続行するのではなく、更新した計画を使って新しいコンテキストウィンドウを開始してください。

実装中の Quint ツールの使い方

必要な作業	ツール
編集後に仕様を型チェックする	quint typecheck を実行します。続行する前に、報告されたエラーをすべて修正します
反例が到達可能か検証する	反例を不変条件として指定して quint run を実行します
安全性不変条件が満たされるか検証する	--max-samples 5000 を指定して quint run を実行するか、quint verify を実行します
対話的に探索する	quint REPL session と quint REPL eval を使用します（CLI では不十分な場合のみ）

---

フェーズ 4：検証

プロパティスイート全体を実行します。

反例（活性チェック）

すべての反例が違反状態である必要があります（つまり、期待される状態に到達可能です）。

• witnesses 内の反例名（または対応付けられた不変条件セレクター）を指定して、quint run を使用します。
• 期待される結果：反例への到達可能性が報告されます（生の CLI 表記での Counterexample found に相当します）。

安全性不変条件

すべての不変条件が違反状態にならない必要があります。

• quint run を使用します（より広いカバレッジが必要な場合は quint verify を使用します）。
• 期待される結果：不変条件違反が報告されないこと。

安全性不変条件に違反した場合

1. 反例のトレースをステップごとに読みます。
2. どの実装ステップで違反が生じたか特定します。
3. フェーズ 2 に戻り、仕様ではなく計画を修正します。
4. 仕様の不変条件に本当に誤りがある場合は、提案する仕様変更をユーザーに提示します。

反例が満たされた場合（アクションに到達できない）

実装で制約をかけすぎています。到達可能であるべき経路が妨げられています。 フェーズ 2 に戻り、どのステップで制約が加わったか特定します。

---

仕様変更の手順

希望する変更に仕様の更新が必要な場合（新しい状態変数、変更された不変条件など）：

1. 仕様変更案を作成する — コードを変更する前に、差分をユーザーに提示します。
2. 更新した仕様を単独で検証する — 型チェックを行い、反例を実行し、不変条件を実行します。
3. 明示的な承認を得る — 仕様変更が承認されるまで、コードに着手してはいけません。
4. その後、更新した仕様を満たすコードを実装します。

これにより、仕様が進化する場合でも、仕様を信頼できる唯一の情報源として維持できます。

---

してはいけないこと

アンチパターン	ワークフローを損なう理由
不変条件の失敗を解消するために仕様を変更する	仕様が信頼できる唯一の基準でなくなります
ステップ間の検証ゲートを省略する	段階的な検証が崩れ、バグが積み重なります
コードベース全体をメインコンテキストに読み込む	コンテキストを圧迫します。代わりにフェーズ 1 で簡潔にカタログ化します
大まかな文章で計画し、「おおよそ」実装する	計画は、ステップごとの検証に十分な精度が必要です
仕様を参考用のドキュメントとして扱う	仕様は形式的な制約であり、機械検証できます
不変条件を弱めて不変条件の失敗を修正する	不変条件は緩めるのではなく、コードで修正する必要があります

---

小規模な変更向けの簡易手順

小さく、内容が明確な変更（単一の関数で、新しい状態を追加しない場合）では：

1. 関連する仕様モジュールを読みます。
2. 変更する動作を対象とする不変条件を特定します。
3. 変更を行います。
4. それらの不変条件を指定して quint run を実行します。
5. 完了です。

フェーズ 0〜1 は省略します。複雑な変更でのみ、フェーズ 2〜4 を使用してください。