Lace / spec

Lace-040 · Exchange Policy and Faceted Exchange Modules

Tags: datalog, policy, query-view, exchange-plan

Purpose

Interlace should let two laces agree on a shared selected record set without turning peer-contributed rules into arbitrary queries over local private record facts. This spec defines the policy layer between Datalog and the interlace state machine: faceted exchange modules, operand origins, local query exposure, binary intersection merge, origin-aware lowering, and the canonical exchange plan used by 050.

The developer model remains set-oriented:

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

The security model is origin-aware:

peer-authored rules can inspect only the local record facts I expose to that
peer's query view.

This document is for profile authors, interlace setup implementors, Datalog engine integrators, and library designers.

Defines

Exchange modules, selector operands, origins, exported facets, local query exposure, active policy sets, deterministic binary intersection, exchange plans, origin-aware lowering, MaySend and MayRequest generation, prepared-route authority, and annotations/provenance.

Terms

A module is one canonical 030 lacegram plus exchange-policy metadata.

A selector operand is one module plus an origin/source label assigned by setup or a binding. A standard interlace exchange plan merges exactly two selector operands, one for each lace. Local N-way policy composition may happen inside a lace before it presents its operand to interlace.

An origin identifies where an operand came from for the current exchange plan. It is not self-asserted by lacegram text.

A viewer is the principal or side whose query view is used when evaluating a peer-origin module on a local machine.

A facet is an exported predicate family with profile-defined meaning, such as selected local records, selected peer advertisements, or local query exposure.

A faceted exchange plan is the canonical policy object that records the two selector operands, their origins, profile version, lowering rules, and required public fact surfaces for one exchange epoch. Record formats, effective advertisement field schema, and limits are negotiated by 050 hello facts and are not part of the E.* policy identifier unless a profile explicitly defines a combined session identifier.

Standard facets

A standard selector exchange module exports selection facets:

Predicate Meaning
SelectHave(P) record P satisfies this module in the local validated-record view available to the module origin
SelectAdvertised(P,S) source S advertised record P as satisfying this module in the advertisement/runtime view available to the module origin

SelectHave(P) is evaluated over record facts from 020. The record facts it can see depend on module origin and the local query view.

SelectAdvertised(P,S) is evaluated over peer advertisement facts from 050 and any record facts the module is allowed to see. Advertisement facts are discovery claims only. A record selected by SelectAdvertised still MUST be validated after transfer before it can produce record facts.

A module MAY define private helper predicates. Helper predicates are private to that operand unless explicitly exported by a profile. Merge/lowering evaluates operands in separate scopes to avoid accidental collisions.

A standard selector exchange module MUST NOT define MaySend/1 or MayRequest/1. Those are generated enforcement predicates of the lowered exchange policy.

Local query exposure facet

Local policy may define which local records are queryable by a peer-origin module through a query/expose facet. The standard conceptual facet is:

Predicate Meaning
AllowQueryRecord(Viewer,P) this local policy allows Viewer to query record P

AllowQueryRecord is a local exposure facet, not a peer selector. A peer-origin operand MUST NOT define what it may query on another side. Query/expose facets are local declassification policy and are not exchanged as ordinary peer operands unless a binding intentionally publishes them. Implementations MAY expose this facet directly or provide a higher-level authoring surface that compiles to it.

The internal query gate defined by 020 is:

CanQueryRecord(Viewer,P)

CanQueryRecord is reserved/internal. It is computed by local policy composition and MUST NOT be defined or overridden by peer operands.

Active local policy sets

Each side has active local policy for an interlace epoch. Local policy may include:

Local query/expose constraints are local inputs to compilation and evaluation. They do not need to be included in the shared exchange plan, and their exact rule text is not disclosed by this profile unless local policy or a binding chooses to publish it.

A side also receives the peer selector operand during setup. Peer-origin operands are untrusted selectors unless local policy marks them as trusted. They MUST be evaluated through origin-aware fact resolution as defined by 020.

Query-view composition

When multiple active local query constraints apply to a viewer, default composition is intersection. A record is queryable by Viewer only when every active local query constraint allows it.

For local exposure modules m1..mN, conceptual lowering is:

CanQueryRecord(Viewer,P) :-
  m1_AllowQueryRecord(Viewer,P),
  m2_AllowQueryRecord(Viewer,P),
  ...,
  mN_AllowQueryRecord(Viewer,P).

If no active local query constraints apply to a viewer, the default query view is empty unless a profile explicitly defines another local default. With the empty default, peer-origin selectors can still inspect peer advertisement facts and public runtime facts, but cannot inspect local record facts.

A local policy MAY explicitly define expanding or union behavior, but expansion MUST be intentional local policy. Adding an ordinary local query constraint SHOULD narrow or preserve the query view.

Operand origins

Setup assigns each selector operand an origin/source label. Origins MUST be stable within the exchange epoch and MUST be assigned or verified by the receiver or binding, not trusted from lacegram text or peer self-assertion. If a peer verifier is proven, the origin SHOULD use that verifier text or a label bound to it. If no verifier is proven, the binding MUST use an opaque exchange-local source label that is not treated as durable identity.

A side MUST reject or relabel an operand that claims local origin or an unproven verifier origin. If HelloSigner is the proof source for a verifier origin, the origin remains provisional until signer proof succeeds; setup MUST abort if the proven signer and assigned verifier origin disagree.

Opaque exchange-local origins

The standard opaque origin label form is:

Opq_<char>

where <char> is one B64A character. For a two-party exchange, each side first computes a full opaque origin digest from binding-assigned setup role, optional public setup nonce, optional proven verifier binding, and its canonical selector operand (facet,module-id,module-digest). The two full digests are B64A-encoded. Let i be the first character position where the two encodings differ. The origin labels are Opq_ plus each side’s character at position i. If no such position exists, setup MUST abort.

The setup role and nonce are tie-break inputs only. They are not authority and are not exposed as A/B roles. The short Opq_* label is exchange-local and MUST NOT be treated as durable identity. If a verifier is proven, the verifier is bound to the opaque origin as metadata rather than used directly as the origin string.

An operand’s origin affects fact resolution. Identical canonical module text from different origins is not semantically identical because it may resolve record facts through different query views.

Deterministic operand normalization

Inputs to exchange-plan compilation are exactly two selector operands:

For each operand, implementations MUST:

  1. Parse and canonicalize the module using 030 canonical lacegram rules.
  2. Validate that standard selector operands define both SelectHave/1 and SelectAdvertised/2, unless the operand is explicitly another profile-defined shared facet.
  3. Reject a module that defines reserved predicates not permitted for its facet, including MaySend/1, MayRequest/1, CanQueryRecord/2, and generated operand-scope prefixes.
  4. Compute the module digest from canonical module bytes.
  5. Preserve the origin/source label assigned by setup.

Operand scopes

Private helpers and exported facet predicates are scoped per operand before intersection and lowering. Operand scopes are lexical hygiene, not authority or identity. They keep private helpers such as Member(K) in operand 0 distinct from private helpers with the same name in operand 1.

This spec writes scoped predicates with abstract notation:

O0.SelectHave(P)
O1.SelectHave(P)
O0.Member(K)
O1.Member(K)

An implementation MAY flatten scoped predicates to ordinary 030 predicate names using deterministic internal names such as o0_SelectHave and o1_SelectHave, or it MAY evaluate operands in separate environments. These names are lowering details and are not exchange-plan identities. Origin/viewer labels such as Opq_<char> MUST NOT be used as predicate namespaces.

A peer-origin operand is closed by default. It MUST NOT reference another operand’s private scoped predicates. Cross-operand references are allowed only through profile-defined exported facets with explicit visibility semantics.

Binary intersection merge for selected records

Faceted selection is positive selection. The shared selected set is the intersection of the two selector operands.

Conceptual intersection is:

MergedSelectHave(P) :-
  O0.SelectHave(P),
  O1.SelectHave(P).

MergedSelectAdvertised(P,S) :-
  O0.SelectAdvertised(P,S),
  O1.SelectAdvertised(P,S).

A record is eligible for transfer only when both selector operands select it in the relevant evidence world. Local N-way policy composition MAY happen inside a lace before setup; the interlace exchange-plan interface remains binary.

Origin-aware lowering

Lowering turns selected-set policy into local enforcement predicates used by the 050 state machine. MaySend(P) and MayRequest(P) are generated mechanics, not the primary application model.

The ordinary lowering is:

MaySend(P) :- MergedSelectHave(P).
MayRequest(P) :- MergedSelectAdvertised(P,S).

During lowering, record-fact lookups inside each operand are resolved according to 020:

The lowered local executable program MAY be represented as a flat 030 lacegram after rewriting, a faceted evaluator, or another internal form. It MUST produce the same MaySend and MayRequest facts for the same exchange plan and local fact snapshot.

Profiles MAY define stricter lowerings. For example, a profile may require additional peer authorization, transport encryption, source constraints, or local receive policy:

MaySend(P) :- MergedSelectHave(P), TransportEncrypted().
MayRequest(P) :- MergedSelectAdvertised(P,S), Peer(S).

A profile-specific lowering MUST still satisfy the 050 send and request invariants.

Faceted exchange plan

The setup output is a canonical faceted exchange plan. Both sides MUST agree on the same plan for an exchange epoch before transfer depends on it.

A plan records shared policy structure, not per-link capability negotiation. It records at least:

Record format intersection, effective advertisement field schema, and limits are negotiated by 050 after both sides know the plan identifier. A binding MAY derive a separate session/capability identifier from (exchange-plan-id, negotiated capabilities).

Canonical exchange-plan transcript

The standard exchange-plan transcript is UTF-8 NFC text with LF line endings, no blank lines, and no comments. Each line is one fact using 050 fact-line constant syntax. Lines are sorted by predicate name, then full line bytes, except that ExchangePlanProfile appears first.

The standard transcript contains:

ExchangePlanProfile('lace-040-exchange-plan-v1')
ExchangePlanLowering('standard-v1')
ExchangePlanRuntime('Here','1')
ExchangePlanRuntime('Peer','1')
ExchangePlanRuntime('Transport','1')
ExchangePlanRuntime('TransportEncrypted','0')
ExchangePlanRuntime('StartTAI','1')
ExchangePlanRuntime('TickTAI','1')
ExchangePlanRuntime('ClockSkewSeconds','1')
ExchangePlanOperand('<index>','<facet>','<module-id>')
ExchangePlanOperandOrigin('<index>','<origin>')
ExchangePlanRequireAdvertisedField('<name>')
ExchangePlanRequireAllAdvertisedFields()

ExchangePlanOperand appears once for operand index 0 and once for operand index 1. ExchangePlanOperandOrigin appears once for each operand and records the semantic origin/viewer label used for origin-aware fact resolution. ExchangePlanRequireAdvertisedField lines appear for required constant advertised fields. ExchangePlanRequireAllAdvertisedFields() appears when any rule requires non-constant advertisement field access; in that case individual required field lines MAY be omitted. Public bindings negotiate exchange plans through operand/facet transcripts; they MUST NOT expose a peer-supplied flat prepared-policy path as an application API.

The plan identifier is:

E.<b64a>

where <b64a> encodes:

BLAKE3-256("lace-exchange-plan/v1" || canonical-exchange-plan-transcript-bytes)

E.* values identify exchange plans only; they are not record hashes and MUST NOT be used as record identifiers.

Local executable program

Each side compiles the agreed faceted exchange plan into a local executable program or evaluator. The two local executables may differ because each side uses its own local query-view facts and full local record store. They are still executions of the same agreed plan.

The 050 state machine observes only the generated local predicates:

MaySend(P)
MayRequest(P)

and the agreed plan identifier.

Trusted local precompilation

A runtime or build system MAY precompile a local executable policy as an internal optimization after it has constructed or loaded the agreed faceted exchange plan. This is trusted local code generation, not a public setup route and not a remote policy format.

Application-facing APIs and interoperable bindings use exchange operands, origin-aware facets, query exposure, and exchange-plan transcripts. A binding MUST NOT accept peer-authored flat 030 rules as trusted local policy unless those rules have first been represented with the origin/facet metadata and query-view limits defined by this specification.

The exchange plan records advertisement-field requirements inferred from operand rules. If any AdvertisedField(P,S,Name,Index,Value) reference uses a constant Name, the plan requires that field name. If a rule references AdvertisedField with a non-constant Name, the plan requires all fields.

During 050 hello negotiation, the effective advertisement field schema MUST satisfy the plan’s requirements. A required field name must be included in the negotiated advertisement field schema, or the schema must allow all fields. An all-fields requirement must be met by an all-fields negotiated schema.

Advertisement field schema limits what peers disclose in advertisement records. Query views limit what peer-origin rules may inspect in local record facts. These are separate controls.

Disclosure property

The intended bounded disclosure property of this policy layer is:

Holding local-authored policy fixed, peer-origin rules can influence local
observable exchange behavior only through that peer's local query view, public
runtime facts, peer advertisement facts, and intrinsic protocol facts such as known-hash
possession.

Queryable means queryable. A peer may learn Datalog-expressible properties of its query view through visible exchange behavior.

Local-origin policy that makes observable behavior depend on private facts is local declassification policy. This spec constrains peer-origin rules; it does not make unsafe local policy safe.

Annotation and provenance

Canonical lacegrams and exchange plans remain annotation-free unless a profile explicitly defines an annotated package format. Tooling SHOULD use source-map sidecars for debugging.

A provenance sidecar MAY record:

RuleSource('U.generated','R.input','U.original')
RuleGeneratedBy('U.generated','040-operand-scope','O0')
RuleGeneratedBy('U.intersection','040-intersection','SelectHave/1')
RuleGeneratedBy('U.may-send','040-lowering','MaySend/1')
RuleOrigin('U.generated','V.alice.H3')

Annotation and provenance facts are metadata. They MUST NOT be visible to Datalog evaluation unless a profile explicitly imports them as runtime facts.

Worked example

Bob exposes only Group X records to Alice’s rules:

AllowQueryRecord('V.alice.H3',P) :- Have(P), Field(P,'Group',_,'X').

Alice’s operand contains a malicious selector:

SelectHave(P) :- Have(P), Field(P,'Group',_,'X').
SelectAdvertised(P,S) :- Advertised(P,S), AdvertisedField(P,S,'Group',_,'X'), Field(Q,'Group',_,'Y').

When evaluated on Bob, Alice’s record-fact lookups resolve through Bob’s query view for Alice. The Field(Q,'Group',_,'Y') atom sees only Bob records that are queryable by Alice. If Bob did not expose Group Y, Alice’s bait record does not become requestable merely because Bob has private Group Y records.

Bob’s own local rules may still use Bob’s full local facts. If Bob writes a rule that exposes Group X behavior based on private Group Y, that is Bob’s local declassification policy.

Rejection examples