§它到底讲了什么

§我是不是看错论文了

前些日子 DeepSeek 发布了自己的 Agent Harness，社区里出现了很多介绍。我陆续看了一些，谈得最多的是它的核心理念 Everything is a Plugin，万物皆插件。模型、工具、记忆和会话都可以是插件，连 Agent Loop 本身也可以被替换。有些文章还深入源码，解释 DSH 怎样执行任务、调度工具。我最近也在学习 Agent Harness，很自然地想看看它的设计，以及它与 Claude Code、Pi 有什么不同。带着这个期待读完官方提供的论文，我的第一反应却是，我是不是看错论文了？

我想了解的任务规划、工具调度和上下文组织，在论文里都没有展开。读到这时才发现，我把社区对 DSH 整体架构的讨论，当成了论文要解释的内容。
DSH 是一个 Agent Harness，Cordis 是它底层的插件运行时，论文研究的是后者。它讨论的问题更为通用。一个允许插件动态安装、卸载和替换的系统，怎样才能在变化中保持正确？

这又让我有了一个疑问，为什么一个 Agent Harness 需要一篇讨论插件运行时的论文？

§自演化的 Harness 意味着什么

论文所说的“自演化 Harness”，究竟在演化什么？模型之外的工具、记忆、存储和调度，共同组成了 Agent 赖以工作的 Harness。模型可以在其中选择工具、读写记忆，但使用这些能力，与修改承载它们的系统，是两件事。

论文设想，未来的 Agent 能够修改自己的 Harness。要让这种修改成为可能，工具、模型服务乃至核心循环，都需要成为 Agent 可以识别和操作的对象。那么 Harness 首先得有一套表达自身结构的方式。
每个部分负责什么，提供哪些能力，又需要哪些支持，这些信息原本可能分散在代码各处。把它们纳入统一的运行时抽象，Harness 才能把自身交给程序管理，这样也才能变成 Agent 有可能修改的对象。
沿着这个要求，“万物皆插件”就容易理解了。DSH 用同一种插件模型描述工具、模型服务和核心循环，让修改 Harness 有了明确的操作单元。

§所谓“万物皆插件”

前端开发者对这个理念应该不陌生。Webpack 就是一个高度插件化的系统，官方文档把 Plugin 称为整个系统的骨架，它自身也建立在用户使用的那套插件系统之上。不过，高度插件化与运行中安全地改变插件组合，仍然是两件事。
Webpack 的插件把回调注册到 Hook 上，再在相应的编译阶段执行。常规配置下，同一个 Compiler 使用的插件集合通常保持稳定，执行时再由 Hook 调用相应回调。模型从已注册的工具中选择一项，也只是一次能力调用，未必改变 Harness 的结构。现有 Agent 也有动态扩展能力，例如 MCP 支持查询工具列表并通知列表变化。所以，只看“能否动态增加工具”，还不足以说明 Cordis 要解决的问题。

Cordis 关心的是插件组合在运行中变化时的正确性。插件可以进入、退出和被替换，运行时要管理系统里有哪些插件，以及它们之间怎样绑定依赖。“动态调用”与“动态组合”的区别就在这里，代码有没有提前加载进内存，并不能说明这种区别。

§“万物皆插件”之后

把能力都变成插件，系统便有了替换它们的操作单元，从程序系统的角度看，每一次自我修改都是一次动态组合。假设一个 Agent 原本通过本地文件系统插件读写工作区，现在准备改用远端 Code Server 环境提供的文件服务。新代码加载以后，旧插件仍可能持有文件句柄、目录监听器和本地缓存；远端实现则需要网络传输与鉴权服务，还要向上层提供相同的读写和监听接口。只把 Context 中的文件服务改指向新实现，正在使用旧实现的插件就可能陷入不一致状态。
系统需要知道旧插件改变过什么，并在它离开时按顺序撤销这些改变。系统也需要知道哪些插件依赖文件服务，它们当前绑定哪个实现，以及这次替换会影响谁。依赖出现、消失或换了提供方，相关插件就需要相应地退出和重新加载。
工程上常用重启来处理这类问题。例如，VS Code 的扩展管理文档说明，卸载、禁用或更新扩展后，会提示重启 Extension Host。进程结束时，操作系统回收它持有的内存、句柄等资源；重新启动后，依赖关系按配置建立。这种办法简单，却也意味着进程内未持久化的执行状态会丢失，需要保存和恢复。Cordis 要支持运行中的动态组合，就得让系统在不重启的情况下安全地更换服务。

论文要回答的，正是怎样完成一次局部替换，而不必让整个系统重新开始。

§术语约定

插件Component

本文对论文中 Component 的称呼，用来定义依赖、供给和加载过程。

插件实例Fiber

插件进入运行时后产生的具体实例。

副作用effect

对共享环境的修改，本文沿用前端的译法，不译作“效应”。

撤销函数inverse

比通常的清理函数（cleanup / disposer）多一层约定，执行后必须撤销对应操作对受管状态的修改。

这里的“受管状态”，指纳入 Context 管理的那部分共享状态。

上下文需求coeffect

描述插件要求环境提供什么，例如文件系统或日志服务。

§从动态替换反推 Cordis

文件服务替换期间，我们希望会话继续运行，编辑、搜索和索引插件仍通过同一套文件接口工作。这要求旧实现的资源得到清理，相关使用方按顺序退出并重新绑定，无关插件则继续运行。已经完成的业务写入，也不应因为文件服务卸载而被一并回滚。
这些要求可以分成两个方向。时间可组合性（temporal composability）关心怎样撤回插件对受管状态的副作用；空间可组合性（spatial composability）关心依赖怎样组合、隔离，并在变化时协调。

§怎样只撤销旧插件

在“万物皆插件”的系统里，插件也是卸载和替换的单位。运行时要拿掉其中一个，就必须分清它和其他插件分别改变了什么。我们希望只撤销目标插件的修改，让其他插件保留当前状态；整个系统倒退到历史快照，显然不符合这个要求。
首先要明确修改的归属。那些不与外界交互、也不被外界持有的局部对象，随插件一起丢弃即可。需要单独处理的是越过插件边界的修改，例如注册目录监听、占用文件句柄，以及向 Context 提供服务。它们必须能归到对应的插件实例上。
知道“是谁做的”，还不等于可以安全地撤销。两个插件可能共同使用一个服务，如果 A 的清理会破坏 B 的结果，就不能把 A 当成独立的撤销单位。我们还需要独立性，让一方的执行和撤销不改变另一方的行为。确实有先后依赖的部分，则要把顺序表达出来。

工具注册表可以说明这个区别。A 用唯一名称注册 format_document，B 注册 search_symbol，卸载时各自只删除自己的条目。如果表只按名称查询，不把插入顺序作为公开语义，移除 A 就不影响 B。这份独立性来自注册表的接口约定，单纯把 A、B 写进两个插件文件，并不能得到同样的保证。
一旦允许同名覆盖，或者清理时直接清空整张表，这个约定就被破坏了。两个插件即使都写了清理函数，也未必能够独立卸载。

明确了归属和独立性，就可以缩小视角，研究一个插件本身。插件加载时，对外产生的是一组副作用；卸载时，需要撤回这一整组修改。“撤回”不必逐字节还原。监听器关闭以后，操作系统的内部计数器可能变了；内存释放以后，堆的布局也不会恢复原样。在其他插件的修改保持不变时，只要通过模型允许的操作，无法区分“目标插件已被卸载”和“它从未加入”的受管状态，就足以认为修改已经撤回。这在论文里叫观察等价（observational equivalence）。它允许忽略内部实现细节，但不能把接口仍能观察到的差别也当作相同。

接下来，要找到完整撤销这组副作用的办法。运行时面对任意 JavaScript 代码，无法等到卸载时再猜测它改过什么、该怎样恢复。掌握这些信息的是执行操作的代码，所以撤销方法必须在副作用发生时就交出来，由上层统一管理。
顺着资源管理的工程直觉，这些撤销函数应该归入当前插件实例，并按执行的反序调用。后创建的资源往往依赖先创建的资源，打开连接以后再建立监听，退出时就先移除监听，再关闭连接。每取得一个新的撤销函数，就把它接到已有清理逻辑的前面，自然得到后进先出的撤销累加器（accumulator）。
这样，插件内部即使分成多个辅助函数，也不需要在卸载回调里重新罗列所有资源。每一处取得资源的代码交出自己的撤销方法，外层只负责组合和调度。

把这个要求写成 API，就是执行操作的代码返回清理方法，把何时清理的控制权交给框架。前端开发者很容易想到熟悉的useEffect范式。

TypeScript
1
2
3
4
useEffect(() => {
  const watcher = fileService.watch(workspace, onChange)
  return () => watcher.close()
}, [fileService, workspace])

Cordis 的ctx.effect也采用类似的形式。

TypeScript
1
2
3
4
ctx.effect(() => {
  const watcher = localFs.watch(workspace, onChange)
  return () => watcher.close()
})

React 的useEffect 会在规定时机调用清理函数，也要求清理逻辑正确地撤销 setup 的工作。论文把这项要求作为组合论证的前提，返回的函数必须撤销对应修改，后面的推导才能成立。两段 API 都把清理交给框架调度；清理函数是否正确，仍需由实现来保证，Cordis 也不会自动证明这一点。

从“怎样单独卸载插件”往下拆解，我们得到了最小的操作单元，一次归属明确、同时交出撤销方法的副作用。怎样把这些单元组合回可撤销的插件，留到后面的论文论证部分。

§怎样只让相关插件跟着变化

副作用上的独立性允许我们保留不受影响的插件，服务之间的依赖则决定谁需要跟着变化。文件服务被替换，索引插件仍然需要调整；与文件服务无关的插件，则不应因此退出。
要确定这个范围，运行时需要一张随当前绑定更新的依赖图。不过，整张图不必由某个插件集中描述。使用方声明需要什么，供给方登记能提供什么，运行时把两端连接起来，就能从局部关系得到整体关系，也能反向查出谁依赖谁。
视角由此缩小到一个插件对环境的要求。远端文件服务需要网络和鉴权，索引插件需要文件读写和监听。这就是论文所说的上下文需求。
怎样把需求表达给系统，已有很多工程方案。静态import、插件的依赖清单、DI 的装饰器，都能表达某一层次的依赖；响应式系统还会从实际读取中被动收集关系。论文选定的是执行前显式声明的模型，没有比较这些方案各自的优劣。

索引插件需要文件系统能力。如果它在声明里写死某个本地实现，替换服务时就得连使用方代码一起修改。因此，需要为这项稳定的需求取一个名称，也就是依赖键（dependency key）。使用方声明需要fs，供给方登记符合接口约定的实现，运行时决定这次绑定到谁。
DSH 使用的 Cordis 通过inject表达这类声明。下面沿用假设的fs服务，省略类型扩充和索引实现，API 形式见官方服务与依赖文档：

TypeScript
1
2
3
4
5
6
7
8
import type { Context } from '@deepseek-ai/cordis'
export const inject = ['fs']
export function apply(ctx: Context) {
  const fs = ctx.fs
  // 使用本次绑定的文件服务建立索引。
}

供给方则通过 ctx.provide 登记已经创建好的服务：

TypeScript
1
ctx.provide('fs', remoteFs)

inject表达需求，ctx.provide登记供给，ctx.fs取得本次运行所绑定的服务。运行时不必理解索引算法，只要把声明和实际绑定联系起来，就能还原当前的依赖关系。
关系变化后怎样传播消息，也符合熟悉的发布订阅思路。依赖声明可以看作订阅依据。服务供给或可用状态发生变化时，运行时通过通知机制重新检查相关插件的依赖，判断是否需要调整它们的运行状态。

空间方向的要求也由此落到了局部。从“怎样找到受影响的插件”，到一个插件需要什么，再到需求与具体供给的绑定。管理好这些关系，运行时就有了确定变化传播范围的依据。

§两个方向在 Context 汇合

依赖关系确定了文件服务退出时会影响谁，撤销机制让这些插件能够清理自己留下的修改。索引插件先移除旧文件服务上的监听，旧服务随后退出；新服务准备好以后，索引插件再建立监听和索引。无关插件继续运行，有依赖的插件按顺序退出和重新进入。把这些加载、运行和清理规则组织起来，就得到了插件生命周期。

Cordis 用 Context 同时承载两类信息。副作用经它追踪，撤销方法归到相应的插件实例；服务也经它提供和取得，依赖绑定因而能被运行时管理。提供服务本身又是一项副作用，供给方退出时，自己加入的绑定也要撤回。时间与空间的管理在这里联系起来。
这就是论文的上下文范式（context paradigm）。Context 把“改过什么”和“依赖什么”放进同一套运行时结构。这些保证以插件遵守约定为前提，Context 自身不提供安全沙箱隔离；绕开它修改共享状态，就不能直接套用论文的结论。

从系统需求一路向下，插件最终被拆成了可以管理的修改和依赖。运行时据此组织插件，无须理解它们的全部业务逻辑。

§论文怎样把结论证明回来

从系统需求出发，自上而下地寻找机制，最后落到具体 API，是一种常见的工程思路。论文的论述其实是从另一端开始的，先约定最小操作应当满足的条件，证明组合后仍然保留这些保证，再把组合的范围逐层扩大，最终得到系统层面的结论。

§从单个副作用到单个插件

最底层先提出的是关于撤销的约定。一次副作用把状态$\gamma$变成$\delta$，同时交出撤销函数$g$；这个函数必须能够撤回本次操作造成的副作用。这是 Definition 8 对副作用实现提出的前提。原文在这里使用等号，随后在第 3.3.2 节统一按观察等价解释；沿用这个口径，可以写成：

$$\begin{array}{rl}e(\gamma )& =(\delta ,g)\\ g(\delta )& \simeq \gamma \end{array}$$

有了这份约定，就可以连接两个副作用 A、B。先执行 A，再执行 B；撤销时先撤回 B，状态便回到 A 刚执行完的时候，A 的撤销函数也就能继续把状态恢复。因此，A、B 组成的整体仍然是一个满足同样约定的副作用。这就是 Theorem 11 的结论，撤销保证在组合后仍然成立。
组合后的撤销函数也可以当作是个独立的撤销行为，因此可以继续与 C 组合，再接入更多操作。每扩大一层，都可以直接使用上一层已经得到的保证，无须重新展开内部实现。于是，单次操作能够撤销，就被推进成了一整串操作能够反序撤销。

这串操作也不必事先全部给出。每完成一步，就把它返回的撤销函数接进累加器。Theorem 16 保证，只要每一步都履行撤销约定，累加器就始终能撤回已经完成的副作用；反序撤销时，每个撤销函数都会遇到自己那次正向操作留下的状态。因此，在步骤之间停止加载，也不妨碍撤销此前已经完成的工作。
论文用副作用迭代器（effect iterator）表示这个逐步执行的过程，形式定义见 Definition 17–18。把它作为插件的加载过程，插件就继承了这段序列的撤销保证。这便得到了局部时间可组合性，“局部”意味着此时还只考虑这个插件自身的操作。

再为这个过程配上依赖声明，就有了开始和退出的依据。只有依赖全部满足才启动，失去依赖则触发撤销；Definition 21–22 由此建立局部空间可组合性。将需求、供给和这段可撤销的加载过程放在一起，并限制共享交互经由声明范围内的 Context 操作发生，就得到了论文的插件定义（Definition 30、Definition 48）。
到这里，单个插件已经知道何时可以启动，也能够撤回自己完成的工作。接下来要把这个保证带到有其他插件参与的环境中。

§从单个插件到多个插件

其他插件加入以后，撤销函数遇到的状态可能已经被其他插件改过了。要让刚才的恢复仍然成立，就必须补上独立性条件。一个过程中的正向操作和撤销操作，都要能与另一个过程的操作换序，而且不能改变对方产生的撤销函数、后续步骤和操作结果。前两类要求来自 Definition 42，能力操作的结果约束由 Definition 44 补足。

只要满足独立性的条件，在证明中就可以把目标撤销函数跨过其他独立操作，移到它对应的正向操作旁边。到了此时，最底层的撤销约定便再次适用，两者抵消，只留下其他操作的副作用了。独立性还保证，剩余操作已经交出的撤销函数仍然有效，因此这个过程可以继续。Theorem 43 在副作用函数这一层给出了结论，可以转述为：

一组各自可撤销、两两独立的副作用执行后，以任意顺序执行本次运行产生的全部撤销函数，都能恢复到初始状态。

这说明，独立操作可以单独撤回，不需要把后来发生的所有操作一起撤销。要把这个结论继续用于插件整体，还需要说明整段加载过程的独立性从哪里来。

论文先把条件落实在单个能力接口上。Definition 29 把操作及其撤销限制在对应键的状态内，因此，真正访问不同状态的键，其操作可以彼此独立，这就是 Theorem 45。两个名字背后仍然修改同一块共享状态，就不能套用这个结论。
共同操作同一个键时，就需要能力提供方保证这个键上的能力操作两两独立。论文把具备这种性质的键称为可交换的（commutative），按照 Definition 46 的要求，这项独立性保证由能力提供方负责，使用方无法仅凭调用方式替它保证。

单个能力的保证具备以后，就可以继续组合到整个插件的加载过程。Theorem 47 给出的条件是：两个过程与共享环境的交互都通过 Context 进行，双方提供的键均不在对方涉及的键范围内。共同操作同一个键时，该键上的能力操作也满足前面说的独立性要求。满足这些条件，两个副作用迭代器便相互独立。能力接口的局部保证，由此成为依据插件声明判断整体独立性的基础。
于是，两个独立插件的操作即使交错发生，也具备了在证明中换序的条件，不必共用一条全局的后进先出顺序。各插件内部有先后依赖的步骤仍然反序撤销，真正存在于插件之间的依赖关系，则留给下一层处理。

§让这些保证在生命周期中继续成立

索引插件必须先取得文件服务，才能向它注册监听；清理监听时，旧文件服务也必须仍然可用。这类操作显然不能任意换序。因此，上一层尚未覆盖的部分，需要由生命周期规则保留顺序，让每个插件的撤销保证有机会正确执行。

运行时为每个插件实例记录本轮实际采用的已提交依赖视图（committed view），另行计算现在应该采用的目标依赖视图（target view）。本轮加载和清理始终保留旧绑定；目标变化时，实例先进入卸载，清理已完成的工作，再决定是否开始下一轮。供给方则必须等既有使用方完成清理，才能撤回自己的服务。这些是第 4.2.2 节对合法生命周期转移施加的条件。

首先要确认，这些规则在执行过程中不会破坏自己的前提。初始插件图满足结构约束后，每次合法转移都必须继续保留有效的父子关系、无冲突的供给声明和可用于清理的依赖绑定。Theorem 64 证明了这种保持性（preservation）。因此，无论已经发生多少次合法变化，下一步仍然能在符合约束的插件图上推理。

现在，前面的保证可以接起来了。插件自己的操作由累加器反序撤销；穿插其中的独立操作可以在证明中换序；不能换序的供给与使用关系，则由生命周期规则维持。每一种交互都有了相应依据，单个插件能够完整撤销自身副作用的保证，便能延伸到整个交错执行过程。
Theorem 68 由此得到精确恢复性（recovery exactness）：执行一个实例的累计撤销函数，会撤销它自身对受管状态产生的副作用，同时保留其他实例独立产生的修改。Corollary 69 再将这份恢复保证应用到卸载完成的时刻。最开始“单次操作能够撤销”的保证，到这里才成为动态系统中的时间可组合性。

同一组规则也把单个插件的依赖要求推进到了插件之间。Theorem 70 证明，供给方先准备好，使用方才能加载；使用方清理结束后，供给方才能完成卸载，因此清理所需的绑定不会提前失效。
有了这份顺序保证，再结合前面的恢复结论，Theorem 71 得到依赖解析一致性（resolution coherence）：加载沿同一份依赖绑定完成，或者因目标变化转入卸载；后一种情况下，卸载完成时恢复已经产生的副作用。这样，依赖变化便不会让一次加载混用新旧绑定。局部的依赖声明与响应，由此得到系统层面的空间可组合性。

§从正确的过程到确定的终态

到这里，论证已经覆盖了变化过程中的恢复和依赖关系，但还要回答一个问题：等待会不会永远结束不了？

这里需要新增前提。依赖优先关系必须无环，副作用迭代的步数有上界，整个运行中曾出现的实例名称集合有限。沿着“供给方还在等谁清理”向后寻找，有限无环图一定能走到末端；末端先完成清理，就能解除前面实例的等待。再利用有界迭代，沿依赖顺序约束各实例的变化次数，便能排除生命周期无限推进的情形。
这就是 Theorem 73 的进展性（progress）与终止结论。在上述条件下，添加、停用、移除插件等外部管理操作停止后，只要还有待处理的生命周期工作，就有合法规则能够推进；持续执行，最终到达没有待完成转移的静止状态（quiescence）。

能够结束，还不等于不同调度会得到相同结果。为继续论证，论文再要求插件激活完成时实际提供声明中的全部键，即 Definition 76 的完全履行供给声明，并且这里只讨论不含失败的运行。
此前的恢复与独立性保证，在这里再次被用上。证明先沿依赖和创建关系，从末端开始消去已经完成卸载的运行片段；这些片段产生的副作用已经撤销，因此不再影响受管终态。剩余步骤中的独立操作可以换序，于是能够保持插件管理操作的相对顺序，将加载过程按依赖与父子创建顺序整理，最后只留下最终活跃的每个实例各加载一次。换序与消去引理（Lemma 78–79） 支撑了这两步，最终得到的状态，等价于将这些实例按上述顺序静态组装起来的结果。这是在证明中整理执行历史，运行时无须真的重新执行一遍。

不同合法调度都能整理到这样的静态组装结果，最终便得到 Theorem 80 的合流性（confluence）。连同前提，其结论可以转述为：

在上述条件下，从相同初始状态出发，执行相同的插件管理操作并保持它们的顺序，不同合法调度到达的静止状态观察等价。这里允许不影响可观察行为的实例内部编号存在差异，但两边的编号须保持一致的一一对应关系。

最底层的撤销约定，在这里成为消去已恢复历史的依据；能力操作的独立性，成为调整剩余执行顺序的依据；依赖与生命周期规则，则保留不能交换的先后关系。组合到最后，动态系统的受管终态就能够用静态组装的结果来理解。这也回答了开头的问题：在这些条件下，系统经历过动态装卸，并不妨碍它最终得到与静态组装结果观察等价的状态。

§这些结论成立到哪里

撤销和独立性必须由插件实现来兑现，受这些保证覆盖的共享交互也必须经过 Context。运行时按规则组织操作，任意插件代码是否符合约定，仍需另行验证。论文证明了遵守这些约定能够得到什么，并没有证明任意接入的插件都会遵守约定。
进展性也不意味着所有插件最终都会激活，缺少依赖的插件可以停在未激活状态。无限创建实例、某一步永远不返回、外部管理操作持续发生，都超出了这里的终止保证。失败扩展允许按约定撤销失败前已完成的部分，但明确把失败情形排除在合流结论之外，不能据此推断成功与失败两条轨迹也有相同终态。

观察等价比较的范围同样有限。文件服务卸载，不会让已经发送的请求消失；两次调度终态等价，也不意味着中间发送消息的顺序相同。论文区分了受管状态与已经向外部发送的请求、消息等行为。申请、打开或创建资源时产生的可撤销副作用，与已经发生的外部业务行为，需要分别看待，不能把这里的保证泛化成整个业务过程都可回滚。

§从前端视角对它的评价

§熟悉的机制与不那么显然的保证

从前端经验看，我最初的感受没有变。副作用与清理成对、资源交给上层管理、显式依赖、变化通知、根据目标调整实例状态，都是熟悉的工程做法。只看“万物皆插件”和一个形似useEffect的 API，很难让我觉得出现了全新的架构思想。
熟悉这些机制，却不等于知道它们组合后在什么条件下仍然正确。先移除监听再关闭连接，几乎是资源管理的直觉。允许其他插件在中间工作，还要单独卸载其中一项，一条反序清理链就不够了。我们还得说明哪些操作独立、哪些必须排序，以及依赖改变时谁仍有权使用旧服务。论文把这些原本需要分别考虑的问题，组织成了一条可以检查的论证。

形式化的价值就在这里。工程上觉得“应该能清理干净”“这两个插件应该互不影响”，论文则要求说明这些判断成立的前提，再据此推导组合后的结论。撤销方法和依赖关系也被保存在运行时里，成为实际调度的依据。论文称这种处理为具象化（reification）。放到工程里看，就是让程序直接持有和管理这些原本需要人手协调的信息。

我更愿意把这里的创新概括为整套动态组合机制的组织与形式化。它说明了熟悉的工程做法怎样配合工作，以及哪些约定决定了保证的范围。对我来说，最值得学习的是接口设计与系统保证之间的这层联系。

§保证背后的工程化问题

这套模型让局部保证有了复用的依据。能力提供方封装资源的申请、创建及其撤销逻辑，并保证接口操作满足独立性；使用方遵守声明，运行时安排生命周期。新增插件时，可以沿这些接口约定推理，无须重新理解整个系统的实现。
前提是提供方把约定做对。它不能在 API 内部修改归属不明的共享状态，也不能交出会破坏其他使用方的撤销函数。普通业务插件未必需要自己实现所有清理机制，提供共享能力的那一层却必须承担这份责任。经过 Context 的代码，仍然可能写错。

现实中的故障也提醒人注意这段距离。DSH 的早期预览版讨论中，有用户报告第三方插件的语法错误使整个 profile 无法启动，也有人报告安装插件后加载了两份工具运行时，导致会话中的工具调用失败。这些是特定版本和环境下的用户报告，无法据此判断定理有误，也不足以把问题归咎于某一方。它们说明，模块加载、依赖版本和故障处理仍有各自的工程问题，一份组合性证明不会自动解决这些问题。

从模型走到可靠的软件，还需要插件作者和宿主维护者共同落实这些前提。依赖声明、资源归属或撤销逻辑出了偏差，实现就可能超出定理覆盖的范围。形式化让这份责任更明确，也让我们知道应该检查什么。

§这篇论文给我的启发

我原本想看 DSH 怎样组织 Agent，结果读了一篇插件运行时的论文，倒也没有白跑一趟。最有收获的是看到作者怎样围绕动态组合，把熟悉的工程手段组织成系统，再逐层论证它能提供什么保证。
我平时更习惯从眼前的问题出发。资源需要清理，就找清理机制；依赖需要管理，就找依赖注入。至于这些办法组合后，整个系统还能保证什么，我很少继续往下想。所以刚读论文时，很容易觉得“这不就是那些工程做法吗”。这次先从插件替换的需求往下梳理，再沿论文的论证往上走，才注意到自己平时略过了多少条件。
以后做类似设计，我想多问一步。除了知道监听怎样清理、依赖怎样声明，还要知道另一项功能同时变化时，这些约定能否继续成立。局部的办法怎样成为整个系统的保证，这是这次阅读留给我最有用的问题。