moonbit-proof

MoonBit 携带证明的代码

当任务涉及编写、扩展或调试经过验证的 MoonBit 代码时，请使用此技能。

常见触发场景：

• 为可执行的 MoonBit 代码添加契约
• 定义抽象模型或表示不变量
• 验证递归数据结构
• 将具体表示关联到集合／映射模型
• 用引理替换可信的证明桥接
• 调试证明失败、超时或前端降级限制

目标

编写携带证明的代码，而不是看起来像证明的注释。

这意味着：

• 运行时代码仍然可执行且易于阅读
• 证明模型明确
• 契约围绕命名谓词／函数展开，且职责一致
• 局部 proof_assert 步骤说明实现为何满足模型

命名

优先使用 model(...)，作为证明侧的值语义视图的默认名称。

示例：

• model(set) : Fset[Int]
• model(map) : Fmap[Int, Int]
• model(tree) : Seq[Int]

只有在更具体的名称能显著提升清晰度时，才使用它：

• elements(node)：当模型确实是递归子树中存储的元素集合时
• domain(bitmap)：当模型特指已占用的索引集合时
• height(tree)：当它是结构度量，而不是主要语义模型时

默认规则：

• 主要语义抽象使用 model
• 辅助视图使用 elements、domain、height 或 rank 等专用名称

默认结构

将包拆分为两层。

• .mbtp
  • model(x) 等模型函数
  • tree_inv(x) 或 sparse_array_inv(x) 等表示不变量
  • insert_pre(...) 和 insert_post(...) 等命名证明谓词
  • 可复用的引理
• .mbt
  • 可执行代码
  • 针对证明侧谓词的契约
  • 在构造、分支和循环之后添加局部 proof_assert 步骤

除非有充分理由，否则使用此默认结构。

推荐工作流

1. 先选择抽象模型。
2. 定义最小且实用的不变量。
3. 使用命名的 *_pre / *_post 谓词编写契约。
4. 实现运行时代码。
5. 为每个与证明相关的循环添加循环不变量。
6. 在求解器需要帮助的地方添加局部 proof_assert 步骤。
7. 只有在看到实际失败的 VC 后，才引入辅助引理。
8. 从构造函数开始，逐步缩减可信桥接。

不要一开始就写一大堆引理。

步骤 1：选择合适的抽象模型

优先选择与可观察行为相符的最简单模型。

• 仅用于成员判定的结构：使用有限集合。
• 键值结构：使用有限映射。
• 递归树／字典树：使用 model(node)；若更清晰，也可使用 elements(node)。
• 紧凑布局：将定义域／布局事实与语义含义分开。

示例：

fn model(set : HashSet) -> Fset[Int] {
  match set.root {
    None => @fset.fset_empty()
    Some(node) => model(node)
  }
}

如果递归辅助函数确实表示子树的元素集合，使用以下写法也很合理：

fn elements(node : Node) -> Fset[Int] {
  match node {
    Empty => @fset.fset_empty()
    Branch(l, x, r) => elements(l).union(elements(r)).add(x)
  }
}

避免将全部语义直接写进每个契约。

步骤 2：保持不变量精简

不变量应主要描述：

• 形状
• 边界
• 布局
• 良构性

语义等式通常应放在后置条件或引理中，而不是放进 *_inv。

好的写法：

predicate sparse_ok(sa : SparseArray) {
  sa.data.length() == count_value(sa.bitmap, 0) &&
  (∀ i : Int,
    valid_idx(i) && mem_value(sa.bitmap, i) →
      0 <= rank_value(sa.bitmap, i, 0) &&
      rank_value(sa.bitmap, i, 0) < sa.data.length())
}

不好的写法：

• 将每个更新定理都放进不变量
• 将完整的语义等式编码进 *_inv

步骤 3：使用命名后置条件

优先使用命名谓词，而不是重复冗长公式。默认命名约定为 *_inv、*_pre 和 *_post。

好的写法：

predicate singleton_post(res : SparseArray, idx : Int, value : Int) {
  sparse_ok(res) &&
  model(res).eq(@fmap.fmap_empty().add(idx, value))
}

pub fn singleton(idx : Int, value : Int) -> SparseArray where {
  proof_require: valid_idx(idx),
  proof_ensure: result => singleton_post(result, idx, value),
} {
  ...
}

这样可以使契约更精简，并为求解器提供可复用的目标。

第 4 步：将数学内容放入 .mbtp

证明侧内容应放在 .mbtp 中。

示例：

fn model(t : Tree) -> Fset[Int] {
  match t {
    Empty => @fset.fset_empty()
    Node(l, x, r, _) => model(l).union(model(r)).add(x)
  }
}

predicate avl(t : Tree) {
  match t {
    Empty => true
    Node(l, x, r, h) =>
      avl(l) &&
      avl(r) &&
      all_lt(model(l), x) &&
      all_gt(x, model(r)) &&
      h == 1 + max2(height(l), height(r))
  }
}

让 .mbtp 专注于：

• 逻辑定义
• 谓词
• 引理

避免在 .mbtp 中塞入运行时实现细节。

以下两种常见的辅助模式尤其有用：

1. 抽象结构的外延相等假设。

示例：

predicate fmap_eq_hyp(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) {
  (∀ k : Int, m1.mem(k) == m2.mem(k)) &&
  (∀ k : Int, m1.mem(k) → m1.find(k) == m2.find(k))
}

lemma fmap_eq_intro(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) where {
  proof_require: fmap_eq_hyp(m1, m2),
  proof_ensure: m1.eq(m2),
} {
}

这通常是完成映射精化证明最简洁的方式。

2. 用于更新的小型传递引理。

示例：

• 在自身键和其他键上添加/移除 mem
• 在自身键和其他键上添加/移除 find
• 添加/移除不存在/存在的元素后设置基数

相比一个庞大的“所有内容都已正确更改”定理，优先使用多个小型传递引理。

第 5 步：在 .mbt 中引导求解器

构造数据后，断言求解器可能遗漏的具体事实。

示例：

let data = FixedArray::make(1, value)
proof_assert data.length() == 1
proof_assert data[0] == value
let result = { bitmap, data }
proof_assert sparse_ok(result)
proof_assert singleton_post(result, idx, value)
result

使用 proof_assert：

• 在构造记录之后
• 在写入数组之后
• 在分情况讨论之后
• 在循环体建立更强的关系之后

优先使用这种方式，而不是引入可调用的受信任包装函数。

第 6 步：尽早编写循环不变量

任何与证明相关的循环，都应在循环结构稳定后尽早添加不变量。

在实践中，带证明的 MoonBit 代码通常会用循环来：

• 复制数组前缀或后缀
• 累计计数或秩
• 逐步构建结果结构
• 遍历子树或紧凑表示

不要等到证明器失败后才编写显而易见的不变量。

典型的不变量：

• 索引边界
• 累加器与抽象模型当前进度之间的关系
• 前缀/后缀复制事实
• 未更改字段的保留情况

示例：

for j = 0, acc = 0; j < idx; {
  let next_acc = if bitmap_mem(bitmap, j) { acc + 1 } else { acc }
  proof_assert next_acc == rank_value(bitmap, j + 1, 0)
  continue j + 1, next_acc
} nobreak {
  acc
} where {
  proof_invariant: 0 <= j,
  proof_invariant: j <= idx,
  proof_invariant: acc == rank_value(bitmap, j, 0),
}

对于数组更新，使用与证明结构相符的分阶段不变量。

示例：

for i = 0; i < pos; {
  new_data[i] = old_data[i]
  continue i + 1
} where {
  proof_invariant: 0 <= i,
  proof_invariant: i <= pos,
  proof_invariant: add_prefix_ok(old_data, new_data, pos, i),
}

在处理完插入/移除的元素后，再加强为第二个不变量。

默认规则：

• 如果循环有助于满足后置条件，其不变量应明确提及证明侧的进度
• 如果循环只修改具体状态，其不变量仍应说明后续抽象引理所需的具体关系
• 如果循环最终产生的值在语义上很重要，请添加 proof_yield，让证明器知道生成的结果满足什么条件

示例：

for i = 0, acc = 0; i < xs.length(); {
  continue i + 1, acc + xs[i]
} nobreak {
  acc
} where {
  proof_invariant: 0 <= i,
  proof_invariant: i <= xs.length(),
  proof_invariant: acc == prefix_sum(xs, i),
  proof_yield: res => res == prefix_sum(xs, xs.length()),
}

当证明需要关于整个循环表达式所产生值的事实，而不仅仅是迭代期间维持的状态时，使用 proof_yield。

第 7 步：验证自然的 API 表面

如果公共 API 以方法为主，请直接验证这些方法。

示例：

pub fn HashSet::contains(self : HashSet, key : Int) -> Bool where {
  proof_require: set_inv(self),
  proof_ensure: result => result == model(self).mem(key),
} {
  ...
}

只有在能改善结构或复用时，才使用顶层已验证辅助函数；不要将其作为规避方法契约的权宜之计。

第 8 步：递归代码采用结构化证明形式

对于递归数据结构：

• 定义语义视图，如 model(node) 或 elements(node)
• 定义形状不变量，如 node_ok(node, level)
• 按结构递归
• 添加 proof_decrease

示例：

fn contains_at(node : Node, key : Int, level : Int) -> Bool where {
  proof_decrease: node,
  proof_require: node_ok(node, level),
  proof_ensure: result => result == model(node).mem(key),
} {
  match node {
    Flat(k) => key == k
    Branch(children) => ...
  }
}

如果求解器难以处理带契约函数中的尾递归循环，请先尝试使用结构化递归代码。

步骤 9：对于打包或索引表示，先证明具体更新，再证明语义含义

当表示经过打包、建立索引或增量重建时，不要直接从底层变更跳到最终的语义定理。

先证明与实现结构相符的具体更新事实，再将它们与抽象模型关联起来。

常见的推进顺序如下：

1. 基本域或索引事实
2. 局部边界或位置事实
3. 未改变区域和已改变区域的具体更新事实
4. 完整的具体更新谓词
5. 最终的语义 *_post 定理

具体的中间谓词取决于实现。选择能反映代码实际阶段的名称。

典型阶段包括：

• 未改变区域
• 已更新区域
• 已移位或重建的区域
• 完整的具体更新谓词
• 最终语义后置条件

示例模式：

predicate update_prefix_ok(before_data, after_data, upto) { ... }
predicate update_middle_ok(before_data, after_data, pos, value, upto) { ... }
predicate update_data_ok(before, key, value, after) { ... }

lemma update_model_lemma(...) where {
  proof_require: update_data_ok(...),
  proof_ensure: update_post(...),
} {
  ...
}

对于稀疏或稠密数组代码，使用更具体的步骤序列（如 *_prefix_ok、*_fill_ok 和 *_data_ok）往往很有效，但应将其视为通用技术的一种实用示例，而非普遍适用的模板。

步骤 10：保持共享 Shim 包精简

如果你有可复用的证明导入项或理论，请将它们放入 Shim 包中。

典型示例：

• 有限集封装
• 有限映射封装
• 位图域、秩和计数辅助函数

这样做的好处是：

• 客户端包能保持专注
• 无需重复导入
• 更容易测试共享推理是否出现回归

但共享 Shim 应保持精简。大型共享引理集可能会扰动无关证明。

还要考虑降级处理的特殊情况：

• 方法可用于契约中，但静态构造函数可能不行
• 即使 Fmap::mk(...) 能解析，仍可能需要像 fmap_mk(...) 这样的自由函数封装
• 请将这些封装放在 Shim 包中，不要在每个客户端中重复定义

如果某个辅助函数只被一个包使用，优先在该包中编写局部引理，而不是从共享 Shim 导出。

步骤 11：将信任视为临时手段

可信辅助函数可以作为范围明确的桥接手段，但不应成为最终设计。

如果无法避免信任：

• 保持前置条件具体明确
• 只针对一个命名谓词
• 将数学陈述保留在 .mbtp 中

良好的临时桥接：

fn singleton_bridge(res : SparseArray, idx : Int, value : Int) -> Unit where {
  proof_axiomatized: true,
  proof_require: valid_idx(idx),
  proof_require: res.data.length() == 1,
  proof_require: res.data[0] == value,
  proof_ensure: singleton_ok(res, idx, value),
} {
  ()
}

然后按以下顺序移除可信桥接：

1. 构造函数
2. 观察函数
3. 更新函数
4. 原始机器字桥接

调试规则：先检查实际故障

证明失败后：

• 运行 moon prove <pkg>
• 检查 _build/verif/<pkg>/<pkg>.proof.json

编辑前先对问题进行分类：

• 缺少算术或索引事实
• 缺少语义桥接
• 量词实例化不当
• 新引理导致求解器受到扰动
• 前端／降级限制

不同原因需要不同的修复方法。

示例：

• 缺少索引事实 → 添加局部 proof_assert
• 缺少模型桥接 → 添加辅助引理或谓词
• 求解器受到扰动 → 将引理移出共享 Shim
• 降级限制 → 简化证明表面，或用更小的复现用例进行探查

常见的复现策略：

• 在一个微型探查包中隔离该结构
• 检查是 moon check 失败、moon prove 崩溃，还是 VC 仅仅超时
• 然后再判断问题出在建模、求解器引导还是编译器降级

回归纪律

每次修改证明后：

moon check <pkg>
moon prove <pkg>
moon test <pkg>   # if runtime code changed

修改共享证明层后，也要重新运行依赖包。

不要认为局部修复在全局范围内一定安全。

反模式

避免：

• 在每个客户端包中重复使用原始 #proof_import
• 使用大型内联契约公式，而不是命名谓词
• 一次性同时更改抽象设计和求解器引导
• 未先检查证明报告就添加许多辅助引理
• 只在可信 .mbt 函数中存放语义定理
• 明明顶层函数更简单，却优先验证方法
• 在单态的第一阶段证明更快时，过早引入泛型抽象

最简检查清单

移交已验证的 MoonBit 更改前，请确认：

• 存在语义明确的 model(...)，或者有充分理由使用 elements(...) 之类更具体的名称
• 存在 *_inv 谓词
• 合约在适当情况下提及命名的 *_pre / *_post 谓词
• 当抽象模型是集合／映射时，已显式处理外延相等性
• 特定于证明的逻辑主要位于 .mbtp 中
• 运行时代码在需要处包含局部 proof_assert
• 与证明相关的循环显式声明了 proof_invariant
• 可信边界明确且尽可能小
• 已运行 moon check、moon prove 以及所需的 moon test 命令