5.6 KiB
dsh-invariants
Runtime event-contract assertions intended for development diagnostics. This pure-listener plugin checks relationships among session events, agent states, scoped dispatches, and model requests; it does not own or change product behavior.
The plugin has no environment guard: it is active wherever it is registered. The default dsh-agent-core bundle mounts it unconditionally; a custom composition can omit it when the runtime cost is undesirable. It doubles as executable documentation of the event taxonomy — the assertions are the contract.
Session itself owns immutable log storage in every composition: it takes one lossless JSON snapshot of each accepted event, deep-freezes that record, and exposes the log through immutable array snapshots. The invariants plugin checks the cross-record and cross-seam rules that storage immutability cannot express.
Session-log assertions run during Cordis internal/dispatch, while Session.append() is resolving the session/event callback snapshot but before it pushes the candidate into the log. A valid transition is staged by exact event identity and applied to the live trace only when that same committed event reaches the plugin's contained post-commit listener. A later internal dispatch check can therefore veto without advancing either the log or the invariant trace, while ordinary session/event observer failures remain observe-only.
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)
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 does not falsely reject the next event. The oracle listeners are explicitly global so pre-commit staging and post-commit application keep the same audience even if the plugin is mounted under a scoped context; their cleanup still belongs to that mounting fiber. The plugin has no configuration.
Invariants asserted
Session log (per session):
seqstrictly increases — the spine of replay equivalence.- turns pair and nest —
turn/startopens a turn,turn/endcloses the matching one; no overlapping turns. - steps nest in turns —
step/startopens a step in the open turn;step/endcloses the matching step. - chunks belong to an open step —
step/startprecedes itsassistant/chunks. - a
tool/resultneeds a priortool/call— but NOT the converse: atool/callmay have no result (a thrown tool-execution pipeline step ends the turn with notool/result, which is legal).
Agent status (per agent):
- legal transitions only —
idle↔runningand(idle|running)→disposed. A no-op transition (setStatusdedups, so it never fires) and leaving the terminaldisposedstate 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 frozenmessagesdeep-equal to the derivation over the log prefix strictly before the in-flight step'sstep/start(rebuilt through a FRESHSession, so the live cache cannot vouch for itself — and boundary-correct: content logged afterstep/startlegitimately belongs to the next request), and every non-content field must equal the latest loggedrequest/header(see the reconstructability RFC). Registered withprepend: trueso a short-circuitingllm/streamlistener (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 assertions remain useful
Session enforces the per-record storage boundary at runtime, where a cast cannot bypass it. Pervasive DeepReadonly<SessionEvent> types would add noise across consumers without expressing relationships such as turn/step nesting, subject-correct scoped dispatch, or equality between a request and its log reconstruction. This plugin checks those relationships wherever it is mounted while dsh-session keeps history immutable in every composition. See source-owned session immutability and dev-mode invariants.
Seeded sessions
A seeded or forked session arrives with events already in its log because construction does not emit session/event for each seed record. Session validates, snapshots, and freezes every seed record before accepting it; on session/created, this plugin replays the accepted log only to rebuild and check its relational trace state.
Model Experience
None, as this observer only validates events and frozen requests and never rewrites prompts, schemas, messages, or streams.
Known Limitations and Deferred Work
- The request-reconstructability assertion covers loop-built requests only — hand-built one-shots (e.g. compaction's summarize call) carry no live
sessionIdmarker and are skipped. - Merge-extended event families get no family-specific assertions —
compact/*lock pairing andhook/*invoked/result pairing are not checked here; only the core turn/step/chunk/tool-result contract is.