fix(invariants): harden runtime contracts and gates
This commit is contained in:
@@ -12,7 +12,7 @@ The reference shape for the happy path is MiniCode's `LLMClient`: a stateful con
|
||||
|
||||
### The principle
|
||||
|
||||
**Model-visible ⟺ logged.** Anything that reaches a model request must be recorded in the session log. The checkable consequence: **every conversation request the loop sends is a pure function of the session log** — anyone holding the log reconstructs it byte-for-byte. Scope, stated precisely: the guarantee covers the loop-built `GenerateOptions`; provider wire bytes follow from it because both adapters' serialization is a pure per-message function at a pinned code version; direct one-shots (compaction's summarize call) log their envelope scalars (`compact/summary.{provider, model, maxTokens}`) and their input is deterministic code over the logged region — reconstructable from log + code, outside the invariant by the unfrozen-request marker.
|
||||
**Model-visible ⟺ logged.** Anything that reaches a model request must be recorded in the session log. The checkable consequence: **every conversation request the loop sends is a pure function of the session log** — anyone holding the log reconstructs it byte-for-byte. Scope, stated precisely: the guarantee covers the loop-built `GenerateOptions`; provider wire bytes follow from it because both adapters' serialization is a pure per-message function at a pinned code version; direct one-shots (compaction's summarize call) log their envelope scalars (`compact/summary.{provider, model, maxTokens}`) and their input is deterministic code over the logged region — reconstructable from log + code, outside the invariant because only the loop marks request ownership.
|
||||
|
||||
Prefix-cache stability is corollary #1, not the headline: an append-only log projected by a per-node pure function yields requests that are append-extensions of their predecessors whenever the header is unchanged — stability is emergent, not managed. Byte-exact audit/replay is corollary #2; resume and fork with *attributable* drift is corollary #3.
|
||||
|
||||
@@ -26,7 +26,7 @@ Each step rebuilds prompt assembly. On the instance's first step, `agent/session
|
||||
|
||||
**`step/start` is the reconstruction boundary.** A step derives messages from events before that sequence. Injection after the snapshot joins the next request, and reentrant appends are rejected during event publication. `agent/pre-step(agent, turn, step, signal)` remains the generic seam for content needed by the current request. Header reconstruction selects the step's `request/header`, or carries the prior snapshot when no new header is written.
|
||||
|
||||
**Enforcement.** The `dsh-agent-loop/invariant` companion registers with `ctx.invariants` and, when selected, independently rebuilds each loop request through a fresh `Session`, so the live cache cannot vouch for itself, then compares messages and folded header fields at `llm/stream`. Loop requests are identified by their frozen shape and session id; direct one-shots are excluded. Correctness depends on sequence-bounded reconstruction rather than listener order. A with-key e2e requires positive cache-read tokens after the first request; per-step usage is the production signal, and a header change or compaction appears as a cache-read drop on the next step.
|
||||
**Enforcement.** The `dsh-agent-loop/invariant` companion registers with `ctx.invariants` and, when selected, independently rebuilds each loop request through a fresh `Session`, so the live cache cannot vouch for itself, then compares messages and folded header fields at `llm/stream`. The loop applies an internal non-enumerable identity before freezing each request; the independently built companion recognizes that identity, while direct one-shots remain excluded regardless of their frozen shape or session id. Correctness depends on sequence-bounded reconstruction rather than listener order. A with-key e2e requires positive cache-read tokens after the first request; per-step usage is the production signal, and a header change or compaction appears as a cache-read drop on the next step.
|
||||
|
||||
### The MiniCode shape: adopted, with the provenance arrow inverted
|
||||
|
||||
|
||||
@@ -2,5 +2,5 @@
|
||||
# side as of the last confirmed-consistent state. Both languages carry equal authority;
|
||||
# after editing either side, bring the other along and re-record with:
|
||||
# pnpm run verify-translation-pairing --write
|
||||
2026-07-19-package-invariant-runtime-contracts.md: 84c632e57b3360756660415d7bdd62397c52e4a3
|
||||
2026-07-19-package-invariant-runtime-contracts.zh.md: 51734f6922f393ae37b0c3999723b7aade7651eb
|
||||
2026-07-19-package-invariant-runtime-contracts.md: ab4301a80b01ac2b4b2870f02c232ab321a6fab1
|
||||
2026-07-19-package-invariant-runtime-contracts.zh.md: 2e0816b2f381fd8fa51df51d8c482d6d4adf48b4
|
||||
|
||||
@@ -34,9 +34,9 @@ The current 94-package workspace has 19 executable companions and 75 justified e
|
||||
| `dsh-session` | Strict sequence growth, turn/step enclosure, and same-step tool call/result pairing. |
|
||||
| `dsh-agent` | Non-repeating agent status and terminal disposal transitions. |
|
||||
| `dsh-scope` | Scoped-event carrier presence and routed-subject consistency. |
|
||||
| `dsh-agent-loop` | Frozen loop request reconstruction from the session event log. |
|
||||
| `dsh-agent-loop` | Explicitly marked, frozen loop request reconstruction from the session event log. |
|
||||
| `dsh-llm` | Stream block grammar, delta type/index matching, single usage, closed blocks, and terminal finish. |
|
||||
| `dsh-llm-retry` | Durable retry records identify the open turn's latest closed step, remain unique per step, increase monotonically, and stay within retry and timer bounds. |
|
||||
| `dsh-llm-retry` | Durable retry records identify the open turn's latest closed step, remain unique per step, increase monotonically, and stay within retry and non-negative timer bounds. |
|
||||
| `dsh-tools` | Monotonic pre/execute/post stages and immutable final execution/result snapshots. |
|
||||
| `dsh-system-prompt` | Authoritative assembly section, tool, and variable data constraints. |
|
||||
| `dsh-compact` | Compaction start/summary/end pairing, range endpoints, token counts, and successful-summary presence. |
|
||||
@@ -49,15 +49,15 @@ The current 94-package workspace has 19 executable companions and 75 justified e
|
||||
| `dsh-workflow` | Workflow and child-agent start/end events preserve run metadata, identity, outcome, count, and error relations. |
|
||||
| `dsh-tasks` | Current and terminal task snapshots preserve id/kind, owner, status, and timestamp relationships. |
|
||||
| `dsh-tool-todo` | Durable whole-list snapshots use unique trimmed items, closed statuses, and at most one active item. |
|
||||
| `dsh-time-context` | Plugin-attributed clock readings agree with the session's open turn and next pre-step position, elapsed baseline, rendered time, and event time. |
|
||||
| `dsh-time-context` | Plugin-attributed clock readings agree with the session's open turn, next pre-step position, and elapsed baseline; rendered time parses and does not postdate its event. |
|
||||
|
||||
Session-backed companions reconstruct their trace from existing durable events when they load. Other checks observe the authoritative live event boundary or mutable service result. Validation runs before publication where accepting an invalid event would otherwise commit bad state.
|
||||
|
||||
### Repository gate and tests
|
||||
|
||||
`verify-package-invariants` discovers every workspace package and enforces companion source, exact-name registration, `./invariant` exports, publication files, dependencies, TypeScript references, and bundle entries. Its AST rule rejects generated markers and unexplained empty installers. A non-empty installer must accept and use the failure reporter, and registration must pass that checked local `install` function. The gate deliberately does not infer semantic quality from method names or helper calls.
|
||||
`verify-package-invariants` discovers every workspace package and enforces companion source, exact-name registration, named-only Loader shape, `./invariant` exports, publication files, dependencies, TypeScript references, and bundle entries. Its AST rule rejects generated markers, default exports, and unexplained empty installers. A non-empty installer must accept and use the failure reporter, and registration must pass that checked local `install` function. The gate deliberately does not infer semantic quality from method names or helper calls.
|
||||
|
||||
Vitest mounts `InvariantService` with `{ enabled: true }` for every package test topology and loads the owning companion. The invariant subpath path mapping resolves source companions instead of stale built output. Focused suites cover every executable companion's valid and invalid observations, and the exhaustive topology loads all companions to prove registration and disposal wiring. Tests that synthesize event streams must produce a valid surrounding lifecycle unless the test is intentionally asserting a violation.
|
||||
Vitest mounts `InvariantService` with `{ enabled: true }` for every package test topology and loads the owning companion. The invariant subpath path mapping resolves source companions instead of stale built output. Focused suites cover every executable companion's valid and invalid observations, and the exhaustive topology runs every source companion through the real Loader namespace normalization. An artifact gate imports every compiled `./invariant` self-reference under plain Node and repeats that Loader-shape check. Tests that synthesize event streams must produce a valid surrounding lifecycle unless the test is intentionally asserting a violation.
|
||||
|
||||
## Alternatives considered
|
||||
|
||||
|
||||
@@ -34,9 +34,9 @@ Status: implemented
|
||||
| `dsh-session` | 序号严格递增、turn/step 包围关系,以及同一 step 内的工具调用/结果配对。 |
|
||||
| `dsh-agent` | agent 状态不得重复,并且不能离开终态 disposed。 |
|
||||
| `dsh-scope` | scoped event 必须携带 carrier,且路由 subject 保持一致。 |
|
||||
| `dsh-agent-loop` | 从 session 事件日志重建冻结的 loop 请求。 |
|
||||
| `dsh-agent-loop` | 从 session 事件日志重建带显式标记的冻结 loop 请求。 |
|
||||
| `dsh-llm` | stream block 文法、delta 类型/索引匹配、单次 usage、block 闭合和终止 finish。 |
|
||||
| `dsh-llm-retry` | 持久化重试记录指向当前打开 turn 中最近关闭的 step;每个 step 的记录保持唯一,重试次数单调递增,并且重试次数和定时器延迟均保持在边界内。 |
|
||||
| `dsh-llm-retry` | 持久化重试记录指向当前打开 turn 中最近关闭的 step;每个 step 的记录保持唯一,重试次数单调递增,并且重试次数和非负的定时器延迟均保持在边界内。 |
|
||||
| `dsh-tools` | pre/execute/post 阶段单调推进,以及最终 execution/result 快照不可变。 |
|
||||
| `dsh-system-prompt` | 权威 assembly 中 section、tool 和 variable 的数据约束。 |
|
||||
| `dsh-compact` | compaction start/summary/end 配对、范围端点、token 数量和成功时必须存在 summary。 |
|
||||
@@ -49,15 +49,15 @@ Status: implemented
|
||||
| `dsh-workflow` | workflow 和 child-agent start/end 事件保持 run metadata、身份、outcome、数量和 error 关系。 |
|
||||
| `dsh-tasks` | 当前与终态 task snapshot 保持 id/kind、owner、status 和 timestamp 关系。 |
|
||||
| `dsh-tool-todo` | 持久化全量 snapshot 使用唯一且已 trim 的条目、封闭 status,并且最多有一个活动条目。 |
|
||||
| `dsh-time-context` | 标注插件来源的时钟 reading 必须匹配 session 当前打开的 turn 和下一个 step 开始前的位置,并在 elapsed baseline、渲染时间和事件时间之间保持一致。 |
|
||||
| `dsh-time-context` | 标注插件来源的时钟 reading 必须匹配 session 当前打开的 turn、下一个 step 开始前的位置和 elapsed baseline;渲染时间必须可解析,且不得晚于对应事件。 |
|
||||
|
||||
基于 session 的 companion 在加载时从已有持久化事件重建 trace。其他检查观测权威 live event 边界或可变服务结果。如果接受无效事件会提交错误状态,验证就在发布前执行。
|
||||
|
||||
### 仓库门禁与测试
|
||||
|
||||
`verify-package-invariants` 发现每个 workspace 包,并强制 companion 源文件、完整名称注册、`./invariant` export、发布文件、依赖、TypeScript reference 和 bundle entry 完整。其 AST 规则拒绝生成标记和没有解释的空安装器。非空安装器必须接收并使用失败报告器,注册时还必须传入该经检查的本地 `install` 函数。门禁不会通过方法名或 helper 调用推断语义质量。
|
||||
`verify-package-invariants` 发现每个 workspace 包,并强制 companion 源文件、完整名称注册、仅含具名 export 的 Loader 形状、`./invariant` export、发布文件、依赖、TypeScript reference 和 bundle entry 完整。其 AST 规则拒绝生成标记、默认导出和没有解释的空安装器。非空安装器必须接收并使用失败报告器,注册时还必须传入该经检查的本地 `install` 函数。门禁不会通过方法名或 helper 调用推断语义质量。
|
||||
|
||||
Vitest 为每个包测试拓扑使用 `{ enabled: true }` 挂载 `InvariantService`,并加载所有者 companion。不变量 subpath 的 path mapping 会解析源 companion,而不是陈旧的构建输出。聚焦 suite 覆盖每个可执行 companion 的有效和无效观测;穷举拓扑加载全部 companion,以证明注册和释放 wiring。合成事件流的测试必须构造有效的外围生命周期,除非测试本身就是在断言违规。
|
||||
Vitest 为每个包测试拓扑使用 `{ enabled: true }` 挂载 `InvariantService`,并加载所有者 companion。不变量 subpath 的 path mapping 会解析源 companion,而不是陈旧的构建输出。聚焦 suite 覆盖每个可执行 companion 的有效和无效观测;穷举拓扑通过真实 Loader 命名空间归一化运行每个源 companion。产物门禁在 plain Node 下导入每个已编译的 `./invariant` 自引用,并重复执行该 Loader 形状检查。合成事件流的测试必须构造有效的外围生命周期,除非测试本身就是在断言违规。
|
||||
|
||||
## 考虑过的替代方案
|
||||
|
||||
|
||||
Reference in New Issue
Block a user