Correct the caller-configured user-namespace topology, bind modeled network readiness to the live sandbox and helper, and keep physical canary, topology, encoding, and capability predicates in compact specification tables below the model boundary.
Promote Host Coordinator + Runtime Supervisor + attached runsc as the product
architecture in the specification, and extend the TLA+ model with generation-scoped
identities, multi-role durable intent, network readiness, prepared-lower lease, and
connectivity-helper ownership. TLC-checked; trim product prose that the model now owns.
Add a TLC-checked invariant requiring any Host Coordinator process record to belong to a non-absent, lock-held Domain. Include the invariant in the aggregate safety operator and remove journal-only markers from protocol model comments so the model remains grounded in product vocabulary.
Add SessionCoordinatorPresent aliases, HC protocol-face naming, and abstract
durable intent/path-mismatch refuse invariants for FM1/FM4/FM5. TLC green at
395837 generated / 110013 distinct / depth 49.
- Replaces stream/socket escalation with a sandboxed regular-file Escalation Mailbox to satisfy runsc isolation boundaries without exposing `host-uds=open`.
- Expands the TLA+ protocol model with role-bound certificates, tuple authorization, and structured domain-failure recovery paths.
- Adds physical integration journals for host terminfo injection, persistent /etc DNS shims, rootless Podman network topology, and static client delivery.
- Establishes specification requirements for safe host-only State Anchor inspection and crash-consistent reset operations.
