constraints

9 files changed, 2417 insertions, 61 deletions

diff --git a/docs/constraints.org b/docs/constraints.org
new file mode 100644
index 0000000..9f866fa
--- /dev/null
+++ b/docs/constraints.org
@@ -0,0 +1,403 @@
+#+TITLE: Constraints and Membership Criteria
+
+* Conceptual Foundation
+
+A relation's *intension* is its meaning: what the relation represents
+in the conceptual model. Where the extension is the set of tuples
+currently admitted, the intension declares which tuples /could/ be
+admitted. Constraints are the formal mechanism by which a relation's
+intension narrows the infinite space of possible tuples to only those
+consistent with the conceptual model.
+
+Because Sakura models everything as a relation, constraints are
+themselves relations. Checking a constraint is checking membership in
+a constraint-relation. When a DML operation (insert/delete)
+manipulates a relation, it verifies that the manipulated data
+satisfies membership in all attached constraint-relations before
+committing the change.
+
+** Membership Criteria vs. Constraints
+
+Sakura distinguishes two levels of admission control:
+
+- *Membership criteria* (=membership_criteria : Tuple.t -> bool=) is
+  the opaque predicate baked into every relation. For stored relations
+  it validates schema/domain conformance. For ephemeral relations
+  (less_than, plus, etc.) it /is/ the intensional definition --- the
+  rule that characterizes the relation rather than an enumeration of
+  members.
+
+- *Constraints* (=Constraint.t=) are declarative, inspectable
+  structures attached to a relation via its =constraints= field. They
+  are evaluated at DML time against the current database snapshot and
+  produce structured diagnostics on failure.
+
+Membership criteria are checked first. If the tuple passes, the
+constraint list is evaluated.
+
+** Negation and Closed-World Reasoning
+
+The =Not= constructor requires an explicit universe relation name.
+This forces closed-world reasoning: negation is only meaningful
+relative to a known domain. Without a declared universe, =NOT P=
+would vacuously hold for anything outside the domain of discourse.
+
+At runtime the universe annotation is declarative --- it is not
+checked as a tuple-existence predicate, because the tuple being
+validated has not been stored yet. The evaluator simply negates the
+body and treats any =MembershipFailed= diagnostic from the body as
+successful negation.
+
+** Cardinality Awareness
+
+Constraints can narrow cardinality. A =Forall= over a finite
+quantifier relation, or a range restriction via comparison relations,
+constrains an otherwise infinite domain to a finite subset. The
+=ConstrainedFinite= variant of =Conventions.Cardinality.t= tags
+relations known to be finite due to constraints but whose exact count
+is not computed.
+
+* Constraint Language
+
+The constraint language is a small first-order logic over relation
+membership:
+
+#+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
+
+** MemberOf
+
+The atomic constraint. It checks whether the tuple, after binding
+resolution, is a member of the target relation.
+
+#+begin_src ocaml
+MemberOf { target = "orders"; binding = BindingMap.singleton "order_id" (Var "order_id") }
+#+end_src
+
+This says: "the value of =order_id= in the current tuple must appear
+as =order_id= in some tuple of the =orders= relation." This is a
+foreign key constraint.
+
+Everything is a relation --- domains, comparison relations, user
+relations. =MemberOf= resolves them uniformly from the database.
+
+** Bindings
+
+Bindings map target attribute names to expressions:
+
+#+begin_src ocaml
+type binding_expr =
+  | Var of attr_name          (* resolve from current tuple *)
+  | Const of AbstractValue.t  (* literal value *)
+#+end_src
+
+A binding like ={ "left" -> Var "age"; "right" -> Const 18 }= applied
+to a tuple with =age=25= produces the pairs
+=[("left", 25); ("right", 18)]=, which are then checked for
+membership in the target relation (e.g., =greater_than_or_equal=).
+
+** Logical Connectives
+
+- =And cs=: All sub-constraints must hold. Short-circuits on first failure.
+- =Or cs=: At least one must hold. Short-circuits on first success.
+- =Not { body; universe }=: The body must /not/ hold. The universe
+  declares the domain of negation for logical soundness.
+
+** Quantifiers
+
+- =Exists { variable; quantifier; body }=: There exists a tuple in
+  the quantifier relation such that, when bound to =variable=, the
+  body holds. The quantifier must be a finite relation.
+- =Forall { variable; quantifier; body }=: For all tuples in the
+  quantifier relation, the body holds. Also requires finiteness.
+
+Quantifiers bind values from the quantifier relation into the tuple's
+attribute map, extending the scope for the body evaluation.
+
+* Comparison Shorthands
+
+Because comparisons are relations, comparison constraints are
+=MemberOf= with the appropriate relation name and binding. Shorthand
+constructors eliminate boilerplate:
+
+#+begin_src ocaml
+Constraint.lt  ~left:(Var "age") ~right:(Const (Obj.repr 65))
+(* equivalent to:
+   MemberOf { target = "less_than";
+              binding = { "left" -> Var "age"; "right" -> Const 65 } } *)
+
+Constraint.between ~value:(Var "score") ~low:(Const 0) ~high:(Const 100)
+(* And [ gte score 0; lte score 100 ] *)
+#+end_src
+
+Available shorthands: =lt=, =lte=, =gt=, =gte=, =eq=, =neq=, =between=.
+
+* Comparison and Arithmetic Relations
+
+The prelude registers domain-parameterized comparison relations. Each
+takes a domain's =compare= function and a predicate over the compare
+result:
+
+| Relation name         | Schema         | Predicate       |
+|-----------------------+----------------+-----------------|
+| =less_than=           | (left, right)  | =compare < 0=   |
+| =less_than_or_equal=  | (left, right)  | =compare <= 0=  |
+| =greater_than=        | (left, right)  | =compare > 0=   |
+| =greater_than_or_equal= | (left, right) | =compare >= 0= |
+| =equal=               | (left, right)  | =compare = 0=   |
+| =not_equal=           | (left, right)  | =compare <> 0=  |
+
+Arithmetic relations follow the same pattern with richer schemas:
+
+| Relation     | Schema                          | Invariant             |
+|--------------+---------------------------------+-----------------------|
+| =plus=       | (a, b, sum)                     | =a + b = sum=         |
+| =times=      | (a, b, product)                 | =a * b = product=     |
+| =minus=      | (a, b, difference)              | =a - b = difference=  |
+| =divide=     | (a, b, quotient, remainder)     | =a = b*q + r, 0<=r<b= |
+
+All are ephemeral (generator-based, infinite). They serve as the
+vocabulary for constraint expressions.
+
+* Domain Compare
+
+Each =Domain.t= now carries a =compare= field:
+
+#+begin_src ocaml
+type t = {
+  name : Name.t;
+  generator : Generator.t;
+  membership_criteria : Tuple.t -> bool;
+  cardinality : Cardinality.t;
+  compare : AbstractValue.t -> AbstractValue.t -> int;
+}
+#+end_src
+
+The =compare= function dispatches comparison for values of that
+domain. The comparison relations use domain comparators rather than
+spreading =Obj.magic= casts at each call site. The four prelude
+domains define their comparators:
+
+- =integer=, =natural=: integer comparison
+- =rational=: float comparison
+- =string=: lexicographic comparison
+
+* Evaluation Engine
+
+** Eval Context
+
+The evaluator cannot depend on =Relation.t=, =Database.t=, or
+=Manipulation= (they compile later). Instead it receives a callback
+record:
+
+#+begin_src ocaml
+type eval_context = {
+  check_membership :
+    relation_name ->
+    (attr_name * AbstractValue.t) list ->
+    bool;
+  iterate_finite :
+    relation_name ->
+    (attr_name * AbstractValue.t) list list option;
+}
+#+end_src
+
+Both callbacks are closed over a specific =(storage, db)= pair at
+construction time. The =db= is a =Management.Database.t= representing
+one exact version (one hash). All relation lookups resolve against
+that snapshot only. This is critical: constraint evaluation sees a
+consistent view of the database, never a partially-mutated state.
+
+** How =check_membership= Works
+
+For a stored relation, =check_membership= loads every tuple from the
+Merkle tree and checks whether any tuple's attributes match the bound
+pairs. For an ephemeral relation (no tree), it delegates to
+=membership_criteria=.
+
+This distinction matters for foreign key constraints. A FK like
+"order_items.order_id must exist in orders" requires checking actual
+tuple existence in the =orders= relation, not just schema
+conformance.
+
+** Evaluation Rules
+
+| Constructor | Rule                                                        |
+|-------------+-------------------------------------------------------------|
+| =MemberOf=  | Bind variables from tuple, call =check_membership=          |
+| =Not=       | Negate body. =MembershipFailed= from body counts as success |
+| =And=       | All must hold (short-circuit on first failure)              |
+| =Or=        | Any must hold (short-circuit on first success)              |
+| =Exists=    | Iterate quantifier, bind each row, true if any body holds   |
+| =Forall=    | Iterate quantifier, bind each row, true only if all hold    |
+
+Quantifiers require finite quantifier relations (=iterate_finite=
+returns =Some rows=). An infinite quantifier produces
+=UnboundedQuantifier= diagnostic.
+
+** Diagnostics
+
+Failures produce structured diagnostics rather than opaque booleans:
+
+#+begin_src ocaml
+type diagnostic =
+  | MembershipFailed of { target : string; bound_values : ... }
+  | RelationNotFound of string
+  | UnboundedQuantifier of { variable; quantifier }
+  | ConstraintFailures of (string * diagnostic) list
+#+end_src
+
+Named constraint evaluation collects all failures into
+=ConstraintFailures=, giving the caller a complete picture of which
+constraints were violated and why.
+
+* Enforcement in Manipulation
+
+Constraints are enforced in =Manipulation.create_tuple=. The sequence is:
+
+1. Check =membership_criteria= (schema/domain validation)
+2. If the relation has constraints, build an =eval_context= from the
+   current =(storage, db)= pair
+3. Evaluate each named constraint against the tuple
+4. On any failure, return =ConstraintViolation= with diagnostic details
+5. On success, proceed to hash, store, and persist
+
+The =eval_context= is built fresh for each =create_tuple= call with
+the /current/ database state. This ensures FK lookups see recently
+inserted tuples, not a stale snapshot from constraint registration
+time.
+
+** Registering Constraints
+
+=register_constraint= performs two actions:
+
+1. Attaches the constraint body to the relation via
+   =update_relation_constraints=, which merges new constraints with
+   any existing ones
+2. Records the constraint name and relation in the =sakura:constraint=
+   catalog relation
+
+The constraint body is stored in the =Relation.t= object's
+=constraints= field, not separately. This means the constraint
+travels with the relation through algebraic operations.
+
+* Propagation Through Algebra
+
+When algebraic operations derive new relations, constraints propagate
+according to rules that preserve soundness:
+
+| Operation | Propagation rule                                    |
+|-----------+-----------------------------------------------------|
+| Select    | Preserve all source constraints                     |
+| Project   | Filter: keep only constraints whose variables are   |
+|           | all within the projected attributes                 |
+| Rename    | Apply variable renaming to constraint references    |
+| Equijoin  | Merge constraints from both input relations         |
+| Union     | Drop all constraints (conservative: constraints     |
+|           | only hold if both inputs agree)                     |
+| Diff      | Preserve left relation's constraints                |
+| Take      | Preserve source constraints                         |
+
+The =filter_by_attrs=, =rename_vars=, and =merge= utility functions
+on =Constraint.t= implement these transformations.
+
+** Example: Project Filtering
+
+Given a relation =R(x, y)= with constraint "=x < 100=", projecting
+to =[y]= drops the constraint because =x= is no longer in scope.
+Projecting to =[x]= or =[x, y]= preserves it.
+
+#+begin_src ocaml
+Constraint.filter_by_attrs ["y"] (Constraint.lt ~left:(Var "x") ~right:(Const 100))
+(* => None — dropped because "x" not in ["y"] *)
+
+Constraint.filter_by_attrs ["x"] (Constraint.lt ~left:(Var "x") ~right:(Const 100))
+(* => Some (lt ...) — preserved *)
+#+end_src
+
+* Utility Functions
+
+=Constraint.t= provides introspection and transformation utilities:
+
+- =vars_in : t -> attr_name list= --- collect all =Var= names
+  referenced in a constraint, recursively through all sub-expressions.
+
+- =rename_vars : (attr_name * attr_name) list -> t -> t= --- rename
+  variable references throughout a constraint tree. Used by the rename
+  algebra operator.
+
+- =filter_by_attrs : attr_name list -> t -> t option= --- returns
+  =None= if the constraint references any variable not in the given
+  set. Used by projection to drop inapplicable constraints. For =Or=,
+  all branches must survive (dropping a branch changes semantics).
+
+- =merge : (string * t) list -> (string * t) list -> (string * t) list=
+  --- AND-merge two named constraint lists. Constraints sharing a name
+  are combined with =And=. Used by equijoin.
+
+* Examples
+
+** Foreign Key
+
+#+begin_src ocaml
+(* order_items.order_id must reference an existing order *)
+let fk =
+  Constraint.MemberOf {
+    target = "orders";
+    binding = Constraint.BindingMap.singleton "order_id" (Var "order_id")
+  }
+in
+register_constraint storage db
+  ~constraint_name:"fk_order"
+  ~relation_name:"order_items"
+  ~body:fk
+#+end_src
+
+Inserting an order_item with =order_id=999= when no such order exists
+produces =ConstraintViolation "constraint fk_order violated"=.
+
+** Mutual Exclusion
+
+#+begin_src ocaml
+(* A ticket cannot be both open and closed *)
+let not_closed =
+  Constraint.Not {
+    body = Constraint.MemberOf {
+      target = "closed_ticket";
+      binding = Constraint.BindingMap.singleton "ticket_id" (Var "ticket_id")
+    };
+    universe = "open_ticket"
+  }
+in
+register_constraint storage db
+  ~constraint_name:"not_closed"
+  ~relation_name:"open_ticket"
+  ~body:not_closed
+#+end_src
+
+** Self-Reference Inequality
+
+#+begin_src ocaml
+(* An employee cannot manage themselves *)
+let neq = Constraint.neq ~left:(Var "emp_id") ~right:(Var "mgr_id") in
+register_constraint storage db
+  ~constraint_name:"no_self_manage"
+  ~relation_name:"reports_to"
+  ~body:neq
+#+end_src
+
+This uses the =not_equal= comparison relation: it checks membership
+in ={(left, right) | left <> right}=.
+
+* References
+
+- Codd, E. F. (1979), "Extending the Database Relational Model to Capture More Meaning"
+- Date, C. J. and Darwen, H. (2006), "The Third Manifesto"
+- McGoveran, D. (1994), "The Semantic Relational Data Model"
diff --git a/lib/algebra.ml b/lib/algebra.ml
index 8701dcb..f03aa53 100644
--- a/lib/algebra.ml
+++ b/lib/algebra.ml
@@ -29,10 +29,15 @@ module Make(Storage : Management.Physical.S) = struct
        | Error _ -> (fun _pos -> Generator.Error ("Failed to load: " ^ rel.Relation.name))
        | Ok ts -> list_generator (List.map (fun t -> Tuple.Materialized t) ts))
 
-  let of_generator ~name ~schema gen =
+  let of_generator ~name ~schema ?constraints ?cardinality gen =
+    let cardinality =
+      match cardinality with
+      | Some c -> c
+      | None -> Conventions.Cardinality.AlephZero
+    in
     Relation.make
-      ~hash:None ~name ~schema ~tree:None ~constraints:None
-      ~cardinality:Conventions.Cardinality.AlephZero
+      ~hash:None ~name ~schema ~tree:None ~constraints
+      ~cardinality
       ~generator:(Some gen)
       ~membership_criteria:(fun _ -> true)
       ~provenance:Relation.Provenance.Undefined
@@ -61,7 +66,8 @@ module Make(Storage : Management.Physical.S) = struct
           else go next (Option.map ((+) 1) pos)
       in fun pos -> go gen pos
     in
-    Ok (of_generator ~name:("σ_" ^ rel.Relation.name) ~schema:rel.Relation.schema lazy_gen)
+    Ok (of_generator ~name:("σ_" ^ rel.Relation.name) ~schema:rel.Relation.schema
+           ?constraints:rel.Relation.constraints lazy_gen)
 
   let project storage (attrs : string list) rel =
     let gen = to_generator storage rel in
@@ -83,7 +89,22 @@ module Make(Storage : Management.Physical.S) = struct
         | Generator.Value (t, next) -> Generator.Value (project_tuple t, go next)
       in fun pos -> go gen pos
     in
-    Ok (of_generator ~name:("π_" ^ rel.Relation.name) ~schema:new_schema lazy_gen)
+    let filtered_constraints =
+      match rel.Relation.constraints with
+      | None | Some [] -> None
+      | Some cs ->
+        let kept =
+          List.filter_map
+            (fun (name, c) ->
+              match Constraint.filter_by_attrs attrs c with
+              | Some c' -> Some (name, c')
+              | None -> None)
+            cs
+        in
+        (match kept with [] -> None | _ -> Some kept)
+    in
+    Ok (of_generator ~name:("π_" ^ rel.Relation.name) ~schema:new_schema
+           ?constraints:filtered_constraints lazy_gen)
 
   let rename storage (renames : (string * string) list) rel =
     let rename_key k = match List.assoc_opt k renames with Some k' -> k' | None -> k in
@@ -104,7 +125,17 @@ module Make(Storage : Management.Physical.S) = struct
         | Generator.Value (t, next) -> Generator.Value (rename_tuple t, go next)
       in fun pos -> go gen pos
     in
-    Ok (of_generator ~name:("ρ_" ^ rel.Relation.name) ~schema:new_schema lazy_gen)
+    let renamed_constraints =
+      match rel.Relation.constraints with
+      | None | Some [] -> None
+      | Some cs ->
+        Some
+          (List.map
+             (fun (name, c) -> (name, Constraint.rename_vars renames c))
+             cs)
+    in
+    Ok (of_generator ~name:("ρ_" ^ rel.Relation.name) ~schema:new_schema
+           ?constraints:renamed_constraints lazy_gen)
 
   let equijoin storage (attrs : string list) left right =
     let right_gen = to_generator storage right in
@@ -155,8 +186,15 @@ module Make(Storage : Management.Physical.S) = struct
         in
         from_left left_gen 0
       in
+      let merged_constraints =
+        match left.Relation.constraints, right.Relation.constraints with
+        | None, None -> None
+        | Some cs, None | None, Some cs -> Some cs
+        | Some cs1, Some cs2 -> Some (Constraint.merge cs1 cs2)
+      in
       let name = "⋈_" ^ left.Relation.name ^ "_" ^ right.Relation.name in
-      Ok (of_generator ~name ~schema:merged_schema join_gen)
+      Ok (of_generator ~name ~schema:merged_schema
+             ?constraints:merged_constraints join_gen)
 
   let union storage rel1 rel2 =
     let gen1 = to_generator storage rel1 in
@@ -170,6 +208,7 @@ module Make(Storage : Management.Physical.S) = struct
       in fun pos -> go gen1 gen2 pos
     in
     let name = "∪_" ^ rel1.Relation.name ^ "_" ^ rel2.Relation.name in
+    (* Conservative: drop constraints since they only hold if both inputs agree *)
     Ok (of_generator ~name ~schema:rel1.Relation.schema chain_gen)
 
   let attrs_equal
@@ -203,7 +242,8 @@ module Make(Storage : Management.Physical.S) = struct
         in fun pos -> go left_gen pos
       in
       let name = "−_" ^ rel1.Relation.name ^ "_" ^ rel2.Relation.name in
-      Ok (of_generator ~name ~schema:rel1.Relation.schema lazy_gen)
+      Ok (of_generator ~name ~schema:rel1.Relation.schema
+             ?constraints:rel1.Relation.constraints lazy_gen)
 
   let take storage n rel =
     let gen = to_generator storage rel in
@@ -216,7 +256,9 @@ module Make(Storage : Management.Physical.S) = struct
           | Generator.Value (t, next) -> Generator.Value (t, go next (count - 1))
       in fun pos -> go gen n pos
     in
-    Ok (of_generator ~name:("τ_" ^ rel.Relation.name) ~schema:rel.Relation.schema lazy_gen)
+    Ok (of_generator ~name:("τ_" ^ rel.Relation.name) ~schema:rel.Relation.schema
+           ?constraints:rel.Relation.constraints
+           ~cardinality:(Conventions.Cardinality.Finite n) lazy_gen)
 
   let materialize storage rel : (Tuple.materialized list, error) Result.t =
     match drain (to_generator storage rel) with
diff --git a/lib/constraint.ml b/lib/constraint.ml
index f6164b2..b7844eb 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -1,8 +1,376 @@
+(** Constraint system for relational membership criteria.
+
+    A relation's intension includes constraints that refine the space of
+    admissible tuples. Since constraints are themselves relations, checking
+    a constraint = checking membership in that constraint-relation.
+
+    Negation requires an explicit universe relation name, forcing
+    closed-world reasoning in first-order logic. *)
+
 type relation_name = string
-type t = 
-  | MemberOf of relation_name
-  | Not of t * relation_name option
+type attr_name = string
+
+(** Binding expressions resolve against a tuple's attributes *)
+type binding_expr =
+  | Var of attr_name
+  | Const of Conventions.AbstractValue.t
+
+module BindingMap = Map.Make (String)
+
+type binding = binding_expr BindingMap.t
+
+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: string; quantifier: relation_name; constraint': t}
-  | Forall of {variable: string; quantifier: relation_name; constraint': t}
+  | Exists of { variable : attr_name; quantifier : relation_name; body : t }
+  | Forall of { variable : attr_name; quantifier : relation_name; body : t }
+
+(* ============================================================================
+   Diagnostics
+   ============================================================================ *)
+
+type diagnostic =
+  | MembershipFailed of {
+      target : string;
+      bound_values : (attr_name * Conventions.AbstractValue.t) list;
+    }
+  | RelationNotFound of string
+  | UnboundedQuantifier of {
+      variable : attr_name;
+      quantifier : relation_name;
+    }
+  | ConstraintFailures of (string * diagnostic) list
+
+(* ============================================================================
+   Utility functions
+   ============================================================================ *)
+
+(** Collect all [Var] names referenced in a constraint *)
+let rec vars_in : t -> attr_name list = function
+  | MemberOf { binding; _ } ->
+    BindingMap.fold
+      (fun _ expr acc ->
+        match expr with
+        | Var v -> if List.mem v acc then acc else v :: acc
+        | Const _ -> acc)
+      binding []
+  | Not { body; _ } -> vars_in body
+  | And cs | Or cs -> List.concat_map vars_in cs |> List.sort_uniq String.compare
+  | Exists { variable; body; _ } | Forall { variable; body; _ } ->
+    let inner = vars_in body in
+    if List.mem variable inner then inner
+    else variable :: inner
+
+(** Rename [Var] references according to a rename list *)
+let rec rename_vars (renames : (attr_name * attr_name) list) : t -> t = function
+  | MemberOf { target; binding } ->
+    let binding' =
+      BindingMap.fold
+        (fun k expr acc ->
+          let k' =
+            match List.assoc_opt k renames with Some n -> n | None -> k
+          in
+          let expr' =
+            match expr with
+            | Var v -> (
+              match List.assoc_opt v renames with
+              | Some n -> Var n
+              | None -> expr)
+            | Const _ -> expr
+          in
+          BindingMap.add k' expr' acc)
+        binding BindingMap.empty
+    in
+    MemberOf { target; binding = binding' }
+  | Not { body; universe } ->
+    Not { body = rename_vars renames body; universe }
+  | And cs -> And (List.map (rename_vars renames) cs)
+  | Or cs -> Or (List.map (rename_vars renames) cs)
+  | Exists { variable; quantifier; body } ->
+    let variable' =
+      match List.assoc_opt variable renames with
+      | Some n -> n
+      | None -> variable
+    in
+    Exists
+      { variable = variable'; quantifier; body = rename_vars renames body }
+  | Forall { variable; quantifier; body } ->
+    let variable' =
+      match List.assoc_opt variable renames with
+      | Some n -> n
+      | None -> variable
+    in
+    Forall
+      { variable = variable'; quantifier; body = rename_vars renames body }
+
+(** Drop constraints referencing attributes not in the given set.
+    Returns [None] if the constraint cannot be kept. *)
+let rec filter_by_attrs (attrs : attr_name list) (c : t) : t option =
+  let all_present c =
+    List.for_all (fun v -> List.mem v attrs) (vars_in c)
+  in
+  match c with
+  | MemberOf _ -> if all_present c then Some c else None
+  | Not { body; universe } -> (
+    match filter_by_attrs attrs body with
+    | Some body' -> Some (Not { body = body'; universe })
+    | None -> None)
+  | And cs ->
+    let kept = List.filter_map (filter_by_attrs attrs) cs in
+    if kept = [] then None else Some (And kept)
+  | Or cs ->
+    (* For Or, all branches must survive *)
+    let kept = List.filter_map (filter_by_attrs attrs) cs in
+    if List.length kept = List.length cs then Some (Or kept) else None
+  | Exists { variable; quantifier; body } -> (
+    match filter_by_attrs (variable :: attrs) body with
+    | Some body' -> Some (Exists { variable; quantifier; body = body' })
+    | None -> None)
+  | Forall { variable; quantifier; body } -> (
+    match filter_by_attrs (variable :: attrs) body with
+    | Some body' -> Some (Forall { variable; quantifier; body = body' })
+    | None -> None)
+
+(** AND-merge two named constraint lists *)
+let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
+    : (string * t) list =
+  let combined = cs1 @ cs2 in
+  (* Group by name and AND-merge duplicates *)
+  let tbl = Hashtbl.create 16 in
+  List.iter
+    (fun (name, c) ->
+      match Hashtbl.find_opt tbl name with
+      | None -> Hashtbl.replace tbl name [ c ]
+      | Some cs -> Hashtbl.replace tbl name (c :: cs))
+    combined;
+  Hashtbl.fold
+    (fun name cs acc ->
+      let merged = match cs with [ c ] -> c | _ -> And cs in
+      (name, merged) :: acc)
+    tbl []
+
+(* ============================================================================
+   Smart constructors
+   ============================================================================ *)
+
+let member_of ~target ~binding = MemberOf { target; binding }
+
+let not_ ~universe body = Not { body; universe }
+
+let and_ cs =
+  match cs with
+  | [ c ] -> c
+  | _ -> And cs
+
+let or_ cs =
+  match cs with
+  | [ c ] -> c
+  | _ -> Or cs
+
+let exists ~variable ~quantifier body =
+  Exists { variable; quantifier; body }
+
+let forall ~variable ~quantifier body =
+  Forall { variable; quantifier; body }
+
+(* ============================================================================
+   Evaluation context (no dependency on Relation/Database/Manipulation)
+   ============================================================================ *)
+
+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;
+}
+
+(* ============================================================================
+   Binding resolution
+   ============================================================================ *)
+
+(** Resolve binding expressions against a materialized tuple *)
+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 []
+
+(* ============================================================================
+   Constraint evaluation
+   ============================================================================ *)
+
+(** Evaluate a constraint against a tuple in the given context.
+    Returns [Ok true] if satisfied, [Ok false] should not occur —
+    failures return [Error diagnostic]. *)
+let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
+    : (bool, diagnostic) result =
+  match c with
+  | 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 })
+  | Not { body; universe = _ } ->
+    (* The universe is a declarative annotation for closed-world reasoning.
+       At runtime, we simply negate the body. The universe ensures logical
+       soundness at the schema level, not as a runtime tuple-existence check
+       (the tuple being validated hasn't been stored yet). *)
+    (match evaluate ctx tuple body with
+     | Ok true -> Ok false
+     | Ok false -> Ok true
+     | Error (MembershipFailed _) -> Ok true
+     | Error d -> Error d)
+  | And cs -> evaluate_and ctx tuple cs
+  | Or cs -> evaluate_or ctx tuple cs
+  | 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 ->
+          (* Bind the quantifier variable into scope *)
+          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)
+  | 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)
+
+and evaluate_and ctx tuple = function
+  | [] -> Ok true
+  | c :: rest -> (
+    match evaluate ctx tuple c with
+    | Ok true -> evaluate_and ctx tuple rest
+    | Ok false -> Ok false
+    | Error d -> Error d)
+
+and evaluate_or ctx tuple = function
+  | [] -> Ok false
+  | c :: rest -> (
+    match evaluate ctx tuple c with
+    | Ok true -> Ok true
+    | Ok false -> evaluate_or ctx tuple rest
+    | Error _ -> evaluate_or ctx tuple rest)
+
+(** Extend a tuple with bindings from a quantifier row.
+    Each row entry [(attr, value)] gets added with [variable] as prefix
+    if the attr name doesn't match an existing attribute. *)
+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 k { Attribute.value = v } acc)
+      tuple.attributes row
+  in
+  { tuple with attributes = extra_attrs }
+
+(** Evaluate a list of named constraints, collecting all failures *)
+let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
+    (named : (string * t) list) : (bool, diagnostic) result =
+  let failures =
+    List.filter_map
+      (fun (name, c) ->
+        match evaluate ctx tuple c with
+        | Ok true -> None
+        | Ok false ->
+          Some (name, MembershipFailed { target = name; bound_values = [] })
+        | Error d -> Some (name, d))
+      named
+  in
+  match failures with
+  | [] -> Ok true
+  | fs -> Error (ConstraintFailures fs)
+
+(* ============================================================================
+   Comparison shorthand constructors
+   ============================================================================ *)
+
+let make_comparison_binding ~left ~right =
+  BindingMap.empty
+  |> BindingMap.add "left" left
+  |> BindingMap.add "right" right
+
+let lt ~left ~right =
+  MemberOf
+    { target = "less_than"; binding = make_comparison_binding ~left ~right }
+
+let lte ~left ~right =
+  MemberOf
+    {
+      target = "less_than_or_equal";
+      binding = make_comparison_binding ~left ~right;
+    }
+
+let gt ~left ~right =
+  MemberOf
+    {
+      target = "greater_than";
+      binding = make_comparison_binding ~left ~right;
+    }
+
+let gte ~left ~right =
+  MemberOf
+    {
+      target = "greater_than_or_equal";
+      binding = make_comparison_binding ~left ~right;
+    }
+
+let eq ~left ~right =
+  MemberOf
+    { target = "equal"; binding = make_comparison_binding ~left ~right }
+
+let neq ~left ~right =
+  MemberOf
+    { target = "not_equal"; binding = make_comparison_binding ~left ~right }
+
+let between ~value ~low ~high =
+  And
+    [
+      MemberOf
+        {
+          target = "greater_than_or_equal";
+          binding = make_comparison_binding ~left:value ~right:low;
+        };
+      MemberOf
+        {
+          target = "less_than_or_equal";
+          binding = make_comparison_binding ~left:value ~right:high;
+        };
+    ]
diff --git a/lib/conventions.ml b/lib/conventions.ml
index 538bc5c..0019447 100644
--- a/lib/conventions.ml
+++ b/lib/conventions.ml
@@ -9,7 +9,7 @@ module Name = struct
 end
 
 module Cardinality = struct
-  type t = Finite of int | AlephZero | Continuum
+  type t = Finite of int | ConstrainedFinite | AlephZero | Continuum
 end
 
 module AbstractValue = struct
diff --git a/lib/domain.ml b/lib/domain.ml
index 753a7b9..87ed1a9 100644
--- a/lib/domain.ml
+++ b/lib/domain.ml
@@ -3,7 +3,8 @@ type t = {
   generator : Generator.t;
   membership_criteria : Tuple.t -> bool;
   cardinality : Conventions.Cardinality.t;
+  compare : Conventions.AbstractValue.t -> Conventions.AbstractValue.t -> int;
 }
 
-let make ~name ~generator ~membership_criteria ~cardinality =
-  { name; generator; membership_criteria; cardinality }
+let make ~name ~generator ~membership_criteria ~cardinality ~compare =
+  { name; generator; membership_criteria; cardinality; compare }
diff --git a/lib/manipulation.ml b/lib/manipulation.ml
index e019fa8..a1d90d6 100644
--- a/lib/manipulation.ml
+++ b/lib/manipulation.ml
@@ -45,6 +45,98 @@ let build_membership_criteria _schema : (Tuple.t -> bool) =
 module Make (Storage : Management.Physical.S) = struct
   type storage = Storage.t
 
+  (* ============================================================================
+     Constraint evaluation context
+     ============================================================================ *)
+
+  (** Build an eval_context closed over a specific (storage, db) snapshot.
+      All relation lookups resolve against this exact database version. *)
+  let build_eval_context (storage : storage) (db : Management.Database.t)
+      : Constraint.eval_context =
+    let check_membership rel_name bound_pairs =
+      match Management.Database.get_relation db rel_name with
+      | None -> false
+      | Some rel ->
+        let attributes =
+          List.fold_left
+            (fun acc (k, v) ->
+              Tuple.AttributeMap.add k { Attribute.value = v } acc)
+            Tuple.AttributeMap.empty bound_pairs
+        in
+        let tuple =
+          Tuple.Materialized { Tuple.relation = rel_name; attributes }
+        in
+        if not (rel.membership_criteria tuple) then false
+        else
+          (* For stored relations, check if a matching tuple actually exists *)
+          match rel.tree with
+          | None ->
+            (* No tree = ephemeral/generator relation, membership_criteria suffices *)
+            true
+          | Some tree ->
+            let hashes = Merkle.keys tree in
+            List.exists
+              (fun h ->
+                match Storage.load_raw storage h with
+                | Error _ | Ok None -> false
+                | Ok (Some bytes) ->
+                  let stored = Storable.Tuple.of_bytes bytes in
+                  (* Check if all bound pairs match the stored tuple's attributes *)
+                  List.for_all
+                    (fun (bk, bv) ->
+                      List.exists
+                        (fun (sk, sh) ->
+                          sk = bk
+                          &&
+                          match Storage.load_raw storage sh with
+                          | Error _ | Ok None -> false
+                          | Ok (Some vbytes) ->
+                            let sv : Conventions.AbstractValue.t =
+                              Marshal.from_bytes vbytes 0
+                            in
+                            Stdlib.( = ) sv bv)
+                        stored.Storable.Tuple.attributes)
+                    bound_pairs)
+              hashes
+    in
+    let iterate_finite rel_name =
+      match Management.Database.get_relation db rel_name with
+      | None -> None
+      | Some rel -> (
+        match rel.cardinality with
+        | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> (
+          match rel.tree with
+          | None -> Some []
+          | Some tree ->
+            let hashes = Merkle.keys tree in
+            let rec load_all acc = function
+              | [] -> Some (List.rev acc)
+              | h :: rest -> (
+                match Storage.load_raw storage h with
+                | Error _ -> None
+                | Ok None -> None
+                | Ok (Some bytes) ->
+                  let stored = Storable.Tuple.of_bytes bytes in
+                  let rec load_attrs attr_acc = function
+                    | [] -> Some (List.rev attr_acc)
+                    | (name, attr_hash) :: attr_rest -> (
+                      match Storage.load_raw storage attr_hash with
+                      | Error _ | Ok None -> None
+                      | Ok (Some vbytes) ->
+                        let value : Conventions.AbstractValue.t =
+                          Marshal.from_bytes vbytes 0
+                        in
+                        load_attrs ((name, value) :: attr_acc) attr_rest)
+                  in
+                  (match load_attrs [] stored.Storable.Tuple.attributes with
+                   | None -> None
+                   | Some pairs -> load_all (pairs :: acc) rest))
+            in
+            load_all [] hashes)
+        | _ -> None)
+    in
+    { Constraint.check_membership; iterate_finite }
+
   (* State Persistence - Store relation and database states *)
 
   (** Store a relation state to storage *)
@@ -219,6 +311,25 @@ module Make (Storage : Management.Physical.S) = struct
       if not (relation.membership_criteria (Tuple.Materialized tuple)) then
         Error (ConstraintViolation "Tuple does not satisfy membership criteria")
       else
+        (* Check constraints *)
+        let constraint_ok =
+          match relation.constraints with
+          | None | Some [] -> Ok true
+          | Some named_constraints ->
+            let ctx = build_eval_context storage db in
+            Constraint.evaluate_named ctx tuple named_constraints
+        in
+        (match constraint_ok with
+         | Error (Constraint.ConstraintFailures failures) ->
+           let msg =
+             String.concat "; "
+               (List.map (fun (name, _) -> "constraint " ^ name ^ " violated")
+                  failures)
+           in
+           Error (ConstraintViolation msg)
+         | Error _ -> Error (ConstraintViolation "Constraint evaluation failed")
+         | Ok false -> Error (ConstraintViolation "Constraint not satisfied")
+         | Ok true ->
         (* Compute tuple hash *)
         let tuple_hash = Hashing.hash_tuple tuple in
 
@@ -275,7 +386,7 @@ module Make (Storage : Management.Physical.S) = struct
                | Ok () ->
                  match store_database storage new_db with
                  | Error e -> Error e
-                 | Ok () -> Ok (new_db, new_relation, tuple_hash))
+                 | Ok () -> Ok (new_db, new_relation, tuple_hash)))
 
   (** Insert multiple tuples into a relation *)
   let create_tuples
@@ -709,20 +820,83 @@ module Make (Storage : Management.Physical.S) = struct
         | Error e -> Error e
         | Ok () -> Ok (new_db, new_relation)
 
-  (** Register a named constraint on a relation in the system catalog. *)
+  (** Attach constraints to an existing relation.
+      Rebuilds membership_criteria to include constraint checking,
+      re-hashes, and persists. *)
+  let update_relation_constraints
+      (storage : storage)
+      (db : Management.Database.t)
+      ~(relation_name : string)
+      ~(constraints : Relation.RelationConstraint.t)
+    : (Management.Database.t * Relation.t) result =
+    match Management.Database.get_relation db relation_name with
+    | None -> Error (RelationNotFound relation_name)
+    | Some relation ->
+      let merged_constraints =
+        match relation.constraints with
+        | None -> constraints
+        | Some existing -> Constraint.merge existing constraints
+      in
+      (* Don't bake constraint evaluation into membership_criteria —
+         create_tuple evaluates constraints with the current db snapshot.
+         membership_criteria stays for schema/domain validation only. *)
+      let new_relation =
+        { relation with
+          constraints = Some merged_constraints;
+        }
+      in
+      (* Re-hash *)
+      let new_relation =
+        match new_relation.tree with
+        | Some tree ->
+          let h =
+            Hashing.hash_relation ~name:relation_name
+              ~schema:relation.schema ~tree
+          in
+          { new_relation with hash = Some h }
+        | None -> new_relation
+      in
+      let new_db =
+        Management.Database.update_relation db ~relation:new_relation
+      in
+      (match store_relation storage new_relation with
+       | Error e -> Error e
+       | Ok () ->
+         (match store_database storage new_db with
+          | Error e -> Error e
+          | Ok () -> Ok (new_db, new_relation)))
+
+  (** Register a named constraint on a relation.
+      Attaches the constraint body to the relation AND records it in
+      [sakura:constraint]. *)
   let register_constraint
       (storage : storage)
       (db : Management.Database.t)
       ~(constraint_name : string)
       ~(relation_name : string)
+      ~(body : Constraint.t)
     : (Management.Database.t, error) Result.t =
-    match Management.Database.get_relation db Prelude.Catalog.constraint_rel_name with
-    | None -> Ok db  (* catalog not initialized *)
-    | Some con_cat ->
-      let con_tuple = Prelude.Catalog.build_constraint_tuple constraint_name relation_name in
-      match create_tuple storage db con_cat con_tuple with
-      | Error e -> Error e
-      | Ok (new_db, _, _) -> Ok new_db
+    (* Attach constraint to the relation *)
+    (match
+       update_relation_constraints storage db ~relation_name
+         ~constraints:[ (constraint_name, body) ]
+     with
+     | Error e -> Error e
+     | Ok (db, _) ->
+       (* Record in system catalog *)
+       (match
+          Management.Database.get_relation db
+            Prelude.Catalog.constraint_rel_name
+        with
+        | None -> Ok db
+        | Some con_cat ->
+          let con_tuple =
+            Prelude.Catalog.build_constraint_tuple constraint_name
+              relation_name
+          in
+          (match create_tuple storage db con_cat con_tuple with
+           | Error e -> Error e
+           | Ok (new_db, _, _) -> Ok new_db)))
 
   (*Query Operations *)
 
diff --git a/lib/prelude/domains.ml b/lib/prelude/domains.ml
index bc1716a..29104bb 100644
--- a/lib/prelude/domains.ml
+++ b/lib/prelude/domains.ml
@@ -40,6 +40,7 @@ let integer : Domain.t =
   in
   Domain.make ~name:"integer" ~generator ~membership_criteria
     ~cardinality:Conventions.Cardinality.AlephZero
+    ~compare:(fun a b -> Stdlib.compare (Obj.magic a : int) (Obj.magic b : int))
 
 (** Natural number domain: non-negative integers (0, 1, 2, …).
     Schema: [value: natural]. *)
@@ -63,6 +64,7 @@ let natural : Domain.t =
   in
   Domain.make ~name:"natural" ~generator ~membership_criteria
     ~cardinality:Conventions.Cardinality.AlephZero
+    ~compare:(fun a b -> Stdlib.compare (Obj.magic a : int) (Obj.magic b : int))
 
 (** Rational number domain: pairs [(numerator, denominator)] where the
     denominator is never zero.  The generator enumerates all such pairs via
@@ -97,6 +99,8 @@ let rational : Domain.t =
   in
   Domain.make ~name:"rational" ~generator ~membership_criteria
     ~cardinality:Conventions.Cardinality.AlephZero
+    ~compare:(fun a b ->
+      Stdlib.compare (Obj.magic a : float) (Obj.magic b : float))
 
 (** String domain: any string value.  Not enumerable.
     Schema: [value: string]. *)
@@ -110,3 +114,5 @@ let string : Domain.t =
   in
   Domain.make ~name:"string" ~generator ~membership_criteria
     ~cardinality:Conventions.Cardinality.AlephZero
+    ~compare:(fun a b ->
+      String.compare (Obj.magic a : string) (Obj.magic b : string))
diff --git a/lib/prelude/standard.ml b/lib/prelude/standard.ml
index 5725978..aca7f93 100644
--- a/lib/prelude/standard.ml
+++ b/lib/prelude/standard.ml
@@ -1,34 +1,362 @@
-let less_than_natural: Relation.t =
-  let rec generator (position: int option): Generator.result =
-    let pair_of_nat n =
-      let nf = float_of_int n in
-      let r =
-        int_of_float (floor ((1. +. sqrt (1. +. 8. *. nf)) /. 2.))
-      in
-      let t_prev = (r * (r - 1)) / 2 in
-      let left = n - t_prev in
-      (left, r) in
-    match position with
-    | Some position -> 
-      let left, right = pair_of_nat position in
-      let attributes: Attribute.materialized Tuple.AttributeMap.t =
-        Tuple.AttributeMap.of_list [("left", Obj.magic left); ("right", Obj.magic right)]
-      in Generator.Value (Tuple.make_materialized ~relation: "less_than" ~attributes: attributes, generator)
-    | None -> Error "Cannot produce a randomly enumerated value for less_than over naturals."
-  in let membership_criteria: Tuple.t -> bool = function 
-        | Tuple.Materialized materialized -> 
-            let left = Tuple.AttributeMap.find "left" materialized.attributes
-            in let right = Tuple.AttributeMap.find "right" materialized.attributes
-            in left < right
-        | Tuple.NonMaterialized _non_materialized -> false (* TODO: Handle references later *)
-  in Relation.make
-    ~hash: None
-    ~name: "natural_natural_less_than"
-    ~schema: (Schema.empty |> Schema.add "left" "natural" |> Schema.add "right" "natural")
-    ~tree: None
-    ~constraints: None
-    ~cardinality: Conventions.Cardinality.AlephZero
-    ~generator: (Some generator)
-    ~membership_criteria: membership_criteria
-    ~provenance: (Relation.Provenance.Base "less_than")
-    ~lineage: (Relation.Lineage.Base "less_than")
\ No newline at end of file
+(** Domain-parameterized comparison and arithmetic relations.
+
+    All comparison relations use a two-attribute schema [(left, right)]
+    with both attributes in the same domain. The domain's [compare] function
+    is used for evaluation — no more spreading [Obj.magic]. *)
+
+(* ============================================================================
+   Comparison relation factory
+   ============================================================================ *)
+
+(** Build a comparison relation parameterized by domain.
+    [pred] receives the result of [Domain.compare left right]. *)
+let make_comparison ~name ~domain_name ~pred ~cardinality ~generator =
+  let schema =
+    Schema.empty |> Schema.add "left" domain_name
+    |> Schema.add "right" domain_name
+  in
+  let membership_criteria : Tuple.t -> bool = function
+    | Tuple.Materialized m -> (
+      match
+        ( Tuple.AttributeMap.find_opt "left" m.attributes,
+          Tuple.AttributeMap.find_opt "right" m.attributes )
+      with
+      | Some l, Some r ->
+        pred (Stdlib.compare l.Attribute.value r.Attribute.value)
+      | _ -> false)
+    | Tuple.NonMaterialized _ -> false
+  in
+  Relation.make ~hash:None ~name ~schema ~tree:None ~constraints:None
+    ~cardinality ~generator:(Some generator) ~membership_criteria
+    ~provenance:(Relation.Provenance.Base name)
+    ~lineage:(Relation.Lineage.Base name)
+
+(* ============================================================================
+   Pair enumeration for comparison generators
+   ============================================================================ *)
+
+(** Enumerate pairs (a, b) from naturals where a < b.
+    Uses triangular indexing: position n maps to row r, column c
+    where a = c, b = r, and a < b. *)
+let pair_of_nat_lt n =
+  let nf = float_of_int n in
+  let r = int_of_float (floor ((1. +. sqrt (1. +. 8. *. nf)) /. 2.)) in
+  let t_prev = (r * (r - 1)) / 2 in
+  let left = n - t_prev in
+  (left, r)
+
+(** Enumerate all pairs (a, b) from naturals via Cantor pairing. *)
+let cantor_pair_of_nat n =
+  let w =
+    int_of_float (floor ((sqrt (float_of_int (8 * n + 1)) -. 1.) /. 2.))
+  in
+  let t = (w * (w + 1)) / 2 in
+  let b = n - t in
+  let a = w - b in
+  (a, b)
+
+(* ============================================================================
+   Concrete comparison relations (natural domain)
+   ============================================================================ *)
+
+let less_than_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some position ->
+      let left, right = pair_of_nat_lt position in
+      let attributes : Attribute.materialized Tuple.AttributeMap.t =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic left); ("right", Obj.magic right) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"less_than" ~attributes,
+          generator )
+    | None ->
+      Error
+        "Cannot produce a randomly enumerated value for less_than over \
+         naturals."
+  in
+  make_comparison ~name:"natural_natural_less_than" ~domain_name:"natural"
+    ~pred:(fun c -> c < 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+let less_than_or_equal_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let a, b = cantor_pair_of_nat n in
+      (* a <= b is always true when a <= b; we enumerate all (a, b) with a <= b *)
+      let left = min a b in
+      let right = max a b in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic left); ("right", Obj.magic right) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"less_than_or_equal" ~attributes,
+          generator )
+    | None -> Error "Cannot enumerate less_than_or_equal randomly."
+  in
+  make_comparison ~name:"natural_natural_less_than_or_equal"
+    ~domain_name:"natural"
+    ~pred:(fun c -> c <= 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+let greater_than_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let left, right = pair_of_nat_lt n in
+      (* Swap: right > left *)
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic right); ("right", Obj.magic left) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"greater_than" ~attributes,
+          generator )
+    | None -> Error "Cannot enumerate greater_than randomly."
+  in
+  make_comparison ~name:"natural_natural_greater_than" ~domain_name:"natural"
+    ~pred:(fun c -> c > 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+let greater_than_or_equal_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let a, b = cantor_pair_of_nat n in
+      let left = max a b in
+      let right = min a b in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic left); ("right", Obj.magic right) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"greater_than_or_equal" ~attributes,
+          generator )
+    | None -> Error "Cannot enumerate greater_than_or_equal randomly."
+  in
+  make_comparison ~name:"natural_natural_greater_than_or_equal"
+    ~domain_name:"natural"
+    ~pred:(fun c -> c >= 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+let equal_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic n); ("right", Obj.magic n) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"equal" ~attributes, generator )
+    | None -> Error "Cannot enumerate equal randomly."
+  in
+  make_comparison ~name:"natural_natural_equal" ~domain_name:"natural"
+    ~pred:(fun c -> c = 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+let not_equal_natural : Relation.t =
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let a, b = cantor_pair_of_nat n in
+      let left, right = if a = b then (a, b + 1) else (a, b) in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("left", Obj.magic left); ("right", Obj.magic right) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"not_equal" ~attributes, generator )
+    | None -> Error "Cannot enumerate not_equal randomly."
+  in
+  make_comparison ~name:"natural_natural_not_equal" ~domain_name:"natural"
+    ~pred:(fun c -> c <> 0)
+    ~cardinality:Conventions.Cardinality.AlephZero ~generator
+
+(* ============================================================================
+   Arithmetic relations (natural domain)
+   ============================================================================ *)
+
+let plus_natural : Relation.t =
+  let schema =
+    Schema.empty |> Schema.add "a" "natural" |> Schema.add "b" "natural"
+    |> Schema.add "sum" "natural"
+  in
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let a, b = cantor_pair_of_nat n in
+      let s = a + b in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [ ("a", Obj.magic a); ("b", Obj.magic b); ("sum", Obj.magic s) ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"plus" ~attributes, generator )
+    | None -> Error "Cannot enumerate plus randomly."
+  in
+  let membership_criteria : Tuple.t -> bool = function
+    | Tuple.Materialized m -> (
+      match
+        ( Tuple.AttributeMap.find_opt "a" m.attributes,
+          Tuple.AttributeMap.find_opt "b" m.attributes,
+          Tuple.AttributeMap.find_opt "sum" m.attributes )
+      with
+      | Some a, Some b, Some s ->
+        (Obj.magic a.Attribute.value : int)
+        + (Obj.magic b.Attribute.value : int)
+        = (Obj.magic s.Attribute.value : int)
+      | _ -> false)
+    | Tuple.NonMaterialized _ -> false
+  in
+  Relation.make ~hash:None ~name:"natural_plus" ~schema ~tree:None
+    ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator:(Some generator) ~membership_criteria
+    ~provenance:(Relation.Provenance.Base "plus")
+    ~lineage:(Relation.Lineage.Base "plus")
+
+let times_natural : Relation.t =
+  let schema =
+    Schema.empty |> Schema.add "a" "natural"
+    |> Schema.add "b" "natural"
+    |> Schema.add "product" "natural"
+  in
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      let a, b = cantor_pair_of_nat n in
+      let p = a * b in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [
+            ("a", Obj.magic a); ("b", Obj.magic b); ("product", Obj.magic p);
+          ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"times" ~attributes, generator )
+    | None -> Error "Cannot enumerate times randomly."
+  in
+  let membership_criteria : Tuple.t -> bool = function
+    | Tuple.Materialized m -> (
+      match
+        ( Tuple.AttributeMap.find_opt "a" m.attributes,
+          Tuple.AttributeMap.find_opt "b" m.attributes,
+          Tuple.AttributeMap.find_opt "product" m.attributes )
+      with
+      | Some a, Some b, Some p ->
+        (Obj.magic a.Attribute.value : int)
+        * (Obj.magic b.Attribute.value : int)
+        = (Obj.magic p.Attribute.value : int)
+      | _ -> false)
+    | Tuple.NonMaterialized _ -> false
+  in
+  Relation.make ~hash:None ~name:"natural_times" ~schema ~tree:None
+    ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator:(Some generator) ~membership_criteria
+    ~provenance:(Relation.Provenance.Base "times")
+    ~lineage:(Relation.Lineage.Base "times")
+
+let minus_natural : Relation.t =
+  let schema =
+    Schema.empty |> Schema.add "a" "natural"
+    |> Schema.add "b" "natural"
+    |> Schema.add "difference" "natural"
+  in
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      (* Enumerate pairs where a >= b, so difference >= 0 *)
+      let b, diff = cantor_pair_of_nat n in
+      let a = b + diff in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [
+            ("a", Obj.magic a);
+            ("b", Obj.magic b);
+            ("difference", Obj.magic diff);
+          ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"minus" ~attributes, generator )
+    | None -> Error "Cannot enumerate minus randomly."
+  in
+  let membership_criteria : Tuple.t -> bool = function
+    | Tuple.Materialized m -> (
+      match
+        ( Tuple.AttributeMap.find_opt "a" m.attributes,
+          Tuple.AttributeMap.find_opt "b" m.attributes,
+          Tuple.AttributeMap.find_opt "difference" m.attributes )
+      with
+      | Some a, Some b, Some d ->
+        let av = (Obj.magic a.Attribute.value : int) in
+        let bv = (Obj.magic b.Attribute.value : int) in
+        let dv = (Obj.magic d.Attribute.value : int) in
+        av - bv = dv && dv >= 0
+      | _ -> false)
+    | Tuple.NonMaterialized _ -> false
+  in
+  Relation.make ~hash:None ~name:"natural_minus" ~schema ~tree:None
+    ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator:(Some generator) ~membership_criteria
+    ~provenance:(Relation.Provenance.Base "minus")
+    ~lineage:(Relation.Lineage.Base "minus")
+
+let divide_natural : Relation.t =
+  let schema =
+    Schema.empty |> Schema.add "a" "natural"
+    |> Schema.add "b" "natural"
+    |> Schema.add "quotient" "natural"
+    |> Schema.add "remainder" "natural"
+  in
+  let rec generator (position : int option) : Generator.result =
+    match position with
+    | Some n ->
+      (* Enumerate (b, q, r) triples where b > 0, then a = b*q + r, 0 <= r < b *)
+      (* We use a nested Cantor pairing: n -> (b_idx, qr_idx) -> (q, r) *)
+      let b_idx, qr_idx = cantor_pair_of_nat n in
+      let b = b_idx + 1 in (* b > 0 *)
+      let q, r_raw = cantor_pair_of_nat qr_idx in
+      let r = r_raw mod b in
+      let a = b * q + r in
+      let attributes =
+        Tuple.AttributeMap.of_list
+          [
+            ("a", Obj.magic a);
+            ("b", Obj.magic b);
+            ("quotient", Obj.magic q);
+            ("remainder", Obj.magic r);
+          ]
+      in
+      Generator.Value
+        ( Tuple.make_materialized ~relation:"divide" ~attributes, generator )
+    | None -> Error "Cannot enumerate divide randomly."
+  in
+  let membership_criteria : Tuple.t -> bool = function
+    | Tuple.Materialized m -> (
+      match
+        ( Tuple.AttributeMap.find_opt "a" m.attributes,
+          Tuple.AttributeMap.find_opt "b" m.attributes,
+          Tuple.AttributeMap.find_opt "quotient" m.attributes,
+          Tuple.AttributeMap.find_opt "remainder" m.attributes )
+      with
+      | Some a, Some b, Some q, Some r ->
+        let av = (Obj.magic a.Attribute.value : int) in
+        let bv = (Obj.magic b.Attribute.value : int) in
+        let qv = (Obj.magic q.Attribute.value : int) in
+        let rv = (Obj.magic r.Attribute.value : int) in
+        bv > 0 && av = bv * qv + rv && rv >= 0 && rv < bv
+      | _ -> false)
+    | Tuple.NonMaterialized _ -> false
+  in
+  Relation.make ~hash:None ~name:"natural_divide" ~schema ~tree:None
+    ~constraints:None
+    ~cardinality:Conventions.Cardinality.AlephZero
+    ~generator:(Some generator) ~membership_criteria
+    ~provenance:(Relation.Provenance.Base "divide")
+    ~lineage:(Relation.Lineage.Base "divide")
diff --git a/test/test_relational_engine.ml b/test/test_relational_engine.ml
index 8ba8226..f7421f1 100644
--- a/test/test_relational_engine.ml
+++ b/test/test_relational_engine.ml
@@ -705,7 +705,8 @@ let%test_unit "catalog: register_constraint inserts into sakura:constraint" =
       in
       let db = match Manipulation.Memory.register_constraint storage db
           ~constraint_name:"orders_id_positive"
-          ~relation_name:"orders" with
+          ~relation_name:"orders"
+          ~body:(Constraint.And []) with
         | Error _ -> assert false | Ok db -> db
       in
       let con_rel = match Manipulation.Memory.get_relation db ~name:"sakura:constraint" with
@@ -1350,3 +1351,1036 @@ let%test_unit "drl: execute Select+Const" =
             Obj.obj (Tuple.AttributeMap.find "name" (List.hd rows).Tuple.attributes).Attribute.value
           in
           assert (name_v = "Alice"))
+
+(* ============================================================================
+   Constraint System Tests
+   ============================================================================ *)
+
+(* ---------- Constraint construction ---------- *)
+
+let%test_unit "constraint: vars_in MemberOf" =
+  let b =
+    Constraint.BindingMap.empty
+    |> Constraint.BindingMap.add "left" (Constraint.Var "x")
+    |> Constraint.BindingMap.add "right" (Constraint.Const (Obj.repr 10))
+  in
+  let c = Constraint.MemberOf { target = "less_than"; binding = b } in
+  let vars = Constraint.vars_in c in
+  assert (List.mem "x" vars);
+  assert (not (List.mem "right" vars))
+
+let%test_unit "constraint: vars_in And" =
+  let b1 =
+    Constraint.BindingMap.singleton "left" (Constraint.Var "a")
+  in
+  let b2 =
+    Constraint.BindingMap.singleton "left" (Constraint.Var "b")
+  in
+  let c =
+    Constraint.And
+      [
+        Constraint.MemberOf { target = "t1"; binding = b1 };
+        Constraint.MemberOf { target = "t2"; binding = b2 };
+      ]
+  in
+  let vars = Constraint.vars_in c in
+  assert (List.mem "a" vars);
+  assert (List.mem "b" vars)
+
+let%test_unit "constraint: rename_vars" =
+  let b =
+    Constraint.BindingMap.singleton "left" (Constraint.Var "old_name")
+  in
+  let c = Constraint.MemberOf { target = "t"; binding = b } in
+  let c' = Constraint.rename_vars [ ("old_name", "new_name") ] c in
+  let vars = Constraint.vars_in c' in
+  assert (List.mem "new_name" vars);
+  assert (not (List.mem "old_name" vars))
+
+let%test_unit "constraint: filter_by_attrs keeps relevant" =
+  let b =
+    Constraint.BindingMap.singleton "left" (Constraint.Var "x")
+  in
+  let c = Constraint.MemberOf { target = "t"; binding = b } in
+  assert (Constraint.filter_by_attrs [ "x" ] c <> None);
+  assert (Constraint.filter_by_attrs [ "y" ] c = None)
+
+let%test_unit "constraint: merge named constraints" =
+  let b = Constraint.BindingMap.empty in
+  let cs1 = [ ("c1", Constraint.MemberOf { target = "t1"; binding = b }) ] in
+  let cs2 = [ ("c2", Constraint.MemberOf { target = "t2"; binding = b }) ] in
+  let merged = Constraint.merge cs1 cs2 in
+  assert (List.length merged = 2)
+
+let%test_unit "constraint: merge duplicate names produces And" =
+  let b = Constraint.BindingMap.empty in
+  let c1 = Constraint.MemberOf { target = "t1"; binding = b } in
+  let c2 = Constraint.MemberOf { target = "t2"; binding = b } in
+  let merged = Constraint.merge [ ("shared", c1) ] [ ("shared", c2) ] in
+  assert (List.length merged = 1);
+  match List.assoc "shared" merged with
+  | Constraint.And _ -> ()
+  | _ -> assert false
+
+(* ---------- Smart constructors ---------- *)
+
+let%test_unit "constraint: and_ singleton" =
+  let b = Constraint.BindingMap.empty in
+  let c = Constraint.MemberOf { target = "t"; binding = b } in
+  match Constraint.and_ [ c ] with
+  | Constraint.MemberOf _ -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: or_ singleton" =
+  let b = Constraint.BindingMap.empty in
+  let c = Constraint.MemberOf { target = "t"; binding = b } in
+  match Constraint.or_ [ c ] with
+  | Constraint.MemberOf _ -> ()
+  | _ -> assert false
+
+(* ---------- Comparison shorthands ---------- *)
+
+let%test_unit "constraint: lt shorthand" =
+  match Constraint.lt ~left:(Var "x") ~right:(Const (Obj.repr 5)) with
+  | Constraint.MemberOf { target = "less_than"; _ } -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: between shorthand" =
+  match
+    Constraint.between ~value:(Var "x") ~low:(Const (Obj.repr 0))
+      ~high:(Const (Obj.repr 100))
+  with
+  | Constraint.And [ _; _ ] -> ()
+  | _ -> assert false
+
+(* ---------- Binding resolution ---------- *)
+
+let%test_unit "constraint: bind resolves Var and Const" =
+  let b =
+    Constraint.BindingMap.empty
+    |> Constraint.BindingMap.add "left" (Constraint.Var "x")
+    |> Constraint.BindingMap.add "right" (Constraint.Const (Obj.repr 42))
+  in
+  let tuple : Tuple.materialized =
+    {
+      relation = "test";
+      attributes =
+        Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 10 };
+    }
+  in
+  let bound = Constraint.bind b tuple in
+  assert (List.length bound = 2);
+  let left_v : int = Obj.obj (List.assoc "left" bound) in
+  let right_v : int = Obj.obj (List.assoc "right" bound) in
+  assert (left_v = 10);
+  assert (right_v = 42)
+
+(* ---------- Evaluation engine ---------- *)
+
+let make_eval_ctx ?(relations = []) () : Constraint.eval_context =
+  {
+    check_membership =
+      (fun rel_name bound_pairs ->
+        match List.assoc_opt rel_name relations with
+        | None -> false
+        | Some checker -> checker bound_pairs);
+    iterate_finite =
+      (fun rel_name ->
+        match List.assoc_opt rel_name relations with
+        | None -> None
+        | Some _ -> Some []);
+  }
+
+let%test_unit "constraint: evaluate MemberOf success" =
+  let ctx =
+    make_eval_ctx
+      ~relations:[ ("my_rel", fun _pairs -> true) ]
+      ()
+  in
+  let b = Constraint.BindingMap.empty in
+  let c = Constraint.MemberOf { target = "my_rel"; binding = b } in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Ok true -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: evaluate MemberOf failure" =
+  let ctx =
+    make_eval_ctx
+      ~relations:[ ("my_rel", fun _pairs -> false) ]
+      ()
+  in
+  let b = Constraint.BindingMap.empty in
+  let c = Constraint.MemberOf { target = "my_rel"; binding = b } in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Error (Constraint.MembershipFailed _) -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: evaluate And short-circuits" =
+  let call_count = ref 0 in
+  let ctx =
+    make_eval_ctx
+      ~relations:
+        [
+          ( "fail_rel",
+            fun _ ->
+              incr call_count;
+              false );
+          ( "ok_rel",
+            fun _ ->
+              incr call_count;
+              true );
+        ]
+      ()
+  in
+  let b = Constraint.BindingMap.empty in
+  let c =
+    Constraint.And
+      [
+        Constraint.MemberOf { target = "fail_rel"; binding = b };
+        Constraint.MemberOf { target = "ok_rel"; binding = b };
+      ]
+  in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  (match Constraint.evaluate ctx tuple c with
+   | Error _ -> ()
+   | _ -> assert false);
+  (* Second branch should not have been called *)
+  assert (!call_count = 1)
+
+let%test_unit "constraint: evaluate Or succeeds on first match" =
+  let ctx =
+    make_eval_ctx
+      ~relations:
+        [
+          ("a", fun _ -> false);
+          ("b", fun _ -> true);
+        ]
+      ()
+  in
+  let b = Constraint.BindingMap.empty in
+  let c =
+    Constraint.Or
+      [
+        Constraint.MemberOf { target = "a"; binding = b };
+        Constraint.MemberOf { target = "b"; binding = b };
+      ]
+  in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Ok true -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: evaluate Not negates" =
+  let ctx : Constraint.eval_context =
+    {
+      check_membership =
+        (fun rel_name _pairs ->
+          match rel_name with
+          | "universe" -> true
+          | "body_rel" -> false
+          | _ -> false);
+      iterate_finite = (fun _ -> None);
+    }
+  in
+  let b = Constraint.BindingMap.empty in
+  let c =
+    Constraint.Not
+      {
+        body = Constraint.MemberOf { target = "body_rel"; binding = b };
+        universe = "universe";
+      }
+  in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Ok true -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: evaluate Exists over finite relation" =
+  let ctx : Constraint.eval_context =
+    {
+      check_membership =
+        (fun _rel_name pairs ->
+          match List.assoc_opt "left" pairs, List.assoc_opt "right" pairs with
+          | Some l, Some r -> (Obj.obj l : int) < (Obj.obj r : int)
+          | _ -> false);
+      iterate_finite =
+        (fun rel_name ->
+          if rel_name = "small_set" then
+            Some
+              [
+                [ ("value", Obj.repr 1) ];
+                [ ("value", Obj.repr 5) ];
+                [ ("value", Obj.repr 10) ];
+              ]
+          else None);
+    }
+  in
+  let b =
+    Constraint.BindingMap.empty
+    |> Constraint.BindingMap.add "left" (Constraint.Var "x")
+    |> Constraint.BindingMap.add "right" (Constraint.Var "value")
+  in
+  let c =
+    Constraint.Exists
+      {
+        variable = "value";
+        quantifier = "small_set";
+        body = Constraint.MemberOf { target = "less_than"; binding = b };
+      }
+  in
+  (* x=3, exists value in {1,5,10} where 3 < value => true (5 or 10 work) *)
+  let tuple : Tuple.materialized =
+    {
+      relation = "test";
+      attributes =
+        Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 3 };
+    }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Ok true -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: evaluate Forall fails when not all match" =
+  let ctx : Constraint.eval_context =
+    {
+      check_membership =
+        (fun _rel_name pairs ->
+          match List.assoc_opt "left" pairs, List.assoc_opt "right" pairs with
+          | Some l, Some r -> (Obj.obj l : int) < (Obj.obj r : int)
+          | _ -> false);
+      iterate_finite =
+        (fun rel_name ->
+          if rel_name = "small_set" then
+            Some
+              [
+                [ ("value", Obj.repr 1) ];
+                [ ("value", Obj.repr 5) ];
+              ]
+          else None);
+    }
+  in
+  let b =
+    Constraint.BindingMap.empty
+    |> Constraint.BindingMap.add "left" (Constraint.Var "x")
+    |> Constraint.BindingMap.add "right" (Constraint.Var "value")
+  in
+  let c =
+    Constraint.Forall
+      {
+        variable = "value";
+        quantifier = "small_set";
+        body = Constraint.MemberOf { target = "less_than"; binding = b };
+      }
+  in
+  (* x=3, forall value in {1,5} where 3 < value => false (3 is not < 1) *)
+  let tuple : Tuple.materialized =
+    {
+      relation = "test";
+      attributes =
+        Tuple.AttributeMap.singleton "x" { Attribute.value = Obj.repr 3 };
+    }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Ok false -> ()
+  | _ -> assert false
+
+let%test_unit "constraint: Forall unbounded quantifier errors" =
+  let ctx : Constraint.eval_context =
+    {
+      check_membership = (fun _ _ -> true);
+      iterate_finite = (fun _ -> None);
+    }
+  in
+  let b = Constraint.BindingMap.empty in
+  let c =
+    Constraint.Forall
+      {
+        variable = "v";
+        quantifier = "infinite_rel";
+        body = Constraint.MemberOf { target = "t"; binding = b };
+      }
+  in
+  let tuple : Tuple.materialized =
+    { relation = "test"; attributes = Tuple.AttributeMap.empty }
+  in
+  match Constraint.evaluate ctx tuple c with
+  | Error (Constraint.UnboundedQuantifier _) -> ()
+  | _ -> assert false
+
+(* ---------- Integrated constraint enforcement in manipulation ---------- *)
+
+let%test_unit "constraint: create_tuple with passing constraint" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema = Schema.empty |> Schema.add "value" "natural" in
+    let db, _rel =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"positives"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Register a constraint: value must be member of natural (always true for naturals) *)
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"is_natural" ~relation_name:"positives"
+          ~body:(Constraint.And [])
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let rel =
+      match Manipulation.Memory.get_relation db ~name:"positives" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let tuple : Tuple.materialized =
+      {
+        relation = "positives";
+        attributes =
+          Tuple.AttributeMap.singleton "value"
+            { Attribute.value = Obj.repr 5 };
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db rel tuple with
+    | Ok _ -> ()
+    | Error _ -> assert false)
+
+let%test_unit "constraint: create_tuple with failing constraint" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema = Schema.empty |> Schema.add "value" "natural" in
+    let db, _rel =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"checked"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Register a constraint that always fails: MemberOf a nonexistent relation *)
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"impossible" ~relation_name:"checked"
+          ~body:
+            (Constraint.MemberOf
+               {
+                 target = "nonexistent_relation";
+                 binding =
+                   Constraint.BindingMap.singleton "x" (Constraint.Var "value");
+               })
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let rel =
+      match Manipulation.Memory.get_relation db ~name:"checked" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let tuple : Tuple.materialized =
+      {
+        relation = "checked";
+        attributes =
+          Tuple.AttributeMap.singleton "value"
+            { Attribute.value = Obj.repr 5 };
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db rel tuple with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* ---------- Scenario tests ported from Erlang ---------- *)
+
+(* Scenario 1: Mutual exclusion between subtypes *)
+let%test_unit "constraint scenario: mutual exclusion subtypes" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema = Schema.empty |> Schema.add "id" "natural" in
+    let db, _employee =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"employee"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    let db, _manager =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"manager"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* manager must NOT be in employee (mutual exclusion) *)
+    let body =
+      Constraint.Not
+        {
+          body =
+            Constraint.MemberOf
+              {
+                target = "employee";
+                binding =
+                  Constraint.BindingMap.singleton "id" (Constraint.Var "id");
+              };
+          universe = "manager";
+        }
+    in
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"not_employee" ~relation_name:"manager" ~body
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    (* Insert into employee first *)
+    let employee =
+      match Manipulation.Memory.get_relation db ~name:"employee" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let emp_tuple : Tuple.materialized =
+      {
+        relation = "employee";
+        attributes =
+          Tuple.AttributeMap.singleton "id"
+            { Attribute.value = Obj.repr 1 };
+      }
+    in
+    let db, _employee, _ =
+      match
+        Manipulation.Memory.create_tuple storage db employee emp_tuple
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Now try to insert same id into manager — should fail *)
+    let manager =
+      match Manipulation.Memory.get_relation db ~name:"manager" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let mgr_tuple : Tuple.materialized =
+      {
+        relation = "manager";
+        attributes =
+          Tuple.AttributeMap.singleton "id"
+            { Attribute.value = Obj.repr 1 };
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db manager mgr_tuple with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* Scenario 2: Foreign key constraint *)
+let%test_unit "constraint scenario: foreign key" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let order_schema = Schema.empty |> Schema.add "order_id" "natural" in
+    let db, _orders =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"orders"
+          ~schema:order_schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    let item_schema =
+      Schema.empty |> Schema.add "item_id" "natural"
+      |> Schema.add "order_id" "natural"
+    in
+    let db, _items =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"order_items"
+          ~schema:item_schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* FK: order_items.order_id must exist in orders *)
+    let fk_body =
+      Constraint.MemberOf
+        {
+          target = "orders";
+          binding =
+            Constraint.BindingMap.singleton "order_id"
+              (Constraint.Var "order_id");
+        }
+    in
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"fk_order" ~relation_name:"order_items"
+          ~body:fk_body
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    (* Insert an order *)
+    let orders =
+      match Manipulation.Memory.get_relation db ~name:"orders" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let order_tuple : Tuple.materialized =
+      {
+        relation = "orders";
+        attributes =
+          Tuple.AttributeMap.singleton "order_id"
+            { Attribute.value = Obj.repr 100 };
+      }
+    in
+    let db, _orders, _ =
+      match
+        Manipulation.Memory.create_tuple storage db orders order_tuple
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Insert item referencing valid order — should succeed *)
+    let items =
+      match Manipulation.Memory.get_relation db ~name:"order_items" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let valid_item : Tuple.materialized =
+      {
+        relation = "order_items";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("item_id", { Attribute.value = Obj.repr 1 });
+              ("order_id", { Attribute.value = Obj.repr 100 });
+            ];
+      }
+    in
+    let db, items, _ =
+      match
+        Manipulation.Memory.create_tuple storage db items valid_item
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Insert item referencing nonexistent order — should fail *)
+    let invalid_item : Tuple.materialized =
+      {
+        relation = "order_items";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("item_id", { Attribute.value = Obj.repr 2 });
+              ("order_id", { Attribute.value = Obj.repr 999 });
+            ];
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db items invalid_item with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* Scenario 3: Self-reference (emp_id != mgr_id via not_equal comparison) *)
+let%test_unit "constraint scenario: self-reference neq" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema =
+      Schema.empty |> Schema.add "emp_id" "natural"
+      |> Schema.add "mgr_id" "natural"
+    in
+    let db, _rel =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"reports_to"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Register the not_equal comparison relation *)
+    let db, _ =
+      match
+        Manipulation.Memory.create_immutable_relation storage db
+          ~name:"not_equal"
+          ~schema:
+            (Schema.empty |> Schema.add "left" "natural"
+            |> Schema.add "right" "natural")
+          ~generator:(fun _ -> Generator.Error "not enumerable")
+          ~membership_criteria:(fun t ->
+            match t with
+            | Tuple.Materialized m -> (
+              match
+                ( Tuple.AttributeMap.find_opt "left" m.attributes,
+                  Tuple.AttributeMap.find_opt "right" m.attributes )
+              with
+              | Some l, Some r ->
+                (Obj.obj l.Attribute.value : int)
+                <> (Obj.obj r.Attribute.value : int)
+              | _ -> false)
+            | _ -> false)
+          ~cardinality:Conventions.Cardinality.AlephZero
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Constraint: emp_id != mgr_id via not_equal relation *)
+    let neq_body =
+      Constraint.neq ~left:(Var "emp_id") ~right:(Var "mgr_id")
+    in
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"no_self_manage" ~relation_name:"reports_to"
+          ~body:neq_body
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let rel =
+      match Manipulation.Memory.get_relation db ~name:"reports_to" with
+      | None -> assert false
+      | Some r -> r
+    in
+    (* Insert (emp_id=1, mgr_id=2) — should succeed *)
+    let valid : Tuple.materialized =
+      {
+        relation = "reports_to";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("emp_id", { Attribute.value = Obj.repr 1 });
+              ("mgr_id", { Attribute.value = Obj.repr 2 });
+            ];
+      }
+    in
+    let db, rel, _ =
+      match Manipulation.Memory.create_tuple storage db rel valid with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Insert (emp_id=3, mgr_id=3) — same person, should fail *)
+    let invalid : Tuple.materialized =
+      {
+        relation = "reports_to";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("emp_id", { Attribute.value = Obj.repr 3 });
+              ("mgr_id", { Attribute.value = Obj.repr 3 });
+            ];
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db rel invalid with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* Scenario 4: Mutual exclusion between open_ticket and closed_ticket *)
+let%test_unit "constraint scenario: open vs closed ticket" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema = Schema.empty |> Schema.add "ticket_id" "natural" in
+    let db, _ =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"open_ticket"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    let db, _ =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"closed_ticket"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* open_ticket must not be in closed_ticket *)
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"not_closed" ~relation_name:"open_ticket"
+          ~body:
+            (Constraint.Not
+               {
+                 body =
+                   Constraint.MemberOf
+                     {
+                       target = "closed_ticket";
+                       binding =
+                         Constraint.BindingMap.singleton "ticket_id"
+                           (Constraint.Var "ticket_id");
+                     };
+                 universe = "open_ticket";
+               })
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    (* Insert ticket 1 as closed *)
+    let closed =
+      match Manipulation.Memory.get_relation db ~name:"closed_ticket" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let t1 : Tuple.materialized =
+      {
+        relation = "closed_ticket";
+        attributes =
+          Tuple.AttributeMap.singleton "ticket_id"
+            { Attribute.value = Obj.repr 1 };
+      }
+    in
+    let db, _, _ =
+      match Manipulation.Memory.create_tuple storage db closed t1 with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Try to open same ticket — should fail *)
+    let open_ =
+      match Manipulation.Memory.get_relation db ~name:"open_ticket" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let t1_open : Tuple.materialized =
+      {
+        relation = "open_ticket";
+        attributes =
+          Tuple.AttributeMap.singleton "ticket_id"
+            { Attribute.value = Obj.repr 1 };
+      }
+    in
+    match Manipulation.Memory.create_tuple storage db open_ t1_open with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* Scenario 5: Weak entity dependency *)
+let%test_unit "constraint scenario: weak entity dependency" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let parent_schema = Schema.empty |> Schema.add "parent_id" "natural" in
+    let db, _ =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"parent"
+          ~schema:parent_schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    let dep_schema =
+      Schema.empty |> Schema.add "dep_id" "natural"
+      |> Schema.add "parent_id" "natural"
+    in
+    let db, _ =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"dependent"
+          ~schema:dep_schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* dependent.parent_id must exist in parent *)
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"parent_exists" ~relation_name:"dependent"
+          ~body:
+            (Constraint.MemberOf
+               {
+                 target = "parent";
+                 binding =
+                   Constraint.BindingMap.singleton "parent_id"
+                     (Constraint.Var "parent_id");
+               })
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    (* Insert parent *)
+    let parent =
+      match Manipulation.Memory.get_relation db ~name:"parent" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let pt : Tuple.materialized =
+      {
+        relation = "parent";
+        attributes =
+          Tuple.AttributeMap.singleton "parent_id"
+            { Attribute.value = Obj.repr 10 };
+      }
+    in
+    let db, _, _ =
+      match Manipulation.Memory.create_tuple storage db parent pt with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Insert dependent with valid parent — succeeds *)
+    let dep =
+      match Manipulation.Memory.get_relation db ~name:"dependent" with
+      | None -> assert false
+      | Some r -> r
+    in
+    let valid_dep : Tuple.materialized =
+      {
+        relation = "dependent";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("dep_id", { Attribute.value = Obj.repr 1 });
+              ("parent_id", { Attribute.value = Obj.repr 10 });
+            ];
+      }
+    in
+    let db, dep, _ =
+      match
+        Manipulation.Memory.create_tuple storage db dep valid_dep
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Insert dependent with nonexistent parent — fails *)
+    let invalid_dep : Tuple.materialized =
+      {
+        relation = "dependent";
+        attributes =
+          Tuple.AttributeMap.of_list
+            [
+              ("dep_id", { Attribute.value = Obj.repr 2 });
+              ("parent_id", { Attribute.value = Obj.repr 999 });
+            ];
+      }
+    in
+    match
+      Manipulation.Memory.create_tuple storage db dep invalid_dep
+    with
+    | Error (Manipulation.ConstraintViolation _) -> ()
+    | _ -> assert false)
+
+(* Scenario 6: Algebra propagation — select preserves constraints *)
+let%test_unit "constraint propagation: select preserves constraints" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema = Schema.empty |> Schema.add "x" "natural" in
+    let db, _rel =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"constrained"
+          ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"c1" ~relation_name:"constrained"
+          ~body:(Constraint.And [])
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let rel =
+      match Manipulation.Memory.get_relation db ~name:"constrained" with
+      | None -> assert false
+      | Some r -> r
+    in
+    match
+      Algebra.Memory.select_fn storage (fun _ -> true) rel
+    with
+    | Error _ -> assert false
+    | Ok result ->
+      assert (result.Relation.constraints <> None))
+
+(* Scenario 7: Algebra propagation — project filters constraints *)
+let%test_unit "constraint propagation: project filters constraints" =
+  with_storage (fun storage ->
+    let db =
+      match Manipulation.Memory.create_database storage ~name:"test" with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let schema =
+      Schema.empty |> Schema.add "x" "natural" |> Schema.add "y" "natural"
+    in
+    let db, _rel =
+      match
+        Manipulation.Memory.create_relation storage db ~name:"xy" ~schema
+      with
+      | Error _ -> assert false
+      | Ok x -> x
+    in
+    (* Constraint on x only *)
+    let c_on_x =
+      Constraint.MemberOf
+        {
+          target = "some_rel";
+          binding =
+            Constraint.BindingMap.singleton "left" (Constraint.Var "x");
+        }
+    in
+    let db =
+      match
+        Manipulation.Memory.register_constraint storage db
+          ~constraint_name:"x_only" ~relation_name:"xy" ~body:c_on_x
+      with
+      | Error _ -> assert false
+      | Ok db -> db
+    in
+    let rel =
+      match Manipulation.Memory.get_relation db ~name:"xy" with
+      | None -> assert false
+      | Some r -> r
+    in
+    (* Project to only "x" — constraint should survive *)
+    (match Algebra.Memory.project storage [ "x" ] rel with
+     | Error _ -> assert false
+     | Ok result -> assert (result.Relation.constraints <> None));
+    (* Project to only "y" — constraint referencing "x" should be dropped *)
+    match Algebra.Memory.project storage [ "y" ] rel with
+    | Error _ -> assert false
+    | Ok result -> assert (result.Relation.constraints = None))