docs for hashed index keys, merged restrictions and narrower where modesindexes

2 files changed, 51 insertions, 39 deletions

diff --git a/docs/modes.org b/docs/modes.org
index 1cd5905..2da300a 100644
--- a/docs/modes.org
+++ b/docs/modes.org
@@ -135,10 +135,11 @@ 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}=.
+- =Where (Base r, b)=, when =r= offers an index on an attribute =a= that
+  =b= binds, has the modes of =r= with =a= taken out of each =bound=, by
+  =Mode.given=. The binding supplies its value, and the index produces
+  the tuples, so ={a; Finite}= becomes ={∅; Finite}=. The other attributes
+  of =b= only filter what the index produces, so they stay bound.
 - Any other =Where (p, b)= keeps the modes of =p=, since it can only
   filter what =p= enumerates.
 
@@ -171,7 +172,7 @@ with =undecidable-membership=.
 
 * Indexes
 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
+keyed by the hash of the 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.
diff --git a/docs/partial-bindings.org b/docs/partial-bindings.org
index cf9cf32..92f52d9 100644
--- a/docs/partial-bindings.org
+++ b/docs/partial-bindings.org
@@ -74,9 +74,11 @@ is sparse.
 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.
+alone, and its key holds a hash of the value rather than the value
+itself. Every key then has the same length, however long the value,
+which keeps both the nodes and their [[file:../lib/kernel/Merkle.ml][chunking]] cheap. Ranges would need
+another index, keyed by 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
@@ -93,46 +95,50 @@ 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.
+[[file:../lib/kernel/Merkle.ml][Merkle]] walks a tree with =foldm_left=, which takes an optional start
+and stop.
 
 #+begin_src ocaml
-val fold_left :
+val foldm_left :
   ?from:K.t ->
   ?until:(K.t -> bool) ->
   S.transaction ->
-  ('c -> K.t -> address -> 'c) ->
+  ('c -> K.t -> address -> ('c, Concepts.Condition.condition) result) ->
   '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.
+first key =until= accepts, or at the first error. 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. =fold_left= is the same walk with a step
+that cannot fail, and the =fold_left= of =Merkle.Interface= takes the same
+range and reads the value at each address it passes.
 
 ** 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.
+The index on an attribute =a= is a tree whose key is the raw hash of the
+encoded value of =a= followed by the raw hash of the tuple, and whose
+value is the hash of the tuple.
 
 #+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₃)
+hash("Codd") ++ hash(t₁)   →  hash(t₁)
+hash("Codd") ++ hash(t₂)   →  hash(t₂)
+hash("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.
+  =Tuple.bencode_of_value=, and hashed. Every key is two hashes long, so
+  the keys of one value are contiguous, and the index is a
+  =Merkle.Interface= over =StringKey=, which compares strings byte by
+  byte, and over tuples.
 - 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.
+  stored twice. The index is built over those addresses, with the
+  =of_list= of its =Tree=, so that building it stores nothing but nodes.
 - The record of a substantial relation holds one root per attribute
   beside the tuple set.
 
@@ -143,9 +149,11 @@ ts4:Date ++ hash(t₃)   →  hash(t₃)
       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=.
+- =store= first checks every tuple against the heading. A tuple with no
+  value for some attribute is refused with =missing-attribute=, and one
+  with an attribute the heading lacks with =unexpected-attribute=, before
+  anything is written. It then hashes each tuple once, builds the tuple
+  set, and one index per attribute of the heading.
 - =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.
@@ -164,7 +172,7 @@ 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
+the index on =a= from the hash of =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.
@@ -185,19 +193,22 @@ type 'r term =
 - 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.
+  attribute it binds, once stored programs are expanded, and merges it
+  into a =Where= it meets when their bindings agree. A restriction asked
+  of a stored program therefore reaches the stored relations the
+  program reads as one binding. 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,
+- Through an index, its modes are those of the base with the attribute
+  the index reads taken out of each =bound=, by =Mode.given=, since the
+  binding supplies its value and the index produces the tuples.
+  ={a; Finite}= becomes ={∅; Finite}=. The other bound attributes stay in
+  each =bound=, because they only filter what the index produces and
+  cannot make it end. Without an index, 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
@@ -214,7 +225,7 @@ being collected. Its cost is a matter of [[*Selectivity][selectivity]], not of m
 
 ** 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
+before any index is built. =TupleSet.of_list= and =Index.Tree.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