#+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. When goals remain that cannot run, two things can happen. If every one of them is pure membership, decidable the moment its variables ground, the answer comes back with those goals as residual constraints: =[Integer value: X]= alone answers =X= conditioned on =[Integer value: X]=, which is exactly what the expression means. Constraining is not searching. If any remaining goal is a stalled search, an unbounded recursion or an infinite universal, the plan is rejected as non total. Membership is never generation either way. 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. * Embedding The solver is a functor over the =WORLD= module type: a host answers =find= for its own relations and links the engine in-process. The embedding test builds a toy kernel catalog in plain OCaml, compiles query text through =World.expr_of_node=, and runs the same solver with the same totality guard. That is the RNT shape: Sakura compiles Sol (and Karuta lowered to Sol) to expressions, the kernel's catalog answers =find=, and no process boundary exists. * 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.