Tags: interlace, exchange, reconciliation, state-machine
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 bidirectional byte transport; listening, acceptance, 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.
The host fixes carrier role and connected proof inputs before one
ILTP carrier starts. Listener/server is side0;
connector/client is side1. Every carrier has one nonempty
canonical Transport(address), one unpredictable nonzero
32-byte nonce seed, an optional local By-secret value, and one resolved
proof assurance:
Disabled
ConfidentialChannel
ChannelBound(exporter32)Each logical session begins with a fresh nonce pair and role-ordered
proof establishment, then freezes immutable Here/1,
PeerConfidential/1, and Transport/1 runtime
facts. 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 local assurance
says the complete carrier is confidential, integrity-protected, and
endpoint-confined for its lifetime. Connected hosts cannot inject final
peer authority, and authority is freshly derived rather than inherited
across logical sessions.
The public optional override is Disabled or
TrustConfidentialChannel. Omission resolves a connected
QUIB exporter to ChannelBound, canonical wss:
to ConfidentialChannel, and every other standard transport
to Disabled. Explicit disable suppresses proof authority;
explicit trust preserves an available QUIB binding and otherwise selects
ConfidentialChannel.
A same-runtime direct pair bypasses proof and receives one explicit
final SessionAuthority per endpoint. Either direct value
may omit all facts. Side labels remain protocol ownership labels, not
identity or authority.
ILTP 1.0 fixes:
lace-040-exchange-plan-v9 profile, including
its fixed lowering;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.
A connected carrier preserves transport role, address, proof assurance, channel binding when present, By-secret value, limits, and nonce generation. 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 the operand. The carrier owns exactly one state:
Prefacing(Initial | Reset)
Running(SessionMachine, optional staged replacement)
Failed(SessionError)
Closed(CloseReason)Prefacing owns one prepared local operand, local-preface
acceptance, and the optional peer nonce. 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
Round.AdvertisingA 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.
Each endpoint round has exactly one local phase:
Advertising
Requesting
Answering
FencingThe 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 listings, requests, obligations, commitments, transfer state, and peer slots. 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. 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.
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
uses the same snapshots, routing, validation, StoreCall, fences,
fixed-point rules, and limits as connected operation.
Each logical session begins only after the carrier has accepted its
local ILTP 1.0 nonce preface and consumed the peer’s nonce preface. 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 semantic fact
blocks.
The fresh session then follows four stable semantic phases: side0 proof, side1 proof, side0 operand, and side1 operand. Each phase receives the ordinary absolute phase deadline. A proof phase carries either one fully valid minimal Seal or one zero-row fact block. A proof Seal wraps an empty Blob and a Plex with exactly:
Group: lace
App: peer-proof
Name: session/side0|side1
TAI: 0000000000:000000000
Challenge-side0: <side0 preface nonce>
Challenge-side1: <side1 preface nonce>
[Channel-Binding-Hash: <b64a digest>]The current proof phase fixes the sender role. No other extra field
is allowed. For ConfidentialChannel, the binding field is
absent. For ChannelBound, it is required and MUST match the
local exporter-derived value. A sender decodes its own preface nonce and
uses those 32 bytes as the Seal Mark auxiliary input. An 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, while still validating a
received exact proof transcript. If either endpoint is disabled, the
pair derives no connected peer authority.
Proof bytes are control material only. They MUST NOT be admitted,
assigned a StoreRecordId, projected into facts, advertised,
transferred, or emitted as application events. Proof and operand bytes
count toward the logical session’s establishment received-control
budget.
The two role-ordered operand Blobs then follow. Each fully validates
under 010, is at most 1 MiB, contains one canonical 030/040 module, and
remains setup material only. After side1’s Blob, each endpoint freezes
freshly derived authority, constructs the same new immutable plan, and
begins local advertising. Malformed, false, wrong-family, reflected,
replayed, duplicate, or out-of-order proof or operand input is
PeerProtocol; local nonce derivation or proof construction
failure is Integration. Establishment has no TAI,
clock-skew, expiry-window, replay-cache, operand reuse, or plan-reuse
mechanism.
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. Group, App, and
Name values also satisfy their coordinate rules, and
indexes use 020 canonical occurrence text. When the plan schema requires
By, a Seal projects exactly
AdvertisedField(Seal,'By','0',by_value).
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.
A listing contains each advertised record at most once. Duplicate
records, duplicate (name,index) rows, noncanonical indexes,
invalid coordinates, omitted required projections, false projections,
and out-of-schema rows are peer protocol failures.
Each endpoint emits exactly one advertisement fact block and one request fact block per round. Fact-block framing completes the listing. A zero-row block is the canonical empty listing. A listing is one semantic block and MUST NOT be split. Partial transport writes do not change its ownership or completion.
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:
StorePosition;StoreRecordId identities;
andAdvertisement 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.
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 received. It atomically publishes that peer listing, starts request evaluation immediately, and freezes:
StorePosition
as its advertisement snapshot;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 listing.
Wire requests are MayRequest('<record>') rows
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 block has been accepted and its complete peer request block 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.
Each endpoint follows these four local phases:
Both endpoints start local advertisement evaluation independently. Each sends its complete listing as soon as it is ready. An endpoint enters Requesting after its own listing is accepted and the peer listing is received.
Each endpoint starts local request evaluation immediately on entry and sends its complete request set as soon as it is ready. An endpoint enters Answering after its own request set is accepted and the peer request set is received.
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.
Each endpoint emits one standalone RoundComplete() block
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:
either frozen request set is nonempty -> next Round.Advertising
both frozen request sets are empty -> FixedPointEvery 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. If the next mandatory
round would exceed the configured limit, the endpoint fails with
LimitExceeded.
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.
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.
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.
Each round state owns only the peer slots required by its current progress:
Per-direction stream order permits bounded phase skew. A matching peer 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 advertisement 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. A WebSocket adapter similarly stops decoding and retains
only bounded transport data. Transport-buffer overflow is a transport
failure, not a semantic response queue.
A sans-IO endpoint owns at most one active opaque
StoreCall. It contains machine identity, side, request
data, the suspended continuation, response construction, and
exactly-once submission state. 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 and response-builder access to 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.
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 complete encoded batch and 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 socket flush, but bounded completion and clean close MUST NOT be published until the final fence writer is empty. On replacement, an accepted old batch drains completely, unaccepted old output is dropped, and the fresh preface is the next accepted output; proof and operands cannot overtake it. WebSocket enqueue is not final flush; the host retains ownership until buffered output is empty.
A terminal failure drops retained output and closes the connected transport immediately, including after a partial write. No terminal protocol item is sent or completed.
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.
FixedPoint is the sole successful settled protocol
state. Every 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 transport settlement finish. For a byte-stream route it stops peer input, flushes final output, and closes or releases the route. For QUIB, peer-settlement authorization is legal only after fixed-point entry, the ILTP codec writer is empty, and every final ILTP byte has entered the QUIC send stream. Codec acceptance alone is insufficient. The bounded host then requests QUIB graceful finish; an open host may grant the same one-way authorization without beginning local finish. If a peer preface linearizes before this boundary, the host follows replacement instead.
After QUIB authorization, peer application close with code zero and
authenticated stateless reset are successful but distinct transport
settlement causes: PeerClose and
PeerStatelessReset. Both preserve the committed semantic
result. On an open operation either cause also delivers boundary EOF
exactly once, producing Closed(PeerClosed). Before
authorization, orderly peer close is premature EOF and authenticated
stateless reset is a transport failure; neither may be reclassified from
fixed-point knowledge alone. Nonzero application close remains a
transport failure.
QUIB owns final data and FIN retransmission, acknowledgement, normal
close, and drain after authorization. Settlement completes through the
route-removal stages defined by 060: the connection emits
RouteDrainEvent, the endpoint emits
RouteRemoval, and the host removes the exact route before
confirming removal to the connection. Post-fixed-point QUIB settlement
uses QUIB’s transport deadlines and host cancellation, not the interlace
phase timeout and not a new operation limit.
An open host uses each Lace-owned current-StorePosition watch. It closes the registration race in this order:
FixedPointWakeBoundary from the
reported FixedPointBoundary;A local position advance starts Round.Advertising
immediately. The resulting advertisement block is the peer’s round-start
notification. A peer advertisement received at fixed point also starts
Round.Advertising, stores that listing in the new round’s
peer slot, and starts local advertisement evaluation concurrently.
Crossed advertisements naturally belong to the same new round. Neither
role coordinates or has priority for an open round.
A watch 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
readiness for that stale boundary; the active output snapshot or next
fixed-point watch covers any store commit.
Ordinary item-boundary EOF at fixed point transitions once to
Closed(PeerClosed) and is clean for bounded and open hosts.
A QUIB close is submitted as that boundary EOF only under the
authorization rules above; an unauthorized close is premature even if
the semantic machine has entered fixed point but final-byte
preconditions have not settled. Cancellation transitions once to
Closed(Cancelled). Optional local work after a bounded peer
closes remains eligible for another session.
Hard replacement changes only the executable local operand. Preparation occurs before touching the carrier or direct pair. Applying an operand canonically equal to the running, prefacing, or already staged operand is a successful no-op.
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 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, 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 before the fresh preface. While awaiting the peer preface, complete old peer items are canonically decoded and discarded under the received-control budget. 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 the current role-owned local operand, enters reset prefacing with the received peer nonce and a fresh local nonce, and emits its preface after any old writer batch drains. 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, and
peer-preface receipt. Once both prefaces are owned, the carrier
constructs one fresh machine at Side0Proof. The fresh
logical session repeats proof, complete operands, immutable plan
construction, and ordinary rounds. It derives fresh authority and
accounting; there is no rollback, reset acknowledgment, generation
number, mutable plan, or old/fresh machine overlap.
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 has no wire
preface or per-slot operation.
EOF during prefacing, establishment, an active or mandatory round, or QUIB post-fixed-point settlement before final-byte authorization is premature and is a peer protocol failure. EOF in the middle of a preface or codec item is framing truncation and is also a peer protocol failure. An authenticated QUIB stateless reset before authorization and every other transport error remain transport failures. Authorized post-fixed-point zero-code close and stateless reset are the two settlement causes defined above, not failures. Valid records already durably admitted remain after failure.
Terminal errors use these categories:
PeerProtocol(detail) for malformed, oversized, false,
unrequested, wrong-phase, or premature peer input;LimitExceeded(limit) for a local configured operation
limit;Timeout(phase) for expiry of an endpoint’s current
absolute phase deadline;Policy, Store, Transport, and
Integration, each with typed source detail.Malformed or hard-cap peer input is PeerProtocol, not a
local limit. Evaluation work, output size, transferred-byte accounting,
and mandatory-round budgets produce LimitExceeded. A
timeout is not a resource limit.
A connected host closes transport immediately on local terminal failure. The peer may observe transport failure, framing truncation, or premature boundary EOF. No wire error report is promised.
Deadlines are host-owned and attached to stable carrier-prefacing or
endpoint phase tokens. Each token receives one absolute deadline on
entry. 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. Authorized QUIB finish, close, and exact-route drain likewise
do not reuse a semantic phase deadline.
Portable hard caps are fixed:
| Item | Hard cap |
|---|---|
| fact line | 1024 bytes excluding LF |
| ILTP item | 64 MiB |
| operand Blob | 1 MiB |
| operand Blobs sent per direction per logical session | 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 evaluation |
| max mandatory rounds | 16 | rounds per logical session before a fixed point |
| phase timeout | 30 s | one prefacing or endpoint semantic phase |
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. 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. Store pages, allocations, and host scheduling do not define logical work. Internal scheduling bounds yield and resume; they are not outcomes.