Lace / docs

Lace-020 · Record Facts and Views

Tags: record, fact, view, exposure

Purpose

Lace rules reason about validated record bytes through explicit facts. This spec defines those facts and the origin-aware views used when one side evaluates peer-contributed rules. It keeps record identity hash-based while giving policies an explicit way to decide which local record facts a peer-authored rule may inspect.

This document is for storage, Datalog, and exchange-policy implementors. After reading it, an implementor should be able to expose facts for validated 010 records and evaluate peer-origin rules without exposing local record facts outside that peer’s exposure view.

Defines

Record identifiers, record fact predicates, local store admission order, fact views, exposure, origin-aware record-fact resolution, and disclosure bounds.

Record identifiers

Record identifiers are typed record hash text for a locally supported record definition. For H3 these are:

B.<b64a>.H3
P.<b64a>.H3
S.<b64a>.H3

A record identifier denotes validated local record bytes only when Have(Record) is present in the relevant fact view. Unsupported record hash formats MAY appear in peer advertisements or record-link targets, but they MUST NOT become local record facts unless their bytes validate under a locally supported record definition.

Validated record facts

A local record-fact view exposes facts only from admitted records that fully validate under 010 and every referenced suite requirement. This includes record structure, outer and embedded hashes, field rules, and Seal-record Mark verification under 009. A merely hash-matching but otherwise invalid record MUST NOT produce record facts.

All fact values are UTF-8 NFC text strings. Projected field names and values are exact; each originating name/value pair jointly satisfied the 010 complete field-line bound. The name and value remain separate fact values, and neither is truncated or omitted. A valid record’s facts are projected completely.

Local store admission order

A local fact view supplies admission order through the 030 expression AdmitOrder(Record). It is available only when Have(Record) is present in that view. The order comes from first admission; storing the same hash again does not change it.

Admission order is not derived from 010 bytes, hash-significant, a wire fact, a record identity, or a public cursor. It reveals only relative order in one local store. Protocol identity remains the record hash.

Compare(AdmitOrder(...),...) and TopK(...,PartitionBy(...),AdmitOrder(...),...) use this same visible local order. Origin-aware visibility is resolved before TopK constructs partitions or ranks candidates. A candidate with no visible independently admitted Have row has no order value and is excluded before partition construction.

Peer-origin evaluation applies exposure gating to every record used by AdmitOrder. A missing, hidden, unsupported, advertisement-only, or embedded but independently unadmitted hash has no admission-order value. Hidden records cannot create a partition, displace a retained fact, add candidate work, or cause a peer-origin resource-limit failure.

Field facts

A projection, or table view, presents these facts as one row per record identifier with selected fields as columns. The projection model is useful for porcelain, but protocol truth remains the explicit facts below.

Field represents singleton protocol fields and repeated Plex extra fields in one ordered model. Name uses the exact 010 field name where one exists. The current H3 record definition uses these field names:

Index is an ASCII decimal occurrence index for one field name within the projected outer record, starting at 0, with no leading zero except 0. Inherited Plex fields on a Seal preserve the embedded Plex occurrences and indexes while using the Seal hash as Record. Singleton fields always use index 0. Repeated extra fields with the same name use increasing indexes in canonical record order. A Field fact is set membership; duplicate same-name/same-value extra field occurrences remain distinguishable by Index.

Group, App, Name, TAI, Plex-record extra fields, and RecordLink exist for valid Plex records and for valid Seal records by reference to the embedded Plex record. By and Mark exist only for valid Seal records. In particular, a Seal with canonical public key text emits Field(Seal,'By','0',by_value). Data-Length exists for Blob records and by reference to the embedded Blob record for Plex and Seal records.

RecordLink is derived only from well-formed 010 record-link fields. Malformed record-link fields remain Field facts but produce no RecordLink facts.

Composite coordinates are not record facts. Field(Record,'Group',...) carries the Group path text; coordinate text is syntax over Group, App, and Name fields.

Canonical containment

ContainsRecord(Outer,Contained) is the complete canonical-containment projection for one admitted outer record. For H3 records it emits exactly:

Both arguments are record identifiers. Contained may occur at any canonical nesting depth; callers do not recursively close the relation. The relation carries no depth, path, role, or occurrence information. It includes only records nested by the validated record definition, not RecordLink targets or record-shaped bytes inside Blob data.

This H3 projection is immutable for the H3 record definition. A future record definition with a different containment shape uses its own record-format suffix and explicitly defines its complete projection.

Independent contained-record admission

ContainsRecord(Outer,Contained) requires admitted, validated Outer, but does not imply Have(Contained). Admitting an outer record does not independently admit, expose, load, advertise, request, send, or order a contained record, assign it a StoreRecordId, or make load-by-hash succeed for it. Have(Contained) exists only after that exact hash is admitted through the ordinary record-admission path. Query and policy evaluation never promote a contained hash into Have and remain side-effect-free over one coherent snapshot.

A store MAY privately materialize or deduplicate contained canonical bytes. That physical state is not Datalog state and does not make an unadmitted contained record independently loadable. If the contained hash is admitted later, the store may reuse those bytes while adding the ordinary admission entry and StoreRecordId. Independent sending requires Have(Contained) in the relevant local fact view; requesting an independently advertised contained hash requires the ordinary advertisement, missing-record, and policy gates. ContainsRecord may bind the checked hash used by that request policy.

Fact views

A fact view is the set of record facts available to one Datalog module during one evaluation snapshot. Fact views are explicit evaluation inputs. A Datalog engine MUST NOT read hidden wall-clock time, fetch record bytes from peers, or consult mutable external state except through explicit fact sources supplied to the current snapshot.

There are two important record-fact views:

1. Full local view: all validated record facts in the local store.
2. Peer exposure view: the subset of local record facts the local side exposes to rules contributed by the other exchange side.

Record facts are never ambient for peer-origin modules. A record-fact lookup is resolved in the context of:

fact owner, rule origin/viewer, evaluation snapshot

The fact owner controls which records are exposed to the rule origin/viewer.

Origins and viewers

An origin identifies which exchange side contributed a policy module operand for the current exchange plan. In standard two-party interlace, origins/viewers are the exchange-local side labels side0 and side1. Setup or the binding assigns side labels before rule evaluation. A module MUST NOT be allowed to grant itself a different origin by declaring text inside the lacegram.

A viewer is the side for which a peer exposure view is computed. Side labels are coordination labels, not By values, authority, capabilities, random tie-breakers, or durable peer names. They are not source-authorable terms in standard policy. Policy that needs key evidence uses explicit proof or evidence such as PeerConfidential(peer_key), Here(local_key), record Marks, or application records.

The standard mental model for two sides is:

side0-authored rules on side0: side0's full local record facts
side1-authored rules on side0: side0's side1-exposed record facts
side1-authored rules on side1: side1's full local record facts
side0-authored rules on side1: side1's side0-exposed record facts

Exposure

Exposure is whole-record declassification for rule evaluation. If a local policy exposes record P to a viewer such as side1, peer-origin rules from that side may inspect the standard record facts for P through the viewer’s peer exposure view. Lace has no field-level privacy boundary inside an exposed record. Exposure specific to a By value must be expressed with explicit key proof or evidence; exposing to side1 is not the same as exposing to that value.

Exposure is not the same as active convergence. Exposing P lets peer-origin rules reason over P as local dynamic scope; it does not by itself advertise, request, transfer, or store P. Active convergence is selected by exchange policy in 040 and executed by interlace in 050.

Local policy exposes whole records through the 040 ExposeRecord/1 facet. The exposure gate is not source-addressable: policy modules MUST NOT define, inspect, or override it. Peer-origin rules may inspect only records in their peer exposure view.

Peer exposure view composition

When multiple active local exposure constraints are composed before becoming one 040 operand, default composition is intersection. A record is exposed only when every active local exposure constraint allows it. If there are no active local exposure rules for a peer-origin operand, that peer’s exposure view is empty unless a profile explicitly defines a different local default.

A local policy MAY explicitly construct a union or expanding view, but expansion MUST be explicit local policy. Adding a local exposure constraint SHOULD narrow or preserve the peer exposure view by default.

Origin-aware record-fact resolution

Local-origin modules use the full local view. Peer-origin modules use only their peer exposure view. This rule applies to every record-fact predicate, every AdmitOrder operand, and the entire module including helper predicates.

Negation and cardinality use the same view as positive atoms. For example, if Alice’s module is evaluated on Bob and Bob did not expose Group Y to Alice, then all of these range over Bob’s peer exposure view for Alice:

Field(Other,'Group',_,'Y')
not Field(Other,'Group',_,'Y')
Cardinality(Field(Other,'Group',_,'Y'),'>=','10')

Exposure means inspectable

A peer exposure view is a declassification boundary. Anything in that view should be treated as inspectable by that peer’s contributed rules at record granularity. If that is not acceptable for a record, do not expose the record to that viewer. The peer may learn Datalog-expressible properties of that view through visible exchange behavior, including requests, advertisements, summaries, timing, negation, and cardinality.

If a Field or RecordLink fact is exposed for record P, then the record identifier P is also disclosed by that fact. Exposing Outer also discloses every contained hash in its ContainsRecord rows, but does not independently expose Contained; reading its fields or admission order still requires independently visible Have(Contained).

For peer-origin evaluation, hidden Outer records MUST NOT contribute containment facts, candidate work, resource-limit failures, or other observable policy behavior. Stores remain exposure-neutral; origin-aware evaluation owns this boundary above storage.

Standard peer exposure views MUST apply the whole-record exposure gate to every record-fact predicate, not only Have; each exposed fact independently discloses any record identifiers it contains.

Disclosure bounds

The intended bounded disclosure property for peer-origin rules is:

Holding local-authored policy fixed, peer-origin rules can influence a side's
observable exchange behavior only through that side's peer exposure view for that peer,
public runtime facts, peer advertisement facts, and intrinsic protocol facts.

Known-hash possession is an intrinsic protocol fact in the current interlace model: if a peer advertises a known hash P, request or non-request may reveal whether the local side already has P. Policy or exchange-plan identifiers may also be visible during setup, diagnostics, or cache use. These disclosures are acceptable in the current design and SHOULD be documented by bindings that expose them.

This bound does not make unsafe local policy safe. Local-origin rules that make peer-visible behavior depend on private facts are declassification policy.