归约与重放验证报告¶

2026-10-21 使用真实 MoonBit 工具链执行一次受控故障注入归约与重放，通过注入的输出差异验证归约流程能否保持指定配置对的分歧。

目标、输入与方法¶

演示入口为 modules/cli/src/examples/reduction/main.mbt，调用现有库入口。它以显式种子 7 和最多 16 个候选运行归约。初始程序来自固定归约输入，生成规则为 template-rules-v1，预算为 128 个节点、深度 6、256 次构造尝试。

从仓库根目录运行：

moon run modules/cli/src/examples/reduction --target native --deny-warn

工具链实际编译和执行候选程序。注入步骤将保存给比较器的 native-release 规范结果改为另一个同类型值，从而与 native-debug 形成指定输出分歧；原始 stdout 单独保留。归约会话固定此配置对。每个候选、独立确认与源码重放都会重新执行程序并取得相应注入证据。其他配置对的差异、编译拒绝或超时不能替代目标差异。

预期与实测结果¶

本流程预期候选继续满足指定的目标差异；实测接受 2 个候选，独立确认和重放均再次满足该条件。归约结果源码为：

fn main {
  println(false)
}

3419 毫秒包括候选搜索、独立确认及相应存证，不含原始执行、归约摘要保存或后续重放。该值是一次受工具链、系统负载与文件缓存影响的观测，不用于算法性能比较。

结论与边界¶

这次演示中，归约、独立确认和源码重放都保持了注入的配置对输出差异；搜索仅遍历所述候选，未验证全局最小性。真实工具链历史案例见历史回归报告；案例与尝试的保存格式及重放行为见CLI 差分执行与存证说明。

真实构建异常的产品演示¶

0.0.1 的发行准备使用种子 1272 和默认 16 个候选，执行当前产品的真实构建异常归约。 五配置为 native debug、native release、wasm-gc debug、wasm debug 和 js debug；没有注入输出。 在被测编译器与 core 0.10.18+6c83a7f62 下，macOS arm64 上仍观察到 native release 构造器未声明诊断。其余四配置正常输出一致，原始比较保持 Incomplete，退出码为 3。

moonsmith run --set seed_start=1272 --set sample_count=1 \
  --set 'execution.configurations=["native-debug","native-release","wasm-gc-debug","wasm-debug","js-debug"]'

发布准备还分别用新工具链和固定旧版 0.10.14+7d59c7ec9 执行三例，材料按编译器分开保存。 最新构建身份、逐候选观察、独立确认和重放结果以平台证据包为准。 归约摘要中的确认尝试目录可以直接传给 moonsmith replay；重放追加执行，不再归约。

189 字节同模式小复现来自人工整理， 并非上述 16 个候选的产品自动归约结果。该调查的 236 个结构化候选、进一步人工修改和阶段实验 保留在历史材料中；它们与本次产品默认预算的结果分别报告。