update docs

8 files changed, 854 insertions, 97 deletions

diff --git a/docs/denial.org b/docs/denial.org
new file mode 100644
index 0000000..d79a394
--- /dev/null
+++ b/docs/denial.org
@@ -0,0 +1,194 @@
+#+TITLE: Denials
+
+* Purpose
+A denial is a relation that must be empty. Each tuple it holds is one
+breach of a rule, so a state where every denial is empty is a state
+where every rule holds. RNT knows no rule language. It knows only that
+denials must be empty, and it refuses to move a branch head to a state
+where one is not. Constraints across relations, the assertions SQL
+names but rarely implements, become relations like any other.
+
+The idea is the denial form of integrity constraints, from Sadri and
+Kowalski ("A theorem-proving approach to database integrity", 1988),
+where a rule is written as a query for its own counterexamples.
+
+* Where denials live
+Each multigroup holds its denials beside its schemas.
+
+#+begin_example
+\system\branch\master\multigroup\library\schema\default\relation\book
+\system\branch\master\multigroup\library\denial\no-books
+#+end_example
+
+A multigroup stores a denial the way a schema stores a relation. An
+[[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]] that wraps a [[file:../lib/kernel/Program.ml][program]] becomes the program's
+evaluator name and source, and any other relation becomes its tuples. A
+program is the usual case, because a rule has to be computed against
+the state it judges. When a branch reads the denial back, the
+[[file:evaluators.org][evaluator]] registered under that name parses the source, and reading
+the denial invokes the program =within= the branch state it was read
+through. The same denial therefore reads one state through the head
+and another through =previous=.
+
+* Judging a state
+[[file:../lib/protocols/Admission.mli][Admission]] is the protocol that judges a state.
+
+#+begin_src ocaml
+type violations = (string * Concepts.Tuple.t) list
+
+class type implementation = object
+  method check : (violations, Concepts.Condition.condition) result
+end
+#+end_src
+
+=check= names every denial that holds a tuple, with one such tuple as
+its witness. An empty list means the state is admitted. An error means
+the state could not be judged, and an unjudged state is not admitted
+either.
+
+A multigroup judges each of its denials in two steps.
+
+1. It asks the denial for its [[file:modes.org][modes]]. If the denial is not
+   exhaustible with nothing bound, the multigroup fails with
+   =unjudgeable-denial= and reads nothing.
+2. Otherwise it reads the denial up to its first tuple. No tuple means
+   the denial holds. A first tuple is the witness, and the multigroup
+   reads no further.
+
+For a denial that wraps a program, the multigroup invokes the program
+once, within the branch state it judges, and asks both questions of the
+relation the program returns.
+
+A branch state asks each of its multigroups and names every violation
+by its path, =\multigroup\[m]\denial\[d]=. Judging belongs to the
+multigroup, the universe its relations describe. The branch only
+versions states and collects the answers. A rule may still read
+relations of any multigroup, because the branch asks all of them.
+
+One witness is enough to refuse a state, and asking for more would cost
+a read of the whole denial, which never ends for a =Countable= one.
+
+* Trust
+The guard rests on what a denial declares. A FOL denial over stored
+relations derives its modes from theirs, so its claim to be finite
+holds. A denial written in another language declares whatever its
+evaluator returns. A program that declares =Finite= and then never ends
+still hangs the check, and RNT cannot tell. The same holds when FOL
+reads a relation from another evaluator, since FOL takes that
+relation's modes as given. A cycle of programs across languages also
+recurses without end.
+
+* Moving a head
+=BranchManager= asks the proposed state for its admission before it
+moves a head. If the state is not admitted, it refuses the move with a
+=refused= condition that names each denial and its witness, and the
+head stays where it was. It asks before taking the head, since a denial
+may run a program that reads storage.
+
+#+begin_src plantuml :file ../images/denial-admission.svg
+@startuml
+participant "Scope.publish" as Publish
+participant BranchManager
+participant "proposed\nbranch state" as Branch
+participant Multigroup
+participant Denial
+
+Publish -> BranchManager : move the head
+BranchManager -> Branch : check
+loop each multigroup
+  Branch -> Multigroup : check
+  loop each denial
+    Multigroup -> Denial : modes
+    alt not exhaustible with nothing bound
+      Multigroup --> BranchManager : unjudgeable-denial
+    else exhaustible
+      Multigroup -> Denial : enumerate, read the first tuple
+      Denial --> Multigroup : a witness, or nothing
+    end
+  end
+  Multigroup --> Branch : violations
+end
+Branch --> BranchManager : violations, named by path
+alt none
+  BranchManager -> BranchManager : move the head
+else some
+  BranchManager --> Publish : refused, one witness per denial
+end
+@enduml
+#+end_src
+
+#+RESULTS:
+[[file:../images/denial-admission.svg]]
+
+The check judges the state itself, not a change to it. Every commit
+lands only if the whole state it makes is admitted, whichever subsystem
+made it, so a rule written in one language guards data written from
+all of them.
+
+* Publishing denials
+[[file:../lib/kernel/Scope.mli][Scope.publish]] binds denials with its relations, in the same state.
+
+#+begin_src ocaml
+Scope.publish root ~branch:"master" ~home:library
+  ~denials:["no-books", Some no_books; "audit:shelved-twice", Some twice]
+  ["book", Some books]
+#+end_src
+
+A name =d= binds in the home multigroup, and =m:d= binds in multigroup
+=m=. A commit can install a rule and the data it guards together, and
+the rule is judged with the data. If the state it makes already breaks
+the rule, the commit is refused. A denial that cannot be judged cannot
+be installed either, since the state that holds it cannot be admitted.
+
+* Judging a state without landing it
+A subsystem that wants to know whether a change would be admitted builds
+the state with [[file:../lib/kernel/Path.mli][Path.assoc_all]] and asks it.
+
+#+begin_src ocaml
+let* next = Path.assoc_all head [Scope.relations library, "book", Some books] in
+let* admission = Protocols.Admission.require next in
+Protocols.Admission.check admission
+#+end_src
+
+Nothing lands. A host can use this to preview a form, a move or an
+import, and show which rule would refuse it.
+
+* Open problems
+** Incremental checking
+Every commit judges every denial of every multigroup over the whole
+state. Decker ("Translating Advanced Integrity Checking Technology to
+SQL", 2002) shows how to check only what a change can break. Take the
+denial of a book shelved twice.
+
+#+begin_example
+{(title, s1, s2) | shelved(title, s1) ∧ shelved(title, s2) ∧ s1 ≠ s2}
+#+end_example
+
+A commit that inserts =shelved("Codd", "A")= can only add violations
+where =title = "Codd"= and one shelf is ="A"=. Asking the denial for
+those tuples, with the other shelf free, is the whole incremental check.
+It is the insertion-only case of [[file:maintenance.org][incremental maintenance]], which covers
+the delta rules it reuses.
+
+RNT cannot ask that today. The question binds some attributes of the
+denial and leaves others free, and no operation produces the tuples of
+a relation under a partial binding. This is the gap that [[file:modes.org::*Reachable bindings][reachable
+bindings]] describes. Closing it takes three pieces.
+
+1. A binding-aware read, which every relation implements and FOL passes
+   through its plans.
+2. Indexes, so that a substantial relation answers such a read by
+   lookup rather than by filtering a scan.
+3. Read sets, so that RNT knows which relations a denial reads and how
+   their attributes line up with the denial's, and can turn an inserted
+   tuple into bindings on each denial it touches.
+
+** Denials do not protect themselves
+A commit that removes a denial and breaks its rule is judged on the
+state it makes, where the denial is gone, so it lands. Guarding
+=\denial= needs the access checks the [[file:../README.org][README]] plans to keep apart
+from lookup.
+
+** Multigroups from before denials
+A multigroup stored before denials existed has no =denials= field and
+does not load.
diff --git a/docs/evaluators.org b/docs/evaluators.org
index b7ce3b8..f1b4be5 100644
--- a/docs/evaluators.org
+++ b/docs/evaluators.org
@@ -1,108 +1,215 @@
-#+TITLE: Evaluators
+#+TITLE: Programs and evaluators
+
+* Why the kernel has no language
+RNT supplies objects, storage and the execution lifecycle, and leaves
+languages to its clients. SQL puts retrieval, data manipulation and data
+definition in one language, and the boundaries between them are hard to
+draw. In RNT, a language =A= may serve retrieval, =B= may serve
+manipulation and definition, and =C= may serve manipulation beside =B=.
+Nothing arbitrates between =B= and =C=, and a client picks either. The
+[[file:../lib/evaluators/FOL.ml][FOL]] evaluator is one such language, shipped with RNT for retrieval.
+
+That leaves the kernel two jobs. It has to run a program without
+knowing its language, and it has to let programs in different languages
+read each other's results. Programs and evaluators are how it does both.
+
+* Programs
+The kernel holds, stores and runs programs whose structure it cannot
+know. A [[file:../lib/kernel/Program.ml][program]] is therefore an image, in the manner of a Windows
+[[https://en.wikipedia.org/wiki/Portable_Executable][Portable Executable]], whose header tells the loader which subsystem
+runs it.
 
-* Position
-RNT should supply objects, storage, and execution
-lifecycle, but not directly a sublanguage. That duty is then on the
-clients to implement one and register it, using the kernel's
-capabilities.
+#+begin_src ocaml
+type kind = ..
+type image = {evaluator: string; kind: kind; source: string}
+#+end_src
 
-In this context, an evaluator is an RNT object, registered and
-selected through the object interface, with a special "evaluator"
-protocol. Unlike SQL where the boundaries between execution contexts
-of the language is confusing and sometmes non-trivial, a sublanguage
-=A= may serve retrieval, =B= may serve DML and DDL while =C= may serve
-DML alongside =B=. Nothing arbitrates between B and C; making the
-client free to opt for one.
+=evaluator= names the evaluator that runs the program, as
+=scope:language=. =kind= is the program as that evaluator understands
+it. =source= is its text, for display and for storage.
 
-The FOL evaluator is therefore, one of such evaluators that is shipped
-alongside RNT for specifically Data Retrieval.
+=kind= is an [[https://ocaml.org/manual/extensiblevariants.html][extensible variant]], extended the way [[file:object-system.org][protocols]] are. Each
+evaluator adds its own constructor, as FOL adds =Fol of Path.t term=.
+The tree keeps its OCaml type, and only the evaluator that defined the
+constructor can match on it, so the kernel passes programs around with
+no encoding in between. The evaluator name is the one string a program
+carries, because the kernel looks evaluators up by name and storage can
+keep a name but not a constructor.
 
-* Capability tags
-An evaluator object declares a set of opaque labels — =drl=, =dml=,
-=ddl=, =vcs=, or anything a client invents. The registry stores and
-indexes them so a client can ask which evaluators declare =dml= and
-get back B and C.
-
-* Protocols
-An evaluator is an object like any other, that can be used to execute
-a program, exactly as an interpreter takes an expression and an
-environment. The plan tree should already bear every value and handle
-the program needs, so there is nothing left to bind. Each invocation
-carries independent state based atop of the handles it was given
-(being therefore hash dependent and isolated).
+Every program speaks [[file:../lib/protocols/Executable.mli][Executable]], and a program built with a root can run.
 
 #+begin_src ocaml
-module Make (P : PROGRAM) : sig
-  class type implementation = object
-    method invoke : P.t -> (Handle.t, condition) result
-  end
-end
+method invoke : Handle.t list -> within:Handle.t -> (Handle.t, condition) result
 #+end_src
 
-The protocol is parameterized by the evaluator's own plan type, so a
-plan is never encoded into values only to be decoded again. Each
-application of the functor yields its own protocol constructor, which
-is what keeps one evaluator from answering another's programs: a
-client obtains the interface through the module of the evaluator it
-intends to speak to. The FOL evaluator, which lives under
-=lib/evaluators= alongside the evaluators shipped with RNT, currently
-understands a single node:
+Invoking a program looks up =\[scope]\evaluator\[language]= under its
+root, and hands that evaluator the kind, the inputs and =within=. A bare
+=language= names the =system= scope. The root is a capability, so a
+program reaches only the evaluators of the root it was given. A program
+built without a root can be stored but not run, and invoking it fails
+with =unloaded-program=. A name with nothing registered under it fails with
+=no-evaluator=.
+
+* Evaluators
+An evaluator is an object with the [[file:../lib/protocols/Evaluator.mli][Evaluator]] protocol.
 
 #+begin_src ocaml
-type plan = Base of Handle.t
+method parse : string -> (kind, condition) result
+method eval : kind -> Handle.t list -> within:Handle.t -> (Handle.t, condition) result
 #+end_src
 
-=Base= carries the handle of a relation, which is enumerated to
-exhaustion. The evaluator only invokes protocols on the handles it
-receives, which keeps it free of storage and of name resolution.
-
-The returned handle carries a result protocol with =Protocols.Cursor=,
-giving it incremental consumption. Since executing a plan node yields
-a cursor, operators stack as cursors over cursors, in the manner of a
-volcano iterator, and no intermediate result is materialized. A
-successor state and a command completion are further result protocols,
-added for DML and DDL later. It's important to notice that the kernel
-enumerates result protocols; it thererfore does not enumerate
-sublanguages. That is not to say however that we cannot have a builtin
-catalog relation installed and configured by the client that
-enumerates them (that's a concern for the future).
-
-* Handles
-There is no evaluation context. Since we are a capability based
-system, holding a handle is what authorizes its use, so the caller
-obtains every handle a program needs beforehand (through the
-directories it was granted) and passes them in. Evaluators reach
-kernel resources *only* through those handles. A program that refers
-to things by name carries the directory they are resolved in, as the
-lambda evaluator does:
-
-#+begin_src ocaml
-type program = Program of term * Directory.t Handle.interface
+=eval= runs a kind, and fails for a kind that is not its own. =parse=
+turns source back into a kind, which is how the kernel reloads a stored
+program. A program built in code skips parsing. =FOL.program term=
+builds one from a tree and prints the tree as its source, so a test can
+build a plan without a syntax. FOL has no text syntax yet, and its
+source is the [[https://en.wikipedia.org/wiki/Bencode][bencoded]] term.
+
+#+begin_src plantuml :file ../images/evaluators-classes.svg
+@startuml
+hide empty members
+skinparam classAttributeIconSize 0
+
+class Program <<image>> {
+  evaluator : string
+  kind : Program.kind
+  source : string
+}
+interface Executable {
+  invoke(inputs, within) : relation
+}
+interface Evaluator {
+  parse(source) : kind
+  eval(kind, inputs, within) : relation
+}
+class "FOL evaluator" as FOL
+class EphemeralRelation
+interface Relation {
+  contains(tuple) : bool
+  modes() : Mode.t
+}
+interface Enumerable {
+  enumerate() : cursor
+}
+interface Schematics {
+  describe() : heading
+}
+
+Program ..|> Executable : runs when given a root
+FOL ..|> Evaluator
+Program --> Evaluator : names it as\nscope:language
+EphemeralRelation ..|> Relation
+EphemeralRelation ..|> Enumerable
+EphemeralRelation ..|> Schematics
+EphemeralRelation o--> "0..1" Program : wraps
+Evaluator ..> EphemeralRelation : eval returns
+@enduml
 #+end_src
 
-Since every object is content addressed and prolly trees do not
-depend on insertion order, equal state yields an equal hash, so the
-relation behind a handle does not change under a running evaluation.
-A successful evaluation and cursor exhaustion never commit. Commit
-should be an explicit host operation.
+#+RESULTS:
+[[file:../images/evaluators-classes.svg]]
+
+* Within
+In RNT, holding a handle is what authorizes its use, so an evaluator
+gets no context beyond one directory. A program names relations by
+path, and its evaluator resolves those paths in the directory the
+program is invoked =within=. It can reach nothing else.
+
+Resolving paths at each invocation is what lets one program run against
+any state. Read through
+=\system\branch\master\multigroup\m\schema\s\relation\r=, a stored
+program runs within that branch state. Read through
+=\system\branch\master\previous\...=, it runs within the previous state
+and reads what was there then. It can never read outside its branch.
+
+Evaluation never commits, and neither does exhausting a cursor.
+Committing is an explicit host operation. Cancellation, budgets and
+resource accounting are not implemented.
+
+* Results
+Programs in different languages can read each other's results only if
+those results share one interface. The result of every program is an
+[[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]]. It describes its heading, declares its [[file:modes.org][modes]] and
+answers membership. Enumerating it gives a cursor, so operators stack
+as cursors over cursors, as in Graefe's Volcano iterator model
+("Volcano, an Extensible and Parallel Query Evaluation System", 1994),
+and nothing in between is materialized.
+
+An ephemeral relation can wrap a program, through
+=EphemeralRelation.of_program=. Reading it invokes the program within
+the state it was given. Asking its modes, or whether it holds a tuple,
+invokes the program and asks the relation the program returns. For FOL
+this is cheap, because FOL builds its result without reading a tuple.
+
+Programs that change state have no result protocol yet.
+
+* Storage
+A multigroup stores an ephemeral relation that wraps a program as the
+program's evaluator name and source, beside its heading. It stores any
+other relation as its tuples. When a branch reads the relation back,
+the evaluator registered under that name parses the source into a kind,
+and the relation wraps the program that comes out. The parse happens at
+lookup, so a missing evaluator or a malformed source fails at
+=Path.lookup= rather than at the first read.
+
+#+begin_src plantuml :file ../images/evaluators-reading.svg
+@startuml
+actor Client
+participant "Path.lookup" as Path
+participant Multigroup
+participant EphemeralRelation as E
+participant Program
+participant "evaluator under\nthe program's name" as Ev
+
+Client -> Path : lookup a relation in a branch state
+Path -> Multigroup : find it
+Multigroup -> E : load (evaluator name, source, heading)
+E -> Program : Program.load root
+Program -> Ev : parse source
+Ev --> Program : kind
+E --> Client : relation wrapping the program
+Client -> E : enumerate
+E -> Program : invoke ~within:branch state
+Program -> Ev : eval kind ~within
+Ev --> Program : result relation
+Program --> E : result relation
+E --> Client : cursor over the result
+@enduml
+#+end_src
 
-Cancellation, budgets, and resource accounting are not implemented.
+#+RESULTS:
+[[file:../images/evaluators-reading.svg]]
 
 * Composition
-Evaluators compose through invocation and result protocols alone. A
-DML program written in B may invoke a retrieval program written in A,
-consume its cursor, and build a successor state from the tuples. A
-retrieval program in A may invoke a procedural relation implemented by
-C. Neither evaluator however knows the other's representation. The
-caller must establish that the callee's contract meets its needs,
-obviously.
+Evaluators compose through programs and results, and neither knows the
+other's kind. When FOL resolves a path to a relation that wraps a
+program, it checks the program's kind.
+
+- A FOL program is inlined into the plan. FOL then sees through it, and
+  refuses a program that reaches itself with =cyclic-program=.
+- A program of any other kind is invoked within the same state, and its
+  result enters the plan like any other relation.
+
+A program in another language reads a FOL program the same way, by
+resolving its path and reading the relation. The [[file:../test/unit/kernel/Branch.ml][branch tests]] do both,
+with a toy language whose programs shout the titles of a FOL relation.
+
+FOL detects cycles only among its own programs. A cycle across
+languages, where a FOL program reads a toy program that reads it back,
+recurses without end. Nothing checks one evaluator's assumptions about
+another's results either, so the caller has to establish that the
+callee's results meet its needs.
 
 * Registration
-Registration is made by the client, and in the case of builtins, 
-automatically at initialization, just as =Relation= and =Schematics=, 
-for example. A foreign registration path is a later concern and is not
-designed for here.
-
-Only =Protocols.Cursor= exists as a result protocol (at least for now), 
-so a successor state, completion, plan persistence, and cross-evaluator 
-optimizations are absent by design.
+The system's evaluators are registered at initialization, under
+=\system\evaluator=. A subsystem mounts its own root with
+[[file:../lib/kernel/Initialization.mli][Initialization.mount]], which holds =\[name]\evaluator=, and registers
+its evaluators there. Its programs then name them as =name:language=. A
+foreign registration path is a later concern.
+
+* Capability tags
+A client should be able to ask which evaluators serve manipulation, and
+get =B= and =C= back. The intent is that each evaluator declares a set
+of opaque labels, such as =drl=, =dml=, =ddl=, =vcs= or any a client
+invents, and that the registry indexes them. None of this is
+implemented.
diff --git a/docs/lifecycle.org b/docs/lifecycle.org
index 80b387d..c23e9a1 100644
--- a/docs/lifecycle.org
+++ b/docs/lifecycle.org
@@ -7,6 +7,9 @@ operates purely on the object tree and never touches storage. "Collection"
 here means dropping the in-memory registry entry, not deleting anything on
 disk.
 
+The manager is a design and is not built. [[*What exists today][What exists today]] describes the
+mechanism the code has now.
+
 * Three independent facts per object
 
 Each registry entry keeps three separate pieces of state, deliberately not
@@ -42,12 +45,11 @@ the =reference_count= of each edge target; unregistration drops it. The edge
 set is a per-kind property and lives next to the registry, because the object
 knows its own shape.
 
-Only ephemeral relations carry edges today. An ephemeral relation is a stored
-plan that reads other relations, so those inputs must not be collected while
-the plan can still be replayed. The edges are branch-local symlink paths, not
-version-pinned paths: as the branch head advances the inputs move with it, and
-=Namespace.resolve= turns the symlink into whatever object is current on this
-branch hash. This is what lets an ephemeral relation behave like a view.
+Only ephemeral relations carry edges today. An ephemeral relation wraps a
+[[file:evaluators.org][program]] that reads other relations, so those inputs must not be collected
+while the program can still run. Its inputs are paths resolved in the branch
+state it is read through, not pinned versions. Read through the head, it reads
+the inputs as they are. Read through =previous=, it reads them as they were.
 
 * Teardown order
 
@@ -80,3 +82,39 @@ collectable like anything else.
 Separate from collection. An exclusive object with an open handle, such as a
 branch head being read, cannot be modified until the handle closes.
 =contention= reports this so writers can be gated.
+
+* What exists today
+Each object carries its own lifecycle, one of the classes in
+[[file:../lib/kernel/Lifecycle.mli][Lifecycle]], and every handle to it calls into that lifecycle when it is
+copied or released.
+
+- =null= is for objects with nothing to release, either because storage
+  can rebuild them or because they hold no resources. Substantial
+  relations, multigroups, branch states, programs and evaluators are
+  =null=.
+- =counted= is for objects that hold resources. It counts handles and runs
+  the object's destructor when the last one is released. Namespaces,
+  sessions, generated cursors and ephemeral relations are counted, and an
+  ephemeral relation releases its inputs when it is destroyed.
+- =exclusive= admits one handle at a time. Nothing uses it since sessions
+  became counted.
+- =retaining= stands in for a handle while it holds a reference to an
+  owner, so that what the handle reads outlives the object that produced
+  it. A cursor over a program's result keeps the result alive this way.
+
+A namespace owns the handles registered in it. =Namespace.update= moves the
+handle in, which invalidates the caller's handle, and releases the handle
+it replaces. A destroyed namespace releases every entry. A caller that
+still needs a handle after registering it registers a =Handle.copy=.
+
+Walking a path opens a handle at every step, and the walk has to release
+all of them except the last. [[file:../lib/kernel/Path.ml][Path]] does this with an autorelease pool,
+named after the [[https://developer.apple.com/library/archive/documentation/Cocoa/Conceptual/MemoryMgmt/Articles/mmAutoreleasePools.html][Cocoa]] mechanism. Each handle found along the way goes
+into the pool, and the pool releases them when the walk ends. =Handle.keep=
+takes the handle the walk returns back out of the pool, and the caller
+releases it. The pool is an OCaml [[https://ocaml.org/manual/effects.html][effect handler]], so the code inside the
+walk adds handles to it without being passed the pool.
+
+A handle to a managed object that the garbage collector reaches while it
+is still valid has leaked. Its finalizer logs a warning with the backtrace
+of where the handle was made, and releases it.
diff --git a/docs/maintenance.org b/docs/maintenance.org
new file mode 100644
index 0000000..42b5075
--- /dev/null
+++ b/docs/maintenance.org
@@ -0,0 +1,104 @@
+#+TITLE: Incremental maintenance
+
+* Purpose
+An [[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]] is computed when it is read. That is right for a
+relation read rarely, and wrong for one read on every commit or over a
+large input, where each read repeats the whole computation. A
+materialized ephemeral relation would store its tuples, so that reading
+it costs what reading a substantial relation costs. Every commit that
+changes its inputs then has to change it as well.
+
+Recomputing it from scratch on each commit costs as much as the
+relation itself. Incremental maintenance computes only the change, from
+the change to the inputs. The literature calls this [[https://en.wikipedia.org/wiki/Materialized_view][incremental view
+maintenance]], and Gupta and Mumick survey it in "Maintenance of
+Materialized Views: Problems, Techniques, and Applications" (1995).
+RNT has none of it yet. This document is the design it should follow.
+
+* Deltas
+A commit changes each relation it touches by a set of inserted tuples,
+Δ⁺, and a set of deleted tuples, Δ⁻. For a relation =D= derived from
+inputs =R₁ … Rₙ=, maintenance computes =ΔD⁺= and =ΔD⁻= from the =ΔRᵢ= and
+the states before and after the commit, operator by operator.
+
+- =Base r= changes exactly as =r= does.
+- =Project (p, A)= gains the projection of each tuple in =Δp⁺= that it
+  did not hold before. It loses the projection of a tuple in =Δp⁻= only
+  if no other tuple of =p= projects to the same tuple, which is the
+  problem [[*Counting][counting]] solves.
+- A join, once [[file:../lib/evaluators/FOL.ml][FOL]] has one, gains =ΔR⁺ ⋈ S= and =R ⋈ ΔS⁺=, against the
+  right states. Computing =ΔR⁺ ⋈ S= means asking =S= for the tuples that
+  agree with each inserted tuple of =R= on the join attributes.
+
+That last question binds some attributes of =S= and leaves the rest
+free. It is the partial binding that no operation in RNT can ask
+today, the gap [[file:modes.org::*Reachable bindings][reachable bindings]] describes. Without it, the only way
+to compute a delta through a join is to read =S= whole, which is
+recomputation by another name.
+
+* Counting
+Deletion through a projection needs to know how many tuples of the input
+produce each tuple of the output. A materialized relation can store that
+count beside each tuple. An inserted input tuple raises the count of
+its projection, a deleted one lowers it, and the projected tuple leaves
+the relation when its count reaches zero. This is the counting algorithm
+of Gupta, Mumick and Subrahmanian ("Maintaining Views Incrementally",
+1993). The same paper gives DRed for recursive relations, where counts
+do not terminate, by deleting an overestimate and rederiving what
+survives.
+
+* Denials are the simplest case
+A [[file:denial.org][denial]] is an ephemeral relation that must stay empty, and checking it
+incrementally is maintenance with most of the work removed.
+
+- Only insertions matter. The state before the commit was admitted, so
+  every denial was empty, and an empty relation has nothing to lose.
+  =ΔD⁻= is always empty.
+- Only emptiness matters. One tuple of =ΔD⁺= is enough to refuse the
+  commit, so the check stops at the first.
+- Nothing is stored. A denial is never materialized, and its delta is
+  thrown away once judged.
+- Nothing is counted, because nothing is ever deleted from a denial.
+
+Incremental denial checking therefore reuses the insertion half of the
+delta rules, stopped at the first tuple. Full maintenance adds
+deletions, counts and storage on top of it.
+
+* What it needs
+Some pieces are shared with incremental denial checking.
+
+1. A binding-aware read, which every relation implements and FOL passes
+   through its plans, to compute deltas through joins.
+2. Indexes, so that such a read is a lookup on a substantial relation
+   rather than a filtered scan.
+3. Read sets, so that RNT knows which relations a derived relation
+   reads and how their attributes line up with its own, and can tell
+   which relations a commit touches.
+4. Tuple deltas. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between
+   two states, and skips subtrees with equal addresses. The tuples that
+   changed inside a relation can be found the same way, by diffing its
+   two tuple sets, since a prolly tree shares every unchanged subtree.
+   RNT does not expose that diff yet.
+
+Others belong to maintenance alone.
+
+5. Materialization, so that a derived relation can be stored with its
+   tuples and counts, and read like a substantial relation.
+6. Deletion rules and counts, as above.
+
+* When maintenance runs
+A commit would apply its changes to the base relations, maintain every
+materialized relation that reads them, then judge the denials against
+the resulting state, and only then move the head. Maintenance has to
+come before judgement, because a denial may read a materialized
+relation. The maintained relations land in the same state as the change
+that caused them, so no state ever holds a stale one.
+
+* Checking it
+A tuple set is content addressed. If the shape of its tree depended only
+on the tuples it holds, and not on the order they were inserted in, a
+maintained relation and the same relation recomputed from scratch would
+have equal addresses exactly when maintenance was correct, and
+comparing the two addresses would test the delta rules completely. The
+chunking in [[file:../lib/kernel/Merkle.ml][Merkle]] is still naive and does not promise that, so until
+it does, the test has to compare the tuples themselves.
diff --git a/docs/modes.org b/docs/modes.org
new file mode 100644
index 0000000..2337b29
--- /dev/null
+++ b/docs/modes.org
@@ -0,0 +1,171 @@
+#+TITLE: Modes
+
+* Extension and intension
+A relation can be known in two ways. Its [[https://en.wikipedia.org/wiki/Extensional_and_intensional_definitions][extension]] is the set of tuples it
+holds, and a tuple belongs to it if it is among them. Its intension is
+the predicate those tuples satisfy, and a tuple belongs to it if the
+predicate says so. A finite relation can be answered from either. A
+relation of [[https://en.wikipedia.org/wiki/Aleph_number][countably infinite]] cardinality can only be answered from
+its intension, since enumerating it never ends.
+
+A reader that waits for the end of an endless relation hangs, so RNT
+has to know before reading whether a read ends, and whether a relation
+can decide membership at all. Modes are how a relation says so. A mode
+states what a relation can answer under a given binding of its
+attributes, and says nothing of whether the answer comes from the
+extension or the intension. The idea comes from logic languages such
+as Mercury, where a predicate declares its [[https://mercurylang.org/information/doc-latest/mercury_ref/Modes.html][modes]], which arguments must
+be bound for a call, and its [[https://mercurylang.org/information/doc-latest/mercury_ref/Determinism.html][determinism]], how many solutions such a
+call has.
+
+* A mode
+[[file:../lib/concepts/Mode.mli][Mode]] describes one with two fields.
+
+#+begin_src ocaml
+type mode = {bound: attributes; yields: Cardinality.t}
+#+end_src
+
+Given values for the attributes in =bound=, the relation produces every
+tuple that agrees with them, and there are at most =yields= of them.
+[[file:../lib/concepts/Cardinality.mli][Cardinality]] has four classes, =Empty=, =Bounded n=, =Finite= and
+=Countable=. Every class but =Countable= is exhaustible, meaning that
+enumeration ends.
+
+A relation declares its modes through the [[file:../lib/protocols/Relation.mli][Relation]] protocol.
+
+#+begin_src ocaml
+method modes : (Concepts.Mode.t, Concepts.Condition.condition) result
+#+end_src
+
+* Generation under a binding
+A mode declared for =B= also serves any binding that includes =B=. The
+relation produces the tuples that agree with =B= and drops those that
+disagree with the extra values, so it produces no more than before.
+
+=Mode.generation modes bound= is therefore the tightest =yields= among
+the modes whose =bound= is a subset of the binding. It is =None= when
+no mode applies, and then the relation cannot be asked under that
+binding at all. This differs from =Countable=, where the relation can
+be asked but its answer never ends. =Mode.exhaustible= tells whether
+the generation ends.
+
+* Membership
+Deciding whether a tuple belongs to a relation means asking the
+relation with every attribute bound. A relation is a set, so at most
+one tuple agrees with a full binding, and a mode over every attribute
+yields =Bounded 1=. That mode is a direct test, an intension. A
+relation without one can still decide by producing the tuples under a
+smaller binding and comparing each, provided that production ends,
+which is deciding by extension. In principle, then, a relation decides
+membership exactly when it is exhaustible with every attribute bound,
+and extension and intension are the same question asked under
+different bindings.
+
+* Reachable bindings
+The principle above is wider than what RNT can do today. The
+[[file:../lib/protocols/Relation.mli][Relation]] and [[file:../lib/protocols/Enumerable.mli][Enumerable]] protocols reach exactly two bindings.
+
+- =enumerate= produces tuples with nothing bound, so it realizes the
+  modes whose =bound= is empty.
+- =contains= answers with every attribute bound, so it realizes the
+  modes whose =bound= is every attribute.
+
+No operation produces the tuples that agree with a partial binding. A
+relation may declare a mode such as ={title; Finite}=, and
+=Mode.generation= takes it into account, but nothing in RNT can act on
+it. In particular, a relation cannot decide membership through a mode
+with a partial binding. It decides only by its own test, or by
+enumerating with nothing bound. A partial mode becomes usable once
+there is an operation that produces tuples under a binding, which is
+also what [[*Indexes][indexes]] need.
+
+* How contains decides
+A substantial relation looks the tuple up by its hash.
+
+An ephemeral relation takes an optional membership test from whoever
+builds it, through =EphemeralRelation.instantiate ?decide=.
+
+- With a test, =contains= uses it.
+- Without one, =contains= enumerates the relation and compares, but
+  only when =Mode.exhaustible modes ∅= holds, meaning its generation
+  with nothing bound ends.
+- Otherwise it fails with =undecidable-membership= and does not
+  enumerate. This is the case when that generation is =Countable=, or
+  when no mode has an empty =bound=.
+
+A relation that declares ={all; Bounded 1}= promises a direct test, so
+whoever builds it must give it one. Nothing checks that promise yet.
+
+The evaluator protocol has no membership method. An ephemeral relation
+generated by a program answers =contains= the way it answers =modes=.
+It invokes the program, asks the relation the program returns, and
+releases it. That result is a relation the evaluator built, and the
+evaluator gave it whatever test it could.
+
+* What relations declare
+A substantial relation stores its tuples in a set keyed by the hash of
+each whole tuple. It declares ={∅; Finite}= for enumerating that set,
+and ={all; Bounded 1}= for the lookup by hash, which needs every
+attribute to compute the hash.
+
+An ephemeral relation that =EphemeralRelation.literal= builds from =n=
+tuples declares ={∅; Bounded n}=.
+
+An ephemeral relation generated by a [[file:../lib/kernel/Program.ml][program]] knows its modes only from
+the relation the program returns, so asking for them invokes the
+program and asks the result. Invoking is lazy. An [[file:evaluators.org][evaluator]] builds
+the result without reading tuples, and FOL reads tuples only when the
+result is enumerated. A program with no state to run within fails with
+=unbound-program=, just as reading its relation would.
+
+A relation that declares no modes cannot be asked under any binding.
+
+* Modes of a FOL plan
+[[file:../lib/evaluators/FOL.ml][FOL]] computes the modes of a plan alongside its heading, before it
+executes anything, and records them on each relation it derives.
+
+- =Base r= has the modes of =r=.
+- =Project (p, A)= keeps the modes of =p= whose =bound= lies within
+  =A=, with the same =yields=.
+
+A projection never yields more tuples than its input, so =yields=
+carries over. A mode that needs an attribute outside =A= no longer
+applies, because a tuple of the projection holds no value for it.
+
+Take =book(title, author)= as a substantial relation, projected on
+=title=. Asking whether ={title: "Codd"}= belongs to the projection
+asks whether some book has that title, by any author. The lookup by
+hash needs the author to hash the whole tuple, so the projection keeps
+only ={∅; Finite}=.
+
+FOL gives a membership test only where it has one. The relation it
+derives for =Base r= takes the =contains= of =r= as its test, so FOL
+over a substantial relation still looks tuples up by hash. The relation
+it derives for a projection has no test, so its =contains= enumerates
+the projection, which reads all of =book=, and compares. That ends
+because =book= is finite.
+
+A projection of a =Countable= relation stays =Countable=. FOL still
+streams it, since a projection reads one tuple at a time and never
+needs the end. Asking such a projection whether it holds a tuple fails
+with =undecidable-membership=.
+
+* Indexes
+An index on an attribute =a= would be a tree keyed by the value of =a=
+and the hash of the tuple, and would add the mode ={a; Finite}=. A
+projection that keeps =a= keeps that mode, so with one index per
+attribute every membership question could stay a lookup. That takes two
+things RNT does not have, the index trees and an operation that
+produces tuples under a partial binding, as [[*Reachable bindings][reachable bindings]]
+explains. Without the operation, the mode an index adds would be
+declared and never used.
+
+Modes carry no cost. A lookup and a full scan both appear as an
+exhaustible generation, and choosing between them belongs to whatever
+plans the query.
+
+* Where exhaustion matters
+Only a reader that runs a relation to its end needs it exhaustible.
+=Relation.read= drains a relation, and admission drains every [[file:denial.org][denial]]
+that holds a tuple, so both hang on a =Countable= relation. Neither
+checks modes yet. Denials will check them once they are reworked.
diff --git a/docs/object-system.org b/docs/object-system.org
index a2f7929..facdda0 100644
--- a/docs/object-system.org
+++ b/docs/object-system.org
@@ -134,7 +134,7 @@ RNT exposes its resources as a hierarchy of objects. The root of this tree is an
 #+end_src
 =register= and =unregister=, as implemented by the root of the hierarchy, allows components to register resources that can be retrieved by users of the system through the corresponding =Directory= interface. The handle passed as an argument to =register= must support being "copy"ed.
 
-As a convenience, a =path= represents a pattern of traversal the object tree. The path ="branch" @/ "master" @/ "multigroup" @/ "universe" @/ this= represents the object that can be retrieved by, from a given reference point, "open"ing the child denoted by ="branch"= on the given reference point, then "open"ing the child denoted ="master"= on the retrieved object, and so on. Every traversal assumes that the object in question has a =Directory= protocol. The ability to construct and manipulate paths is implemented by the =Path= module:
+As a convenience, a =path= represents a pattern of traversal the object tree. The path ="system" @/ "branch" @/ "master" @/ "multigroup" @/ "universe" @/ this= represents the object that can be retrieved by, from a given reference point, "open"ing the child denoted by ="system"= on the given reference point, then "open"ing the child denoted ="branch"= on the retrieved object, and so on. Every traversal assumes that the object in question has a =Directory= protocol. The ability to construct and manipulate paths is implemented by the =Path= module:
 #+begin_src ocaml
   module Path : sig
     type path
diff --git a/docs/object-taxonomy.org b/docs/object-taxonomy.org
index d948845..dda3de3 100644
--- a/docs/object-taxonomy.org
+++ b/docs/object-taxonomy.org
@@ -21,7 +21,9 @@ may remain invariant while the extension differs between the earlier
 and later states.
 
 A branch identifies one such coherent state and provides the basis
-from which another may be produced. It therefore gives RNT a
+from which another may be produced. Each state names the one it
+succeeded, under =previous=, so the history of a branch is reached by
+path. It therefore gives RNT a
 representation of change without requiring mutation to be part of the
 relational semantics. How successive states are physically
 represented, shared, or persisted is an implementation concern.
@@ -253,6 +255,10 @@ state exposed through a branch. A branch may reference multiple
 multigroups and determine the particular state of each that is visible
 from that view of the world.
 
+Within a multigroup, relations are grouped into schemas, which for now
+are only namespaces: \multigroup\[m]\schema\[s]\relation\[r]. The
+canonical name of an attribute is therefore =m:s:r:a=.
+
 * Session
 A session contains state specific to an interaction between a client
 environment and the RNT kernel. It establishes the execution context
diff --git a/docs/roadmap.org b/docs/roadmap.org
new file mode 100644
index 0000000..c9d14cc
--- /dev/null
+++ b/docs/roadmap.org
@@ -0,0 +1,137 @@
+#+TITLE: Roadmap
+
+The work after the [[file:denial.org][denial]] rework, in the order it can be built. Each step
+says why it comes where it does and what has to hold before the next
+one starts. The design behind the steps is in [[file:modes.org][modes]], [[file:denial.org][denials]] and
+[[file:maintenance.org][incremental maintenance]]. Each step lands with its own tests.
+
+* Done
+- Programs are images that name their evaluator, and evaluators
+  =parse= and =eval= their own kinds. See [[file:evaluators.org][programs and evaluators]].
+- Ephemeral relations wrap programs, and storage keeps a program as its
+  evaluator name and source.
+- Every relation declares its modes, and =contains= decides by a test
+  or by reading, never by reading without end.
+- Admission refuses to judge a denial that does not end, and stops at
+  one witness per denial.
+
+* 1. Binding-aware read
+Incremental checking and maintenance both ask a relation for the tuples
+that agree with a partial binding, and no operation can ask that today.
+A mode such as ={title; Finite}= can be declared, and nothing can act on
+it. This is the [[file:modes.org::*Reachable bindings][reachable bindings]] gap, and every later step depends
+on closing it.
+
+The step adds an operation that produces the tuples of a relation under
+a binding of some of its attributes, implemented by every relation.
+
+- A substantial relation filters a scan until it has indexes.
+- FOL passes a binding through a projection to its input when the
+  projection keeps the bound attributes.
+- A relation that wraps a program passes the binding to the relation
+  the program returns.
+
+Membership becomes the case where every attribute is bound.
+
+It is done when a mode with a partial =bound= is usable, and the read
+does what =Mode.generation= says it can. Two questions are open: how a
+binding is represented, and what a relation does when no mode covers
+the binding. Filtering a read under a smaller binding works when that
+read ends, and failing as undecidable is the only other honest answer.
+
+* 2. Indexes
+Without an index, a binding-aware read on a substantial relation still
+reads the whole relation and filters it. It is correct and no faster,
+and a projection still loses the lookup by hash.
+
+The step adds one index per attribute, a prolly tree keyed by the value
+of the attribute and the hash of the tuple, written in the same
+transaction as the tuple set. Each index adds the mode ={a; Finite}=, and
+a projection that keeps =a= keeps it, so membership in a projection
+becomes a lookup.
+
+It is done when a read bound on an indexed attribute reads only the
+matching tuples. Two questions are open: whether indexes on combinations
+of attributes are needed, and whether an index takes part in the
+relation's address. It should not, since an index is derived from the
+tuples.
+
+* 3. Read sets
+RNT cannot tell which denials a commit can break, because a relation
+does not say what it reads. It also cannot turn an inserted tuple into
+bindings on a denial, because it does not know how the denial's
+attributes line up with those of the relations it reads.
+
+The step has every derived relation state the relations it reads and
+where each of its attributes comes from. The =provenance= field of an
+attribute description is the natural place to start.
+
+It is done when, given the relations a commit changed, RNT lists the
+denials that read them, and for each one the binding an inserted tuple
+puts on it.
+
+* 4. Tuple deltas
+The checks in the next steps start from the tuples a commit inserted and
+deleted. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between two states,
+and stops at subtrees with equal addresses. The same walk over the two
+tuple sets of a relation finds the tuples that changed inside it, since
+a prolly tree shares every unchanged subtree.
+
+It is done when RNT gives the inserted and deleted tuples of each
+relation a commit changed, at a cost proportional to the change.
+
+* 5. Incremental denial checking
+Every commit judges every denial over the whole state. With the four
+steps above, a commit can judge only what it can break. For each tuple
+it inserted, it asks each denial that reads that tuple's relation for
+its tuples under the binding the tuple implies, and the first tuple
+found refuses the commit. Deletions never matter, because every denial
+was empty before the commit.
+
+The full check stays for a commit that installs a denial, since a new
+denial has no earlier emptiness to rely on, and for denials that
+declare no usable mode for the binding.
+
+It is done when a commit that touches one relation reads only the bound
+instances of the denials that read it, and its verdict equals the full
+check's on the same states.
+
+* 6. Incremental maintenance
+A materialized ephemeral relation would cost what a substantial one
+costs to read, but every commit that changes its inputs has to change
+it as well. Incremental denial checking is the insertion half of that
+work. Maintenance adds the rest.
+
+- Materialization, so that a derived relation is stored with its tuples.
+- Deletion rules, and a count per tuple of how many input tuples
+  produce it.
+- An order for each commit: apply the change, maintain every
+  materialized relation that reads it, judge the denials, then move the
+  head.
+
+It is done when a maintained relation holds the same tuples as the same
+relation recomputed from scratch, after every commit in the tests.
+
+* Alongside
+These do not block the steps above.
+
+- =Relation.read= reads a relation whole, and a multigroup stores a
+  relation that wraps no program by reading it whole. Both hang on a
+  =Countable= relation and should check its modes first, as admission
+  does.
+- A relation that declares ={all; Bounded 1}= promises a membership
+  test, and nothing checks that it gives one. A program that declares
+  =Finite= and never ends still hangs any reader.
+- FOL detects cycles only among its own programs. A cycle across
+  languages recurses without end.
+- Denials do not protect themselves. Removing one is judged on a state
+  where it is gone. This needs the access checks the [[file:../README.org][README]] plans.
+- Evaluators should declare capability tags, such as =dml=, and the
+  registry should index them.
+- Programs that change state have no result protocol.
+- Once [[file:../lib/kernel/Merkle.ml][Merkle]] chunking depends only on the tuples a tree holds,
+  maintenance can be checked by comparing addresses instead of tuples.
+- =Path.update= keeps the target it looks up and never releases it, so
+  each call leaks one reference to a counted namespace. This came with
+  the lifecycle rework and needs a decision.
+- The signatures in [[file:object-system.org][the object system]] predate the code.