ADR-129
Run state and evidence state are distinct: the writer's lease, the INCOMPLETE exit, the resident's interrupted
accepted · 2026-09-04 · L3 L4 · cites 6
0ADR-129: Run state and evidence state are distinct #
Context #
A journal with no terminal frame is either a run in flight or the remains
of a writer that died. The store folded frames, and a dead process writes
no frame, so trace ls said running forever for a killed run (#1442,
measured twice by the wave-7 gauntlet), while trace verify printed
INCOMPLETE and exited 0 — a monitor wired on the exit code greened a dead
run. The resident's interrupted (ownership lost after a restart) had no
journal twin and read like a fifth run state (#1443). ADR-128 gave the run
ONE settlement; the evidence needed its own truth, kept apart from it.
Decision #
- A dead process proves incomplete evidence, never a failed run. No door invents a terminal frame for a writer that died; the run's own settlement is its terminal frame, and there is none.
- The writer's lease. The run that writes a journal holds
<trace>.lock(owner-only,{"pid","host"}) under an exclusive advisory lock for the journal's lifetime (nika_dap::liveness, taken by the trace sink at open); the kernel releases it when the process ends, however it ends. A reader asks the lock: held →alive, free on this host →dead, no lease or another host →unknown. It never guesses. The lease dies with its journal (trace rm· retention). - The words.
trace lsprintsdead(both faces ·livenesson the machine one) for a running trace whose writer died;runningfor a live writer or one this host cannot judge. The run state staysRunning— the word is about the evidence. - The exit.
trace verifyexitsINCOMPLETE(5) for a journal that never reached a terminal frame, and names the writer's liveness; FILE (2) stays the broken or forged chain, ENV (3) the missing input. The UNSEALED tier keeps its opt-in strictness (--require-seal). - The resident's `interrupted` is an evidence state — ownership lost, effect settlement unknown, the journal INCOMPLETE — published as such in the OpenAPI, never mapped from a run state.
Consequences #
- Positive: a dead run is told from a live one on every door; CI cannot green incomplete evidence; the vocabulary keeps RunState and EvidenceState apart as the one-door invariants require.
- Negative:
trace verifyon a run in flight now exits 5 (honest: not yet complete); a lease sidecar rides beside every journal (0600, tens of bytes); a journal copied to another host readsunknown. - Follow-ups: the serve status matrix (#1443); the seal's teardown word.
Alternatives considered #
- The pid on the opening frame: not portable and not a liveness proof (a reused pid lies); the lease is judged by the kernel.
- Inventing
workflow_failedfor a dead writer: rejected — a reader would be writing evidence it does not have.
read at v0.118.7 · the decision record ships with the engine