# ADR-044: Fleet intake liveness — BackstopTick + PostureEdge complete the host transition relation

**Status: accepted** (2026-09-12, ergo epic `TB4QGX`; tasks `3RKEV6` -> `5L4FSL` -> `LMNDZ4` -> `PEVBO4` -> `VXP27K` -> `PPIJJO` -> `XATYL5`).
Ratified in a two-peer workshop (`peer_a` glm-5.3, `peer_b` kimi-k3, both FINAL
ACCEPT), stress-tested by an adversarial review session across the task chain,
and mechanized as properties in `PPIJJO`.

## Context

The second live settlement-bot run deadlocked its registration crawl at
**9,955 registered paths**. Under a `Cordoned` posture the fleet intake backlog
held units; the crawl driver's bounded submission window
(`REG_INTAKE_WINDOW = 32`) blocked on a parked receipt; the host — which only
pumped on a message — parked in `rx.recv()` forever. Safety (never-drop) held;
liveness failed. Evidence: `degenbot_engine_registered_paths` frozen at 9955,
registration skips frozen, no `[build_paths] Path discovery complete`, every
`work-fleet-pool*` thread in futex, Python main in `ep_poll`.

## Root cause: an incomplete transition relation

`HostMsg { Enqueue, SeatDone }` was the **entire input alphabet**, while posture
is mutated by the block-pump thread and only *sampled* as a guard. That leaves

```
(backlog != empty, posture Nominal, in-flight = 0, no pending messages)
```

a reachable **terminal** state: no symbol in the alphabet can leave it. The
retired wake-discipline note argued that a continuing flood of submissions
would self-wake the backlog, but that is a **client-fairness assumption**, and
the driver's bounded window falsifies it — the client legitimately stops
submitting while its window is full.

### Guard vs input (the analysis that decided the fix)

Posture is a *live guard variable* mutated by another thread. The host samples
it only when it runs; a transition relation over `{Enqueue, SeatDone}` cannot
observe a guard change that produces no message. Two families of fix exist:

1. **Mirror the guard as an input** (push posture values into the host).
2. **Add a wake source that forces a re-read of the live guard.**

(1) duplicates state and invites divergence (a stale mirror is a new bug class);
it was rejected. (2) requires no value transfer and cannot go stale — only a
*nudge* to re-run the pump. The ratified design takes (2), with (1)'s
responsibility falling on the pure admission predicate instead.

## Decision (ratified design)

1. **Posture stays a live guard; no host mirror.** The `PostureHeld` hand-back
   remains the TOCTOU backstop.
2. **Two inputs added:** `BackstopTick` (mandatory liveness) and `PostureEdge`
   (untrusted, seq-stamped hint — never a value).
3. **`recv_timeout` is armed iff the backlog is non-empty**; on timeout the
   host runs `pump()`. An idle host blocks indefinitely (no polling cost).
4. **`PostureEdge` delivery** is a bot-side, block-pump-fed waker
   (`arb_engine::fleet_wake`): no new thread, no layering inversion, plus a
   feeder-site contract (every owner-mutating site emits on a non-`Held`
   change).
5. **Progress FSM: `Idle` / `Backed` / `Faulted` / `Closed`**, with admission
   expressed as a **pure predicate** over `(queue_len, queue_cap,
   posture_admits)`.
6. **`Faulted` keys on the typed `LaneDeath` latch** (never a duration
   heuristic); it drains held receipts with **typed terminal receipts**, while
   in-flight units complete naturally.
7. **K consecutive admit-but-no-progress ticks -> loud `discipline.fail`**; K is
   a typed config constant.
8. **Properties:** S = unit conservation
   (`submitted == in-flight + queued + backlog + resolved-receipts`);
   L = every reachable `Backed` state receives a `BackstopTick` within Delta,
   re-evaluating every mutable guard => `AF(drained | Faulted | loud-abort)`.

The observable counterpart is the `degenbot_fleet_intake_backlog{role=...}`
gauge: a held backlog is visible and must be driven to zero by the backstop.

## Consequences

- A held backlog is drained at the latest one backstop interval after a guard
  change, even with zero client messages.
- A stuck intake with capacity is loud within K ticks rather than silent.
- A dead lane resolves every waiting receipt terminally (typed error) and
  latches sticky until a fresh process — no parked driver, no silent loss.
- Hosts that persist no pyo3-owned receipts (`sim`/`solve`) never enter
  `Faulted`; held work there is not applicable.

## Alternatives considered (rejected)

- **Floor-not-hold** (let one unit trickle through a cordon): changes the
  fleet-wide duty-window intent, and a floor-1 trickle keeps the duty window
  dirty so exit hysteresis may never fire.
- **Per-host bridge thread**: a new thread per host with no never-drop gain,
  and a lifetime/supervision surface the fleet does not need.
- **Owner-side sender registry**: the posture owner would have to know host
  channels — a layering inversion, and a registration surface that must be
  kept in sync with host lifetimes.
- **Bare timed `recv` (unconditional polling)**: an idle host would wake and
  re-run the pump forever; the conditional arming (`backlog != empty`) keeps
  the backstop a liveness floor instead of a busy-spin.
- **Posture mirror in the host**: duplicates a guard and invites stale-value
  divergence; the pure predicate plus a hint is strictly simpler.
- **Respawn/retry of parked units**: breaks at-most-once and the never-execute
  semantics of terminal receipts.

## References

- `rust/crates/engine/degenbot-bot/src/arb_engine/seat_host.rs` — `HostPump`
  (`run`/`apply_host_msg`/`pump`), backlog, wake discipline, properties.
- `rust/crates/engine/degenbot-workers/src/posture.rs` — `PostureOwner`/
  `PostureWatch`, `LaneDeath` latch, feeder-site contract.
- `rust/crates/engine/degenbot-workers/src/dispatcher.rs` — `FleetHost`,
  `try_enqueue` (`PostureHeld`), `posture_admits_role`.
- `rust/crates/engine/degenbot-bot/src/arb_engine/fleet_wake.rs` — bot-side waker.
- `rust/crates/engine/degenbot-bot/src/bot_core/block_pump.rs` — per-header posture
  feed.
- `src/degenbot/runner/build_paths.py` — `run_registration` window,
  `_consume` operator path.
- `docs/spike-intake-terminal-receipts.md` — the terminal-receipt spike.