2026-07-30 15:32:06 +08:00
|
|
|
|
# Agent Note: 种子结束日志边界
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
|
|
|
|
|
Status: implemented
|
|
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
[English](2026-07-30-session-end-seed-log-boundary.md) | 中文
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
|
|
|
|
|
## Problem
|
|
|
|
|
|
|
|
|
|
|
|
拥有独立开／闭括号的插件无法区分一个已死的标记和一个存活的标记。`compact/start` … `compact/end` 就是已发布的实例：当接手一份日志、而它最后的压缩事件是一个未配对的 `compact/start` 时，"上一个写入方在压缩中途死掉了"与"此刻正有一次压缩在运行"在存储历史中是逐字节相同的。所有方只能二选一：拒绝压缩一份其实空闲的日志（把会话卡死），或者在一份确实繁忙的日志上继续压缩。
|
|
|
|
|
|
|
|
|
|
|
|
日志中没有任何东西标出继承历史在哪里结束。`session/created`、`session/disposed` 与 `session/flush` 是 cordis 运行时信号，不是日志事件；`agent/session-start` 只发射不落盘。`Session.firstLiveSeq` 本来就精确地持有这个答案——本生命周期第一次自有写入的 seq——但只存在于内存中，因此读取存储字节的消费方看不到它。
|
|
|
|
|
|
|
|
|
|
|
|
崩溃修复既没有填上这个缺口，也不应该去填：`interruptedTurnClosers` 合成轮次、步骤与工具边界，是因为核心拥有那套词汇表，而 `compact/*` 属于压缩 seam。一个会关闭插件括号的核心修复流程，等于把每个插件的括号语义都搬进核心。
|
|
|
|
|
|
|
|
|
|
|
|
## Decision
|
|
|
|
|
|
|
2026-07-31 13:24:30 +08:00
|
|
|
|
`Session` 的构造函数紧接显式传入的构造种子（包括空种子）之后追加仅日志事件 `session/end-seed`，作为带种子会话的第一次实时写入，位置正是 `firstLiveSeq` 指出的 seq。该事件是那个字段的持久投影：`firstLiveSeq` 为持有对象的消费方回答本生命周期的写入从哪里开始，`session/end-seed` 则为只持有存储字节的消费方回答同一问题。它的 payload 为空——位置与 `time` 承载全部含义——并且不是 `SurfaceEventType`，因此不产生消息，也无法扰动派生历史。这个 seq-0 标记把从空日志恢复的会话与真正的全新会话区分开来，从而防止恢复期间应用新会话默认值。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
括号所有方按位置读取它：在 `session/end-seed` 之前的未配对开启标记具有更小的 seq，来自构造种子，并且属于一个已结束的生命周期。核心写入该边界但不从中读取任何内容；每个括号的词汇表仍归其所属插件，因此在没有消费方来塑形之前，核心不会先发布谓词辅助函数。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-30 12:01:45 +08:00
|
|
|
|
选择构造函数，是因为它是每一个带种子会话都必经的唯一收窄处。全部六个入口都会到达它：`agents.resume()`、在已持久化 id 上的配置驱动启动（`restoreOrCreateConfigured`）、`sessions.fork()`、子代理 fork 子会话、`coordinator.adopt()` 的实时前缀路径，以及裸的 `sessions.create(id, {seed})`。在持久化加载时写入的边界会漏掉两条 fork 路径——而一个继承了仍在运行的父会话开放 `compact/start` 的 fork 子会话，恰恰是必须可判定的场景。在 loop 启动时写入的边界会漏掉 `fork()` 与 `adopt()`，并且不得不在 `SessionStartSource: 'startup'` 上触发——那正是 fork 子会话发布的取值，于是该字段将不再具有区分力。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-31 22:48:30 +08:00
|
|
|
|
两条守卫让这个标记保持精确。省略种子时不写入任何内容，因为这是全新会话。种子本身已以该事件结尾时不会重复标记，这让写入具备幂等性。幂等性是承重的，而不是为了整洁：每次绑定到 Agent 的冷会话接手都会经过 `agentFor()`；没有这条守卫，重复的控件操作即使没有执行任何工作，也会让日志增长。只执行检查的 `session.history` 与 `session.fork` 源端路径不会在源会话中创建这条边界。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
|
|
|
|
|
## 持久化无需任何改动
|
|
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
构造函数中的 append 发生在 `enter()` 之前，因此会话尚无 store attachment：该标记不会在 `session/event` 上发布，与它之前的种子事件完全一样。它属于 `initFor` 捕获的那份创建种子，并通过普通的种子路径落盘——`onCreated` 的 `createCore` + `appendCore`，或无主认领的后缀写入。因此监听 firehose 的消费方永远看不到这条边界，必须从日志中读取它。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
fix(session): close the review gaps the boundary opened
- `SessionSummary.updatedAt`'s wire doc still said "Persisted file mtime",
which stopped being true for attached sessions.
- The core invariant let `session/inherited` fall through the merge-extensible
default. It is core-owned, so it gets an explicit case; an unbalanced seed
legally places it inside an open turn, which the relation permits.
- The Agent Note claimed the boundary reaches disk via `live.pending`/
`scheduleDrain`. Verified false: the constructor append precedes `enter()`,
so it never publishes on `session/event` and rides the creation seed instead.
Attaching is therefore a write where none happened before — recorded, since
only `load()` stays a pure read.
- The deferred-index proposal asserted this change documented the cold-mtime
skew on `dsh-host-apiproxy`. It did not; the README entry now exists.
- `firstLiveSeq`'s firehose gap runs through its own seq, not below it.
- The boundary is not always at `firstLiveSeq` (the idempotence guard), so
consumers scan for the last one.
- `lastActivityTime` excludes by type, so a pickup time still leaks onto a
synthetic closer when a boundary ends an open turn. Documented.
- Pin the fork claim end-to-end: a child inherits a still-running parent's
open bracket below its own boundary, while the parent has none. Fails if the
write moves back to the load path.
- Fix the telemetry title that contradicted its own assertions.
The `/status` call site cannot be pinned the way the other two are: the
command appends its own `command/run` before rendering, so the boundary is
never the log tail there. Its fixture now at least renders over a
boundary-bearing log.
2026-07-30 13:59:08 +08:00
|
|
|
|
对 seam 的影响：`load()` 仍是纯读取，没有 revision 递增，对平衡日志不走 `commitRepair`，被拒绝的 `append` 也不留下持久标记。但**接手不是纯读取**——如今一次拾起会在此前完全无写入的路径上产生写入，因此只读存储或磁盘写满会在 `session/created` 处报错，而不是在第一个真实轮次处。这是本放置方式新增的唯一成本，并且比加载路径方案的成本更窄（后者会让加载本身失败）。
|
|
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
若崩溃发生在种子写入到达磁盘之前，边界会丢失，而这没有代价：待处理批次按序写入，所以丢掉一个边界意味着它之后的每个事件也一起丢掉。下一次接手读到的字节与上一次相同，会追加自己的边界，并对括号作出完全相同的判定。进程内消费方应优先使用 `firstLiveSeq`，它在任何写入之前就是精确的。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
|
|
|
|
|
## 保证的适用范围
|
|
|
|
|
|
|
|
|
|
|
|
该谓词对*本*会话继承的括号成立，而不是关于其他写入方的存活信号。一个并发存活的会话可能在同一段存储历史上持有开放括号，而它自己的边界在别处。必须容忍并发写入方的消费方需要日志之外的存活信号，不能仅凭这个事件就省掉它。
|
|
|
|
|
|
|
|
|
|
|
|
## Alternatives considered
|
|
|
|
|
|
|
2026-08-07 22:52:19 +08:00
|
|
|
|
**由持久化协调器的冷加载路径写入边界。** 最初将其实现为 `session/resumed` 边界，并在合并前放弃。它完全覆盖不到 fork，而 fork 恰恰是继承括号的所有方可能仍然存活的那一种情形。由于标记是在加载时铸造的，它还必须在读取路径上做持久写入，这把成本铺开到整个 seam：每次冷加载都递增 revision、对一份无需修复的平衡日志也要走 `commitRepair`、需要一个已存储时间下限来维持钳制的单调性，以及加载在只读存储上会失败。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
**在 loop 启动时追加边界。** loop 调用 `resumeWith`，因此覆盖恢复路径，但完全漏掉 `fork()` 与 `adopt()`，而且事件不得不在 `'startup'` 上触发——那是 fork 子会话发布的来源——于是 `SessionStartSource` 将不再具有区分力。它还会在追加标记之前就发布会话，因此 `session/created` 监听方可能观察到一份没有边界的带种子日志。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
|
|
|
|
|
**复用 `header.seedLength`。** 它是持久的 *fork 血缘*边界，并且刻意在恢复时保留原始 fork 取值——而恢复时构造种子是整份存储日志。这两个事实并不相同，混同会同时失去两者。
|
|
|
|
|
|
|
|
|
|
|
|
**让崩溃修复连同轮次边界一起关闭 `compact/*`。** 否决：这会把每个插件的括号语义搬进核心的修复流程，而核心无法知道关闭另一个包的括号应该记录什么。
|
|
|
|
|
|
|
|
|
|
|
|
## Consequences
|
|
|
|
|
|
|
2026-07-30 12:01:45 +08:00
|
|
|
|
买到的：一条边界，在一处写入，对全部六条带种子启动路径都正确——包括持久化层方案触及不到的 fork 缺口。持久化各包保留纯读取路径。`firstLiveSeq` 获得一个持久孪生体，而不是关于同一边界的第二套彼此竞争的概念。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-31 13:24:30 +08:00
|
|
|
|
代价：带种子会话的日志长了一个事件，空日志恢复也包括在内。seq 期望会随这条边界移动。两处更新是承重的而非机械的：telemetry 的收养测试断言该边界*会*被导出，因为它是本生命周期的自有写入；属性测试套件的回放不变式则是"种子逐字节复现，外加一个仅日志边界"，并把幂等性作为独立属性。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-30 15:32:06 +08:00
|
|
|
|
`session/end-seed` 加入了落盘词汇表。在预发布立场下（`SESSION_FORMAT_VERSION` 固定为 `0`，不作兼容承诺），更旧的日志只是没有它，而没有边界的日志会正确地判定没有任何内容属于构造种子历史。
|
feat(session): project the inherited-history boundary into the log
A plugin owning a standalone open/close bracket cannot tell a dead marker
from a live one: an unmatched `compact/start` reads identically whether the
previous writer died mid-compaction or a compaction is running now.
`Session.firstLiveSeq` already holds that answer exactly, but only in memory.
Append the log-only `session/inherited` event at that seq from the seeded
constructor — the single waist all six seeded-start paths pass through
(resume, configured startup on a persisted id, `sessions.fork()`, a subagent
fork child, `adopt()`'s live prefix, and a bare seeded `create`). Read it
through the new `isInheritedSeq(events, seq)`.
The constructor placement means persistence needs no changes: the marker is
already in `events` when a backend captures the creation seed, so it rides
the ordinary seed path with no load-time write. It also covers fork, where
the inherited bracket's owner may still be running — the case a
persistence-layer boundary could not reach.
Activity ordering excludes the boundary through `lastActivityTime()`, since
lazy resume makes browsing a pickup and the three call sites would otherwise
float every opened session to the top of a picker or list.
2026-07-30 11:38:51 +08:00
|
|
|
|
|
2026-07-30 17:40:25 +08:00
|
|
|
|
[排队手动压缩决策](../feature/2026-07-30-queued-manual-compaction.md)如今提供了第一个消费方。其尾部扫描会分别查找未匹配的 `compact/start` 与最新 end-seed，只把位于该边界之后的 start 视为活动锁，并在同一个回放转换上清除不变量追踪状态。该谓词仍位于压缩包中，不会成为通用核心辅助函数。
|