{"row":{"n":"0007","slug":"nep-0007-trace-format-and-equivalence","file":"nep-0007-trace-format-and-equivalence.md","headline":"The trace leaves the private dialect: a normative journal, a required witness, a differential oracle","title":"The run journal is a versioned chapter of the spec, every permit decision is a required trace frame, and check ⇔ run agreement is proven by a differential oracle","status":"Draft","type":"Standards Track","created":"2026-07-23","author":"Thibaut Melen (SuperNovae Studio)","lede":"NEP-0003 through NEP-0006 hardened WHAT the boundary refuses.","sections":[{"title":"Abstract","anchor":"abstract"},{"title":"Motivation","anchor":"motivation"},{"title":"Specification","anchor":"specification"},{"title":"Conformance test","anchor":"conformance-test"},{"title":"Compatibility impact","anchor":"compatibility-impact"},{"title":"Rejected alternatives","anchor":"rejected-alternatives"}],"words":1095,"sha256":"730f680968ff38df66acbeecd1d2647a6528789cd0f9bb2d526f01296c5ec3dc"},"prev":{"n":"0006","slug":"nep-0006-data-as-code-sink","file":"nep-0006-data-as-code-sink.md","headline":"The data-as-code sink: a fetch of a code-bearing artifact is never innocent","title":"The contract distinguishes inert reads from code-bearing reads: a fetch whose artifact class can execute is refused, unless the read is declared inert","status":"Draft","type":"Standards Track","created":"2026-07-23","author":"Thibaut Melen (SuperNovae Studio)","lede":"NEP-0003 sealed the absent boundary, NEP-0004 the values flowing under\nit, NEP-0005 the environment plane.","sections":[{"title":"Abstract","anchor":"abstract"},{"title":"Motivation","anchor":"motivation"},{"title":"Specification","anchor":"specification"},{"title":"Conformance test","anchor":"conformance-test"},{"title":"Compatibility impact","anchor":"compatibility-impact"},{"title":"Migration plan","anchor":"migration-plan"},{"title":"Rejected alternatives","anchor":"rejected-alternatives"}],"words":1230,"sha256":"465beb460148e07bac89375b0876e98b66a2a791ad60bd1bc0e516fc389c5aa6"},"next":{"n":"0008","slug":"nep-0008-egress-permit-bound","file":"nep-0008-egress-permit-bound.md","headline":"The sandboxed egress proxy is the permit's exact projection","title":"The sandboxed egress proxy is the exact projection of `permits.net.http` — exact-host allowlists, proxy-side DNS, a normative port floor, one allowlist per run, and no dead grants","status":"Draft","type":"Standards Track","created":"2026-07-23","author":"Thibaut Melen (SuperNovae Studio)","lede":"NEP-0003 through NEP-0006 hardened WHAT the boundary refuses; NEP-0007\nmade the refusal attributable.","sections":[{"title":"Abstract","anchor":"abstract"},{"title":"Motivation","anchor":"motivation"},{"title":"Specification","anchor":"specification"},{"title":"Rationale","anchor":"rationale"},{"title":"Backwards Compatibility","anchor":"backwards-compatibility"},{"title":"Reference Implementation","anchor":"reference-implementation"},{"title":"Deferred (P2, by decision)","anchor":"deferred-p2-by-decision"},{"title":"Copyright","anchor":"copyright"}],"words":1189,"sha256":"7193b92df0e733bf9f0a85d812e697187c2cbdcf6a357db61f5ee8d02a988017"},"total":18}

[{"k":"h","depth":1,"text":"NEP-0007 · The trace leaves the private dialect: a normative journal, a required witness, a differential oracle","id":"nep-0007--the-trace-leaves-the-private-dialect-a-normative-journal-a-required-witness-a-differential-oracle"},{"k":"list","ordered":false,"items":[[{"k":"strong","text":"NEP"},{"k":"text","text":": 0007 (next free integer · 0001 reserved for the v1 surface · 0002 the trifecta gate · 0003 absent permits · 0004 the parameterization taint · 0005 the environment permit · 0006 the data-as-code sink)"}],[{"k":"strong","text":"Title"},{"k":"text","text":": The run journal is a versioned chapter of the spec, every permit decision is a required trace frame, and check ⇔ run agreement is proven by a differential oracle"}],[{"k":"strong","text":"Author"},{"k":"text","text":": Thibaut Melen (SuperNovae Studio)"}],[{"k":"strong","text":"Status"},{"k":"text","text":": Draft"}],[{"k":"strong","text":"Type"},{"k":"text","text":": Standards Track"}],[{"k":"strong","text":"Created"},{"k":"text","text":": 2026-07-23"}]]},{"k":"h","depth":2,"text":"Abstract","id":"abstract"},{"k":"p","inline":[{"k":"text","text":"NEP-0003 through NEP-0006 hardened WHAT the boundary refuses. This NEP\nhardens the claim that the three deciders agree: the static judge, the\nrunning engine, and the journal a verifier reads MUST decide the same\nartifact · invariant 4, judged = executed = attested. Three deliverables\nmake the invariant checkable instead of asserted. (1) The trace format\nbecomes a normative, versioned chapter ("},{"k":"link","text":"17","href":"../spec/17-trace.md"},{"k":"text","text":" ·\n"},{"k":"code","text":"trace_format: 2"},{"k":"text","text":" · the frame grammar, the hash chain, the prologue\nmanifest, the kind vocabulary · graved from an observed run, never\ninvented). (2) Every permit decision the run takes · granted and\nrefused alike, across every plane · is a REQUIRED "},{"k":"code","text":"permit_checked"},{"k":"text","text":"\nframe: the boundary becomes attributable after the fact. (3) The\nequivalence is proven the Cedar way: a differential oracle replays the\nsame inputs through the checker and the engine and FAILS on any verdict\ndivergence, with coverage DERIVED by the suite itself · never « we\ntested it well »."}]},{"k":"h","depth":2,"text":"Motivation","id":"motivation"},{"k":"p","inline":[{"k":"text","text":"The empirical driver is the measured spec↔engine skew (23 commits of\ndrift between what the documents said and what the code did, found by\nthe cross-audit): prose alignment decays, only a machine-checked\nequivalence survives. The trace was an engine-private dialect (its\nformat documented in an internal crate spec), so no second\nimplementation could verify a journal, and permit decisions were\ninvisible in it · the vocabulary reserved a "},{"k":"code","text":"permit_checked"},{"k":"text","text":" kind that\nproduction never emitted. A boundary that cannot be audited after the\nfact is a boundary on trust."}]},{"k":"h","depth":2,"text":"Specification","id":"specification"},{"k":"p","inline":[{"k":"text","text":"The law (MUST):"}]},{"k":"list","ordered":true,"items":[[{"k":"strong","text":"The format is the chapter."},{"k":"text","text":" A conformant engine writes the run\njournal exactly as "},{"k":"link","text":"17 · Trace","href":"../spec/17-trace.md"},{"k":"text","text":" specifies:\nNDJSON frames, the sha256 chain over exact previous-line bytes\n(genesis-tagged, head reported), the "},{"k":"code","text":"workflow_started"},{"k":"text","text":" prologue\nmanifest carrying "},{"k":"code","text":"trace_format: 2"},{"k":"text","text":", terminal frames for the\nworkflow and every settled task, and the closed-per-minor kind\nvocabulary. A wire change that breaks a version-2 reader MUST bump\n"},{"k":"code","text":"trace_format"},{"k":"text","text":"; additive fields and kinds MUST NOT."}],[{"k":"strong","text":"The witness is required."},{"k":"text","text":" Every permit decision taken at the\ndispatch boundary · the exec program gate, the tool grant, the taint\nre-gate (NEP-0004), the environment composition (NEP-0005 · the\npassed names), the data-as-code sink (NEP-0006) · emits one\n"},{"k":"code","text":"permit_checked"},{"k":"text","text":" frame naming the gate, the decision\n("},{"k":"code","text":"allow"},{"k":"text","text":" | "},{"k":"code","text":"deny"},{"k":"text","text":"), the law applied, and the task. Granted decisions\nare witnessed, not only refusals: an auditor reconstructs WHAT\nauthority was exercised, not only what was blocked. The\nper-operation fs and net enforcement decisions live INSIDE the\nbuiltin sinks (canonicalize-then-confine walks the real filesystem ·\na dispatch-side pre-witness could claim allow where the sink then\nrefuses a symlink escape, a lying witness): their refusals already\nsurface as typed task failures, and their allow-side witness is the\nDECLARED v1 residual · it lands with the builtin-journal plumbing,\nnever as a dishonest pre-computation."}],[{"k":"strong","text":"Old journals stay readable, honestly."},{"k":"text","text":" The witness requirement is\nbehavioral (a conformance requirement on the engine), not a wire\nbump: "},{"k":"code","text":"trace_format"},{"k":"text","text":" stays 2. A verifier reading a journal that\nexercised effects with zero permit-decision frames MUST report a\nFINDING (the witness is absent · the journal predates NEP-0007 or\nthe engine is not conformant) · never FORGED (the chain still\nbinds), never a crash."}],[{"k":"strong","text":"Equivalence is proven differentially."},{"k":"text","text":" The conformance suite\nreplays the same inputs through BOTH evaluators · the static checker\nand the running engine · and FAILS on any verdict divergence, under\nthe mapping law: a check-time refusal (the AUTH series) means the\nrun refuses before its prologue; a check-time deferral (NEP-0004\nlaw 4 · NEP-0006 law 3) means the run's twin refuses at effect time\n("},{"k":"code","text":"NIKA-SEC-004"},{"k":"text","text":"); a clean check means the run stays inside the\ndeclared boundary. Cases outside the mapping (pause · resume ·\ncancel) are DECLARED out of scope, never silently forced."}],[{"k":"strong","text":"Coverage is derived."},{"k":"text","text":" The differential suite counts and prints\nwhat it covered (families × planes × fixtures); no coverage figure\nis ever hand-written. What is not covered is named residual."}]]},{"k":"p","inline":[{"k":"text","text":"Registry and prose touched:"}]},{"k":"list","ordered":false,"items":[[{"k":"strong","text":"LAW-AUTH-0328"},{"k":"text","text":" is added to "},{"k":"code","text":"canon/laws/authority.yaml"},{"k":"text","text":" (status\nactive) · the machine row of this NEP."}],[{"k":"code","text":"spec/17-trace.md"},{"k":"text","text":" is NEW (the chapter) · "},{"k":"code","text":"spec/00-overview.md"},{"k":"text","text":" maps\nit."}],[{"k":"text","text":"No new diagnostic code: the verify surface reports the absent witness\nas a finding in its own verdict vocabulary, and the runtime refusal\nvoice stays "},{"k":"code","text":"NIKA-SEC-004"},{"k":"text","text":"."}],[{"k":"text","text":"Implementation surfaces: the event vocabulary (the reserved\n"},{"k":"code","text":"permit_checked"},{"k":"text","text":" kind gains its payload contract) · the runtime\ngates (emission) · the trace verifier (the REQUIRED-witness rule) ·\nthe conformance differential suite."}]]},{"k":"h","depth":2,"text":"Conformance test","id":"conformance-test"},{"k":"p","inline":[{"k":"text","text":"The golden journal ships as a conformance artifact · a REAL run's\ntrace (chained · sealed head · byte-verifiable) with its workflow ·\nplus verify contracts: the intact journal verifies clean; the same\njournal judged under NEP-0007 with effects and no witness frames is a\nFINDING; a tampered byte is FORGED. The differential suite is\nengine-side (it needs both evaluators) and prints its derived coverage."}]},{"k":"h","depth":2,"text":"Compatibility impact","id":"compatibility-impact"},{"k":"p","inline":[{"k":"text","text":"Additive. Old journals read clean under the chain walk and report the\nabsent witness as a finding (law 3). New journals grow one frame kind\nper permit decision · the same order of magnitude as "},{"k":"code","text":"tool_invoked"},{"k":"text","text":",\nbounded by the existing retention caps."}]},{"k":"h","depth":2,"text":"Rejected alternatives","id":"rejected-alternatives"},{"k":"list","ordered":false,"items":[[{"k":"strong","text":"Bumping `trace_format` to 3 for the witness"},{"k":"text","text":" · rejected: the frame\ngrammar is unchanged; version churn without a wire break makes every\nreader gate on a number that means nothing."}],[{"k":"strong","text":"A new diagnostic code for the absent witness"},{"k":"text","text":" · rejected for v1:\nthe verifier's verdict vocabulary already distinguishes FINDING from\nFORGED; minting a wire code for a verify-surface report adds registry\nweight without a new refusal class."}],[{"k":"strong","text":"Witnessing refusals only"},{"k":"text","text":" · rejected: refusals already surface as\ntask failures; the auditable gap is the GRANTED authority · the\nboundary you cannot reconstruct is the one that was exercised."}],[{"k":"strong","text":"Proving equivalence by shared code"},{"k":"text","text":" · rejected as the sole answer:\nshared predicates (the house pattern) kill one drift class, but only\nthe differential replay proves the COMPOSED pipelines agree end to\nend (the Cedar lesson · RS-13)."}]]}]

NEP-0007

The trace leaves the private dialect: a normative journal, a required witness, a differential oracle

Draft · Standards Track · opened 2026-07-23 · 1095 words

NEP-0007 · The trace leaves the private dialect: a normative journal, a required witness, a differential oracle #

NEP: 0007 (next free integer · 0001 reserved for the v1 surface · 0002 the trifecta gate · 0003 absent permits · 0004 the parameterization taint · 0005 the environment permit · 0006 the data-as-code sink)
Title: The run journal is a versioned chapter of the spec, every permit decision is a required trace frame, and check ⇔ run agreement is proven by a differential oracle
Author: Thibaut Melen (SuperNovae Studio)
Status: Draft
Type: Standards Track
Created: 2026-07-23

Abstract #

NEP-0003 through NEP-0006 hardened WHAT the boundary refuses. This NEP hardens the claim that the three deciders agree: the static judge, the running engine, and the journal a verifier reads MUST decide the same artifact · invariant 4, judged = executed = attested. Three deliverables make the invariant checkable instead of asserted. (1) The trace format becomes a normative, versioned chapter (17 · trace_format: 2 · the frame grammar, the hash chain, the prologue manifest, the kind vocabulary · graved from an observed run, never invented). (2) Every permit decision the run takes · granted and refused alike, across every plane · is a REQUIRED permit_checked frame: the boundary becomes attributable after the fact. (3) The equivalence is proven the Cedar way: a differential oracle replays the same inputs through the checker and the engine and FAILS on any verdict divergence, with coverage DERIVED by the suite itself · never « we tested it well ».

Motivation #

The empirical driver is the measured spec↔engine skew (23 commits of drift between what the documents said and what the code did, found by the cross-audit): prose alignment decays, only a machine-checked equivalence survives. The trace was an engine-private dialect (its format documented in an internal crate spec), so no second implementation could verify a journal, and permit decisions were invisible in it · the vocabulary reserved a permit_checked kind that production never emitted. A boundary that cannot be audited after the fact is a boundary on trust.

Specification #

The law (MUST):

The format is the chapter. A conformant engine writes the run journal exactly as 17 · Trace specifies: NDJSON frames, the sha256 chain over exact previous-line bytes (genesis-tagged, head reported), the workflow_started prologue manifest carrying trace_format: 2, terminal frames for the workflow and every settled task, and the closed-per-minor kind vocabulary. A wire change that breaks a version-2 reader MUST bump trace_format; additive fields and kinds MUST NOT.
The witness is required. Every permit decision taken at the dispatch boundary · the exec program gate, the tool grant, the taint re-gate (NEP-0004), the environment composition (NEP-0005 · the passed names), the data-as-code sink (NEP-0006) · emits one permit_checked frame naming the gate, the decision (allow | deny), the law applied, and the task. Granted decisions are witnessed, not only refusals: an auditor reconstructs WHAT authority was exercised, not only what was blocked. The per-operation fs and net enforcement decisions live INSIDE the builtin sinks (canonicalize-then-confine walks the real filesystem · a dispatch-side pre-witness could claim allow where the sink then refuses a symlink escape, a lying witness): their refusals already surface as typed task failures, and their allow-side witness is the DECLARED v1 residual · it lands with the builtin-journal plumbing, never as a dishonest pre-computation.
Old journals stay readable, honestly. The witness requirement is behavioral (a conformance requirement on the engine), not a wire bump: trace_format stays 2. A verifier reading a journal that exercised effects with zero permit-decision frames MUST report a FINDING (the witness is absent · the journal predates NEP-0007 or the engine is not conformant) · never FORGED (the chain still binds), never a crash.
Equivalence is proven differentially. The conformance suite replays the same inputs through BOTH evaluators · the static checker and the running engine · and FAILS on any verdict divergence, under the mapping law: a check-time refusal (the AUTH series) means the run refuses before its prologue; a check-time deferral (NEP-0004 law 4 · NEP-0006 law 3) means the run's twin refuses at effect time (NIKA-SEC-004); a clean check means the run stays inside the declared boundary. Cases outside the mapping (pause · resume · cancel) are DECLARED out of scope, never silently forced.
Coverage is derived. The differential suite counts and prints what it covered (families × planes × fixtures); no coverage figure is ever hand-written. What is not covered is named residual.

Registry and prose touched:

LAW-AUTH-0328 is added to canon/laws/authority.yaml (status active) · the machine row of this NEP.
spec/17-trace.md is NEW (the chapter) · spec/00-overview.md maps it.
No new diagnostic code: the verify surface reports the absent witness as a finding in its own verdict vocabulary, and the runtime refusal voice stays NIKA-SEC-004.
Implementation surfaces: the event vocabulary (the reserved permit_checked kind gains its payload contract) · the runtime gates (emission) · the trace verifier (the REQUIRED-witness rule) · the conformance differential suite.

Conformance test #

The golden journal ships as a conformance artifact · a REAL run's trace (chained · sealed head · byte-verifiable) with its workflow · plus verify contracts: the intact journal verifies clean; the same journal judged under NEP-0007 with effects and no witness frames is a FINDING; a tampered byte is FORGED. The differential suite is engine-side (it needs both evaluators) and prints its derived coverage.

Compatibility impact #

Additive. Old journals read clean under the chain walk and report the absent witness as a finding (law 3). New journals grow one frame kind per permit decision · the same order of magnitude as tool_invoked, bounded by the existing retention caps.

Rejected alternatives #

Bumping `trace_format` to 3 for the witness · rejected: the frame grammar is unchanged; version churn without a wire break makes every reader gate on a number that means nothing.
A new diagnostic code for the absent witness · rejected for v1: the verifier's verdict vocabulary already distinguishes FINDING from FORGED; minting a wire code for a verify-surface report adds registry weight without a new refusal class.
Witnessing refusals only · rejected: refusals already surface as task failures; the auditable gap is the GRANTED authority · the boundary you cannot reconstruct is the one that was exercised.
Proving equivalence by shared code · rejected as the sole answer: shared predicates (the house pattern) kill one drift class, but only the differential replay proves the COMPOSED pipelines agree end to end (the Cedar lesson · RS-13).

This proposal in the spec repo The specification it amends