# 历史格式 v1

历史输入格式保持兼容；文中 8 事务搜索预算属于旧入口，balanced 补全为 12 个已提交事务，见 [高级约定](balanced-profile.md)。

根对象只接受 `schemaVersion`、`name`、`model`、`initial`、`versionOrders`、`transactions`。未知字段、重复 JSON 键（包括转义后相同的键）、不合法 JSON 会被拒绝。`schemaVersion` 默认 1，`model` 默认 `serializable`，`name` 是可选描述，不参与分析。

## 版本和操作

`initial` 是键到初始版本字符串的映射，涵盖全部操作中的键。操作仅为 `read` 或 `write`，使用 `type`、`key`、`version` 三个字段。读操作记录实际观察到的版本，写操作记录分配给这次写入的版本。

事务 ID、键和版本均须非空，最多 256 个 UTF-16 单元，禁止 C0 控制字符及 DEL。事务 ID 全局唯一；`(key, version)` 写入标记在全部事务、全部状态间唯一，不可重复使用该键的初始版本。不同键可使用相同版本字符串。业务值不是版本 ID。

`ops` 数组严格保留事务内部发生顺序。事务可以写同一键多次，只有最后一次是该事务对该键的最终写入。自身读可观察自己刚写入的中间版本；其他已提交事务不能读取这一中间版本。

## 提交结果

每个事务须提供 `id`、`status`、`ops`。`status` 可为：

- `committed`：参与串行顺序、依赖图和读写异常检查。
- `aborted`：其写入可用于识别已提交事务的回滚数据读取；其自身读不作已提交历史的保证。
- `unknown`：保留其写入来源，报告提交状态缺失；不纳入已提交图。

事务之间在输入数组中的顺序没有因果意义。空事务合法。本模型检查已提交事务，不是所有回滚或执行中事务的 opacity 检查器。

## 同键写入顺序

`versionOrders` 可省略或只提供一部分键。一个键的顺序必须：

1. 首项为该键初始版本。
2. 后续项覆盖每个已提交事务在该键上的最终写入，恰好一次。
3. 不含外部版本、回滚/未知结果的写入或被自身后续写入覆盖的中间版本。

顺序是输入提供的可信约束，例如专门采集的版本链。它不是工具推断的数据库序列化顺序。错误但形式合法的顺序也可能产生异常证据，因此报告始终以“提供的历史和版本约束”为范围。

未提供顺序时，0 个或 1 个已提交最终写入的键可以推断顺序；多写者键先记录 `missing_version_order`。v0.0.2 起，在没有其他信息缺失或既有异常的小历史中执行精确串行重放搜索：找到执行则返回正常及可能顺序；完整搜索无解则返回确定异常；超过预算仍为无法判定。

报告的 `versionOrderSources` 区分 `asserted`（输入提供）、`single-writer`（0/1 写者可推断）、`searched`（可能执行的补全）、`missing`。`searched` 不是数据库观测事实。搜索尊重已有输入顺序，不能补造未知提交结果、未知读来源或缺失时间。

搜索只处理最多 8 个已提交事务、512 操作、128 个初始键，最多尝试 100,000 个候选前缀和 1,000,000 次操作检查。穷举无解可能没有依赖环，使用自包含复现包回放完整结论，而不是导出虚构的环。

## 严格模型的时间

`start`、`end` 是可选的非负整数或 `null`，最大值为 9,007,199,254,740,991，均提供时要求 `start <= end`。单位自选，但必须来自**同一单调观察时钟**。通常分别采集于事务开始调用之前和提交结果返回之后。

`strict-serializable` 对每个已提交事务要求完整时间区间，否则返回 `missing_interval`。当 A 的 `end <` B 的 `start` 时加入 A → B 的 RT 边。相同时间刻度不证明先后，重叠区间不加入 RT 边。`serializable` 不使用区间决定事务间次序。

多台机器上未经同步保证的墙上时间不能直接作为此共同观察时钟。

## 输入预算

| 项目 | 上限 | 超限处理 |
| --- | --- | --- |
| 事务 | 512 | 输入无效 |
| 操作总数 | 10,000 | 输入无效 |
| 解析字符 | 1,048,576 UTF-16 单元 | 输入无效 |
| CLI 历史文件 | 2 MiB UTF-8 | 退出码 2 |
| JSON 嵌套 | 64 层 | 输入无效 |
| 图依赖 | 50,000 | 标记截断；无证据时无法判定 |
| CLI 证据文件 | 32 MiB UTF-8 | 退出码 2 |

JSON Schema 用于编辑器的结构提示。事务 ID 唯一性、跨操作版本唯一性、UTF-16 长度、总操作预算和版本顺序完整性由 MoonBit 核心作进一步验证，不能仅凭 Schema 校验通过认为日志有效。