#+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 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.
