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 local exposure are the complete policy boundaries. No host approval, route option, local executable, or third policy input may add a selected record or widen a peer-origin rule’s record-fact 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. The plan does not store separate per-operand copies of position-derived slot, origin, facet role, or lowering scope. A typed local slot is exactly slot0 or slot1. One compiled plan plus that slot is the complete provenance for a side-local executable.

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 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
`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.

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. It does not advertise, request, transfer, or authorize a record. It has no advertisement fact source.

Session authority

Before plan evaluation, the route fixes immutable 030 base facts Here/1, PeerConfidential/1, and Transport/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 enabled confidential-channel assurance; the connected host cannot inject or carry final authority across logical sessions. These facts may affect outputs only through operand rules. They are neither plan inputs nor host approval, and they do not enter plan identity. 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. The compiler 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 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. Static operation wrappers use ordinary fixed modules: capture and observer operands derive TxDisabled(), and provider operands derive RxDisabled().

Directional disabling is independent of exposure and creates no special wire transition.

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 both complete listings are received, the machine atomically publishes the current peer listing. A 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;
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. Imports, package dependencies, and linked relations MUST already be resolved and lowered into each module’s canonical bytes. 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. Its public surface MUST NOT permit mutation or accept parallel caller-supplied slot, origin, schema, or executable provenance. A side-local executable is derived from that plan and one typed local slot.

Plan derivation is deterministic and has no host approval input. After obtaining the two valid modules, both endpoints independently derive the same plan. No wire confirmation or locally supplied plan metadata participates.

Generated selection outputs

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

MaySend(Record) =
  operand0.SelectStoredRecord(Record)
  and operand1.SelectStoredRecord(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.

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 all 020 field names, including By in the v9 profile. 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.

There are no endpoint field capability offers, wildcard intersections, local executable schema expansion, or host schema approval. Implementations MUST NOT advertise fields outside the schema, omit occurrences inside it, truncate valid fields, or substitute checked Field facts for advertisement claims.

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-v9 profile. The profile is the domain separator and fixes the standard facets, lowering, runtime-fact surface, and schema algorithm. The first line is ExchangePlanProfile; remaining lines sort by predicate name then full bytes. Canonical bytes have no trailing LF.

ExchangePlanProfile('lace-040-exchange-plan-v9')
ExchangePlanOperand('0','<module-0-id>')
ExchangePlanOperand('1','<module-1-id>')
ExchangePlanRequireAdvertisedField('<name>')
ExchangePlanRequireAllAdvertisedFields()

ExchangePlanOperand appears exactly once per slot. The advertisement schema is represented by zero or more unique ExchangePlanRequireAdvertisedField lines, or by exactly one ExchangePlanRequireAllAdvertisedFields() line, never both. Zero schema lines means hash-only advertisements. The two field-requirement forms shown above are alternatives, not simultaneous example rows.

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.

Policy modules

Trusted local extended policy modules may define linked relations and compose constraints before an operand is finalized. A transmitted operand MUST be ordinary canonical 030 Datalog with no raw @. Every connected logical-session establishment transfers the exact canonical operand Blob for each role-assigned slot; plan construction never resolves local packages or providers.

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.