path: root/docs/sakura-RNT-integration.org

#+TITLE: Sol / Sakura / RNT Integration
#+AUTHOR: Marcos Magueta

* Purpose

This document records the architectural decisions binding Sol to the
Sakura relational engine (=../sakura=) and the RNT database kernel
(=../RNT=). These decisions were reached by adversarial design review
(2026-07-11) and are normative: later documents (the pipeline
specification and the VM specification) must not contradict them
without revisiting the arguments recorded here.

* The Stack, As It Exists

Facts established from the codebases, not decisions:

- *RNT* is a database kernel currently being rewritten in OCaml (the
  original execution core was C++; its design carries over). Its
  execution core, *FOL* (=lib/backend/execution/FOL.ml=), mechanically
  evaluates first-order relational plans under the Volcano pull
  model. Every plan terminates: evaluation is model
  checking against one fixed, finite model, which is decidable. RNT
  makes no independent termination judgements; it trusts plan
  annotations.
- *Sakura* (OCaml) is the authoritative source of semantics. It owns
  cardinality analysis (=Finite= / =ConstrainedFinite= / =AlephZero= /
  =Continuum=), termination enforcement (=TAKE= insertion), join
  ordering, and physical storage.
- Sakura's sublanguages are cleanly separated modules: DRL (pure
  retrieval, total), ICL (integrity constraints as membership checks),
  DCL (branch management and 3-way merge over content-addressed
  tips), DML (delta semantics), DDL, with TCL planned.
- =sublanguage.ml= classifies operations categorically: a *Query* is a
  natural transformation between instance functors (state unchanged);
  a *Transition* is a morphism in the category of database states.
- RNT tuples are content-addressed: each tuple is stored under the
  SHA256 digest of its serialized bytes. DCL branches point to tips
  identified by hash. Database states are therefore already
  first-class Merkle-style values in this architecture.
- *Karuta* is a Prolog-like language targeting the BEAM, positioned at
  the application layer.

* Decision 1: Totality Is a Stack-Wide Invariant

** The decision

Sol is total, and so is the entire database language stack. The
previously entertained idea of a Turing-complete PPL (predicate
procedure language) — recorded in =sakura/lib/sublanguage.ml= ("PPL ->
new effect class: potentially non-terminating computation") and in
=karuta-integration.org= ("a predicate procedure language might [be
Turing complete]") — is *retracted*.

Problems that genuinely require Turing-complete computation belong in
the application layer (Karuta on the BEAM), not in the database.

** The argument

- P1. A very large class of useful programs is expressible in a total
  language: arithmetic, data-structure algorithms, parsers, theorem
  provers, sorting, type checkers, relational evaluators — anything
  whose recursion is structural and provably terminating.
- P2. Admitting unbounded recursion anywhere in the stack re-imports
  the halting problem into every layer above it, destroying the
  termination guarantee that RNT's execution core is *named after*
  (see =RNT/new-docs/fol.org=: "do not make the query language
  Turing-complete").
- P3. Stored procedures are the layer where users write the most
  logic; that is the worst possible place to lose the guarantee.
- C. Therefore the database language is total, with no partial
  escape hatch inside the database. Partiality lives outside, in the
  application layer.

* Decision 2: Sol Is the Database Language; Karuta Compiles to It

** The decision

- Sol is *the* language of the Sakura/RNT RDBMS, and its VM is the
  database runtime. It plays the role SQL plays in PostgreSQL: the
  language exposed at the REPL and over the wire.
- Karuta remains the application-layer language. It compiles to the
  s-expression interchange form and internally targets Sol; this
  compilation happens *inside Sakura* — Sakura hosts the Karuta
  front-end and lowers it onto Sol, the same way it receives Sol
  directly from the REPL or the wire. Karuta does not front the
  sublanguages directly anymore; Sol does.
- The sublanguages (DRL, ICL, DCL, DML, DDL, TCL) are not separate
  surface languages. They are fragments of Sol, distinguished
  semantically (query vs. transition), not syntactically balkanized
  as in SQL.

** The argument

- P1 (uniformity requirement). A stored relation and a computed
  relation must be handled identically: the same application syntax,
  the same membership semantics. "The same way we handle a relation
  stored in the database, we invoke a function facing a relational
  interface."
- P2. Two surface languages over one semantic core is the negation of
  uniformity — it reproduces the SQL disease: a *collection* of
  sublanguages with no harmonic whole.
- C. One language, Sol. Everything else (Karuta included) is a
  compiler front-end or client of it.

* Decision 3: Transitions Are Relations Over Database States

** The decision

Sol expresses state change (DML, DDL, DCL) as *relations between
database states*. A database state =S= is a first-class value — which
the architecture already supports, since tuples are content-addressed
and branch tips are hashes.

An insert is a relation:

#+BEGIN_SRC sol
[Insert relation: Person tuple: T before: S after: S']
#+END_SRC

This proposition holds exactly when state =S'= is state =S= with =T=
admitted into =Person= (which entails =T= passing every ICL
constraint attached to =Person= — membership checking and integrity
control are the same operation, per the language specification).

Exactly *one* primitive effect exists, outside the logic, at the
edge: *commit* — advancing a branch tip (HEAD) from =S= to =S'=. As
in git: everything is pure value manipulation until the single
mutable reference moves.

** The alternatives rejected

- *Two-layer language* (pure core + imperative command shell, à la
  Haskell IO): honest, but bifurcates the grammar into expressions
  and commands — DML becomes a foreign sublanguage again, violating
  Decision 2's uniformity premise.
- *Smalltalk message-sends with hidden effects* (=Person insert: T=
  mutating in place): the surface says "message", the internals
  perform a state morphism. Dishonest syntax — the construct's
  surface form would not mean what the internals do. Rejected on the
  syntax-honesty principle.

** The argument

- P1 (uniformity). Transitions expressed as relations use the same
  application syntax, the same conjunction, the same proof-search
  semantics as everything else in Sol.
- P2 (fact). Database states are already first-class Merkle values in
  RNT/Sakura (content-addressed tuples, hash-identified branch
  tips). State-as-value is not an invention; it is a recognition.
- P3 (honesty). =sublanguage.ml= already classifies DML/DDL/ICL/DCL
  as morphisms in the category of database states. Making the states
  and the morphism explicit in the surface syntax makes the language
  say exactly what the semantics do.
- C. An insert *is* a relation over states.

** What this buys

Because =Insert(R, T, S, S')= is an ordinary proposition, it can be
*queried* as well as *performed*:

- provenance and audit are ordinary conjunctions over the state
  chain;
- time-travel queries are membership checks against old states;
- dry-run is evaluating the transition relation without committing;
- a transaction is a composition of transition relations
  =S → S' → S''=, committed atomically by moving HEAD once, to the
  final state;
- DCL merge is already a ternary relation over states (two tips and
  an ancestor) — Decision 3 makes the rest of the language match it.

** Acknowledged costs

- State identity and equality must be defined precisely (hash
  equality of content-addressed states is the candidate, but
  canonical serialization must be specified).
- Sequencing becomes conjunction over chained state variables; the
  planner must order these chains. This is real planning work, though
  of the same kind DCL merge already performs.

* Decision 4: Sol Is a Library; RNT Links Its Compiler and VM In-Process

** The decision

Sol — the whole pipeline: normalizer, planner, totality checker, and
VM — is built as a host-neutral OCaml library, parameterized over a
=WORLD= interface: the store that answers which relations exist,
their capabilities, how membership is checked against stored tuples,
and what commit means.

Two hosts consume it:

- *Standalone Sol*: a thin binary links the library with an
  in-memory or file-backed world. This world exposes only the pure
  fragment: no branches exist, so transition relations and commit are
  simply absent capabilities (see Decision 5). This satisfies the
  requirement that Sol be usable as a separate language for ordinary
  (total) programs.
- *RNT*: the kernel links the library in-process as its execution
  layer. RNT's planned split between "terminating first-order logic
  and higher-order logic execution" is filled directly: the FOL core
  executes the finite-plan fragment (=Plan.t=, Volcano), and the HOL
  slot *is* Sol's engine — not a reimplementation, the same compiler
  internals. The world is the object manager plus the
  content-addressed store; commit advances a branch tip atomically
  inside the kernel.

** The argument

The earlier framing — "Sol VM inside the kernel" versus "Sol VM as a
client of the kernel" — was a false dichotomy.

- P1 (requirement). Sol must run standalone, with no database
  present.
- P2 (Decisions 2–3). Sol's VM is the database runtime, and commit —
  the single effect — must be atomic against RNT's branch tips.
- P3. A client-process VM satisfies P1 but makes the only effect
  distributed, breaking P2. A kernel-welded VM satisfies P2 but
  cannot exist without the database, breaking P1.
- C. The VM must be neither: a library over an abstract world. RNT
  linking it in-process preserves atomicity; the standalone host
  preserves independence. One implementation, two hosts — an
  embeddable runtime in the manner of SQLite or Lua, where one of
  the embeddings is the database kernel itself.

The language specification already gestures at this seam: membership
criteria "constructed at the host language," capabilities as declared
operational permissions, =World= as a relation. The =WORLD= interface
is that seam made explicit.

** Acknowledged costs

- The world interface is a hard public contract. Capability
  negotiation — which worlds support enumeration, solving, bounded
  generation — must be specified precisely.
- Standalone-world semantics must be a strict subset of
  database-world semantics, so that a program proven total against
  the standalone world remains total in-kernel.

* Decision 5: A State Is a Branch's Whole Tree

** The decision

The state values =S=, =S'= in transition relations denote *branch
states*: the catalog, schemas, ICL constraints, and the extension of
every relation *as one branch sees them*, as one content-addressed
tree — exactly a git commit object. Concretely, =S= is the Merkle
root hash of the branch's tree: a snapshot handle into the
content-addressed store, cheap to hold, structurally shared with
neighboring states.

There is no global "database state" spanning branches. Transition
relations are meaningful only within a branch: a stored procedure
receives the branch's current root hash, evolves it purely — each
transition producing the successor hash — and yields the final hash,
which commit installs as the new tip.

It works like git: all value manipulation is pure; history is a chain
of whole-database states; the single effect (Decision 3) is advancing
a branch tip to a new state.

Consequently, transition relations exist only in the RNT/Sakura
world. The standalone world has no branches, hence no transitions and
no commit — standalone Sol is the pure total fragment. This is
capability negotiation (Decision 4) doing its job, not a special
case.

** The alternative rejected

Per-relation states — the database as a bag of independently
versioned relations — fail on two counts:

- P1. DDL and ICL changes are also transitions (Decision 2); a
  per-relation state has no place to record "the schema changed" or
  "a constraint was added."
- P2. Integrity constraints span relations (foreign keys as
  membership checks against *other* relations). A transition's
  validity must be judged against a consistent snapshot of all
  relations, or ICL checking is unsound.
- P3 (fact). DCL already works on whole tips: a branch is one hash,
  and 3-way merge operates on two tips and an ancestor.

Nothing is lost: in a content-addressed tree, per-relation hashes
still exist as internal nodes, and unchanged subtrees share
structure.

** Acknowledged costs

- Hashing must be incremental — a transition recomputes hashes along
  the changed path only (O(path), not O(database)) — or commit
  throughput dies. Merkle trees provide exactly this.
- Canonical serialization of states must be specified early; state
  equality is hash equality only if serialization is deterministic.

* Decision 6: Sequencing Comes from Linear State Threading, Not Syntax Order

** The decision

Transition sequencing derives *solely* from state-variable sharing,
never from syntactic position:

#+BEGIN_SRC sol
[Insert relation: Person tuple: T1 before: S0 after: S1] :and
[Insert relation: Person tuple: T2 before: S1 after: S2]
#+END_SRC

=:and= remains honestly commutative: swapping the conjuncts changes
nothing, because the chain =S0 → S1 → S2= is carried by unification.
The planner topologically sorts the state chain, the same discipline
Sakura already applies when ordering joins by variable binding.

State variables obey a *linear discipline*, in the manner of
Mercury's =di=/=uo= (destructive-input / unique-output) modes on
=io.state=: within a transaction, each state value is consumed
exactly once (as =before:=) and produced exactly once (as =after:=).
The felt experience is procedural — a timely order, step after step —
but the order is implied by the dataflow, not decreed by the page.

A transaction is a relational expression whose state variables form
one linear chain from the branch tip (=S0= = HEAD) to a final state,
followed by one commit of that final state (Decision 3).

** The argument

- P1. =:and= means logical conjunction, and conjunction is
  commutative.
- P2 (syntax honesty). The surface form must mean what the internals
  do. If evaluation order were read off the page, =:and= would be a
  lie — sequencing dressed as conjunction. This is the same sin the
  language specification already rejects in "newline adjacency
  secretly means conjunction."
- P3. Unification is Sol's only binding mechanism; threading state
  through shared variables introduces no new primitive.
- C. Order-from-dataflow is the only admissible sequencing. The
  linear mode discipline makes chain-hood a static property: a fork
  (two transitions consuming the same =S=) or a reuse is a mode
  error caught at admission, not a planner heuristic.

** Sugar policy

A convenience form (e.g. a =Transaction do:= that auto-threads the
state variables) is permitted *only* as sugar with a published
elaboration into the explicit chain. It must never become a
primitive with its own semantics.

** Acknowledged costs

- Verbosity until sugar lands: users name =S0=, =S1=, =S2=
  explicitly.
- The mode/linearity checker must be specified as part of admission
  checking, alongside schema and totality checks.

* Decision 7: Reads Are State-Scoped

** The decision

In the RNT/Sakura world, *every* read of a stored relation happens
from an explicit state. In the core language, a stored-relation
application carries the state it reads at:

#+BEGIN_SRC sol
[Person id: P age: A at: S1]
#+END_SRC

A scoping form is provided as sugar, with a published elaboration
that distributes the state over the stored-relation applications in
its body (Decision 6's sugar policy):

#+BEGIN_SRC sol
[At state: S1 body: [Person id: P age: A] :and [Adult person: P]]
#+END_SRC

At the REPL, a bare query elaborates to =at:= the current branch
tip's state — one uniform rule, not a second semantics.

Standalone Sol is untouched: it has no stored relations, hence no
=at:=.

** The argument

- P1 (Decision 6). Order on the page carries no meaning; so "read
  whatever the previous statement produced" is not available — it is
  positional order, the outlawed lie.
- P2. Reads must therefore name their state, or a hidden convention
  decides — dishonest syntax.
- P3. The alternative — all reads pinned to the transaction's initial
  =S0= — makes read-your-own-writes inexpressible: a procedure that
  inserts and then validates against the result cannot be written,
  even though ICL checking inside the chain already reads
  intermediate states. The language would forbid users what its own
  machinery does.
- C. Reads are state-scoped in the core; terseness is recovered by
  sugar, never by convention.

** Acknowledged costs

- =at:= becomes a reserved label on stored-relation applications; it
  cannot be a schema attribute name.
- The elaboration of =At state: body:= must be specified precisely,
  including its interaction with nested =At= forms (innermost wins)
  and with transition relations (which are already explicit and are
  not rescoped).

* Decision 8: The Kernel Arbitrates Only the Tip; Conflict Policy Is DCL

** The decision

The only point of contention in RNT is the tip of a branch. The
kernel therefore provides exactly one concurrency primitive: *atomic
compare-and-swap on a branch tip* — install =Sn= as the tip iff the
tip still equals the =S0= the transaction started from.

Everything above that primitive is the version-control language's
domain, and DCL is a fragment of Sol (Decision 2) operating on
states as values (Decision 5):

- *fast-forward*: the tip is an ancestor of =Sn= — install directly;
- *rebase*: re-execute the procedure from the new tip — sound and
  safe because a transaction is a pure, total function of its
  initial state (Decisions 3, 6); nothing partial ever escaped;
- *3-way merge*: already a ternary relation over two tips and their
  ancestor, with declared strategies (=PreferLeft=, =PreferRight=,
  =RevertToAncestor=).

Conflict policy is thus *expressed in the language*, not hardcoded
in the kernel.

** The argument

- P1. A pure total transaction has no partial effects to undo;
  re-execution from a moved tip is always safe and always
  terminates. The classical difficulty of transaction retry does not
  exist here.
- P2. Given P1, any policy the kernel could hardcode (retry, merge,
  reject) is expressible as relations over states — and DCL already
  contains the vocabulary.
- P3 (minimality). A kernel primitive should exist only where the
  kernel is the sole possible arbiter. Tip installation is the one
  such place; policy is not.
- C. Kernel = CAS on the tip. Policy = DCL, in Sol.

** Acknowledged costs

- Any retry/arbitration loop is unbounded under contention. It lives
  outside the total language — in the commit arbiter or client,
  alongside the REPL loop. Sol proves each execution terminates; the
  arbiter decides how many executions happen. Partiality is confined
  to that boundary and must be documented as such, with a
  fairness/backoff policy.

* Decision 9: No DRL Syntax — the Plan Is Chosen by Analysis

** The decision

There is no distinguished DRL surface form. The user writes uniform
Sol; the planner decides how each subexpression executes. Since
*both* engines are total, engine choice is not a semantic
distinction and must not be a syntactic one: it changes performance,
never meaning (Codd's theorem licenses the lowering — the finite
first-order fragment and the plan algebra are the same queries).

What actually distinguishes subexpressions is what their relations
*are*:

- *stored relations* — scanned at an explicit state =S=
  (Decision 7);
- *ephemeral relations* — algebraic artifacts of relational
  operations, carrying provenance and lineage (Sakura's existing
  notion);
- *rule- and procedure-defined relations* — unfolded, or evaluated
  by fixpoint on Sol's engine.

The planner — reusing Sakura's cardinality propagation (=Finite= /
=ConstrainedFinite= / =AlephZero= / =Continuum=), constraint
propagation, boundness/mode analysis, and join ordering — identifies
maximal finite, first-order, non-recursive subexpressions and lowers
them to the plan algebra (=Plan.t=) for RNT's FOL core. Everything
else runs on Sol's engine, which pulls from lowered plans as cursors
(Volcano composes across the seam).

** The argument

- P1 (Decision 2). Sublanguages are semantic fragments, not
  syntactic ones; a DRL marker would re-balkanize the language.
- P2 (totality, Decision 1). Both engines halt, so there is no
  observable semantic difference for a marker to honestly denote.
- P3 (fact). Sakura already computes the needed evidence —
  cardinality tags, TAKE insertion, boundness-driven join ordering.
  The lowering criterion reuses existing analysis.
- C. Fragment-by-analysis. The FOL core is an invisible optimization
  target; the observable contract is only the tuple stream.

** Acknowledged costs

- Each lowering must be meaning-preserving and should be checkable
  (the =Plan.t= translation is a verifiable step, not a trusted
  one).
- A user who needs the guarantee "this runs as a flat finite plan"
  gets it as a declarable *assertion* (reject if not lowerable),
  never as a separate language.

* Decision 10: Totality Is Established at Admission, Verified in Rocq

** The decision

Totality evidence is checked at *admission time*: defining a rule or
procedure is itself a DDL transition (=[DefineRule ... before: S
after: S']=), and the definition fails — the successor state does not
come to exist — unless the evidence is present. A state containing a
non-total rule is unrepresentable; queries therefore run against
states where everything is already proven total and pay nothing at
query time.

The evidence is a closed ladder; each rung is recorded in the rule's
metadata:

1. *Structural decrease* — the checker finds a strictly decreasing
   argument (e.g. =Tail= < =[Head | Tail]= in =Length=). Automatic;
   covers most honest recursion.
2. *Bounded quantification* — the searched space is =Finite= or
   =ConstrainedFinite= by Sakura's cardinality analysis.
3. *Symbolic discharge* — algebraic properties prove the universal
   or the recursion (e.g. =Plus(X, 0) = X= over all integers).
4. *Certificate* — a Rocq proof, checked before admission. Because
   the certificate is verified, this rung is not a trusted escape
   hatch. A merely *trusted* declaration remains possible only as a
   last resort: named, auditable, and loud.

Anything fitting no rung is *rejected* — never admitted as a pending
obligation.

Two levels, not conflated:

- *Object level*: the ladder above, run by the in-engine admission
  checker on each definition.
- *Metatheory*: Rocq/Coq proves the guarantees of RNT/Sakura
  themselves — soundness of the admission checker ("any accepted
  rule is total"), meaning-preservation of the =Plan.t= lowering
  (Decision 9), soundness of ICL checking, and merge respecting its
  specification. Since RNT and Sakura are OCaml, the critical
  checkers should be *extracted* from Rocq to OCaml, so the thing
  proven is the thing running.

** The argument

- P1 (Decision 5). States are values. A state containing an unproven
  rule is a state whose queries might not halt; admitting it
  falsifies the totality invariant *inside* every descendant state.
- P2. "Obligation pending" is Coq's =admit=: tolerable in an
  interactive proof, poisonous in a database that other parties
  query concurrently.
- P3. A checker that is itself unverified moves the trust boundary
  rather than discharging it; the Rocq metatheory closes that gap.
- C. Total-or-absent at admission; verified checker; certificates as
  proofs, not promises.

** Acknowledged costs

- The structural-decrease checker and the symbolic-discharge engine
  must be specified precisely (the pipeline document owns this).
- Rocq extraction constrains implementation style in the affected
  modules (pure, extraction-friendly OCaml).
- Proof maintenance is a real, ongoing cost paid for the guarantee
  that is the project's entire premise.

* Decision 11: The Catalog Is Relations

** The decision

Everything in a state is a relation, and everything is queryable —
including the catalog itself. Relation definitions, schemas, rules,
constraints, and capabilities are tuples in catalog relations, stored
in the same content-addressed tree, read at a state like anything
else:

#+BEGIN_SRC sol
[Relation name: N schema: Sch at: S]
[Constraint name: C relation: R body: B at: S]
#+END_SRC

(A concrete catalog plan already exists on the Sakura/RNT side; this
decision binds Sol to it.)

** What follows

- DDL is DML on catalog relations: =DefineRelation= is an insert
  into the catalog — one mechanism, not two (Decision 3 already made
  DDL a transition; this removes its last special machinery).
- Admission checking (Decision 10) becomes ICL on the catalog: "a
  rule tuple enters =Catalog.Rule= only with totality evidence" is
  an ordinary integrity constraint on an ordinary relation.
- Introspection is an ordinary query at =S= — which merge,
  migrations, and tooling need anyway.

** The argument

- P1 (Decision 2). A catalog reachable only through special forms is
  a second interface — the SQL disease; =information_schema= is
  SQL's own admission that it bolted this on too late.
- P2. Catalog-as-relations lets Decisions 3 and 10 collapse into
  existing machinery instead of demanding parallel mechanisms.
- C. The catalog is stored relations, guarded by ICL, versioned in
  the tree, queryable in Sol.

** Acknowledged costs

- Metacircular bootstrap: the catalog's schema must describe itself
  (the fixed point every self-describing catalog has — Postgres's
  =pg_class= describes =pg_class=), and some base constraints must
  be primitive rather than ICL-expressed.

* Decision 12: Subtyping Is Proven Inclusion; Identity Is Intensional; Quotients Are Canonical

** The decision

Sol's type system represents subtyping, and it is *semantic*
subtyping — subtyping is relation inclusion:

#+BEGIN_EXAMPLE
S <: T  ≜  ∀x. S(x) → T(x)
#+END_EXAMPLE

Subsumption is not a rule added to the logic; it is the transitivity
of membership: =x ∈ S ∧ S ⊆ T ⊢ x ∈ T=. A refinement is a subtype by
construction (it is an intersection). =Natural <: Integer= because
ℕ ⊆ ℤ.

Three clauses make this precise:

*** (1) Inclusion judgments go through the evidence ladder

=S <: T= is a universal over a possibly infinite domain —
undecidable in general. A subtyping judgment is therefore admitted
by exactly the regime of Decision 10:

- declared-and-checked facts for the base lattice (=Natural <:
  Integer= lives in the catalog, queryable, per Decision 11);
- symbolic discharge for refinements (constraint implication:
  =x ≥ 18 → x ≥ 0=);
- finite scan for finite relations;
- Rocq certificate otherwise.

Inclusion between arbitrary relations is never silently inferred.

*** (2) Relation identity is intensional, never structural

Two relations with identical label sets are not the same relation.
Identity comprises the schema *and* the membership criterion (the
intension) — one relation conjoined with a =GreaterThan= constraint
is semantically different from its unconstrained twin — and, for
ephemeral relations, provenance and lineage (Sakura's existing
notions). Consequently:

- shape implies nothing: no structural typing, no implicit width
  subtyping;
- a tuple with more labels does not silently inhabit a
  narrower-schema relation — *projection* is the explicit morphism
  for forgetting attributes, and it stays explicit.

*** (3) Quotient domains use canonical minimal-shape representatives

Rationals expose the classical quotient problem: ℚ is
ℤ × (ℤ∖{0}) quotiented by =(a,b) ~ (c,d) ⟺ ad = bc=, so
={numerator: 2 denominator: 2}=, ={numerator: 1 denominator: 1}=,
and =1= all denote one value. Sol resolves quotients by *canonical
representatives*, enforced by the domain's own membership criterion,
and canonicalization picks the *minimal shape*: an integer-valued
rational normalizes to the ground integer itself
(={numerator: 2 denominator: 2}= normalizes to =1=, not to
={numerator: 1 denominator: 1}=).

Therefore ℤ ⊂ ℚ holds *literally, as membership inclusion* —
representation does not limit inclusion, and no injection or
coercion machinery exists. Non-canonical pairs are pre-values that
normalize in, via a normalization relation declared as part of the
domain's catalog definition:

#+BEGIN_SRC sol
[RationalNormalize raw: {numerator: 2 denominator: 2} canonical: 1]
#+END_SRC

The alternative — setoids, where all representatives are members and
every relation carries congruence obligations with a per-domain
=Equal= — is rejected: congruence proofs metastasize over every rule
ever defined.

** The argument

- P1 (Decision 5). States are content-addressed; state equality is
  hash equality. If two representatives of one value could both be
  stored, equal databases would hash differently — hash equality
  would be a lie. Canonical forms are *mandated* by the Merkle
  store, not merely preferred.
- P2. Given canonical forms, choosing the minimal shape as canonical
  is the unique choice under which numeric-tower inclusion
  (ℤ ⊂ ℚ) is true on the nose rather than simulated by coercion.
- P3. Normalization is already one third of Sol's execution model
  ("proof search, constraint propagation, and normalization") — no
  new primitive is introduced.
- C. Subtyping as proven inclusion, intensional identity, canonical
  quotients.

** Acknowledged costs

- Operations over quotient domains accept mixed shapes and
  normalize at the boundary (e.g. =Plus= over =Rational= handles
  ground integers and canonical pairs).
- A quotient domain without a declared normalization relation is
  rejected at admission: no equivalence without a normalizer.
- The subtype lattice for base domains must be seeded in the catalog
  bootstrap (Decision 11's metacircular fixed point grows slightly).

* Decision 13: OCaml for the Implementation, Rocq for the Proofs

** The decision

The Sol compiler and VM are written in OCaml. The verified checkers
of Decision 10 are written in Rocq and extracted to OCaml. Other
languages were considered and rejected for the kernel line; the
exploration appetite is spent above it: Rocq itself, Karuta on the
BEAM, and wire clients in any language.

** The argument

- P1 (Decision 4). Sol is a library that RNT links in-process, and
  RNT and Sakura are OCaml. A foreign runtime inside the kernel
  process reintroduces FFI seams exactly where atomicity and shared
  representation of content-addressed values matter most.
- P2 (Decision 10). The extraction pipeline is load-bearing: "the
  thing proven is the thing running." Rocq's mature extraction
  target is OCaml; Scheme extraction is unmaintained, and no
  extraction to Common Lisp exists.
- P3. The performance and correctness profile wanted here (native
  compilation, memory safety, strong static types) is OCaml's exact
  niche, and it is the lingua franca of compiler construction.
- C. OCaml for compiler and VM; Rocq with extraction for the
  verified core.

* Decision 14: No Application in Term Position

** The decision

A block =[Relation ...]= is a proposition, never a term. Nested
application as a value, as in =[Equal left: [Plus left: X right: 0]
right: X]=, is rejected from the language. Statements about the
results of relations are written flat, as membership:

#+BEGIN_SRC sol
[Plus left: X right: 0 result: X]
#+END_SRC

** The argument

- P1 (delimiter law). Each delimiter has exactly one role. An
  application that is a proposition in one position and a value in
  another reintroduces the position-dependent meaning the delimiter
  law exists to forbid.
- P2 (relations are not functions). Elaborating an application into
  a term requires knowing which attribute is "the" result, but a
  relation is a set of labeled tuples with no distinguished output;
  label symmetry and mode freedom are core doctrine. The sugar would
  smuggle function orientation into the semantics, and it is only
  coherent at modes where the relation happens to be single valued:
  a partial, mode-dependent elaboration hidden behind innocent
  syntax.
- P3 (the motivation dissolves). The nested form is a functional
  accent, not expressive power: =Equal(Plus(X, 0), X)= is exactly
  =Plus(X, 0, X)=, which is shorter and states the law as
  membership, which is what Sol says everything is.
- C. Applications are propositions, everywhere.

** The one honest future door

If ergonomic pressure ever genuinely demands nested applications,
they are admissible only as sugar over relations whose catalog
schema *declares* a principal result attribute and a single
valuedness capability at the relevant mode, with a published
elaboration (fresh variable plus flat conjunct). The privilege must
be explicit and queryable, never assumed from position. Until a real
program hurts without it, it is not built.

* Decision 15: Relation References Are a Term Kind, Written #Name

** The decision

A relation reference is a first-class ground value denoting a
relation by name, written with the Smalltalk symbol notation:

#+BEGIN_SRC sol
[Insert relation: #Person tuple: {name: "Ana" age: 12} before: S after: S2]
#+END_SRC

It is a new lexical kind, distinct from variables, strings, and
propositions. A reference denotes the *catalog entry* resolved at a
state, not an extension: two states where =Person= holds different
tuples share the reference. Wherever a relation must appear as data,
the reference is the value: transition arguments, higher-order
arguments (=[Map relation: #Increment ...]=), and the attributes of
the catalog relations themselves (decision 11).

** The alternatives rejected

- *Strings* (=relation: "Person"=): a conflation. The text and the
  relation are different things with different semantics; a string
  is inert, a reference resolves against a catalog at a state.
  Identity is not representation (decision 12's own diagnosis).
- *Context-resolved atoms* (=relation: Person= with the loader
  special-casing certain argument positions): position-dependent
  meaning of one spelling, the exact dishonesty the delimiter law
  forbids, over an open set of special positions.

** What it buys

- P1 (honesty). Different semantics get a visibly different form.
- P2 (decision 11). "You may only insert into a relation that
  exists" stops being transition machinery and becomes an ordinary
  foreign key into the catalog, checked at the =before:= state.
- P3 (higher-order, grounded). A reference variable ranges over the
  catalog, and the catalog is finite: an unbound relation variable
  is *bounded generation*, admissible like =Between=. The
  specification's higher-order restriction becomes ordinary
  cardinality analysis instead of a prohibition.

** Acknowledged costs

- A new lexical category through the whole pipeline: token, term
  and pattern kind, checker leaf, printing.
- The resolution semantics (reference = name resolved through the
  catalog of a state) must be respected by every world.

* Consequences for the Pending Documents

- =docs/core-design-and-pipeline.org= must treat transition relations
  as first-class in normalization, planning, and totality checking.
- =docs/virtual-machine-specification.org= must specify: the state
  value representation (content-addressed), the evaluation of
  transition relations, and the single commit primitive as the only
  effectful operation in the VM.
- Sol's DRL fragment must normalize to plans executable by RNT's FOL
  core (the =Plan.t= algebra: Scan, Project, Join, Union, Rename,
  Take, Materialize), with Sakura-style cardinality annotation.