How a *read* client reaches a KB — directly in-process, or over the daemon HTTP API
(`vaelii.host.serve`).  It re-exports the slice of the `vaelii.core` read surface the
browser uses, so the browser is written once against these names and runs unchanged
against a local KB or a remote daemon.

A **target** is either a KB, read in-process, or an access value from `remote`.  A
KB-read op dispatches on it:

  :remote  → the client (`vaelii.host.client/call`) — one HTTP round-trip
  a KB     → `vaelii.core`, via `serve/ops` (the very allowlist the daemon serves, so
             local and remote answer through the same table and cannot drift)

The pure display fns (`term-role`, `reified-term?`, `readable-sentence`,
`indexable-terms`, `negative?`, `rests-on`, `query-contexts`, `assertable-strengths`,
`sort-by-content`, `levels`, `calculi`), the bootstrap fns (`open-kb`, `clear!`), the
in-process `write-hazards` and the process-wide `switch-value` take no target and
delegate to `vaelii.core`.  They are here so a caller can require this one namespace
and reach the whole surface it needs.

Reads — including `check` / `check-edit`, which answer what `assert` would refuse
and write nothing — plus the four writes the browser performs: `edit` (an
assert/retract batch in one settle), `edit-with-consequences` (the same batch, plus
the belief it moved), `forward-chain`, and `preview` (which stores nothing but applies
a batch and rolls it back, so it holds the single writer).  A remote result is already
EDN-clean (the daemon projects sentex records to maps); a local result is the raw
record, and both answer to the same keys, so a caller handles them identically.

What knowledge bases this process can load, and the lifecycle of loading one.

Everything above the engine assumes it is holding *the* KB.  A browser that lists the
KBs available, loads one while you watch, and switches to it needs two things the
engine does not have: a description of a KB that has not been loaded yet, and somewhere
for a load that takes minutes to run while the pages keep answering.  Those are the two
halves here.

**A source** is a KB you could load, as data — a kind, a name, and wherever the content
comes from.  Six kinds:

| kind         | content                                             | loader |
|--------------|-----------------------------------------------------|--------|
| `:core`      | the CxCore vocabulary head alone               | `vaelii.host.core-context` |
| `:starter`   | the shipped schema-only ontology                    | `vaelii.host.starter` |
| `:generated` | synthesized from numbers — types, rules, a fwd mix  | `vaelii.host.io.generate` |
| `:corpus`    | a translated sentence corpus (OpenCyc)              | a foreign reader, `:cyc-corpus` |
| `:dump`      | a vaelii export dump                                | `vaelii.impl.io.import` |
| `:store`     | an on-disk KB already in vaelii's own format        | opened in place |

The first three ship in this repo and are always offered.  The last three are **found**:
each directory on the search path (`VAELII_KB_PATH`, else `./kbs` and `~/.vaelii/kbs`)
is probed, and what marks it — a corpus `meta.edn`, a dump `meta.edn`, a `records/` +
`index/` pair — decides its kind.  A `catalog.edn` (`VAELII_KB_CATALOG`, else
`~/.vaelii/catalog.edn`) names sources outside the search path.  Nothing about a
machine's paths is baked into the repo.

**An entry** is a source that has been loaded, or is loading: a KB, a status, and a
progress reading the loaders report into (`:on-progress`, reported by every loader —
the corpus reader, `io.import/import-dump` and `io.generate/load-into`).  The running
half of that is not here: a load is a **job** (`vaelii.browser.jobs`), which is what gives
it a thread of its own, the progress reading, the cancel flag and the report — so an
entry carries the job's id and reads its status rather than keeping one.  One load runs
at a time, since a load claims this process's writer, and cancelling one is cooperative:
the loaders have no other safe interruption point, and an import is not a transaction,
so a cancelled load leaves the KB holding what had already landed.

**A KB is readable before it is finished.**  `activate` asks only that an entry hold a
KB, so the one arriving can be the one every page reads — a corpus is browsable from
its first thousand sentexes, and a store that opens in seconds is browsable while
belief is still being rebuilt behind it.  What that costs a reader is completeness, not
correctness, and `active-caveat` is what says so.

**And a KB can go back out.**  `export-entry!` writes a loaded one as an export dump as
a job like any other, which closes the loop: a dump written under the search path is a
`:dump` source the moment its `meta.edn` lands, so exporting and reloading needs nothing
outside this namespace.

**Unloading never deletes an on-disk KB.**  A memory-backed entry has its stores
cleared (they would otherwise hold the corpus for the life of the JVM); every other
backend is *closed* — the file lock released, the directory left exactly as it was, an
adapter's connection closed.  The same directory can then be loaded again, or opened by
another process.

Worked examples of the reasoning the shipped ontology actually does — the data, and
the one function that runs one.

**Nothing here is a story about the engine.**  Each example names the sentexes it
rests on, and those are looked up in the live KB before anything is claimed: an
example whose `rests-on` sentences are not stored is reported *unavailable* rather
than answered, so switching to another corpus greys the examples out instead of
silently showing a verdict computed from vocabulary that is not there.  The verdict
itself is an ordinary `ask` / `escalate` / `check`, and the proof is `why`.

Two kinds, and the split is about what the KB ships rather than about presentation:

  **read-only** — no premises.  The shipped schema is types, taxonomy, metadata and
  rules, so everything asked *of kinds* is answerable with no write at all, and the
  page computes it on render.  This is where the taxonomy, `transitiveInArg`,
  disjointness and the predicate meta-ontology live.

  **sandboxed** — premises naming individuals.  The starter ships no cast (the
  fables and their casts live in the test-world), so an example about defaults,
  joins or refusals has to bring its own, and it writes them into the reader's own
  sandbox context.  Nothing shipped can see in, and the sandbox reset takes the
  whole thing away.

`:expect` is what the ontology is supposed to answer, and `examples_test` asserts
every one of them — so the page cannot drift away from the KB it describes.

:running → :cancelling → :done | :cancelled | :failed

Long work, as jobs: one registry, one progress reading, one cancel.

Three things this process does take minutes rather than milliseconds — filling a KB
from a corpus, writing one back out, and joining every rule over everything stored.
Each of them wants the same four capabilities, and they are the only four: run on a
thread of its own so the pages keep answering, say where it has got to, stop when
asked, and leave a report somebody can read afterwards.  That shape is here once.

**A job** is `{:id :label :kind :status :progress :started :finished :error :summary
:result-url}`, plus a cancel flag and the future, which no view carries.  `submit`
returns the id; `job` reads one; `jobs` lists them, newest first.  The caller's `work`
is handed a `progress!` fn and nothing else: what it records shows up under
`:progress`, and what it *throws* is how cancellation lands, because a tight assert
loop has no other point at which stopping is safe.

**One status vocabulary**, whatever the job is doing:

    :running → :cancelling → :done | :cancelled | :failed

`:cancelling` is the state between the request and the stop: `cancel!` sets the flag and
returns, and the work keeps running until it reaches its next progress report — which,
for a phase that reports none (opening a large store scans its whole record log before
it says anything), can be a while.

**The single writer stays single.**  `:writes` names the KB a job writes, or `true` for
one it has not opened yet, and **one writing job runs at a time**: a second is refused
with a message naming the job that holds the writer.  Two interleaved writers are not
serializable (docs/storage.md, the single-writer contract), and a registry that let two
through would be a way around the contract rather than a place to watch it from.
`writes-kb?` is the other half of the same question, asked by identity, so a job filling
one KB is never a reason to refuse a write to another.  The browser's write monitor is
a separate thing: it is process-wide, and a chaining job holds it for its whole run, so
a write to any KB waits for the chain (docs/web.md).

**Cancellation is cooperative, and for a KB-writing job that is not negotiable.**  A
thread interrupt landing mid-cascade on a durable store surfaces as
`ClosedByInterruptException` and can leave a torn removal, so a job with `:writes` is
flagged and never interrupted however long it takes to notice.  A job that writes
nothing may say `:interruptible? true` and be cancelled the hard way as well; the
registry checks both, so the two can never be confused for one another.  A job's thread
is the *pool's* once its body has unwound, so the hard tier is fenced: the body
publishes `:released` under the job's `:monitor` and `cancel!` re-reads it there, which
is what stops an interrupt aimed at a job that has already finished from landing on
whatever the pool runs next.

**A finished job's report outlives the job**, for an hour — long enough to read what it
did, since the page that would have shown it is usually the page you navigated away
from.  The registry holds the newest `max-settled-jobs` settled reports at most, so a
caller submitting no-op jobs holds a bounded number of them.  Nothing *unsettled* is ever dropped, at any age: forgetting a job is releasing
its writer claim, and a thread that is still running is still writing.  So a wedged job
keeps its place and keeps counting towards the running badge, which is the truth about
the process — better than a store two writers took turns on.

The development browser's source reloader, which only `scripts/start-vaelii-dev.sh`
turns on (`vaelii.browser.web/dev-repl`).  Before each request it reloads every watched
source file that changed since the last request, together with every loaded namespace
that requires one of them, transitively, in dependency order.

**A protocol, record, type or interface is never redefined.**  Re-evaluating a
`defprotocol` defines a new interface and empties the protocol's extension map, and
re-evaluating a `defrecord`, `deftype` or `definterface` defines a new class, so a KB
loaded before the reload would hold values the reloaded code no longer recognizes.  A
reload therefore loads a file form by form and leaves out each of those forms whose
protocol or class already exists; every other form is evaluated.  A record keeps its
methods inline, where protocol dispatch is a direct interface call, and a method that
calls a function reaches the reloaded function through its var.  An edit inside such a
form is not loaded: `restart-owed` names it until the process restarts, and the page
shows that list.  A form for a class that does not exist yet is evaluated.

**A held namespace is never re-evaluated at all.**  A namespace whose ns symbol carries
`:clojure.tools.namespace.repl/load false` holds protocols and method-less records
(`vaelii.impl.types.*`, `vaelii.impl.protocols`, …).  An edit to one reloads nothing on
its account, and `restart-owed` names it.

**Form by form, not tools.namespace's `refresh`.**  `refresh` removes each namespace with
`remove-ns` before it loads the file again, which re-evaluates every `defonce` in it and
empties the state a loaded KB keeps there: the cache registry, the change feed's
listeners, the thaw guard's installed readers.  Loading into the existing namespace
keeps a `defonce`'s value, as `require :reload` does.

**Only loaded namespaces reload.**  A dependent this process never loaded stays
unloaded: loading it would run code the
running server does not use.

tools.namespace ships in the `:dev` profile only, so its dependency graph and ns-form
reader are resolved when `wrap-reload` builds the reloader, never at this namespace's
load.  The standalone jar compiles this namespace and has no tools.namespace.

Somewhere safe to be wrong.

A **sandbox** is a scratch context of one browser session's own, hung below
`CxWell` so it sees what CxWell sees (every shipped context but the opt-in theories,
the `kb/middle/` files that state no `genlCx` edge from CxWell) and nothing shipped
sees it.  A
reader can therefore use every type, every relation and every rule the KB ships, and
cannot damage any of them: their content is visible only from inside, and one control
takes all of it away again.

Why that shape and not a permission system: visibility here is *logical*, not
administrative.  `genlCx` already decides what a context can see, and hanging the
sandbox at the bottom of the spindle gives exactly the asymmetry wanted — everything
flows in, nothing flows out — with no new concept and nothing to enforce.  A shipped
rule firing over sandbox facts places its conclusion **in the sandbox**, because
placement is the maximal common descendant of the rule's context and the antecedents'
(docs/contexts.md), and the sandbox is the only context below both.  So the derived
content is inside the thing that gets discarded, without anything arranging for that.

Four facts about the lifecycle:

- **The context is created on the first write, not on the first page.**  A reader who
  only looks costs the KB nothing, and a KB full of empty sandboxes would be a KB with
  a `genlCx` edge per idle visitor.
- **The server mints the session token and tags it.**  The cookie carries the token and
  an HMAC of it under a key fixed at start, and a cookie whose tag does not check is
  replaced with a fresh one, so a client cannot choose a sandbox.  The context name
  carries a digest of the token rather than the token, because every reader sees every
  context's name (`/find`, `CxWell`'s term page, `/op :contexts`).
- **A process keeps at most `max-sandboxes` per KB.**  Opening one more resets the
  lowest-priority sandbox on the roster below (docs/web.md).
- **Reset is a real teardown**, not a flag: every sentex in the extent goes through
  `edit`'s `:remove`, and the `genlCx` edge with them.  The edge is not in the
  extent — `genlCx` is a forced-decontextualized predicate, so it is stored in
  `CxUniverse` — which is why it is fetched by hand rather than swept up with the
  rest.

Promotion — moving something out of a sandbox into a context that outlives it — is
deliberately not here.  A sandbox is a dead end, and a dead end that cannot be
half-escaped is easier to reason about than one with an entry point in it.

The inline-SVG primitives the term page's concept graph is drawn with: a node, an
edge, an arrowhead, and the arithmetic that lays out a row, a column or a ring.

**No graph library.**  The browser ships two JavaScript files and this adds none — a
layout that is a fold over a row of boxes is a dozen lines, and a dependency that drew
it would be the largest thing the client loads.  Nor a shell-out: a page that renders
by starting a process is a page that cannot be served.

Everything here is **pure** — no KB, no access facade, no belief — so it is tested on
hand-built maps.  What a node *means* is the caller's: it supplies the term, the
colour class, the link and the tooltip, and this decides only where the box goes and
what shape it is.

Coordinates live in one flat user space and may be negative; `scene` crops the
`viewBox` to the union of what was actually drawn, so a sparse graph is centred rather
than adrift in a fixed canvas and a long snake_case label is never clipped.  Every
number reaching an attribute is a **long**: Clojure's `/` yields a ratio, and `1/2` in
an SVG attribute is not a coordinate.

A small reitit-ring web browser over a KB:

  /                 the upper ontology (contexts, types, core predicates, disjointness)
  /stats            KB-wide counts, contexts by size, and the reasoning-health ledgers
  /find?q=<pattern> the terms whose name matches, from the index's term roster
  /term?q=<term>    every sentex containing the term, grouped by the index root that
                    reaches it (functor / argument-position / context / term-index)
  /sentex/:id       a sentex (literal or rule): its belief state (IN, or the why-not
                    reason — superseded / defeated / unsupported), supports, dependents
  /justification/:id    a justification: its supports (arguments) and dependent sentex
  /levels?q=<goal>  the lookup-to-query stack: what each of the 8 levels answers
  /edit             the multi-sentex editor (GET seeds it, POST saves) — a fragment
  /{term,find,levels}/rows   one more page of a capped list, as bare rows

Run it with `lein run -m vaelii.browser.web` (serves a starter-loaded KB on :3000).
Handlers are pure `request -> response`, so they are testable without a server.

Every page is answered twice over: as a whole document, and — when htmx asks, which
is every navigation and search — as the `#main` fragment that actually lands.  What a
page costs in KB reads is part of what this demonstrates, since the browser reads the
public surface alone and each read is a round-trip under `--attach`; see the `view`
section below and docs/web.md.

Drive a KB from the shell: assert, match, query, and an interactive REPL.

Public because it is a documented entry point — `lein cli`, or
`lein run -m vaelii.cli`.  The implementation is `vaelii.host.cli`, which is free to
change.

A thin EDN-over-HTTP client for the vaelii daemon (`vaelii.serve`).  Runs no engine:
it POSTs `{:op :args}` and reads the result back, over JDK `java.net.http` (no
dependency — JDK 21 ships it).

Every call threads an **explicit connection handle** as its first argument —
`(query conn '(dog ?x) 'Ctx)` — the network mirror of `vaelii.core`'s explicit-`kb`
API.  A `conn` from `client` holds a reusable `HttpClient`; no socket opens until a
call.  A daemon reply of `{:ok false}` becomes an `ex-info` carrying the daemon's
`:error`, `:type` and `:status`, so a remote naming or disjointness refusal surfaces
like a local one and the HTTP status under it is readable without writing the request
by hand.

A daemon with `VAELII_API_TOKEN` set answers 401 (`:unauthorized`) to a call that
presents no bearer token; the `conn` reads the same variable, so a client in the
daemon's environment carries it with nothing said.

Public because a client is a thing applications write against; the implementation is
`vaelii.host.client`, which is free to change.  Result shapes are `vaelii.core`'s: a
sentex comes back as a plain map (the daemon projects the record), a solution as a
binding map.

**Every op the daemon serves has a wrapper here**, spelled as `vaelii.core` spells the
fn — bare or `!`-marked exactly as it does — and at its arities, with `kb` replaced by
`conn`.  The ones below are written out; the rest are generated from the daemon's op
table by `lein regen-client`, which is also what makes the claim checkable rather than
aspirational (`client_surface_test`).  `call` still reaches any op directly, which is
what a caller wants for `serve/feed-ops` and for an op newer than this build.

Vaelii — a contextualized common-sense knowledge base.

A KB bundles a record store (the durable ground truth), an index store (derived
from it, rebuildable), a JTMS, and a taxonomy (cached genl / genlCx closures).
The unit of knowledge is a *sentex*: a sentence plus the context it holds in.
Rules are sentexes too.

Public API: `open-kb`, `assert`, `assert-rule`, `forward-chain`, `query`,
`sentexes-matching`, `ask`, `prove`, `retract!`, `why`, `in?`, `isa?`.  This is a
signpost, not the roster — docs/api.md is that, and its "Choosing a query
function" table is what separates the five ways to answer a goal.

This namespace is the engine's whole API; the engine itself lives in layered
`vaelii.impl.*` namespaces (kb <- checks <- special <- integrate <- chain <-
settle) and everything here is either a delegation into that stack or the
`assert` / `retract!` / `recover` orchestration that spans it.

Five entry points are public beside it, each a thin shim over the same stack:
`vaelii.client` (the network client), `vaelii.starter` (the bundled ontology),
and `vaelii.web` / `vaelii.serve` / `vaelii.cli` (the browser, the daemon, the
command line).  Those six namespaces are the compatibility boundary — everything
under `vaelii.impl.*` is free to change without notice.

A command-line driver for a KB — the shell dual of the in-process API, launched with
`lein run -m vaelii.host.cli <cmd> <args…>`.  It runs the engine in-process (no
daemon); to talk to a running daemon use `vaelii.host.client` instead.

  lein run -m vaelii.host.cli assert  '(dog Muffet)'  CxNaturalWorld --dir /tmp/kb
  lein run -m vaelii.host.cli query   '(dog ?x)'    CxNaturalWorld --dir /tmp/kb
  lein run -m vaelii.host.cli why     3                                 --dir /tmp/kb
  lein run -m vaelii.host.cli export  /tmp/dump                         --dir /tmp/kb
  lein run -m vaelii.host.cli repl --starter          # interactive, starter schema
  lein cli help                                      # every command and what it takes

`help` is a word rather than only a flag because Leiningen answers `lein cli --help`
itself, printing the alias expansion — the flag never reaches this namespace through
the alias, though it does through the full `lein run -m vaelii.host.cli --help`.

**Backend.**  `--dir <path>` opens the store there under the backend its files were
written by (`v/store-backend`), or a new durable `:disk-log` store when it holds none —
recovered on open, so a fact asserted in one invocation is there in the next.  A `--dir`
whose parent does not exist is refused (`open-kb-from`) rather than created.
`upgrade` opens a store, brings its reasoning image and index image up to this build, and
closes it (`upgrade!`); `--verify` recovers anyway and compares the two images.
With no `--dir` the KB is
in-memory and lives only for the process — useful for `repl` or a single compound
session, pointless across one-shot commands.  `--starter` loads the shipped schema
(types, contexts, relation rules) so you can explore the ontology.  `--strength
monotonic` marks an `assert` or `assert-rule` known-true.  `export` takes `--variant
records|records+index` and `--compression gzip|xz|none`.

**A flag belongs to the commands that read it** (`command-flags`), and one carried by
a command that does not is refused rather than dropped — those three are the driver's
and go anywhere, the rest do not.  A *value* it cannot honour is refused on the same
argument: `--format texr` and `--depth twice` name nothing.

**stdout is the answer.**  `err!` keeps a refusal off it, and `on-stderr` keeps the
engine's own log lines off it too — Trove's console backend prints to `*out*`, which
here is what a script redirects.  A refusal is one stderr line, `error: [<:type>]
<message>` (`refusal-line`), so a script branches on the keyword and not on the prose.

**One writer.**  A `--dir` KB takes the single-writer file lock (docs/storage.md), so
the CLI and a daemon cannot own the same directory at once — by design.  `diff` and
`upgrade` open no KB of the run's (`without-a-kb`), so `diff` answers beside a daemon
that holds `--dir`.

A thin EDN-over-HTTP client for the vaelii daemon (`vaelii.host.serve`).  Runs no
engine: it POSTs `{:op :args}` and reads the result back, over JDK `java.net.http`
(no dependency — JDK 21 ships it).

Every call threads an **explicit connection handle** as its first argument —
`(query conn '(dog ?x) 'Ctx)` — the network mirror of `vaelii.core`'s explicit-`kb`
API.  A `conn` from `client` holds a reusable `HttpClient`; no socket opens until a
call.  A daemon reply of `{:ok false}` becomes an `ex-info` carrying the daemon's
`:error`, `:type` and `:status`, so a remote naming/disjointness refusal surfaces like
a local one and the coarse client-fault/server-fault split the status carries is
readable without writing the request by hand.

**The bearer token rides on the request the daemon requires it on**: the `conn`
carries it (`VAELII_API_TOKEN` unless `:token` says otherwise) and every call sets one
more header on the builder it was already using.  No dependency, no client state, and
the `conn` is still a map you can read.

**One wrapper per op, and they are generated** (`vaelii.regen-client`, `lein
regen-client`).  The daemon's op table is the single source — an op is a `vaelii.core`
fn with the KB supplied — so a wrapper here is that fn's own spelling, bare or
`!`-marked exactly as `vaelii.core` spells it, at its own arities with `kb` replaced by
`conn`.  It is generated at *build* time rather than macroexpanded from `serve/ops`,
because requiring the table would pull the engine, jetty and reitit onto the classpath
of a namespace whose whole point is not needing them.  `client_surface_test` compares
this file against what the generator would write now, so an op added to the daemon
fails the suite until the wrapper is written.

The CxCore ontology — Vaelii's vocabulary context.  It defines and
documents the core predicates the engine interprets, as sentexes in CxCore:
the special-predicate surface (types/contexts, arg, disjoint, the `set/*Rule`
wrappers, the predicate metadata, negation, `ist`, the evaluables) and the
predicate meta-ontology.  Documentation rides on `comment` sentexes,
`(comment <term> "...")` — ordinary sentexes (stored, indexed, queryable) — so the
KB documents itself in its own representation.

The content is a KB file, `resources/kb/CxCore.txt` (read by
vaelii.host.seed); this namespace loads it and reads the docs back.

CxCore is the spindle **head**: the root every context sees, and the only
layer a core-only KB has.  The layers below it — the definitional `upper`
contexts (between Core and Universe) and the theory `middle` contexts (between
Universe and Well) — are the starter's, not the core KB's, and each wires itself
into the spindle in its own KB file (see vaelii.host.starter).

(comment eats "(eats ?animal ?food) means that ?animal takes ?food as nourishment. …")
(comment genl "(genl ?subtype ?supertype) means that every ?subtype is a ?supertype. …")

A sentence in English, **composed** from what the KB already says about its own
vocabulary rather than generated.

The read path is the one with no verifier.  Nothing in the engine can say that an
English sentence describing `(genl penguin bird)` is wrong, so a fluent gloss is a way
to teach a reader something false through their only window onto the formal content —
which makes reading the more dangerous direction here, not the safer one.  The defence
is to not write prose at all where the KB has already written it.

## The comment is the template

The vocabulary documents itself: every shipped predicate carries a `comment` sentex,
and those comments are written in a shape that is already a template —

    (comment eats "(eats ?animal ?food) means that ?animal takes ?food as nourishment. …")
    (comment genl "(genl ?subtype ?supertype) means that every ?subtype is a ?supertype. …")

a **signature** naming the argument positions with variables, then a clause saying what
the predicate means *in those names*.  So glossing `(eats Muffet kibble)` is not a
generation problem: read `eats`'s comment, take its first clause, substitute the actual
arguments for the signature's variables.

The variables are why it reads: a parameter spelled `?animal` cannot be mistaken for an
individual the way `Animal` can, and because the *name* carries the sort, the clause
after it needs no sortal noun to lean on — so what substitutes is the sentence a reader
wants rather than one with `place Paris` in it.  Everything past that first clause is
documentation for a reader, not template: how the predicate is used, what it is not,
and what the KB does with it.

A signature written with plain capitalized words and a colon — `(eats Animal Food):
Animal eats Food` — is read the same way, since an imported vocabulary spells its own
comments and they are not ours to rewrite.

This is why the composer is a lookup and a substitution rather than a table of
hand-written patterns: adding a predicate with a documented signature gives it a gloss
for free, and a comment edited to say something else changes the gloss with it.  Of the
328 shipped comments, 210 carry a signature; the 118 that do not are nouns — 100 types
and 18 individuals (the units, the dimensions, the three signs) — which need none,
because a type gloss is "X is a dog" and the comment is the apposition after it.

What the composition rate does **not** measure is whether a gloss is worth reading.  It
helps a reader where the predicate name is opaque — `genl` glossed as "Every dog is an
animal" teaches a reader what `genl` means — and adds nothing where the predicate is
already an English verb.

## What it will not do

A term with no comment **degrades to naming the term**.  It does not invent a
description, because an invented description is exactly the failure this exists to
prevent, and a reader who sees the bare name has lost nothing they were entitled to.
Every result carries `:source` saying which it got:

  :composed   every literal came from a comment
  :partial    some did; the rest are named
  :named      nothing to compose from — the terms, in a frame

The formal sentence is never replaced by the gloss — that is the caller's contract, and
`docs/web.md` states it for the browser.

The HTTP guards both servers hold to — `vaelii.browser.web` (the browser) and
`vaelii.host.serve` (the daemon).

The browser authenticates nobody and the daemon only when a token is set
(`api-token`), and both bind loopback for that reason.  Loopback is what makes the
checks here necessary rather than sufficient: a browser running on the same machine
*is* a local client, so "only this machine may reach it" does not mean "only this
machine's owner may drive it".  Two attacks follow from that, and each guard below
closes one.

**Cross-site request forgery.**  Any page the operator visits can `fetch` a loopback
URL.  `same-origin?` rejects the write whenever the browser stamps `Origin`.
`edn-body?` closes the case where it does not: `application/edn` is not a
CORS-*simple* content type, so a browser must preflight it, and a server answering
no CORS headers fails that preflight before the request is ever sent.

**DNS rebinding.**  `same-origin?` compares `Origin` against the request's own
`Host`, so an attacker controlling both — a domain that re-resolves to 127.0.0.1
once the page is loaded — satisfies it.  `host-allowed?` is the check that does not
fold, because the `Host` header must then name the interface the server was actually
started on.

Synthesize a knowledge base of a chosen **shape**.

The two other kinds of KB are given: a shipped ontology (`vaelii.host.starter`) is
fixed content, and an imported corpus (`vaelii.impl.io.import`, or a translated one)
is whatever the source says.  Neither lets you ask *what happens at ten times the
rules*, and that is the question a scale or behaviour measurement is made of.  So this
namespace generates a KB from a handful of numbers — how many types, individuals,
predicates, facts and rules, how the rules split forward/backward, how many of them are
defeasible — and each number is a knob the browser renders as a slider (`knobs`).

Two properties make a generated KB usable as a measurement rather than as noise:

* **Deterministic.**  Each of `plan`'s three draw streams owns a `java.util.Random`
  seeded from the plan seed and its own constant (`stream-seeds`), so the same
  parameters give the same KB whichever order a reader realizes the streams in — a
  shape can be reproduced from the numbers alone, and a run compared against a rerun.
* **Stratified.**  Predicates are split into layers: facts populate layer 0, and a rule
  concluding a layer-k predicate draws its antecedents only from layers below k.  The
  rule set is therefore acyclic, so forward chaining cascades base → derived →
  further-derived and terminates, instead of the runaway recursion a rule set wired at
  random produces.  Individuals and predicates are Zipf-sampled, so the corpus has hot
  terms and a long tail like a real one rather than a uniform smear.

`plan` is pure — the whole KB as data, nothing asserted.  `load-into` asserts it,
reporting progress through an optional `:on-progress` callback (which may throw to
cancel the load, the flag `vaelii.browser.catalog` cancels on).

The browser editor's line format: a stored sentex as the sentence its author would
type back in.

The editor seeds its textarea with these sentences and diffs the text it gets back
against them **by content**, so a sentence spelled two ways would turn an untouched line
into a retract plus an assert of the same fact.  It lives here rather than in the
browser because spelling a rule's wrappers reads the rule record's slots
(`rules/rewrap-sentex`), and the browser requires no `vaelii.impl` namespace.

kb/CxCore.txt        the vocabulary head (see vaelii.host.core-context)
kb/upper/<C>.txt          definitional layers, between Core and Universe
kb/middle/<C>.txt         theory layers, between Universe and Well

Ontology KB files: declarative content held as **plain text on the classpath**
rather than as code.

A KB file is a list of ordinary vaelii sentences — one s-expression each, with
`;;` line comments and blank lines allowed — named for the context its sentences
assert into, and grouped **term-centrically**: every sentence about a vocabulary
term sits together, and the terms run in natural sort order.  A rule is just a
sentence carrying an `implies` / `set/*Rule` / `exceptWhen` wrapper.

**The format itself — reader and writer both — is `vaelii.impl.io.text`**, which is
where its one non-sentence spelling lives (`(set/monotonic S)`, the known-true class)
and what `vaelii.core/export-text!` writes.  What is here is the *classpath* side: the
shallow tree under `resources/kb/` and how a layer's files are discovered in it.

The files live under `resources/kb/`, in a shallow tree that mirrors the context
spindle:

    kb/CxCore.txt        the vocabulary head (see vaelii.host.core-context)
    kb/upper/<C>.txt          definitional layers, between Core and Universe
    kb/middle/<C>.txt         theory layers, between Universe and Well

The file *name* is the context; the sub-directory is the layer.  Only the layer a
caller names is discovered, so a sibling directory under `kb/` that names no layer here
is not loaded: `kb/koinii/` is one, an application's own context files, which that
application loads for itself.  What stays in
**code** (vaelii.host.starter) is the *order* the files load in and the handful of
genuinely computed assertions.  Sentences read with `clojure.edn`, so a KB file is
data and can never run code.

Headless EDN-over-HTTP daemon: one JVM owns one KB and serves it to remote clients
(`vaelii.host.client`).  A thin reitit-ring + jetty layer over `vaelii.core`, the
network dual of the in-process API.

**Wire format is EDN.**  A sentence is a symbol s-expression — `(dog Muffet)`, `?x`,
`(genl dog animal)` — which EDN round-trips losslessly; JSON would mangle the symbols.
The body of every call is `{:op <keyword> :args [...]}`, and the reply is
`{:ok true :result …}` or `{:ok false :error "…"}`.  EDN is read with
`clojure.edn/read-string` (never `clojure.core/read-string`), so an untrusted body
cannot evaluate code — EDN has no reader-eval.

**A refusal's `:type` is a plain keyword** — `:body-too-large`, `:not-edn`,
`:cross-origin`, `:bad-host` — and so is the `:type` an engine `ex-info` carries
through.  The protocol is what a client written against another build discriminates
on, so it cannot be qualified by the namespace that happens to serve it: a
`::`-qualified keyword names *this* namespace, and a client matching on it would be
matching on where the daemon's code lives.

**The daemon is the single writer** (docs/storage.md, the single-writer contract): it
owns the one process allowed to mutate the store, so it serializes every op through
one monitor.  Concurrent client writes therefore apply one at a time and cannot
interleave; reads pay the same lock, which is conservative but keeps the contract
simple.

**Only the allowlisted ops are reachable** (`ops`).  Each is a `vaelii.core` fn with
the KB supplied by the daemon — the client sends only the op and the remaining args —
so no client can reach an arbitrary var.  Sentex records in a result are projected to
plain maps before they hit the wire (the `sentex`-map contract), so the client reads
them back without the `impl` record class.

**The change feed is the one thing that is not a `vaelii.core` fn** (`feed-ops`), and
it is a table of its own for that reason: `core/watch` takes a callback, so what a
remote caller holds open instead is a subscription with a **cursor** — `:watch`,
`:poll`, `:unwatch`, `:watchers`, over the per-handler registry `app` builds
(`vaelii.host.subscribe`, docs/feed.md).  A `:poll` that waits runs **outside** the
monitor; everything else about them is an ordinary EDN op.

**One shared bearer token authenticates the caller.**  With `VAELII_API_TOKEN` set
(`guard/api-token`), every request presents `Authorization: Bearer <token>` or is
answered 401 with a `WWW-Authenticate: Bearer` challenge; `GET /health` is the one
route that answers without it.  One token for the process, not a session and not an
identity — per-caller identity is a reverse proxy's job, and this is the check that
has to exist below it.  Binding anything but loopback **requires** a token (`-main`
refuses to start otherwise); on the loopback default it is optional, and a daemon
without one is drivable by every process on the machine.

`vaelii.host.guard` covers what a token does not, and matters most on the open
loopback daemon: `POST /op` requires `Content-Type: application/edn`, refuses a
cross-origin `Origin`, and answers only to a `Host` naming the interface it was
started on.  Together those stop a page the operator happens to visit from driving
the KB over loopback — which binding to loopback alone does not.

Bring a KB's shipped spindle up to the running engine's.

A KB stores the starter ontology it was built with, and the engine that opens it later
ships its own: a strength marked `set/monotonic`, a vocabulary term added to CxCore, a
disjointness the ontology stopped stating.  `sync-spindle!` makes the KB state what this
engine ships, context by context, and leaves everything else alone.

**What is shipped** is what `starter/load-into` produces, read off a scratch in-memory KB
it is loaded into — not the text of the files.  The two differ: `genlCx` edges are stored
in CxUniverse whichever file states them, and the closing `unary_predicate` batch is
stated by no file.  Each premise is attributed to the file whose load stored it.

**Which contexts are synced exactly**: CxCore and the `kb/upper/` and `kb/middle/`
contexts.  These are the engine's, so a premise there that the engine does not ship is
retracted, a strength that differs is restated, and a missing one is asserted.  A
context an author adds to the spindle — wired between CxCore and CxUniverse, say — is
not one of them and is not read.

**Which are only added to**: the collectors (`kb/` root files, CxUniverse today) and any
other context a shipped file's content is stored in.  A collector gathers what the
engine routes there from every context, so what it holds beyond the shipped content is
not the engine's to retract.

**Only the layers a KB has.**  A file whose context holds nothing in the KB is not
loaded into it, and the collector files and the `unary_predicate` batch follow the upper
layer: a core-only KB stays core-only.

Comparison is by the form a KB file writes (`text/premise-entries`): a fact or rule
under its strength wrapper, an `exceptWhen` as the wrapper it was asserted as.  A
strength the engine **raised** is only an assertion, since `assert` raises a held
premise's strength in place; one it **lowered** is the form retracted and the weaker one
asserted, since nothing lowers a strength in place.

**One batch.**  The sync is one `v/edit!`: the additions first, then the retractions,
one settle.  So the belief a retraction would sweep and the addition rebuild keeps its
witness through the batch, where retracting first tore the TMS down only to build it
back up.  What cannot go in that order — a retraction of a record an addition lands on —
goes before it (`sync-spindle!`).

A starter common-sense KB: a documented, **schema-only** upper + middle ontology.
It loads the CxCore vocabulary (vaelii.host.core-context), then the starter's own
contexts, each a KB file on the classpath under resources/kb/:

  * upper (definitional — between Core and Universe): what things *are*, always
    true, like `genl`.  Split by domain, one context each:
      - CxAbstract.txt — the abstract type skeleton (physical/intangible and
                              their kinds) + the structural relations partOf/locatedIn.
      - CxOrganism.txt — the biological taxonomy + its disjointness.
      - CxLife.txt     — the organism relations (parentOf, siblingOf, flies,
                              mortal, birthYearOf, olderThan, …) with arg + metadata.
      - CxSociety.txt  — the social relations (marriedTo, likes, owns).
      - CxMeasure.txt  — the theory of measurement: the two measure terms, the
                              dimensionOf/conversionFactor table with the units that
                              fill it, the comparisons, weightOf / heightOf, and the
                              sign vocabulary for the quantities nobody has a figure
                              for (signOf / trendOf / the qualitative* arithmetic).
      - CxReflection.txt — the expression lattice (atomic and non-atomic, open and
                              closed, well-formed and ill-formed expressions) and the
                              use/mention vocabulary (proposition, means, denotes,
                              expresses).
      - CxSpace.txt    — qualitative space, four independent calculi: RCC-8
                              topology (eight base + six derived), cardinal direction
                              (nine + four), relative direction over a frame's own axes
                              (nine + four, the frame being the context), and
                              qualitative distance (seven + three).
      - CxTime.txt     — qualitative time: Allen's interval relations (thirteen
                              base + seven derived), the point algebra over instants,
                              the three calendar constructors and the InstantFn moment
                              a calendar term's startOf and endOf are computed as, plus
                              the length / totalDuration / overlapDuration vocabulary
                              the arithmetic computes over.
  * middle (theory — between Universe and Well): how the definitional things
    *interrelate*, where several overlapping theories can coexist.
      - CxAnatomy.txt   — what kinds of thing have what kinds of part.
      - CxBiology.txt   — birds fly by default except penguins; organisms
                               are mortal; flight enables travel; sleep is what the
                               theory is willing to assume.
      - CxChange.txt    — a simple event calculus: a state persists until an
                               event ends it, so holdsAt is inertia over what
                               initiates and terminates say.
      - CxComputing.txt — relations over software tools, their invocations and
                               receipts, media resources and DNS names, and
                               the kinds the relations are typed over.
                               Opt-in: it sees CxUniverse and CxWell does not
                               see it.
      - CxKinship.txt   — grandparentOf, ancestorOf, olderThan, and parenthood
                               from maternity and paternity.
      - CxMereology.txt — a part is located where its whole is; owning a whole
                               entails owning its parts.
      - CxNormalPhysicalConditions.txt — the states of matter at room temperature
                               and pressure: stone, wood and glass are solid,
                               mercury is liquid, a metal is solid by default.
                               Opt-in: it sees CxUniverse and CxWell does not
                               see it.
      - CxPerception.txt — perception relations: perceives, sees, seeImage,
                               watchVideo. Opt-in: it sees CxUniverse and CxWell
                               does not see it.
      - CxSize.txt      — comparative size: stated between kinds, computed
                               between objects from their measures.
      - CxSocial.txt    — what acquaintance follows from; employment as one way
                               of belonging; the general relationship and
                               dwelling vocabulary over two persons.
      - CxSocialExtension.txt — relationship and plural-identity vocabulary
                               narrower than CxSocial's own. Opt-in: it sees
                               CxSocial and CxWell does not see it. The
                               Extension suffix names a theory that extends
                               an existing starter theory with vocabulary
                               most contexts under the base theory have no
                               occasion to see.

A spindle is three layers — a head every member sees, members that see the head and
not each other, and a collector that sees every member — and the topology is two of
them stacked, most general (top) to most specific (bottom): CxCore heads the
upper spindle, whose members are `kb/upper/` and whose collector is CxUniverse, and
CxUniverse heads the middle spindle, whose members are `kb/middle/` and whose
collector is CxWell.  Each member file wires itself to its own head and collector, so
the topology is data.  **No cast and no contingent facts ship**: the starter is a schema, and
contingent data (a cast, worked examples, the Aesop fables) belongs below CxWell
and lives in the tests that need it.

The unit table is the one place individuals ship, and it applies that rule rather
than excepting itself from it: a minute is sixty seconds by stipulation, so the
factor is vocabulary and not a measurement anybody took.  CxMeasure.txt states
the test it holds a unit to.

What stays in code here is the *order the layers* load in — loading order is logic,
the definitional layer must precede the theories that reason over it — and the one
computed batch (every type is also a unary_predicate).  Within a layer, every
context file present is loaded (discovered from the classpath), so adding a KB is
dropping a file in kb/upper/ or kb/middle/, no code change.  `seed/root-contexts`
discovers the top-level collector files (`kb/Cx<Name>.txt` other than `CxCore.txt`,
today `CxUniverse.txt`) from the classpath as well.

The change feed with a **cursor** where the in-process one has a callback — the
daemon-side state a remote caller holds a feed open against.

`core/watch` takes a function, and a function does not cross an EDN wire (the same
wall `:export`'s `:on-progress` hits).  So the wire's half of the feed is not the
callback marshalled somehow; it is the one thing a request/response protocol can
carry, which is **state with a cursor**: the daemon registers an ordinary listener of
its own, that listener files each event into a bounded ring, and a caller reads the
ring forward from where it left off.  Three ops — register, read, drop — every one of
them EDN in and EDN out, so the guards, the client and the error taxonomy that already
exist carry it unchanged (docs/operations.md).

**A cursor counts events, not handles.**  It starts at 0 when the subscription is
registered and advances by one per delivered event, so a caller compares nothing and
stores one integer.  `poll` answers the events past the cursor it was handed and the
cursor to send next time.

**The ring is bounded, and falling off it is said out loud.**  A subscriber that stops
reading must not grow the daemon's heap, so the ring keeps `max-events` and drops the
oldest past it — and the *count* of what it dropped is reported as `:lagged` on the
next poll.  That number is the whole reason this is usable: a feed with a silent gap
is strictly worse than polling, because the caller believes it is current and is not.
`:lagged` is present on every reply, zero and all, so a client that forgets to read it
is a client that cannot have one.

**A token that names no subscription is refused, never answered empty.**  The same
argument: a reaped, dropped or invented token answering `{:events []}` is a feed that
has silently stopped.  `:unknown-subscription` says so.

**What a subscription costs the daemon, and what bounds it.**  One listener on the
KB's feed and one ring of at most `max-events` events; `max-subscriptions` of those at
once, and one that nobody has polled inside `idle-ms` is reaped at the next call.
Nothing here authenticates the caller — that is the bearer token's job, one layer out
(`vaelii.host.serve`) — but heap a stranger can allocate wants a ceiling whether or
not it is authenticated, and the reap is what keeps an abandoned subscription from
holding a slot against a live one.

**The wait happens here, outside the daemon's monitor.**  A long poll parks on the
subscription's own signal object, so a writer serialized behind `serve`'s one monitor
runs to completion while a poll is parked — the feature is about liveness, and a
parked poll that blocked every writer would be a global stall wearing its name.  The
writing thread's only cost is the swap that files the event and a `notifyAll` on a
monitor no poller holds for longer than a compare.

The three entry points are spelled without `!` for `core/watch`'s reason: nothing here
destroys stored knowledge (docs/api.md).  See docs/feed.md, "Across the wire".

Abduction: the scratch-context lifecycle, the gate on what may be assumed, and the
mint/re-prove loop over the dead ends `res/prove` reports.  See docs/abduction.md.

Everything this namespace needs from `vaelii.core` arrives in one `ops` map —
`{:rules-fn (fn [kb goal context]) :assert f :edit f}` — and nothing here names
`vaelii.core`.  Handing them down works because `vaelii.core` is the sole caller of
the entry points that write; a NAT mint, reached from inside the chaining fixpoint,
goes through `vaelii.impl.wiring` instead.

Pure ASPIF text emitter. No vaelii deps, no I/O.

ASPIF is the Potassco Answer Set Programming Intermediate Format, the
ground-program protocol between gringo and clasp.

**This emits what the engine's programs are built from**, and no more:
the rule line (type 1) as facts, choice atoms, normal rules and
integrity constraints, weight-body rules and constraints (the
cardinality bound a `asp/atMost` / `asp/atLeast` translates to), plus
minimize (2) and output (4).

The rest of the format — projection (3), externals (5), assumptions
(6), heuristics (7), acyclicity edges (8), and type 1's disjunctive
and multi-head choice heads — has no encoder here. An encoder nobody
executes is not coverage of a format; it is unverified text generation
claiming to be. What the engine needs, it emits and its tests
exercise, and nothing else is written here.

Wire format of what is emitted (line-oriented, space-separated):
  Line 1: `asp 1 0 0`
  Rule:     1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...>
              head_type = 0 disjunctive | 1 choice
              body_type = 0 normal (list of signed literals)
                     or = 1 weight  (a cardinality/weight body)
              body literal: +atom for positive, -atom for default-negated
  Weight body: 1 <lower_bound> <n> <lit_1> <w_1> ... <lit_n> <w_n>
              satisfied when the summed weight of the satisfied literals is
              at least <lower_bound>.  A cardinality constraint is the unit-weight
              case: `k+1 <= #count{ ... }` is a weight body of bound k+1 over
              weight-1 literals.  Emitted headless (an integrity constraint that
              excludes any model reaching the bound) or with a head (an atom that
              holds when the bound is reached, for a soft/minimized violation).
  Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n>
  Output:   4 <str_len> <str> <n_conditions> <atoms...>
  End:      0

Atom ids are positive integers; 0 is the terminator and must not
appear as an atom. String lengths in show statements count bytes
(equal to character count for ASCII); non-ASCII names need UTF-8
byte counting which we do not currently handle.

The public API has two halves:

  (1) Statement constructors (`fact`, `choice`, `rule`, `constraint`,
      `minimize`, `show`) that return plain data maps. Data form is
      inspectable, easy to assemble programmatically, and trivial to
      unit-test.

  (2) `render` turns a sequence of statements into the full ASPIF
      text with header and terminator.

Bidirectional atom id table for ASPIF translation.

ASPIF atoms are positive integers; every entity referenced in the
emitted program — sentex or contradiction marker — needs a unique id.
Atom 0 is reserved as the ASPIF terminator and is never allocated.

The table maps two kinds of source value to atom ids, sharing a
single counter so ids are unique across kinds:

  (1) sentex ids — the :id field of a vaelii sentex record. These
      become the atoms the ASP solver reasons about.

  (2) contradiction descriptors — nested sentence-shaped Clojure
      values of the form
        (contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
      where `<head>` is a sentence-shaped tag (e.g. `(negation S)`,
      `(disjointTypes ent t-a t-b)`, or a user-named head emitted by
      a grounding rule like `(wrongBulbCount 3 4)`) and `:involved`
      lists the sentex handles that participated. Atoms backed by
      contradiction descriptors get weight in the minimize statement;
      the solver avoids models in which they are true.

Two kinds because two are what the translator emits: every atom in a
program stands for a contested assumption or for a violation. A third
namespace for translator scratch would be an interning path nothing
calls, which is the same unverified machinery `aspif` keeps out of the
emitter.

Labels are short string identifiers that appear in clasp's witness
output; we read them back during result parsing to recover the
originating sentex or contradiction. Format:

  s<sentex-id>   — sentex-backed atoms
  c<atom-id>     — contradiction-backed atoms

Using `s`/`c` prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.

The table is a clojure.core/atom wrapping a plain map. Intern
operations use swap! for atomicity; lookups are pure derefs. All
intern operations are idempotent.

Subprocess wrapper around the clasp ASP solver.

Consumes ASPIF text on stdin, returns parsed results as Clojure maps.
clasp exit codes encode the solve outcome (10=sat, 20=unsat, 30=optimum,
bitmask combinations) and are NOT error codes — we rely on the JSON
`Result` field from `--outf=2` and only throw when clasp itself fails
to run or produces no parseable output.

The four modes are the ones `vaelii.impl.asp.edge` asks for:
:label, :all-optima, :classify-true, :classify-supportable.

Every run is single-threaded under a fixed seed and carries `--solve-limit` from
`config/asp-solve-limit` when it is positive (`search-args`), so where a search stops
is a function of the program.  `--time-limit` from `config/asp-time-limit` (0 lifts
it) is the backstop, and a process still running at `deadline-ms` is killed.  A
search stopped by either limit is read as `:interrupted` (`stopped-short?`).

Ownership: `run-clasp` starts the process and is its only owner.  It returns only
after the process has exited, and it kills the process and every descendant on the
paths that leave it running: the deadline and a throw out of the wait (an interrupt).

In-process ASP solver: a JNA binding to the native clingo C API (which
embeds clasp). Same solve modes and return shape as
`vaelii.impl.asp.clasp/solve`, but without the subprocess + JSON round-trip.

`solve` takes a translated program map `{:aspif <text> :stmts <statements>}`
and injects the ground `:stmts` straight through the `clingo_backend_*`
accessors — no ASPIF text, no temp file, no parse (`backend-load!`). Each
program atom id is interned as the function symbol `a(<id>)` carrying its s/c
label; a model's true atoms come back through clingo_model_symbols and are
mapped to labels through that symbol association, so no show statement is
emitted. `classify-both` keeps the ASPIF-text path (`clingo_control_load_aspif`
over a temp file), since one live control serves both enumerations.

Why in-process: it drops the per-solve fork and JSON round-trip the
subprocess pays, which is the whole win on the small programs
`vaelii.impl.asp.solver` routes here.

The four modes map to clingo configuration passed as command-line arguments
to clingo_control_new (clingo accepts clasp's flags): --opt-mode=optN so
brave/cautious enumerate over optimal models only, --enum-mode=brave|cautious,
--models=0|1. The lexicographic cost vector comes from clingo_model_cost.

Native lib: a system libclingo (brew install clingo) reachable via
jna.library.path, or an absolute path in -Dvaelii.clingo.lib. Crash isolation
is lost vs the subprocess — every native return is checked, every solve handle
is closed in a finally and every Control is freed in one; a malformed program
throws rather than segfaults.

The search flags are clasp's (`clasp/search-args`): one thread, a fixed seed, and
`--solve-limit` from `config/asp-solve-limit`, which the control takes as a solver
option and applies to each solve.  A search the solve limit stops reports neither
the exhausted bit nor the interrupted one, and `finalize` reads that as
`:interrupted`.

The time limit (`config/asp-time-limit`), the backstop behind it, is not a flag here
— libclingo's control takes solver options only and refuses `--time-limit` — so each
solve runs async and is drained through `clingo_solve_handle_wait` with what remains
of the budget; a solve still running when it runs out is cancelled and reports the
interrupted bit, read as `:interrupted`.

v :- a_h1, a_h2, ...

:- a_h1, a_h2, ...

d :- a_1, ..., not a_k.

:- k+1 <= #count{ a_m1, a_m2, ... }        # at-most-k: never k+1 together

v :- k+1 <= #count{ ... }                  # breaching the bound costs, not excludes

The real ASP backend behind `vaelii.impl.types.solve/Solver` — the edge solver.

`solve.clj` describes *what* an edge solve is: most of the KB is monotonic or
default-true with no conflict, so only the contested defeasible nodes are sent,
known-true content is fixed background, and contradictions are soft and
prioritized so a solve never fails.  This namespace renders that `Program` to
ASPIF and reads an answer set back.

## The encoding

Each contested assumption is a **choice atom**: true means believed, false means
defeated.  Known-true (`:fixed`) members of a contradiction are *not* atoms —
they hold by assumption, which is exactly what makes them background.

A contradiction `#{h1 h2 ...}` becomes a violation atom derived from its
contested members:

    v :- a_h1, a_h2, ...

and a **weak** constraint minimizing `v`.  Weak rather than hard is the whole
point: an unsatisfiable contradiction costs, it does not make the program UNSAT,
so it comes back in `:violated` instead of throwing.

A nogood carrying `:hard true` (a `set/hardConstraint` rule ground by
`solve-context`) is instead a **hard integrity constraint**

    :- a_h1, a_h2, ...

with no violation atom and no minimize term: a model satisfying its whole body is
excluded outright.  That is what makes graph 3-coloring plain satisfaction rather
than optimality-proving over soft violations — an adjacency clash is never
tradeable.  Soft nogoods (the default) keep the minimize path above.

A solve's **normal rules** (`program`'s `:derivations`, ground from `set/solveRule`s by
`solve-context`) are rendered as they are written,

    d :- a_1, ..., not a_k.

over the choice atoms and the **derived** atoms (`:derived`), which get atoms after the
choices and carry no choice rule and no minimize term: the rules alone decide them.  A
hard nogood left with no atom holds in every model and renders as the empty integrity
constraint.

A **cardinality** entry (`program`'s `:cardinalities`, ground from a `asp/atMost` /
`asp/atLeast` rule) is a bound on how many of a set of choice heads may or must hold,
rendered as ONE weight-body statement rather than the `C(n, k+1)` subset nogoods a
hand-written encoding needs.  A hard bound is a weight-body integrity constraint

    :- k+1 <= #count{ a_m1, a_m2, ... }        # at-most-k: never k+1 together

a soft one derives a violation atom the same minimize path penalizes

    v :- k+1 <= #count{ ... }                  # breaching the bound costs, not excludes

and at-least-`k` is the mirror over the default-negated members (`card-encoding`).

In practice `:violated` comes back empty, and that is correct rather than a gap.
An irreducible known-true clash never reaches a solver: `decide/verdict`
classifies it as *hard* and reports it directly, and `solve/program` drops any nogood
with no contested member.  What does arrive always has a contested member, and
defeating that member always satisfies it.
The `:doomed` path below is therefore defensive — it adds no work and stays
correct if nogoods ever grow beyond today's `S` vs `(not S)` pairs.

## The objective, most significant first

Higher ASPIF minimize priorities dominate lower ones, so the levels are:

| level | minimizes | why |
|---|---|---|
| `2 + rank(p)` | violation atoms | satisfy contradictions, caller priority first |
| `1` | defeated assumptions | give up as little belief as possible |
| `0` | a content-keyed weight | break remaining ties *stably* |

Caller priorities are mapped through their ascending rank rather than used as
levels directly, so any integers work and none can collide with the two levels
below.

## Determinism

A tie between equally-good answer sets has no principled winner, but it must not
depend on assertion order — the engine-wide invariant in docs/nmtms.md.  Atom ids
are allocated in `solve/content-key` order, and level 0 weights defeating the
greatest content-key most cheaply, mirroring the stub's choice.  Same knowledge
in any order, same answer set.

## Availability

`edge-solver` degrades rather than fails **when there is no backend at all**: with no
clingo and no clasp reachable it delegates to `solve/local-solver`, so installing it is
always safe.  Degradation is confined to that case on purpose — see below.

## A result that is not an answer

A backend's result is an answer set only at `:optimum` or `:sat`.  `:interrupted`
(the solve limit, `config/asp-solve-limit`; the time limit, `config/asp-time-limit`;
or a signal) and `:unknown` carry **no** witness, and every reader here maps an atom's
absence to *defeated* or *not kept* — so read as an answer, an empty result defeats
every contested assumption and labels every choice head false.  `answered?` gates each reader.

**With a backend present, `edge-solver` decides nothing rather than degrading.**  The
stub and ASP disagree — measured on two nogoods sharing a member, the stub defeats
`{1,3}` where the optimum defeats `{2}` — and the two are not interchangeable halves of
one answer.  A labeling solve that runs out of budget while the classification solve
beside it finishes would pair a stub labeling with an ASP classification, which
`label/check-agrees` reports as `:labeling-inconsistent`, blaming the encoding for a
disagreement the fallback introduced.  A labeling committed from such a pair would
differ run to run on identical knowledge — the order-independence invariant in
docs/nmtms.md is a claim about *knowledge*, and a wall clock is not knowledge.  So `undecided` is
returned instead: no defeat, the contested assumptions all stand, and `:error` names
what went wrong for a caller that can act on it.  With no backend the two degrade
together and stay consistent for free — `classify-program` claims nothing without one —
which is why that case, and only that case, still falls back.

A backend that **throws** — clingo's `:solver-failed`, clasp's `:solver-unavailable`,
a JNA `Error` against a missing libclingo — reads the same way, and the catch is here
rather than at the caller because this is the boundary a native failure crosses.
`undecided` hands the failure back as data, and `label/solved-labeling` raises its
`:error` before the labeling asserts anything.

`:unsat` is different and keeps its own reading: a definite *no model*, the same answer
in every run, so it costs the invariant nothing.  Each reader has a word for it —
`edge-solver` degrades, `kept-of` keeps nothing, `enumerate-optima` is empty.

The imperative readers (`kept-of`, `enumerate-optima`, `classify-program`) refuse an
unanswered result with `:solver-failed` rather than return a world nobody computed.
They are not mid-arbitration, so a throw there adds no work and says more.

:true        ⊆ believed        (cautious holds in the committed model)
:false       ∩ believed = ∅    (excluded holds in no model, including that one)
:supportable — either way, by definition

Brave/cautious classification of a settled tie, and materializing one labeling as
a specialization context.

## What this adds over `in?`

The TMS answers *what do I believe*. After `settle` arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. `in?` cannot tell them apart; both read as "believed".

Brave/cautious classification separates them by asking the solver for *all* optimal
answer sets rather than one:

| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
| `:true` | yes | yes | forced — no consistent labeling gives it up |
| `:supportable` | no | yes | arbitrary — the current belief is one of several |
| `:false` | no | no | excluded — no consistent labeling holds it |

`:supportable` is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are `:supportable`: whichever the TMS committed to, the
other was equally available.

## Concert with the TMS

Two rules keep these from drifting apart from belief.

**Classification reads the recorded program, never a recomputed one.** Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. The `:program` atom on the KB holds what the solver was
actually asked (see the KB record); `vaelii.core/last-program` is the public read of it.

**Labeling reads the TMS, not a fresh solve.** `label-context` materializes the
labeling the engine *committed to*, taken from `jtms/in?`, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.

So the invariants hold by construction, and `asp_label_test` pins them:

    :true        ⊆ believed        (cautious holds in the committed model)
    :false       ∩ believed = ∅    (excluded holds in no model, including that one)
    :supportable — either way, by definition

## Requirements

Classifying a `Program` needs a real ASP backend; `local-solver` produces one labeling
and cannot enumerate optima. With no backend reachable, `classify-program` reports every
contested assumption as `:supportable` — correct (each *is* one of several options)
and never overclaims `:true`.  A represented dilemma is classified and labeled off the
dependency graph instead (`classify-local`), on every build.

A query-time prover for `(bravely S)` and `(cautiously S)` — brave/cautious reading
of the dilemmas the KB currently holds, answered as a read and never committed.

## What it answers

`(cautiously S)` holds when `S` is in **every** optimal labeling of the current
dilemmas; `(bravely S)` when `S` is in **some**.  Over a coexisting `P`/`¬P` dilemma the
engine declines to arbitrate (docs/exceptions.md), both sides are IN, and an ordinary
`ask` reports both — so it cannot tell the *forced* belief from the *arbitrary* one.  A
brave/cautious read can: in a Nixon diamond `(bravely (pacifist N))` holds and
`(cautiously (pacifist N))` does not, because the other labeling gives it up.

This is the read-path delivery of the forced/arbitrary signal.  The only prior route to
it, `do/labeling`, **commits** — it re-asserts the kept side at `:monotonic` and defeats
the loser everywhere (docs/labeling.md).  This prover commits nothing: it reads
`label/classify-datum` — the solve-free `label/classify-local`, refined by a backend's
`classify-program` only past its caps — all pure reads over settled belief, so a query
answers and leaves belief, `contradictions` and `last-program` exactly as they were.

## Opting in

Registered like the other optional reasoners — `(add-reasoner kb :brave-cautious)` — so
the ASP stack stays off a KB's load path until a caller asks (docs/asp.md).  **It reads
the solve-free JTMS bracket** (`label/classify-local`) with or without a backend, which
enumerates the dilemmas' optimal resolutions from the dependency graph and classifies
each datum by which resolutions keep it — `:true` in every, `:supportable` in some,
`:false` in none.  Exact for a datum whose
clusters it enumerates: the one cluster its support touches, or several whose product of
resolutions stays within `VAELII_CLASSIFY_MAX_JOINT_OPTIMA`.  A datum past that cap, or
one touching a cluster too large to enumerate, degrades to `:supportable`; a backend
refines a member of such a cluster when no member of it derives from another, where a
`Program` is exact (docs/labeling.md).

## Where it stops

**Ground `S` only.**  `(bravely (pacifist N))` is answered; an open `(bravely (pacifist
?x))` is not applicable and no prover answers it, rather than enumerating the contested
atoms — the same restraint `different` takes.

**A query, not a fact and not an antecedent.**  `bravely`/`cautiously` are not
assertible (`wff/brave-cautious-problems`): a stored one would be a computed value with
no way to keep it current, the reason the aggregates and `unknown` are refused too.  As a
rule antecedent the answer carries no support (it is not a `SupportingProver`), so the
forward join drops it and it derives nothing — a read, not something belief rests on.
Threading its support (the dilemma's contested handles) so a rule could rest on it is the
open design point, deferred until a use asks for it.

Solving as a **persistent, inert** artifact: `assumptionRules` define choices, a
solve grounds them (scoped to a base context), enumerates the optimal answer sets,
and materializes **each one as its own labeling context** — a `genlCx` child of
the base holding the chosen truth values as inert sentexes.  `classify` then gathers
brave/cautious over those labelings.

The two imperatives `(do/label Base Into)` and `(do/classify Into)` route here.

## Why inert, and why per-answer-set

Belief in this KB is global (one JTMS, not an ATMS): a *believed* `(not head)` in a
context that sees the base would defeat the base's `head` everywhere — so only one
labeling could ever exist (the `do/labeling` global-commit).  Materializing the truth
values **inert** (`core/assert-inert` — stored and indexed but not a JTMS premise)
sidesteps that entirely: an inert sentex is never IN, so it is invisible to the
belief-filtered nogood scan, forms no contradiction, and moves no belief.  Every
answer set therefore coexists as its own context, the base KB is untouched, and the
result **persists in the records** for inspection.

## What persists, and what does not

The **answer** persists: the labeling contexts and the classification, as inert
sentexes in the records.  The **grounding** — the menu of candidate choice heads —
never does.  A grounding is derived solver working state, recomputable from the
assumptionRules and the base's believed facts; an inert copy would carry no
justification linking it back to what produced it, so it would rot silently the
moment the base moved.  The Program keys on program-local ids (see `build`), and
`label` returns the menu as `:choices` for a caller who wants to see it.

And what persists is **replaced on re-run**, never accreted: `label` clears a
previous run's artifacts under the same `Into` before writing (see `clear-run!`),
and `classify` clears its own previous classification.  Truth values from two
different groundings unioned into one context assert nothing at all.

## What a choice constrains (docs/solving.md)

Constraints reach the ground choice heads and the atoms the solve rules derive from
them: the engine's own contradictions among the choice heads — a `(not X)`/`X` pair, a
`functional` predicate given two values, a `disjoint` type clash — and every
`hardConstraint` / `softConstraint` rule ground over the program's atoms.  A choice
propagates through a `set/solveRule` and through nothing else: the solve rules are
ground into the program's normal rules (`ground-derivations`), and a rule without the
wrapper is not — nothing runs the chainer with a choice held hypothetically.

Backend selector for vaelii's ASP solver. Callers (`asp.edge`, `asp.label` and
`asp.solve-context`) use `solver/solve`/`solver/available?` so the engine can run
the in-process clingo backend (default, when libclingo + JNA are present) or fall
back to the clasp subprocess — without any caller change.

The clingo backend is loaded LAZILY via requiring-resolve so JNA/libclingo
stay optional: a plain build (without the `:with-clingo` profile) has no JNA
on the classpath, the resolve fails cleanly, and the facade falls back to
clasp. clasp is also the deliberate fallback for long-running daemons, since
an in-process native crash takes down the whole JVM.

Select explicitly with -Dvaelii.asp.solver or VAELII_ASP_SOLVER = clingo|clasp.
Default is auto: prefer in-process clingo when it loads, else clasp.

The per-sentence write entry point: what `vaelii.core/assert` does once it has one
sentence in one context.

Three things live together here because the assert path runs them as one step and
`preview` has to undo all three:

- **The premise mark**, written to the network node and the record slot together
  (`put-premise-mark`), and resolved from content rather than arrival order
  (`mark-premise` says why a bare re-assert may not downgrade a class).
- **The rule slots**, reconciled when a rule is stated twice
  (`reconcile-rule-slots!`, `join-engines`).
- **The dispatch** a sentence takes — imperative, `ist`, rule, or plain fact
  (`assert-one`).

`*premise-audit*` is the hook a batch rollback reads (`core/rollback-batch!`).

**`assert-one` takes the re-entry as an argument.**  An `(ist Ctx S)` sentence is not
stored — it asserts `S` in `Ctx` — so the dispatch re-enters the caller's own entry
point.  That is `vaelii.core/assert`, and an engine namespace may not require
`vaelii.core`, so the caller passes it in.

Resource-bounded / anytime realization of an answer stream.

The engine's query paths are **lazy** — `ask`, `query`, and the level stack
all yield one solution at a time, paying per result consumed.  Resource-bounding
is therefore the *consumer-side* discipline of realizing that stream under a
bound and reporting whether it ran dry or was cut short — and resumption falls
out of laziness for free, because the unrealized tail **is** the continuation.

A **budget** is a map of optional bounds (any subset; nil / {} means unbounded):

  :max-ms       wall-clock milliseconds — a soft deadline, checked *between*
                yielded results (between DFS steps and node expansions in
                `prove-within`), and inside one only by a walk that reads
                `*deadline*` (the argument-preservation prover's claim walk);
                every other single pull or step runs to its end
  :max-results  stop after this many solutions
  :max-cost     a qualitative prover-cost ceiling — a tier keyword (see
                `vaelii.impl.provers/cost-tiers`).  Honored by `ask-within`,
                which drops provers above the tier before the stream is built;
                ignored *here*, since it selects *which* work runs, not how much
                of a stream to realize.
  :max-depth    transformation (rule-expansion) depth — honored by `prove-within`
  :max-term-growth
                how many levels of compound nesting a subgoal may add over what its
                own derivation path has already met (`res/default-max-term-growth`,
                8) — the DFS prover's other termination guard, honored by
                `prove-within` through `prove-bounds`

A key outside those five is refused (`:unknown-option`, `check-budget!`): every
bound is optional, so a misspelt one is not missing — the run is simply unbounded,
in silence.

A **partial result** — the anytime contract returned by `collect` / `from-batch`
/ `resume`:

  :results      the solutions realized in *this* step (a vector)
  :status       :complete  the source ran dry — the answer is exhaustive
                :timeout   :max-ms elapsed with work remaining
                :capped    :max-results reached with work remaining
  :count        (count :results)
  :elapsed-ms   wall-clock spent in this step
  :resume       nil when :complete; otherwise a 1-arg fn (budget -> partial
                result) that continues exactly where this step stopped

`:results` are per-step, **not cumulative**: concatenate across steps for the
whole answer.  The resume continuation captures an in-memory lazy tail (or, for
`prove-within`, the DFS goal stack), so resumption is **in-process only** — it
does not survive a restart, and holding one pins its captured state in the heap
(see the single-writer contract in docs/storage.md).

What this process is holding beside the stores — one register every derived,
droppable structure declares itself in, and one read over the lot.

The stores are measured elsewhere: `catalog/heap` reports the JVM's own figure and
`catalog/footprint` estimates what a loaded KB costs.  Neither says anything about the
**caches** — the atoms and plain maps holding answers the engine would otherwise
recompute — and a hit rate is the only evidence a cost model has.  "The
second query was fast" is a demo; "the second query was fast because it was served
from a cache, and here is the rate" is a measurement.

**A register rather than a dozen accessors.**  This namespace requires only `config` and
the logger, neither of which holds a cache, so the reader still has no require edge down
to a namespace holding one: every such namespace requires *this* one and declares itself at load, and
there is no list here that a new cache has to be added to twice.  The `config` edge reads
one switch, `VAELII_CACHE_SCALE`, and `limit-of` applies it to every count-bounded
cache's limit.  A cache in a namespace this
process never loaded — a qualitative calculus nobody registered, the metric-time
reasoner — is absent from the read because it is absent from the process, rather than
present as a row of zeroes.

**Two scopes, and never one wearing the other's clothes.**  `:scope` says what a row's
`:entries` counts: `:kb` for a cache hanging off a KB record, `:process` for a static
one every KB in the JVM shares.  `:counters` says the same about `:hits` / `:misses`,
separately: the closure neighbours keep process counters over entries only a live
search step can count, and a row counted by a derived-state tally counts per structure.

**`:unit` is not decoration.**  One cache counts literals, another counts networks, a
third counts symbols, and a column of bare integers compares none of them.

A row whose `:entries` is nil is one that cannot be counted from outside — the
scope-bound caches, bound for the length of one chaining run or one search step and
garbage when it returns.  They are registered all the same, with the reason in
`:note`, so the list is complete rather than merely finite.

**A row answers for itself, and fails for itself.**  The register is open, so a read
here runs code this namespace has never seen; one that throws is reported as a row
carrying `:error` rather than allowed to take the answer down with it.  A diagnostic
is worth most while something is already wrong, which is exactly when it must not be
the next thing to break.

The clock behind the calendar constructors — where `(YearFn 2000)` stops being a name
the interval algebra relates and starts being a **stretch between two moments**.

`vaelii.impl.datetime` reads a calendar term to its fields and to the half-open
`[start end]` it lies between; this namespace is the KB-facing half, one prover
answering three families of goal out of that reading and storing nothing:

  (startOf (YearFn 2000) ?i)              ?i = (InstantFn 2000 1 1 0 0 0)
  (endOf   (YearFn 2000) ?i)              ?i = (InstantFn 2001 1 1 0 0 0)
  (instantBefore (InstantFn 1999 6 1 0 0 0) (InstantFn 2000 1 1 0 0 0))
  (during (MonthFn 2000 3) (YearFn 2000))
  (meets  (MonthFn 2000 2) (MonthFn 2000 3))

**Answered, never stored.**  Nothing here mints a term, asserts a sentex or posts a
justification, so a computed endpoint is not a belief, needs no retraction, and leaves
no orphan for the NAT sweep to ask about (docs/nat.md).  What it rests on is the
calendar and the convention, both of which are in this code rather than in the store —
which is why it implements `Prover` and not `SupportingProver`: there is no handle to
name, and a prover that names none is one whose answer no retraction can invalidate
(docs/inference.md, "What a computed answer rests on").

**Half-open, `[start, end)`.**  A term's end is the first moment of the next term at the
same precision, so the end of 1999 and the start of 2000 are the same term and
consecutive calendar terms **meet**.  `(before (YearFn 1999) (YearFn 2000))` therefore
does *not* hold and `(precedes …)` does — before is Allen's strict one, with a gap, and
`precedes` is the ordering that does not care whether the two touch, which is what
"1999 comes before 2000" means (docs/time.md).

**Fields, not endpoints, answer an interval relation.**  The relation between two
calendar terms is fixed by their bounds, so `relation` classifies it directly rather
than routing through `startOf` / `endOf` and a constraint network — one comparison of
two six-field vectors against a network build.  The endpoints stay answerable because
they are what joins this to the metric layer, not because anything here needs them.

**Both ends bound, always.**  An open variable on either side of an instant ordering or
an interval relation would ask this to enumerate the calendar, which is not an answer
but a process that does not come back — so `applicable?` refuses it, exactly as the
point algebra's own prover answers nothing for a pair of open variables.  The one
variable it binds is a `startOf` / `endOf` **result**, which is a function of the
interval and so exactly one term.

The callers' entry point to the **optional** storage capabilities: one function per
capability that uses it when the store has it and falls back to the plain
`RecordStore` op when it does not.

It is beside `vaelii.impl.protocols` rather than in it because that file is
protocol-only — the `IndexStore` declaration there is large enough that
re-evaluating the form (as cloverage does, form by form, to instrument a
namespace) overflows the JVM's 64 KB per-method bytecode limit, so the whole
namespace is loaded but not instrumented (scripts/coverage.sh).  A protocol
carries no code to cover; these fallbacks do, and here they stay measured.
`vaelii.impl.jtms-protocol` is split from `vaelii.impl.jtms` for the same reason.

Each entry point is the same shape: `satisfies?` the capability, take its op, else the
loop it replaces.  A caller therefore never branches on a capability, and a store
without one reads exactly as it did before the capability existed.  `hinting` and
`recovery-hint-chunk` are not entry points but the chunking a prefetch entry point is used
through, which is why they sit here beside it.

Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible
rules alike, with the definitional checks re-run on the derivation path and the
`exceptWhen` guard consulted before a conclusion is placed.

Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): a firing joins antecedents against stored facts (kb), checks its
conclusion (checks), and reflects what it places into the caches through the
derivation-path choke point (special).  Belief settling happens *after* a run,
in `vaelii.impl.settle` — nothing here defeats or arbitrates.

The definitional checks — arg argument types, disjointness, functionality —
plus ground-ness and the stratification glue over the rule index.

Second layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle):
every check reads the KB (taxonomy, index, believed matches) and returns a value
or throws — nothing here writes.  Both mutation paths consume these: `assert`
(vaelii.core) throws the value, the derivation path (vaelii.impl.chain) records
it in the violations ledger.

The clashes a reader reads: the hard clashes and dilemmas of every placed nogood as
reports, each with the declarations it convicts through, and the disjointness clashes
no single writer could see.  Nothing here writes belief.  See docs/nmtms.md, "The clash
reports".

The dense **columnar trie** index — the `:memory-columnar` backend, off by default.

The flat-map index (`vaelii.impl.kv`) stores each trie node as three entries keyed by
a boxed **vector of the full path prefix**; a path's every prefix is a separate object,
so the structure is redundant boxed keys + HAMT overhead — `bench/…/densetrie.clj`
measured that at ~487 MB of the 592 MB index (300k real facts), and it is the index's
dominant cost.  The bench also found the win is the *layout*, not interning: a
fastutil-map-per-node recovers only 1.28×, a columnar layout ~15–20×.

So here the trie is a real node graph, not a map of prefixes:

  * nodes are `int` ids; node data lives in **grow-on-demand parallel arrays** indexed
    by id — `counts` (primitive `int[]`), `toks`/`tgts` (a node's child edges: a
    **sorted `int[]`** of tokens and the parallel `int[]` of child node ids while the
    node is narrow, one primitive `Int2IntOpenHashMap` once it is wide), `leaves` (an
    `IntPostings`, the same tiered `int[]`/Roaring set Phase 1 uses — this is where the
    two phases unify);
  * edges carry **interned `int` tokens** from a `vaelii.impl.tokens` dictionary, not
    boxed symbols/markers/lists; the dictionary's inverse decodes them for `children`.

**Mutable, not a static CSR.**  A compressed-sparse-row trie is the densest a trie
gets, but it is *static* — the index mutates on every assert/retract.  A per-node
sorted `int[]` supports incremental add/remove (binary-search + array splice) while
still dropping the boxed prefixes and the per-node hashmap slack; the node ids of a
pruned subtree are recycled through a free list.  Freezing the cold majority to a true
CSR is a later compaction pass (the mutable-head / compacted-tail pattern the record
store already uses), justified by measuring where this lands.

**A node's child structure is tiered on its width, and that is a measurement.**  The
splice above costs O(children already there), and nothing bounds a node's width: the
level-2 node holds one child per distinct first argument of a predicate, so an
array-only node structure loads one broad relation — `(genl S T)`, any hot
relation — in time quadratic in that relation's own extent.  It is the *node* that is
expensive, not the trie: holding 200k facts fixed and varying only the widest node's
fan-out, an array-only structure reads 4.2 s at 2,000 children, 9.0 s at 20,000 and
18.2 s at 200,000.  So past `promote-at` children a node's edges become one primitive
`Int2IntOpenHashMap` (O(1) insert, no splice) and drop back to the array pair below
half of it.  Blanket maps are the wrong answer in the other direction — the bench found
a fastutil map per node worth 1.28× against the columnar layout's ~15–20× — and the
tiering is what takes both, since the overwhelming majority of nodes are narrow and
never leave the dense pair.

**Composition keeps the new surface small.**  Only the trie families
(`index`/`unindex`/`lookup`/`count-at`/`children`) are native here; the secondary
roots, the rule / exception indexes, the inverted term index, and the term roster
beside it — all flat `key → set` maps — delegate to an embedded `KvIndexStore` over a
Phase-1 `TieredKvBackend` (int-dense postings already).  `index-sentex` and
`unindex-sentex!` take the ops for those families from `kv/flat-family-adds` /
`kv/flat-family-retires` and batch them straight to the shared backend, so both stores
write the same keys in the same order and the delegated reads stay consistent.

Single-writer, like every index: the arrays are mutated in place; `lookup`/`children`
/`leaves` materialize fresh Clojure collections at the boundary.  Proven set-equal to
`KvIndexStore` by `columnar_index_oracle_test`.

**Single-*threaded*, which is narrower than single-writer.**  The `Trie` fields are
`^:unsynchronized-mutable`, so a write publishes through no barrier: a second thread
reading this index may see an array reference, a capacity or the CSR-mode flag from
before a growth or a compaction, and there is no happens-before edge that would stop
it.  The atom- and lock-based backends give an incidental reader beside the writer a
consistent view; this one does not, and it is the caller's job to keep its reads on
the writer's thread or behind a synchronizer of its own.  The fields are unsynchronized
because the walk reads them at every frontier node, which is the index's hottest loop
— a volatile read there is paid per node per lookup, to buy a guarantee the engine's
own single writer never needs.

The build's switches — the `vaelii.*` JVM system properties and the `VAELII_*`
environment variables — read in one place, each against a domain, and **refused when
the value is outside it**.

This is `kb/check-opts!`'s invariant one layer out: *an option that is not read is not
an option*.  A switch read as a membership test or an equality against one spelling has
no wrong value — every misspelling falls to the other branch — so under that reading
`vaelii.disk.auto-compact=disabled` is compaction **on** and `vaelii.disk.fsync=always`
is the three-second tick, which is the durability level the operator is trying to
leave.  A process that reports itself configured and is not is the failure
`check-opts!` exists to prevent, on the property that decides whether a crash loses
data.  So no switch is read that way here.

## One vocabulary for the boolean switches

`truthy` and `falsy` below, case-insensitively, and nothing else: every boolean switch
reads the same words, so a spelling that works on one works on all of them and a
spelling that works on none is an error rather than the opposite setting.  A blank
value is *unset* — an exported-but-empty environment variable is the shell's way of
saying nothing.

## Where a refusal lands

`check!` reads every switch at `kb/open-kb`, so a wrong value fails the open — before a
record is written and while what the operator typed is still legible.  It reads the
whole set rather than the ones this KB's backend uses, because gating the check on the
configuration is how a wrong value in the configuration escapes it.

Where each switch is read **besides** that is the `:read-at` column of `switches`, and
`read-at-kinds` says what the three values mean.  It is a column rather than a list of
names here for the reason `check!` is a walk rather than a list of calls: a roster
spelled twice is one that can disagree with itself, and this one had.

The two that make the eager read worth its cost are visible there as `:worker` and
`:load`.  A `:worker` row is read inside `fsync-all`'s `catch Throwable`, which logs an
exception's class name and nothing else — an unattributable line repeating every three
seconds with auto-compaction silently dead.  A `:load` row is the root value of a var
and cannot be deferred at all; it refuses at that namespace's load, naming itself, for
`guard/max-body-bytes`' reason: a silent fallback leaves an operator believing a setting
they never made, and a raw parse failure out of a `def` reports as a namespace that
would not load rather than as the typo it is.  `log-level` is `:load` for a different
reason — it is the one switch whose effect is an *install*, and the entry point it belongs at
is the moment the engine is loaded rather than the moment a KB is opened.

## What is not checkable here

Five switches name a path or a label with no domain to check — `vaelii.disk.dir`,
`vaelii.kb.path`, `vaelii.kb.catalog`, `vaelii.build`, `vaelii.clingo.lib`.
`vaelii.web.port` / `VAELII_WEB_PORT` is the browser's
own, read at `web/default-port`, where an unparseable value falls through to the next
source rather than stopping a start over a convenience variable (docs/web.md).

Three more belong to the two servers and are read at `vaelii.host.guard`, which both
of them read: `VAELII_API_TOKEN` and `VAELII_ALLOWED_HOSTS` are a secret and a host
list, neither of which has a domain to hold them to, and the ceiling
`VAELII_MAX_BODY_BYTES` refuses at `guard/max-body-bytes` for the reason
`assertive-arg-types?` refuses at load — it is the root value of a var.
`VAELII_SANDBOX_KEY`, the key the browser tags its sandbox cookies with, is a secret
read at `vaelii.browser.sandbox`, with no domain either.

The structural genlCx producer for reified-NAT contexts — docs/context-nat.md.

A `(contextArgSubrelation F pos R)` declaration says two `F`-contexts identical except
at argument `pos` are ordered by the sub-relation `R` on that argument.  This namespace
reads the declarations and the context NATs of `F` from the store and **materializes**
the `genlCx` edges they entail: for two siblings whose `pos` arguments stand in `R`, the
more specific one (its argument `R`-below the other's) is deduced to `genlCx` the more
general, as a **justified** sentex in CxUniverse.  So the edge belief-follows for free —
retract a context (its `termOfUnit` map), the declaration, or the `R`-evidence, and the
ordinary JTMS relabel withdraws it.  It is never a premise anyone asserted.

`R` is resolved by a **bounded** oracle, because the producer runs on the assert
maintenance path and a genlCx edge feeds the taxonomy closure a relabel loop reads — so
a prover search is out (docs/naf.md): either a registered pure structural comparator
(the datetime one, keyed on `subintervalOf` over `DatetimeFn` terms) answers it, or a
believed stored `(R a b)` fact does.  A comparator answer is a pure function of the two
expressions, already carried by the `termOfUnit` antecedents, so it needs no extra
supporter; a stored fact contributes its own handle so defeating it withdraws the edge.

Materialization reuses the derived-sentex pattern `special/deduce-lift` uses:
`find-or-create-sentex`, then `special/derived-sentex-added` to reach the genlCx closure
and post the re-check triggers, then a JTMS justification under the
`contextArgSubrelation` informant.  What the edge shows the contexts under it is the
settle's (`special/drain-context-moves!`), as for an edge somebody asserted (vaelii#56),
so the caller settles once an edge was built.

Calendar containment — the first time dimension for context NATs
(docs/context-nat.md), read off two spellings of the same interval.

A `DatetimeFn` is a **structural** (`unreifiable_function`) constructor taking a
reduced-precision ISO 8601 string that denotes an *interval*: `"2000"` is the year,
`"2000-01"` its January, `"2000-01-15"` a day, `"2000-01-15T13"` an hour, and so on
down through minute and second.  Because the string stays readable inside the context
expression (an unreifiable NAT is never minted), the structural genlCx producer can read
two such terms and decide containment from their shape alone.

`YearFn` / `MonthFn` / `DayFn` are the **calendar constructors** over the same three
coarsest fields, written as numbers instead of as a string: `(YearFn 2000)`,
`(MonthFn 2000 1)`, `(DayFn 2000 1 15)`.  They are unreifiable for the same reason
`DatetimeFn` is — the fields are what the ordering reads, and a minted constant would
hide them — and each carries **one field per argument**, so the arity *is* the
precision and there is no string to parse or mis-parse.  A calendar term and the ISO
string naming the same interval read to the same fields, so the two spellings order
against each other as readily as against themselves.

Containment is **field nesting**: a more-precise interval is inside a less-precise one
whose fields it shares — `(MonthFn 2000 1) ⊆ (YearFn 2000)`, `"2000-01-15" ⊆
"2000-01"`, while `"2001" ⊄ "2000"` (the year differs) and `"2000" ⊄ "2000-01"`
(the year is the *coarser* interval, so it contains the month, not the other way).
Two sibling months nest neither way, which is what keeps January's facts out of
February.

`InstantFn` is the other half, and the one thing here that is about **moments** rather
than stretches: `(InstantFn 2000 1 1 0 0 0)` is one instant, six integer fields wide,
and `bounds` reads a calendar term to the two of them it lies between — half-open, so
the end of 1999 and the start of 2000 are the *same* term.  `vaelii.impl.calendar`
answers `startOf` / `endOf` and the orderings out of that (docs/time.md).

Everything here is a **pure, bounded** computation — parse two short forms and compare
vectors — so the producer may call it inside the settle/relabel loop, where a prover
search is forbidden (docs/naf.md).  Fields are compared by numeric value, so `"2000-1"`
and `"2000-01"` denote the same month, and so does `(MonthFn 2000 1)`.

The nogood candidate index.  Each family keeps its rows of one candidate index
(`:nogood-candidates`), which the placement detectors read; this namespace runs the
families as one index, holds the forced-monotonic roster, and decides a placed nogood
from its members' classes (`verdict`).  See docs/nmtms.md, "A nogood placed as a
conclusion".

The arity family: a tuple whose length breaks the length a reader binds its functor
to, and two predicates a `genl` edge relates whose own lengths differ, each placed as a
conclusion (`chain/place-arities!`).  See docs/nmtms.md, "A nogood placed as a
conclusion".

The inherited family's rows of the candidate index: the clashes the settle's detector
found (`discovery/discover-inherited!`), each with its vantages, where each is placed.
See docs/nmtms.md, "The inherited-clash memo".

The membership families: two memberships of one term whose types a separation holds
apart (`disjoint`), a membership beside a denial of a supertype of its type
(`supertype`), and a membership under a cover's whole beside a denial of each part
(`covering`), placed as nogoods (`chain/place-memberships!`).  See docs/nmtms.md, "A
nogood placed as a conclusion".

The negation family: a stored `(not B)` and a stored `B` whose contexts have a common
descendant, placed there as a nogood (`chain/place-negations!`).  The bodies stored in
both polarities and their members are an index family (`reads/as-stored-opposed-…`).
See docs/nmtms.md, "A nogood placed as a conclusion".

The declarations over related types: a `disjoint` over two types one reaches the other
of through `genl`, a cover naming a part a `disjoint` separates from its whole, and an
`orthogonal` over two types a `genl` edge or a separation contradicts.  See
docs/reference.md, decision 8.

The two tuple families.  The self and converse family: a ground binary self tuple under
`irreflexive`, and a tuple and its stored converse under `anti_symmetric`.  The
tuple-mark family: the determinants under `functional` and `functionalInArg`, the
`anti_transitive` chains and the `asymmetric` converse pairs.  Both find their nogoods
from a stored tuple's own arguments and share the converse pairs, and each nogood is
placed as a conclusion (`chain/place-tuples!`).  See docs/nmtms.md, "A nogood placed as
a conclusion".

  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here

  nodes / premises / in / blocked / forced mono, out, void
  touched / touched-in / touched-new / touched-out           RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)

The dense truth-maintenance network — the `:tms :dense` option, the default since
0.9.0 (it holds the network in ~3.8× less RAM at corpus scale; docs/density.md).

The JTMS is **always resident**, so its footprint is a wall in its own right
(measured: ~467 B/node, which is ~43 GB at 100M nodes), and the decomposition
(`lein bench-jtms`) says exactly where the bytes are:

```
  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here
```

Two findings shape everything below.  **The per-node scalars are already free** —
stripping `:depth`, `:premise?` or `:datum` from the reference releases *nothing*,
because they are shared cached objects (small `Long`s, keywords, booleans).  So the
lever is not "shrink the fields", it is "stop having a map per node": a node here
is a bit in a bitmap and, where it has one, an entry in a primitive-keyed map.  And
**belief sets are the opposite regime from the index's postings** — `bench-postings`
found RoaringBitmap a *loss* (1.07-1.45x) on the index's millions of tiny postings,
while `:in` holds nearly every node and compresses 384x.  Both measurements are
right; density is the variable.

```
  nodes / premises / in / blocked / forced mono, out, void
  touched / touched-in / touched-new / touched-out           RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)
```

The depths, the two adjacency maps and the three justification columns keyed by id are
the fact-scaled half of that table, and the network reaches them through the
`TmsColumns` interface rather than as fields.  `HeapColumns` holds them in the fastutil
maps above.  Every relabel, sweep and mutation below is written once against the
interface, so an implementation that holds the six elsewhere runs the same fixpoint.

Two of those deserve their reasons.  **The defeat-classes are one bitmap** because
the lattice has exactly two elements (`vaelii.impl.strength` — monotonic > default,
and the reference already stores only the entries *above* the bottom), so "the
class map" is precisely "the set of monotonic datums".  **Adjacency reuses Phase
1's `IntPostings`** (a sorted `int[]` promoted to a bitmap past 128) rather than a
bare `int[]`: a node's supports are usually one or two, but the *consequences* of a
much-used premise — a rule's node lists every justification it licensed — grow
without bound, and an array-copy insert would make loading such a
rule quadratic.

## Why this is a second implementation and not a swap

`RoaringBitmap` is mutable, and the reference is an atom over one persistent map
whose all-or-nothing mutation `jtms_atomicity_test` pins.  A mutable bitmap inside
that value would break `swap!`'s retry semantics and let a reader observe a
half-applied relabel — so the dense structures cannot be dropped into the reference,
and the two ship side by side behind `vaelii.impl.jtms-protocol/Tms`.  That is the same shape
the index took (`:memory-columnar` is a whole second trie beside `KvIndexStore`),
and it carries the same obligation: the algorithms are duplicated here against the
dense structures, so `jtms_dense_oracle_test` proves the two answer identically
under randomized operation streams before either is trusted.

**Concurrency.** A `StampedLock` gives the incidental reader the consistent view the
single-writer contract owes one — "a reader thread beside a writer thread (the web
browser over a REPL's KB) is the supported shape" (docs/storage.md), and the atom-
over-persistent-map reference gives that reader a consistent view for free.  The dense
network mutates its bitmaps in place, so it earns the same guarantee with a lock, and
the lock is chosen so the engine's own single writer never pays for it.  Writers take
the exclusive stamp — serializing exactly as the reference's `swap!` retry does.  Point
reads (`in?`, the hottest call in the engine, one per candidate on the match path) run
**optimistically**: no lock in the steady state, since writes are bursty and reads are
the hot path, validated after the fact and redone under a shared read stamp only if a
write intervened or the lock-free read saw torn state.  Iterating reads take the shared
stamp directly — they already allocate O(nodes), so the acquisition disappears into the
materialization, and an unlocked walk over a bitmap a writer is rewriting in place could
tear.  A reader never observes a partially-applied relabel; it sees the state either
fully before or fully after, exactly as it would on the reference.  The lock is
**non-reentrant**: every protocol method below takes a stamp once and calls only
raw-field helpers (no method re-enters), and every read body is side-effect-free (so the
optimistic retry is safe).

**Precondition.** `ensure-node` precedes `add-justification`, and a justification's
antecedents already have nodes — which every engine path does.  (The reference
tolerates the violation by growing a malformed phantom node; neither implementation
is specified there.)

**Limit.** The bitmaps and the fastutil maps are `int`-keyed, so a handle or
justification id must fit a 32-bit int: the ceiling is 2^31-1 = 2,147,483,647.
Handles are allocated in assertion order and never reused, so this bounds a KB's
*cumulative* allocations (~2.1B), not its live node count — 21x the engine's 100M
target, but reachable by a long-lived writer that churns assert/retract for long
enough.  Crossing it throws `:type :handle-ceiling`, an actionable error naming the
ceiling and carrying `:remedy {:tms :reference}` (`check-handle!`, at the two entry
points a new id enters), rather than the bare "integer overflow" the cast would raise — and never a silent truncation
that would collide two handles, so belief is never corrupted.  A KB that expects to
churn past 2^31 pins `{:tms :reference}`, whose `Long`-keyed persistent maps have no
such ceiling.  This is measured in density.md.

A dense in-memory `KvBackend` (`vaelii.impl.kv`) — the `:dense` index axis, under either
record store (`:memory-dense`, `:disk-dense`).

The index's handle-set families (trie leaves, the context / functor / argument roots, the
rule and exception indexes) are the bulk of its RAM, and a bake-off across candidate
encodings found a **packed sorted `int[]`** ~5.6× denser than the
`PersistentHashSet<Long>` the memory backend stores, with `RoaringBitmap` winning only the
few large/hot postings.  So a handle set here is an `IntPostings`: an exact sorted `int[]`
while small, promoted to a `RoaringBitmap` once it crosses a threshold (dense for large,
O(log) add, fast intersect).  The trie's child-*label* set (`[:trie :children …]`) holds tokens —
including numbers — not handles, so it stays an ordinary set; counters stay `Long`s.  The
backend dispatches on the key tag.

`kv-intersect` narrows **in that representation** rather than in the sets it would make:
`RoaringBitmap/and` where both sides are hot, a sorted merge where both are cold, and a
probe of the cold side into the bitmap where the tiers differ, and a binary search of the
short run into the long one where neither is a bitmap.  Smallest posting first, and one
Clojure set built at the end at the size of the answer.  What that buys is not mainly
speed on the big case (hot ∩ hot at 32k: 29.2 → 0.56 ms) but the *shape* of the common
one: a query pins a rare argument on a hot predicate, and 4 handles against a root of n
went from 4.73 ms at n=32,000 to 0.0015 ms at any n — flat in the extent the argument
roots exist to avoid scanning.  `lein perf --only intersect-selectivity` is the gate on
that, and what cost is left tracks the answer rather than the columns, which is the
boundary contract and not the narrowing.

Off by default (`:index :dense`); proven set-equal to `MemoryKvBackend` by
`dense_kv_oracle_test`.  Single-writer: the int structures are mutated in place, and
`kv-members` / `kv-intersect` materialize a fresh Clojure set at the boundary so a caller
never holds the mutable structure.  Handles fit `int` through 2³¹ (≫ 100M).

A key-interning `KvBackend` (`vaelii.impl.kv`) for the columnar index's non-trie
families — the context root, the count tries ending in the context, the opposed members
by context, the exception index, and the inverted term index.

Those families are flat `structured-vector-key → handle-set` maps, and the columnar
measurement (`bench/…/densetrie.clj`) found their **boxed vector keys**
(`[:term-index term]`, `[:context-root ctx]`, …) to be ~150 MB — the majority of the
columnar index once the trie went native.  This backend keeps the *values* as
`IntPostings` (Phase 1's tiered
`int[]`/Roaring set) but collapses the keys: the term is interned to an `int` through
the **shared trie dictionary** (`vaelii.impl.tokens`) — so a predicate/individual gets
the same id the trie edges use — and the whole key becomes one packed `long`
(`family | pos | term-id`) into a single primitive `Long2ObjectOpenHashMap`.  No boxed
vectors, no HAMT nodes, one map.

It stays a full `KvBackend` so the existing composition (an embedded `KvIndexStore`
over it) is unchanged: only the recognized index families are int-routed; any other key
— a counter keyed by the vocabulary, a scalar, the contract test's synthetic keys —
falls back to a plain in-memory backend (in the columnar store the trie is native, so no
`[:trie …]` key ever reaches here).

**Every handle family routes**, the count tries' leaves included: an argument leaf's
`(pred, pos, ctx)` scope, and any other count trie leaf's context scope `(ctx, 0, ctx)`,
is interned to a dense id of its own (`argfam-id`) and rides the `pos` field, which
the flat families do not use.  The tries' child sets and every name set (the term,
slot and membership rosters, the keys a handle installs) route as packed keys too, their
members held as ids in the shared dictionary.  So the fallback holds only the
vocabulary's counters, and the fact-scaled mass is one packed map — or, under a
snapshot, one mapped run.  Single-writer, like every index;
`kv-members` / `kv-intersect` materialize a fresh Clojure set at the boundary — but
`kv-intersect` builds it at the size of the *answer*, narrowing through
`postings/intersect-postings` in whichever representation each posting is in, a mapped run
included.  Proven set-equal to `MemoryKvBackend` on the index families by
`dense_roots_oracle_test` —
which, like every behavioural check, cannot see a family that falls back when it should
route, since the fallback answers identically; `dense_routing_test` reads the
representation and covers that.

**Single-*threaded*, which is narrower than single-writer.**  The mapped-section fields
on `DenseRoots` are `^:unsynchronized-mutable`, so installing or thawing a snapshot
publishes through no barrier and a second thread may read this backend mid-install —
`mapped?` true against a `mkeys` it has not seen, say.  The atom- and lock-based
backends give an incidental reader beside the writer a consistent view; this one does
not.  Same trade as `vaelii.impl.columnar`, whose docstring states it: these fields are
read on the hot lookup path, and a volatile read there buys a guarantee the engine's own
single writer never needs.

The detector of the one nogood family a settle finds: the clashes argument preservation
infers between a stored claim and a known-true claim no one stored, each with the most
general contexts that read it whole, where `chain/place-inherited!` places it.  The
memo `:preserved-clashes` carries a clash whose inputs did not move.  See docs/nmtms.md,
"The inherited-clash memo".

The durable-store entry point: open (once per directory) a `DiskRecordStore` and/or a
`KvIndexStore` over a `DiskKvBackend`, take the single-writer lock, and wire what was
opened to the durability daemon.

**The two halves open independently.**  A KB's records and its index are chosen on
separate axes (`vaelii.impl.kb`), and only one of the combinations that reach here
wants both: `:disk-log` is durable records *and* a durable index, while `:disk-memory` /
`:disk-dense` / `:disk-columnar` keep the derived index in RAM and want the record store
alone — no index log, no index WAL, nothing written to the directory but the records.  So each
component is opened on first use rather than as a pair, and the registry records which
ones a directory actually has.  A directory opened both ways in one JVM therefore
shares its record store across both KBs and hands the RAM-index one no durable index
at all.

A process-global registry keyed by canonical directory mirrors the memory backend's
space registry: two KBs constructed over the same directory share one set of
stores — so a KB "restarted" over the same directory in one JVM (the recovery
tests) sees the durable records the first wrote, with its own fresh taxonomy/TMS, and
the file handles + durability registration + lock are taken once rather than leaking
across the suite's hundreds of KB constructions.  A true cross-JVM restart opens the
directory fresh and rebuilds the RAM state from the durable logs.

How a record is shaped on its way into a log frame, and back.

nippy freezes a Clojure record by writing its **type tag and every field name** into
the frame — so a store of 100M sentexes writes `vaelii.impl.types.sentex.LiteralSentex` and
`:sentence :context :id :strength` 100M times.  Measured on a large imported store,
that scaffolding is **56% of the store** (87 of 155 B/record) and it says nothing a
frame needs to carry: the field layout is a property of the code, identical in every
frame.

So a frame holds the fields **positionally** — a plain vector, the shape known here —
which is 1.85× smaller and needs no dictionary, no id allocation, and no new durable
ground truth (`lein bench-records`).  The codec is per *kind*, because each kind has
one known set of shapes: a sentex frame is tagged `literal`/`rule`, a justification frame
is a bare vector (there is only one shape), and provenance is an open application map
that passes through untouched.

**Reading is backward-compatible in both directions.**  `decode` dispatches on the
thawed frame: a vector is positional, anything else is returned as it thawed.  So a
store written before this codec reads exactly as it did (its frames are records), and
a plain map handed to `put-sentex` — which the tests do, and which is not a `LiteralSentex`
— round-trips as the map it is.

Decoding also **interns** the symbols it rebuilds (`sentex/intern-deep`), so a record
paged off disk shares the one vocabulary object per name with every other record and
with the in-memory store, rather than minting its own copy per fetch.  That matters
most for the records the hot cache retains.

**Tokenized bodies** are the second, opt-in step (`vaelii.disk.tokens`): the positional
frame still spells its sentence out in full, and the vocabulary — the same few hundred
thousand predicate and individual names — is written into every one of the frames.  A
tokenized frame replaces the s-expression fields with a varint byte string of ids from
the durable dictionary (`vaelii.impl.disk.tokens`), 2.6× smaller again.  It is a
separate pair of *frame tags*, not a format change: a store can hold plain and
tokenized frames side by side, so enabling it costs no rewrite and disabling it leaves
what is already written readable.

**No frame this codec writes carries a sign, and no rule frame carries a sentence.**  A
negative literal's sentence is `(not S)` and `sentex/negative?` reads that, so no
written frame holds a polarity field; a rule record holds its antecedent and consequent
and no sentence (`sentex/sentence-of` builds it), so a rule frame holds none either.
The older tags each carry one or both of those fields, and decoding reads past them.

Durability management for the disk backend.  Each disk store/kv registers itself
here on open; one daemon fsyncs every registrant on a tick (default 3 s), and one
JVM shutdown hook closes them all on exit.  Without it, a crash between manual
fsyncs loses everything since the last one.

Registration is capability-based — callers hand in `{:fsync :close :label}` (plus an
optional `{:compact :dead-ratio}` for background compaction), so this namespace does
not depend on the stores it drives (which would cycle).

Config (system properties): `vaelii.disk.sync-ms` (tick interval, 0 disables the
daemon), `vaelii.disk.auto-compact`, `vaelii.disk.compact-dead-ratio` (default 0.5),
`vaelii.disk.compact-min-interval-ms` (default 300000).  Every one is read through
`vaelii.impl.config`, which owns their domains and refuses a value outside one —
and the two the tick reads are why `config/check!` runs at the open: a refusal *here*
lands inside `fsync-all`'s `catch Throwable` below, which logs a class name every
three seconds and leaves auto-compaction dead.

Low-level file primitives for the on-disk backend.

- Append-only `.log` files hold length-prefixed nippy frames.
  Frame layout: `[len: i32 big-endian][nippy-bytes]`.  The offset returned from
  `append-record!` points at the len prefix.
- `.idx` files are fixed-width arrays of 24-byte slots, indexed by id.
  Slot layout:
    bytes  0..7  offset (i64, -1 = empty, -2 = tombstone)
    bytes  8..15 length (i64)
    bytes 16..19 flags  (u32; bit 0 = the premise bit is meaningful, bit 1 = premise,
                         bits 2..3 = a premise's strength rank, 0 when unrecorded)
    bytes 20..23 gen    (u32, reserved — written as 0)
  Reads rely on the OS page cache; writes overwrite the slot in place.
  A slot is read in **one positional channel read**, not a seek plus four primitive
  `readLong`/`readInt` calls — a `RandomAccessFile` is unbuffered, so each of those is
  its own syscall and moving 24 bytes cost six of them (measured: 52% of a warm
  record fetch, `lein bench-records`).
- `.nippy` files hold whole-blob metadata (counters, the premise set).  Callers
  rewrite them atomically via `write-nippy-atomic!`.

**Shared-pointer invariant.**  A seek→read/write pair on a `RandomAccessFile` uses that
object's single shared file pointer, so any access to a store's live RAF must hold the
owning kind lock; the disk adapters take a per-kind lock around every such touch (write,
`force!`) for exactly this reason.  The *read* primitives here (`read-slot`,
`read-record`, `read-record-sized`) are positional `FileChannel` reads instead — they
name the file offset in the call and never touch the pointer, so they neither disturb a
concurrent seek nor need one of their own.

Compression: frames freeze under the nippy compressor named by the
`vaelii.disk.compress` system property (`lz4` | `zstd` | `none`); default none.
nippy reads the compressor id from each frame header, so mixed frames thaw
correctly.  Durability: `vaelii.disk.fsync=dsync` opens logs `rwd` (O_DSYNC) so
every append is synchronous — off by default (the durability daemon fsyncs on a
tick instead).

A **mapped snapshot** of the columnar index, which pages its cold tail to disk
instead of holding all of it in heap.

`:disk-columnar` keeps durable records and rebuilds the derived index on every open.
That rebuild is O(records) — measured at 5.6 s for 313k, ~30 min at 100M — and the
rebuilt structure is then wholly resident, which is the wall the scale plan names.
This writes the compacted index to disk once and maps it back, so an open reads bytes
and the fact-scaled postings live in the page cache rather than the heap.

## The design is a snapshot, not a store

The index is **derived state**: `reindex` rebuilds every entry from the records.  That
is what makes this cheap — no write-ahead log, no op log, no crash-consistent mutation
protocol, no bucket directory.  It needs a *snapshot* that can be thrown away and
rebuilt whenever it is in doubt, and "in doubt" resolves to `reindex` in every case.

It is also why there is no directory to page.  A flat-map index keys every trie node by
a boxed vector of its whole path prefix, so an out-of-core design over it has to page
the keys themselves; the columnar trie has no keys at all — a node's identity is its
`int` id and its position in the parallel arrays *is* the directory.  `columnar/compact!`
already produces exactly the arrays this writes.

## What is written

Under `<dir>/index/`, four things:

* `trie.csr` — the trie's six CSR sections (`fcounts` `foffsets` `fedge-tok`
  `fedge-tgt` `fleaf-off` `fhandles`), each a raw little-endian `int` run behind a
  header naming the counts.
* `roots.csr` — **every** root family (the context roots, the predicate extent, the
  argument roots, the term, rule and exception indexes) as the same CSR shape over
  `dense-roots`' packed `long` keys: sorted keys, an offset column, one shared handle
  run (an argument node's run holds context token ids).  Plus the scope table the count
  tries' leaves decode through — one `(predicate, position)` pair, `(predicate, position,
  context)` triple or `(context, 0, context)` context scope per entry, as three columns
  with -1 for a pair's context, indexed by the scope id their packed keys carry
  (`dense-roots`' `argfam-id`).  The
  table is vocabulary-scaled and rides this file because this file's key column is its
  only reader: written in one pass, discarded as one unit, so the two cannot drift.
* `roots-fallback.nippy` — everything the routed families do not claim: the counters
  keyed by a predicate, functor, rule key or kind, which are vocabulary-scaled.  It is
  still index truth — the predicate extent's count is what the planner prices a scan
  by — so its entry count and byte length ride the meta and are checked on open like
  the CSR sections' lengths, and its load is strict (`read-fallback`).
* `tokens.log` — the durable token dictionary the `int` edges cite, in
  `vaelii.impl.disk.tokens`' format (append-only, id = append position, content-keyed,
  first-writer-wins, never reused).  That module is reused rather than a second
  dictionary format minted: persisting the trie's `int` edges is precisely the format
  `vaelii.impl.tokens` names as its durable variant.

**One file per structure**, not one per section.  A structure is mapped or discarded as
a unit, so per-section files would multiply the crash window by six for nothing; the
section table in the header already names the offsets `map` needs.

## The residency split

`scale-100m.md`'s rule is *never page the walk* — the worst measured index pathology was
the leading-variable trie fan, 18,512 lookups for one query, and a disk seek is worse
than the round trip that pathology was made of.  So the load is deliberately asymmetric:

* **resident** — the CSR skeleton (`fcounts` `foffsets` `fedge-tok` `fedge-tgt`), the
  roots' key and offset columns, the scope table, the token dictionary, and the
  fallback blob.  Every one of them is path- or vocabulary-scaled.
* **mapped** — `fleaf-off` / `fhandles` and the roots' handle run.  Each posting is
  touched only when its own term is queried.  Cold by construction.

**No handle family is an exception to that split.**  The resident half is where the
index's *shape* lives and the mapped half is where its mass lives, and the line between
them is the line between what the vocabulary sizes and what the facts do.

With `mmap` the OS page cache is the residency policy, which is the point — but only
because the skeleton stays hot.

## Validity is the whole design

The failure to fear is a stale snapshot that passes its check: one can be perfectly
self-consistent and describe a KB that no longer exists.  So the stamp covers the
**records**, not the snapshot's own bytes, and it is checked on **every** open — never
behind a flag.  Three things must agree or the snapshot is discarded and `reindex` runs:
the format and `kv/index-layout-version`, the byte-order tag (the sections are always
little-endian, so this guards a future format that changes the order, not this machine's
architecture), and `record-store/slot-fingerprint`.  The
decision carries a reason from `import`'s vocabulary — `:absent` `:layout-changed`
`:records-differ` `:entries-truncated` `:unsupported-platform` — because a rebuild
nobody can explain is a rebuild nobody notices.

## The platform

The commit is an atomic rename over a file this process has mapped, which Windows does
not permit, so `:index :snapshot` is **refused** there (`enabled?`) and an image
found on disk is discarded as `:unsupported-platform` rather than read and never
refreshed.  Nothing else in the durable store is implicated: the logs are appends and
the slots are positional writes.

A commit is one atomic step: the sections are written to temps and fsynced, the meta is
**deleted**, the temps are renamed into place, and the meta is written last.  Its
presence is the commit point, so a crash anywhere leaves no meta, and no meta means
reindex.

## What it measured

1.72–1.84× off the index's resident heap and a 1.5× faster open, on a corpus whose
vocabulary is fixed — and resident heap that still grows with the facts, because the
token dictionary is fact-scaled and the CSR skeleton is path-scaled.  The acceptance
property it was built for does **not** hold, which is why it is off by default.

The **log index** — the `:disk-log` half of `:disk-log` and `:pg-disk-log`: a
`KvBackend` (`vaelii.impl.kv`) over a durable write-ahead log.

The index is derived state (small next to the records, and `reindex` can rebuild it
from the records alone), so the disk KV keeps the whole key→value map in RAM — a `Long` at
each counter key, a set at each set key, exactly the shape `MemoryKvBackend` holds —
and durably logs every mutation to a `kv.log` of length-prefixed nippy frames.  Reads
are the in-RAM map, so `kv-members` / `kv-intersect` are the same reference /
`set-intersection` operations the memory backend does — the disk only buys durability.

**Logical (op) logging.**  A frame is the write op itself — `[:add-to-set k m]`, `[:remove-from-set k
m]`, `[:put k v]`, `[:delete k]`, `[:increment k]`, `[:decrement k]` — not the resulting value.  A
set-add logs the one added member, O(1), so a bulk load of N members into one root
writes O(N) WAL bytes; new-value logging re-serialized the size-i set on the i-th add
and cost O(N²).  On open the log replays by folding each frame through `kv/apply-op`, the
same function that applies a live op.  `compact!` rewrites the log as one `[:put k v]`
op per live key, so every frame — ordinary or post-compaction — is a uniform op and
the reader needs no snapshot-vs-delta discrimination; it also bounds replay length and
reclaims the delta frames (compaction is this store's snapshot cadence).

Crash-safety: the open truncates a torn tail (a partial op frame is dropped whole,
never half-applied), and compaction rewrites the log crash-safely
(`files/recover-compaction!`).  A frame that does not thaw with frames after it is
damage inside the log (`files/scan-log`'s `:damaged-frame`): the replay keeps the ops
before it and flags the store `damaged`, which the open gate answers by rebuilding the
index from the records.  All log writes hold the backend lock (the RAF file pointer is
shared).

Single-writer guard for the on-disk KB.

The disk record store and the disk KV index have no cross-process file locking:
two JVMs appending to the same logs tear them.  This namespace takes an OS advisory
`FileLock` on `<dir>/.vaelii.lock` when a disk backend opens, and fails fast if
another live JVM already holds it.  This is the single-writer contract
(docs/storage.md) — one process holds the KB.

The lock is exclusive and ref-counted per canonical directory (the record store and
the index share one dir, so both acquire and the last release drops it).  The OS
releases it when the JVM exits, so a crash leaves no stale lock to reap.  Set
`vaelii.disk.lock=false` (system property) to disable in a trusted single-host
scenario.

The record store on disk — an implementation of `RecordStore` over per-kind
log/idx pairs (`vaelii.impl.disk.files`).

Three int-keyed kinds — sentexes, justifications, provenance — each a `.log` of
length-prefixed nippy frames plus a `.idx` of fixed 24-byte slots mapping handle →
log offset.  A frame holds its record's fields **positionally**
(`vaelii.impl.disk.codec`), so the type tag and field names are not rewritten into
every one of them; a frame written before that codec still reads, as its own shape.  A record is **paged** from disk on `get`: read the slot, read the frame
it points at, thaw it — two positional reads, no seek, and the records do not sit in
RAM.  What does sit in RAM per kind is the set of live handles (so enumeration is
O(1)), rebuilt from the idx on open, and a **bounded LRU of hot records** in front
of the read (`vaelii.disk.cache`, 0 to disable).

That live set is a **compressed bitmap** (`vaelii.impl.roster`'s `LiveRoster`), not a
`PersistentHashSet<Long>`.  Handles are minted in assertion order, so a live set is a
strided run of longs with holes where records were deleted, and the boxed set retains
48–75 bytes a handle for it — 9.47 GB at 100M records, the second-largest resident row
in the engine (`docs/density.md`).  A bitmap answers all four things the
set is asked (membership, iteration, cardinality, a first handle) at about a bit a
handle.  What it costs is a monitor: the bitmap is mutated in place and is not
thread-safe, so a read of the live set takes the kind lock, exactly as a write does —
see the two-monitors section below.

`next-id` is a monotonic counter recovered as `max(the counters blob, 1 + the
highest slot id across the record kinds)` — the highest slot id is stable across
deletes (a tombstone keeps its slot) and across compaction (slot ids are preserved),
so a handle is never reused even if the counters blob is stale after a crash.  Within
a session every write holds the same bound (`clear-counter!`), because a record can
arrive carrying its own `:id` and nothing re-reads the slots until the next open.

A premise is exactly a sentex whose `:strength` is non-nil (the strength lives on
the record, as on every backend), so the premise set is derived from the durable
records — rebuilt on open, maintained in lockstep by mark/unmark — rather than
stored separately.  Rebuilding it does not mean *reading* them: every write records
the answer in its idx slot's flags, so the open reads the set off the slot walk it
already makes.  A slot that does not carry the bit sends that one handle to its
record, and the record is authoritative wherever both speak (`rebuild-premises!`).

The premise's **strength rank** rides the same slot flags (bits 2..3), so
`premise-strength` — read once per premise on every `recover` — answers off the 24-byte
slot instead of paging the whole record for one keyword.  A slot carrying no rank (a
non-premise, or one older than the bits) falls back to the record, the same
no-format-bump story as the premise bit itself (`f/slot-strength`).

Recovery on open: finish any interrupted compaction, truncate a torn log tail, then
tombstone any slot whose frame now extends past the log (`validate-idx-tail!`).
Crash-safety rests on the write ordering (append the frame, then point the slot at it)
and on `files`' crash-safe compaction.  Where it stops is the slot itself: 24 bytes do
not divide a page, so a crash can leave one spliced from two writes, and a splice still
pointing inside the log is reported as a thaw failure on that handle rather than caught
here (`f/validate-idx-tail!` says what it does and does not cover).

The tail is located from the frame *lengths*
(`files/log-tail-offset`) and nothing is decoded to find it — and a clean `close!`
records each log's length, so an open whose log is still that long skips even the walk.
The marker is consumed here, so it never describes a store in use; every disagreement
falls back to the walk.

Every RAF touch holds the owning kind's lock.  A write or `force!` must, because the
file pointer is shared (see `files`' shared-pointer invariant); a read is positional
and need not, but still does, because that is what serializes it against a concurrent
append and its slot write.

**Two monitors, and which resident field sits under which.**  Three threads touch this
store — the writer, the durability daemon (`fsync`, every few seconds) and the
compaction executor — so the resident state is not the writer's alone and a field
mutated outside a monitor is one a reader can catch mid-pair.

- The **kind lock** covers that kind's log, its idx, and the resident state derived
  from them: `live-ids`, `live-bytes`, the hot-record cache, `compacting` and
  `failed`.  A store, a kill, a batch and the compactor's reconcile each take it once
  and do both halves inside it, so an id is never live to a reader while its slot says
  tombstone, and the compaction delta set is never cleared under a writer folding an id
  into it.

  It covers `live-ids` on the **read** side too, which the other three do not need: the
  roster is a bitmap mutated in place, so a tally or an enumeration taken beside a
  concurrent `addLong` reads a structure mid-edit.  A read that hands the set onward
  takes a `roster/live-snapshot` inside the lock and lets go of it — the copy costs the
  bitmap's size, not the corpus's, which is what makes holding the writer's monitor for
  an enumeration affordable at all.
- **`counters-lock`** covers the three that move together and belong to no kind: the
  handle `counter`, the `counters.nippy` blob, and `synced-seq` — read and written by
  `fsync` on the daemon's thread and by `clear-records!` on the writer's.  Its own
  monitor rather than a kind's, because a whole-file blob rewrite held inside a kind
  lock would put a record append behind it every tick that minted a handle.

`premises` is a `LiveRoster` too, and sits under the **sentexes** kind lock for reads
and writes alike, because a premise is a sentex handle.  It is not folded into
`store!`'s acquisition: a premise joins the roster after its record lands, in a second
acquisition, so a failed write leaves no handle in `premise-ids` whose `get-sentex` is
nil.  The compactor's `drop-lost!` removes from it only when compacting the sentexes
kind, under the lock it already holds.

A **durable** token dictionary for a disk store: `symbol/keyword ↔ int`, append-only,
ids assigned in append order and never reused.  It is what lets a record frame spell
its sentence as ids rather than names (`vaelii.impl.disk.codec`), which is 2.6× smaller
than the positional frame it replaces — the vocabulary is written once here instead of
once per frame in all 100M of them.

**The ordering that makes it safe.**  A frame referencing an id the dictionary cannot
decode is unreadable data, so the dictionary must never lag the records that cite it.
Two rules give that, and neither costs a write:

- a token is appended **before** the record frame citing it (`emit!` interns as it
  encodes, which happens before the frame is written), so the token log leads the
  record log in *write* order at all times;
- `fsync` fsyncs this log **first, holding the sentexes kind lock**, so nothing is
  appended between the two fsyncs.  Every record durable after a tick therefore has
  its tokens durable too.

fsyncing *per new token* would also give the ordering, and is what this did first —
but it makes a cold load fsync-bound (measured: ~217 records/s, since a new token is
not rare during one).  Between ticks the two logs can still skew on a machine crash,
exactly as the record log and its idx can; `open-record-store` repairs it the same way
it repairs those, by tombstoning a record whose ids the dictionary does not hold.

**Only symbols and keywords are interned.**  Those are bounded by the ontology.
Numbers and strings are not — a KB of measurements would mint a dictionary entry per
distinct value — so `codec` carries them beside the id stream as literals instead.

Ids are **content-keyed and first-writer-wins**, so they are stable for the life of the
store; the id *value* depends on first-encounter order, which nothing above this reads.
Tokens are never deleted (an id must keep decoding), so the log has no dead frames and
needs no compaction; only a whole-store `clear-records!` empties it.

Writes take the log's lock (there is one writer, and the append must not interleave);
the *reverse* map is an atom holding a vector, so a decode — which runs on every fetch,
under a different lock — reads it without one and still sees a safely published entry.

Qualitative distance: seven classes tiling `[0, ∞)`, three derived ranges, composition
computed from the class bounds by the triangle inequality, and the calculus and prover
over `vaelii.impl.qcn-kb`. See docs/space.md.

Interval duration arithmetic: `DurationProver` answers `(totalDuration (list I1 I2 …) D)`
and `(overlapDuration I1 I2 D)` from the stored `(length I M)` facts, on `[lo hi]`
magnitude bounds, with the overlap sharpened by `stp/overlap-window-with-support`.
Opt-in, as the `:duration` reasoner.  See docs/duration.md.

The visibility `except` roster: which handles a believed `except` hides from a
reading context, with the meta-except cascade; and the read walk that applies the
placed `defeat`s at a reader.  See docs/exceptions.md and docs/nmtms.md.

The change feed's registry and its accumulator — the leaf boundary a settle files its
relabelled region into, and the one place a listener list lives.

An application driving the KB otherwise learns that belief changed only by asking
again, which misses whatever happened between two asks and costs the most on the KBs
where the least is moving.  Everything a feed needs is already computed: a settle
knows the **region** it relabelled and which of that region was believed when it
first touched it (`jtms/touched` / `jtms/touched-in`), and it throws both away.  This
namespace catches them.

**Why here.**  `vaelii.impl.observe` is the precedent and the shape is the same: a
choke point deep in the stack has to reach a consumer defined above it, so the
indirection is a leaf both can see.  What differs is the altitude.  `observe`'s
observers fire on *storage*, which is what an alpha memory mirrors; a feed is about
**belief**, and belief is decided at settle time — an `assert` can store a sentex whose
label several later justifications settle.  So nothing here is notified from
`kb/create-sentex`, and the region is the unit rather than the record.

**What is split where.**  The registry, the accumulator and the reentrancy guard are
here, on the KB's `:feed` atom.  Turning a region into the `{:believed-added
:believed-removed}` entries a listener receives is `vaelii.core`'s job — those are
`preview`'s entry shapes, built from `why-not` and the supporting justifications, and
they belong beside the code that already renders them.  `core` installs that renderer
with `install-dispatch!` when it loads, and `deliver!` calls it.

**What a KB with no listener pays.**  `note-region!` is one deref and a `seq` on the
listener vector, and nothing accumulates.  A KB *with* one pays per relabelled region
— the same region a `preview` diffs — and never per stored sentex; see
`lein perf`'s `feed-listener-scaling`.  See docs/feed.md.

The per-instant functionality audit for fluent-carried values.

`functional` (checks / special) enforces at-most-one-value over the **bare** literals of
a marked predicate: two co-believed `(P a v1)` / `(P a v2)` derive `(equals v1 v2)` and
merge.  A value carried the event-calculus way never appears in a bare literal — it rides
inside a fluent NAT under `initiates`, and `holdsAt` derives it at a moment (docs/time.md,
CxChange).  So the equality closure never sees the pair, and per-instant functionality —
a function that has at most one value for one subject at any single instant — is enforced
by nothing at assert.

Whether two fluents overlap at an instant follows from `initiates`, `terminates` and the
clipping closure, and is not known when a fluent is asserted.  So this reads it on demand,
the shape `vaelii.impl.predall/specified-violations` uses for the analogous reason: an
audit reports, it does not mutate belief.  A merge-eligible clash (two symbol values) is
reported as `:merge` and a non-mergeable one (two numbers or strings) as `:contradiction`,
mirroring `functional`'s own split, and the caller decides what to do with the report.

Reached from outside through `vaelii.core/functional-at-instant-violations` and
`vaelii.core/all-functional-at-instant-violations`, thin delegations to the readers here.
This namespace sits **below** `vaelii.core`, which requires it, so no delegation runs
through `vaelii.impl.wiring`.  The fact reads are `vaelii.core/ask`'s per-context step
(`quasiquote/ask-prepared`); the one read that needs a rule — `holdsAt`, which the
registry does not expand — runs the node engine directly (`inference/solutions`) at a
bounded depth, the below-`vaelii.core` form of the read `vaelii.core/query` runs.  The audit
still answers what a user's read answers: it passes only concrete contexts, and the `genlCx`
ancestor scoping is applied in the matching layer below (docs/namespaces.md,
"The layering").

{:engine-dump vaelii.foreign.engine/reader
 :cyc-corpus  vaelii.foreign.cyc/reader}

(when-let [r (foreign/reader :engine-dump)] ((:decode-frame r) frame))
((:load-dir! (foreign/reader! :cyc-corpus)) kb path opts)

Formats vaelii **reads and does not write**, and the plugin extension point they arrive through.

A foreign reader is a bridge, not a feature: an engine-dialect dump and a translated
OpenCyc corpus are how knowledge that predates this build gets in, and each one is
finished the day its corpus has been converted once into the format we do write
(`vaelii.impl.io.export`).  Carried in-tree it would be code that must keep compiling,
keep passing tests, and keep being read by whoever changes a record shape, in exchange
for nothing.  So no reader ships here.  This engine reads its own dump format and
nothing else, and the bridges are **separate artifacts** that teach it a format when
they are on the classpath — `vaelii-foreign` is the one we publish.

## What a plugin does

It ships a namespace holding a `reader` var and one resource, `vaelii/foreign.edn`,
which is a map of `kind -> the var holding its reader map`:

    {:engine-dump vaelii.foreign.engine/reader
     :cyc-corpus  vaelii.foreign.cyc/reader}

Every copy of that resource on the classpath is read and merged, so a build reads the
union of the bridges it was given and several plugins compose without knowing about
each other.  A manifest is **edn**, so it declares a name and can never run code, and
the symbols in it are resolved with `requiring-resolve` **on use** — a plugin's
namespaces are loaded when something actually asks for its format, and no reference to
one exists in this build's compile-time graph.  `register` is the same registration
done in code, for an embedding application that has the reader in hand.

Nothing else in this repo names a reader namespace, and nothing here has to change to
add or drop a format.  A build with no plugin refuses a foreign dump or corpus **by
name** instead of half-reading it, which is this file's job.
`foreign_contract_test` is what keeps all of that true.

## Asking for a reader

A caller asks by kind and gets a map of functions, or nil:

    (when-let [r (foreign/reader :engine-dump)] ((:decode-frame r) frame))
    ((:load-dir! (foreign/reader! :cyc-corpus)) kb path opts)

`reader` for a path that has a fallback (the importer reads its own dialect either
way), `reader!` for one that does not (there is no other way to load a corpus).  What
a reader map holds is the reader's own business — the extension point carries capability, not a
protocol, because two foreign formats have nothing in common but being on the way
out.

The `do/` imperatives — the one shape given to `assert` that is neither a fact nor
a rule but an *instruction*: run a labeling / classification and return its result,
storing nothing.  `assert` dispatches a `do/` form here (`run`) before any naming or
well-formedness check, since those expect a sentence.

This is not part of the assertion write-path — it is a separate feature (answer-set
labeling, docs/labeling.md) routed through `assert` for one entry point — so it lives
outside `vaelii.core`.  The backing functions live under `vaelii.impl.asp.*`, which
requires the engine, so they are resolved **lazily**: a static require would be
circular, and the resolve keeps ASP optional (a build without a backend still loads,
and the backend choice is made inside the resolved fn).  An unavailable build throws a
legible error rather than failing to load the engine.

node:   [ L₁ … Lᵢ … Lₙ ]                        σ
rule:   A₁…Aₖ ⟹ C,  with  b = unify(Lᵢ, C)
child:  [ b(L₁) … b(Aᵢ…) … b(Lₙ) ]              σ ∪ b

A **backward** chainer whose state is a set of nodes ordered by cost — not
`vaelii.impl.chain`'s *forward* agenda, which is a queue of newly believed data
waiting to be matched against rules.  This one runs from a query towards the facts,
and what its agenda holds is unfinished proofs.

The other backward chainer is path-structured, walking an explicit goal stack
(`res/prove-from`).  Here
the unit is a **node** — a whole conjunction plus everything accumulated to reach it —
and expanding one is a single rewrite:

    node:   [ L₁ … Lᵢ … Lₙ ]                        σ
    rule:   A₁…Aₖ ⟹ C,  with  b = unify(Lᵢ, C)
    child:  [ b(L₁) … b(Aᵢ…) … b(Lₙ) ]              σ ∪ b

The rule's antecedents under the head unifier are the **residual** — what is left to
prove if this rule is the one that fires — spliced in where `Lᵢ` was.  Applied
repeatedly, that transformation is the whole search: every node is the query rewritten
through some sequence of rules, and a node whose conjunction solves against facts
alone is a completed proof.

Two things follow from the state being a value rather than a call stack.  A stop
between two expansions leaves an **agenda**, not a continuation closure, so a bounded
run is `budget/collect` over the result stream and nothing else.  And the tree is an
artifact that outlives the search, which is where dead ends and "why did this cost so
much" answers come from.

A third follows from the frontier being a priority queue: **which** node pops next is a
policy rather than a structure, and it lives in `vaelii.impl.tactics` — one additive
estimate whose signs the caller picks.  Every tactician returns the same answer set;
what differs is when.

**What it is good at, measured.**  The residual stays *symbolic* — `(anc ?y ?z)` is
not re-asked once per binding of `?y`, it is rewritten once — so the node count is a
function of the rule graph and the depth bound, not of the data.  Over a kinship DAG
the same seven nodes answer 16 leaves and 64 of them, and an open query runs 2-6x
faster than the DFS because each node's conjunction is one planned join rather than a
tuple-at-a-time walk.  A **bound** query is the other way round (2-4x slower): the
rewrite ignores what the caller already knows and computes the relation, then filters.
A conjunctive query is 2-3x slower still, because a k-literal conjunction has more
ways to be rewritten than a single goal does.

**What it cannot do.**  Termination here is the depth bound, and nothing else.  The
DFS is data-driven — it substitutes as it goes, so a chain of length n terminates
after n steps whatever bound it was given — while a symbolic residual grows a conjunct
per rewrite and would grow forever.  So `*max-depth*` is a real ceiling: a derivation
deeper than it is not found, and the depth a query needs is a property of the *data*.
Answer-set parity with `prove` therefore holds up to the bound and not past it, which
is why the selector defaults to `:dfs` (`core/*query-engine*`).  Iterative deepening
is what would close that, and it is not built.

See docs/inference.md.

(transitiveInArg        P n R)   ; a stored (P … w …) licenses (P … a …) when (R w a)
(transitiveInArgInverse P n R)   ; …licenses it when (R a w)

**Argument-position preservation** — when a claim about one term licenses the same
claim about another.

`(largerThan dog cat)` says something about two *kinds*.  Whether it also says
something about a golden retriever and a maine coon is not decidable from the
sentence: it depends on whether the relation distributes over the kinds' members.
Some relations do (`disjoint` — subtypes of disjoint types are disjoint) and some
emphatically do not (a chihuahua is a dog, a maine coon is a cat, and the maine coon
is bigger).  So it is **declared**, per predicate, per argument position:

    (transitiveInArg        P n R)   ; a stored (P … w …) licenses (P … a …) when (R w a)
    (transitiveInArgInverse P n R)   ; …licenses it when (R a w)

`R` is any **transitive** relation — `genl` and `genlCx` through their cached
closures, or a predicate declared `(transitive R)` walked over stored facts.  A
declaration over anything else is refused at assert
(`wff/arg-preserving-problems`): the reach is walked to a fixpoint, so a relation
that was never said to compose would have transitivity *manufactured* for it, and
`(arg transitiveInArg 3 transitive)` cannot say so — arg is
open-world, and an untyped relation cannot violate it.  Naming the relation is what
keeps this from being a `genl` special case: an argument can equally be preserved
along `partOf`, `connectedTo`, or anything else transitive.  `transitiveInArg` carries
the claim along `R`'s arrow and `transitiveInArgInverse` against it, the directions of
Cyc's `transitiveViaArg` / `transitiveViaArgInverse`; the two names exist so neither
direction requires declaring an inverse predicate that has no other purpose.

Several declarations may name one argument position; their reaches **union**, since
each independently licenses the claim.

## Preservation stays on one side of the type/instance line

`genl` relates **types**, so `(largerThan dog cat)` preserved along `genl` reaches
`golden_retriever` and `maine_coon` and stops there.  It says nothing about Rex and
Whiskers, and that is not a gap here to fill: `relation_kind` is a `disjoint_metatype`
over `type_relation_predicate` and `instance_relation_predicate`, so one predicate
symbol relates kinds *or* instances and never both.  A `largerThan` that inherited
across the line would be a predicate of both kinds at once, which the KB's own
meta-ontology refuses.

Preservation moves an argument along a relation, leaving the predicate and the level
it lives at alone.  Crossing the line is a *different* claim — it links two
predicates and has a quantifier reading to pin down (every member? some member?) —
and the vocabulary for it is `(typeToInstancePred TypePred InstancePred)`, which
records the pairing for a reader and is inferred from by nothing.

## Specificity, and why it is not the deleted axis

The interesting case is a claim that inherits *and* a more specific claim that
disagrees.  `(typicallyLargerThan dog cat)` reaches `[chihuahua maine_coon]`;
`(typicallyLargerThan maine_coon chihuahua)` is stated directly.  The stated one
wins, and the general one simply **does not fire for that pair** — undercutting, not
defeat.  Nothing is derived, so there is nothing to arbitrate.

That matters, because `docs/nmtms.md` deleted genl-based specificity as an
arbitration axis on the grounds that it was inference *about* the knowledge rather
than *from* it: it scored a type by the size of its up-closure, a numeric proxy that
tied silently whenever the exception was not keyed on a narrower type.  Nothing here
reconstructs an ordering.  Two claims are compared along the **very relation the
inheritance travels down** — `[maine_coon chihuahua]` is below `[cat dog]` because
`(genl maine_coon cat)` and `(genl chihuahua dog)` are edges the KB holds.  Claims
that are genuinely incomparable are not ranked at all; they come back `:ambiguous`,
which is the same answer the engine gives every other unresolvable clash.

## Strict versus typical, for free

A `:monotonic` claim is **never** undercut.  Strength already propagates from a
justification's antecedents, so `(largerThan dog cat)` asserted `{:strength
:monotonic}` inherits as known-true and a contrary specific claim is a
contradiction, while `(typicallyLargerThan dog cat)` at the default `:default`
inherits defeasibly and yields to the specific claim.  One declaration, both
behaviours, and the difference is stated where it belongs: on the claim, not on the
vocabulary.

A stored `(not (P a b))`, and a stored `(P b a)` under an `asymmetric` mark on `P` or
above it, are paired with the inherited claim by `discovery/preserving-nogoods`, whose
members are the general claim and everything the reading rests on, so `decide/verdict`
weighs the set and the weakest member decides (`clashing-claim` and `converse-claim`
below, `docs/inherit.md` for the readings).

Ground goals only.  An open argument is left to the fact and rule provers, in the
shape `different` and the NAF operators already use — enumerating it would mean
walking the inverse reach of every stored witness, which is a different and much
larger question than the one a closed goal asks.

Store mutation is the boundary: the two choke points everything that stores or
removes a sentex must pass through.

Fourth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): the table of what each special predicate *means* lives below in
`vaelii.impl.special`; what lives here is the guarantee that its arms — and the
exception re-check queue they feed — are never skipped.  exceptWhen correctness
depends on every mutation path posting a re-check.  Scattering that call across the
mutation sites makes a missed one invisible — the failure mode is stale excepted
conclusions, silently, and the next mutation path (a bulk load, a new merge) is one
forgotten call from that bug.  So the sequence is stated once per direction:

  sentex-added     integrate through the table + queue the re-check — the assert
                   path's reflection of a sentex that just landed (storage and
                   indexing having happened in `kb/create-sentex`, which is the
                   store-side half of the same boundary)
  sentex-removed!  disintegrate + unindex + delete the record + queue the
                   re-check — the one teardown, shared by `retract!` and the
                   excepted-conclusion sweep
  symmetrize-      the third direction, and the only one that moves a record
    existing       without moving a handle: a late `(symmetric P)` mark re-spelling
                   the rows stored before it and folding a mirrored pair into one
                   (see the section at the foot of this namespace)

The derivation path's twin (`special/derived-sentex-added`) sits beside the table
instead, because the equality arms are themselves derivation sites and must reach
it from below.  The triggers that are *not* store mutations stay explicit at
their own sites: a taxonomy edge change (posted inside the genl / genlCx
arms — the trigger is the closure moving, not the sentex), rule indexing (posted
in `special/index-rule-sentex` — the trigger is the rule gaining an exception to
evaluate), and `recover` (nothing about blocking survives a restart, so it
re-queues everything wholesale).

Bounded, read-only KB integrity reporting: the passes `kb-integrity` runs under a work
meter (`vaelii.impl.budget`).  `vaelii.core` requires this namespace; it requires
`predall` and `provers`, which also sit below `vaelii.core`.  See docs/integrity.md.

Allen's interval algebra — a relation algebra over the generic constraint network in
`vaelii.impl.qcn`, and the third alongside the RCC-8 topology of `vaelii.impl.space`
and the cardinal directions of `vaelii.impl.orientation`.  Those two say where things
are; this one says *when* they are, and about intervals rather than instants: an
interval has extent, so two of them can meet, overlap, or nest, and not merely precede
one another.

The thirteen base relations are jointly exhaustive and pairwise disjoint, so exactly
one holds of any two intervals.  Each is a claim about the four ways their endpoints
can compare — writing an interval as `[start end]` with `start < end`:

  :before        a-end   < b-start
  :meets         a-end   = b-start
  :overlaps      a-start < b-start < a-end < b-end
  :finished-by   a-start < b-start,  a-end = b-end
  :contains      a-start < b-start,  a-end > b-end
  :starts        a-start = b-start,  a-end < b-end
  :equal         a-start = b-start,  a-end = b-end
  :started-by    a-start = b-start,  a-end > b-end
  :during        a-start > b-start,  a-end < b-end
  :finishes      a-start > b-start,  a-end = b-end
  :overlapped-by b-start < a-start < b-end < a-end
  :met-by        a-start = b-end
  :after         a-start > b-end

Six of them pair off with their converses (`:before`/`:after`, `:meets`/`:met-by`,
`:overlaps`/`:overlapped-by`, `:starts`/`:started-by`, `:during`/`:contains`,
`:finishes`/`:finished-by`); `:equal` is its own converse and the algebra's identity.

Intervals are **stored as ordinary sentexes** — the thirteen named binary predicates
(`before`, `meets`, `during`, …), plus seven derived predicates (`precedes`,
`subintervalOf`, `sharesTimeWith`, …) that each name a *disjunction* of them.
Intervals are ordinary individuals; nothing about them is special, and nothing here
reasons about clocks, dates or durations — only about order and containment.

The calculus reads every asserted interval relation visible from a context into a
qualitative constraint network — `{[i j] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all thirteen — and `qcn/path-consistent` tightens it to a
fixpoint.  the prover then answers a goal `(P i j)` by **entailment**: it holds iff
every relation still possible between i and j satisfies P, `possible ⊆ denotation(P)`.
So `(before A B)` and `(before B C)` entail `(before A C)`, and `(during A B)` with
`(during B C)` entails `(during A C)` and the weaker `(subintervalOf A C)` with it.

**Stored facts are not the only reader.**  This is the one calculus with a
`qcn-kb` **narrowing**: `stp/allen-narrowing-with-support` closes the metric constraints
over the instants `(startOf I P)` / `(endOf I P)` name and reads back what they pin down
about the interval relations, and that is intersected into the same network.  So a KB
that states two meetings' start and end times, and the gap between them, answers
`(before A B)` with no interval relation written anywhere — and the entailment names the
metric facts, the endpoint facts and the unit rows behind it, so retracting any of them
withdraws whatever was concluded from it.  It runs one way only: metric narrows
qualitative, never the reverse (docs/stp.md).

The **point network** is a second such reader (`points-narrowing-with-support`): the
instant facts over two things' `(StartFn X)` / `(EndFn X)` points leave some of the four
endpoint comparisons settled, and a relation whose endpoint signature needs an ordering
the point network rules out is removed.  Also one way only: an interval fact does not
constrain the points.

An emptied constraint anywhere means the asserted relations are unsatisfiable, and then
*no* interval goal is answered — an inconsistent theory should not be mined for
conclusions.

**Soundness.** Path consistency is sound but not in general complete: it decides the
maximal tractable subclass of the interval algebra and no more, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `arg` and `exceptWhen` take.

The vocabulary ships as `kb/upper/CxTime.txt`, an *upper* context rather than the
vocabulary head: these twenty predicates are *about* time, so CxCore keeps only the
grammar they are declared in.  The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves interval relations as
ordinary facts without paying for the network.

<dump>/
  meta.edn                     the marker, the schema, and the counts
  sentexes.nippy.stream        one frame per sentex
  justifications.nippy.stream  one frame per justification
  provenance.nippy.stream      [handle provenance-map] per frame (omitted when none)
  index/entries.nippy.stream   [key value] per frame — only in :records+index
  index/index.edn              the layout version + the records fingerprint

Write a KB out as a portable **export dump** — a directory holding the record
store's three streams, in a format that survives a backend change, an
index-representation change, and a record class rename.

The `:disk` store directory looks like an archive and is not one: it holds frozen
*records*, so renaming a record class makes every frame in it thaw to a
`{:nippy/unthawable …}` placeholder — silently, because a placeholder is a perfectly
good map.  Hence the one non-negotiable rule of this format:

> **A frame never carries a class name.**

A frame is the record's **field map** — `(into {} record)`, a plain map — so a rename
changes nothing a dump holds, and `vaelii.impl.io.import`'s `field-map` already
accepts one.

What a dump holds is what the record store holds, because everything else the KB has
is derived from it: sentexes, justifications, and per-handle provenance.  A premise
needs no stream of its own — a premise *is* a sentex whose `:strength` is non-nil, a
field on the record in both backends, so the mark rides along with it.  The index is
a cache (`reindex`), the taxonomy and the TMS labels are recomputed (`recover`).

    <dump>/
      meta.edn                     the marker, the schema, and the counts
      sentexes.nippy.stream        one frame per sentex
      justifications.nippy.stream  one frame per justification
      provenance.nippy.stream      [handle provenance-map] per frame (omitted when none)
      index/entries.nippy.stream   [key value] per frame — only in :records+index
      index/index.edn              the layout version + the records fingerprint

**The index is optional and always discardable.**  `:variant :records+index` writes it
as well, in the `[structured-key value]` projection every index backend shares
(`p/index-entries`), so an index written by one backend loads into another.  It is a
*cache*: a reader replays it only when it can prove the entries were derived from
exactly the records beside them (`vaelii.impl.io.fingerprint`), and rebuilds otherwise.
That is what makes writing it safe — an index that does not match its records is worse
than no index, because every lookup then answers confidently and short.

**Framing** is the chunked layout `vaelii.impl.io.frames` writes and reads: a
run of `[int32 length][compressed chunk]`, each chunk an independent compression
window over back-to-back nippy frames.  Constant memory on both sides — the writer
holds one chunk, never the corpus.  `meta.edn` *states* the framing rather than
implying it through a version number, because the engine's dumps number their own
format and a reader must never have to guess.

**`meta.edn` is written last**, which makes it double as the completion marker:
`vaelii.browser.catalog/classify` keys on it, so a half-written or cancelled export is
not offered as loadable.  That is the one ordering constraint in the whole format.

Export from a KB nobody is writing: the walk fetches record by record, and the
single-writer contract offers no snapshot to walk instead.

What makes a dumped index and a dumped set of records provably the same KB.

The index is derived from the records, so an index dump is only valid *against the
records it was derived from*.  Nothing downstream can notice when it is not: a stale
trie node simply reports fewer handles and a query returns fewer results — no
exception, no warning, just a KB that quietly knows less.  So the writer records a
fingerprint over the records and the reader recomputes it while storing them; a
mismatch discards the index and rebuilds.

**A sum, not a chain.**  The digest is the sum (mod 2⁶⁴) of a per-record hash, so it is
commutative — the reader accumulates it in whatever order the frames arrive, which is
not the order the writer walked — and *additive* rather than xor, so two identical
records cannot cancel each other out.

**What is hashed is what the index is a function of**: the handle, the sentence
(`sentex/sentence-of`, which is a rule's `implies` form), `:context`, the sign
(`sentex/polarity`), a rule's `:antecedent` / `:consequent`, and a choice or
constraint rule's `:effect`, which the trie key spells in its two trailing slots
(a `:derive` rule's is left out, so its hash is its implies form's).  `sentex/path`,
`kv/root-keys`, `kv/sentex-terms` and the rule index read exactly those, and the handle
because a posting *is* a set of handles — the same content at a different handle makes
every posting naming it wrong.  Deliberately **not** hashed: `:strength`, `:varmap`,
`:engines`, `:defeasible`.  None of them changes a single index entry, so a dump
differing in one of them still has a valid index, and hashing them would make the cache
go unused for a reason that is not a reason.  (`:strength` also arrives after the
storing pass — a premise mark is applied once every record is down — so hashing it
would cost the second pass over the records this exists to avoid.)

The hash is FNV-1a over the fields' own `hash` values: cheap, deterministic across
runs, and strong enough for the question being asked, which is whether two sets of
records are *the same* — not whether an adversary can forge one.  A dump is not a
trust boundary; if it were, this would be a real digest and signed.

**Two granularities, one rule.**  `accumulator` (over `record-hash`) folds in what a
record *says*, and needs the record — the export rides it on the sentex walk it is
already making, and the import rides it on the frames it is already decoding.
`slot-accumulator` (over `slot-hash`) folds in where each record *is*:
`(id, offset, length)` off the idx, no frame decoded and no record fetched.  The mapped index snapshot (`vaelii.impl.disk.index-snapshot`) is
checked with that one, because an image exists to make an open cost bytes read rather
than records read, and a content digest would put every record back on the open path.
It is the coarser hash in one direction and the finer one in the other: it cannot see
a record rewritten to the same bytes at the same offset (nothing can produce that),
and it *does* see a rewrite the index does not care about — a premise mark, or a
compaction moving every frame — so a snapshot is discarded and rebuilt after one.
Both directions are safe, because a discard is always legal for derived state.

The chunked **nippy stream** framing every serialization in the engine writes to a
file or a sink — one home, so the export dump, the import reader and the snapshot sink
cannot drift.

A chunked stream is a run of `[int32 length][compressed chunk]`, each chunk an
independent compression window over back-to-back nippy frames.  Constant memory on both
sides: the writer holds one chunk and never the corpus, and the reader thaws a chunk on
demand and drops it.  A *frame* is whatever the caller freezes — a record's field map, an
index `[key value]` pair, a JTMS `[handle label]` pair — this namespace neither reads a
frame nor cares what one is.

**Why it is its own namespace and not `export`'s private helper.**  Three callers write
and read this format — `vaelii.impl.io.export` (the dump), `vaelii.impl.io.import` (the
reader) and `vaelii.impl.io.snapshot` (the index image) — and the snapshot sink
is meant to be *a thin adapter over this framing, not a second copy of it*.  A second
copy is exactly the drift a shared projection was created to avoid one layer up: two
writers that agree today and diverge on the next compression tweak.  So the framing lives
once, here, and the container-specific concerns (what a dump's `meta.edn` records, an
image's manifest) stay with each caller.  The dump's stream **names** are not one of
those concerns: which streams exist and what each is called is the layout the writer
and the reader must agree on — a second copy is the same drift one level down — so the
names live here too, beside the framing they name (`meta-file` and its six siblings
below).

The legacy single-window reader (`read-window-seq`) is kept for a v4/v5 foreign dump that
wrote one compression window over the whole file; the engine's own dumps have been chunked
since v6.

sentexes.nippy.stream        one field-map frame per sentex
justifications.nippy.stream  one per justification
provenance.nippy.stream      [handle map] per frame — optional

Import a vaelii **export dump** — a directory of record streams — into a KB,
landing in exactly the state the engine's own restart path (`reindex` / `recover`) already
knows how to produce.

A dump is a directory whose `meta.edn` is the marker and schema; every other file is
a nippy stream:

    sentexes.nippy.stream        one field-map frame per sentex
    justifications.nippy.stream  one per justification
    provenance.nippy.stream      [handle map] per frame — optional

A `:records+index` dump also carries the index, as a **cache** that is used only when
it can be proved to describe the records that were just stored (see *the index* below);
otherwise the index is rebuilt, and the summary says which happened and why.

**Framing.**  A chunked stream is a run of `[int32 length][compressed chunk]`, each
chunk a compression window over back-to-back nippy frames; a window stream is one
compression window over the lot.  Our own dumps **state** which (`:framing`); a
foreign dump's is inferred from its own version line.  Both are constant-memory lazy
seqs.

**A frame of our own dialect is a plain field map** whose `:sentence` is already
there — but a rule's `set/*Rule` wrappers and its variable names canonicalized *into*
the record (`:engines` / `:defeasible` / `:effect` / `:varmap`), so both are written back around
it before the constructor sees it.  A frame that is *not* ours goes to a foreign
reader (`vaelii.impl.foreign`), which is resolved at runtime and may not be in the
build at all.  The discrimination is on the **frame**, never on `meta.edn`'s
`:dialect`: a declaration is not an authority over the bytes beside it, and keying off
the frame keeps a mixed dump readable.

Whatever the dialect, **every sentence is re-canonicalized** through this build's own
constructor (`res/kb-sentex`).  A stored canonical form is never trusted, not even
our own: variable numbering, symmetric argument order and comparison folding belong to
the *reading* build, and a record indexed under a key this build's `lookup` never
reproduces would be silently unfindable.

**Handles are preserved** for a dump of ours: every record is stored at the handle the
dump gave it, so a handle means the same thing either side of an export.  Safe because
the destination must be empty and because a store's counter clears any handle written
that way (`p/next-id`) — without which the next `assert` would mint handle 1 again and
overwrite the first imported record.  Two things can still stop a handle landing as
given, and neither is silent: a frame with no `:id`, and a frame whose canonical form
is one already stored, which **collapses** onto that handle (a dedup this build is
right to perform — two engine forms can canonicalize to one stored record — and the
dump's numbering cannot survive it).  Either makes the import `:remapped`, and then one
`old->new` map carries the dump's ids across: justification references, and the
`(sentexHandle H)` a meta-sentex embeds *inside stored content*, which
`rewrite-embedded-handles!` rewrites in the sentence.  A meta-sentex whose embedded
handle cannot be resolved is **dropped**, and the drop reaches the map as well as the
store (`forget-deleted`): a dump id whose record is gone has to stop resolving, or the
references to it resolve to a handle nothing is stored at.

**The index is replayed only when it can be proved to fit**, and discarding it is
always safe — which is what makes a cache out of what would otherwise be a risk.  An
index that does not match its records is *worse* than no index: every lookup then
answers confidently and short, and nothing in the engine is positioned to notice.  So
all three of these must hold (`index-decision`):

* the entries are keyed in the layout this build reads (`kv/index-layout-version`);
* the fingerprint accumulated **while storing** equals the one written beside the
  entries (`vaelii.impl.io.fingerprint`) — accumulated, not recomputed, since a second
  pass over the records to validate a cache would cost more than the cache saves;
* the handles were preserved, so a posting names the record it named in the source.

Anything else rebuilds, at `:info`, with the reason named.  A cache that silently
stops being used is a cache nobody maintains.

The store-facing replay is written against the engine's real protocols: populate the record
store with the re-canonicalized records + justifications + premise marks, then either
install the dumped index (`p/index-load`) or rebuild it (`reindex`), then
`core/recover` — which rebuilds the JTMS and the taxonomy **from the records**, so a
replayed index shortcuts the index and nothing else.  Out of scope: the `:pg-memory`
variant.

A **snapshot** of the KB's derived state, and the two-op *sink* it is written through.

Derived state — the index, and (from 0.9.0's second thread) the taxonomy and the JTMS
labels — is rebuilt from the records on every open by `reindex` / `recover`, at a cost
that is O(records).  A snapshot is a *cache* of that rebuild: written once, read back on
the next open, and installed instead of recomputed.  It is never a source of truth.  Its
only failure mode is "recompute", never "wrong answer", which is what keeps it clear of
order independence — a snapshot is stamped to the exact records it was derived from, and a
mismatch takes the slow path (`reindex`/`recover`), never a stale belief.

## One image, many sinks

There is more than one place a snapshot might live — a directory of files, a Postgres
blob, memory for a test — and letting each invent its own serialization is the drift the
shared `[key value]` index projection was created to avoid one layer up.  So the shape is
one **sink**:

* a snapshot is a set of **named sections** plus a **manifest**;
* a `SnapshotSink` knows only how to *write a named section* (a constant-memory stream of
  frames) and to *commit a manifest*; a `SnapshotSource` knows how to *read a section back*
  and to *read the manifest*;
* the **projections** (the index's `[key value]`, and later the taxonomy's edges and the
  JTMS's labels) and the **validity check** (`decision`) live here, above the sink, written
  once;
* the **targets** — `file-sink` / `file-source` over `vaelii.impl.io.frames`, and
  `memory-medium` for a test — live below it, each a small adapter.

A section written to one sink loads from another, the same property `p/index-entries` /
`p/index-load` already give the index across backends.

**The protocol has out-of-tree implementations, so it is a published shape and not a private
one.**  `vaelii-postgres` (`vaelii.postgres.snapshot/pg-sink` / `pg-source`) and
`vaelii-sqlite` (`vaelii.sqlite.snapshot/sqlite-sink` / `sqlite-source`) each implement
both protocols and drive them through `save-index!` / `load-index!`, and both suites
cross-load a section against `memory-medium` to check the two targets agree.  What is
reached only from this repo's own tests is `file-sink` / `file-source`: the reference
target, and the one that shows an implementer what a section and a manifest have to be.

## The manifest is the commit point

It is written **last**, exactly as a dump's `meta.edn` is: a half-written image has no
manifest, so `read-manifest` returns nil and the image is never offered — the caller
rebuilds.  Opening a `file-sink` deletes any existing manifest first, so the window in
which an old manifest could describe half-rewritten sections does not exist.

## Validity is the whole design

`decision` is lifted from `vaelii.impl.disk.index-snapshot/decision`: one reason per
mismatch class, and any non-nil reason discards the *whole* image and falls back to a
rebuild.  The classes:

* `:absent`          — no manifest (missing, or a save that never committed);
* `:layout-changed`  — the snapshot format version, or `kv/index-layout-version`, is not
                       this build's (an index in another layout reads as *empty* rather
                       than wrong, which is the undiagnosable failure this forecloses);
* `:records-differ`  — the manifest's records stamp is not the store's now (a different
                       KB, or the same one after a write);
* `:entries-truncated` — a section is short or unreadable, caught while installing (a torn
                       nippy chunk is indistinguishable from a clean EOF, so truncation shows only as a
                       frame count below what the manifest recorded).

There is no `:byte-order` class here, though `index-snapshot` has one: that image writes
raw little-endian `int` runs, so an image from a machine of the other endianness must be
refused; these sections are nippy frames, which are endian-neutral, so a byte-order
mismatch cannot arise and the format version subsumes any encoding change.

The stamp is `vaelii.impl.io.fingerprint`'s records digest, which **ports**: a `:disk`
store hashes its slots, a `:memory` store folds its records, a SQL store answers a count
— and all compare against the same manifest number.  Which digest a caller passes is its
business; the sink only compares.

The **text KB format** — one file per context, one s-expression per sentence — read
and written.

It is the format the shipped ontology is authored in (`resources/kb/`,
`vaelii.host.seed`), and this is where the writer for it lives, so a KB an author
edited as text can be got back out of a store as text.  The three formats a KB moves
in are different questions and stay separate entry points:

| | what it holds | who reads it |
|---|---|---|
| **text** (here) | premises, in the author's own spelling, no handles | `assert` |
| **export dump** (`io.export` / `io.import`) | every record and justification at its own handle | `import!` |
| the **store** itself | the live KB | the engine |

A dump is a KB's *state*; text is a KB's *content*.  Only the second survives a
re-derivation, a rename or an engine that concludes something new — which is what an
author editing an ontology wants, and what a dump deliberately is not.

## The format

Every form is one sentence, read with `clojure.edn`, so a KB file is data and can
never run code.  `;;` comments and blank lines are free — the reader is the EDN
reader, so it skips them without a line-oriented pass.  **The file name is the
context**: `CxKinship.txt` asserts into `CxKinship`, and a sentence for another
context says so with `(ist Cx S)` as it would anywhere else.  A rule carries its
`set/*Rule` / `set/defaultRule` wrappers and its `exceptWhen` exactly as an author
writes them, because that is what `assert` reads.

**One wrapper is not part of the sentence**: `(set/monotonic S)`, the known-true
class.  A strength is an *option* on the assertion rather than part of the sentence, so
there is nowhere in an s-expression for it to go, and a text KB that could not say it
would round-trip a KB's monotonic premises down to defaults.  It is peeled by
`load-entries!` below into `{:strength :monotonic}` and never reaches the store as a
functor.  `:default` is the entry point's own fallback and is written as nothing, which is why
no shipped file carries a wrapper.

**An `exceptWhen` states a strength per half**, because it asserts two things: the rule,
and the exception qualifying it.  The outer wrapper is the assertion's own option and
`assert` gives it to *both*, so it can only state a class the two share; a wrapper on
the **query** states the exception's own, and `assert` reads that one itself
(`sentex/peel-exception-strength`), so a hand-written KB spells it the same way.  Four
pairings, four spellings:

| rule | exception | written as |
|---|---|---|
| default | default | `(exceptWhen Q R)` |
| default | known-true | `(exceptWhen (set/monotonic Q) R)` |
| known-true | default | `(exceptWhen Q R)`, and `(set/monotonic R)` on a line of its own |
| known-true | known-true | `(set/monotonic (exceptWhen Q R))` |

The third takes two lines because there is no wrapper for *weakening* a half: the rule
gets a line of its own at the stronger class, and `mark-premise` resolves a premise
asserted twice to the stronger of the two.

## What a text export holds, and what it does not

**Premises only.**  A derived sentex is what the engine concluded from the premises,
so writing it out would store as a premise what the KB believes as a conclusion — a
reload would hold it against retraction of everything it followed from.  Chaining
puts it back at load, which is the whole point.

**No handles.**  A text KB is re-asserted rather than restored, so it lands at
whatever handles the loading KB mints.  A caller who needs handle identity across the
round trip wants `export!`, not this.

**Deterministic.**  Files are named for their contexts and their forms are ordered by
content (`nm/by-print-key`), never by handle — so two KBs holding the same knowledge
export byte-identical files whatever order they were built in
(docs/defenses.md, "Tie-breaks and orderings key on content").

The class-name check on every nippy thaw the engine runs over a file.

A frozen nippy value can **name a class** in three of its type ids, and reading one
resolves that name and builds an instance of it: a record frame (`Class/forName`, then
the static `create`), a deftype frame (`Class/forName`, then the first public
constructor over the fields that follow), and a `Serializable` frame (an
`ObjectInputStream` over the bytes that follow).  nippy 3.9.0 gates the third behind
`*thaw-serializable-allowlist*` and the first two behind nothing at all.

Every file the engine reads is **untrusted input** — a store directory or a dump
arrives from wherever an operator copied it — so all three are gated here, and the
gate is the tightest one there is:

> **A vaelii frame never carries a class name.**

That is already the export format's stated rule (`vaelii.impl.io.export`), and the
disk codec writes a record's fields **positionally** for a size reason
(`vaelii.impl.disk.codec`), so nothing the engine writes states a class either.  A
frame that names one therefore came from somewhere else, and `allowed-classes` is
empty: the name is refused (`:disallowed-class`) before the class is resolved.

**The `Serializable` allowlist is pinned rather than inherited.**  nippy's default is
a safe set, but it lives in a dynamic var an embedding application is invited to
widen — nippy documents `allow-and-record-any-serializable-class-unsafe` for exactly
that migration — and a host that widened it would widen the engine's file readers with
it.  Binding it per read makes the entry point this namespace's rather than the host's.

**How the first two are gated**, since nippy exposes no hook for them: the readers
`taoensso.nippy.io` dispatches to are vars, and this namespace installs a checked
reader in place of each.  A refusal is thrown from there, which is *before* nippy's own
`try` — so it travels rather than becoming the `{:nippy/unthawable …}` placeholder a
failed resolution otherwise reads as, and no class is loaded on the way.  The
replacement calls straight through to the reader it replaced unless `with-guard` is in
force, so a host application thawing its own records in this JVM is unaffected.

**What holds that wrap to the release it was written against** is
`pinned-nippy-version`: three internals are reached into here, and a bump that keeps
their names while routing deserialization around them would narrow this entry point without
reddening anything.  So the version is checked at load and the namespace refuses to
come up against another one.

A journal of the handles each update of a persistent map can move, kept in the map and
written in the update that moves them, so a reader reads what moved since its last
position instead of the whole map: the candidate index's candidates and the flat-cache
keys the taxonomy's `:cache-moves` journals; and an
index of a map's handles by context read again off its journal (`indexed`).  See
docs/nmtms.md, "The candidate journal" and "The inherited-clash memo".

A non-monotonic truth-maintenance system.

Each TMS *node* corresponds to a datum (a sentex handle) and records: its label
(IN/OUT), whether it is a premise (and at what assumption *strength*), its
derivation depth, the justifications that conclude it (:supports), and the
justifications that use it as an antecedent or name it as their rule (:consequences).

A node holds **no reference to the sentex it labels** — only its handle.  The record
store is where a sentex lives, so a copy here would be a second one to keep in step;
and because this graph is always resident, a strong reference from it would hold every
record in RAM, which on a paging backend defeats the paging entirely (measured: the
nodes reached 50% of the record store).  A caller that needs the sentence fetches it
by handle.

Belief is a least fixpoint: a node is IN when it is a premise or has a valid
justification (all antecedents IN).  Because labels are computed from the current
justification set rather than accumulated as events arrive, belief is
order-independent.  A contradiction takes nothing OUT here: the settle places it as a
`contradicts` and a `defeat`, and the read walk hides the loser at the readers where the
defeat is in force (`vaelii.impl.except`), so the network holds support labels only.

## Two invariants

**Order independence.** The same knowledge, given in any order, yields the same
beliefs.  Every operation here recomputes labels from current state, so nothing
depends on arrival order.  (The one place this can leak is a *tie-break* between
two equally-strong beliefs: keying it on handle id would smuggle assertion order
back in, so the contradiction layer keys it on content — see
`vaelii.impl.solve/content-key`.)

**Locality.** No operation recomputes the whole graph.  A change can only affect
nodes downstream of it, so every relabel is scoped to the *affected region* — the
forward consequence closure of whatever changed — with the rest of the graph held
fixed as the boundary.  Cost is proportional to the region, not to the size of the
KB, which is what lets belief maintenance scale.

These two pull against each other, and the reconciliation is the whole design:
a local fixpoint over the region, with boundary labels fixed, has a *unique*
solution, and it is the same one a global fixpoint would produce.  See
`relabel-region*`.

  * strength — every premise carries a strength (:monotonic / :default); every
    justification carries a *strength* too (:monotonic for a bare rule, :default for
    a defeasible one), capping the class it confers.  From these, `relabel` derives
    each IN node's *defeat-class* (monotonic > default, see
    vaelii.impl.strength).  Strength **propagates**: a justification confers no more
    than the weakest of its antecedents' classes, so a conclusion is never stronger
    than what it rests on.  That makes the class equation recursive, and
    `region-classes` solves it as a least fixpoint inside the region relabel.
    The class decides who loses a soft contradiction at a reader
    (`vaelii.impl.decide`); the network records no defeat, and nothing forces a datum
    OUT.

  * superseded — a *map* `datum -> reason` of datums displaced by an equality
    merge: the stale spelling of a fact whose terms have been rewritten to their
    class representative (docs/equality.md).  Three things make it its own state
    rather than a reuse of `blocked`:

    - `blocked` names *justifications*, and a directly asserted `(bornIn Dep
      Chicago)` is a **premise with no justification at all** — `region-fixpoint`
      seeds every premise IN unconditionally, so there is nothing for a block to
      invalidate.  Superseding has to act on the datum.
    - A superseded spelling lost no argument; it was restated, and `why-not` must be
      able to say so — hence the map carries the displacing representative rather than
      being a bare set.
    - It is **not** a forced OUT inside the fixpoint.  A superseded datum stays in
      `:in` for the purposes of `valid?`, because its rewritten twin is justified
      *by it*: forcing it OUT structurally would invalidate the twin's own
      justification and the merge would believe neither spelling.  What
      supersession removes is *reported* belief — `in?` and `in-datums` subtract
      it — so the stale spelling stops matching and stops answering queries, while
      everything derived from it stands.  The nogood families detect over the IN
      label (`network-in?`), so a nogood with a superseded member keeps its
      placement, and the clash reports leave it out (docs/nmtms.md).

    Retention is the point: the spelling is the **caller's premise**, so unlike an
    excepted conclusion it is never swept, and dropping the equality gives it back.
    Like `blocked` the map is *derived* — core recomputes it each
    settle from the equality closure — so belief stays order independent.

  * forced — three sets the forced-monotonic roster writes (docs/nmtms.md, "The
    forced-monotonic roster"): `:mono`, premises whose class is `:monotonic` whatever
    strength they carry; `:out`, datums the fixpoint never adds, a premise included;
    and `:void`, justifications that support nothing and confer no class.  Each is an
    **attribute** of the element it names, written by the caller with the element and
    rewritten when the roster moves (`set-forced`), so the stored content keeps the
    strength it was written at and every record a forced set governs stays stored.

  * blocked — a set of *justification* ids whose rule's exception currently holds
    (`exceptWhen`, see docs/exceptions.md).  A blocked justification is simply
    **invalid**, so it supports nothing and confers no defeat-class — which is what
    lets the ordinary dependency-directed sweep garbage-collect an excepted
    conclusion.  This module is pure and has no
    KB, so it cannot run the exception query itself: the caller evaluates the
    exception and hands the answer in with `set-blocked`, which relabels only the
    region the change reaches.  The set is *derived* — computed
    from current state each settle, never accumulated — so belief stays order
    independent.

Retraction is dependency-directed: drop the premise, relabel, then SWEEP the
affected closure — datums that end up OUT with no valid support are solely supported
by the retraction, so they (and their non-premise justifications) are returned for the
caller to delete from the stores.

This module owns the in-memory graph; the caller owns physical deletion, since
only it holds the stores.

The representation boundary of the truth-maintenance system: the `Tms` protocol
alone, with no implementation.

It lives in its own namespace, apart from `vaelii.impl.jtms` (the reference
network) and `vaelii.impl.dense-jtms` (the dense one), for two reasons.  Both
implementations depend on it, and the reference depends on nothing of the dense one, so
the boundary is the one thing they share; the dense network also calls two helpers of
the reference namespace (`graph-just`, `dissoc-all`).  And it is large — forty-odd methods, each documented — which
makes the generated protocol map big enough that re-evaluating the form (as
cloverage does, form by form, to instrument a namespace) overflows the JVM's
64 KB per-method bytecode limit; isolated here, the protocol is loaded but not
instrumented while the whole of `vaelii.impl.jtms` still is (scripts/coverage.sh).

A held namespace (`vaelii.impl.types.prover` states what that means): it defines the `Tms` protocol and requires no vaelii namespace, so the development browser's reloader never re-evaluates it, and an edit to it takes a restart.

The KB record, its constructor, and the ground floor of retrieval:
find/create sentexes, the belief-filtered `sentexes-matching`, and the equality-closure
goal rewriting that keeps a retired spelling usable as a question.

Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle <- vaelii.core): everything here reads the storage protocols, the taxonomy, the
JTMS and the matchers — never assertion, chaining, or settling.  `sentexes-matching`
lives here rather than in core because the layers above it (`integrate-sentex`) need
*querying*, not asserting.

The key-value substrate the index rests on, and the one `IndexStore`
implementation written over it.

The index — the trie, the secondary roots, the rule indexes, the exception
re-check index, and the inverted term index — is *all* sets and counters keyed
by structured vectors.  `KvIndexStore` encodes that structure once, in terms of a
small `KvBackend` protocol; a backend is then just an adapter that says how a
scalar, a counter, and a set live in some store.  An in-memory map
(`vaelii.impl.memory`) and an on-disk WAL (`vaelii.impl.disk.kv`) are two such
adapters; a SQL or overlay backend is another.

## The count-aware trie

A sentex is indexed by its trie path.  Every node, identified by its path
prefix, is exactly three keys:

  count-key  [:trie :count prefix]  ->  integer: how many sentexes live at the leaves
                                   under this prefix (selectivity without walking).
  set-key    [:trie :children prefix]  ->  a SET: the next possible token labels (the
                                   node's child edges).
  leaf-key   [:trie :handles prefix]  ->  a SET: the handles of the sentexes whose path
                                   ends exactly here.

**Child edges and leaf handles are separate keys because the trie is ragged.**
Paths differ in length with arity, so one sentex's *full* path can be a proper
prefix of another's: `(rel A B)` in `CxCee` keys as `[rel A B CxCee]`,
and `(rel A B CxCee X)` in `CxDee` keys as `[rel A B CxCee X
CxDee]` — the first path is an interior node of the second.  Storing both
handles and child tokens in one set therefore mixed them, and a caller could not
tell them apart by type (a handle is an integer, and so is the token `1970`).  Two
keys make the distinction structural: `lookup` reads only the leaf key at its
terminus, so it can never return a token as a handle, and `children` reads only
the child set, so `plan`'s fan-out divisor can never count a handle as a branch.

Alongside the trie sit eleven smaller count tries whose last level is the context — the
argument roots, the predicate extent, the two rule indexes, the rule extent, the
opposed bodies, the self tuples, the arity bindings, the taxonomy's supporters and the
mint family's two
("The count tries that end in the context" below) — and three flat sets whose
cardinality is their own size: the context root, the exception re-check index and the
inverted term index.  One more flat set, the **term roster**
`[:term-roster]`, holds the term index's *names* rather than handles, so the
vocabulary can be listed and counted in O(terms) instead of a walk over every record.

Contract: lookup expects a *full* path (sentence tokens + a context slot; the
context may itself be a variable).  A short pattern terminates on an interior
node, whose leaf key is empty, so it yields nothing rather than that node's child
labels dressed up as handles.

## The `KvBackend`

Logical keys are structured vectors and set members are bare values; a backend
turns those into whatever its store wants (an in-memory map uses them directly; the
on-disk backend nippy-frames them into its log).  The required ops are
`kv-batch` (the whole index write for one sentex lands as one unit — one batched
write) and `kv-intersect` (the multi-column narrowing `sentexes-with-args` needs, one
set intersection rather than N fetch-and-filter reads).  A batch op is a vector
`[op key & args]` with `op` one of `:put`, `:delete`, `:increment`,
`:decrement`, `:add-to-set`, `:remove-from-set`; `kv-batch`
returns one reply per op in order (only `:increment`/`:decrement` replies — the post-op
counter value — are read; the rest are placeholders that keep the vector aligned).

**`kv-member?` is a membership test, not a fetch**, and it is its own op because on
several backends those cost different orders.  `exception-rule?` is the gate
`chain/rule-view-of` takes once per candidate rule per new datum, so answering it by
materializing the roster and testing the result makes forward chaining a product of
two KB-sized quantities.  A flat-map backend hands the stored set back by reference
and hides the distinction entirely; a dense one holds the roster as an `IntPostings`,
where 1e5 gate calls against a roster of 1,000 cost 15,926 ms built-then-tested
against 87 ms on the flat map — so the op exists to let each backend answer with the
probe it already has (a hash lookup, a binary search, a bitmap test).

The lookup-to-query stack: eight levels of escalating interpretive machinery over
the same goal, from a raw index read to full backward chaining.

Every layer the engine already has is a *point on a ladder* — the trie knows
nothing but paths, `raw-match` adds unification, `matches-visible` adds context
inheritance, the prover engine adds closures and rules.  Naming those points and
giving them one call shape makes the cost of an answer legible: you can ask what
the cheapest machinery that answers a goal is (`escalate`), or watch an answer
appear as machinery is switched on (`explain`).

  0 :raw      handles at an index location — no sentence semantics at all
  1 :extent   one literal context, narrowed by functor; no unification
  2 :local    + unification and the symmetric mirror, one literal context
  3 :visible  + context inheritance (the genlCx up-closure)
  4 :typed    + predicate inheritance (the genl spec walk)
  5 :closed   + transitive closure for transitive predicates
  6 :solved   the whole prover registry — no member of it expands a rule
  7 :proved   + rule expansion (the recursive chainer, registry as its leaf)

Each level adds **exactly one** mechanism to the one below it, so a result that
appears at level n and not at n-1 is attributable to that mechanism alone.

**Monotonicity, and the two joints where it is not free.**  Levels 3-5 are wider
calls to the same matcher, and level 5 is literally `level 4 ∪ the closure`, so an
answer reachable at one of them is reachable at the next.  Two joints are not like
that, and naming them is half of what naming the levels is for:

  1 -> 2 **narrows**.  Level 1 is candidate retrieval and never looks at the goal's
  arguments; level 2 unifies.  So for any goal that pins an argument level 2 is a
  *subset* of level 1 — which is one of the two reasons `escalate` floors at 2.

  3 -> 4 can **drop** an answer.  Level 4 is `res/matches-visible`, which reads the
  `except` visibility filter that `res/raw-match` does not, so a sentex a believed
  `(except (sentexHandle H))` hides from the view context is matched at levels 2 and
  3 and gone from level 4 up.  Level 4 is right and the engine agrees — `ask` denies
  that goal too.  What it costs is `escalate`, which will name level 2 as the
  machinery sufficient for a goal the engine does not answer.  No floor fixes that:
  whether a level over-reports is a property of the KB, not of the level.

Level 6 delegates to the real engine (`provers/solve-goal-with`) and therefore
inherits its behaviour, including the short-circuit where a prover claiming
completeness 100 runs *alone*: for a `genl` goal, level 6 returns the taxonomy
closure rather than the union of closure and stored facts, which is why level 6
answers may carry no handle where level 4's did.

What does **not** bend is the content.  Completeness 100 claims a superset of what
every other applicable prover would answer for that goal (`provers`, the contract at
the head of the file), and a prover bearing on a channel it cannot read reports below
100 for the goal so the union runs.  So from level 4 up an answer climbing the stack
can lose its handle and never its existence.

**Laziness.** Every level returns a lazy seq, and each is lazy as deep as the
layer under it allows, so taking one result is strictly cheaper than taking all.
Where that is impossible it is inherent, not an oversight, and is noted at the
site: reading a stored set is one operation whether you take one member or all of
them, and a transitive closure has no partial answer.  The property that does
hold everywhere is that per-result work — a record fetch, an expensive prover, a
rule expansion — is paid per result consumed.

Canonical variable names for a **solution** cache keyed by a literal, and the
translation back into the caller's names.

A backward proof asks the same question many times.  Two sibling branches that both
need `(parentOf Tom ?y)` each solve it in full, and a diamond-shaped rule set pays for
the shared literal once per path through the diamond — `res/prove-from`'s per-path
`:seen` guard stops a goal from re-*expanding* itself on one path, and says nothing
about the same goal being re-*solved* on another.  Keying an
answer by the literal is what collects that sharing, and the key has to be blind to
what the caller happened to name its variables: `(P ?x)` and `(P ?y)` are one question.

**Why `res/goal-key` is not that key.**  It collapses *every* variable to `?`, so
`(P ?x ?x)` and `(P ?x ?y)` share a key.  That is sound for a loop guard, which only
has to be conservative — over-matching prunes a branch that was going to be pruned —
and unsound for a solution cache, where the second goal's answers include the pairs
the first excludes.  Serving one for the other invents solutions.  So the renaming
here is **repetition-preserving**: distinct variables get distinct names and a
repeated variable keeps its repetition.

**Why `sentex/alpha-rename` is not it either.**  That one builds an *index* key, where
a variable means "anything in this position" and each anonymous `_` is therefore
fresh and unshared.  `unify` does not read `_` that way — `variable?` admits it and
`unify-var` chases its binding, so `(P _ _)` fails against `(P A B)` exactly as
`(P ?x ?x)` does.  A cache keyed on retrieval semantics would hand `(P _ _)` the
answers of `(P ?0 ?1)`, so `_` is renamed here as the ordinary variable it is.

**What is cached, and why there.**  The unit is one literal's *visible matches*
(`res/matches-visible`), not one literal's *solutions* (`provers/solve-goal`).  That
is where the repetition measurably is — a rule-heavy query re-asks a handful of
metadata literals (`(arg P n ?t)`, read per believed sentex per argument position
by `provers/inferred-types`) hundreds of times, while its rule subgoals arrive
already substituted and so are mostly distinct.  It is also the only layer at which
the answer is a function of the KB alone.  `solve-goal` is **tier**-dependent, because
`ask-capped` drops provers above a cost tier, and **scope**-dependent, because provers
underneath it read the taxonomy closures and the resident networks through
`observe/cached` — so inside a pinned scope they answer from the view that scope froze.
An answer cached at that layer would therefore have to carry the tier and the scope
that produced it.  `matches-visible` carries neither and reads nothing through
`observe/cached`, so a pinned scope cannot hand it a view the clock has left.

There is **one layer, not two**.  A per-query memo would be redundant: a query
performs no mutation, so the change clock cannot move while one runs, and every
repeat a per-query memo would catch is a repeat this cache already serves under an
unmoved stamp.

The log dial: how much the engine's own `trove/log!` calls print, as a value a
*running* process can change.

Verbosity is otherwise decided before a process starts, and the process that most
needs a different setting is the one nobody can restart — a daemon a week into a run,
on a durable KB that pays `recover` on the way back up.  So the level is an **atom**,
read per call by the one backend installed here; turning the dial is a `reset!` and
never a second install, and two dials wrapped around each other is a state this cannot
reach.

## The engine installs nothing unasked

`vaelii.core/set-log-level` and `VAELII_LOG_LEVEL` install a backend.  Nothing else
does: opening a KB does not, and neither does loading this namespace with the variable
unset.  A library that replaces `taoensso.trove/*log-fn*` because it was *loaded*
takes over the logging of the application that loaded it — a worse failure than a
quiet engine, since the host loses its own lines and has nothing left to correlate.
The variable is read at load, which is also the ordering that keeps it true: a host
installing its own backend does so after requiring the engine, and wins.

## A level check, not a backend

The sink is Trove's console backend and the ranking below is the whole of what this
puts in front of it.  The ranking covers Trove's seven levels rather than the five the
dial takes, so a message at `:fatal` or `:report` sorts above `:error` and prints
under every setting instead of falling to a rank of zero and being suppressed by all
of them.

The default in-memory backends for the two storage protocols, selected at KB
construction.  The engine above the protocols never touches a concrete store, so a
KB built on these runs the whole engine with no external dependency; the on-disk
backend (`vaelii.impl.disk`) is the durable alternative.

The record store implements `RecordStore` directly over maps.  The index reuses
`vaelii.impl.kv/KvIndexStore` — the one trie/roots/index implementation — over a
`MemoryKvBackend`: one map keyed by the structured key vectors (equal vectors are
equal keys), holding a `Long` at each counter key and a set at each set key.
`kv-intersect` is a `clojure.set/intersection`; `kv-members` returns the stored set
by reference (no serialization, no copy).

**Durable-within-the-JVM semantics by space number.**  Two KBs constructed over the
same `:space` number must share state, or the persistence/recovery tests (a second KB
restarted over the same databases) would find an empty store.  A process-global
registry keyed by space number provides that: `(memory-record-store {:space 15})` twice
returns records backed by *one* state atom, and by one handle counter beside it.
`clear-records!` / `clear-index!` empty a space.  (State lives only for the life of
the JVM; the on-disk backend is what survives a process restart.)

**Single-writer.**  Pure runs one writer (docs/storage.md, "The single-writer
contract"), so a store's state is one atom mutated by `swap!`; reads deref a snapshot
and are lock-free.  Interleaved *writers* would not be serializable.

Beliefs without new primitives.

Two agents can believe contradictory things without the KB being inconsistent —
that is what a context lattice is *for*, and the engine already has the lattice.
What this namespace adds is the **projection**: a way to ask what an agent believes
and get the answer from inside that agent's own context.

The whole idea is one convention and one prover, over machinery that already exists:

- **The convention** lives here — a deterministic bijection between an agent symbol
  and its context.  Agent `Alice` owns context `CxAgentAlice`; asking
  `(believes Alice P)` is answering `P` in `CxAgentAlice` rather than in the asker's
  context.  A generated name passes exactly the checks a hand-written context name
  does (`naming/context?`), so nothing downstream can tell a minted agent context
  from any other.
- **The prover** lives in `vaelii.impl.provers` (`BeliefProjectionProver`), where the
  `Prover` protocol and the registry are — it recognizes a modal goal and sub-queries
  the inner sentence in the agent's context.

An agent context is an **ordinary context** created through the ordinary assert path:
the caller asserts `Alice`'s beliefs into `CxAgentAlice` and the projector reads them
back.  Nothing here teaches the JTMS, the taxonomy or the index about agents — a
belief is a fact in a context, and an agent context is a context like any other.

**Which predicates project is a KB property, not a hard-coded set.**  `believes` is
one of them, and `knows` / `desires` / `intends` are the same projection under a
different predicate; a predicate projects exactly when `(modal_predicate P)` is
believed where the query is asked — read context-scoped through `has-prop? :modal`,
the way `abducible_predicate` grants abduction.  So the table is open (assert the
marker to add one) and it is a *policy of a context* rather than a global switch.

This is a **projector, not a modal logic**: no axiom schema (K, T, 4, 5), and no
special handling of a nested `(believes A (believes B P))` beyond what falls out of
the marker's own visibility.  See docs/belief.md.

predicate    camelCase, lowercase-initial, arity 2+         parentOf, genlCx, arg
individual   CapitalCamelCase                               Muffet, Tom
type         snake_case, lowercase, unary predicate         dog, physical_object
sense        a type, plus which sense of it is meant        abrasive-grit
context      Cx prefix, then CapitalCamelCase               CxUniverse, CxCore
lexeme       the `lex` namespace; the name is parse input   lex/fool's_gold

KB naming invariants, as predicates over symbols — and the walk that applies them to
  every **literal** of a sentence rather than to its outermost functor alone.

    predicate    camelCase, lowercase-initial, arity 2+         parentOf, genlCx, arg
    individual   CapitalCamelCase                               Muffet, Tom
    type         snake_case, lowercase, unary predicate         dog, physical_object
    sense        a type, plus which sense of it is meant        abrasive-grit
    context      Cx prefix, then CapitalCamelCase               CxUniverse, CxCore
    lexeme       the `lex` namespace; the name is parse input   lex/fool's_gold

  Single lowercase words (dog, genl, parentOf) satisfy both `predicate?` and
  `type-symbol?`; role is disambiguated by position and arity, not the symbol alone.
  A sense is a type too, so it is unary for the same reason, and a lexeme is the one
  role a *namespace* decides — its text is a surface form and not ours to spell.
The spelling is a **biconditional on arity**.  A functor carrying an underscore is a
  type name and nothing else, and types are used as *unary* predicates — `(dog Muffet)`,
  not `(isa Muffet Dog)` — so it is legal at arity 1 and nowhere else.  And the converse
  now holds too: a *camelCase* functor at arity 1 is refused, because a one-place
  predicate is a kind or a property rather than a relation between terms, and the whole
  point of a spelling that reads a role is that it reads it in both directions.
  `(lives_in penguin cold_place)` is a type name doing a relation's job;
  `(warmBlooded Muffet)` is a property wearing a relation's spelling.  A bare lowercase
  word (`dog`, `alive`) satisfies both conventions and is caught by neither, which is
  where the rule stops: it marks the names that carry more than one word.

  How hard these are enforced is the **KB's** to say, not this namespace's: `open-kb`'s
  `:naming` selects `:strict` / `:warn` / `:off` (`policies`, below) and `assert` reads
  it.  The predicates themselves do not move — `:off` stores a name nothing can classify,
  not one classified differently.

  `problems` checks the functor of every literal a sentence contains — a rule's
  antecedents, its consequent, an `exceptWhen` query's conjuncts, a `not` body, an
  `ist`-directed sentence, a negation-as-failure query — not only the outermost one.
  A rule consequent is exactly where generated content lands, and the outermost
  functor there is `implies`.

Non-atomic terms (NATs) via reification — Strategy A.

A NAT is a function-application term `(F arg…)` that denotes an entity —
`(FruitFn AppleTree)`, `(CapitalOf France)`.  A function splits by declaration
into two kinds:

  (reifiable_function F)    object-denoting.  A ground `(F a…)` is a **reified NAT**: it
                           reifies to an opaque `nat/`-namespaced constant `K`
                           *before* it reaches the index, so the reified NAT autoindexes
                           exactly like a hand-minted symbol — no trie-key change,
                           no term-index change.
  (unreifiable_function F)  evaluated/interpreted.  The NAT is a **structural NAT** and stays
                           *structural* — `(QuantityFn 5 Meter)` keeps its magnitude
                           and unit readable for a downstream prover; it is never
                           minted.

The constant↔expression map is itself an ordinary stored fact, `(termOfUnit K E)`
in CxUniverse, so the inverted term index makes `E`'s constituents (and `K`)
discoverable natively — no KV side tables.  `K` stays STABLE across renames: a
rename rewrites the expression inside the one `termOfUnit` sentex in place, and
nested NATs referencing `K` need no cascade.

This namespace holds the detectors, the index-backed lookups, display expansion,
and the reify — **both** modes: the read-mode (dedup, never mint) and the
write-mode (mint a fresh constant, materialize its result types, merge rename
collisions).  The write-mode stores its `termOfUnit` and result-type facts through the
full assert path, reached by `vaelii.impl.wiring` — which is where the reason that is
not an ordinary require is written down.  So all NAT reification lives here.

What sits above this and *calls* the reify rather than reimplementing it:
`vaelii.impl.skolem` mints the witness an existential rule head fires to, and
`vaelii.impl.nat-maintenance` sequences the post-assert reconciliation and drops an
orphaned reified NAT when its last use is retracted (it rides the `retract!` sweep).

Reads the store, the taxonomy and belief directly (nat <- kb); reaches assertion only
through the fns above.

The reified-NAT maintenance the write paths run once their own work is done —
docs/nat.md, docs/context-nat.md.

Three entry points, one per site in `vaelii.core`:

- `reconcile-assert`, after a sentence is stored: the collision merge an equality may
  have caused, the correspondence reconciliation, and the structural `genlCx` edges the
  new fact entails.
- `reconcile-revivals!`, after a teardown has settled: the edges the producer could not
  build while their declaration was OUT.
- `collect-orphans!`, on the same teardown: the reified constants no live use
  references any more, removed to a fixpoint.

Sits above both `vaelii.impl.nat` and `vaelii.impl.context-nat`, because the assert-path
sequencing spans the two, and above `vaelii.impl.settle`, because a computed `genlCx`
edge owes a chain and a settle of its own.

The teardown entry point is an **argument**, not a require: the orphan sweep retracts
through `vaelii.core/retract!`, and the engine never requires the API namespace
(docs/namespaces.md, "The layering").  `vaelii.core` hands its own `retract!` in.

The leaf extension point the engine's mutation choke points notify **without a require cycle**.
Two things ride on it, and they are independent: named observers of the stored fact
set, and one counter saying that *something* changed.

**Observers.**  The incremental rule-matcher (`vaelii.impl.rete`) keeps RAM alpha
memories that must mirror the stored fact set exactly.  The only structural mutations
to that set are `kb/create-sentex` (add) and `integrate/sentex-removed!` (remove), but
both of those namespaces sit *below* `rete` in the layering — `rete` needs `kb`,
`resolution`, and `plan` to match — so they cannot call it directly.  They call the atoms
here instead, and `rete` installs itself into them when it is engaged.

When nothing is engaged the atoms hold `nil` and `notify-*` is a single deref plus
a `nil?` check, so the reference forward chainer pays essentially nothing.  The
observer is global rather than per-KB (single-writer, like the rest of the engine);
the installed functions dispatch on `kb` themselves, so several KBs can be live at
once and each keeps its own alpha memories.

**The change clock** is the cheapest possible version of the same idea, for a cache
that has to notice a change nobody registered to hear about.  See `note-change`.

**The resident caches** the clock exists for are here too (`cached`), and each declares
itself to `vaelii.impl.caches` at the bottom of this file so a reader can see what the
process is holding.