moonbit-proof

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

MoonBit Proof-Carrying Code

Use this skill when the task is to write, extend, or debug verified MoonBit code.

Typical triggers:

add contracts to executable MoonBit code
define an abstract model or representation invariant
verify a recursive data structure
connect a concrete representation to a set/map model
replace trusted proof bridges with lemmas
debug proof failures, timeouts, or frontend lowering limits

当你需要编写、扩展或调试经过验证的MoonBit代码时，可以使用本技能。

典型触发场景：

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

Goal

目标

Write proof-carrying code, not proof-shaped comments.

That means:

the runtime code remains executable and readable
the proof model is explicit
contracts talk about named predicates/functions with consistent roles
local
```
proof_assert
```
steps explain why the implementation satisfies the model

编写带证明的代码，而非形似证明的注释。

这意味着：

运行时代码保持可执行性和可读性
证明模型清晰明确
契约围绕具有一致角色的命名谓词/函数展开
局部
```
proof_assert
```
步骤解释实现为何符合模型

Naming

命名规则

Prefer

model(...)

as the default name for the proof-side semantic view of a value.

Examples:

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

Use a more specific name only when it is materially clearer:

```
elements(node)
```
when the model is literally the set of elements stored in a recursive subtree
```
domain(bitmap)
```
when the model is specifically the occupied index set
```
height(tree)
```
when it is a structural measure, not the main semantic model

Default rule:

use
```
model
```
for the main semantic abstraction
use specialized names like
```
elements
```
,
```
domain
```
,
```
height
```
, or
```
rank
```
for auxiliary views

默认优先使用

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
```
等专用名称

Default Structure

默认结构

Split the package into two layers.

```
.mbtp
```
- model functions such as
```
model(x)
```
- representation invariants such as
```
tree_inv(x)
```
  or
```
sparse_array_inv(x)
```
- named proof predicates such as
```
insert_pre(...)
```
  and
```
insert_post(...)
```
- reusable lemmas
```
.mbt
```
- executable code
- contracts over the proof-side predicates
- local
```
proof_assert
```
  steps after construction, branching, and loops

Use this default unless there is a strong reason not to.

将包拆分为两层。

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

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

Recommended Workflow

Step 1: Pick the Right Abstract Model

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

Prefer the simplest model that matches the observable behavior.

Membership-only structure: use a finite set.
Key-value structure: use a finite map.
Recursive tree/trie: use
```
model(node)
```
or, if clearer,
```
elements(node)
```
.
Packed layout: separate domain/layout facts from semantic meaning.

Example:

moonbit

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

If a recursive helper really denotes the element set of a subtree, this is also reasonable:

moonbit

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

Avoid putting the whole semantics directly into every contract.

优先选择与可观察行为匹配的最简模型。

仅需成员关系的结构：使用有限集合。
键值结构：使用有限映射。
递归树/前缀树：使用
```
model(node)
```
，若更清晰则使用
```
elements(node)
```
。
紧凑布局：将域/布局事实与语义含义分离。

示例：

moonbit

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

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

moonbit

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

避免将整个语义直接写入每个契约。

Step 2: Keep the Invariant Small

步骤2：保持不变量精简

The invariant should mostly describe:

shape
bounds
layout
well-formedness

Semantic equalities usually belong in postconditions or lemmas, not inside

*_inv

Good:

moonbit

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())
}

Not good:

putting every update theorem into the invariant
encoding the entire semantic equality into
```
*_inv
```

不变量应主要描述：

形状
边界
布局
良构性

语义等式通常属于后置条件或引理，而非

*_inv

内部。

良好示例：

moonbit

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
```
中

Step 3: Use Named Postconditions

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

Prefer named predicates over repeating large formulas. As a default naming convention, use

*_inv

*_pre

, and

*_post

Good:

moonbit

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),
} {
  ...
}

This keeps contracts short and gives the solver a reusable target.

优先使用命名谓词，而非重复大型公式。默认命名约定为

*_inv

、

*_pre

和

*_post

。

良好示例：

moonbit

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),
} {
  ...
}

这能保持契约简洁，并为求解器提供可复用的目标。

Step 4: Put the Math in

.mbtp

步骤4：将数学逻辑放入

.mbtp

Proof-side material belongs in

.mbtp

Examples:

moonbit

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))
  }
}

Keep

.mbtp

focused on:

logic definitions
predicates
lemmas

Avoid filling

.mbtp

with runtime implementation details.

Two recurring helper patterns are especially useful:

Extensional equality hypotheses for abstract structures.

Example:

moonbit

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),
} {
}

This is often the cleanest way to finish map-refinement proofs.

Small transport lemmas for updates.

Examples:

add/remove
```
mem
```
at self and other keys
add/remove
```
find
```
at self and other keys
set cardinality after adding/removing an absent/present element

Prefer several small transport lemmas over one giant “everything changed correctly” theorem.

证明侧内容应放在

.mbtp

中。

示例：

moonbit

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

中填充运行时实现细节。

有两种反复出现的辅助模式特别有用：

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

示例：

moonbit

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),
} {
}

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

用于更新的小型传输引理。

示例：

添加/移除自身及其他键的
```
mem
```
属性
添加/移除自身及其他键的
```
find
```
属性
添加/移除不存在/存在元素后的集合基数

优先使用多个小型传输引理，而非一个包含所有变更的巨型定理。

Step 5: Guide the Solver in

.mbt

步骤5：在

.mbt

中引导求解器

After constructing data, assert the concrete facts the solver may miss.

Example:

moonbit

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

Use

proof_assert

after record construction
after array writes
after case splits
after loop bodies establish a stronger relation

Prefer this over introducing a callable trusted wrapper function.

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

示例：

moonbit

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

：

记录构造后
数组写入后
分支判断后
循环体建立更强关系后

优先使用此方式，而非引入可调用的可信包装函数。

Step 6: Write Loop Invariants Early

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

Any loop that is relevant to the proof should get invariants as soon as the loop shape stabilizes.

In practice, proof-carrying MoonBit code often relies on loops for:

copying array prefixes or suffixes
accumulating counts or ranks
building a result structure incrementally
iterating over a subtree or packed representation

Do not wait for the prover to fail before writing the obvious invariants.

Typical invariants:

index bounds
relationship between the accumulator and the abstract model so far
prefix/suffix copy facts
preservation of unchanged fields

Example:

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 array updates, use staged invariants that match the proof shape.

Example:

moonbit

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),
}

Then strengthen to a second invariant after the inserted/removed element is handled.

Default rule:

if a loop contributes to a postcondition, its invariant should mention the proof-side progress explicitly
if a loop only mutates concrete state, the invariant should still state the concrete relation needed by the next abstraction lemma
if the loop's final yielded value matters semantically, add
```
proof_yield
```
so the prover knows what the yielded result satisfies

Example:

moonbit

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()),
}

Use

proof_yield

when the proof needs a fact about the value produced by the whole loop expression, not just the state maintained during iteration.

任何与证明相关的循环，应在循环形状稳定后立即添加不变量。

实际上，带证明的MoonBit代码通常依赖循环完成以下任务：

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

不要等到 prover 失败后才编写明显的不变量。

典型不变量：

索引边界
累加器与当前抽象模型的关系
前缀/后缀复制事实
未变更字段的保留

示例：

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),
}

对于数组更新，使用与证明形状匹配的分阶段不变量。

示例：

moonbit

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
```
以便 prover 知道返回结果满足的条件

示例：

moonbit

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

。

Step 7: Verify the Natural API Surface

步骤7：验证自然API表面

If the public API is method-oriented, verify the methods directly.

Example:

moonbit

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

Use top-level verified helper functions only when they improve structure or reuse, not as a workaround for method contracts.

如果公共API是面向方法的，直接验证方法。

示例：

moonbit

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

仅当能改善结构或复用性时，才使用顶层已验证辅助函数，而非作为方法契约的变通方案。

Step 8: Use Structural Proof Shape for Recursive Code

步骤8：为递归代码使用结构化证明形状

For recursive data structures:

define a semantic view like
```
model(node)
```
or
```
elements(node)
```
define a shape invariant like
```
node_ok(node, level)
```
recurse structurally
add
```
proof_decrease
```

Example:

moonbit

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) => ...
  }
}

If the solver resists tail-recursive loops in contracted functions, try structurally recursive code first.

对于递归数据结构：

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

示例：

moonbit

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) => ...
  }
}

如果求解器在带契约的函数中抗拒尾递归循环，先尝试结构化递归代码。

Step 9: For Packed or Indexed Representations, Prove Concrete Updates Before Semantic Meaning

步骤9：对于紧凑或索引表示，先证明具体更新再处理语义含义

When a representation is packed, indexed, or incrementally rebuilt, do not jump straight from low-level mutation to the final semantic theorem.

First prove concrete update facts that match the implementation structure, then connect them to the abstract model.

A common progression is:

basic domain or indexing facts
local bounds or position facts
concrete update facts for unchanged and changed regions
a full concrete-update predicate
the final semantic
```
*_post
```
theorem

The exact intermediate predicates depend on the implementation. Choose names that reflect the actual stages in the code.

Typical stages are:

unchanged region
updated region
shifted or rebuilt region
full concrete-update predicate
final semantic postcondition

Example pattern:

moonbit

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(...),
} {
  ...
}

For sparse or dense-array code, a more specific ladder like

*_prefix_ok

*_fill_ok

, and

*_data_ok

is often effective, but treat that as one useful instance of the general technique rather than a universal template.

当表示是紧凑、索引或逐步重建的，不要直接从低级突变跳到最终语义定理。

先证明与实现结构匹配的具体更新事实，再将其与抽象模型关联。

常见步骤：

基本域或索引事实
局部边界或位置事实
未变更和变更区域的具体更新事实
完整的具体更新谓词
最终语义
```
*_post
```
定理

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

典型阶段：

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

示例模式：

moonbit

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

这样更具体的阶梯式结构通常有效，但应将其视为通用技术的一个有用实例，而非通用模板。

Step 10: Keep Shared Shim Packages Small

步骤10：保持共享垫片包精简

If you have reusable proof imports or theories, put them in shim packages.

Typical examples:

finite-set wrappers
finite-map wrappers
bitmap domain/rank/count helpers

The benefit is:

client packages stay focused
imports are not duplicated
shared reasoning is easier to test for regressions

But keep shared shims minimal. Large shared lemma sets can perturb unrelated proofs.

Also account for lowering quirks:

methods may work in contracts while static constructors do not
a free wrapper like
```
fmap_mk(...)
```
may still be needed even if
```
Fmap::mk(...)
```
parses
keep those wrappers in the shim package, not duplicated in every client

If a helper is only needed by one package, prefer a local lemma there rather than exporting it from a shared shim.

如果有可复用的证明导入或理论，将其放入垫片包。

典型示例：

有限集合包装器
有限映射包装器
位图域/排名/计数辅助函数

好处是：

客户端包保持专注
导入不会重复
共享推理更容易测试回归

但要保持共享垫片最小化。大型共享引理集可能干扰无关证明。

同时考虑降级 quirks：

方法可能在契约中有效，而静态构造器不行
即使
```
Fmap::mk(...)
```
能解析，仍可能需要
```
fmap_mk(...)
```
这样的自由包装器
将这些包装器放在垫片包中，不要在每个客户端重复

如果某个辅助函数仅被一个包需要，优先在该包中使用局部引理，而非从共享垫片导出。

Step 11: Treat Trust as Temporary

步骤11：将信任视为临时状态

Trusted helpers are acceptable as narrow bridges, but they should not be the design endpoint.

If trust is unavoidable:

keep preconditions concrete
target one named predicate
keep the mathematical statement in
```
.mbtp
```

Good temporary bridge:

moonbit

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),
} {
  ()
}

Then remove trusted bridges in this order:

constructors
observers
update functions
primitive machine-word bridges

可信辅助函数可作为窄桥使用，但不应是设计终点。

如果信任不可避免：

保持前置条件具体
针对一个命名谓词
将数学声明放在
```
.mbtp
```
中

良好的临时桥：

moonbit

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),
} {
  ()
}

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

构造器
观察器
更新函数
原始机器字桥

Debugging Rule: Inspect the Actual Failure First

调试规则：先检查实际失败原因

After a proof failure:

run
```
moon prove <pkg>
```
inspect
```
_build/verif/<pkg>/<pkg>.proof.json
```

Classify the problem before editing:

missing arithmetic/index fact
missing semantic bridge
bad quantifier instantiation
solver perturbation from a new lemma
frontend/lowering limitation

Different causes need different fixes.

Examples:

missing index fact → add a local
```
proof_assert
```
missing model bridge → add a helper lemma or predicate
solver perturbation → move a lemma out of a shared shim
lowering limitation → simplify the proof surface or probe a smaller reproducer

Common reproducer strategy:

isolate the construct in a tiny probe package
check whether
```
moon check
```
fails,
```
moon prove
```
crashes, or the VC merely times out
only then decide whether the issue is modeling, solver guidance, or compiler lowering

证明失败后：

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

在编辑前分类问题：

缺失算术/索引事实
缺失语义桥
量词实例化错误
新引理导致的求解器干扰
前端/降级限制

不同原因需要不同修复。

示例：

缺失索引事实 → 添加局部
```
proof_assert
```
缺失模型桥 → 添加辅助引理或谓词
求解器干扰 → 将引理移出共享垫片
降级限制 → 简化证明表面或探索更小的复现用例

常见复现策略：

将构造隔离到一个小型测试包中
检查
```
moon check
```
是否失败、
```
moon prove
```
是否崩溃，或验证条件是否仅超时
然后再决定问题是建模、求解器引导还是编译器降级导致的

Regression Discipline

回归规范

After every proof edit:

text

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

After editing shared proof layers, rerun dependent packages too.

Do not assume a local fix is safe globally.

每次编辑证明后：

text

moon check <pkg>
moon prove <pkg>
moon test <pkg>   # 如果运行时代码有变更

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

不要假设局部修复在全局是安全的。

Anti-Patterns

反模式

Avoid:

repeating raw
```
#proof_import
```
in every client package
large inline contract formulas instead of named predicates
changing abstraction design and solver guidance in one step
adding many helper lemmas without checking the proof report first
storing semantic theorems only in trusted
```
.mbt
```
functions
verifying methods first when top-level functions would be simpler
introducing generic abstractions too early when a monomorphic first slice will prove faster

避免：

在每个客户端包中重复原始
```
#proof_import
```
使用大型内联契约公式而非命名谓词
一步更改抽象设计和求解器引导
在检查证明报告前添加大量辅助引理
仅在可信
```
.mbt
```
函数中存储语义定理
当初始顶层函数更简单时先验证方法
当单态初始切片能更快完成证明时过早引入泛型抽象

Minimal Checklist

最小检查清单

Before handing off a verified MoonBit change, confirm:

a semantic
```
model(...)
```
exists, or there is a clear reason to use a more specific name like
```
elements(...)
```
a
```
*_inv
```
predicate exists
contracts mention named
```
*_pre
```
/
```
*_post
```
predicates when appropriate
extensional equality is handled explicitly when the abstract model is a set/map
proof-specific logic is mostly in
```
.mbtp
```
runtime code has local
```
proof_assert
```
where needed
proof-relevant loops have explicit
```
proof_invariant
```
the trusted surface is explicit and as small as possible
```
moon check
```
,
```
moon prove
```
, and any needed
```
moon test
```
commands were run

在交付已验证的MoonBit变更前，确认：

存在语义
```
model(...)
```
，或有明确理由使用更具体的名称如
```
elements(...)
```
存在
```
*_inv
```
谓词
契约在适当情况下提及命名的
```
*_pre
```
/
```
*_post
```
谓词
当抽象模型是集合/映射时，显式处理外延相等
证明特定逻辑大多在
```
.mbtp
```
中
运行时代码在需要的地方有局部
```
proof_assert
```
与证明相关的循环有明确的
```
proof_invariant
```
可信表面明确且尽可能小
已运行
```
moon check
```
、
```
moon prove
```
及任何需要的
```
moon test
```
命令

moonbit-proof

Original

Translation

MoonBit Proof-Carrying Code

MoonBit Proof-Carrying Code

Goal

目标

Naming

命名规则

Default Structure

默认结构

Recommended Workflow

推荐工作流程

Step 1: Pick the Right Abstract Model

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

Step 2: Keep the Invariant Small

步骤2：保持不变量精简

Step 3: Use Named Postconditions

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

Step 4: Put the Math in .mbtp

步骤4：将数学逻辑放入.mbtp

Step 5: Guide the Solver in .mbt

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

Step 6: Write Loop Invariants Early

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

Step 7: Verify the Natural API Surface

步骤7：验证自然API表面

Step 8: Use Structural Proof Shape for Recursive Code

步骤8：为递归代码使用结构化证明形状

Step 9: For Packed or Indexed Representations, Prove Concrete Updates Before Semantic Meaning

步骤9：对于紧凑或索引表示，先证明具体更新再处理语义含义

Step 10: Keep Shared Shim Packages Small

步骤10：保持共享垫片包精简

Step 11: Treat Trust as Temporary

步骤11：将信任视为临时状态

Debugging Rule: Inspect the Actual Failure First

调试规则：先检查实际失败原因

Regression Discipline

回归规范

Anti-Patterns

反模式

Minimal Checklist

最小检查清单

Step 4: Put the Math in
`.mbtp`

步骤4：将数学逻辑放入
`.mbtp`

Step 5: Guide the Solver in
`.mbt`

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