1 files changed, 83 insertions, 0 deletions
diff --git a/docs/vm.org b/docs/vm.org
new file mode 100644
index 0000000..e104b0f
--- /dev/null
+++ b/docs/vm.org
@@ -0,0 +1,83 @@
+#+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.
+
+* 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.