About

This document specifies the runtime that executes Sol. Everything in the first sections is implemented in lib/ and tested; the last section specifies what the runtime owes the future and how it will grow without changing the meaning of what already runs.

Object model

The VM manipulates a small set of value kinds, all immutable:

terms (Term.t)

canonical closed values. Integers and strings ground the tower; rationals are irreducible with denominator greater than one; records are nonempty labeled tuples in canonical attribute order; #() is the empty sequence. Canonicity is sealed at construction, so structural equality is value equality and a term can be hashed as it stands.

patterns (Pattern.t)

terms open over logic variables. Rule heads, rule bodies, goals and answers are patterns.

substitutions (Pattern.Subst.t)

the unification store. Grow only; unification runs an occurs check because Sol terms are finite.

expressions (World.expr)

compiled propositions: application, conjunction, disjunction, denial, universal.

relation definitions (World.def)

a table (schema plus finite stored tuples) or a rule set. Rules carry their name, head bindings, body, and, when recursive, the decrease witness label that admission found.

worlds

whatever satisfies the WORLD module type: a total answer to "which definition lives under this name". The engine holds no other state about storage.

Execution

One mechanism runs everything: goal search over a substitution.

A relational expression flattens into goals. Each step, the engine runs any goal decidable under the current substitution:

• a builtin decides membership, unifies equality, computes or solves arithmetic, compares, or enumerates a bounded range;
• a table application scans finite facts, unifying goal bindings against each tuple;
• a rule application unfolds: variables rename apart with an unlexable stamp, goal bindings unify with the head, and the body's goals join the queue. Unfolding requires every recursive rule's witness argument ground, which turns the admission proof into a runtime termination measure;
• a denial runs once its variables are ground, refuting by exhaustive search of a total subproblem;
• a universal runs once its quantifier is decidable, checking the body against every quantifier solution.

Goals that are not yet decidable wait. When only waiting goals remain, membership residuates and search rejects: if every remaining goal is builtin membership, the answer carries them as residual constraints; if any is a stalled search, the plan is rejected with the stuck goals named. This is the whole of the distinction the specification demands: membership checks or residuates, constraints wait, generation only under bounds, and non total plans do not execute.

Answers are the query's free variables resolved to canonical values, plus the residual constraints the answer is conditioned on; the common case is ground and residue free. Variables that live only under a universal are not answer variables. Integrity criteria accept only residue free proof: a conditioned answer admits no fact.

Totality accounting

The engine terminates on every admitted program. The argument, each piece machine checkable and one piece machine checked today:

1. every rule that unfolds recursively carries its component's lexicographic measure, all positions ground at unfolding, and every call cycle through the component strictly decreases it;
2. strict containment decreases a natural measure, the induced order is well founded (proven in theories/Decrease.v), and the lexicographic product of well founded orders is well founded;
3. tables are finite, builtins decide or defer without search, and bounded generators enumerate finite ranges;
4. disjunction and rule choice branch finitely.

The containment check itself is no longer hand written: admission runs the checker extracted from theories/DecreaseChecker.v, where its soundness (a successful check really is strict containment, leaves and labels included) and the decrease theorem are proven. What remains trusted: the injective conversion from Pattern.t to the checker's term shape, the two equality functions handed to it, and the surrounding admission logic. Each future extraction shrinks that list.

Integrity control hooks

Admission is the integrity boundary. Facts enter a world only through: groundness, exact schema match, primitive domain membership decided by the host, and membership criteria solved against the complete extension. A criterion is an ordinary expression with one free variable, so foreign keys, refinements and range checks are the same hook. Embedded hosts run the same hook by constructing pending checks and solving them with the same engine.

Interaction with stored relations

The engine never owns storage. A world answers find, now state scoped: the reserved at: label names the state a stored relation is read from, stripped before unification and demanded ground before the read runs. A world also answers transition: transition relations like Insert are the world's, never the engine's; the VM unifies the successor state with after: and defers ungrounded chains. The standalone world ignores states and has no transitions (decision 5). lib/branch is the reference stateful world: content-addressed states, append-only store, tip per branch, commit as compare and swap, and the linearity check of decision 6 over transition chains. RNT implements the same contract against its kernel. See docs/states.org.

Error and proof obligation reporting

Two error channels, both total:

• admission errors name the offense: the rule without a decrease, the mutual cycle, the unknown reference, the ill typed fact, the violated criterion;
• planning errors name the stuck goals, which is the language telling you which variable to bind or which search to bound.

Nothing is deferred as an unproven obligation; a program is admitted whole or not at all.

What the runtime owes the future

Specified, not yet implemented; each grows admission or planning without changing admitted semantics:

• richer propagation: the interval store today reads domains and one-sided comparisons; difference constraints between variables, arithmetic relations, and propagation through record structure are the next strengths;
• symbolic discharge beyond the interval fragment: algebraic identities of relations (universals mentioning Plus and kin), and arithmetic decrease measures for recursion that structural containment cannot see;
• Rocq certificates as admission evidence, and extraction of the lexicographic search itself (the containment core is already extracted);
• lowering of finite first order subplans to RNT's Plan.t algebra with Sakura's cardinality tags, per decision 9;
• tabling for shared subderivations, an optimization the pure semantics licenses.