update docs with partial bindings

6 files changed, 505 insertions, 118 deletions

diff --git a/docs/denial.org b/docs/denial.org
index d79a394..31d5a58 100644
--- a/docs/denial.org
+++ b/docs/denial.org
@@ -170,18 +170,23 @@ 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
+The question binds some attributes of the denial and leaves others
+free. FOL can state it as a =Where= over the denial's plan, which it
+pushes down to the stored relations and answers from their indexes, as
+[[file:partial-bindings.org][partial bindings]] describes. A denial that binds attributes of its own,
+such as =Where (Base book, {title: "Codd"})=, is already judged that way,
+reading only the index entries it binds. Checking incrementally still
+takes four pieces.
+
+1. 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.
+2. Tuple deltas, so that a commit names the tuples it inserted.
+3. A check offered by the evaluator, since the kernel knows no rule
+   language and cannot derive the restriction for a program it cannot
+   read.
+4. Joins in FOL, since this denial and most others worth checking
+   incrementally join two relations.
 
 ** Denials do not protect themselves
 A commit that removes a denial and breaks its rule is judged on the
diff --git a/docs/maintenance.org b/docs/maintenance.org
index 42b5075..519ea37 100644
--- a/docs/maintenance.org
+++ b/docs/maintenance.org
@@ -26,15 +26,18 @@ the states before and after the commit, operator by operator.
   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.
+- =Where (p, b)= changes as =p= does, keeping only the changed tuples
+  that agree with =b=.
 - 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.
+free. FOL states it as =Where (S, b)=, for the binding =b= each inserted
+tuple puts on the join attributes, and answers it from the index of a
+stored =S=, as [[file:partial-bindings.org][partial bindings]] describes. Without the index, the only
+way to compute a delta through a join would be to read =S= whole, which
+is recomputation by another name.
 
 * Counting
 Deletion through a projection needs to know how many tuples of the input
@@ -65,26 +68,26 @@ 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.
+Two pieces both depend on are in place: FOL's =Where=, which restricts a
+plan to a binding and pushes it down to the stored relations, and
+indexes, which answer such a restriction by lookup rather than by a
+filtered scan. Other 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
+1. 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
+2. 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.
+3. Joins in FOL, since the deltas worth computing run through them.
 
 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.
+4. Materialization, so that a derived relation can be stored with its
+   tuples, counts and indexes, and read like a substantial relation.
+5. Deletion rules and counts, as above.
 
 * When maintenance runs
 A commit would apply its changes to the base relations, maintain every
diff --git a/docs/modes.org b/docs/modes.org
index 2337b29..1cd5905 100644
--- a/docs/modes.org
+++ b/docs/modes.org
@@ -70,14 +70,21 @@ The principle above is wider than what RNT can do today. The
 - =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.
+Neither produces the tuples that agree with a partial binding, and RNT
+does not ask every relation for them. A binding is a condition on
+tuples, and conditions belong to a query language, as [[file:partial-bindings.org::*Where a binding belongs][partial bindings]]
+explains. Two pieces reach partial bindings instead.
+
+- A substantial relation offers =lookup= through the [[file:../lib/protocols/Indexed.mli][Indexed]] protocol,
+  the tuples whose attribute =a= holds a given value, read from its
+  index on =a=. That realizes its mode ={a; Finite}=.
+- A FOL =Where= restricts a plan to the tuples that agree with a
+  binding, and reads an index when its input offers one, as [[*Modes of a FOL plan][the modes
+  of a FOL plan]] describe.
+
+A mode with a partial =bound= that neither reaches is still declared and
+unused. A relation still decides membership only by its own test, or by
+enumerating with nothing bound.
 
 * How contains decides
 A substantial relation looks the tuple up by its hash.
@@ -104,9 +111,10 @@ 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.
+each whole tuple, and keeps an [[*Indexes][index]] on each attribute. It declares
+={∅; Finite}= for enumerating that set, ={all; Bounded 1}= for the lookup
+by hash, which needs every attribute to compute the hash, and
+={a; Finite}= for the index on each attribute =a=.
 
 An ephemeral relation that =EphemeralRelation.literal= builds from =n=
 tuples declares ={∅; Bounded n}=.
@@ -127,23 +135,34 @@ 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=.
+- =Where (Base r, b)=, when =r= offers an index on an attribute =b=
+  binds, has the modes of =r= with the attributes of =b= taken out of
+  each =bound=, by =Mode.given=. The binding supplies their values, and
+  the index produces the tuples, so ={a; Finite}= becomes ={∅; Finite}=.
+- Any other =Where (p, b)= keeps the modes of =p=, since it can only
+  filter what =p= enumerates.
 
 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.
+applies, because a tuple of the projection holds no value for it. A
+restriction never yields more tuples than its input either.
 
 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}=.
+hash needs the author to hash the whole tuple, so the projection loses
+it, and keeps ={∅; Finite}= and the mode ={title; Finite}= of the index
+on =title=.
 
 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.
+because =book= is finite. Asking the same question as
+=Where (Project (book, title), {title: "Codd"})= reads only the index
+entries for ="Codd"=, since FOL pushes the restriction below the
+projection when the projection keeps every attribute it binds.
 
 A projection of a =Countable= relation stays =Countable=. FOL still
 streams it, since a projection reads one tuple at a time and never
@@ -151,14 +170,11 @@ 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.
+A substantial relation keeps an index on each attribute =a=, a tree
+keyed by the encoded value of =a= and the hash of the tuple, and each
+adds the mode ={a; Finite}=. A projection that keeps =a= keeps that mode,
+and a FOL =Where= that binds =a= reads only the matching entries.
+[[file:partial-bindings.org][Partial bindings]] describes how the indexes are stored, read and built.
 
 Modes carry no cost. A lookup and a full scan both appear as an
 exhaustible generation, and choosing between them belongs to whatever
@@ -167,5 +183,6 @@ 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.
+that holds a tuple, so both hang on a =Countable= relation. Admission
+asks a denial for its modes first and refuses one that does not end.
+=Relation.read= does not check them yet.
diff --git a/docs/partial-bindings.org b/docs/partial-bindings.org
new file mode 100644
index 0000000..cf9cf32
--- /dev/null
+++ b/docs/partial-bindings.org
@@ -0,0 +1,331 @@
+#+TITLE: Partial bindings
+
+* Purpose
+A partial binding gives values to some attributes of a relation and
+leaves the rest free. Asking =shelved= for the tuples where
+=title = "Codd"=, with the shelf free, is one. Both [[file:denial.org::*Incremental checking][incremental denial
+checking]] and [[file:maintenance.org][incremental maintenance]] are built from such questions.
+
+This document says why answering a partial binding well takes indexes,
+where the binding itself belongs, how RNT stores and reads its indexes,
+and what is still missing, including builds that do not fit in memory.
+
+* Why a partial binding needs an index
+A [[file:../lib/kernel/SubstantialRelation.ml][substantial relation]] keeps its tuples in a tree keyed by the hash of
+each whole tuple.
+
+- With every attribute bound, the hash can be computed, and the answer
+  is one path down the tree. That is =contains=, and it costs the depth
+  of the tree.
+- With some attribute free, there is no hash to compute. The hash
+  scatters tuples uniformly, so the tuples that agree with the binding
+  sit in arbitrary leaves, and every leaf has to be read.
+
+Correctness does not need an index. Filtering a scan answers any
+binding, at the cost of reading the whole relation, and two questions
+show what that costs.
+
+- An incremental check on the denial of a book shelved twice turns the
+  insertion of =shelved("Codd", "A")= into =shelved(title="Codd", shelf=_)=.
+  Without an index, every commit that shelves a book scans all of
+  =shelved=.
+- Asking whether ={title: "Codd"}= belongs to =book= projected on =title=
+  reads all of =book=, as [[file:modes.org::*Modes of a FOL plan][the modes of a FOL plan]] describe.
+
+An index holds the same tuples ordered by the value of one attribute.
+All the tuples with =a = v= are then contiguous, and answering the
+binding means seeking to the first of them and walking until the value
+changes. That costs the depth of the tree plus the number of matches.
+
+* Where a binding belongs
+A binding is an equality condition on some attributes, and a condition
+on tuples belongs to a query language. RNT does not ask every relation
+to answer one. [[file:../lib/evaluators/FOL.ml][FOL]] states it with a term of its own, and a stored
+relation offers its indexes to whoever reads it.
+
+An earlier design had every relation answer a binding-aware read, so
+that the kernel could ask a denial in any language for its tuples under
+a binding. That buys nothing. The rules that turn a change into
+bindings are written operator by operator for each language, as
+[[file:maintenance.org::*Deltas][maintenance]] shows, and the kernel cannot derive them for a program it
+cannot read. Incremental checking is therefore something an evaluator
+offers, and an evaluator that knows its own plans passes a binding
+through them without the kernel's help.
+
+* Indexing every attribute
+Every attribute of a substantial relation gets an index. Three reasons
+make that the right default rather than a choice per relation.
+
+- The indexes of a relation are then a function of its tuples and its
+  heading alone. Their roots sit in the relation's record, and so in
+  its address, without changing what the address means, since two
+  relations with the same tuples have the same indexes. That holds
+  only while the shape of a tree depends on its keys alone, which
+  [[file:maintenance.org::*Checking it][Merkle does not promise yet]].
+- Each index adds the mode ={a; Finite}=, and a FOL projection keeps it
+  whenever it keeps =a=.
+- A binding over several attributes reads the index of one of them and
+  filters on the rest, so indexes on combinations are not needed yet.
+
+RNT has no NULLs, so every tuple appears in every index, and no index
+is sparse.
+
+** Equality only
+A mode binds attributes to values. It cannot say that an attribute lies
+in a range, and [[file:../lib/concepts/Value.mli][Value]] has only =equal=, with no order, least of all
+between strings and integers. An index therefore answers equality
+alone. Its key keeps the encoded value rather than a hash of it, so that
+ranges stay possible later, given an encoding that sorts in value order
+and modes that can state a range.
+
+** Inside the relation
+An index is not an object of its own in the kernel. It is derived from
+the tuples, and an index that could be published or removed at a path
+could disagree with them, which only access checks could prevent. The
+relation keeps its indexes and reads them on request.
+
+** Selectivity
+Modes carry no cost. An index on a boolean attribute declares the same
+={a; Finite}= as one on a key, and nothing can prefer the selective one.
+A restriction on several attributes reads the index of whichever bound
+attribute the relation lists first. Counts of entries kept in the nodes
+of each tree would give estimates later.
+
+* What RNT has
+** Walking a range of a tree
+[[file:../lib/kernel/Merkle.ml][Merkle]]'s =fold_left= takes an optional start and stop.
+
+#+begin_src ocaml
+val fold_left :
+  ?from:K.t ->
+  ?until:(K.t -> bool) ->
+  S.transaction ->
+  ('c -> K.t -> address -> 'c) ->
+  'c ->
+  node ->
+  ('c, Concepts.Condition.condition) result
+#+end_src
+
+The walk starts at the first key not below =from= and stops before the
+first key =until= accepts. In a trunk it descends only into the child
+that holds =from=, using the same rule as =lookup=, and once it stops it
+fetches no further children. Without either, it is the whole walk it
+always was.
+
+** Index trees
+The index on an attribute =a= is a tree whose key is the encoded value
+of =a= followed by the raw hash of the tuple, and whose value is that
+hash.
+
+#+begin_example
+book(title, author), index on title
+
+ts4:Codd ++ hash(t₁)   →  hash(t₁)
+ts4:Codd ++ hash(t₂)   →  hash(t₂)
+ts4:Date ++ hash(t₃)   →  hash(t₃)
+#+end_example
+
+- The value is encoded as a tuple encodes its values, with
+  =Tuple.bencode_of_value=. Bencode is injective and no encoding is a
+  prefix of another, so the keys of one value are contiguous, and the
+  index is a =Merkle.Make= over =StringKey=, which compares strings byte
+  by byte.
+- The hash of a tuple is the address under which the tuple set stored
+  it, so an index entry points at the stored tuple, and no tuple is
+  stored twice.
+- The record of a substantial relation holds one root per attribute
+  beside the tuple set.
+
+  #+begin_src ocaml
+  type t =
+    { schematics: Concepts.Hash.hash;
+      tuples: TupleSet.address;
+      indexes: Index.address BatMap.String.t }
+  #+end_src
+
+- =store= hashes each tuple once, builds the tuple set, and then one
+  index per attribute of the heading. A tuple with no value for some
+  attribute is refused with =missing-attribute=.
+- =instantiate= stores no tuples under the heading its schema
+  describes, so an empty relation has empty indexes.
+- =modes= adds ={a; Finite}= for each index the record holds.
+
+A relation stored before indexes has no =indexes= field and does not
+load, as [[file:denial.org::*Multigroups from before denials][multigroups from before denials]] do not.
+
+** Reading an index
+A substantial relation offers the [[file:../lib/protocols/Indexed.mli][Indexed]] protocol.
+
+#+begin_src ocaml
+class type implementation = object
+  method indexes : string list
+  method lookup : string -> Concepts.Value.value -> (Handle.t, Concepts.Condition.condition) result
+end
+#+end_src
+
+=lookup a v= returns a cursor over the tuples whose =a= is =v=. It walks
+the index on =a= from the encoded =v= until a key no longer starts with
+it, and reads each tuple at the address its entry holds. An attribute
+with no index is refused with =unindexed-attribute=. =indexes= names the
+attributes that have one, so that a reader can choose without asking.
+
+** Restriction in FOL
+FOL has a term that restricts a plan to the tuples agreeing with a
+binding, named after the =WHERE= of Tutorial D.
+
+#+begin_src ocaml
+type binding = Concepts.Value.value BatMap.String.t
+
+type 'r term =
+  | Base of 'r
+  | Project of 'r term * string BatFingerTree.t
+  | Where of 'r term * binding
+#+end_src
+
+- A binding may name only attributes of the heading it restricts, and
+  =describe= refuses any other with =unknown-attribute=.
+- =instantiate= pushes each =Where= below a =Project= that keeps every
+  attribute it binds, once stored programs are expanded. A restriction
+  asked of a stored program therefore reaches the stored relations the
+  program reads. A =Where= that binds an attribute the projection drops
+  stays where it is and is refused.
+- A =Where= over a =Base= reads the base relation itself. If it offers an
+  index on a bound attribute, the restriction looks that value up.
+  Otherwise it enumerates. Either way it keeps only the tuples that
+  agree with the whole binding.
+- Its membership test checks the binding, then asks its input.
+- Through an index, its modes are those of the base with the bound
+  attributes taken out of each =bound=, by =Mode.given=, since the binding
+  supplies their values and the index produces the tuples. ={a; Finite}=
+  becomes ={∅; Finite}=. Otherwise it keeps the modes of its input,
+  since it can only filter what that input enumerates.
+
+A denial written as =Where (Base book, {title: "Codd"})= is therefore
+exhaustible with nothing bound, and judging it reads only the index
+entries for ="Codd"=.
+
+* Memory
+** Reading
+An index is a tree in storage like the tuple set, and LMDB maps it in
+as it is read. A lookup holds one path and the leaf it is in, a few
+nodes of some kilobytes each, whatever the size of the index. A value
+that matches half the relation streams through the cursor rather than
+being collected. Its cost is a matter of [[*Selectivity][selectivity]], not of memory.
+
+** Building today
+=store= receives its tuples as a list, so the relation is in memory
+before any index is built. =TupleSet.of_list= and =Index.of_list= then
+insert one entry at a time inside =with_batch=. Each insert persists the
+whole path to its leaf, and the batch keeps every version of every node
+until it flushes, so a build holds about =N × depth= nodes of some 64
+entries each rather than =N= entries. The indexes are built one after
+another, so the peak is the tuple list, the entries of one index, and
+one batch.
+
+** Steady state
+With [[file:roadmap.org::*2. Tuple deltas][tuple deltas]], a commit would insert and remove its changed tuples
+in the tuple set and in each index, touching about the size of the
+change times the depth of the tree in each. Nothing would be rebuilt.
+
+** Builds that do not fit
+Some builds start from nothing: an import, a relation materialized for
+the first time, a relation stored before indexes, or a new kind of index
+added later. Three things in them outgrow memory, and RNT handles none of
+them yet.
+
+| What grows                    | Why                                                                                                   | What to do                                                                                                                    |
+|-------------------------------+-------------------------------------------------------------------------------------------------------+-------------------------------------------------------------------------------------------------------------------------------|
+| The input to sort             | entries arrive in the order of the tuple hash, and each index needs them in the order of its own key | sort externally: write sorted runs to scratch storage and merge them into the builder; a scratch LMDB database can do the sort at first |
+| The builder                   | building by repeated =insert= copies a path on each insert and keeps every version                    | build bottom-up from the sorted stream, holding one node per level                                                            |
+| The batch and the transaction | =with_batch= keeps every node it makes until the end, and one transaction holds every page it writes   | write nodes directly, in short transactions of a bounded number of entries                                                    |
+
+Writing outside the commit's own transaction is safe because nodes are
+content addressed. Nothing reaches a node until the head moves to a
+state that holds it, and the head moves atomically. A build that fails
+leaves nodes nothing reaches, which a garbage collector has to reclaim.
+A publish that fails already leaves such nodes today, since each level
+of a commit writes in its own transaction.
+
+A bottom-up build must make the same tree that inserting the same keys
+would, or the address of a relation would depend on how it was built.
+
+** What storing a relation reads
+=Multigroup= stores a relation by reading it whole, and that read is
+easy to misjudge.
+
+- A relation with an address never reaches the read. Its admission
+  stores it as that address.
+- A program is stored as its source, and is not read either.
+- What is read is a relation with neither: a literal, whose tuples are
+  already in memory, or a lazy relation, such as the result of a query,
+  read for the first time.
+
+The large read is the caller's. [[file:../lib/kernel/Scope.mli][Scope.publish]] binds whole relations and
+FOL has no union, so adding one tuple to a stored relation means
+reading all of it into a literal first.
+
+** Delta relations
+A delta relation would be a stored relation, its base, together with
+the tuples to insert, =I=, and the tuples to delete, =D=.
+
+#+begin_example
+t ∈ delta  ⇔  t ∈ I ∨ (t ∈ base ∧ t ∉ D)
+#+end_example
+
+Its membership is decided by lookups, without reading the extension.
+Admission would store it by applying =I= and =D= to the tree of the base
+and to each of its indexes, reading only the change, and =publish= would
+take one in place of a whole relation.
+
+* Reuse for maintenance and checking
+Views in RNT are [[file:../lib/kernel/EphemeralRelation.ml][ephemeral relations]], and [[file:maintenance.org][incremental maintenance]]
+would materialize them. Each piece above is one that maintenance and
+incremental checking need.
+
+- Delta rules are restrictions. =ΔR⁺ ⋈ S= asks =S= for the tuples that
+  agree with each inserted tuple of =R= on the join attributes, which is
+  a =Where= on =S=, answered from its index.
+- A denial check for an inserted tuple is the denial restricted by the
+  binding that tuple implies, stopped at its first tuple. For a FOL
+  denial, the restriction passes through its plan to the stored
+  relations it reads.
+- Applying a change to a materialized view would be admitting a delta
+  relation, with =ΔV⁺= and =ΔV⁻= as =I= and =D=.
+- A materialized view stored as a substantial relation has indexes of
+  its own, maintained by the same change, so a view over a view stays
+  incremental.
+- Deleting through a projection asks how many tuples of the input
+  produce a tuple of the view. That binds every attribute of the view,
+  so it is a lookup by hash.
+- With the index roots in the address, comparing a maintained view
+  with the same view recomputed from scratch, as [[file:maintenance.org::*Checking it][checking it]] proposes,
+  tests the maintenance of its indexes too.
+
+A view that is not materialized needs none of this. A restriction
+passes through its plan, and it pays for the computation on each read.
+
+* What is missing
+1. Read sets, so that RNT knows which denials a commit can break and
+   how an inserted tuple binds each of them.
+2. Tuple deltas, and delta relations to carry them in a commit.
+3. A check offered by the evaluator: given the tuples a commit inserted
+   into the relations a denial reads, restrict the denial by each and
+   read its first tuple.
+4. Joins in FOL. Most rules worth checking incrementally join two
+   relations, and a restriction through a join binds both sides on the
+   join attributes.
+5. Builds that do not fit in memory, once there is a large or lazy
+   source to build from.
+
+* Open questions
+- Where a materialized view keeps its counts. If a count lives in the
+  record a tuple set points to, a change of count changes that address.
+  Index entries should point to the tuple itself, so that a count can
+  change without touching any index.
+- When indexes on combinations of attributes earn their place.
+- What collects the nodes that failed builds and failed publishes leave
+  behind.
+- A tuple's =type_= is part of its hash and not of its heading. Two
+  tuples that differ only in =type_= agree with every binding, so
+  ={all; Bounded 1}= holds only while the tuples of a relation share
+  one =type_=.
diff --git a/docs/roadmap.org b/docs/roadmap.org
index f36bdbd..4e95f7a 100644
--- a/docs/roadmap.org
+++ b/docs/roadmap.org
@@ -2,8 +2,9 @@
 
 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.
+one starts. The design behind the steps is in [[file:modes.org][modes]], [[file:denial.org][denials]],
+[[file:partial-bindings.org][partial bindings]] and [[file:maintenance.org][incremental maintenance]]. Each step lands with its
+own tests.
 
 * Done
 - Programs are images that name their evaluator, and evaluators
@@ -14,49 +15,20 @@ one starts. The design behind the steps is in [[file:modes.org][modes]], [[file:
   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
+- [[file:../lib/kernel/Merkle.ml][Merkle]] walks a range of keys, from a key and until a predicate.
+- A substantial relation keeps an index on each attribute, declares
+  ={a; Finite}= for each, and answers =lookup= through the [[file:../lib/protocols/Indexed.mli][Indexed]]
+  protocol. See [[file:partial-bindings.org::*What RNT has][partial bindings]].
+- FOL restricts a plan with =Where=, pushes the restriction below the
+  projections that keep its attributes, and reads an index when its
+  input offers one. A denial can bind attributes, and admission judges
+  it through the index.
+
+These two replace the binding-aware read this roadmap once planned for
+every relation. A binding is a condition on tuples, and conditions
+belong to a query language, as [[file:partial-bindings.org::*Where a binding belongs][partial bindings]] explains.
+
+* 1. 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
@@ -64,45 +36,62 @@ 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.
+attribute description is the natural place to start, and a FOL plan
+knows both from its terms.
 
 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
+* 2. 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.
 
+A commit should also be able to carry such a change rather than a whole
+relation. Today [[file:../lib/kernel/Scope.mli][Scope.publish]] binds whole relations, so adding one
+tuple means reading the relation into a literal first. A [[file:partial-bindings.org::*Delta relations][delta
+relation]], a stored base with tuples to insert and delete, would let
+admission apply the change to the base's tuple set and indexes alone.
+
 It is done when RNT gives the inserted and deleted tuples of each
-relation a commit changed, at a cost proportional to the change.
+relation a commit changed, at a cost proportional to the change, and a
+commit that changes one tuple writes only the paths to it.
 
-* 5. Incremental denial checking
-Every commit judges every denial over the whole state. With the four
+* 3. Incremental denial checking
+Every commit judges every denial over the whole state. With the two
 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
+it inserted, each denial that reads that tuple's relation is restricted
+by 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 kernel knows no rule language and cannot derive that restriction
+for a program it cannot read, so the evaluator offers the check. For a
+FOL denial it is a =Where= over the denial's plan, which FOL already
+pushes down to the stored relations and answers from their indexes. A
+denial whose evaluator offers no such check keeps the full check, and
+so does a commit that installs a denial, since a new denial has no
+earlier emptiness to rely on.
+
+Most rules worth checking this way join two relations, so FOL needs
+joins for the step to reach them. A restriction through a join binds
+both sides on the join attributes.
+
+It is done when a commit that touches one relation reads only the
+restricted denials that read it, and its verdict equals the full
 check's on the same states.
 
-* 6. Incremental maintenance
+* 4. 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.
+- Materialization, so that a derived relation is stored with its tuples
+  and its indexes.
 - Deletion rules, and a count per tuple of how many input tuples
   produce it.
 - An order for each commit: apply the change, maintain every
@@ -112,6 +101,24 @@ work. Maintenance adds the rest.
 It is done when a maintained relation holds the same tuples as the same
 relation recomputed from scratch, after every commit in the tests.
 
+* 5. Builds that do not fit in memory
+A substantial relation builds its tuple set and each index by inserting
+one entry at a time inside =with_batch=, which keeps every version of
+every node until it flushes. A build holds about =N × depth= nodes, more
+than the tuples it stores. Tuple deltas remove the rebuild from ordinary
+commits, but an import, a first materialization, or a relation stored
+before indexes still builds from nothing.
+
+The step sorts the entries of each tree, on disk when they do not fit,
+builds the tree bottom-up from the sorted stream, and writes its nodes
+in short transactions. [[file:partial-bindings.org::*Builds that do not fit][Partial bindings]] gives the details. A tree
+built bottom-up must equal the tree inserting the same keys would make,
+or a relation's address would depend on how it was built.
+
+It is done when building a relation holds a bounded number of nodes,
+whatever its size, and yields the same address as building it by
+insertion.
+
 * Alongside
 These do not block the steps above.
 
@@ -122,6 +129,9 @@ These do not block the steps above.
 - 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.
+- A tuple's =type_= is part of its hash and not of its heading, so
+  ={all; Bounded 1}= holds only while the tuples of a relation share one
+  =type_=.
 - 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
@@ -131,10 +141,8 @@ These do not block the steps above.
 - 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.
-- Storing a relation reads it whole. [[file:../lib/kernel/Multigroup.ml][Multigroup]] admits a relation by
-  draining it with =Relation.read= before the write begins, and
-  [[file:../lib/kernel/SubstantialRelation.ml][SubstantialRelation]] builds its tree from that list. Streaming the
-  cursor into the tree instead would read during the write, holding
-  the writer lock while the relation is computed, and =with_batch=
-  would still keep every node it makes until the batch ends.
+- A leaked handle's finalizer can dereference a handle that was already
+  invalidated, so tests fail with =Attempt to dereference an invalid
+  handle!= in whichever test the collector happens to run, depending on
+  the size of the minor heap.
 - The signatures in [[file:object-system.org][the object system]] predate the code.
diff --git a/docs/subsystem-interop.org b/docs/subsystem-interop.org
new file mode 100644
index 0000000..b8503c1
--- /dev/null
+++ b/docs/subsystem-interop.org
@@ -0,0 +1,23 @@
+RNT is going for a route of a microkernel, and here is one use case
+for its servers: imagine a subsystem A and subsystem B. Each register
+an evaluator and has their specific program image execution from their
+own server, operating under an RNT supervisor. A program image from
+subsystem A should be able to invoke and interop with programs from B,
+as they both share the common ephemeral relation protocol.
+
+A more concrete case that is warranted is Sakura and Karuta. Here is a
+brief introduction of what each is:
+
+- Sakura :: A purely relational algebra system that performs strictly
+  first order logic for data retrieval, and integrates other
+  subsystems for DDL, DML and version control.
+- Karuta :: A logic language targeting the BEAM, similar to Prolog,
+  but that operates under microKanren.
+
+Karuta compiles programs to a /.beam/ format, and embeds them with two
+additional /.lfe/ files: karuta.lfe & sakura.lfe, and executes them with
+/play/ lfescript that glues all together.
+
+Our goal with the subsystem integration is to make Karuta produce
+Sakura programs (it already does), that can be loaded as program
+images on RNT, executing through the registered evaluator.