add nested loop join strategy to VM and tests

1 files changed, 98 insertions, 0 deletions

diff --git a/docs/tarski-sakura-separation.md b/docs/tarski-sakura-separation.md
new file mode 100644
index 0000000..a33e2e3
--- /dev/null
+++ b/docs/tarski-sakura-separation.md
@@ -0,0 +1,98 @@
+# Tarski / Sakura Separation of Concerns
+
+This document describes how query analysis responsibilities are divided between
+the **Sakura** OCaml frontend and the **Tarski** FOL runtime inside the C++ VM.
+
+## The Two Runtimes
+
+The VM hosts two distinct execution cores:
+
+| Core | Language | Responsibility |
+|---|---|---|
+| **Tarski** | C++ (this repo) | Mechanical FOL plan execution via Volcano pull model |
+| **Sakura** | OCaml | Query parsing, cardinality analysis, plan emission, physical storage |
+
+Sakura is the authoritative source of data and of query semantics. The SQLite
+backend in this repository exists only for isolated testing; in production,
+CursorManager streams data from Sakura over a well-defined interface.
+
+## What Sakura Is Responsible For
+
+### Cardinality analysis and constraint propagation
+
+Every relation in Sakura carries a cardinality tag: `Finite`, `ConstrainedFinite`,
+`AlephZero`, or `Continuum`. When a query joins multiple relations, Sakura
+propagates these tags through the plan to determine the cardinality of the result.
+
+This analysis is non-trivial. Consider:
+
+```karuta
+natural[A], natural[B], natural[C], plus[A,B,C], eq[C, 10].
+```
+
+Each of `natural`, `plus`, and `eq` is individually `AlephZero`. But Sakura can
+determine that binding `C = 10` via `eq` constrains `plus[A,B,10]` to a finite
+set of natural-number pairs, making the overall result finite. Replacing
+`natural` with `integer` changes the result to infinite, because negative pairs
+also satisfy `plus[A,B,10]`.
+
+Tarski does not repeat this analysis. It receives a plan that is already
+annotated with cardinality metadata and executes it mechanically.
+
+### Termination guarantees
+
+If a query produces an infinite result set, Sakura adds a `TAKE` node to the
+plan before emission. Tarski enforces the `TAKE` limit but makes no independent
+judgement about whether a plan terminates.
+
+### Join ordering
+
+Sakura orders the children of each JOIN so that variables are bound from the
+outer (left) side before the inner (right) side is probed. This ensures that
+builtin relations — which may have `AlephZero` cardinality when arguments are
+unbound — are always probed with fully or partially bound arguments, enabling
+O(1) membership validation rather than unbounded enumeration.
+
+### Physical storage
+
+Sakura owns the physical storage layer. CursorManager pulls paginated tuple
+streams from Sakura; the cursor abstraction hides whether the underlying data
+comes from a stored relation or an ephemeral builtin generator.
+
+## What Tarski Is Responsible For
+
+### Mechanical plan execution
+
+Tarski receives a complete, annotated plan tree from Sakura and executes it via
+the Volcano pull model: `VM::Next(PlanNode*)` propagates demand from the root
+to the leaves, returning one tuple at a time.
+
+### Cardinality-aware execution strategy
+
+Each `PlanNode` carries the cardinality tag Sakura attached at plan time. Tarski
+uses this tag only to choose an execution strategy — never to reason about
+termination:
+
+- **Finite / ConstrainedFinite inner side** → safe to materialize for
+  nested-loop join.
+- **AlephZero inner side, all args bound** → probe via `membership_criteria`
+  in O(1); the generator is never called.
+- **AlephZero inner side, unbound args** → should not occur; Sakura must have
+  added a `TAKE` node or reordered the join. Tarski may assert in debug builds.
+
+### TAKE enforcement
+
+`TAKE` is a first-class node in the plan tree. When `VM::Next` passes through a
+`TAKE` node it decrements a counter and returns `nullptr` once the limit is
+reached, regardless of what the subtree would produce.
+
+## Why This Division Is Correct
+
+The cardinality analysis described above requires understanding the **semantics**
+of each relation — what `plus` means over naturals versus integers, how `eq`
+interacts with a functional relation, and so on. That knowledge lives in Sakura.
+Duplicating it in Tarski would couple two layers that must remain independent and
+would place type-level reasoning inside a mechanical executor.
+
+Tarski's contract is simple: given a safe plan, produce correct tuples. Sakura's
+contract is: emit only safe plans.