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. It defines fact projection for the generic fields in 010 records and evaluation of 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 application field names and values are exact; each originating name/value pair jointly satisfied the 010 complete field-line bound. They remain separate fact values and are never truncated or omitted. A valid record’s facts are projected completely.

Field facts

Field represents synthetic record kind, structural record fields, and generic Plex application fields in one ordered occurrence model. The current H3 projection uses these names:

Synthetic names start with :, which no 010 field name contains, so they correspond to no stored field line and need no reserved name. :Length counts every byte of the record’s own canonical bytes: glyph lines, structural and application field lines, the blank line, and the data. A Seal’s :Length is its own length, not that of its embedded Plex. :Type and :Length exist for every record. Data-Length exists for Blob records and by reference to the embedded Blob for Plex and Seal records. By and Mark exist only for Seal records. Plex application fields exist for Plex records and are inherited unchanged by Seal records from their embedded Plex. A rule that ranges over application fields only skips names starting with : and the structural names, as the 030 examples show.

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. Synthetic and structural fields are singleton occurrence 0. Repeated application fields with the same name use increasing indexes in canonical record order. Inherited fields preserve their embedded Plex indexes while using the Seal hash as Record. A Field fact is set membership; duplicate same-name/same-value application occurrences remain distinguishable by Index.

For example, admitting only the byte-exact Seal vector from 010 projects this complete set of record facts:

Have('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3',':Length','0','393')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3',':Type','0','S')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','App','0','chat')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','App','1','archive')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','Group','0','room7')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','Name','0','note')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','TAI','0','tomorrow')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','Data-Length','0','5')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','By','0','V.8qgOfsaEJkK1tzX51sTT9NKdM8J2SrzQq6k8cRPzvP0.H3')
Field('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','Mark','0','t9QAUgyE1c391D6RsPH_gok2OXEPTRfcp4HOa_Wcyx8143adV34c1ReKeGmWXXn6ictYPxDz5ULgqz0RK4sbPl')
ContainsRecord('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','P.roNBC0l3CG4ezmPY5F3H_pLBDBecaAYZRbOJ1aT7pqK.H3')
ContainsRecord('S.ZGEVHbEEKmCMF2aSbmbQ4~trwxANOQFmraeGg_JAp9C.H3','B.kQIYZC1_~Q_ji4~Twe2_7m9Zn2scg_Cu9zNTkbk9zq8.H3')

The application names in this vector have no special projection rules. The App indexes show inherited same-name occurrence order. No Have fact for the contained Plex or Blob follows from admitting the Seal; each appears only if it is independently admitted.

RecordLink is derived only from well-formed 010 record-link application fields. Its name and index are the same values used by the corresponding Field fact. A Seal inherits each embedded Plex RecordLink using the Seal hash as Record and preserving the Plex field index. Malformed record-link fields remain Field facts but produce no RecordLink facts.

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 records relative first-admission order within one local store. It is local metadata rather than part of 010 bytes or record identity; it is not a wire fact or public cursor. 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 before using AdmitOrder. Only a visible, independently admitted Have row has an admission-order value. Records outside that view cannot affect partitioning, ranking, candidate work, or peer-origin resource limits.

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 projects its containment rows into each fact view where that outer record is visible, but leaves each contained record outside the independently admitted set. Have(Contained) exists only after that exact hash passes through the ordinary record-admission path. Until then, the contained record is not independently exposed, loadable, advertised, requested, sent, ordered, or assigned a StoreRecordId. Query and policy evaluation are side-effect-free over one coherent snapshot and do not promote containment rows into Have.

A store MAY privately materialize or deduplicate contained canonical bytes. That physical state is separate from Datalog state and does not make an unadmitted contained record independently loadable. Later independent admission 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 uses the ordinary advertisement, missing-record, and policy gates. ContainsRecord may supply the checked hash to 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 exchange-local coordination labels assigned by setup or the binding and are not source-authorable terms in standard policy. Policy that needs identity or key authority uses explicit 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 controls which local records peer-origin rules may inspect. Active convergence is a separate process: exchange policy in 040 selects records for advertisement and request, and interlace in 050 transfers them. Exposure alone does not advertise, request, transfer, or store a record.

Transfer requires exposure: a side sends only records its local operand exposes and both operands select (040). A peer-origin rule may select a record by exact hash without inspecting it, but learning a link target or contained hash does not independently expose or select that record.

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.

The same peer-exposure-view rules govern guest rules composed under 130 inside one local operand, with the authoring inputs in the role of the local side. 130 defines that authoring exposure view, the field exclusions that remove matching records from it and from every composed facet, and the guest disclosure bound.

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 records carrying an application field Topic: private to Alice, then all of these range only over Bob’s peer exposure view for Alice:

Field(Other,'Topic',_,'private')
not Field(Other,'Topic',_,'private')
Cardinality(Field(Other,'Topic',_,'private'),'>=','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.

Facts projected from an exposed record P disclose the identifier P. 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 the record whose projection supplies each Have, Field, RecordLink, or ContainsRecord row. A visible row discloses every record identifier it contains, including link targets and contained hashes, without independently exposing those referenced records.

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, the standard runtime facts `Here/1` and `PeerConfidential/1` when
present, 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.