首先，想说声谢谢。数十万用户使用过 omp，报告故障、提出需求，共同塑造了它今天的模样。这篇文章和 omp² 本身，都因你们而存在。
听说 omp² 之后，很多人马上问：“可是，为什么要重做？”
给 fetch 套一个 while 循环，听起来很简单。但 OpenCode、Pi、OpenClaw 和 omp 都在同时进行全面重构，是有原因的：这类软件以前并不存在。只有从简单版本起步，我们才能看到裂缝，进而找到更好的实现方式。
无法避免的复杂性，必须有人负责。现在，复杂性守恒的天平偏向了扩展和用户，让人在 omp 或 Pi 之上几乎无法编写可靠的软件。我已经听到有人说：“什么？它的扩展机制明明又简单又好用。” 给我几章的篇幅，让我试着改变你的想法。
Dijkstra 写过，“简单是可靠的前提”，可他又以用算法解决寻路问题而闻名。为什么不直接暴力搜索？他根本不是在主张我们如今反复念叨的简单就是好，复杂就是坏。那句话是为了帮助实现者推理。可我们却令人惭愧地拿它当借口，让实现者不必推理。
Ousterhout 在斯坦福的讲义中补上了另一半。他告诉模块作者，要“拥抱痛苦”：接下难题，把它彻底解决，再让其他人轻松使用成果。把复杂性压到模块内部。让少数实现者承担它，而不是让每个调用者各自承担一份更小、又略有差别的副本。
不少读者应该还记得，那条把 Claude Code 比作游戏引擎的推文引发了一波梗图。这种比喻听起来有点牵强，但如果列出智能体运行框架（harness）的职责，先把渲染放到一边，其实相当吻合。
它维护一个权威的世界状态，把变更记入日志，执行不可信操作，将状态复制给多个视图，调度参与者，解释命令，适配互不兼容的协议，并渲染实时界面。
是不是很熟悉？游戏引擎似乎已经为这些同类复杂性负责了几十年。
接下来的内容，既是复盘，也是设计手册：
- omp 给我们的教训：指出我们在一个真实用户使用的系统中遭遇的失败。
- omp² 的改变：描述替代架构——其中一些已经实现，另一些还在推敲。
设计边界
在讨论智能体运行框架的任何子系统之前，先想象四种截然不同的产品都要依赖它：
- 多智能体共享工作区：多个智能体及子智能体在同一文件夹中工作的本地环境。
- 远程操控端：用户用手机上的远程客户端，操控云端智能体，或桌下那台机器上的智能体。
- 旁观端：通过 Web 客户端观看 Claude 智能体工作。
- Factorio：通过 SDK 处理不可信输入的自动化软件工厂。
这不是市场用户画像，而是架构测试。它们共同覆盖了那些会让运行框架不再只是聊天循环的维度：
| 测试场景 | 本地或远程 | 交互或自主 | 信任边界 | 并发 |
|---|---|---|---|---|
| 多智能体共享工作区 | 本地 | 交互式 | 大体可信 | 多个智能体，一个工作区 |
| 远程操控端 | 远程 | 交互式 | 主机与客户端分离 | 一个或多个智能体 |
| 旁观端 | 远程视图 | 只观察 | 不可信的展示输入 | 多名观看者 |
| Factorio | 远程或集群 | 自主运行 | 恶意仓库与工具输入 | 多个作业 |
只适用于第一种场景的设计，往往会把控制器偷偷塞进 TUI，把状态保存在闭包里，让扩展在引擎进程中执行，并假设一个没有资源或时间上限的调用出了问题，人总能救场。要同时经受住四种场景，设计就不得不建立更好的边界。
本手册余下的内容围绕五个推论展开：
- 唯一的权威会话。 回退、分叉、恢复、复制和检查，都必须从同一份记入日志的状态派生。
- 可信的控制平面。 策略和会话所有权留在主机；沙盒只接收有明确限制的执行请求。
- 有界工作。 工具调用、子智能体和后台作业，都应是可取消的流，拥有集中的限制与可观测性。
- 显式兼容性。 模型和提供商的特殊行为，应成为结构化知识，而不是散落在调用点的分支判断。
- 视图只是投影。 TUI、Web 客户端、远程客户端和子智能体检查器渲染同一份状态，而不是成为额外的权威来源。
这些约束贯穿全文。后面提出 DOM、convar、Director、微型 VM 桩程序或组件渲染器时，都是为了解决这五项需求中的某一项，而不是为了炫技去引入子系统。
第一项是基础：在决定代码在哪里运行、如何渲染之前，运行框架首先得知道什么才是真实状态。
状态
哪些东西必须保留下来
如果希望某个东西能持久保存、回退、容忍崩溃并支持分叉，你有三种选择：
- 保存产生它的历史。
- 保存你关心的属性变化。
- 保存机器本身。
Source Engine 在网络同步中使用了第二种方案的变体。omp 和 Pi 目前则……没有一致地采用其中任何一种。它们有事件，但状态并不真正源于这些事件，违背了事件溯源的首要原则：仅凭事件就必须能够推导出状态。
omp 给我们的教训：两个权威来源
replay(.dem) == original. Pi's journal covers the message tree only, while authoritative state lives outside it—rewind, fork, and resume all lie.走到这一步，原因可以理解。在每份日志里重复保存系统提示词和 AGENTS.md 确实浪费；对模板求哈希、保存变量就能解决。而且，这种状态建模方式在 TypeScript 中并不常见，毕竟它并没有真正的运行时类型。
但结果仍然是两个事实来源：
| 维度 | Source Engine | Pi 式运行框架 |
|---|---|---|
| 事实来源 | 就是 entity list。服务端模拟，客户端预测。 |
消息树加上待办状态、重试计数、子智能体注册表、流式标志，以及其他持久化层看不见的状态 |
| Δ 的单位 | { Δ entity ... }，覆盖所有字段，因为每个增量都是实体增量 |
message / custom / custom_message，没有引擎负责的状态归约；每个扩展手写推导逻辑 |
| 全局状态 | CCSGameRules 是一个单例实体，没有特例 |
分成三个层次，其中一个能正常工作 |
| 插件状态 | 插件写实体字段，所以状态默认就能网络同步和回放 | 模块级闭包：let turnCount = 0、new Map()、new Set() |
| 回放 | 加载 .dem，跳转到某个 tick，重新推导状态 |
加载 .jsonl；叶节点指针移动，其他权威来源却任意重置或保留 |
全局状态那一行尤其有意思。Source 没有会话全局变量，它们只是实体的属性。我们的全局状态却有自己的一套层级：
Source 的正确性，并非来自精心编写的协调器或出色的文档。它让不可回放的状态根本无法表示。正确性来自这个约束，而不是寄希望于每位扩展作者都记得注册两个钩子、定义一种更新结构。
证据：API 把正确性变成了可选项
我们检查了 Pi 的 78 个官方扩展示例。其中 60 个无状态；17 个有状态的示例里，只有两个是正确的。（译注：原文总数为 78，而上述两类合计为 77，未说明余下一个示例的归类。）
| 示例 | 脱离权威管理的状态 | 用户可见的故障 |
|---|---|---|
git-checkpoint.ts |
检查点引用由临时 Map 持有 |
/fork 执行前，agent_settled 已经清空检查点 |
plan-mode/index.ts |
从整个文件而非选中分支恢复计划模式 | 回退后限制仍生效；恢复会话可能让已废弃分支复活 |
status-line.ts |
轮次计数保存在闭包里 | 从第 3 轮回退到第 1 轮后，下一轮显示第 4 轮；恢复会话则从零开始 |
dynamic-tools.ts |
运行中的扩展注册表 | 工具在回退后仍存在，恢复会话后却消失 |
snake.ts |
恢复时扫描了废弃分支 | 废弃分支的存档重新出现 |
bookmark.ts |
“最后”按文件顺序定义 | 给废弃分支上用户看不到的助手消息加了书签 |
kimi-deferred-tools.ts |
没有重新推导活跃工具列表 | 回退到发现之前，Calculator 仍处于活跃状态 |
auto-commit-on-exit.ts |
关闭事件混淆了进程退出和会话切换 | /new、/resume 或 /fork 会提交工作树 |
tic-tac-toe.ts |
实时写入与恢复读取使用不同条目类型 | 崩溃可能让用户的一步棋消失 |
细节见附录 A。重点在于，文档无法修复这样一整类分散的缺陷。引擎需要让状态只能存在于一个地方。
tic-tac-toe.ts：落下 X，在 O 回应前崩溃，再恢复会话，X 就消失了。实时写入与恢复读取使用了不同的条目类型。omp² 的改变：一份物化会话
如果整个会话物化为一个 DOM 呢？当然，你也可以使用带序列化的 ECS 系统，或者其他任何表示形式。我主要选择 XML，是因为它让状态非常容易组合、检查和调试。
<meta>
<todo>…</todo> <!-- persistent components, journal-derived -->
<jobs>…</jobs>
</meta>
<body> <!-- the live chain, entries as elements -->
<user id="e12">…</user>
<ai id="e13">…</ai>
<Read id="e14" status="ok">
<input path="src/main.rs:1-80"/>
<result lines="80">…</result>
</Read>
</body>
<queues>
<steering>...</steering>
<prompts>...</prompts>
</queues>
它的事件就是属性变更流：
: todo.done
event: patch@1
by: e41
data: {"ops":[["set",412,"status","completed"],["set",415,"status","in_progress"]]}
树是权威来源，日志保存树的增量变更。运行时对象可以缓存它、为它建立索引，但不能成为第二个保存事实的地方。在日志的任意位置，运行框架都能物化整个会话，因此也能为整个会话生成快照。
唯一权威来源带来了什么
状态与会话记录放在同一棵树中后，几个难题就都归结为同一种操作。
回退就是 DOM diff。 对当前物化状态和目标状态求差异。一个 <subagent> 元素消失了？销毁元素，终止它。出现了一个？创建元素，恢复或启动它。增量本身，就是完整的生命周期待办清单。
新增有状态功能，不会给回退、分叉、恢复或复制增加任何调用点。
提示词成为投影。 不再需要给每个模板传入一个长达 100 行的状态对象。系统提示词读取的，是与其他部分相同的那棵树：
- {{ count(select("todo item[status!=completed]")) }} open items
复制成为订阅。 应用逻辑和状态推导已经具备了。远程客户端消费补丁流，而不是追踪文件尾部。远程操控端和旁观端不再需要单独的状态传输管线。
渲染成为投影。 组件注册表可以根据相同的元素状态，渲染 Read、Bash、消息或子智能体。流式参数修改 <input>，流式输出修改 <result>。第七章会把它落成类型化界面，而不是又一个定制渲染器。
控制器与参与者
这种分离也让子智能体可以被检查。Pi 的视图直接读取实时会话状态——页脚调用 sessionManager.getEntries()——因此，要新增“检查子智能体”，就得把控制器状态穿过 UI 内部层层传递。
让控制器和参与者彻底分离：控制器拥有会话状态；参与者只渲染状态快照及补丁流。TUI、远程客户端和子智能体检查器成为平等的客户端。检查子智能体，只需要把同一个参与者指向子会话的状态。
忠实的状态模型是基础，但如果不可信代码掌控了修改状态的策略，这个基础依然会被破坏。下一章将划定运行时边界。
运行时
状态一章确立了运行框架认定的事实。运行时一章决定谁能修改它、不可信工作在哪里执行，以及当执行可能持续数小时、流式输出、甚至无视礼貌的停止请求时，“工具调用”究竟意味着什么。
沙盒应该执行，而不是决策
从设计边界里的 Factorio 场景出发。假设我们克隆 roboomp，让 gpt spark 把所有名字替换成 CodeWhatever，然后凭这套神奇技术向用户收取成千上万的费用。工具由谁运行？当然是 VM。嗯，真这么简单吗？
把执行器放进 VM 后，会发生这些事：
嗯，这行不通。因为：
- 程序化使用工具，需要访问所有工具；我们不能任意拆开操作运行框架状态的工具和操作环境状态的工具。
- 我们得构建双向网关，让 VM 能调用主机工具；这会：
- 违背初衷——要么给 DoS 开绿灯，要么对自家 VM 的某些操作做限流。
- 让事情更复杂。谢谢，不必了。
好吧，那把驱动应用也放进 VM！
- 现在，应用提示词和内部源码都泄露了。除非把应用移出 VM，通过网络 RPC 连接运行框架，并把会话存储也移出去。
- 可会话存储在外面，就得授予 VM 写入权限，于是又同时回到了问题 1 和问题 2。
解决办法是：在 VM 里只放一个听命行事的桩程序，并且非常谨慎地限制回传数据流的最大体积——你不会想让一次误用的 Read 调用返回 2GB 响应：
这些图最终指向同一条边界：
- 主机拥有会话状态、模型推理、策略、工具路由、审批、限制和日志记录。
- 沙盒通过一个小巧、只负责执行的协议，管理环境内的执行。
- 所有回传流都受到限制，不能让不可信一侧耗尽主机内存或上下文。
这种安排满足 Factorio 场景，也不会让本地使用变差。同一个主机可以让桩程序面向本地进程、容器、VM 或远程机器。
子智能体跨越的是同一条边界
部署位置不只是主机与 VM 的区别。子智能体在文件系统层面也需要相同边界：worktree 只隔离受跟踪文件，而 pi-iso 利用 APFS、btrfs、ZFS、overlayfs、ProjFS，或以复制作为后备方案，为每个子智能体提供整个工作区的写时复制视图。子智能体独立修改，父智能体接收 diff。
子智能体获得视图，返回变更，不共享父智能体的可变权威状态。这是同一条主机／沙盒规则在文件系统层面的体现。
omp 给我们的教训：一次调用，三个脱节的 API
那么，工具该怎么定义？稍后再谈最初做过的修改，不过核心契约基本没变：
export const myCustomTool: ToolDefinition = {
name: "my_tool",
parameters: mySchema,
// 1. Called during argument streaming & before execute()
renderCall(args, theme, context) {
if (context.argsComplete) {
// Trigger async preview computation
}
return new Text("Pre-execution preview UI...", 0, 0);
},
// 2. Main execution
async execute(_id, params) {
/* ... -> string */
},
// 3. Called after execute() settles
renderResult(result, options, theme, context) {
return new Text("Final execution result UI", 0, 0);
},
};
这个契约看起来简洁可爱，却把一个操作拆成了三个互不相关的阶段。预览、执行、模型看到的结果、人看到的结果、诊断、流式更新、取消和日志记录，描述的其实都是同一次调用。API 却迫使它们假装不是一回事。
回调拆分导致重复工作
首先，拆开渲染路径后，响应式更新变成了可选项。即使工具的显示形态没有突然切换，作者也得重复编写许多展示逻辑。
更大的问题在于 execute 的工作方式。以 Edit 为例：
renderCall打开文件，最好还把读取内容缓存到某处——哪里呢？——然后应用修改并渲染 diff。execute再次打开文件，应用全部修改、写回，并以模型友好的格式返回 diff。renderResult拿到这个 diff 后，还得解析我们选定的格式！为什么？因为人当然想看带颜色、带高亮的版本，也许还要更漂亮的行号。
这种直觉式实现带来了：
- I/O 浪费：文件打开两次。
- CPU 浪费：修改结果不是算一次，也不是两次，而是每个字符变化时都从头算一遍——
renderCall不是协程！ - 对任意格式进行不必要的序列化和反序列化：为了实现
renderResult，我们必须解析模型输出；或者把信息塞进 details，导致日志重复保存数据。
要提高效率，就得在这个定义之外实现并驱动一个协程，找地方保存其句柄，而且整套结果反序列化逻辑仍然跑不掉。
问题不只是代码重复。这个契约缺少一个权威对象，来承载从“参数流式传入”到“运行中”再到“已结束”的状态演进。每种实现都得为这套生命周期发明一条旁路。
omp² 的改变：执行就是状态流
此外，也没有通用方式添加结构化警告、诊断或截断通知。大多数 Pi 工具最终都会做类似的事：
text += `\n${theme.fg("warning", `[Truncated: ${truncation.outputLines} lines shown (${formatSize(truncation.maxBytes ?? DEFAULT_MAX_BYTES)} limit)]`)}`;
模型只能猜测工具数据在哪里结束、运行框架的说明从哪里开始。由于 execute 不是生成器，流式输出又需要在更新通道上叠加一套协议。
DOM 模型消除了这两种特例：
- 流式输出修改
<result>的内容。 - 添加警告就创建
<diag severity="warn">。
执行期间，客户端接收这个状态的补丁。执行结束时，把相对上一状态的最终 diff 记入日志。
在统一会话模型里，一次调用就是一个包含结构化子节点的元素：
<Edit id="e41" status="running" version="3">
<input i="Update the parser without changing the public API">…</input>
<result>…streaming structured state…</result>
<diag severity="warn">…</diag>
<usage tokens="0" elapsed-ms="842"/>
</Edit>
执行器在运行时修改这个元素。模型、用户、日志、远程客户端和测试框架，观察的是同一状态的不同投影。执行结束后冻结最终 diff；客户端不再需要解析结果字符串，去重建序列化之前原本就存在的丰富对象。
限制是原语的一部分
Pi 的工具没有限制：返回 1 MB 文本，它就会原样转发给模型。暴露这样的原语，层次太低了。
统一限制输出
Pi 自己在 Bash 和 Read 上也遇到了这个问题，于是导出一个截断工具函数，供各实现复用。omp 为它增加了产物系统，让模型可以读回保留的完整输出；但责任仍然和 Pi 一样，落在每个实现身上。
向模型发送 1 MB 数据，也许值得保留为一种能力。但应该由集中实现默认截断，允许通过显式的 notrunc 属性退出，而不是让截断这种良好设计成为主动选择。辅助函数保持可选，会带来两类问题。
大多数工具都需要某种截断，所以可选辅助函数必然覆盖不均：
- 不知道这个函数存在的作者，各自实现，提示文本略有不同。
- 从没想到结果可能很大的作者，什么也不做。
在工具实现内部而不是对话渲染层截断，又会破坏 Code mode：
- 智能体在
Eval中无法放心依赖工具输出；每次都得先从数据中解析并剥离运行框架通知。 Eval的结果本身也可能被截断，因此每次调用都会在同一份数据外面叠出 N+1 层独立截断。
统一限制阻塞时间
把任何东西转入后台、限制调用最多阻塞多久，也应由库层负责，而不是由碰巧运行较久的工具各自处理。
第一个原因是缓存和用户体验。否则，意外的长调用会让智能体无法及时发现并调整；用户回来时看到卡住的会话；自主作业无限等待；提供商的 KV 缓存甚至会在调用返回前过期。
第二个原因是重复实现，omp 也犯了这个错。每个工具自己实现后台运行，就会各自长出 spawn、poll、message、kill 和 list 辅助接口。看看 Claude 为自己的 Task 和 Bash 工具画的这张图：
两者最终都收敛到进程接口：signal + stream in + stream out。后台 shell、子智能体、开发服务器守护进程、远程函数，以及超出预算的普通调用，其实都是同一种对象：带 stdin、stdout、退出状态和信号句柄的作业。应由一个具有 stdio 形态的作业原语封装它们。这样，阻塞预算在一处执行，溢出输出写到统一产物路径，检查、发消息或终止任何作业都使用同一个接口，而不是每个工具各抄一份。
对可观测性的期待也相同。想看子智能体状态的用户，也想看后台 shell。在不同运行框架实例间互相发消息的智能体，也想看到对方运行的守护进程，这样同一目录中的 N 个智能体就能共享一个支持 HMR 的 bun dev，而不是在 N 个端口启动 N 份副本。
取消需要可强制终止的边界
扩展——也就是自定义工具——与引擎共享 JavaScript isolate，会酿成灾难。真正的热重载几乎不可能实现；工具调用一旦脱离协作式取消机制，就无法被强行停止。
JavaScript 和 Go 通过 AbortSignal、context.Context 提供取消机制：这些协议很有用，却没有强制执行力。忘记传递信号、调用不接受信号的依赖、执行同步工作，或进入无限重试循环，都会让超时仅仅告诉智能体继续往下走，而原来的工作仍可能在后台消耗资源。
因此，安全的主机必须拥有真正可以终止的执行单元——进程、worker、子解释器、VM 请求，或其他等效边界；终止它不能连会话权威状态一起毁掉。取消属于运行时契约，不能靠每个工具作者自觉。
让必要的边界好用起来
刻意保持简单的沙盒桩程序，还带来最后一个 SDK 问题：扩展作者现在面对两个文件系统。一个自定义编辑函数，可能不得不从一边读取文件，完整传输到另一边，再写回去。
这就是 omp² 为扩展选择 Python 的原因。Python 可以通过标准库检查自己的 AST，打包函数所需源码，再提交给另一个运行时；@remote 标记可以把看起来像本地函数的调用变成 RPC。Modal 的 Python SDK 等系统中，远程函数之所以自然好用，也是因为这个特性。
自带 Python 运行时，还让 Eval 变得可靠，不必依赖用户恰好安装了哪个解释器。一举两得。
工作有了可信的负责人和可取消的执行原语之后，运行框架仍然需要一套一致方式来控制配置值和多轮行为。这就是控制平面。
控制平面
运行时负责两种不同控制。配置值回答当前使用哪个模型、服务档位、主题或策略；行为回答智能体是否可以交还控制权、是否必须再运行一轮，或是否临时需要某项能力。如果每个调用者都维护私有 setter 或标志，两者都会失去一致性。
配置值：在定义设置时声明策略
配置系统也变成了雷区：脏状态跟踪，多层配置——全局、会话级、临时级……大多数 get/set 操作像 Pi 一样，都经过 AgentSession 类型，因为变更必须持久化到 JSONL。
知道哪个配置系统多年前就解决了这些问题吗？没错，Source Engine！
尤其值得一提的是，玩过 Valve 游戏的人，大多不用查就知道 sv_cheats 做什么。大家自定义配置这么多年，我想不起有什么用户对此不满。其他软件的配置，你能想出类似例子吗？
convar 是一个带类型的变量，包含名称、默认值、帮助文本和一组标志位，在定义处声明一次：
ConVar sv_gravity("sv_gravity", "800", FCVAR_REPLICATED | FCVAR_NOTIFY, "World gravity.");
持久化、所有权、作用域、复制，甚至回放是否忠实，都是变量的属性，从定义之初就说清楚。没人需要通过一个上帝对象执行 set，也没人手写脏状态跟踪。
sv_cheats, ARCHIVE decides what reaches config.cfg — and every change is stamped into the .dem.convar 不是会话 DOM 旁边的第二个配置数据库。会话级 convar 就是权威树上另一个记入日志的节点；其标志声明它如何参与恢复、回退、派生子会话、复制和归档。
继承不该需要第二个设置
如今 omp 的服务档位，也就是 /fast，专门给子智能体设了另一项配置。
tier:
openai: priority
subagent: inherit # separate setting
在 convar 体系里，ai_fastmode 只有一个变量，标记为 SESSION：随会话写入日志，恢复时自然恢复其值。继承甚至不需要标志：默认情况下，新建子会话的所有变量都以父会话当前值初始化，无需主动启用。
想把子会话固定到特定值？一行就够：
# subagent.cfg — auto-exec'd for every spawn
ai_fastmode 0
# sonic.cfg — auto-exec'd when a sonic spawns, class config
ai_model @smol
ai_thinking low
主会话用 config.cfg；任意数量的用户 cfg 都能充当配置方案；每次派生子会话自动执行 subagent.cfg，再叠加 <agent>.cfg。顺便解决了那个拥有一千个属性的上帝对象。TF2 早就知道该怎么做！
现在，一个值就能描述主会话及其子会话。继承规则位于变量定义处，不再成为不断膨胀的会话上帝对象上的又一个属性。
配置方案和快捷键沿用同一命令通道
有了 cfg，再加上绑定就更好了——bind、toggle 和 alias 本身也是控制台命令。我们不断为之发明 schema 的各种输入模式，都能留在同一命令体系里。用户想绑定一个隐藏思考内容的快捷键？
bind ctrl+t "cl_showthinking 0" # careful — one-way; the second press still writes 0
bind ctrl+t "toggle cl_showthinking" # there we go; toggle also cycles value lists
alias +thinkhud "cl_showthinking 1" # fires on key-down...
alias -thinkhud "cl_showthinking 0" # ...and on key-up
bind ctrl+h +thinkhud # hold to peek at the thinking stream
这才应该是我们的快捷键层，而不是一套附带独立默认值表的专用 schema！
命令流把一切连接起来：cfg 文件、控制台输入、别名、按键绑定、远程管理和日志回放，都围绕同一批声明变量，使用同一种语言。定制不再催生一套又一套一次性 schema。
行为：循环形状的缺口
另一个值得关注的话题是可扩展性。我认为 Pi 的扩展层确实很出色，但它有一个“循环”形状的缺口。
我安装了 Pi 中最流行的 Plan 和 Goal 实现，同时启用两者，结果是：
好吧！有意思，可这里并没有“工作流”API。那它们怎么实现的？答案是各自定义：
export const WORKFLOW_MUTEX_CHANNEL = "workflow:mutex:v1";
export const AGENT_WORKFLOW_GROUP = "agent-workflow";
export class WorkflowMutex {
private session: object | undefined;
private readonly heldGroups = new Map<string, WorkflowMutexOwner>();
private generation = 0;
private readonly pi: Pick<ExtensionAPI, "events">;
constructor(pi: Pick<ExtensionAPI, "events">) {
this.pi = pi;
pi.events.on(WORKFLOW_MUTEX_CHANNEL, (payload) => {
this.answer(payload);
});
}
原来如此！这两个实现来自同一个作者。他遇到这个问题后，做出了一套能在自己那组插件之间协作的方案。
引入系统来封装这种行为的复杂性，被转嫁给了插件作者；而他们只能构建在自家扩展之间有效的系统。
omp 也有类似问题：
// modes/interactive-mode.ts — the exclusivity "system", in its entirety
if (this.goalModeEnabled || this.goalModePaused) { this.showWarning("Exit goal mode first."); return; }
if (this.vibeModeEnabled) { this.showWarning("Exit vibe mode first."); return; }
// …restated by hand at six other entry points
独立编写的行为一碰面，缺失的抽象就暴露出来了。私有互斥锁可以防止同一作者的 Plan 和 Goal 插件冲突，却无法让任意扩展组合。omp 手写的模式检查也有同样的局限。
由此得出两个决定：给负责控制循环的原语一个名字——Director——并把更多内置行为移到公共扩展接口上，让接口的缺口无法再被忽视。
Director 负责裁决候选交还点
智能体有一个循环。越来越多的功能想指挥这个循环：plan 希望在计划完成前再运行一轮，goal 希望在目标完成前再运行一轮，/force 希望改变下一次模型推理，待办提醒希望在交还控制权之前再获得一次提出异议的机会。
那就给智能体层一个统一负责这项决策的对象：Director 栈。
这里的“栈”指会话 DOM 中一棵实时子树，不是一个承诺以后再序列化的 Python 数组。DOM 才是权威来源；运行时只是遍历它。
candidate yield flows this way ────────────────────────────────┐
▼
Base → TodoReminder → Goal → Plan → ForceTool(write)
parent child/top
循环依旧平平无奇：
while True:
request = directors.prepare_inference(base_request) # outside → inside
turn = await inference(request)
await execute_tools(turn)
if turn.has_tool_calls:
continue
decision = await directors.on_yield(turn) # inside → outside
match decision:
case Continue(): continue
case Yield(): return
prepare_inference 从外向内遍历栈，让最内层行为可以细化父级即将发出的请求。on_yield 则反向向外遍历。每个 Director 可以：
- Pass：让下一个 Director 检查这次候选交还。
- Continue：接管这次交还，继续运行一轮。
- Yield：接管这次交还，真正把控制权交给用户。
- Push：在自身上方压入一个子 Director。
- Done：弹出自身，再把同一次候选交还提交给父级。
- Fail：带错误弹出。
因此，回退会移除 Director，恢复会话会还原它们，远程检查器也能看到当前由哪个行为负责裁决候选交还。
完整实现计划模式
假设计划模式已经启用，模型还没写计划文件就想交还控制权。Plan 会先于任何外层行为看到这次候选交还：
class Plan(Director):
async def on_yield(self, agent, turn):
if not turn.wrote(self.plan_file):
return agent.force_tool(
"write",
until=lambda turn: turn.wrote(self.plan_file),
reminder="Write the plan file before yielding.",
retries=3,
)
if not turn.called("ask") and not turn.proposed_plan():
return agent.force_tool(
"required",
until=lambda turn: turn.called("ask") or turn.proposed_plan(),
reminder="Propose the plan, or ask the user what is missing.",
retries=3,
)
return Yield()
随后，软模式下的 force_tool("write") 会压入一个小型内置 Director，向下一次推理请求添加相应能力要求：
class ForceTool(Director):
def prepare_inference(self, request):
return request.with_tool_choice(self.tool)
async def on_yield(self, agent, turn):
if self.until(turn):
return Done() # pop; offer the yield back to Plan
if self.retries_left:
return Continue(self.reminder)
return Fail("tool requirement exhausted")
Plan 下方原本还有另一个 Director：
Base → TodoReminder → Plan
候选交还先到达 Plan。Plan 活跃时，要么继续，要么压入子 Director，要么直接把控制权交给用户。它不会 Pass，所以外层 TodoReminder 看不到这次交还。
扩展使用完全相同的接口：
await agent.direct(VerifyBeforeYield(...))
<directors>
<todo-reminder id="d1">
<plan id="d2" plan-file="local://auth-plan.md">
<force-tool id="d3" tool="write" attempts="1" max-attempts="3"/>
</plan>
</todo-reminder>
</directors>
这是一套完整的组合机制，而不是又一个特殊模式。Plan 负责交还决策，临时压入 ForceTool，在子级结束后重新收到同一次候选交还，再决定继续还是交给用户。
钩子、Director 与模型推理
- 钩子观察或修改一次推理或一轮执行。
- Director 可以跨轮次保有控制权，拦截交还。
- Director 能以有明确语义的方式堆叠、嵌套、结束，并恢复父级。
这足以让 plan、goal、vibe、autoresearch、提醒和外部验证行为使用同一个智能体层原语，无需让每种行为了解其他所有行为的私有标志。
ForceTool 表达的是语义请求：“下一次成功的轮次必须调用 write。”它不知道所选提供商有没有原生 tool_choice，不知道强制调用会不会破坏缓存，也不知道本地模型是否需要额外提示。这个转换属于推理层。
控制平面现在能够表达应该发生什么。下一章要让这份要求在互不兼容的模型和提供商之间，仍然具有相同含义。
模型推理
控制平面请求的是语义行为：让这个模型流式输出，强制使用那项能力，约束这种结构，统计这些 token。推理层则必须把请求转换为：这个具体模型，在这个具体主机上，通过这个具体 API，实际能做到的事情。
omp 给我们的教训：特殊行为会变成架构
这点很好解释，因为 omp v1 已经有一个前后对照提交。
在 dd57045396 之前，OpenAI 兼容性逻辑集中在一个 880 行的文件里，围绕一个巨大的构建器展开。打开文件，迎面就是：
const isCerebras = modelMatchesHost(hostModel, "cerebras");
const isZai = modelMatchesHost(hostModel, "zai");
const isKimiModel = isKimiModelId(spec.id);
const isMoonshotKimi = isKimiModel && isMoonshotNative;
const isAnthropicModel =
modelMatchesHost(hostModel, "anthropic") ||
isClaudeModelId(spec.id) ||
isAnthropicNamespacedModelId(spec.id);
// …then DeepSeek, Qwen, MiMo, Grok, Mistral, OpenCode, local servers
这些布尔值又派生出其他布尔值，再经过几层嵌套三元表达式，最后生成一个巨大的 compat 对象。Kimi 能不能在思考时强制调用工具？取决于哪个 Kimi、运行在哪个主机、通过哪个 API。这个回环地址代表 llama.cpp，还是代理其他服务的 LiteLLM？再加一个特判吧。
单看任何一个分支，都没有错！每个分支都修复了真实的提供商问题。问题是，同一份知识最终被编码到了多个地方：
compat/openai.ts：880 行。model-thinking.ts：977 行。variant-collapse.ts：1,776 行。- 独立的 Bedrock、Anthropic 和 Devin 兼容性构建器。
- 服务发现和提供商序列化器里，还有更多基于名称的识别逻辑。
替代它们的是什么？
taxonomy/ "what model is this string?"
classes/ "what is true of this model lineage?"
providers/ "what does this host change?"
现在，Anthropic 的思考能力规则读起来是这样：
class "anthropic" {
on "anthropic" "amazon-bedrock" "google-vertex" {
family "sonnet" {
revision ">=3.7 <4.6" { thinking-mode "budget" }
}
revision ">=4.7" {
thinking-mode "anthropic-adaptive"
}
}
}
这才是我们真正想表达的知识！Sonnet 4.6 之前的版本使用预算式思考；Anthropic 4.7 及之后使用自适应思考；而且只对已经验证过的主机作此判断。
KDL 本身并没有魔法。真正让我们避免用更漂亮的格式重建一团乱麻的，是编译器：
- 未知指令或取值？报错。
- 两条同等具体的规则设置同一项？报错——文件顺序不能偷偷决定谁赢。
- 没有匹配规则？是未知，不是“false”。
这让提供商不再古怪了吗？当然没有。我们仍有 requires-mistral-tool-ids、qwen-preserve-thinking、strip-deepseek-special-tokens 这样的兼容性维度，还有十种“关闭推理”的写法。看看这些名字，真让人想哭。
它免除的，是为下一个怪癖再到四个函数里各加一个分支。现在只需在负责这个事实的地方写一条规则；优先级有歧义，编译器就会大声报错。推理层终于能回答：这个具体模型在这个具体主机上，到底支持什么？
收益不是怪癖更少了，而是每个事实都有唯一负责人、优先级明确，并且当库尚未确定答案时，能表示 unknown。运行框架其余部分，不再靠提供商名称分支反复猜测模型身份。
提供商不只是 stream
我为 Pi 实现 Web 搜索插件时，这个问题几乎注定会回来找我。事实上，同样的压力也冲击了仓库最初的极简设计，Pi 新增的图像模型实现就说明了这一点。
Pi 将提供商建模为 stream 和 streamSimple，基本就这些！这很适合快速接入一个提供商，却不适合在其上不断叠加能力，因为：
- Anthropic 的 token 计数接口怎么办？
- Codex 的 WebRTC 语音端点和远程压缩呢？
- Anthropic／OpenAI 的 Web 搜索呢？
- 嵌入向量呢？
- 图像／视频生成呢？
- 分词呢？
- 用量查询呢？
- 模型发现呢？
你觉得每个做这些事的扩展，都正确实现了同步协调的 OAuth 刷新和重试吗？
此外，能使用推理提供商最新的控制能力，本身就很有价值，例如：
- 约束采样。
- OpenAI 的文本详细程度选项。
- Google 的上下文过滤选项。
- 强制工具调用。
- Developer 角色。
- 会话中途的系统提示词。
- ……
认证刷新、重试、token 计数、搜索、生成、发现和提供商原生控制，都是共享基础设施。把它们留给扩展，就必然会出现同一协议的多个残缺实现。
能力策略：强制工具调用
强制工具调用很好地说明了，为什么“支持一个标志”还不够：
- 遇到不支持的提供商就报错：任何原生功能想使用它，都得排除一大批模型。
- 悄悄忽略：调用者意外得到尽力而为的执行路径，只能自己发明强制执行循环。
- 盲目透传：提供商的副作用会变成产品缺陷。例如，Anthropic 的强制调用可能导致整个对话缓存未命中。
- 不暴露能力：了解内情的调用者会绕过库，把上述三种失败模式再实现一遍。
理想的运行框架实现应当：
- 始终注入软提示，告诉模型下一轮必须调用该工具。无条件这样做是值得的：OpenAI 等托管 API 会悄悄替你加上这种提示，开源推理引擎却不会。因此，vLLM 后面的模型可能面对一个从未被告知的硬约束，在启用推理时无所适从。软提示抹平了这项差异。
- 只有没有额外代价时，才设置原生标志。如果提供商支持强制工具调用且无副作用，就透传；如果有代价，就跳过标志，只依靠软提示。
- 不服从时逐步升级。如果模型没有调用工具，就在有限次数内重试；最后手段是在有代价的情况下也设置原生标志。说服失败之后，正确性优先于缓存。
这是上一章 Director 在提供商一侧的实现。ForceTool 声明不变量；推理层选择成本最低、又真正满足要求的方式，并在模型不服从时升级措施。
工具 schema 是面向模型的协议
工具的 parameters 字段严格定义参数结构。对人类 API 来说很理想，但模型不是通用 API 客户端。它们的错误往往与工具名、以及训练中见过的运行框架有关。
强化学习优化到极致的智能体，可能拿另一个框架的 schema 调用熟悉的工具。Composer 模型有时会按自己预期的结构生成 Grep 调用，即使根本没有 Grep 工具。Codex 看见 paths: string[]，也可能随当天心情传来一个用 ; 或 , 分隔的字符串。
因此，库既要验证，也要纠正。对工具的语义契约严格，对模型的方言宽容：映射没有歧义时，把 paths: "a,b" 修复成列表；否则返回结构化、可重试的错误。一个原始的 JSON Schema 验证器，无法独自承担这一层。
严格采样需要预算与方言管理
约束采样是我们最早加到 Pi 上的功能之一：
+ strict?: boolean;
+ customFormat?: { syntax: "lark" | "regex"; definition: string };
+ customWireName?: string;
几个月后，Pi 也加入了 LARK 和 strict 支持，但只把它暴露为供提供商层透传的不透明结构。两项全局约束决定了，这样还不够：
- strict schema 容量是共享预算。 许多提供商限制 strict schema 的数量。独立编写的扩展装得足够多，提供商就可能拒绝每一次请求。用户不该为了让框架恢复工作，靠二分排查并修改插件。
- 语法方言因提供商而异。 把同一份 LARK 语法传给所有提供商，本身就可能无效。扩展无法维护完整兼容性映射，因为用户可能通过原生主机、代理或自定义提供商访问同一个模型。
因此，这套看起来“复杂”的实现应该属于推理层：
strict actually takes: provider capability, a strict-schema budget with priorities, per-dialect normalization, and a client-side repair path—none of which an opaque pass-through struct can provide.扩展声明意图——严格程度、语法、优先级。推理层负责能力、预算、方言归一化、回退、修复和最终传输格式。
纠错式推理
推理库还需要：
- 修复格式错误的 JSON。
- 检测 Gemini、DeepSeek 等模型的重复循环。
- 解析各模型的输出方言；结构化输出泄漏到文本时，合成为规范的
tool_call和think块。
工具调用方面的细节，可以看我的前一篇文章。支持一个提供商或模型，不只是接上 URL，还得处理它的个体怪癖。
提供商适配器能打开流，不代表它已经完整。只有在遇到畸形 JSON、重复、泄漏的推理内容或模型特有的工具调用方言时，框架其余部分仍能收到一个规范轮次，适配才算完成。
压缩应该调度，而不是临界触发
这里，天真的设计恰好也带来了最糟的体验：用户最投入的时候，却要等待整个会话中最大的一次请求。
除了 Snapcompact 这样的方法，还有很大改进空间。
更好的做法，是在距离上限约 10% 时，提前试探性启动压缩。相当于把对话分成两个并发版本：一边让用户和模型继续工作，另一边由模型压缩对话。
收到压缩结果后，再把它拼接进另一分支。这样还能保持工作势头：模型不会因历史里只剩一条交接消息而困惑，而是能看到那些它本来就应该完成的进展。
除了提示词，还有几种值得考虑的方法：
- 远程压缩：由提供商在服务端完成。OpenAI API 返回一个不透明状态 blob；由于服务端能访问解密后的思考内容，可以显著缓解上下文损失。
- 交接：不要让模型“总结”，试着让它“交接”工作。
- Shake：完全本地执行，直接裁掉历史中体积较大的工具结果。
注意，这也应该体现在 UI 渲染与请求渲染的抽象差异中。用户查看历史时，会希望所有消息仍保持原样；但对模型而言，那些消息已经不存在了。因此，构造请求时，应把提示词历史中的每个条目建模为一个归约步骤 fn(this, req) -> req，并在 <Handoff> 的实现中处理。
用小型本地模型处理框架内部工作
微型本地模型超级有用！即使你只用前沿模型工作，我也建议内嵌一个 tiny 模型，尤其可以看看 LiquidAI 的模型。分类、生成标题、翻译、判断用户对对话进展是否满意等小任务，都能省下大量延迟和费用。当然还有 TTS／STT，本地已经可以获得业界领先的表现。
这不是第二个“智能体”，而是一项低成本的内部能力，用来处理不该支付前沿模型延迟和费用的小任务。
兼容性和修复集中处理后，常驻工具接口就能保持精简。下一章讨论的是：什么值得在每次请求中占据一个 schema，什么绝对不值得。
工具接口
运行时一章定义了工作如何执行，推理一章定义了 schema 如何适配模型和提供商。现在终于可以问产品层面的问题：哪些操作值得占用模型的常驻语法？
每个 schema 都有成本
向模型提供大多数工具的最好方式，是根本不把它们放进常驻工具列表。
前阵子，有人抱怨 omp 在同一个任务上比 codex 慢——不是 token 用量，而是实际耗时。我本以为这没什么实质问题，没想到竟然是真的，甚至接近两倍！
sol, median of 6 runs, fresh session each · cyan = omp variants, grey = external references · annotations are deltas vs the row above.罪魁祸首是工具列表。限制为五个核心工具后，耗时就变成 36.6s，快于 Codex 的 42.2s 和 Pi 的 37.0s。为什么？工具语法！即使对模型只是文本描述，对大多数前沿模型提供商来说，它也会实际参与 token 生成过程，促使模型始终输出有效 JSON——这还不算描述本身消耗的 token。
不能因为模型可能会需要，就认为加一个工具是零成本收益；这也是动态工具发现背后的思路。但动态方式一改变工具列表，就会使缓存失效，所以我们并不太喜欢它。
Pi 有一点做对了，我们一直赞同：MCP 的设计很糟，不该进入常驻工具层。那怎么同时满足想用 Figma MCP 的用户，以及模型推理的约束？
动态工具发现避开了常驻语法成本，却在每次列表变化时让缓存失效。更好的目标，是稳定而极小的语法，再通过普通组合方式触达长尾能力。
把长尾能力放在稳定接口后面
来认识 dyn CLI！当然，它不是真正的独立 CLI，而是我们的 Bash 实现暴露的内置命令。它给模型提供稳定的发现协议，既能方便地从 Bash 调用，也能在 Eval 中作为 Python 函数使用。
dyn
dyn --q github
dyn github/list_prs --state open | jq '.[] | .title'
cat query.sql | dyn database/query - --params limit=5
dyn image_gen "blueprint of a frog" > result.json
找到感兴趣的工具后，和工具搜索一样，用 --help 获取详情：
$ dyn github/create_pr --help
dyn github/create_pr <title> [OPTIONS]
Arguments:
<title>
Options:
-d, --draft / --no-draft
-r, --reviewers <TEXT>[,…] (repeatable)
-p, --pr-meta.priority <INTEGER>
-m, --pr-meta.notify / --no-pr-meta.notify
-j, --json <JSON>
-h, --help
这些自然都是从 JSON schema 自动生成的；光有 schema，就足够生成一套好用的 CLI 映射。
面对大输入时，这种方式尤其方便：
dyn database/query "SELECT 1" # literal
dyn database/query @query.sql # file contents
cat query.sql | dyn database/query - # stdin
还得处理一个边界情况：返回图像的工具怎么办？omp 通过什么给你显示图像？Sixel 或 Kitty 协议，对吧？那就在 Bash 工具中解析相同输出，并把图像附上！顺便还能通过 ssh 查看远程图像，不错。
如果这些操作都属于同一个 API，还有第二种选择：暴露代码接口。Browser 保留 open / run / close，在持久化标签页上执行代码；Computer 在持久会话中暴露 desktop、wait 和 assert。只需一个稳定 schema，在一次调用内部组合操作。有限操作集用 schema，开放式操作集用代码接口。
两种形式服务于不同形态的 API。有限操作集可以继续使用 schema；开放式操作集则更适合代码或命令接口，在单次调用中组合多个操作。两者都不要求发现工具后再修改常驻列表。
契约规范：意图与版本
契约中有个小改动值得一提：每个工具都获得一个 i 意图参数。它在参数流式传入时到达，因此 renderCall 可以在调用完成前，展示模型认为自己正在做什么。日志也能获得可读摘要，不必让每个工具各自发明 reason / purpose。
大家应该给工具加版本号。
这样运行轨迹就好用得多：可以解析频繁变化的工具 I/O，评估成功率随时间的变化，而不必猜测每次调用究竟来自哪个版本的契约。
名称、版本、意图、输入、输出、诊断和用量，都是协议数据。一旦轨迹用于评估或修复，对其中任何一项靠猜，都是本可避免的技术债。
功能深厚的内置工具
小型工具列表能成立，前提是原语的广度来自统一语义，而不是把不相关功能塞进同一个 switch。omp 的内置工具就是很好的例子。
Read：把资源转成可用表示
omp 里最无聊的工具，实际上囊括了其他框架可能拆成 20 个工具的能力。
- 可以读取目录，不必另设
Ls。 - 读取
.ipynb文件，默认就有易读输出，不必再加ReadNotebook。 .pdf、.docx、.pptx、.xlsx、.epub？返回提取后的 Markdown。.cpuprofil, .sample.txt？没错，返回性能瓶颈摘要。.sqlite、.sqlite3、.db、.db3？可以列出表、检查 schema 和行，甚至查询。- 图像返回图像本身；不使用视觉时则返回元数据。预览 SVG，加上
:img。 - 无需解压就能寻址归档内容，不仅支持 ZIP 和 TAR，也支持 JAR、wheel 和 ASAR。
- 同样的投影适用于
http://...在线资源，按需读取范围；普通网页则像web_fetch一样转换成 Markdown。
这并不是为了显得聪明而搞多态。从模型角度看，它们全是同一种操作：
把这个资源转成最适合我理解和推理的表示形式。
对于代码，它还能返回结构摘要，用省略号替代大型声明体。模型不必仅为找到类 X，就把整个大文件拖进上下文。
需要关注原始字节时，:raw 可以绕过投影。:conflicts 则为每个未解决的合并冲突块返回一行，不必让模型在整个文件里翻找。
范围可以没有结束位置、按长度指定，也可以互不连续：
:50
:50-
:50-200
:50+150
:5-16,960-973
:raw:50-100
:50-100:raw
还有这些非 Web URL：
artifact://<id>
agent://<id>
history://<id>
issue://123
pr://123/diff/2
skill://react
rule://foo
memory://...
local://...
vault://...
security://...
omp://...
xd://browser
ssh://host/path
mcp://...
仓库信息、MCP 资源、子智能体会话记录、技能、记忆、本地临时空间、omp 文档，甚至通过 SSH 访问的远程机器，都能纳入同一个内部 URL 子系统。我们推荐这种设计。
Read 也会处理不那么显眼的恢复逻辑：依据唯一的工作区路径后缀，修正错误的绝对路径；在 Windows 上展开 ~；避免其他浪费轮次的路径错误。
它能不能只写成这样？
return await Bun.file(path).text();
能。然后扩展作者会自己实现读取器，或者模型寻找 shell 变通方案；与此同时，框架又会用 web_fetch 等不同名字暴露形态相近的能力。
这不是更少的复杂性，而是同样的复杂性被复制到 shell 命令、提示词、扩展和失败的工具调用里。没人负责，每个人都略有不同地实现其中 30%。
Read 复杂，是为了让读取不复杂。
复杂性由一个地方负责。操作保持稳定，资源特定的投影放在其后。
Bash：理解策略的命令语言
Bash 工具不该只是调用外部 Bash。听起来很疯。
omp 在进程内提供完整的 bash 解析器、解释器，以及全套 coreutils。这个选择很好，原因很简单：
- 保留模型的肌肉记忆。它可以继续用
grep；由于 omp 就是解释器，我们能拦截命令，将适合的参数路由到 ripgrep 引擎。谁也不必在AGENTS.md里消耗上下文，苦求模型改用rg。 - 几乎免费获得跨平台能力。不需要 WSL 或 Git Bash：omp 在 Windows 上就能在进程内执行大多数 Bash 调用。无需多言。
- 控制台状态跨调用保留，包括变量、退出码、
$!等。
当 Claude 发来这样的调用时，更有意思的优势就出现了：
INC="…/10.0.22621.0"; declare -A R
for d in um shared ucrt; do while IFS= read -r f; do b="${f##*/}"; R["${b,,}"]="$f"; done \
< <(find "$INC/$d" -maxdepth 1 -type f -name "*.[hH]"); done
n=0
while IFS= read -r ref; do case "$ref" in */*) continue;; esac; r="${R[${ref,,}]:-}"; \
[ -n "$r" ] || continue; rd="${r%/*}"; rn="${r##*/}"; \
if [ "$ref" != "$rn" ] && [ ! -e "$rd/$ref" ]; then ln -s "$rn" "$rd/$ref"; n=$((n+1)); fi; \
done < <(grep -rhoiE "#[[:space:]]*include[[:space:]]*<[^>]+>" "$INC/um" "$INC/shared" "$INC/ucrt" \
| sed -E "s/.*<([^>]+)>.*/\1/" | sort -u)
你能在 5 秒内说出它在做什么吗？如果你说能，那你在撒谎。
不管你对工具审批持什么看法，这都很糟：没人会认真读。Anthropic 最近的研究也指向同样结论，auto mode——让另一个 Claude 读取命令——明显胜过人类。
omp 自己解释命令时，可以等执行到 ln 的那一刻才询问；之前的操作全是只读。如果用户已允许写入该目录，连这次询问也能省掉。
这让运行框架不再像给“Bash”过安检，而是审批具体能力：“我可以用 Git 推送吗？”find、cat、ln 等常用命令在进程内运行，在需要时才查询访问模型，并继承用户已有的读写策略。
主机解释常用命令，意味着审批可以发生在真正重要的能力边界：git push、工作区外写入、网络请求，而不是一串难以阅读的 shell 字符串边界。第三章的运行时策略由此可以被强制执行，同时保留模型的 shell 肌肉记忆。
AutoQA：给智能体一条报缺陷的路径
我们创建分叉一个月后就加入了这个工具，比 Anthropic 在自家产品中加入类似功能还早。
你通常会提供某个渠道，让用户报告产品问题，对吧？这就是面向智能体的对应版本。它让你完全自动地收集：工具哪些地方好用，哪些地方令人困惑，哪些行为看起来有错。
报告质量确实不算出色。例如，Codex 没有正确重命名东西时，就爱把文件被外部修改的问题归咎于 Read 或 LSP 工具——不是我的错，去问 TypeScript 那帮人。不过，这类报告很容易过滤。过滤之后，就能获得大量有价值的信号，知道哪些工具失败、如何改进。
AutoQA 让工具设计与上线后的实际行为形成闭环。它有噪声，但剔除明显误归因之后，就能揭示：哪个操作让模型困惑，哪种投影隐藏了必要数据，哪些修复该由运行框架承担。
现在，工具有了受限运行时、稳定的发现接口和结构化状态。只是为了安全地显示这些状态，不该还要求每个工具作者——往往就是 Claude——都成为终端渲染和安全专家。
界面
- 267 秒 → 90 毫秒：单个会话的渲染时间。
- 13%：性能采样中，一个
.includes调用占用的 CPU 比例。 - 98.7 秒：花在
wrapAnsi重新换行上的时间。 - 0 张：该会话中的图像数量。
会话 DOM 和工具状态流，让每个客户端获得相同事实。但它们本身并不会自动产生安全、快速、一致的界面。渲染器仍可能把这些事实变成反复解析的字符串、扩展各自的样式约定，以及无法挽回的回滚缓冲区缺陷。
omp 给我们的教训：字符串开销会层层放大
这其实是我最早向 pi-mono 提交的几个 PR 之一所处理的问题。修改之前，如果对 Pi 执行整个任务的过程做性能分析，再查看 CPU 用量榜，榜单几乎全被——你猜对了——渲染器占据！
作为 TypeScript CLI，有些成本难以避免。光是字符串内部使用 UTF-16，就意味着每一帧都得经历相对昂贵的转码，除非你像个狂人一样，用 Uint8Array 到处传递文本。
但让成本层层放大的，是契约本身。想嵌入一个子组件？现在你得处理：
- 清理这个
string，并丢弃 ANSI 转义序列，或解析时跳过它们。 - 处理每一行的填充、截断和尺寸计算。
图像还可能以 base64 文本混在某一行里，这就更糟了。仅检查一行是否为图像行的 .includes，就占了整个会话 CPU 周期的 20%。（译注：本章开头的摘要写 13%，此处正文写 20%；原文未解释统计口径差异，译文保留两处数字。）账单可不小——而且这个会话根本没有图像！
这还只是 JavaScript 一侧的图表。在这种设计下，渲染管线成了反复折腾堆内存的机器：不停分配、拆解、丢弃字符串和字符串数组；拼接、切分、截断、填充，每一步都重复。真不妙。
同一契约还让扩展缺少共同设计语言。只要用过任何 Pi 扩展，你就知道，除了让 Clawd 逐个重做样式、再自己维护，没有办法让它们遵循共同规范。
没有契约规定该不该用圆角边框、能不能用 Nerd Font 图标、会不会用你喜欢的颜色表达操作语义。你会发现：
- 99% 的时候，它只做最低限度的工作，也就是截断或折行，所有工具都成了难以区分的灰色矩形。
- 1% 的时候，它过于努力地追求花哨，与你其余极简配置格格不入。
Pi 目录中的一个社区渲染器，展示了这种契约会怎样影响最终呈现给用户的内容：
if (cq.sources.length > 0) {
lines.push("");
for (const s of cq.sources) {
const domain = s.url.replace(/^https?:\/\//, "").replace(/\/.*$/, "");
const title = s.title.length > 50 ? s.title.slice(0, 47) + "..." : s.title;
lines.push(theme.fg("muted", ` \u25b8 ${title}`) + theme.fg("dim", ` \u00b7 ${domain}`));
}
}
lines.push("");
} else {
const textContent = result.content.find((c) => c.type === "text")?.text || "";
const preview = textContent.length > 500 ? textContent.slice(0, 500) + "..." : textContent;
for (const line of preview.split("\n")) lines.push(theme.fg("dim", line));
}
if (details?.fetchUrls?.length) {
if (details.curated) {
lines.push(theme.fg("muted", `Fetching ${details.fetchUrls.length} URLs in background`));
} else {
lines.push(theme.fg("muted", "Fetching:"));
for (const u of details.fetchUrls.slice(0, 5)) {
const display = u.length > 60 ? u.slice(0, 57) + "..." : u;
lines.push(theme.fg("dim", " " + display));
}
if (details.fetchUrls.length > 5) lines.push(theme.fg("dim", ` ... and ${details.fetchUrls.length - 5} more`));
}
}
这里的问题不少：
- 它按码点而不是可见宽度切文本，因此一旦把终端缩到 40 列以下，就会越出本行，把下面的内容撞乱。
- 它不知道终端宽度，所以即便空间充足，仍然给你省略号！
- 最重要的是，它无视 Pi 组件的第一条规则，没有清理外部输入。因此，抓取的内容只要送来合适的 ANSI 转义序列，就能把整个 UI 换成一张鸭子图片。当然不可能再干其他坏事啦！
把复杂性推给毫无防备的开发者——往往就是 Claude——自然会出现这种事。
每次被要求“帮忙做个工具 UI”时，LLM 不会记得运行框架的所有内部细节。说实话，有时我也不想记，而冒烟测试依然会判定它可用。
性能、安全和一致性问题，都来自同一个原因：一段已经渲染好的字符串，同时被当作布局树、样式树、内容、传输载体和终端程序。
omp² 的改变：单遍处理原语
最底层的调用者——除非你来提交 PR，否则不是你——把 RichText (Style, String) 推入传给它们的抽象管线 (&mut impl Out)。
这把 267 秒的渲染时间降到了 90 毫秒：
render(): string[] — N components × M transforms, every buffer re-parsed, re-measured, and re-allocated, every frame. After: RichText runs stream through the abstract pipeline in a single pass into the frame diff.临时对象、ANSI 解析、字素处理：在帧渲染器以下的每一层里，统统消失！显然就该如此。
既然可以流式写入填充，再写一行组件内容，如此重复，为什么还要先给整个组件补齐再往下传？既然可以在省略号之后直接停止消费流，或在变换过程中自行分行，为什么要让你先把 255 行 diff 全部彩色渲染出来，再 .slice(0, 3)，只为截成另一个字符串缓冲区数组？
底层原语统一负责测量和变换。高层永远不该解析 ANSI，去重新发现自己刚刚输出的结构。
类型化组件模型
接下来，string[] 会被真正的组件模型替代。高层调用者只需堆叠盒子，让 LSP 为自己指路：
<text> 内嵌套元素，会在编辑时触发 lint 错误，而不是到运行时才把画面弄坏。
<box>、<row>/<col>、<ico:new/> 图标、水平 magenta..cyan 渐变，以及由 $$ \frac{1}{2} $$ 实时渲染的 ½。我可能不喜欢写前端，但我可太喜欢好的抽象了。只需 (Element, Props, Children)，再搭配一个布局引擎，相比之下就已经美妙得多。
DOM 一章承诺，任何参与者都能渲染一个工具元素。下面就是这个承诺的具体样子。
这是 Read 组件的模样。还不错，对吧？
<box bc=muted>
<row kind=title gap=1>
<text>•</text>
<text bold>Read</text>
<a href={input.path}>{input.label}</a>
{#if status=error}<badge tone=error>exit {code}</badge>{/if}
</row>
{#if result.head}<pre lang={result.lang} wrap=word start={result.start}>{result.head}</pre>{/if}
{#if @expanded}
{#if result.blob}<pre lang={result.lang} numbers start={result.start} blob={result.blob}></pre>{/if}
{/if}
{#each diag as d}<callout tone={d.severity}>{d.msg}</callout>{/each}
{#if result.src}
<hr title="Output"/>
<row gap=1 fg=muted>
<text>⟨Resolved path:</text>
<text>{result.src}⟩</text>
</row>
{/if}
{@render usage}
</box>
工具作者描述结构和语义。TUI、Web 客户端、快照测试和远程检查器，决定如何在自己的界面上布局这些结构。
展示策略属于渲染器
组件模型免费带来两个有用特性：
<ico:new/>为每个插件提供方便的图标，同时尊重用户选择 ASCII、Unicode 还是 Nerd Font。边框也一样。- 语义颜色不再需要把主题对象穿过每个渲染器。Claude 可以请求
info，而不是挑一个字面颜色，再祈祷它适合用户主题。
border=round bc="info" 解析为主题中的语义颜色；fg="red..blue" 表示渐变。不需要到处传递主题对象。文本流的节奏也需要统一管理。Claude 和 Codex 输出分块的节奏很不一样：一个每次几个词，另一个每次几个字符。抹平这些差异，会改变框架给人的响应速度感受：持续运动看起来是在推进，突然喷出一段再停住则不是。嘿。
语义图标、边框、颜色、截断和流式节奏，现在都有唯一负责人。扩展请求 info、error 或 <ico:new/>，不必把主题对象穿过每个函数，也不用替所有用户选择 Nerd Font 字形。
验证是界面的一部分
在当下这套玩法中，投入产出比最高、又几乎不额外花钱的事情，就是让智能体为任何交互式 TUI／GUI 实现调试协议。如果“怎么验证”不明确、没定义，智能体就会另走旁路，做出一个貌似验证的东西——多数情况下，就是新建一个其实没检查什么的测试文件。
提前定义“验证”意味着什么，并提供方便的使用形式，就能大幅降低摩擦，让验证真正成为开发循环的一部分。
具体形式不重要，也随时可以调整：自定义工具、Python 包或 API 都行。但必须提供某种非破坏性、离屏、支持多实例的东西，防止智能体重新定义——通常是降低——成功标准。
换句话说，调试协议成为“这个 UI 是什么”的机器可读定义，而不只是测试辅助工具。
会话记录是一种协议
TUI 真正不可能做到的事，是 GitHub 上没有任何抱怨它坏了的 issue。人们总会对自己不了解的事抱有理想化期待。不幸的是，很多人不知道，他们想要的完美 TUI 体验根本不可能实现：无论组件位于哪里，都永远完全最新，并且能动态修改。
块
我们把规范会话记录定义为一个块列表。每个块生成文本行，并经历以下生命周期：
活跃（active）→ 定稿（finalized）→ 提交（committed）
块 i 存活时，展示当前快照 Wi，它是一个行数组。定稿时，冻结为不可变快照 Fi。
块有两种模式：
- 可变：每个新快照都可以整体替换前一个，例如旋转指示器和进度。快照是推测性的，永远不会进入历史；只有 Fi 会。
- 仅追加：快照只增不减，每个快照都是下一个的前缀，最后一个快照也是 Fi 的前缀，例如流式文本。
当块超过分配给它的视口空间时，这种区别很重要。可变快照不能提前进入历史，因为后续更新可能替换它，那就得把已经滚走的行拽回来。助手思考内容这样的仅追加块，只会扩展稳定前缀，所以该前缀可以立即开始提交。
终端
宽为 W、高为 H 的终端有两个缓冲区：
- V：视口，包含 H 行可见内容。
- S：原生回滚缓冲区，无界、仅追加。
技术上，我们可以清空并重写回滚缓冲区，但那会导致用户经常抱怨的行为；因此，不这样做现在成为不变量。
折行函数 wrapW 将逻辑行转换为物理行，取决于当前宽度。视口下方没有可寻址区域。写过底部会让终端滚动，并把顶部行不可逆地推入 S。
逻辑历史 L 以未折行的行保存，因此与宽度无关：按块顺序排列的已提交最终快照，每个恰好出现一次，再加上当前流式块已经放行的部分。令 c 为最后一个已提交块，j = c+1：
L = F1 · F2 ⋯ Fc · Wj[1..ej]
其中 ej 表示流式队首块已经写入历史的行数。除非块 j 正在以仅追加模式流式输出，否则 ej = 0。
因此：
- 已提交的最终快照，按块顺序连续出现，恰好一次。
- 可变的推测快照永远不进入 L。
- 仅追加的队首块可以在仍然流式输出时，逐行进入 L。
- 定稿本身不写入任何内容。
- 提交只追加 Fj 中尚未输出的行。
调整尺寸
调整尺寸不会改变任何逻辑状态：所有 Wi、Fi 和 c 都保持不变。只重新计算折行和视口空间分配。已经进入原生回滚缓冲区的行不能重写，因此必须为它们明确选择一种策略：
- 保留（Preserve）：保留终端模拟器已经折行的历史。
- 追加（Append）：追加重新渲染的历史，可能产生重复物理行。
- 重建（Rebuild）：开启新的物理显示纪元，并把历史回放进去。
这些规则分开了三种容易混淆的东西：视口内可变的展示、与宽度无关的逻辑历史，以及不可逆的原生终端行。把它们命名之后，调整尺寸和流式输出就成为策略选择，而不是口口相传的玄学。
为不可能的部分写规范
为什么要让你经历这一大段“数学”？因为这个算法极其复杂，很难验证它是否合理。上一次迭代，我们不得不写模糊测试器，才达到稳定状态。这一次，我想避免重走老路。
于是，我们用 TLA+ 对上述行为建模，要求迭代修改块的提交与定稿处理，直到所有明确规定的不变量都满足。
现在，如果真想改点东西，比如放手提交部分内容，或禁止块截断，我们有一份可以更新的参考规范，也有一个极其简单的办法知道修改能否成立；失败时还会给出反例。
论文与完整的 ElasticSlots.tla 源码位于附录 B。
这解锁了什么
例行炫耀一下，然后继续！现在如果有人抱怨 TUI 坏了，我就能给他一个形式化证明，解释为什么它修不了。太好了。
TUI、Web 客户端和远程检查器可以布局不同，但事实不能不同。工具作者描述语义状态，组件系统负责展示，会话记录协议负责恰好一次的历史。
又是同一个设计动作：把难以维持的不变量下沉到能够强制执行它的层。实现所用的技术栈应该强化这些不变量，而不是邀请每位贡献者——以及每个编程智能体——发明局部风格。
技术栈
前几章讲的是架构。语言选择决定了，当下一个“好心”的局部特例出现时，代码库会在它与架构之间设置多大阻力。当大量实现由智能体生成，而它们学到的是各生态的默认习惯和毛病时，这一点尤其重要。
语言选择就是架构
眼下，除非不得不与前端代码打交道，否则 TypeScript 是个糟糕的选择。
如今启动项目，最有影响力的决定之一，就是选对工具。三年前，要是看到文章这样开头，我大概已经开始吐槽了。但……如果你不信，试着给 Claude 完全相同的提示词，描述一个想做的小组件。
再把 macOS（Swift）换成 Linux（Qt/JS）。前者会给你一个玻璃质感的小组件，看起来天生属于这个操作系统；后者会给你一个矩形，UI 元素互相重叠，交互选择令人怀疑，让你觉得自己刚看完定义 UI 所需的 XML schema，正在第一次尝试编译。
当然，提示方式有影响，你也确实可以写得更详细。但过一阵你会发现，无论怎么做，一边总能几乎不费力地胜过另一边。macOS 历来有件事做得好：强迫开发者遵循一致的设计风格。这对 LLM 同样有效。
重点不是 Swift 自带品味而 JavaScript 没有，而是默认值、标准库、规范项目结构、编译器反馈和生态约定，会成为生成代码的先验。一门允许二十种局部风格都同样正常的语言，等于要求模型还没碰到产品问题，就先做二十个选择。
TypeScript 会变成你自己的语言
遗憾的是，我曾经喜欢 TypeScript 的一点，恰恰是它最后总会变成你自己的语言：
- 用
camelCase还是snake_case？或者干脆把库叫$？ - 写跨越 200 行的泛型，还是一个泛型也不用？
- 用
Buffer还是Uint8Array？ - 用 Zod 还是 Typebox？
- 用
Array<T>还是T[]？ - 用 ESM 还是 CJS？扩展名呢，
.ejs, .cjs, .mjs, .js? - 用 TypeScript 还是 JSDoc？
- 用类，还是坚持对象？甚至
new function()？ - 要不要默认导出？
- 用星号重新导出，还是逐项命名？
- 用
private foo还是#foo？ - 用
module/index.ts还是module.ts？ - 用
const x = () => ..还是function x() {？ - 用
function x(args)还是function x(...args)？ - 如果选后者，用
...args: any[]还是...args: unknown[]？ - 用
const X = 1、enum E { X = 1 }，还是const enum E { X = 1 }？
你看，我在人生中最强的只写不读语言——C++——上花了十年，所以确实能从中找到乐趣。但当必须在 Zod 与 Typebox 之间选择时，你那位“初级同事”只会自己写一个所谓的 isRecord。能直接联合类型，为什么用泛型？能加个 typeof 分情况，为什么在脑子里确保每条分支对两种类型都有效？为什么用类，不就是对象和原型吗？
也许是世上糟糕的 JS 代码实在太多，也许是模型训练时吞下了一堆压缩代码，但我已经厌倦了。考虑到同一个“初级同事”还能发现 Linux 零日漏洞，换作是我，就不会再指望对的模型或对的代码质量工具，也不会继续费劲绕圈子。
也许 EffectJS 会改变这一点。我认为最终 Go 会在这里胜出，尤其是 WASM 的 GC 提案定稿之后，原因类似 Swift 在设计上占优的原因，再加上编译速度和交叉编译的便利。不过，有些场景需要更底层的系统语言，所以我们在这里选择了 Rust。
智能体仍经常需要引导，因为它们总走通向目标的最短路径：不处理复杂借用，改为分配副本；不用 thiserror，改为传递字符串错误。但 std 加上 serde 生态，已经提供了它们工作所需的大部分东西，编译器也提供了相当程度的安全保障，于是就这么定了。
扩展使用 Python
下一项决定，是要不要为了可扩展性把 TS 请回来。我们说不，主要因为：
- 智能体能写出不错的 Python，顺理成章也就能写出不错的扩展。
- 想用很小的体积做出符合规范的 JS 运行时，基本不可能，感谢 Locale；而没有生态，还不如用 Lua。
- 扩展占运行时间甚至不到 1%，没什么必要上 JIT。
- 内嵌完整 Python 运行时，就能保证
eval开箱即用，而不是要求用户安装 py3，却始终无法在交付的工作流里可靠依赖它。 - Python 代码原生就能检查自己的 AST。这正是运行时一章中
@remote设计能够成立的原因。
运行时一章介绍了 @remote 边界。Python 的自省和属性模型让这个边界好用：SDK 能检查函数、打包相关源码，并在沙盒运行时执行，不必让每位扩展作者手写 RPC。
自带运行时，也让 Eval 成为可靠的内置能力，而不是只有用户碰巧安装了兼容 Python 才能工作的功能。
结语
开篇的问题是：“可是，为什么？”直接回答就是：上述每一章，都是一类已有数十年经验积累的软件问题——复制、沙盒隔离、配置、调度、协议兼容、实时渲染，以及语言和运行时设计。
omp² 仍在依照这份文档构建，各部分进度从已经上线到仍在思考不等。我们真诚感谢每一位愿意尝试它、并分享各种精彩用法的人：从让 omp 运营软件工厂，到让它直接在所在手机上为自己构建相机应用。
你们塑造了 omp，我们相信未来也会同样有趣！
附录 A：官方示例中的状态故障
状态一章按类别概述了这些故障。本附录保留原始证据：源码链接、最小代码片段，以及复现视频。
这不是理论上的指控。我们检查了 78 个官方扩展示例：60 个无状态；17 个有状态的示例中，只有两个正确。
1. /fork 还没来得及使用，检查点就已被清空：git-checkpoint.ts
源码：缺少持久的检查点所有权；/fork 在空闲时调用，而 agent_settled 已经清空唯一保存 stash 引用的映射。
const checkpoints = new Map<string, string>();
// …
pi.on("agent_settled", async () => {
checkpoints.clear();
});
2. 会话树导航不恢复状态：plan-mode/index.ts
源码：缺少 session_tree 和 getBranch()；回退后计划模式及其工具限制仍生效，恢复会话却可能让废弃分支的快照复活。
const entries = ctx.sessionManager.getEntries();
const planModeEntry = entries
.filter((e) => e.type === "custom" && e.customType === "plan-mode")
.pop();
3. 计数器不会统计历史：status-line.ts
源码：缺少按分支推导的逻辑；从第 3 轮回退到第 1 轮，下一轮却显示 4，而恢复会话又从零开始。
let turnCount = 0;
// …
pi.on("turn_start", async (_event, ctx) => {
turnCount++;
4. 动态添加的工具在回退后保留，恢复会话后却消失：dynamic-tools.ts
源码：/add-echo-tool echo_branch 只写入运行中的扩展注册表；/tree 不会重启注册表，所以回退保留工具，但 --continue 会新建注册表，工具便消失了。
const registeredToolNames = new Set<string>();
// …
registeredToolNames.add(name);
pi.registerTool({
5. 废弃分支的存档回来了：snake.ts
源码：恢复时扫描整个会话文件；在分支 A 保存，回退到保存之前，再打开 /snake，已废弃的存档就会回来。
const entries = ctx.sessionManager.getEntries();
for (let i = entries.length - 1; i >= 0; i--) {
const entry = entries[i];
if (entry.type === "custom" && entry.customType === SNAKE_SAVE_TYPE) {
6. “最后一条消息”指的是文件里的最后一条：bookmark.ts
源码：缺少 getBranch()；回退后，/bookmark 可能给废弃分支上用户看不到的助手消息加标签。
const entries = ctx.sessionManager.getEntries();
for (let i = entries.length - 1; i >= 0; i--) {
const entry = entries[i];
if (entry.type === "message" && entry.message.role === "assistant") {
7. 回退到发现之前，Calculator 仍然活跃：kimi-deferred-tools.ts
源码：tool_search 激活 Calculator，却没有 session_tree 处理器重新推导活跃列表；导航回发现工具之前，Calculator 仍然活跃。
const active = pi.getActiveTools();
const added = active.includes("Calculator") ? [] : ["Calculator"];
if (added.length > 0) pi.setActiveTools([...active, ...added]);
// Missing: session_tree → derive active tools from selected branch.
8. 切换会话会提交工作树：auto-commit-on-exit.ts
源码：缺少仅用于进程退出的边界；/new、/resume 和 /fork 都会触发 session_shutdown，进而暂存并提交有未提交变更的工作树。
pi.on("session_shutdown", async (_event, ctx) => {
// …
await pi.exec("git", ["add", "-A"]);
await pi.exec("git", ["commit", "-m", commitMessage]);
});
9. 实时状态与恢复状态不一致：tic-tac-toe.ts
恢复逻辑；用户落子：重建只接受工具结果，用户落子却使用 custom 条目；如果在 X 落子后、O 落子前崩溃，X 就会消失。
if (entry.type !== "message") continue;
if (msg.role !== "toolResult") continue;
// User moves take a different path:
pi.appendEntry(SAVE_TYPE, getBoardDetails());
附录 B：弹性推测槽位
界面一章把协议及结论放在主线内容中。本附录提供论文，以及用于检查会话记录不变量的完整 TLA+ 模型。
ElasticSlots.tla — 完整规范
---- MODULE ElasticSlots ----
\* =========================================================================
\* Elastic Speculative Slots: a formally verified rendering protocol for
\* streaming concurrent output blocks through a bounded terminal viewport
\* into append-only scrollback.
\*
\* Three decoupled layers, related by invariants (see ELASTIC_SLOTS2.tex):
\* 1. semantic block state (phase/mode/want/final/emitted per block)
\* 2. logical history ledger (`history`: width-independent, exactly-once)
\* 3. physical native rows (`native`: width-rendered, source-tagged)
\* =========================================================================
EXTENDS Naturals, Sequences, FiniteSets, TLC
\* Naturals: arithmetic; Sequences: <<>>/Len/SubSeq/\o; FiniteSets:
\* Cardinality/IsFiniteSet; TLC: model-checking utilities.
CONSTANTS N, H, MaxResizes, MaxLive, RowValues, SnapshotValues,
NoFinal, Placeholder, Blank, OverflowMarker
\* N : number of block identities (blocks are 1..N, in commit order)
\* H : maximum viewport (live transcript) height, in rows
\* MaxResizes : bound on resize events (keeps the state space finite)
\* MaxLive : uncommitted-block count that constitutes "pressure"
\* RowValues : finite row alphabet (what a semantic line of output "is")
\* SnapshotValues: finite universe of block contents (sequences of rows)
\* NoFinal : sentinel "this block has no final snapshot yet"
\* Placeholder : synthetic viewport row shown for an empty slot
\* Blank : synthetic viewport row for unused screen space
\* OverflowMarker: synthetic viewport row summarizing hidden older blocks
ASSUME
∧ N ∈ ℕ \ {0} \* at least one block
∧ H ∈ ℕ \ {0} \* viewport can be nonempty
∧ MaxResizes ∈ ℕ \* zero resizes is allowed
∧ MaxLive ∈ ℕ \ {0} \* pressure threshold >= 1
∧ IsFiniteSet(RowValues) \* finite row alphabet
∧ RowValues ≠ {} \* ... and nonempty
∧ IsFiniteSet(SnapshotValues) \* finite snapshot universe
∧ SnapshotValues ⊆ Seq(RowValues) \* snapshots are row sequences
∧ ⟨⟩ ∈ SnapshotValues \* the empty snapshot exists
∧ (∃ snapshot ∈ SnapshotValues : Len(snapshot) = 1) \* a length-1 snapshot exists
∧ (∃ snapshot ∈ SnapshotValues : Len(snapshot) > 1) \* a longer one exists too
∧ NoFinal ∉ SnapshotValues \* sentinel distinct from real data
∧ Placeholder ∉ RowValues \* synthetic rows are not
∧ Blank ∉ RowValues \* ... confusable with
∧ OverflowMarker ∉ RowValues \* ... semantic rows,
∧ Placeholder ≠ Blank \* and are pairwise
∧ Placeholder ≠ OverflowMarker \* distinct from
∧ Blank ≠ OverflowMarker \* each other.
Blocks ≜ 1‥N \* the block identities
ModelRows ≜ {"row-a", "row-b"} \* tiny concrete row alphabet for TLC
ModelSnapshots ≜ \* a richer snapshot universe (unused by the shipped cfg)
{⟨⟩, \* empty block
⟨"row-a"⟩, \* one-liner
⟨"row-b"⟩, \* one-liner, other row
⟨"row-a", "row-b"⟩, \* two distinct rows
⟨"row-b", "row-a"⟩, \* order matters
⟨"row-a", "row-b", "row-a"⟩} \* length three, with repeat
SmallModelSnapshots ≜ {⟨⟩, ⟨"row-a"⟩, ⟨"row-a", "row-b"⟩} \* the cfg's universe: lengths 0, 1, 2
WidthValues ≜ {"Wide", "Narrow"} \* two-point abstraction of terminal width
ResizeModes ≜ {"Preserve", "Append", "Rebuild"} \* policy chosen at a width-changing resize
ReplayModes ≜ {"None", "Append", "Rebuild"} \* pending replay (None = no replay in flight)
BlockModes ≜ {"Undeclared", "Mutable", "AppendOnly"} \* presentation contract, fixed at Create
Phases ≜ {"Absent", "Queued", "Active", "Finalized", "Committed"} \* block lifecycle, monotone left-to-right
StopReasons ≜ {"Running", "Graceful", "Detach", "WriteFailure"} \* why the host stopped (Running = it hasn't)
NativeSources ≜ {"Append", "Retire", "Replay", "Resize", "FailedWrite", "Exit"} \* provenance tag on every native row
CellRows ≜ RowValues ∪ {Placeholder, Blank, OverflowMarker} \* what a viewport cell may display
Cells ≜ [owner : 0‥N, row : CellRows] \* a viewport cell: owning block (0 = chrome) + row
TaggedRows ≜ [owner : Blocks, row : RowValues] \* a ledger row: semantic, width-independent
NativeRows ≜ [source : NativeSources, owner : 0‥N, row : CellRows, width : WidthValues]
\* a native row: provenance source, owner, rendered row, and the width it was rendered at
SnapshotLengths ≜ {Len(snapshot) : snapshot ∈ SnapshotValues} \* set of occurring snapshot lengths
MaxSnapshotLength ≜ \* L_max: the longest snapshot length
CHOOSE maximum ∈ SnapshotLengths : \* (CHOOSE is fine here: the maximum
∀ length ∈ SnapshotLengths : length ≤ maximum \* of a finite set is unique)
MaxFailureRows ≜ 2 * N * MaxSnapshotLength \* K_max: upper bound on one physical write batch
\* (factor 2 = worst-case Narrow doubling)
BlankCell ≜ [owner ↦ 0, row ↦ Blank] \* the unused-screen-space cell
OverflowCell ≜ [owner ↦ 0, row ↦ OverflowMarker] \* the "N older blocks hidden" summary cell
\* -------------------------------------------------------------------------
\* State variables (one tuple entry per column of Table 1 in the paper).
\* -------------------------------------------------------------------------
VARIABLES c, phase, mode, want, final, emitted, alloc, target,
history, native, width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason
\* c : commit frontier -- blocks 1..c are committed (retired)
\* phase : lifecycle phase per block
\* mode : Mutable / AppendOnly contract per block
\* want : current speculative snapshot per block
\* final : frozen final snapshot per block (NoFinal until finalized)
\* emitted : rows of the head block already streamed into history
\* alloc : painted slot height per block (rows on screen now)
\* target : requested slot height per block (animation target)
\* history : the logical ledger (layer 2)
\* native : the physical scrollback of the current epoch (layer 3)
\* width, height : current terminal geometry
\* resizes : how many resizes happened (bounded by MaxResizes)
\* epoch : display epoch; Rebuild resets native and bumps this
\* replayMode : pending replay policy (None / Append / Rebuild)
\* replayCursor : first committed block to replay (invariantly 1 while replaying)
\* replayEnd : last committed block to replay (= c at replay start)
\* replayPartial : how many stable head rows to replay
\* replayPrepared : replay frame computed and cut fixed (gates the scheduler)
\* replayCut : rows of the replay frame that must scroll into native
\* flush : explicit "retire everything" request (never reset)
\* shutdown : graceful shutdown initiated
\* running : host still alive; every action requires it
\* stopReason : why we stopped (Running while alive)
vars ≜ ⟨c, phase, mode, want, final, emitted, alloc, target,
history, native, width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩
\* the full variable tuple, used for stuttering ([Next]_vars) and UNCHANGED
Maximum(left, right) ≜ IF left ≥ right THEN left ELSE right \* max of two naturals
\* -------------------------------------------------------------------------
\* Width rendering: the two-point abstraction of soft-wrap reflow.
\* -------------------------------------------------------------------------
RECURSIVE DoubleRows(_)
DoubleRows(snapshot) ≜ \* Narrow rendering:
IF Len(snapshot) = 0 THEN ⟨⟩ \* empty stays empty;
ELSE ⟨Head(snapshot), Head(snapshot)⟩ ∘ DoubleRows(Tail(snapshot))
\* every semantic row occupies TWO physical rows (models a wrapped line)
Render(snapshot, wx) ≜ IF wx = "Wide" THEN snapshot ELSE DoubleRows(snapshot)
\* rho_omega: Wide = identity, Narrow = row doubling; prefix-monotone by construction
Tag(i, snapshot) ≜ \* tg_i: stamp each row with its owner
[j ∈ 1‥Len(snapshot) ↦ [owner ↦ i, row ↦ snapshot[j]]]
SnapshotSlice(snapshot, lo, hi) ≜ \* s[lo..hi], empty when lo > hi
IF lo > hi THEN ⟨⟩ ELSE SubSeq(snapshot, lo, hi)
TagSlice(i, snapshot, lo, hi) ≜ Tag(i, SnapshotSlice(snapshot, lo, hi)) \* owner-tagged slice
NativeTag(source, i, snapshot, wx) ≜ \* ntg: render at width wx, then tag
[j ∈ 1‥Len(Render(snapshot, wx)) ↦ \* one native row per RENDERED row
[source ↦ source, owner ↦ i, \* provenance + owner
row ↦ Render(snapshot, wx)[j], width ↦ wx]] \* rendered row + width it used
NativeTagSlice(source, i, snapshot, lo, hi, wx) ≜ \* native-tag a semantic slice
NativeTag(source, i, SnapshotSlice(snapshot, lo, hi), wx)
NativeCells(source, cells, wx) ≜ \* lift screen cells to native rows
[j ∈ 1‥Len(cells) ↦ \* (used when the emulator itself
[source ↦ source, owner ↦ cells[j].owner, \* pushes viewport rows into
row ↦ cells[j].row, width ↦ wx]] \* scrollback, e.g. on resize/exit)
PrefixOf(sequence, count) ≜ [j ∈ 1‥count ↦ sequence[j]] \* first `count` elements
\* -------------------------------------------------------------------------
\* The logical ledger as a FUNCTION of state (invariant ECH says
\* `history` always equals CommittedRows(c, final) \o PartialHeadRows).
\* -------------------------------------------------------------------------
RECURSIVE CommittedRows(_, _)
CommittedRows(k, finals) ≜ \* C(k): finals of blocks 1..k,
IF k = 0 THEN ⟨⟩ \* tagged, concatenated in
ELSE CommittedRows(k - 1, finals) ∘ Tag(k, finals[k]) \* block (= commit) order
RECURSIVE TaggedRange(_, _, _)
TaggedRange(lo, hi, finals) ≜ \* tagged finals of blocks lo..hi
IF lo > hi THEN ⟨⟩ \* (empty range allowed)
ELSE Tag(lo, finals[lo]) ∘ TaggedRange(lo + 1, hi, finals)
RECURSIVE NativeRange(_, _, _, _, _)
NativeRange(source, lo, hi, finals, wx) ≜ \* same, but width-rendered and
IF lo > hi THEN ⟨⟩ \* source-tagged for `native`
ELSE NativeTag(source, lo, finals[lo], wx)
∘ NativeRange(source, lo + 1, hi, finals, wx)
RetirementRows(lo, hi, finals, firstEmitted) ≜ \* logical retirement batch:
IF lo > hi THEN ⟨⟩ \* head block lo contributes only
ELSE TagSlice(lo, finals[lo], firstEmitted + 1, Len(finals[lo])) \* its UNstreamed suffix,
∘ TaggedRange(lo + 1, hi, finals) \* later blocks contribute in full
NativeRetirementRows(source, lo, hi, finals, firstEmitted, wx) ≜
IF lo > hi THEN ⟨⟩ \* physical twin of RetirementRows:
ELSE NativeTagSlice( \* the same rows,
source, \* provenance-tagged
lo, \* (Retire on success,
finals[lo], \* FailedWrite on failure),
firstEmitted + 1, \* starting after the already-
Len(finals[lo]), \* streamed head prefix,
wx \* rendered at the current width
)
∘ NativeRange(source, lo + 1, hi, finals, wx) \* then full later finals
FinalizedRange(lo, hi) ≜ \* "blocks lo..hi are all Finalized"
∀ i ∈ lo‥hi : phase[i] = "Finalized" \* (a retirement batch precondition)
Unemitted(snapshot, i, emission) ≜ \* U_i(s): the part of s not yet
IF mode[i] = "AppendOnly" \* streamed into history --
THEN SnapshotSlice(snapshot, emission[i] + 1, Len(snapshot)) \* suffix for append-only,
ELSE snapshot \* everything for mutable blocks
\* -------------------------------------------------------------------------
\* Live-viewport geometry: who is presented, who is visible, how much
\* space is reserved. All operators take the ambient tuple explicitly so
\* that action guards can evaluate them at SUCCESSOR values.
\* -------------------------------------------------------------------------
Presented(ph, finals, emission, i, wx) ≜ \* block i occupies viewport iff
∨ ph[i] = "Active" \* it is actively producing, or
∨ ∧ ph[i] = "Finalized" \* it is finalized AND still has
∧ Len(Render(Unemitted(finals[i], i, emission), wx)) > 0 \* unstreamed content to show
PresentedSet(ph, finals, emission, wx) ≜ \* the set of presented blocks
{i ∈ Blocks : Presented(ph, finals, emission, i, wx)}
PresentedCount(ph, finals, emission, wx) ≜ \* pi: how many are presented
Cardinality(PresentedSet(ph, finals, emission, wx))
Overflow(ph, finals, emission, wx, hx) ≜ \* ovf: more presented blocks
PresentedCount(ph, finals, emission, wx) > hx \* than viewport rows
SummaryRows(ph, finals, emission, wx, hx) ≜ \* sigma: one summary row is
IF hx > 0 ∧ Overflow(ph, finals, emission, wx, hx) THEN 1 ELSE 0 \* shown iff overflowing (and h>0)
NewerPresented(ph, finals, emission, wx, i) ≜ \* how many presented blocks are
Cardinality({ \* NEWER (higher index) than i --
j ∈ Blocks : \* used to privilege recency
j > i ∧ Presented(ph, finals, emission, j, wx)
})
VisiblePresented(ph, finals, emission, wx, hx, i) ≜ \* vis(i): presented AND, under
∧ Presented(ph, finals, emission, i, wx) \* overflow, among the hx-1
∧ IF Overflow(ph, finals, emission, wx, hx) \* newest presented blocks
THEN ∧ hx > 0 \* (one row is sacrificed to
∧ NewerPresented(ph, finals, emission, wx, i) < hx - 1 \* the summary marker)
ELSE TRUE \* no overflow: presented = visible
RECURSIVE AllocationTotal(_, _)
AllocationTotal(al, i) ≜ \* sum of painted heights,
IF i > N THEN 0 ELSE al[i] + AllocationTotal(al, i + 1) \* blocks i..N
RECURSIVE ReservationTotal(_, _, _)
ReservationTotal(al, requested, i) ≜ \* Res: each block is charged
IF i > N THEN 0 \* max(painted, requested) --
ELSE Maximum(al[i], requested[i]) + ReservationTotal(al, requested, i + 1)
\* growth pays up front, shrink keeps its old charge until painted
AllocationStateOK(al, requested, ph, finals, emission, wx, hx) ≜ \* A_OK: allocation admissibility
∧ al ∈ [Blocks → 0‥H] \* painted heights in range
∧ requested ∈ [Blocks → 0‥H] \* requested heights in range
∧ ∀ i ∈ Blocks :
IF VisiblePresented(ph, finals, emission, wx, hx, i)
THEN IF ph[i] = "Active"
THEN ∧ al[i] ∈ 1‥H \* visible active: painted >= 1,
∧ requested[i] ∈ 1‥H \* target >= 1 (may differ: animating)
ELSE ∧ al[i] ∈ 1‥H \* visible finalized: painted >= 1,
∧ requested[i] = al[i] \* and frozen (no more animation)
ELSE ∧ al[i] = 0 \* invisible blocks hold
∧ requested[i] = 0 \* no space at all
∧ ReservationTotal(al, requested, 1) \* reservation invariant:
+ SummaryRows(ph, finals, emission, wx, hx) ≤ hx \* reservations + summary fit in h
CanonicalAllocation(ph, finals, emission, wx, hx) ≜ \* kappa: the safe default --
[i ∈ Blocks ↦ \* one row per visible block,
IF VisiblePresented(ph, finals, emission, wx, hx, i) THEN 1 ELSE 0] \* zero otherwise
SnapshotHeight(ph, wants, finals, i, wx) ≜ \* dm(i): row demand of block i
CASE ph[i] = "Active" →
Maximum(1, Len(Render(Unemitted(wants[i], i, emitted), wx))) \* live: >= 1 row
□ ph[i] = "Queued" →
Maximum(1, Len(Render(Unemitted(wants[i], i, emitted), wx))) \* queued demands space too
□ ph[i] = "Finalized" →
Len(Render(Unemitted(finals[i], i, emitted), wx)) \* finalized: exactly its unstreamed rows
□ OTHER → 0 \* absent/committed demand nothing
RECURSIVE FullRows(_, _, _, _, _)
FullRows(ph, wants, finals, wx, i) ≜ \* D: total row demand of
IF i > N THEN 0 \* blocks i..N
ELSE SnapshotHeight(ph, wants, finals, i, wx)
+ FullRows(ph, wants, finals, wx, i + 1)
CreatedCount ≜ Cardinality({i ∈ Blocks : phase[i] ≠ "Absent"}) \* gamma: how many blocks exist
PartialHeadExists ≜ \* PH: the head block (c+1) has
∧ c < CreatedCount \* been created,
∧ mode[c + 1] = "AppendOnly" \* is append-only,
∧ phase[c + 1] ∈ {"Active", "Finalized"} \* is live,
∧ emitted[c + 1] > 0 \* and has streamed some rows
PartialHeadRows ≜ \* A(c): the head's streamed
IF PartialHeadExists \* prefix as tagged ledger rows
THEN TagSlice(c + 1, want[c + 1], 1, emitted[c + 1]) \* (prefix of `want`, stable by
ELSE ⟨⟩ \* the append-only contract)
RowPressure ≜ FullRows(phase, want, final, width, 1) > height \* demand exceeds viewport
Pressure ≜ \* pressure = row pressure OR
∨ RowPressure \* too many uncommitted
∨ CreatedCount - c ≥ MaxLive \* blocks piling up
RetirementRequested ≜ flush ∨ Pressure \* Req: when retirement may fire
Replaying ≜ replayMode ≠ "None" \* a replay is in flight
PreviewSource(i) ≜ \* what a slot displays:
IF phase[i] = "Active" \* live blocks show their
THEN Unemitted(want[i], i, emitted) \* unstreamed speculation,
ELSE Unemitted(final[i], i, emitted) \* others their unstreamed final
PreviewCell(i, snapshot) ≜ \* the representative cell of a slot:
LET rendered ≜ Render(snapshot, width) IN \* render at current width;
[owner ↦ i,
row ↦ IF Len(rendered) = 0 \* empty content shows the
THEN Placeholder \* placeholder row, otherwise
ELSE rendered[Len(rendered)]] \* the LAST rendered row (tail view)
Repeat(value, count) ≜ [j ∈ 1‥count ↦ value] \* value^count as a sequence
Slot(i, snapshot, allocation) ≜ Repeat(PreviewCell(i, snapshot), allocation)
\* a slot = its preview cell repeated alloc[i] times (abstracting the real tail window)
RECURSIVE PresentedCells(_)
PresentedCells(i) ≜ \* all slots, ascending block
IF i > N THEN ⟨⟩ \* order (newest at the bottom,
ELSE (IF alloc[i] = 0 THEN ⟨⟩ ELSE Slot(i, PreviewSource(i), alloc[i])) \* next to the cursor);
∘ PresentedCells(i + 1) \* zero-alloc blocks contribute nothing
Screen ≜ \* Q: the whole viewport, top to bottom:
Repeat(
BlankCell, \* blank filler first,
height - AllocationTotal(alloc, 1) - SummaryRows(phase, final, emitted, width, height)
) \* (exactly the unclaimed rows)
∘ (IF SummaryRows(phase, final, emitted, width, height) = 1
THEN ⟨OverflowCell⟩ \* then the overflow summary if any,
ELSE ⟨⟩)
∘ PresentedCells(1) \* then the block slots
\* -------------------------------------------------------------------------
\* Replay geometry: what a width-changing resize must re-render.
\* -------------------------------------------------------------------------
ReplayRows ≜ \* R: the full replay frame --
IF ¬Replaying
THEN ⟨⟩ \* nothing when no replay pending
ELSE NativeRange("Replay", replayCursor, replayEnd, final, width) \* committed finals 1..c
∘ (IF replayPartial = 0 \* re-rendered at the NEW width,
THEN ⟨⟩ \* plus the head's already-
ELSE NativeTagSlice( \* streamed stable prefix
"Replay", \* (if it had streamed rows
replayEnd + 1, \* at resize time) --
want[replayEnd + 1], \* prefix of want, immutable
1, \* under the append-only
replayPartial, \* contract, so stable while
width \* the replay is in flight
))
ReplayRoom ≜ \* how many blank rows the
Cardinality({j ∈ 1‥height : Screen[j] = BlankCell}) \* viewport can absorb scroll-free
RequiredReplayCut ≜ \* cut*: replay rows that do NOT
IF Len(ReplayRows) > ReplayRoom THEN Len(ReplayRows) - ReplayRoom ELSE 0
\* fit in the blank region and must scroll into native scrollback
PreparedReplayTail ≜ \* the part painted bottom-first
IF replayPrepared \* into blank rows (no scroll);
THEN SnapshotSlice(ReplayRows, replayCut + 1, Len(ReplayRows)) \* only meaningful once
ELSE ⟨⟩ \* the frame is prepared
Prefix(left, right) ≜ \* left is a prefix of right
∧ Len(left) ≤ Len(right) \* (the partial order behind the
∧ ∀ j ∈ 1‥Len(left) : left[j] = right[j] \* append-only contract)
NoEarlierQueued(i) ≜ ∀ j ∈ 1‥(i - 1) : phase[j] ≠ "Queued" \* FIFO admission guard
\* =========================================================================
\* Initial state: nothing created, full-height wide viewport, empty
\* histories, no replay, host running.
\* =========================================================================
Init ≜
∧ c = 0 \* nothing committed
∧ phase = [i ∈ Blocks ↦ "Absent"] \* no block exists
∧ mode = [i ∈ Blocks ↦ "Undeclared"] \* no contract chosen
∧ want = [i ∈ Blocks ↦ ⟨⟩] \* empty speculation
∧ final = [i ∈ Blocks ↦ NoFinal] \* nothing finalized
∧ emitted = [i ∈ Blocks ↦ 0] \* nothing streamed
∧ alloc = [i ∈ Blocks ↦ 0] \* no slot painted
∧ target = [i ∈ Blocks ↦ 0] \* no slot requested
∧ history = ⟨⟩ \* empty ledger (= CommittedRows(0,...))
∧ native = ⟨⟩ \* empty scrollback
∧ width = "Wide" \* initial geometry:
∧ height = H \* wide, full height
∧ resizes = 0 \* no resizes yet
∧ epoch = 0 \* first display epoch
∧ replayMode = "None" \* no replay pending
∧ replayCursor = 0 \* replay window empty
∧ replayEnd = 0
∧ replayPartial = 0
∧ replayPrepared = FALSE \* no frame prepared
∧ replayCut = 0
∧ flush = FALSE \* no flush requested
∧ shutdown = FALSE \* not shutting down
∧ running = TRUE \* host alive
∧ stopReason = "Running" \* ... and not stopped
\* =========================================================================
\* Actions. Every guard conjoins `running`; most also require ~shutdown.
\* =========================================================================
Create(declaration) ≜ \* a new block is declared
∧ running \* host alive
∧ ¬shutdown \* no new work during shutdown
∧ CreatedCount < N \* an identity is still free
∧ phase[CreatedCount + 1] = "Absent" \* blocks are created contiguously
∧ declaration ∈ {"Mutable", "AppendOnly"} \* contract chosen now, forever
∧ phase' = [phase EXCEPT ![CreatedCount + 1] = "Queued"] \* enters the queue
∧ mode' = [mode EXCEPT ![CreatedCount + 1] = declaration] \* contract recorded
∧ UNCHANGED ⟨c, want, final, emitted, alloc, target, history, native,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* pure bookkeeping: no paint, no history
Admit(i) ≜ \* a queued block gets a live slot
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ phase[i] = "Queued" \* must be waiting
∧ NoEarlierQueued(i) \* FIFO: no older block still queued
∧ LET newPhase ≜ [phase EXCEPT ![i] = "Active"] \* candidate successor phase,
newAlloc ≜ [alloc EXCEPT ![i] = 1] \* with a fresh 1-row slot
newTarget ≜ [target EXCEPT ![i] = 1] \* painted and requested
IN ∧ ¬Overflow(newPhase, final, emitted, width, height) \* admission may NOT overflow --
∧ AllocationStateOK(newAlloc, newTarget, newPhase, final, emitted, width, height)
\* ... and the new slot must fit the reservation invariant; otherwise the
\* block simply stays queued (denied, not summarized)
∧ phase' = newPhase \* commit the candidate state
∧ alloc' = newAlloc
∧ target' = newTarget
∧ UNCHANGED ⟨c, mode, want, final, emitted, history, native, width, height,
resizes, epoch, replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* repaint only: histories untouched
Update(i, snapshot) ≜ \* speculation evolves
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ phase[i] ∈ {"Queued", "Active"} \* only unfinalized blocks change
∧ (mode[i] = "Mutable" ∨ Prefix(want[i], snapshot)) \* THE append-only contract:
\* mutable blocks may replace their content arbitrarily; append-only
\* blocks may only extend it (old rows are immutable)
∧ snapshot ≠ want[i] \* no stuttering updates
∧ want' = [want EXCEPT ![i] = snapshot] \* the only writer of speculation
∧ UNCHANGED ⟨c, phase, mode, final, emitted, alloc, target, history, native,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* repaint only
RequestAllocation(newTarget) ≜ \* the app asks for new slot heights
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ AllocationStateOK(alloc, newTarget, phase, final, emitted, width, height)
\* admissible against the CURRENT paint: max(painted, newly-requested)
\* must fit, so every later animation frame is pre-paid (dominance)
∧ newTarget ≠ target \* no stuttering requests
∧ target' = newTarget \* targets change; paint doesn't yet
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, history, native,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* nothing visible happens yet
BridgeHeight(sampled, requested) ≜ \* B(a,t): next painted height
IF sampled < requested THEN requested \* growth jumps straight to target;
ELSE IF sampled > 2 ∧ requested = 1 THEN 2 \* a deep shrink (>2 -> 1) pauses at 2
ELSE requested \* all other shrinks are direct
\* the 2-row bridge frame makes deep collapses read as contractions, not snaps
ApplyAllocation(i) ≜ \* one animation frame is painted
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ phase[i] = "Active" \* only active slots animate
∧ alloc[i] ≠ target[i] \* something to do
∧ LET nextHeight ≜ BridgeHeight(alloc[i], target[i]) \* bridged next height
newAlloc ≜ [alloc EXCEPT ![i] = nextHeight]
IN ∧ AllocationStateOK(newAlloc, target, phase, final, emitted, width, height)
\* always satisfiable along a bridge: B never raises max(alloc, target)
∧ alloc' = newAlloc \* paint the frame
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, target, history, native,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* repaint only
FinalizeActive(i, snapshot) ≜ \* a live block completes
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ phase[i] = "Active" \* it was producing
∧ (mode[i] = "Mutable" ∨ Prefix(want[i], snapshot)) \* final must honor the contract
∧ LET newPhase ≜ [phase EXCEPT ![i] = "Finalized"]
newFinal ≜ [final EXCEPT ![i] = snapshot] \* the final value, frozen forever
newAlloc ≜ CanonicalAllocation(newPhase, newFinal, emitted, width, height)
IN ∧ phase' = newPhase \* lifecycle advances
∧ want' = [want EXCEPT ![i] = snapshot] \* want converges to final
∧ final' = newFinal \* (invariant: final = want)
∧ alloc' = newAlloc \* ALL slots collapse to canonical
∧ target' = newAlloc \* 1-row previews: finished content
∧ UNCHANGED ⟨c, mode, emitted, history, native, width, height, \* no longer animates
resizes, epoch, replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* repaint only: nothing retires yet
FinalizeQueued(i, snapshot) ≜ \* a block completes WITHOUT ever
∧ running \* having held a slot (finished
∧ ¬shutdown \* before space freed up)
∧ phase[i] = "Queued" \* straight from the queue
∧ (mode[i] = "Mutable" ∨ Prefix(want[i], snapshot)) \* same contract check
∧ LET newPhase ≜ [phase EXCEPT ![i] = "Finalized"]
newWant ≜ [want EXCEPT ![i] = snapshot]
newFinal ≜ [final EXCEPT ![i] = snapshot]
newAlloc ≜ CanonicalAllocation(newPhase, newFinal, emitted, width, height)
IN ∧ phase' = newPhase \* note: THIS transition may cause
∧ want' = newWant \* overflow (a hidden block becomes
∧ final' = newFinal \* presented) -- summarization, not
∧ alloc' = newAlloc \* denial, handles it here
∧ target' = newAlloc
∧ UNCHANGED ⟨c, mode, emitted, history, native, width, height,
resizes, epoch, replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* repaint only
AppendStable ≜ \* natural streaming: ONE stable row
∧ running \* of the append-only HEAD block
∧ ¬shutdown \* scrolls into both histories
∧ ¬Replaying \* never interleaves with replay
∧ c < CreatedCount \* a head block exists
∧ mode[c + 1] = "AppendOnly" \* only append-only blocks stream
∧ phase[c + 1] ∈ {"Active", "Finalized"} \* and only while live
∧ RowPressure \* only under ROW pressure: with
\* room to spare, stable rows stay in the viewport (still repositionable)
∧ emitted[c + 1] < Len(want[c + 1]) \* a stable row remains to stream
∧ LET next ≜ emitted[c + 1] + 1 \* index of the row to emit
newEmitted ≜ [emitted EXCEPT ![c + 1] = next]
newAlloc ≜ CanonicalAllocation(phase, final, newEmitted, width, height)
IN ∧ history' = history ∘ TagSlice(c + 1, want[c + 1], next, next) \* ledger += 1 semantic row
∧ native' =
native
∘ NativeTagSlice("Append", c + 1, want[c + 1], next, next, width)
\* native += the same row, rendered (1 or 2 physical rows), tagged Append
∧ emitted' = newEmitted \* the stable frontier advances
∧ alloc' = newAlloc \* layout recanonicalizes (the
∧ target' = newAlloc \* streamed row left the viewport)
∧ UNCHANGED ⟨c, phase, mode, want, final,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* frontier c itself does not move
CompleteAppendOnly ≜ \* the fully-streamed head commits
∧ running \* host alive
\* (deliberately NO ~shutdown: draining the head stays possible while
\* shutting down)
∧ ¬Replaying \* never during replay
∧ c < CreatedCount \* head exists
∧ mode[c + 1] = "AppendOnly" \* head is append-only
∧ phase[c + 1] = "Finalized" \* head is done
∧ emitted[c + 1] = Len(final[c + 1]) \* every row already streamed
∧ LET newPhase ≜ [phase EXCEPT ![c + 1] = "Committed"]
newEmitted ≜ [emitted EXCEPT ![c + 1] = 0] \* emitted counter retires with it
newAlloc ≜ CanonicalAllocation(newPhase, final, newEmitted, width, height)
IN ∧ c' = c + 1 \* frontier advances: PURE
∧ phase' = newPhase \* bookkeeping -- every row is
∧ emitted' = newEmitted \* already in both histories,
∧ alloc' = newAlloc \* so nothing is written
∧ target' = newAlloc
∧ UNCHANGED ⟨mode, want, final, history, native, width, height,
resizes, epoch, replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* note: history unchanged!
BeginFlush ≜ \* someone asks for full retirement
∧ running \* host alive
∧ ¬flush \* idempotent: set once,
∧ flush' = TRUE \* never reset
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target,
history, native, width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
shutdown, running, stopReason⟩ \* a pure request: no effect yet
RetireSuccess(batchEnd) ≜ \* in-order retirement of a batch
∧ running \* host alive
∧ ¬Replaying \* never during replay
∧ batchEnd ∈ (c + 1)‥N \* batch = blocks c+1 .. batchEnd
∧ FinalizedRange(c + 1, batchEnd) \* ... ALL of them finalized
∧ RetirementRequested \* only under flush or pressure
∧ history' =
history ∘ RetirementRows(c + 1, batchEnd, final, emitted[c + 1])
\* ledger += head's unstreamed suffix, then later finals in full
\* (emitted[c+1] is the only possibly-nonzero emitted counter)
∧ native' =
native
∘ NativeRetirementRows( \* native += the same rows,
"Retire", \* tagged Retire, rendered at
c + 1, \* the current width; realized
batchEnd, \* on a real terminal as ONE
final, \* streamed write (paper,
emitted[c + 1], \* Lemma "streaming
width \* realization")
)
∧ LET newPhase ≜ [i ∈ Blocks ↦
IF i ≤ batchEnd THEN "Committed" ELSE phase[i]] \* batch commits
newEmitted ≜ [i ∈ Blocks ↦
IF i ≤ batchEnd THEN 0 ELSE emitted[i]] \* counters reset
newAlloc ≜ CanonicalAllocation(newPhase, final, newEmitted, width, height)
IN ∧ c' = batchEnd \* frontier jumps to batch end
∧ phase' = newPhase
∧ emitted' = newEmitted
∧ alloc' = newAlloc \* retired slots disappear;
∧ target' = newAlloc \* survivors recanonicalize
∧ UNCHANGED ⟨mode, want, final, width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown, running, stopReason⟩ \* finals themselves are untouched
RetireFailure(batchEnd, count) ≜ \* the SAME write, torn partway:
∧ running \* same enabling conditions
∧ ¬Replaying \* as RetireSuccess ...
∧ batchEnd ∈ (c + 1)‥N
∧ FinalizedRange(c + 1, batchEnd)
∧ RetirementRequested
∧ LET rows ≜
NativeRetirementRows( \* the batch that WOULD have
"FailedWrite", \* been written, tagged
c + 1, \* FailedWrite for forensics
batchEnd,
final,
emitted[c + 1],
width
)
IN ∧ count ∈ 0‥Len(rows) \* the terminal accepted `count`
∧ native' = native ∘ PrefixOf(rows, count) \* rows: an arbitrary PREFIX --
\* never reordered, never a row from outside the batch
∧ running' = FALSE \* fail-stop: the host halts;
∧ stopReason' = "WriteFailure" \* no retry path exists, so
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target, history,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial, replayPrepared, replayCut, flush, shutdown⟩
\* CRITICAL: c and history do NOT advance -- the ledger never lies about
\* what committed, so duplication/reordering after failure is impossible
Resize(newWidth, newHeight, resizePolicy, pushed) ≜ \* terminal geometry changes
∧ running \* host alive
∧ ¬shutdown \* not during shutdown
∧ resizes < MaxResizes \* bounded (finite model)
∧ newWidth ∈ WidthValues \* new geometry and the
∧ newHeight ∈ 0‥H \* policy for native history
∧ resizePolicy ∈ ResizeModes
∧ newWidth ≠ width ∨ newHeight ≠ height \* an actual change
∧ pushed ∈ 0‥Len(Screen) \* emulator may scroll 0..h top
\* viewport rows into scrollback during the resize (e.g. height shrink)
∧ LET widthChanged ≜ newWidth ≠ width
effectiveMode ≜ IF widthChanged THEN resizePolicy ELSE "Preserve"
\* height-only resizes never replay: rendered rows are still valid
pushedRows ≜ NativeCells("Resize", PrefixOf(Screen, pushed), width)
\* rows pushed by the emulator, tagged Resize, at the OLD width
beginReplay ≜ effectiveMode ≠ "Preserve" ∧ (c > 0 ∨ PartialHeadExists)
\* replay only if there is committed/streamed content to re-render
newPhase ≜ phase \* lifecycle is untouched
newAlloc ≜ CanonicalAllocation(newPhase, final, emitted, newWidth, newHeight)
IN ∧ width' = newWidth \* adopt the new geometry
∧ height' = newHeight
∧ resizes' = resizes + 1 \* burn one resize budget
∧ alloc' = newAlloc \* layout recanonicalizes at
∧ target' = newAlloc \* the new geometry
∧ native' = IF effectiveMode = "Rebuild"
THEN ⟨⟩ \* Rebuild: native display is wiped ...
ELSE native ∘ pushedRows \* else: record what the emulator pushed
∧ epoch' = IF effectiveMode = "Rebuild" THEN epoch + 1 ELSE epoch
\* ... and the display epoch increments (native monotonicity is epoch-scoped)
∧ replayMode' =
IF beginReplay THEN effectiveMode \* start a replay,
ELSE IF Replaying THEN replayMode ELSE "None" \* or keep/clear the old one
∧ replayCursor' =
IF beginReplay THEN 1 \* replay window = committed
ELSE IF Replaying THEN replayCursor ELSE 0 \* blocks 1..c
∧ replayEnd' =
IF beginReplay THEN c
ELSE IF Replaying THEN replayEnd ELSE 0
∧ replayPartial' =
IF beginReplay
THEN IF PartialHeadExists THEN emitted[c + 1] ELSE 0 \* plus the streamed head prefix
ELSE IF Replaying THEN replayPartial ELSE 0
∧ replayPrepared' = FALSE \* ANY resize invalidates a
∧ replayCut' = 0 \* previously prepared frame
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, history,
flush, shutdown, running, stopReason⟩
\* resize logical-neutrality: ledger, frontier, and semantics never move
PrepareReplay ≜ \* compute the replay frame
∧ running \* host alive
∧ Replaying \* a replay is pending
∧ ¬replayPrepared \* and not yet prepared
∧ replayPrepared' = TRUE \* freeze the frame NOW:
∧ replayCut' = RequiredReplayCut \* cut = rows that must scroll
\* from here the scheduler gate (see Next) admits ONLY the two replay
\* writes, so the sampled cut cannot be invalidated by interleaving
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target,
history, native, width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
flush, shutdown, running, stopReason⟩ \* pure computation: no write yet
ReplaySynchronousSuccess ≜ \* the single buffered write lands
∧ running \* host alive
∧ Replaying \* replay pending
∧ replayPrepared \* frame prepared (gate open)
∧ native' = native ∘ PrefixOf(ReplayRows, replayCut) \* exactly `cut` rows scroll into
\* native; the tail was painted into blank rows (no scroll, no history)
∧ replayMode' = "None" \* replay fully drains:
∧ replayCursor' = 0 \* all replay state returns
∧ replayEnd' = 0 \* to its idle shape
∧ replayPartial' = 0
∧ replayPrepared' = FALSE
∧ replayCut' = 0
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target,
history, width, height, resizes, epoch,
flush, shutdown, running, stopReason⟩ \* logically neutral: ledger untouched
ReplaySynchronousFailure(count) ≜ \* the same write, torn partway
∧ running \* host alive
∧ Replaying \* replay pending
∧ replayPrepared \* frame prepared
∧ count ∈ 0‥replayCut \* an arbitrary prefix of the
∧ native' = native ∘ PrefixOf(ReplayRows, count) \* scrolled portion landed
∧ running' = FALSE \* fail-stop, as with
∧ stopReason' = "WriteFailure" \* RetireFailure: halt, no retry
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target, history,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
flush, shutdown⟩ \* ledger and frontier still truthful
BeginGracefulShutdown ≜ \* wind-down begins
∧ running \* host alive
∧ ¬shutdown \* only once
∧ LET newPhase ≜ [i ∈ Blocks ↦
IF phase[i] = "Absent" THEN "Absent" \* never-created stay absent;
ELSE IF i ≤ c THEN "Committed" ELSE "Finalized"] \* all live work freezes
newFinal ≜ [i ∈ Blocks ↦
IF phase[i] = "Absent" THEN NoFinal \* absent: still no final;
ELSE IF i ≤ c ∨ phase[i] = "Finalized"
THEN final[i] \* already-frozen finals kept;
ELSE want[i]] \* queued/active freeze AT their
newAlloc ≜ CanonicalAllocation(newPhase, newFinal, emitted, width, height)
IN ∧ phase' = newPhase \* current speculation (f := w)
∧ final' = newFinal
∧ alloc' = newAlloc \* layout collapses to canonical
∧ target' = newAlloc
∧ flush' = TRUE \* permanent flush: everything
∧ shutdown' = TRUE \* must drain, then exit
∧ UNCHANGED ⟨c, mode, want, emitted, history, native, width, height,
resizes, epoch, replayMode, replayCursor, replayEnd, replayPartial,
replayPrepared, replayCut,
running, stopReason⟩ \* nothing retires in this step itself
GracefulExit(push) ≜ \* clean exit after full drain
∧ running \* host alive
∧ shutdown \* shutdown was initiated,
∧ ¬Replaying \* replay has drained,
∧ c = CreatedCount \* and EVERY block committed
∧ push ∈ 0‥1 \* optionally scroll one last row
∧ push = 0 ∨ height > 0 \* (only if a viewport row exists)
∧ running' = FALSE \* host stops
∧ stopReason' = "Graceful" \* ... cleanly
∧ native' = IF push = 0
THEN native \* either no final scroll, or the
ELSE native ∘ NativeCells("Exit", ⟨Screen[1]⟩, width)
\* top viewport row scrolls out (restoring the shell prompt),
\* tagged Exit
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target, history,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial, replayPrepared, replayCut, flush, shutdown⟩
DetachExit(push) ≜ \* abandon ship: exit NOW,
∧ running \* uncommitted work is dropped
∧ ¬shutdown \* (a detach, not a shutdown)
∧ push ∈ 0‥1 \* same optional final scroll
∧ push = 0 ∨ height > 0
∧ running' = FALSE \* host stops
∧ stopReason' = "Detach"
∧ native' = IF push = 0
THEN native
ELSE native ∘ NativeCells("Exit", ⟨Screen[1]⟩, width)
∧ UNCHANGED ⟨c, phase, mode, want, final, emitted, alloc, target, history,
width, height, resizes, epoch,
replayMode, replayCursor, replayEnd, replayPartial, replayPrepared, replayCut, flush, shutdown⟩
\* ECH guarantees `history` holds exactly the committed content at detach
\* -------------------------------------------------------------------------
\* Existentially closed action wrappers (for fairness and Next).
\* -------------------------------------------------------------------------
RetireSuccessAction ≜ ∃ batchEnd ∈ Blocks : RetireSuccess(batchEnd) \* some batch retires
RetireFailureAction ≜ \* some batch write fails at
∃ batchEnd ∈ Blocks : \* some prefix length
∃ count ∈ 0‥MaxFailureRows : RetireFailure(batchEnd, count)
ReplaySynchronousFailureAction ≜ \* replay write fails at some
∃ count ∈ 0‥MaxFailureRows : ReplaySynchronousFailure(count) \* prefix length
\* -------------------------------------------------------------------------
\* The scheduler gate: once a replay frame is prepared, the ONLY possible
\* steps are the replay write landing or failing. This is what the word
\* "synchronous" means, and it is what keeps replayCut = RequiredReplayCut
\* stable (nothing may repaint in between).
\* -------------------------------------------------------------------------
Next ≜
IF replayPrepared
THEN ReplaySynchronousSuccess ∨ ReplaySynchronousFailureAction \* gate closed: write or die
ELSE ∨ ∃ declaration ∈ {"Mutable", "AppendOnly"} : Create(declaration) \* gate open:
∨ ∃ i ∈ Blocks : Admit(i) \* any protocol
∨ ∃ i ∈ Blocks, snapshot ∈ SnapshotValues : Update(i, snapshot) \* step may fire
∨ ∃ newTarget ∈ [Blocks → 0‥H] : RequestAllocation(newTarget)
∨ ∃ i ∈ Blocks : ApplyAllocation(i)
∨ ∃ i ∈ Blocks, snapshot ∈ SnapshotValues : FinalizeActive(i, snapshot)
∨ ∃ i ∈ Blocks, snapshot ∈ SnapshotValues : FinalizeQueued(i, snapshot)
∨ AppendStable
∨ CompleteAppendOnly
∨ BeginFlush
∨ RetireSuccessAction
∨ RetireFailureAction
∨ ∃ newWidth ∈ WidthValues, newHeight ∈ 0‥H,
resizePolicy ∈ ResizeModes, pushed ∈ 0‥H :
Resize(newWidth, newHeight, resizePolicy, pushed)
∨ PrepareReplay
∨ BeginGracefulShutdown
∨ ∃ push ∈ 0‥1 : GracefulExit(push)
∨ ∃ push ∈ 0‥1 : DetachExit(push)
Spec ≜
∧ Init \* start in the initial state,
∧ □[Next]_vars \* take Next steps (or stutter),
∧ WF_vars(RetireSuccessAction) \* and don't ignore forever:
∧ WF_vars(PrepareReplay) \* retirement, replay preparation,
∧ WF_vars(ReplaySynchronousSuccess) \* the replay write,
∧ WF_vars(AppendStable) \* head streaming,
∧ WF_vars(CompleteAppendOnly) \* and head commitment.
\* Weak fairness: an action enabled forever is eventually taken. Failures
\* and exits are NOT fair -- they may happen, but are never forced.
\* =========================================================================
\* Invariants (checked by TLC in every reachable state).
\* =========================================================================
TypeOK ≜ \* T: every variable in range
∧ c ∈ 0‥N \* frontier within block ids
∧ phase ∈ [Blocks → Phases] \* valid phase per block
∧ mode ∈ [Blocks → BlockModes] \* valid mode per block
∧ want ∈ [Blocks → SnapshotValues] \* speculation from the universe
∧ final ∈ [Blocks → SnapshotValues ∪ {NoFinal}] \* final or the sentinel
∧ emitted ∈ [Blocks → 0‥MaxSnapshotLength] \* emitted counter bounded
∧ alloc ∈ [Blocks → 0‥H] \* painted heights bounded
∧ target ∈ [Blocks → 0‥H] \* requested heights bounded
∧ history ∈ Seq(TaggedRows) \* ledger rows well-formed
∧ native ∈ Seq(NativeRows) \* native rows well-formed
∧ width ∈ WidthValues \* geometry in range
∧ height ∈ 0‥H
∧ resizes ∈ 0‥MaxResizes \* resize budget respected
∧ epoch ∈ 0‥MaxResizes \* epochs only at resizes
∧ replayMode ∈ ReplayModes \* replay state in range
∧ replayCursor ∈ 0‥(N + 1) \* (loose bound; really 0 or 1)
∧ replayEnd ∈ 0‥N
∧ replayPartial ∈ 0‥MaxSnapshotLength
∧ replayPrepared ∈ BOOLEAN
∧ replayCut ∈ 0‥MaxFailureRows \* cut bounded by max batch size
∧ flush ∈ BOOLEAN
∧ shutdown ∈ BOOLEAN
∧ running ∈ BOOLEAN
∧ stopReason ∈ StopReasons
LifecycleShape ≜ \* LS: blocks form three bands --
∧ c ≤ CreatedCount \* can't commit the uncreated
∧ ∀ i ∈ 1‥c : \* band 1: 1..c
∧ phase[i] = "Committed" \* all committed,
∧ mode[i] ∈ {"Mutable", "AppendOnly"} \* with a declared mode
∧ ∀ i ∈ (c + 1)‥CreatedCount : \* band 2: live blocks
∧ phase[i] ∈ {"Queued", "Active", "Finalized"}
∧ mode[i] ∈ {"Mutable", "AppendOnly"}
∧ ∀ i ∈ (CreatedCount + 1)‥N : \* band 3: not yet created
∧ phase[i] = "Absent"
∧ mode[i] = "Undeclared"
SnapshotDiscipline ≜ \* SD: finals exist exactly for
∀ i ∈ Blocks : \* finalized/committed blocks,
IF phase[i] ∈ {"Finalized", "Committed"}
THEN ∧ final[i] ∈ SnapshotValues \* are real snapshots,
∧ final[i] = want[i] \* and equal the last speculation
ELSE final[i] = NoFinal \* everyone else: the sentinel
EmissionDiscipline ≜ \* ED: streaming is head-only --
∧ ∀ i ∈ Blocks :
∧ emitted[i] ≤ Len(want[i]) \* never emitted more than exists
∧ (mode[i] ≠ "AppendOnly" ⇒ emitted[i] = 0) \* mutable blocks never stream
∧ (emitted[i] > 0 ⇒
∧ i = c + 1 \* only the HEAD may have
∧ phase[i] ∈ {"Active", "Finalized"}) \* streamed rows, and only live
∧ (PartialHeadExists ⇒ emitted[c + 1] ≤ Len(want[c + 1])) \* (redundant safety belt)
Capacity ≜ AllocationStateOK(alloc, target, phase, final, emitted, width, height)
\* CAP: the reservation invariant holds of the ACTUAL alloc/target at all times
ExactCommittedHistory ≜ history = CommittedRows(c, final) ∘ PartialHeadRows
\* ECH, the central equation: the ledger IS the committed finals in block
\* order, plus the head's streamed prefix -- no dupes, no gaps, no reorders
NoPrematureHistory ≜ \* every ledger row is owned by
∀ j ∈ 1‥Len(history) :
LET owner ≜ history[j].owner IN
∨ ∧ owner ∈ 1‥c \* a committed block, or
∧ phase[owner] = "Committed"
∨ ∧ PartialHeadExists \* the streaming head --
∧ owner = c + 1 \* speculation NEVER leaks
ScreenCapacity ≜ \* the screen is exactly right:
∧ Screen ∈ Seq(Cells) \* well-formed cells,
∧ Len(Screen) = height \* exactly `height` of them,
∧ ∀ i ∈ Blocks :
Cardinality({j ∈ 1‥height : Screen[j].owner = i}) = alloc[i] \* each block owns alloc[i] rows,
∧ Cardinality({j ∈ 1‥height : Screen[j] = OverflowCell})
= SummaryRows(phase, final, emitted, width, height) \* the summary row appears iff overflowing,
∧ Cardinality({j ∈ 1‥height : Screen[j] = BlankCell})
= height - AllocationTotal(alloc, 1)
- SummaryRows(phase, final, emitted, width, height) \* the rest is blank -- accounts balance
ReplayShape ≜ \* RS: replay bookkeeping is sane
∧ (replayMode = "None" ⇒ \* idle: all replay state zeroed
∧ replayCursor = 0
∧ replayEnd = 0
∧ replayPartial = 0
∧ ¬replayPrepared
∧ replayCut = 0)
∧ (replayMode ≠ "None" ⇒ \* in flight: window is 1..replayEnd
∧ replayCursor = 1
∧ replayEnd ∈ 0‥c \* over COMMITTED blocks only,
∧ replayPartial ≤ MaxSnapshotLength
∧ IF replayPrepared
THEN ∧ replayCut = RequiredReplayCut \* prepared: the sampled cut is
∧ Len(PreparedReplayTail) ≤ ReplayRoom \* still exact (the gate!) and
ELSE replayCut = 0) \* the tail fits the blank region
NativeSourceSafety ≜ \* NSS: provenance never lies --
∀ j ∈ 1‥Len(native) :
LET owner ≜ native[j].owner IN
∧ (native[j].source = "Retire" ⇒ \* Retire rows: from blocks that
∧ owner ∈ 1‥c \* really are committed
∧ phase[owner] = "Committed")
∧ (native[j].source ∈ {"Append", "Replay"} ⇒ \* streamed/replayed rows: from
∧ owner ∈ Blocks \* committed blocks or the
∧ (∨ owner ∈ 1‥c \* append-only head -- never
∨ ∧ owner = c + 1 \* from mutable speculation
∧ mode[owner] = "AppendOnly"))
∧ (native[j].source = "FailedWrite" ⇒ stopReason = "WriteFailure") \* failure rows only after failing
∧ (native[j].source = "Exit" ⇒ ¬running) \* exit rows only after exiting
\* =========================================================================
\* Temporal (action and liveness) properties.
\* =========================================================================
HistoryExtension ≜ Prefix(history, history') \* one step never rewrites the ledger
HistoryMonotonicity ≜ □[HistoryExtension]_vars \* ... in ANY step: append-only forever
NativeEpochStep ≜ \* per step, native either
IF epoch' = epoch
THEN Prefix(native, native') \* grows at the end (same epoch)
ELSE ∧ epoch' = epoch + 1 \* or is wiped exactly when the
∧ native' = ⟨⟩ \* epoch increments (Rebuild)
NativeEpochDiscipline ≜ □[NativeEpochStep]_vars \* holds of every step
FinalsStayFixed ≜ \* finals are immutable:
∀ i ∈ Blocks :
phase[i] ∈ {"Finalized", "Committed"} ⇒ final'[i] = final[i]
FinalImmutability ≜ □[FinalsStayFixed]_vars \* once frozen, frozen forever
AppendOnlyPrefixStep ≜ \* the append-only contract as
∀ i ∈ Blocks : \* an action property:
(mode[i] = "AppendOnly" ∧ phase[i] ∈ {"Queued", "Active"})
⇒ Prefix(want[i], want'[i]) \* want only ever extends
AppendOnlyMonotonicity ≜ □[AppendOnlyPrefixStep]_vars
ResizeKeepsLogicalHistoryStep ≜ \* resize logical-neutrality:
(width' ≠ width ∨ height' ≠ height) ⇒ \* a geometry change moves
∧ history' = history \* NONE of the semantic state --
∧ c' = c \* not the ledger, not the
∧ mode' = mode \* frontier, not modes,
∧ want' = want \* speculation,
∧ final' = final \* finals,
∧ emitted' = emitted \* or streamed counters
ResizeKeepsLogicalHistory ≜ □[ResizeKeepsLogicalHistoryStep]_vars
FailedWriteStops ≜ □( \* fail-stop: a write failure
stopReason = "WriteFailure" ⇒ ¬running \* and a live host never coexist
)
StoppedStep ≜ ¬running ⇒ UNCHANGED vars \* a stopped host is frozen:
StoppedQuiescence ≜ □[StoppedStep]_vars \* every later step stutters
AllFinalized ≜ \* every created block is done
∀ i ∈ 1‥CreatedCount : phase[i] ∈ {"Finalized", "Committed"}
AllCommitted ≜ \* everything retired, and the
∧ c = CreatedCount \* ledger is exactly the
∧ history = CommittedRows(c, final) \* committed finals
FlushLiveness ≜ \* drain guarantee: finalized +
(AllFinalized ∧ flush ∧ shutdown ∧ running ∧ ¬Replaying) \* flushing + shutting down
↝ (AllCommitted ∨ ¬running) \* eventually fully commits (or halts)
ReplayLiveness ≜ (Replaying ∧ running) ↝ (¬Replaying ∨ ¬running)
\* every replay eventually drains (or the host halts trying)
QueuedDemand ≜ ∃ i ∈ Blocks : phase[i] = "Queued" \* someone is waiting for space
QueuedPressureRetirement ≜ \* pressure + queued demand
∀ i ∈ Blocks : \* eventually sweeps a finalized
(∧ running \* head block into history:
∧ ¬Replaying
∧ c = i - 1 \* i is the head,
∧ phase[i] = "Finalized" \* it is done,
∧ Pressure \* space is scarce,
∧ QueuedDemand) \* and someone needs it
↝ (c ≥ i ∨ ¬running) \* => i eventually commits (or halt)
\* NB: this needs MaxLive small enough that queued demand implies
\* PERSISTENT count pressure; pure row pressure alone can evaporate
\* (see the paper's sharpness remark)
====