1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
#+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 containment check itself is no longer hand written: admission
runs the checker extracted from =theories/DecreaseChecker.v=, where
its soundness (a successful check really is strict containment,
leaves and labels included) and the decrease theorem are proven.
What remains trusted: the injective conversion from =Pattern.t= to
the checker's term shape, the two equality functions handed to it,
and the surrounding admission logic. Each future extraction shrinks
that list.
* 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.
|
