lack of provenance on shadowing of tuple merge quantification fix

3 files changed, 708 insertions, 2 deletions

diff --git a/docs/dcl-quantification.org b/docs/dcl-quantification.org
new file mode 100644
index 0000000..81e9cad
--- /dev/null
+++ b/docs/dcl-quantification.org
@@ -0,0 +1,480 @@
+#+TITLE: DCL Quantification: Runtime Model and Evaluation
+
+* Overview
+
+This document describes precisely how DCL constraints are represented, compiled,
+and evaluated at runtime. It covers the full stack from the s-expression syntax
+through AST compilation, context construction, and recursive evaluation — with
+particular attention to the cost model of quantifiers, which is the primary target
+for future performance work.
+
+* Constraint Type (~lib/constraint.ml~)
+
+The runtime constraint type is an algebraic tree:
+
+#+begin_src ocaml
+type t =
+  | MemberOf of { target : relation_name; binding : binding }
+  | Not      of { body : t; universe : relation_name }
+  | And      of t list
+  | Or       of t list
+  | Exists   of { variable : attr_name; quantifier : relation_name; body : t }
+  | Forall   of { variable : attr_name; quantifier : relation_name; body : t }
+#+end_src
+
+A ~binding~ is a ~BindingMap~ (a ~Map.Make(String)~) from target attribute names
+to ~binding_expr~:
+
+#+begin_src ocaml
+type binding_expr =
+  | Var   of attr_name               (* resolved from current tuple at eval time *)
+  | Const of Conventions.AbstractValue.t  (* literal, resolved at compile time *)
+#+end_src
+
+The ~variable~ field in ~Exists~ and ~Forall~ names the bound tuple for use in
+~Var~ expressions inside the body. Attributes from the quantifier row are merged
+into the evaluation tuple under the prefix ~variable ^ "."~, so ~(Var "d.dept_id")~
+unambiguously refers to the ~dept_id~ attribute of the tuple bound to variable ~"d"~.
+See [[*Tuple Extension: ~extend_tuple~][Tuple Extension: extend_tuple]] for the implementation and [[*The Variable Namespacing Problem][The Variable Namespacing Problem]]
+for the history of the bug this fixes.
+
+* Evaluation Context (~eval_context~)
+
+Evaluation does not access storage or the database directly. It works through an
+~eval_context~ record built once per insert operation and closed over a specific
+~(storage, db)~ snapshot:
+
+#+begin_src ocaml
+type eval_context = {
+  check_membership :
+    relation_name ->
+    (attr_name * Conventions.AbstractValue.t) list ->
+    bool;
+  iterate_finite :
+    relation_name ->
+    (attr_name * Conventions.AbstractValue.t) list list option;
+}
+#+end_src
+
+Both fields are closures. This indirection decouples ~Constraint.evaluate~ from
+the storage backend and allows the same constraint tree to be evaluated against
+different snapshots.
+
+** ~check_membership~
+
+Built in ~Manipulation.Make.build_eval_context~. Given a relation name and a list
+of ~(attr_name, value)~ pairs, it returns ~true~ iff a tuple exists in the named
+relation whose attributes match every pair in the list.
+
+The implementation:
+1. Looks up the relation in the ~db~ snapshot.
+2. Constructs a synthetic ~Tuple.Materialized~ from the bound pairs and runs
+   ~rel.membership_criteria~ against it. If it fails, returns ~false~ immediately.
+3. If the relation has no Merkle tree (ephemeral/generator relation),
+   ~membership_criteria~ alone is trusted and the function returns ~true~.
+4. If the relation has a tree, it calls ~Merkle.keys tree~ to obtain *all* tuple
+   hashes, then linearly scans them. For each hash it:
+   a. Loads the raw bytes from storage (~Storage.load_raw~).
+   b. Deserialises the ~Storable.Tuple.t~ to get the attribute hash list.
+   c. For each bound pair ~(bk, bv)~, finds the matching attribute by name, loads
+      its value bytes from storage (~Storage.load_raw~ again), unmarshals it, and
+      compares with ~Stdlib.(=)~.
+   d. Short-circuits to ~true~ on the first tuple that satisfies all pairs.
+   e. Returns ~false~ if no tuple matches.
+
+The cost of a single ~check_membership~ call on a relation of cardinality /n/ with
+/a/ bound attributes and average /k/ attributes per stored tuple is:
+
+  O(n · (1 + a · k))   storage round-trips in the worst case.
+
+No indexes exist. Every check is a full table scan at the storage level.
+
+** ~iterate_finite~
+
+Given a relation name, returns ~Some rows~ where ~rows~ is a fully materialised
+list of rows, each a ~(attr_name * AbstractValue.t) list~. Returns ~None~ if the
+relation has infinite or unconstrained cardinality
+(~AlephZero~ or ~Continuum~ in ~Conventions.Cardinality~).
+
+Only relations with cardinality ~Finite _~ or ~ConstrainedFinite~ are iterable.
+Generator-based relations with no tree return ~Some []~.
+
+The materialisation path:
+1. ~Merkle.keys tree~ — loads all tuple hashes.
+2. For each hash: ~Storage.load_raw~ → ~Storable.Tuple.of_bytes~ → attribute hash list.
+3. For each attribute hash: ~Storage.load_raw~ → ~Marshal.from_bytes~.
+
+This eagerly materialises the *entire* quantifier relation into memory before
+evaluation begins. For a relation of cardinality /n/ with /k/ attributes each,
+the cost is O(n · k) storage loads and the full result occupies O(n · k) memory.
+
+* Variable Resolution: ~bind~
+
+Before a ~MemberOf~ check is executed, the binding map is resolved against the
+current tuple via ~bind~:
+
+#+begin_src ocaml
+let bind (b : binding) (tuple : Tuple.materialized)
+    : (attr_name * Conventions.AbstractValue.t) list =
+  BindingMap.fold
+    (fun target_attr expr acc ->
+      let value = match expr with
+        | Const v    -> Some v
+        | Var src_attr ->
+          match Tuple.AttributeMap.find_opt src_attr tuple.attributes with
+          | Some attr -> Some attr.Attribute.value
+          | None      -> None
+      in
+      match value with
+      | Some v -> (target_attr, v) :: acc
+      | None   -> acc)
+    b []
+#+end_src
+
+Key behaviour:
+- ~Const v~ is lifted directly; no attribute lookup.
+- ~Var src_attr~ looks up ~src_attr~ in ~tuple.attributes~. If the attribute is
+  absent, the pair is *silently dropped* from the bound list. A ~MemberOf~ with
+  incomplete bindings may match unintended tuples or always pass if the target
+  relation contains tuples with fewer attributes.
+- The result is a plain assoc list, not a map; duplicate keys are possible if
+  the binding contains both a ~Const~ and a ~Var~ targeting the same name.
+
+* Tuple Extension: ~extend_tuple~
+
+When a quantifier (~Exists~ or ~Forall~) iterates over a row, it extends the
+current evaluation tuple by merging that row's attributes in:
+
+#+begin_src ocaml
+and extend_tuple (tuple : Tuple.materialized)
+    (variable : attr_name)
+    (row : (attr_name * Conventions.AbstractValue.t) list)
+    : Tuple.materialized =
+  let extra_attrs =
+    List.fold_left
+      (fun acc (k, v) ->
+        Tuple.AttributeMap.add (variable ^ "." ^ k) { Attribute.value = v } acc)
+      tuple.attributes row
+  in
+  { tuple with attributes = extra_attrs }
+#+end_src
+
+Two important facts:
+
+1. *Quantifier attributes are namespaced by the variable name.* Each attribute ~k~
+   from the quantifier row is inserted as ~variable ^ "." ^ k~. The incoming tuple's
+   own attributes are never overwritten. ~(Var "dept_id")~ resolves to the base
+   tuple's value; ~(Var "d.dept_id")~ resolves to the value contributed by the
+   quantifier bound to ~"d"~. See [[*The Variable Namespacing Problem][The Variable Namespacing Problem]] for the
+   earlier behaviour where ~variable~ was ignored and overwrites were silent.
+
+2. *A new ~AttributeMap~ is allocated on every extend call.* With /a/ existing
+   attributes and /r/ new attributes from the row, ~fold_left~ performs /r/
+   ~AttributeMap.add~ operations each building on the previous map. For /q/
+   nested quantifiers of cardinalities /n₁, n₂, ..., nq/, ~extend_tuple~ is
+   called /n₁ · n₂ · ... · nq/ times total — once per combination.
+
+* Recursive Evaluation: ~evaluate~
+
+#+begin_src ocaml
+let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
+    : (bool, diagnostic) result =
+#+end_src
+
+The function is structurally recursive over the constraint tree. Each case:
+
+** ~MemberOf~
+
+#+begin_src ocaml
+| MemberOf { target; binding } ->
+  let bound_values = bind binding tuple in
+  if ctx.check_membership target bound_values then Ok true
+  else Error (MembershipFailed { target; bound_values })
+#+end_src
+
+Resolves bindings from the current tuple (O(|binding|) attribute lookups), then
+delegates to ~check_membership~. Returns ~Ok true~ or ~Error~ (never ~Ok false~)
+— the ~Ok false~ branch of ~Exists~/~Forall~ is distinguished from ~Error~.
+
+** ~Not~
+
+#+begin_src ocaml
+| Not { body; universe = _ } ->
+  match evaluate ctx tuple body with
+  | Ok true              -> Ok false
+  | Ok false             -> Ok true
+  | Error (MembershipFailed _) -> Ok true
+  | Error d              -> Error d
+#+end_src
+
+~MembershipFailed~ from the body is treated as ~Ok true~ (negation of a failed
+membership = the tuple is not a member = negation succeeds). The ~universe~ field
+is a declarative annotation for closed-world reasoning and is not used at runtime.
+
+** ~And~ / ~Or~
+
+Both use short-circuit evaluation:
+- ~And~: stops at the first ~Ok false~ or ~Error~.
+- ~Or~: stops at the first ~Ok true~; swallows ~Error~ branches and continues.
+
+Neither produces diagnostics for the other branches once a decision is reached.
+Note that ~evaluate_named~ (which evaluates all named constraints on a tuple) does
+*not* short-circuit — it collects all failures before returning.
+
+** ~Exists~
+
+#+begin_src ocaml
+| Exists { variable; quantifier; body } ->
+  match ctx.iterate_finite quantifier with
+  | None      -> Error (UnboundedQuantifier { variable; quantifier })
+  | Some rows ->
+    let rec check = function
+      | []           -> Ok false
+      | row :: rest  ->
+        let extended_tuple = extend_tuple tuple variable row in
+        match evaluate ctx extended_tuple body with
+        | Ok true  -> Ok true
+        | Ok false -> check rest
+        | Error _  -> check rest
+    in
+    check rows
+#+end_src
+
+The execution model:
+1. ~iterate_finite~ is called, fully materialising the quantifier relation.
+2. Rows are iterated sequentially. For each row, ~extend_tuple~ merges it into
+   the current tuple, and ~evaluate~ recurses into the body.
+3. The first ~Ok true~ short-circuits: remaining rows are not evaluated.
+4. Both ~Ok false~ and ~Error~ from the body are treated identically — the row is
+   skipped and iteration continues. *Errors inside the body of an ~Exists~ are
+   silently discarded.*
+5. If all rows are exhausted without ~Ok true~, returns ~Ok false~.
+
+An ~Exists~ over a relation of cardinality /n/ with a body whose evaluation cost
+is /C/ has worst-case cost O(n · C). Nesting two ~Exists~ quantifiers over
+relations of cardinalities /n/ and /m/ has worst-case cost O(n · m · C).
+In general, /q/ nested quantifiers produce O(∏ nᵢ · C) body evaluations — a
+Cartesian product.
+
+** ~Forall~
+
+#+begin_src ocaml
+| Forall { variable; quantifier; body } ->
+  match ctx.iterate_finite quantifier with
+  | None      -> Error (UnboundedQuantifier { variable; quantifier })
+  | Some rows ->
+    let rec check = function
+      | []          -> Ok true
+      | row :: rest ->
+        let extended_tuple = extend_tuple tuple variable row in
+        match evaluate ctx extended_tuple body with
+        | Ok true               -> check rest
+        | Ok false              -> Ok false
+        | Error (MembershipFailed _) -> Ok false
+        | Error d               -> Error d
+    in
+    check rows
+#+end_src
+
+Symmetric to ~Exists~ but short-circuits on ~Ok false~ or ~MembershipFailed~.
+Unlike ~Exists~, other ~Error~ variants (e.g., ~UnboundedQuantifier~) are
+propagated rather than silently consumed. The cost model is identical: O(∏ nᵢ · C).
+
+* The Variable Namespacing Problem
+
+This section documents the original bug and explains why the current implementation
+is correct. In the initial implementation, ~extend_tuple~ took ~variable~ as
+~_variable~ — a named-but-discarded argument — and merged quantifier row attributes
+flat into the tuple under their original names. This had two consequences.
+
+** Attribute Shadowing (fixed)
+
+If the incoming tuple and the quantifier row shared an attribute name, the
+quantifier's value won silently. Concretely: an Employee with ~dept_id=99~ being
+checked by an ~Exists~ over Department rows would have its ~dept_id~ overwritten
+by each Department row's ~dept_id~ in turn. ~(Var "dept_id")~ in the body then
+resolved to the Department's own id, not the Employee's. An FK constraint written
+as ~(MemberOf (target "Department") (binding ((dept_id (Var "dept_id")))))~ inside
+an ~Exists~ over Department would always pass — it was validating the Department
+against itself rather than checking whether the Employee's ~dept_id~ existed.
+
+** Multi-Quantifier Ambiguity (fixed)
+
+With two nested quantifiers over relations sharing attribute names, the inner
+quantifier's pass through ~extend_tuple~ overwrote what the outer one had written.
+There was no way to write a body that simultaneously referred to attributes from
+two distinct quantifier rows of the same name.
+
+** Resolution
+
+Both problems are resolved by namespacing: each attribute ~k~ from the quantifier
+row is stored as ~variable ^ "." ^ k~. The base tuple is never modified. The
+~variable~ argument, previously discarded as ~_variable~, is now the namespace
+prefix. The fix is in ~lib/constraint.ml~ with an inline TODO describing the
+deeper issue of tuple-level provenance as a structural solution.
+
+* N-Ary Quantification
+
+The current AST represents each quantifier as a single ~(variable, quantifier)~
+pair. N-ary constraints across three or more relations require nesting:
+
+#+begin_src lisp
+(Exists (variable "b") (quantifier "Building")
+  (Exists (variable "r") (quantifier "Room")
+    (Exists (variable "s") (quantifier "Suite")
+      ...)))
+#+end_src
+
+This is semantically correct once namespacing is in place, but verbose and implies
+a strict left-to-right evaluation order with no opportunity for reordering.
+
+The proposed n-ary form makes the binding list first-class:
+
+#+begin_src lisp
+(Exists
+  (bindings ((b "Building") (r "Room") (s "Suite")))
+  (body ...))
+#+end_src
+
+The executor folds over the binding list left-to-right, extending the tuple at
+each step — equivalent to nested ~Exists~ but expressed as a single node:
+
+#+begin_src ocaml
+| Exists { bindings; body } ->
+  let rec go bindings tuple =
+    match bindings with
+    | [] -> evaluate ctx tuple body
+    | (variable, quantifier) :: rest ->
+      match ctx.iterate_finite quantifier with
+      | None -> Error (UnboundedQuantifier { variable; quantifier })
+      | Some rows ->
+        let rec check = function
+          | []           -> Ok false
+          | row :: rest' ->
+            let extended = extend_tuple tuple variable row in
+            match go rest extended with
+            | Ok true  -> Ok true
+            | Ok false | Error _ -> check rest'
+        in
+        check rows
+  in
+  go bindings tuple
+#+end_src
+
+The cost remains O(∏ nᵢ · C) — the n-ary form does not change the complexity,
+but it makes the binding structure explicit and opens the door to reordering
+optimisations (e.g., evaluate the smallest relation first).
+
+* Performance Inventory
+
+The following is a precise account of known costs and inefficiencies, intended
+as a reference for future optimisation work.
+
+** Eager Full Materialisation of Quantifier Relations
+
+~iterate_finite~ loads every tuple in the quantifier relation from storage before
+the first body evaluation begins. For a ~Forall~ whose first body call returns
+~Ok false~, all subsequent tuples were loaded needlessly. A streaming/lazy
+iterator would allow early termination before full materialisation.
+
+** Linear Scan in ~check_membership~
+
+Every ~MemberOf~ check performs a full linear scan over all tuple hashes in the
+target relation's Merkle tree. There are no secondary indexes. For a relation of
+cardinality /n/:
+
+- /n/ calls to ~Storage.load_raw~ to fetch stored tuples.
+- For each tuple, up to /a/ additional ~Storage.load_raw~ calls to fetch
+  attribute values.
+- Comparison via structural equality (~Stdlib.(=)~) on unmarshalled ~Obj.t~ values.
+
+An index mapping ~(relation_name, attr_name, value_hash)~ to tuple hashes would
+reduce this to O(log n) or O(1) per ~MemberOf~ check.
+
+** AttributeMap Allocation per ~extend_tuple~ Call
+
+~extend_tuple~ allocates a new ~AttributeMap~ on every invocation by folding over
+the row into the existing map. For nested quantifiers of cardinalities
+/n₁ × n₂ × ... × nq/, this allocates ∏ nᵢ maps during a single constraint check.
+A persistent/functional map amortises this somewhat (structural sharing), but
+each call still produces a new root node.
+
+A flat association list or array, indexed by a fixed schema, would be cheaper
+for extend and lookup at the cost of schema rigidity.
+
+** Redundant Storage Loads Across Constraints
+
+The ~eval_context~ is built once per ~create_tuple~ call, but it is not a cache —
+every ~check_membership~ and ~iterate_finite~ call re-reads from storage. If a
+relation is referenced in multiple constraints or multiple ~MemberOf~ nodes within
+one constraint tree, its tuples are loaded multiple times.
+
+A constraint-session cache (a ~Hashtbl~ from relation_name to materialised rows,
+populated lazily on first access) would eliminate redundant loads within a single
+tuple insertion.
+
+** No Short-Circuit Across Named Constraints
+
+~evaluate_named~ evaluates every constraint in the named list, collecting all
+failures before returning:
+
+#+begin_src ocaml
+let failures =
+  List.filter_map
+    (fun (name, c) ->
+      match evaluate ctx tuple c with
+      | Ok true  -> None
+      | Ok false -> Some (name, ...)
+      | Error d  -> Some (name, d))
+    named
+in
+#+end_src
+
+For a tuple that violates the first constraint, all remaining constraints are
+still evaluated at full cost. Short-circuiting on first failure is correct when
+complete diagnostics are not required (e.g., interactive insertion). A lazy stream
+of failures, computed on demand, would support both use cases.
+
+** Cartesian Product Complexity of Nested Quantifiers
+
+For /q/ nested ~Exists~/~Forall~ quantifiers over relations of cardinalities
+/n₁, n₂, ..., nq/ with body cost /C/:
+
+  Worst-case body evaluations = n₁ × n₂ × ... × nq
+
+  Worst-case storage loads = (∑ nᵢ · kᵢ) + n₁ · n₂ · ... · nq · C_membership
+
+Where /kᵢ/ is the attribute count of relation /i/ and /C_membership/ is the cost
+of ~check_membership~ on the body's target relation.
+
+Mitigations:
+- *Evaluate smallest relation first* (selectivity-based reordering): reduces the
+  Cartesian product by pruning earlier.
+- *Push ~MemberOf~ filters into the iteration*: instead of iterating all rows of
+  the quantifier relation and then checking membership, filter the quantifier rows
+  during iteration using the same index that would accelerate ~check_membership~.
+- *Semi-join reduction*: for FK-style constraints, a single hash lookup suffices
+  and no Cartesian product is needed.
+
+* Summary of Call Chain for a Single Tuple Insertion
+
+#+begin_example
+create_tuple
+  └── build_eval_context (storage, db)            [once per insertion]
+  └── evaluate_named ctx tuple named_constraints  [once per insertion]
+        └── evaluate ctx tuple c                  [once per named constraint]
+              ├── Exists / Forall
+              │     └── iterate_finite quantifier  [materialises full relation]
+              │           ├── Merkle.keys tree
+              │           └── Storage.load_raw × (n × k)
+              │     └── for each row:
+              │           ├── extend_tuple          [allocates new AttributeMap]
+              │           └── evaluate ctx extended_tuple body
+              │                 └── MemberOf
+              │                       ├── bind      [resolves Vars from extended tuple]
+              │                       └── check_membership target bound_values
+              │                             ├── Merkle.keys tree
+              │                             └── Storage.load_raw × (n' × (1 + a))
+              └── And / Or / Not
+                    └── evaluate (recursive)
+#+end_example
diff --git a/docs/n-way-binding.org b/docs/n-way-binding.org
new file mode 100644
index 0000000..39c9d65
--- /dev/null
+++ b/docs/n-way-binding.org
@@ -0,0 +1,206 @@
+#+TITLE: N-Way Binding in DCL Constraints
+#+DATE: 2026-03-11
+
+* Overview
+
+The DCL constraint language supports quantified membership checks via ~Exists~ and ~Forall~.
+This document illustrates the hotel/building/room/suite example to motivate n-ary quantification
+and show how 3-wise (and deeper) relational composition is expressed.
+
+* DML — Schema
+
+#+begin_src lisp
+(CreateRelation
+  (name "Building")
+  (schema
+    ((building_id "integer")
+     (building_name "string")
+     (floors "integer"))))
+
+(CreateRelation
+  (name "Room")
+  (schema
+    ((room_id "integer")
+     (building_id "integer")
+     (floor "integer")
+     (room_number "string"))))
+
+(CreateRelation
+  (name "Suite")
+  (schema
+    ((suite_id "integer")
+     (room_id "integer")
+     (suite_name "string")
+     (capacity "integer"))))
+#+end_src
+
+* DML — Data
+
+Tower B has only 2 floors, which is what causes the ~suite_in_tall_building~ constraint
+to fire when suites referencing its rooms are inserted.
+
+#+begin_src lisp
+(InsertTuple
+  (relation "Building")
+  (attributes
+    ((building_id (Int 1))
+     (building_name (Str "Tower A"))
+     (floors (Int 10)))))
+
+(InsertTuple
+  (relation "Building")
+  (attributes
+    ((building_id (Int 2))
+     (building_name (Str "Tower B"))
+     (floors (Int 2)))))   ;; ≤ 3 — suites in rooms here will be rejected
+
+(InsertTuples
+  (relation "Room")
+  (tuples
+    (((room_id (Int 101)) (building_id (Int 1)) (floor (Int 1)) (room_number (Str "1A")))
+     ((room_id (Int 102)) (building_id (Int 1)) (floor (Int 2)) (room_number (Str "2A")))
+     ((room_id (Int 201)) (building_id (Int 2)) (floor (Int 1)) (room_number (Str "1B"))))))
+
+;; Suites 1001 and 1002 reference room 101 (Tower A, 10 floors) — accepted.
+;; Suite 1002 references room 102 (Tower A, 10 floors) — accepted.
+;; Suite 1003 references room 201 (Tower B, 2 floors) — rejected by suite_in_tall_building.
+(InsertTuples
+  (relation "Suite")
+  (tuples
+    (((suite_id (Int 1001)) (room_id (Int 101)) (suite_name (Str "Presidential")) (capacity (Int 4)))
+     ((suite_id (Int 1002)) (room_id (Int 101)) (suite_name (Str "Standard"))     (capacity (Int 2)))
+     ((suite_id (Int 1003)) (room_id (Int 102)) (suite_name (Str "Deluxe"))       (capacity (Int 3))))))
+#+end_src
+
+* DCL — Constraints
+
+Binary FK constraints compose to enforce referential integrity along the chain
+~Suite → Room → Building~. Each link is declared independently.
+
+#+begin_src lisp
+;; FK: every Room must belong to an existing Building
+(RegisterConstraint
+  (constraint_name "fk_room_building")
+  (relation_name "Room")
+  (body (MemberOf
+    (target "Building")
+    (binding ((building_id (Var "building_id")))))))
+
+;; FK: every Suite must belong to an existing Room
+(RegisterConstraint
+  (constraint_name "fk_suite_room")
+  (relation_name "Suite")
+  (body (MemberOf
+    (target "Room")
+    (binding ((room_id (Var "room_id")))))))
+#+end_src
+
+* DRL — Queries
+
+The 3-wise join is expressed by composing binary joins. No special n-ary syntax is needed
+in DRL — the relational model handles this naturally through join composition.
+
+#+begin_src lisp
+;; All suites with their room and building — full 3-way join
+(Join
+  (room_id)
+  (Base "Suite")
+  (Join
+    (building_id)
+    (Base "Room")
+    (Base "Building")))
+
+;; Suites in Building 1 only
+(Select
+  (Const ((building_id (Int 1))))
+  (Join
+    (room_id)
+    (Base "Suite")
+    (Join
+      (building_id)
+      (Base "Room")
+      (Base "Building"))))
+
+;; Just suite names and the building they ultimately belong to
+(Project
+  (suite_name building_name)
+  (Join
+    (room_id)
+    (Base "Suite")
+    (Join
+      (building_id)
+      (Base "Room")
+      (Base "Building"))))
+#+end_src
+
+* Motivation for N-Ary ~Exists~
+
+The binary FK constraints above can be decomposed into independent ~MemberOf~ checks.
+However, some constraints require joining through intermediate variables before a
+membership check can be made. These cannot be decomposed.
+
+Example: /a suite is only valid if its room belongs to a building with more than 3 floors/.
+The chain ~suite.room_id → room.building_id → building.floors~ requires two intermediate
+variables — it is inherently a 3-wise constraint.
+
+Each ~Exists~ record field must be wrapped by name when written in s-expression form, as
+required by ~[@@deriving sexp]~. The ~body~ field of the inner ~Exists~ must be written
+explicitly as ~(body ...)~, not passed positionally.
+
+#+begin_src lisp
+(RegisterConstraint
+  (constraint_name "suite_in_tall_building")
+  (relation_name "Suite")
+  (body
+    (Exists (variable "r") (quantifier "Room")
+      (body
+        (Exists (variable "b") (quantifier "Building")
+          (body
+            (And
+              ((MemberOf (target "Room")
+                 (binding ((room_id (Var "room_id")))))
+               (MemberOf (target "Building")
+                 (binding ((building_id (Var "r.building_id")))))
+               (MemberOf (target "greater_than_natural")
+                 (binding ((left (Var "b.floors")) (right (Const (Int 3)))))))))))))
+#+end_src
+
+With the current single-binding ~Exists~, this requires nesting. With the proposed n-ary form,
+it becomes flat and the quantifier chain is explicit:
+
+#+begin_src lisp
+;; Proposed n-ary Exists (not yet implemented)
+(RegisterConstraint
+  (constraint_name "suite_in_tall_building")
+  (relation_name "Suite")
+  (body
+    (Exists
+      (bindings ((r "Room") (b "Building")))
+      (body
+        (And
+          ((MemberOf (target "Room")
+             (binding ((room_id (Var "room_id")))))
+           (MemberOf (target "Building")
+             (binding ((building_id (Var "r.building_id")))))
+           (MemberOf (target "greater_than_natural")
+             (binding ((left (Var "b.floors")) (right (Const (Int 3))))))))))))
+#+end_src
+
+* Namespacing
+
+Attributes from quantifier rows are namespaced by the variable name in ~extend_tuple~,
+so that same-named attributes from different scopes do not overwrite each other.
+~Var "attr"~ without a namespace refers to the tuple being checked (the relation the
+constraint is registered on). ~Var "x.attr"~ refers to attribute ~attr~ from the row
+bound to variable ~x~.
+
+| Expression              | Resolves to                                   |
+|-------------------------+-----------------------------------------------|
+| ~(Var "room_id")~       | ~suite.room_id~ (the incoming tuple)          |
+| ~(Var "r.building_id")~ | ~building_id~ from the ~r~ (Room) quantifier  |
+| ~(Var "b.floors")~      | ~floors~ from the ~b~ (Building) quantifier   |
+
+Without namespacing, ~extend_tuple~ would overwrite the incoming tuple's attributes
+with same-named attributes from the quantifier row, silently making ~Var~ resolve to
+the wrong scope. See ~lib/constraint.ml~ and ~docs/dcl-quantification.org~ for a full
+account of this failure mode and the provenance TODO.
diff --git a/lib/constraint.ml b/lib/constraint.ml
index 42f8f88..0ba7d4f 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -240,17 +240,37 @@ and evaluate_or ctx tuple = function
     | Error _ -> evaluate_or ctx tuple rest)
 
 and extend_tuple (tuple : Tuple.materialized)
-    (_variable : attr_name)
+    (variable : attr_name)
     (row : (attr_name * Conventions.AbstractValue.t) list)
     : Tuple.materialized =
+  (* TODO: Provenance for tuples at the relation level.
+     Attributes from quantifier rows are namespaced by the variable name
+     (e.g. "d.dept_id") to avoid silent overwriting of same-named attributes
+     from the base tuple or other quantifiers. Without namespacing, the
+     following FK constraint silently passes for an invalid insertion:
+       - Employee { emp_id=1, dept_id=99 } is being inserted.
+       - Constraint: Exists d in Department, MemberOf Department (dept_id = Var "dept_id").
+       - Department contains only { dept_id=1, dept_name="Engineering" }.
+       - extend_tuple overwrites dept_id=99 with dept_id=1 from the Department row.
+       - Var "dept_id" resolves to 1, check_membership succeeds trivially.
+       - The insertion is accepted even though dept_id=99 does not exist.
+     Namespacing is a syntactic encoding of provenance: the variable prefix
+     records which quantifier scope each value came from. A more principled
+     solution would attach provenance metadata directly to each attribute in
+     the relation, making the origin of every value explicit and queryable
+     without relying on name conventions. This would also eliminate the
+     ambiguity that arises when two quantifiers range over relations sharing
+     attribute names — currently resolved by namespacing, but ideally enforced
+     structurally by the type system or relation schema. *)
   let extra_attrs =
     List.fold_left
       (fun acc (k, v) ->
-        Tuple.AttributeMap.add k { Attribute.value = v } acc)
+        Tuple.AttributeMap.add (variable ^ "." ^ k) { Attribute.value = v } acc)
       tuple.attributes row
   in
   { tuple with attributes = extra_attrs }
 
+(* TODO: Sometimes it's more efficient and sufficient to simply halt at the first constraint violated. However, it's also important to be able to adjudicate which constraints failed on the tuple materialization. For that reason, we should likely return a lazy stream that computes the constraints on demand. *)
 let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
     (named : (string * t) list) : (bool, diagnostic) result =
   let failures =