Refine modeled terminal behavior into PTY mechanics

docs/specification.md

@@ -590,15 +590,23 @@ 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.
+  before the `CommitSessionTerminal` refinement completes.
-- Window resize applies `TIOCSWINSZ` to the host PTY master and then delivers
+- Before guest startup, the Client transfers its validated terminal modes and
-  guest `SIGWINCH` to that process group through runsc. Rows and columns are
+  initial window size and the Host Coordinator applies them to the host PTY.
-  nonzero unsigned 16-bit values; pixel dimensions may be zero when unknown.
+  Rows and columns are nonzero unsigned 16-bit values; pixel dimensions may be
-- Client `Interrupt`, `Quit`, and `Suspend` events translate respectively to
+  zero when unknown.
-  `SIGINT`, `SIGQUIT`, and `SIGTSTP` for that process group. Raw control bytes do
+- The model's `Keyboard` delivery to `GuestPtyForeground` is realized by writing
-  not substitute for these events. Host CLI suspension is local: the CLI
+  Client keyboard bytes, including configured interrupt, quit, and suspend
-  restores its terminal before stopping itself and sends the current window size
+  bytes, to the exact Session PTY. The terminal line discipline applies its
-  after resuming; it does not synthesize a guest signal.
+  configured foreground-process-group semantics.
+- The model's `Resize` and `Break` deliveries to `ExactSessionPty` are realized
+  respectively by `TIOCSWINSZ` and `tcsendbreak()` on the host PTY master.
+  Terminal foreground semantics apply any resulting `SIGWINCH`.
+- The model's local terminal events are recognized after a line boundary:
+  `~^Z` restores and suspends the Client and sends the current window size after
+  resume, `~.` disconnects, and `~B` requests BREAK. A doubled `~~` sends one
+  literal tilde. External `SIGHUP`, `SIGINT`, `SIGQUIT`, and `SIGTERM` restore
+  and terminate the local Client.
 - 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.
@@ -607,57 +615,64 @@ Disconnected Client Sessions close rather than reattach to an unbounded scrollba
 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
+this refinement. Interactive sessions negotiate `lazaret-control/2` through
-encoding. One Host Coordinator event loop serializes input, resize, signal,
+TLS ALPN before any version-specific record is decoded. A new Client refuses an
+old coordinator during ALPN negotiation; a new coordinator explicitly refuses
+interactive execution over `lazaret-control/1` while retaining v1
+non-interactive execution. Rust protocol records and fixed codec tests own each
+encoding. One Host Coordinator event loop serializes input, resize, BREAK,
 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
+control capacity. The event loop applies the model's terminal interaction
-modeled terminal route is the sandbox route. An invalid Session ID, inactive
+admissibility and authority decisions before performing these physical actions.
-route, stale generation, or terminal in release refuses the event.
 
-PTY output is forwarded only while the modeled terminal route is the sandbox
+The Host Coordinator reads and forwards PTY output while the modeled terminal
-route. During `Prompt` or `HostProcess` routing the Host Coordinator stops reading
+route is `Sandbox`. While the route is `Prompt` or `HostProcess`, it 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
+does not accumulate an unbounded user-space queue. It resumes PTY reads when the
-the model restores the sandbox route.
+model restores the `Sandbox` route. Prompt input is read from the exact Client
+connection rather than the PTY.
 
-Normal guest completion begins the modeled session close and physical release,
+Normal guest completion refines `CompleteSessionTerminal`. Its physical sequence
-so no new terminal or escalation event is admitted. The Host Coordinator
+serializes cancellation of any active prompt or exact host process before terminal
-first cancels any active prompt or exact host process and serializes that
+output. The Host Coordinator then collects and reaps the exec client, drains and
-cancellation before terminal output. It then collects and reaps the exec client,
+forwards PTY bytes in order until EOF or a bounded drain deadline, and emits at
-drains and forwards PTY bytes in order until EOF or a bounded drain deadline,
+most one `SessionExit` after the last forwarded byte on the closing connection.
-and emits at most one `SessionExit` after the last forwarded byte on the closing
+If the connection is already lost, the outcome is not retained for reattachment.
-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.
+1. The Host Coordinator refines `BeginSessionTerminal` by recording 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.
+   acquisition protocol with the expected committed HC pidfs authority. Before
+   releasing the wrapper, it applies the validated transferred terminal modes
+   and initial window size to the PTY.
    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
+4. The `CommitSessionTerminal` refinement uses one Domain Store transaction to
-   client ownership to committed, records the PTY, container, guest leader, and
+   promote the exact Host Coordinator and exec-client ownership to committed,
-   guest process-group identities, and marks the Session Terminal running.
+   record the PTY, container, guest leader, and guest process-group identities,
-5. Only then may the Host Coordinator accept terminal events for the session.
+   and mark the Session Terminal running.
+5. The Host Coordinator then applies the model's terminal interaction
+   admissibility rules to events for the Session.
 
-Failure before the running state never admits the terminal. A live Host Coordinator uses
+If physical acquisition fails before the transaction in step 4, a live Host
-its in-memory exact handles to terminate any partial exec and guest group and
+Coordinator uses its in-memory exact handles to terminate any partial exec and
-records release intent. If HC itself is lost, the armed exec edge stops the host
+guest group and records release intent. If HC itself is lost, the armed exec edge
-client and the generation lease-loss path stops the guest sandbox; bootstrap
+stops the host client and the generation lease-loss path stops the guest sandbox;
-recovery cleans the retained Intent only after runtime absence.
+bootstrap recovery performs modeled cleanup after establishing 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
+1. Refine the applicable modeled close transition by recording terminal release
-   record terminal release intent while retaining all exact identities.
+   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
@@ -674,18 +689,17 @@ 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
+Hard Host Coordinator loss closes its PTY descriptors. The exec-client lifetime
-sessions; the exec-client lifetime edge prevents an unrecorded or recorded exec
+edge prevents an unrecorded or recorded exec client from surviving that loss.
-client from surviving that loss. The surviving Runtime Supervisor follows the
+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
+still-live exact exec-client host process, and then performs modeled Session
-Terminal clean. Intent without physical identities becomes clean only
+Terminal cleanup. A process, container, PTY, or generation
-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.
 
@@ -1203,7 +1217,7 @@ 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. 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-15** | For each interactive Client Session, Lazaret shall refine the application model's Session Terminal lifecycle, routing, interaction-authority separation, peer isolation, and liveness properties through the wire, PTY, process-identity, release, and recovery mechanisms specified in the Session Terminal refinement. |
 | **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. |