在一切开始之前，先说声谢谢。数十万人使用过 omp，报告过故障，提出过缺失的能力，并共同塑造了它的样子。本文和 omp² 本身都因你们而存在。
听说 omp² 后，许多人立刻问道：「但为什么？」
围绕一次 fetch 的 while 循环听起来很简单，但 OpenCode、Pi、OpenClaw 与 omp 正在同时进行完整重构，是有原因的：这种软件此前并不存在；只有从简单版本开始，我们才能看见裂缝，并朝着更好的版本努力。
不可避免的复杂性必须有人负责。目前，复杂性守恒定律将复杂性倾向扩展和用户，使得无法在 omp 或 Pi 之上编写可靠的软件。我已经能听见 「什么嘛，它扩展起来明明很简单、很愉快。」 再给我几章时间，我会改变你的想法。
Dijkstra 写道，「简单性是可靠性的前提」，但他也以用算法解决寻路问题著称。为什么不直接暴力求解？他完全不是在提出我们现在重复的 简单好，复杂坏 这种主张。这条建议是为了帮助实现者推理。我们可耻地用它来让实现者免于推理。
Ousterhout 在其斯坦福课程笔记中给出了缺失的另一半。他告诉模块作者要「拥抱痛苦」。接下困难的问题，彻底解决它，并让结果对其他所有人都易于使用。将复杂性压入模块。让少数实现者承担它，而非让每个调用者都承担一个更小、略有不同的副本。
我相信许多读者还记得那波把 Claude Code 比作游戏引擎的推文梗图。这个比较听来牵强，但若把渲染先放一边，列出一个 harness 的职责，二者确实相当吻合。
它维护权威世界、记录变更日志、运行不受信任的操作、向多个视图复制状态、调度参与者、解释命令、适配不兼容的协议，并渲染实时界面。
听起来熟悉吗？游戏引擎似乎已花费数十年，承担了同类复杂性的责任。
以下内容既是一次事后分析，也是一本行动手册：
- omp 教会我们的事 讲述我们在一个真实用户使用的系统中遇到的故障。
- omp² 的改变 描述替代架构——部分已经实现，部分仍在推进。
设计边界
在讨论智能体 harness 的任何子系统之前，先设想有四种截然不同的产品都将依赖它：
- 多路复用工作区 一个本地环境，多个 agent 与 subagent 位于同一文件夹。
- 远程驱动端 远程客户端通过手机驱动云端 agent——或桌下那台机器。
- 旁观者 一个观看 Claude agent 工作的 Web 客户端。
- Factorio 使用 SDK、面向不受信任输入的自动化软件工厂。
这些不是市场用户画像，而是架构测试。它们共同变化了使 harness 不再只是聊天循环的维度：
测试
本地或远程
交互式或自主式
信任边界
并发性
多路复用工作区
本地
交互式
大多可信
多个 agent，一个工作区
远程驱动端
远程
交互式
主机/客户端分离
一个或多个 agent
旁观者
远程视图
观测式
不受信任的呈现输入
多个观看者
Factorio
远程或集群
自主式
恶意的仓库与工具输入
多个任务
仅能服务第一个场景的设计，往往会把控制器塞进 TUI、将状态保存在闭包里、允许扩展在引擎进程中执行，并假定人类可以从无界调用中恢复。能在四种场景中存活的设计会被迫划出更好的边界。
本书余下部分沿着五个结果展开：
- 一个权威会话。 回退、分叉、恢复、复制与检查都必须源自同一份日志化状态。
- 受信任的控制平面。 策略和会话所有权留在主机；沙箱只接收有界的执行请求。
- 有界工作。 工具调用、subagent 和后台作业都是可取消的流，拥有中央限制与可观测性。
- 显式兼容性。 模型和提供商的怪癖是结构化知识，而非散落在调用点的分支。
- 视图是投影。 TUI、Web 客户端、远程客户端和 subagent 检查器渲染相同的状态，而非成为额外权威。
这些约束是下文一切内容的连接组织。后续章节提出 DOM、convar、Director、微小的 VM stub 或组件渲染器时，都是在解决这五项要求之一——不是为了聪明而引入一个子系统。
第一项要求是地基：在决定代码在哪里运行或如何渲染之前，harness 需要知道什么是真的。
状态
必须存续的内容
若希望某个东西可持久化、可回退、能容忍崩溃并可分叉，你有三种选择：
- 保存产生它的历史。
- 保存你关心属性上的变更。
- 保存机器本身。
Source Engine 在网络同步中采用了第二种方案的一个变体。omp 和 Pi 目前则是……没有任何一种被始终如一地采用。虽然存在事件，但状态并不真正从这些事件中派生，这违反了事件溯源的第一原则：状态必须能仅由事件推导出来。
omp 教会我们的：两个权威来源
走到这里有可以理解的理由。在每条日志中重复 system prompt 和 AGENTS.md 会很浪费；这可以通过对模板做哈希并保存其变量来解决。而且这种状态建模风格在 TypeScript 中并不常见，它实际上没有运行时类型。
然而，结果仍然是两个真相来源：
Source Engine
Pi 风格 harness
真相来源
entity list，仅此而已。服务器模拟；客户端预测。
消息树 加上 todo 状态、重试计数器、subagent 注册表、流式标志及其他持久化不可见的状态
Δ 的单位
{ Δ entity ... }，覆盖每个字段，因为每个 delta 都是 entity delta
message / custom / custom_message，没有引擎拥有的 fold；每个扩展手写派生
全局变量
CCSGameRules 是单例 entity。没有特殊情况。
三个层级，其中一个有效
插件状态
插件写入 entity 字段，因此状态默认会联网并重放
模块级闭包：let turnCount = 0、new Map()、new Set()
重放
加载 .dem，定位到一个 tick，并重新派生
加载 .jsonl；leaf 指针移动，而其他权威任意重置或存活
全局变量这一行最有趣。Source 没有会话全局变量；它们只是一个 entity 的属性。我们的则有自己的层级：
Source 的正确性并非来自仔细编写的协调器或出色的文档。它让不可重放的状态 无法表示。正确性来自该约束，而非每位扩展作者都记得注册两个 hook 并定义一个更新形状。
证据：在 API 中正确性是可选的
我们查看了 78 个官方 Pi 扩展示例。60 个是无状态的；有状态的 17 个里，仅有两个正确。
示例
逃离权威的状态
用户可见的故障
git-checkpoint.ts
checkpoint ref 由瞬态 Map 持有
/fork 在 agent_settled 已清空 checkpoint 后运行
plan-mode/index.ts
plan mode 从整个文件而非选中分支恢复
回退后限制仍生效；恢复可让已死分支复活
status-line.ts
回合计数保存在闭包中
从第 3 回合回退到第 1 回合会得到第 4 回合；恢复从零开始
dynamic-tools.ts
实时扩展注册表
工具在回退后仍存在，恢复后又消失
snake.ts
恢复扫描已放弃的分支
已死分支中的存档会回来
bookmark.ts
「最后」按文件顺序定义
已放弃分支中隐藏的 assistant 消息被加入书签
kimi-deferred-tools.ts
活动工具列表未重新派生
Calculator 在发现点之前仍保持活动
auto-commit-on-exit.ts
关闭将进程退出与会话切换混为一谈
/new、/resume 或 /fork 提交工作树
tic-tac-toe.ts
实时写入和恢复读取使用不同的 entry 类型
崩溃可能让用户的走子消失
你可在附录 A中找到详情，但重要的是，文档无法修复这种 bug 分布。引擎需要一个状态唯一能够存在的位置。
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"]]}
树才是权威；日志保存其增量变更。运行时对象可以缓存或索引它，但不会成为真相存放的第二处。在日志的任意位置，harness 都能物化——也因此能快照——整个会话。
单一权威带来的收益
状态与转录记录都在同一棵树中后，若干棘手问题就归约成同一个操作。
回退就是一次 DOM 差异比较。 将当前物化结果与目标状态比较差异。一个 <subagent> 元素消失了？销毁该元素即可终止它。出现了一个？创建该元素即可恢复或启动它。差异本身就是完整的生命周期工作清单。
新增一项有状态功能，永远不会为回退、分叉、恢复或复制增加一个调用点。
提示词成为投影。 不再有一个 100 行的状态对象被传入每个模板。系统提示词与其他一切一样，读取同一棵树：
- {{ count(select("todo item[status!=completed]")) }} open items
复制成为订阅。 我们已经具备应用及其派生过程。远程客户端消费补丁流，而非尾随读取文件。远程驱动端和旁观者场景不再需要单独铺设状态管线。
渲染成为投影。 组件注册表可从相同的元素状态渲染 Read、Bash、消息或 subagent。流式参数修改 <input>；流式输出修改 <result>。第七章会将其变为类型化接口，而不是另一个定制渲染器。
控制器与 actor
这种分离也使 subagent 可被检查。Pi 的视图直接读取实时会话状态——页脚调用 sessionManager.getEntries()——因此加入“检查 subagent”就意味着必须把控制器状态穿过 UI 内部层层传递。
应将控制器与 actor 完全分离：控制器拥有会话状态；actor 只渲染它的快照与补丁流。TUI、远程客户端和 subagent 检查器成为对等方。检查子级，只需让同一个 actor 指向子级的状态。
忠实的状态模型是基础，但若不受信任的代码拥有修改状态的策略，它仍可能被破坏。下一章将划定运行时边界。
运行时
状态章节确立了 harness 所认定的真相。运行时章节决定谁可以改变它、不受信任的工作在哪里运行，以及当执行可能持续数小时、流式输出或无视礼貌的停止请求时，“工具调用”究竟意味着什么。
沙箱应执行，而非决策
从设计边界中的 Factorio 场景开始。假设我们克隆 roboomp，请 gpt spark 将其中每一处名称都替换为 CodeWhatever，再开始为这项神奇技术向人们收取数千元。谁来运行工具？VM，当然了。才怪。
把执行器放进 VM 后，情况如下：
嗯，这不行。因为：
- 编程式工具使用需要访问全部工具；所以我们无法任意切分 harness 状态工具和环境状态工具。
- 我们需要构建双工网关，使 VM 能调用主机工具；而这会：
- 击败目的（不是启用了 DoS；就是必须以特定操作限流自己的 VM）
- 让这一切更复杂了，不，谢谢。
好吧，那就把驱动 app 放进 VM！
- 现在除非把 app 放到 VM 外面，并通过网络 RPC 连接 harness，同时把会话存储也移出去，否则 app prompt 与内部源代码都会泄漏。
- 但会话存储在外面，意味着必须授予 VM 写权限，这又同时回到了问题 #1 和 #2。
解决方案是在 VM 内放入一个单一、顺从的 stub，并且极其谨慎地限制回传流的最大数据量（你不会想让误用的 Read 工具返回 2GB 响应）：
这些图导向同一条边界：
- 主机 拥有会话状态、推理、策略、工具路由、审批、限制和日志记录。
- 沙箱 通过一个小而顺从的协议拥有环境执行。
- 每条回传流都会先受限，之后不受信任的一方才有机会耗尽主机内存或上下文。
这一安排满足 Factorio，又不会让本地使用变差。相同主机可以让 stub 指向本地进程、容器、VM 或远程机器。
Subagent 跨越同一边界
部署不只是主机对 VM。Subagent 在文件系统层也需要同一边界：worktree 仅隔离已跟踪文件，而 pi-iso 通过 APFS、btrfs、ZFS、overlayfs、ProjFS 或复制回退，为每个 child 提供整个工作区的写时复制视图。child 分歧；parent 收到 diff。
child 收到一个视图并返回变更。它不共享 parent 的可变权威。这是同一主机/沙箱规则的文件系统形式。
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 却迫使它们假装不是。
回调拆分重复了工作
首先，拆开渲染路径使响应式变成 opt-in。即使渲染出的工具不会「突然变成」新形态，作者也得复制大部分呈现逻辑。
更大的问题是 execute 的工作方式。以 Edit 为例：
renderCall会打开文件，最好在某处缓存读取的部分（哪里？），应用编辑并渲染 diffexecute随后会再次打开文件，完整应用、更改写入，并返回模型友好格式的 diffrenderResult接着拿到这个 diff，却必须解析我们选定的任何格式！为什么？因为人类当然想看带颜色和高亮的版本，也许还有更好的行号。
这导致一种本能式实现：
- 浪费 I/O 时间：文件打开两次
- 浪费 CPU 时间：应用的计算不是一次、不是两次，而是在每个字符变化时反复进行（
renderCall不是协程！） - 在任意格式上进行不必要的序列化/反序列化：为实现
renderResult，我们不得不解析模型输出（或在 details 中传递片段，复制已记录的数据）
要让它高效，你得实现一个在此定义之外驱动的协程，找地方保存其 handle，且仍不得不实现整套结果反序列化。
问题不只是重复的代码。这个契约没有一个权威对象，其状态可从「参数流式传输」经过「运行中」移动至「已完成」。每个实现都为这一生命周期发明一个侧信道。
omp² 的改变：执行是状态流
也没有通用方法来加入结构化警告、诊断或截断提示。多数 Pi 工具实现最终会写成这样：
text += `\n${theme.fg("warning", `[Truncated: ${truncation.outputLines} lines shown (${formatSize(truncation.maxBytes ?? DEFAULT_MAX_BYTES)} limit)]`)}`;
模型随后不得不猜测工具数据在哪里结束、harness 评论在哪里开始。因为 execute 不是 generator，流式输出还要经由 update channel 上的另一套协议。
DOM 模型移除了这两个特殊情况：
- 流式输出变更
<result>主体； - 添加警告会创建
<diag severity="warn">。
执行进行时，客户端会收到对此状态的 patch。完成后，与先前状态的最终 diff 会被记录。
在统一会话模型中，一次调用是一个拥有结构化子节点的 element：
<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>
executor 在运行时变更此 element。模型、用户、日志、远程客户端和测试 harness 观察同一状态的不同投影。完成会冻结最终 diff；没有客户端需要解析结果字符串来恢复序列化前存在的丰富对象。
限制是原语的一部分
Pi 工具没有限制：返回 1 MB 文本，它会逐字转发给模型。这是一个过于底层、不应直接暴露的原语。
一次性限制输出
Pi 自己曾在 Bash 与 Read 中面对这个问题，并以导出的截断工具来回答，供实现共享。omp 用 artifact 系统扩展了该工具，让模型可读回完整的保留输出，但职责仍和 Pi 一样，留给每个实现。
向模型发送 1 MB 可能是值得保留的能力，但它应当是 opt-out——一个中心实现和显式 notrunc 属性——而非将截断做成对好设计的 opt-in。将 helper 设为可选会以两种方式失败。
大部分工具都需要某种截断，因此 opt-in helper 必然造成覆盖不均：
- 不知道 helper 存在的作者自行实现，每一个都有略不同的提示；
- 从未想到结果会很大的作者什么也不做。
在工具实现内部而非会话渲染层截断，会破坏 Code mode：
- agent 永远无法在
Eval中信赖工具输出；每次使用前都得先从数据中解析出 harness 提示； Eval结果本身也可能被截断，因此每次调用都会围绕同一数据叠加 N+1 层互相独立的截断。
一次性限制阻塞时间
将 任何东西 后台化，并限制调用可阻塞多久，也属于库层——而非碰巧运行很久的每个工具。
第一个理由是缓存和 UX。否则，一次意外漫长的调用会让 agent 无法注意并调整、让用户回到一个卡住的会话、让自主任务无限等待，并让提供商的 KV cache 在调用返回前过期。
第二个理由——omp 也弄错了——是重复。每个工具都发展出自己的后台化时，也会发展出自己的 spawn、poll、message、kill 和 list helper。看看 Claude 围绕其 Task 和 Bash 工具绘制的图：
二者都汇聚到进程接口：signal + stream in + stream out。后台 shell、subagent、dev-server daemon、远程函数以及超过预算的普通调用，都是同一个对象——一个拥有 stdin、stdout、退出状态和 signal handle 的 job。一个 stdio 形状的 job 原语应封装它们全部。于是阻塞预算在一处强制执行，输出溢出到一条 artifact 路径，检查、发送消息或杀死其中任意一个也成为一个表面，而不是每工具一份副本。
可观测性的期望也以相同方式汇聚。想查看 subagent 状态的用户也想查看后台 shell。跨 harness 实例向同伴发消息的 agent 也想看见这些同伴运行的 daemon，以便一个目录中的 N 个 agent 共享同一个 HMR bun dev，而非在 N 个端口启动 N 个副本。
取消需要 kill 边界
扩展——因此也包括自定义工具——与引擎的 JavaScript isolate 共享，会导致灾难。正确的热重载几乎不可能，而工具调用一旦脱离协作式取消，就无法被强制停止。
JavaScript 和 Go 分别通过 AbortSignal 与 context.Context 暴露取消：这是有用的协议，却不是强制机制。忘记传递 signal、调用不接受 signal 的依赖、运行同步工作，或进入无限重试循环，timeout 只会通知 agent 继续；工作本身仍可能在后台燃烧资源。
因此，安全的 host 需要一个它真正可以终止的执行单元——进程、worker、subinterpreter、VM 请求，或一个等效边界，其死亡不会带走会话权威。取消属于运行时契约，而不是每位工具作者的良好行为。
让强制边界易于使用
一个刻意愚笨的 sandbox stub 带来 SDK 的最后一个问题：扩展作者现在看到了两个文件系统。否则，一个自定义 edit 函数可能不得不在一侧读取文件、完整传输，再在另一侧写回。
这就是 omp² 为扩展选择 Python 的原因。Python 能用标准库检查自身 AST，打包一个函数所需的源代码，并提交给另一个 runtime；@remote 属性可把看似本地的函数变成 RPC。这与让远程函数在 Modal 的 Python SDK 等系统中感觉自然，是同一种属性。
带入 Python runtime 也使 Eval 变得可靠，而非取决于碰巧安装了哪个解释器。一石二鸟。
当工作拥有受信任的所有者和可取消的执行原语后，harness 还需要一个一致的方式控制值和多回合行为。这就是控制平面。
控制平面
运行时拥有两种不同的控制。值 回答哪个模型、层级、主题或策略处于活动状态。行为 回答 agent 是否可以让出、是否必须再进行一回合，或是否暂时需要一种能力。每个调用者都拥有私有 setter 或 flag 时，二者都会失去一致性。
值：用设置声明策略
配置系统也成了雷区，有脏追踪和多个配置层级（全局、会话级、临时……）。与 Pi 中一样，大多数 get/set 操作都通过 AgentSession 类型路由，因为变更必须持久化到 JSONL。
你知道多年前解决所有这些问题的是什么配置系统吗？没错，Source Engine！
尤其值得注意的是，大多数玩过 Valve 游戏的人都能脱口而出 sv_cheats 的作用。尽管这么多年人们都在定制设置，我想不起任何一个不满的用户。你还能想起任何其他软件的任何其他配置吗？
convar 是具有名称、默认值、帮助字符串和 flags 位字段的类型化变量，在定义点声明一次：
ConVar sv_gravity("sv_gravity", "800", FCVAR_REPLICATED | FCVAR_NOTIFY, "World gravity.");
持久化、所有权、作用域、复制，甚至重放诚实性：都只是变量的 属性，在它诞生处声明。没有人通过一个上帝对象路由 set，也没有人手写脏追踪。
convar 不是会话 DOM 旁边的第二个设置数据库。会话作用域 convar 是权威树中又一个日志化节点；其 flags 声明它如何参与恢复、回退、spawn、复制和归档。
继承不应需要第二个设置
当前 omp 中，service tier（即 /fast）有一个仅为 subagent 设立的独立设置。
tier:
openai: priority
subagent: inherit # separate setting
在 convar 世界，ai_fastmode 是 一个 变量，标记为 SESSION：随会话记录，因此恢复会还原值。继承根本不需要 flag：默认情况下，spawn 的 child 会从 parent 的实时值播种 每一个 变量。没有任何东西需要 opt in。
想改成固定 child？一行即可：
# 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 作为 profile，subagent.cfg 在每次 spawn 时自动执行，<agent>.cfg 叠加其上，也解决了拥有千个属性的上帝对象。TF2 早就知道正确道路！
现在，一个值描述主会话及其 child。继承规则存在于值的定义处，而不是变成不断膨胀的会话上帝对象的另一个属性。
配置档与快捷键保持带内
一旦 cfg 存在，bind 会变得更好——bind、toggle 与 alias 也是 console command，因此我们不断为其发明 schema 的每种输入模式都能保持带内。用户想要一个隐藏 thinking 的快捷键？
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
这才是我们的快捷键层应有的样子：不是带有自己 defaults 表的定制 schema！
命令流是连接组织：cfg 文件、console 输入、alias、bind、远程管理及日志重放，都通过同一已声明变量说同一种语言。定制不再不断增加一次性 schema。
行为：循环形状的空洞
另一个受关注的话题是可扩展性。现在我要说 Pi 实际上拥有很好的扩展层，但它有一个「循环」形状的空洞。
我安装了 Pi 中最流行的 Plan 和 Goal 实现。尝试同时激活二者会得到：
好吧！这很有意思，但并没有“workflow” 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 拥有候选让出结果
agent 有一个循环。越来越多的事物想要指挥这个循环：plan 希望继续一回合直到计划存在，goal 希望继续一回合直到目标完成，/force 想改变下一次推理，todo 提醒则想在我们让出前得到最后一次提出异议的机会。
因此，应在 agent 层提供一个拥有该决策的对象：一组 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 mode
假设 plan mode 正在活动，而模型试图在未写入计划文件的情况下让出。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 活动时，它要么继续、压入子级，要么直接让给用户。它不会 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 与推理
- hook 会观察或编辑一次推理或一回合。
- Director 可跨回合保持控制权，并拦截让出。
- Director 可有意义地堆叠、嵌套、完成并恢复其父级。
这已足以让 plan、goal、vibe、autoresearch、提醒和外部验证等行为使用同一个 agent 层原语——而无需把其他每一种行为的私有 flag 教给它们。
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。这个回环 URL 是 llama.cpp，还是代理其他东西的 LiteLLM？最好再加一个特例。
任何单独的分支都没有问题！每一个都修复了真实的提供商 bug。问题在于，同一份知识最终被编码在多处：
compat/openai.ts：880 行model-thinking.ts：977 行variant-collapse.ts：1,776 行- 独立的 Bedrock、Anthropic 和 Devin 兼容性构建器
- discovery 和提供商序列化器中的更多名称检测
什么取代了它们？
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"
}
}
}
这才是我们真正试图表达的知识！4.6 之前的 Sonnet 版本使用预算式思考；Anthropic 4.7+ 使用自适应思考；只应在我们验证过的主机上声明这一点。
KDL 本身并不神奇。真正让我们免于以更漂亮的格式重建这团乱麻的是编译器：
- 未知指令或值？报错。
- 两条同样具体的规则设置同一项？报错——文件顺序不会暗中获胜。
- 没有匹配规则？是未知，而不是“false”。
这让提供商变得没那么古怪了吗？当然没有。我们仍有名为 requires-mistral-tool-ids、qwen-preserve-thinking、strip-deepseek-special-tokens 的兼容性轴，以及十种表达“关闭推理”的方式。看看这些名字，然后哭吧。
它让我们避免的是：在四个不同函数中再加一个分支来表达下一个怪癖。现在它是一条规则，位于拥有该事实的位置；优先级模糊时编译器会报错——推理层终于可以回答：这个精确模型在这个精确主机上实际支持什么？
收益不在于怪癖变少，而在于每个事实都有一个所有者、优先级明确，并且当库尚未确定答案时有 unknown 状态。harness 的其余部分不再通过提供商名称分支反复重新识别模型身份。
提供商不止有 stream
我为 web-search 实现 Pi 插件的那一刻起，这几乎注定会回来困扰我。事实上，这种压力也已触及仓库的极简起源；从 Pi 新增的图像模型实现中就能看出来。
Pi 将提供商建模为 stream 和 streamSimple，差不多就这些！这很适合快速搭建一个提供商，却不利于在其上持续构建更多能力，因为：
- Anthropic 的 token 计数接口怎么办？
- Codex 的 WebRTC 语音端点与远程压缩怎么办？
- Anthropic/OpenAI 的 web-search 怎么办？
- embedding 怎么办？
- 图像/视频生成怎么办？
- 分词怎么办？
- 用量查询怎么办？
- 模型发现怎么办？
你认为每个实现其中一项功能的扩展，也都正确实现了同步 OAuth 刷新和重试吗？
此外，能访问推理提供商所支持的前沿控制项也是一大收益，例如：
- 受约束采样
- OpenAI 的文本详略选项
- Google 的上下文过滤选项
- 强制工具调用
- 开发者角色
- 会话中途的系统提示词
- ...
身份验证刷新、重试、token 计数、搜索、生成、发现和提供商原生控制项都是共享基础设施。将它们留给扩展，必然会得到同一协议的多个不完整实现。
能力策略：强制工具调用
强制工具调用说明了为何“支持一个 flag”还不够：
- 在不支持的提供商上报错： 没有任何 harness 原生功能能使用它而不排除大部分模型阵容。
- 悄悄丢弃： 调用方会得到意料之外的尽力而为路径，并不得不发明自己的强制循环。
- 盲目透传： 提供商副作用会变成产品 bug；例如 Anthropic 可让强制调用导致整个对话缓存未命中。
- 不暴露它： 知情的调用方会绕过库，并重建全部三种失败模式。
理想的 harness 实现应当：
- 始终注入软提示词，告知模型下一回合必须调用该工具。无条件这样做是值得的：像 OpenAI 这样的托管 API 会悄悄替你追加这条提醒，而开源推理引擎不会；因此，vLLM 背后的模型会得到从未被告知的硬约束，并在启用推理时不知所措。软提示词能拉平这个差异。
- 仅在原生 flag 没有代价时设置它。若提供商支持无副作用的强制工具调用，就透传它；若它有代价，则跳过 flag，只依赖软提示词。
- 对不遵从进行升级处理。模型未调用工具时，进行有限次数重试；最后手段是在即使有代价的地方也设置原生 flag。一旦劝说失败，正确性胜过缓存。
这是上一章 Director 的 provider 侧实现。ForceTool 声明不变量；inference 选择满足它的最廉价且诚实的方式，并在模型不遵守时升级。
工具 schema 是面向模型的协议
工具的 parameters 字段严格定义其参数形状。这对人类 API 来说很理想；模型却不是通用 API 客户端。它们的错误往往与工具名称，以及训练中所代表的 harness 有关。
RL-maxxed agent 可能以另一种 harness 的 schema 调用熟悉的工具。Composer 模型有时会按其预期形状输出 Grep，即使根本没有 Grep 工具。Codex 可能看见 paths: string[]，就依当天心情发送以 ; 或 , 分隔的单个字符串。
因此库既应验证，也应修正。严格对待工具的语义契约，但宽容对待模型方言：映射无歧义时，将 paths: "a,b" 修复为列表；否则返回结构化、可重试的错误。原始 JSON Schema validator 无法独自拥有这一层。
严格采样需要预算和方言
受约束采样是我们最早加入 Pi 的功能之一：
+ strict?: boolean;
+ customFormat?: { syntax: "lark" | "regex"; definition: string };
+ customWireName?: string;
数月后 Pi 也加入 LARK 与 strict 支持，却将其作为不透明结构暴露，让 provider 层透传。两项系统级约束使这不够：
- 严格 schema 容量是共享预算。 许多 provider 限制严格 schema 的数量。因此，足够多独立编写的扩展便能使 provider 拒绝所有请求。用户不应必须二分查找并修补插件，才能恢复 harness。
- 语法方言依 provider 而定。 将 LARK grammar 传给每个 provider 本身可能无效。扩展无法维护兼容性映射，因为用户可将同一模型通过原生 host、proxy 或自定义 provider 路由。
这就是表面上「复杂」的实现应属于 inference 层的原因：
strict 所需的内容：提供商能力、带优先级的严格 schema 预算、按方言归一化，以及客户端修复路径——不透明的透传结构一个也无法提供。扩展声明意图——strictness、grammar、priority。inference 层拥有能力、预算、方言归一化、fallback、修复和最终 wire format。
修正性推理
推理库也需要：
- 修复格式错误的 JSON；
- 检测 Gemini、DeepSeek 等模型中的重复循环；
- 解析每个模型的输出方言，并在结构化输出泄漏到文本时合成规范化的
tool_call和thinkblock。
你可以阅读我先前关于此主题中工具调用一面的文章。支持一个提供商或模型，既需要接通 URL，也需要处理它独有的怪癖。
提供商适配器能够打开流时并不算完成。只有在面对畸形 JSON、重复、泄漏的推理或模型特有的工具调用方言时，harness 的其他部分仍收到一个规范回合，它才算完成。
压缩应被调度，而非被触发
朴素设计在这里也恰好带来最糟的 UX：用户在自己最投入的时刻，等待整个会话中最大的请求。
除了使用 Snapcompact 等方法，这里仍有大量改进空间。
更好的做法是在达到上限前约 10% 时，推测性地启动压缩过程。实质上，你让对话分叉为两个并发版本：一个让用户和模型继续工作，另一个让模型压缩对话。
收到响应后，将其拼接进另一个分支。这也能保留工作的势头：模型不会被一条作为历史中唯一消息的交接消息弄糊涂，而是会看到它本来就应当完成的全部进展。
除提示词外，还值得考虑：
- 远程压缩：由提供商在服务器端完成。OpenAI 的 API 返回一个不透明状态 blob；但因为它可访问解密后的思考，它能显著降低上下文损失。
- 交接：不要求摘要，而是要求模型“交接”这项工作。
- 摇晃：完全在本地完成；只需从历史中裁去沉重的工具结果。
请注意，这也是你应在 UI 渲染与请求渲染抽象中考虑的事：用户查看历史时，期望所有消息维持原样；但对模型而言，那些消息都将不存在。因此，创建请求 fn(this, req) -> req 时，应将提示词历史中的每个条目建模为一个“折叠”，并在 <Handoff> 的实现内处理它。
用小型本地模型完成 harness 工作
微型本地模型非常有用！即使你确实只使用前沿模型，我仍建议实现某种内嵌 tiny 模型（尤其可以看看 LiquidAI 模型）：它会为分类任务，以及生成标题、翻译、判断用户对对话进展满意度等小任务节省大量延迟与费用。当然，TTS/STT 也是一个用途，现在已可在本地获得 SoTA 性能。
这不是第二个“agent”，而是供小任务使用的廉价内部能力；它们不应承担前沿模型的延迟或成本。
一旦兼容与修复被集中处理，常驻工具表面就能保持精简。下一章将讨论哪些操作值得在每个请求中拥有 schema——以及哪些绝对不值得。
工具表面
运行时章节定义了工作如何执行。推理章节定义了 schema 如何跨模型与提供商存续。现在终于可以提出产品问题：哪些操作值得占据模型的永久语法？
每个 schema 都有代价
向模型呈现大多数工具的最佳方式，是根本不把它们放入常驻工具列表。
不久前，有人抱怨 omp 完成同一任务比 codex 慢；不是 token 维度，而是实际墙钟时间。我完全预期这会是件无足轻重的小事，但出乎意料的是，它是真的，甚至几乎慢了一倍！
sol，每项取 6 次运行的中位数，每次均为新会话 · 青色 = omp 变体，灰色 = 外部参考 · 注释为相对上一行的差值。罪魁祸首是工具列表。将它限制为五个必需工具，便得到 36.6s，领先于 Codex 的 42.2s 和 Pi 的 37.0s。为什么？工具 grammar！即使它只是给模型的文本描述，对于大多数前沿模型 provider，它也会主动参与 token 生成，因为它影响 token 的生成过程，驱使模型总是给出有效 JSON（还不包括描述它所耗的 token）。
工具并不是「万一模型需要」就免费的收益；这就是动态工具发现的思想。但这种动态方法一变更工具列表就会造成 cache invalidation，这也是我们不太喜欢它的原因。
Pi 有一部分做对了，我们也始终同意：MCP 的设计糟糕透顶，不属于永久工具层。那么怎样同时满足想要 Figma MCP 的用户和 inference 约束？
动态工具发现避免永久 grammar 成本，却会在每次工具列表变动时使 cache 失效。更好的目标是稳定、极小的 grammar，并通过普通组合抵达长尾。
将长尾置于稳定表面之后
认识 dyn CLI！这当然不是真实 CLI，而是由我们的 Bash 实现暴露的 builtin，它为模型提供稳定发现协议，并提供一种通过 Bash 或作为 Python 函数经 Eval 使用它的便利方式。
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 合成的，而这已经足以生成漂亮的 CLI mapping。
大型输入是它特别出色的地方：
dyn database/query "SELECT 1" # literal
dyn database/query @query.sql # file contents
cat query.sql | dyn database/query - # stdin
需要处理一个边缘情况：返回 image 的工具怎么办？那么 omp 如何向你显示 image？Sixel 或 Kitty protocol，对吧？何不在 Bash 工具中解析同样的输出并附加 image！现在还能通过 ssh 查看远程 image，妙。
当所有这些操作属于一个 API 时，还有第二种选择：暴露 code surface。Browser 保留 open / run / close 并对持久 tab 运行代码；Computer 在持久会话中暴露 desktop、wait 和 assert。一个稳定 schema，操作在一次调用中组合。有界操作集合：schema。开放操作集合：code surface。
这两种形式服务于不同形状的 API。有界操作集合可保持为 schema；开放操作集合需要 code 或 command surface，让数项操作在一次调用中组合。两者在发现后都无需改动永久列表。
契约卫生：意图与版本
契约有一个值得指出的小变更：每个工具都会获得一个 i intent 参数。它在参数流式传输时到达，因此 renderCall 可在调用完成前显示模型认为自己正在做什么。日志也获得易读摘要，而不必让每个工具发明 reason / purpose。
人们应当 给工具版本化。
它让 trace 更易使用：你可以解析频繁变动工具的 I/O，并随时间评估其成功率，无需猜测每次调用由哪一份契约产生。
深层 builtin
小型列表只有在其原语因语义理由而宽广时才有效——不是因为无关功能都被扔进一个 switch statement。omp 的 builtin 是有用示例。
Read：具象化资源
omp 中最无聊的工具，实际打包了其他系统中会是 20 个工具的能力。
- 可以读取目录，不需要
Ls。 - 不必加一个
ReadNotebook工具，读取.ipynb文件时默认就有漂亮输出。 .pdf、.docx、.pptx、.xlsx、.epub？会得到提取出的 markdown。.cpuprofil, .sample.txt？猜对了！会得到 bottleneck 摘要。.sqlite、.sqlite3、.db、.db3？可列出表、检查 schema、行，甚至查询。- image 会返回 image 或无需 vision 的 metadata。要预览 SVG，加上
:img。 - archive 无需解压即可寻址——不仅 ZIP 和 TAR，也包括 JAR、wheel 和 ASAR。
- 同样的投影适用于
http://...的在线资源，按需读取范围；普通网页会成为 markdown，就像web_fetch。
这并非为了聪明而多态。从模型视角，这些都是同一操作：
将此资源具象化为我能推理的最有用表示。
对于代码，它也能返回结构摘要，用省略号替换大型声明体。模型无需为了找到 class X 而将整个大文件拉入上下文。
当 bytes 很重要时，:raw 会绕过投影。:conflicts 为每个未解决 merge-conflict block 给出一行，而不是让模型在整个文件中寻找。
范围可以是开放式、基于长度或不连续：
: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 resource、subagent transcript、skill、memory、本地 scratchspace、omp 文档，甚至通过 SSH 的远程机器，都适配同一个内部 URL 子系统。我们推荐这一设计。
Read 还处理不那么可见的恢复：根据唯一工作区后缀解析错误的绝对路径、在 Windows 上展开 ~，以及避免其他浪费回合的路径错误。
这本可以是：
return await Bun.file(path).text();
是的。扩展作者便会实现自己的 reader，或者模型会找到 shell workaround，而 harness 则会以 web_fetch 等分离名称暴露形状相似的功能。
这不是更少的复杂性。它是同一复杂性，被复制进 shell command、prompt、extension 与失败工具调用中；没有人拥有它，而每个人都以略有不同的方式实现其中 30%。
Read 很复杂，因而读取无需复杂。
复杂性有唯一所有者。操作保持稳定，而资源特定投影移到其后。
Bash：感知策略的命令语言
Bash 工具不应只是 shell out 到 Bash。这听起来很离谱。
omp 随附完整 bash parser、interpreter 以及整套 coreutils，并在进程内运行；基于简单原因，这一直是好的选择：
- 保留模型的肌肉记忆。它可以使用
grep；因为 omp 是 interpreter，我们可以拦截命令并将合适参数路由给 ripgrep engine。没有人需要在AGENTS.md中花上下文恳求模型使用rg。 - 平台中立几乎免费获得。没有 WSL 或 Git Bash：omp 可在 Windows 上进程内执行大多数 Bash 调用。不必多言。
- console 在调用间保持状态，包含变量、exit code、
$!等等。
更有趣的优势会在 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 的瞬间询问；此前一切均只读。用户已允许向该目录写入时，它甚至可跳过该提示。
这让 harness 从「Bash」的 TSA 安检屏，变成能力审批者：「我可以用 Git push 吗？」find、cat 和 ln 等常见命令在进程内运行，实时查询访问模型，并继承用户已有读/写策略。
由于 host 解释常见命令，审批可发生在真正重要的能力边界——git push、工作区外写入、网络请求——而非不可读 shell string 边界。第 3 章的 runtime policy 因此可被强制执行，同时不丢弃模型的 shell 肌肉记忆。
AutoQA：给 agent 一条 bug report 路径
我们在 fork 的一个月后加入此工具，早于 Anthropic 为他们自己的产品加入等价物。
通常你会在某处提供让用户报告产品问题的方式，对吧？这是等价物，但服务对象是 agent。它让你全自动收集它们对工具的喜好、它们觉得困惑的事，以及它们观察到错误行为的信息。
报告质量并不算 很高，例如 Codex 喜欢在 Read 或 LSP 工具没有正确重命名时，将外部对文件的编辑怪罪给它们（不是我的错兄弟，去问 TypeScript 那帮人），但非常容易筛掉；一旦筛掉，就能获得大量关于哪个工具失败、应如何改善的信号。
AutoQA 闭合了工具设计与已部署行为之间的循环。它很嘈杂，但过滤明显的错误归因后，它会揭示哪项操作令模型困惑、哪种投影隐藏所需数据，以及哪种修复应归属 harness。
工具现在具有有界运行时、稳定发现表面与结构化状态。用户不应需要每位工具作者——往往是 Claude——都成为 terminal rendering 和 security 专家，才能安全地显示状态。
界面
267s → 90ms渲染时间，一个会话
13% 经分析的 CPU 耗在一次 .includes 上
98.7s耗于在 wrapAnsi 中反复包装
0该会话中的 image
会话 DOM 和工具状态流为每个客户端提供相同事实。但它们本身并不能产生安全、快速、一致的界面。renderer 仍可能把事实变成重新解析的字符串、扩展特定的样式约定，以及不可逆的 scrollback bug。
omp 教会我们的事：字符串会复合
这确实是我向 pi-mono 提交的第一个 PR 的主题之一。变更之前，若你在一项任务期间 profile Pi 并查看 CPU 使用，列表会完全被 renderer 占据，没错！
身为 TypeScript CLI，部分开销不可避免（仅字符串内部使用 UTF-16 这一点，就意味着每一帧都要经历相对昂贵的转码步骤，除非你疯狂地始终用 Uint8Array 表示文本）。
但真正让这项开销不断累积的是契约本身。想嵌入一个子组件？现在你得处理：
- 清理该
string，并丢弃或跳过解码 ANSI 转义序列 - 处理每一行的填充、截断和计算
而图像还可能作为 base64 文本经由其中一行传入，这也不会让情况变好。仅检查一行是否为图像行的 .includes，就占一个会话全部 CPU 周期的 20%。代价很高（而该会话甚至没有图像！）。
这还只是 JS 一侧的图表。这种设置下的渲染管线是一台堆整理机器：你不断分配、拆解并丢弃字符串与字符串数组——连接、切分、截断、填充，一步接一步反复进行。并不好。
同一份契约也让扩展没有共享的设计语言。只要用过任何 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 列以下，就会溢出当前行并撞坏下方的一切。
- 它完全不知道 terminal 宽度，因此即使还有空间，也会显示省略号！
- 最重要的是，它无视 Pi 组件的第一条规则，且不清理外部输入；这意味着被获取的内容只需送入正确的 ANSI 转义序列，就能把整个 UI 替换成一张鸭子图片。用它当然 不可能 做 别的事！
当你把复杂性下放给毫无防备的开发者——往往是 Claude——时，这类事情自然会发生。
每次要求 LLM“做个工具 UI 呗”时，它都不会记住 harness 的每个内部细节。说真的，我有时也不想记，而冒烟测试还会以“能用”通过。
性能、安全性和一致性问题有同一个根源：一个已渲染的字符串同时被用作布局树、样式树、内容、传输载体和 terminal 程序。
omp² 的改变：单次传递原语
最底层的消费者（即不是你，除非你提交 PR）将 RichText (Style, String) 推入交给它们的抽象管线 (&mut impl Out)。
这将 267 秒渲染时间降至 90ms：
render(): string[] ——N 个组件 × M 次转换，每一帧都重新解析、重新测量并重新分配每个缓冲区。之后：RichText 片段经抽象管线单次流入 frame diff。临时对象、ANSI parsing、grapheme 处理：在 frame renderer 之下的每一层都完全消失了，显然！
何必将 component 填充后往下传？我们直接……流式输出 padding、再输出你的其中一行，然后重复即可。何必让你完整以彩色渲染 255 行 diff，再 .slice(0, 3) 截断为另一组 string buffer array？我们直接……在省略号后丢弃流，或由自己把它作为 transformation 的一部分分行即可。
底层原语一次性拥有测量与转换。高层绝不应解析 ANSI 来发现它们自己发出的结构。
类型化组件模型
接下来，string[] 将被适当的 component model 替代。高层 consumer 只需堆叠 box，并享受 LSP 的引导：
<text> 内嵌套元素会在编辑时成为 lint 错误，而非在运行时生成损坏的帧。
<box>、<row>/<col>、一个 <ico:new/> 图标、水平 magenta..cyan 渐变，以及从 $$ \frac{1}{2} $$ 实时渲染的 ½。我可能不喜欢做前端，但天啊我真喜欢好的 abstraction。(Element, Props, Children) 加上 layout engine，就是让这一切如此美好的全部所需。
DOM 章节承诺工具 element 可由任何 actor 渲染。以下就是该承诺的具体形状：
这便是 Read component 的样子。还不错，对吧？
<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 client、snapshot test 和 remote inspector 决定如何在各自 surface 上布置该结构。
呈现策略属于 renderer
component model 免费带来两个有用属性：
<ico:new/>让每个 plugin 都方便地使用图标，同时尊重用户的 ASCII、Unicode 或 Nerd Font 选择。边框同理。- 语义颜色不再要求把 theme object 穿过每个 renderer。Claude 可以请求
info，而非选择字面颜色并希望它适合用户主题。
border=round bc="info" 解析为主题的语义色；fg="red..blue" 是渐变。没有任何主题对象被层层传递。还需要拥有 text stream 的节奏。Claude 和 Codex 以非常不同的 cadence 输出 chunk——一个每次几个单词，另一个每次几个字符。平滑这些差异会改变 harness 的响应感：稳定移动读作进展，爆发后停顿则不是。嘿。
语义 icon、border、color、truncation 与 stream pacing 现在都有唯一所有者。extension 请求 info、error 或 <ico:new/>；它们不再将 theme object 穿过每个函数，也不代表每位用户选择 Nerd Font glyph。
验证是界面的一部分
在当前这个「meta」中，最大 ROI、且几乎不花成本的投资，是要求 agent 为任意交互式 TUI / GUI 实现 debug protocol。若「如何验证」未知且未定义，agent 会走侧信道做一个 look-alike，也就是多数情况下创建一个实际上不检查任何事的测试文件。
预先定义「验证」的含义并提供便利形状，能大幅降低摩擦，从而使其成为开发循环的活跃部分。
具体形状并不重要，且随时可以更新：它可以是自定义工具、Python package 或 API，但绝对必须提供一个非破坏性、离屏、多实例的 东西，防止 agent 重新定义（通常是降级）成功的定义。
换言之，debug protocol 变成 UI 的机器可读定义，而不只是测试 helper。
transcript 是协议
TUI 真正不可能的部分，是关于它损坏的 GH issue 数量为 0。人们会对未知之物抱持理想主义；可惜许多人不知道他们想要的完美 TUI 体验不可能存在（每个 component 无论位置都完全实时更新、可动态变更）。
块
我们将规范 transcript 定义为 block 列表。一个 block 产生文本行，并经历生命周期：
活动 → 已定稿 → 已提交
存活期间，block i 显示当前 snapshot Wi，它是行数组。finalization 时，它冻结为不可变 snapshot Fi。
block 有两种模式：
- 可变：每个新 snapshot 可以整体替换前一个（spinner、进度）。snapshot 是推测性的，绝不成为历史；只有 Fi 会。
- 仅追加：snapshot 只会增长：每个 snapshot 都是下一个的前缀，最后一个 snapshot 是 Fi 的前缀（流式文本）。
当 block 长大到超出 viewport allocation 时，这一区分很重要。可变 snapshot 无法提前进入历史，因为后续更新可能会替换它；我们不得不拉回已经滚动的行。assistant thinking 等仅追加 block 只会扩展稳定前缀，因此该前缀可立刻开始提交。
终端
宽度为 W、高度为 H 的 terminal 有两个 buffer：
- V：viewport，含 H 个可见行
- S：native scrollback，无界、仅追加
技术上，我们可以清除并覆写 scrollback，但这会导致用户经常抱怨的行为；所以现在它是一个不变量。
换行 wrapW 将逻辑行变为物理行，取决于当前宽度。viewport 以下没有可寻址区域。写过其底部会滚动 terminal，并将顶部行不可逆地推入 S。
逻辑历史 L 以未换行的行保存，因而与宽度无关：按 block 顺序排列的已提交 final，每个恰好一次，外加当前 streaming block 已放行的部分。令 c 为最后一个 committed block，j = c+1：
L = F1 · F2 ⋯ Fc · Wj[1..ej]
其中 ej 计数 streaming head 已发射到历史的行（除非 block j 是流中仅追加 block，否则 ej = 0）。
因此：
- committed final 按 block 顺序连续且恰好出现一次；
- 可变的 speculative snapshot 永不进入 L；
- 仅追加 head 在仍流式传输时可逐行进入 L；
- finalization 不写入任何内容；
- commitment 只追加尚未发射的 Fj 行。
调整大小
resize 不改变任何逻辑内容：每个 Wi、每个 Fi 和 c 均不变。只有换行与 viewport allocation 会重新计算。native scrollback 中已有的行无法重写，因此 resize 对它们需要一条明确策略：
- Preserve：维持 emulator 换行后的历史原样。
- Append：追加重新渲染的历史，可能重复物理行。
- Rebuild：开始新的物理 epoch，并将历史重放进去。
这些规则将三项容易混淆的事物分开：viewport 中的可变呈现、宽度无关的逻辑历史、不可逆的 native terminal 行。一旦为它们命名，resize 和 streaming 就成为策略选择，而非经验之谈。
规定不可能的部分
为什么要让你经历这些「数学」？因为这是一个很复杂、很难验证其正确性的算法；上一迭代中，我们不得不写 fuzzer 才达到稳定点，这次我想避免。
因此，我们如所述在 TLA+ 中建模行为，并要求迭代地变更这些 block 的 commit 与 finalization 处理方式，直到所有明确指定的不变量都被满足。
现在，如果我们想做改动，例如 YOLO 地 commit partial，或不允许 block truncation，就有一份可更新的参考，也有一种极易知道它是否可行的方式；失败时会给出 counterexample。
论文与完整 ElasticSlots.tla 源码位于附录 B。
这带来了什么
例行炫耀一下，然后继续！现在如果有人抱怨 TUI 坏了，我可以给他们一份形式化证明，说明为什么它无法修复，太好了。
TUI、Web client 和 remote inspector 的布局可以不同，但真相不能不同。工具作者描述语义状态；component system 拥有呈现；transcript protocol 拥有恰好一次的历史。
这又是同一个设计动作：将艰难不变量压入能强制它的层。实现技术栈应加强那些不变量，而不是邀请每位贡献者——以及每个 coding agent——发明一种局部风格。
技术栈
前面的章节讲的是架构。语言选择决定 codebase 在该架构和下一个「好心」的局部例外之间设置多少摩擦。当很大一部分实现由接受过各生态系统默认值与病理训练的 agent 产出时，这尤其重要。
语言选择就是架构
除非必须与前端代码交互，否则目前 TypeScript 是一个糟糕的选择。
现在启动项目时，你能作出的最有影响力决定之一，就是选择正确工具。若三年前看到这样开头的文章，我会开始痛骂，但……若不信我，试着给 Claude 完全相同的 prompt，描述你想构建的 widget。
然后将 macOS（Swift）换成 Linux（Qt/JS）。前者会得到一个像属于 OS 的 glassmorphic widget，后者会得到一个 UI element 重叠、UX 选择堪忧的矩形，让你感觉像刚读完定义 UI 所需 XML schema，这是第一次编译它。
当然，你的 prompt 方式有影响，你确实可以给出更多细节；但过一阵便会注意到，无论做什么，其中一个都会几乎毫不费力地优于另一个。macOS 历来做得好的一件事是强迫开发者采用一种一致设计风格，LLM 也是如此。
重点不是 Swift 自带品味，而 JavaScript 没有。重点是默认值、标准库、规范项目形状、compiler feedback 和生态惯例，充当生成代码的先验。一种允许二十种同样正常局部风格的语言，会要求模型在触及产品问题前先作二十个决定。
TypeScript 会变成你的语言
我喜欢 TypeScript 的一件事，不幸的是，它最终总会变成 你的 语言：
- 用
camelCase还是snake_case？还是干脆把库命名为$？ - 写跨越 200 行的 generic，还是一个也不写？
- 用
Buffer还是Uint8Array？ - 用 Zod 还是 Typebox？
- 用
Array<T>还是T[]？ - 用 ESM 还是 CJS？（扩展名呢？
.ejs, .cjs, .mjs, .js?） - 用 TypeScript 还是 JSDoc？
- 用 Class，还是对象（或者天啊，
new function()）？ - 默认导出还是不默认？
- 用 star re-export，还是逐一命名？
- 用
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 }？
你看，我花了人生 10 年与最大的只写语言 C++ 相处，确实从中找到乐趣。但当被迫在 Zod 和 Typebox 中选择时，你的初级朋友只会写出我们称为 isRecord 的东西。既然可以直接 union 类型，为什么要用 generic？既然可以用一点 typeof 特化，为什么在脑中确保每个分支都对两种类型成立？为什么用 class，它不就是 objects 和 prototypes 吗？
可能是互联网上糟糕 JS 代码实在太多，也可能是它们一路吞了一堆 minified code，但我厌倦了。考虑到同一个初级开发者能发现 Linux 0-day，若我是你，我会停止期待 正确的模型 或 正确的代码质量工具，也别再折腾了。
也许 EffectJS 会改变这一点；我认为最后 Go 会在这里胜出（尤其是 WASM 的 GC proposal 定稿后），理由类似 Swift 在设计上胜出的原因（尤其是编译速度与交叉编译的便利），尽管某些场景需要更底层的系统语言，所以我们在这里选择 Rust。
它们仍然需要频繁引导，会走最短路径到目标；分配副本而非处理复杂 borrow、将错误作为字符串传递而非使用 thiserror，但配合 serde 生态，它们在 std 中拥有使其工作的绝大部分必要条件，而 compiler 也提供了足够安全性，所以就此决定。
用于扩展的 Python
下一个决定是是否为可扩展性邀请 TS 回来。我们说不，主要因为：
- Agent 能产出不错的 Py => 连带产出不错的 extension
- 在小 footprint 中实现规范兼容的 JS runtime 基本不可能（谢谢你，Locale）；而没有生态，我们还不如运行 Lua
- Extension 甚至不占运行时间的 1%，所以根本不需要 JIT
- 嵌入完整 Py runtime 后，还能保证
eval工具开箱即用，而非要求用户安装 py3 并永远无法在我们交付的 flow 中依赖它。 - Python 代码开箱即可检查自身 AST。这让 runtime 章节的
@remote设计成为可能。
运行时章节介绍了 @remote 边界。Python 的 introspection 和 attribute model 令这一边界使用起来顺手：SDK 可以检查函数、打包相关源代码，并在 sandbox runtime 执行它，而不用要求每位 extension 作者手写 RPC。
引入 runtime 也让 Eval 成为可靠的 builtin，而不是只在用户碰巧安装兼容 Python 时才可用的特性。
结语
「但为什么？」是开篇问题。直接回答是，上述每一章都是拥有数十年既有技术的软件类别：复制、沙箱、配置、调度、协议兼容性、实时渲染，以及语言/运行时设计。
omp² 仍在根据本文构建，状态从已交付到仍在思考不等；但我们真诚感谢每一个试用它并与我们分享各种绝妙用法的你们，从让它运行软件工厂，到让它在同一台手机上为自己构建 camera app。
你们塑造了 omp，我们期待未来同样有趣！
附录 A：官方示例中的状态故障
状态章节按类别概述了这些故障。本附录保留原始证据：源链接、最小代码摘录和复现视频。
这一主张并非理论。我们查看了 78 个官方扩展示例：60 个无状态；有状态的 17 个中，仅有两个正确。
1. checkpoint 在 /fork 能使用前被清除：git-checkpoint.ts
source：缺少持久的 checkpoint 所有权；/fork 在 idle 时调用，此时 agent_settled 已清空唯一 stash ref map。
const checkpoints = new Map<string, string>();
// …
pi.on("agent_settled", async () => {
checkpoints.clear();
});
2. 树导航不会恢复状态：plan-mode/index.ts
source：缺少 session_tree 和 getBranch()；回退会使 plan mode 及其工具限制保持活动，恢复却可让已死分支的 snapshot 复活。
const entries = ctx.sessionManager.getEntries();
const planModeEntry = entries
.filter((e) => e.type === "custom" && e.customType === "plan-mode")
.pop();
3. 计数器无法计数历史：status-line.ts
source：缺少分支派生；从第 3 回合回退到第 1 回合，下一个回合显示 4，而恢复会从零重新开始。
let turnCount = 0;
// …
pi.on("turn_start", async (_event, ctx) => {
turnCount++;
4. 动态添加的工具在回退后仍存在，恢复后又消失：dynamic-tools.ts
source：/add-echo-tool echo_branch 仅写入实时 extension registry；/tree 不会重启该 registry，因此回退后工具仍在，但 --continue 启动新 registry，工具就消失。
const registeredToolNames = new Set<string>();
// …
registeredToolNames.add(name);
pi.registerTool({
5. 一个存档从已放弃分支返回：snake.ts
source：restore 扫描整个 session file；在分支 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
source：缺少 getBranch()；回退后，/bookmark 可能标记用户看不到的已放弃分支上的 assistant 消息。
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
source：tool_search 激活 Calculator，但没有 session_tree handler 再次派生活动列表；导航至发现前的点后，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
source：缺少仅退出边界；/new、/resume 和 /fork 会触发 session_shutdown，进而 stage 并 commit 脏工作树。
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
restore；user move：重建仅接受工具结果，而用户走子是 custom entry；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：弹性推测槽位
界面章节在主阅读路径中保留协议与结论。本附录包含用于检查 transcript 不变量的论文和完整 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)
====