kani-proof

前置条件

编写证明前，请确认工具已安装：

1. **Kani：**运行 cargo kani --version。如果未安装：

   cargo install --locked kani-verifier
   cargo kani setup
   

2. **Linter（可选，但建议安装）：**需要 Node.js。通过 npx -p @workersio/klint klint 运行。

Kani 形式化验证

Kani 是一个有界模型检查器——它会探索界限内符号输入的所有可能值，因此证明是穷尽式的（不像模糊测试那样只是抽样）。

关键规则

这些规则可避免最常见的证明失败。违反任何一条都很可能导致证明失败。

1. **首次尝试时不要使用 #[kani::unwind] 或 #[kani::solver]。**完全省略这两个装饰器。只有在出现“展开断言”错误后才添加 #[kani::unwind(N)]，且只有在超时后才添加 #[kani::solver(kissat)]。Kani 的默认设置比猜测参数效果更好。

2. **直接在内联代码中断言目标属性，而不是通过辅助方法。**不要调用检查多个不变量或遍历集合的方法——这会引入循环、额外断言和无关的失败点。直接读取结构体字段并自行编写比较：

   // WRONG — helper checks more than the target property, adds loops
   assert!(engine.check_all_invariants());
   
   // RIGHT — asserts exactly what you're proving, no extra logic
   assert!(engine.x.get() >= engine.y.get() + engine.z.get());
   

3. **首先使用 kani::any()，不要使用 kani::assume() 设置边界。**只有在超时或内存不足后才添加 assume 约束。对于求解器来说，不受约束的符号值往往比有界范围更容易处理。

4. **只能通过公共 API 构建状态。**使用构造函数、add_user()、deposit() 等。绝不要直接赋值给结构体字段——这会创建不可达状态，导致虚假失败。唯一例外是 vault 或其他没有 setter API 的类似顶层字段。

5. **使用栈分配，不要使用 Box。**使用 let mut engine = Engine::new(params)，而不是 Box::new(Engine::new(params))。Box 会增加求解器的堆跟踪开销。

6. **使用较小的配置参数。**如果构造函数接受用于控制循环的大小／容量参数（例如 max_accounts），请传入较小的值（4–8），并与分析 Agent 找到的 #[cfg(kani)] 常量相匹配。

工作流

对证明进行分类

选择工作流前，先对证明进行分类：

• **简单：**目标是纯函数（没有 &mut self），或模式为 P7（算术安全）／P11（具体已知错误）／安全性／等价性；且调用图中没有循环，并且不需要构建多实体状态。
• **标准：**其他所有情况——有状态变更、P1–P6／P8–P10／P12、循环、多实体状态。

---

简单流程（不启动 Agent）

对于简单证明，直接内联完成，无需启动子 Agent：

1. **编写证明：**直接根据模式模板编写。阅读相应的 references/templates/ 文件（例如，P7 使用 arithmetic-safety.rs，安全性／等价性使用 safety.rs），并根据需要调整。从 references/templates/infrastructure.rs 开始，了解共享宏。

2. **内联执行 Linter：**直接运行 Linter：

   npx -p @workersio/klint klint <file>
   

   继续前先修复所有错误或警告。

3. **内联验证：**直接运行 Kani：

   cargo kani --harness <harness_name>
   

   如果失败，请按照诊断失败中的方法修复，然后重新运行。

---

标准流程（使用 Agent）

对于需要分析代码库、构建状态或迭代调试的复杂证明：

步骤 1 — 分析代码库

按照 references/agents/kani-analyzer-agent.md 启动 Explore Agent。它会返回循环边界、现有基础设施和状态构建模式。请勿跳过此步骤。

步骤 2 — 编写证明

使用 Agent 的输出编写 harness。从模式表中选择一个模式，并参阅 references/proof-patterns.md 获取模板。模板文件位于 references/templates/——阅读相应的模板并根据需要调整。先从 infrastructure.rs 开始，了解共享宏（assert_ok!、assert_err!、快照类型）。

步骤 3 — 检查证明

编写证明后、运行 cargo kani 之前，按照 references/agents/kani-linter-agent.md 的说明启动一个检查器 Agent。该检查器可在几秒内静态检测 23 种常见反模式（矛盾的假设、缺少展开、空洞证明风险、过度约束的输入等），比耗时数分钟的 cargo kani 运行快得多。

• 错误 → 必须在继续验证前修复（矛盾的假设、无效断言、harness 参数）
• 警告 → 应修复，以避免挂起／OOM／空洞证明（缺少展开、没有符号输入、状态空间过大）
• 建议 → 可考虑采纳，以提高证明质量（缺少 cover、假设顺序）

修复所有错误并处理警告，然后重新运行检查器，直到检查通过，再继续步骤 4。

步骤 4 — 验证并迭代

检查器通过后，按照 references/agents/kani-verifier-agent.md 的说明启动一个验证器 Agent。它会运行 cargo kani、解析输出并返回结构化诊断结果。

如果验证器报告 FAIL：

• unwinding assertion → 添加 #[kani::unwind(N)]，N 取错误中的值
• OOM → 缩小符号范围、调低配置参数、移除 Box
• assertion failed → 检查失败的断言并修复证明逻辑
• timeout → 尝试 #[kani::solver(kissat)]，缩小范围
• covers UNSATISFIABLE → 假设相互矛盾，放宽限制

迭代：根据诊断结果修复证明，重新运行检查器，然后重新运行验证器。切勿提交未经验证的证明。

完整的 Kani API（合约、桩替换、具体回放、分区验证）请参阅 references/kani-features.md。

Kani 专属概念

非空洞性

即使什么也没有证明，证明也可能报告 SUCCESS。如果没有执行路径能到达断言，就会发生这种情况——例如，操作总是因输入而失败、假设相互矛盾、结果被丢弃，或者状态为空／无实际内容。

使用 kani::cover!(condition, "message") 检测——如果 Kani 报告 UNSATISFIABLE，说明该路径从未执行。

通过显式处理结果来避免：

// VACUOUS — if operation always fails, nothing is checked
if result.is_ok() { assert!(invariant); }

// NON-VACUOUS — proof fails if operation can't succeed
match result {
    Ok(_) => { /* assert properties */ },
    Err(_) => { kani::assert(false, "must succeed"); unreachable!() }
};

**相互矛盾的假设：**如果每条路径都会命中 assume(false)，或者所有 kani::cover!() 检查都为 UNSATISFIABLE，那么你的 kani::assume() 约束就相互矛盾——不存在有效输入。移除约束，从不设限制的状态开始。

循环展开

只有遇到“unwinding assertion”错误时才需要处理。在 N = 最大迭代次数 + 1 时添加 #[kani::unwind(N)]。追踪调用图中的所有循环（目标函数 + 被调用函数 + 构造函数）。检查是否存在会缩小集合大小的 #[cfg(kani)] 常量。

**由参数驱动的循环：**如果构造函数会遍历配置参数（例如 for i in 0..capacity），该参数必须较小（4–8）。如果存在 #[cfg(kani)] 常量，请使用它们。

诊断失败

Kani 输出	修复方法
unwinding assertion	添加 #[kani::unwind(N)]，其中 N = 循环次数 + 1
Timeout / solver hang	添加 kani::assume() 缩小范围，尝试 #[kani::solver(kissat)]
VERIFICATION:- FAILED	使用 cargo kani -Z concrete-playback --concrete-playback=print --harness name
OOM / out of memory	缩小状态大小、移除 Box、减少符号变量
assume(false) on all paths	移除 kani::assume() 约束——它们相互矛盾
VERIFICATION:- SUCCESSFUL	检查 kani::cover!() 语句是否为 SATISFIED（非空洞性）

**迭代方法：**从简单开始（不加修饰符、输入不设限制、通过 API 构建状态）→ 仅在超时／OOM 时添加约束 → 仅在出现展开错误时添加 unwind → 仅在超时时切换求解器。

何时不应使用 Kani

Kani 有实际局限。以下情况会在注定失败的证明上浪费大量时间：

情况	Kani 难以应对的原因	更合适的工具
浮点运算	不支持符号化 f32/f64	proptest, bolero
异步代码	未对运行时建模	tokio::test + proptest
网络/IO	无法对系统调用建模	集成测试
没有契约的深层递归	展开次数无界	函数契约或 proptest
状态过大（>1000 个元素）	求解器超时	使用 #[cfg(kani)] 缩小规模或进行模糊测试

证明模式

完整的模式文档请参见 references/proof-patterns.md。模板文件位于 references/templates/ — 读取适当的模板并进行调整。从 infrastructure.rs 开始，其中包含共享宏（assert_ok!、assert_err!、快照类型）。

模式	适用场景	证明内容
守恒	移动、创建或销毁数量	账目等式保持不变
框架 / 隔离	针对多实体系统中的单个实体	未受影响的实体保持不变
不变量保持	任何状态变更	变更前后均满足规范不变量
错误路径	输入验证 / 前置条件	返回特定错误，且状态完全不变
单调性	计数器、时间戳、累加器	值只会朝一个方向变化
幂等性	结算、同步、重新计算	执行两次 = 执行一次
算术安全	数值计算	不会溢出、下溢或除以零
访问控制	特权操作	拒绝未经授权的调用者
状态机	生命周期转换	只发生有效的转换
归纳增量	核心账目（最强形式）	等式对原始基元成立
生命周期 / 序列	多步骤用户流程	属性在连续操作过程中保持成立

Harness 框架

#[cfg(kani)]
mod kani_proofs {
    use super::*;

    #[kani::proof]
    // NO #[kani::unwind] — only add after getting unwinding assertion error
    // NO #[kani::solver] — only add after getting timeout
    fn proof_name() {
        // 1. Build state through public API (NOT field mutation)
        // 2. Symbolic inputs: kani::any() with NO kani::assume() bounds
        // 3. Call function, handle result explicitly (no if result.is_ok())
        // 4. Assert ONLY the target property using raw field access
        //    (NOT check_conservation or other aggregate methods)
        // 5. kani::cover!() for non-vacuity
    }
}

代码库准备

Explore Agent 会识别所需的准备工作。常见准备包括：

• #[cfg(kani)] const MAX_ITEMS: usize = 4; — 缩小集合大小
• 在 Cargo.toml 中添加 [workspace.metadata.kani] flags = { tests = true }
• 在 crate 根目录添加 #[cfg(kani)] extern crate kani;

参考文件

• references/proof-patterns.md — 模式目录，包含模板和示例
• references/templates/ — 每种证明模式对应的 Rust 模板文件（infrastructure、conservation、frame-isolation、arithmetic-safety、inductive-delta、safety）
• references/kani-features.md — Kani API：契约、桩函数、具体回放、分区验证
• references/invariant-design.md — 分层不变量设计方法
• references/anchor-verification.md — 使用 OtterSec 注解验证 Anchor 程序
• references/agents/kani-analyzer-agent.md — 用于证明前代码库分析的 Explore Agent
• references/agents/kani-linter-agent.md — 用于静态 lint 检查的 Explore Agent（验证前运行）
• references/agents/kani-verifier-agent.md — 用于证明后验证和诊断的 Explore Agent