⚡

不变性王牌 invariant-ace

这个技能用于在软件开发中定义和强制执行不变性，通过验证和边界检查防止不可能状态的发生，确保系统正确性和鲁棒性。关键词包括不变性、验证、协议、测试、架构设计、幂等性、并发控制、算法正确性、边界精炼、状态机、模型检查、属性测试、反例追踪。

架构设计 0 次安装 0 次浏览 更新于 3/8/2026

名称: invariant-ace 描述: “通过定义拥有的归纳不变性并在解析/构造/API/数据库/锁/事务边界处强制执行它们，并附带验证信号，将‘不应发生’变为‘无法发生’。当提示提到不变性、不可能状态、验证蔓延、缓存/索引漂移、幂等性/版本控制、重试/重复/乱序事件、竞争/线性化错误、循环正确性或通过不变性检查首先强化另一个工作流（例如$fix）时使用。”

不变性王牌

使命

以最小化、高杠杆的更改将“不应发生”变为“无法发生”：选择拥有的归纳不变性；在最强的廉价边界处强制执行；通过具体反例追踪和验证信号证明。

使用时机（信号）

  • 空值/形状意外、运行时验证蔓延或输入解码分散在代码库中。
  • 冗余存储事实漂移（缓存/索引/非规范化列）或“修复”代码经常运行。
  • 标志/状态爆炸；不可能组合出现；“不可达”变得可达。
  • 竞争、重复/乱序事件、重试、部分失败或“恰好一次”假设。
  • 幂等键、单调版本/纪元检查、陈旧写入或线性化问题是核心。
  • 循环/算法正确性依赖于注释或直觉；棘手的索引/算术/终止。
  • “不应发生”分支出现在日志或错误跟踪器中。

路由优先级

  • 如果任务具有不变性/协议线索并要求广泛实现（$tk，$fix，$work），首先运行此技能以锁定不变性，然后执行编辑。
  • 如果无法命名状态所有者+过渡，在实现前切换到澄清/发现。

核心模型（快速定义）

  • 不变性：谓词P(state) 旨在在作用域内对所有可达状态保持为真。
  • 归纳的：初始时为真 AND 由该作用域内每个允许的过渡保持。
  • 所有者：控制所有突变以保持P的单个模块/类型/事务/锁/参与者。
  • 前置条件/后置条件：调用者义务 vs 操作保证；不要将这些误标为不变性。
  • 派生属性：可重新计算的事实；除非集中更新，否则避免存储为“必须匹配”。
  • 安全性与活性：不变性是安全性（“没有坏事”）；保持进度（“最终”）分开。

即时扫描

  • 状态所有者：真理在哪里（类型/模块/服务/表）？
  • 状态边界：原始数据在哪里进入（API/数据库/文件/队列）？
  • 允许的过渡：列出突变状态的操作/事件（包括重试和并发）。
  • 当前失败：一个具体追踪（输入 + 过渡 + 时间表）达到坏状态。
  • 保护级别：希望 -> 运行时 -> 构造时 -> 类型/编译时 -> 持久化/协议/原子性。
  • 痛点标签：数据 | 并发/协议 | 算法/循环（通常多个）。

保护阶梯

选择最便宜的强层，使违反变得困难或不可能。

  • 基于希望：注释、假设、“不可达”。
  • 运行时：分散的守卫/验证器靠近使用点。
  • 构造时：在边界处一次解析/验证；核心代码仅处理精炼值。
  • 类型/编译时：非法状态无法表示（抽象数据类型、类型状态、不透明包装器）。
  • 持久化：模式/约束/事务在静态时强制执行不变性。
  • 并发边界：锁/参与者/CAS/事务定义不变性必须保持的位置（锁下、提交时、线性化点）。

协议（反例驱动）

  1. 声明作用域 + 所有者。

    • 写“P在何时/何处保持”：始终 | 构造后 | 锁下 | 事务提交时 | 消息应用后。
    • 如果无法命名所有者，不变性将漂移；首先选择一个扼制点。

  2. 列出过渡并尝试打破P。

    • 对于每个过渡（及重试/乱序变体），尝试反例追踪。
    • 如果P失败，决定：错误 vs 错误作用域 vs 缺失状态 vs 错误所有者。

  3. 使P归纳（或降级它）。

    • 弱化P、将其移至前置/后置条件，或添加辅助状态（版本/纪元/状态/幂等键），直到它在过渡下闭合。

  4. 运行协调检查（并发/分布式）。

    • 问：两个各自有效的并发过渡可以合并成违反P的状态吗？
    • 如果是，需要协调（锁/事务/共识） OR 必须重新设计不变性/操作（分区、托管、单调合并、幂等性）。

  5. 在最强的廉价边界编码强制执行。

    • 偏好：解析器/解码器 + 智能构造函数 + 狭窄/不透明类型 + 集中突变。
    • 避免：N个分散验证器、没有单一写者的重复真理、每次读取的“修复”例程。

  6. 如果完整强制执行必须分阶段进行，则添加可观察性。

    • 添加廉价触发器（断言/日志/指标）和隔离路径（拒绝/死信/补偿）。
    • 记录可重放上下文（过渡名称、ID、版本），而非原始秘密。

  7. 用正确的测试验证。

    • 数据：模糊/属性测试解析器/构造函数。
    • 状态机：有状态/基于模型的测试（序列）。
    • 并发：压力 + 时间表扰动；在静止点断言。
    • 协议：小型模型检查/模拟丢弃/重复/重排序。
    • 算法：循环中的不变性断言 + 与参考的差异测试。

紧凑模式（快速路径）

当任务小或时间有限时使用。

  1. 反例：一个具体失败追踪（<=5个过渡）。
  2. 不变性：1-2个谓词，具有明确所有者 + 作用域。
  3. 强制执行边界：一个选择的扼制点（解析/构造/API/数据库/锁/事务）。
  4. 验证：一个信号链接到一个谓词。

如果任何上述内容模糊或非归纳，则升级到完整协议。

不变性记录（使用此格式）

  • 谓词：P(state)（精确，可检查）
  • 所有者：模块/类型/服务/表/锁/事务
  • 保持：始终 | 构造后 | 锁下 | 提交时 | 应用后
  • 由维护：必须保持P的过渡
  • 在处强制执行：解析/构造/API/数据库/锁/事务/协议
  • 要避免的反例：今天打破它的最小追踪
  • 验证：属性/有状态/压力/模型/差异

按痛点分类模式

数据建模和输入有效性

  • 边界精炼：原始 -> 解析 -> 验证；仅验证进入核心。
  • 规范化：尽早规范化（大小写/空格/时区/ID格式），以便相等性和缓存稳定。
  • 显式缺失：显式建模可选性；避免核心中的“有时为空”。
  • 跨字段耦合：将耦合字段合并为一个值，防止非法组合。
  • 非规范化纪律：如果存储派生事实，集中写入或使其可重新计算。

并发和协议正确性

  • 锁/事务不变性：P在锁下或提交时保持；定义线性化点。
  • 单调元数据：版本/纪元/计数器只增加；拒绝陈旧写入。
  • 幂等性：重试和重复是安全的（幂等键、去重表、“应用一次”）。
  • 显式状态机：枚举状态 + 允许过渡；持久化足够元数据以拒绝乱序事件。
  • 协调决策：如果P依赖于全局唯一性或并发借计下的非负性，选择协调或重新设计（分区/托管）。

算法和循环密集代码

  • 循环不变性：断言每迭代保持什么（分区区域、排序前缀、守恒定律）。
  • 变体/终止：命名递减度量；如果不能，预期非终止边。
  • 表示不变性：在API后隐藏内部结构；为测试/调试添加表示检查。
  • 差异测试：与简单、慢参考实现比较，捕捉角落情况。

之前/之后草图（语言无关）

边界精炼（数据）

之前：函数接受RawInput并临时验证
之后：  parseRaw(...) -> ValidatedValue | 错误
        核心函数仅接受ValidatedValue

幂等性 + 版本控制（并发/协议）

之前：handle(event) 直接突变状态（重试重复副作用）
之后：  if seen(event.id) return
        if event.version <= state.version return（或拒绝）
        apply(event) 在单个原子边界（锁/事务/CAS）

循环不变性（算法）

之前：注释说“数组左侧是分区”
之后：  assert(invariant(state)) 在循环内
        测试：随机数组，缩小失败案例，与参考比较

验证

选择至少一个信号，并将其链接到特定不变性谓词。

  • 属性/模糊：解析器、构造函数、规范化。
  • 有状态/基于模型：操作序列；每一步后检查不变性。
  • 并发压力：N线程 + 抖动；在静止点断言不变性。
  • 协议模拟：重排序/重复/丢弃 + 崩溃/重启；断言安全不变性。
  • 模型检查（可选）：小状态 + 穷举探索协议。
  • 差异/参考：算法输出等于随机输入的参考。
  • 运行时触发器：分阶段推出的断言/日志记录/指标。

研究锚点（心智模型，非要求）

  • Hoare/Floyd/Dijkstra：不变性作为证明对象；最弱前置条件。
  • ADT/表示不变性（Liskov风格）：抽象函数 + 局部推理。
  • 抽象解释：过近似可达状态；推断不变性。
  • 动态不变性挖掘（Daikon风格）：候选生成；用反例证伪。
  • 分离逻辑/框架：不变性链接到所有权；干扰感知推理。
  • 依赖保证和线性化：时间表下的并发不变性。
  • TLA+/Alloy思维方式：协议作为过渡 + 不变性；反例追踪。
  • 协调避免 / CRDT法则：当不变性需要协调 vs 合并安全设计时。

输出契约（必要标题）

在最终响应中为此技能使用这些确切标题：

  1. 反例
  2. 不变性
  3. 所有者和作用域
  4. 强制执行边界
  5. 接缝（之前 -> 之后）
  6. 验证
  7. 可观察性（可选）

可交付清单

  1. 反例：最小破坏追踪（包括时间表/重试，如果相关）。
  2. 不变性：1-5个谓词，具有所有者 + 作用域（“在何时保持”）。
  3. 强制执行边界：边界/类型/API/数据库/锁/事务/协议选择 + 原因。
  4. 接缝（之前 -> 之后）：使违反困难的最小结构更改。
  5. 验证：属性/有状态/压力/模型/差异链接到至少一个谓词。
  6. 可观察性（可选）：如果推出必须分阶段，触发器/隔离/指标。

跨协调

  • 如果出现更广泛的故障，依赖不健全性清单。
  • 如果更强不变性影响人体工程学，参考枪伤防护措施。

测量（seq）

用seq跟踪采用和合规性：

uv run codex/skills/seq/scripts/seq.py skill-trend --skill invariant-ace --bucket week
uv run codex/skills/seq/scripts/seq.py skill-report --skill invariant-ace \
  --sections "Counterexample,Invariants,Owner and Scope,Enforcement Boundary,Seam (Before -> After),Verification,Observability (optional)" \
  --sample-missing 5