受限可靠流状态机

接收者不是按“包到达的次序”拼字符串，而是按包写明的位置补格子。确认报告连续填满到哪里。最后一段先到只会填后面的格子；缺口补上时，前缀可以一下推进很多字节。

重复包会再次触发确认，这正好修复“数据到了，确认没到”的情况。字节只追加一次与ACK可以发送很多次并不矛盾。

取 $X$ 为十六进制 00 03 43 41 54 00 02 4F 4B，$N=9,m=3$，三段依次为P0=[0,3)、P1=[3,6)、P2=[6,9)。发送者先发三段，因此 $n=9,u=0$。按以下轨迹复算：

只有第四步新增交付9字节；第五步没有第二份消息内容。数据发送共4次，含原始P0的丢失与一次重传；网络额外复制P1一次不算发送者调用。接收者发出4个ACK，其中一个丢失。这里不把三次“到达后段”理解成三个TCP重复ACK规则；R9没有Reno。

若最后ACK及以后所有ACK永久丢失，接收者可能早已完成，发送者仍无法确认完成。设定有限尝试上限可以让发送者退出，但返回只能表明“传输未获完整确认”；不能证明对端没收到，更不能回滚已交付前缀。若允许重启、旧流ID复用或位串篡改，本协议的证明前提失效，需要新增机制。

前缀安全为什么不依赖包的顺序 ​

采用归纳不变量理路不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。：每个已填格 $i$ 都等于 $X[i]$；输出恰为 $X[0:r)$；$r$ 是从0开始连续填满的最大末端；发送侧 $0\le u\le r\le N$ 且 $u\le n\le N$。初态显然满足。合法数据包只复制原位置的字节，推进循环只越过已填格，因此保持输出前缀。ACK由某个过去的 $r$ 生成，而 $r$ 单调，接受ACK便仍有 $u\le r$。丢失不改变端点状态，重复只重复填同值，乱序只改变哪些格先填。这逐类覆盖了全部事件。

什么时候能最终完成 ​

活性理路安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。另需公平条件：持续未完成时，发送者最终发出所有新段并持续重传最早未确认段；某个数据包若被发送无穷多次，就被交付无穷多次；同样规则适用于反向ACK；接收者持续处理并保留流状态。若 $u$ 永远停在某段起点，该段会反复到达，接收者最终产生至少越过该段末端的ACK。可取的ACK值有限，某个这样的值被发送无穷多次，最终到达，迫使 $u$ 前进，矛盾。有限个段依次推进，得到 $u=N$。公平性没有给完成时间上界。

位图与缓存占 $O(N)$ 空间。数组实现每个到达字节检查一次，前缀推进总共 $N$ 次；若累计收到 $D$ 个含重复字节的载荷字节，接收数据处理成本为 $O(N+D)$；若还计入A次独立ACK处理，则再加 $O(A)$，发送复制成本按实际发送载荷字节另计。无限丢失时通信量没有有限上界。有限窗口理路滑动窗口与接收方流量控制Sliding window flow control · Receive window · rwnd · Zero-window probing把已确认位置、已发送前沿和通告窗口分开，计算可新增发送量及零窗口恢复，说明接收消费而非ACK释放接收缓存。会进一步限制在途与缓存范围，但需要相应地改写发送规则，不能把本页的整流缓存假定悄悄删去。