第26篇 Spanner 本地有限模型证据

日期：2026-09-23
源码：examples/distributed-systems/spanner26/check.py
源码 SHA-256：455aa3529cc240a248621807dc01e373d17abd4f953b9d742fd24d3f08623f81

正式运行一：Python 3.14.4，工具 chunk 45617d，退出0。
正式运行二：/usr/bin/python3 3.9.6，工具 chunk 720bbf，退出0。
两次 observations JSON 逐字相同。

四组结果：
1. 正常提交：s=111；决定已复制但 earliest 尚未越过 s 时不得完成；earliest=112 后通过。
2. 跳过等待：T1 在真实时间101返回、提交戳111；T2 在真实时间103开始、提交戳105，检出一组外部时间戳逆序。参与组独立，结论不扩大为单独键值历史必然不可线性化。
3. 时钟契约：诚实宽区间继续等待；不含真实时间的错误区间会错误通过 after，先标为前提破坏。
4. 快照和safe time：固定19读到(0,0)，固定20读到(1,1)，分开读取可得到(0,1)；应用进度118及未决prepare形成的119均阻塞快照125，解决并应用后safe=130。

CLI：--help 退出0；--unexpected 退出2，工具 chunk 709289。
三TMP变量均指向仓库 examples/distributed-systems/.build/spanner26/tmp；使用 -B，无子进程、网络、下载、编译或临时程序。

边界：Paxos复制是显式布尔状态转移；整数时间不是TrueTime实现；有限固定轨迹不覆盖任意调度、真实故障、持久化、时钟硬件或云服务。