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 outside this domain. Profiles define maximum accepted values for each use. Complete-module validation MUST reject a constant term used by Int when that constant is outside the domain. A dynamic fact value outside the domain remains valid text and follows the non-matching Compare and ineligible-candidate TopK semantics below.

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 the base-fact subset 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 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 and PeerConfidential/1 when present. A direct composition fixes explicit final authority. Before policy evaluation, connected establishment derives Here from the local By-secret and derives PeerConfidential only from live peer proof under either host-asserted confidential-channel or locally verified channel-bound assurance. The binding and encrypted-channel settings are not facts or plan inputs. The standard profile accepts no generic caller-supplied runtime-fact bag. 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:

A selector can combine exact generic fields with a text-shape test:

selected(Record) :- Have(Record), Field(Record,'Topic',_,'notes'), Field(Record,'Path',_,path), TextShape(path,'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. 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 and all application field values are represented as text. 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 predicates PeerConfidential/1 and Here/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 the static constant :Type, :Length, Data-Length, By, or Mark, validators MUST reject an uppercase record-reference variable in the value position because 020 defines those synthetic or structural values as text. Every application field name is generic: a static application field name imposes no value kind, so an uppercase value variable is accepted as an explicit record-reference shape constraint. If the field name is dynamic, an uppercase value variable has that same shape-constraint meaning 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:

Rule bodies are conjunctions. Multiple rules with the same head predicate are union. A predicate declared by the active profile but supplied with no base facts and defined by no rules has an empty extension.

Safety

Rules are range-restricted:

• every variable in the head MUST appear in a positive non-builtin body atom or in a TopK candidate atom;
• _ is not a variable for safety and MUST NOT appear in a rule head;
• every variable in a negated atom MUST appear in a positive non-builtin body atom;
• every variable in !=, Compare, TextShape, or TextMatch MUST appear in a positive non-builtin body atom;
• _ MUST NOT appear in !=, Compare, TextShape, or TextMatch;
• Cardinality does not bind variables. A variable that appears both inside and outside a Cardinality atom MUST satisfy safety outside the Cardinality atom. Variables that appear only inside the counted atom are local to the cardinality test.

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

true, inequality, Compare, TextShape, TextMatch, 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 top-level 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 program; 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 control items 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, TextShape, TextMatch, Cardinality, and TopK are builtin body forms with dedicated syntax, not predicates; a rule head or relation atom with one of those names is invalid. 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, including the supplied runtime-fact subset.
2. Validate safety, reserved-predicate rules, shadowing, and stratification.
3. Assign strata so negative, cardinality, and aggregate dependencies point to lower strata.
4. 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. A dynamically substituted value outside the Int domain is an ordinary false Compare or ineligible TopK candidate, not an evaluation, policy, fact-source, or resource error.

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. Equal-length B64A payloads are designed so this order matches decoded byte order. Applications may define other fixed-width texts for which bytewise order has application meaning.

Int compares canonical unsigned decimal integer text numerically without a native fixed-width-integer bound. Complete-module validation MUST reject a constant Int term outside that domain. For each evaluated binding, if either dynamically substituted Int operand is outside the domain, the Compare atom is false for that binding; other bindings continue normally.

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:

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.

TextMatch(Text, 'Pattern')

TextMatch is a non-binding boolean body test that matches the complete value. Text is a generic-kind term, as in TextShape: a quoted constant or a text or record-reference variable already safe-bound by a positive non-builtin atom. It is not a text-only kind position. The pattern MUST be a quoted constant, never a variable or _. The builtin is invalid in a rule head, relation atom, counted atom, or TopK candidate, and has no aggregate or binding form. To negate a match, derive a helper relation and use ordinary stratified negation.

Preparation MUST validate every pattern in the complete program before pruning, including unused rules, dependencies beneath zero-bound aggregates, and public parsed-program inputs. Invalid patterns are preparation errors, never runtime non-matches. Structural composition and lowering preserve the builtin and its constant; it adds no fact source or authority.

Value and source bounds

Pattern source MUST be at most 128 UTF-8 bytes after host-language and Datalog/Interlang string decoding, but before pattern escapes are interpreted. It MUST NOT contain CR or LF. Text longer than 128 UTF-8 bytes returns false immediately without inspecting its contents. These are fixed matcher bounds, not configurable limits; the ordinary 1024-byte value/constant bound remains unchanged.

The empty pattern is valid and matches only empty text. Literals are Unicode scalars; . accepts any scalar, including input CR/LF where the surrounding value contract permits them. Repetition counts scalars, not bytes or graphemes. Ordinary UTF-8 and NFC boundary validation still applies; matching adds no normalization, case folding, or locale behavior. A syntactically valid pattern whose minimum expansion exceeds 128 bytes is accepted and cannot match a permitted input.

Pattern grammar

Here * and ? denote grammar repetition and optionality, not pattern syntax:

pattern        := piece*
piece          := atom repetition? | group
atom           := literal | '.' | class
repetition     := '{' count '}' | '{' count ',' count '}'
count          := '0' | [1-9][0-9]*
class          := '[' '^'? class-items ']'
group          := '(' literal-string '|' literal-string ')'

Counts MUST be in 0..128, with min <= max, no whitespace, missing bound, or leading zero except 0. Repetition applies to one atom only and cannot be stacked. At most one repeat in the entire pattern may have unequal bounds, even when another piece makes the pattern impossible. {n,n} is exact and {0} is valid. Any number of exact repeats is allowed within the source-byte bound, with no separate piece-count or expanded-state limit.

At most one group is permitted. It contains exactly two nonempty literal strings, which may differ in byte and scalar length. The variable repeat may occur on either side. Groups cannot nest or repeat. Unescaped dot, class, and repetition syntax is invalid inside a group; escaped punctuation is literal, for example the raw pattern (a\|b|\(x\)).

There are no *, +, ?, anchors, flags, captures, bindings, backreferences, lookaround, named Unicode properties, top-level alternation, substring search, or replacement. Additional alternatives use ordinary rules.

Escapes and ASCII classes

Outside classes, .[]{}\^$|()*+? are metacharacters, valid only in the grammar positions above or when escaped. Other characters, including bare hyphen and spaces, are literals. In every context, backslash quotes only a metacharacter from that set or hyphen. Unknown escapes such as \d, \w, \s, numeric escapes, and a trailing backslash are invalid.

Classes contain one or more ASCII literals or ascending inclusive ASCII ranges. A positive class matches only ASCII. A negated class matches every Unicode scalar outside that ASCII set, including every non-ASCII scalar. Duplicate and overlapping entries have set semantics.

Leading unescaped ^ negates the class. Elsewhere ^ and [ require escaping; ] and backslash require escaping to be included. Other punctuation, including ., is literal within a class. Empty classes ([], [^]) and non-ASCII entries such as [é] are invalid.

A bare hyphen is a standalone literal only at the first or last item after optional ^, never a range endpoint. Ranges parse left to right, consuming both endpoints without reuse. [-a-z], [a-z-], [-], and [--] are valid; [--a], [a--], and [a-b-c] are invalid. Escape a hyphen to use it elsewhere literally or as a range endpoint. Descending ranges are invalid.

Quoting and identity

Datalog quoting and pattern escaping are separate. For example, TextMatch(name,'a\\.b') passes the raw pattern a\.b and matches exactly a.b; a[.]b avoids the pattern backslash. Host-language strings may add another quoting layer.

Canonicalization MUST preserve decoded pattern spelling under ordinary canonical string escaping, not normalize pattern equivalence. For example, [ab] and [a-b] may retain different operand hashes. Local compiled set or literal normalization does not change canonical bytes. Deterministic work is defined by 050.

TextShape retains its distinct dynamic prefix/suffix and first-delimiter semantics; neither builtin is a rewrite of the other.

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, TextMatch, 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,topic,revision),PartitionBy(topic),Lex(revision),'>','1')
TopK(candidate(Record,kind,topic,revision),PartitionBy(kind,topic),Lex(revision),'>','1')
TopK(score(Item,bucket,points),PartitionBy(bucket),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. obtains the substituted primary ordering value and, for Int, excludes the complete candidate when that value is outside the canonical integer domain;
5. substitutes the PartitionBy(...) variables and partitions the remaining eligible complete facts by exact positional equality of the resulting text tuples;
6. orders and retains at most k complete facts independently in each partition; and
7. 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 topic and then joins those winners with allowed:

selected(Record) :- allowed(topic), TopK(candidate(Record,topic,revision),PartitionBy(topic),Lex(revision),'>','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:

• the candidate is an app helper or declared base/profile predicate valid in positive body position; output facets, compiler/control predicates, builtins, and aggregates are invalid candidates;
• candidate variables are bindings produced by TopK; constants, repeated variables, and _ retain ordinary atom semantics;
• PartitionBy() uses the empty tuple and therefore one global partition;
• partition equality is exact and positional over fact text; record references partition by record hash text, never by StoreRecordId;
• the ordering term MUST occur in the candidate atom and MUST NOT be _;
• direction MUST be the quoted constant '>' for greatest facts or '<' for least facts; '>=' and '<=' are invalid;
• k MUST be a quoted canonical unsigned decimal constant and preparation rejects a bound above the configured derived-fact limit;
• within each partition, facts first compare by the primary ordering expression, then by every complete candidate component in argument order using bytewise UTF-8 value order; direction applies to this complete order, and record references compare by hash text;
• candidate argument order is therefore semantic: in TopK(candidate(Record,topic,revision),PartitionBy(topic),Lex(revision),'>','1'), equal revision values are next decided by greatest Record hash text;
• Lex uses ordinary bytewise UTF-8 lexicographic order, including prefix ordering;
• Int accepts canonical unsigned decimal text and compares it numerically without a native fixed-width-integer bound; complete-module validation rejects an Int ordering constant outside that domain, including when k = 0;
• for k > 0, a dynamically substituted Int value outside the domain excludes that complete candidate before partition construction; it creates no partition, occupies no retained slot, cannot displace a valid candidate, and does not count toward the retained-fact bound;
• visiting an out-of-domain dynamic Int candidate incurs the ordinary candidate-visit and projected-fact-byte work charged to a valid candidate, with no separate integer-test work unit;
• a missing AdmitOrder excludes that candidate before partition construction instead of failing evaluation;
• k = 0 selects no facts without visiting candidate facts or validating dynamic ordering values, although errors while deriving the lower-stratum candidate relation still fail evaluation and static Int constants were already validated during preparation;
• cycles through TopK are unstratified; and
• TopK selects a set and defines no result order.

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-fact limit also bounds the complete facts retained across all partitions of each syntactic TopK occurrence. 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.

Body equality uses joins rather than =

Lace Datalog expresses equality by reusing a variable across terms. = is not a body atom. Core Lace parsers, canonicalizers, authoring-source readers, and resource validators MUST reject source text that contains = as a body atom and MUST NOT emit it through canonicalization. != remains the canonical inequality builtin.

Canonical lacegrams

Lacegrams exchanged or identified by hash MUST use canonical text:

• UTF-8 NFC;
• LF line endings only;
• one rule per line;
• no blank lines;
• no comments;
• exactly one space before and after :-;
• exactly one space after each comma that separates body atoms;
• no spaces inside atom argument lists;
• constants use the shortest valid escaping;
• rules are sorted by head predicate name, then full rule bytes;
• duplicate rules are removed.

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.

Source compilation

Lace-120 defines self-contained Interlang; Lace-130 defines its compilation and structural composition of complete policy constraints. Both produce ordinary canonical Datalog before evaluation.

Canonical APIs and ILTP operand Blobs MUST reject authoring syntax, module declarations, qualified helper calls, and raw @ providers. Relations are not evaluator values. The complete finalized program MUST satisfy this specification and its execution profile. Canonical validation and execution do not depend on an authoring compiler. Generic finite Datalog preparation and evaluation remain independent of Interlang’s exchange-policy compilation target.

Resource limits

A generic Datalog implementation MUST enforce configurable preparation and finite-input evaluation limits. Defaults MUST be at least:

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.

One prepared generic program retains its limits through evaluation and every resumption. Preparation checks distinct rules, predicate arity, static TopK bounds, and TextMatch patterns across the complete program, including unused rules. Identical rules count once. A transformed program MUST satisfy the same checks before execution.

Generic finite-input evaluation counts the complete supplied fact sets before executing rules, including unused inputs. Base facts include record facts, advertisements, and runtime facts; runtime facts additionally count toward their own bound. Record facts count their complete 020 projection, not just records or referenced predicates. Counting does not require materializing fact tuples. The derived-fact limit applies to each relation an evaluation builds, counting its distinct complete facts when its stratum reaches a fixed point. A predicate that a transformed program replaces by an identical relation, such as a copy of another predicate, builds no relation of its own. Each TopK occurrence has the separate combined retained-fact bound defined above. The iteration limit applies each time evaluation brings a stratum to a fixed point, including each update of an incremental evaluation.

The standard exchange profile in 040/050 uses lazy, origin-aware record-fact access rather than a generic finite-input snapshot. For that profile, 050’s logical-work budget replaces total base-fact cardinality accounting; control-byte budgets bound advertisement input, and session authority has its fixed fact shape. Implementations MUST NOT scan or count an entire store to apply generic input limits to exchange. Hidden record facts remain excluded from peer-origin work and limit failures under 020. Exchange preparation, derived-fact, TopK, and iteration bounds remain enforced as defined by 040/050.

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

Lexicographically greatest 100 versions in the current view

candidate(Record,version) :- Have(Record), Field(Record,'Topic',_,'notes'), Field(Record,'Path',_,path), TextShape(path,'links/','',''), Field(Record,'Version',_,version).
selected(Record) :- TopK(candidate(Record,version),PartitionBy(),Lex(version),'>','100').

Dynamic integer values outside the domain do not match

Here banana makes the Compare atom false for that binding. In the aggregate, banana is excluded before partition construction, so b is the valid winner.

candidate('a','banana') :- true.
candidate('b','10') :- true.
newer(item) :- candidate(item,version), Compare(Int(version),'>',Int('5')).
selected(item) :- TopK(candidate(item,version),PartitionBy(),Int(version),'>','1').

Compare application Unix timestamps

An application can represent a nonnegative Unix timestamp as canonical unsigned seconds since 1970-01-01T00:00:00Z and compare it with Int. For example, this selects records whose declared timestamp is at least 2026-01-01T00:00:00Z:

recent(Record) :- Have(Record), Field(Record,'Timestamp','0',timestamp), Compare(Int(timestamp),'>=',Int('1767225600')).

The application defines the field convention and its evidence requirements. A separate time-zone field can guide display without changing the timestamp or its comparison. These are ordinary record values, not a Datalog clock, trusted-time proof, or additional runtime fact. Negative pre-epoch timestamps are outside the unsigned Int domain.

Select by complete record length

The synthetic :Length field is the record’s complete canonical byte length, so it counts field lines as well as data:

small(Record) :- Have(Record), Field(Record,':Length','0',length), Compare(Int(length),'<=',Int('4096')).

Count application fields only

A wildcard Field atom also matches the 020 synthetic and structural fields. This counts records with more than eight application field occurrences:

projected(name) :- Have(Record), Field(Record,name,_,_), TextShape(name,':','','').
projected('Data-Length') :- true.
projected('By') :- true.
projected('Mark') :- true.
application_field(Record,name,index) :- Have(Record), Field(Record,name,index,_), not projected(name).
crowded(Record) :- Have(Record), Cardinality(application_field(Record,_,_),'>','8').

Match one skipped segment

selected(Record) :- Have(Record), Field(Record,'Path',_,path), TextShape(path,'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,'Purpose',_,'blocked-key'), Field(Record,'Key',_,by_value).
selected(Record) :- Have(Record), Field(Record,'By',_,by_value), not blocked(by_value).

Rejection examples

• selected(Record,value) :- Field(Record,'Topic',_,'notes'). has unbound value in the head.
• selected(_) :- Have(Record). uses anonymous _ in a rule head.
• selected(Record) :- Have(Record), TextShape(_,'links/','',''). uses anonymous _ in a builtin.
• selected(Record) :- Have(Record), Field(Record,'Topic',_name,'notes'). uses invalid _name in term position.
• selected(Record) :- Compare(AdmitOrder(Record),'>',AdmitOrder(Other)). leaves both variables unsafe.
• selected(Record) :- Have(Record), Compare(Lex(Record),'>',Int('1')). mixes ordering-expression kinds.
• selected(Record) :- Have(Record), Compare(Int('01'),'>',Int('0')). contains a static left Int constant outside the canonical unsigned decimal domain; the same rejection applies to an invalid right constant.
• candidate('x','banana') :- true. plus selected(item) :- TopK(candidate(item,'banana'),PartitionBy(),Int('banana'),'>','0'). contains an invalid static Int ordering constant; k = 0 does not defer static validation.
• Have(Record) :- true. shadows a record fact predicate.
• a(Record) :- not b(Record). plus b(Record) :- not a(Record). is unstratified.
• a(Record) :- candidate(Record), Cardinality(a(Other),'<','100'). is unstratified.
• A canonical lacegram that calls an undeclared capitalized predicate is invalid.
• A lacegram containing x = y is invalid; = is not Lace Datalog.
• TopK(candidate(Record,topic,revision),PartitionBy('fixed'),Lex(revision),'>','1') is invalid because partition entries must be variables.
• TopK(candidate(Record,topic,revision),PartitionBy(topic,topic),Lex(revision),'>','1') is invalid because partition variables must be distinct.
• TopK(candidate(Record,topic,revision),PartitionBy(other),Lex(revision),'>','1') is invalid because other does not occur in the candidate atom.
• TopK(candidate(Record,topic,revision),PartitionBy(_),Lex(revision),'>','1') is invalid because _ cannot be a partition entry.
• TopK(candidate(Record,topic,revision),By(topic),Lex(revision),'>','1') is invalid because By is not the partition expression.
• A canonical lacegram with comments, CRLF, blank lines, duplicate unsorted rules, or non-canonical escaping is not canonical.