# 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: | Predicate | Meaning | |---|---| | `MaySend(P)` | record `P` is in the local exposed set for this peer | | `MayRequest(P)` | record `P` is in the local receive target from this peer | `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: ```text 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: ```text 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: ```text Predicate('constant',...) ``` Zero-arity facts are written with empty parentheses, for example: ```text 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: | Predicate | Arity | Meaning | |---|---:|---| | `Here(V)` | 1 | local verifier for this context, if any | | `Peer(V)` | 1 | transport-proven peer verifier for this context, if any | | `Transport(S)` | 1 | address string of the active transport connection | | `TransportEncrypted()` | 0 | active transport provides confidentiality, if true | | `StartTAI(T)` | 1 | shared negotiated exchange-start TAI | | `TickTAI(T)` | 1 | shared tick time for this evaluation | | `ClockSkewSeconds(N)` | 1 | absolute clock skew in decimal seconds | 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. | Predicate | Arity | Meaning | |---|---:|---| | `Advertised(P, S)` | 2 | source `S` advertises record `P` | | `AdvertisedField(P, S, Name, Index, Value)` | 5 | claimed record field occurrence | `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: | Predicate | Arity | Meaning | |---|---:|---| | `ExchangeOperand(Index, R, Origin, Facet)` | 4 | active 040 operand index, module identifier, assigned origin/source, and facet role | 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: ```text 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: | Predicate | Arity | Meaning | |---|---:|---| | `HelloExchangePlan(E)` | 1 | exchange plan identifier `E.` | | `HelloSigner(V)` | 1 | proven sender verifier `V..H3`, when available | | `HelloTAI(T)` | 1 | sender TAI at hello exchange start | | `HelloTickInterval(N)` | 1 | minimum tick interval in decimal nanoseconds | | `HelloRecordFormat(F)` | 1 | accepted record hash suffix | | `HelloAdvertisedField(Name)` | 1 | supported 020 `Field` name for advertisements | | `HelloAllAdvertisedFields()` | 0 | all 020 `Field` names are supported for advertisements | | `HelloLimit(Name, Value)` | 2 | decimal limit value | Example when the binding proves the sender verifier: ```text 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: ```text 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: ```text 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: | Predicate | Arity | Meaning | |---|---:|---| | `AdvertisementPartition(Prefix, Count, Root)` | 3 | partition summary | | `ListAdvertisementPartition(Prefix)` | 1 | request full advertisement records for a partition | | `NarrowAdvertisementPartition(Prefix)` | 1 | request child 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: ```text MayRequest('P.EXAMPLE.H3') ``` A sender that can no longer send a requested record reports: ```text NotAvailable('P.EXAMPLE.H3') ``` ## Tick readiness facts Open exchanges advance shared time with tick readiness facts: | Predicate | Arity | Meaning | |---|---:|---| | `TickReady(T)` | 1 | sender's local clock has reached aligned tick `T` | `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: ```text 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.` 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: ```text 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: ```text 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: ```text 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: ```text HelloAdvertisedField('Type') HelloAdvertisedField('Group') HelloAdvertisedField('App') HelloAdvertisedField('Name') HelloAdvertisedField('TAI') HelloAdvertisedField('Signed-By') HelloAdvertisedField('Signature') HelloAdvertisedField('') 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: ```text local_ready_tai = StartTAI peer_ready_tai = StartTAI TickTAI = StartTAI ``` When a side's local clock reaches an aligned tick, it MAY send `TickReady('')`. 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: ```text 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: ```text 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: ```text 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. `StoreRecordId`s 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: ```text 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: ```text Group: lace App: receipt Name: store/ TAI: Stored-Hash: Stored-From: ``` 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. | Condition | Action | |---|---| | peer verifier mismatch | abort | | exchange plan identifier mismatch | abort | | unsupported record format | abort | | unsupported advertisement field schema | abort | | malformed fact block | abort | | malformed exchange module | abort | | exchange-plan compilation failure | abort | | malformed prepared policy | abort | | malformed partition summary | abort | | advertisement list root mismatch | abort | | phase timeout | abort | | oversized fact block | abort | | transfer limit exceeded | abort with partial result | | record response with no current outstanding requested hash | abort | | record validation failure for a requested hash | reject record and continue | | requested hash no longer sendable | report `NotAvailable(P)` and continue | After abort, valid records already stored remain stored. A later interlace starts from negotiation. ## Limits Implementations MUST enforce configurable limits. | Limit | Default | Scope | |---|---:|---| | max fact block size | 64 MiB | block | | max advertisement records listed | 100,000 | partition/listing | | max partition summaries | 16,384 | exchange | | max narrowing depth | 12 | partition | | max total transferred bytes | 1 GiB | round | | max loop iterations | 16 | round | | phase timeout | 30 s | phase | ## 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 ```text 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 ```text 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. ```text 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.