Contents

Lace-040 · Exchange Policy and Faceted Exchange Modules

Lace-040 · Exchange Policy and Faceted Exchange Modules

Tags: datalog, policy, exposure, exchange-plan

Purpose

Interlace lets two laces agree on a selected record set without giving peer-contributed rules ambient access to private local facts. This spec defines the policy layer between Datalog and the 050 state machine: two side-agnostic faceted operands, origin-aware whole-record exposure, binary selection intersection, directional vetoes, request-only advertisement facts, one plan-derived advertisement schema, and immutable output snapshots.

The application model is:

my active module + peer active module
-> shared selected record set
-> validated record transfer to a fixed point

The security model is:

peer-authored rules inspect only local record facts exposed through that peer's
exposure view

The two operands and the local operand’s exposure output are the complete policy boundaries. Their intersection determines selection, and the exposure output determines the local facts visible to peer-origin rules. A host, endpoint configuration, local executable, or third policy input MUST NOT add a selected record or widen that view.

Terms

A faceted interlace module is one self-contained canonical 030 lacegram accepted under the fixed standard exchange profile. It is side-agnostic source with no stream role, viewer, slot, or operand origin.

An operand is one faceted module in ordered slot 0 or 1. A standard exchange plan has exactly two operands. Position alone gives slot 0 origin side0 and slot 1 origin side1 and determines each module’s hygienic lowering scope.

A facet is an exported predicate family with profile-defined meaning. The standard module exports SelectStoredRecord/1, SelectAdvertisedCandidate/1, ExposeRecord/1, TxDisabled/0, and RxDisabled/0.

A compiled exchange plan is the opaque immutable result of the two ordered modules and the fixed standard profile. It privately owns exactly those two modules and the one symmetric advertisement schema. A typed local slot is exactly slot0 or slot1. The plan plus that slot derives a side-local executable: both scoped operands, their origin-aware fact views, the merged selection and veto relations, and the shared advertisement schema for that endpoint.

A round record boundary is one coherent finite local record-fact boundary shared by both local output evaluations in one round. An advertisement snapshot is one frozen outbound evaluation and its complete advertisement records. A request snapshot is the separately frozen inbound evaluation begun after both current advertisement listings are complete; it adds the complete peer listing, the listing the route materialized for the session under 050, 060, and 061, while reusing the round record boundary.

Predicate	Meaning
`SelectStoredRecord(Record)`	checked local record is selected by this operand for active convergence
`SelectAdvertisedCandidate(Record)`	current peer advertisement is a request candidate
`ExposeRecord(Record)`	checked local record is exposed to peer-origin rules; sending also requires this local exposure
`TxDisabled()`	this operand vetoes transmission from its assigned side
`RxDisabled()`	this operand vetoes reception by its assigned side

Source may define each facet with zero or more ordinary Datalog rules. An absent facet has the empty relation. Source MUST NOT reference output facets in rule bodies. Exact facet arities are mandatory.

For each round, both endpoints first freeze and exchange advertisement outputs. After each endpoint has its local output accepted and receives the complete peer listing, it freezes its request output. Transfer then follows those immutable outputs. The sections below define the inputs and gates for each stage.

SelectStoredRecord evaluates only over checked local facts and immutable session-authority facts. It has no advertisement fact source.

SelectAdvertisedCandidate evaluates over the current complete peer advertisement listing and checked facts visible to the module origin. Advertisement claims remain untrusted until transferred bytes pass 010 validation and exactly match their advertisement projection.

ExposeRecord is whole-record declassification by the operand’s authoring and running side. Exposure alone does not advertise, request, or transfer a record. It has no advertisement fact source.

Session authority

Before plan evaluation, the route fixes immutable 030 base facts Here/1 and PeerConfidential/1 when present. Direct composition accepts explicit final authority. Each connected logical session derives Here from its local By-secret value and PeerConfidential only from that logical session’s valid live proof under host-asserted confidential-channel or externally established channel-bound assurance defined by 050/060; the connected host cannot inject or carry final authority across logical sessions. The channel binding and encryption settings are not runtime facts or plan inputs; this establishment mechanism does not change the lace-040-exchange-plan-v13 profile. These facts may affect outputs only through operand rules. They are neither plan inputs nor host approval, and they do not enter plan identity. Endpoint configuration and diagnostics MUST NOT become policy facts, exchange-plan or proof inputs, or protocol authority. The standard profile has no setup-time clock facts.

For a connected logical session, the carrier’s fixed stream role assigns the local module to its ordered slot. A direct interlace receives both modules in slot order. Source cannot assert or inspect slot or origin.

Advertisement dependencies are request-only

The receiver-owned discovery facts are:

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

They are available only while evaluating SelectAdvertisedCandidate/1 and private helpers reachable exclusively from that facet. Validation MUST reject an Advertised/1 or AdvertisedField/4 dependency reachable from any of:

SelectStoredRecord/1
ExposeRecord/1
TxDisabled/0
RxDisabled/0

This includes transitive dependencies through helpers, negation, cardinality, and TopK. A helper carrying an advertisement dependency cannot be shared with a forbidden facet. Request-only helpers may read the current complete listing.

Advertisement facts are source-free discovery claims. Stream role, direction, connection identity, and route state are metadata outside Datalog. No advertisement fact is a checked record fact. A peer claim cannot unlock outbound selection, exposure, or vetoes. Peer evidence affects later outbound policy only after it is requested, validated, and admitted as an ordinary local record.

Negation, cardinality, and aggregates in request-only rule graphs use the same complete listing as positive advertisement atoms. A partially received or partially materialized listing never becomes a policy fact.

Ordinary interlace is duplex. If an operand derives neither disabled facet, it contributes no directional veto.

TxDisabled() :- true.

makes that operand receive-only: its assigned side’s advertisement listing is empty.

RxDisabled() :- true.

makes that operand send-only: its assigned side’s request listing is empty.

Both facets may be derived. They may use ordinary helpers, checked record facts, immutable session-authority facts, negation, cardinality, and TopK, subject to 020 and 030. They MUST NOT depend on advertisement facts. Multiple local disabled constraints compose by union. Selection and exposure constraints compose by intersection.

A veto belongs to the immutable output snapshot it gates. For local side S, the advertisement snapshot freezes S.TxDisabled and P.RxDisabled; the request snapshot freezes P.TxDisabled and S.RxDisabled. A later fact change cannot retract or reopen that output. Directional disabling is independent of exposure; it changes the affected listing to empty while the ordinary round progression remains unchanged. Static capture and observer operands derive TxDisabled(), while provider operands derive RxDisabled().

Output snapshots

When advertisement evaluation starts, the endpoint freezes the round record boundary. An advertisement snapshot freezes:

that coherent finite local record-fact boundary;
immutable session-authority facts;
origin-aware exposure views;
stored selection, exposure, and disabled outputs;
selected hashes and retained StoreRecordId identities; and
complete canonical advertisement records.

It has no advertisement fact source.

After its local advertisement listing is accepted and the complete peer listing is received, an endpoint atomically publishes the peer listing. Its request snapshot then freezes:

the same round record boundary used by the advertisement snapshot;
the same immutable session-authority facts;
the current complete peer advertisement listing, as materialized by the route;
origin-aware checked-fact views;
missing-record results;
request selection and disabled outputs; and
the complete request set.

A local commit after the round record boundary freezes cannot affect either output in that round. It may affect a later mandatory or open round. Both request snapshots freeze before transfer starts.

Exposure views

On each side, local-origin rules use the full local record view and peer-origin rules use the peer exposure view selected by the local operand’s ExposeRecord/1 output. The whole-record and AdmitOrder requirements are defined by 020 and apply symmetrically to both operand assignments.

Exposure is evaluated and frozen for each output snapshot over the shared round record boundary. Stores remain exposure-neutral.

Side origins

The connected carrier fixes stream roles before any logical-session establishment. side0 supplies operand 0; side1 supplies operand 1 in every logical session on that carrier. Side labels are coordination roles, not identity, authority, application roles, or durable peer names. Source cannot assert or inspect its origin. Policy that needs identity uses immutable session-authority evidence such as PeerConfidential(peer_key).

Identical canonical module bytes in different operand slots are not semantically interchangeable because origin-aware fact resolution differs.

Deterministic plan construction

Plan compilation receives exactly two self-contained canonical modules in ordered slots 0 and 1. Each module MUST contain all of its helper definitions as ordinary canonical rules. Plan compilation MUST NOT resolve additional local rules or helpers or accept a precompiled local policy as another input.

For each module, implementations MUST validate canonical 030 source, reject profile-fact definitions and malformed facets, reject output facets in bodies and compiler/control predicates, reject source predicate names containing :, scope private helpers hygienically from the module’s position, enforce request-only advertisement dependencies, and compute the module identifier. The fixed profile supplies the export set and all lowering semantics.

The compiled plan privately retains the two ordered modules. The plan and one typed local slot derive the side-local executable. Its public surface MUST NOT permit mutation or accept parallel caller-supplied slot, origin, schema, or executable provenance.

Both endpoints derive the same plan deterministically from the two valid modules and the fixed profile. Wire confirmation and locally supplied plan metadata do not participate.

Resource accounting

The fixed standard exchange profile accepts at most 256 distinct rules in each finalized operand, predicate arity at most 8, and a static TopK bound at most 2^18. Local compilation and 130 constraint composition MUST apply these bounds to each complete contribution and to the complete finalized operand. Duplicate canonical contributions and duplicate rules do not consume additional slots. Interlang per-output rules, advertised specializations, and local composition wrappers count their emitted source rules, including wrappers retained by nested composition.

Each endpoint evaluates each generated output once per round. That evaluation permits at most 2^18 derived facts in each relation it builds, at most 2^18 retained facts across partitions of each TopK occurrence, and at most 1000 iterations per stratum, as 030 counts them. Every relation the evaluation builds counts, whether authored or generated by lowering; a copy predicate replaced by its source relation builds none. The generic configurable limits in 030 do not add interlace operation options or plan inputs.

Generated executable rules are not another source operand: hygienic copies, exposure wrappers, and merge rules do not consume either operand’s source-rule allowance. Their finite generation follows the two bounded operands and the fixed lowering. Implementations MUST validate the complete generated program’s arity and aggregate bounds before output specialization. Evaluation additionally uses 050’s configurable logical-work budget, not a count of all facts in the local store.

Generated selection outputs

For local side S and peer side P, lowering defines:

MaySend(Record) =
  operand0.SelectStoredRecord(Record)
  and operand1.SelectStoredRecord(Record)
  and S.ExposeRecord(Record)
  and not S.TxDisabled()
  and not P.RxDisabled()

MayRequest(Record) =
  operand0.SelectAdvertisedCandidate(Record)
  and operand1.SelectAdvertisedCandidate(Record)
  and Advertised(Record)
  and not Have(Record)
  and not P.TxDisabled()
  and not S.RxDisabled()

Each operand is evaluated in its origin-aware view. Binary operand intersection is the complete selection rule: neither endpoint nor host may add records after this merge.

The local operand’s exposure gates MaySend: a side sends only records its own operand exposes and both operands select. Knowing a hash grants no additional access. A peer-origin rule may select a record by exact hash without inspecting it, such as a link target of an exposed manifest or a hash constant, but the target still requires the sender’s independent selection and exposure. Exposing a manifest does not automatically expose or select its linked graph.

MaySend is evaluated once for an advertisement snapshot. The machine retains the selected hash, StoreRecordId, and complete canonical advertisement projection as a send commitment. A request for that advertised hash is serviced from the commitment; policy and disabled facets are not reevaluated at transfer time. Because admitted records are immutable by hash and stores expose no delete operation, the retained identity is sufficient to reload bytes. Missing or mismatched bytes at that identity are a terminal store or integration failure.

MayRequest is evaluated once for the request snapshot. Its complete output is frozen before either transfer direction begins. A record admitted after the round record boundary does not cancel a request selected from that boundary.

Policy fact changes after the round record boundary affect a later round or a later logical session. They do not retract current-round advertisements, requests, or send commitments. A compiled plan remains immutable for its logical session; hard policy replacement retires that complete session and constructs another plan from a fresh role-ordered operand pair.

Plan-derived symmetric advertisement schema

The plan computes one exact symmetric advertisement schema from every reachable AdvertisedField/4 dependency in the two request-only rule graphs. Dependency analysis includes helpers, negation, cardinality, and TopK candidate relations.

A constant field-name argument requires that exact name. A non-constant field-name argument requires the complete generic 020 Field projection. The all-fields form ranges over every field name and occurrence projected for each advertised record; it is not a fixed field-name registry. Advertised/1 requires no field. PartitionBy(...) adds no dependency. The resulting union is used in both stream directions even when only one local request evaluation needs a field. This intentional over-projection keeps one plan-owned schema.

The plan-derived schema is the sole advertisement schema in both directions. Implementations MUST NOT advertise fields outside it, omit occurrences inside it, truncate valid fields, or substitute checked Field facts for advertisement claims. A name-specific schema includes every occurrence of that name projected by 020, including inherited Plex fields on a Seal. An all-fields schema includes every 020 Field occurrence for the advertised record.

The schema can change how mutually selected candidates are described. It cannot add a record to binary selection or widen the local operand’s exposure gate for peer-origin rules.

Canonical exchange plan

The standard plan transcript is UTF-8 NFC, LF-only, with no blank lines or comments. It is a deterministic function of the two ordered canonical module identifiers and the fixed lace-040-exchange-plan-v13 profile. The profile is the domain separator and fixes the canonical 030 language, including TextMatch, the standard facets, lowering, runtime-fact surface, schema algorithm, and 050 evaluation-work accounting. The first line is ExchangePlanProfile; remaining lines sort by predicate name then full bytes. Canonical bytes have no trailing LF.

Every transcript begins with these rows:

ExchangePlanProfile('lace-040-exchange-plan-v13')
ExchangePlanOperand('0','<module-0-id>')
ExchangePlanOperand('1','<module-1-id>')

ExchangePlanOperand appears exactly once per slot. The advertisement schema is represented by zero or more unique ExchangePlanRequireAdvertisedField('<name>') rows, or by exactly one ExchangePlanRequireAllAdvertisedFields() row, never both. Zero schema rows means hash-only advertisements.

The transcript contains no derived origin, fixed facet, separate lowering, runtime-fact, dynamic facet truth, output, or session-authority rows. Operand position and the fixed profile already determine those values.

The plan identifier is the 010 Blob-record hash of the canonical transcript. The transcript is derived locally and is not transferred. Changing either module or a request-only field dependency changes the plan identifier.

Canonical plan vector

This canonical module has 238 UTF-8 bytes and no trailing LF:

ExposeRecord(Record) :- Have(Record), Field(Record,'App',_,'chat').
SelectAdvertisedCandidate(Record) :- Advertised(Record), AdvertisedField(Record,'App',_,'chat').
SelectStoredRecord(Record) :- Have(Record), Field(Record,'App',_,'chat').

Its 010 Blob resource identifier is:

B.iqoRCCeq_CgxobqVC0gYoCBIUKbq3P~7mHmopRj6mBO.H3

Using that module in both slots produces this 243-byte transcript with no trailing LF:

ExchangePlanProfile('lace-040-exchange-plan-v13')
ExchangePlanOperand('0','B.iqoRCCeq_CgxobqVC0gYoCBIUKbq3P~7mHmopRj6mBO.H3')
ExchangePlanOperand('1','B.iqoRCCeq_CgxobqVC0gYoCBIUKbq3P~7mHmopRj6mBO.H3')
ExchangePlanRequireAdvertisedField('App')

The plan identifier is:

B.B_HirqJFeSbm26gMM96xw8LaV6Sk3qXXtt1pOnSMSmd.H3

The App requirement is an ordinary exact field-name dependency. Replacing the profile row with lace-040-exchange-plan-v12, adding an all-fields row alongside the exact App row, adding a trailing LF, or omitting either operand row makes an invalid standard-plan transcript; conforming plan construction never accepts or produces any of those mutations.

Local policy composition

Lace-130 compiles complete self-contained Interlang contributions and composes complete canonical policy constraints before plan construction. Private helpers remain isolated; contributed selection and exposure facets intersect, and directional vetoes union. Composition may confine guest inputs to the authoring inputs’ exposure view and remove records matching field exclusions from every facet. It still produces one operand, not another plan input or authority boundary.

A transmitted operand MUST be ordinary canonical 030 Datalog. Every connected logical-session establishment names the exact canonical operand Blob of each role-assigned slot by hash and transfers it to a peer that does not hold it. Plan construction performs no source loading or version-selection queries. Source distribution grants no independent authority.

Disclosure

The exposure boundary and disclosure property are defined by 020. Directional facets do not widen it. Request-only advertisement dependencies can make request behavior depend on peer claims, but cannot affect outbound selection, exposure, or vetoes. Host authority is inspectable only through the fixed runtime facts that a module explicitly references.

Rejection examples

Invalid modules include those that define Have/1, use malformed facet arities, reference any output facet in a body, reference protocol control predicates, define non-authoring predicates, use sourceful advertisement arities, use : in predicate names, or make an advertisement dependency reachable from any facet other than SelectAdvertisedCandidate/1. A plan is invalid if it does not own exactly two ordered modules, ignores position-derived origin, derives a second advertisement schema, accepts host approval or locally supplied plan metadata, or merges selection by anything other than intersection.