DeepSeek-Harness系列（二）：万物皆插件背后，是一篇论文
TL;DR 全文速览
- Cordis 论文（DeepSeek×北大）指出，卸载留残留、依赖对不上、系统底层难以改造，这三个多年没人理清的老毛病，其实是同一个问题：动态组合性缺失
- 解法是两条强制规矩：插件每做一件事，当场登记撤销动作；每用一个依赖，事先声明。两条规矩共用同一个全局上下文；定理保证内核的调度自由不改变终点，最终状态等同于把启用的组件按依赖顺序装载一次
- 论文的分量在三处：给这个老问题起了名字；把"出了事再补救"换成"从结构上让它出不了事"；给插件系统配上能证明的保证，据我所知此前没有插件框架做到过
- 但别高估它：它只保证撤销动作被按顺序执行，不保证撤销本身写得对；框架之外的世界（比如已经发出去的邮件）不可逆。论文也没跑过任何对比基准
- 我装插件把 dsh 搞崩过两次，升级内核又崩一次，三次都倒在装配阶段，前面那些保证还没来得及生效。文末进阶篇按论文原文重讲机制，带定义与定理编号，小白可跳过
一个把"万物皆插件"当招牌的系统 dsh（DeepSeek Harness），却被一个小插件搞崩了。我遇到两次。
dsh 是 DeepSeek 开源的 Agent 底盘（dsh系列第1篇讲过）：模型、工具、权限，连驱动 Agent 干活的主循环，都能拆下来换。撑起这套插件的底座叫 Cordis，聊天机器人平台 Koishi 在它上面跑了四年；DeepSeek 和北大后来给 Cordis 补了一篇论文，讲清楚这套东西凭什么能用。
把论文读完我不由感叹，DeepSeek 是真厉害：这篇论文最硬的一层创新，是给一个插件系统配上了能数学证明的保证，据我所知此前没有哪个插件框架做到过。它的承诺也有边界，装崩我的那次，恰好落在边界之外。
拆干净副作用、依赖图、响应式重算，这些概念都不新鲜，各有几十年历史。但这篇论文把多年来散落各处的麻烦收进同一个问题，起了名字，拆成两个轴，最后用一条定理证明整套做法自洽。
这篇讲这套机制怎么运作、为什么成立、又在哪里失效。讲机制的时候，Cordis 和 dsh 两个名字会混着用：论文和框架叫 Cordis，跑在它上面的产品叫 dsh，机制是同一套。文末的进阶篇按论文原文重讲一遍，带定理编号，写给较真的专业读者，其他人建议跳过。
三个你天天见的老毛病
1、卸载留残留。卸载过浏览器插件吧？卸完配置目录里还留着残留文件夹，运气差还有个开机启动项阴魂不散。
2、依赖对不上。插件 A 要某个库的 2.0，插件 B 只认 1.0，装了这个那个崩。于是装之前得仔细检查谁跟谁冲突。
3、定制很困难。想深度定制核心底层？VSCode 改不掉主循环，Claude Code 的 Agent Loop 改不了。想改就得复制整个源码自己维护，永远在合并上游更新的路上。
这三个毛病，多年来被当成三个互不相干的工程烦恼，各自打补丁。dsh 背后那篇论文（DeepSeek×北大，《A Programming Paradigm for Spatiotemporal Composability》）指出，它们是同一个病：系统支持运行时装拆零件，但从没人认真回答过"拆装的时候要保证什么"。
答案被拆成两个轴。时间轴管"拆走的东西痕迹能不能干净消失"，空间轴管"零件之间的依赖怎么对上、怎么跟着变"。卸载留残留是时间轴没做，依赖对不上是空间轴没做，定制困难是两轴都没做，所以这不是加几个功能就能解决的事。
dsh 怎么做：和传统做法对比着看
论文的两个主角，一个叫效应，一个叫共效应。效应回答"这段程序会做什么"，写文件、发请求、改状态。共效应回答"这段程序需要什么"，环境得给它提供哪些东西才能跑。
几十年来这两样只在代码检查工具里用一下，检查完就扔，程序真正跑起来时它们不存在。这篇论文的核心动作就是：把这两张检查清单搬进运行时，变成强制规矩。
卸载：从凭良心到强制记账
说到插件卸载，传统做法是，框架给插件作者一个口子，叫 dispose（或 destroy、cleanup，各家命名不同）：卸载前想清理什么，插件作者自己写。听着合理，实际很难保证。清理是可选的，忘了写的就漏了；就算写了，它和安装代码是两段分离的程序，装了三个东西只拆了两个，编译器不报错，测试跑不出来，只有跑了很久之后系统慢慢变脏。传统系统动不动就"重启保平安"，确实拆不干净。
dsh 不给你写"总清理函数"的口子。规矩改成：你每做一件事，必须当场交出撤销这件事的动作。
ctx.effect(() => {
const handler = (msg) => console.log(msg)
bus.on('message', handler) // 做：挂上监听
return () => bus.off('message', handler) // 撤：摘掉监听
})传进去的函数立刻执行，它返回的函数就是撤销动作，框架记下来。卸载时框架按"后拆先装"的倒序清账，插件不用记得自己装过什么。
传统做法里"拆干净"是每个作者的个人修养，而 dsh 把它变成框架的职责，作者有一个义务：做每件事时顺手写好怎么撤销。写歪了框架会照办（这个边界后面说），但"忘了拆"和"拆错顺序"这两类事故，从设计上就不可能发生了。
数据库的日志、编辑器的撤销栈早就在各自领域干同样的事。据我所知，没人做过的是把撤销和插件生命周期定义成同一件事：卸载插件，就是它全部痕迹的自动回滚。
依赖：从自己找到只声明
传统做法，插件要依赖什么自己导入进来。有三个问题：找不着当场报错；版本不对跑一半炸；最麻烦的是，你依赖的东西哪天被换掉，没有任何人通知你，你的插件握着失效引用继续跑，直到某天诡异崩溃。
更先进的系统有依赖注入（DI）：启动时容器把依赖塞给你，但塞完就下班，之后依赖换没换，容器不管。
dsh 的做法，插件不找依赖，只声明：
export const inject = ["tools", "llm"]; // 我需要工具注册表和模型接口剩下的全是框架的事。装之前算好谁依赖谁，按顺序挂载；依赖中途被换掉或消失，框架会通知受影响的插件，自动决定它们该留该走。运行中换掉数据库后端，用它的日志插件不用重启，收到通知自动改连新的。注入是一次性的，这里是持续的照看。
两本账合一，再上一道保险
这两样单看都不新鲜：拆账数据库里有，依赖拓扑 DI 容器里有。论文往前走的一步在合账：干活的账和依赖的账记在同一个本子上，一个贯穿全局的上下文，由同一套机制协调。
账必须合在一起。只记账不管依赖，插件还挂着空引用；只管依赖不记账，副作用没人收尾。有其一不解决，定制困难的问题就治不了。
最后，上一道数学保险，合流定理。它说的是：在同一批装卸指令下，内核先走哪一步、从哪个出口退出这些调度自由，不会改变终点；终点等同于"每个最终启用的组件按依赖顺序装载一次、中途从不卸载"。这个"等同"还是站在观测等价上说，不是物理状态分毫不差，而是没有谁能观察到差别。分布式系统里这叫收敛：各节点不管以什么顺序收到更新，最终状态一致。
这就是 dsh 敢把主循环、权限、沙箱全做成插件的底气：别家靠核心代码写得好保平安，它靠结构上出不了这类事保平安。这套底盘有一个真实生态的样本：同款框架搭的聊天机器人平台 Koishi，四年、四千多个插件，装得多卸得勤，也没出大问题。
创新到底新在哪
拆账、依赖图、响应式重算，哪个都不是新发明。那这篇论文到底新在哪？
答案其实在三个更高的层面。
第一层，它把问题本身重新定义了。科学史上反复出现这样的事：一个领域最重要的进展，往往是发现好几个看似无关的麻烦其实是同一个问题。牛顿之前，苹果落地和月亮绕地是两件事。这篇论文干的是同类的事：浏览器插件的残留、npm 的依赖地狱、改造上游代码的痛，三个领域的三种苦，被统称为"动态组合性缺失"，再拆成时间/空间两轴。
命名之前，每个领域各打各的补丁，打了几十年。重新定义之后，才有了统一解。别小看这一步，dsh 的架构文档、配置系统、插件规范，全部建立在这套定义之上。
第二层，把事后补救倒转成事前结构。看看别家怎么对待同类问题：VSCode 的扩展宿主崩了会重启扩展进程，出了事再救；浏览器靠权限审核和沙箱，防着出事；传统服务靠灰度发布和回滚脚本，出了事再逃。姿态都是"问题会发生，我备一套应对"。
Cordis 整个反过来：让"拆不干净"在结构上无处发生。每个副作用在诞生那一刻就被定义好，交出撤销动作；每个依赖在声明那一刻就被登记，进入拓扑。你可以说它苛刻，插件作者没有"先干再说"的自由了。但正是这种把约束焊进最小构造单元的做法，才让第三层成为可能。
第三层，工程直觉第一次拿到了定理背书。别家系统的插件承诺是什么？"我们测试过，大多数情况下卸载是干净的。"这是统计承诺，QA 部门背书。Cordis 的承诺是：在给定规则下，调度顺序不改变终点，终点等价于把启用的组件按依赖顺序静态装配一次。这是结构承诺，有定理背书。
这两者的高度完全不同。整个软件工业里拿到这种待遇的东西一只手数得过来：数据库的 ACID、Git 的不可变历史、类型系统的可靠性。而据我所知，插件系统还没有被这样证明过。这个领域原有的语言，dispose 回调、生命周期文档，根本写不出可证明的命题。先用演算把命题写出来，再实现它，顺序反过来了。这就是"范式"二字在这篇论文标题里的分量。
第 1 篇《dsh 到底是什么》里说的"心脏可换、零 Fork 税"，都是这三层创新的结果。这两个能力具体表现是什么样呢？
运行中的 dsh 是一棵插件树，ctx.llm 管模型调用，ctx.tools 管工具，ctx.sessions 管会话日志，而驱动 Agent 干活的主循环（ctx.agentLoop）、权限审批、沙箱，全是这棵树上的普通节点，和其他插件走同一条装卸规矩。对比一下：Claude Code 能换模型端点、能写 hook，但换不掉它的循环和权限系统，那叫可配置；dsh 这叫可重组。
定制不动源码这个问题，使用树的解法是图层式的：Bundle（官方素材包）→ Profile（你的命名组合）→ patch（你的图层，按 ID 定位某行配置，整行替换或插新行），越往上优先级越高。想换模型，在自己那层写三行，不碰任何源码。官方升级官方的图层，你的图层永远躺在最上面，上游照升，不用合并一行代码。官方仓库甚至不接受外部 PR，架构文档原话："There is no privileged core to patch"（没有哪个核心需要特批才能改），真是霸气的很。有开发者把从零写插件到发布 npm 的全程记成帖子，本地调试就是 --patch 指向自己目录，没碰官方源码一根毫毛。
别家在产品层面竞争，它在范式层面竞争，差距就在这。
那为什么装个插件还能把 dsh 搞崩？
开头说过，我装插件把 dsh 搞崩过两次。让我开始怀疑的是第三次，这次我什么都没装，只是升级了内核。
完整经过：官方发了新版本，我 npm 一升，dsh web 再也起不来。报错说，一个叫 prompt-optimizer 的插件，从内核的 dsh-llm 包里导入一个叫 deepFreeze 的函数，新内核把这个函数删了，导入失败，整个 dsh 启动失败。这个插件是干嘛的？优化提示词的，一个纯外围的舒适型零件。而我为了救回整台车，只能手改 profile 目录下的配置文件，把它的名字从加载清单里挖掉。大半夜的，一行行对着报错修复系统。
一个不重要的插件没跟上版本，为什么能瘫痪整个系统？
先定位故障：prompt-optimizer 死在装配阶段，它的代码压根没装进去。而前面讲的整套机制，记账、撤销、依赖协调、合流定理，全部是为"装进去之后怎么干净拆出"准备的。一个没装进去的插件，对这套机器来说等于不存在。
所以准确地说，故障发生在了承诺范围之外。Cordis 保证组合性，装得进、退得干净；但不保证质量与隔离，装进来的没毛病、装不进的不拖累别人。这是生态问题。插件质量、版本管理、兼容性承诺，dsh 也解决不了。
那为什么一颗外围零件坏掉，能熄掉整台车？这个设计其实也有它的道理，得替它辩护一下。
第一，它在保卫"配置即真相"。dsh 的核心承诺是：你声明的配置等于实际运行的系统。假设加载器遇到坏插件就跳过、继续启动。听起来很贴心，可你声明了 15 个插件，实际跑着 14 个，那棵树开始说谎了，而且没人知道少的是哪颗。跳过坏插件，等于编译器"帮你"忽略出错的代码行继续编译，产出的程序你敢跑吗？合流定理也建立在这个前提上：配置是良定义的，"最终状态唯一"才有意义。"全有或全无"是原子性，像数据库事务，不存在提交一半。
第二，静默跳过会把小病拖成大病。插件之间有依赖：A 加载失败被跳过，依赖 A 的 B 照常启动，B 拿到一个不存在的服务。错误不消失，只是从启动时一条清晰报错，变成会话进行到一半的诡异崩溃。启动期死给你看，反而是成本最低的死法。
第三，当前加载方式物理上接不住这个错误。加载插件用的是 JavaScript 的静态 import，语言层面就要求被导入的东西必须存在，出错时程序无法捕获、无法继续。这是语言规定，dsh 没得选。
但它的软肋也在这里。
软肋一，故障域不分级。prompt-optimizer 是外围零件，dsh-llm 是内核包，但在这条加载链里两者地位一模一样，都有对启动的一票否决权。看看成熟系统：浏览器禁用坏扩展继续跑；VSCode 的扩展宿主崩了编辑器还在；systemd 把失败单元标记为 failed，引导照常完成。共同点就一句，外围零件没有资格绑架核心启动。dsh 把所有插件装进同一条"全有或全无"的链，外围和内核共享一根保险丝。
软肋二，自救通道一起陪葬。启动失败时最需要的是"进系统把坏插件卸了"，可恰恰这时连 Web UI 都起不来，唯一的管理界面被它要管理的故障干掉了。本来是为了自保，结果把自己也锁在了门外。
软肋三，也是最麻烦的一条："配置即真相"的原子性承诺，和"生态会出错"的现实之间，有一块没被填上的真空。Cordis 的数学覆盖良定义配置之下的一切行为，生态的现实是配置常常不良定义，版本不兼容、依赖缺失、代码写错。真空里的每条出路，跳过、隔离、降级、写回，都会触碰"配置即真相"：跳过会让树说谎，隔离需要定义"部分运行"的语义，降级需要让配置表达"我容忍缺谁"。
所以 dsh 在这里留了个白：装配期的容错策略被悬置，答案留给未来的设计，也留给了事故。怎么在不清算"配置即真相"的前提下填这块真空，是这个架构悬而未决的题。
还有个实用推论：插件树是启动时装配的，装卸插件后要重启才生效。我有次"插件卸载成功了还报错"，最后发现就是服务进程没重启，内存里还是旧插件树。
再往深一层：这套架构在赌什么
最后说三件我一直在琢磨的事。
1、它赌"约束前置"这条路能赢。软件工程的历史里有两股反复拉锯的力量：一股信纪律，用规范、评审、测试约束人的随意；一股信结构，用类型系统、事务、不可变性让错误无处发生。Cordis 把注全押在后者：副作用必须在诞生时交出撤销，依赖必须在装载时进入拓扑。
代价也很明确，每个插件作者都背上一层"显式化的税"，写插件前得先想清楚自己会动什么。这和当年静态类型、和 Rust 的所有权模型遭遇的抵抗一模一样：结构派的每次胜利，都是先用不适感换正确性，再等工具链把不适感磨平。Cordis 押的是同一条历史曲线。它赢不赢，不取决于定理对不对（定理已经在了），取决于那层税最终能磨到多低。
2、可逆性是"自我改写的 Agent"的前置条件，但它同时圈定了自我改写的边界。一个会改自己的 Agent（我会新开文章专门说），如果每次自改都不可逆，改错一次就永久劣化；只有变更可回滚，"自我进化"才是工程模式而非研究奇观。Cordis 的可逆内核正是为此准备的。
可另一面很少有人提：框架只保证账本内的世界可逆，而 Agent 真正有后果的行动几乎都在账本外，发出的邮件、合并的提交、花掉的钱、对人说的话。一个只敢在可撤销世界里行动的系统，永远在沙盒里打转；一个在不可逆世界里行动的系统，得靠判断力，系统机制在这里帮不上忙。
所以可逆内核不是"让 Agent 安全"的答案，它只是把安全问题的边界从"系统能不能悔棋"推进到了"Agent 该什么时候落子不悔"。后者是能力问题，任何框架都替代不了。dsh 把地基打到了这条线的正下方，这已经是框架能做的极限。
3、"可塑"重新定义了开源，也重新分配了责任。开源许可证让代码可看，插件内核让代码可换：透明是"信不信由你，代码摆在这"，可塑是"不用信我，不满意就换掉我"。
官方仓库不接受外部 PR，贡献被导向生态而非主干。这在开源项目里算相当激进的一步：它把"参与"的定义从"帮我改代码"改成了"在我上面盖楼"。
但权力不是白给的：当万物皆插件，你的系统好不好用，从此取决于你装了什么。发动机舱打开了，装错零件的责任也快递到付给了你。看这套架构什么时候成熟，别数插件数量，看它和它的用户什么时候学会共担：框架保证底盘的上限，装什么货、怎么验证货，是所有人的事。
进阶篇：按论文原文重讲一遍
以下部分写给较真的读者，小白可以跳过。论文是 A Programming Paradigm for Spatiotemporal Composability↗（arXiv:2608.25512，DeepSeek×北大），下面提到的小节号、定义号和定理号都来自它，引文是我自己译的。
论文的第一刀，是划维度
开始讲机制之前，论文先做了一件更基础的事。它说静态世界里这两个维度早就各自有解，只是没人把它们当成同一个问题的两面：时间维退化成词法作用域（C++ 的 RAII、bracket pattern），空间维退化成模块导入解析。到了动态世界，两者同时失效，因为效果的生命周期不再被作用域框住，依赖会在运行中出现、消失、换人。
论文也把"退而求其次"的代价算了一遍。重启进程能清掉一个模块的烂账，代价是丢掉所有进程内状态（缓存、连接、算了一半的活），重建要几秒到几分钟；容器编排能管服务之间的依赖，管不了同一个地址空间里组件之间的依赖，还把本地函数调用变成了网络往返。粒度对不上，就只能在组件这一层管效果和依赖。
可逆效应：累加器、逆操作，和一条复合性定理
效应函数在论文里是一串阶段（stage）。每个阶段可以产出（yield）一个逆操作，运行时把这些逆操作收进一个累加器（accumulator，实现里叫 fiber.dispose），组件卸载时按 LIFO 应用。
为什么必须是 LIFO，论文给了理由：反序应用，每个逆操作拿到的正是它自己正向执行之后留下的那个状态。正序应用会先把资源释放掉，再回头去拆还在引用它的东西。
这里有一条容易被跳过的地基（Theorem 5）：一次记一对（正向、逆向），和把整串扭在一起一次记，结果一致。所以一整串被追踪的效果，可以被当作单个被追踪的效果来推理，记账本身是可组合的。后面所有全局定理都踩在这条上面。
不过，论文自己指出，§3.1 那个"恢复等于原状态"是理想化的（Theorem 7）：free 把块还给分配器，不会把堆恢复成 malloc 之前那副样子；生成的名字也不会被"丢弃"这个逆操作还原，因为下一次创建会取一个新名字。所以这个保证得在下一节那个等价关系的精度上读。
观测等价：什么叫"没有谁能分辨"
论文不拿"状态相等"当标准，而是构造了一个等价关系。它的出发点是问：观察者手上有什么？一个值的观察者拿到的是这个 key 上的一组操作；一个上下文的观察者拿到的是它携带的共效应。
定义是这样的：一个 test 是"由正向映射和产出的逆组成的有限字"，每个字母作用在前一个字母留下的值上；两个值不可区分，当且仅当没有任何 test 能分辨它们的产出。上下文之间的关系，由各个 key 上的关系拼装而成。
所以"干净"在这套理论里有了精确含义：一个被明确定义出来的等价关系下的商。这句话的分量在于，它同时说明了这套保证能管多细：凡是观察不到的区别，理论就不管；凡是观察得到的，理论才负责。
反应式共效应：三分类，和局部保证漏掉的两件事
组件声明它需要什么，运行时把每一次上下文变化，相对这份声明，分类为三种之一：激活（activating）、失活（deactivating）、中性（neutral）。激活触发效果执行，失活触发累加器回收。
这样就得到了局部空间可组合性：组件只在满足声明的状态下激活，所以它永远不会读到一个不存在的绑定；每次上下文变化都被对着声明分类，所以"失去满足"在发生的地方就被发现，并驱动一次失活。
但论文紧接着说：有两件事这个局部判据不管，而且都要等系统里同时有多个组件时才会冒出来。一是提供者不能在自己引发的失活全部结束之前就收回绑定；二是激活期间读到的绑定，不能在中途被换掉。这两条约束的是"别的组件"，属于全局保证，论文把它们留到 §4.3.3 去证。
组件、演算，和五条元定理
组件在论文里是个三元组：它会做什么（效应）、它从环境读什么、它向环境提供什么（Definition 48）。组件的一个实例叫 fiber，带自己的生命周期状态；registry 持有所有 fiber，共效应上下文是从 registry 里读出来的。
演算的规则分两侧：生命周期侧有 L-Begin、L-Iter、L-Finish、L-Divert、L-Leave、L-Unload；编排侧有 O-Insert、O-Retire、O-Remove。
元理论是五件事。
保持（Preservation）：走一步不破坏不变量。
时间可组合性：局部保证要提升到全局，关键条件只有一个，插进来的那些步骤得和累加器交换。论文为此定义了独立（independence，Definition 65）、纠缠（两个 fiber 的供给与声明相遇）、以及成对独立的步骤序列，语言直接取自 trace theory："可交换的动作生成序列上的一个等价关系，在这个等价关系下，交换两个相邻的独立动作不改变终点。"
空间可组合性：前面漏掉的那两条在这里补上，落到 Theorem 70（Ordering）：提供者只有在解析过它的依赖者全部失活之后，才收回绑定。这条排序定理和一条"一致性"定理是同一个不变量的两半，所以论文把它们放在一起证。
推进（Progress）：光有排序不够，还得保证那个"等依赖者走完再撤"的闸门终究会放开。论文定义了一个先序关系 ≺（Definition 72），并在 ≺ 无环的前提下证明推进（Theorem 73）。这里有个必须说清的细节：无环是假设，不是定义能给的。一个组件若声明了自己提供的 key，它就先于自己。
合流（Confluence）：这是全篇最强的一条，也是外面传得最走样的一条。合流讲的是 registry 的性质，编排步骤是输入；输入不同，结果不同，这没什么可说的。问题在于内核调度上有自由，下一步走哪个 fiber、从哪个出口退出，这些自由会不会导致分歧？
不会，因为"哪个 fiber 提供某个 key"不在选择之列（一个 key 至多有一个可能的提供者，Definition 50），所以调度能挑的只有顺序和出口。定理（Theorem 80）分两句。第一句叫规范形：终点可以从初始状态出发，按"编排步骤的原序，加上对支撑集（support set，Definition 74）的一个线性化顺序、各跑一个 episode"到达。第二句才是合流：任何两条走同样编排步骤的序列，到达的状态经重命名后互相等价。前提是每个组件对自己的供给是全的（total，Definition 76）。
论文对这个结果的定性是：系统的动态历史不留痕迹，它收敛到的规范形就是静态装配出来的那个；论文自己把它类比为增量计算里"与从头算一遍一致"。
惯性、失败，和实现里其他名词
论文给了四个扩展，跟日常使用最相关的是异步。同步规则里，一步的状态映射是整体应用的；异步宿主里，迭代和逆操作产出的是 future，飞在半路的映射不管还要不要都会跑完，"中途放弃"这个选项，这种宿主根本提供不了。论文把这种宿主叫惯性（inertial）：它只取 L-Divert 的落地分支；一个 fiber 如果在迭代过程中目标变了，它会在这一轮落地之后才失活，手里还攥着自己产出的那个逆操作。
惯性在这里是一个受限的规则选择，算不上补丁。§4.3 的所有结果都是对"所有步骤序列"量化的，所以惯性宿主照样落在保证范围内，照样能静止下来（quiesce）。
实现侧（§5）能对上号的名字：fiber.state（有 LOADING、UNLOADING，还有一个承载失败结果的 FAILED）、fiber.dispose（累加器）、fiber.committed（已提交的视图）、fiber.inertia（在途转换的句柄）、fiber.target（由 refresh 重算）。其余几个是 fiber.uid、fiber.ctx、fiber.inject、fiber.apply、fiber.parent。加载器侧是声明式配置、配置调和、热替换，热替换的第三步在论文里叫事务性重载（transactional reload）；Algorithm 5 实现的就是 §4.4 那台惯性状态机，靠 resolve(inject) 和 provided(fiber) 两个查询工作。
边界：论文自己划的那条线
论文没有把"可逆"吹成万能，它划了一条系统边界，而且划法很讲究：边界不按介质划，按位置划。一个位置在边界内，当且仅当系统能独占修改它、并且能把它恢复到修改之前；两项能力缺一，这个位置就在边界外，对它的一切操作在上下文里等价于恒等（id_Γ），既不追踪也不回滚。
边界还能移动。一个共效应可以把外部位置具体化（reify）：把对它的访问收束到一组由你提供的操作上，每个操作自带逆，于是原本在边界外的位置被拉进边界内。论文同时说清这是一笔权衡，一边是环境是否提供可逆语义，一边是每次访问为此付出的代价；6.7 节专门谈了它与语言、操作系统的协同设计。
另外两个词值得记住。一个是输出提交问题（output commit problem）：有些输出一旦发出就注定留下，回滚恢复对它无能为力。另一个是补偿（compensation）：它不回滚，改做一个恢复动作，把创建的文件删掉，恢复到的等价关系比观测等价更强。补偿可以像逆操作一样按 LIFO 复合，但元理论不跟着转移：Definition 65 的交换性是对着观测等价证的，而不是等价。
这大概是 §6 里含金量最高的一句提醒：定理的适用半径，跟它所依据的那个等价关系一样宽。
论文自己承认的局限
案例研究是 Koishi，前面正文里提过的那个生态。论文用它说明两件事：一是表达力，它的原语足够撑起一个完整的生产系统，宿主框架只提供领域词汇；二是通用性，Koishi 的 Web 控制台是另一个独立的 Cordis 应用，跑在浏览器的原语上，和服务器端用的是同一个模型。
但论文自己加了个脚注：Koishi 目前用的是 Cordis v3，本文给出的是 v4；v4 重做了效应与共效应的语义，重新设计了加载器，两个版本共享核心的组合模型。此外，论文对这项案例研究的定性是"观察性的，不是受控对比"，而"相对于基线的开发者生产率影响，仍是 future work"。
所以正确的读法是：这篇论文证明的是存在性，至少这套范式能被实现、能在一个真实生态里活下来。
三句总结
一，它的贡献落在问题的坐标上：把"插件系统很麻烦"拆成时间与空间两个可以分别证明的维度。
二，它给的保证有精确精度：状态恢复成立于观测等价的意义上，合流成立于"同一批编排输入之下、调度自由不改变终点"。
三，它自己划了边界，也自己指出了边界之外的开放问题：边界如何随语言和操作系统协同移动，补偿能不能有配套的元理论。