# Daemon laws: the supervisor and its workers

Shared rules (what a law secures, adversary): [harness.md](harness.md).

### D1. Supervisor

The daemon is a supervisor: one worker process per active session. Laws: `laws/supervise.bend`, `laws/orphan.bend`, `laws/replace.bend`, `laws/launcher.bend`, `laws/notice.bend`, `laws/revive.bend`. Proofs: `proof/supervise/`, `proof/launcher/`, `proof/revive/` and `proof/orphan/`. Bridge: `crates/eukhe-daemon/src/supervision_bridge.rs` runs the timeouts and the revival in Rust and in their models on the same scenarios; transcripts must match. The restart budget, the orphan exit and the replacement's gate, commit and adoption run as their compiled models.

| Rule | Rust | Model | Law |
|---|---|---|---|
| A worker failing more than 5 times in the restart window (15 minutes, monotonic clock) is given up. Restart pause doubles per failure in the window (250 ms to 30 s). | `supervisor/restart_budget.rs` `RestartBudget` (clock), `decide` (compiled model: `bend/ffi_supervise.bend`) | `bend/supervise.bend` | `restart_gives_up`, `restart_decide_window`, `restart_decide_verdict`, `restart_wire_*`, `restart_ffi_*` |
| Each timeout = sum of the timeouts it waits for: stop grace covers kernel teardown and Harness close; launcher waits for the whole supervisor drain; a parent's kill of a child covers kill route and child drain; a lost worker sees a relaunched supervisor before exit; busy evidence outlives one refresh; a quiesced gate stays closed after the answer phase; the restart window holds the give-up count of crash-loop steps. | `timeouts.rs`, `eukhe-types` `daemon/timing.rs`, `eukhe-core` `kernel/shared.rs` | `bend/supervise.bend` `Tm` | `timeouts_ordered` |
| A worker with work re-records busy evidence every 5 minutes; if its latest record says idle (work started after a run ended), the tick records busy. Work is one set: run, compaction, queued input, admitted run start, background job, user bash, unsettled child or workflow run (withdrawn input is not work). A boot within 25 minutes of the crash revives it, however long the run. Never revives a dead worker with no busy record time. | `revival_gate.rs` `busy_evidence_fresh`, `revival_veto`; `worker/run_gate.rs` `session_work`; `worker.rs` `start_busy_refresh`; `journal.rs` `refresh_session_busy` | `bend/revive.bend` | `revive_after_refresh` |
| A worker whose supervisor stays lost exits after the lost-exit window (two windows with work in flight; a window past the wire's range, about 3170 years, never expires). With work (same set): records busy, aborts nothing; a later supervisor resumes. Without work: closes the session. | `supervisor_lost.rs` `monitor`, `leave_orphaned`; `work_gate.rs` `orphan_decision` (compiled model: `bend/ffi_orphan.bend`), `orphan_exit` | `bend/orphan.bend` | `orphan_never_aborts_resumable`, `orphan_idle_exit_due`, `orphan_work_exit_due`, `orphan_capped_window_never_expires`, `orphan_exit_by_work`, `orphan_wire_*`, `orphan_ffi_*` |
| Idle shutdown (launcher replacing an older daemon) never aborts a run. Supervisor asks each worker to quiesce: idle closes its run gate; busy answers busy and leaves its gate as it was. A run starts only at an open gate. Stops workers only if all quiesced; else reopens gates, answers busy. The client never decides. | `work_gate.rs` `WorkGate` (`admits`, `quiesce`, `release`), `idle_shutdown_commits` (compiled model: `bend/ffi_launcher.bend`) | `bend/launcher.bend` | `idle_shutdown_never_aborts`, `launcher_ffi_answers`, `launcher_ffi_malformed`, `launcher_ffi_example` |
| Adopts a live worker only with the same build. Others stop as lost workers do (work stays resumable); their sessions restart on this build. A failed boot launch (revival, move to this build, unreachable live worker) retries under the restart budget. Before each retry, stops an earlier process that survived its stop (identity-gated); never launches beside it; a survivor living on again counts as one more failure. | `supervisor/adoption.rs` `adoption_verdict` (compiled model: `bend/ffi_launcher.bend`; the request names the worker's build by whether it equals the supervisor's), `retry_failed_launch`; `supervisor/supervision.rs` `watch_worker` | `bend/launcher.bend` | `adopt_same_build`, `launcher_ffi_answers` |
| A kernel started over a namespace snapshot stores one restore notice in the session. Each attach (reconnect, worker restart) rebuilds the transcript from all stored messages. A view shows each notice once; after an attach, one notice per restore. | `eukhe-tui` `restore_notices.rs` `RestoreNotices` (bridge test in the same file) | `bend/notice.bend` | `notice_shown_once`, `notice_per_restore` |
| A client start keeps or replaces the daemon on its socket. Order: semver for releases; a `-dev` or older-scheme build (e.g. `0.9.9-main.46`) is below its series' releases. Only an interactive start (TUI, `eukhe chat`) replaces, and only a lower version. Background clients (dashboard, gateway, ACP, relaunch of a lost daemon) never replace. Never replaces a newer daemon or another build of the same version; tells the user. So no downgrade; k builds cause at most k - 1 replacements. | `eukhe-tui` `daemon_build.rs` `replacement_verdict`, run by the compiled core (entry `bend/ffi_replace.bend`), used by `eukhe-cli` `interactive_mode/daemon.rs` | `bend/replace.bend` | `replace_never_downgrades`, `replacement_terminates`, `background_never_replaces`, `replace_rank_reads_semver`, `replace_relation_exact`, `replace_verdict_exact`, `replace_ffi_relation`, `replace_ffi_verdict`, `replace_rank_cut` |

- An attached client relaunches a lost supervisor of its own build within one minute (`CLIENT_RELAUNCH_WITHIN_MS`) when no daemon listens; never replaces a daemon another client started. The relaunched supervisor adopts live workers.
- A worker gives a lost supervisor five minutes (`WORKER_LOST_EXIT_DEFAULT_MS`).
- A client older than the daemon uses it if the protocol agrees and says "this eukhe (vX) is older than the running daemon (vY): update or run `eukhe shutdown`"; if not, it stops with this message.
- The launcher replaces a daemon only with `shutdown` and `ifIdle`, only if it advertises `idle_shutdown`. Busy daemons and daemons without the capability keep serving.
- Supervisor waits one `QUIESCE_ANSWER_MS` window for quiesce answers. A quiesced worker reopens its run gate after `QUIESCE_HOLD_MS` without stop or release.
- Each park (a run end, a session opening idle) re-checks two releases with the same work set: an idle unattached root worker past `idleEvictionMinutes` asks the supervisor to stop it; a parent-owned child (`rlm_depth > 0`) with no pause lease and no registered scheduled job releases its kernel (namespace snapshot flushed; the next kernel use revives it). The release disposes the kernel, so a running kernel `bash()` handle or detached cell holds it; the job's settlement wakes a run, whose end parks again and releases then. Code: `worker/passivation.rs` `release_settled_child_kernel`, `worker/run_gate.rs` `background_work`; test `worker::passivation::tests::a_parked_child_keeps_its_kernel_while_a_background_job_runs`.

Not covered: wall clock between processes (journal timestamps; `REVIVAL_CLOCK_SKEW_MS` bounds it), OS process signals, timer scheduling.