Files
deepseek-harness/packages/support/invariants
Tianyi Cui 65d644b161 invariants: a loop-built request must be exactly what the log reconstructs
The dev-mode cross-check on llm/stream: a frozen request with a live
sessionId (the loop-built marker; hand-built one-shots stay unfrozen
and skipped) must carry messages deep-equal to the derivation over the
log prefix strictly before the in-flight step's step/start, and header
fields equal to the fold of the log's request/header* events. The
messages side rebuilds through a FRESH Session over the boundary
prefix — same projection code, zero shared state — so the live cache
cannot vouch for itself, and the seq-bounded rebuild is boundary-
correct: content appended after step/start (an agent/request-window
inject) legitimately belongs to the next request and cannot false-fire
the check. prepend:true only defends against the replay adapter's
short-circuit (append-registered); correctness never rests on listener
ordering. There is no divergence-allowance caveat: nothing can shape
request content outside the log.
2026-07-06 03:14:07 +08:00
..

dsh-invariants

Dev-mode event-contract invariants and session-log freeze. A pure-listener plugin (everything is a plugin) that asserts the harness event contract at runtime and, optionally, freezes logged session-event data so any code that mutates history throws instead of corrupting silently.

Off in production. Enable it in tests and the demos, where a contract violation should fail loudly. It costs nothing when not registered, and doubles as executable documentation of the event taxonomy — the assertions are the contract.

Plugin

A functional plugin — register the module namespace (this is what loading by name in cordis.yml does):

import type { Context } from 'cordis'
import * as Invariants from '@deepseek-ai/dsh-invariants'

declare const ctx: Context

await ctx.plugin(Invariants)                     // freeze on (default)
await ctx.plugin(Invariants, { freeze: false })  // assert contract, don't freeze

inject: ['sessions'] — it reads ctx.sessions.list() at apply time to rebuild trace state for sessions that already exist (so a hot reload mid-turn doesn't falsely reject the next event). It listens on session/created, session/event, and agent/status.

Config

Key Default Meaning
freeze true Deep-freeze each logged event's data so mutating a logged event throws. Set false to assert the contract without freezing.

Invariants asserted

Session log (per session):

  • seq strictly increases — the spine of replay equivalence.
  • turns pair and nestturn/start opens a turn, turn/end closes the matching one; no overlapping turns.
  • steps nest in turnsstep/start opens a step in the open turn; step/end closes the matching step.
  • chunks belong to an open stepstep/start precedes its assistant/chunks.
  • a tool/result needs a prior tool/call — but NOT the converse: a tool/call may have no result (a thrown tool-execution pipeline step ends the turn with no tool/result, which is legal).

Agent status (per agent):

  • legal transitions onlyidle↔running and (idle|running)→disposed. A no-op transition (setStatus dedups, so it never fires) and leaving the terminal disposed state are violations.

Model requests (on llm/stream):

  • a loop-built request is exactly what the log reconstructs — a frozen request with a live sessionId (the loop-built marker; hand-built one-shots like compaction's summarize are unfrozen and skipped) must carry frozen messages deep-equal to the derivation over the log prefix strictly before the in-flight step's step/start (rebuilt through a FRESH Session, so the live cache cannot vouch for itself — and boundary-correct: content logged after step/start legitimately belongs to the next request), and every non-content field must equal the fold of the log's request/header* events (see the reconstructability RFC). Registered with prepend: true so a short-circuiting llm/stream listener (the replay adapter) cannot silence it; prepend orders it against append-registered listeners only — correctness rests on the seq-bounded rebuild, never listener timing.

On any violation it throws InvariantError (code: 'INVARIANT').

Why runtime, not deep-readonly types

A DeepReadonly<SessionEvent> is high type-noise across every log consumer, and a plugin can cast straight through it. A dev-mode freeze plus these assertions catch real corruption at zero production cost and zero type noise. The always-on half of that defense — cloning derived messages so request/adapter mutation can't reach back into the log — lives in dsh-session's deriveMessages. This package is the dev-mode tripwire. See dev-mode invariants.

Seeded sessions

A seeded/forked session arrives with events already in its log (the Session constructor copies the seed without emitting session/event). On session/created the plugin replays the existing log through the checker and freezes those entries, so seeded history is held to the same contract.