invariant-check git:20261104.bccf3e5A

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

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

# 不变量检查

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

1. **写不变量**：只挑最贵的几条承诺，每条一句话写性质、一句话写违反时的危害，指到需求或项目文档的原文。三类性质都要过一遍：
   - 最终收敛：“几次正常推进之内一定恢复成一套与当前库兼容的完整服务”；
   - 推进途中不中断：“站点在线时，恢复或下一次发布都不得让它下线”；
   - 仍在使用的资源不被销毁：在途连接、排空中的 worker、未确认的消息。
   需求里两条承诺看似冲突时（“排空尽力而为”与“排空后才停旧实例”），两条都写成不变量，让检查把冲突暴露出来，不先选一种解读。完成标准：每条承诺原文都对应到一条不变量或一句“不查”的理由。

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

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

4. **先跑无故障**：所有世界不注入故障跑一遍。这一步常直接找出缺陷，也是清掉检查自身误报的地方：违反要么是真缺陷，要么修好检查。基线解释清楚后，再穷举单故障，最后加随机双故障。

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

6. **用它修**：反例用代码里的名词写成一串短步骤。同一不变量下的反例一次修完，修到全部通过再送审；修复本身也会引入新反例，每次改完都重跑。只找不修的任务到这里为止，直接汇报。

7. **留存**：检查放在项目里，一条命令按需运行。项目 AGENTS.md 加一行条件指针（“改到某某时跑某命令”），检查里记下覆盖的文件和最后核对过的提交。要放进 CI 或长期保留，先经用户认可。

汇报：不变量与出处、世界维度、推进事件与故障种类、替身假设、场景数与耗时、找到的反例、破坏验证结果，以及没有覆盖的部分。通过只代表在建模的世界里成立。