报告 003 · 依赖校验与慢速结果复核

文档索引 · 当前设计 · 研究问题

日期：2026-09-19。证据层次：受限状态模型。完成本实验枚举与补充场景；没有调用模型、运行真实并发服务或测量性能。

1. 实验范围

在一个手工定义的资源占用任务中，从相同合法快照生成候选，再枚举 12 种变化、长度 0～3 的所有序列。共 1,885 条路径，其中参考要求仍满足的为 186 条，不再满足的为 1,699 条。

参考要求包含资源可用、同一 incarnation、无其他占用、授权与交互仍有效、提供者未变化和时间未到期。任务需求及前置条件由实验作者明确给出，没有验证模型自动发现依赖的能力。

集合读取包含空结果；占用记录新增时不修改目标对象版本。对象重建可复用 ID 和初始版本号。纯时钟推进不增加全局版本。条件、策略及枚举范围见实验说明。

2. 实际计数

公共守卫检查授权代号、交互轮次、提供者身份和有效期，各正式版本策略使用相同守卫。仅全局版本是负向对照；两个漏项组是消融。

表中数值只表示所枚举路径，不是生产故障率。完整条件与参考判定拥有相同信息，因此零误判是该对照的预期上界，不能据此宣称已找到普适的智能复核算法。

3. 最短反例

时间流逝但版本不变。 连续推进三个时钟刻度，候选到期，全局版本仍为初值。仅比较版本会接纳过期结果。

无关更新导致拒绝。 一次无关对象更新就使全局版本策略拒绝仍合法的候选。给目标改一个不影响占用的标签，则会触发目标对象和完整依赖版本的保守拒绝。

空查询不是没有依赖。 新增一条占用记录，目标对象版本不变，仅目标版本校验仍然接纳，违反任务要求。

同 ID 不等于同一资源。 重建资源时恢复初始局部版本，业务 ID 也保持相同。忽略 incarnation 的条件策略会把新资源误当作原来对象。

4. 背景变化下的进展

给每组最多 8 次候选机会，每次从最新状态开始，再在结果产生前插入指定背景变化：

所有这些候选在参考条件下仍合法。该固定时序说明保守失效可以持续阻碍进展；它不代表真实任务的平均重算次数，候选次数也不是 token 或耗时测量。

5. 串行提交仍可能接纳两个冲突计划

两个请求都在同一空占用集合下形成，然后按 A、B 顺序提交，各自新增不同的占用行。仅目标对象版本策略与漏掉集合条件的策略都接纳 A 和 B，最终占用数为 2，违反最多一个占用的约束。

完整依赖版本或完整条件拒绝第二个请求。这里提交已经串行；反例针对依赖校验不完整，而不是说明必须采用某种多心智调度方式，也不评价真实数据库的默认事务隔离。

6. 校验后的执行窗口

宿主在初始状态完成检查后，在执行前插入 8 个指定场景：无关更新，以及不可用、新占用、重建、撤权、新轮次、提供者重启和时间到期。

第三组假定所有条件可由同一权威执行者原子读取并强制执行，属于理想化上界。实际跨服务授权、用户取消和物理状态不一定满足这一假设。第二组仍能保护其声明范围内的目标条件，只是不能替代集合、授权和时间检查。

7. 设计结论及限制

保留全局版本用于溯源或保守判断；细化读取清单以覆盖对象代号、查询集合与空结果；对授权、轮次、提供者和时间独立复核。执行允许与原决策是否合理继续分开处理，详见结果复核设计。

本实验没有测量真实模型的依赖表达、条件提取准确率、部分结果复用质量、并发吞吐、数据库实现成本或远端条件执行。也没有证明将所有条件交给宿主手写是合适的认知架构。

枚举路径包含重复状态和人工选择的事件分布，计数受这些选择影响。可以推广的是已找到的具体反例及其前提，不能将本表排序直接当作生产策略排名。

依赖仅为标准库。

脚本 SHA-256：545fcba37d6632f5a505a2141c9abde9626280fa421616860c5bc2d8409b19e9。

所有有限模型断言通过。生成结果保留各策略最短误判路径、8 次机会场景、两个请求的提交结果和执行窗口的逐项结果；没有真实外部动作。

数据可用性

本报告公开实验条件、汇总统计和失败分析。原始输入、脚本及逐次运行记录未随报告发布，因此不能仅凭本文独立复现实验。