Lace / docs

Lace-030 · Datalog and Lacegrams

Tags: datalog, engine, lacegram

Purpose

Lace needs one portable rule language for record-set selection, support closure, authority evidence, exposure, and exchange policy. This spec defines that Datalog profile: syntax, safety, stratification, evaluation, built-ins, canonical lacegrams, and resource limits.

020 defines record facts and origin-aware record-fact views. 040 and 050 define exchange policy, peer advertisement facts, and generated exchange predicates. This document defines the rule language over fact sources supplied by those profiles.

This document is for Datalog engine implementors and profile authors. It should enable them to parse, validate, canonicalize, and evaluate Lace rule programs over explicit finite fact sources with portable semantics.

Defines

Values, terms, fact classes, rule syntax, safety, shadowing, stratification, evaluation, ordered and other built-ins, canonical lacegrams, lacegram resource identifiers, limits, and incremental evaluation.

Values

All fact values are UTF-8 NFC text strings. The independent generic Datalog and profile-input value bound is 1024 bytes and is not configurable. It is not the 010 stored-record field-line bound. An implementation MUST reject a non-NFC or oversized fact at its input boundary.

Hash texts, By values, resource paths, and decimal numbers are represented as text values in facts.

Unsigned decimal integer text is either 0 or [1-9][0-9]*. Signs, leading zeroes, empty strings, and whitespace are invalid. Profiles define maximum accepted values for each use.

Fact classes

The engine evaluates two fact classes:

  1. Base facts: supplied by a profile for this evaluation snapshot. They include record facts from 020, peer advertisement facts from 050, immutable session-authority facts, facts from peer exposure views defined by 020/040, and profile-defined local facts.
  2. Derived facts: produced by rules.

Runtime facts are base facts supplied by a runtime, binding, profile, or exchange driver for the current snapshot. The standard exchange runtime facts come from immutable session authority frozen by the direct composition or connected proof establishment.

A Datalog implementation MUST NOT read hidden wall-clock time, fetch record bytes from peers, or consult mutable external state except through explicit base facts supplied to the current evaluation snapshot.

Derived predicates are ordinary rule heads. A profile may designate some derived predicates as outputs read by a runtime, but core Datalog gives no predicate name special exchange behavior. Deriving an output has no side effect during solving.

Fact sources and views

Datalog evaluation is parameterized by fact sources. A fact source may expose all facts, queries, and counts for a predicate. Profiles define module access to fact sources.

For record facts, 020 defines origin-aware record-fact resolution. A peer-origin module evaluated on a local machine sees local record facts only through the peer exposure view for that peer. This applies equally to positive atoms, negated atoms, and cardinality atoms.

When supplied by the exchange profile, advertisement and session-authority facts are ordinary base facts. Advertisement facts are discovery claims, not record facts. The standard exchange profile supplies immutable Here/1, PeerConfidential/1, and Transport/1 when present. A direct composition fixes explicit final authority; connected establishment derives it from the local By-secret value, peer proof, and transport address before policy evaluation. Datalog has no setup-time or moving-time fact.

Rule syntax

A lacegram is UTF-8 NFC text. Each non-empty line is one rule:

Head(Term, ...) :- BodyAtom, BodyAtom.

Zero-arity predicates are written with empty parentheses, for example:

trusted_route()

A fact-like rule with no body uses lowercase true:

trusted_key('V.EXAMPLE_BY_B64A.H3') :- true.

Quick reading guide:

Source shape Meaning
helper(Record, text) :- body(Record, text). derive helper for every binding where the body is true
trusted_key('V.EXAMPLE_BY_B64A.H3') :- true. derive one fact-like output
a(x) :- b(x), c(x). conjunction: both body atoms must hold
a(x) :- b(x). plus a(x) :- c(x). union: either rule may derive a(x)
not b(x) lowercase closed-world negation over the current stratum and fact view
_ anonymous wildcard; it matches but does not bind
TextShape(name,'links/','','') anchored text-shape test, here a prefix match

A common selector rule for local records under a Group/App/Name prefix is:

selected(Record) :- Have(Record), Field(Record,'Group',_,'u'), Field(Record,'App',_,'ding'), Field(Record,'Name',_,name), TextShape(name,'links/','','').

On the local machine, this local-origin rule resolves Have and Field against the full local record view. As a peer-origin rule on another machine, it resolves them against that machine’s peer exposure view for the rule origin.

Predicate names use casing to separate application helpers from declared Lace, profile, runtime, builtin, and exported-facet predicates:

app/helper predicate       [a-z][a-z0-9_]*
Lace/profile predicate     [A-Z][A-Za-z0-9_]*

Every lowercase predicate referenced in a canonical lacegram body MUST be defined in that lacegram. Authoring tools MAY accept imports or package-provided helpers only in pre-canonical source; before canonicalization they MUST resolve and lower every reachable dependency to ordinary rules in the finalized lacegram. Undefined lowercase helper references are errors, not silent empty relations. An app helper MUST NOT use a capitalized predicate name. A capitalized predicate is valid only when the active profile declares that name and arity; unknown capitalized predicates are profile errors. Standard shared Lace profiles MUST NOT assign special system meaning to bare lowercase predicates.

Predicate names beginning with _, matching _[A-Za-z][A-Za-z0-9_~-]*, are reserved for local-only or profile-defined predicates such as diagnostics. They are not part of the standard shared exchange surface unless a profile explicitly permits them.

Record-reference variables match:

[A-Z][A-Za-z0-9_]*

Text variables match:

[a-z][a-z0-9_]*

There are only two source variable kinds: record-reference and text. A record-reference variable binds typed record hash text such as B.*, P.*, or S.*, not a store-local StoreRecordId. By values, field values, names, and times are text values constrained by predicate position. Use lowercase text variables for By values: by_value is text such as V.<payload>.H3; an uppercase variable such as Key is record-reference-shaped and invalid for statically known By values.

_ is the anonymous term. It matches any value and never binds. Each _ occurrence is independent; repeated _ terms do not require equal values. Underscore-prefixed names such as _name are not variables and are invalid in term position.

true and not are reserved lowercase logic syntax. Quoted constants such as 'true' and 'not' are ordinary text constants.

Constants are single-quoted UTF-8 NFC strings. Inside a constant, \\ encodes a backslash and \' encodes a single quote. Constants MUST NOT contain LF or CR. Constants used in typed positions are checked by that position; for example, Have('P.EXAMPLE.H3') is valid only when the literal is valid record-reference text for an accepted record format.

Record-reference positions include Have/1, the first argument of Field/4 and AdvertisedField/4, both RecordLink record arguments, both arguments of ContainsRecord/2, the term in AdmitOrder(record-term), SelectStoredRecord/1, SelectAdvertisedCandidate/1, and ExposeRecord/1. Runtime key and transport predicates such as PeerConfidential/1, Here/1, and Transport/1 are text-only positions.

Field and AdvertisedField are generic-value predicates. Their value position accepts a lowercase text variable, an uppercase record-reference variable, a constant, or _. A lowercase variable may bind any text, including text that happens to look like a record reference. An uppercase variable adds a record-reference shape constraint but does not imply Have.

When the field-name position is a static constant for a standard 020 field whose value kind is known text, validators MUST reject an uppercase record-reference variable in the value position. This applies to Type, Data-Length, Group, App, Name, TAI, By, and Mark. If the field name is dynamic, an uppercase value variable remains a record-reference shape constraint rather than a static field-kind error.

+Link and *+Link field values are link text, not target hashes; use RecordLink(Record,name,index,data,Target) for parsed link targets.

Helper predicate argument kinds are inferred from all source uses and checked for consistency across rules and call sites. An uppercase variable in a helper argument position makes that argument record-reference-shaped; a lowercase variable makes it ordinary text. Forward references, recursion, and mutually recursive helpers are allowed, but each helper’s final inferred argument-kind shape must be coherent.

Valid body atoms are:

Form Meaning
Predicate(Term, ...) or Predicate() positive atom
not Predicate(Term, ...) stratified negation
x != y inequality
Compare(Int(a),op,Int(b)) decimal integer comparison
Compare(Lex(a),op,Lex(b)) bytewise lexicographic comparison
Compare(AdmitOrder(A),op,AdmitOrder(B)) local store-admission-order comparison
TextShape(text, start, delims, end) anchored text-shape test
Cardinality(Predicate(term, ...), op, n) stratified threshold test
TopK(Predicate(term, ...),PartitionBy(variable, ...),Ordering,direction,k) bind the least or greatest candidate facts independently per explicit partition
true lowercase logic syntax; always true as a standalone body literal

Rule bodies are conjunctions. Multiple rules with the same head predicate are union. A predicate with no base facts and no rules has an empty extension.

Safety

Rules are range-restricted:

_ MAY appear inside positive, negated, cardinality, and TopK candidate atoms as an anonymous, non-binding wildcard.

true, inequality, Compare, TextShape, and Cardinality are non-binding builtins. TopK binds the variables in its candidate atom; its PartitionBy expression introduces no additional binding. true is valid only as a standalone body literal; it is not a candidate, counted atom, term, or helper predicate name. Other builtins MUST NOT create variable bindings.

Reserved and shadowed predicates

A derived predicate MUST NOT have the same name and arity as any base predicate defined by the profile evaluating the lacegram.

Profiles define their base facts, exported facets, and other permitted source predicates. A lacegram MUST NOT define profile base facts or non-authoring predicates. Private helpers remain private to their source module; source text is not rejected merely because a helper name resembles an implementation’s private name.

Predicate names beginning with _ are reserved for local-only or profile-defined predicates. Standard shared interlace modules MUST NOT expose leading-underscore predicates through operand merge, exchange-plan identity, advertisements, request lists, or peer-visible fact blocks unless the active profile explicitly defines that behavior.

The standard record fact predicates from 020 are reserved base predicates:

Have/1
Field/4
RecordLink/5
ContainsRecord/2

Compare/3 is a reserved builtin. Lex, Int, and AdmitOrder are ordering expression names, and PartitionBy is a partition expression name; none are predicates.

The standard exchange profile exports SelectStoredRecord/1, SelectAdvertisedCandidate/1, ExposeRecord/1, TxDisabled/0, and RxDisabled/0. They may appear only in rule heads at those arities; source rule bodies MUST NOT reference them. All other non-base source predicates are private helpers. Generated send, request, exposure, and merged relations are not source predicates. Their exchange semantics are defined by 040.

Standard peer advertisement base predicates are Advertised/1 and AdvertisedField/4. Sourceful advertisement arities such as Advertised/2, AdvertisedField/5, and SelectAdvertisedCandidate/2 are invalid in the standard exchange profile.

These advertisement predicates are available only to the SelectAdvertisedCandidate/1 rule graph. Profile validation MUST reject a direct or transitive advertisement dependency reachable from SelectStoredRecord/1, ExposeRecord/1, TxDisabled/0, or RxDisabled/0. A helper with an advertisement dependency therefore cannot be shared between request selection and one of those facets. This reachability check includes negation, cardinality, and TopK candidates. 040 defines the current complete listing supplied to valid request-only rule graphs.

Leading-underscore diagnostic outputs are local diagnostic profile predicates. Standard shared interlace modules MUST NOT define or expose them.

Stratification

A rule for Q that contains positive P gives Q a positive dependency on P; not P gives a negative dependency; Cardinality(p(...), op, n) gives a cardinality dependency. TopK(p(...),PartitionBy(...),ordering,direction,k) gives an aggregate dependency.

A valid lacegram MUST be stratified: no predicate may transitively depend on itself through a negative edge or cardinality or aggregate edge. Predicates read by Cardinality and TopK are evaluated in a lower stratum than the containing rule.

Negation is closed-world over the current evaluation snapshot and fact view only. Lacegrams that need a bounded universe SHOULD define it explicitly, for example with Have(Record) or with profile-defined runtime facts.

Evaluation

Evaluation derives facts from explicit inputs: base facts, runtime facts, and rules. No hidden clock, peer fetch, or mutable outside state is part of a result.

The engine evaluates bottom-up to a least fixed point:

  1. Load the base fact sources for the current evaluation snapshot and module view.
  2. Load runtime facts supplied for the current evaluation snapshot.
  3. Validate safety, reserved-predicate rules, shadowing, and stratification.
  4. Assign strata so negative and cardinality dependencies point to lower strata.
  5. Evaluate strata from low to high until each stratum reaches a fixed point.

Implementations MAY use any strategy that produces the same facts as full bottom-up evaluation over the same resolved fact sources.

Rule evaluation is side-effect free over the current snapshot. Implementations MUST NOT fetch record bytes from peers, create record facts from unvalidated claims, or read hidden clocks or mutable external state during fact lookup. Each evaluation MUST use one coherent finite snapshot of base facts, runtime facts, resolved facts from peer exposure views, and peer advertisement facts. Lazy local indexes and iterators are allowed only when they expose the same facts that the current snapshot already contains.

Within a stratum, facts are added monotonically and the active domain is finite, so evaluation terminates unless a resource limit is exceeded.

Built-ins

Compare(ordering-expression, op, ordering-expression)

Ordering expressions have exactly these forms:

Lex(term)
Int(term)
AdmitOrder(record-term)

Ordering expressions are accepted only by Compare and TopK and never become fact values. Both Compare operands MUST use the same form. op is '<', '<=', '>', or '>='.

Lex compares substituted text bytewise over UTF-8. TAI text and equal-length B64A payloads are designed so this order matches their intended numeric byte order.

Int requires canonical unsigned decimal integer text and compares it numerically. Invalid integer text is an evaluation error.

AdmitOrder(Record) reads first-admission order from the resolved local fact view. It has a value only when Have(Record) is visible in that view. It does not expose a store id or claim chronology across stores. Peer-origin evaluation applies exposure gating to every referenced record.

TextShape(Text, Start, Delims, End)

TextShape is a boolean test. It does not bind variables. Delims MUST be a quoted constant in the current profile. Text, Start, and End are ordinary terms whose variables must already be safe-bound by positive non-builtin atoms.

All comparisons are exact UTF-8 text comparisons. Delims is interpreted as a set of Unicode scalar values; duplicate delimiter characters have no extra effect.

When Delims is the empty string, TextShape(Text,Start,'',End) is true iff there exists a middle string such that:

Text = Start + middle + End

middle may be empty, but Start and End do not overlap. Equivalently, after matching Start, the remaining suffix must be at least as long as End and end with End.

Common TextShape forms:

Use Form Matches example Rejects example
prefix TextShape(k,'links/','','') links/a notes/a
suffix TextShape(k,'','','.json') a.json a.txt
prefix and suffix TextShape(k,'links/','','.md') links/a.md links/a.txt
one skipped segment TextShape(k,'links/','./','msg') links/bob/msg, links/bob.msg links/msg, links/bob/alice/msg

When Delims is non-empty, TextShape(Text,Start,Delims,End) is true iff:

  1. Text starts with Start;
  2. the first Unicode scalar value after Start that is in Delims exists;
  3. the skipped text before that delimiter is non-empty;
  4. the complete suffix after that one delimiter is exactly End.

Delimiters inside Start are ignored. Delimiters inside End are ordinary text. A delimiter immediately after Start fails because the skipped segment is empty. If End is empty, the first delimiter after a non-empty skipped segment must be the final scalar value in Text.

Cardinality(predicate(term, ...), op, n)

Cardinality counts distinct facts for one predicate atom under the current outer binding and resolved fact view. Variables already bound outside the Cardinality atom are substituted. Variables that appear only inside the counted atom are existential local variables scoped to that atom. Repeated occurrences of the same local variable inside the counted atom MUST match the same value. _ remains an independent wildcard per occurrence. Op is one of '<', '<=', '>', '>='. N is an unsigned decimal integer string.

Cardinality is a threshold test. It does not bind variables outside the counted atom and is not a general aggregation mechanism. Evaluation preserves distinct-fact semantics and stops once the result is decided: >= N succeeds at witness N, > N succeeds at N+1, < N fails at N, and <= N fails at N+1. Opposite outcomes require exhaustion. The counted atom may name an app helper or a declared Lace/profile predicate that is valid in counted body position. Cardinality MUST NOT count output-only facets such as SelectStoredRecord, SelectAdvertisedCandidate, ExposeRecord, TxDisabled, or RxDisabled, compiler/internal predicates, logic syntax such as true, ILTP/control fact names, or boolean builtins such as TextShape and Compare.

For origin-aware record facts, cardinality counts the record facts visible to the module origin. A peer-origin module cannot count raw local facts outside its exposure view.

TopK(predicate(term, ...),PartitionBy(variable, ...),ordering-expression,direction,k)

TopK binds selected complete candidate facts in the containing rule after its candidate relation reaches a lower-stratum fixed point. PartitionBy() creates one global partition. A non-empty PartitionBy(...) applies the bound independently to each distinct partition tuple:

TopK(candidate(Record),PartitionBy(),AdmitOrder(Record),'>','200')
TopK(candidate(Record,name,tai),PartitionBy(name),Lex(tai),'>','1')
TopK(candidate(Record,group,app,name,tai),PartitionBy(group,app,name),Lex(tai),'>','1')
TopK(score(Item,room,points),PartitionBy(room),Int(points),'<','10')

PartitionBy is an expression accepted only as the second argument of TopK. It is not a fact, predicate, helper, ordering expression, or standalone body atom. Every PartitionBy entry MUST be a distinct variable occurring in the candidate atom. _, constants, repeated variables, and variables absent from the candidate are invalid partition entries. Uppercase record-reference variables and lowercase text variables retain their candidate kinds. Written partition-variable order is canonical content and is preserved rather than sorted or inferred.

For each TopK occurrence, evaluation:

  1. evaluates the candidate predicate to its lower-stratum fixed point;
  2. applies candidate constants, repeated variables, record-reference shapes, and _ with ordinary positive-atom semantics;
  3. resolves candidate facts through the module’s coherent origin-aware fact view;
  4. substitutes the PartitionBy(...) variables and partitions eligible complete facts by exact positional equality of the resulting text tuples;
  5. orders and retains at most k complete facts independently in each partition; and
  6. unions the retained facts into one relation that binds the candidate variables in the containing rule.

Other body atoms join against that selected relation after the aggregate. They do not constrain or repartition it, so body atom order cannot change aggregate meaning. For example, this computes one winner for every candidate name and then joins those winners with allowed:

selected(Record) :- allowed(name), TopK(candidate(Record,name,tai),PartitionBy(name),Lex(tai),'>','1').

TopK ranks complete facts before projecting variable bindings. Facts that differ only in candidate _ positions can consume distinct slots and then produce the same projected binding; ordinary derived-fact set deduplication occurs afterward.

Rules:

Peer-origin evaluation applies exposure before candidate work, partition construction, and ranking. Hidden records therefore cannot create a partition, displace a retained fact, contribute candidate work, or cause a resource-limit failure through this aggregate.

The configured derived-facts-per-predicate limit also bounds the complete facts retained across all partitions of each syntactic TopK occurrence in one evaluation run. The per-partition k does not bound the aggregate’s total selected relation: at most partition count × k facts are retained, subject to that combined per-occurrence limit. Exceeding the limit fails evaluation; implementations MUST NOT truncate partitions or reduce k. Separate TopK occurrences receive separate retained-fact bounds.

Equality is not Lace Datalog

= is not a Lace Datalog body atom. Core Lace parsers, canonicalizers, authoring-source readers, and resource validators MUST reject source text that contains = as a body atom. They MUST NOT normalize equality constraints into canonical lacegram text.

!= remains a canonical boolean builtin. It is not an equality-normalization constraint.

A DSL outside the core Lace library can provide its own syntax and compile it to valid Lace Datalog, but that source syntax is not Lace Datalog and is not accepted by core Lace Datalog APIs.

Canonical lacegrams

Lacegrams exchanged or identified by hash MUST use canonical text:

Canonical lacegram bytes are the canonical rule lines joined by one LF byte with no trailing LF. An empty canonical lacegram is invalid unless a profile explicitly permits it.

The current lacegram resource identifier is the 010 Blob-record hash of a Blob whose data bytes are the canonical lacegram bytes:

B.<b64a>.H3

Context defines that the Blob data is parsed as canonical 030 lacegram text. The Blob resource may be supplied during setup without admitting that Blob to the application record store or deriving Have('B.*').

Faceted exchange plans defined by 040 derive a canonical transcript and identify it by the 010 Blob-record hash of those transcript bytes. The transcript is not a setup resource and is not transferred: both endpoints derive it from the ordered operand resources and fixed profile. A lacegram Blob hash is not interchangeable with an exchange-plan identifier unless the profile explicitly says so.

Extended policy module source

Canonical Lace-030 lacegrams do not contain linked-relation markers. A Lace runtime or tool MAY accept extended policy module source before canonicalization. Extended module source is Datalog-shaped source plus linked relation calls and heads:

@name(term, ...) :- body.

A linked relation name after @ uses helper predicate syntax [a-z][a-z0-9_]*. Linked relations are a module-linking surface, not canonical Datalog predicates or macros. A policy module linker MUST resolve and lower all reachable linked relations to ordinary predicate names before emitting a canonical 030 lacegram for public exchange operands or executable policy. Public canonical lacegram APIs and ILTP resource Blobs MUST reject raw @ source.

In the v1 module-linking profile, linked-relation arguments are text-only and a linked-relation definition body MUST be a static fact/private-helper chain. It MUST NOT read record facts, advertisement facts, runtime facts, facts from peer exposure views, non-static builtins, negation, or cardinality. Ordinary safety, variable-kind, and stratification checks run on the finalized canonical lacegram.

Resource limits

An implementation MUST enforce configurable limits. Defaults MUST be at least:

Limit Minimum supported value
base facts 2^20
runtime facts 2^20
derived facts per predicate 2^18
rule count 256
stratum iterations 1000
tuple arity 8

The engine MUST stop with an error rather than exceed a limit. The fixed 1024-byte standard value bound is defined under Values; it is not a resource option.

Incremental evaluation

Implementations MAY evaluate incrementally when base facts, runtime facts, or rules change. Incremental evaluation MUST produce the same result as full evaluation of the new snapshot and resolved fact views.

If facts are removed, implementations MUST use a deletion strategy that handles stratified negation correctly, such as counting derivations or full re-evaluation of affected strata.

Examples

Follow linked support records visible in the current view

support(Target) :- Have(Record), RecordLink(Record,'+Link',_,'evidence',Target).

Refine contained-record kind

Typed hash text identifies contained-record kind. TextShape refines the bound record when a rule needs a particular kind; containment has no role or kind argument.

contained_blob(Blob) :- ContainsRecord(Outer,Blob), TextShape(Blob,'B.','','').
contained_plex(Plex) :- ContainsRecord(Outer,Plex), TextShape(Plex,'P.','','').

Correlate Seals over the same contained Plex record

seal_subject(Seal,Plex,by_value) :- Have(Seal), ContainsRecord(Seal,Plex), TextShape(Plex,'P.','',''), Field(Seal,'By',_,by_value).
attester(Plex,by_value) :- seal_subject(Seal,Plex,by_value).

Latest 100 records in the current view

candidate(Record,tai) :- Have(Record), Field(Record,'Group',_,'u'), Field(Record,'App',_,'ding'), Field(Record,'Name',_,name), TextShape(name,'links/','',''), Field(Record,'TAI',_,tai).
selected(Record) :- TopK(candidate(Record,tai),PartitionBy(),Lex(tai),'>','100').

Match one skipped segment

selected(Record) :- Have(Record), Field(Record,'Name',_,name), TextShape(name,'links/','./','msg').

This matches links/bob/msg and links/bob.msg, but rejects links/msg, links/bob/alice/msg, and links/.msg.

Deny blocked By values

blocked(by_value) :- Have(Record), Field(Record,'Group',_,'keys'), Field(Record,'App',_,'blocked'), Field(Record,'Name',_,by_value).
selected(Record) :- Have(Record), Field(Record,'By',_,by_value), not blocked(by_value).

Rejection examples