# 找共同祖先：Loro 历史图遍历算法的规格与证明骨架
状态：草稿 v2，2026-08-01。对应 `crates/loro-internal/src/dag.rs` 中的
`_find_common_ancestor_new`（含 PR #1058 与 tips 去重修复之后的版本）。
这份文档是自包含的：读者不需要了解 Loro、CRDT 或本仓库的代码。
需要的全部预备知识是：集合、有向图、数学归纳法，以及"堆/优先队列"这个数据结构。
文档先讲问题从哪里来（第 1 章），再给出数学模型（第 2 章）、算法（第 3 章）、
我们承诺的性质即"规格"（第 4 章）、证明骨架（第 5 章），最后是待定问题（第 6 章）
和词汇表（第 7 章）。写作顺序都是**先直观解释、再数学定义**。
---
## 1. 问题从哪里来
### 1.1 多人协作编辑与操作历史
Loro 是一个协作编辑库。它要解决的场景是：几个人（或几台设备）同时编辑同一份
文档——比如一份购物清单——而且允许离线编辑，之后再同步。同步之后，
所有人看到的结果必须完全一致。实现这一点的数学工具叫 CRDT，
但本文档不需要你懂 CRDT，只需要懂下面这个更基本的东西：**操作历史**。
每个参与者（叫一个 **peer**，可以理解为"一台设备上的一个副本"）
做的每一次修改都是一个**操作（op）**。操作不会被覆盖或删除，只会不断追加，
所以整个文档的历史就是所有人产生的所有操作的集合。
每个操作有一个全局唯一的编号：**(p, c)**，读作"第 p 个 peer 的第 c 个操作"，
文本形式记作 **c@p**（counter 在前，与 Loro 代码输出一致；见第 2 章记法约定）。
同一个 peer 的 c 从 0 开始，每做一个操作加一。
操作之间有一种天然的先后关系：**做某个操作时，作者已经看到了哪些别的操作**。
比如 Bob 在看到 Alice 写下"牛奶"之后才补了一句"鸡蛋"，那么"鸡蛋"这个操作
就**依赖**"牛奶"那个操作。反过来，如果两个人离线时各改各的，
互相都没看见对方的修改，这两个操作就是**并发的（concurrent）**——谁也不依赖谁。
把每个操作画成一个点、依赖画成有向边，整个历史就是一张**有向无环图（DAG）**。
一个具体的小例子（A = Alice，B = Bob；箭头为 **happened-before** 方向，
由早指向晚——与 Eg-walker 论文一致；注意存储时每个事件记录的是反向的
"父事件"引用）：
```
A0 "加入苹果" ──→ A1 "加入牛奶" ──→ A2 "加入面包"
│
└────────────→ B0 "加入鸡蛋"
```
- A1 依赖 A0（同一个人的下一个操作，天然依赖上一个）；
- B0 是 Bob 看到 A1 之后做的，所以 B0 依赖 A1；
- A2 是 Alice 在**没看到** B0 的情况下做的，所以 A2 只依赖 A1。
- A2 和 B0 互相都不依赖：它们是并发的。
### 1.2 版本与前沿（frontier）
"文档在某一时刻的版本"是什么？直观上：**一个操作集合**——这一时刻已经发生
（且被这个副本看到）的所有操作。这种集合有个重要特点：**因果闭合**——
你看到了某个操作，就必然看到了它依赖的一切操作（否则你根本无法理解它）。
因果闭合的集合不需要逐个元素列出来，只要报出它的"最新端点"就够了：
比如上图中"Bob 视角的版本"是 {A0, A1, B0}，只要说"我最新到 B0"即可，
因为 B0 的全部祖先自动包含在内。这组最新端点就叫**前沿（frontier）**。
一个前沿里不会有谁是谁的祖先（否则那个祖先是多余的），
这种"两两互不为祖先"的集合在数学上叫**反链（antichain）**。
前沿可以有多个端点：上图中 Alice 同步了 B0 之后，她的版本是全部 5 个操作，
前沿是 {A2, B0}——两个并发的端点，谁也代表不了谁。
### 1.3 要解决的问题：给两个版本找"重放起点"
Loro 里有两个高频动作：
- **import（导入）**：收到别人发来的更新，把新操作合并进本地历史；
- **checkout（检出/时间旅行）**：把文档切换到历史上任意一个版本。
两者的核心都是同一个计算：**给定旧版本 L 和新版本 R（各用一个前沿表示），
算出文档状态从 L 到 R 的"差量"（diff）**。计算差量的通用办法是**重放**：
从两个版本**共同拥有**的历史中选一个起点，把起点之后的操作按因果顺序重演一遍，
一边重演一边算出状态差。
于是问题变成：**重放起点选哪里？**
- 起点选得**太老**：要白白重演大量双方本来就共有的历史。这不是理论担忧——
本仓库最近修的一个真实 bug（PR #1058）就是起点被错误地退到了历史开头，
导致导入一个 124 字节的小更新要重演全部历史、耗时是正常情况的几百倍。
- 起点选**错**（比如漏掉某条并发分支的分岔点）：差量会算错，
文档内容错乱。这比慢严重得多。
直觉上理想的起点是两个版本公共操作中"最靠上"的那些——本文档记作
meet（版本格的最大下界前沿，第 2 章 D8 给精确定义；它是一个反链，
不一定是单点）。但 meet 只是**候选**：起点还必须满足一个"切得开"的
条件（critical version，D8b），meet 不满足时要向更早处回退——
这正是场景④"保守回退"的由来，严格定义见 4.1 节。
除了起点，调用方还需要知道第二件事：**R 是否完全包含 L**？
如果是（典型情况：导入的更新完全建立在本地版本之上），差量计算可以走快路径
（不需要重建复杂的中间结构）；如果否（存在并发），必须走慢而稳的路径。
算法把这个判断以"模式"（mode）的形式一并返回：
- `Linear`：R 包含 L，且新增部分是一条无分叉的直线；
- `ImportGreaterUpdates`（下文简称 IGU）：R 包含 L；
- `Checkout`：其余所有情况（存在并发、或时间倒流），走保守路径。
### 1.4 为什么这个问题不平凡：三个陷阱
**陷阱一：隐式依赖造出"冗余路径"。**
同一个 peer 的第 c 个操作天然依赖第 c−1 个，这条边**不会被显式存储**
（存了就太浪费了），遍历时要自己补上。这会造出"一个祖先、两条到达路径"的局面：
```
0@1 ──→ 0@2（中转） ──→ 1@1
│ ↑
└──────（隐式：同 peer 前驱）─┘
```
peer 1 做完 0@1 后，peer 2 基于它做了 0@2；然后 peer 1 看到 0@2 又做了 1@1。
1@1 显式依赖 0@2，同时隐式依赖自己的前驱 0@1。从 1@1 出发往下走会分出两条路：
显式路经 0@2 到 0@1，隐式路直达 0@1。第二条路是**冗余**的——它到达的一切
都能从第一条路到达。但一个只看"这条路走到死也没碰到对方"的简单算法
会把冗余路误判成**并发分支**，进而把重放起点错误地退到历史开头。
这正是 PR #1058 修复的 bug。区分"冗余路"和"真并发分支"是本算法最微妙的部分。
**陷阱二：操作是按"段"存储的。**
为了效率，同一个 peer 连续的一串操作打包成一个**节点**（内部叫 Change）存储，
遍历时弹出的是一整段。而别的路径的依赖可能恰好指向这一段的**中间**某个操作。
算法必须保证"整段前进"不会大步跨过别人指向的中间点（3.3 节的"对齐"机制）。
**陷阱三：性能约束。**
历史可以有百万级操作。遍历的开销必须只和"两个版本附近的区域"成正比，
不能做全图搜索。手段是给每个操作配一个 **lamport 时间戳**（2.1 节），
永远从"时间戳最大"的未处理条目开始处理——像水面从高处向低处退去，
两个版本的探索会在共同祖先附近自然会合，不必触碰更深的历史。
---
## 2. 数学模型
本章把上面的直观图景变成精确定义。每个定义前先用一句话回顾直观含义。
**D1（操作 id）** 操作的编号是二元组 (p, c) ∈ P × ℕ，P 是 peer 的集合。
**记法约定** 具体 id 的文本形式一律写作 **c@p**（counter 在前、peer 在后），
与代码中 `ID` 的 Display 输出一致（`loro-common/src/id.rs`）。数学元组仍写
(p, c)，读作"peer p 的第 c 个操作"；若行文需要 peer 在前的紧凑形式，写
P⟨p⟩_C⟨c⟩，**绝不写 p@c**，以免与标准文本形混淆。叙事中的字母形
（A0 = Alice 的第 0 个操作）仅用于故事。
**D2（节点划分；公理 A2）** *——"连续操作打包存储"。*
每个 peer 的操作序列被划分为若干互不重叠的连续区间，每个区间叫一个**节点**
N = [s, e)（含 s 不含 e）。每个操作恰好属于一个节点。节点携带一个
**显式依赖集** deps(N) ⊆ Ids，语义上挂在节点的第一个操作 (p, s) 上。
**D3（父事件 parents 与事件图；Eg-walker §2.2）**
*——"做这个操作前刚看到的最新操作们"。*
每个事件 e 携带**父事件集** parents(e)（论文记 e.parents；Loro 代码称 deps）：
- 隐式父：(p, c−1) ∈ parents((p, c))，对一切 c > 0；
- 显式父：deps(N) ⊆ parents((p, s))，s 是节点 N 的起点。
事件与父引用构成**事件图（event graph）**：一张 DAG，每个节点是一个事件
（一次操作 + 唯一 id + 父事件 id 集，论文 §2.2）。
**D4（happened-before → 与并发 ∥；Eg-walker §2.2）**
*——"由早指向晚的因果链"。*
a **happened before** b（记 **a → b**）当且仅当沿父引用存在从 b 回到 a 的
有向路径：a → b ⟺ a ∈ parents(b) ∨ ∃e: a → e ∧ e ∈ parents(b)。
箭头方向沿用论文与 Lamport：**由早指向晚**（父引用存储方向与之相反）。
**并发**：a ∥ b ⟺ a ≠ b ∧ a ↛ b ∧ b ↛ a（论文 §2.2）。
引理中常用的自反版本 **≤**：v ≤ u ⟺ v = u ∨ v → u。
祖先闭包沿用论文记法 **Events(·)**（§2.3）：
Events(V) = V ∪ { e₁ ∣ ∃e₂ ∈ V: e₁ → e₂ }。
为行文简短，本文把 Events({u}) 记作 ancestry(u)、Events(F) 记作 ancestry(F)。
**D5（lamport 时间戳；公理 A1）** *——"逻辑时钟：你依赖的东西一定比你早"。*
函数 lamport : Ids → ℕ 满足：
- 沿父引用严格递减：a ∈ parents(b) ⟹ lamport(a) < lamport(b)；
- 节点内逐操作加一：lamport(p, c+1) = lamport(p, c) + 1。
由传递性立即得到本文档最常用的推论：
> **L0**：v → u（v happened before u） ⟹ lamport(v) < lamport(u)。
注意反过来**不成立**：lamport 小不代表 happened-before（并发操作的 lamport 也可比较大小）。
**D6（前沿 / version；Eg-walker §2.3）** 有限反链（成员两两并发）。
论文把因果闭子图 G′ 的前沿称为它的 **version**：
Version(G′) = { e₁ ∈ G′ ∣ ∄e₂ ∈ G′: e₁ → e₂ }（没有后继的事件全体）。
前沿与因果闭集互逆：Events(Version(G′)) = G′，Version(Events(F)) = F。
算法输入是两个前沿 L 和 R。
**D7（版本与版本向量）** *——"版本 = 因果闭合的操作集 = 每个 peer 报一个前缀长度"。*
称操作集 S 是**因果闭**的，若 u ∈ S 且 v ≤ u 则 v ∈ S。ancestry(F) 总是因果闭的。
由隐式边，因果闭集在每个 peer 上必是前缀 {(p,0), …, (p,k−1)}，
所以一个因果闭集可以用"每个 peer 一个数字 k(p)"紧凑表示——这就是**版本向量**。
两个版本的包含关系等价于逐 peer 比较数字：
> vv(R) ⊇ vv(L) ⟺ ancestry(L) ⊆ ancestry(R)。
**D8（公共历史与 meet 前沿）** C(L, R) = ancestry(L) ∩ ancestry(R)。
两个因果闭集的交仍是因果闭的。定义 **meet(L, R) := Max(C(L,R))**，
即 C 中的极大元全体——版本格（因果闭集按 ⊆ 构成的格）中两版本最大下界
的前沿，这是一个反链。测试里的"oracle"（暴力对照实现）算的就是这个对象。
命名说明：本文档与代码曾把它借称为 "LCA"，2026-08-01 起已全面弃用：
代码中 `iter_from_lca_causally` 改名 `iter_from_replay_base_causally`、
`lca_vv` 改名 `replay_base_vv`、回退函数命名为
`latest_single_head_critical_version`，文档改名
`critical-version-spec.md`。理由：经典 LCA 是图上两个**节点**的最深公共
祖先（单点），而这里的对象是两个**版本**在格上的最大下界；更重要的是，
meet 只是算法的**候选**，不是算法真正要交付的东西（见 D8b 与 4.1 节）。
`find_common_ancestor` 这个名字保留——它返回的确实是公共祖先版本。
1.1 节例子中：L = {A2}，R = {B0}，C = {A0, A1}，meet = {A1}。
**D8b（critical version；Eg-walker，arXiv:2409.14252 §3.5）**
*——"能把历史一刀两断的版本"。*
版本 V 在事件图 G 中是 **critical** 的，当且仅当它把 G 划分为
G₁ = Events(V)（V 的祖先闭包）与 G₂ = G − G₁，使得 G₁ 中每个事件都
happened-before G₂ 中每个事件：∀e₁∈G₁, ∀e₂∈G₂: e₁ → e₂。
等价说法：切口两侧没有任何一对并发事件。空版本 ∅ 平凡地 critical
（G₁ 为空，条件真空成立）。
重放起点的**合法性判据**正是它：以 B 为起点重放区域 G − Events(B) 时
tracker 无需 B 以下的任何位置上下文 ⟺ B 在联合图
ancestry(L) ∪ ancestry(R) 中 critical。Eg-walker 合并新事件时取
"发生在双方之前的**最晚** critical version"为起点（§3.6 的 V_crit）。
**D9（段 / OrdIdSpan）** *——"节点的一个前缀切片"。*
⟨N, e⟩ 表示节点 N 内的操作段 [s .. e]（含两端）。记
id_last = (p, e)，lamport_last = lamport(p, e)。
from_dag_node(u) := 包含 u 的节点在 u 处截断的段。
**段的 deps 恒等于所属节点的 deps**（挂在节点起点上），与截断位置无关——
这一点很重要：截掉段的尾部不会丢失任何依赖边。
**D10（浅历史 / trimmed；公理 A5）** *——"太老的历史可能已被裁剪掉"。*
可用操作集 D ⊆ Ids；查询函数 get 在 D 之外返回"不存在"。
输入前沿的成员都在 D 内，但节点的 deps 可以指向 D 外（裁剪边界）。
---
## 3. 算法
### 3.1 直观图景：两支探险队下山
把事件图想成一座山：lamport 时间戳是海拔，事件越晚海拔越高
（A1：happened-before 箭头由山下指向山上）；队员沿**父引用**向山下走。
- 给左版本 L 派一支**红队**，从 L 的每个前沿端点出发；
给右版本 R 派一支**蓝队**，从 R 的端点出发。
- 所有队员放进同一个**优先队列**，永远先处理**海拔最高**的那个队员。
队员每一步沿依赖边往山下走（一个队员分出几条依赖就分裂成几个队员）。
- **红蓝两队在同一个操作上相遇 → 该点染紫**：它是公共祖先，收进候选集 ans，
并且**不再继续往下走**（紫点以下全是更老的公共历史，无需探索——
这是性能的关键，也是后面一切微妙性的来源）。
- 某个队员**走到了死路**——走到没有依赖的根，或者队列里已经没有别人了——
却始终没碰到对方颜色，说明什么？
最后一问正是陷阱一。有两种可能：
1. 这个队员代表一条**真正的并发分支**（对方版本里根本没有这段历史）——
此时必须放弃候选起点、保守回退（把起点退到最老，模式 Checkout）；
2. 这个队员只是一条**冗余路**（1.4 节的隐式前驱路径）：它要到达的地方，
别的队友早就经由紫点到达了。它"死"只是因为紫点不再展开、没人来接应它。
此时**不应该**回退。
区分办法（**tips 机制**）：每个队员身上带一块牌子（tips），
写着"我是从哪个岔路口分出来的"。队员死亡时，查它的牌子：
> 岔路口 ∈ 已找到紫点的祖先集？
> 是 → 整条死路都在公共历史里，冗余，虚惊一场；
> 否 → 真并发分支，保守回退。
这个检查本身也是一次山上的小规模走查（从紫点出发往下、按海拔剪枝），
它只在有死路时发生。
### 3.2 精确描述
堆条目为三元组 e = (span, type, tips)：span 是一个段（D9），
type ∈ {A（红，来自 L）, B（蓝，来自 R）, Shared（紫）}，tips ⊆ Ids。
堆按 (lamport_last, peer, 更短的段优先) 的字典序弹出最大者。
**初始化**：L 的每个成员 u 以 (from_dag_node(u), A, tips₀) 入堆；R 同理入堆为 B。
其中 tips₀：若该侧前沿有多个端点，则为 {u}（每个端点自成一个"岔路口"）；
单端点时为空集（这条路还没分过岔）。
**主循环**——弹出 e = (n, t, tips)，依次执行：
1. **聚合**：只要堆顶条目与 n 的段相等、或 id_last 相同：把它也弹出并合并进 e；
两者 type 不同 ⟹ t := Shared；tips 取并集（**去重**——不去重会指数爆炸，
这是本次 review 修复的性能 bug）。
2. **会合**：若 t = Shared：ans 收进 id_last(n)；continue（不展开）。
3. **死亡（队空）**：若堆已空：记录 unmatched（tips 非空记 tips，
否则记 id_last(n) 自身）；break。
4. **偏序线索**：若 t = A（红队员在堆非空时被单独弹出，说明左侧有右侧
尚未包含的操作）：is_right_greater := false。
5. **对齐**（设堆顶为 o）：
a. 若 n 包含 id_last(o) 且 t ≠ type(o)：把 n 截断为以 id_last(o) 结尾，
重新入堆；continue。 *（对方指向我的中间：先切到对齐，下一轮聚合。）*
b. 否则若 len(n) > 1：把 n 收缩到 lamport_last 不超过 o 的 lamport_last
（且至少缩短 1，即取 min(按海拔对齐的长度, len − 1)），重新入堆；continue。
*（长段不许大步跨过任何海拔更高的旁人。"len − 1"上限处理海拔并列：
并列时按海拔对齐算出的长度等于自身，若原样重入堆即死循环；
上限强制严格进展，这正是 L10 终止度量在此分支下降的原因。
丢弃的段尾是安全的：依赖边挂在节点起点上（D9），截尾不丢边；
且以段尾为终点的条目会先被聚合分支合并，未来也不再有指向该海拔的
新条目（L1），故段尾不可能是任何会合点。）*
6. **展开**：parents* := 显式 deps(N) ∪ {隐式前驱（若未被显式依赖覆盖）}
（即 e.parents，D3；代码中称 deps）。
- 可解析且非空：每个 d ∈ parents* 以 (from_dag_node(d), t, tips_d) 入堆；
其中 tips_d：若 tips = ∅ 且 |parents*| > 1（**第一次分岔**），
则 tips_d = {id_last(d)}（在岔路口发牌子）；否则继承 tips。
is_linear := false。
- 不可解析（依赖被裁剪，D10）：unresolved := true；continue。
- parents* = ∅（走到根）且堆非空：记录 unmatched（同步骤 3）；continue。
**收尾**：
- ans := ans 的极大元反链（去掉互为祖先的冗余成员）；
- uncovered := unresolved ∨ ¬( unmatched 中每个 tip ∈ ancestry(ans) )。
覆盖判定用**单次**多源走查：从 ans 的所有成员出发向下，
按"尚未证实的 tips 的最小 lamport"剪枝（L0 保证剪枝安全）；
- 若 uncovered 且 ans 的依赖未触及裁剪边界：
ans := 并集图上最晚的单头 critical version（L11 扫描；不存在则 ∅）；
- 若 uncovered：is_right_greater := false；
否则若 ans = L：is_right_greater := true；
- mode := Checkout（若 ¬is_right_greater）；否则 Linear（若 is_linear 仍为真）；
否则 IGU。
此外实现里还有三个**快速路径**（R 为空、L 为空、L 与 R 都是单点且同 peer），
它们绕过主循环直接返回。每个都需要独立的小证明（见 Q6）。
### 3.3 三个机制再各给一个直观注解
**聚合**：站在同一位置的队员合并成一人；红 + 蓝 = 紫。合并同时合并牌子（去重）。
**对齐（回应陷阱二）**：一个段是"一列纵队"。规则 5b 说：纵队每轮最多下行到
与堆中次高者平齐的海拔，绝不越过；规则 5a 说：若对方明确指着我纵队中间的
某个人，我先在那个人处断开。两条规则合起来保证：
**任何指向段中间的会合都不会被跳过**。为什么"迟到的指针"不存在？
因为指向 (p, c) 的条目是由它的某个 depender 展开时入堆的，
而 depender 的海拔严格高于 (p, c)（L0）；再加上"堆的最高海拔单调下降"（L1），
指针必然在覆盖 (p, c) 的段消亡之前就已入堆。这就是第 5 章的 L3。
**tips 与覆盖检查（回应陷阱一）**：牌子只在"第一次分岔"时发放，
之后一路继承；两条路合流时牌子取并。于是不变式是：
**一条路径死亡时，它走过的每个操作都是它某块牌子的祖先**（L6）。
所以"牌子 ∈ ancestry(紫点)"就足以证明整条死路都泡在公共历史里（L7）——
检查牌子（少数几个点）而不必检查整条路径（可能很长）。
### 3.4 模式判定的含义
- is_right_greater 想回答"ancestry(L) ⊆ ancestry(R) 且起点可以就用 L"。
它有两个信息来源：走查过程中红队员是否曾被单独弹出（步骤 4），
以及收尾时死路是否全部被覆盖、ans 是否恰好等于 L。
- is_linear 想回答"新增历史是一条无分叉直线"：任何一次依赖展开都会把它清 false。
- 三种模式对下游意味着：Linear/IGU → 从 L 直接重放、走快路径；
Checkout → 从 ans（可能为 ∅ = 历史开头）重放、走保守路径。
---
## 4. 规格：我们向调用方承诺什么
| S1 | ans ⊆ C(L,R) | 给出的起点确实是双方共有的历史 |
| S2 | ans 是反链 | 起点集合里没有冗余成员 |
| S3 | mode ∈ {Linear, IGU} ⟹ ans = L ∧ ancestry(L) ⊆ ancestry(R) | 宣布"快路径可用"时，R 确实完整包含 L，且起点就是 L |
| S3L | mode = Linear ⟹ 上述之外还有 \|ans\| ≤ 1，且新区 ancestry(R)∖ancestry(L) 是 ≤-全序链 | 宣布"直线"时新历史真的无分叉（表述待定，见 Q2） |
| S4 | mode ≠ Checkout ⟹ 新区每个事件 ≥ L 的全部头（已强化，见下） | 由入场检查（L12）保证 |
| S5a | mode = Checkout ⟹ 只承诺 S1 ∧ S2（ans = ∅ 合法） | 保守模式下起点允许偏老，偏老只影响速度不影响正确性 |
| S5b | 猜想 C1：走查无死路 ⟹ ans = meet(L,R)（精确） | 常规情形下起点不多退一步（是否纳入规格待定，见 Q1） |
| T | 算法总终止 | |
**S4（已强化，2026-08-01）**：mode ≠ Checkout ⟹ 新区每个事件都
因果晚于 L 的**全部**头（即 L 对并集图 critical）。
历史背景：本条曾是"非目标声明"——旧版只承诺版本级包含
（vv(R) ⊇ vv(L)），把逐操作并发交给下游守卫兜底。两个反例都会通过：
```
反例一（同 peer 段截断）：L = {A5, L2}，R = {r}，deps(r) = {A9, L2}，
A6..A9 与 L2 并发；
反例二（movable tree 线上 issue）：L = {B6, A0}，新区 A1..A3 只依赖
A0、与 B6 并发。
```
后者证明了 Tree 计算器的 IGU 快速路径**没有**守卫（不同于 text/list
的 `mark_source_not_in_op_context`）：A1 未与 B4..B6 打擂台就被采纳，
增量状态与全量重放分叉。现由**入场检查**（L12）在多头 L 时强制验证，
两个反例都会被降级为 Checkout + L11 安全基准；单头 L 由 L9 的覆盖
论证自动满足本条。
### 4.1 算法真正在找什么（严格版，按 Eg-walker 的语言）
算法的候选是 meet(L,R)（D8），但合法重放起点的严格判据是
**critical version**（D8b）：起点 B 合法 ⟺ B 在联合图
ancestry(L) ∪ ancestry(R) 中 critical ⟺ 重放区域里没有任何事件与
ancestry(B) 中的事件并发。Eg-walker 的理论最优是"发生在双方之前的
最晚 critical version"（§3.6 的 V_crit）。据此把算法的行为分三类：
1. **meet 恰好 critical**（场景①③的常规形状）：候选即答案，
"找 meet"与"找合法起点"重合。
2. **meet 不 critical，且走查探测到证据**（uncovered 死路，场景④）：
回退到**并集图上最晚的单头 critical version**（已实现，2026-08-01）：
复用主循环的聚合/对齐机件，从 L ∪ R 做一次单色下山扫描；
待处理堆首次收窄为单个段的时刻，其 id_last 即所求（引理 L11）。
若某条链在堆非空时死于根或裁剪边界，其端点与其下一切事件并发，
之后不再可能有合法单头切口——立即放弃并返回 ∅（即旧行为；
场景④的双根正是此情形）。扫描只在回退真正发生时执行，
代价不超过随后重放区域的一次遍历。
与 Eg-walker 的 V_crit 相比仍有两处已知取舍：只找**单头**切口
（多头 critical version 无法用"堆宽 = 1"判据探测）；
找不到单头切口时不再细分、直接 ∅。
3. **meet 不 critical，但走查未探测到**（2026-08-01 起大幅收窄）：
IGU 候选（ans = L 且无死路）现在必须通过**入场检查**（L12）：
新区每个入场 change 的因果父集必须版本覆盖 L 的全部头，
不过则降级并调用 L11 扫描取安全基准。这消灭了原第 3 类中影响
IGU 的全部已知构造（S4 的两个反例）。仍然遗留的是 **Checkout
模式下 ans = meet 非 critical** 的情形（双根 x ∥ y 菱形：四条路
全部会合、无死路，meet = {x,y}，但区域内有事件与 y 并发）：
text/list 依赖下游守卫兜底，Tree 的 Checkout 路径是否暴露
尚未查证——见 Q7。
因此严格的安全陈述是**双层契约**：「(ans, mode) + 下游守卫」合起来
保证收敛；单看走查，无条件承诺的只有 S1/S2/S3/T。用论文语言可以把
守卫公理写准（这就是 Q3 要拍板的边界）：
> **守卫公理（接口）**：对任意被重放的 change c，若 vv(c) ⊉ vv(起点)，
> 则 tracker 以完整上下文重建后再应用 c，其效果与从任一合法
> critical version 重放一致。
---
## 5. 引理骨架（未来 Lean 里的定理清单）
每条引理：直观一句话 → 精确陈述 → 证明思路。
**L0（海拔与 happened-before）** *越晚的事件海拔严格更高。*
v → u ⟹ lamport(v) < lamport(u)。
证明：沿父引用逐条严格递减（A1），传递。
**L1（无迟到）** *水位只降不升；新入堆者总在水位之下。*
堆中最大 lamport_last 随时间单调不增；且任何一次 push 的条目，
其 lamport_last 严格小于 push 发生时刻的堆最大值。
证明：三类 push——展开（新条目是被弹条目的父事件，L0 给出严格更小）、
对齐重入（收缩后 ≤ 原值）、聚合不 push。弹出只移除最大者。归纳。
推论：**水位一旦降到 λ 之下，海拔 ≥ λ 的条目永远不会再出现。**
**L2（锁步）** *长纵队不越人。*
len > 1 的段只能通过聚合被吸收或通过对齐被收缩；
只有收缩到 len = 1（即只剩节点起点）时才会展开依赖；
且届时堆中不存在 lamport 更高的未处理条目。
证明：直接读主循环的分支结构——步骤 5b 拦截一切 len > 1 且未聚合的段。
**L3（会合对齐定理）** *该相遇的一定会相遇，哪怕会合点在段中间。*
若操作 u 既 ∈ 红队探索范围又 ∈ 蓝队探索范围，
则两侧条目必在 u 处（经对齐与聚合）合并为 Shared。
证明思路：指向 u 的条目由某 depender 展开产生，lamport(depender) > lamport(u)
（L0）；由 L1，该 push 发生时水位 > lamport(u)，而覆盖 u 的段
按 L2 要到水位 = lamport(节点起点) ≤ lamport(u) 时才消亡——
所以两个条目必有同时在堆的时刻；此后对齐规则 5a/5b 使两者 id_last 相等，
聚合规则将其合并。（分侧讨论 A/B/双向、以及等海拔并列的情形。）
**L4（颜色不变式）** *红队只踩左山，蓝队只踩右山，紫点必是公共的。*
任意时刻：A 型条目的段 ⊆ ancestry(L)；B 型 ⊆ ancestry(R)；
Shared 仅由 A 与 B 条目聚合产生。
证明：对"初始化、截断、收缩、展开"四种状态变迁归纳；
段是节点前缀 + 段的 deps 属于节点起点（D9）保证展开不越界。
**⟹ S1**。
**L5（极大化正确性）** 收尾的 shrink 恰好输出输入集合的极大元反链。**⟹ S2**。
**L6（牌子上界）** *死路走过的每一步都是某块牌子的祖先。*
一条路径自最近一次牌子发放（初始化多端点、或第一次分岔）之后
访问的每个操作 u，满足 ∃ t ∈ tips，u ≤ t。
证明：对"继承、合并取并、截断"归纳；发牌时刻 tips = {路径当前最新端}成立。
**L7（覆盖 ⟹ 冗余）** *牌子泡在紫水里，整条路都泡在紫水里。*
死路径的每个 tip ∈ ancestry(ans) ⟹ 该路径访问过的全部操作 ∈ ancestry(ans) ⊆ C。
证明：L6 + ancestry 的传递性（u ≤ t ≤ ans 成员）。
**L8（覆盖走查正确性）** 收尾的多源剪枝走查返回真 ⟺ tips ⊆ ancestry(ans)。
证明：完备性——走查是从 ans 出发沿父引用（逆 → 方向）的可达性搜索；
剪枝安全性——被剪节点的一切祖先 lamport 低于剩余 tips 的最小 lamport（L0），
不可能"包含"任何剩余 tip。
**L9（模式一致性）** 收尾后 is_right_greater = true ⟺ ans = L ∧ 无 uncovered。
关键子引理：**红条目一旦在堆非空时被单独弹出，ans ≠ L**——
因为该 L 成员随后要么被截短（id_last 变小）、要么被展开消耗，
再也不会以完整 id 进入 ans。
另一方向：ans = L ∧ 全覆盖 ⟹ L 的每个成员都聚合成了紫点
⟹ L ⊆ ancestry(R) ⟹（D7）vv(R) ⊇ vv(L)。**结合 L3、L6–L8 ⟹ S3**。
**L10（终止）** 度量：堆条目按 (lamport_last, len) 取字典序，
整个堆构成一个多重集，用 Dershowitz–Manna 多重集序比较。
每轮循环：聚合/弹出移除元素；对齐以严格更小的元素替换；
展开以有限个严格更小（lamport_last 更小，L0）的元素替换被弹元素。
多重集序良基 ⟹ 终止。**⟹ T**。（mathlib 已有 Dershowitz–Manna 序。）
**L11（回退扫描的正确性）** *堆是未探索区域的切口；
切口收窄成单个段的瞬间，段尾就是最晚的单头 critical version。*
设从 L ∪ R 出发做单色下山扫描（聚合与对齐机件同主循环），
且此前没有链在堆非空时死于根或裁剪边界。若某次弹出并聚合后堆恰为空，
记被弹段的 id_last = v，则 {v} 在并集图 Events(L) ∪ Events(R) 中
critical，且 v 是最晚的单头 critical version。证明要点：
(a) **切口不变式**：任意时刻，每个已发现未处理的事件都 ≤ 某个堆中条目
（同 L1 的推入论证）；堆空 ⟹ 未发现事件全部 ≤ v。
(b) **已处理事件 ≥ v**：每个已处理事件的每条向下路径都经由对齐/聚合
汇入唯一幸存的段；截断分支保证段尾取所有汇入点的最小 counter，
故所有已处理事件 happened-after (p, e) = v。
(c) **根死亡毒化**：某链在堆非空时死于根 r，则对其后任何候选 v：
v ≤ r 不可能（r 无祖先），r ≤ v 不可能（v 在 r 之后弹出 ⟹
lamport(v) ≤ lamport(r)，而 r → v 要求严格更大，L0），故 r ∥ v，
{v} 不 critical——必须放弃。裁剪死亡同理（链的延续未知，保守放弃）。
最晚性：扫描按 lamport 降序推进，首个满足条件的时刻即最高的切口。
**L12（入场检查的正确性）** *新区经由"入场 change"挂到旧历史上；
入场者看全了 L，其一切后代自动看全。*
设 IGU 候选成立（ans = L、无 uncovered）。定义入场 change 为新区中
因果父集（显式 deps ∪ 隐式同 peer 前驱）全部落在 Events(L) 内的
change。断言：新区每个事件 ≥ L 的全部头 ⟺ 每个入场 change 的父集
版本覆盖 L。
证明要点：（⇐）新区任意事件 e 沿因果链下行必经某入场 change c，
e ≥ c ≥ Events(父集) ⊇ L；（⇒）入场 change 自身是新区事件。
跨节点straddle 情形（节点前半旧、后半新）：多头 L 下节点中部的新 op
只有隐式父，其父若覆盖 L 全部头则该父 ≥ 每个头、又 ≤ 某头，
与反链性矛盾——故按节点起点父集判定与逐 op 判定等价。
**依赖图**：
S1 ← L4；S2 ← L5；S3 ← L9 ← {L3, L6, L7, L8}；T ← L10 ← L0；
S5b(C1) ← L3 + "无死路 ⟹ Max(C) 的每个成员被双侧到达"（未证，猜想）。
**引理与现有测试的对应**（代码一致性的桥）：
四套随机 oracle 测试 ≈ S1/S2/S3 的随机检验；
三个定向单测（trimmed、左多头、右多头）分别钉 L9 的三个分支；
criss-cross ladder 测试钉"tips 去重后复杂度线性"（性能声明，不进证明范围）。
---
## 6. 待定问题（需要维护者拍板）
- **Q1** 猜想 C1（无死路 ⟹ ans = 精确 meet）要不要写进规格？
现有 oracle 在 Checkout 模式下不检查精确性，纳入则需补测试。
- **Q2** Linear 的外延表述（"新区是 ≤-全序链且因果晚于 L"）
与差量计算器的实际假设是否一致？
- **Q3**（已部分解决，2026-08-01）movable tree issue 证明守卫公理对
Tree 不成立，故不再把守卫当作 IGU 正确性的依据：入场检查（L12）使
S3/S4 直接成立。守卫仍是 text/list 在 Checkout 模式下的兜底，其公理
化留给 Q7。
- **Q7**（已核查，2026-08-01：安全）Checkout 模式下 meet 非 critical 时
Tree 的 checkout_diff 是否一致？机制审计发现 Tree 的 Checkout 路径是
**相对**计算（retreat/forward 都按 lca 前沿的 change 起点 lamport 开窗，
窗外 op 静默跳过）——窗口隐含 critical 假设。但可证明修复后恒安全：
区域内经会合进入公共历史的 op 必 ≥ 某 meet 头（在窗口内）；与 meet 头
并发的 op 必产生 uncovered 死路 → L11 扫描 → critical 基准 → 窗口从
基准起点覆盖全区域。实证：非 critical meet 菱形（tree/movable list/
text）与低 lamport 并发分支两组 checkout 探针全部 canonical，已钉为
回归测试 `checkout_across_non_critical_meet_stays_canonical` 与
`checkout_with_low_lamport_concurrent_branch_stays_canonical`
（后者显式保护"扫描 ↔ Tree 窗口"的耦合：削弱扫描会静默破坏它）。
- **Q8**（已解决，2026-08-01：澄清而非改行为）深入推演后确认这是
**刻意的双模式设计**：顶层返回值是**方向模式**（origin），其唯一消费者
`DocState::apply_diff` 只用它做方向敏感的死容器缓存策略（Checkout 可能
倒退 → 全清；其余模式必为前进 → 只清 alive 标记），语义正确；逐容器的
`InternalContainerDiff::diff_mode` 才是**计算模式**（各计算器如实上报，
Persist 降级后亦然），`need_check`/`need_compare` 消费的是它，配套一致。
风险只在"易混淆"，已修：`calc_diff_internal` 内部局部量改名
`calc_mode`，两处消费点各加不变式注释。
- **Q9**（新，维护性）`find_path` 使用独立的旧版 `_find_common_ancestor`
实现（仅服务诊断 API `find_id_spans_between`，不参与状态变更；
relay 形状实证输出精确）。双实现存在漂移风险，建议择机合并或改为
vv 差集直接计算。
- **Q4** trimmed 情形：uncovered 但 ans 触及裁剪边界时保留非空 ans，
其安全性依赖 oplog 层把重放起点钳制到浅历史根部。
规格按"走查 + 钳制成对成立"写，还是要求走查单独成立？
- **Q5** Lean 先证**模型层**（本文档的数学对象），
Rust 代码一致性由穷举小规模 oracle 测试桥接——可接受，
还是希望直接做 Rust 代码级验证（Verus/Creusot，成本高得多）？
- **Q6** 三个快速路径：纳入证明范围，还是从代码中删除以换取更小的可信基？
其中"单-单同 peer"窥孔的证明要用到 A2 划分公理，是三者中最绕的。
---
## 7. 词汇表
| CRDT | 一类允许离线并发编辑、合并后自动一致的数据结构；本文档不依赖其细节 |
| peer | 一个参与编辑的副本/设备 |
| op（操作） | 一次不可再分的修改，编号 (p, c) |
| Change / 节点 | 同一 peer 连续操作的存储打包单位 |
| span / 段 | 节点的一个前缀切片，遍历的基本单位 |
| lamport | 逻辑时间戳：沿 happened-before 严格递增（a → b ⟹ lamport(a) < lamport(b)） |
| parents / deps | 事件的父事件集（论文记 e.parents；Loro 代码称 deps） |
| happened-before → | a → b：a 在 b 的因果过去（由早指向晚，Lamport 方向；Eg-walker §2.2） |
| ∥（并发） | a ∥ b ⟺ a ≠ b ∧ a ↛ b ∧ b ↛ a |
| Events(V) / Version(G) | 论文记法（§2.3）：版本的祖先闭包 / 因果闭子图的前沿，两者互逆 |
| V_crit | Eg-walker §3.6：合并的理论最优起点——发生在双方之前的最晚 critical version（Loro 已实现其单头近似，见 L11） |
| frontier / 前沿 | 用"最新端点"反链表示一个版本 |
| 反链 | 集合中两两互不为祖先 |
| 因果闭集 | 包含成员的所有祖先的操作集；与合法版本一一对应 |
| 版本向量 | 因果闭集的紧凑表示：每 peer 一个前缀长度 |
| C(L,R) | 两版本的公共历史 ancestry(L) ∩ ancestry(R) |
| meet 前沿 | C 的极大元反链——版本格最大下界；算法的候选起点（旧文借称 "LCA"，不严格） |
| critical version | 能把事件图一刀两断的版本（Eg-walker §3.5）；重放起点的合法性判据，∅ 平凡成立 |
| import / checkout | 导入远端更新 / 切换到任意历史版本 |
| 重放（replay） | 从起点按因果序重演操作以计算状态差 |
| tips / 牌子 | 路径携带的分岔点标记，用于死路的冗余性判定 |
| unmatched / 死路 | 未与对方会合而终止的路径 |
| uncovered | 存在牌子不在 ans 祖先集内的死路 ⟹ 真并发 ⟹ 保守回退 |
| trimmed / 浅历史 | 早期历史被裁剪，依赖可能指向不可用区 |