Daemon laws: the supervisor and its workers #

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

D1. Supervisor #

The daemon is a supervisor: one worker process per active session. Laws: laws/supervise.bend, laws/timeouts.bend, laws/orphan.bend, laws/replace.bend, laws/launcher.bend, laws/notice.bend, laws/revive.bend. Proofs: proof/supervise/, proof/timeouts/, proof/launcher/, proof/revive/ and proof/orphan/. The restart budget, the timeouts' derivation, the revival veto, the orphan exit and the replacement's gate, commit and adoption run as their compiled models: Rust gathers the facts and acts on the answer.

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.	base values: timeouts.rs, eukhe-types daemon/timing.rs, eukhe-core kernel/shared.rs; timeouts.rs derived (compiled model: bend/ffi_timeouts.bend, asked once per process)	bend/supervise.bend Tm	timeouts_ordered, timeouts_ffi_*
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. Vetoes, in order: given up, archived session, live lease holder, no busy record time, a stamp that cannot be read, is more than REVIVAL_CLOCK_SKEW_MS in the future or older than the max age.	revival_gate.rs revival_veto (gathers the facts; compiled model: bend/ffi_revive.bend); worker/run_gate.rs session_work; worker.rs start_busy_refresh; journal.rs refresh_session_busy	bend/revive.bend	revive_after_refresh, revive_veto_ages_as_model, revive_ffi_*
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 (timeouts::Derived::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 the quiesce hold (timeouts::Derived::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.