[{"k":"h","depth":1,"text":"17 · Trace","id":"17--trace"},{"k":"quote","inline":[{"k":"text","text":"Every run leaves a journal · one NDJSON file, one event per line, each\nline chained to the last by hash. The trace is the run's flight\nrecorder ("},{"k":"code","text":"nika trace show|replay|verify"},{"k":"text","text":"), the resume substrate, and\nthe stream the receipt folds FROM ("},{"k":"link","text":"15","href":"./15-proof.md"},{"k":"text","text":"). This chapter\nmakes the dialect NORMATIVE: "},{"k":"code","text":"trace_format: 2"},{"k":"text","text":", the frame grammar, the\nchain law, the kind vocabulary, and the permit-decision witness\n(NEP-0007) · the trace stops being an engine-private dialect. What is\nwritten here is the OBSERVED wire, grave-not-invented: the conformance\ngolden is a real run's journal, byte-verifiable."}]},{"k":"hr"},{"k":"h","depth":2,"text":"The journal (normative)","id":"the-journal-normative"},{"k":"p","inline":[{"k":"text","text":"One run → at most one journal file · "},{"k":"code","text":"<trace-dir>/<ISO-compact>-<short -id>.ndjson"},{"k":"text","text":" (production: "},{"k":"code","text":".nika/traces/"},{"k":"text","text":"). Three laws shape it:"}]},{"k":"list","ordered":false,"items":[[{"k":"strong","text":"Lazy open"},{"k":"text","text":" · file creation waits for the FIRST emitted frame (a run\nrefused before its prologue · audit refusal · composition failure ·\nleaves no file)."}],[{"k":"strong","text":"Infallible rider"},{"k":"text","text":" · journal I/O failure never changes the run's\nverdict or its primary output; the error surfaces AFTER the run as a\nnote. The journal tees BESIDE the chosen primary lane, byte-identical\nwith or without it."}],[{"k":"strong","text":"Append-only"},{"k":"text","text":" · frames are written in emission order and never\nrewritten; the chain (below) makes any rewrite evident."}]]},{"k":"h","depth":2,"text":"The frame (normative)","id":"the-frame-normative"},{"k":"p","inline":[{"k":"text","text":"One event per line · one JSON object · the member set:"}]},{"k":"list","ordered":false,"items":[[{"k":"text","text":"Key · Type · Meaning"}],[{"k":"text","text":"`chain` · string · sha256 hex of the PREVIOUS line's exact bytes (the chain law below)"}],[{"k":"text","text":"`id` · object · `{ \"uuid\": \"<UUIDv7>\" }` · unique per frame · time-ordered"}],[{"k":"text","text":"`timestamp` · integer · unix epoch **nanoseconds**"}],[{"k":"text","text":"`kind` · string · the closed-per-minor kind vocabulary (below)"}],[{"k":"text","text":"`fields` · array · ordered `{ \"key\": string, \"value\": any }` pairs · the frame's payload"}],[{"k":"text","text":"`run` · string | null · the run correlation id when one is set"}],[{"k":"text","text":"`correlation` · string | null · causal correlation across runs when one is set"}]]},{"k":"p","inline":[{"k":"text","text":"Field VALUES are JSON values (string · number · object-as-string when a\npayload is itself serialized · the observed "},{"k":"code","text":"permits_json"},{"k":"text","text":" and "},{"k":"code","text":"outcome"},{"k":"text","text":"\ncarry serialized JSON as a string, so the frame grammar stays flat).\nSensitive payloads are hashed by the emitter, never carried raw.\n"},{"k":"strong","text":"Additive law"},{"k":"text","text":" · a reader MUST ignore an unknown member and an unknown\n"},{"k":"code","text":"fields"},{"k":"text","text":" key (report « unrecorded », never guess); an unknown "},{"k":"code","text":"kind"},{"k":"text","text":" is\ntolerated by verifiers (the walk continues · the chain still binds it)."}]},{"k":"h","depth":2,"text":"The chain (normative)","id":"the-chain-normative"},{"k":"p","inline":[{"k":"text","text":"The first line's "},{"k":"code","text":"chain"},{"k":"text","text":" is the sha256 of the GENESIS tag; every later\nline's "},{"k":"code","text":"chain"},{"k":"text","text":" is the sha256 hex of the previous line's EXACT bytes.\nAfter the run, the last line's hash is the journal's HEAD · printed at\nrun end and carried by the seal. Verification recomputes the walk:\nany byte edit, insertion, deletion, or reorder breaks every subsequent\nlink ("},{"k":"code","text":"nika trace verify"},{"k":"text","text":" · FORGED). The chain proves INTEGRITY of the\nsequence; it does not prove authorship (the seal and anchor rails of\n"},{"k":"link","text":"15","href":"./15-proof.md"},{"k":"text","text":" carry authenticity)."}]},{"k":"h","depth":2,"text":"`trace_format: 2` (normative · the version)","id":"trace_format-2-normative--the-version"},{"k":"p","inline":[{"k":"text","text":"The dialect version rides the FIRST frame (the prologue's\n"},{"k":"code","text":"trace_format"},{"k":"text","text":" field). It versions the JOURNAL WIRE · orthogonal to\nthe language (v1 · never typed in the file · "},{"k":"link","text":"01 §nika","href":"./01-envelope.md"},{"k":"text","text":"),\n"},{"k":"code","text":"receipt_format: 1"},{"k":"text","text":" (the folded receipt) and\n"},{"k":"code","text":"graph_format: 3"},{"k":"text","text":" (the projection). Version 2 is THIS chapter. A wire\nchange that breaks a version-2 reader MUST bump it; additive fields and\nadditive kinds MUST NOT."}]},{"k":"h","depth":2,"text":"The prologue (normative · `workflow_started`)","id":"the-prologue-normative--workflow_started"},{"k":"p","inline":[{"k":"text","text":"The first frame is "},{"k":"code","text":"workflow_started"},{"k":"text","text":", and it is the run's MANIFEST.\nVersion-2 fields (the observed set):"}]},{"k":"list","ordered":false,"items":[[{"k":"text","text":"Field · Meaning"}],[{"k":"text","text":"`workflow` · the workflow id"}],[{"k":"text","text":"`permits` · the boundary posture, human-readable (`declared boundary · default-deny` | the zero-authority note)"}],[{"k":"text","text":"`permits_json` · the DECLARED `permits:` block, serialized verbatim · the boundary the run was judged under"}],[{"k":"text","text":"`workflow_sha256` / `workflow_sha256_lf` · the source bytes' digest (raw · LF-normalized)"}],[{"k":"text","text":"`semantic_hash` · the semantic identity ([15](./15-proof.md) · H(domain ‖ version ‖ JCS(IR)))"}],[{"k":"text","text":"`sandbox` · the OS-confinement backend the run selected (`seatbelt` · `landlock` · `noop`, loudly)"}],[{"k":"text","text":"`trace_format` · this dialect's version · `2`"}],[{"k":"text","text":"`engine_version` · the emitting engine"}],[{"k":"text","text":"`platform` · `os/arch`"}]]},{"k":"p","inline":[{"k":"text","text":"An engine MAY add fields (additive law); it MUST NOT drop these."}]},{"k":"p","inline":[{"k":"strong","text":"The prologue is the run's BOOT MANIFEST"},{"k":"text","text":" (normative) · beyond the\nidentity above it names the CONTRACT the run booted under, so the\njournal self-describes what it ran by rather than leaving a reader to\ninfer it ·"}]},{"k":"list","ordered":false,"items":[[{"k":"text","text":"Field · Meaning"}],[{"k":"text","text":"`spec_pin` · the spec commit this engine's conformance was proven at"}],[{"k":"text","text":"`stamper_kind` · the event-identity seam the `run:` declaration resolved to · `deterministic` | `system`"}],[{"k":"text","text":"`clock` · the resolved run clock ([01](./01-envelope.md) §`run`) · `virtual` | `system`"}],[{"k":"text","text":"`seed` · present exactly under a determinism demand (`seeded: N` → `N` · `none` → the zero stream); an ambient run carries **no** seed claim"}]]},{"k":"p","inline":[{"k":"strong","text":"A manifest claims only what exists."},{"k":"text","text":" Where a fact has no recording\nsurface the field is ABSENT and a reader says « unrecorded » — never a\nguessed value, never a fabricated zero. Absence is the honest claim,\nand the additive law above already makes it readable by older readers."}]},{"k":"h","depth":2,"text":"The kind vocabulary (normative · closed per minor)","id":"the-kind-vocabulary-normative--closed-per-minor"},{"k":"p","inline":[{"k":"text","text":"Version 2 names exactly these kinds · additive per minor, never\nre-meant:"}]},{"k":"p","inline":[{"k":"code","text":"workflow_started"},{"k":"text","text":" · "},{"k":"code","text":"workflow_completed"},{"k":"text","text":" · "},{"k":"code","text":"workflow_failed"},{"k":"text","text":" ·\n"},{"k":"code","text":"workflow_cancelled"},{"k":"text","text":" · "},{"k":"code","text":"workflow_paused"},{"k":"text","text":" · "},{"k":"code","text":"task_scheduled"},{"k":"text","text":" ·\n"},{"k":"code","text":"task_started"},{"k":"text","text":" · "},{"k":"code","text":"task_completed"},{"k":"text","text":" · "},{"k":"code","text":"task_failed"},{"k":"text","text":" · "},{"k":"code","text":"task_skipped"},{"k":"text","text":" ·\n"},{"k":"code","text":"task_retrying"},{"k":"text","text":" · "},{"k":"code","text":"task_recovered"},{"k":"text","text":" · "},{"k":"code","text":"task_cancelled"},{"k":"text","text":" ·\n"},{"k":"code","text":"task_cache_hit"},{"k":"text","text":" · "},{"k":"code","text":"verb_invoked"},{"k":"text","text":" · "},{"k":"code","text":"tool_invoked"},{"k":"text","text":" ·\n"},{"k":"code","text":"checkpoint_written"},{"k":"text","text":" · "},{"k":"code","text":"cost_incurred"},{"k":"text","text":" · "},{"k":"code","text":"infer_chunk"},{"k":"text","text":" ·\n"},{"k":"code","text":"permit_checked"},{"k":"text","text":" · "},{"k":"code","text":"lift"},{"k":"text","text":" · "},{"k":"code","text":"run_sealed"},{"k":"text","text":" ·\n"},{"k":"code","text":"agent_tools_selected"},{"k":"text","text":" · "},{"k":"code","text":"agent_nudge"},{"k":"text","text":" · "},{"k":"code","text":"agent_stalled"},{"k":"text","text":" ·\n"},{"k":"code","text":"agent_compose_checked"},{"k":"text","text":" · "},{"k":"code","text":"agent_budget_checkpoint"}]},{"k":"p","inline":[{"k":"text","text":"Per-task terminal frames carry the task's witness fields (the observed\n"},{"k":"code","text":"task_completed"},{"k":"text","text":": "},{"k":"code","text":"task"},{"k":"text","text":" · "},{"k":"code","text":"note"},{"k":"text","text":" · "},{"k":"code","text":"duration_ms"},{"k":"text","text":" · "},{"k":"code","text":"def_hash"},{"k":"text","text":" ·\n"},{"k":"code","text":"input_hash"},{"k":"text","text":" · "},{"k":"code","text":"output"},{"k":"text","text":" · "},{"k":"code","text":"outcome"},{"k":"text","text":" · the outcome record serialized)."}]},{"k":"h","depth":2,"text":"The permit witness (normative · REQUIRED · NEP-0007)","id":"the-permit-witness-normative--required--nep-0007"},{"k":"p","inline":[{"k":"text","text":"Every permit decision taken at the dispatch boundary is a\n"},{"k":"code","text":"permit_checked"},{"k":"text","text":" frame · granted AND refused alike: the exec program\ngate, the tool grant, the taint re-gate ("},{"k":"link","text":"10","href":"./10-authority.md"},{"k":"text","text":" ·\nNEP-0004), the environment composition (NEP-0005 · the passed names),\nand the data-as-code sink (NEP-0006). The per-operation fs/net\nenforcement decisions live inside the builtin sinks (their refusals\nsurface as typed task failures; their allow-side witness is the\ndeclared v1 residual · NEP-0007 law 2). The frame's fields name the "},{"k":"code","text":"gate"},{"k":"text","text":" (the\nbound consulted), the "},{"k":"code","text":"decision"},{"k":"text","text":" ("},{"k":"code","text":"allow"},{"k":"text","text":" "},{"k":"text","text":"|"},{"k":"text","text":" "},{"k":"code","text":"deny"},{"k":"text","text":"), the "},{"k":"code","text":"why"},{"k":"text","text":" (the\nlaw applied), and the "},{"k":"code","text":"task"},{"k":"text","text":". This is a CONFORMANCE requirement on the\nENGINE, not a wire bump: the frame grammar is unchanged (one more kind\nin the stream), so "},{"k":"code","text":"trace_format"},{"k":"text","text":" stays 2. A journal from an OLDER\nconformant engine simply lacks the frames: "},{"k":"code","text":"nika trace verify"},{"k":"text","text":" reports\na run that exercised effects with zero permit-decision frames as a\nFINDING (the witness is absent · the journal is old or the engine is\nnot NEP-0007-conformant) · never FORGED (the chain still holds), never\na crash."}]},{"k":"p","inline":[{"k":"text","text":"The witness is what makes invariant 4 · judged = executed = attested ·\nCHECKABLE: the static judge's verdicts, the runtime's decisions, and\nthe journal's frames speak the same boundary, and the conformance\ndifferential replays the same inputs through checker and engine and\nFAILS on any verdict divergence."}]},{"k":"h","depth":2,"text":"The end of the run (normative · the teardown seal and `incomplete`)","id":"the-end-of-the-run-normative--the-teardown-seal-and-incomplete"},{"k":"p","inline":[{"k":"text","text":"The chain proves the sequence; the run's END is a separate claim, and\nit has three parts."}]},{"k":"p","inline":[{"k":"strong","text":"1 · The seal binds the teardown."},{"k":"text","text":" A "},{"k":"code","text":"run_sealed"},{"k":"text","text":" frame's "},{"k":"code","text":"covers"},{"k":"text","text":"\nobject carries the classic four — the chain "},{"k":"code","text":"head"},{"k":"text","text":", the frame "},{"k":"code","text":"events"},{"k":"text","text":"\ncount, the "},{"k":"code","text":"workflow"},{"k":"text","text":" hash, the "},{"k":"code","text":"engine"},{"k":"text","text":" — and extends "},{"k":"strong","text":"additively"},{"k":"text","text":"\nwith the teardown facts: "},{"k":"code","text":"receipt_digest"},{"k":"text","text":" (the receipt folded at the\nseal instant, over this seal's own pre-seal chain facts), "},{"k":"code","text":"budgets"},{"k":"text","text":"\n(the consumed ρ, present only when metered — never a fabricated zero),\nand "},{"k":"code","text":"effects"},{"k":"text","text":" (the exercised ε beside the declared bound). A seal\nwithout teardown facts stays "},{"k":"strong","text":"byte-identical"},{"k":"text","text":" to the classic\nfour-field form and verifies exactly as before; a seal that carries\nthem binds them under the same signature. One signature surface, not a\nsecond artifact."}]},{"k":"p","inline":[{"k":"text","text":"A failed run owes the same seal an "},{"k":"strong","text":"attested quarantine"},{"k":"text","text":": when it\ndies after producing partly-written outputs, the teardown names those\nartifacts and marks them quarantined, and a quarantined artifact\nre-entering as a later run's input is a finding. v1 owes the NAMING and\nthe CONTAINMENT — not the undoing. Compensating actions across services\nare a different problem and stay out; what a half-written file must\nnever do is pass for a whole one."}]},{"k":"p","inline":[{"k":"strong","text":"2 · A journal with no terminal frame is `incomplete`."},{"k":"text","text":" A chain walk\nthat reaches no lifecycle-terminal frame ("},{"k":"code","text":"workflow_completed"},{"k":"text","text":" ·\n"},{"k":"code","text":"workflow_failed"},{"k":"text","text":" · "},{"k":"code","text":"workflow_cancelled"},{"k":"text","text":" · "},{"k":"code","text":"workflow_paused"},{"k":"text","text":" ·\n"},{"k":"code","text":"run_sealed"},{"k":"text","text":") classifies the journal "},{"k":"strong","text":"`incomplete`"},{"k":"text","text":" — and that\nclassification is the READER's, never a frame the dying process emits.\nA process killed mid-flight cannot attest its own death: any protocol\nthat asks it to is vacuous exactly when it matters, so the verifier —\nthe only party guaranteed to exist at reading time — carries the name."}]},{"k":"p","inline":[{"k":"code","text":"incomplete"},{"k":"text","text":" is "},{"k":"strong","text":"never"},{"k":"text","text":" success and "},{"k":"strong","text":"never"},{"k":"text","text":" silently equal to\nfailure or to forgery: the chain still binds, so the journal is\nhonestly what it is — a run whose end is unknown. Before it had a\nname, « no verdict » was routinely read as « fine »."}]},{"k":"p","inline":[{"k":"strong","text":"3 · Judged ≠ booted is a refusal."},{"k":"text","text":" A check report stamped with the\nsemantic hash of the workflow it judged must match the workflow the run\nis booting. On mismatch the run REFUSES "},{"k":"strong","text":"before its first frame"},{"k":"text","text":" —\nzero events, no file (the lazy-open law above) — rather than producing\na journal a reader must later distrust. The grain is SEMANTIC: a\ncosmetic edit (whitespace · a comment) re-keys nothing and never\nrefuses; a content edit does, structure-preserving or not. An\nUNSTAMPED report skips the clause — the stamp is the producer's opt-in,\nand the trust backstops stand either way."}]},{"k":"h","depth":2,"text":"The fold law (pointer)","id":"the-fold-law-pointer"},{"k":"p","inline":[{"k":"text","text":"Every proof consumer reads THIS stream: the receipt folds from it\n("},{"k":"link","text":"15","href":"./15-proof.md"},{"k":"text","text":"), "},{"k":"code","text":"--resume"},{"k":"text","text":" replans from it, "},{"k":"code","text":"nika trace show|replay"},{"k":"text","text":" renders it, the verify walk re-hashes it. One stream, no\nside-channel."}]},{"k":"p","inline":[{"k":"strong","text":"Resuming across engine versions is judged, never assumed"},{"k":"text","text":"\n(normative) · a journal records the "},{"k":"code","text":"engine_version"},{"k":"text","text":" that wrote it. A\nresume under a DIFFERENT engine is either an explicit refusal naming\nboth versions, or a compatibility the operator DECLARES — and the\ndeclaration must name the recorded version exactly (a journal from\nbefore versioning is named "},{"k":"code","text":"unrecorded"},{"k":"text","text":"). A blanket force is not\navailable, because a blanket force is precisely the silent degradation\nthis law retires: the old implicit fallback quietly replanned an empty\nplan and called it a resume. The declared compatibility is journaled on\nthe new run's boot manifest, so the attestation says under whose\nauthority the versions were crossed."}]},{"k":"h","depth":2,"text":"Conformance","id":"conformance"},{"k":"p","inline":[{"k":"text","text":"A v1-conformant engine MUST ·"}]},{"k":"list","ordered":true,"items":[[{"k":"text","text":"Write one chained NDJSON journal per run that emits at least one frame (lazy open · append-only · infallible rider)"}],[{"k":"text","text":"Open with the version-2 prologue (the manifest fields above · "},{"k":"code","text":"trace_format: 2"},{"k":"text","text":")"}],[{"k":"text","text":"Chain every line to the previous line's exact bytes (genesis-tagged · the head reported at run end)"}],[{"k":"text","text":"Emit a terminal workflow frame ("},{"k":"code","text":"workflow_completed"},{"k":"text","text":" "},{"k":"text","text":"|"},{"k":"text","text":" "},{"k":"code","text":"workflow_failed"},{"k":"text","text":" "},{"k":"text","text":"|"},{"k":"text","text":" "},{"k":"code","text":"workflow_cancelled"},{"k":"text","text":" "},{"k":"text","text":"|"},{"k":"text","text":" "},{"k":"code","text":"workflow_paused"},{"k":"text","text":") and a terminal task frame per settled task"}],[{"k":"text","text":"Emit a "},{"k":"code","text":"permit_checked"},{"k":"text","text":" frame for every permit decision, granted and refused alike (NEP-0007 · the witness)"}],[{"k":"text","text":"Tolerate unknown members, fields, and kinds when READING a journal (the additive law · report « unrecorded », never guess)"}],[{"k":"text","text":"Classify a journal reaching no lifecycle-terminal frame as "},{"k":"code","text":"incomplete"},{"k":"text","text":" when READING it — never as success, never as forgery (§the end of the run)"}]]},{"k":"hr"},{"k":"p","inline":[{"k":"text","text":"🦋 "},{"k":"em","text":"Related · [15 · Proof](./15-proof.md) · [10 · Authority](./10-authority.md) · [07 · Conformance](./07-conformance.md)"}]}]

the spec · 17

Trace

Every run leaves a journal · one NDJSON file, one event per line, each line chained to the last by hash.

17 · Trace #

Every run leaves a journal · one NDJSON file, one event per line, each line chained to the last by hash. The trace is the run's flight recorder (nika trace show|replay|verify), the resume substrate, and the stream the receipt folds FROM (15). This chapter makes the dialect NORMATIVE: trace_format: 2, the frame grammar, the chain law, the kind vocabulary, and the permit-decision witness (NEP-0007) · the trace stops being an engine-private dialect. What is written here is the OBSERVED wire, grave-not-invented: the conformance golden is a real run's journal, byte-verifiable.

The journal (normative) #

One run → at most one journal file · <trace-dir>/<ISO-compact>-<short -id>.ndjson (production: .nika/traces/). Three laws shape it:

Lazy open · file creation waits for the FIRST emitted frame (a run refused before its prologue · audit refusal · composition failure · leaves no file).
Infallible rider · journal I/O failure never changes the run's verdict or its primary output; the error surfaces AFTER the run as a note. The journal tees BESIDE the chosen primary lane, byte-identical with or without it.
Append-only · frames are written in emission order and never rewritten; the chain (below) makes any rewrite evident.

The frame (normative) #

One event per line · one JSON object · the member set:

Key · Type · Meaning
`chain` · string · sha256 hex of the PREVIOUS line's exact bytes (the chain law below)
`id` · object · `{ "uuid": "<UUIDv7>" }` · unique per frame · time-ordered
`timestamp` · integer · unix epoch **nanoseconds**
`kind` · string · the closed-per-minor kind vocabulary (below)
`fields` · array · ordered `{ "key": string, "value": any }` pairs · the frame's payload
`run` · string | null · the run correlation id when one is set
`correlation` · string | null · causal correlation across runs when one is set

Field VALUES are JSON values (string · number · object-as-string when a payload is itself serialized · the observed permits_json and outcome carry serialized JSON as a string, so the frame grammar stays flat). Sensitive payloads are hashed by the emitter, never carried raw. Additive law · a reader MUST ignore an unknown member and an unknown fields key (report « unrecorded », never guess); an unknown kind is tolerated by verifiers (the walk continues · the chain still binds it).

The chain (normative) #

The first line's chain is the sha256 of the GENESIS tag; every later line's chain is the sha256 hex of the previous line's EXACT bytes. After the run, the last line's hash is the journal's HEAD · printed at run end and carried by the seal. Verification recomputes the walk: any byte edit, insertion, deletion, or reorder breaks every subsequent link (nika trace verify · FORGED). The chain proves INTEGRITY of the sequence; it does not prove authorship (the seal and anchor rails of 15 carry authenticity).

`trace_format: 2` (normative · the version) #

The dialect version rides the FIRST frame (the prologue's trace_format field). It versions the JOURNAL WIRE · orthogonal to the language (v1 · never typed in the file · 01 §nika), receipt_format: 1 (the folded receipt) and graph_format: 3 (the projection). Version 2 is THIS chapter. A wire change that breaks a version-2 reader MUST bump it; additive fields and additive kinds MUST NOT.

The prologue (normative · `workflow_started`) #

The first frame is workflow_started, and it is the run's MANIFEST. Version-2 fields (the observed set):

Field · Meaning
`workflow` · the workflow id
`permits` · the boundary posture, human-readable (`declared boundary · default-deny` | the zero-authority note)
`permits_json` · the DECLARED `permits:` block, serialized verbatim · the boundary the run was judged under
`workflow_sha256` / `workflow_sha256_lf` · the source bytes' digest (raw · LF-normalized)
`semantic_hash` · the semantic identity ([15](./15-proof.md) · H(domain ‖ version ‖ JCS(IR)))
`sandbox` · the OS-confinement backend the run selected (`seatbelt` · `landlock` · `noop`, loudly)
`trace_format` · this dialect's version · `2`
`engine_version` · the emitting engine
`platform` · `os/arch`

An engine MAY add fields (additive law); it MUST NOT drop these.

The prologue is the run's BOOT MANIFEST (normative) · beyond the identity above it names the CONTRACT the run booted under, so the journal self-describes what it ran by rather than leaving a reader to infer it ·

Field · Meaning
`spec_pin` · the spec commit this engine's conformance was proven at
`stamper_kind` · the event-identity seam the `run:` declaration resolved to · `deterministic` | `system`
`clock` · the resolved run clock ([01](./01-envelope.md) §`run`) · `virtual` | `system`
`seed` · present exactly under a determinism demand (`seeded: N` → `N` · `none` → the zero stream); an ambient run carries **no** seed claim

A manifest claims only what exists. Where a fact has no recording surface the field is ABSENT and a reader says « unrecorded » — never a guessed value, never a fabricated zero. Absence is the honest claim, and the additive law above already makes it readable by older readers.

The kind vocabulary (normative · closed per minor) #

Version 2 names exactly these kinds · additive per minor, never re-meant:

workflow_started · workflow_completed · workflow_failed · workflow_cancelled · workflow_paused · task_scheduled · task_started · task_completed · task_failed · task_skipped · task_retrying · task_recovered · task_cancelled · task_cache_hit · verb_invoked · tool_invoked · checkpoint_written · cost_incurred · infer_chunk · permit_checked · lift · run_sealed · agent_tools_selected · agent_nudge · agent_stalled · agent_compose_checked · agent_budget_checkpoint

Per-task terminal frames carry the task's witness fields (the observed task_completed: task · note · duration_ms · def_hash · input_hash · output · outcome · the outcome record serialized).

The permit witness (normative · REQUIRED · NEP-0007) #

Every permit decision taken at the dispatch boundary is a permit_checked frame · granted AND refused alike: the exec program gate, the tool grant, the taint re-gate (10 · NEP-0004), the environment composition (NEP-0005 · the passed names), and the data-as-code sink (NEP-0006). The per-operation fs/net enforcement decisions live inside the builtin sinks (their refusals surface as typed task failures; their allow-side witness is the declared v1 residual · NEP-0007 law 2). The frame's fields name the gate (the bound consulted), the decision (allow | deny), the why (the law applied), and the task. This is a CONFORMANCE requirement on the ENGINE, not a wire bump: the frame grammar is unchanged (one more kind in the stream), so trace_format stays 2. A journal from an OLDER conformant engine simply lacks the frames: nika trace verify reports a run that exercised effects with zero permit-decision frames as a FINDING (the witness is absent · the journal is old or the engine is not NEP-0007-conformant) · never FORGED (the chain still holds), never a crash.

The witness is what makes invariant 4 · judged = executed = attested · CHECKABLE: the static judge's verdicts, the runtime's decisions, and the journal's frames speak the same boundary, and the conformance differential replays the same inputs through checker and engine and FAILS on any verdict divergence.

The end of the run (normative · the teardown seal and `incomplete`) #

The chain proves the sequence; the run's END is a separate claim, and it has three parts.

1 · The seal binds the teardown. A run_sealed frame's covers object carries the classic four — the chain head, the frame events count, the workflow hash, the engine — and extends additively with the teardown facts: receipt_digest (the receipt folded at the seal instant, over this seal's own pre-seal chain facts), budgets (the consumed ρ, present only when metered — never a fabricated zero), and effects (the exercised ε beside the declared bound). A seal without teardown facts stays byte-identical to the classic four-field form and verifies exactly as before; a seal that carries them binds them under the same signature. One signature surface, not a second artifact.

A failed run owes the same seal an attested quarantine: when it dies after producing partly-written outputs, the teardown names those artifacts and marks them quarantined, and a quarantined artifact re-entering as a later run's input is a finding. v1 owes the NAMING and the CONTAINMENT — not the undoing. Compensating actions across services are a different problem and stay out; what a half-written file must never do is pass for a whole one.

2 · A journal with no terminal frame is `incomplete`. A chain walk that reaches no lifecycle-terminal frame (workflow_completed · workflow_failed · workflow_cancelled · workflow_paused · run_sealed) classifies the journal `incomplete` — and that classification is the READER's, never a frame the dying process emits. A process killed mid-flight cannot attest its own death: any protocol that asks it to is vacuous exactly when it matters, so the verifier — the only party guaranteed to exist at reading time — carries the name.

incomplete is never success and never silently equal to failure or to forgery: the chain still binds, so the journal is honestly what it is — a run whose end is unknown. Before it had a name, « no verdict » was routinely read as « fine ».

3 · Judged ≠ booted is a refusal. A check report stamped with the semantic hash of the workflow it judged must match the workflow the run is booting. On mismatch the run REFUSES before its first frame — zero events, no file (the lazy-open law above) — rather than producing a journal a reader must later distrust. The grain is SEMANTIC: a cosmetic edit (whitespace · a comment) re-keys nothing and never refuses; a content edit does, structure-preserving or not. An UNSTAMPED report skips the clause — the stamp is the producer's opt-in, and the trust backstops stand either way.

The fold law (pointer) #

Every proof consumer reads THIS stream: the receipt folds from it (15), --resume replans from it, nika trace show|replay renders it, the verify walk re-hashes it. One stream, no side-channel.

Resuming across engine versions is judged, never assumed (normative) · a journal records the engine_version that wrote it. A resume under a DIFFERENT engine is either an explicit refusal naming both versions, or a compatibility the operator DECLARES — and the declaration must name the recorded version exactly (a journal from before versioning is named unrecorded). A blanket force is not available, because a blanket force is precisely the silent degradation this law retires: the old implicit fallback quietly replanned an empty plan and called it a resume. The declared compatibility is journaled on the new run's boot manifest, so the attestation says under whose authority the versions were crossed.

Conformance #

A v1-conformant engine MUST ·

Write one chained NDJSON journal per run that emits at least one frame (lazy open · append-only · infallible rider)
Open with the version-2 prologue (the manifest fields above · trace_format: 2)
Chain every line to the previous line's exact bytes (genesis-tagged · the head reported at run end)
Emit a terminal workflow frame (workflow_completed | workflow_failed | workflow_cancelled | workflow_paused) and a terminal task frame per settled task
Emit a permit_checked frame for every permit decision, granted and refused alike (NEP-0007 · the witness)
Tolerate unknown members, fields, and kinds when READING a journal (the additive law · report « unrecorded », never guess)
Classify a journal reaching no lifecycle-terminal frame as incomplete when READING it — never as success, never as forgery (§the end of the run)

🦋 Related · [15 · Proof](./15-proof.md) · [10 · Authority](./10-authority.md) · [07 · Conformance](./07-conformance.md)

nika-spec@2b3d6ac3e · 17-trace.md · sha256 4eed0a409939e8e7… · the pack upstream