Algorithms & formal foundations
Maelys DL is an embedded Datalog micro-kernel for security policy decisions. Its design follows the classical database-theory view of Datalog: a policy is a finite logical program, inputs are finite relations, and evaluation computes the least fixpoint of all rules.
Maelys DL also reuses ideas that appear in modern Datalog systems such as Soufflé: semi-naive evaluation, stratified negation, join planning, and provenance-oriented explanations. The difference is the target. Soufflé optimizes Datalog for large static-analysis workloads. Maelys DL optimizes Datalog for bounded, auditable, fail-closed decisions inside a constrained C runtime.
Datalog as a least-fixpoint model
A Datalog program is a finite collection of Horn rules. Evaluation starts from base facts and repeatedly applies rules until no new derived fact can be produced. The result is the least fixpoint: the smallest set of facts that satisfies the program. Maelys DL uses this classical bottom-up semantics because it is deterministic, explainable, auditable, and naturally fail-closed.
- ▸EDB facts are runtime input facts supplied by the caller
- ▸POLICY_FACT facts are trusted facts embedded in the policy
- ▸IDB facts are derived by rule evaluation
- ▸Positive rules are monotone and can only add facts
- ▸Negation is handled through stratification, not as negative facts
- ▸The result is the least fixpoint implied by the program
- ▸No new derived fact after an iteration means the fixpoint is reached
facts = EDB ∪ POLICY_FACTS
repeat:
new_facts = {}
for each rule H :- B1, ..., Bn:
for each substitution θ satisfying B1θ, ..., Bnθ:
new_facts += Hθ
delta = new_facts - facts
facts = facts ∪ delta
until delta = ∅
return factsSemi-naive evaluation
Naive bottom-up evaluation repeats too much work because every iteration reuses facts that were already known. Semi-naive evaluation uses the observation that a genuinely new derivation must depend on at least one fact derived in the previous round. Maelys DL therefore separates current facts, delta facts, and merge facts.
- ▸idb_current contains facts already stabilized before the current round
- ▸idb_delta contains facts derived in the previous round
- ▸idb_merge collects facts newly derived in the current round
- ▸Each variant chooses one delta-eligible IDB body literal
- ▸EDB and POLICY_FACT literals never scan delta
- ▸Fixpoint is reached when idb_delta becomes empty
idb_current = {}
idb_delta = base_derivation(rules, EDB ∪ POLICY_FACTS)
while idb_delta ≠ ∅:
idb_merge = {}
for each rule r:
for each delta-eligible IDB literal i:
derive r with:
body[i] read from idb_delta
other IDBs read from idb_current ∪ idb_delta
base atoms read from EDB ∪ POLICY_FACTS
append only genuinely new facts to idb_merge
idb_current = idb_current ∪ idb_delta
idb_delta = idb_mergeStatic join-order planning
Rule evaluation is a sequence of joins. A bad join order can explode intermediate combinations. Soufflé uses advanced compilation, indexing, and join optimization for large workloads. Maelys DL makes a different embedded-systems trade-off: it computes a deterministic static order using bounded stack state and variable-binding masks.
- ▸The delta literal is forced to join_order[0] for semi-naive variants
- ▸Positive relational atoms bind variables
- ▸Comparisons and negated atoms are constraints, not binders
- ▸A literal is safe only when all required variables are already bound
- ▸Orphan variables fail closed at plan time
- ▸Tie-breaking uses original body index for deterministic output
planned = {}
bound_vars = {}
order = []
if semi_naive_variant:
delta = selected_delta_literal
require delta is a positive IDB atom
order.push(delta)
bound_vars += vars(delta)
while order.size < body.size:
candidates = safe_unplanned_literals(body, bound_vars)
if candidates = ∅:
FAIL CLOSED
best = max_score(candidates)
order.push(best)
if best is positive relational atom:
bound_vars += vars(best)
return orderStratified negation
Negation in Datalog is not monotone: adding a fact may invalidate a previously true not(p). Stratified negation restores a well-defined semantics by requiring all negated dependencies to point strictly downward. Maelys DL assigns predicates to strata and rejects recursion through negation.
- ▸Positive dependency: stratum(head) ≥ stratum(body)
- ▸Negative dependency: stratum(head) > stratum(body)
- ▸EDB and POLICY_FACT predicates are treated as stratum 0 inputs
- ▸Recursion through negation is rejected
- ▸Negative cycles are rejected before evaluation
- ▸A non-stratifiable policy fails closed
for each predicate p:
stratum[p] = 0
repeat up to MAX_PREDICATES:
changed = false
for each rule r:
required = stratum[r.head]
for each body literal L:
s = stratum[L.predicate]
if L is negative:
s = s + 1
required = max(required, s)
if required > stratum[r.head]:
stratum[r.head] = required
changed = true
if !changed:
return strata
FAIL CLOSEDFrozen stratum windows
A negative literal must be evaluated against a complete and stable relation. Maelys DL freezes each lower stratum before evaluating higher strata. Derived IDB facts live in one bounded flat pool; stratum boundaries record which slice belongs to each completed stratum.
- ▸A stratum is evaluated only after all lower strata are frozen
- ▸Negative lookup never reads an actively mutating window
- ▸Each frozen window is sorted and deduplicated
- ▸The IDB pool is partitioned by boundaries, not duplicated
- ▸not(p(t)) succeeds exactly when p(t) is absent from the frozen lower window
start[0] = 0 for s in 0..max_stratum: evaluate all rules whose head is in stratum s sort facts derived in stratum s deduplicate facts derived in stratum s end[s] = current_idb_end frozen[s] = true negative_lookup(p, tuple): s = stratum[p] require frozen[s] return !binary_search(idb_facts[start[s]..end[s]], p(tuple))
Sorted-array fact store
General-purpose Datalog engines often use indexes, hash tables, tries, or compiled relational operators. Maelys DL instead uses bounded sorted arrays. This is less general than a database engine, but predictable, compact, portable C, and suitable for policy decisions where fact counts are explicitly capped.
- ▸Facts have a canonical lexicographic order
- ▸The comparison key is predicate id, arity, then terms
- ▸Lookup uses binary search once a window is sorted
- ▸Deduplication is a linear pass after sorting
- ▸Windows are tracked by index ranges rather than heap containers
- ▸The hot decision path avoids malloc
fact_key(f) = ( f.predicate_id, f.arity, f.terms[0], f.terms[1], ... ) append_unsorted(window, fact) freeze(window): sort(window, by=fact_key) deduplicate_adjacent_equal_facts(window) contains(window, query): require window.sorted return binary_search(window, query)
Bounded proof-tree provenance
Datalog provenance explains why a fact exists. Soufflé has a scalable provenance line of work for large Datalog analyses. Maelys DL adapts the same idea to an embedded policy kernel: solve_once records bounded derivation provenance for derived IDB facts. Proof nodes carry derived facts and parent links, and callers can extract an ancestors-first derivation chain for a solved fact.
- ▸Proof nodes are recorded in lockstep with derived IDB facts
- ▸Each derived fact can carry a proof index
- ▸Parent links describe the derivation dependencies
- ▸Sorting and deduplication preserve fact/proof pairing
- ▸Proof extraction returns a bounded ancestors-first chain
- ▸Truncation is non-fatal and does not change decision semantics
- ▸PBI receipts still expose a compact summary, not the full proof tree
derive fact F by rule R using parents P:
proof_index = proof_add(
derived_fact = F,
rule_id = R.id,
parents = P
)
idb_facts.append(F)
idb_proof_index.append(proof_index)
extract_proof_for_fact(F):
root = proof_index_for(F)
chain = ancestors_first(root)
remap parent indexes locally
return chainPolicy identity and decision receipts
A policy decision is only auditable if it can be attributed to the exact policy that produced it. Maelys DL hashes policy material at load time and stores the resulting SHA-256 digest in the ruleset. Decision receipts carry the policy hash, making the decision traceable to a concrete policy version.
- ▸Manifest-loaded policies verify file bytes against the manifest hash
- ▸Embedded policies are hashed from source or structural material
- ▸Receipts copy the ruleset hash rather than inventing a value
- ▸Hash mismatch fails closed at load time
- ▸The hash identifies policy material, not merely a policy name
- ▸Receipts summarize decisions without exposing raw prompt or payload content
load_policy(path, manifest_hash):
actual = sha256(file_bytes(path))
if actual != manifest_hash:
FAIL CLOSED
ruleset.sha256 = actual
decide(request):
result = solve_once(ruleset, request.edb)
receipt.policy_sha256 = ruleset.sha256
receipt.decision = query(result, allow(request.id))
return receiptMaelys DL and Soufflé
A high-performance Datalog system for static program analysis. It emphasizes synthesis of analyzers, compilation, indexing, specialized data structures, scalable provenance, and join optimization.
A bounded embedded Datalog evaluator for security policy decisions. It emphasizes deterministic execution, fail-closed behavior, bounded C data structures, explicit fixpoint evaluation, proof-tree provenance, and auditable receipts.
Maelys DL therefore reuses the Datalog foundations and explanation ideas associated with systems such as Soufflé, but changes the engineering contract. It does not synthesize a large native analyzer. It embeds a small evaluator inside a security runtime, where bounded memory, deterministic failure, and decision attribution matter more than peak throughput on massive relations.
The Datalog core records bounded proof-tree provenance for solved IDB facts. PBI decision receipts currently expose a compact bounded decision summary; they do not yet serialize the full proof tree, even though the solver can record and expose bounded derivation chains.