virtual machine specification document

2 files changed, 140 insertions, 8 deletions

diff --git a/README.org b/README.org
index 94ab342..40d59e2 100644
--- a/README.org
+++ b/README.org
@@ -121,12 +121,13 @@ the unrestricted partiality of ordinary Turing-complete languages.
 
 ** Virtual Machine Specification
 
-This document has not been written yet.
+See: [[file:docs/virtual-machine-specification.org][docs/virtual-machine-specification.org]]
 
-It should describe the runtime architecture required to execute Sol
-programs.
+It describes the runtime architecture that executes Sol programs, as
+implemented in =lib/= and =theories/=, and what the runtime owes the
+future.
 
-Expected topics include:
+Topics covered include:
 
 - VM object model;
 - relation objects;
@@ -194,7 +195,7 @@ core claim, that strict containment decreases a well founded
 measure, is proven in Rocq and compiled as part of the default
 build.
 
-The next document to produce is
-=docs/virtual-machine-specification.org=, building on the language
-specification, the integration decisions, and the implementation as
-it stands.
+The design documents promised at the project's start now all exist:
+the language specification, the integration decisions, the core
+design and pipeline document, and the virtual machine
+specification.
diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org
new file mode 100644
index 0000000..8699f94
--- /dev/null
+++ b/docs/virtual-machine-specification.org
@@ -0,0 +1,131 @@
+#+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. If none can ever run, the plan
+is rejected with the stuck goals named. This is the whole of the
+distinction the specification demands: membership checks, constraints
+wait, generation only under bounds, and non total plans do not
+execute.
+
+Answers are the query's free variables resolved to canonical values.
+Variables that live only under a universal are not answer variables.
+
+* 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 remaining trusted gap between the OCaml checker and the Rocq
+statement closes by extraction (decision 10): the admission checker
+is the piece to extract first.
+
+* 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:
+
+- residuation: a constraint store that returns residual constraints
+  for satisfiable but underdetermined queries instead of rejecting;
+- 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.