ADR 0034 — logos-db is a theory-agnostic engine; theories attach per-judgment through one seam

Status: proposed
Date: 2026-07-01
Builds on: 0027 (the component-release is the unit — logos-db-seam and logos-db are independently-versioned components, and the per-lane roll now cuts them), 0016 (stele is the substrate service; here stele sheds its engine to a thin shell), 0030 (a theory judgment is decided once, providers realize — logos-db is the shared judgment engine those runtimes embed)
Relates: 0028 (thesmos's authority law is unchanged; logos-db carries none of it), 0029 (kosmos is a runtime over logos-db, not a second integration layer — pending kosmos confirmation, kosmos#97)
Grounded in: stele research-docs/0001 (the theory-seam / adapter-necessity study the split paused on), the maintainer's ratification (2026-07-01), and the cross-board design pass (stele · thesmos · horos · accounts CCAs + the atlas CCCA)

logos-db is a theory-AGNOSTIC, embeddable logic-database engine — the substrate's logos check/solve machinery plus the stateful store, carrying no theory vocabulary. It exposes SearchAndCertify(Query{Program, Profile, FactView, Goal}) and owns the drive loop + the generic bare→partitioned rebind internally. There is ONE theory model: every theory is a Program (its law/definitions as a logos program) + evidence rules + judgments, and every judgment is certified by logos check() — the universal spine. SearchAndCertify is just search-for-a-derivation → check(), so search is an optional front-end, not a different kind of theory. A theory engages two engine capabilities — FactView projection (value-store → fact-EDB) and the search drive-loop — opt-in, per judgment: horos v1 engages neither (structural recognition → check() only, no binding, zero engine dep); thesmos engages both. No theory is structurally different from another; does-it-project / does-it-search is a per-judgment dial, not a design fork. Type-safety is the FactView's configurable type layer — a typed-by-default projection plus an optional horos-authored shape schema verified by check(). ontos-codec stays ontos-owned (the frozen canonical value codec, ontos-codec-v1); bindings depend on it, never absorb it. Topologically logos-db is a new substance-tier member (deps ontos + logos) shipping a contract-only logos-db-seam + the logos-db engine; each theory adds a thin <theory>-db-binding lane in its own repo, only for the judgments that engage the engine; stele sheds its engine to become a service shell. Rollout is additive-first. This ratifies the frame, topology, and seam contract — not a wire format.

Context

The maintainer ratified (2026-07-01) extracting the substrate's logic engine out of stele into a standalone, embeddable, general-purpose library. Today stele is the engine: it embeds logos check/solve, wires thesmos's authorization law, and serves it. Every consumer that wants that machinery (accounts, kosmos) therefore couples to stele — a heavy dependency on a service for what is really a library concern. The goal: a consumer gets the engine by depending on a library, and its theory by depending on a thin, contract-only binding — never on stele.

The split was paused on a seam ruling (stele research-docs/0001, "theory-seam / adapter-necessity"): how tightly must a theory bind to the engine, and does each theory need a bespoke runtime adapter? The cross-board design pass — with a load-bearing observation from the horos CCA that horos is search-free by charter (it binds logos check(), never SearchAndCertify) — resolved it. This ADR ratifies the resulting frame + the topology and substrate wiring atlas owns; the seam contract it states is the single frame the paired ADR set freezes against.

The v0.4.0 substrate convergence is complete (stele#394, the last member; active release 2026.06.06-a31081b2e273), which opens the standup window this ADR sequences into.

Decision

1. One theory model — the seam (ratified frame)

Every theory = a Program + evidence rules + judgments. Every judgment is certified by logos check() — the universal spine; nothing decides without ending in a check. SearchAndCertify = search-for-a-derivation → check(): search is an optional front-end.

A theory engages two engine capabilities, opt-in per judgment (not per theory):

FactView projection — turn the value-store into the fact-EDB a derivation reasons over.
search drive-loop — find the derivation vs recognize it structurally.

	projects?	searches?	binding
horos v1 (wf(T), v:T over structural types)	no	no	none — `check()` over a structurally-recognized witness
horos + deferred S<:T (if it needs search)	yes	yes	a conditional `horos-db-binding`, that judgment only
thesmos (authorization: find a grant-chain)	yes	yes	`thesmos-db-binding` — the both-capabilities template

No theory is structurally different from another — only in which capabilities its judgments switch on. A new theory is a point on the same line: define Program + evidence + judgments; certify with check(); turn on projection/search only where a judgment needs it.

Type-safety is the FactView projection's configurable type layer: the projection is typed by default (each projected literal carries its ontos type — facts are never stringly-typed), and an optional horos-authored shape schema (well-formedness wf(T) + conformance v:T, both decided by check()) is the configurable enforcement layered on top. Schema supplied → type-safe; none → schema-less. horos is the canonical shape-provider, never a forced coupling. Coverage boundary (horos CCA seam-fit): horos's recognizer currently types 6 of ontos-data's 8 embeddings (int / utf8-text / bool / list / map / set — not decimal/null, horos#103), so a horos-typed FactView inherits that boundary: a decimal- or null-embedded projected literal is fail-closed (rejected or schema-less), never mistyped, until horos#103 (v2) decides decimal/null.

ontos-codec stays ontos-owned. It is the frozen canonical value byte-codec (ontos-codec-v1, "a side axis over core, not a higher semantic layer"; one of the three type-identity-critical components sharing the ontos go module). A binding depends on it for the value→bytes step of its projection; the theory-specific fact canonicalization (envelope/selection/ordering/dedup — what counts as "the same fact") lives in the binding and builds on ontos-codec. Depend, don't move.

2. Topology (atlas-owned)

logos-db — a new substance-tier member, dependsOn ontos + logos only. It ships two packages per language, following the logos-contract/logos-kernel precedent exactly:
- logos-db-seam — contract-only seam types (the logos-contract analogue): the Query/FactView/CheckProfile shapes a theory binds against. A theory deps the seam, never the engine runtime.
- logos-db — the engine (the logos-kernel analogue): the drive loop + bare→partitioned rebind + the store.
<theory>-db-binding is a lane in the theory's own repo (e.g. thesmos-db-binding in thesmos; deps <theory>-core + logos-db-seam, never the engine runtime), present only for judgments that engage projection/search. Anti-proliferation: one engine, N thin per-theory bindings; check-only theories (horos v1) need none. Future theories add their own lane — no new repos per theory.
stele drops from embeds-the-engine to a service shell — a consumer of logos-db + thesmos-db-binding. Its topology edges re-draw accordingly (regenerated with the constellation figure at standup).
Naming. logos-db / logos-db-seam / thesmos-db-binding are X-suffix infrastructure, not new Greek-concept primitives — consistent with the constellation naming rule (a new fundamental semantics earns a Greek name; infrastructure on an existing concept takes the <concept>-X form, cf. logos-bench).
Prerequisite: a design wordmark/mark must be minted for logos-db before the constellation figure can render it (the same gate horos hit at design#275).

3. Substrate wiring (atlas-owned)

logos-db enters the substrate as a component-release (0027); its seam and engine packages are independently versionable per language, which the roll already supports (the per-lane-version fix, atlas#698/#699 — source tag ≠ npm version).
Rollout is additive-first: consumers pin logos-db alongside raw ontos/logos, which stay the fleet floor. logos-db is the default surface; a raw-ontos direct pin is the documented exception (else rs/ts Value-identity splits — Go MVS unifies, rs/ts do not). "Becomes-the-floor" (consumers pin logos-db instead of raw ontos/logos) is an explicitly earned later step, not a day-one mandate.
The certify-only floor — a consumer that only needs check() over its own theory — depends on <theory>-core + logos-contract and no engine (accounts' tier-a posture is exactly this).

4. The paired ADR set + freeze gate

This ADR (topology + substrate wiring + the seam frame) is one of a coherent set that freezes against one seam definition — do not diverge per-repo:

topology/substrate-wiring — this ADR (atlas CCCA).
stele = logos-db service shell — stele anchor ADR (stele CCA).
thesmos-db-binding — the both-capabilities binding template; thesmos owns the binding conformance oracle (the byte-parity vectors: envelope/selection/projection/evidence/hints/ordering/dedup/rebind/check) (thesmos CCA, section signed) — pinned as thesmos ADR 0017 (Proposed, merged 2026-07-01; thesmos PR #245), which mirrors the locked seam ruling verbatim.
accounts-boundary — the consumer-boundary + tier-a floor (accounts CCA).

Freeze gate: kosmos#97 (async — kosmos ratifies the one engine-vs-runtime positioning paragraph) + thesmos CCA (signed) + accounts CCA. The horos CCA's core owner assesses the FactView-typed + deferred-S<:T seam-fit before freeze.

Consequences

Maximal theory alignment. Every theory is authored, reviewed, and wired identically; a binding is just "which optional capabilities this theory's judgments switch on." horos being search-free is not a special case — it is the zero-capability instance of the one model.
stele decouples. accounts/kosmos get authorization from logos-db + thesmos-db-binding with no stele dependency; stele shrinks to a shell.
General-purpose by design. logos-db carries no constellation/thesmos vocabulary and is usable outside Bitspark; type-safety is opt-in configuration, not a baked-in coupling.
Sequencing. Paper (this ADR + the set) proceeds now; the logos-db repo standup + the substrate re-homing land in the post-convergence window (now open — v0.4.0 closed at stele#394). The where-it-sits + constellation figures regenerate as part of standup (folds in the pre-existing atlas#687 figure staleness — no separate regen).
Not ratified here: the wire format / the concrete logos-db-seam type signatures (the horos CCA + core owner + thesmos's conformance-oracle spec fill those at standup), and the "becomes-the-floor" flip (a later, earned decision).

References

stele research-docs/0001 — theory-seam / adapter-necessity.
atlas#698/#699 — the per-lane-version roll (independently-versioned seam/engine).
kosmos#97 — kosmos engine-vs-runtime positioning (async freeze-gate leg).
0027 · 0016 · 0030 · 0029.