Daemon laws: the supervisor and its workers #

The shared rules (what a law secures, the adversary) are in 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.