#+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. - recursion must exhibit a lexicographic structural decrease. Admission groups rule defined relations into strongly connected components of the call graph and searches for an ordered list of labels such that every call inside the component strictly shrinks at some position, all earlier positions staying equal. Self recursion is the one label case, like =T= inside =#(H | T)=; mutual recursion like Even and Odd passing a shrinking list back and forth is admitted the same way. The measure is stamped on the recursive rules as their witness. No measure, no world. - 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, the engine first propagates over the waiting membership constraints as one interval store. Bounds with an empty intersection fail the branch outright: =X > 5= with =X < 3= answers no, not a conditioned maybe, and so does asking one value to be both an integer and a string. An integer variable squeezed into a finite range converts to bounded generation: =[Natural value: X] :and [LessThan left: X right: 4]= enumerates 0 through 3, the same admissible enumeration =Between= performs explicitly, because the combination of constraints is a finite relation. This is Sakura's cardinality analysis working inside the engine. If propagation finds neither a contradiction nor a finite range, two things can happen. If every waiting goal 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. Variables that live only under a universal are not answer variables. A universal over an infinite domain is never enumerated. It gets one chance at symbolic discharge: when quantifier and body both read as kind and interval constraints over the quantified variable, the engine decides entailment algebraically. Every natural is at least zero: proven. Not every integer is: refuted, and the refutation is backed by a concrete counterexample. Every integer is a rational: proven, which is decision 12's subtype inclusion decided symbolically. The unit identities of the numeric relations discharge too: =[Plus left: X right: 0 result: X]= holds over all integers by the algebra of =Plus=, in the flat membership form of decision 14, and fails over strings, which do not add. A universal outside that fragment is a non total plan, rejected, as decision 10 requires. * 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.