# 分析设计与证据边界

本文描述兼容分析核心；v0.1.0 推荐入口、优化搜索与 v2 证据见 [高级约定](balanced-profile.md)。

## 从观察到依赖

图顶点为已提交事务，操作下标从 0 开始。边保留事务 ID、类型、键、两个操作下标、版本与依据，以便定位原日志。

| 边 | 依据 | 强制次序 |
| --- | --- | --- |
| WR | 读到其他已提交事务的唯一最终版本 | 写者 → 读者 |
| WW | 输入同键顺序中相邻最终写入 | 较早写者 → 较晚写者 |
| RW | 外部/初始读版本早于某个已提交最终写入 | 读者 → 后续写者 |
| RT | 共同观察时钟中 A.end < B.start | A → B |

RW 指向全部已知较晚最终写者；WW 相邻边表达全顺序。即使缺少写者之间的顺序，读初始版本也必须早于全部已提交写者。读取自己的最新写入不生成外部依赖。直接异常包括读取回滚/外部中间版本和自身操作矛盾。

有完整版本约束、没有直接异常和信息缺失时，图无环的拓扑顺序是可行串行执行。已知环足以证明这些必要约束矛盾。来源未记录的读取可能来自日志窗口之外，返回无法判定，不直接判作凭空生成数据。

## 缺失顺序的有预算精确搜索

仅当没有既有异常、其他信息完整、未解决项全为 missing_version_order 时，最多对 8 个已提交事务的整个事务执行进行回溯。每次候选满足已有图依赖，并重放事务内部操作；读取必须等于该时刻的最新版本。输入已有的版本顺序仍作为约束。

- 找到执行：返回 consistent、可重放的 serialOrder，以及来源为 searched 的可能版本顺序。
- 所有允许前缀搜索完且无解：返回 violation / no_serial_execution；图可能无环，因此不伪造环证据。
- 超过规模或搜索预算：保留 inconclusive，不把“未找到”当作“没有”。
- 有未知结果、未知读来源或严格模型缺时间：不通过搜索补造这些事实。

限 512 操作、128 初始键、100,000 次候选前缀和 1,000,000 次操作检查。search.blockers 仅记录最多 32 个候选读冲突示例，不能单独作为全称证明。完整负面结论可通过 replay 重新运行搜索复现。

## 最短环与定位

v0.0.6 先用 Tarjan 分解强连通分量，再仅在含环分量内作广度优先搜索。跨分量边不能在环中；跳过无环区域保留全图最短有向简单环。并列时按稳定遍历顺序选择一个，二事务环可提前结束。

复杂度为 SCC 的 O(V+E)，加含环分量内的 BFS；最坏仍为 O(V×(V+E))。最短按边数/事务数定义，仅针对预算内实际构建的图；不是全部异常或全局最小日志。graph 报告分量数、含环事务数、BFS 起点数和边预算状态。SCC 不保证端到端耗时优于旧版，实测记录保留真实结果。

coverage 统计逐键已提交读、最终写、未知来源读；versionOrderSources 明确 asserted、single-writer、searched、missing。人类报告用中文说明依据与下一步采集需求。诊断建议不改变确定性结论。

## 反例缩减

reduce_history 先块删除，再单事务删除，固定初始状态和剩余事务内部操作。删除事务后只裁剪原输入声明的版本顺序，不把搜索补全转成输入事实。候选必须再次产生确定 violation 才接受。

最多 64 原事务、2,048 操作、128 检查。oneMinimal 只有完成最后单删扫描才为 true；它是当前分析器异常谓词下的一最小事务集合，不是全局最少事务或操作最小化。预算用尽时保留已验证反例并明确未完成。

## 环证据与语义回放

verify 重新推导依赖，检查工具、支持版本、schema、模型、异常状态、完整边来源、事务路径及闭合。支持本项目 schema 1 的 0.0.1–0.0.6。为兼容旧证据，JSON 边的稳定解释字段保留。复核不调用 SCC/最短环搜索，不能验证最短性或报告其他字段。

replay 首先验证自包含包结构及存储文本 UTF-8 的 SHA-256，然后重新分析历史，比较状态、模型、完整性、统计、发现、依赖、环、串行/版本顺序，及存在的搜索与版本来源字段。因此可复现无环直接异常、完整搜索无解和正常判断。

语义复核不认证展示补充字段、来源身份或日志采集真实性；SHA-256 不是签名。cycle verify 与生产推导共享规则；独立正确性证据来自测试中的全事务串行重放 oracle 与 DFS，而非哈希。

## 模块职责

| 模块 | 责任 |
| --- | --- |
| types.mbt | 输入、依赖、搜索、诊断、结果类型 |
| json_guard.mbt / parse.mbt | 深度、重复键、结构与语义校验 |
| analyze.mbt | 写来源、顺序、依赖与直接异常 |
| search.mbt | 有预算的精确串行重放 |
| graph.mbt | SCC、最短环、拓扑顺序 |
| reduce.mbt | 事务反例缩减 |
| diagnostics.mbt | 逐键覆盖及来源缺口 |
| report.mbt / render.mbt | 报告及环复核 |
| replay.mbt | 语义复现、包结构、模型对比 |
| bridge/ | MoonBit JavaScript 导出 |
| cmd/ | 有界本地 I/O、哈希、CLI、SDK、演示 |
| scripts/oracle.mjs | 独立串行重放、DFS 和缩减核对 |

核心无数据库或网络依赖，使用 MoonBit core/json。CLI 拒绝覆盖现有文件，导出失败只清理本次新建配套文件。SQLite 示例是独立的实际执行采集器，不是核心分析器内置 SQL 插桩。没有后台服务或遥测。