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，直接进入阶段 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：验证

运行完整的属性套件。

见证（活性检查）

所有见证都必须被违反（这表示预期状态可达）：

• 使用 quint run，并在 witnesses 中指定见证名称（或映射后的不变量选择器）。
• 预期结果：报告见证可达性（等同于原始 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。