spec: TLA+ 模型（统一事件协议、跨运行时同步、远程租约、行生命周期、调用生命周期、节点托管行） #613

属于 #183 第四步（EventsHost.tla 在"再做"，其余在"然后"）。对应质量规范 Q9.1.2、Q11.2、Q8.3、Q5.1.1；统一事件的协议规格 §四、§五、§七、§九；风险 EV1–EV4（#612）。

为什么

• 统一事件（统一事件：一个逻辑总线（实现） #464，0.13）是 0.10 以来最大的多方协议：监听器表分在宿主、各运行时和相连节点上，靠 events.on / events.off / events.elsewhere 同步；分发在运行时本地（快速路径）或经宿主进行，规格要求两条路径结果相同。Q9.1.2 要求这类协议在设计阶段完成模型检查后才定稿，这次没有做，两份设计稿里都没有模型检查。
• 定稿（2026-10-18）之后，协议规格又因实现中发现的问题改了十几次，多数是时序规则：emit 的回复按帧序就地接收（c2c1b7e8）；Node 同步等待期间对 emit 调用是就地执行还是扣住，同一天先改成就地（aa14b061），又改回扣住，并让快速路径上的 emit 排在被扣住的之后（a2748bf3）；排队的 emit 随行卸载丢弃（0.15 review(events): 排队 emit 缺少行归属，卸载不丢弃/取消；run_emit panic 卡住队列 #536）；rows.ended 与 events.* 按帧序处理（fix(bridge): rows.ended 与同一会话的 events.* 按帧的顺序处理 #587）；节点上先于提供到达的宣告（fix(events): 节点连接上先于提供到达的宣告，不被尚未列出这次提供的 link.offers 撤下 #593）；0.15.1 作用域从送达规则改为描述（migration-0.13: Process::emit 写成 parallel 会误导父子方向的迁移 #604、events: scope 下缺少向子树广播，Process::emit 没有等价替代 #605）。
• 这些问题都是审查、一致性用例和 nightly 偶发失败找到的（fix(events): 运行时按帧的顺序接收 emit 的回复，order-across-fast-path 第 2 步不再依赖时序 #513、fix(events): Node 按帧序就地开始 emit 方式的监听器调用，补同步等待用例、回复原语测试与文档 #520、fix(events): Node 保持不可重入，快速路径上的 emit 排在被扣住的同名调用之后；等待图记入口，修复可重入运行时上查不出的卡死 #527、fix(node): a related later emit waits behind an earlier held emit #557、fix(events): drop a row's queued emits when it ends #564、fix(swift): RutisApp 开始与停止按调用顺序、监听加升级时限、带过滤器的 emit 保持顺序（0.15 审查） #519、fix(swift): close a dialed connection and push filtered emits in order #554；nightly: 2026-10-21 失败 #530 里 2026-10-21 的 events-all order/、serial/ 失败）。事件的核心承诺目前都由测试验证（一致性套件 events.expected.json、库级测试、各语言自己的测试），检查的都是构造出来的时序；还没有能穷举交错的验证（Q8.3 举的"测试和模型检查"）。

先定下的一点：协议不承诺顺序一致

两个运行时各自登记同名的监听器，各自在 elsewhere 还没更新时走快速路径发出：每次分发只调用本进程的条目，任何与两个进程程序顺序一致的全序都排不出这两次分发。这是 §5.2 允许的。所以"一个逻辑总线"在模型里不写成对单表总线的精化，而是下面各条性质的合取：每次分发看到的条目有因果上的下界（RegisteredThenSeen）和上界（WithdrawnStaysOut），条目之间的先后处处一致（OneOrder）。协议规格 §4.4 和 guarantees.md 加一条"明确不保证"写明上面的情形，事件设计开头"结果都和所有监听器在同一个进程里一样"一句随之限定（Q5.1.1）；配置 sees-all（预期被违反）用 TLC 的反例记下它。

第二点：同一进程里并发的两次发出没有先后。 EmitOrder 只约束有先后的发出（同一线程的程序顺序，或经同步建立的先后）。Go / Swift / Kotlin 在锁内取快照、解锁后才开始监听器，两个并发的发出方在两个监听器上的顺序可以不同，这是允许的。协议规格 §5.5 补这一句。

模型：specs/events/

宿主部分写成 EventsHost.tla，按名字、行、会话、条目 id 的集合写；下面三个模块和 #616 共用它。EventsHost.tla 把宿主的规则按协议写全：名字与前缀的匹配；export / import 的匹配与收窄；五种方式何时开始下一个调用（emit、parallel 一起开始，serial、bail 等上一个的结果，waterfall 等上一个监听器调用 next）；过滤器对每个候选的真假。这些只是定义，不增加状态；三个模块的配置只用其中一部分，#616 用全的。宿主里 Rust 插件的登记、撤下与发出（含 rutis/*）是宿主的动作；等待环的拒绝（SyncWaitCycle）、取消、值发不出去是"可以发生"的选择，不由宿主模块判断。每个模块只含它的性质需要的动作。每个会话每个方向按序送达，延迟任意。

运行时的规则分三种：R1 = Node（不可重入，同步等待时扣住）；R2a = 读到帧就开始调用、同一个监听器的调用可以在 await 处交叠（Python、Bun）；R2b = 每个监听器一个串行队列、一次调用跑完才开始下一次（Go、Swift、Kotlin）。两个运行时规则不同，不用 SYMMETRY。

R2a 对 Python 成立有一个前提：现在 Python 只原地处理 return / throw / cancel / release，events.call、events.elsewhere 都用 call_soon 推迟（peer.py 约 1375 行；runner.py _invocation 的注释说"下一帧读之前就开始"，代码没做到），emit 的回复却原地处理。配置 python-deferred 按现在的做法建，预期违反 EmitOrder 或 FastPathByFrame；修复后改为通过。TLC 若找不到反例，这条疑点不成立，配置改为通过。

因果用幽灵变量记：每个进程和每条在途的帧带一个"已知的登记与撤下"集合。进程自己登记时加入的项只在本进程里算（程序顺序），不随帧传出去；宿主接受登记、处理撤下时加入的项，随宿主之后发出的帧传给别的进程；进程撤下（含发出 rows.ended）时加入的项，随它之后的帧传出。收帧时并入。

配置里不出现（EventsHost.tla 里有定义，三个模块的配置不用）：前缀条目；export / import 的匹配与收窄；过滤器对单个候选的真假（配置里只有"全部保留，可能迟到"和"永不回答"）；parallel、bail、waterfall（配置里方式只有 emit 和 serial，后者代表"一次开始一个调用"的方式）。

不建模：rows.update（等价于撤下再登记）；next 只能调一次之类的单进程规则（Q11.2.2）；值、错误内容、AggregateError 的聚合（一致性套件覆盖）；作用域（0.15.1 起只是过滤用的描述）。同步方式 bail、waterfall-sync 与等待环检测在 #614。

性质

修复前的配置

模型在这些开关下必须找到反例，说明它抓得住已经发生过的问题：

现在的实现里的疑点（预期被违反；TLC 找不到反例则疑点不成立，配置改为通过）：

另外，每个性质配一个故意引入的错误（变异），做法同 remote-lease。

待复现的疑点（模型之外，用测试确认）

• Node 的 behind 任务在发出它的行卸载时不丢弃（events.mjs 约 335 行交给 session.behind；session.mjs 只在 close()（约 191–198 行）丢弃排队的 behind 任务）。
• Bun 的过滤器在同步调用里会泵帧，嵌套的较晚 emit 先开始。
• Node / Bun / Python 的过滤器若是异步的（返回 Promise / 协程），被当作全部保留，不报错：按 docs(spec): 多语言运行时、同步调用、挂载、事件与值的规格按代码修订 #637，rutis 自己的 filter(predicate) 改为这次分发失败（Cordis 的 Context.filter 照 Cordis）。

规模与运行

• 每个模块先只开一个动作族跑最小配置，再逐个打开；README 记下每一步的状态数。PR 上的配置每个模块 1 分钟以内，超出的放每周的运行（ci(nightly): 每天全量跑 install/dylib/specs/sdk-repro/events，频率过高 #576）。
• events/run.sh 要认死锁（"不卡住"）、不变式与通过（cross-runtime-sync 的 run.sh 认这三种；remote-lease 的认时序性质、不认死锁）。

对应的实现

产出

• specs/events/：EventsHost.tla、EventsTable.tla、EventsEmit.tla、EventsLink.tla、.cfg、expected.txt、run.sh、README（中英：对应的设计、简化、性质、结果、每步的状态数）
• 七个修复前的配置都找到反例；每个性质一个变异；sees-all 的反例写进 README
• 协议规格 §4.4（中英）与 guarantees.md 加"明确不保证"，事件设计（中英）开头那句随之限定；上表"随模型补登记"的两条登记进 guarantees.md，其余各条的验证一列加上模型
• TLC 找到的新反例：修复，并转成 rutis-bridge/tests/event_hub.rs 的测试或 events.expected.json 的用例（所有运行时和测试工具都跑）
• python-deferred、accept-unlocked 的结论：属实的修复（Python 改为原地处理 events.*；accept() 三步在一个临界区里），配置改为通过
• 协议规格 §5.5 补"并发的发出没有先后"
• 上面三条模型之外的疑点确认，属实的修复并加测试
• CI specs 任务的矩阵加 events；specs/README.md 的表加一行

追踪表中归本 issue 的规则（#634）

范围是下面这些规则的全部，不只是正文举出的几条，共 87 条。完成时，应有形式化检查的规则在追踪表里都是"已覆盖"（形式化检查通过，并有变异或修复前的配置证明它不是空的；一致性用例写上用例名）；只靠测试的写上测试名、保持"不适用"；改为其他手段的写明理由。

这次补进来的：EVP-9-17（不带 epoch 的宣告 id 只按 id 替换），EventsLink 要加。规格的修订（Swift / Kotlin、作用域残留、rutis 的 filter(predicate) 不接受异步谓词）在 #637，模型照修订后的规格建。

• 登记表 §6–§8a（13）：events/order a、events/presence a、events/presence b、events/hub-dispatch a、events/hub-dispatch b、events/hub-flat b、events/hub-lifecycle a、events/hub-lifecycle b、events/hub-lifecycle d、events/node-links c、events/node-links d、events/one-bus a、events/no-multi-hop
• 登记表 §9–§15（11）：sdk/leaf-events a、sdk/leaf-events b、events/bun-runtime、events/emit-order、events/liveness、events/node-runtime、events/registration、events/table-watch、events/unload、events/via-host、events/withdrawn
• 事件（56）：EVP-4.1-2、EVP-4.1-5、EVP-4.1-6、EVP-4.3-1、EVP-4.3-4、EVP-4.4-1、EVP-4.4-2、EVP-4.4-3、EVP-4.4-4、EVP-4.5-1、EVP-4.5-2、EVP-4.5-3、EVP-5.1-1、EVP-5.1-3、EVP-5.2-1、EVP-5.2-2、EVP-5.2-4、EVP-5.3-14、EVP-5.4-1、EVP-5.4-2、EVP-5.5-1、EVP-5.5-2、EVP-5.5-4、EVP-5.5-5、EVP-5.5-6、EVP-5.5-7、EVP-5.5-9、EVP-5.5-10、EVP-5.5-11、EVP-5.5-12、EVP-5.5-13、EVP-5.5-14、EVP-5.5-15、EVP-5.5-16、EVP-5.5-17、EVP-5.5-18、EVP-5.5-19、EVP-5.5-20、EVP-7.1-1、EVP-7.1-2、EVP-7.1-3、EVP-7.1-8、EVP-7.2-1、EVP-7.2-2、EVP-7.2-4、EVP-9-4、EVP-9-8、EVP-9-13、EVP-9-14、EVP-9-15、EVP-9-16、EVP-9-17、EVP-9-21、EVP-15.29-1、EVD-1-1、EVD-1-2
• 远程（7）：REM-5.1-7、REM-5.2-10、REM-5.2-11、NOD-3-2、NOD-3-4、NOD-3-5、NOD-3-7

并入 #614：spec(cross-runtime-sync): 模型跟上等待图的修改（#561、#597）、每个调用一个线程的运行时和事件的同步方式

属于 #183 第四步（然后：按协议覆盖全部规则）。对应质量规范 Q11.2.3（设计修改时，模型同步修改）；模型；多语言设计 §九；风险 EV5（#612）。

为什么

• 为修 0.15 review(events): 等待图对同步/异步/控制调用的分类不准，慢路径丢链 #537，fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561 和 fix: 0.15 review 剩余项（等待图、清单生命周期、服务重名、Swift、Node、host dev） #597 改了 waits.rs 的等待图：慢路径 spawn 之后保留调用链、取消一个已经在运行的同步调用时保留标记（fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561）；宿主自己发起的同步调用即使没有调用链也记为一跳（fix: 0.15 review 剩余项（等待图、清单生命周期、服务重名、Swift、Node、host dev） #597）；已标记调用链上转发的调用一律记为一跳（854bef5d；经 unchained 的通知、回到来源会话的调用不记）。多语言设计 §九 跟着改了取消的规则（fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561），fix: 0.15 review 剩余项（等待图、清单生命周期、服务重名、Swift、Node、host dev） #597 的规则还没写进去；模型没有改（最后一次修改是 fix(bridge): 等待图的入口是调用链的边界（修复误报 SyncWaitCycle），检查近线性；补 Node 监听器时机的例外说明 #535 的 6488c8c）。
• 0.15 review(events): 等待图对同步/异步/控制调用的分类不准，慢路径丢链 #537 的分类（含宿主自己的同步调用）与取消两类问题，落在模型写明不覆盖的地方：README 的"简化"里有"运行时发出的调用都是同步的"和"取消、会话关闭不建模"，"待定"里有"Rust 自己发起的同步调用"。慢路径丢链则是实现没做到模型的前提（投递带着发出方的调用链）。
• 模型里的运行时都是一个调用栈（声明 sync-stack）。Go、Swift、Kotlin 声明 reentrant-sync 和 sync-wait，不声明 sync-stack：每个进来的调用在自己的线程上执行，策略 B 对它们不加"放到一边""栈顺序"两类边（waits.rs 的 Profile.stacked = false）。这一类没有建模。
• 统一事件加了两种同步分发：bail 和 waterfall-sync（next 是指回分发方的同步回调），它们像同步服务调用一样参加等待环检测（协议规格 §5.4）。模型里的事件只有 emit 的投递（MaxPosts）。

改动

每一项单独一个配置，MaxRoots = 2、MaxDepth = 3，不与 posts 叠在一起。Workers 除 policy-b-workers1 外都取 MaxRoots，线程数不成为卡死的原因。

• 每个调用一个线程的运行时：常量 Threaded，这些运行时上每个进来的调用在自己的线程上执行，RustSucc 对它们不加"放到一边""栈顺序"两类边。配置 policy-b-threaded（n、g、p）检查不死锁与 NoFalseCycle。
• 宿主作为参与者：执行 Rust 插件代码（Rust 服务、同步监听器、bail 的分发、Rust 自己发起的同步调用）的线程，个数是常量 Workers；读线程不算（events/hub-dispatch）。同步等待占着线程；链上的进来调用交给等待的线程（M1 §7.2），不在链上的要空闲线程，没有就排队。宿主自己发起的同步调用（path 为空）是一跳。Workers = 1 的宿主相当于一个不可重入的参与者；策略 B 不为宿主自己的线程建边（waits.rs 只按会话的对端记 Profile，进 Rust 服务的调用不是一跳），所以 policy-b-workers1 预期卡死，反例写进 README（例：Rust 的顶层调用同步调用可重入的 p 的 x，x 同步调用 q；这时另一个运行时 r 自己同步调用 p 的服务 s2，p 在等，把 s2 嵌套在 x 上执行；s2 同步调用 Rust 服务 S。S 不在前者的链上，要一个工作线程，而唯一的那个被占着；x 要等 s2 返回才能继续）。多语言设计 §九 和插件 API 文档写明（明确不保证，Q5.1.1）：Rust 代码同步等待时占着一个工作线程；同时进行的这种等待占满工作线程、其中一条又在等一个不在它链上、要新线程的进来调用时会卡住，SyncWaitCycle 不检测。按实现核对 Rust 服务在哪个执行器上执行、同步调用是否占着它的线程；不占时这一项从"待定"删掉，配置改为预期通过。
• 事件的同步方式：bail、waterfall-sync 建成宿主参与者上的一次执行：每个监听器调用是同步的 events.call，next 是回到宿主这条链上的调用。
• 异步等待结果的分发：宿主参与者上的执行还有 serial（代表 parallel / waterfall）：在一个已标记的调用之下执行（例如 Rust 服务处理一个运行时的同步调用时分发），每个监听器调用是异步的 events.call，执行等它的结果；开始第一个调用之前可以挂起一次（过滤器）。
• 调用的分类按现在的 waits.rs 建模：同步调用（sync: true）记为一跳；调用链末尾是已标记的调用时，异步调用也记为一跳（854bef5d）；其余的异步调用在有调用被标记时记为入口。运行时在处理一个已标记的调用时发出的异步调用分两种：结果要等的（await 之后才返回），是真实的等待边；发出即不管的，没有边。854bef5d 把两种都记为一跳，模型两种都建。控制通知（经 unchained 发出）不在任何栈上、不发起调用，不建模。"已标记链上的异步调用记为一跳"若违反 NoFalseCycle，就是现有的缺陷：修实现并加测试。
• emit 的调用链：fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561 写明 emit 的过滤器和监听器调用在总线的任务上执行、不带调用链。main 上分三种：运行时发出的 emit，在读线程上就地开始、发往其他会话的调用带着发出方的调用链；发回发出方自己会话的调用从不带（caller_of）；宿主 Rust 插件经 Bus::emit_erased 发出的不带（fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561）。模型的 RustPost、waits.rs 的模块说明（"an events.call carries its emitter's chain"）和多语言设计 §九 都说带着。按这三种逐一核对：实现对，就改模型、waits.rs 的说明和 §九，重跑 policy-b-posts*；模型对，就修实现并加测试。
• 取消：调用方取消一个同步调用时，被调用方可能已经开始执行；标记保留到这个调用真正结束；调用方取消之后迟到的 ret 被丢弃（否则通道被堵住，TLC 报出假的死锁）。
• 对应表补 Go、Swift、Kotlin：go/rutis/internal/peer/peer.go、swift/rutis/Sources/Rutis/Session/Peer.swift、kotlin/rutis/rutis/src/shared/kotlin/arcships/rutis/internal/peer/Peer.kt（现在 Go 不在表里）。
• 本地放弃的同步调用：Go（ctx 取消）、Swift（Task 取消）、Kotlin（中断）放弃一个同步调用时不发 cancel，宿主留着这条等待边。模型加"调用方在本地放弃"的动作，检查 NoFalseCycle；被违反就让这三种运行时放弃时发 cancel。
• Python 从别的线程发起的同步调用：经 run_coroutine_threadsafe，不带 sync 标记，宿主看不见这条等待。模型里作为宿主看不见的边，检查不死锁；被违反就让它带上标记，否则写成明确不保证。
• Node 的细节：按键扣住（同键的 emit 调用不越过更早的）、behind 任务不在等待之上运行、等待链上对未完成 promise 的 await 得到 SyncWaitCycle、原地处理的帧。现在模型里的 Node 只有"只执行链上的，其余放到一边"。
• Cordis 节点的连接会话：没有原地处理和扣住，每个 connector 一个泵；在一条连接上等待时不读别的会话，形成宿主看不见的跨会话等待。模型加一个这样的参与者；成环时宿主查不出，就写成明确不保证。
• 跨主机的环：经节点连接跨两台主机的环，每台的等待图只看见自己那一段，检测不到。模型不建，写进多语言设计 §九 和 bridge/sync-wait-cycle-refused 作为明确不保证。
• 运行时一侧的有界线程池（Kotlin 的 IO 池 64、Swift 的协作池）不建，README 的"简化"写明。
• 新性质 MarkedWhileRunning：宿主收到、由 Rust 代码执行的同步调用，在它真正结束之前一直被标记；所以它之下发往其他会话的同步转发都是带调用方的一跳（发回来源会话的不记，同 waits.rs）。原有的性质（不死锁、RoutingSound、ChainRecognised、NoFalseCycle）不变。

修复前的配置

产出

• CrossRuntimeSync.tla、新配置、expected.txt、README（中英）："对应的设计和代码"补 waits.rs 的分类、Profile、取消，events/hub.rs 的 bail 分发；"简化""待定"按上面更新；每个新配置的状态数
• before-lost-chain、before-cancel 找到反例，before-host-call 预期通过、README 写明原因；三者与 fix(bridge): keep wait-graph marks across slow dispatches and cancels (#537) #561、fix: 0.15 review 剩余项（等待图、清单生命周期、服务重名、Swift、Node、host dev） #597 的测试（session/rpc/tests.rs、session/rpc/waits.rs、rutis-loader/tests/sync_cycles.rs）一一对应
• TLC 找到的新反例：修复并加测试；结论写回多语言设计 §九（中英），包括 fix: 0.15 review 剩余项（等待图、清单生命周期、服务重名、Swift、Node、host dev） #597 的规则（宿主自己发起的同步调用是一跳）和上面三条明确不保证
• cycle_among 的差分属性测试：与按模型 RustSucc 的定义建全部边、再做 DFS 的朴素实现比较（约 20 跳的随机图、随机 profile）
• 等待图的 trace validation：记录 waits.rs 的六个操作（profile、marked、answered、returned、ended、forward）与每次判定，在 sync_cycles.rs、rpc_callbacks.rs 的运行上对照模型（做法同 spec(events): 用 events-all 运行中宿主的动作日志做 trace validation #616、test: trace validation 与一致性套件补列（events-all 的宿主动作日志、接入点、Swift / Kotlin / Go / Bun 列） #624）

依赖 #624：sync_cycles 的 Kotlin 列。

追踪表中归本 issue 的规则（#634）

范围是下面这些规则的全部，不只是正文举出的几条，共 57 条。完成时，应有形式化检查的规则在追踪表里都是"已覆盖"（形式化检查通过，并有变异或修复前的配置证明它不是空的；一致性用例写上用例名）；只靠测试的写上测试名、保持"不适用"；改为其他手段的写明理由。

这次补进来的：SYN-9-3（可重入运行时的服务可能在它自己的同步调用中途被调用：加一条预期被违反的性质锁定，同 NeverCycle）；SYN-9-26（未声明 sync-wait 的运行时不计入等待图：明确不保证，加配置锁定）；SYN-9-30（会话结束时它的调用全部从表里移除：模型加会话结束）。§九 的文字按代码重写在 #637。

• 登记表 §6–§8a（4）：events/serial-bail c、boundary/5.6、events/hub-dispatch c、events/hub-bail b
• 登记表 §9–§15（5）：bridge/sync-wait-cycle-refused a、bridge/sync-wait-cycle-refused b、bridge/sync-wait-cycle-refused c、events/remote-sync、events/session
• 事件（10）：EVP-5.3-1、EVP-5.3-4、EVP-5.4-12、EVP-5.4-13、EVP-5.4-19、EVP-6-5、EVP-7.2-3、EVP-11-6、EVP-12.1-7、EVD-1-2
• 会话（5）：TAG-5-3、M1-5.3-4、M1-7.2-3、M1-7.2-5、M1-7.2-6
• 运行时（28）：SYN-5-13、SYN-9-1、SYN-9-2、SYN-9-3、SYN-9-5、SYN-9-6、SYN-9-7、SYN-9-8、SYN-9-9、SYN-9-10、SYN-9-11、SYN-9-12、SYN-9-13、SYN-9-15、SYN-9-17、SYN-9-18、SYN-9-24、SYN-9-25、SYN-9-26、SYN-9-27、SYN-9-28、SYN-9-30、SYN-9-31、SYN-9-32、MNT-3-15、MNT-5-9、MNT-11-6、REQ-5-6
• 远程（5）：REM-6.2-4、REM-6.2-10、REM-6.2-11、REM-6.2-15、REM-6.3-4

并入 #615：spec(remote-lease): 对应表补 Swift / Kotlin，加停止后再开始和故障之后的活性

属于 #183 第四步（然后：按协议覆盖全部规则）。对应质量规范 Q11.2.3、Q6.13.3；模型；风险 AH1、AH2（#612）。

为什么

• 模型 README 的"对应的设计和代码"：接管顺序一行列了 Python / Go / Node（Bun 写"同"）；拨出规则只列 Python，Go / Node / Bun 只写"同样的规则"。0.15 的 Swift、Kotlin（插件运行时和 iOS / Android 应用托管）各自实现了监听端的接管顺序和拨出方的再拨规则（swift/rutis/Sources/Rutis/Remote/Listen.swift、Dial.swift；kotlin/rutis/rutis/src/shared/kotlin/arcships/rutis/internal/remote/Listen.kt、Dial.kt、Dialing.kt），没有对照模型核对过。0.15 的审查在这一层修了多处开始、停止与连接的问题（fix(swift): RutisApp 开始与停止按调用顺序、监听加升级时限、带过滤器的 emit 保持顺序（0.15 审查） #519、fix(kotlin): 监听的写有时限且不阻塞读与心跳、主线程拒绝经 rutis 的 bail、拨出心跳按配置超时等（0.15 审查） #521、fix(swift,go): 监听的 stop() 等端口释放后返回、swift_app 读完所有行再看状态；放开的过滤器不报告，Go 的 On 不再 panic #532、fix(swift): close a dialed connection and push filtered emits in order #554）。
• 应用托管让"停止"不再是终态：RutisApp 停止之后可以再开始（比如回到前台）。模型里控制方 link 与拨出方的停止是终态（StoppedStaysDown）；接入点的停止再启动已经建模。
• Cordis 应用作节点的连接（node/rutis-runtime/src/bridge/link.mjs）自带一套退避常量（500 ms、30 s、稳定 60 s、被拒 30 s）和接管逻辑，也不在对应表里。
• Node / Bun 的 serve 在接管时 5 秒后强杀旧子进程（serve.mjs 约 103 行、remote.ts 约 179 行），短于清理截止时间（默认 10 秒），旧租约的清理会被截断；模型把清理当成瞬时的。
• 活性只在没有故障的运行里检查；"瞬时故障过去之后，最终有人持有租约"没有检查。

改动

• 对应表加 Swift、Kotlin、Cordis 节点的连接，拨出规则逐个语言列出（Go dial.go、Node dialing.mjs、Bun dialing.ts、Swift Remote/Dial.swift、Kotlin internal/remote/Dialing.kt、Cordis 节点 bridge/link.mjs），逐条核对：远程插件 §4.4 的接管顺序（鉴权 → 关闭旧会话 → 清理旧租约 → 回应新 hello）；停止时取消重试；按失败类型等待（被吊销、4003 按认证失败等待，其余退避）。不一致的按 spec: TLA+ 远端租约接管、重连与吊销（#210） #432 的做法处理：模型里加修复前的配置，修复实现，加测试。
• 停止后再开始：拨出方和监听端可以停止之后再开始（次数有限）。再开始时拨号次数和连接编号从头数，连接记为 <<c, 轮, n>>。监听端停止：关闭当前会话和排队的连接、清理租约、不再接受。StoppedStaysDown 的幽灵标记按轮记。新增 RestartIsFresh：控制方 Ready、拨出方 connected、监听端正在服务的连接，都属于各自当前这一轮；变异：按编号匹配握手结果，不看轮次。
• 清理有截止时间：模型里清理旧租约改为"开始清理 → 完成，或超时被强杀"两步，检查强杀时 OneLease、OldCommandsStayOld 仍成立。实现上 Node / Bun 的强杀改为跟随 RUTIS_SHUTDOWN_TIMEOUT 加 2 秒（与 Go / Swift 重启时的做法相同）。
• 新连接的心跳：Kotlin 接管时，新连接的心跳把等待旧清理的沉默也算进去，心跳超时 ≥ 30 秒时新连接被 1001 断开。改为从回应 hello 起算。
• 故障之后的活性：拨号失败、断线（瞬时故障）总数不超过 MaxFaults；额度只算建立成功的连接，因故障而重拨的那一次不计，所以额度用完时，最后建立的连接还在，或者因故障断开后还能再拨一次。在这些配置上检查 EndsHeld，不用 SYMMETRY（TLC 带对称时检查活性可能漏报）；规模取每方 2 次成功连接、MaxFaults = 2，不开吊销与停止。

产出

• README（中英）的对应表和核对结论
• RestartIsFresh 与它的变异；故障之后的活性配置；expected.txt；状态数
• 核对出的不一致：修复前的配置、修复、测试
• Node / Bun 强杀时间、Kotlin 心跳起算点的修复与测试
• 疑点确认，属实的修复并加测试

依赖 #624：leases 的 Swift / Kotlin 列。

待复现的疑点

• Kotlin RutisApp（RutisApp.kt:142-144）：run(previous) 在 join 之后才读 current。start / stop / start / stop / start 下，被取代的线程服务最新一轮，最后一次 stop 之后还多拨或多绑一次，违反 StoppedStaysDown / RestartIsFresh（用 test: 非 Rust 运行时的可控调度与静态检查（Kotlin Fray / Lincheck、Swift 严格并发与 TSan、Python 可控事件循环、JS 帧泵、Go 显式闸门） #630 的 Fray 模型复现；确认与修复在本 issue）。
• Swift 停止之后才到的 .accepted 连接没有关闭。

追踪表中归本 issue 的规则（#634）

范围是下面这些规则的全部，不只是正文举出的几条，共 55 条。完成时，应有形式化检查的规则在追踪表里都是"已覆盖"（形式化检查通过，并有变异或修复前的配置证明它不是空的；一致性用例写上用例名）；只靠测试的写上测试名、保持"不适用"；改为其他手段的写明理由。

这次补进来的：CHN-7-4（Incompatible 时控制方 link 停止自动重试）；REM-7-5（承载验证身份，权限与拨号方向无关）；静态监听 link 一组——DIA-3-2、DIA-5-13，以及 bridge/revocation-closes-only-its-connections a、CHN-1-4、CHN-8-5、CHN-8-8、REM-3.2-5、DIA-5-7、DIA-5-10 中静态 link 的一半（rutis 监听、运行时或对端拨入；接管先 old.end() 再 start；吊销后保留注册、处于 Waiting { AuthRejected }；移交之后才发现吊销时以 4003 关闭）：加一份配置，不再只当接入点的特例；DIA-5-11（吊销后以这个 id 打招呼的连接在 hello 之后以 4003 拒绝）；INS-5-3、INS-6-3（实例里的节点连接：同一对端不同时接受同一节点的两条连接；随实例关闭断开、导入的服务撤销）。DIA-6-3、6-5、6-6、6-7 缺的拨出分类用例在 #639。规格修订在 #636，模型照修订后的规格建。

• 登记表 §9–§15（6）：bridge/dial-out-rules g、bridge/revocation-closes-only-its-connections a、loader/remote-runtime-lease a、loader/remote-runtime-lease b、swift/app-start-stop a、swift/app-start-stop b
• 会话（10）：CHN-1-4、CHN-5-6、CHN-6-3、CHN-6-5、CHN-6-6、CHN-7-4、CHN-7-7、CHN-8-5、CHN-8-8、CHN-10-10
• 运行时（3）：REQ-8-2、INS-5-3、INS-6-3
• 远程（36）：REM-1-4c、REM-1-4d、REM-2-3、REM-2-4、REM-3.1-2、REM-3-2、REM-3-5、REM-3.2-4、REM-3.2-5、REM-3.2-8、REM-4.4-1、REM-4.4-2、REM-4.4-4、REM-4.4-5、REM-4.4-6、REM-4.4-7、REM-4.4-8、REM-4.4-9、REM-4.4-11、REM-7-5、DIA-3-2、DIA-5-7、DIA-5-10、DIA-5-11、DIA-5-13、DIA-6-3、DIA-6-5、DIA-6-6、DIA-6-7、DIA-6-8、DIA-6-9、DIA-6-10、DIA-6-17、APP-4-1、APP-4-3、NOD-1-1

并入 #625：spec: 用 TLA+ 验证宿主与运行时之间的行生命周期（代次、rows.ended、拒绝、服务公告、宿主服务租约）

属于 #183 第四步（规格一项在"先做"，其余在"然后"）。形式化覆盖图 T4（#612）；规范 Q11.2、Q9.1.2。

为什么

宿主和运行时之间的"行"有一套跨进程的规则：宿主按代次装载、卸载一行，运行时回报行结束、拒绝撞名的服务、宣布服务，宿主为行租用宿主服务。这些规则只写在代码里，没有设计模型，也没有成文的规格。修过的缺陷约 10 个，多数是一条跨代次规则被补进来：

• a88fb65：Node 的行按代次记，迟到的 rows.ended 只结束它自己那一代；
• 54a7e82：装载中结束的行，等装载成功后才报告；
• d94aae9：撞名拒绝只让它引起的那次重启失败；
• 6f8fb5c：行在和运行时一起解析完之前保持过期，不在临时解析上装载；
• 2f830f8：Python 线程里宣布的服务也等宿主答复后才回 rows.load；
• rutis-runtime: a Node row whose plugin disposes its own fiber keeps reading as Running(Active) on the host #247（自行 dispose 的 Node 行在宿主上仍是 Running）、flaky: signals::a_signal_while_starting_ends_the_host 偶发在启动完成前已打印行状态 #314（runtimes_ready 早于运行时放行行就返回）、flaky: bun_runtime::an_edited_plugin_is_imported_again 偶发等不到服务撤下（投影在发布中途关闭时丢掉撤下） #372（投影在发布中途关闭时丢掉撤下）、runtime: a row with loader inject hides its plugin's apply failure (gate fiber) #584（带 inject 的行藏住了 apply 失败）、e2e(S7): Rust 应用嵌入与多租户实例——创建、编辑、关闭、重启恢复 #191（语言行卸载后留下投影任务和导出槽）。

先把这些规则写成规格，模型照它建，穷举它们之间的交错；历史缺陷用作"修复前"的配置。

模型：specs/row-lifecycle/

参与者：宿主的加载器（一行的代次、两阶段解析、拒绝记录、服务投影、宿主服务租约）；一个运行时进程（它的行表；可以崩溃并以新会话重启）；会话两个方向各自按序、延迟任意。

动作：rows.load（带代次）、rows.unload、运行时报告 rows.ended、运行时宣布 / 撤下服务（带版本）、宿主拒绝撞名的服务、hosts.provide / hosts.withdraw（租约）、行重启、运行时崩溃与重启、依赖出现与消失、解析从临时变为确定。

性质

修复前的配置：before-generation-key（a88fb65b 之前，不按代次记行）→ OwnGenerationOnly；before-ended-during-load（54a7e824 之前）→ OwnGenerationOnly；before-refusal-scope（d94aae9a 之前）→ OwnGenerationOnly；before-stale（6f8fb5c7 之前）→ NoProvisional；before-thread-announce（2f830f81 之前）→ ServicesBeforeRunning；before-projection-close（#372 之前）→ NewerWins。每个性质另配一个变异。

简化：一行加一个运行时；运行时的行处理按 Node 的规则（单线程、按帧序），其余语言的差异写进对应表；事件的登记与 rows.ended 的帧序在 #613，这里不重复。

对应的实现

宿主：crates/rutis-loader/src/runtime.rs（JsRow、代次、Refusals）、runtime/rows.rs；crates/rutis-bridge/src/runtime/process.rs（Imports、行的记账、租约）、projection.rs、rows.rs。运行时：node/rutis-runtime/src/runner.mjs、bun/rutis-bun/src/runner.ts、python/rutis/rutis/runner.py、go/rutis/runtime.go、swift/rutis/Sources/Rutis/API/Runtime.swift、kotlin/rutis/rutis/src/shared/kotlin/arcships/rutis/internal/Runtime.kt。

相关的疑点（读代码推出，未复现；建模时逐条确认）

• Process::lease() 在等 hosts.provide 时被丢弃（行重启或 dispose），计数留在 1、没有 HostLease，服务永不撤下，之后同 id 的租约跳过 hosts.provide。
• 运行时一侧：Go 的 tasks.Wait() 没有截止时间，晚到的 Ctx.Go 与 Wait 竞争；Kotlin 卸载清理没有总上限；Swift 在 dispose 快照之后到达的 rows.load 泄漏这一行；Python 线程里的 ctx.on / provide 与卸载是先查后做；Node 第二次 unload、endRow 或 dispose 不等已在进行的卸载；Bun 的 update 不发 events.off（现在只在 Cordis 的 volatile 字段上触发）。

完成

• 规则写成规格：多语言设计或一份新的行协议说明（中英），guarantees.md 的 loader/ 条目验证一列加上模型
• specs/row-lifecycle/：.tla、.cfg、expected.txt、run.sh、README（中英：对应的设计和代码、简化、性质、结果）
• 六个修复前的配置都找到反例；每个性质一个变异
• 上面的疑点逐条确认：属实的修复并加测试（宿主一侧进 rutis-loader/tests/runtime_rows.rs，运行时一侧进各语言的 row contract 测试）
• CI specs 矩阵加 row-lifecycle

追踪表中归本 issue 的规则（#634）

范围是下面这些规则的全部，不只是正文举出的几条，共 88 条。完成时，应有形式化检查的规则在追踪表里都是"已覆盖"（形式化检查通过，并有变异或修复前的配置证明它不是空的；一致性用例写上用例名）；只靠测试的写上测试名、保持"不适用"；改为其他手段的写明理由。

这次补进来的：SYN-2-14 与 loader/runtimes-do-not-wait-for-each-other（运行时之间不互相等待，几个运行时同时冷启动各自就绪）、SYN-4-4（一个运行时崩溃，其他运行时、挂载与不用它的行照常）：模型从"一行加一个运行时"扩到两个运行时；SYN-4-8（只改易变字段时就地 rows.update）；MNT-4.2-3（服务公告在同步调用链内到达时，在调用返回前处理）；REM-4.3-3（解析刷新在独立任务里，不在进行中的 reconcile 内同步等待）。REM-5.1-3、REM-5.3-5（节点托管行）改归 #640；M1-5.1-3、M1-14-1、M1-14-9（方法形状的推断）是一致性用例，改归 #639；SYN-2-13、SYN-5-2 的跨语言一致那一半也在 #639。

• 登记表 §6–§8a（2）：boundary/5.1a、boundary/5.8e
• 登记表 §9–§15（15）：bridge/exported-services d、bridge/caller-row a、bridge/caller-row b、loader/rows-gate-on-services b、loader/rows-gate-on-services c、loader/announced-services b、loader/announced-services c、loader/runtimes-do-not-wait-for-each-other、loader/runtime-down-stops-its-rows、loader/row-unload-leaves-nothing b、loader/row-unload-leaves-nothing c、loader/self-dispose b、loader/gated-row-failure、loader/instance-close-leaves-nothing、loader/remote-runtime-rows
• 事件（2）：EVP-7.1-4、EVP-7.1-7
• 会话（22）：M1-5.2-1、M1-5.2-2、M1-5.3-1、M1-5.3-2、M1-5.3-3、M1-5.3-5、M1-5.4-2、M1-5.4-3、M1-5.4-4、M1-5.4-5、M1-5.4-6、M1-6.1-1、M1-6.2-1、M1-6.2-2、M1-6.2-3、M1-6.2-4、M1-14-2、M1-14-3、M1-14-4、M1-14-8、CHN-5-1、CHN-6-5
• 运行时（38）：SYN-2-13、SYN-2-14、SYN-2-15、SYN-2-16、SYN-4-2、SYN-4-3、SYN-4-4、SYN-4-6、SYN-4-7、SYN-4-8、SYN-4-10、SYN-5-2、SYN-5-5、SYN-5-8、SYN-5-9、SYN-5-10、SYN-6-1、SYN-6-3、SYN-6-4、SYN-11-1、M2-2-4、MNT-4.1-2、MNT-4.2-2、MNT-4.2-3、MNT-5-6、MNT-5-8、MNT-6-1、MNT-6-8、REQ-1-2、REQ-4-2、REQ-5-1、REQ-5-8c、RTP-2-6、RTP-2-9、RTP-2-12、INS-4.2-5、INS-4.2-6、INS-6-2
• 远程（9）：REM-3-4、REM-4.2-3、REM-4.2-4、REM-4.2-5、REM-4.2-6、REM-4.2-11、REM-4.3-2、REM-4.3-3、REM-4.3-4

并入 #626：spec: 用 TLA+ 验证调用生命周期（取消、计数释放、关闭、读线程写回），定下取消之后的回复规则

属于 #183 第四步（然后：按协议覆盖全部规则）。形式化覆盖图 T5（#612）；规范 Q11.2；风险 P4、P6、C4。

为什么

会话上的一次调用经过 Call → Return / Throw，中间可能有 Cancel、引用的计数 Release、会话关闭；经宿主中继时还多一跳。七个实现（Rust、Node、Bun、Python、Go、Swift、Kotlin）各自处理这些帧，有几条规则从没写下来：

• 取消之后被调用方要不要回复。 协议只说"回复仍可能到达"。Rust 作被调用方时，排队中的调用和 await 被取消后不再回复（已在运行的同步调用照常回复）；调用方的 cancelled 表要等迟到的回复才清，所以在 Rust ↔ Rust 的节点连接上只增不减。
• 读线程写回会不会互相卡死。 读线程会写 Throw（decode_args、too_deep）、Release（丢弃迟到的回复、被取消的进来调用），中继的 Import 被丢弃时还会写到别的会话。通道都有界（内存 64 条、WebSocket 管道 4 MiB、socket 缓冲区）。两端读线程都在写、都在等对方读时会不会卡住，没有测试也没有论证。

修过的缺陷：48794010（通道拒收的消息只让它自己的调用失败，退回授予）、fa292fd5（回复写不出时持着写锁去关闭，死锁）、963d977b（放弃的分发没有取消用 future 回复的远程调用）。

模型：specs/call-lifecycle/

参与者：两个端点，加一个中继（宿主）；每个方向的通道按序、容量 1–2；每端一个读线程（读到帧就处理，可能要写回）和调用方。

动作：Call、Return、Throw、Cancel、Release（带计数）、Close；被调用方在取消之后选择回复或不回复（按实现分配置）；中继转发调用、回复、取消、释放。

性质

简化：值只建引用；一个引用最多被授予两次；同步调用与等待图在 #614，这里只建异步调用。

结论写回

• 定下"取消之后的回复规则"，写进会话协议（中英）和插件 API，七个实现照此修改；不回复的实现，调用方在收到取消确认或会话结束时清掉 cancelled。
• 如果模型证明读线程写回会卡死：改成读线程不直接写（交给写线程或有界之外的队列），并写明。

对应的实现

crates/rutis-bridge/src/session/rpc.rs（Calls、cancel()、Frame::Cancel、Exports / Import、close()）、rpc/relay.rs；各语言 session.mjs、session.ts、peer.py、internal/peer/peer.go、Session/Peer.swift、internal/peer/Peer.kt。

完成

• specs/call-lifecycle/：.tla、.cfg、expected.txt、run.sh、README（中英）
• 每个性质一个变异；"被调用方从不回复"的配置找到 BoundedTables 的反例
• 回复规则写进协议并在七个实现里落实，session::testing 的一致性检查加上这一条
• 读线程写回的结论写进 README；要改的话修实现并加测试
• CI specs 矩阵加 call-lifecycle

追踪表中归本 issue 的规则（#634）

范围是下面这些规则的全部，不只是正文举出的几条，共 53 条。完成时，应有形式化检查的规则在追踪表里都是"已覆盖"（形式化检查通过，并有变异或修复前的配置证明它不是空的；一致性用例写上用例名）；只靠测试的写上测试名、保持"不适用"；改为其他手段的写明理由。

这次补进来的：MNT-6-5（dispose 同时启动插件卸载与在途调用的排空，不先等调用结束）。取消之后的回复规则定下后写进 #635 的会话帧规格。

• 登记表 §6–§8a（2）：core/D30e、boundary/5.8b
• 登记表 §9–§15（11）：bridge/in-flight-call-fails-once、bridge/no-call-on-a-dead-session、bridge/cancel-reaches-callee a、bridge/cancel-reaches-callee b、bridge/multihop-cancel-and-release、bridge/replies-match-calls、bridge/release-count、bridge/reference-release-count a、bridge/reference-release-count b、bridge/revocation-closes-only-its-connections b、bridge/cancellation
• 事件（2）：EVP-5.7-1、EVP-10-4
• 会话（16）：SES-7.1-3、SES-8-6、SES-8.2-3、SES-8.2-6、SES-10-4、SES-10-8、SES-10-9、SES-10-12、SES-10-13、M1-7.1-1、M1-7.1-2、CHN-2-9、CHN-4-7、CHN-4-9、CHN-4-10、CHN-5-5
• 运行时（13）：SYN-5-11、MNT-2-11、MNT-3-8、MNT-3-9、MNT-3-12、MNT-3-13、MNT-3.1-5、MNT-3.1-7、MNT-6-5、MNT-6-6、REQ-6-1、REQ-7-4、REQ-7-5
• 远程（9）：REM-1-4c、REM-3-3、REM-3.2-3、REM-5.2-15、REM-6.2-5、REM-6.2-7、REM-6.2-8、REM-7-2、DIA-5-8

并入 #640：spec: 用 TLA+ 验证节点托管行（peer rows）

属于 #183 第四步。追踪表 #634；形式化覆盖图 T6（#612）；规范 Q11.2。

为什么

节点托管行（peer:<节点>/<插件>，一个节点经连接替另一个节点运行行）已经实现、已经登记（loader/peer-rows a–c），规则写在远程插件 §5.1–§5.3。之前定为"等 peer 设计恢复、定稿之前再建"；按现在的覆盖范围（登记表 + 规格的全部规则），已实现、已登记的规则现在就要覆盖。它满足 Q11.2.1：两个节点、连接会断开重连、提供（link.offers）与装载交错，错误只在特定交错下出现（#435、#437、#438 都是这一类）。

模型：specs/peer-rows/

参与者：两个节点 A、B（各自可以替对方运行行），一条连接（可断开重连）；A 的 PeerRowsPlugin（解析、离线 / 在线、schema 刷新）与 PeerRow（apply 发 plugins.load，disposer 发 plugins.unload）；B 的 Host（每个会话一张已装载表）。

动作：连接建立 / 断开 / 重连；对端提供或撤回 plugins 族（带 epoch）；行 apply、dispose、restart；宿主 dispose；装载在途时被取消。

性质

修复前的配置：#438（PeerRows 在行排上之后、应用之前被撤下，行停在 Failed，#439 修复）；#435 / #437（同时登记的两个族被宣告成两次提供，peer: 行被重启）。

待复现的疑点

• 节点托管行在加载中被取消时不登记 disposer，宿主照常装载完，留下孤儿插件；先到的卸载什么都不做，之后的装载照样插入（从 spec: 用 TLA+ 验证宿主与运行时之间的行生命周期（代次、rows.ended、拒绝、服务公告、宿主服务租约） #625 移来）。对应 NoOrphan。
• PeerRow 的键是 ctx.instance()，跨重启不变，但注释说"每一代都新"；安全性靠对端每个会话的 Host.loaded，模型要把这一点写明。

规则（12 条）

• 登记表 §9–§15（3）：loader/peer-rows a、loader/peer-rows b、loader/peer-rows c
• 远程（9）：REM-3-6、REM-5.1-3、REM-5.1-5、REM-5.3-1、REM-5.3-3、REM-5.3-4、REM-5.3-5、REM-5.3-6、NOD-4-1

相关的一致性用例（REM-1-3、REM-3-1、REM-5.1-2、REM-5.1-6、REM-5.2-6、NOD-4-1 等）在 #639。

对应的实现

crates/rutis-loader/src/peer.rs（PeerRowsPlugin、PeerRow）、crates/rutis-bridge/src/host.rs（Host::{describe,load,update,unload}）、crates/rutis-bridge/src/compose.rs。

完成

• specs/peer-rows/：.tla、.cfg、expected.txt、run.sh、README（中英）
• 两个修复前的配置都找到反例；每个性质一个变异
• 疑点确认，属实的修复并加测试（rutis-loader/tests/peer_rows.rs）
• CI specs 矩阵加 peer-rows；追踪表对应行改为已覆盖