Lace / spec

Lace-050 · Interlace State Machine

Tags: interlace, exchange, reconciliation, state-machine

Purpose

Interlace is Lace’s record-set convergence primitive. Two laces agree on a 040 exchange plan, advertise validated records in the plan’s selected set, request advertised records they are missing, validate received bytes, and repeat until a fixed point or close condition.

Interlace is a pair of peer state machines, not a socket protocol. This spec names abstract events and state transitions. Concrete transports, framing, process boundaries, and APIs are bindings defined outside this state machine.

This document is for interlace engine, driver, and binding implementors. After reading it, an implementor should be able to run setup, negotiation, advertisement, reconciliation, transfer, validation, bounded exchange, and open exchange while preserving the trust boundary between advertisements and validated record facts.

Defines

Exchange plan negotiation, exchange runtime facts, peer advertisement facts, local state, state-machine invariants, ticking, advertisement, reconciliation, request evaluation, transfer, validation, fixed points, open and bounded drivers, errors, limits, and performance guidance.

Model

An interlace exchange is defined by:

• one agreed 040 faceted exchange plan;
• each side’s local record store and 020 record facts;
• each side’s local executable policy derived from the plan;
• exchange runtime facts;
• peer advertisement facts reconstructed from advertisements;
• negotiated record formats, advertisement field schema, and limits.

The local executable policy derives two enforcement predicates:

MaySend(P) and MayRequest(P) are local enforcement predicates generated by 040 policy. Application-facing APIs should describe selected record sets and convergence, not ask developers to hand-author directional transfer rules for ordinary use.

A side may request record P only when:

MayRequest(P) and Advertised(P, S_peer) and not Have(P)

and the record hash suffix is accepted by local policy.

A side may send record P only when:

MaySend(P) and Have(P)

at send time.

Advertisement facts are discovery claims. A transferred record becomes record facts only after full 010 validation. Record lookup, Datalog evaluation, and advertisement inspection MUST NOT fetch support records implicitly; any support or evidence records needed by an application must also be selected by the exchange plan.

A fixed point means there is no record that is currently requestable by a side, advertised by the peer, missing locally, and still sendable by the peer. It is not a global claim that both record stores are identical.

Setup routes

Ordinary setup uses the exchange-plan route: each side contributes one active 040 selector operand and local query/expose policy. Setup computes the agreed binary faceted exchange plan and each side compiles a local executable policy.

A runtime MAY cache or precompile the local executable generated from an agreed plan, but that cache is not a public prepared-policy setup route. Peer-authored rules enter ordinary interlace only through origin-aware 040 operands and query views.

Local machine state

Each peer runs one InterlaceMachine per link. A machine has at least this local state:

• active local operand identifier and canonical bytes;
• active peer operand identifier and canonical bytes;
• agreed exchange plan identifier and canonical bytes;
• local executable policy derived from the plan;
• negotiated record format set;
• negotiated advertisement field schema;
• local record store and record facts from 020;
• exchange runtime facts from negotiation, transport, ticking, and policy;
• current peer advertisement snapshot;
• current effective send set;
• current local advertisement records and partition summaries;
• current request set;
• incoming peer request list;
• received, rejected, sent, and not-available hash sets;
• advertisement cursor state;
• StoreRecordId cursor/high-water state for open exchanges, wake routing, and diagnostics;
• tick state for open exchanges;
• configured limits and accounting.

The machine’s peer advertisement snapshot is local state reconstructed from peer advertisements. It is not proof of record validity.

State-machine invariants

Implementations MUST preserve these invariants:

• do not send P unless MaySend(P) and Have(P) are true at send time;
• do not request P unless MayRequest(P), Advertised(P,S_peer), not Have(P), and local record-format acceptance are true in the current evaluation;
• do not treat AdvertisedField facts as Field facts;
• do not create record facts from advertisements;
• validate record hash, structure, embedded hashes, and Seal-record signature before storing received bytes or exposing record facts;
• do not enter the transfer loop until both sides agree on the same exchange plan;
• re-run setup when either active operand changes in an open exchange;
• re-evaluate after newly validated records, advertisement-state changes, runtime fact changes, or tick changes when they may affect MaySend or MayRequest;
• stop with an error rather than exceed configured limits.

Interlace fact blocks

Interlace control data is represented as UTF-8 NFC text blocks. Each non-empty line is one fact:

Predicate('constant',...)

Zero-arity facts are written with empty parentheses, for example:

HelloAllAdvertisedFields()

Fact block rules:

• lines end with LF only;
• CR and CRLF are invalid;
• constants use the 030 constant escaping rules;
• constants MUST NOT contain LF or CR;
• predicate names use the 030 predicate-name syntax;
• fact lines MUST be valid UTF-8 NFC;
• a fact block MUST NOT contain rules, comments, or blank lines.

A binding MAY exchange these blocks as text, represent them directly as tuples, or expose equivalent predicate iterators. The predicate names below define the abstract interlace event surface.

Exchange runtime facts

The interlace runtime supplies these profile-defined runtime facts to the 030 engine when present:

These runtime facts are explicit shared exchange inputs. Implementations MUST NOT add private or implementation-derived runtime facts to peer-origin evaluation unless a profile explicitly exposes them.

Peer(V) is present only when the runtime has proof that the remote endpoint is verifier V. TransportEncrypted() is present only when the runtime has proof that the active transport provides confidentiality for stream bytes. Their absence means the property is not proven to the rule engine.

Here(V) is a runtime context parameter, not a substitution token. Each side evaluates the same exchange plan with a different Here(V) value.

StartTAI(T) is the agreed exchange start time. TickTAI(T) is the shared moving evaluation time for an open exchange. ClockSkewSeconds(N) is the absolute clock skew in decimal seconds, computed from the two HelloTAI values and identical on both sides. Lacegrams that depend on time MUST use explicit time facts; implementations MUST NOT allow hidden wall-clock reads during rule evaluation.

Peer advertisement facts

Peer advertisement facts are runtime facts that describe records advertised by a peer or source. S is the source label for the advertiser. When the peer verifier is proven, S SHOULD be that verifier text. When no verifier is proven, the binding MUST provide an opaque UTF-8 NFC source label that is stable for this exchange and MUST NOT be treated as proof of peer identity.

AdvertisedField uses the same Name, Index, and Value model as 020 Field. AdvertisedField facts are claims used for discovery only. A transferred record becomes record facts only after full validation, and its validated Field facts MAY differ from the peer’s advertised claims.

An interlace link negotiates which advertisement field names are advertised. If the exchange plan references AdvertisedField(P,S,Name,Index,Value) with a constant Name outside the negotiated schema, negotiation MUST fail. If it references AdvertisedField with a non-constant Name, negotiation MUST fail unless the schema explicitly allows all field names.

Setup facts

Examples in this document use symbolic identifiers such as R.GROUP_X, E.EXAMPLE, and P.EXAMPLE.H3. Real identifiers use the encodings and hashes defined by their respective specs.

Exchange-plan setup announces the sender’s selector operand with:

A setup fact block contains exactly one ExchangeOperand fact for the sender’s active selector operand and represents the sender’s complete selector operand for the exchange epoch. Index is 0 or 1, assigned by the setup binding so that both sides compute the same binary exchange-plan transcript. Local query/expose policy is local declassification policy and is not exchanged as an ordinary operand unless a binding intentionally publishes it. The binding supplies canonical module bytes when the peer does not already have them.

Example:

ExchangeOperand('0','R.GROUP_X','V.alice.H3','selector')

Setup facts are protocol control data; they are not Datalog runtime facts exposed to the exchange plan unless a profile explicitly imports them.

Hello facts

Peers negotiate the exchange plan with hello facts:

Example when the binding proves the sender verifier:

HelloExchangePlan('E.EXAMPLE')
HelloSigner('V.EXAMPLE.H3')
HelloTAI('1640995200:000000000')
HelloTickInterval('10000000000')
HelloRecordFormat('H3')
HelloAdvertisedField('Type')
HelloAdvertisedField('Group')
HelloAdvertisedField('App')
HelloAdvertisedField('Signed-By')
HelloLimit('max_total_transferred_bytes','1073741824')

Advertisement records

Advertisement records use peer advertisement facts:

Advertised('P.EXAMPLE.H3','V.PEER.H3')
AdvertisedField('P.EXAMPLE.H3','V.PEER.H3','Type','0','P')
AdvertisedField('P.EXAMPLE.H3','V.PEER.H3','Group','0','u')
AdvertisedField('P.EXAMPLE.H3','V.PEER.H3','App','0','ding')
AdvertisedField('P.EXAMPLE.H3','V.PEER.H3','Name','0','links/1')

Each advertisement record contains Advertised(P,S) and the negotiated AdvertisedField facts available for that record.

The canonical advertisement record is a UTF-8 NFC fact block for one (P,S) pair. Advertised(P,S) appears first. Remaining AdvertisedField(P,S,Name,Index,Value) facts are ordered by Name using bytewise ascending order, then by numeric Index ascending. Lines end with LF.

The advertisement record digest is:

BLAKE3("lace-advertisement-record/v1" || canonical-advertisement-record-bytes)

Reconciliation facts

The baseline reconciliation mechanism is full listing of advertisement records for the current effective send set. Implementations MUST support full listing.

Efficient bindings MAY use partition summaries:

Prefix is the partition prefix. Count is decimal text. Root is the B64A encoding of the 32-byte partition Merkle root.

Partition summaries MUST summarize only advertisement records generated from the current effective send set. They are observable disclosures about that set.

MayRequest and availability facts

A request list uses:

MayRequest('P.EXAMPLE.H3')

A sender that can no longer send a requested record reports:

NotAvailable('P.EXAMPLE.H3')

Tick readiness facts

Open exchanges advance shared time with tick readiness facts:

TickReady(T) is protocol control data. It is not an advertisement fact and is not a Datalog fact exposed directly to lacegrams. The runtime computes the runtime fact TickTAI(T) from both sides’ latest valid readiness values.

Record transfer associations

Record bytes are binary data and are not encoded as interlace fact lines. A transfer response associates each sendable record hash with stored record bytes through the current execution binding. A record response is valid only when it matches a currently outstanding requested hash in that binding’s current transfer phase.

Transition: establish exchange plan

In the exchange-plan route, peers exchange setup facts before hello facts. Each side sends one ExchangeOperand fact for its active selector operand. A setup block MUST contain exactly one active selector operand unless a profile defines a safe empty-selection default. The block is a complete snapshot for the exchange epoch; it replaces any previous operand snapshot from that sender.

Both sides MUST obtain the canonical bytes for both operand module identifiers. If a side cannot obtain bytes for an announced module, setup MUST abort. Each module MUST validate under 030 and 040 for its facet role.

Both sides compile the same binary operand pair:

operand 0 + operand 1

Operand indexes, origins, facet roles, and module bytes follow 040. The machines compile the same canonical faceted exchange plan and compute the same E.<b64a> identifier.

Bindings may cache local executable policies derived from exchange plans, but setup still authenticates the exchange-plan identity. Peer-authored policy fragments require 040 origin/facet metadata.

Transition: negotiate exchange plan

Peers exchange hello facts for the exchange plan.

HelloSigner(V) is a proven signer fact, not a self-assertion. A runtime MUST NOT send or accept HelloSigner(V) unless the execution binding or an application-defined proof establishes that the sender controls the corresponding signing secret. When a remote HelloSigner(V) is accepted, the runtime supplies Peer(V). If signer proof is unavailable, HelloSigner is absent and Peer(V) is absent. A received HelloSigner without valid proof is a negotiation failure.

Origins in setup are assigned or verified by the receiver/binding. If setup uses a verifier origin that depends on HelloSigner, that origin is provisional until hello proof succeeds. Negotiation MUST abort if an operand origin claims a local origin, an unproven verifier, or a verifier that differs from the proven sender for that operand.

Both sides MUST use the same HelloExchangePlan value. If plan identifiers differ, interlace MUST abort unless the binding supplies the canonical exchange plan bytes and both sides compute the same identifier before continuing.

Both sides MUST include HelloTAI and HelloTickInterval. The runtime computes the shared start TAI and absolute clock skew:

StartTAI = max(HelloTAI_A, HelloTAI_B)
ClockSkewSeconds = |HelloTAI_A - HelloTAI_B|_seconds

max compares TAI text lexicographically. ClockSkewSeconds is a non-negative decimal integer string computed as floor(abs(nanosecond_difference) / 1_000_000_000) using the TAI epoch and arithmetic from 010. Both sides receive the same value.

The negotiated tick interval is:

TickInterval = max(HelloTickInterval_A, HelloTickInterval_B)

HelloTickInterval values are decimal nanoseconds, MUST be nonzero, and MUST fit within local configured limits.

When both sides agree, StartTAI(T) is set to the negotiated shared start value for both engines. TickTAI(T) is initially equal to StartTAI(T). ClockSkewSeconds(N) is set to the computed absolute skew.

HelloLimit(Name, Value) facts are optional decimal limit advertisements. For a recognized limit name, the effective limit is the minimum of the local configured limit and all valid advertised values for that name. Unknown limit names MAY be ignored. Malformed limit values or values outside local supported ranges are a negotiation failure.

Link identity

When both sides have proven signer verifiers A and B, Link-Id is:

BLAKE3(min(A,B) || max(A,B) || exchange-plan-id)

min and max use bytewise ordering of verifier text. Link-Id identifies cursor storage and diagnostics for signer-bound links. When either side lacks a proven signer, the binding MAY use a local cursor key for the connection or endpoint, but that key is not a verifier-bound Link-Id and MUST NOT be treated as proof of peer identity.

Record format and advertisement field schema

The negotiated record format set is the intersection of both sides’ HelloRecordFormat facts. If the intersection is empty, interlace MUST abort. An interlace participant MUST NOT request record hashes whose suffix is outside the negotiated record format set or its local accepted record format set. A receiver MUST reject transferred record bytes whose record format is unsupported by its local store.

The advertisement field schema is the intersection of both sides’ advertisement capabilities:

HelloAdvertisedField('Type')
HelloAdvertisedField('Group')
HelloAdvertisedField('App')
HelloAdvertisedField('Name')
HelloAdvertisedField('TAI')
HelloAdvertisedField('Signed-By')
HelloAdvertisedField('Signature')
HelloAdvertisedField('<extra-header-name>')
HelloAllAdvertisedFields()

HelloAllAdvertisedFields() is a wildcard capability. Intersecting all-fields with an explicit field set yields the explicit field set. Intersecting all-fields with all-fields yields all fields. Intersecting two explicit field sets yields only the field names present in both sets.

Advertised(P,S) is always available. Field names are exact 020 Field names.

The negotiated advertisement field schema MUST satisfy the exchange plan’s advertisement-field requirements from 040. If the plan requires a constant field Name, that field name must be included by both schemas or the negotiated schema must allow all fields. If the plan requires all fields because a rule references AdvertisedField with a non-constant Name, interlace MUST abort unless both schemas explicitly allow all field names.

Transition: advance tick

TickTAI(T) is the shared moving time used by time-dependent exchange policies during an open exchange. It exists to keep both sides evaluating rules against the same time boundary.

Both sides start with:

local_ready_tai = StartTAI
peer_ready_tai = StartTAI
TickTAI = StartTAI

When a side’s local clock reaches an aligned tick, it MAY send TickReady('<tai>'). A side SHOULD piggyback its latest TickReady(T) on ordinary control fact blocks.

A valid TickReady(T) value:

• MUST be greater than or equal to StartTAI;
• MUST NOT be lower than the sender’s previous valid TickReady;
• MUST be aligned to StartTAI + k * TickInterval for a non-negative integer k, using TAI nanosecond arithmetic;
• MUST NOT be accepted as proof of wall-clock correctness beyond ordinary clock-skew policy and local runtime trust in the peer.

The runtime computes the shared tick time as:

TickTAI = min(local_ready_tai, peer_ready_tai)

min compares TAI text lexicographically. TickTAI never decreases. When TickTAI changes, the runtime replaces the old TickTAI runtime fact with the new one and re-evaluates the local executable policy over the new fact set.

A bounded exchange normally uses TickTAI = StartTAI for its whole run. An API MAY expose an option for a bounded exchange to wait for one or more ticks before closing, but that is a wrapper close condition.

Transition: evaluate and advertise send set

Each side evaluates its local executable policy to compute:

EffectiveSend(P) = MaySend(P) and Have(P)

Before the first peer advertisement reconciliation in a round, this evaluation uses the stored peer advertisement state for the link, or an empty peer advertisement state when none exists. Each policy evaluation uses an explicit finite evaluation snapshot of record facts, runtime facts, and peer advertisement facts. Store implementations MAY use internal read snapshots or transactions to make lazy fact queries and counts coherent for one evaluation, but those snapshots are implementation details and do not define bounded interlace visibility.

A bounded exchange MUST NOT pin store ids for default visibility semantics. Local records stored before a later bounded evaluation MAY affect that exchange. A bounded exchange is not required to wait for records stored after its final fixed-point evaluation.

For each P in EffectiveSend, the side creates one advertisement record containing Advertised(P,S) and all negotiated AdvertisedField facts available from validated local record facts. An advertisement record is a claim; a receiver MUST NOT treat it as validated record metadata until the record bytes are received and verified.

Advertisement records and partition summaries MUST be computed only from EffectiveSend.

Transition: reconcile peer advertisements

Reconciliation discovers which selected records may be missing without treating peer metadata as trusted record facts. The result is a current peer advertisement state that the local machine can evaluate against MayRequest(P) before requesting bytes.

Implementations MUST support full listing of advertisement records. Implementations MAY use Merkle partition summaries, cursors, or direct in-memory access as optimizations if they produce the same peer advertisement state as valid full listing.

A cursor contains the last accepted peer advertisement records plus optional partition summaries. It is local state, not protocol proof.

For partition reconciliation, advertisement records are partitioned by the first k B64A payload characters of P, excluding the record type prefix (B., P., or S.) and hash suffix such as .H3. Record type does not participate in the standard partition prefix; records of different record types with the same digest payload prefix are in the same partition. The standard starting k is 2. A non-standard prefix length requires a profile or binding extension that includes that value in the agreed exchange plan or an explicitly negotiated capability. Child partitions append one B64A character to the parent prefix.

The root is a Merkle root over sorted advertisement record digests for that partition:

leaf  = BLAKE3("lace-advertisement-leaf/v1" || record-digest)
node  = BLAKE3("lace-advertisement-node/v1" || left || right)
empty = BLAKE3("lace-advertisement-empty/v1")

A binary tree is built over the sorted leaves and padded with empty leaves to a power of two. The root of an empty partition is empty.

After listing, the receiver verifies that the listed records match the advertised count and Merkle root. If verification fails, interlace MUST abort.

When reconciliation finishes, each side has current advertisement facts for the peer.

Transition: evaluate request set

Each side evaluates its local executable policy with:

• local record facts from validated storage;
• local query-view facts needed for origin-aware modules;
• exchange runtime facts from negotiation and ticking;
• peer advertisement facts from the reconciled advertisement state.

The extension of MayRequest(P) determines which advertised missing records the local side may request. The extension of MaySend(P) determines what the local side may advertise in the next loop iteration.

Evaluation errors are terminal for the round.

Transition: transfer and validate

Each side sends a request list as MayRequest(P) facts. A request list is a bounded subset of the current requestable missing records; it need not contain every record that is currently requestable. A request list MUST contain only hashes where local evaluation derived MayRequest(P), the peer advertised Advertised(P,S_peer), local storage lacks Have(P), and the hash suffix is accepted by the local store.

A receiver MAY validate and store a response for a hash that was validly included in the current request list even if other records in the same transfer batch would make that hash no longer requestable under a later evaluation.

A sender MAY service only a local bounded subset of the current request list in one transfer phase, for example to bound record-store lock time, store access time, record count, byte count, or stream time. For each requested hash it services, the sender checks that MaySend(P) and Have(P) are still true. If not, it reports NotAvailable(P) for that hash.

Requested hashes that receive neither record bytes nor NotAvailable(P) before the transfer phase ends are deferred. Deferral is sender-local scheduling and backpressure; it is not a record validation failure, not NotAvailable(P), and not a change to peer advertisement state. A receiver MAY request a deferred hash again in a later phase if it remains advertised, missing, and requestable.

Record responses associate requested hashes with stored record bytes. A response MAY use the 010 trailer-hash form for streaming record bytes if the execution binding supports it. A record response whose hash or binding-level response association does not match a current outstanding requested hash is a malformed or out-of-phase record response, and the receiver MUST abort the current round.

The receiver MUST validate each requested record response: hash, record structure, embedded hashes, and Seal-record signature when present. Invalid bytes or hash-mismatched bytes for a requested hash are record validation failures: they are rejected, do not produce record facts, and do not by themselves abort the round.

Drivers: bounded and open exchange

An interlace driver repeatedly applies the transitions:

1. establish an exchange plan and compile or load its trusted local executable;
2. negotiate link identity, exchange plan identifier, advertisement field schema, and limits;
3. evaluate local send set;
4. advertise current effective send set;
5. reconcile peer advertisements;
6. evaluate request set;
7. transfer requestable missing records that the peer can still send;
8. validate received records and add new record facts;
9. repeat from send-gate evaluation if record facts produced by this exchange, locally visible store facts, exchange runtime facts, peer advertisements, ticks, raw MaySend, raw MayRequest, or effective advertisements changed, or if deferred requested hashes may still be requestable;
10. report transfer metadata and, for bounded exchanges, store updated advertisement cursors and close.

A bounded exchange is lifecycle-bounded. It runs ordinary interlace until the current fixed point, then closes, unless a configured loop, transfer, time, cancellation, or error limit closes it earlier. Boundedness is not store-id snapshot isolation and is not a record-count, read-batch, request-batch, transfer-batch, or result-count limit.

A bounded exchange MUST NOT pin store ids for default visibility semantics. Records stored by another task or interlace while the bounded exchange is active MAY participate in a later evaluation, advertisement, request, or transfer loop if they are visible to that loop’s explicit evaluation snapshot and satisfy policy. A bounded exchange MUST NOT wait for future stored records after its final fixed-point evaluation; a later operation or open exchange can observe those records.

StoreRecordIds are used for wake routing, open cursors, diagnostics, and store ordering. They are not part of bounded exchange visibility semantics by default.

A bounded exchange closes when both machines have no further requestable records available from the peer under the final local record facts and current peer advertisement states, or when a configured non-lifecycle limit is hit. Ending a transfer phase because a sender-local service budget was reached is not by itself a fixed point.

An open exchange remains active after the current fixed point. Open exchanges track StoreRecordId cursors. When a side’s local records stored after its observed cursor, exchange runtime facts, tick, effective send set, or peer advertisement set changes, the driver repeats advertisement, reconciliation, evaluation, transfer, and validation until it reaches another fixed point or a configured limit.

When a side’s active operand changes during an open exchange, it sends a new setup block and both machines establish a new exchange plan. If the exchange plan identifier changes, this starts a new exchange epoch for advertisement cursors and diagnostics. Valid records already stored remain stored. Either side may close the exchange. A later reconnect starts a new interlace exchange.

At a fixed point, each side may report:

Interlace-Result {
  link-id
  exchange-plan-id
  peer-verifier
  received-hashes
  rejected-hashes
  not-available-hashes
  bytes-received
  bytes-sent
  cursor-updated: true|false
}

Non-monotonic policies

MayRequest(P) and MaySend(P) may grow or shrink when records arrive or disappear. Interlace MUST NOT assume monotonic growth, subset direction, append-only advertisements, or a unique final received record set.

With non-monotonic policies, different valid transfer schedules MAY complete with different accepted record sets. Both schedules are correct when every accepted record was validated and the final evaluation has no requestable, advertised, missing record that the peer can still send.

Applications requiring deterministic result sets SHOULD use monotonic selection rules over Have, or apply an application-level selection policy after the exchange over validated record facts.

Operation wrappers

Interlace is the primitive exchange operation between two laces. A binding MAY expose operation-shaped convenience APIs, but those APIs are local wrappers around the ordinary interlace state machine. They do not add transfer commands or wire messages.

Operation wrappers contribute ordinary local policy that is compiled into the side’s 040 selector operand before setup:

• open interlace: keep an exchange active and deliver local observations when newly validated records match a local result rule;
• get one record: contribute temporary selection constraints and local result behavior, then run bounded interlace;
• list records: use the same selected-record pattern and return a many-result local shape;
• store records: contribute local record bytes plus a sending selection constraint, interlace with a peer whose policy selects them, and report the transfer result.

Operation event streams and result collectors are runtime-local behavior. They are not invoked by core/store code, are not interlace facts, and are not visible to a remote peer.

Receipts

A receiver MAY publish a receipt after storing records. A receipt is an ordinary Seal record over a Plex record, for example:

Group: lace
App: receipt
Name: store/<received-hash>
TAI: <tai>
Stored-Hash: <received-hash>
Stored-From: <peer-verifier>

The Seal record’s Signed-By is the receiver verifier. Receipts are application-level records governed by normal rules; they are not required by interlace.

Error handling

Interlace failures are terminal for the current round unless noted.

After abort, valid records already stored remain stored. A later interlace starts from negotiation.

Limits

Implementations MUST enforce configurable limits.

Performance guidance

This section is non-normative. Optimized implementations can replace serialized fact exchange with direct data access when the logical result is unchanged.

In-memory interlace engine

An implementation can run both sides of interlace inside one process with trusted store-machine-backed access to both participants. Such an engine can evaluate send sets, advertisement states, request sets, and transfers without serializing hello facts, advertisement records, partition summaries, or request lists, but it still preserves store-machine read/load/store boundaries and does not expose raw store access as an application API.

The engine should still preserve the abstract state transitions: establish the same exchange plan, negotiate equivalent exchange runtime facts, compute effective send sets, expose peer advertisements, evaluate requests, transfer requested records, validate received records, and repeat to a fixed point.

Lazy fact sources

Record facts and advertisement facts can be generated on demand. Instead of materializing all tuples, a Datalog engine can resolve predicates by calling storage or advertisement accessors. For peer-origin modules, lazy record fact access must still enforce 020 query views.

Reconciliation bypass

When both current advertisement states are available through trusted store or diagnostic boundaries, an implementation can compute changed advertisement records or requested hashes directly and skip Merkle partition narrowing. This optimization should produce the same peer advertisement state that a valid summary/list reconciliation would produce.

Examples

First follow

1. App and server exchange active 040 modules. The agreed exchange plan selects
   Group 'u', App 'ding', and Name values under 'links/'.
2. Each side compiles the plan locally with its own query views.
3. App has no cursor for the server, so all non-empty server advertisement partitions are
   reconciled or listed.
4. App evaluates MayRequest over the server's advertisement facts.
5. App requests missing requested hashes.
6. Server sends records it can still send.
7. App validates records, stores them, and updates its cursor.

Store one local record

1. An operation wrapper has record P locally.
2. The wrapper contributes a module selecting P.
3. The server contributes ordinary acceptance constraints.
4. Setup compiles the faceted exchange plan.
5. Server receives an advertisement record for P when P satisfies MaySend on the sender.
6. Server requests P when P satisfies MayRequest on the server.
7. The wrapper sends P if P is still valid and exposed.
8. Server validates and stores P.

Evidence closure

A module can select support evidence and then use validated evidence to select more records. When this module is peer-origin on another machine, its record-fact lookups are limited to that peer’s query view on that machine.

SelectHave(P) :- Have(P), Field(P,'Group',_,'u'), Field(P,'App',_,'member').
SelectHave(P) :- Have(P), Field(P,'Group',_,'u'), Field(P,'App',_,'ding'), Field(P,'Signed-By',_,V), ActiveMember(V).
SelectAdvertised(P,S) :- Advertised(P,S), AdvertisedField(P,S,'Group',_,'u'), AdvertisedField(P,S,'App',_,'member').
SelectAdvertised(P,S) :- Advertised(P,S), AdvertisedField(P,S,'Group',_,'u'), AdvertisedField(P,S,'App',_,'ding'), AdvertisedField(P,S,'Signed-By',_,V), ActiveMember(V).
ActiveMember(V) :- Have(P), Field(P,'Group',_,'u'), Field(P,'App',_,'member'), Field(P,'Name',_,V).

A first loop may fetch member records. A later loop can select more records from the newly validated evidence.