update docs with partial bindings

1 files changed, 77 insertions, 69 deletions

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.