Contents

Lace-050 · Interlace State Machine

Tags: interlace, exchange, reconciliation, state-machine

Purpose

Interlace is Lace’s record-set convergence primitive. Two participants derive one exchange plan from two canonical policy operands, advertise validated local records, request missing advertised records, validate and admit responses, and repeat until neither side requests a record.

Interlace is a sans-IO state machine, not a socket protocol. A connected carrier begins only after a host establishes a role-bearing duplex byte capability. The physical IO may be one duplex owner or independent reader and writer owners; listening, acceptance, process supervision, and service admission are outside interlace state. This specification defines direct and proof-derived session authority, carrier and logical-session ownership, establishment, symmetric round phases, snapshots, effects, fixed point, open operation, hard policy replacement, errors, and limits. 060 binds these semantics to ILTP byte streams.

Connected peer authority comes only from live protocol proof

The host fixes carrier role and connected proof inputs before one ILTP carrier starts or decodes any ILTP byte. CarrierRole::Listener is side0 and CarrierRole::Connector is side1; paired endpoints use complementary roles, and roles are neither inferred nor negotiated. Every carrier has one unpredictable nonzero 32-byte nonce seed, an optional local By-secret value, and one resolved proof assurance:

Disabled
ConfidentialChannel
ChannelBound(binding)

Each logical session begins with a fresh nonce pair and role-ordered proof establishment, then freezes immutable Here/1 and PeerConfidential/1 runtime facts when present. Here(local_key) exists when the carrier’s local By-secret value corresponds to local_key. PeerConfidential(peer_key) exists only when the live peer’s valid proof binds that logical session’s nonce pair and the resolved assurance establishes confidentiality and integrity for the complete carrier. ConfidentialChannel relies on host-asserted endpoint confinement; ChannelBound(binding) additionally requires the proof to match the locally completed encrypted channel’s immutable binding under 060. Connected hosts cannot inject final peer authority, and authority is freshly derived rather than inherited across logical sessions.

The public assurance is Disabled by default. The host may explicitly supply ConfidentialChannel or ChannelBound(binding) with its adopted IO. The binding owns exactly 32 opaque bytes derived by the protected channel’s implementation; Lace neither establishes that channel nor interprets a transport method. Transport endpoint configuration and diagnostics supply no assurance and MUST NOT become policy facts, plan or proof inputs, or protocol authority. Explicit disable suppresses proof authority.

Connected construction MAY also supply one optional expected peer By value, or a selector MAY supply one per logical session as defined under ports. It is an explicit rejection-only constraint, not endpoint-derived authority or a policy, plan, or proof-transcript input. When present, resolved proof assurance MUST be ConfidentialChannel or ChannelBound(binding); an expectation MUST NOT enable trust. An invalid local combination MUST fail construction through the existing configuration error before protocol IO. Raw peer verification does not require a local By-secret. Channel-bound construction requires a local By-secret and a nonempty valid peer proof even without an expected peer By.

A connected carrier exposes the key of its latest logical session’s PeerConfidential fact as the peer’s proved By, a diagnostic. It exists from that session’s validated peer proof until the next preface cut and is absent otherwise and for a direct pair. It MUST NOT become a policy fact, plan or proof input, or protocol authority.

A same-runtime direct pair bypasses proof and receives one explicit final SessionAuthority per endpoint. Each value contains at most one Here/1 and one PeerConfidential/1 fact; either or both may be absent. It contains no other fact family. Side labels remain protocol ownership labels, not identity or authority.

Channel assurance and proof freshness are separate

ConfidentialChannel asserts an existing property of the complete adopted carrier; it neither enables encryption nor authenticates the transport. The host MUST establish confidentiality, integrity protection, and endpoint confinement before selecting it. This assertion covers every segment, including proxies, tunnel endpoints, and plaintext local forwarding legs. Components that can read or modify ILTP bytes remain inside the trusted boundary; inner proof does not protect against them. A loopback address alone does not establish this assurance.

The ILTP nonce pair gives proof freshness: an old proof cannot satisfy a fresh pair. In the unbound ConfidentialChannel context, it does not bind the proof to an underlying encryption session. A terminating intermediary can establish two encrypted channels and relay the live ILTP nonces and valid proofs unchanged between them, then read or modify the subsequent ILTP traffic. No signature forgery or nonce reuse is needed. The host’s channel assurance MUST exclude such an untrusted intermediary. Unauthenticated encryption, including TLS with peer verification disabled, is therefore insufficient by itself for ConfidentialChannel.

PeerConfidential(peer_key) is conditional on both a valid live proof and that host assurance. Proof alone does not establish that the encryption endpoint controls the By-secret. Independently authenticated transport between trusted endpoints can satisfy the assurance without exposing transport keying material to ILTP. The application nonces are not channel binding. The ChannelBound context instead verifies the 060 Channel-Binding field against the local encrypted channel, preventing live proof relay between independently terminated channels. The host supplies the binding with the established IO. The channel implementation MUST derive it from the actual completed protected channel carrying these bytes, with application/transport domain separation and any required stream scope. The binding MUST agree at both endpoints, resist reuse across independently terminated channels, remain immutable for the carrier, and be safe to disclose. An endpoint, certificate fingerprint or arbitrary shared nonce is not such a derivation. Lace trusts the local channel implementation to supply valid protected IO and its binding; it does not infer either property from the binding bytes.

A bound proof authenticates the presented By identity on this channel and logical session, not a human, intended service, executable, configuration, or policy. Without an expected peer By, it does not select an intended identity. A holder of the By-secret or an accepted Seal-signing capability can authenticate a session it controls. Proof-shaped application Seals remain ordinary records: implementations MUST NOT reserve Proof-Profile or Channel-Binding, restrict ordinary Seal construction, or infer that policy constraints accompany a signature to another session.

Fixed profile and policy boundary

ILTP 0.13 fixes:

Each connected direction’s 065 stream encoding is the only negotiated element. Record formats, lowering, advertisement capabilities, parser caps, and operation budgets are not negotiated. An incompatible set requires another protocol version.

Exactly two canonical operands are the complete policy inputs. Their ordered slots deterministically derive one immutable compiled plan. Operand position derives origin and lowering scope. A compiled plan plus the endpoint’s typed local slot is the complete executable provenance. There is no host approval or third policy input.

The plan retains 040’s binary selection intersection, origin-aware whole-record exposure, request-only advertisement facts, directional vetoes, and symmetric advertisement schema. The schema cannot add selected records or widen the local exposure boundary.

Carrier and logical-session ownership

A connected carrier preserves carrier role, proof assurance and any channel binding, operand source, By-secret value, configured stream encodings and port, operand cache, limits, and nonce generation. The configured stream encodings and port fix the offers and Port in every preface the carrier sends; each fresh preface pair selects each direction’s encoding for that logical session under 065. A direct pair encodes nothing. Its protected IO owner preserves the established channel across logical sessions; re-prefacing MUST NOT re-establish it or change its binding. Reconnection creates fresh channel and nonce-seed ownership. The By-secret value and nonce seed use concrete zeroizing secret owners. Changing any of these carrier inputs recreates the carrier; policy replacement changes only a fixed operand. The operation that claims host-established IO owns it through connected settlement or terminal retirement; process, listener, admission, and service lifecycle remain application-owned. The carrier owns exactly one state:

Prefacing(Initial | Reset)
Running(SessionMachine, optional staged replacement)
Failed(SessionError)
Closed(CloseReason)

Prefacing owns the session’s prepared local operand once known, local-preface acceptance, and the optional peer nonce and port. Running owns one logical session and at most one staged replacement. A logical session owns exactly one semantic state:

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

Establishment is role ordered:

Side0Proof
Side1Proof
Side0Operand
Side1Operand
Side0Delivery
Side1Delivery   only when side0 reports side1's operand missing
Round.Advertising

A logical session owns one current local operand: establishment owns it until plan compilation, then the immutable plan owns it. The carrier does not keep a parallel operand copy. A fresh preface pair constructs one fresh session; old and fresh session machines are never active together.

A logical session also retains two listings: the previous local listing, the last complete listing this endpoint advertised, and the previous peer listing, the last complete peer listing it received. Both start empty. A connected session additionally owns its first-round reconciliation state and the entries each side requested in the previous round, which extend the next 060 delta’s base. All of it is discarded with the session on re-prefacing or hard replacement.

Each endpoint round has exactly one local phase:

Advertising
Requesting
Answering
Fencing

A round whose two frozen request sets are both empty ends in Requesting; Answering and Fencing occur only when either set is nonempty. The state is the sole authority for the legal phase, round-local data, current effects, fixed-point boundary, and terminal status. Starting a round replaces all prior requests, obligations, commitments, transfer state, and peer slots; the retained listings are replaced only when the round’s local listing is accepted and its complete peer listing is received. Round numbers are local diagnostics and never appear in protocol data.

Each endpoint progresses independently. The two endpoints MAY temporarily occupy different local phases. Neither endpoint waits for the other endpoint to finish local work before starting the same symmetric phase. An implementation MUST NOT turn the four phases into side0-then-side1 phase ownership.

An endpoint owns at most one active machine effect at a time: one StoreCall or one retained peer output. The exception is admission: while its output waits for its next owner, an endpoint still admits a received response through one StoreCall, so two endpoints answering at once never wait on each other’s reads. State-local peer slots are input state, not additional effects. Polling a direct pair exposes ready effects from both endpoints together so one endpoint’s pending work does not hide the other’s. Runtime-owned Lace failure is host lifecycle rather than a machine effect or peer input; it retires every operation using that Lace, including an operation waiting on a StoreCall or retained output.

A same-runtime direct pair receives both prepared operands and both host-supplied authority values, which may be empty, derives the same plan, and starts both endpoints in Round.Advertising. It exchanges complete typed listings every round, never reconciling or sending a delta in place of a listing, and uses the same hash-ordered listings, snapshots, routing, validation, StoreCall, fences, fence-less fixed point, and limits as connected operation.

A local output is accepted when ownership passes to its next local owner: the peer endpoint’s matching slot for a direct pair, or the retained encoder and writer for a connected route. Acceptance does not mean IO flush or peer receipt. Each prefacing or semantic phase receives one absolute deadline on entry; partial IO and unrelated progress do not reset it. When the batch accepted at the transition into fixed point remains buffered, its original phase deadline remains attached until that batch is fully written and flushed to the adopted IO; that batch is the settled round’s final request item, under its Requesting deadline. Fixed-point or clean-close publication waits for that boundary; the deadline is never reset or extended.

A port selects a session’s operand

A connected carrier takes its local operand from one source fixed at construction:

A preface MAY carry its sender’s port, what it wants to talk to over this carrier; a carrier sends its configured port, if any, in every preface. A direct pair has no port. Once a selecting carrier has consumed a logical session’s peer preface, it asks the host for that session’s operand with the peer’s port or its absence, before announcing an operand and without reading further peer input. The carrier owns no operand for the session until the host answers, and its prefacing deadline still runs. The host answers with one prepared operand and an optional expected peer By, or refuses. A refusal fails the logical session, and with it the carrier, as PeerProtocol("port refused"). An answer that a fixed operand could not be constructed with fails it with that local category: an expected peer By without confidential-channel or channel-bound assurance is Integration, and an operand Blob above 1 MiB LimitExceeded. The selected expectation is checked at the session’s proof phase as a fixed one is. A fixed-operand carrier serves whatever port it receives.

A host MAY open a selecting carrier without a local participant. The host’s first answer then also names the participant, and the carrier adopts its operand cache, record staging, and position-or-terminal-failure signal before constructing the first session; until that answer the carrier owns its transport and prefacing deadline but no participant, store work, or subscription. The participant is fixed for the carrier: a later answer naming another participant is a refusal, and fails the session as PeerProtocol("port refused").

A port selects a session’s operand and, on a carrier opened without a participant, that participant; it is not identity or authority. It MUST NOT become a fact, plan or proof input, or record, and is never admitted, advertised, observed, or exposed to policy. Every fresh preface pair consults the selector again, including a peer re-preface; policy replacement on a selecting carrier is unavailable and returns Policy, because the selector supplies each session’s policy. The port of the latest peer preface remains readable from the carrier as a diagnostic.

Nonce, proof, and operand establishment

Each logical session begins only after the carrier has accepted its local ILTP 0.13 preface, consumed the peer’s preface, and, when selecting, received the host’s operand. The role-mapped nonce texts are Challenge-side0 and Challenge-side1. They MUST be canonical B64A encodings of fresh unpredictable nonzero 32-byte values and MUST differ within the pair. The prefaces are framing and reset cuts, not policy facts.

The fresh session then follows stable semantic phases: side0 proof, side1 proof, side0 operand, side1 operand, side0 delivery, and side1 delivery when side0 reports side1’s operand missing. Each phase receives the ordinary absolute phase deadline. Expiry in side0 delivery reports Side0Operand and in side1 delivery Side1Operand. A proof phase carries one item, either ::as unknown or an ::as item containing one fully valid minimal Seal. A proof Seal wraps an empty Blob and a Plex with exactly these fields in canonical order:

Challenge-side0: <side0 preface nonce>
Challenge-side1: <side1 preface nonce>
Proof-Profile: lace-iltp-peer-proof-v3
Proof-Role: side0|side1

This is the unbound form. ChannelBound(binding) adds exactly one Channel-Binding line between Challenge-side1 and Proof-Profile, containing the canonical encoding of the local opaque binding defined by 060. No other field is allowed. Each displayed field is singleton. The current proof phase fixes the sender role, and Proof-Role MUST match it. No other Plex field is allowed. A sender decodes its own preface nonce and uses those 32 bytes as the Seal Mark auxiliary input. The Mark subject is the embedded Plex-record digest. An unbound enabled side without a By-secret value sends an empty proof but may discover a peer that presents one. Disabled sends an empty proof and derives no PeerConfidential, but still validates a received unbound proof completely. A bound context requires both a local By-secret and a nonempty peer proof. Missing, malformed, duplicate, unknown, or different binding fields fail as PeerProtocol; an unbound context MUST reject a bound proof and MUST NOT treat its binding as an unchecked annotation. There is no retry or fallback.

Validation first checks the complete Seal, nested records, hashes, and Mark, then exact profile, empty Blob, role, and field shape, then both challenges, then the binding against the immutable local context, then any expected peer By, before advancing the proof phase. Proof text cannot select assurance or a binding method. If either raw endpoint is disabled, the pair derives no connected peer authority. Lace-060 supplies byte-exact proof vectors.

For each fresh logical session, the carrier supplies that session’s expected peer By, the fixed operand’s unchanged one or the selected one, to establishment. After normal validation of the received peer proof and before advancing that proof phase, establishment MUST compare the live proof’s validated By with the expectation when present. An empty proof or a valid proof from a different By MUST fail as PeerProtocol with explanatory detail, before operand exchange or application-record work. Malformed proofs retain their ordinary validation failure. No expectation supplies a runtime fact or substitutes for live proof; absence of an expectation leaves proof behavior unchanged. Policy replacement repeats this check with fresh proof; changing a fixed expectation requires recreating the carrier.

Proof bytes are control material only. They MUST NOT be admitted, assigned a StoreRecordId, projected into facts, advertised, transferred, or emitted as application events. Complete proof, policy announcement, policy answer, and policy-body items, including their labels, count toward the logical session’s establishment received-control budget.

The operands then follow by hash, role ordered as 060 fixes. Each side announces the H3 B. hash of its operand Blob. A side holds the peer’s operand when the hash equals its own operand’s or names one in its operand cache; otherwise it reports the operand missing, and the peer delivers the Blob in its next turn. A delivered Blob fully validates under 010, hashes to the announced value, is at most 1 MiB, contains one canonical 030/040 module, and remains setup material only. A peer operand, held or delivered, whose canonical Blob is larger than the operation’s max_operand_bytes fails with LimitExceeded. Once it knows both operands, each endpoint freezes freshly derived authority, constructs the same new immutable plan, and begins local advertising. Malformed, false, wrong-family, reflected, replayed, duplicate, unrequested, missing, or out-of-order proof or operand input is PeerProtocol; local nonce derivation or proof construction failure is Integration. Fresh nonces, proof, and operand announcement apply to every logical session; establishment has no clock-skew, expiry-window, replay-cache, or plan-reuse mechanism.

An operand cache holds peer operands by Blob hash, most recently used first, up to a configured number of entries; zero entries hold none. Each validated delivered operand enters it. It is local runtime state that one Lace shares among its connected operations, and it is never persisted, admitted, observed, or exposed to policy. A carrier given no Lace’s cache uses its own. A side’s own operand needs no entry.

Peer advertisement facts

Request policy reads the current complete peer listing through:

Advertised(Record)
AdvertisedField(Record,name,index,value)

These are receiver-owned discovery claims, not checked record facts. Sender role, stream direction, session, and route provenance remain outside Datalog. The facts are available only to SelectAdvertisedCandidate/1 and private helpers reachable exclusively from that facet, as defined by 030 and 040.

For H3 fields, every advertised name/value pair satisfies 010’s complete field-line bound, and indexes use 020 canonical occurrence text. When the plan schema requires By, a Seal projects exactly AdvertisedField(Seal,'By','0',by_value).

In the policy fact view, one advertisement record has this shape:

Advertised('<record>')
AdvertisedField('<record>','<name>','<index>','<value>')
...

Advertised precedes that record’s field rows. Field rows contain exactly every 020 occurrence selected by the plan schema, ordered by field name bytewise and then numeric occurrence index. A schema requiring all fields includes every occurrence. Rows outside the schema are forbidden. Records are ordered by bytewise order of their canonical hash text; local admission order is never wire order. Lace-060 encodes these facts as + HASH entries with indented field lines; occurrence indexes are implicit in each name’s line order.

A listing contains each advertised record at most once. Duplicate records, duplicate (name,index) rows, noncanonical indexes, field names that are neither 010 field names nor 020 synthetic names, invalid values, omitted required projections, false projections, out-of-schema rows, and rows out of hash order are peer protocol failures.

Each endpoint produces exactly one complete listing and one request set per round. A listing is one semantic value: the frozen complete local listing at the sender and the complete peer listing at the receiver. A direct pair passes it as one typed value and may pass the sender’s change since its previous listing beside it, so the receiver need not compare listings; the complete value remains the listing. A connected carrier encodes it as one 060 ::offers-changed item against the previous listing, extended after a fenced round by the records its sender requested, except in a logical session’s first round, which uses 061 listing reconciliation. The complete peer listing is the listing those items materialize, published atomically once complete; partial reconciliation or delta state is never a listing. The received-control budget bounds the materialized listing as 060 accounts it.

Immutable round and output snapshots

Each endpoint freezes one coherent finite local record-fact boundary when its advertisement evaluation begins. That round record boundary supplies local record facts and StorePosition to both the advertisement and request evaluations. Each output separately freezes its other inputs and results when that output begins; later local commits cannot alter either output in the round.

An advertisement snapshot freezes:

Advertisement evaluation has no peer-advertisement fact source. A side advertises exactly its frozen 040 MaySend(Record) and Have(Record) output. A transmission veto produces an empty listing. Each selected hash, retained local identity, and complete schema projection is a frozen send commitment.

Request snapshot

An endpoint enters Requesting only after its local advertisement listing has been accepted by its next owner and its complete peer advertisement listing has been materialized. It atomically publishes that peer listing, starts request evaluation immediately, and freezes:

A side requests exactly the unique hashes for which:

MayRequest(Record)
and Advertised(Record)
and not Have(Record)

hold in that snapshot. A reception veto produces an empty request set. On the wire, a ::want item lists those hashes in strictly increasing bytewise order, reporting the receiver’s frozen decision; peer input cannot define the receiver’s generated policy predicate.

An endpoint enters Answering only after its local request item has been accepted and its complete peer request item has been received. Both endpoints therefore freeze both request sets before transferring records, but they may reach that boundary at different times. A local commit after an endpoint’s round record boundary freezes cannot affect its advertisement or request in that round; it may affect a later mandatory or open round.

Symmetric round progression

Each endpoint follows these four local phases:

Advertising

Both endpoints start local advertisement evaluation independently. Each sends its complete listing as soon as it is ready; a connected carrier carries it as 061 reconciliation or a 060 delta under this phase’s single deadline. An endpoint enters Requesting after every local listing output is accepted and the complete peer listing is materialized.

Requesting

Each endpoint starts local request evaluation immediately on entry and sends its complete request set as soon as it is ready. After its own request set is accepted and the peer request set is received:

either frozen request set is nonempty -> Answering
both frozen request sets are empty     -> FixedPoint

When both are empty, no response can follow, so the two request items are the round’s settled boundary; no fence is sent, and a peer fence in that round is a peer protocol failure.

Answering

An endpoint concurrently:

One side’s store latency MUST NOT prevent the other endpoint from starting or progressing its symmetric work. An endpoint enters Fencing when all its incoming and outgoing response obligations have settled. It does not wait for the peer to enter Fencing.

Fencing

Each endpoint emits one standalone ::round-end item immediately on entry. A peer fence may arrive while the local endpoint is still Answering and is retained in that round’s dedicated peer-fence slot. No endpoint emits more ordinary content for a round after its local fence.

After the local fence is accepted and the peer fence is received, the endpoint enters the next Round.Advertising. Every frozen request therefore forces another complete round, including a request whose admission was a duplicate. Repetition depends on the union of the two frozen request sets, not advertisement comparison, store novelty, or a result counter.

A fixed point does not claim that stores are equal. It means neither side requested a record in the settled round under this plan and these snapshots.

Transfer commitments and validation

Each frozen request creates exactly one response obligation. The known request set determines response-phase completion; there is no response-end control. A response is one complete stored record whose glyph hash identifies the matching outstanding request, carried in a ::response item on a connected route.

The sender loads the matching frozen commitment by retained StoreRecordId. It MUST NOT reevaluate selection, exposure, or directional vetoes. A missing row, wrong hash, or different immutable bytes at that identity is a terminal store or integration failure.

The receiver validates the response’s requested hash, record structure, embedded hashes, and Seal Mark. It projects the record through the plan schema and requires exact equality with the remembered advertisement record. Invalid bytes, an unrequested record, wrong hash association, or any projection mismatch is a peer protocol failure and MUST NOT produce record facts.

A valid response is admitted through the ordinary store path before its obligation settles. Duplicate admission settles successfully. A response phase completes only after every obligation has a received, validated, and settled response. There is no successful per-record negative response.

RecordSent is produced when a committed response is emitted. RecordSaved is a local observation after valid receiver admission settles. Fixed-point entry and clean closure are one-time lifecycle observations. These observations do not change protocol state or publish store positions. Policy replacement has no observation or activation event.

State-local peer input and backpressure

Each round state owns only the peer slots required by its current progress:

Per-direction stream order permits bounded phase skew. A matching peer reconciliation item, delta, or typed listing may fill its dedicated slot while local evaluation is pending. A peer fence may fill its dedicated slot while local Answering finishes. At fixed point, one peer listing fills the next round’s peer-listing slot and starts that round.

Input is validated immediately against the owning state. Duplicate, skipped, wrong-family, unrequested, or otherwise out-of-order input is a peer protocol failure; it never enters a general semantic queue. At most one complete decoded item may wait for immediate machine handoff.

A connected host reads or decodes semantic input only while the current state has a legal free peer slot and no StoreCall is active. While StoreCall is active, the endpoint consumes no peer input, starts no other effect, and relies on transport backpressure. Transport-buffer overflow is a transport failure, not a semantic response queue.

StoreCall ownership

A sans-IO endpoint owns at most one active opaque StoreCall. It contains machine identity, side, request data, the suspended continuation, and an empty or filled complete response. Submission consumes the active call exactly once. While it is active, that endpoint accepts no peer input or policy replacement and starts no second effect. A direct pair may own two concurrently, one per endpoint; either sibling may otherwise continue independently, but routing into a blocked endpoint waits.

Polling exposes borrowed request access and complete-response filling on that same object. The host snapshots request data, executes it against the endpoint’s policy-neutral store, reacquires the active StoreCall, fills its response, and submits once. It does not create another response owner. Wrong machine, wrong kind, incomplete coverage, and duplicate completion are integration failures. Pending execution never becomes empty facts or a store outcome.

Exact-load and store results are positional against the ordered request retained by StoreCall. Load outcomes contain loaded record bytes or Missing; store outcomes contain disposition and returned StoreRecordId. They do not echo requested hashes, requested identities, input hashes, or response slots. Loaded bytes are still validated against their requested or frozen expected hash. Broad-query discoveries, current StorePosition, and typed store errors remain actual result data.

The runtime-owned Lace that adopted the store owns mutating execution through durable-outcome classification, current-position refresh, current-StorePosition publication, and response submission. A store error remains an error even if durable progress occurred; the Lace still publishes confirmed progress once.

Every terminal transition retires the active StoreCall in its semantic owner: a connected SessionMachine retires its endpoint effect, and a DirectPair retires both endpoint effects. ConnectedCarrier does not own or separately retire session-held StoreCall. If cancellation, timeout, peer failure, local failure, or owner retirement wins after execution starts, non-cancellable work may finish while retaining its owning Lace long enough to classify and publish confirmed durable progress, but it MUST NOT submit to the retired machine. Later polls MUST NOT expose stale StoreCall; terminal retirement belongs only to the semantic owner.

Peer-output ownership

An endpoint owns at most one retained peer output. Polling borrows that output; it does not clone the item list.

A direct pair may accept one output in each direction concurrently. One direction MUST NOT block acceptance in the other. A connected writer owns one accepted batch, encoded as it is written, and its offset until every byte is written; a batch may contain one or more ILTP items from one accepted machine output. Machine phase may advance after output acceptance, not IO flush, but the batch accepted at the transition into fixed point, the settled round’s final request item, retains its absolute Requesting deadline until fully written and flushed. Bounded completion, fixed-point observation, and clean close MUST NOT be published before that boundary. On replacement, an accepted old batch drains completely, unaccepted old output is dropped, the old encoding’s end mark follows when it has one, and the fresh preface is the next accepted output; proof and operands cannot overtake it.

A terminal failure drops retained output and initiates connected transport closure immediately, including after a partial write. No further output is submitted and no terminal protocol item or end mark is generated. Bytes already handed to the underlying IO platform may still arrive; terminal retirement does not recall them or establish whether the peer saved their records.

Round-scoped concurrent commits

An interlace does not pin a logical-session-start store snapshot. Each endpoint obtains one finite coherent StorePosition boundary when its advertisement evaluation starts in each round. Its advertisement and request evaluations both use that boundary.

A local record visible at the round boundary may affect either output. A commit after that boundary cannot alter either output in the round. An unrelated external commit does not force an additional active round. Frozen requests force repetition independently of store novelty.

Fixed point and open operation

FixedPoint is the sole successful settled protocol state. A bounded operation settles its output and route and then returns. An open operation remains at the fixed point until local store progress or a peer advertisement starts another round, replacement starts another logical session, or closure ends the operation.

Every fixed-point entry creates one fresh opaque FixedPointId, produces one fixed-point observation, and contributes one FixedPointWakeBoundary to the machine’s FixedPointBoundary. The FixedPointBoundary contains the settled round and one independently tokened wake boundary per endpoint. Each wake boundary contains that fixed-point identity and the terminal round’s local record-fact StorePosition boundary.

Later polls wait; they do not reproduce the entry observation.

Fixed-point entry commits the semantic result, but a connected bounded host does not return until required final output and raw byte transport settlement finish. It stops delivering peer input to the machine. Under the settled round’s Requesting deadline, it then writes and flushes the final batch, writes and flushes the 065 end mark of a compressed outgoing encoding, and shuts down the writer, also after a failed end-mark write. Meanwhile it reads the peer direction until it ends, decoding and discarding any further item, so neither endpoint’s final writes wait on the other’s reads. It releases the reader and writer only once both finish: releasing IO while the peer still writes can make the transport reset the connection and destroy output the peer has not yet read. If a peer preface linearizes before this boundary, the host follows replacement instead.

The operation completes when the end-mark write and the shutdown succeed. On a transport without half-close, such as a WebSocket, shutdown closes both directions, so a peer that completed first can make either step fail in a correct exchange. A failed step, including failed delivery of output the channel owner accepted, therefore still completes when the peer direction ended cleanly: boundary EOF as 060 defines it, with no further item. Otherwise that failure stands. If the peer direction has not ended by the deadline, the operation fails with Timeout(Requesting).

An open host uses each Lace-owned retained position-or-terminal-failure signal. It closes the registration race in this order:

  1. subscribe to the Lace state signal;
  2. install the endpoint’s FixedPointWakeBoundary from the reported FixedPointBoundary;
  3. read the signal’s retained state;
  4. retire the operation if that state is terminal failure; and
  5. otherwise sleep only when the retained position is not greater than the wake boundary’s position.

A local position advance starts Round.Advertising immediately. The resulting listing, a delta on a connected carrier, is the peer’s round-start notification. A peer listing received at fixed point also starts Round.Advertising, stores the complete listing in the new round’s peer slot, and starts local advertisement evaluation concurrently. A round started at fixed point is a delta round on a connected carrier whichever side started it. Crossed advertisements naturally belong to the same new round. Neither role has priority for an open round.

A position wait captures the complete boundary, including FixedPointId. Delivery is legal only while the endpoint owns that exact fixed point. If a peer advertisement, logical-session replacement, or another transition has retired it, the host discards position readiness for that stale boundary; the active output snapshot or next fixed-point wait covers any store commit. Retained Lace terminal failure is host lifecycle rather than position readiness and retires every still-subscribed operation using that Lace.

Ordinary boundary EOF at fixed point, at an item boundary and at the end of the peer direction’s encoding under 060, transitions once to Closed(PeerClosed) and is clean for bounded and open hosts. Cancellation transitions once to Closed(Cancelled). Optional local work after a bounded peer closes remains eligible for another session.

Hard policy replacement

Hard replacement changes only the executable local operand. Preparation occurs before touching the carrier or direct pair. Applying the already staged operand is a successful no-op. Applying the current prefacing operand is also a no-op. Applying the running operand cancels any different staged replacement and leaves the running session unchanged.

On a connected open interlace, replacement is synchronous staging through the same exclusive mutable owner that drives the interlace. Success replaces the operand in Prefacing or stores at most one replacement in Running; a later successful call may supersede or cancel it before stepping. Staging MUST NOT poll or retire a machine, read peer input, execute StoreCall, touch the writer, deliver or create observations, or mean that the replacement has activated.

At the start of the next ordinary carrier poll or step, before endpoint work or fixed-point watch delivery, a staged replacement atomically retires the complete logical session, including its retained listings and reconciliation state, drops machine-owned unaccepted output and unsettled observations, and enters reset prefacing with the staged operand and a fresh local nonce. An already writer-owned old batch drains, then the old encoding’s end mark when it has one, before the fresh raw preface. While awaiting the peer preface, complete old peer items are canonically decoded and discarded under the received-control budget; they are never applied or semantically validated. Malformed framing remains terminal because a preface cannot cut through an item.

A fresh peer preface delivered to a running carrier performs the same retirement, extracts a fixed carrier’s current local operand or discards a selected one, enters reset prefacing with the received peer nonce and port and a fresh local nonce, and emits its preface after any old writer batch and the old encoding’s end mark. A preface received during proof, operands, rounds, or fixed point is therefore a hard reset. Crossed replacement forms one preface pair; a second peer preface before construction of the fresh machine is a duplicate peer-protocol failure. Replacement while already prefacing only replaces the forming local operand and emits no additional preface.

Prefacing has one absolute deadline covering writer drain, local-preface acceptance, canonical old-input discard, peer-preface receipt, and operand selection. Once both prefaces and the operand are owned, the carrier constructs one fresh machine at Side0Proof. The fresh logical session repeats proof, operand announcement, immutable plan construction, and ordinary rounds. It derives fresh authority and accounting. The old session is fully retired before the fresh machine is constructed.

Endpoint-exclusive StoreCall prevents staging or peer-preface delivery to that endpoint until execution, durable-position publication, and response submission settle. A direct replacement waits for both endpoint StoreCall effects when present. At the next direct poll or step it atomically retires both endpoints and their plan, drops unaccepted typed output and machine-owned observations, and constructs a fresh direct pair from the fully prepared operand pair with the same explicit authorities and limits. Direct replacement recreates the pair as one operation rather than replacing one slot independently.

EOF and failure

EOF during prefacing, establishment, or an active or mandatory round is premature and is a peer protocol failure. EOF in the middle of a preface or codec item, or before a compressed encoding’s end mark, is framing truncation and is also a peer protocol failure. Every non-EOF transport error remains a transport failure. Valid records already durably admitted remain after failure.

Terminal errors use these categories:

Malformed or hard-cap peer input is PeerProtocol, not a local limit. Evaluation work, output size, transferred-byte accounting, and peer operand size budgets produce LimitExceeded. A timeout is not a resource limit.

A connected host initiates transport closure immediately on local terminal failure without waiting for a peer close acknowledgment. The peer may observe transport failure, framing truncation, or premature boundary EOF. No wire error report is promised. An incomplete operation may have saved records; only a successfully reported fixed point confirms that its requested transfers settled. That confirmation does not promise permanent retention or independently attested remote persistence.

Established transport obligations

Applications establish protected IO before Lace adopts it. Dialing, transport handshakes, their deadlines and cancellation belong to that external owner, not an ILTP phase. Empty-store disposal drives no ILTP; it does not imply that the application performed no prior transport establishment.

The adopted writer’s flush completes when the local channel implementation has accepted ownership of all preceding plaintext. The channel implementation MUST bound what it buffers and then owns that output’s required processing, including any encryption, and its delivery or failure. Flush promises neither network output nor remote receipt. The final accepted batch’s original phase deadline covers flush before fixed-point publication, bounded completion or clean close. Shutdown MUST settle the channel implementation’s required owned output and report its failure as an IO error; abort retires transport without draining arbitrary queued work.

A protected reader MUST deliver only authenticated plaintext and bounded ingress. Protection failure MUST surface as an IO error, never successful EOF. Such IO errors are Transport; malformed ILTP remains PeerProtocol. After adoption, ordinary legal-input and active-StoreCall gates apply. Reads, writes, flush, shutdown and cancellation need independent progress within the adapter’s bounded buffers. Dropping a borrowing IO future does not release retained transport progress. ILTP budgets count decoded canonical ILTP bytes, not 065 stream encoding or outer transport framing.

Deadlines

ILTP deadlines are host-owned and attach to stable carrier-prefacing or endpoint phase tokens. Each token receives one absolute deadline on entry. The host retains the Requesting token and deadline of the final request item that remains buffered across the machine’s transition to fixed point until that batch is written and flushed; a bounded host retains that deadline through bounded completion. With active StoreCall, the connected host races only that execution, deadline, and cancellation; otherwise it races legal peer input or EOF, retained write progress, deadline, cancellation, and any legal fixed-point watch. Event reads, partial IO, replacement staging, and progress by another endpoint do not reset or extend a deadline. Fixed-point waiting uses store watches rather than a phase deadline.

Claiming a connected participant transfers its IO to the operation. A caller may signal runtime-local cancellation but MUST NOT directly close claimed IO. The runtime retires the machine and transport, waits for already-started store work through durable-position publication, and reports language-native call cancellation. When an open operation is cancelled at fixed point with an idle writer and a compressed outgoing encoding, the runtime first offers the 065 end mark to the writer once. If the writer accepts it without waiting, transport closure follows it; otherwise closure proceeds without it and the peer observes framing truncation. Dropping a Rust open operation performs the same retirement, including this offer, without a waitable result. Cancellation is not an ILTP item, runtime fact, bounded terminal, or resource limit.

Limits

Portable hard caps are fixed:

Item Hard cap
control line 129 bytes excluding LF
complete ILTP item, including framing 64 MiB
operand Blob 1 MiB
operand Blobs sent per direction per logical session at most 1
H3 Blob data 32 MiB, from 010

One operation also has local configurable lifecycle limits:

Limit Default Scope
max received control bytes 64 MiB one received direction and prefacing, establishment, or round
max transferred record bytes 1 GiB one transfer direction and round
max evaluation work 10,000,000 units one output in one round
phase timeout 30 s one prefacing phase or one endpoint semantic phase
max operand bytes 1 MiB one peer operand Blob, held or delivered

These values are local and are not exchanged. Each connected host owns its carrier’s operation limits; one direct operation owns one limits value for the pair. Implementations MAY configure lower operation values but MUST support the defaults. The phase timeout and evaluation work MAY also exceed their defaults: the phase timeout is any positive duration of at most 2^64 − 1 milliseconds and evaluation work any positive count of at most 2^64 − 1 units, since legitimate work grows with the selected records. Fixed hard caps are not configuration choices. Replacement starts fresh logical-session accounting without changing configured values or adding a replacement limit.

Evaluation work counts logical candidate visits, projected fact bytes, join attempts, builtin tests, deduplication probes, and distinct aggregate witnesses. The first round of a logical session or direct pair evaluates each output in full; a later round charges each output the work of updating it with what changed since the previous round. Work on relations independent of peer advertisements is charged to the advertisement output, also when only request evaluation reads them. Store pages, allocations, and host scheduling do not define logical work. Internal scheduling bounds yield and resume; they are not outcomes.

TextMatch work

For each evaluated 030 TextMatch, let:

The total builtin charge is exactly:

N > 128:    1, then return false immediately
otherwise:  1 + B * (P + N)

Evaluation MUST charge this total once before matching from the existing output evaluation-work budget. It includes the base builtin charge; that base MUST NOT be charged again. Insufficient work takes the ordinary LimitExceeded path before matching. Oversized text is rejected without scanning its contents.

Early mismatch, literal factoring, exact-zero pieces, and other local fast paths MUST NOT reduce the charge. Source length and syntactic branch presence remain available after compilation. Thus equal canonical pattern bytes receive the same charge across runtimes, while equivalent pattern spellings may receive different charges. There is no additional matcher budget, operation option, or expanded-state limit.