# Daemon laws: the supervisor and its workers

The shared rules (what a law secures, the adversary) are in [harness.md](harness.md).

### D1. Supervisor

The daemon is a supervisor. It starts one worker process for each active
session. The laws are in `LAWS.bend` section `supervisor`; `PROOF.bend` section `supervisor`
proves them. The bridge test `crates/eukhe-daemon/src/supervision_bridge.rs`
runs the Rust code and each model on the same scenarios and requires the
same transcript.

| Rule | Rust | Model | Law |
|---|---|---|---|
| A worker that fails more than 5 times in the restart window (15 minutes, monotonic clock) is given up. The pause before a restart doubles with each failure in the window (250 ms to 30 s). | `supervisor/restart_budget.rs` `RestartBudget` | `bend/supervise.bend` | `restart_gives_up` |
| Each timeout is the sum of the timeouts it waits for: the stop grace covers the kernel teardown and the Harness close; the launcher waits for the whole drain of the supervisor; a parent's kill of a child covers the kill route and the drain of the child; a lost worker sees a relaunched supervisor before it exits; 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 records its busy evidence again every 5 minutes; when its latest record says idle (work that started after a run ended), the tick records it busy. Work is one set everywhere: a run, a compaction, a queued input, an admitted run start, a background job, a user bash, an unsettled child or workflow run (a withdrawn input is not work). A boot within 25 minutes of its crash revives it, however long its run took. A boot never revives a dead worker that has no busy record time. | `revival_gate.rs` `busy_evidence_fresh` and `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). With work in flight (the same work set) it records the session busy and aborts nothing, so a later supervisor resumes the work. Without work it closes the session. | `supervisor_lost.rs` `exit_due` and `leave_orphaned`, `work_gate.rs` `orphan_exit` | `bend/orphan.bend` | `orphan_never_aborts_resumable` |
| An idle shutdown (the launcher's replacement of an older daemon) never aborts a run. The supervisor asks each worker to quiesce. An idle worker closes its run gate; a busy worker answers busy. The supervisor stops the workers only when every worker quiesced, else it opens the gates again and answers busy. The client never decides. | `work_gate.rs` `WorkGate`, `idle_shutdown_commits` | `bend/launcher.bend` | `idle_shutdown_never_aborts` |
| A supervisor adopts a live worker only when the worker reports the same build. Another worker stops as a lost worker does (its work stays resumable) and its session starts again on this build. A boot launch that fails (a revival, a move to this build, or a live worker the boot cannot reach) is retried under the restart budget. Before each retry the supervisor stops an earlier process that survived its stop (identity-gated). It never launches beside that process; a survivor that lives on again counts as one more failure. | `supervisor/adoption.rs` `adoption_verdict` and `retry_failed_launch`, `supervisor/supervision.rs` `watch_worker` | `bend/launcher.bend` | `adopt_same_build` |
| A worker that starts a kernel over a namespace snapshot stores one restore notice in the session. Each attach (a reconnect, a worker restart) rebuilds the transcript from all stored messages. A view shows each restore notice one time: an attach does not show a notice that the view showed before. After an attach, the view showed one notice for each restore. | `eukhe-tui` `restore_notices.rs` `RestoreNotices` (its bridge test is in the same file) | `bend/notice.bend` | `notice_shown_once`, `notice_per_restore` |
| A client start keeps or replaces the daemon on its socket. Versions have an order: the semver order of releases; a `-dev` build or an older-scheme build (such as `0.9.9-main.46`) is below the releases of its series. Only an interactive start (the TUI, `eukhe chat`) replaces a daemon, and only a daemon of a lower version. A background client (the dashboard, the gateway, ACP, the relaunch of a lost daemon) never replaces a daemon. A client never replaces a newer daemon or another build of the same version; it tells the user. Thus the daemon never goes back to a lower version, and k builds cause k - 1 replacements at most. | `eukhe-tui` `daemon_build.rs` `replacement_verdict` (its bridge test is `daemon_build/bridge.rs`), used by `eukhe-cli` `interactive_mode/daemon.rs` | `bend/replace.bend` | `replace_never_downgrades`, `replacement_terminates`, `background_never_replaces` |

An attached client relaunches a lost supervisor of its own build within
one minute of the loss (`CLIENT_RELAUNCH_WITHIN_MS`) when no daemon
listens. It does not replace a daemon that another client started. The
relaunched supervisor adopts the live workers. A worker gives a lost
supervisor five minutes (`WORKER_LOST_EXIT_DEFAULT_MS`).

A client older than the daemon uses the daemon when the protocol
agrees, and says: "this eukhe (vX) is older than the running daemon
(vY): update or run `eukhe shutdown`". When the protocol does not agree,
the client stops with this message.

The launcher replaces a daemon only with `shutdown`
and `ifIdle`, and only when the daemon advertises the `idle_shutdown`
capability. A busy daemon, or a daemon without the capability, keeps
serving. The supervisor waits one `QUIESCE_ANSWER_MS` window for all
quiesce answers. A quiesced worker opens its run gate again after
`QUIESCE_HOLD_MS` when no stop and no release comes.

What the laws do not cover: the wall clock between two processes (the
journal's timestamps; `REVIVAL_CLOCK_SKEW_MS` bounds it), the operating
system's process signals, and the scheduling of the timers.