# 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: ```text my active constraints + peer active constraints -> shared selected record set -> validated record transfer to a fixed point ``` The security model is origin-aware: ```text 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: ```text 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 storage-context constraints; - application view constraints; - peer-specific constraints; - temporary operation constraints; - local query/expose constraints; - local send/receive restrictions. 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: ```text 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: ```text Opq_ ``` where `` 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: - operand index `0` or `1`; - each operand's origin/source label; - each operand's facet role; - each operand's canonical module bytes; - the standard export set and profile version; - advertisement-field requirements inferred from operand rules. 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: ```text 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_` 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: ```text 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: ```text MaySend(P) :- MergedSelectHave(P). MayRequest(P) :- MergedSelectAdvertised(P,S). ``` During lowering, record-fact lookups inside each operand are resolved according to 020: - local-origin operands evaluated on their own machine use the full local record view unless local policy narrows it; - peer-origin operands evaluated on a local machine use `CanQueryRecord(Viewer,P)` for the corresponding peer/viewer; - negation and cardinality use the same resolved view as positive record-fact atoms; - the entire operand, including helpers, uses the same origin-aware resolution. 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: ```text 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: - profile/lowering version; - operand `0` and `1` origins/source labels; - operand `0` and `1` canonical bytes or identifiers; - operand facet roles; - binary selector intersection order; - query-view composition semantics defined by the profile; - generated enforcement predicate definitions; - required advertisement field names inferred from rules, or an all-fields requirement; - public runtime fact surface required by the plan. 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: ```text 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('','','') ExchangePlanOperandOrigin('','') ExchangePlanRequireAdvertisedField('') 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: ```text E. ``` where `` encodes: ```text 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: ```text 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. ## Advertisement field schema requirements 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: ```text 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: ```text 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: ```text AllowQueryRecord('V.alice.H3',P) :- Have(P), Field(P,'Group',_,'X'). ``` Alice's operand contains a malicious selector: ```text 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 - A selector module that defines `SelectHave/1` but not `SelectAdvertised/2` is invalid under the standard selector facet. - A selector exchange module that defines `MaySend/1`, `MayRequest/1`, `CanQueryRecord/2`, or a generated operand-scope prefix is invalid unless a profile explicitly permits it. - A binary merge implementation that treats identical canonical bytes from different origins as semantically interchangeable is invalid under origin-aware semantics. - A peer-origin operand that references another operand's private scoped helper is invalid. - Treating peer-authored flat rules as trusted local policy without origin/facet metadata and query-view enforcement violates this profile.