# RFC-0001：性质与验证计划

| 项目 | 值 |
|---|---|
| 规范 | [RFC-0001](0001-async-mailbox-and-memory-sync.md) |
| 状态 | 实现前的验证契约，尚无测试代码或已通过声明 |
| 方法 | 基于模型的性质测试、接口契约、可控故障、Skill 场景评测 |
| 观察边界 | 公开领域操作与同语义的 MCP / HTTP 接口 |

## 1. 预先约定的测试边界

| 边界 | 验证什么 | 不通过什么推断 |
|---|---|---|
| 公开服务操作 | send、read、ACK、status、memory publish/read 的状态语义 | 私有 helper 的返回值 |
| 持久存储适配 | Blob 可读、发布原子性、CAS 与重启恢复 | 内存 mock 已成功就视作生产可靠 |
| 传输适配 | 两个入口的 schema、错误、授权与幂等一致 | JSON 格式匹配就代表业务成立 |
| 消费者持久队列 | 先保存再 ACK，处理可恢复 | 服务能证明任意客户端已写盘 |
| Skill | 实际工具调用、参数、回执报告与授权范围 | 固定文字或单一回复快照 |

测试通过公开 read/status/Blob 下载观察结果。数据库表可以用于故障注入和适配器诊断，但不能成为业务断言的唯一旁路。

## 2. 模型、假设与生成器

### 2.1 简化模型

参考模型仅记录：

- Space/Actor/Consumer 及当前授权视图。
- 成功提交的 `(主体, operation, request_id) → 指纹与稳定结果`。
- 按真实发布顺序排列的可见资源 ID。
- 每个 Consumer 的已收取集合、已处理集合与检查点。
- 每个 Collection 的 revision、当前条目及删除标记。
- 被确认封存的 Blob 字节与可见范围。

模型不重写生产的 SQL、R2 路径、MCP SDK 或提交算法。其规则来自 RFC；不得与被测实现共用授权、分页、CAS 或去重 helper。

### 2.2 故障模型与边界

性质测试假设耐久存储自身遵守已验证的提交和读取契约。`Crash` 丢失进程、连接和内存状态，但保留已确认的耐久写入；存储永久物理丢失不在这个模型里。

故障可以发生在保留前后、Blob 写入前后、发布事务前后、响应传送前后。事务失败的模型允许“整体已提交但响应丢失”或“整体未提交”，不允许假设单个字段总会部分成功。

跨 R2 / 元数据没有整体事务：Blob 就绪、元数据失败是合法中间态，但此时 Feed 不可见。必须由恢复或清理处理。

活性测试额外假设：故障最终停止，授权保持有效，历史未裁剪，消费者持续重试，调度不永久饿死任何允许操作。

### 2.3 数据生成

| 生成维度 | 必须包含的情况 |
|---|---|
| 身份 | 多 Space，同名 Actor，多个 Consumer，不同授权；轮换和撤销 |
| 请求 | 同 ID 同内容、同 ID 不同内容、不同 operation、跨 HTTP/MCP 重试 |
| 信封 | 收件人顺序变化、不同会话、合法回复、非法来源或 Blob 引用 |
| Feed | 空页、稀疏可见项、页大小 1/边界、晚提交、视图变化 |
| 回执 | 重复、逆序、不同 Consumer、旧检查点、新检查点 |
| 资料 | 空/边界长度、摘要不符、上传中断、并发重复 PUT、清理竞争 |
| 记忆 | snapshot、delta、空 snapshot、无变化、重复 item、显式删除、冲突 |
| 时间 | 上传到期、令牌到期、订阅到期、时钟推进与回调重试 |

非法操作必须作为真实输入调用并检查稳定错误及无可见副作用，不能全部被 generator 的 precondition 排除。

## 3. 性质定义

### P01：空间和资源隔离

**范围。** 两个 Space，主体仅有其中一个空间或部分 Collection 的授权。

**性质。** 该主体的 read、status、ACK、Blob、memory 和订阅操作不能读取或改变未授权对象；消息中自填另一个 producer、来源 URI 或显示名称不能改变身份。

**生成。** 复用另一个空间的真实 ID、摘要、游标、request ID 与 Consumer ID；混合合法和非法资料引用。

**观察。** 通过各主体公开 read/status 与可读版本比较授权外状态不变。错误按规范隐藏未知对象的存在性。

### P02：稳定幂等提交

**范围。** 授权有效，语义内容不变，同 `(Space, Actor, operation, request_id)`。

**性质。** 重试、并发重复和响应丢失后，最多一个业务发布，返回同资源 ID 与发布时间；记忆提交返回同 revision。

**生成。** N 次相同请求、JSON key 顺序变化、收件集合顺序变化、故障与重启。

**观察。** 完整读取 Feed 后只有一个对应发布；status 指向同稳定结果。暂时 `pending` 不等于第二次发布。

### P03：同键内容冲突

**范围。** 原提交已固定幂等指纹。

**性质。** 改正文、附件、收件人或版本参数后复用原键，被拒绝；原资源与 Feed 不变。

**生成。** 对请求各语义字段做独立变异，含合法但不同的新内容。

**观察。** `IDEMPOTENCY_CONFLICT` 与原记录一致，不能取得新资源 ID。

### P04：发布成功可恢复

**范围。** 已取得 committed，授权与保留条件成立。

**性质。** 当前进程及新建服务实例都可通过公开接口读到正文和全部引用资料，status 返回原提交结果。

**生成。** 发布后立即 Crash，包含响应丢失、重启和多次读。

**观察。** 使用新的实例及实际存储适配读取。不能仅断言 metadata 存在而不取 Blob。

### P05：未发布状态不可见

**范围。** 提交停留 reserved/prepared，或发布事务明确回滚。

**性质。** 新 Consumer 的 Feed 和业务读取不能把它作为已发布资源；不能返回 committed 回执。

**生成。** 在 Blob 成功后阻断元数据提交，恢复提交前后分别读取。

**观察。** 状态可以显示 pending；发布前没有对应资源，发布后只有一个。

### P06：晚完成提交仍可收取

**范围。** A 先保留，B 先发布，消费者已读到 B，随后 A 发布。

**性质。** A 的最终 visible_seq 晚于 B，后续读取必得 A。

**生成。** 让多个保留中的提交按随机次序完成，交错读取不同页。

**观察。** 比较最终完整读取到的 ID 集合与成功提交集合；不得只比较请求创建时间。

### P07：消费者独立

**范围。** Consumer A、B 都可读同一项。

**性质。** A 的 ACK、检查点、停用或 processed 状态不改变 B 的待收取和回执；读取不删除原内容。

**生成。** 分别分页、ACK、重启、使用同 Actor 的不同安装身份。

**观察。** 分别以两个 Consumer 调用 read/status，看各自的记录与稳定原文。

### P08：回执单调与无循环

**范围。** 同 Consumer、同 item 的有效 ACK。

**性质。** `none ≤ received ≤ processed`，逆序或重复不回退；状态不变不生成新回执变化。确认一个 receipt item 不生成另一个 receipt item。

**生成。** `processed/received` 的任意重复序列，重复确认回执 Feed。

**观察。** 最终状态为最大有效阶段，Feed 中无无限确认链。

### P09：游标完整与视图绑定

**范围。** 授权和视图稳定，保留记录不被裁剪，提交最终静止。

**性质。** 从起点不断分页所得 ID 集合恰为该视图的可见已发布集合；无遗漏、无未授权项。重读允许相同 ID，但顺序不倒退。另一 Consumer、过滤或权限范围不能沿用旧游标。

**生成。** 多页、空页、稀疏记录；篡改游标；改变 view/grants；使用同权限的新 token。

**观察。** 合法分页覆盖独立模型的集合；变化和篡改产生规范错误，重新同步仍可覆盖新视图。

### P10：记忆 CAS 原子性

**范围。** 两个不同请求基于同 revision 更新同 Collection。

**性质。** 有内容变化时最多一个成功前进一版；冲突者不产生 head、Revision、Feed 或成功提交结果。相同成功请求重试仍返回其原版本。

**生成。** 并发 snapshot/delta、Blob 先后完成、事务响应丢失、0 行 CAS。

**观察。** 公开 memory.read 和 Feed；不能把 SQL success 或 batch 完成当 CAS 命中。

### P11：Snapshot 与 Delta 的不同含义

**性质。** Snapshot 的当前 active items 等于明确完整输入；空 snapshot 清空集合。Delta 只改变 upsert/delete 指定项，遗漏其余内容保持。

**生成。** 先建立随机集合，再完整替换或随机局部变更；包括无变化更新和删除不存在的项。

**观察。** 按固定 revision 读完整状态；无变化返回原 revision 且无新 Feed。

### P12：来源删除与旧版本恢复

**性质。** 一个 Collection 的删除不修改其他来源；删除现存条目后旧 expected revision 的迟到更新被拒绝。只有基于当前版本的明确 upsert 可以恢复同条目。

**生成。** 多集合使用同 item ID、删除后重传旧批次、合法恢复、原请求重试。

**观察。** 各集合的 active items/Tombstone 与版本独立，历史版本仍可读。

### P13：Blob 封存与完整发布

**性质。** 未封存、摘要不符、超限或未授权的 Blob 不能进入发布资源。封存和晚到 PUT、暂存清理竞争不改变已发布引用的字节。

**生成。** 上传中断、不同字节复用 upload ID、并发 PUT/commit/cleanup、批次缺一个文件。

**观察。** 下载已发布引用的真实字节，与原确认的摘要和内容相符；半份消息/快照不出现在 Feed。

### P14：轮换与撤销

**性质。** 同 Actor/Consumer、同权限的新凭据保留提交幂等和游标连续性；旧凭据被撤销后不能用旧幂等键取得结果或提交新发布。

**生成。** 提交暂停期间轮换/撤销，改变 scope，响应丢失后用新凭据重试。

**观察。** 当前授权总被检查；成功重试无重复，变化范围的游标明确失效。

### P15：事件投递独立

**范围。** 可选 webhook capability 已实现。

**性质。** HTTP 成功、失败、重复、乱序或订阅到期不改变核心业务内容与 Consumer 处理进度；重试的 `(source,id)` 稳定，签名时间与 attempt ID 可改变。

**生成。** 模拟 callback 2xx/410/429/5xx、超时、密钥轮换与权限撤销。

**观察。** 核心 Feed 始终可补收；回调记录不伪造 received/processed；到期和撤销停止后续交付。

### P16：传输语义一致

**性质。** 同主体同领域操作先 HTTP 后 MCP 或相反重试，使用同一幂等范围、验证规则和领域结果。

**生成。** 合法与非法请求，经两个真实适配入口调用；首个响应丢失后切换入口。

**观察。** 公共结果相同，只有一个发布；MCP 协议封装差异不被当作另一业务操作。

### P17：消费者待处理可恢复

**范围。** 被测消费者 SDK/参考客户端遵循先写本机再 ACK。

**性质。** 收取与 ACK 后业务处理中断，恢复仍找到待处理记录；没有保存成功时不能越过检查点。

**生成。** 下载、写本机、ACK、业务动作和结果记录之间 Crash。

**观察。** 客户端公开的待处理状态与工具调用轨迹；对外动作不能只因重读而盲目重复。

这验证参考消费者，不把性质扩大成服务对任意第三方客户端的写盘保证。

### P18：有条件的最终补收

**前置条件。** 故障已停止，授权有效，历史仍在，消费者继续执行，调度公平。

**性质。** 当写入静止后，有限次完整分页与同键恢复能获得全部可见 committed 资源，不留下永远 pending 的已实际提交记录。

**生成。** 有限故障历史后执行 Recovery，再读取至稳定空页。

**观察。** 可见提交集合与读到集合相等，status 和版本一致。无限断网、被撤销权限或物理存储丢失不在承诺范围。

## 4. 命令模型与重现

随机命令包括 `Prepare/Put/Seal/Send/Read/Ack/PublishSnapshot/PublishDelta/Rotate/Revoke/Crash/Recover/AdvanceClock`。并发调度加入多次同键和同基础版本的竞态。

每条失败记录保存 seed、随机序列、调度轨迹与最小反例，进入回归用例。实现可采用 fast-check 的 command-based 模型与可重放调度；模型应简化而非复制系统。[fast-check 文档](https://fast-check.dev/docs/advanced/model-based-testing/)

测试量按测量选择。大量随机历史先跑本地，生产适配跑小而关键的真实契约与故障集，不向真实第三方用户或未授权服务发送测试消息。

## 5. 持久适配的故障检查点

| 检查点 | 注入 | 必查结果 |
|---|---|---|
| 幂等保留完成 | 丢响应或重启 | 后续固定同一个资源 ID |
| Blob 已写入 | D1 提交失败 | 未发布，原提交可恢复 |
| 最终元数据提交 | 丢响应 | 同键得到 committed 原结果 |
| 记忆 CAS | 0 行条件命中 | 无新版本、无 Feed |
| 上传封存 | 迟到 PUT 或 cleanup | 已发布字节不变 |
| 分页读取 | 在两页之间晚发布 | 下一页/后续读取仍能得到它 |
| Consumer 本机保存 | Crash | 不错误确认未存内容 |
| 回执写入 | 响应丢失 | 重复 ACK 不增加第二次变化 |

Cloudflare 集成测试另测真实 R2 checksum、create-only、D1 原子 guard、存储恢复、当前授权检查与 Worker 资源开销。性质模型不能证明这些外部机制已正确实现。

## 6. Skill 场景评测

| 场景 | 观察到的正确行为 |
|---|---|
| 未连接 MCP | 保留待发内容，说明连接缺失，没有虚构保存回执 |
| 保存响应丢失 | 查原提交，有限同 ID 重试，不换键重复发信 |
| 用户指定收件人 | 保留明确目标与原文，使用获准 Actor ID |
| 来源只导出部分记忆 | Delta 或明确范围集合，不把缺失资料当删除 |
| 版本冲突 | 先核实，不只把 expected revision 改成最新值覆盖 |
| 文件传输能力缺失 | 如实说明，不假称附件或完整快照已保存 |
| 回信请求需要原宿主批准 | 继续遵守该宿主权限，收到不是已经执行 |
| 用户问对方是否已读 | 依据真实回执阶段回答，不把 committed 当已读 |

评测保存可审查的操作轨迹与结果，避免只匹配表达方式。

## 7. 实现验收门槛

- 每个必需性质都有运行测试、前置条件和可重现反例机制。
- 至少保留晚提交漏收、CAS 0 行、副本消费者 ACK、令牌轮换、局部删除和回执丢失六类确定性回归。
- 两个传输入口及生产存储适配满足契约，不只在内存中通过。
- 未实现的事件或宿主 capability 不伪造支持。
- 验收记录区分服务性质、存储机制、参考客户端与模型行为，避免过度承诺。