Algorithms & formal foundations

For positive Datalog, evaluation starts from base facts and applies rules until no new fact is produced: the least fixpoint. With stratified negation and aggregates, the engine completes each lower layer before evaluating the next. Maelys implements fail-closed loading and solving: an error is not a successful negative answer, and an incomplete solve is not published as a result. The embedding application must authorize only after successful solving and a successful positive query.

Evidence (v0.11.1): implementation · regression tests

# Positive rules within one evaluation layer.
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 facts

Naive bottom-up evaluation repeats work on old facts. Semi-naive evaluation requires each iterative rule variant to read at least one newly derived IDB fact. The pseudocode below separates old facts and delta conceptually. In Maelys, delta is a range inside the accepted current prefix of one bounded pool; merge is the appended candidate range. These are not three independently allocated copies.

Evidence (v0.11.1): implementation · regression tests

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_merge

Rule evaluation is a sequence of joins. A bad order can multiply intermediate combinations. Maelys uses a deterministic greedy heuristic with bounded masks: it favors bound terms and constants, imposes a delta pivot for semi-naive variants, and selects only safe literals. This is a Maelys implementation choice, not a new general join-optimization algorithm or an optimality guarantee. The complexity below describes the built-in planner, not arbitrary extension callbacks or the joins themselves.

Evidence (v0.11.1): implementation · regression tests

planned = {}
bound_vars = {}
order = []

if semi_naive_variant:
  delta = selected_delta_literal
  require delta is a positive IDB atom
  order.push(delta)
  planned += delta
  bound_vars += vars(delta)

while order.size < body.size:
  candidates = safe_literals(body - planned, bound_vars)

  if candidates = ∅:
    FAIL CLOSED

  best = max_score(candidates)
  order.push(best)
  planned += best

  bound_vars += variables_bound_by(best)

return order

Negation is not monotone: adding a fact can invalidate an earlier absence test. Stratification requires a negated relation to be complete before it is read. Maelys also gives aggregate dependencies a strict downward edge: a counted or summed relation must not depend on the result of that aggregate. Positive recursion is allowed within the lower layer; cycles through negation or aggregation are rejected.

Evidence (v0.11.1): implementation · regression tests

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 or an aggregate:
        s = s + 1

      required = max(required, s)

    if required > stratum[r.head]:
      stratum[r.head] = required
      changed = true

  if !changed:
    return strata

FAIL CLOSED

A negative literal reads a complete lower relation, as required by stratification. The Maelys representation keeps derived facts in one bounded flat pool and records the boundaries of each completed stratum. Sorted slices support membership checks without duplicating the pool. These internal stratum windows are not the last-N event windows described below.

Evidence (v0.11.1): implementation · regression tests

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
  start[s + 1] = end[s]

negative_lookup(p, tuple):
  if p is EDB or POLICY_FACT:
    return !base_contains(p, tuple)
  s = stratum[p]
  require frozen[s]
  return !binary_search(idb_facts[start[s]..end[s]], p(tuple))

Maelys stores bounded fact sets in arrays, with a canonical comparator and adjacent deduplication after sorting. Its typed sort is an introsort: median-of-three partitioning, insertion sort for small segments, and a heapsort fallback when the depth budget is exhausted. Only the smaller partition recurses. The adaptation avoids allocator calls and variable-length arrays; introsort itself is an established algorithm. Why-false additionally uses a separate context-aware heapsort.

Evidence (v0.11.1): implementation · regression tests

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)

Why-true explains one retained derivation of a present IDB fact. Each step records its rule and lexical premises, including positive facts, negative absence, comparisons, filters and aggregates. IDB premises link to earlier steps, and shared parents are emitted once: the result is a bounded directed acyclic witness graph, not simply a single-parent chain. This is not an enumeration of every derivation or a guarantee of the smallest explanation.

Evidence (v0.11.1): implementation · regression tests

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)
  graph = ancestors_first_dag(root, deduplicate_shared_parents=true)
  remap parent indexes locally
  return graph

Why-false starts from an absent query and explores candidate rules against the completed result. It reports obstacles such as a missing positive fact, a present negated fact, a failed comparison, filter or aggregate condition. PUG is related work on why/why-not provenance, not a claim that Maelys implements the PUG algorithm. Maelys keeps this diagnostic exploration separate from solving and bounds its candidates, branches, depth and output.

Evidence (v0.11.1): implementation · regression tests

require successful membership query says absent
frontier = candidate_rules(query)

while frontier is not empty and explanation budgets remain:
  candidate = next_in_canonical_order(frontier)
  inspect candidate against the completed result
  retain bounded obstacles and nested causes

return document(obstacles, complete_or_truncated)
# No solve and no mutation of the result.

The language supplies count, min, max and sum over a completed lower relation. Count deduplicates the projected typed values. Sum instead adds one integer contribution per distinct source fact: two different facts with the same projected amount both contribute. Signed overflow and invalid aggregate input fail the solve; they are not silently clamped or published as partial answers. These are language and engineering contracts, not newly invented aggregate operators.

Evidence (v0.11.1): implementation · regression tests · min/max/sum and failure tests

source = completed_relation_for_bound_group()
count = number_of_distinct_typed_projected_values(source)

sum = 0
for each distinct source fact:
  require projected value is an integer
  sum = checked_int64_add(sum, projected value)

on domain error or overflow:
  reject the solve

A reference session keeps its preparation and bounded working storage for successive requests. Only one result may be alive per session. Explanation workspace reuse is optional: prepare one explanation, measure it, then format it without repeating the exploration while the cached query is unchanged. Allocation-free native hot paths are tested, but this does not make construction, output text allocation or Python objects allocation-free. In 0.11.1, sessions also share engine-owned immutable policies; caller-owned policy storage still receives an independent session snapshot.

Evidence (v0.11.1): implementation · regression tests · allocation guard

session = prepare(policy, optional_workspace)
for each request:
  result = solve(session, complete_input_snapshot(request))
  query(result)
  optionally explain(result)
  release(result)
release(session)

Maelys separates the manifest file digest from compiled-policy and execution identities. Canonical policy material includes the vocabulary, rules and applicable extension identities; the execution identity additionally records the selected backend and execution configuration. Applications can record these with a decision. SHA-256 identifies material: it does not authenticate its author, replace a signature, or guarantee confidentiality.

Evidence (v0.11.1): implementation · regression tests

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)
  decision = query(result, allow(request.id))
  return { decision, source_digest, policy_fingerprint, execution_fingerprint }