# Lace-020 ยท Record Facts and Views Tags: record, fact, view, query ## Purpose Lace rules reason about validated record bytes through explicit facts. This spec defines those record facts and the origin-aware views used when one side evaluates rules contributed by another side. The purpose is to keep record identity hash-based while giving policies a safe, explicit way to decide which local record facts a peer-authored rule may query. 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 letting them inspect local record facts outside the local query view for that peer. ## Defines Record identifiers, record fact predicates, fact views, query exposure, origin-aware record-fact resolution, and disclosure bounds for queryable facts. ## Record identifiers Record identifiers are typed record hash text for a locally supported record definition. In the current H3 record definition these are: ```text B..H3 P..H3 S..H3 ``` A record identifier denotes validated local record bytes only when `Have(P)` 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 The storage layer exposes record facts only from locally stored, hash-valid 010 records. Invalid records MUST NOT produce record facts. | Predicate | Arity | Meaning | |---|---:|---| | `Have(P)` | 1 | validated record bytes for `P` are locally stored | | `Field(P, Name, Index, Value)` | 4 | one record field occurrence | | `RecordLink(P, Name, Index, Data, Target)` | 5 | one well-formed 010 record-link field occurrence | | `BlobHash(P, H)` | 2 | embedded Blob-record hash for a Plex record | | `PlexHash(P, H)` | 2 | embedded Plex-record hash for a Seal record | All fact values are UTF-8 NFC text strings. An implementation MUST reject a fact value that is not valid UTF-8 NFC or that exceeds the configured tuple value limit of the evaluating Datalog profile. ## Field facts A projection, or table view, is a presentation over these facts: choose field names and show one row per record identifier with those fields as columns. The projection model is explanatory and useful for porcelain, but protocol truth remains the explicit facts below. `Field` represents singleton protocol fields and repeated Plex extra headers in one ordered model. `Name` uses the exact 010 header name where one exists. The current H3 record definition uses these field names: | Name | Meaning | |---|---| | `Type` | record type: `B`, `P`, or `S` | | `Data-Length` | Blob-record data length as decimal text | | `Group` | Plex-record group path | | `App` | Plex-record app namespace | | `Name` | Plex-record app-local name | | `TAI` | Plex-record TAI text | | `Signed-By` | Seal-record verifier text | | `Signature` | Seal-record signature text | | any Plex-record extra header name | one extra header occurrence | `Index` is a decimal occurrence index for `Name` within record `P`, starting at `0`, with no leading zero except `0`. Singleton fields always use index `0`. Repeated extra headers with the same name use increasing indexes in canonical record order. A `Field` fact is set membership; duplicate same-name/same-value extra header occurrences remain distinguishable by `Index`. `Group`, `App`, `Name`, `TAI`, Plex-record extra header fields, `RecordLink`, and `BlobHash` exist for valid Plex records and for valid Seal records by reference to the embedded Plex record. `Signed-By`, `Signature`, and `PlexHash` exist only for valid Seal records. `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(P,'Group',...)` carries the Group path text; coordinate text is syntax over `Group`, `App`, and `Name` fields. ### Embedded record `Have` Plex records and Seal records embed inner record bytes. The outer record's facts include selected facts by reference to those embedded records as described above. Storing or validating an outer record does not by itself require the store to expose `Have(H)` for the embedded Blob-record or Plex-record hash `H`. `Have(H)` means the store admits `H` as a locally stored record in its own right. Implementations MAY admit embedded records separately, and thin-record reconstruction may require that inner records are already known, but independent sending or requesting of an inner record requires `Have(inner)` in the relevant local fact view. ## 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 query view**: the subset of local record facts the local side exposes to rules contributed by a particular peer or origin. Record facts are never ambient for peer-origin modules. A record-fact lookup is resolved in the context of: ```text fact owner, rule origin/viewer, evaluation snapshot ``` The fact owner controls which records are queryable by the rule origin/viewer. ## Origins and viewers An origin identifies where a policy module or selector operand came from for the current exchange plan. Origins are assigned by exchange setup or by a binding. A module MUST NOT be allowed to grant itself a different origin by declaring text inside the lacegram. A viewer is the principal or side for which a query view is computed. A viewer MAY be a proven verifier, an exchange-local source label, a side label, or a binding-defined principal. Unauthenticated or peer-chosen labels SHOULD default to the least or empty query view unless local policy explicitly grants them a view. The standard mental model for two peers Alice and Bob is: ```text Bob-authored rules on Bob: Bob's full local record facts Alice-authored rules on Bob: Bob's Alice-queryable record facts Alice-authored rules on Alice: Alice's full local record facts Bob-authored rules on Alice: Alice's Bob-queryable record facts ``` ## Query exposure The standard internal record-level query gate is: | Predicate | Arity | Meaning | |---|---:|---| | `CanQueryRecord(Viewer, P)` | 2 | record `P` is queryable by `Viewer` in this local context | `CanQueryRecord` is a reserved profile predicate. Peer-origin modules MUST NOT be able to define or override another side's `CanQueryRecord` facts. Local policy exposes queryable records through local-only query/expose facets. Conceptually, a local policy may derive: ```text AllowQueryRecord(Viewer,P) :- Have(P), Field(P,'Group',_,'X'). ``` The exact authoring surface for query/expose facets is defined by the exchange policy profile in 040. The required semantic property is: ```text peer-origin rules may inspect only records allowed by the local query view for that peer/viewer. ``` ## Query-view composition When multiple active local query constraints apply to a viewer, default composition is intersection. A record is queryable only when every active local query constraint allows it. Conceptual lowering for constraints `1..N` is: ```text CanQueryRecord(Viewer,P) :- AllowQueryRecord_1(Viewer,P), AllowQueryRecord_2(Viewer,P), ..., AllowQueryRecord_N(Viewer,P). ``` If there are no active local query constraints for a viewer, the default query 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 query constraint SHOULD narrow or preserve the query view by default. ## Origin-aware record-fact resolution When a local-origin module is evaluated on its own machine, record fact predicates resolve against the full local view unless local policy selects a narrower view. When a peer-origin module is evaluated on a local machine, record fact predicates resolve through `CanQueryRecord(Viewer,P)`: ```text Have(P) => Have(P) and CanQueryRecord(Viewer,P) Field(P,N,I,V) => Field(P,N,I,V) and CanQueryRecord(Viewer,P) RecordLink(P,N,I,D,T) => RecordLink(P,N,I,D,T) and CanQueryRecord(Viewer,P) BlobHash(P,H) => BlobHash(P,H) and CanQueryRecord(Viewer,P) PlexHash(P,H) => PlexHash(P,H) and CanQueryRecord(Viewer,P) ``` This transformation may be implemented by rewriting rules, by a faceted fact resolver, or by an internal representation with owner/viewer arguments. The observable semantics MUST be the same. The transformation applies to the entire peer-origin module, including helper predicates. A peer-origin helper predicate MUST NOT be able to read raw local record facts and then expose the result to exported selection predicates. Negation and cardinality use the same resolved fact 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 Alice-queryable view, not Bob's raw store: ```text Field(Q,'Group',_,'Y') not Field(Q,'Group',_,'Y') Cardinality(Field(Q,'Group',_,'Y'),'>=','10') ``` ## Queryable means queryable A query view is a declassification boundary. Anything included in a peer's query view should be treated as queryable by that peer's contributed rules. 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`, `RecordLink`, `BlobHash`, or `PlexHash` fact is exposed for record `P`, then the record identifier `P` is also disclosed by that fact. Profiles SHOULD expose `CanQueryRecord` consistently with non-`Have` record facts, but each exposed fact independently discloses any record identifiers it contains. ## Disclosure bounds The intended bounded disclosure property for peer-origin rules is: ```text Holding local-authored policy fixed, peer-origin rules can influence a side's observable exchange behavior only through that side's query 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.