#+TITLE: The VM

* About

This document describes the first working version of the Sol
pipeline: parser, loader, admission checks and solver. A program goes
from text to answers entirely inside the library; the binary in
=bin/= is a thin host that links the standalone world, exactly as
decision 4 prescribes. RNT embeds the same engine by satisfying the
=WORLD= module type with its own catalog.

* Surface

The parser produces one uniform node category. Atoms and variables
share a spelling, so classification happens at loading, by context: a
name in term position is a variable, a block is a proposition, and a
top level bare block asserts a fact. Directives are message sends:

#+BEGIN_SRC sol
Relation named: Person schema: #( [name domain: String] [age domain: Integer] )
[Person name: "Marcos" age: 30]
Rule name: "adult" head: [Adult name: N] body:
  [Person name: N age: A] :and [GreaterEqual left: A right: 18]
Query expression: [Adult name: N]
#+END_SRC

Delimiters follow the law of the specification: =[]= for
propositions, ={}= for records, =#()= for sequences, =()= for
grouping. =:or= binds looser than =:and=.

* Loading is admission

A program only becomes a world if everything in it is admitted:

- facts must be ground, match their schema exactly, and satisfy each
  attribute domain. This is integrity control at load time, the same
  membership check it always is. A Natural is an Integer and an
  Integer is a Rational, literally.
- a recursive rule must exhibit a structurally decreasing argument:
  some label whose call argument sits strictly inside the head
  argument, like =T= inside =#(H | T)=. The label is kept as the
  rule's witness. No witness, no world.
- mutual recursion between relations is rejected for now. Self
  recursion with a witness is the admitted form.
- every referenced relation must exist, either builtin or declared.

This is rung one of the evidence ladder in decision 10. Bounded
quantification exists through =Between=; symbolic discharge and Rocq
certificates are future rungs.

* Solving

The solver works by dynamic goal selection. At each step it runs any
goal decidable under the current bindings; goals that are not yet
decidable wait. So conjunction stays commutative in fact, not just in
doctrine: the page order of =:and= operands never matters, and the
tests assert it.

If no remaining goal can ever run, the plan is rejected as non
total. =[Integer value: X]= alone is not an enumeration, it is an
error telling you to bind or bound =X=. Membership is not generation.

Recursive rules unfold only when their witness argument is ground, so
the admission proof becomes a runtime termination measure: the
witness shrinks structurally at every unfolding and the search
bottoms out.

* Negation and quantifiers

=:not= is decidable denial. =u :not d= establishes the universe =u=
and then refutes =d=; the denial only runs when its variables are
ground, deferring like any other goal, so negation as failure over
open goals cannot happen.

=Exists= lowers to a conjunction at loading, since query variables
are existential already; its =variable:= is renamed apart so the
scope cannot be forged. =ForAll= runs when its quantifier is
decidable: every solution of the quantifier must satisfy the body. A
universal over an infinite domain is a non total plan, rejected, as
decision 10 requires. Variables that live only under a universal are
not answer variables.

* Membership criteria as domains

A schema attribute is constrained by a primitive domain or by a
criterion: any relational expression with exactly one free variable,
the subject, bound to the attribute value at admission.

#+BEGIN_SRC sol
Relation named: Employee schema: #(
  [name domain: String]
  [dept domain: ([Department id: D])]
  [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
)
#+END_SRC

A foreign key is the criterion =([Department id: D])=, nothing more
special than that. Criteria run against the complete extension, so
the order facts appear in the source does not matter, the same way a
committed state is judged whole. A fact whose attribute fails its
criterion is an integrity violation and the program gets no world.

* Builtins

Domains check membership once ground: Integer, Natural, Rational,
String. Equality unifies. Plus and Times evaluate forward and solve
backward through the rationals, and results collapse to minimal
shape, so =[Plus left: 1/2 right: 1/2 result: R]= binds =R= to the
integer =1=. Comparisons decide once both sides are ground. Between
is the one relation allowed to enumerate, because its range is finite
by construction.

* Running

=sol file.sol= loads the program and prints each query's answers.
=sol= alone is a REPL where declarations accumulate and queries run
immediately. Answers print as variable bindings in Sol notation, or
=yes.= and =no.= for closed queries.