Lace / spec

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:

B.<b64a>.H3
P.<b64a>.H3
S.<b64a>.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.

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:

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:

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:

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:

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:

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:

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:

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):

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:

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:

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.