Using the notebook? Start with guide/QUICKSTART.md: install, the tutorial, a notebook of your own and one over your code. The rest of this page is the language and the repository.

Nothing to install: disentinel.github.io/rofl runs a notebook in the browser. Drop a .rofl.md on it (with the files it reads, or its folder), or link one: ?gh=owner/repo/path@ref or ?url=<a GitHub or raw link>, for example ?gh=Disentinel/rofl/examples/visual/claim-proof.rofl.md.

ROFL v1

ROFL — Relation-Oriented Fixpoint Language. A Datalog-family language with perspectives (first-class truth contexts), explicit time, kernel-emitted provenance, structured terms, and budgets. Turing-complete by design; budgets are part of the semantics.

Also known as Reshetnikov's Opinionated Formal Logic

Also known as Research -> Observe -> Formalize -> Lock

The kernel is a generic inference machine: all semantics — including the schema of what a "rule" is and the rules that validate rules — live in the graph as data (boot.rofl). The engine is Rust (the rofl binary under rust/, one native file); the TypeScript engine under src/ is the parity reference, has zero runtime dependencies (the optional code scanner under scanners/ is the only component with one, @babel/parser) and runs under Node ≥ 22.

Using it

npm i rofl

import { readFileSync } from 'node:fs';
import { Rofl } from 'rofl';

const r = new Rofl();
r.load(readFileSync('node_modules/rofl/boot.rofl', 'utf8'), 'boot.rofl');
r.load(`
  edge(a, b). edge(b, c).
  path(X, Y) :- edge(X, Y).
  path(X, Z) :- path(X, Y), edge(Y, Z).
`, 'p.rofl');
r.evaluate();

r.query('path(X, Y)').rows;   // a->b, a->c, b->c
console.log(r.why('path(a, c)').text);

path[main](a,c)  <= rd2f1f53d @tick 0
  path[main](a,b)  <= r7e93750a @tick 0
    edge[main](a,b) [axiom]
  edge[main](b,c) [axiom]

Plain node, no flags, no dependencies — the published tarball is the compiled engine and nothing else. boot.rofl is the semantics as data and carries the audits; a program loads without it and answers less about itself.

The libraries that ship with it

rules/inquiry/ is a discipline for deciding things under incomplete evidence — claims, evidence with polarity and freshness, four epistemic grades (supported, refuted, contested, unknown), obligations that block or merely require, and authority-gated acceptance of a residual gap. rules/policies/ holds the two policies it reads. rules/decisions/ holds two decision packs built on it. They are written in ROFL and shipped as ROFL: read them, change them, or take the four lines you want.

import { fileURLToPath } from 'node:url';
const at = (s) => fileURLToPath(import.meta.resolve(s));

// ORDER MATTERS: a pack is loaded before the packs that read it.
for (const f of ['inquiry/ontology.rofl', 'inquiry/terminology.rofl',
                 'inquiry/epistemic.rofl', 'inquiry/obligations.rofl',
                 'inquiry/intents.rofl', 'inquiry/perspectives.rofl',
                 'policies/evidence.rofl', 'policies/authority.rofl',
                 'decisions/production-readiness.rofl']) {
  r.load(readFileSync(at(`rofl/${f}`), 'utf8'), f);
}
r.load(`
  inquiry(ship_it, decide).
  pack(ship_it, production_readiness).
  decision_authority(ship_it, vadim).
  claim(tests_pass). blocking(ship_it, tests_pass). observable(tests_pass).
  refutes[obs](ci_run, tests_pass). evidence_kind[obs](ci_run, measured).
`, 'mine.rofl');
r.evaluate();
r.query('recommendation(I, V)').rows;   // ship_it -> no_go

and why answers for the verdict the same way it answers for anything else:

recommendation[main](ship_it,no_go)  <= r989a9b8b @tick 0
  violated_blocking[main](ship_it,tests_pass)  <= r05e01676 @tick 0
    inquiry[main](ship_it,decide) [axiom]
    blocks_on[main](ship_it,tests_pass)  <= r6e89f9d7 @tick 0

The other forty rule packs in this repository are models OF this repository — its JavaScript, its ledger, its own layering — and do not ship.

Large worlds are the other engine's. src/ is built for small ones; the Rust engine is reached through the same JSON protocol from rofl/port, and the division is deliberate rather than a staging post — see docs/port-surface.md.

Everything below this line is for working ON the engine rather than with it.

What is in the tree

The kernel is one of several things here, and the rest of the file says which of them a claim is about. npm run … names in the right column are the entry points; the whole list is in package.json.

where	what it is	entry point
src/	the kernel: parser, store, evaluator, reflection, API, REPL. Zero runtime dependencies, closed vocabulary (below), mechanically checked	repl
boot.rofl	the semantics as DATA — what a rule is, the rules that validate rules, the audits	loaded by every store
policy.rofl safety.rofl	the kernel's own two programs, carried as data rather than as code — see The kernel's own programs	gated by test/kernel-policy-program.test.ts (gate removed 2026-09-11)
scanners/	code and cost turned into facts: the JS/TS source scanner, the JS model, the Python AST scanner (py_ast.py, its model in rules/py-model.rofl, grown for the question in examples/jodit/), and the self-measuring scanners this repository argues with	scan evalcost parsecost ruleshape perminv
rules/	the inquiry kernel, the decision packs, the JS model's rule packs (js-*.rofl: since 1.1 js-surface.rofl, the [surface] book a file shows the others, docs/surface-split.md, and js-concat.rofl, a string built from parts as a node with parts and its text as a term), the service graph (js-fetch.rofl, js-express.rofl, js-service.rofl) and the net library it walks (net/: names, addresses, listeners, hops, guards, tls), the stage plan's checks (stage-plan.rofl), the aggregates programme (agg.rofl), and the rule packs that used to live in boot.rofl	report findings test:split
shrug.rofl	the closed vocabulary of a shrug, the third answer: every cause and reason an engine may write in shrug(Target, Reason, Meta) (docs/aggregates.md)	compiled into src/kernel-dense.ts by build:dense
runtime/	the report renderer, the admission gate, the scheduler, the tick loop, the port client	report pair
adapters/	the storage port: a FactStore behind an interface, with a SQLite adapter, gated by a byte-identical canonicalState() against the in-memory reference	boundary
rust/	the Rust engine, and the reference for performance (CLAUDE.md, Rust is the engine): one binary, rofl (load, load --seed, serve, render), under rust/rofl/src/bin/rofl/; the engine's new parts since 1.0.5 are engine/ (delta.rs plans fired from their news, addition.rs facts and rules added to an evaluated world, prov.rs provenance written when asked, vclosure.rs a declared closure answered from its tree, alias.rs an alias read from its source, resume.rs a stop by budget continued, par.rs a round's level over threads, cost.rs the rule that blows up named while it runs, latkept.rs lattices kept with a volume, labeled.rs, datastrat.rs, joinplan.rs), volume.rs/store/volume.rs/arena.rs (a kept world opened mapped, docs/staged-evaluation.md), cell.rs/tag.rs/shrug.rs (aggregates), structure.rs/structures.rs/forest.rs (declared structures and their detection report), md/ (a .rofl.md read into rules, the port of scripts/read.ts, held to it by npm run mdcheck)	cargo test under rust/
scripts/	the harnesses: goldens.ts (test, bless), whycheck.ts, mdcheck.ts, agg_mutants.ts and agg_breaks.ts (test:agg, test:agg:breaks), surface_split.ts (test:split), structures.ts, render_docs.ts (docs), pool.ts (the ROFL_JOBS pool); vscode_corpus.ts and vscode_curve.ts build the vscode subset and measure the side-effect question over it, vscode_pieces.ts evaluates it in pieces of a fixed time, each its own process; stage_plan.ts plans a corpus into stages under a memory limit and runs them; bench.ts is the reference benchmark (bench, facts/bench.rofl); js_lab/ is the rule-rewriting lab of docs/optimising-a-world.md	test whycheck structures
examples/ facts/ docs/	runnable demos, the ledgers and goldens, the design decisions. New since 1.0.5: examples/checks/ holds the small proof worlds of the engine (aggregates, demand, asks, trees, addition), examples/vscode/ the side-effect question over a vscode subset (side-effects.rofl, its notebook, mini/ and split/ corpora), examples/surface/ the surface lint, examples/concat/ path values, examples/shapes/ the costly-shape finder, examples/services/ the service graph over two small services; facts/commands.rofl is the source of CLAUDE.md's commands and knobs, facts/surface-lint.rofl and facts/cost-shapes.rofl the registers of the surface lint and the costly shapes	test
visual/	the view vocabularies a notebook draws with (graph, time, table, space, notation) and viewpoints.rofl.md, sixty viewpoints to pick a picture by (docs/schemas.md); a cell's draw K shows them, VS Code draws a graph as a schema (vscode/visual/schema.ts), notebook/draw.ts writes them as mermaid, DOT, Argdown, Markdown, Vega-Lite (docs/renderers.md, examples in examples/visual/)	nb playground

Documents

docs/ fixes decisions so they do not have to be re-argued. They are grouped by what they bind.

The model — time-and-continuity.md (what not p means, where a veto belongs), choosing-perspectives.md (perspective = ledger, never status or modality), books-and-permission.md (every relation with who may write it, derived from boot.rofl and gated by test/permission-doc.test.ts (gate removed 2026-09-11)), inquiry-kinds.md (typed inquiry roots), three-valued-answers.md (the alternating fixpoint and what unknown means), intents.md (a world that wants: want heads, capabilities declared in an adapter's book, adapters as federated books; designed, not built).

A run — scaling-a-corpus.md (the incremental ingest loop over the whole of eslint, and the four defects the run found that reading did not), normalisation-and-profiling.md, volumes-and-residency.md (how a corpus stays cold), working-with-ledgers.md, test-maintenance-cost.md, failure-modes.md (the process failures, catalogued and priced), schemas.md (how a graph is drawn, which viewpoint to pick for a question), optimising-a-world.md (a cookbook: how to measure a world on Rust release, the seal, the costly rule shapes and their rewrites, aggregates, declared structures, demand; each recipe with its measured gain and its finding).

The process as its own subject — three documents that turn the question where does a claim about this work live into something checkable. ledger-as-an-instrument.md reads the ledger as a thing with functions, side effects and contradictions rather than as a log. claims-outside-the-store.md measures the gap: measured holds 3 rows while the word MEASURED appears in 436 comment lines, and 2 210 comment blocks over 78 files carry no verdict at all. Failure mode 17 in failure-modes.md is the entry they answer.

The engine and the port — the-target.md (what everything on this branch is instrumental to), medium-and-large.md (two engines, and the line between them, which negation decides), port-surface.md (what the Rust engine has to expose), performance-invariants.md (what this kernel costs and what the field costs), data-structures.md (declared structures: a promise the system checks and a licence for the engine to store a relation as a tree, an alias, a key, a span), demand-cones.md (answering a question in the part of the world it reaches: the asks cone, when it is the whole world, what it saves, what growing it needs), staged-evaluation.md (a world evaluated in stages that fit memory: kept volumes, resume after a budget, the stage planner), modelling-a-language.md (the JS model as a research programme), aggregates.md (every aggregate class as one cell engine with two syntaxes, and the matrix that holds the work to it), surface-split.md (a file as a volume with a resident [surface] book of what escapes it: the crossing measured on vscode, the book rules/js-surface.rofl, the parity world and the lint that hold it, and the driver), knobs.md (every flag and ROFL_* variable of the tree with its verdict: the few an agent uses are CLAUDE.md's table, the rest are oracles of a check harness or leftovers).

The plan — roadmap.md (what the next version commits to, each item naming the finding that holds its evidence). sentence-form.md closes one question of the plan: the Markdown sentence form as a source after 1.1, what the round trip established, what the form is now, and what is open. releases/1.4.md is what changed since 1.3.2, what an agent must do differently and the known gaps; releases/1.3.md, 1.2.md and 1.1.md (since 1.0.5) before it.

The programme — formal-reasoning-landscape.md (ROFL among the formal reasoning systems, and why the projection is ROFL-centric by construction). The plan itself is the ledger.

The other entry points — what a user meets besides the language:

• Writing a world as Markdown — md-world.md (ROFL 1.05): the sentence form as a source, X.rofl.md (executable Markdown; a plain .md is a document), how to write one, what the reader reports; examples/review.rofl.md is one, and npm run repl -- examples/review.rofl.md asks it in its own sentences.
• The JS playground — playground/, built by npm run playground into playground/dist: JavaScript on one side, a notebook over it on the other, the engine, the scanner, the reader and part of the JS model running in the browser. The code may be several files importing each other. A formal cell is written in sentences, as a .rofl.md is, and a rofl cell in plain Datalog; ? S lists, never S is an invariant, unsure S under it says what it could not see, why S explains; a natural cell is translated by Claude when the page runs as an artifact.
• The notebook — notebook/: a notebook is a .rofl.md world whose fenced ```rofl (sentences), ```datalog (plain ROFL) and ```natural (plain language) blocks are its cells; model: js, code: and reads: in the front matter name the model, the code and the worlds it stands on. npm run nb -- F.rofl.md [--json] [--cell N] [--all] runs it and prints the answers with the file:line of each code node (twelve a line in the text, fifty in the JSON, every one with --all), exit 0 / 1 (a never fails) / 2 (something not read) / 3 (every never holds, some only as far as the model sees); npm run nb -- edit F.rofl.md --cell N [--lang L] writes the new text of cell N from stdin (N one past the last adds a cell), only if the file then reads back as written, the way for an agent or a script to change a notebook; npm run nb -- translate F.rofl.md writes a rofl cell under each natural one with the model npm run nb -- models names (VS Code's own language model in the editor; notebook/model.ts runs each command-line harness with no tools), only after it read, and saves each as it lands; npm run nb -- vocab [F.rofl.md] [word] lists the sentences a cell can use (the JS model's, or that notebook's), those with the word, and a sentence that is not read names the three nearest. The kernel (notebook/kernel.ts) does no I/O; the command line is a printer over it. The goldens load every notebook under examples/<dir>/ as a world, read in its model's words but without the model. examples/notebook/self.rofl.md is the notebook's own acceptance, npm run test:nb and npm run test:nb:product (the kept kernel, the harnesses, what a user meets first) the behavioural half.
• The notebook kept alive for the command line — notebook/serve.ts: npm run nb keeps its kernel between runs. The first run starts a background process that holds the evaluated code model; later runs send it the notebook over a unix socket and print exactly what an in-process run prints, with the same exit codes. Every run re-reads the notebook, the code files and the read worlds, so an edit is always seen. The daemon exits after 60 idle minutes (ROFL_NB_IDLE seconds), a new one starts when the engine's source changes, and a dead or refusing daemon leaves the run to the process itself. Nothing to set up; ROFL_NB_DAEMON=0 turns it off. Over the Grafema MCP package (40 files) a cell edit is about 9 s through it against about 64 s in a fresh process; npm run test:nb pins its answers against a fresh process.
• The notebook in VS Code — vscode/: npm run vscode -- <dir> opens a window with the extension loaded (VS Code 1.132 or later: it runs the TypeScript unbuilt; the packaged VSIX built by npm run dist ships plain JS and needs only 1.101, per dist/INSTALL.md); any .rofl.md opens as a notebook, prose as Markdown cells, the front matter and the fenced blocks as code cells, and the file is written back byte for byte. Run All goes through the same runFile as the command line, in a worker that keeps the model loaded; each code node in an answer links to its line, a failing never is an error in the Problems panel on its line and on the code lines it names, and Translate natural cells inserts the translation as an unsaved edit. npm run test:vscode (the round trip, the smoke run in the installed VS Code and one planted defect) and npm run test:vscode:mutants (three more; -- --break NAME runs one by name) are its tests; cd vscode && npm ci once for them.
• The NPC yard, live — playground/npc.html, built with the playground: examples/npc run one tick at a time in the browser, each agent's knowledge, intents, options and chosen act on the page, why and whynot on any of them at any kept tick, the rule the agents propose from their holes, taken and applied to the past, and the loop the declared tie order walks the yard into, noticed, explained from tie[audit] and broken by three rules taken at run time; the night ends at the model's own horizon. The yard's core is examples/npc/sim.ts, which demo.ts also runs; its sentences are examples/npc/phrases.rofl.
• The JS model, rendered — docs/js/, the JS model's rule files (twenty-one since 1.3: js-surface and js-concat joined in 1.1, js-fetch, js-express and js-service in 1.3) as Markdown with a link on every use, by npm run render:js (needs cargo build --release in rust/); phrases in facts/js-phrases.rofl. npm run view -- docs/js makes one HTML page of them to open in a browser, with the reader's own Markdown parser (scripts/md_blocks.ts). npm run read reads a rendered file back into rules (the reading itself is readMd in scripts/read_md.ts, a function with no file access, which the playground runs in a browser); npm run untyped (rules/untyped.rofl.md, a world authored as Markdown with no .rofl twin, read into rules by npm run read) lists the one-letter variables nothing in their rule types.
• The rings, in their own words — docs/rings/: the kernel's four programs of rules (boot.rofl, safety.rofl, policy.rofl, rules/strata.rofl) and the front end written in ROFL (examples/ring1/ring1.rofl, charclass.rofl) and its host's contract (examples/ring1/host.rofl, checked by npm run conform) rendered as sentences by npm run render:rings, phrases in facts/kernel-phrases.rofl and facts/ring1-phrases.rofl; each reads back into its source clause for clause. docs/rings/README.md says what is there and what is not.

How to run

# the loop: every world, both engines, against facts/goldens.rofl (CLAUDE.md)
npm test                      # Node ≥ 22.6, type stripping; needs `cargo build --release` in rust/
npm run test:bun              # the same under bun, by hand

# REPL
npm run repl                  # loads boot.rofl automatically
node --experimental-strip-types src/repl.ts examples/sensors.rofl

# typecheck (dev-only dependency; the runtime has none)
npm i && npx tsc -p tsconfig.json

Node ≥ 22.6 is not optional and the failure is quiet. The sources are erasable-syntax TypeScript run through Node's built-in type stripping. On an older Node npm test dies in five lines with node: bad option: --experimental-strip-types and prints no ℹ tests line at all — so a guard that only compares the reporter's numbers reads the absence as agreement. package.json declares the floor in engines; check what you are about to run with node -v before believing a green.

The gates

Every one of these is a check somebody paid for. A typecheck, the release build and npm test are what CI runs on every push (.github/workflows/ci.yml); the engine and the VSIX are built on main and release tags only; the rest are run by hand.

command	what it refuses
npm test	a world whose hash or per-relation census moved against facts/goldens.rofl, on either engine (it prints how many worlds and how long; npm run test:engine, test:library, test:mutants run the node --test suites)
npm run whycheck	a why, why all, whynot or excise of the Rust binaries that differs by a byte from src/api.ts, over every world npm test loads
npm run nbcheck	a notebook that rofl nb prints other text or another exit code for than npm run nb, over every one in the tree that rofl nb runs (not draw, code or model: js); needs a build
npm run mdcheck	a .rofl.md the Rust reader (rofl render, rust/rofl/src/md/) reads to other rules, sentences or report than scripts/read.ts, over every one in the tree; needs a release build
npm run test:agg:breaks	a planted fault of the engine (--features breaks) that no world turns red
npm run test:split	a file of the surface-split corpus that, alone with the others' [surface], differs from the whole world by a fact (both engines, both orders)
npm run structures -- --check	a detection report of declared structures that moved against its committed proof fixture
npm run textcheck	a byte in the tree that a human or grep cannot read
npm run speccheck	a duty in START.md that nothing in the tree discharges
npm run measurecheck	a number quoted without the run that produced it
npm run flagcheck	an API flag that no demo in examples/ EXERCISES (CLAUDE.md)
npm run findings	the open findings backlog — every one demands a reaction
npm run lint	-- <files>: heads with five or more bodies, relation pairs read together by five or more rules, bodies of seven or more conditions — counted by the counting semiring over the reflection, so no order on atoms is needed

And the scanners that MODEL something rather than check it — each writes facts that a rule pack then argues with, so every row has a why:

command	the question it answers
npm run evalcost + npm run whyjoin	where the join actually goes
npm run parsecost + npm run whyslow	what a parse costs, by stage
npm run floorcensus + npm run whyfloor	which reflection relations may be sealed
npm run perminv + npm run whyperm	who may write what
npm run ruleshape	which rule bodies pay a cross product
npm run keycoupling npm run booklocality npm run boundary	how coupled the store's key spelling, books and port surface are
npm run necessity	what is load-bearing and what is not

REPL commands: ? L, why L, whynot L, excise F, budget N { CMD }, load FILE, who NAME, retract F, tick, run [N], save FILE, restore FILE, facts [REL], quit; any other line ending in . is asserted as program text.

Code scanner

npm run scan -- DIR --out code.rofl turns a JS/TS source tree into the facts the JS model reads: scanners/js_ast.ts over each file and the host's path and string facts, as the notebook host gives them. Not part of the kernel — it lives outside src/ and the kernel grep test on purpose. The model then runs in the Rust engine:

npm run scan -- path/to/src --out code.rofl
rofl why 'flows[code]("api/server.js", "api/users.js")' @rules/js.files code.rofl

The stages, the relations each writes and the exit codes are in docs/cli.md.

Inquiry layer

rules/inquiry/ is the Phase 1 guided-formal-reasoning kernel (docs/inquiry-kinds.md, docs/choosing-perspectives.md): a typed inquiry root, epistemic states as a derived [epistemic] ledger over an [obs] evidence journal (authority: runtime only), proof obligations, and candidate-intent generation. runtime/report.ts renders the anytime epistemic report:

npm run report -- examples/atlas-launch/frame.rofl \
  examples/atlas-launch/evidence.rofl --who-obs runtime \
  --pack production-readiness examples/atlas-launch/context.rofl

The rest of the loop: runtime/admission.ts validates agent results (schemas/intent-result.json — agents cannot mint measured evidence, and unattributed admission is refused), runtime/scheduler.ts picks a top-K batch (blocking claims first), runtime/tick.ts runs the bounded derive → execute → admit → recompute loop with stagnation and budget checkpoints. rules/decisions/production-readiness.rofl is the first decision pack (GO / CONDITIONAL_GO / coverage gaps, authority-gated gap acceptance); rules/policies/ holds evidence freshness and authority. skills/guided-formal-reasoning/ is the agent-facing skill seed. Findings discovered while working live in facts/findings.rofl and replay at session start until settled (rules/findings.rofl, CLAUDE.md).

npm run build:skill assembles the self-contained marketplace bundle in dist/guided-formal-reasoning/ — instruction files at the root, the engine (kernel, rules, runtime, schemas, the synthetic demo fixture) under engine/, zero dependencies, runnable from any directory on bare Node >= 22.6. The build smoke-tests the bundle by running a real pair session inside it.

Grammar

program    := (clause ".")*
clause     := fact | rule
fact       := literal                           -- ground, atom perspective
rule       := literal ":-" body
body       := blit ("," blit)*
blit       := literal | "not" literal | builtin
literal    := rel persp? "(" terms ")" temporal?
persp      := "[" (name | Var) "]"              -- omitted => [main]
temporal   := "@init" | "@now" | "@next"        -- omitted => @now
terms      := (term ("," term)*)?          -- may be EMPTY: `p()` is a proposition
term       := Var | int | string | atom | functor "(" terms ")"
builtin    := expr OP expr                      -- OP ∈ {=, !=, <, <=, >, >=, is}
expr       := arithmetic over +, -, *, /, mod   -- ints; / truncates toward 0
Var        := /[A-Z_][A-Za-z0-9_]*/             -- `_` is a fresh wildcard
atom/rel   := /[a-z][A-Za-z0-9_]*/
comment    := "--" to end of line

The temporal set is exactly the three above. @async was reserved syntax until 2026-09-16 and is not reserved now — the effects executor is not going to be built, so the word was holding a place for nothing, and it is refused as the unknown marker it is (LIMITS.md). @next is not allowed in bodies; @init is not allowed on rule heads.

A relation may take ZERO arguments, spelled p() — added 2026-09-10, and the grammar above says so (terms may be empty). A relation of arity n is a set of n-tuples and there is exactly one 0-tuple, so a nullary relation's extension is either empty or that singleton: it is a truth value, and a proposition is the base case of the predicate logic this language already was. It was excluded until then by one production written the obvious way, with no reason recorded anywhere and with the store already able to hold one.

The spelling is p() and never a bare p: a body element is tried as an expression before it is re-read as a literal, and a term is also an atom, so ident ( ) is the one shape that needs no lookahead into what follows. examples/flag/ exercises it; npm run nullary reports which existing rules are propositions wearing a dummy argument or a passenger variable.

Kernel vocabulary

Reserved, write-protected: domain rules may read these, never conclude into them (a rule concluding into one is rejected at load; hand-asserted reflection surfaces as breach in boot.rofl). This is the closed list of relation names the kernel knows, plus the read-interface below — mechanically enforced by the two engines agreeing, since scripts/kernel_grep.ts was deleted on 2026-09-10 (15 commits of appeasement, 3% coverage).

relation	arity	meaning
derived_by(Fact, RuleId, Tick)	3	provenance, emitted on every derivation; Fact is a $fact(Rel, Persp, Args) term
rule(Id) has_premise(Id,K) premise_pos(Id,Rel) premise_neg(Id,Rel) concludes(Id,Rel) has_conclusion(Id,K)	–	reflection of rules as subgraphs
premise_lit(Id,K,Lit) conclusion_lit(Id,K,Lit)	3	full reified rule content ($lit/$not/$builtin terms); the evaluator's only rule source
conclusion_tense(Id,Tense)	2	the head's temporal marker, now or next — the one part of a rule's tense a rule can read, since the marker itself lives inside the $lit of conclusion_lit
reads_from(Id,Persp) writes_to(Id,Persp)	2	perspective signature of a rule (a variable perspective is recorded by name, as $var("S"))
bridge_decl(Id,From,To)	3	explicit head annotation crossing perspectives
asserted_by(Fact,Who,Tick)	3	the dated assertion trail: who asserted the fact, and in which tick — emitted only when a who is given. The tick is the clock at the moment of the assert, never of a later evaluation, so replaying the trail rebuilds a past state instead of storing it. A fact asserted twice keeps two rows, and each pairs its own who with its own tick
uses_builtin(Id,Op)	2	rule uses builtin Op (a string)
mode(Builtin, ModeList)	2	declared directionality of builtins, kernel-emitted at boot
reserved(Rel)	1	this table itself, queryable
authority(Persp, Who)	2	who may assert; kernel registers each perspective on first use as authority(P, $kernel)
hole(QueryId, Reason)	2	inability marker — the kernel could not finish, said so rather than returning an empty answer that reads like an honest no. Ids: $q(N), $tick(T), $load(N), $adhoc, $rule(Id), and $next(Rel, Book, T, Args) for a conclusion a hole kept from being staged into tick T, unknown there. Reasons: budget_exhausted and space_exhausted when an evaluation runs out of steps or of rows it may hold; arith_type_error, arith_zero_divisor and arith_overflow (a result outside [-2^60, 2^60), never a wrapped one) for an is whose expression could not be evaluated; support_withdrawn on a rule whose negation could not decide, for what a hole left out could have matched, and fault_left_out on what such a conclusion carries into the next tick (see Arithmetic that cannot be evaluated below); and str_type_error, str_index_error, str_empty_separator for a string destructor given an operand it cannot take; and reflection_sealed, the one reason that is not a failure — the program declared sealed(Body) and the kernel stopped keeping that body, so the answer is missing on purpose. Id $sealed(Body) for the standing declaration, $q(N) for a query that asked a sealed body
edb(Rel)	1	relation has base facts (also emitted for all reserved relations at boot)

in_perspective(Fact, Persp) WAS IN THIS TABLE AND IS GONE, removed from the kernel because it was a projection of its own key — Fact IS $fact(rel, persp, args), so the relation stored the second argument of the term it was keyed by. Measured before removing it, on 16 eslint files: 41 722 rows, a third of the world. Every rule that read it destructures the term instead. The row survived here, and in the grep check's whitelist, until 2026-09-10 — which is the tidiest possible argument against a hand-kept vocabulary list: the check whose job was to keep this table honest was itself carrying a name the kernel had deleted.

Read interface (not reserved): the kernel reads stratum(Rel,N) and unstratified(Rel), never writes them; rules may conclude into them. §3.2 of the spec names these two as the whole stratification contract between kernel and boot, and they are in the grep-test whitelist.

It is no longer two names, and the whole set is below. Every row is a relation whose name appears in kernel source because a PROGRAM writes it and the kernel reads it, or the other way round — never because the kernel hardcodes a domain. The table is the grep-test whitelist's IFACE_RELS, and that is a measured identity rather than a promise: test/vocabulary-doc.test.ts (gate removed 2026-09-11) re-derives both sides on every run and refuses a name that is in one and not the other. Every relation from policy.rofl and safety.rofl down is concluded by the kernel's own programs — see the section under this one.

relation	written by	read by	what it says
stratum(Rel, N)	the program, and boot.rofl for its own relations (boot_rank, copied into it every tick; examples/checks/strata-boot-canon-check.rofl holds those ranks to what rules/strata.rofl derives over boot)	the kernel	the phase a relation settles in. Computed on the primary path instead (peelRounds), so only the stock evaluator reads it
unstratified(Rel)	the program	the kernel	the program is unstratifiable — the stock evaluator's refusal
semantics(Sem)	the program	the kernel	semantics(well_founded) asks for the alternating fixpoint instead of the phase-ordered run
unknown(Atom)	the kernel	the program	one row per atom the alternating fixpoint leaves undefined, in the atom's own perspective. why unknown(win(a)) is answerable
sealed(Body)	the program	the kernel	the floor-sealing declaration — one of rules, assertions, provenance is no longer published. READ, never inferred; see the last section of this file
rule_reads(A, B)	policy.rofl	the kernel	A's rules look at B, positively or negatively, ACROSS the tick boundary
rule_relation(A)	policy.rofl	the kernel	every relation the rules mention, on either side
cone(A, C)	policy.rofl	the kernel	the reflexive-transitive closure of rule_reads — the dependency cone the reuse plan needs
opaque_closed(A)	policy.rofl	the kernel	A holds something the evaluation cannot promise to reproduce, closed upward through reads
opaque_seed(A)	the host	policy.rofl	the seed of that closure. It stays with the host because it needs a premise's tense and a store-shape fact the reflection does not carry flat
unsafe_rule(R)	safety.rofl	the kernel	R's body does not bind everything its head or its builtins name — the range-restriction verdict, which used to be a fold in TypeScript
premise_var(R, K, Slot, I, V) slot_arity(R, K, Slot, N)	the host	safety.rofl	the two inputs the reflection does not carry flat: which variable stands where in a premise, and how wide a slot is
late_rule(R)	safety.rofl	the kernel	a monotone rule that may not run before the program has judged itself
demand_rel(Rel)	safety.rofl	the kernel	Rel is unfolded top-down at call sites rather than materialized
trigger_of(P, X)	safety.rofl	the kernel	what a positive premise on P can set off
neg_relation(A)	safety.rofl	the kernel	some rule negates A
provenance_reader(R)	safety.rofl	the kernel	R reads derived_by — so provenance cannot be pruned out from under it

Term and string destructors (Out is op(In, …), seven of them). They are not relations and they are not arithmetic: the parser has exactly one term-producing builtin form, so the output is the LEFT operand of is and the declared mode is [out, in, …]. Indices are CODE POINTS, not UTF-16 code units — indexing by code unit can cut a surrogate pair in half and hand back half a character, which the store would then carry. Operands compose, so str_len(str_seg(S, Sep, 0)) is the length of the first segment.

destructor	inputs	what it answers
str_len(S)	1	length of S in code points
str_char(S, I)	2	the code point at I
str_sub(S, I, L)	3	the substring by RANGE — what the separator-based cuts cannot say
str_pre(S, Sep)	2	the part before the FIRST Sep, and empty when there is none — the one thing str_seg(S, Sep, 0) cannot say, since that answers the whole string when the separator is absent
str_seg(S, Sep, N)	3	the Nth segment. The argument list admits TERMS and not expressions, so the last segment is N is str_segs(S, Sep), K is N - 1, T is str_seg(S, Sep, K)
str_segs(S, Sep)	2	how many segments — and it is what tells str_pre's empty answer apart from an empty first segment
atom_of(S)	1	the atom of a string. It crosses a sort boundary and produces a TERM; a term only becomes an executable rule through the reflection rows, which breach[audit] and the write protection on conclusion_lit already watch

Three refusals, kept apart because they demand three different repairs, and each arrives as a hole rather than as silence: str_type_error (the program is wrong — no data makes a number into a string), str_index_error (the data reached a boundary the program did not guard; the repair is a premise), str_empty_separator (an empty Sep, which two of five operations once accepted in silence). An UNBOUND operand is not a refusal, for the same reason it is not one in arithmetic.

They are no longer on the primary path. The default evaluator peels its phase order off the decoded rules before a single rule fires (src/aggeval.ts, peelRounds): round 0 is every relation no @now rule concludes, round N is every unsettled relation whose negative dependencies all settled earlier, closed under positive dependency. The round number is the stratum number, and a round that settles nothing while work remains is the refusal — no table, no unstratified/1, nothing derived about the program in order to run it. The stock evaluator survives as new Rofl({ evaluator: 'strata' }) and still reads both names; rules/strata.rofl is the ten rules that supply them, which boot.rofl carried until nothing needed them. boot.rofl still ranks ITS OWN relations, as data (boot_rank, ten rows), so a strata world with boot alone loads and answers; a program's relations stay the program's to rank. See the deviation register below.

Two more names are on the same footing, and they are the whole three-valued contract: the PROGRAM writes semantics(well_founded) to ask for the alternating fixpoint instead of the phase-ordered run, and the kernel writes one unknown(Atom) row per atom that fixpoint leaves undefined — in the atom's own perspective, with the atom as an ordinary term, so why unknown(win(a)) can be typed and answered. Rules may read unknown; a rule that conclusions its way back into a negated relation through it is rejected, because the answer was settled before those facts existed. Under this semantics stratum/2 is not computed — a program whose rules conclude it is told so in a diagnostic, because its own rule diverges on a negative cycle, which is what a negative cycle MEANS for a stratum number. The cycle is still reportable, as a fact about the program rather than a verdict on it: peeling the same rules names every relation that can never settle, which reaches further than unstratified/1 did — it includes relations that merely negate something on the cycle. See docs/three-valued-answers.md.

Audits over this vocabulary (boot.rofl, all in [audit]). Six are about BOOKS AND PERMISSION — leak, forged, collected, exported, unattributed, widened — and the whole model for those is in one place: docs/books-and-permission.md, derived from boot.rofl and gated by test/permission-doc.test.ts (gate removed 2026-09-11). Four are STRUCTURAL and required empty on load: malformed — a rule with no premises or no conclusion; breach — a rule concluding into a reserved relation; unmoded — a rule using a builtin with no declared mode; and undefined_premise(RuleId, Rel) — a rule with a positive premise on a relation that no rule concludes and no base fact populates. That rule is not wrong, it is unpopulatable: hit(N) :- msg(N, S), contains(S, "404") loads clean because contains is not a builtin, and hit is then silently empty forever. edb(Rel) doubles as the declaration that a relation comes from outside the program, which is why boot.rofl declares edb(imports) for its own host-supplied perspective-import graph.

$-prefixed atoms/functors ($lit, $not, $builtin, $var, $fact, $cons, $nil, $any, $kernel, $q, $tick, $load, $rule, $sealed, $init, $now, $next, plus $adhoc for an evaluation nobody named and $t for a query's own term) are the kernel's reification markers. A program can write them too: examples/ring1/ring1.rofl builds $lit, $cons and $var in its heads, and examples/ring1/demo.ts says how a source term written $var("X") stays apart from the kernel's own. $kernel_authority is the one a FILE may carry: as the FIRST clause of the FIRST load it says the text being read is the kernel's own, so everything in it is signed $kernel rather than user. Both conditions are load-bearing — a file cannot slip the claim in halfway, and after that first load the door is shut for the life of the store, with a second claim REFUSED rather than ignored.

The kernel's own programs

Every rule in policy.rofl and safety.rofl was a decision the evaluator made in TypeScript. They are the same move the kernel already makes with boot.rofl, taken one ring further in: the kernel does not merely READ a program that describes rules, it SHIPS one, the way bootstrapKernel already ships facts into every store.

• safety.rofl — range restriction, and everything that rests on the verdict. A left-to-right fold over the body tracking bound variables was Evaluation.classify; it is now unsafe_rule/1, plus late_rule, demand_rel, trigger_of, neg_relation and provenance_reader derived from it. No negation stands inside the fold, so the program is stratified and the default evaluator answers it.
• policy.rofl — what the reuse plan may keep: rule_reads (which is dep from rules/strata.rofl WITHOUT its same-tick filter, because a @next conclusion is still something the rule read), the dependency cone, and opaque_closed. Measured set for set against the host's own walk over Evaluation.rules: boot alone 35 pairs, +strata 52, +findings 51, +kernel-policy 64, +the ring 1 grammar 248 — agreeing on every one.

Why it has to be shipped rather than loaded. A rule that is not loaded is not a conservative answer, it is a wrong one, and 22 of the 95 worlds in this repository never load boot.rofl. So each file is the SOURCE and src/reflect.ts carries a copy — the shape examples/ring1/l1.dense.rofl already has, a program in two forms, one readable and one the machine installs. That is only honest with a gate keeping them identical, which test/kernel-policy-program.test.ts (gate removed 2026-09-11) is.

Two inputs travel the other way, from the host INTO the programs, because the reflection does not carry them flat: opaque_seed needs a premise's tense and a store-shape fact, and premise_var/slot_arity need which variable stands where in a premise. They are declared edb for exactly that reason.

The Rust engine

rust/ is the port, and docs/the-target.md is what it is for: a Rust engine that can chew all of grafema's code. Everything on this branch is instrumental to that, and a piece of work that cannot say which rung it moves is not on the path. docs/medium-and-large.md draws the line to the engine after it, and the line is not a size threshold — negation decides it, because not p(X) asserts something about a relation's WHOLE extension, so a relation that is negated anywhere cannot be answered from a part of the corpus.

• rust/rofl/ — the engine. session.rs is the surface docs/port-surface.md designs, gated by rust/rofl/tests/session.rs. What that gate found on its first run is why it exists: the design says "ask(query)" without ever writing a query down, and the first implementation invented rel@book(args) for a language whose book is rel[book](args) and whose @ is the TENSE.

• runtime/port.ts is the JS-side client; npm run portcorpus builds the corpus both engines are diffed over, and the oracle is a byte-identical canonicalState().

• A proof without the TypeScript engine. rofl serve answers why, whynot and excise over its JSON protocol (RoflSession.why/whynot/excise in runtime/port.ts), and rofl load answers them on the command line:

  rust/target/release/rofl load boot.rofl facts/js-dataflow.rofl rules/js-dataflow.rofl \
    --why 'flows_to(code, audit)' --whynot 'flows_to(audit, code)'

  A question replaces the state dump (--state puts it back, first); the answers come in flag order, each followed by an empty line; a refused question prints its message as the answer and exits 4. --why-all is why all, and --depth N --nodes N bound every --whynot (below 1 is 1); --budget, --ticks, --space, --strata apply as they do to the dump. The text is the reference's own, byte for byte: npm run whycheck puts its questions, refusals included, from every world npm test loads to both binaries and compares each with src/api.ts (docs/port-surface.md, "Explanation reaches the binaries").

The engine is checked with cargo test under rust/. It is not in .github/workflows/ci.yml — the CI jobs are node and bun only.

Storage adapters

adapters/ puts a FactStore behind an interface and ships a SQLite adapter over node:sqlite (a Node builtin, so the zero-dependency claim is unchanged). The conformance oracle is a byte-identical canonicalState() against the in-memory reference, and what it does NOT see is measured rather than assumed (CLAUDE.md, one mutant is liveness, a set is coverage): of five mutants it killed unsorted keys and dropped witnesses, and slept through reversed read order, sorted-instead-of-arrival order, and a dropped variable-holding fact — because matchPremise sorts before returning, negHolds reads for existence, and no program here holds a fact with a variable in it.

The JS model

rules/js-*.rofl is a model OF JAVASCRIPT — structure, modules, resolution, call graph, data flow, control flow, effects, environments, globals, hosts — fed by scanners/js_ast.ts and indexed as a matrix of (node kind × layer) cells, each modelled, waived with a reason, or not_modelled. The methodology, and the one measurement that decides whether it is science or bookkeeping, is docs/modelling-a-language.md; docs/scaling-a-corpus.md is the run over the whole of eslint (1 426 files, 29.9 s, 1 290 volumes cooled to 200 MB, the world never above 1 938 540 facts against a 2 000 000 ceiling) and the four defects that run found which reading did not.

Pipeline

Per evaluation (each tick, and on every load/assert since rules are just facts): decode rules from the reflected store → peel the rounds off those rules; a round that settles nothing while relations remain ⇒ reject, naming them → run monotone rules to fixpoint (seminaive) → run the negation rounds in order → @next conclusions staged (they settle no relation, so they run last) → tick boundary: freeze provenance, drop tick facts, install staged EDB.

Under evaluator: 'strata' that first step is instead: run monotone rules to fixpoint → read unstratified(_); nonempty ⇒ reject with the reach-trace → read stratum/2 → run negation strata in order. That path needs the program to derive a description of itself first, which is why the monotone phase is split in two waves there — the wave concluding the table has to finish before the verdict can be read — and why refusing a bad program used to cost the whole budget: boot's own stratum(Rel,N) :- …, N is M + 1 has no fixpoint on a negative cycle. Peeling invents no value and is bounded by construction: each round settles at least one relation or stops.

Under semantics(well_founded) that middle is replaced: no phase order, no rejection, and every not p judged against a frozen round instead of against the store being built — generous rounds and mean rounds converging on the true atoms from both sides, with the gap between the two limits written out as unknown/1.

A @next-headed rule with negation runs in the FINAL pass, after every stratum, not at its head relation's level: nothing in this tick can read a staged conclusion, so nothing orders it against the strata, while its own negative premises must be judged against relations that are complete — and staging is monotone, so one premature firing can never be taken back.

Determinism: facts, rules, and firings are processed in lexicographic order of their canonical serialization everywhere; same program + same inputs ⇒ bit-identical state, tick log, and provenance regardless of insertion order (tested over 100 shuffles).

Deviations from START.md (and why)

• Vocabulary additions. bridge_decl, uses_builtin are added to the §2 table as the appendix note instructs; premise_lit / conclusion_lit are added because the §2 reflection relations alone don't carry argument terms, and the evaluator must read rules only from the store (§4). Rule ids are content hashes (r + FNV-1a of the canonical clause), so re-loading a rule is idempotent.

• conclusion_tense is added because §2's concludes(Id,Rel) records a relation NAME and nothing else, so a conclusion written @next was indistinguishable from one derived here and now, and boot.rofl drew a same-tick dependency edge for it — refusing a sense→decide→act→world loop that is perfectly acyclic in time. not p means p is not derivable in the CURRENT TICK's store, so a @next head contributes no dependency edge and settles no relation: it is base for the tick that sees it, which is what such a fact IS. (Under the stratum table that took a floor rule, stratum(Rel, 0) :- concludes(R, Rel), conclusion_tense(R, next), because with the edge gone the relation would have had no stratum at all. The peel needs no floor: it never gives such a relation a level, so nothing orders it and it runs last.) The marker is otherwise unreachable — it sits inside the reified $lit of conclusion_lit, and $ is unwritable in surface syntax. concludes stays tense-blind, so every other reader of it (breach, undefined_premise) is unchanged.

• flows_to, the transitive closure of flow. The appendix reads leak[audit](A, B) :- flow(A, B), ..., and flow is one rule's signature — this rule reads that ledger and writes this one. So the audit was LOCAL where the property it guards is TRANSITIVE: content walks out of a ledger along a chain whose every step is separately licensed (red to case declared, case to report declared) and nothing asks about red to report. Measured: for said[red](a). claim[case](P,X) :- said[P](X). digest[report](X) :- claim[case](_,X). the store ends with claim[case](red, a) — the ledger name survives collection as an ordinary argument — and then digest[report](a), attribution projected away. The comparison was also lopsided, since sees has always been the reflexive-transitive closure of imports; flow was the half that was not closed. boot.rofl adds flows_to(A,B) :- flow(A,B). and flows_to(A,B) :- flows_to(A,X), flow(X,B)., and the leak rule reads flows_to. test/flow-closure.test.ts (gate removed 2026-09-11) carries the old single-hop rule beside the new one in one store, so "the closure did not swallow the direct crossing" is a measurement and not a claim.

• collects, the collection graph. The closure above made one class of crossing permanently unreportable and unfixable. A rule polymorphic in the ledger (claim[case](P, X) :- said[P](X)) reflects as a read of $var("P"), which has no authority fact and never will, so imports(To, $var("P")) is not a sentence this language can write — and the only remedy left was a paragraph in a README, which is not auditable, does not go stale loudly, and no check reads. collects(X) is host data declared like imports, and says: X deliberately gathers from ledgers it does not name. Three properties, each measured rather than asserted, in test/flow-closure.test.ts (gate removed 2026-09-11). Narrow: it licenses a crossing only where the SOURCE is not a registered perspective, so imports still gates every named ledger. The wide form (not collects(B) as a bare premise on leak) silences a walk from a named [secret] into a collecting [case], which makes it an off switch; the shipped form reports it. Keyed on the gatherer: collects_from(X, A) requires flow(A, X), so the declaration goes on the ledger that gathers. Keyed on the destination instead, a [case] feeding both [worlds] and [ledger_x] demands a collects fact on each reader — statements that are false about them — and another the day a third reader appears. Askable: collected[audit](X) is derived only when X actually collected something, so why collected[audit](case) names collects(case) as an axiom and not perspective($var("P")) as the reason the escape applied, while asserted_by names who declared it. A licence nobody can ask about is the invisible absence this replaced, and the same row distinguishes a declaration doing work from one nobody needed.

• stratum/unstratified appear in kernel source. §3.2 requires the kernel to read them while §5's grep test forbids non-§2 names. Resolved by documenting them as the kernel's read-interface (they cannot be reserved — a program may conclude into them, and rules/strata.rofl does). The grep whitelist equals this README's tables — and that sentence was a promise until 2026-09-10, when it was measured and was false by twenty names: the read interface had grown from two to eighteen and the destructors from zero to seven while the document said neither. It went stale in the SAFE direction, which is why nothing noticed — a whitelist wider than the document turns nothing red, it only stops the document describing the kernel. test/vocabulary-doc.test.ts (gate removed 2026-09-11) now re-derives both sides on every run and refuses a name that is in one and not the other, so the sentence is a measurement. The primary path reads neither stratum nor unstratified, so on that path the two names survive in kernel source only for the stock evaluator and the alternating fixpoint.

• Perspective registration. On first use of a perspective the kernel emits authority(P, $kernel). Without it, boot's perspective(P) :- authority(P,_) never sees main, so sees(P,P) is empty and every same-perspective rule becomes a leak — boot alone would fail its own audit. User authorities coexist; forged still works (it checks the specific asserting Who).

• Variable perspectives. Appendix B uses reading[S](…) although the grammar says persp := "[" name "]". The appendix wins: a variable perspective is parsed and matches facts in any perspective, binding the variable — an explicit wildcard read, recorded as reads_from(Id, $var("S")): the variable by NAME, so a rule that reads and writes the same variable carries one term at both ends and boot's leak audit sees an identity rather than a crossing ($any remains for a perspective that is neither a name nor a variable). Visibility enforcement is exact-perspective matching: a literal in [p] only ever sees facts stored in [p]; imports/sees are audit-level data (boot's leak), not kernel matching rules.

• Moded (demand) relations. Appendix B's close/2 ("mode note: both bound") and Appendix C's tape helpers are not range-restricted, so they cannot be materialized bottom-up. Rules whose head or builtin inputs are not grounded by their positive premises (in written premise order — premise order matters, Prolog-style) are evaluated top-down at call sites by unfolding; relations depending on such rules through positive premises unfold transitively (@next rules never unfold). Ground demand results are materialized with full derived_by provenance, so why/excise treat them uniformly.

• Timeless kernel facts. Facts in kernel-vocabulary relations (rule reflection, authority, mode, reserved, edb, provenance) persist across ticks. §3.3's "persistence is not a storage property" is applied to the domain world; if rule subgraphs were tick-scoped, every multi-tick program would need a rule-copying meta-rule and boot.rofl (which has no @next rules) could not survive tick 0. Provenance from completed ticks is frozen, which is what makes the diverging-TM partial trace queryable.

• Facts may be asserted into reserved relations. §2's enforcement is defined over rule conclusions ("may read, never conclude into") and sensors.rofl itself asserts authority(s1, sensor_net). The API therefore blocks rules, not facts; boot's breach audit catches hand-asserted reflection (tested).

• edb for reserved relations. Emitted at bootstrap even when empty, so boot's stratum rules can ground strata for audits over possibly-empty kernel relations (forged needs stratum(authority, 0) even before any authority fact exists). Rules whose head stratum is still unknown (empty dependency cones) run in a final pass — see LIMITS.md.

• Unstratifiable rejection is budget-mediated — on the stock path only. On an unstratifiable program boot's own stratum(Rel, N) :- …, N is M + 1 diverges; the load budget cuts the monotone fixpoint and the unstratified(_) check on the partial store rejects the load (with a why trace through dep/dep_neg/reach as the diagnostic) and rolls the store back. This is budgets-as-semantics (§5.6), not a special case. The primary path is not budget-mediated at all: the peel stalls before a rule fires, so the refusal costs zero derivation steps and is identical at any budget (test/reject-budget-invariance.test.ts (gate removed 2026-09-11) pins that at 2 000 and 32 000).

• Rounds replace the stratum table, and the table left boot.rofl with it. §3.2 of the spec puts stratification in boot.rofl as data and keeps it out of the kernel; peelRounds is a stratification computation in src/, so that sentence is not kept as written. What is kept is the reason for it — no hardcoded boot rule, one policy seam, the schedule readable — and what is bought is measured: 44.8% fewer derivation steps across the 34-program corpus (107 235 → 59 184), a refusal that reaches every relation that can never settle rather than only those on the cycle, termination by construction where N is M + 1 had none, and the closing of a hole where any rule could write stratum/2 and steer the phase order with no audit signal. What is lost is named too: the refusal no longer carries the reach trace that showed why, and the check is computed rather than read from data. The ten rules that derived dep, dep_neg, reach, unstratified and stratum now live in rules/strata.rofl as an ordinary pack — the stock evaluator still reads what they conclude, and any program may load them.

• Budget accounting. A derivation step is a distinct rule firing (deduplicated by rule + premise tuple) or one demand-unfolding node. hole facts are frozen (they survive re-evaluation — the record that a budget was exhausted is history, not derived state).

• Arithmetic that cannot be evaluated. N is "hello" + 1 used to derive nothing and say nothing, so a type error inside an expression was indistinguishable from a premise that legitimately failed. is now emits hole($rule(Id), arith_type_error) — or arith_zero_divisor for X / 0 and X mod 0 — and the premise still fails, so no derivation changes: only the store's ability to state the inability does. Three things this does NOT do, each deliberate. It does not fire on an unbound variable: a builtin whose variables are not yet bound is an ordinary state, not an error, and reporting it would put a hole under every rule. It does not fire on a comparison: X >= 0 on a string still ANSWERS — the row is not one of the numbers — and examples/slop uses exactly that as the numeric type test the language does not otherwise have, whereas is must PRODUCE a value and so has no "no" available to it. And it does not mark the evaluation partial, unlike the budget hole: the fixpoint is complete, one expression in it was not. One hole per rule, not per offending substitution; the rule id is a key into the reflected program, so premise_lit(Id, K, Lit) still recovers the expression.

• why embeds finite-failure demos. For a negated premise, why inlines the whynot demonstration of the negated fact (Appendix B requires why outlier[trust](s3) to be a finite-failure demo of corroboration), in its single-step form — one level, the failing premises named. Cross-tick witnesses whose premise facts no longer exist render as [past tick] leaves.

• whynot recurses; three guards make it terminate. Asked directly, whynot explains each failing premise in turn, so the answer to "which stage dropped this row" is the chain down to the builtin that failed on real values. A literal already being explained above is marked [cycle] and not re-entered; one already explained in full earlier in the answer is K [above] (why too: a fact or an aggregate's cell is written once, so an answer is the size of its derivation graph); depth (default 6) shapes the tree; nodes (default 64) bounds it outright — the node cap alone is what guarantees termination, since it caps how many literals the whole tree may explain. Both announce themselves in the output when they fire.

• File layout, and the size target is exceeded by 3.5x. api.ts carries ?/why/whynot/excise/load per §4's repl.ts / api.ts line; the REPL is a thin shell. src/ was 1 909 lines over seven files when the 1 500–2 000 target was met; measured 2026-09-10 it is 6 778 over twelve — engine.ts 1 924, api.ts 1 235, reflect.ts 1 115, store.ts 884, unify.ts 310, rounds.ts 307, semiring.ts 262, parser.ts 224, dense.ts 200, tokens.ts 141, repl.ts 93, kernel-dense.ts 83. The number is written down rather than the target quietly restated: the growth bought a second evaluator (rounds.ts), the well-founded semantics, the dense form, semirings, and a store that can cool volumes to disk, and whether that trade was worth 4 800 lines is a judgement a reader should be able to make against the original figure.

  AND THIS PARAGRAPH IS A DELIVERABLE, NOT A FOOTNOTE. START.md:107 does not merely set a target, it sets a STOP: "If it grows past ~2,500, stop: something that belongs in boot.rofl as rules has leaked into the host. That signal is itself a deliverable — report it rather than pushing through." src/ is 2.7x past that line and the duty (s_report_loc_overrun in facts/spec.rofl) is one of the 28 npm run speccheck reports as covered by nothing mechanical — so the stop was passed without the report the spec asks for, which is what this is. The signal is delivered; whether it means what START.md predicts is the owner's to judge, and the evidence cuts both ways. FOR: engine.ts alone is 1 924 lines, as large as the whole kernel once was. AGAINST: the prescribed remedy is already running in the other direction — policy.rofl and safety.rofl are code that LEFT src/ and became rules, and rules/strata.rofl is ten more, so the leak is being paid back rather than accumulating unexamined.

• tm.rofl uses one @next rule plus moded helpers (step, move) and explicit carry rules for delta and the halted cfg — Appendix C is a sketch; carrying delta forward is the "persistence is not a storage property" discipline applied honestly.

• Node ≥ 22.6 instead of ≥ 20. The spec says "Bun or Node ≥ 20"; the sources are erasable-syntax TypeScript executed via Node's built-in type stripping, which shipped in 22.6. Nothing in the code needs Node 22 — compiling with tsc would restore Node 20 support at the cost of a build step; zero-toolchain execution was judged closer to the spec's intent.

• Optimization passes exist, and START.md section 8 said not to build them. The engine is a SEMINAIVE fixpoint (src/aggeval.ts), the derived layer is REUSED per relation under an exact fingerprint with the switch defaulting to on, and premises against a demand-backed relation are solved TOP-DOWN with the recursion capped at 512. Each was a deliberate decision and each already carries its own limit in LIMITS.md — l_reuse_fingerprint, l_reuse_a_no_read_reused, l_reuse_b_stratum_gate, l_reuse_c_tick_boundary, l_reuse_switchable, l_demand_premise_order, l_demand_depth_512, l_demand_no_enumeration. So the prohibition was not quietly broken; it was replaced, in detail, by eight sentences in the document that came after it, and l_no_aggregation was the one line that never caught up: it read No aggregation, no optimization passes, no syntax sugar, no GPU anything in the same file as those eight. It is amended in place (2026-10-02): GPU alone holds, as its own limit l_no_gpu; aggregation is the next entry (docs/aggregates.md), and the sentence form and the aggregate phrases are the sugar (docs/sentence-form.md).

• Aggregation exists, and START.md section 8 said not to build it. Decided 2026-09-28 by the owner: not one stratified count but every aggregate class, as ONE CELL ENGINE with two syntaxes. A body aggregate (N is count(R : body), sum, min, max, or, and, the holistic median, quantile and rank, and the threshold at_least) reads a relation closed below it, as a negation does; a relation declaration (lattice dist(A, C, min D), with a declared widening where the height is infinite), a semiring tag and subsumption under a declared order are cells keyed by the head. The algebra of the kind decides what may recurse. A cell an overflow, a type error or a budget cut touched is a hole and never a value, and its witness is its contributions, so why prints every row a value stood on. Rust first, the TypeScript engine best-effort at small scale. The account, the matrix of what is proved and what is open, and the design reasons are docs/aggregates.md, facts/agg.rofl and rules/agg.rofl. The amendment is d_aggregates_in_the_kernel in facts/spec.rofl, which retires l_no_aggregation.

• Rust is the engine, and START.md asked for TypeScript with zero runtime dependencies under Bun or Node. Decided 2026-10-02 by the owner (f_rofl_moves_to_rust_first, f_rust_is_the_engine_ts_is_the_reference): the rofl binary under rust/ is the engine every measurement is taken on, and it links crates (serde_json, memmap2) at build time. The two duties are narrowed, not dropped, and each now says one thing per engine. s_zero_deps: the TypeScript engine under src/ still has no runtime dependency (package.json has no dependencies); the Rust engine is one static binary that needs nothing installed beside it, and its crates are build-time. s_two_runtimes: the TypeScript engine runs under Node, which CI holds (goldens (node)); Bun is no longer checked since the owner removed its job on 2026-10-11; the Rust engine is native and runs under neither. Both engines are held to one golden by npm test.

Acceptance status

All Phase 1–4 criteria were covered by test/phase{1..4}.test.ts, 31 tests (suite removed 2026-09-11): transitive closure & structured terms; naive ≡ seminaive over 120 seeds; why to EDB axioms; perspective isolation; strata read from stratum/2 facts; unstratifiable rejection (with the reach-trace on the stock path, with the stuck set on the primary one); the kernel grep test; runtime rule addition; the malformed-validator sibling condemnation; store round-trip through a fresh process with no re-parse; counter 1..5 with silent fixpoint; 100-shuffle bit-identical replay; busy-beaver halt (13 steps, 6 ones, cross-checked against an independent simulation) and the diverging variant yielding hole with a queryable partial trace; boot's six audits empty plus whynot flows_to(red, blue); the full sensors scenario including excise blast radius and multiple-support soundness.

Two of those read differently now and the difference is registered above, not hidden here. Strata read from stratum/2 facts is checked on the stock evaluator, with rules/strata.rofl supplying the table boot.rofl used to derive, and the same program is checked ordering itself with no table at all on the primary path. Boot's audits empty plus a finite whynot lost the unstratified(X) -> empty line — the question is now answered by the file loading at all, since a program whose peel stalls never reaches a query — and the finite-failure demonstration is asked of flows_to, the transitive closure that remains.

The floor-sealing declaration

(Appended at the end of the file on purpose: facts/spec.rofl anchors duties here by line number, and a block inserted above unfounds every citation below it — measured, 17 of them. boot.rofl carries the same note for the same reason.)

A third is on the same footing, and it decides what the kernel KEEPS rather than how it runs: the program writes sealed(Body) to declare that one of the three bodies of metadata the kernel maintains about it is no longer published. sealed(rules) withholds has_conclusion, reads_from, writes_to and uses_builtin; sealed(assertions) withholds in_perspective and asserted_by; sealed(provenance) withholds derived_by. Nothing else may be sealed, and the boundary is measured rather than chosen: rules/floor-census.rofl derives it from an ablation over every reflection relation plus a census of who reads each one, and test/sealed.test.ts (gate removed 2026-09-11) asserts that the derived set equals the kernel's table. The relations the evaluator reads to RUN a program (rule, conclusion_lit, premise_lit) and the ones the kernel's own two programs read about it (has_premise, concludes, premise_pos, premise_neg, conclusion_tense) are not in any body and no declaration reaches them.

The declaration is READ, never inferred, and that is the point of it: dropping rows because nothing currently reads them makes a later audit return empty and look correct. So the kernel writes hole($sealed(Body), reflection_sealed) when the declaration arrives, and a ? query of a withheld relation returns partial: true with a hole rather than an empty answer — asking a sealed floor REFUSES. A body name the kernel does not know is data, not an error, the same contract semantics/1 has. examples/ring1/ring1.rofl exercises it: the grammar seals its own rule reflection, which is 456 of 2450 facts in the image the parser forks once per clause, and boot.rofl's malformed, leak and unmoded audits over those 126 rules lose their subject and say so.

Under sealed(provenance) the Rust engine keeps no witness either, where nothing withdraws, and a budget step is then a new fact rather than a firing: the same program reaches a budget at a different place with the seal and without it, which is accepted because the seal is the program's own word.

In a provenanced world the Rust engine keeps the witness of every firing (what why renders) and writes the derived_by rows of the firings no rule reads only when something asks: the canonical state, a query for derived_by, a tick boundary. The state it answers is the state of an engine that writes every row; a world that evaluates and is not read for them holds 44% fewer facts. A rule that reads derived_by of a named relation keeps that relation's rows as they fire. sealed(provenance) remains the declaration that no row and no witness is wanted (f_derived_by_is_written_when_asked).