Zenith Logic Foundry

Internals: The WAM Runtime

zlf has a single Warren Abstract Machine (WAM) runtime — zlf-prolog::wam::WamRuntime. There is deliberately no second evaluator.

Layering

ZlfDatabase (zlf-query)
  -> WamRuntime (zlf-prolog::wam)
       -> WamExecutor  (engine: machine, heap, environment stack, trail, choice points)
       -> CompositeFactProvider
            - StorageFactProvider   (nodes/edges/properties/labels)
            - FactStoreProvider     (logical P/3+ facts)
            - IndexFactProvider     (bm25 / vector / temporal)
            - IntrospectionProvider (predicate/3, rule/3, capability/1, ...)
            - GraphViewProvider / GraphAlgorithmProvider
            - PreparedRetrievalProvider
       -> StorageRuleStore (compiled rule artifacts)
       -> tabling (positive fixpoint evaluator + persisted tables)
  -> RocksDB (Storage)

Execution model

• Term representation: parser_ast::Term — Variable | Atom | Integer | Float | String | Compound | List | Object, serde-serializable.
• Heap: a typed cell store. Constants are type-tagged strings ($a: atom, $s: string, $i: integer, $f: float), so integer 1, float 1.0, atom x, and string "x" never unify.
• Unification is a stack-based MGU over the cell store with a trail for undo on backtracking.
• Registers / environments / choice points: a register file passes arguments; environment frames hold permanent variables; choice points snapshot the machine state for multi-clause predicates.
• Instructions: the compiler (WamCodegen) lowers queries, rules, and facts to an instruction set (put_*, get_*, unify_*, call, allocate, switch_on_*, try/retry/trust, cut variants, proceed). Compiled rule artifacts (CompiledRuleArtifact) persist via StorageRuleStore and reload on reopen.

Dispatch order

For a goal with no compiled program entry, dispatch_call resolves in this order:

1. compiled program (rules) — program.entry(key)
2. builtin executor (BuiltinExecutor::execute)
3. provider (try_provider_call -> CompositeFactProvider::facts_for_goal)

A compiled rule for P/N therefore shadows provider facts for the same key (pre-existing semantics).

Builtins

Builtins are a mix of catalogued native handlers (term/conversion/list/arithmetic/control) and stdlib rules compiled at runtime construction (once/1, \+/1, ;/2, ->/2, list library rules, …). Dynamic database builtins (asserta/assertz/retract/retractall/clause/current_predicate) write through StorageFactWriter / StorageRuleStore.

Tabling

Tabled predicates evaluate through a separate positive fixpoint evaluator (tabling/evaluator.rs) — not the main SLD loop:

• run_fixpoint seeds from provider facts and iterates rule evaluation to a fixpoint, deduplicating derived ground answers.
• Tables are persisted (RocksTableBackend) and selectively invalidated through reverse dependency indexes (table:revdep:*).
• Stratified negation (S1) lets a negated lower-stratum tabled goal complete its table first (tabling/negation.rs), erroring if that table is left Evaluating/Failed.

Proofs

Proof capture is opt-in (query_prolog_with_proof). Non-tabled queries produce derivation trees (ProofTree of ProofNodes). Top-level tabled queries produce one shallow ProofKind::Table node per answer; deep per-derivation provenance inside the fixpoint is deferred.

Stratification

storage/stratification.rs extracts signed dependencies (parity-carrying descent through call/once/,/;/->); storage/strata.rs runs Tarjan SCC + stratum assignment. StorageRuleStore::add_compiled_rule rejects non-stratified artifacts atomically, persisting signed deps under strat:* in the same batch as the rule.