Interlace Transition Tables

These tables make the 050/060 ownership model executable. A connected carrier owns prefacing or one logical session; a direct pair owns two endpoints. Its runtime transport may own one duplex IO value or split reader and writer values without changing carrier state. Host cancellation retires that complete connected transport. Listener acceptance, process supervision, admission, and task and service ownership remain outside these tables. The numbered specifications remain authoritative for validation and wire encoding.

A phase deadline is one absolute deadline created when a stable prefacing, establishment, or endpoint phase token changes. Partial IO, event reads, replacement staging, and progress by the other endpoint do not reset it. If the machine enters fixed point while the batch accepted at that transition, the settled round’s final request item, remains buffered, the driver retains that batch’s Requesting token and deadline until it is fully written and flushed to the adopted IO; it does not publish FixedPoint first.

Connected carrier owner

CarrierState =
  Prefacing {
    cause: Initial | Reset,
    local_operand: optional (operand, optional expected peer By),
    local_preface: Pending(nonce) | Accepted(nonce),
    peer_nonce: optional nonce,
  }
  | Running {
    session: SessionMachine,
    staged_replacement: optional InterlaceModule,
  }
  | Failed(SessionError)
  | Closed(CloseReason)

CarrierRole::Listener derives protocol side0 and CarrierRole::Connector derives protocol side1. The role is fixed before decoding and is not inferred or negotiated. Carrier role, proof assurance and binding, operand source, By-secret value, configured stream encodings and port, limits, nonce seed, and next nonce sequence survive logical-session replacement. The operand source is Fixed(expected peer By), whose operand replacement changes, or Selected, which asks the host for each session’s operand and expected peer By. The carrier also retains the port of the latest peer preface as a diagnostic. Construction constraints are defined by Lace-050. Endpoint configuration and diagnostics are not policy facts, plan or proof inputs, or carrier authority. The carrier, ConnectedConfig, and Rust runtime connected inputs retain the nonce seed in the core zeroizing NonceSeed owner; each config clone owns an independently erased seed, and unclaimed participants and failed setup erase theirs on drop. These owners, BySecret, and schnorr-blake3’s seed-derived SigningKey use maintained zeroize for owned secret storage. The guarantee covers current owned storage, not caller copies, prior moves, compiler temporaries, registers, opaque hash state or C-library scratch. See schnorr-blake3 for the cryptographic boundary.

The running machine owns the current local operand: establishment owns it until compilation, then its immutable plan owns it. The carrier keeps no duplicate. A selecting carrier owns no operand in prefacing until the host answers.

The decoder stops at a preface before parsing any bounded suffix. During initial prefacing, ordinary input is premature. During locally initiated reset prefacing, complete old peer items are decoded under the old encoding and discarded until the peer’s end mark, if any, and preface. Malformed or oversized input fails normally. One absolute prefacing deadline covers accepted old-writer drain, local-preface acceptance, discard, peer-preface receipt, and operand selection.

SelectOperand is a poll result, not a host callback: the sans-IO carrier stays synchronous and owns no selector, and each runtime driver answers it with select_operand from its own selector before polling again. Rust drivers call their selector inline, Python on the driving thread, and JavaScript awaits a returned promise. Until the answer, the carrier has no session, effect, or legal peer input.

A connected writer owns at most one accepted batch, ending with the direction’s flush. The codec validates the batch on acceptance, then renders and encodes it into one bounded chunk at a time as the writer takes bytes; an identity direction writes a record larger than the free chunk room from the record’s own bytes. An accepted old batch drains, then the old encoding’s end mark when it has one, before the fresh raw preface; unaccepted old output is dropped. The fresh preface is the next accepted output, and proof or operand bytes cannot overtake it.

Logical session owner and establishment

SessionState =
  Establishing(EstablishmentState)
  | Round(RoundState)
  | FixedPoint(FixedPointState)
  | Failed(SessionError)
  | Closed(CloseReason)

Rust establishment applies Lace-050’s proof validation before advancing the proof transitions above. Lace-060 defines the proof grammar.

Complete proof, policy announcement, policy answer, and policy-body items, including their labels, count toward logical-session establishment control. Proof and operands are control material, not store admission. A direct pair bypasses establishment, derives its plan from prepared modules and explicit authorities, and starts both endpoints in Round.Advertising.

Round state shape

RoundPhase = Advertising | Requesting | Answering | Fencing

A listing slot stores one complete listing and its change since the previous listing. The endpoint owns the session’s local listing, frozen as the previous local listing until the next round changes it; on a connected carrier the session adapter owns the previous peer listing, the entries each side requested in the previous round, the first-round reconciliation state, and the 060 delta and 061 reconciliation encodings, while the endpoint sees only complete listings with their changes. Starting a round drops all other round-local state. The two endpoints may occupy different phases.

Advertising

Requesting

A local commit after the round boundary freezes cannot affect either the advertisement or request snapshot in that round.

Answering

A direct sibling endpoint may continue while this endpoint owns StoreCall, but routing into the blocked endpoint waits.

Fencing and fixed point

Fencing occurs only in a round where either frozen request set is nonempty.

Fixed point is entered from Requesting when both frozen request sets are empty; a fence received for such a round is PeerProtocol.

The machine reports:

FixedPointBoundary {
  round: InterlaceRoundId,
  wake_boundaries: [FixedPointWakeBoundary],
}

FixedPointWakeBoundary {
  machine: MachineId,
  fixed_point: FixedPointId,
  position: StorePosition,
}

A connected machine reports one wake boundary; a direct pair reports one per protocol side. Same-Lace composition retains two independently tokened wake boundaries.

A retained terminal failure from a runtime-owned Lace is host lifecycle, not a machine input: the driver retires this operation and reports the same typed failure retained by that Lace.

A position delivery must match the complete current boundary. A replacement, peer input, or newer fixed point invalidates the old identity; stale readiness is discarded. Lace terminal failure is never discarded as stale. Fixed-point entry commits the semantic result. A bounded host then stops delivering peer input and settles its route under the settled round’s Requesting deadline, as Lace-050 defines. The write rows and the read row progress concurrently:

Endpoint-exclusive effects

An endpoint owns at most one effect: StoreCall or peer output. Only the admission of a received response starts a StoreCall while peer output waits for the writer; the machine then reports the StoreCall first. While StoreCall is active, that endpoint consumes no peer input, stages no replacement, and starts no other effect. The connected driver races store execution, phase deadline, cancellation, and retained terminal failure from its runtime-owned Lace. Lace failure retires the semantic operation before already-started work can submit. Durable-position publication or Lace poisoning and response submission finish before ordinary polling resumes.

Every terminal transition retires active StoreCall in the semantic owner. SessionMachine retires its connected endpoint effect and DirectPair retires both endpoint effects; ConnectedCarrier, hosts, and FFI have no terminal discard input. Already-started work may retain its Lace long enough to publish a confirmed durable mutation, but cannot submit after retirement.

A direct pair may expose one effect from each endpoint in the same poll, including two StoreCall objects. A retained effect on one side never hides the other. Direct replacement is staged synchronously only through exclusive pair ownership and waits until both endpoint store effects settle. At the next poll, before endpoint or watch work, it atomically retires both endpoints and their plan, drops unaccepted typed output and machine observations, and constructs a fresh pair with the prepared operands, existing explicit authorities, and limits.

Peer output and input ownership

Machine output remains borrowed until direct insertion or connected-writer acceptance. The writer retains one accepted batch, its current chunk and offset through partial writes. Replacement drains the entire accepted old batch and writes the old encoding’s end mark before writing a fresh preface. The IO adapter owns any protection/framing and delivers only authenticated plaintext when protected. Its flush completes when it has accepted ownership of preceding plaintext within bounded buffering; it then owns delivery or failure. Reads and writes progress independently while respecting legal-input and active-StoreCall gates. Terminal failure drops retained output and aborts IO immediately. The batch accepted at the transition into fixed point retains its original absolute phase deadline through full write and flush; that flush gates fixed-point observation, bounded completion and clean close.

ConnectedCarrier::peer_record_ingress directs each peer record by the carrier’s state. The host’s codec state checks it at the record’s start, when its canonical length is known, before any byte reaches memory, staging or the store:

At most one decoded input may wait for immediate handoff. Without active StoreCall, the carrier classifies an already decoded item as accepted, immediately rejectable by core validation, or backpressured; hosts do not reconstruct this from owning state. Input is accepted only into the current state-local slot. Duplicate, out-of-order, wrong-family, or unrequested input fails at handoff rather than entering a semantic queue. The decoder retains item labels and listing forms; a label or form that does not match the owning state fails with PeerProtocol.

Failure and EOF

Transport establishment precedes Lace adoption and has no ILTP phase or deadline. The application owns its setup failures and cancellation. After adoption, EOF finalizes the ILTP decoder; a partial item or missing end mark still fails and only fixed-point boundary EOF is clean. Decoded canonical ILTP bytes alone count against ILTP control/transfer budgets.

Terminal handling drops retained output and staged replacement, writes no end mark, and immediately initiates carrier closure, without waiting for a peer close acknowledgment. Already platform-queued bytes may still arrive; no subsequent Lace work is submitted. Records already durably admitted remain stored. Successful fixed-point publication confirms settled transfer obligations, not permanent remote retention.