Restore specification and model authority boundaries

docs/specification.md

@@ -9,12 +9,15 @@ 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 |
 | [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 records, protocol data shapes, network-policy documents, readiness evidence, and their relationships |
 
 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
 
@@ -181,9 +184,9 @@ initiated by a host Lazaret CLI invocation, not by a resident scheduler.
 
 ### 3.2 Trusted Host Configuration Refinement
 
-The trusted-host configuration has the closed v1 shape in the
+The repository [design schemas](schema.md) encode the closed v1 trusted-host
-[design schemas](schema.md). Lazaret chooses its configuration file from an
+configuration described by this refinement. Lazaret chooses its configuration
-explicit host CLI option or, when absent, from
+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
@@ -201,9 +204,10 @@ 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 selected profile name and canonical workspace
-bytes produce `DomainIdV1` exactly as defined by the schema.
+bytes produce `DomainIdV1` as described by this refinement and encoded by the
+repository schema.
 
-The explicit configuration path follows the schema's strict host-path grammar.
+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
@@ -483,14 +487,15 @@ they do not claim to recognize a hypothetical equal tuple after wrap.
 
 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 in
+Its signed Trust Manifest binds both roots to the generation identity defined by
-the schema. The Session Coordinator TLS and protocol credentials use distinct
+this specification and the protocol model. The Session Coordinator TLS and
-leaf keys physically held by HC; the Agent Sandbox uses another request-signing
+protocol credentials use distinct leaf keys physically held by HC; the Agent
-key. The publication identity pins the CA, manifest, and coordinator TLS leaf in
+Sandbox uses another request-signing key. The publication identity pins the CA,
-the validated host-private Domain path, while the exact sandbox credential mount
+manifest, and coordinator TLS leaf in the validated host-private Domain path,
-pins the same manifest. Protocol credential IDs are SHA-256 digests of their
+while the exact sandbox credential mount pins the same manifest. Protocol
-signed claims. `SessionCoordinator` remains the logical protocol role; HC is its
+credential IDs are SHA-256 digests of their signed claims. `SessionCoordinator`
-physical key holder, not another principal.
+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
@@ -549,14 +554,14 @@ Interactive terminal control requires:
 Disconnected Client Sessions close rather than reattach to an unbounded scrollback
 owned by the coordinator.
 
-The session connection carries the terminal events and messages defined by the
+The session connection carries the terminal events and messages described by
-normative design schema. One Host Coordinator event loop serializes input,
+this refinement and encoded by the repository schema. One Host Coordinator event
-resize, signal, close, prompt-routing, PTY output, and exec-client completion for
+loop serializes input, resize, signal, close, prompt-routing, PTY output, and
-each Session ID. It uses bounded queues and PTY backpressure; terminal data for
+exec-client completion for each Session ID. It uses bounded queues and PTY
-one session cannot consume another session's control capacity. Input, resize,
+backpressure; terminal data for one session cannot consume another session's
-and signal events are accepted only while the modeled terminal route is the
+control capacity. Input, resize, and signal events are accepted only while the
-sandbox route. An invalid Session ID, inactive route, stale generation, or
+modeled terminal route is the sandbox route. An invalid Session ID, inactive
-terminal in release refuses the event.
+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
@@ -722,22 +727,19 @@ Sentry still makes host `.git/config` read-only and replaces default
 path, cross-policy atomic rename, and device-node creation are refused as defined
 above and are not compatibility promises.
 
-The committed `lazaret-ignored-workspace-contract-v1` corpus is the executable
+The repository `lazaret-ignored-workspace-contract-v1` corpus is a
-acceptance inventory for these semantics. It covers ignore precedence and live
+non-authoritative executable test inventory derived from these semantics. It
-changes, non-UTF-8 and case-folded matching, linked worktrees and nested
+covers ignore precedence and live changes, non-UTF-8 and case-folded matching,
-repositories, every operation class above, open-handle transitions, concurrent
+linked worktrees and nested repositories, every operation class above,
-host and sandbox mutation, router loss, and absence of silent loss or copy-back.
+open-handle transitions, concurrent host and sandbox mutation, router loss, and
-The same corpus defines the benchmark protocol. Qualification runs direct-host
+absence of silent loss or copy-back.
-and routed placements within the recorded qualification class, uses identical
+Its benchmark protocol compares direct-host and routed placements using identical
-fresh fixture materialization for each sample, and reports the direct-placement
+fresh fixture materialization and reports metadata, Git, offline package
-calibration, routed absolute median, and paired routed/direct median ratio.
+installation, and offline build results. Exact observed hardware, storage,
-Metadata, Git, offline package installation, and offline build workloads must
+filesystem, kernel, and tool versions belong in generated run metadata.
-meet all three limits. Exact observed hardware, storage, filesystem, kernel, and
+Qualification constraints, sampling rules, variance checks, and numeric budgets
-tool versions are generated run-result metadata rather than source-controlled
+in fixtures are engineering evidence and regression targets, not product
-eligibility identities. The qualification constraints, direct calibration,
+conformance requirements.
-preparation states, sampling order, variance tolerance, normalization, and
-numeric budgets are part of the corpus and may not be relaxed by a production
-implementation.
 
 Ignored-path isolation is defense in depth and does not replace the mandatory Git
 Sentry protections below.
@@ -806,10 +808,10 @@ before the `network` participant records readiness. Sessions and the generation
 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
+The repository [design schemas](schema.md) encode the logical records and
-[design schemas](schema.md). Their implementation representation must preserve
+relationships described by these refinements. Their implementation
-the distinct Domain Store and Storage Catalog boundaries. Opaque generation
+representation must preserve the distinct Domain Store and Storage Catalog
-documents are not a product storage format.
+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
@@ -903,8 +905,9 @@ and publication gates follow the protocol model.
 
 #### Derived policy and readiness encoding
 
-The policy, attestation, readiness-identity projection, and fingerprint inputs
+The repository [design schemas](schema.md) encode the policy, attestation,
-are defined by the normative [design schemas](schema.md).
+readiness-identity projection, and fingerprint inputs described by this
+refinement.
 
 The Host Coordinator passes canonical policy bytes through a write-sealed
 inherited memfd. The Runtime Supervisor verifies the seals and digest, installs
@@ -953,12 +956,13 @@ 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 defined by the normative design
+Mailbox files carry the signed protocol records described by this refinement and
-schema; TLS is not layered over the regular-file transport. HC opens each ready
+encoded by the repository schema; TLS is not layered over the regular-file
-entry relative to a confined directory handle, rejects links and non-regular
+transport. HC opens each ready entry relative to a confined directory handle,
-files, bounds the complete file before allocation, and reads it once. It verifies
+rejects links and non-regular files, bounds the complete file before allocation,
-the signature over those owned bytes before parsing. Pathnames, file ownership,
+and reads it once. It verifies the signature over those owned bytes before
-mailbox identity files, PIDs, and start times are not authentication evidence.
+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 in the schema. Postcard payloads
@@ -1035,13 +1039,13 @@ not duplicated here.
 | **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. Production Session PTYs shall not depend on `runsc exec -console-socket`. |
-| **FR-15** | For each interactive Client Session, Lazaret shall preserve the Session Terminal record and protocol in the normative design schema; 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-15** | For each interactive Client Session, Lazaret shall preserve the Session Terminal record 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** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper. The Domain Store shall record independent `helper` intent before launch and exact committed helper and supervising Runtime Supervisor pidfs ownership 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-18** | Product network-readiness evidence shall include the readiness fingerprint plus the generation-bound deny/permit/DNS probe result described by the network-readiness 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** | 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-21** | The Domain Store and Storage Catalog shall preserve the records, ownership variants, identities, and 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