#+TITLE: Virtual Machine Specification
* 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 has a witness whose argument
is ground and strictly contained in the head's at each unfolding;
2. strict containment decreases a natural measure, and the induced
order is well founded: proven in =theories/Decrease.v=;
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=; the standalone
world is an immutable map built by loading; RNT's world is the
kernel catalog, where tuples are content addressed and a branch tip
names the state being read. State scoped reads (decision 7) enter
here: the host resolves =at:= to a snapshot and serves =find= from
it. Transitions and commit stay outside the engine, in DCL and the
kernel's single compare and swap (decisions 3, 5, 8).
* 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:
- constraint propagation: residuated constraints today wait and
return; a store that actively narrows domains and detects
unsatisfiable residue early is the next strength;
- symbolic discharge: algebraic evidence for universals over
infinite domains, and arithmetic decrease measures for recursion
that structural containment cannot see;
- Rocq certificates as admission evidence, and extraction of the
checker itself;
- mutual recursion under lexicographic measures;
- 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.
