Define schema authority and durable store refinements
This commit is contained in:
parent
0e8269ab71
commit
1698296ecd
1 changed files with 551 additions and 107 deletions
|
|
@ -8,11 +8,13 @@ This document is the normative product specification for Lazaret.
|
|||
| :--- | :--- |
|
||||
| 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 |
|
||||
| Development journal | Implementation strategy, experiments, and historical rationale (local checkout: [journal index](journal/00_INDEX.md), [implementation plan](journal/implementation-plan.md)) |
|
||||
| [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 |
|
||||
| [Design schemas](schema.md) | Logical durable records, network-policy documents, readiness evidence, and their relationships |
|
||||
|
||||
This specification does **not** restate the protocol state machine. If a product
|
||||
requirement needs a protocol rule the model does not yet express, either extend
|
||||
the model or state that the requirement is outside the current model abstraction.
|
||||
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.
|
||||
|
||||
## 1. Problem Statement
|
||||
|
||||
|
|
@ -61,14 +63,14 @@ 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.
|
||||
|
||||
Host configuration is read only by host Lazaret processes. A configuration file
|
||||
must not be mounted into, or located beneath a host path mounted into, the Agent
|
||||
Sandbox.
|
||||
The physical refinement of model configuration confinement canonicalizes the
|
||||
configuration file and every bind-mount source, compares their resolved ancestry,
|
||||
and omits configuration bytes from the sandbox mount specification.
|
||||
|
||||
## 2. Glossary
|
||||
|
||||
These terms and identifiers are stable across the specification, protocol model,
|
||||
implementation plan, logs, and user interfaces.
|
||||
implementation, logs, and user interfaces.
|
||||
|
||||
| Term | Definition |
|
||||
| :--- | :--- |
|
||||
|
|
@ -80,7 +82,7 @@ implementation plan, logs, and user interfaces.
|
|||
| **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** | Ephemeral session credentials that bind protocol messages to a registered Session ID and route them to the owning host CLI. |
|
||||
| **Session Coordinator** | The logical Domain role that exclusively owns and coordinates a Domain generation's runtime resources and Client Sessions. It is realized by exactly three constitutive processes: Host Coordinator, Runtime Supervisor, and attached runsc client. |
|
||||
| **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. |
|
||||
|
|
@ -111,6 +113,7 @@ implementation plan, logs, and user interfaces.
|
|||
| **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
|
||||
|
||||
|
|
@ -154,14 +157,13 @@ flowchart TB
|
|||
Net --> Network[Permitted destinations]
|
||||
```
|
||||
|
||||
The logical Session Coordinator for a Domain generation is the composition of the
|
||||
Host Coordinator, Runtime Supervisor, and attached runsc client. The Host
|
||||
Coordinator is the sole protocol and session face for Client CLIs. The Runtime
|
||||
Supervisor owns generation-bound runtime namespaces and supervised resources. The
|
||||
attached runsc client is the non-detached causal edge to the Agent Sandbox.
|
||||
The physical Session Coordinator refinement uses an HC→RS parent/child edge and
|
||||
lifetime pipe. The RS creates the generation 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. Lazaret owns sandbox lifetime through the Session Coordinator process
|
||||
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
|
||||
|
|
@ -170,39 +172,25 @@ 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.
|
||||
Active Domains have per-generation and per-session processes whose authority is
|
||||
scoped by Domain ID, generation, configuration fingerprint, role identity, and
|
||||
exact physical ownership. Bootstrap recovery for a Domain is initiated by a host
|
||||
Lazaret CLI invocation for that Domain, not by a resident scheduler.
|
||||
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 Domain and Session Lifecycle
|
||||
### 3.2 Domain and Session Lifecycle Refinement
|
||||
|
||||
One logical Session Coordinator exclusively owns a Domain generation's Agent
|
||||
Sandbox, Network Sidecar resources, State Anchor mounts, host-only sockets,
|
||||
Escalation Mailbox, durable generation state, and active-session registry.
|
||||
Concurrent CLI processes for the same Domain join the published Host Coordinator
|
||||
and attach separate Client Sessions to the shared sandbox. Different Domains never
|
||||
share these resources.
|
||||
|
||||
An exclusive non-blocking Domain lock elects at most one Host Coordinator startup
|
||||
or recovery leader for a Domain. Losers fail closed. Client CLIs start, join, or
|
||||
recover a Domain through that lock and publication rather than a global control
|
||||
plane.
|
||||
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, exact
|
||||
ownership records) and must not assume those resources disappeared with an owner
|
||||
process.
|
||||
|
||||
Session control and escalation use the Session Coordinator ID on the Host
|
||||
Coordinator face, not Runtime Supervisor, attached runsc, or connectivity-helper
|
||||
process identifiers. Network attachment uses the Network Sidecar ID as the
|
||||
generation's network-policy role identity, not a helper or Runtime Supervisor
|
||||
process id.
|
||||
mounts, `slirp4netns`, PTYs, runsc clients, durable store encoding, and exact
|
||||
ownership records). Physical recovery enumerates and inspects those resources
|
||||
independently of process liveness.
|
||||
|
||||
### 3.3 Session Terminals
|
||||
|
||||
|
|
@ -226,10 +214,9 @@ Interactive terminal control requires:
|
|||
control characters alone are not a sufficient contract.
|
||||
- Per-session exit status collected from the non-detached `runsc exec` client as
|
||||
the primary source.
|
||||
- On session close, PTY master loss, or exec-client loss: deregister the session
|
||||
before further terminal or escalation traffic for that session, stop the guest
|
||||
session process or process group with generation-exact runsc operations, reap
|
||||
the exec client, and close the PTY.
|
||||
- On session close, PTY master loss, or exec-client loss: apply the modeled
|
||||
session-close transition, stop the exact guest session process or process
|
||||
group through runsc, reap the exec client, and close the PTY.
|
||||
|
||||
Disconnected Client Sessions close rather than reattach to an unbounded scrollback
|
||||
owned by the coordinator.
|
||||
|
|
@ -282,23 +269,17 @@ Anchor lower. Archive export alone is not a complete preparation boundary;
|
|||
container tooling may participate only as transport into Lazaret-owned
|
||||
preparation. Ad hoc unsupported tar extractors are not a production preparer.
|
||||
|
||||
Prepared-artifact identity is independent of its storage pathname. Before State
|
||||
Anchor mount, Host Coordinator durable state binds the Domain generation to the
|
||||
prepared-artifact ID with a prepared-lower lease. Distinct generations sharing
|
||||
an artifact hold separate leases; an engine mount refcount is not a lease.
|
||||
|
||||
Concurrent preparation of the same source may reuse a completed artifact or
|
||||
publish a new prepared-artifact ID. An incomplete preparation is never a State
|
||||
Anchor lower. Preparation, lease acquisition, and reclaim serialize so GC acts
|
||||
only after the final lease is released. Recovery may reclaim an abandoned
|
||||
preparation only from matching exact-owned durable intent; foreign or mismatched
|
||||
trees remain untouched.
|
||||
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.
|
||||
|
||||
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
|
||||
#### 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.
|
||||
|
|
@ -315,9 +296,62 @@ in typed tables under a schema/db version (unknown newer versions fail closed
|
|||
until an explicit Host Coordinator migration), including generation identity,
|
||||
minted runtime component IDs, and participant ownership material (for example
|
||||
prepared-artifact ID, pid/start, mount identity, network readiness fingerprint).
|
||||
Participant roles include at least those the model tracks, plus product modules
|
||||
such as `git_routing`, `sessions`, and `publication` as they land. Deterministic
|
||||
paths are lookup hints for physical recovery, not ownership proofs.
|
||||
Participant roles are `prepared_lower`, `state_anchor`, `git_routing`, `network`,
|
||||
`helper`, `sandbox`, and `publication`. The `helper` participant independently
|
||||
records durable intent and exact connectivity-helper pid/start identity before
|
||||
the `network` participant records readiness. Sessions and the generation mailbox
|
||||
are separate generation records. Deterministic paths are lookup hints for
|
||||
physical recovery, not ownership proofs.
|
||||
|
||||
The normative logical records and relationships are defined in the
|
||||
[design schemas](schema.md). Their implementation representation must preserve
|
||||
the distinct Domain Store and Storage Catalog boundaries. Opaque generation
|
||||
documents are not a product storage format.
|
||||
|
||||
Each catalog operation acquires host-wide `storage-catalog.lock`, opens the
|
||||
catalog, performs one redb transaction, closes it, and releases the lock. The
|
||||
lock covers lease changes, prepare publication, and transition to `Reclaiming`.
|
||||
This permits concurrent Domain coordinators without a persistent global daemon
|
||||
or concurrent redb opens.
|
||||
|
||||
The physical lease-acquisition refinement is:
|
||||
|
||||
1. Commit `prepared_lower = Intent` in the Domain Store with the intended
|
||||
prepared-artifact identity.
|
||||
2. Under `storage-catalog.lock`, insert the exact `(prepared-artifact ID, Domain
|
||||
ID, generation)` lease in one catalog transaction.
|
||||
3. Commit `prepared_lower = LeaseHeld` in the Domain Store.
|
||||
4. Commit `state_anchor = Intent`, create the exact mount, and then commit
|
||||
`state_anchor = Prepared` with its mount identity.
|
||||
|
||||
The physical unmount and lease-release refinement is:
|
||||
|
||||
1. Commit `state_anchor = ReleaseIntent` 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 `state_anchor = Clean` and `prepared_lower = ReleaseIntent` in the
|
||||
Domain Store.
|
||||
4. Under `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 `prepared_lower = Clean` in the Domain Store.
|
||||
|
||||
Recovery resumes only from matching durable identity. `state_anchor =
|
||||
ReleaseIntent` retains the catalog lease while recovery verifies and completes
|
||||
the unmount. `prepared_lower = ReleaseIntent` permits removal of a still-present
|
||||
exact catalog lease only after the exact mount is absent; an already-absent lease
|
||||
permits the Domain participant to become `Clean`. A catalog lease with missing,
|
||||
unreadable, non-release, or mismatched Domain evidence is retained and reported.
|
||||
A Domain `LeaseHeld` record whose exact catalog lease is absent is inconsistent
|
||||
and fails closed; recovery neither recreates the lease nor mounts the State
|
||||
Anchor. These rules make every interrupted release conservative and prevent a
|
||||
mounted State Anchor from becoming unleased.
|
||||
|
||||
Store version acceptance occurs before physical resource inspection. The first
|
||||
product version has no product predecessor. Future migration steps create and
|
||||
validate destination rows in one redb transaction and update the version last.
|
||||
|
||||
Files not represented in the upper layer follow the selected base image. Files,
|
||||
directories, and whiteouts recorded in the upper layer remain authoritative when
|
||||
|
|
@ -341,15 +375,21 @@ publication gates follow the protocol model.
|
|||
|
||||
#### Derived policy and readiness encoding
|
||||
|
||||
The Host Coordinator derives the generation's derived network policy from trusted
|
||||
host configuration. The Runtime Supervisor installs only that derived policy and
|
||||
attests readiness by observing installed routes and helper readiness in the
|
||||
enforcement namespace—not by process exit status alone. The product records a
|
||||
network readiness fingerprint as the durable encoding of protocol network
|
||||
readiness. Before publication, Lazaret verifies from the Agent Sandbox network
|
||||
view (or an equivalent generation-bound probe on the same enforcement namespace)
|
||||
that default-denied private destinations are unreachable and that required
|
||||
permitted reachability, including selected DNS resolvers, works.
|
||||
The policy, attestation, readiness-identity projection, and fingerprint inputs
|
||||
are defined by the normative [design schemas](schema.md).
|
||||
|
||||
The Host Coordinator passes canonical policy bytes through a write-sealed
|
||||
inherited memfd. The Runtime Supervisor verifies the seals and digest, installs
|
||||
the policy, and returns observed route, helper, process, and namespace evidence
|
||||
over an inherited Host Coordinator-created private `SOCK_SEQPACKET` channel.
|
||||
Before helper launch, the Host Coordinator commits the independent `helper`
|
||||
participant as `Intent`. After launch it verifies and commits the exact helper
|
||||
and supervising Runtime Supervisor pid/start identities before accepting network
|
||||
readiness evidence and advancing the `network` participant.
|
||||
The Host Coordinator independently reads the Runtime Supervisor's namespace
|
||||
identity and persists the attestation, fingerprint, and generation-bound
|
||||
deny/permit/DNS probe result. Persisted readiness files are evidence after this
|
||||
exchange, not its transport.
|
||||
|
||||
#### Default policy and deny representation
|
||||
|
||||
|
|
@ -370,22 +410,22 @@ Normal Linux longest-prefix routing determines the most specific matching route.
|
|||
IPv4 and IPv6 must either receive equivalent policy or an address family must be
|
||||
disabled.
|
||||
|
||||
The topology and policy-installation sequence must ensure that all external Agent
|
||||
Sandbox traffic traverses the configured enforcement path. Dynamic policy changes
|
||||
are not a requirement unless the implementation can apply them without weakening
|
||||
that property.
|
||||
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.7 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. The Host Coordinator owns the mailbox
|
||||
for the published generation. Host-only CLI/coordinator control may use
|
||||
host-private Unix sockets that are never mounted into the Agent Sandbox.
|
||||
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.
|
||||
|
||||
Auto-approved host commands are launched as an argument vector without a shell.
|
||||
Trailing arguments require an explicit grant on the matched rule.
|
||||
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
|
||||
|
|
@ -415,54 +455,46 @@ 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-2** | Host configuration shall never be mounted into the Agent Sandbox or located beneath a host path mounted into it. |
|
||||
| **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** | Domain network policy shall be established before the Agent Sandbox starts. Network-administration capability for policy install shall be held only on the Runtime Supervisor-owned Network Sidecar install path; the Agent Sandbox shall not receive network-administration capability. |
|
||||
| **SR-5** | Network-administration capability for policy installation shall be confined to the Runtime Supervisor-owned Network Sidecar install path; the Agent Sandbox process specification shall omit that capability. |
|
||||
| **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 the production deny representation. |
|
||||
| **SR-7** | Host actions shall execute only under protocol-model approval (developer or auto-rule). |
|
||||
| **SR-8** | Auto-approved host commands shall execute without a shell and shall permit trailing arguments only when the matched rule explicitly grants them. |
|
||||
| **SR-9** | Protocol peer authentication and authorization shall follow the protocol model (role, Agent Profile, Domain ID, and runtime component ID binding). |
|
||||
| **SR-10** | Domain sockets, mailboxes, and coordination files shall reside in a host-private directory owned by the developer. |
|
||||
| **SR-11** | Runtime and persistent resources belonging to different Domain IDs shall remain isolated. |
|
||||
| **SR-12** | The Agent Sandbox shall not join host user, PID, IPC, UTS, cgroup, or network namespaces; the only shared network namespace permitted is the Domain's Network Sidecar enforcement namespace prepared for that generation. |
|
||||
| **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 runsc OCI specification shall create private PID, IPC, UTS, mount, and user namespaces and set its network namespace path to the independently verified Runtime Supervisor namespace descriptor. 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 production State Anchor lower; the lower shall be a Lazaret-owned prepared lower bound by a prepared-lower lease. Archive export alone shall not be treated as a complete preparation boundary. |
|
||||
| **SR-16** | Session control, registration, and Host Escalation shall authenticate the Session Coordinator ID on the Host Coordinator protocol face and shall not treat Runtime Supervisor or attached runsc process identifiers as substitute protocol peer identities. |
|
||||
| **SR-17** | Network Sidecar ID in attachment authorization shall name the Network Sidecar role instance, not a connectivity-helper or Runtime Supervisor process identifier. |
|
||||
| **SR-15** | Lazaret shall not use a live container-engine image mount as the production 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-2** | Concurrent Client Sessions in one Domain shall share one logical Session Coordinator, Agent Sandbox, Network Sidecar, and State Anchor for the published generation. |
|
||||
| **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-5** | Escalation prompt routing and Escalation Result delivery shall follow the protocol model on the Host Coordinator face. |
|
||||
| **FR-6** | Teardown when no Client Sessions remain shall follow the protocol model; product teardown shall release the generation's physical resources. |
|
||||
| **FR-7** | Product recovery shall not assume external runtime resources disappeared with their owner process and shall apply protocol intent/mismatch refuse rules to physical leftovers (exact-owned cleanup only). |
|
||||
| **FR-7** | Product recovery shall inspect external runtime resources independently of owner-process liveness and compare typed pid/start, 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-10** | Session registration and escalation identity binding shall follow the protocol model. |
|
||||
| **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-12** | The logical Session Coordinator for a Domain generation shall be realized by exactly the Host Coordinator, Runtime Supervisor, and attached runsc client as constitutive processes. |
|
||||
| **FR-13** | The Host Coordinator, Runtime Supervisor, and attached runsc process chain shall realize Session Coordinator presence and sandbox coupling for the protocol model, with product recovery limited to exact-owned physical leftovers. |
|
||||
| **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. Production Session PTYs shall not depend on `runsc exec -console-socket`. |
|
||||
| **FR-15** | For each interactive Client Session, Lazaret shall apply window resize to the host PTY master and deliver guest `SIGWINCH` to the exact session process or process group through runsc; translate Client control events into runsc signal operations for that process or process group; collect exit status primarily from the non-detached `runsc exec` client; and on session end deregister before further terminal or escalation traffic for that session, stop the guest session process or process group with generation-exact runsc operations, reap the exec client, and close the PTY. |
|
||||
| **FR-16** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper, with exact-owned process identity for recovery under the protocol helper ownership rules. |
|
||||
| **FR-17** | The Domain durable store shall be opened for read or write only by the Host Coordinator process that holds the Domain exclusive lifecycle lock; no other process shall open the store file. Mutations shall apply as whole store transactions. Protocol durable intent is encoded in that store. |
|
||||
| **FR-18** | Product network readiness encoding shall include a network readiness fingerprint and the pre-publication reachability verification described under network isolation; protocol publication and readiness gates follow the protocol model. |
|
||||
| **FR-15** | For each interactive Client Session, Lazaret shall apply window resize to the host PTY master and deliver guest `SIGWINCH` to the exact session process or process group through runsc; translate Client control events into runsc signal operations; collect exit status primarily from the non-detached `runsc exec` client; and after the modeled session-end transition stop the exact guest process or process group, reap the exec client, and close the PTY. |
|
||||
| **FR-16** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper. The Domain Store shall record independent `helper` intent before launch and exact helper and supervising Runtime Supervisor pid/start identities before network readiness. |
|
||||
| **FR-17** | The Domain Store shall be opened only by the Host Coordinator process holding the Domain `flock`; mutations shall use whole redb transactions. Storage Catalog opens shall be bounded by `storage-catalog.lock` and one transaction. Cross-store lease release shall follow the durable release-intent, exact-unmount, catalog-delete, Domain-clean ordering defined by the durable generation refinement. |
|
||||
| **FR-18** | Product network-readiness evidence shall conform to the normative design schema and include the readiness fingerprint plus the generation-bound deny/permit/DNS probe result. |
|
||||
| **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** | Before publication, Lazaret shall verify from the Agent Sandbox network view, or an equivalent generation-bound probe using the same enforcement namespace, that default-denied private destinations are unreachable and that required permitted reachability including selected DNS resolvers works. |
|
||||
| **FR-21** | The durable generation document encoding shall include schema/db version, generation identity, minted runtime component IDs, model-governed durable decision and participant intent, and ownership material for product recovery. Unknown newer schema versions shall fail closed until an explicit Host Coordinator migration runs. |
|
||||
| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. A durable generation-bound prepared-lower lease shall exist before State Anchor mount. |
|
||||
| **FR-20** | The physical network probe shall execute in the Agent Sandbox network view or an equivalent generation-bound process using the same enforcement namespace and record configured deny, permitted reachability, and selected DNS resolver observations. |
|
||||
| **FR-21** | The Domain Store and Storage Catalog shall preserve the records, ownership variants, identities, and relationships in the normative design schema. |
|
||||
| **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
|
||||
|
||||
|
|
@ -479,10 +511,6 @@ follow a symlink outside the Domain Root.
|
|||
|
||||
| ID | Requirement |
|
||||
| :--- | :--- |
|
||||
| **OR-1** | The Session Coordinator shall maintain exclusive runtime ownership of Domain generation resources. An exclusive Domain lock shall elect at most one Host Coordinator leader for cold start or recovery of a Domain; concurrent losers shall fail closed. |
|
||||
| **OR-2** | Accepted protocol requests shall resolve per the protocol model. |
|
||||
| **OR-3** | Cancellation and process termination shall follow the protocol model (no stranded host command, no permanent block of another Client Session). |
|
||||
| **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported runsc, filesystem, and network configurations. Test evidence belongs in the journal. |
|
||||
| **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported runsc, filesystem, and network configurations. |
|
||||
| **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 that holds mutable runtime authority across Domains. Per-Domain authority shall be scoped by Domain ID, generation, configuration fingerprint, role identity, and exact physical ownership. |
|
||||
| **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. |
|
||||
| **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. |
|
||||
|
|
|
|||
Loading…
Reference in a new issue