# Moon HistoryCheck 项目申报参考书

## 并发历史线性一致性检查与可验证反例证据

账号：123123213weqw。日期：2026 年 10 月 20 日。主要语言：MoonBit。许可：Apache-2.0。  
GitHub：https://github.com/123123213weqw/moon-historycheck  
公共模块：123123213weqw/moon_historycheck@0.7.0（已发布）（已发布）

本稿供个人参考，按实际实现编写。用户指定以本项目替换原 PolicyForge 申报；公开源码和发布记录不代表报名表替换已经完成，回执状态另附核对表。

## 一 项目目标与应用场景

HistoryCheck 检查一份并发操作历史能否解释为符合顺序规范、保留已知实时先后关系的串行执行。面向并发组件和存储服务测试，调用者提供输入、调用返回及观察输出，工具返回合法执行顺序、确定失败、未知或输入错误，并为失败提供可缩减、可重放和可独立检查的证据。

已实现寄存器与 CAS、独立键值寄存器、FIFO 队列、LIFO 栈、互斥锁、成员集合、整数计数器、键值映射、LWW 元素集合、单调 max 寄存器、只增集合、两阶段集合、min 寄存器、LWW 寄存器、有界队列、双端队列、计数信号量、读写锁、多重集合、优先队列、正负计数器与 LWW 映射二十四个顺序模型。项目没有把全文检索、规则求值或任务执行器改名复用为主体，也没有继承 FindCore 的源码、测试和提交历史。

## 二 已完成交付能力

| 能力 | 实际机制 | 输出及边界 |
|---|---|---|
| 历史校验 | 唯一身份、全局记录序号、调用返回配对、模型与选项检查 | 畸形输入报错，未完成调用返回未知 |
| 有界线性化搜索 | 前驱约束下搜索，记忆化包含已选集合和完整模型状态 | 找到顺序或穷尽；预算中断不算失败 |
| 成功见证验证 | 重新计算时序约束，检查全覆盖并逐步重放模型输出 | 拒绝遗漏、重复和不合法顺序 |
| 独立键分区 | kv_register 与 map 按键分解为子历史，合并局部顺序和全局实时边 | 完整见证再验证，不拆分事务 |
| 反例缩减 | 按连续块删除操作后重新求解，接受后细化粒度并重新扫描 | 有条件报告单操作删除的 1-minimal |
| 失败闭包证书 | 独立广度搜索构图，另一路核对每个合法分支和后继 | 检出遗漏分支、错误状态及绑定错误 |
| 使用入口 | MoonBit 公共库、Node 文件或标准输入 CLI、异步记录示例 | 判定、证据和退出状态可被脚本消费 |

## 三 核心工程机制

并发历史不能只按调用时间排序。写调用先发生但与读重叠时，读返回旧值可能合法；写已经返回后读才调用，才形成写必须先于读的约束。实现保留这种差别，搜索候选顺序，不把一条固定排序路径当作全部可能。

记忆键同时记录已选操作和模型状态。同一组操作采用不同写入顺序时可能留下不同值，只按操作集合剪枝会错误合并。当前采用完整规范化状态键，负面记忆表只收录完全穷尽的状态；候选操作按最早返回序号优先探索，与实时序一致的见证更早出现；状态数、条目数或字符串单位预算耗尽均返回未知。

成功见证验证入口不信任搜索前驱数组，而重新逐对计算必须先行关系并重放规范。失败证据则由另一条广度搜索构造有限状态图，证书验证器核对初始绑定、所有启用合法分支、后继状态和已选集合、节点可达性，以及不存在完成全部操作的终止节点。它是有限历史相对模型的运行时闭包证据，不是对检查器本身的形式化证明。

缩减同样遵守证据合同。未知不能证明一次删除有效；接受删除后，旧历史上的删除结论不能直接沿用。只有完成最终逐项检查，才报告单操作删除意义下的最小性，不将其称作全局最小反例。

## 四 可复现案例

examples/overlap.json 中，write(1) 区间为 [1,4]，返回 0 的 read 区间为 [2,3]。实现能找到 read、write 的顺序，报告 linearizable 并验证见证。

examples/stale.json 中，write(1) 在序号 2 完成，read 在 3 才调用但返回 0，报告 non_linearizable。将 operation 改为 certify 可生成有限闭包证书，再交给 verify_certificate；删除合法写分支会被拒绝。

examples/reduce.json 加入无关读取，缩减后仍保留写入和陈旧读取这对失败操作。examples/unknown.json 保留没有确定返回的写，报告 unknown，不假设该写没有生效。确定失败退出 2，未知退出 3，输入错误退出 64；这些属于结果协议。

## 五 验证与实际规模

当前有 39 项手写 MoonBit 测试和 120 项由固定 API 夹具生成的测试，共 159 项声明。同样 120 组夹具也经过真实 CLI，不重复计算为另一批独立功能。独立 Python 枚举对照覆盖 2280 份历史，另核对 240 次分区（kv_register 与 map 各 120 次）和 20 次缩减。有限闭包对照覆盖 360 份历史，其中 155 份负面证书、205 份成功见证，并检查篡改拒绝。oracle 已重构为按模型列表驱动，新增模型成为纯追加。

规模入口涵盖 256 操作串行历史、100 个独立键的 200 操作历史，以及 13 路重叠下的预算截断与记忆化命中。串行规模与高重叠搜索分开说明，不宣称任意高并发历史都能快速完成。

scripts/stats.py 当前统计：自有生产有效行 1,551 行，排除共同值类型、扩展声明和 CLI 后的领域实现为 1,313 行。依赖、测试、生成夹具和文档不计生产代码；这不是 4,000 行以上成果，也不以重复代码增加数量。公共 CI、源码 SHA、安装和校验和以最终交付核对表记录，不以命令列表代替实际结果。

## 六 使用与验收

使用者添加公共模块后调用 execute(Json)，或构建 JS CLI 输入示例。scripts/record-demo.mjs 实际发起异步调用、分配统一序号，分别运行正确与受控陈旧读实现，保存历史和报告。该演示不作为生产数据库采用证据。

复核入口包含四后端测试、CLI 夹具、独立枚举、独立闭包遍历、规模检查和异步记录场景。核心求解由 MoonBit 完成；Python 仅用于独立参考，Node 负责文件和演示宿主，没有用外部 Go 检查器替代内核。

## 七 当前边界与来源

只判断给定有限历史。记录必须有可信统一顺序，不能使用未校准的跨机器墙钟推断先后。未完成调用保留为未知。模型值采用有限 Double 和结构 JSON 相等，不提供任意精度数值。历史最多 256 操作，高重叠可能耗尽资源；预算不是完整堆内存或墙钟时限。现版本不支持事务和任意可执行模型插件。

问题定义参考 [Porcupine](https://github.com/anishathalye/porcupine)，分解思想参考 [P-compositionality 论文](https://arxiv.org/abs/1504.00204)。未复制其源码或测试数据，不主张算法首创；本次未执行 Porcupine 性能或行为差分。MoonBit 生态已有 MoonRaft 等相关项目，不主张未经证实的生态空白。共同基础代码和 AI 编程辅助见 THIRD_PARTY.md。

本项目提供可运行工具和明确边界。有效工作量、创新性与替换申报资格仍由组委会审核，公开发布本身不是审核通过的证明。