Плейбук харнесса

Прежде всего — спасибо. Сотни тысяч из вас пользовались omp, сообщали о том, что сломалось, предлагали, чего не хватает, — и сделали его тем, чем он стал. И этот пост, и сам omp² существуют благодаря вам.

2 сентября 2026

Перевод статьи Can Bölük с stencil.so. Оригинал: The Harness Playbook.

Can Bölük

Джан — инженер, автор omp и omp², кодинг-агентов в терминале. До этого много лет занимался реверс-инжинирингом и системным ПО.

Услышав про omp², многие из вас сразу спросили: «а зачем?»

Цикл while вокруг fetch — звучит просто. Но не зря OpenCode, Pi, OpenClaw и omp одновременно переписывают всё с нуля: такого класса программ раньше просто не существовало, и только начав с простой версии, мы увидели трещины — и поняли, куда двигаться дальше.

Неизбежной сложности нужен хозяин. Сейчас закон сохранения сложности работает против расширений и пользователей: надёжный софт поверх omp или Pi написать невозможно. Я уже слышу: «что-о-о, да он же так просто и приятно расширяется». Дайте мне несколько глав, чтобы вас переубедить.

Дейкстра писал, что «простота — необходимое условие надёжности», — и при этом известен тем, что решал поиск пути алгоритмически, а не полным перебором. Он вовсе не утверждал того, что мы теперь повторяем: «простое — хорошо, сложное — плохо». Совет должен был помочь разработчику рассуждать — а мы бессовестно используем его, чтобы избавить разработчика от рассуждений.

Недостающую половину даёт Остерхоут в конспектах своих стэнфордских лекций. Он призывает авторов модулей «принять страдание»: беритесь за сложные задачи, решайте их целиком и отдавайте остальным простой результат. Прячьте сложность внутрь модуля — пусть её несут несколько разработчиков, вместо того чтобы каждый вызывающий тащил свою собственную, чуть меньшую и чуть другую копию.

Многие читатели наверняка помнят волну мемов вокруг твита, сравнившего Claude Code с игровым движком. Сравнение звучит притянутым, но если перечислить обязанности харнесса — отложив рендеринг в сторону, — оно подходит удивительно хорошо.

Он держит авторитетный мир, журналирует изменения, запускает недоверенные действия, разносит состояние по нескольким представлениям, планирует актёров, интерпретирует команды, согласует несовместимые протоколы и рендерит интерфейс в реальном времени.

Ничего не напоминает? Похоже, игровые движки десятилетиями владеют ровно теми же категориями сложности.

Дальше — одновременно постмортем и плейбук:

• Чему нас научил omp — о сбоях, с которыми мы столкнулись в системе, которой люди реально пользовались.
• Что меняет omp² — об архитектуре на замену: часть уже построена, часть ещё прорабатывается.

Рамки проектирования

Прежде чем обсуждать любую подсистему агентного харнесса, представьте, что от неё зависят четыре совершенно разных продукта:

• Мультиплексированное рабочее место
  Локальная среда, где несколько агентов и субагентов работают в одной папке.
• Удалённый пульт
  Удалённый клиент, который с телефона ведёт облачного агента — или машину, стоящую под столом.
• Наблюдатель
  Веб-клиент, наблюдающий за работой Claude-агента.
• Factorio
  Автоматизированная софтверная фабрика, которая через SDK обрабатывает недоверенный ввод.

Каждый из них нагружает своё измерение — и именно оно не даёт харнессу остаться чат-циклом:

Дизайн, который работает только в первом сценарии, обычно прячет контроллер в TUI, держит состояние в замыканиях, исполняет расширения прямо в процессе движка и предполагает, что человек спасёт ситуацию после неограниченного вызова. Дизайн, который переживает все четыре сценария, вынужден строить границы как следует.

Вся остальная книга выводит пять следствий:

1. Одна авторитетная сессия. Откат, форк, возобновление, репликация и инспекция — всё это должно выводиться из одного и того же журналируемого состояния.
2. Доверенная контрольная плоскость. Политика и владение сессией остаются на хосте; песочницы получают только ограниченные запросы на исполнение.
3. Ограниченная работа. Вызовы инструментов, субагенты и фоновые джобы — это отменяемые потоки с центральными лимитами и наблюдаемостью.
4. Явная совместимость. Причуды моделей и провайдеров — это структурированное знание, а не ветки, разбросанные по точкам вызова.
5. Представления — это проекции. TUI, веб-клиент, удалённый клиент и инспектор субагентов рендерят одно и то же состояние, а не превращаются в дополнительные авторитетные источники.

Всё, что будет дальше (DOM, конвары, Директоры, VM-стаб, компонентный рендерер), существует, чтобы закрыть одно из этих пяти требований.

Состояние

Что должно выживать

Если вы хотите, чтобы что-то было долговечным, отматываемым, устойчивым к падениям и переживало форки, у вас три варианта:

1. Сохранять историю, которая это порождает.
2. Сохранять изменения нужных вам свойств.
3. Сохранять саму машину.

Source Engine использует вариант второго подхода для сетевой игры. omp и Pi сейчас не используют… ни одного из них последовательно. События-то есть, но состояние из них на самом деле не выводится — а это нарушает первый принцип event sourcing: состояние должно выводиться из одних только событий.

Чему нас научил omp: два авторитета

До этого места мы дошли по понятным причинам. Повторять системный промпт и AGENTS.md в каждой записи журнала расточительно; это решается хэшированием шаблона и хранением его переменных. Да и такой стиль моделирования состояния в TypeScript не принят — там попросту нет типов в рантайме.

Но результат всё равно — два источника истины:

Строка про глобальные переменные — самое забавное место. В Source нет глобалов сессии; это просто свойства сущности. А у нас сложилась собственная иерархия:

Source добился этого не тщательным реконсилятором и не хорошей документацией. Он сделал нереиграбельное состояние невыразимым — поэтому автору расширения не нужно помнить о регистрации двух хуков и определении формы апдейта.

Доказательства: корректность в API опциональна

Мы просмотрели все 78 официальных примеров расширений Pi. Шестьдесят не хранили состояния; из 17 состояниевых корректными оказались только два.

Подробности — в Приложении A. Такой разброс багов не вылечить улучшенной документацией; у движка должно быть одно место, где живёт состояние.

Что меняет 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. Сравните текущую материализацию с целевым состоянием. Элемент <subagent> исчез? Завершите его, удалив элемент. Появился? Возобновите или заспаньте его, создав элемент. Сама дельта — это полный список работ по жизненному циклу.

Добавление фичи с состоянием никогда не добавляет точек вызова в откат, форк, возобновление или репликацию.

Промпты становятся проекциями. Больше никакого объекта состояния на сто строк, проталкиваемого в каждый шаблон. Системный промпт читает то же дерево, что и всё остальное:

- {{ 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 один-единственный послушный стаб и очень-очень аккуратно ограничить максимальный объём данных, который стримится обратно (вам ведь не нужен ответ на 2 ГБ от злоупотреблённого Read):

Итого разделение такое:

• Хост владеет состоянием сессии, инференсом, политикой, маршрутизацией инструментов, аппрувами, лимитами и журналированием.
• Песочница владеет исполнением в окружении через маленький послушный протокол.
• Каждый поток, пересекающий границу в обратную сторону, ограничен — до того, как недоверенная сторона сможет исчерпать память хоста или контекст.

Локальное использование от этого не ухудшается: тот же хост может направить стаб на локальный процесс, контейнер, VM или удалённую машину.

Субагенты пересекают ту же границу

Размещение — это не только «хост против VM». Субагентам нужна та же граница на уровне файловой системы: ворктри изолируют только отслеживаемые файлы, а pi-iso даёт каждому ребёнку copy-on-write-представление всего рабочего пространства через APFS, btrfs, ZFS, overlayfs, ProjFS или запасной вариант с копированием. Ребёнок расходится; родитель получает дифф.

Чему нас научил 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);
	},
};

Маленький и приятный — но он разбивает одну операцию на три несвязанных колбэка, хотя превью, исполнение, результат для модели, результат для человека, диагностика, потоковые обновления, отмена и запись в журнал — всё это описывает один и тот же вызов.

Разбивка на колбэки дублирует работу

Во-первых, разделение пути рендеринга делает реактивность опциональной. Даже когда отрендеренный вызов не «защёлкивается» в новую форму, автору приходится дублировать большую часть логики представления.

Но главная проблема — как работает execute. Возьмём для примера Edit:

• renderCall откроет файл, в идеале закэшировав прочитанное где-то (где?), применит правки и отрендерит дифф;
• execute затем откроет файл ещё раз, применит всё, запишет и вернёт дифф в формате, удобном модели;
• renderResult получит этот дифф — и будет вынужден распарсить тот формат, который мы выбрали! Почему? Потому что человек, конечно, хочет видеть подсвеченную версию, может быть, с более красивыми номерами строк.

Это привело к реализации, получившейся самой естественной, которая:

• тратила время на 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">.

Пока исполнение идёт, клиенты получают патчи этого состояния. Когда оно завершается, в журнал пишется финальный дифф против предыдущего состояния.

В унифицированной модели сессии вызов — это элемент со структурированными потомками:

<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>

Исполнитель мутирует этот элемент, пока работает. Модель, пользователь, журнал, удалённый клиент и тест-харнесс наблюдают разные проекции одного и того же состояния. Завершение замораживает финальный дифф — и ни одному клиенту не нужно парсить строку результата, чтобы восстановить более богатый объект, существовавший до сериализации.

Лимиты — часть примитива

У инструмента Pi нет лимитов: верните мегабайт текста — и он будет передан модели как есть. Слишком низкоуровневый примитив, чтобы такой выставлять наружу.

Ограничивайте вывод один раз

Pi сам столкнулся с этим в Bash и Read и ответил утилитой усечения, экспортированной для совместного использования реализациями. omp расширил её системой артефактов, чтобы модель могла прочитать сохранённый полный вывод обратно, — но ответственность оставил там же, где её оставил Pi: на каждой реализации.

Отправка мегабайта модели может быть способностью, которую стоит сохранить, — но это должен быть opt-out: одна центральная реализация и явное свойство notrunc. А не opt-in в хороший дизайн, как сейчас. Оставить помощник опциональным — значит проиграть дважды.

Большинству инструментов усечение так или иначе нужно, поэтому опциональный помощник гарантирует неравномерное покрытие:

• авторы, не знающие о существовании помощника, пишут свои — каждый с чуть отличающимся уведомлением;
• авторы, не представившие огромный результат, не пишут ничего.

А усечение внутри реализации инструмента, а не на слое рендеринга диалога, ломает Code-режим:

• агент никогда не может полагаться на вывод инструмента внутри Eval: каждое использование вынуждено сначала выпарсивать уведомления харнесса из данных;
• результат Eval сам может быть усечён, так что каждый вызов накладывает N+1 независимых слоёв усечения на одни и те же данные.

Ограничивайте время блокировки один раз

Увод чего угодно в фон и ограничение того, как долго вызов может блокировать, тоже принадлежат слою библиотеки, а не каждому инструменту, которому случилось работать долго.

Первая причина — кэширование и UX. Иначе неожиданно долгий вызов оставляет агента неспособным заметить и подстроиться, пользователя — вернувшимся к зависшей сессии, автономные задачи — ждущими вечно, а KV-кэш провайдера — истёкшим к моменту возврата вызова.

Вторая причина, с которой omp тоже справился неправильно, — дублирование. Когда каждый инструмент обзаводится собственным фоновым режимом, он же обзаводится собственными хелперами spawn, poll, message, kill и list. Взгляните на диаграмму, которую Claude нарисовал вокруг своих же инструментов Task и Bash:

Обе сходятся на интерфейсе процесса: signal + stream in + stream out. Фоновый шелл, субагент, демон дев-сервера, удалённая функция и обычный вызов, выбежавший за бюджет, — всё это один и тот же объект: задача со stdin, stdout, кодом выхода и дескриптором сигнала. Один примитив задачи в форме stdio должен инкапсулировать их всех. Тогда бюджет блокировки обеспечивается в одном месте, вывод переливается в один путь артефактов, а инспекция, сообщение или убийство любого из них — одна поверхность, а не копия на каждый инструмент.

Ожидания наблюдаемости сходятся так же. Пользователи, желающие видеть состояние субагента, хотят видеть и фоновые шеллы. Агенты, шлющие сообщения соседям между инстансами харнесса, хотят видеть и демоны, которые те соседи запускают, — чтобы N агентов в одной директории делили один bun dev с HMR, а не поднимали N копий на N портах.

Отмена требует границы убийства

Расширения — а значит, и кастомные инструменты, — разделяющие JS-изолят движка, ведут к катастрофе. Надёжная горячая перезагрузка становится почти невозможной, а вызов инструмента нельзя принудительно оборвать, если реализация убежала за пределы кооперативной отмены.

JavaScript и Go выставляют отмену через AbortSignal и context.Context: полезные протоколы, но не принудительные. Забудьте передать сигнал, вызовите зависимость, которая его не принимает, запустите синхронную работу или войдите в бесконечный цикл ретраев — и таймаут лишь скажет агенту продолжить; сама работа может продолжать жечь ресурсы в фоне.

Безопасному хосту поэтому нужна единица исполнения, которую он действительно может завершить: процесс, воркер, сабинтерпретатор, VM-запрос или эквивалентная граница, чья смерть не может забрать с собой авторитет сессии.

Сделайте обязательную границу приятной

Намеренно тупой стаб песочницы создаёт одну последнюю проблему для SDK: авторы расширений теперь видят две файловые системы. Кастомной функции правки иначе пришлось бы прочитать файл на одной стороне, передать его целиком и записать обратно на другой.

Вот почему omp² выбрал Python для расширений. Python умеет инспектировать собственный AST через стандартную библиотеку, упаковывать исходник, нужный функции, и отправлять его в другой рантайм; атрибут @remote может превратить локально выглядящую функцию в RPC. Это то же свойство, что делает удалённые функции естественными в системах вроде Python SDK от Modal.

Встроенный Python-рантайм также делает Eval надёжным — а не зависящим от того, какой интерпретатор оказался установлен. Два зайца одним выстрелом.

Контрольная плоскость

Здесь живут два вида контроля. Значения: какая модель, тарифный уровень, тема или политика активна. Поведения: может ли агент вернуть управление, обязан ли сделать ещё один ход или временно нуждается в какой-то возможности. И то и другое превращается в кашу, когда у каждого вызывающего свой сеттер или свой флаг.

Значения: объявляйте политику там, где определена настройка

Система конфигурации тоже превратилась в минное поле — с отслеживанием «грязности» и несколькими уровнями (глобальный, сессионный, эфемерный…). Большинство операций get/set маршрутизировались через тип AgentSession, как и в Pi, — потому что изменения надо персистить в JSONL.

Знаете, какая система конфигурации решила все эти проблемы много лет назад? Да, Source Engine!

Особенно примечательно, что большинство людей, трогавших какую-нибудь игру Valve, навскидку помнят, что делает sv_cheats. Несмотря на все годы кастомизации, я не припомню ни одного несчастного пользователя. А сможете ли вы назвать систему конфигурации хоть какой-то другой программы?

Конвар — это типизированная переменная с именем, значением по умолчанию, строкой справки и битовым полем флагов — объявленная один раз, в месте определения:

ConVar sv_gravity("sv_gravity", "800", FCVAR_REPLICATED | FCVAR_NOTIFY, "World gravity.");

Персистентность, владение, область, репликация и даже честность реплея — всё это свойства переменной, заявленные там, где она рождается. Никто не маршрутизирует set через бог-объект, никто вручную не отслеживает «грязность».

Конвары не означают вторую базу настроек рядом с DOM сессии: конвар уровня сессии — просто ещё один журналируемый узел дерева, а его флаги объявляют, как он ведёт себя при возобновлении, откате, спавне, репликации и архивации.

Наследование не должно требовать второй настройки

Сегодня в omp у сервисного уровня (то есть /fast) есть отдельная настройка специально для субагента.

tier:
  openai: priority
  subagent: inherit   # separate setting

В мире конваров 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 — тоже консольные команды, поэтому каждый паттерн ввода, под который мы изобретали схемы, остаётся в том же канале. Пользователь хочет кейбинд, скрывающий размышления?

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

Вот как должен выглядеть наш слой биндингов — а не отдельная схема со своей таблицей дефолтов!

cfg-файлы, консольный ввод, алиасы, бинды, удалённое администрирование и реплей журнала — все говорят на одном командном языке над одними и теми же переменными.

Поведения: дыра в форме цикла

Ещё одна тема для беспокойства — расширяемость. У Pi, я бы сказал, на самом деле отличный слой расширений. Но в нём есть дыра в форме цикла.

Я пошёл и поставил самые популярные реализации Plan и Goal для Pi. Попытка активировать обе сразу даёт:

Любопытно! Только вот никакого «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. Поэтому мы назвали примитив, владеющий циклом, Директором — и перенесли больше встроенного поведения на публичную поверхность расширений, чтобы её дыры нельзя было игнорировать.

Директоры владеют кандидатами на возврат управления

У агента есть цикл. И всё больше вещей хотят этот цикл направлять: plan хочет ещё ходов, пока нет плана; goal — пока не достигнута цель; /force хочет изменить следующий инференс; напоминалка про todo хочет последнюю возможность возразить перед возвратом управления.

Так дайте слою агента один объект, владеющий этим решением: стек Директоров.

Под «стеком» мы имеем в виду живое поддерево в 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 идёт обратно наружу. Каждый Директор может:

• Пропустить (Pass) — дать следующему Директору посмотреть на кандидата на возврат.
• Продолжить (Continue) — потребить возврат и сделать ещё один ход.
• Вернуть (Yield) — потребить и реально вернуть управление пользователю.
• Протолкнуть (Push) — положить дочернего Директора поверх себя.
• Завершиться (Done) — сняться со стека и предложить тот же кандидат родителю.
• Упасть (Fail) — сняться с ошибкой.

Отсюда следствие: откат убирает Директоров, возобновление их восстанавливает, а удалённый инспектор видит, какое поведение сейчас владеет кандидатом на возврат.

Режим плана, целиком

Скажем, режим плана активен, а модель пытается вернуть управление, не записав файл плана. 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") в своём мягком режиме проталкивает маленького встроенного Директора, который добавляет эту возможность в следующий запрос инференса:

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 уже есть другой Директор ниже по стеку:

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, получает того же кандидата обратно, когда ребёнок завершается, — и либо продолжает, либо отдаёт его пользователю.

Хуки, Директоры и инференс

• Хук наблюдает или редактирует один инференс или ход.
• Директор может удерживать контроль через ходы и перехватывать возврат управления.
• Директоры осмысленно стекаются, вкладываются друг в друга, завершаются и возобновляют своего родителя.

Это покрывает plan, goal, vibe, autoresearch, напоминалки и внешнюю верификацию — и никому из них не нужно знать чужие флаги.

ForceTool выражает семантический запрос: «следующий успешный ход должен вызвать write». Он не знает, есть ли у выбранного провайдера нативный tool_choice, разрушает ли форсинг кэш и нужен ли локальной модели дополнительный промпт. Этот перевод принадлежит слою инференса.

Инференс

Чему нас научил 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. Означает ли этот loopback-URL llama.cpp или LiteLLM, проксирующий что-то ещё? Лучше добавить ещё одно исключение.

В каждой отдельной ветке нет ничего плохого! Каждая чинила реальный баг провайдера. Проблема в том, что одно и то же знание оказалось закодировано в нескольких местах:

• compat/openai.ts: 880 строк
• model-thinking.ts: 977 строк
• variant-collapse.ts: 1776 строк
• отдельные билдеры совместимости для 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 и десять способов написать «выключи рассуждение». Смотрите на имена и плачьте.

От чего это нас спасло — от выражения очередной причуды ещё одной веткой в четырёх разных функциях. Теперь это одно правило, в месте, которое владеет фактом, с компилятором, орущим при неоднозначном приоритете, — и слой инференса наконец может ответить на вопрос: что именно эта модель на этом именно хосте на самом деле поддерживает?

Провайдер — это больше, чем stream

Этому почти гарантированно суждено было вернуться и укусить меня в ту самую секунду, когда я реализовал свой плагин web-search для Pi. На деле то же давление ударило и по минималистичным истокам репозитория — как видно по новой реализации image-моделей в Pi.

Pi моделирует провайдеров как stream и streamSimple — и на этом всё! Отлично, чтобы быстро поднять провайдера. Не очень — чтобы строить поверх всё больше и больше, потому что:

• что насчёт интерфейса подсчёта токенов Anthropic?
• или WebRTC-голосового эндпоинта и удалённой компакции Codex?
• или web-search у Anthropic/OpenAI?
• или эмбеддингов?
• или генерации картинок и видео?
• или токенизации?
• или запроса использования?
• или дискавери моделей?

Как вы думаете, каждое расширение, делающее что-то из этого списка, ещё и правильно реализует синхронизированное обновление OAuth и ретраи?

Кроме того, доступ к самым свежим рычагам, которые поддерживает провайдер инференса, — большой выигрыш. Несколько примеров:

• Constrained sampling
• Опции многословности текста у OpenAI
• Опции контекстных фильтров Google
• Принудительные вызовы инструментов
• Роль разработчика
• Системные промпты посреди сессии
• …

Политика возможностей: принудительные вызовы инструментов

Принудительный вызов инструмента показывает, почему «поддерживать флаг» недостаточно:

• Ошибка на неподдерживающих провайдерах: ни одна встроенная фича харнесса не сможет её использовать, не исключив большую часть списка моделей.
• Молча уронить его: вызывающие получают неожиданный best-effort-путь и вынуждены изобретать собственный цикл принуждения.
• Слепо пробросить: побочные эффекты провайдера становятся багами продукта; Anthropic, например, может превратить принудительный вызов в промах кэша по всему диалогу.
• Не выставлять его: осведомлённые вызывающие обходят библиотеку и воспроизводят все три режима отказа.

Идеальная реализация харнесса:

1. Всегда вставлять мягкий промпт, говорящий модели, что на следующем ходу она обязана вызвать инструмент. Это стоит делать безусловно: хостед-API вроде OpenAI тихо добавляют такой толчок за вас, а опенсорсные движки инференса — нет. Так что модель за vLLM получает жёсткое ограничение, о котором её никто не предупредил, и барахтается при включённом рассуждении. Мягкий промпт выравнивает это поле.
2. Ставить нативный флаг только когда это бесплатно. Если провайдер поддерживает принудительные вызовы без побочек — пробрасывайте. Если за это что-то платится — пропускайте флаг и полагайтесь на мягкий промпт.
3. Эскалировать при невыполнении. Если модель не вызвала инструмент, ретрайте ограниченное число раз; в крайнем случае ставьте нативный флаг даже там, где он чего-то стоит. Когда убеждение провалилось, корректность важнее кэша.

Это инференс-половина ForceTool: Директор говорит, что должно произойти, а слой провайдера выбирает самый дешёвый способ этого добиться — и эскалирует, если модель не слушается.

Схемы инструментов — это протоколы, обращённые к модели

Поле parameters инструмента строго определяет форму его аргументов. Для человеческого API это было бы идеально; но модели — не генерические API-клиенты. Их ошибки часто специфичны к имени инструмента и к харнессам, представленным в обучающих данных.

Агенты, прокачанные RL, могут вызвать знакомый инструмент по схеме чужого харнесса. Модели Composer иногда испускают Grep с ожидаемой ими формой, даже когда никакого инструмента Grep не существует. Codex может увидеть paths: string[] и прислать одну строку, разделённую ; или ,, — по настроению дня.

Поэтому библиотека должна валидировать и чинить. Быть строгой к семантическому контракту инструмента, но снисходительной к диалекту модели: чинить paths: "a,b" в список, когда отображение однозначно; иначе возвращать структурированную, ретраибельную ошибку. Голый валидатор JSON Schema не может владеть этим слоем в одиночку.

Строгому сэмплингу нужны бюджеты и диалекты

Constrained sampling была одной из первых фич, которые мы добавили в Pi:

+   strict?: boolean;
+   customFormat?: { syntax: "lark" | "regex"; definition: string };
+   customWireName?: string;

Pi последовал через несколько месяцев — с поддержкой LARK и strict, но выставил это как непрозрачную структуру, пробрасываемую слою провайдера. Два общесистемных ограничения делают этого недостаточным:

1. Ёмкость strict-схем — общий бюджет. Многие провайдеры ограничивают число strict-схем. Достаточно независимо написанных расширений — и провайдер начнёт отклонять каждый запрос. Пользователь не должен бинарным поиском патчить плагины, чтобы вернуть харнесс к жизни.
2. Диалект грамматики специфичен к провайдеру. Передача LARK-грамматики каждому провайдеру сама по себе может быть невалидной. Расширение не может поддерживать карту совместимости — ведь пользователи могут маршрутизировать одну и ту же модель через нативные хосты, прокси или кастомных провайдеров.

Вот почему кажущаяся «сложной» реализация принадлежит слою инференса:

Корректирующий инференс

Библиотекам инференса также нужно:

1. чинить сломанный JSON;
2. детектить циклы повторений в моделях вроде Gemini и DeepSeek;
3. парсить диалект вывода каждой модели и синтезировать канонические блоки tool_call и think, когда структурированный вывод утекает в текст.

Об этой стороне вопроса можно прочитать мой прошлый пост про вызовы инструментов. Поддержка провайдера или модели требует обработки её личных причуд наравне с подключением URL.

Компакция планируется, а не срабатывает

Наивный дизайн, как выясняется, даёт ещё и худший UX.

Пользователь ждёт самый большой запрос сессии ровно в тот момент, когда он больше всего вовлечён.

Даже при использовании методов вроде Snapcompact здесь ещё много места для улучшений.

Вместо этого стоит спекулятивно запускать компакцию примерно за 10% до достижения лимита. По сути вы разветвляете диалог на две конкурентные версии: в одной пользователь и модель продолжают работать; в другой модель компактит диалог.

Получив ответ, вы встраиваете его внутрь другой ветки — что позволяет сохранить импульс работы: модель не запутается в сообщении-передаче, стоящем единственным в истории, а увидит весь прогресс, который ей и полагалось сделать.

Помимо промпта, стоит рассмотреть и другие методы:

• Удалённая компакция: провайдер делает её на стороне сервера. API OpenAI возвращает непрозрачный блоб состояния, но раз у него есть доступ к расшифрованным размышлениям, это может существенно уменьшить потерю контекста.
• Передача (handoff): вместо суммаризации попробуйте попросить модель «передать» работу дальше.
• Shake: полностью локально — можно просто обрезать тяжёлые результаты инструментов из истории.

Заметьте: это стоит учитывать и в вашей абстракции «рендеринг для UI против рендеринга для запроса». Пользователь ожидает, что все сообщения в истории останутся как есть; для модели же ни одного из них не существует. Поэтому каждую запись в истории промпта стоит моделировать как «свёртку» при создании запроса — fn(this, req) -> req — и обрабатывать внутри реализации <Handoff>.

Используйте маленькие локальные модели для работы харнесса

Крошечные локальные модели суперполезны! Даже если вы работаете только с пограничными моделями, я рекомендую встроить какую-нибудь tiny-модель (особенно посмотрите на LiquidAI): это сэкономит вам кучу латентности и денег на задачах классификации, а также на мелочах вроде генерации заголовка, перевода или оценки того, насколько пользователю нравится, как идёт диалог. Ещё один сценарий, конечно, — TTS/STT, где локально уже можно получить качество уровня SoTA.

Поверхность инструментов

Каждая схема — это налог

Лучший способ представить модели большинство инструментов — вообще не класть их в постоянный набор.

Как-то раз мне пожаловались, что omp медленнее codex на одной и той же задаче — не по токенам, а по настенным часам. Я ожидал, что это пустяк, но к моему удивлению оказалось правдой — почти в два раза!

Виновником оказался набор инструментов. Ограничьте его пятью необходимыми — и получите 36.6с, впереди Codex с 42.2с и Pi с 37.0с. Почему? Грамматика инструментов! Даже если для модели это просто текстовое описание, у большинства провайдеров пограничных моделей оно активно участвует в генерации токенов — заставляет их всегда выдавать валидный JSON (вдобавок к токенам, потраченным на само описание).

Инструмент — не бесплатный выигрыш на случай, если модели вдруг понадобится. Впрочем, из этой идеи вырос динамический дискавери инструментов — но он приносит инвалидацию кэша при каждом изменении набора, поэтому мы не большие его фанаты.

Pi одну часть понял правильно, и мы всегда с этим соглашались: MCP спроектированы ужасно и не принадлежат постоянному слою инструментов. Так как же удовлетворить и пользователя, желающего Figma MCP, и ограничения инференса?

Спрячьте длинный хвост за стабильные поверхности

Знакомьтесь: CLI dyn! Конечно, это не настоящий 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-схемы — а её уже достаточно, чтобы сгенерировать красивый 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 в постоянной сессии. Одна стабильная схема, а операции композятся внутри одного вызова. Ограниченный набор операций — схема. Открытый набор операций — поверхность кода. В любом случае постоянный набор после дискавери никогда не меняется.

Гигиена контракта: намерение и версия

Одно маленькое изменение контракта стоит отметить: каждый инструмент получает аргумент намерения i. Он приходит, пока аргументы ещё стримятся, так что renderCall может показать, что модель думает, будто делает, — до завершения вызова. Журнал тоже получает читаемую сводку — без того, чтобы каждый инструмент изобретал свой reason / purpose.

Людям стоит версионировать свои инструменты.

Это делает трейсы гораздо удобнее: можно парсить ввод-вывод часто меняющегося инструмента и оценивать его успешность во времени, не гадая, какой контракт породил каждый вызов.

Глубокие встроенные

Маленький набор работает, только если каждый инструмент покрывает много земли — и покрывает её потому, что это одна операция, а не switch по несвязанным фичам. Вот как это делают встроенные инструменты omp.

Read: материализуй ресурс

Самый скучный инструмент в omp на самом деле упаковывает то, что в других было бы двадцатью.

• Можно читать директории — Ls не нужен.
• Вместо отдельного ReadNotebook при чтении .ipynb-файла по умолчанию получаешь красивый вывод.
• .pdf, .docx, .pptx, .xlsx, .epub? Получаешь извлечённый маркдаун.
• .cpuprofil, .sample.txt? Верно, угадали! Получаешь сводку узких мест.
• .sqlite, .sqlite3, .db, .db3? Можно перечислить таблицы, инспектировать схемы и строки — или даже сделать запрос.
• Картинки возвращают либо само изображение, либо метаданные без зрения. Чтобы превьюить SVG, добавьте :img.
• Архивы можно адресовать без распаковки — и не только ZIP и TAR, но и JAR, wheel и ASAR.
• Те же проекции работают и для онлайн-ресурса по http://..., с диапазонами, читаемыми по требованию; обычные веб-страницы становятся маркдауном, как web_fetch.

Это не полиморфизм ради умничества. С точки зрения модели всё это одна и та же операция:

Материализуй этот ресурс в наиболее полезное представление, о котором я могу рассуждать.

Для кода она может вернуть ещё и структурную сводку, заменяя тела больших объявлений многоточием. Модели не нужно тянуть в контекст весь большой файл, чтобы найти класс 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. Никто не тратит контекст, умоляя модель использовать rg в AGENTS.md.
• Платформенная нейтральность почти бесплатна. Ни WSL, ни Git Bash: omp может исполнять большинство вызовов Bash внутри процесса на Windows. Сказано достаточно.
• Консоль остаётся стейтфульной между вызовами — включая переменные, коды выхода, $! и так далее.

Более интересное преимущество появляется, когда 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)

Можете сказать, что это делает, за пять секунд? (Если сказали «да» — вы врёте.)

Каково бы ни было ваше мнение об аппруве инструментов — это ужасно: никто не станет это читать. Свежие исследования Anthropic указывают в ту же сторону: авто-режим — ещё один Claude, читающий команду, — побеждает людей с большим отрывом.

Когда omp сам интерпретирует команду, он может спросить в тот самый момент, когда исполнение доходит до ln; всё до этого — только чтение. И может пропустить даже этот вопрос, если пользователь уже разрешил запись в эту директорию.

Это превращает харнесс из таможенного досмотра «Bash» в аппрувера возможностей: «Можно мне использовать git для пуша?» Частые команды вроде find, cat и ln выполняются внутри процесса, запрашивают модель доступа точно в срок и наследуют существующую политику пользователя на чтение/запись.

AutoQA: дайте агентам путь для багрепортов

Мы добавили этот инструмент через месяц после форка — до того, как Anthropic добавила эквивалент в свой продукт.

Знаете, как вы обычно даёте пользователям способ где-то сообщить о проблемах с продуктом? Это эквивалент того же — но для агентов. Она позволяет собирать — полностью автономно — информацию о том, что им понравилось в инструменте, что показалось запутанным и что вело себя ошибочно.

Качество репортов, правда, не такое уж высокое — Codex, например, обожает жаловаться на внешние правки файлов, виня инструмент Read или LSP, когда он неправильно переименовывает вещи (не моя вина, чувак, спросите ребят из TypeScript). Но их очень легко отфильтровать — и тогда вы получаете огромное количество сигнала о том, какой инструмент фейлит и как его улучшить.

Интерфейс

Чему нас научил omp: строки множатся

Это, кстати, была тема одного из моих первых PR в pi-mono. До изменения стоило профилировать Pi на протяжении задачи и посмотреть на использование CPU — весь список был занят, угадали кем, рендерером!

TypeScript CLI делает часть этого неизбежной (уже то, что строки внутри — UTF-16, означает относительно дорогой шаг перекодирования на каждом кадре — если только вы не таскаете Uint8Array как текст, как маньяк).

Но именно контракт заставляет этот расход множиться. Хотите встроить дочерний компонент? Теперь придётся иметь дело с:

• санитизацией этой string и отбрасыванием или декодированием ANSI-эскейпов;
• паддингом, усечением и подсчётом каждой строки.

Не лучше и то, что картинки могут передаваться одной из этих строк как base64-текст. Одна проверка .includes на «является ли эта строка картинкой» съедала 20% всех циклов CPU, потраченных в сессии. Дорогой счёт — а в той сессии вообще не было картинок!

Это лишь график 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 колонок;
• нет никакого знания о ширине терминала, так что даже при наличии места вы получите многоточие;
• и самое главное — игнорирует первое правило компонентов Pi и не санитизирует внешний ввод: то, что оно фетчит, может просто скормить ему правильные ANSI-эскейпы и заменить весь ваш UI картинкой утки. Точно ничего больше с этим сделать нельзя!

Такие вещи естественны, когда вы спихиваете сложность на ничего не подозревающего разработчика — часто на Claude.

LLM не будет помнить каждую внутреннюю деталь вашего харнесса каждый раз, когда её просят «сделай UI тулзы пжлст». Чёрт, я и сам иногда не очень хочу — а смоук-тест пройдёт как «работает».

Проблемы производительности, безопасности и консистентности родом из одного места: готовая строка выполняет работу дерева лейаута, дерева стилей, контента, транспорта и терминальной программы одновременно.

Что меняет omp²: однопроходный примитив

Потребители нижнего уровня (т.е. не вы, если только вы не делаете PR) проталкивают RichText (Style, String) в абстрактный пайплайн (&mut impl Out), переданный им.

Это срезает 267 секунд рендер-времени до 90 мс:

Временные объекты, парсинг ANSI, обработка графем: ПОЛНОСТЬЮ ИСЧЕЗЛИ из каждого слоя ниже рендерера кадра — очевидно!

Зачем нам паддить ваш компонент и передавать его дальше, если можно просто… стримить паддинг, потом одну вашу строку — и повторять? Зачем заставлять вас рендерить дифф на 255 строк в полном цвете, а потом делать .slice(0, 3), чтобы усечь это в ещё один массив строковых буферов, — если можно просто… оборвать ваш поток после многоточия или нарезать его на строки прямо внутри самой трансформации?

Типизированная модель компонентов

Дальше string[] будет заменён полноценной моделью компонентов. Потребители более высокого уровня будут просто стекать боксы и наслаждаться тем, как LSP показывает им путь:

Может, я и не люблю работать с фронтендом, но чёрт возьми, как я люблю хорошую абстракцию. (Element, Props, Children) — буквально всё, что нужно в связке с движком лейаута, чтобы сделать это чудесным в сравнении.

Вот так выглядит компонент 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, веб-клиент, снапшот-тест и удалённый инспектор раскладывают её каждый по-своему.

Политика представления принадлежит рендереру

Модель компонентов даёт два полезных свойства бесплатно:

• <ico:new/> даёт каждому плагину удобную иконку, уважая выбор пользователя — ASCII, Unicode или Nerd Font. Рамки работают так же.
• Семантические цвета больше не требуют объекта темы, протянутого через каждый рендерер. Claude может попросить info вместо того, чтобы выбирать буквальный цвет в надежде, что он впишется в тему пользователя.

Ещё нужно владеть темпом потока текста. Claude и Codex выдают куски с очень разной каденцией — один по несколько слов, другой по несколько символов. Сглаживание этой разницы меняет ощущение отзывчивости харнесса: равномерное движение читается как прогресс; рывки с простоями — нет. Хех.

Верификация — часть интерфейса

В нынешней «мете» самое ROI-ное вложение, которое ничего не стоит, — попросить агента реализовать отладочный протокол для любого интерактивного TUI / GUI. Если «как проверить» неизвестно и не специфицировано, агент обойдётся сторонним каналом — look-alike'ом, то есть создаст тестовый файл, который в большинстве случаев ничего реально не проверяет.

Определяя заранее, что значит «верификация», и давая ей удобную форму, вы значительно убираете трение — и она становится активной частью цикла разработки.

Форма не так важна и всегда может быть обновлена: это может быть кастомный инструмент, Python-пакет или API — но абсолютно необходимо предоставить неразрушающую, внеэкранную, мультиинстансную штуку, которая не даёт агенту переопределить (и обычно занизить) определение успеха.

Транскрипт — это протокол

Действительно невозможная часть TUI — иметь ноль ишью на GitHub о том, что она сломана. Люди — идеалистические существа насчёт того, чего не знают, и, к сожалению, многие не знают, что идеальный TUI-опыт, которого они хотят, невозможен (каждый компонент полностью актуален вне зависимости от расположения, динамически мутируемый).

Блоки

Мы определяем канонический транскрипт как список блоков. Блок производит строки текста и проходит жизненный цикл:

active → finalized → committed

Пока жив, блок i показывает текущий снимок W_i — массив строк. При финализации он замораживается в неизменяемый снимок F_i.

Блоки бывают в двух режимах:

• Мутабельный: каждый новый снимок может заменить предыдущий целиком (спиннеры, прогресс). Снимки спекулятивны и никогда не становятся историей; ею становится только F_i.
• Только на приращение: снимки только растут: каждый снимок — префикс следующего, а последний снимок — префикс F_i (стримящийся текст).

Различие важно, когда блок перерастает своё вьюпортное выделение. Мутабельный снимок не может войти в историю раньше времени — более поздний апдейт может его заменить, и пришлось бы выдёргивать уже проскролленные строки. Блок «только на приращение» вроде размышлений ассистента лишь расширяет стабильный префикс, так что этот префикс может начать коммититься сразу.

Терминал

Терминал шириной W и высотой H имеет два буфера:

• V: вьюпорт из H видимых строк
• S: нативный скроллбэк, неограниченный, только на приращение

Технически мы могли бы очищать и переписывать скроллбэк, но это приводит к поведению, на которое пользователи часто жалуются, — так что теперь это инвариант.

Перенос wrap_W превращает логические строки в физические и зависит от текущей ширины. Под вьюпортом нет адресуемой области. Запись за его нижний край скроллит терминал и необратимо проталкивает верхние строки в S.

Логическая история L хранится в неперенесённых строках, так что она независима от ширины: закоммиченные финалы в порядке блоков, каждый ровно один раз, плюс столько текущего стримящегося блока, сколько уже было пропущено. С c — последним закоммиченным блоком и j = c+1:

L = F₁ · F₂ ⋯ F꜀ · Wⱼ[1..eⱼ]

где eⱼ считает строки, которые стримящаяся голова уже испустила в историю (eⱼ = 0, если только блок j не является блоком «только на приращение» посреди стрима).

Поэтому:

• закоммиченные финалы встречаются ровно один раз, подряд, в порядке блоков;
• мутабельные спекулятивные снимки никогда не входят в L;
• голова «только на приращение» может входить в L построчно, ещё стримясь;
• финализация ничего не пишет;
• коммит добавляет только строки F_j, ещё не испущенные.

Изменение размера

Ресайз ничего логически не меняет: каждый W_i, каждый F_i и c выживают неизменными. Пересчитываются только перенос и вьюпортное выделение. Строки, уже попавшие в нативный скроллбэк, переписать нельзя, поэтому для них нужна одна явная политика:

• Сохранить: оставить историю, перенесённую эмулятором, как есть.
• Дописать: дописать перерендеренную историю, возможно дублируя физические строки.
• Перестроить: начать новую физическую эпоху и прогнать историю в неё.

Специфицируйте невозможную часть

Зачем я провёл вас через всю эту «математику»? Потому что это очень сложный алгоритм для проверки вменяемости: в прошлой итерации нам пришлось написать фаззер, чтобы добраться до стабильной точки, а в этот раз я бы хотел этого избежать.

Вместо этого мы смоделировали поведение в TLA+, как описано, и просили итеративные изменения в том, как обрабатываются коммит и финализация этих блоков, — пока все чётко специфицированные инварианты не были удовлетворены.

Теперь, если мы захотим что-то поменять — скажем, йоло-коммитить части или запретить усечение блоков, — у нас есть референс для обновления и чрезвычайно простой способ узнать, сработает это или нет, с контрпримером при провале.

Полный текст статьи и весь исходник ElasticSlots.tla живут в Приложении B.

Что это открывает

Обязательный хвастливый момент — и поехали дальше! Теперь, если кто-то пожалуется, что TUI сломана, я могу предъявить формальное доказательство, почему это невозможно починить. Отлично.

Стек

Выбор языка — это архитектура

TypeScript — ужасный выбор на данный момент, если только у вас нет другого выхода, кроме как взаимодействовать с фронтенд-кодом.

Одно из самых влиятельных решений, которое вы можете принять, начиная проект прямо сейчас, — выбор правильного инструмента. Если бы я увидел статью, начинающуюся так, 3 года назад, я бы начал ругаться, но… если мне не верите, попробуйте дать Claude один и тот же промпт, описывающий виджет, который хотите построить.

Теперь поменяйте macOS (Swift) → Linux (Qt/JS). Первый выдаст вам стеклянный виджет, выглядящий как родной для ОС; второй — прямоугольник с налезающими элементами UI и сомнительными UX-решениями, от которого остаётся чувство, будто вы только что дочитали XML-схему, требуемую для описания UI, и впервые скомпилировали её.

Конечно, то, как вы промптите, играет роль, и вы действительно могли бы уточнить детали. Но через какое-то время вы заметите: что бы вы ни делали, один будет обгонять другой почти без усилий. Одна вещь, которую macOS исторически делала хорошо, — загоняла разработчиков в единый консистентный стиль дизайна; и с LLM ровно так же.

У Swift нет собственного вкуса — у него сильные дефолты. Стандартная библиотека, привычная раскладка проекта, ошибки компилятора и конвенции экосистемы — всё это работает априорным знанием для сгенерированного кода. Язык с двадцатью одинаково нормальными стилями заставляет модель выбирать один из них двадцать раз, прежде чем она доберётся до вашей задачи.

TypeScript становится вашим языком

Единственное, что я любил в TypeScript, к несчастью, — это то, что он всегда в итоге становится вашим языком:

• camelCase или snake_case? или просто назвать свою либу $
• писать дженерики на 200 строк или не иметь ни одного?
• использовать Buffer или Uint8Array?
• использовать Zod или Typebox?
• использовать Array<T> или T[]?
• использовать ESM или CJS? (а расширение? .ejs, .cjs, .mjs, .js?)
• использовать TypeScript или JSDoc?
• использовать Class или остаться на объектах (или, чёрт, new function())?
• экспортировать через default или нет?
• использовать звёздные реэкспорты или именовать каждый?
• использовать 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 }?

Видите ли, проведя десять лет жизни с самым большим write-only языком, известным как C++, я нахожу радость и в этом. Однако, когда приходится выбирать между Zod и Typebox, ваш джуниорский друг просто напишет то, что мы называем isRecord. Зачем дженерики, если можно просто объединить типы? Зачем мысленно проверять, что каждая ветка работает для обоих типов, если можно специализироваться маленьким typeof? Зачем классы — это же просто объекты и прототипы, да?

Может, дело в чистом количестве плохого JS-кода в мире, а может — в том, что они по пути проглотили кучу минифицированного кода, но я устал от этого. Учитывая, что тот же джуниор может найти 0-day в Linux, будь я вами, я бы перестал надеяться на правильную модель или правильный инструмент качества кода и перестал прыгать через обручи.

Возможно, EffectJS это изменит, но по мне, Go в итоге станет победителем здесь (особенно когда GC-предложение для WASM финализируется) по причинам, сходным с теми, почему Swift побеждает в дизайне (особенно со скоростью компиляции и лёгкостью кросс-компиляции) — хотя некоторые случаи требуют более низкоуровневого системного языка, поэтому здесь мы выбрали Rust.

Их всё ещё приходится довольно часто направлять — они идут кратчайшим путём к цели: копируют аллокации вместо разбирательства с заковыристыми борроу, передают ошибки строками вместо thiserror — но у них есть большая часть необходимого для работы в std в связке с экосистемой serde, а компилятор даёт приличное количество безопасности. Вот и всё.

Python для расширений

Следующим решением было — возвращать ли TS для расширяемости. Мы сказали нет, в основном потому что:

1. Агенты выдают приличный Py => приличные расширения, по совместительству
2. Соответствующий спецификации JS-рантайм — в принципе невозможен в маленьком футпринте (спасибо, Locale), а без экосистемы мы с тем же успехом могли бы запускать Lua
3. Расширения не составляют и 1% времени исполнения, так что JIT нам не очень нужен
4. С полным встроенным Py-рантаймом мы можем гарантировать, что инструмент eval работает из коробки — вместо того чтобы просить пользователя поставить py3 и никогда не иметь возможности полагаться на него в потоках, которые мы поставляем
5. Python-код умеет инспектировать собственный AST из коробки. Именно это делает возможным дизайн @remote из главы про рантайм.

В заключение

Так, зачем? Потому что каждая глава выше — вид софта, который люди строят десятилетиями: репликация, песочницы, конфигурация, планирование, совместимость протоколов, рендеринг реального времени и дизайн языков и рантаймов.

omp² всё ещё строится по этому документу — в состояниях от «уже выкачено» до «ещё обдумывается». Но мы искренне благодарим каждого из вас за то, что вы пробовали omp и делились с нами всеми классными способами его использования — от управления фабрикой софта до просьбы собрать себе приложение камеры на том же самом телефоне.

Вы сформировали omp — и мы ждём от будущего не менее интересного!

Приложение A: баги состояния в официальных примерах

Ссылки на исходники, минимальные отрывки кода и видео с воспроизведением для сбоев из главы про состояние.

1. Чекпойнт очищается до того, как /fork может его использовать: git-checkpoint.ts

исходник: отсутствует долговечное владение чекпойнтом; /fork вызывается в простое, после того как agent_settled уже опустошил единственную мапу рефов стэша.

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

restore; ход пользователя: реконструкция принимает только результаты инструментов, но ходы пользователя — кастомные записи; падение после 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: Elastic Speculative Slots

Статья и полная модель 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)

====