# 归约与重放验证报告

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

## 目标、输入与方法

演示入口为 [`modules/cli/src/examples/reduction/main.mbt`](<https://github.com/zrr1999/moonsmith/blob/main/modules/cli/src/examples/reduction/main.mbt>)，调用现有库入口。它以显式种子 7 和最多 16 个候选运行归约。初始程序来自[固定归约输入](<https://github.com/zrr1999/moonsmith/blob/main/cases/moonbit/reduce-root-call/main.mbt>)，生成规则为 `template-rules-v1`，预算为 128 个节点、深度 6、256 次构造尝试。

| 环境条件 | 实测值 |
| --- | --- |
| 宿主 | Darwin 27.0.0 arm64 |
| Moon / moonrun | `0.1.20260920`，提交 `914d7da` |
| 编译器与 core | `0.10.14+7d59c7ec9` |
| 执行配置 | native-debug、native-release、wasm-gc-debug |
| 每次编译 / 执行超时 | 30000 / 2000 毫秒 |

从仓库根目录运行：

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

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

## 预期与实测结果

| 指标 | 实测结果 |
| --- | --- |
| 语言模型节点 | 128 → 1；移除 127 个，约 99.2% |
| 整数常量绝对值之和 | 21474836510 → 0 |
| 源码 UTF-8 字节数 | 1193 → 29 |
| 提交 / 接受候选 | 2 / 2；候选上限 16 |
| 搜索停止 | 当前候选枚举完成 |
| 独立确认 | 新执行保持指定配置对的分歧 |
| 确认源码重放 | 另一次新执行再次观察到目标分歧 |
| 搜索与独立确认耗时 | 3419 毫秒，Host 单调时钟 |

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

```moonbit
fn main {
  println(false)
}
```

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

## 结论与边界

这次演示中，归约、独立确认和源码重放都保持了注入的配置对输出差异；搜索仅遍历所述候选，未验证全局最小性。真实工具链历史案例见[历史回归报告](<https://docs.moonsmith.zrr.dev/historical-regressions/index.md>)；案例与尝试的保存格式及重放行为见[CLI 差分执行与存证说明](<https://github.com/zrr1999/moonsmith/blob/main/modules/cli/README.md#差分执行与存证>)。

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

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

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

| 项目 | 产品自动归约结果 |
| --- | --- |
| 节点 | 128 → 117 |
| 源码 UTF-8 字节数 | 1273 → 1147 |
| 提交 / 接受候选 | 16 / 2 |
| 停止原因 | 候选预算耗尽 |
| 独立确认 | 重新执行最佳源码，保持相同构建异常及有效控制结果 |

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

[189 字节同模式小复现](<https://docs.moonsmith.zrr.dev/native-release-analysis/#189-字节的同模式小复现>)来自人工整理， 并非上述 16 个候选的产品自动归约结果。该调查的 236 个结构化候选、进一步人工修改和阶段实验 保留在历史材料中；它们与本次产品默认预算的结果分别报告。