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