强最终一致性

普通“最终一致”只说停止更新并等待足够久后会靠拢，可能容许两个已见完全相同历史的副本因到达顺序不同而暂时不一致。SEC 加强了函数性：状态由已经吸收的更新历史唯一决定。网络负责让历史最终相同，数据类型负责让相同历史立刻映成相同结果。

这把安全与活性分开。Strong convergence 是安全性质：一旦发现同历史不同状态，已经出现反例；eventual delivery 是活性性质：任何有限观察都不能证明它永远不会发生。测试只等待几秒看到相等，不能替代对公平传播的论证。

“等价状态”应按可观察 query 定义，内部压缩表示可不同。例如一个副本保存完整 dot 集，另一个保存等价前缀摘要，只要未来 merge 与 query 行为一致即可；若压缩使旧值未来复活，就不再等价。仅有相同更新数量、相同最大时间戳或相同当前 query 都不足以判定 histories 相同。

两个 grow-only set 副本初态为空。A 加入 $x$，B 并发加入 $y$。A 先后吸收事件序列 $(x,y)$，B 先后吸收 $(y,x)$；二者已见事件集合都是 $\{x,y\}$，集合并给

这见证 strong convergence。若 C 此刻只收到 $x$，其状态 $\{x\}$ 不必与二者相同；eventual delivery 要求 $y$ 以后到达 C，不能把当前差异误报为 SEC 失败。

分区期间先让 A 的写 red 完成，再调用并完成 B 的写 blue，最后从尚未收到 B 更新的 A 读到 red；其间没有第三次写。这个明确的实时顺序要求线性一致读返回 blue，因此读 red 不合法。一个按 marker 最终选择 blue 的 LWW CRDT 仍可在愈合后让所有副本收敛，满足 SEC；后来的共同赢家不会回溯性地修复这次读取。

若整数 increment effectors 在 A 去重、在 B 重复执行一次，两边即便收到相同消息包也得不同数值。问题应归到 multiplicity 合同，而不能用“最后再同步一次”修复。反过来，A 只收到事件 $\{u\}$、B 只收到另一个事件 $\{v\}$，即便二者都“收到一个更新”且 query 偶然相等，也不触发 strong convergence 的前件。

SEC 适合作为 CRDT 验收规格：模型检查可枚举更新事件、合法交付偏序与重复策略，验证任何相同 history frontier 的 query 相等。网络故障注入则验证 eventual delivery 和崩溃恢复是否保留去重、因果依赖与未传播状态。Method termination 还要注明是否允许无限等待缺失依赖；后台交付可等待，不代表前台调用也可无界挂起。

产品文档仍应额外说明读取保证。SEC 系统可以提供本地低延迟读，也可叠加 session token 获得 read-your-writes；若需要 linearizable conditional update、唯一用户名或余额约束，必须加入协调或专门的 invariant-confluent 设计。