lazaret/docs/specification.md

# Lazaret Specification

This document is the normative product specification for Lazaret.

### Document authority

| Document | Authoritative for |
| :--- | :--- |
| This specification | Product north star, trust model, stable vocabulary and identifiers, below-abstraction architecture, and product requirements |
| [TLA+ application protocol model](protocol/Lazaret.tla) and [TLC config](protocol/Lazaret.cfg) | Protocol lifecycle, communication semantics, publication, registration, escalation, recovery, and checked invariants |
| [Prepared-lower TLA+ model](protocol/PreparedLower.tla) and [TLC config](protocol/PreparedLower.cfg) | Prepared-artifact publication, generation leases, mounts, reclamation, stage recovery, and checked invariants |

This specification does **not** restate modeled actions or invariants. The TLA+
models are authoritative above their abstraction boundaries. This specification
owns physical refinements below those boundaries. A new above-abstraction rule
belongs in the applicable model before a product refinement relies on it.
Schemas, executable corpora, fixtures, examples, journals, and scratchpad work
are non-authoritative implementation artifacts. They must conform to this
specification and the applicable TLA+ model; they do not add product requirements
when those authorities are silent.

## 1. Problem Statement

AI coding agents need broad local capabilities: they run arbitrary tools, modify a
project, use Git, install dependencies, and access selected network services. Code
produced or invoked by an agent is not trusted to run directly on the developer's
host. A conventional container reduces risk, but poor terminal behavior, transient
tool state, restricted Git access, and manual setup can make the safe path too
inconvenient for routine work.

Lazaret's north star is:

> Make isolated agent execution the easiest way to work, while ensuring that every
> transition from the sandbox to host authority is explicit, attributable, and
> controlled by the developer.

Lazaret therefore provides a rootless gVisor sandbox with a bidirectionally shared
workspace, persistent sandbox-local tooling, controlled network egress, and a
human-in-the-loop host escalation path.

### 1.1 Trust Model

The following components are trusted:

- The developer and host operating system.
- The Lazaret CLI and the domain's Session Coordinator (Host Coordinator, Runtime
  Supervisor, and attached runsc client).
- Host configuration selected by the developer.
- Domain network-policy installation and connectivity helpers under Runtime
  Supervisor ownership, and the policy Lazaret installs for the Domain.

The following components are untrusted:

- The agent and every process it launches.
- Code, tools, and package installation scripts executed inside the Agent Sandbox.
- Data received from the network by sandboxed processes.

All Client Sessions in the same Domain intentionally share an Agent Sandbox and
are one sandbox trust domain. Session identity distinguishes ownership and routes
terminal interactions; it is not an isolation boundary between processes in that
sandbox.

The Agent Workspace is intentionally writable. Lazaret protects the host outside
the explicitly mounted workspace and volumes. Tracked and ordinary untracked
workspace paths remain writable, while Git-ignored paths are isolated into
Domain-scoped sandbox state by default. The developer may explicitly disable that
isolation in trusted host configuration.

The trusted-host configuration refinement below owns strict parsing,
canonicalization, path authority, and configuration fingerprinting. Successful
loading is the physical meaning of the model's `ConfigSafe`; configuration bytes
never enter a sandbox mount specification.

## 2. Glossary

These terms and identifiers are stable across the specification, protocol model,
implementation, logs, and user interfaces.

| Term | Definition |
| :--- | :--- |
| **Agent Profile** | A developer-selected host configuration describing an agent image and its granted storage, network, environment, and escalation capabilities. |
| **Agent Workspace** | The canonical host project directory mounted read-write at `/workspace` in the Agent Sandbox. |
| **Agent Sandbox** | The rootless gVisor container in which an agent and its child processes execute. One sandbox is shared by all Client Sessions in a Domain. gVisor sentry, gofer, and guest processes are the sandbox, not the Session Coordinator. |
| **Agent Sandbox ID** | A runtime-unique identifier assigned to one Agent Sandbox instance and bound to its Domain protocol identity. |
| **Client CLI ID** | A runtime-unique identifier assigned to one host Lazaret CLI process. It is authenticated as a protocol identity and bound to one Client Session. |
| **Client Session** | One active host Lazaret CLI process and the interactive or non-interactive command it attaches to the Agent Sandbox. |
| **Session ID** | A cryptographically random identifier unique to one Client Session. |
| **Session Anchor** | An ephemeral host-only signing key whose public key binds developer decisions to a registered Session ID and owning Client CLI. |
| **Session Request Capability** | An ephemeral Session Coordinator-signed binding of one live Client Session to the exact Agent Sandbox generation and its protocol credentials. HC physically holds the signing key. It is a routing capability within the shared sandbox trust domain, not a process-isolation boundary. |
| **Session Coordinator** | The logical Domain role defined by the protocol model. The selected physical refinement maps it to Host Coordinator, Runtime Supervisor, and attached runsc processes. |
| **Session Coordinator ID** | A runtime-unique identifier for the logical Session Coordinator as a protocol peer, authenticated on the Host Coordinator face. Generation scoping and stale-credential refuse follow the protocol model. |
| **Host Coordinator** | The constitutive Session Coordinator process that runs in the host user and mount namespaces. It is the protocol face: Domain lock, durable state store, Session PTY masters, escalation mailbox and routing, publication and session admission, and lifetime authority over the Runtime Supervisor. |
| **Runtime Supervisor** | The constitutive Session Coordinator process that runs in the Domain generation's user, mount, and network namespaces under a Host Coordinator lifetime lease. It owns supervised filesystem and network resources for the generation, arms the parent-death edge to attached runsc, and launches the attached runsc client. |
| **Attached runsc** | The constitutive Session Coordinator process that is the non-detached `runsc` client child of the Runtime Supervisor. It supplies the causal coupling edge to the complete Agent Sandbox. |
| **Domain** | The shared runtime and persistent-state scope for one `(Agent Profile, canonical Agent Workspace)` pair. |
| **Domain ID** | A deterministic identifier derived from the Agent Profile name and canonical Agent Workspace path. It namespaces Domain resources but is not an authentication credential. |
| **Domain generation** | One attempt to prepare, publish, operate, and tear down or recover a Domain's transient runtime resources under a single Session Coordinator instance and durable generation identity. |
| **Domain Root** | The host-only directory containing persistent state and metadata for one Domain. |
| **Network Sidecar** | The logical Domain network-policy role for one Domain generation: derived-policy application, enforcement network-namespace preparation, connectivity-helper supervision, and network readiness attestation. Under the selected architecture this role is realized on the Runtime Supervisor-owned install path (with a supervised connectivity helper). It is not a constitutive Session Coordinator process and need not be a separate OS process. The Agent Sandbox never holds network-administration capability. |
| **Network Sidecar ID** | Protocol component identifier for the Domain generation's Network Sidecar role instance (not a Runtime Supervisor or connectivity-helper process id, and not a filesystem path). Generation scoping follows the protocol model. |
| **Connectivity helper** | The supervised process that provides user-space connectivity for the Domain enforcement network namespace. Lazaret v1 uses `slirp4netns`. Ownership and lease coupling follow the protocol model; process identity is product recovery material, not the Network Sidecar ID. |
| **Derived network policy** | The generation-bound policy document Lazaret derives from trusted host configuration and fixed product topology (default and profile allow/deny prefixes, connectivity-helper routes, address-family disposition). Only derived policy is installed; the Agent Sandbox never supplies policy. |
| **Network readiness fingerprint** | Product encoding of protocol network readiness: a cryptographic digest over Domain ID, generation, configuration fingerprint, Network Sidecar ID, derived-policy digest, and enforcement network-namespace identity material. |
| **Prepared lower** | A Lazaret-owned immutable root filesystem tree materialised from the selected base image. Content is identified by a prepared-artifact identity. |
| **Prepared-artifact ID** | A Lazaret-assigned identity for one immutable prepared-lower tree (content-addressed or otherwise unique among prepared lowers under the Storage Root). |
| **Prepared-lower lease** | Product binding of a Domain generation to a prepared-artifact ID for State Anchor use (not a container-engine mount refcount). Lease lifecycle follows the protocol model. |
| **Durable intent** | Protocol durable intent that Lazaret intends to create or has created a named external resource for a Domain generation (see protocol model). |
| **Publication** | Protocol publication of a Domain generation for Client Session registration and service (see protocol model). |
| **Git Sentry** | The protective mount layout that preserves bidirectional workspace and Git access while preventing writes to the host's default Git hooks and repository configuration. |
| **Ignored Workspace State** | Domain-scoped sandbox-local storage presented at Git-ignored Agent Workspace paths instead of exposing the corresponding host content. |
| **State Anchor** | The Domain-scoped persistent writable filesystem layer merged over selected paths from the sandbox base image prepared lower. |
| **Trust Anchor** | The ephemeral Domain-generation trust package containing separate TLS certificate-authority and protocol-credential issuer keys. |
| **Protocol Credential** | A Trust Anchor-issued binding of a protocol-signing public key to an exact Domain generation, component role, and runtime component ID. |
| **Protocol Identity** | An authenticated binding of a component role, Agent Profile, Domain ID, and runtime component ID. Identifiers, paths, filenames, and process IDs name resources but do not authenticate protocol peers by themselves. |
| **Escalation Client** | The Lazaret-provided executable through which a sandboxed process requests a host action. |
| **Escalation Mailbox** | Host-private, Domain-scoped regular-file message paths mounted into the Agent Sandbox for signed escalation requests and correlated results. |
| **Escalation Request ID** | A cryptographically random identifier used to correlate one host escalation request and response. |
| **Escalation Result** | The terminal response to an accepted Host Escalation, correlated by Escalation Request ID and carrying its outcome plus command exit status and output when execution occurred. |
| **Host Escalation** | A request by a sandboxed process for Lazaret to execute a developer-approved or auto-approved action with host authority. |
| **Configuration Fingerprint** | A cryptographic digest of the validated host configuration that created or joined a running Domain. |
| **Storage Root** | The trusted host directory beneath which Lazaret stores Domain Roots and profile-scoped state. |
| **Storage Catalog** | The versioned redb store for prepared artifacts, preparation operations, and cross-Domain generation leases. Domain coordinators serialize short catalog transactions with the Storage Catalog lock; no process keeps the catalog open as global runtime authority. |

## 3. Architecture

### 3.1 System Boundaries

```mermaid
flowchart TB
    subgraph Host[Trusted host]
        CLI[Client CLI]
        Config[Host configuration]
        HostWorkspace[Agent Workspace]
        HC[Host Coordinator]
        RS[Runtime Supervisor]
        Runsc[Attached runsc]
        State[State Anchor / FUSE]
        Net[Network policy + connectivity helper]
        Mailbox[Escalation Mailbox]
        HostExec[Approved host process]
    end

    subgraph Sandbox[Untrusted Agent Sandbox - rootless gVisor]
        Agent[Agent and child processes]
        Workspace[/workspace mount]
        Escalate[Escalation Client]
    end

    Config --> CLI
    HostWorkspace <--> Workspace
    CLI <--> HC
    HC --> RS
    RS --> Runsc
    Runsc --> Sandbox
    RS --> State
    RS --> Net
    HC <--> Mailbox
    Agent <--> Workspace
    Agent --> Escalate
    Escalate <--> Mailbox
    HC --> HostExec
    Agent --> Net
    Net --> Network[Permitted destinations]
```

The physical Session Coordinator refinement uses an HC→RS parent/child edge and
lifetime pipe. Before releasing the RS, the HC creates its user namespace through
`newuidmap` and `newgidmap` and verifies the live maps. Namespace ID 0 maps to the
invoking host UID or GID, and namespace IDs 1 through 65536 map to the lowest
configured contiguous subordinate allocation of at least 65536 IDs. The RS
creates the generation mount and network namespaces, arms the parent-death edge,
and launches a non-detached runsc client. Client CLI protocol descriptors
terminate in the HC process.

The Agent Sandbox uses gVisor's application-kernel isolation under rootless
operation. The product launches runsc directly through the HC→RS→runsc process
chain; an external container engine does not own the Domain's Agent Sandbox.
Rootless operation limits the host authority of runtime helpers, while gVisor
interposes a separate userspace kernel between untrusted processes and the host
kernel. Network policy installation and connectivity helpers are trusted and are
not part of the untrusted agent environment.

Lazaret is daemonless: it does not require a persistent global Unix service or
cross-Domain runtime authority that survives independently of Domain generations.
Runtime paths and durable rows carry Domain ID, generation, configuration
fingerprint, role identity, and physical ownership fields. Bootstrap recovery is
initiated by a host Lazaret CLI invocation, not by a resident scheduler.

### 3.2 Trusted Host Configuration Refinement

Rust configuration records and their codec tests own the closed v1 document
shape described by this refinement. Lazaret chooses its
configuration file from an explicit host CLI option or, when absent, from
`$XDG_CONFIG_HOME/lazaret/config.toml`, with
`$HOME/.config/lazaret/config.toml` as the XDG fallback. It derives the Storage
Root from `storage.data_root` when present, otherwise from
`$XDG_DATA_HOME/lazaret`, with `$HOME/.local/share/lazaret` as the fallback. The
Runtime Root is `$XDG_RUNTIME_DIR/lazaret`; v1 has no configuration field that
can redirect runtime control state elsewhere. Required XDG and home inputs must
be NUL-free host paths. An unset, empty, or relative XDG config or data value is
treated as unset and uses its home fallback; the home path and XDG runtime path
must be present and absolute. An invalid fallback or runtime value refuses
loading.

The caller supplies one profile name explicitly. Lazaret never selects the
first profile, infers a profile from an image or executable, or falls back to a
different profile. The canonical Agent Workspace is the existing directory
selected by the caller, normally the current working directory. Lazaret opens
it as a directory, obtains its canonical raw pathname and filesystem identity,
and retains the descriptor. The v1 Domain ID is SHA-256 over the
`lazaret-domain-id-v1` context followed by the selected profile name and
canonical workspace bytes, each framed by an unsigned 32-bit big-endian length.

The primary developer launch form is `lazaret <profile>`. It selects the current
working directory as the Agent Workspace and starts `/bin/bash` as a new
interactive Client Session. `lazaret <profile> -- <command> [arguments...]`
replaces that default with the exact supplied argument vector. Host options may
select another workspace or configuration source. The explicit
`lazaret run --profile <profile>` form has the same default and remains an
equivalent compatibility interface. `state` is reserved as the maintenance
command name; a profile with that name is launched through the explicit form.

The explicit configuration path follows this refinement's strict host-path grammar.
The loader resolves any declared symlink once to a canonical target and builds
a no-symlink confined plan to that target. The source is limited to 1,048,576
bytes, must be a regular file owned by root or the invoking user with exactly
one hard link, and must not grant group or other write permission. Lazaret first
opens it
with an O_PATH-style descriptor so validating the file type cannot activate a
special file, reopens that exact descriptor for nonblocking read, and compares
their identities. It records size and nanosecond change time, reads exactly the
recorded size into owned bytes, refuses trailing growth or a short read, reads
the same range a second time, and requires equal bytes and unchanged identity,
size, and change time before and after both reads. The loader never retries a
changed source. It then performs recursive strict TOML decoding and v1 dispatch.
No parser default or permissive flattening may make an unknown, duplicate,
aliased, or unknown-version field meaningful. Every profile is structurally
decoded, but filesystem and environment resolution applies only to the
explicitly selected profile.

Path resolution produces confined path authority, not an ambient absolute path.
It retains a validated ancestor directory descriptor and a normalized relative
suffix, records the ancestor's device, inode, and mount identity, and keeps
canonical raw pathname bytes only as a diagnostic label or digest input.
Lazaret-owned filesystem access and mutation use descriptor-relative opens with
beneath, no-magic-link, no-symlink, and no-mount-crossing resolution and
revalidate the expected identity and type. A trusted external component whose
interface requires a pathname may receive the canonical label only after
Lazaret reopens it through the plan and revalidates it at the handoff boundary.
A failed revalidation refuses the operation; it does not fall back to opening
the label as authority. Replacement by a trusted host process after a successful
handoff is ordinary host concurrency rather than Agent Sandbox authority.

Lazaret creates a missing Storage, Runtime, profile, or Domain root one path
component at a time beneath its retained existing ancestor. Every created
component has mode `0700`. Creation refuses symlinks, magic links, and child
mounts, and reopens each new component before proceeding. The selected root, if
it already exists, and every component Lazaret creates beneath the closest
existing ambient ancestor are Lazaret-owned: each must be a directory owned by
the invoking user with mode exactly `0700`. Ambient ancestors above that
ownership boundary use the same descriptor-relative confinement but need not
use Lazaret's ownership or mode; an ordinary `0755` home-directory ancestor
therefore does not by itself refuse loading. A creation or validation failure is
final for that load and never authorizes a partially resolved root.

The profile directory is the `profiles/<profile-name>` child of the Storage
Root. Persistent and runtime Domain roots use the lowercase hexadecimal Domain
ID beneath separate `domains` children of the Storage and Runtime Roots. Those
fixed layouts are created and mutated only through validated root handles.
Canonical labels may identify them at a trusted external pathname handoff only
after the exact root has been revalidated through its retained plan; a path
string or matching digest alone is not Lazaret filesystem authority over a root.

Configuration confinement compares canonical component ancestry and retained
filesystem identities after every source has been opened. The configuration
file, Agent Workspace, Storage Root, Runtime Root, and their Domain/control
trees may not overlap in either ancestor direction. Volume sources may be
strict descendants of the profile directory, but they may not overlap the
configuration source, Agent Workspace, runtime or Domain control trees, or one
another. Other volume sources must be disjoint from all Lazaret data and control
trees as well. All paths are reopened through their plans after the comparisons;
any identity or mount change refuses the complete load. Volume creation is
limited to a declared directory strictly beneath the profile directory and uses
the same component-wise `0700` creation rules.

Configuration resolution also requires a closed sandbox layout. Its
closed protected-destination set contains `/workspace` and every product-owned
sandbox mount destination selected by default bundle construction. Volumes and
protected trees may not overlap in either ancestry direction. Persistent paths
follow the same rule except that a bundle-classified exact transient mount may
replace a child of a persistent parent. The child remains protected and may not
itself contain or be selected as persistent state. The configuration loader does
not guess paths for control, credential, mailbox, proc, sys, dev, runtime, or
later product mounts, and a layout cannot be constructed without `/workspace`.
Bundle construction, rather than trusted-host configuration syntax, owns the
exact destination choices and transient-child classification.

An omitted profile `persistent_dirs` field selects `/root`, `/usr`, `/var`,
`/etc`, and `/opt`. An explicit list replaces that default in full, including an
empty list or paths used by an unorthodox distribution.

The optional `runtime.runsc_dcache` field sets the maximum number of
zero-reference dentries retained by the global runsc gofer-client cache in each
Domain sandbox. It defaults to 50,000 and accepts values from 0 through 262,144
inclusive; zero disables zero-reference dentry retention. The maximum keeps the
cache-entry ceiling at half of the 524,288 per-process descriptor budget,
leaving nominal headroom for referenced files and non-cache activity.
Configured capacity is allocated on demand, while populated capacity consumes
Domain-local sentry and routed-workspace descriptors and memory. Concurrent
Domains have independent caches and their host resource consumption is
additive.

The loader resolves environment references only after structural, path, and
network validation. A missing, non-UTF-8, or NUL-containing host value refuses
the selected profile. Resolved values live only in one move-owned,
non-serializable configuration authority whose diagnostics redact values. Only
reference names enter the configuration
fingerprint. Configuration bytes, nonselected profiles, and unreferenced host
environment values are not retained as runtime authority or copied into the
Agent Sandbox.

The Host Coordinator derives the selected profile's effective IPv4 policy and
Configuration Fingerprint from every normalized input that affects Domain
behavior, excluding resolved environment values as described above. IPv6 is
disabled for a v1 sandbox. Joining a running Domain requires the same Domain ID
and configuration fingerprint; the modeled configuration-mismatch path refuses
every other value.

For auto-approval, the configured executable resolves to one canonical path
outside every sandbox-writable or Lazaret control tree. That path, rather than a
`PATH` lookup or basename, is fingerprinted and matched. On every approved
execution the Host Coordinator reopens the current object through its confined
plan, requires a regular file with exactly one hard link, root or invoking-user
ownership, no group or other write permission, and an executable mode for the
invoking user, and passes that open descriptor into the causal launch wrapper.
The same checks apply when configuration is loaded. The wrapper
executes `/proc/self/fd/<inherited-descriptor>` while retaining that descriptor,
so pathname replacement after validation cannot select another object. There is
no shell, numeric descriptor supplied by the requester, ambient-path reopen, or
fallback execution path. Scripts are subject to the kernel's ordinary shebang
handling; the rule authorizes the exact opened script object, not an arbitrary
requester-selected interpreter.

The requested command argument vector is nonempty. Every element is UTF-8 and NUL-free;
element zero is an absolute path byte-equal to the rule's canonical executable,
and elements one onward are matched against the rule arguments. Lazaret performs
no `PATH` lookup. The v1 structured request language accepts no command-string
or shell-expansion form; an unsupported form cannot auto-approve. The launcher
never inserts or interprets a shell. An explicitly configured `/bin/sh -c ...`
vector can match only its exact configured rule. A directly configured script
continues to use ordinary kernel shebang handling for the same opened script
object.

Any shell-requiring request form, invalid executable, post-load path conflict,
or argument mismatch follows the modeled developer approval path or is refused;
it is never widened into automatic approval. Requiring one hard link rejects
hardlinked package layouts, including affected Nix-style binaries, in v1. This
is a deliberate conservative compatibility boundary. Relaxing it requires a
new executable-alias authority policy in a later version; v1 has no exception or
fallback.

Configuration resolution occurs before a generation, durable intent, external
runtime resource, or session admission relies on it. Across a process boundary,
a consumer may resolve configuration independently, but it must first match the
exact expected Domain ID and Configuration Fingerprint. A mismatch refuses
before creating or joining the generation. Each consumer uses one resolved
value for its subsequent path, network, environment, fingerprint, and approval
decisions; it does not combine decisions from different loads.

### 3.3 Domain and Session Lifecycle Refinement

The Host Coordinator implements Domain ownership with a non-blocking host
`flock`, Domain-scoped runtime paths, an exclusive Domain Store handle, and
generation identity records. Client CLIs reach the Host Coordinator through its
host-private protocol face rather than a global control plane.

Protocol lifecycle—startup, registration, cancellation, recovery, teardown,
publication, escalation, generation-scoped identities, durable intent, network
readiness, prepared-lower lease, and connectivity-helper ownership—is defined by
the [TLA+ application protocol model](protocol/Lazaret.tla). Product
implementation refines that model with physical resources (prepared-lower trees,
mounts, `slirp4netns`, PTYs, runsc clients, durable store encoding, and exact
ownership records). Physical recovery enumerates and inspects those resources
independently of process liveness.

#### Host process identity and causal acquisition refinement

Lazaret supports host-process authority on Linux x86-64 kernels at or above 6.9.
It checks the platform and kernel-version floor before a generation or external
runtime resource is created. Linux 32-bit, other architectures, and kernels
below 6.9 refuse. Required pidfd and pidfs operations fail closed at their point
of use; Lazaret does not attest, qualify, build, update, or roll back the running
kernel.

The v1 pidfs process identity separates three kinds of data:

- The boot ID plus pidfs device and inode is the only positive durable
  host-process authority. The boot ID is stored as the 16 UUID bytes in
  canonical UUID field order; both pidfs values are unsigned 64-bit values
  distinct from general filesystem device and inode identities.
- The host PID is an unsigned 32-bit lookup locator interpreted only in the host
  PID namespace where Host Coordinator and bootstrap recovery run.
- The unsigned 64-bit `/proc/<pid>/stat` start time is negative evidence.
  Equality of PID and start time adds no authority; inequality or an unreadable
  required observation refuses.

A retained pidfd is the primary live authority. Polling, waiting, signaling,
and termination act through that exact retained descriptor. Host process
control has no numeric-PID signal or reopen-and-signal fallback.

The causal child acquisition protocol applies to every Lazaret-owned child that
can become durable process ownership. Each Host Coordinator and Runtime
Supervisor has one exclusive in-process broker for all spawn, `SIGCHLD`, and
reap operations. The
process has default non-auto-reaping `SIGCHLD`; no same-parent spawn or reap and
no dependency process API bypasses the broker while acquisition is active. The
broker performs this sequence:

1. Persist the owning participant or terminal intent without positive process
   ownership.
2. Hold process-wide spawn/reap exclusion and create an inherited fail-closed
   launch barrier.
3. Spawn a direct repository-owned wrapper that blocks before target work;
   barrier EOF or malformed release exits without executing the target.
4. Capture the host-visible child PID, call `pidfd_open` exactly once, and call
   `waitid(P_PIDFD, WEXITED | WNOHANG | WNOWAIT)` on that descriptor. `ECHILD`
   or any other error refuses; `WNOWAIT` never reaps the child.
5. Call `fstatfs` on that exact pidfd and require `f_type == PID_FS_MAGIC`;
   any error or wrong magic refuses. Call `fstat` on the same descriptor; any
   error refuses. Read the current boot ID and diagnostic start time, and form
   the v1 pidfs process identity.
6. Persist staged ownership. For an RS-launched child, HC receives the complete
   staged ownership tuple and RS waits for an authenticated commit
   acknowledgement that echoes the same Domain, generation,
   generation-scoped coordinator ID, ownership role, and process identity.
   Lost, mismatched, unknown-version, unauthenticated, or duplicate
   acknowledgement after release is never success.
7. Release the wrapper barrier only after the exact staged ownership commit is
   acknowledged. The receiver consumes the acknowledgment once while that
   exact barrier is pending.
8. The wrapper arms its parent-death action, rechecks the expected parent pidfs
   authority to close the arming race, and execs the foreground,
   non-daemonizing target in place.
9. Promote ownership to committed only after target-specific readiness.
   Staged ownership cannot satisfy readiness, publication, dependent-resource
   creation, or adoption. It remains positive authority for exact same-handle
   cleanup and exact pidfs recovery matching, including bootstrap recovery.

Every durable host-process slot is exactly unassigned, staged with a current
pidfs process identity, or committed with current host-process ownership. Only a
current pidfs identity may be staged or committed. Current staged and committed
identity both authorize exact matched cleanup; only committed ownership may
satisfy an active role, readiness, publication, or adoption.

A role-bound participant is first committed as bare intent with no ownership
snapshot. Once physical acquisition begins, its role snapshot is present and
never returns to absent. Every non-process physical field is optional while
acquisition is partial; every process field uses the three-phase slot above.
During acquisition, optional fields move only absent-to-present. A newly
acquired child slot moves only from unassigned to staged to committed with the
exact same current identity. An already committed current owner or supervising
process may enter a newly created dependent-role snapshot directly, but that
recorded identity then remains immutable. Recorded evidence cannot be replaced
or cleared.
The direct existing-process edges are Network RS, Helper RS, Sandbox HC, and
Session Terminal HC. State Anchor daemon, Git-routing daemon, Helper process,
Sandbox RS, attached runsc, and Session Terminal exec client are acquired child
edges and require staging.
No bare intent moves directly to an active state: a non-empty acquisition
snapshot is committed first. Prepared-lower acquisition records lease intent
before catalog insertion and becomes lease-held only after that insertion.

An active prepared lower has a held lease; an active State Anchor and Git
router are prepared; and active network, helper, sandbox, and publication
ownership is committed. An active snapshot contains all role-required physical
evidence and current committed pidfs ownership in every required process slot.
A running Session Terminal likewise requires its
container, PTY, guest identity, and current committed HC and exec-client slots.
Staged or unassigned process ownership cannot satisfy either boundary.
Network readiness evidence must also name the enclosing generation and match
its policy, fingerprint, namespace, and committed RS identity internally.

Any partial or active snapshot moves to release intent while preserving every
recorded identity. A staged current identity remains exact cleanup and recovery
authority during release. Release becomes clean only after exact or independent
absence proof; that transaction clears every process slot to unassigned and
every optional physical field to absent. Clean retains the
logical generation key, role, and state as an explicit empty role snapshot. A
bare intent may become that explicit clean snapshot only after the sealed
runtime-absence check. No ordinary lifecycle transition may clear evidence or
produce clean state.

An exited, unreaped child remains pinned while acquisition completes. The
descriptor-based child check rejects a foreign replacement, while the exclusive
same-parent broker prevents a replacement child from passing the same-parent
control case. Implementations preserve these as safety conditions rather than
timing assumptions.

Exact pidfs recovery matching is the only positive recovery reacquisition path:

1. Read and validate the current boot ID.
2. On boot mismatch, do not look up the stored PID. Reconcile only resources
   whose independent exact ownership survives reboot.
3. Verify that the stored locator is a host-PID-namespace PID; nested or
   ambiguous mappings refuse before lookup.
4. Call `pidfd_open` exactly once for that locator. `ESRCH` or any other error
   cannot authorize process action.
5. Call `fstatfs` on that exact pidfd and require `f_type == PID_FS_MAGIC`;
   any error or wrong magic refuses and closes it without action. `fstat` the
   same descriptor and compare its device and inode exactly with the durable
   authority. Any error or either mismatch likewise refuses and closes it
   without action.
6. Apply start-time and expected namespace observations only as negative checks.
7. Use that same matched pidfd for every action. An action-time `ESRCH` or
   observation failure refuses without numeric fallback.

The contract accepts two residual assumptions: Linux boot-ID collision is
operationally negligible but not mathematically impossible, and the Linux 6.9+
boot-monotonic 64-bit pidfs inode counter does not wrap during one boot. Codecs
and comparisons support `u64::MAX` and refuse every unequal authority tuple;
they do not claim to recognize a hypothetical equal tuple after wrap.

#### Protocol cryptography refinement

Before starting the Agent Sandbox, the Host Coordinator creates one ephemeral
Trust Anchor package containing separate Ed25519 TLS-CA and protocol-issuer keys.
Its signed Trust Manifest binds both roots to the generation identity defined by
this specification and the protocol model. The Session Coordinator TLS and
protocol credentials use distinct leaf keys physically held by HC; the Agent
Sandbox uses another request-signing key. The publication identity pins the CA,
manifest, and coordinator TLS leaf in the validated host-private Domain path,
while the exact sandbox credential mount pins the same manifest. Protocol
credential IDs are SHA-256 digests of their signed claims. Session Coordinator
remains the logical protocol role; HC is its physical key holder, not another
principal.

The host-private protocol socket uses TLS 1.3 with the generation CA, fixed ALPN
`lazaret-control/1`, no early data, and no session resumption. A connection with
no client certificate may perform only a credential enrollment of at most 8,192
bytes from the trusted developer UID beneath that runtime directory. HC verifies
the signed CSR and issues a one-hour `clientAuth` leaf; all other operations
require a new mTLS connection whose leaf matches the issued Client CLI and
generation. The HC leaf is `serverAuth`-only for
`coordinator.lazaret.invalid`. Peer PID and process start time are not protocol
identity evidence.

The Client CLI keeps its Session Anchor private key in host memory. HC delivers
the signed Session Request Capability with guest execution and mounts the Agent
Sandbox signing key, credential, Trust Manifest, and Session Coordinator
verification credential read-only at the fixed credential path. No TLS,
protocol-issuer, coordinator-signing, or Session Anchor private key enters the
sandbox. HC unlinks the sandbox-key source after the running sandbox holds the
mount and retains only its public key.

All Trust Anchor and session cryptographic material is ephemeral. Normal teardown
withdraws publication before dropping keys and credential artifacts. HC loss
destroys the in-memory package; bootstrap never restores it into another
generation.

### 3.4 Session Terminals

The Host Coordinator owns one host PTY master per interactive Client Session. The
PTY slave is attached to non-detached `runsc exec` standard streams with a guest
TTY. The root attached `runsc run` client remains terminal-neutral and is not the
Session PTY attachment path. Lazaret does not depend on `runsc exec
-console-socket`.

Session terminal ownership is the Host Coordinator; a Client CLI never inherits
the sandbox Session PTY. For each Client Session the coordinator maintains the
session identity needed for routing and cleanup, including Session ID, PTY master,
`runsc exec` client process identity, and guest process or process-group identity.

Interactive terminal control requires:

- Each interactive command starts as the leader of a generation-bound guest
  process group. The Host Coordinator records both the leader PID and process
  start time and the process group ID relative to the exact runsc container
  before admitting terminal events.
- Window resize applies `TIOCSWINSZ` to the host PTY master and then delivers
  guest `SIGWINCH` to that process group through runsc. Rows and columns are
  nonzero unsigned 16-bit values; pixel dimensions may be zero when unknown.
- Client `Interrupt`, `Quit`, and `Suspend` events translate respectively to
  `SIGINT`, `SIGQUIT`, and `SIGTSTP` for that process group. Raw control bytes do
  not substitute for these events. Host CLI suspension is local: the CLI
  restores its terminal before stopping itself and sends the current window size
  after resuming; it does not synthesize a guest signal.
- Per-session exit status comes from the non-detached `runsc exec` client. An
  interactive PTY produces one merged output byte stream, so the protocol does
  not label its bytes as separate stdout and stderr streams.

Disconnected Client Sessions close rather than reattach to an unbounded scrollback
owned by the coordinator.

The session connection carries the terminal events and messages described by
this refinement. Rust protocol records and fixed codec tests own their v1
encoding. One Host Coordinator event loop serializes input, resize, signal,
close, prompt-routing, PTY output, and exec-client completion for each Session
ID. It uses bounded queues and PTY
backpressure; terminal data for one session cannot consume another session's
control capacity. Input, resize, and signal events are accepted only while the
modeled terminal route is the sandbox route. An invalid Session ID, inactive
route, stale generation, or terminal in release refuses the event.

PTY output is forwarded only while the modeled terminal route is the sandbox
route. During `Prompt` or `HostProcess` routing the Host Coordinator stops reading
the PTY master and relies on bounded kernel PTY buffering and backpressure; it
does not accumulate an unbounded user-space queue. Forwarding resumes only after
the model restores the sandbox route.

Normal guest completion begins the modeled session close and physical release,
so no new terminal or escalation event is admitted. The Host Coordinator
first cancels any active prompt or exact host process and serializes that
cancellation before terminal output. It then collects and reaps the exec client,
drains and forwards PTY bytes in order until EOF or a bounded drain deadline,
and emits at most one `SessionExit` after the last forwarded byte on the closing
connection. This close handshake does not restore session routing. If the
connection is already lost, the outcome is not retained for reattachment.

Physical Session Terminal acquisition is ordered as follows:

1. The Host Coordinator records terminal intent in the Domain Store.
2. It allocates the PTY and starts the exec wrapper through the causal child
   acquisition protocol with the expected committed HC pidfs authority.
   The wrapper arms its HC parent-death edge, rechecks that authority, and aborts
   before invoking runsc if it differs. It may create the guest process only
   after staged exec-client ownership is durably committed and the barrier is
   released.
3. It establishes the guest process group and obtains the guest leader PID,
   start time, and group ID.
4. One Domain Store transaction promotes the exact Host Coordinator and exec
   client ownership to committed, records the PTY, container, guest leader, and
   guest process-group identities, and marks the Session Terminal running.
5. Only then may the Host Coordinator accept terminal events for the session.

Failure before the running state never admits the terminal. A live Host Coordinator uses
its in-memory exact handles to terminate any partial exec and guest group and
records release intent. If HC itself is lost, the armed exec edge stops the host
client and the generation lease-loss path stops the guest sandbox; bootstrap
recovery cleans the retained Intent only after runtime absence.

Session close, Client connection loss, PTY loss, or exec-client loss starts the
same physical release:

1. Apply the modeled session close, remove terminal and escalation routing, and
   record terminal release intent while retaining all exact identities.
2. If the exact generation is still serviceable and the guest leader identity
   and group still match, send `SIGHUP`, wait for a bounded grace period, then
   send `SIGTERM`, wait again, and send `SIGKILL` if the group remains. A leader
   mismatch refuses the numeric process-group signal. If the leader is absent,
   an empty recorded group needs no signal; a nonempty group is left in release
   intent for Domain teardown.
3. Terminate and reap the exact exec client when it is still a Host Coordinator
   child and close the exact PTY master. Record the terminal clean only
   after the guest group, exec client, and PTY are absent; otherwise retain
   release intent.

The process-group boundary is the per-session cleanup contract, not a security
boundary. A sandbox process may daemonize or move into another process group;
the final Client Session leaving the Domain triggers Domain teardown, which is
the containment boundary for such processes.

Hard Host Coordinator loss closes its PTY descriptors and fails modeled open
sessions; the exec-client lifetime edge prevents an unrecorded or recorded exec
client from surviving that loss. The surviving Runtime Supervisor follows the
generation lease-loss teardown: it stops the complete Agent Sandbox, unmounts
the exact State Anchor while retaining the prepared-lower lease, and exits.
Bootstrap recovery waits until the Runtime Supervisor and attached runsc are
absent, never recreates a PTY or reattaches a Client Session, releases the
retained prepared lower under the durable generation refinement, verifies that
the exact generation container and guest processes are gone, terminates any
still-live exact exec-client host process, and then records each retained Session
Terminal clean. Intent without physical identities becomes clean only
after that runtime-absence check. A process, container, PTY, or generation
mismatch fails closed and retains the record; it is never adopted or signaled as
the recorded session.

### 3.5 Filesystem and Git Model

The Agent Workspace is mounted read-write. Tracked paths and untracked paths that
are not ignored propagate in both directions. The Git index, `HEAD`, references,
and objects are shared with the host in real time. Lazaret does not create a
separate worktree or branch and does not promise that the host working tree
remains unchanged.

By default, paths matched by the repository's effective Git ignore rules are
redirected to Ignored Workspace State. Existing host content at those paths is not
exposed to the Agent Sandbox, and sandbox writes remain Domain-scoped and persist
across restarts. This prevents agent-modified dependency trees, virtual
environments, generated executables, caches, and other ignored artifacts from
later being executed by host tools. Trusted host configuration may disable this
behavior when fully bidirectional ignored paths are required.

#### Ignored Workspace State routing contract

Lazaret v1 routes Ignored Workspace State through a dedicated rootless host FUSE filesystem.
It presents
one workspace tree and chooses exactly one backing for each pathname operation:
the canonical Agent Workspace for tracked and ordinary non-ignored paths, or the
Domain's Ignored Workspace State for ignored untracked paths. The `.git` entry is
host-backed, subject to the Git Sentry mounts below. Classification uses Git's
effective byte-path rules, including repository and nested `.gitignore` files,
negation and precedence, the applicable common-directory `info/exclude`, the
configured global excludes file, tracked-index state, linked worktrees, nested
repositories, and `core.ignoreCase`. Non-UTF-8 path components are supported as
opaque bytes; NUL and `/` retain their ordinary pathname meaning and cannot be
components.

Each pathname operation uses one immutable classification snapshot. Publication
of a changed index or ignore input serializes against new pathname operations and
either installs one complete new snapshot or leaves the prior snapshot active.
There is no partially updated matcher. Existing file descriptions, mappings,
locks, and directory streams remain pinned to the backing object and snapshot
under which they were opened. A subsequent lookup or open uses the current
snapshot. Writes, flushes, locks, and mapping writeback through an old handle
affect only its original backing object; a transition never rebinds a handle or
copies its content to the other backing.

Directory lookup and enumeration expose only the entry selected by the current
snapshot. An ignored host entry is hidden even when no isolated entry exists. A
stale isolated entry is retained but hidden while its pathname is host-backed.
On a non-ignored-to-ignored transition, subsequent lookups expose the retained
isolated entry or absence and hide the host entry. On an
ignored-to-non-ignored transition, subsequent lookups expose the host entry or
absence and retain the isolated entry hidden. Neither transition imports,
exports, merges, deletes, or otherwise copies content between backings.

A same-backing `rename` or hard link has the backing filesystem's atomicity and
error behavior. If the source and destination route to different backings,
`rename`, `RENAME_NOREPLACE`, `RENAME_EXCHANGE`, and hard link return `EXDEV`
before either backing is changed. `RENAME_WHITEOUT` returns `EOPNOTSUPP` without
mutation. Lazaret never reports a copy-and-unlink sequence as a successful
rename or a copied file as a hard link. Applications may react to `EXDEV` with
their own visible copy and unlink operations.

An index publication that would make an isolated object tracked is accepted only
when a type-compatible host worktree object already exists independently. The
router then selects that host object and retains the isolated object hidden; it
does not compare, merge, or copy isolated bytes. A guest index-lock rename that
would instead create a tracked path with only an isolated object returns `EBUSY`
before replacing the index. If an unmediated host index change creates that
state, pathname access to the inconsistent path fails with `EIO` until the host
index/worktree tuple is made consistent or reverted. The isolated object remains
recoverable Domain state. Consequently, ordinary add and commit are
supported for host-backed paths, while force-adding an isolated-only path is an
explicitly unsupported Git operation rather than implicit host copy-back or
silent disappearance.

The v1 operation contract supports lookup, bytewise directory enumeration,
regular-file and directory creation, open, read, write, truncate, allocation,
sync, unlink, and same-backing rename and hard link. It supports symbolic links
without following a backing symlink during routing, nanosecond timestamps,
`user.*` extended attributes, POSIX ACLs where the backing filesystem supports
them, sparse-file hole/data queries and hole punching, same-backing copy range,
shared and private mappings, BSD `flock`, POSIX record locks, FIFOs, and Unix
domain sockets. Cross-backing copy range returns `EXDEV`. Character and block
device creation returns `EPERM`. Backing filesystems may return their native
documented unsupported error for an optional feature, but the router may not
turn a partial operation into success or fall through to the other backing.

The supported Git contract covers status, diff, ordinary add and reset, commit,
checkout and restore, branch and reference updates, merge, rebase, stash,
worktree-local index locking, linked worktrees, and nested repositories. These
operations retain Git's ordinary conflict and concurrent-writer behavior. Git
Sentry still makes host `.git/config` read-only and replaces default
`.git/hooks` with sandbox-local transient storage. Force-adding an isolated-only
path, cross-policy atomic rename, and device-node creation are refused as defined
above and are not compatibility promises.

The repository `lazaret-ignored-workspace-contract-v1` corpus is a
non-authoritative executable test inventory derived from these semantics. It
covers ignore precedence and live changes, non-UTF-8 and case-folded matching,
linked worktrees and nested repositories, every operation class above,
open-handle transitions, concurrent host and sandbox mutation, router loss, and
absence of silent loss or copy-back.
Its benchmark protocol compares direct-host and routed placements using identical
fresh fixture materialization and reports metadata, Git, offline package
installation, and offline build results. Exact observed hardware, storage,
filesystem, kernel, and tool versions belong in generated run metadata.
Qualification constraints, sampling rules, variance checks, and numeric budgets
in fixtures are engineering evidence and regression targets, not product
conformance requirements.

Ignored-path isolation is defense in depth and does not replace the mandatory Git
Sentry protections below.

Lazaret applies narrow protective mounts over host integration files that must not
be modified by the agent:

- The host repository's `.git/config` is exposed read-only.
- The host repository's `.git/hooks` is hidden behind sandbox-local transient
  storage.
- Supported host editor configuration directories may be hidden behind
  sandbox-local transient storage.

These protections do not make the workspace immutable. Their purpose is to stop
the sandbox from writing the protected host Git configuration and default hook
directory while preserving normal Git operations and bidirectional source edits.

### 3.6 Persistent Sandbox State

The State Anchor preserves developer tooling and selected sandbox system paths for
one Domain. It combines a Lazaret-owned prepared lower from the selected base
image with a Domain-scoped writable upper directory.

#### Prepared lower

Preparation resolves the selected base image, applies layers with a supported
OCI-aware preparer, and materialises an immutable Lazaret-owned root filesystem
tree under the Storage Root. The tree carries a prepared-artifact ID and a source
image identity. A live container-engine image mount cannot serve as the State
Anchor lower. Archive export alone is not a complete preparation boundary;
container tooling may participate only as transport into Lazaret-owned
preparation. Lazaret does not use an unsupported ad hoc tar extractor.

Prepared-artifact identity is independent of its storage pathname. The Domain
Store and Storage Catalog encode the model's generation-to-artifact lease with
separate Domain and generation fields; an engine mount refcount is not its
physical representation. Preparation uses descriptor-relative staging,
publication, quarantine, and deletion beneath validated Storage Root handles.
Materialisation runs in a short-lived preparation worker under the same verified
user-namespace map used by the Runtime Supervisor. It applies logical image
ownership inside that namespace, so nonzero image UIDs and GIDs become
subordinate host IDs without granting initial-user-namespace authority.

The prepared rootfs preserves OCI modes and is exposed only as a read-only State
Anchor lower. Lazaret enforces immutability through artifact ownership and
lifecycle rather than by rewriting image permission bits.

#### Durable generation document refinement

Durable Domain state is an embedded store opened exclusively by the Host
Coordinator process that holds the Domain's exclusive lifecycle lock for write.
No other process opens the store for read or write: Client CLIs, the Runtime
Supervisor, recovery observers, and status tools obtain state only through Host
Coordinator IPC or by becoming the lock-holding Host Coordinator. Domain flock
serializes which process may be that exclusive opener. Store mutations use
atomic transactions; an interrupted write leaves the last successfully committed
document, never a half-applied generation decision.

Protocol durable decision vocabulary, multi-role intent, and mismatch refuse are
defined by the protocol model. The v1 store encodes that generation document
in typed tables under a store version (unknown versions fail closed before
row interpretation), including generation identity,
minted runtime component IDs, and participant ownership material (for example
prepared-artifact ID, staged or committed pidfs process ownership, mount
identity, and network readiness fingerprint).
Prepared lower, State Anchor, Git routing, network, connectivity helper, sandbox,
and publication ownership remain independently represented. Connectivity-helper
ownership independently
records durable intent and exact committed connectivity-helper pidfs ownership
before network ownership records readiness. Sessions and the generation mailbox
are separate generation records. Deterministic paths are lookup hints for
physical recovery, not ownership proofs.

Rust durable records and their codec tests own the store row shapes described
by these refinements. Implementations must preserve the distinct Domain Store
and Storage Catalog authority boundaries and the independently recoverable
ownership described above.

Lazaret v1 stores the catalog in redb. Each catalog operation holds the
host-wide Storage Catalog lock for one bounded open, transaction, and close
section. The lock covers lease changes, prepare publication, and transition to
reclamation. This permits concurrent Domain coordinators without a persistent
global daemon or concurrent catalog opens.

The physical lease-acquisition refinement is:

1. Commit prepared-lower intent in the Domain Store with the intended
   prepared-artifact identity.
2. Under the Storage Catalog lock, insert the exact `(prepared-artifact ID, Domain
   ID, generation)` lease in one catalog transaction.
3. Commit that the prepared-lower lease is held in the Domain Store.
4. Commit State Anchor intent, create the exact mount, and then commit prepared
   State Anchor ownership with its mount identity.

The physical unmount and lease-release refinement is:

1. Commit State Anchor release intent while retaining its exact mount and
   prepared-artifact identity.
2. Verify the recorded mount identity and unmount it. A mismatched mount refuses
   release and remains untouched.
3. After independently observing that the exact mount is absent, atomically
   commit clean State Anchor state and prepared-lower release intent in the
   Domain Store.
4. Under the Storage Catalog lock, recheck the matching Domain release intent and
   absence of the exact mount, then remove only the exact generation lease in one
   catalog transaction.
5. Commit clean prepared-lower state in the Domain Store.

Host Coordinator hard loss uses the model's split lease-loss refinement. The
surviving exact Runtime Supervisor stops the sandbox and sidecar, verifies and
unmounts its exact State Anchor, and exits without opening the Domain Store or
Storage Catalog. The original durable anchor intent and exact Prepared ownership
authorize rollback of the resource the supervisor created; they do not authorize
catalog lease removal. The catalog lease remains held after unmount.

Bootstrap recovery begins only after the Runtime Supervisor and attached runsc
are absent. If the exact mount remains, the bootstrap Host Coordinator records
State Anchor release intent and completes normal exact unmount. If the
surviving Runtime Supervisor already unmounted it, bootstrap independently
verifies exact mount absence. It then atomically commits clean State Anchor
state and prepared-lower release intent, removes the exact catalog lease under
the catalog lock, and commits clean prepared-lower state. Thus lease-loss
unmount and lease release are distinct: only a lock-holding Host Coordinator
releases the prepared-lower lease.

Recovery resumes only from matching durable identity. State Anchor release
intent retains the catalog lease while recovery verifies and completes the
unmount. Prepared-lower release intent permits removal of a still-present exact
catalog lease only after the exact mount is absent; an already-absent lease
permits the Domain ownership to become clean. A catalog lease with missing,
unreadable, non-release, or mismatched Domain evidence is retained and reported.
A Domain record claiming a held lease whose exact catalog lease is absent is
inconsistent and fails closed; recovery neither recreates the lease nor mounts
the State Anchor. A failed generation with a prepared anchor, an absent exact
mount, and a still-present exact catalog lease is the conservative HC-loss
state above; only bootstrap recovery may advance it to release intent. These
rules make every interrupted release conservative and prevent a mounted State
Anchor from becoming unleased.

Store version acceptance occurs before row interpretation or physical resource
inspection. The first product Domain Store identity is
`lazaret-domain-store-v1` at version `1`; unversioned, unknown, older, and newer
metadata refuses without fallback.

Files not represented in the upper layer follow the selected base image. Files,
directories, and whiteouts recorded in the upper layer remain authoritative when
the lower image changes. This permits installed tools to survive restarts while
allowing unmodified base-image content to follow the selected image.

Persistent state is sandbox state, not host configuration. It must not contain or
override Lazaret's host control plane.

### 3.7 Network Isolation

This section refines physical network mechanisms below the protocol model's
`networkReady` abstraction. The model owns helper intent, sandbox lifetime,
readiness, publication, and session-admission ordering.

| Concern | Physical refinement |
| :--- | :--- |
| Policy owner | The Network Sidecar role is realized on the Runtime Supervisor install path. Driving nftables through runsc into the guest is unsupported. |
| Connectivity | Lazaret v1 uses supervised `slirp4netns`. |
| Network authority | The Runtime Supervisor holds network-administration capability only while preparing, importing, and attesting the enforcement namespace. Successful physical attestation requires its irreversible drop. |
| Trusted runtime | Stock attached runsc may retain network-administration capability only in the subordinate Domain user namespace. It has no initial-user-namespace network authority. |
| Agent Sandbox | The OCI process joins only the prepared enforcement namespace, never the host network namespace, and receives no network-administration capability. |

#### Derived policy and readiness encoding

Rust network records and fixed codec tests own the v1 policy, attestation,
readiness-identity projection, and fingerprint encodings described by this
refinement.

| Encoding boundary | v1 mechanism |
| :--- | :--- |
| Policy transport | Canonical bytes in a write-sealed inherited memfd; the Runtime Supervisor verifies seals and digest. |
| Evidence transport | Observed route, helper, process, and namespace evidence over an inherited Host Coordinator-created private `SOCK_SEQPACKET` channel. |
| Independent identity | The Host Coordinator reads the Runtime Supervisor's enforcement namespace identity directly. |
| Durable encoding | The network readiness fingerprint binds the generation, configuration, policy, role, and namespace identities. |

The fixed v1 topology is:

| Purpose | Value |
| :--- | :--- |
| Reserved topology | `10.137.54.0/23` |
| `slirp4netns` network | `10.137.54.0/24` |
| Gateway | `10.137.54.2` |
| Synthetic DNS | `10.137.54.3` |
| Sandbox address | `10.137.54.100` |
| Canary network | `10.137.55.0/29` |
| Enforcement endpoint | `10.137.55.1` |
| Allowed canary endpoint | `10.137.55.2` |
| Denied canary endpoint | `10.137.55.3` |

A configured allow intersecting the reserved topology, or a configured deny
within it at `/23` or greater specificity, is invalid. Broader denies remain
valid and Lazaret's fixed more-specific routes take precedence. Lazaret passes
the `slirp4netns` CIDR explicitly.

The protocol model treats the following physical refinement as the atomic
`MarkNetworkReady` action:

| Evidence boundary | Required observation |
| :--- | :--- |
| Linux policy state | A versioned policy-semantic rtnetlink projection exactly matches derived policy and fixed topology. It includes destination, table, next-hop, and precedence semantics, but excludes counters, cache state, and presentation. IPv6 is disabled, with no non-loopback IPv6 address or route. |
| Known-live control | Both canary endpoints authenticate independent generation-bound challenges before policy installation. Final policy has an aggregate loopback-unicast canary deny and a more-specific allowed `/32`. |
| Imported behavior | A static, closed-environment non-user root init verifies canary and `tap0` identity, authenticates the allowed endpoint, cannot reach the known-live denied endpoint, observes no non-loopback IPv6 address or route, has empty network-administration capability sets, and cannot mutate a route. |
| Exact cleanup | With no concurrent link mutator, the Runtime Supervisor closes responder and peer-namespace descriptors and deletes the veth only when its current rtnetlink shape matches its versioned creation record. Namespace and ifindex alone are insufficient. |
| Cleanup observation | The formerly allowed endpoint is unreachable, `tap0` remains present, and IPv6 disposition is unchanged. |
| Authority drop | The Runtime Supervisor irreversibly drops network-administration capability. No canary listener, peer namespace, or host interface remains. |

Any failed or mismatched predicate refuses physical attestation. The root init
is product-owned, statically linked, has no ELF interpreter or dynamic section,
receives a closed product environment, and never receives profile environment.
The canary adds no durable process role.

Network readiness never depends on a DNS response, public egress, or
availability of a configured permitted destination. Lazaret v1 supplies the
protected sandbox resolver configuration and route for the slirp4netns
synthetic DNS endpoint; upstream resolver failure is an ordinary runtime
connectivity failure. Persisted readiness files are evidence after this
exchange, not its transport.

#### Default policy and deny representation

IPv4 destinations are permitted by default except for the RFC 1918 private
address ranges (`10.0.0.0/8`, `172.16.0.0/12`, `192.168.0.0/16`), which are denied
by default. Explicit, more-specific allow rules may grant access within those
ranges. Lazaret also installs the fixed connectivity-helper routes needed for
the slirp4netns gateway and synthetic DNS endpoint. Those routes and their
precedence over the default RFC 1918 deny are explicit inputs to the canonical
derived policy and its digest, not post-install route exceptions. Other
permitted and denied destination prefixes come from trusted host configuration.

Default and configured deny prefixes are enforced with **loopback-unicast deny
routes** in the Domain enforcement network namespace (routes that direct matching
destinations to a loopback unicast address so packets are not forwarded). Linux
`blackhole` routes are not used for denial on this path.
Equal-prefix allow/deny conflicts must be rejected or resolved in favor of denial.

Normal Linux longest-prefix routing determines the most specific matching route.
Lazaret v1 disables IPv6 in the Linux enforcement namespace before helper and
canary setup and requires both the Linux namespace and imported sandbox view to
have no non-loopback IPv6 address or route. The sandbox-visible check does not
depend on Linux sysctl files because gVisor need not expose them.

The OCI configuration joins only the Domain enforcement network namespace, and
`slirp4netns` attached to that namespace is the sole external egress mechanism.
Dynamic policy changes are outside the current physical refinement.

### 3.8 Host Escalation

The Escalation Client exchanges request and result records through the
Escalation Mailbox: regular files written by atomic rename beneath host-private,
Domain-scoped paths. Request and result paths may use different mount modes. The
mailbox is not an authentication boundary. Its paths include Domain and
generation identity and are opened through Host Coordinator-owned directory
handles. Host-only CLI/coordinator control may use host-private Unix sockets that
are never mounted into the Agent Sandbox.

Mailbox files carry the signed protocol records described by this refinement;
Rust protocol records and fixed codec tests own their v1 encoding. TLS is not
layered over the regular-file transport. HC opens each ready entry relative to a
confined directory handle,
rejects links and non-regular files, bounds the complete file before allocation,
and reads it once. It verifies the signature over those owned bytes before
parsing. Pathnames, file ownership, mailbox identity files, PIDs, and start times
are not authentication evidence.

Requests, cancellations, acknowledgements, developer decisions, chunks, and
terminal results use the signer relationships defined by the protocol
cryptography refinement. The v1 wire format uses Postcard payloads and signs
`lazaret/v1/`, the lower-kebab record name, the exact encoded length, and the
encoded bytes. A complete record is at most 65,536 bytes; a result chunk
contains at most 49,152 output bytes.

The Escalation Client acknowledges the highest contiguous result sequence with an
Agent Sandbox signature. HC retains at most eight unacknowledged chunks per
request and pauses the exact host process's output pipes at that bound. Session
loss, cancellation, or acknowledgement timeout terminates and reaps the process
before removing its result files.

The physical host-process launcher invokes an executable with an argument vector
and contains no shell-expansion path.

Escalation authentication, correlation, approval, execution, cancellation, result
delivery, and terminal routing are defined by the
[TLA+ application protocol model](protocol/Lazaret.tla).

### 3.9 State Inspection and Reset

The host CLI provides read-only discovery, inspection, structural verification,
and explicit reset operations for Domain State Anchors. These operations resolve
a Domain through trusted host metadata and never accept an arbitrary host
filesystem path as an upper-layer target.

Inspection reports metadata and overlay changes without printing file contents by
default. Structural verification requires an inactive Domain and exclusive
lifecycle ownership so its result is not invalidated by concurrent writes. A
reset may target one configured persistent container path or all State Anchors in
the Domain. It discards the selected upper-layer state so the next launch follows
the current prepared lower; it does not modify the prepared lower artifact, Agent
Workspace, Ignored Workspace State, or unselected State Anchors.

Reset is permitted only after Lazaret holds the Domain's exclusive lifecycle lock
and has established that no Client Session, Session Coordinator constitutive
process, sandbox, network helper, host process, or overlay mount is using the
selected state. Confirmation flags may suppress the human prompt but may not
bypass these safety conditions. Reset must be crash-consistent and must never
follow a symlink outside the Domain Root.

## 4. Requirements

These requirements cover physical mechanisms and encodings below the TLA+
abstraction boundaries. Modeled safety and liveness requirements are intentionally
not duplicated here.

### 4.1 Security Requirements

| ID | Requirement |
| :--- | :--- |
| **SR-1** | Agent processes shall execute in a rootless gVisor sandbox and shall not receive host root authority. |
| **SR-3** | Host paths outside the Agent Workspace, developer-configured volumes, and Lazaret-owned fixed control mounts shall not be accessible to the Agent Sandbox. |
| **SR-4** | The sandbox shall be unable to modify the host repository's `.git/config` or default `.git/hooks` directory through the workspace mount. |
| **SR-5** | Successful physical network attestation shall require the Runtime Supervisor's irreversible network-administration capability drop. Trusted attached runsc may retain that capability only in the subordinate Domain user namespace. The trusted init and Agent Sandbox process specifications shall omit the capability and set `noNewPrivileges`. |
| **SR-6** | Network policy shall cover every enabled address family and shall deny equal-specificity policy conflicts. Default and configured deny prefixes shall be enforced with loopback-unicast deny routes in the Domain enforcement network namespace; Linux blackhole routes shall not be used for denial on this path. |
| **SR-10** | Domain sockets, mailboxes, and coordination files shall reside in a host-private directory owned by the developer. |
| **SR-11** | Runtime and persistent path construction shall begin from validated Domain roots, include the Domain ID in resource identities, and verify stored Domain identity before reuse. |
| **SR-12** | The Host Coordinator shall launch preparation workers and the Runtime Supervisor in independently verified caller-configured user namespaces whose ID maps bind namespace ID 0 to the invoking host identity and namespace IDs 1 through 65536 to configured subordinate IDs. The runsc OCI specification shall create private PID, IPC, UTS, and mount namespaces, join the independently verified Runtime Supervisor network namespace descriptor, and omit a nested user namespace and OCI UID/GID mappings. It shall contain no host namespace path entry. |
| **SR-13** | Git-ignored Agent Workspace paths shall use Ignored Workspace State by default, preventing the sandbox from reading or modifying corresponding host content; only trusted host configuration may disable this behavior. |
| **SR-14** | State Anchor maintenance shall remain confined to the resolved Domain Root. Destructive maintenance shall require exclusive lifecycle ownership and an inactive, unmounted target. |
| **SR-15** | Lazaret shall not use a live container-engine image mount as the State Anchor lower; the lower shall be a Lazaret-owned prepared lower. Archive export alone shall not be treated as a complete preparation boundary. |

### 4.2 Functional Requirements

| ID | Requirement |
| :--- | :--- |
| **FR-1** | Lazaret shall derive a stable Domain ID from the selected Agent Profile and canonical Agent Workspace. |
| **FR-3** | Tracked and non-ignored workspace edits and supported Git operations shall propagate bidirectionally between host and sandbox. |
| **FR-4** | Selected sandbox paths and Ignored Workspace State shall persist across Domain restarts without copying Lazaret host configuration into the sandbox. |
| **FR-7** | Product recovery shall inspect external runtime resources independently of owner-process liveness. Host-process action shall require a retained pidfd or exact pidfs recovery match against staged or committed current process identity; unequal pidfs authority, boot or namespace ambiguity, and unreadable negative evidence shall refuse without numeric-PID signaling. Staged ownership authorizes only exact cleanup/recovery, never service or adoption. Recovery shall also compare namespace, mount, artifact, path, and inode evidence before physical cleanup. |
| **FR-8** | Lazaret shall support interactive terminal sessions without degrading supported host terminal capabilities. |
| **FR-9** | Trusted host configuration shall allow the developer to disable Git-ignored path isolation for an Agent Profile. |
| **FR-11** | The host CLI shall list, inspect, structurally verify, and reset all or selected State Anchors without requiring direct manipulation of Lazaret's storage layout. |
| **FR-14** | The Host Coordinator shall own one host PTY master per interactive Client Session; the PTY slave shall attach through non-detached `runsc exec` standard streams. The root attached `runsc run` client shall remain terminal-neutral. Session PTYs shall not depend on `runsc exec -console-socket`. |
| **FR-15** | For each interactive Client Session, Lazaret shall preserve the durable terminal authority and protocol described by the Session Terminal refinement; serialize bounded terminal events and merged output by Session ID; map resize and the `Interrupt`, `Quit`, and `Suspend` events to the specified exact process-group operations; collect exit status from the non-detached `runsc exec` client; and follow the specified release and hard-loss recovery ordering without reattachment or mismatched cleanup. |
| **FR-16** | Lazaret v1 shall use supervised `slirp4netns` with the explicit product CIDR as the Domain connectivity helper. |
| **FR-17** | The Domain Store shall be opened only by the Host Coordinator process holding the Domain `flock`; mutations shall use atomic transactions. Storage Catalog access shall use one bounded lock/open/transaction/close section. Cross-store lease release shall follow the durable release-intent, exact-unmount, catalog-delete, Domain-clean ordering defined by the durable generation refinement. |
| **FR-19** | The Host Coordinator shall derive generation-bound network policy from trusted host configuration; the Runtime Supervisor shall install only that derived policy and attest readiness by observed namespace state. Durable network participant state shall record the network readiness fingerprint. |
| **FR-20** | Physical network readiness shall use product-owned known-live targets. DNS, public egress, and configured destination availability shall not gate it. |
| **FR-21** | The Domain Store and Storage Catalog shall preserve the independently recoverable ownership, identities, and authority relationships described by the durable-generation and prepared-lower refinements. |
| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. |

### 4.3 Developer-Experience Requirements

| ID | Requirement |
| :--- | :--- |
| **DX-1** | `lazaret <profile>` shall launch the explicitly named Agent Profile in the current workspace and start `/bin/bash` as a new interactive Client Session. A trailing `-- <command> [arguments...]` shall replace that default with the exact supplied argument vector. |
| **DX-2** | Tools installed in configured persistent sandbox paths and dependencies stored in Ignored Workspace State shall remain available on later launches of the same Domain. |
| **DX-3** | Normal source editing, `git status`, staging, committing, and reference updates shall work from inside the Agent Sandbox. |
| **DX-4** | Escalation prompts shall identify the requesting profile, session, command, and justification without mixing terminal input or output between sessions. |
| **DX-5** | Failures shall report actionable diagnostics and shall not leave the developer's terminal in a corrupted mode. |
| **DX-6** | State inspection shall provide human-readable and machine-readable output without exposing persisted file contents by default, and reset shall show its resolved Domain and exact scope before confirmation. |

### 4.4 Operational Requirements

| ID | Requirement |
| :--- | :--- |
| **OR-4** | Release qualification shall cover the supported runsc launch, routed-workspace filesystem, and rootless network paths. |
| **OR-5** | An interrupted State Anchor reset shall recover to either the prior generation or a new empty generation; it shall not leave a partially reset active upper layer. |
| **OR-6** | Lazaret shall not require a persistent global daemon or multi-Domain resident process. Shared Storage Catalog operations shall use bounded lock/open/transaction/close critical sections. |
| **OR-7** | Product GC shall provide policy-controlled reclamation for prepared artifacts after all protocol leases for the prepared-artifact ID are released. Shared-artifact reclaim shall wait until no lease remains for that artifact. In-progress prepare trees and foreign trees shall not be deleted; exact-owned abandoned prepare trees may be reclaimed only through fail-closed recovery backed by durable prepare intent. |