invariant-check git:20261105.956d98aA

Immutable. This exact content never changes and is served at /api/v1/blob/934315280c5339ea.

---
name: invariant-check
description: 不变量检查：改动碰到会持久化、要在失败或崩溃后恢复的状态机（发布与迁移、送达与确认、重试与标记文件、定时叫醒），或审查一轮轮在同一状态机上找出新的中断点时使用。
---

# 不变量检查

审查逐个想中断点，每轮只能多找到一个；把“每一步 × 每种故障”穷举一遍，崩溃、断电、重跑造成的卡死和残留能一次找全。它只查写成不变量的性质，漏写一条，那一类缺陷就全漏，所以它补审查，不替代审查。在第一次送审前做，或者审查第二次在同一状态机上报新实例时，停止逐个修补，改做这个。

1. **写不变量**：只挑最贵的几条承诺，每条一句话写性质、一句话写违反时的危害，指到需求或项目文档的原文。三类性质都要过一遍：
   - 最终恢复：“几次正常的轮询或重跑之内，一定恢复成一套与当前库兼容的完整服务”；
   - 过程中不中断：“站点在线时，恢复或下一次发布都不得让它下线”；
   - 仍在使用的资源不被销毁：在途连接、排空中的 worker、未确认的消息。

   需求里两条承诺看似冲突时（“排空尽力而为”与“排空后才停旧实例”），两条都写成不变量，让检查把冲突暴露出来，不先选一种解读。完成标准：每条承诺原文都对应到一条不变量或一句“不查”的理由。

2. **选做法**：
   - 外部依赖能在进程边界上换成替身时，对真实代码做穷举故障注入：被测代码全用真的，只替换外部命令、网络、数据库、时钟。没有模型与代码不同步的问题，首选这个。
   - 编译慢、替身难做准（真实子进程、复杂异步时序）时，用 TLA+ 之类的模型检查器写小模型，每个动作指回代码里的位置，并记下覆盖的文件和最后核对过的提交。

   完成标准：写下选的做法和理由；用模型检查时，每个动作都已指到代码位置。

3. **定场景、恢复事件与故障**：
   - 场景是会改变结果的初始状态与外部行为的组合。维度从需求和外部接口逐项列：要不要迁移、版本谁领先、旧版是否兼容、上一次运行留下的状态、有没有在途连接或未完成的工作，外部接口返回空、被替换、并发写入等。漏掉一维，那一维上的缺陷就抓不到。
   - 列出真实系统里触发恢复的事件（定时器重跑同一任务、下一个新任务到来、重启），只用这些事件驱动恢复，不自己发明：由谁触发恢复会直接改变判定。
   - 注入点是每个外部动作和每次文件改动（写、改名、截断、删除）。故障至少五种：某一步失败；进程被杀（不执行任何异常处理，例如 fork 后 `os._exit`）；宿主崩溃；断电（没 fsync 的写入和改名回退或变空）；依赖一段时间不可用。
   - 替身的每条行为假设写下来并标置信度，反例依赖哪条假设也标上。替身遇到没建模的命令或参数时报检查自身的错误，不记成被测代码失败；换一个提交重跑时先看这类错误数。
   - 完成标准：所有场景能在几分钟内跑完，输出违反数、检查自身错误数和每个反例的步骤序列；太慢就只对关键场景做逐步单故障，其余场景只跑无故障。

4. **先跑无故障**：所有场景不注入故障跑一遍。这一步常直接找出缺陷，也是清掉检查自身误报的地方：违反要么是真缺陷，要么修好检查。基线解释清楚后，再穷举单故障，最后加随机双故障。完成标准：无故障下的每个违反都已判定为真缺陷或修掉的误报，检查自身错误数为 0。

5. **证明它能失败**：破坏从需求推出，不从已建的模型推出：每条承诺原文至少对应一处破坏（例如“不等排空就停旧实例”）。只破坏模型里已有的东西，证明不了漏写的不变量。先确认破坏真的改变了代码行为（例如抛出的异常没被同一函数自己吞掉），再看检查是否抓到。有修好的版本就在它上面破坏；只有原版时在原版上破坏，按（场景、故障、不变量）的组合与原版比违反数，不按步号比，破坏会让步号平移。抓不到就补不变量、场景维度、恢复事件或故障种类，不改破坏。完成标准：每条承诺至少有一处破坏，每处都被抓到。

6. **用它修**（只找不修的任务跳过这一步和第 7 步，直接汇报）：同一不变量下的反例一次修完，修到全部通过再送审；修复本身也会引入新反例，每次改完都重跑。完成标准：修好的版本上所有场景通过，检查自身错误数为 0。

7. **留存**：问用户要不要留下这条检查。留就放进项目：一条命令按需运行，记下覆盖的文件和最后核对过的提交，项目 AGENTS.md 加一行条件指针（“改到某某时跑某命令”）；放进 CI 另外问。完成标准：照用户的答复做完。

汇报：不变量与出处、场景维度、恢复事件与故障种类、替身假设、场景数与耗时、找到的反例（用代码里的名词写成一串短步骤）、破坏验证结果，以及没有覆盖的部分。通过只代表在建模的场景里成立。