Polarity walker, constraint and manipulation refactor with batteries

11 files changed, 1543 insertions, 1276 deletions

diff --git a/bin/dune b/bin/dune
index 27cf07a..5a6c7d4 100644
--- a/bin/dune
+++ b/bin/dune
@@ -11,9 +11,3 @@
  (modules server)
  (libraries relational_engine unix)
  (modes byte exe))
-
-(executable
- (name bench)
- (modules bench)
- (libraries relational_engine unix)
- (modes exe))
diff --git a/flake.nix b/flake.nix
index 6a1e1a2..bee021b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -109,6 +109,8 @@
               ppx_sexp_conv
               lwt
               lwt-exit
+              batteries
+              num
             ]);
 
             strictDeps = true;
@@ -272,6 +274,8 @@
               # legacyPackages.nixfmt-classic
               ocamlPackages.lwt
               ocamlPackages.lwt-exit
+              ocamlPackages.batteries
+              ocamlPackages.num
               ppx_protocol_conv
               ppx_protocol_conv_xml_light
               ocamlPackages.earlybird
@@ -283,6 +287,7 @@
 
 
             shellHook = ''
+              export CAML_LD_LIBRARY_PATH="''${CAML_LD_LIBRARY_PATH:+$CAML_LD_LIBRARY_PATH:}$(ocamlfind query num)"
               # echo MERKLECPP_INCLUDE_PATH=$MERKLECPP_INCLUDE_PATH
               echo LIBRESSL_INCLUDE_PATH=$LIBRESSL_INCLUDE_PATH
               echo LIBRESSL_LIB_PATH=$LIBRESSL_LIB_PATH
diff --git a/lib/constraint.ml b/lib/constraint.ml
index 527a7dc..05442ab 100644
--- a/lib/constraint.ml
+++ b/lib/constraint.ml
@@ -1,11 +1,11 @@
 (** 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.
+    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. *)
+    Negation requires an explicit universe relation name, forcing closed-world
+    reasoning in first-order logic. *)
 
 (* TODO: lt/lte/gt/gte/eq/neq/between at the bottom reference target names
    like "less_than" that don't match the prelude relation names
@@ -14,12 +14,12 @@
 
 type relation_name = string
 type attr_name = string
-
-type binding_expr =
-  | Var of attr_name
-  | Const of Conventions.AbstractValue.t
+type binding_expr = Var of attr_name | Const of Conventions.AbstractValue.t
 
 module BindingMap = Map.Make (String)
+module PolarityMap = Map.Make (String)
+module StringSet = Set.Make (String)
+module FingerTree = BatFingerTree
 
 type binding = binding_expr BindingMap.t
 
@@ -37,96 +37,89 @@ type diagnostic =
       bound_values : (attr_name * Conventions.AbstractValue.t) list;
     }
   | RelationNotFound of string
-  | UnboundedQuantifier of {
-      variable : attr_name;
-      quantifier : relation_name;
-    }
+  | UnboundedQuantifier of { variable : attr_name; quantifier : relation_name }
   | ConstraintFailures of (string * diagnostic) list
 
-let rec vars_in : t -> attr_name list = function
-  | MemberOf { binding; _ } ->
+let vars_in (c : t) : attr_name list =
+  let add_from_binding set 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
-
-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 }
+        match expr with Var v -> StringSet.add v acc | Const _ -> acc)
+      binding set
+  in
+  let rec loop set worklist =
+    match FingerTree.front worklist with
+    | None -> set
+    | Some (rest, node) -> (
+        match node with
+        | MemberOf { binding; _ } -> loop (add_from_binding set binding) rest
+        | Not { body; _ } -> loop set (FingerTree.cons rest body)
+        | And cs | Or cs ->
+            let next = FingerTree.append (FingerTree.of_list cs) rest in
+            loop set next
+        | Exists { variable; body; _ } | Forall { variable; body; _ } ->
+            loop (StringSet.add variable set) (FingerTree.cons rest body))
+  in
+  loop StringSet.empty (FingerTree.singleton c) |> StringSet.elements
 
-(** 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)
+let rename_vars (renames : (attr_name * attr_name) list) : t -> t =
+  let rename_map = BindingMap.of_seq (List.to_seq renames) in
+  let rename_name name =
+    match BindingMap.find_opt name rename_map with Some n -> n | None -> name
+  in
+  let rec go = function
+    | MemberOf { target; binding } ->
+        let binding' =
+          BindingMap.fold
+            (fun k expr acc ->
+              let k' = rename_name k in
+              let expr' =
+                match expr with Var v -> Var (rename_name v) | Const _ -> expr
+              in
+              BindingMap.add k' expr' acc)
+            binding BindingMap.empty
+        in
+        MemberOf { target; binding = binding' }
+    | Not { body; universe } -> Not { body = go body; universe }
+    | And cs -> And (List.map go cs)
+    | Or cs -> Or (List.map go cs)
+    | Exists { variable; quantifier; body } ->
+        let variable' = rename_name variable in
+        Exists { variable = variable'; quantifier; body = go body }
+    | Forall { variable; quantifier; body } ->
+        let variable' = rename_name variable in
+        Forall { variable = variable'; quantifier; body = go body }
   in
+  go
+
+(** 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)
+      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)
+      let kept = List.filter_map (filter_by_attrs attrs) cs in
+      if kept = [] then None else Some (And kept)
   | Or cs ->
-    (* All branches must survive for Or to remain sound *)
-    let kept = List.filter_map (filter_by_attrs attrs) cs in
-    if List.length kept = List.length cs then Some (Or kept) else None
+      (* All branches must survive for Or to remain sound *)
+      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)
+      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)
+      match filter_by_attrs (variable :: attrs) body with
+      | Some body' -> Some (Forall { variable; quantifier; body = body' })
+      | None -> None)
 
-let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
-    : (string * t) list =
+let merge (cs1 : (string * t) list) (cs2 : (string * t) list) :
+    (string * t) list =
   let combined = cs1 @ cs2 in
   let tbl = Hashtbl.create 16 in
   List.iter
@@ -144,105 +137,99 @@ let merge (cs1 : (string * t) list) (cs2 : (string * t) list)
 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 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 }
 
 type eval_context = {
   check_membership :
-    relation_name ->
-    (attr_name * Conventions.AbstractValue.t) list ->
-    bool;
+    relation_name -> (attr_name * Conventions.AbstractValue.t) list -> bool;
   iterate_finite :
-    relation_name ->
-    (attr_name * Conventions.AbstractValue.t) list list option;
+    relation_name -> (attr_name * Conventions.AbstractValue.t) list list option;
 }
 
-let bind (b : binding) (tuple : Tuple.materialized)
-    : (attr_name * Conventions.AbstractValue.t) list =
+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)
+            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)
+      match value with Some v -> (target_attr, v) :: acc | None -> acc)
     b []
 
-let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t)
-    : (bool, diagnostic) result =
+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.
+      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 negate the body; the universe enforces logical soundness
        at the schema level, not as a runtime tuple-existence check. *)
-    (match evaluate ctx tuple body with
-     | Ok true -> Ok false
-     | Ok false -> Ok true
-     | Error (MembershipFailed _) -> Ok true
-     | Error d -> Error d)
+      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 ->
-          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)
+      match ctx.iterate_finite quantifier with
+      | None -> Error (UnboundedQuantifier { variable; quantifier })
+      | Some rows ->
+          let rec check = function
+            | [] -> Ok false
+            | row :: rest -> (
+                let extended_tuple = extend_tuple tuple variable row in
+                match evaluate ctx extended_tuple body with
+                | Ok true -> Ok true
+                | Ok false -> check rest
+                | Error _ -> check rest)
+          in
+          check rows)
   | 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)
+      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)
+      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)
-
-and extend_tuple (tuple : Tuple.materialized)
-    (variable : attr_name)
-    (row : (attr_name * Conventions.AbstractValue.t) list)
-    : Tuple.materialized =
+      match evaluate ctx tuple c with
+      | Ok true -> Ok true
+      | Ok false -> evaluate_or ctx tuple rest
+      | Error _ -> evaluate_or ctx tuple rest)
+
+and extend_tuple (tuple : Tuple.materialized) (variable : attr_name)
+    (row : (attr_name * Conventions.AbstractValue.t) list) : Tuple.materialized
+    =
   (* Quantifier attributes are namespaced by the variable name (for example "d.dept_id")
      so they cannot silently overwrite same-named attributes from the base tuple
      or from other quantifiers. Without such namespacing, a constraint like
@@ -272,113 +259,157 @@ let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized)
         match evaluate ctx tuple c with
         | Ok true -> None
         | Ok false ->
-          Some (name, MembershipFailed { target = name; bound_values = [] })
+            Some (name, MembershipFailed { target = name; bound_values = [] })
         | Error d -> Some (name, d))
       named
   in
-  match failures with
-  | [] -> Ok true
-  | fs -> Error (ConstraintFailures fs)
+  match failures with [] -> Ok true | fs -> Error (ConstraintFailures fs)
+
+(** Fast-path evaluator: halts at the first non-passing constraint. Use in
+    cascade and deferred checking where a single violation suffices. *)
+let evaluate_first_failure (ctx : eval_context) (tuple : Tuple.materialized)
+    (named : (string * t) list) : (bool, diagnostic) result =
+  let rec loop = function
+    | [] -> Ok true
+    | (_name, c) :: rest -> (
+        match evaluate ctx tuple c with Ok true -> loop rest | r -> r)
+  in
+  loop named
 
-(** Polarity analysis: determines whether each relation name appears in
-    a positive (must-exist) or negative (must-not-exist) position within
-    a constraint tree. Used for cascade checking: when a tuple is deleted,
-    only relations with Positive or Both polarity need re-validation. *)
+(** Polarity analysis: determines whether each relation name appears in a
+    positive (must-exist) or negative (must-not-exist) position within a
+    constraint tree. Used for cascade checking: when a tuple is deleted, only
+    relations with Positive or Both polarity need re-validation. *)
 
 type polarity = Positive | Negative | Both
+type polarity_index = polarity PolarityMap.t
 
 let merge_polarity a b =
-  match a, b with
+  match (a, b) with
   | Positive, Positive -> Positive
   | Negative, Negative -> Negative
-  | _                  -> Both
+  | _ -> Both
 
 let flip_polarity = function
   | Positive -> Negative
   | Negative -> Positive
-  | Both     -> Both
-
-let merge_polarity_maps m1 m2 =
-  List.fold_left (fun acc (name, pol) ->
-    match List.assoc_opt name acc with
-    | None      -> (name, pol) :: acc
-    | Some prev ->
-      (name, merge_polarity prev pol)
-      :: List.filter (fun (n, _) -> n <> name) acc)
-    m1 m2
-
-let rec polarity_of ?(neg = false) (c : t) : (relation_name * polarity) list =
-  let pos p = if neg then flip_polarity p else p in
-  match c with
-  | MemberOf { target; _ } ->
-    [(target, pos Positive)]
-  | Not { body; _ } ->
-    polarity_of ~neg:(not neg) body
-  | And cs | Or cs ->
-    List.fold_left (fun acc c ->
-      merge_polarity_maps acc (polarity_of ~neg c)) [] cs
-  | Exists { quantifier; body; _ } ->
-    merge_polarity_maps
-      [(quantifier, pos Positive)]
-      (polarity_of ~neg body)
-  | Forall { quantifier; body; _ } ->
-    merge_polarity_maps
-      [(quantifier, pos Negative)]
-      (polarity_of ~neg body)
+  | Both -> Both
+
+let polarity_of ?(neg = false) (c : t) : polarity_index =
+  let with_neg is_neg pol = if is_neg then flip_polarity pol else pol in
+  let add_pol acc name pol =
+    match PolarityMap.find_opt name acc with
+    | None -> PolarityMap.add name pol acc
+    | Some prev -> PolarityMap.add name (merge_polarity prev pol) acc
+  in
+  let rec loop acc worklist =
+    match FingerTree.front worklist with
+    | None -> acc
+    | Some (rest, (is_neg, node)) -> (
+        match node with
+        | MemberOf { target; _ } ->
+            loop (add_pol acc target (with_neg is_neg Positive)) rest
+        | Not { body; _ } -> loop acc (FingerTree.cons rest (not is_neg, body))
+        | And cs | Or cs ->
+            let children =
+              List.map (fun child -> (is_neg, child)) cs |> FingerTree.of_list
+            in
+            let next = FingerTree.append children rest in
+            loop acc next
+        | Exists { quantifier; body; _ } ->
+            let acc' = add_pol acc quantifier (with_neg is_neg Positive) in
+            loop acc' (FingerTree.cons rest (is_neg, body))
+        | Forall { quantifier; body; _ } ->
+            let acc' = add_pol acc quantifier (with_neg is_neg Negative) in
+            loop acc' (FingerTree.cons rest (is_neg, body)))
+  in
+  loop PolarityMap.empty (FingerTree.singleton (neg, c))
+
+let polarity_find name (pols : polarity_index) = PolarityMap.find_opt name pols
 
 (** Constraint timing: immediate (checked on every mutation) or deferred
     (checked at transaction commit). *)
 type timing = Immediate | Deferred
 
+type substitute_mode =
+  | SubstituteGo
+  | SubstituteApply of Conventions.AbstractValue.t BindingMap.t
+
+type substitute_instr =
+  | Visit of substitute_mode * t
+  | BuildNot of relation_name
+  | BuildAnd of int
+  | BuildOr of int
+  | BuildExists of attr_name * relation_name
+  | BuildForall of attr_name * relation_name
+
 (** Given a constraint, a deleted relation name [dep_rel], and the deleted
-    tuple's attributes, return a filter: [(attr_name, value)] pairs that
-    narrow which constrained-relation tuples could be affected.
+    tuple's attributes, return a filter: [(attr_name, value)] pairs that narrow
+    which constrained-relation tuples could be affected.
 
-    For a Var binding like [dept_id = Var "dept_id"] targeting [dep_rel],
-    the deleted tuple's [dept_id] value becomes the filter: only constrained
-    tuples with that exact [dept_id] need re-checking.
+    For a Var binding like [dept_id = Var "dept_id"] targeting [dep_rel], the
+    deleted tuple's [dept_id] value becomes the filter: only constrained tuples
+    with that exact [dept_id] need re-checking.
 
     Returns [] if no narrowing is possible (Const bindings, unrelated rel). *)
-let rec focused_filter (c : t) (dep_rel : relation_name)
-    (deleted : (attr_name * Conventions.AbstractValue.t) list)
-  : (attr_name * Conventions.AbstractValue.t) list =
-  match c with
-  | MemberOf { target; binding } when target = dep_rel ->
-    BindingMap.fold (fun _target_attr expr acc ->
-      match expr with
-      | Var src_attr ->
-        (match List.assoc_opt src_attr deleted with
-         | Some v -> (src_attr, v) :: acc
-         | None   -> acc)
-      | Const _ -> acc)
-      binding []
-  | MemberOf _ -> []
-  | Not { body; _ } -> focused_filter body dep_rel deleted
-  | And cs | Or cs ->
-    List.concat_map (fun c -> focused_filter c dep_rel deleted) cs
-  | Exists { body; _ } | Forall { body; _ } ->
-    focused_filter body dep_rel deleted
+let focused_filter (c : t) (dep_rel : relation_name)
+    (deleted : (attr_name * Conventions.AbstractValue.t) list) :
+    (attr_name * Conventions.AbstractValue.t) list =
+  let add_from_binding acc binding =
+    BindingMap.fold
+      (fun _target_attr expr acc ->
+        match expr with
+        | Var src_attr -> (
+            match List.assoc_opt src_attr deleted with
+            | Some v -> (src_attr, v) :: acc
+            | None -> acc)
+        | Const _ -> acc)
+      binding acc
+  in
+  let rec loop acc worklist =
+    match FingerTree.front worklist with
+    | None -> acc
+    | Some (rest, node) -> (
+        match node with
+        | MemberOf { target; binding } when target = dep_rel ->
+            loop (add_from_binding acc binding) rest
+        | MemberOf _ -> loop acc rest
+        | Not { body; _ } | Exists { body; _ } | Forall { body; _ } ->
+            loop acc (FingerTree.cons rest body)
+        | And cs | Or cs ->
+            let next = FingerTree.append (FingerTree.of_list cs) rest in
+            loop acc next)
+  in
+  loop [] (FingerTree.singleton c)
 
 (** Extract Const binding values from a constraint for a given [dep_rel].
 
-    These are fixed-value preconditions: if the deleted tuple doesn't have
-    these exact values, the constraint cannot be violated by the deletion.
-    The cascade checker uses this to bail out early. *)
-let rec trigger_constants (c : t) (dep_rel : relation_name)
-  : (attr_name * Conventions.AbstractValue.t) list =
-  match c with
-  | MemberOf { target; binding } when target = dep_rel ->
-    BindingMap.fold (fun target_attr expr acc ->
-      match expr with
-      | Const v -> (target_attr, v) :: acc
-      | Var _   -> acc)
-      binding []
-  | MemberOf _ -> []
-  | Not { body; _ } -> trigger_constants body dep_rel
-  | And cs | Or cs ->
-    List.concat_map (fun c -> trigger_constants c dep_rel) cs
-  | Exists { body; _ } | Forall { body; _ } ->
-    trigger_constants body dep_rel
+    These are fixed-value preconditions: if the deleted tuple doesn't have these
+    exact values, the constraint cannot be violated by the deletion. The cascade
+    checker uses this to bail out early. *)
+let trigger_constants (c : t) (dep_rel : relation_name) :
+    (attr_name * Conventions.AbstractValue.t) list =
+  let add_from_binding acc binding =
+    BindingMap.fold
+      (fun target_attr expr acc ->
+        match expr with Const v -> (target_attr, v) :: acc | Var _ -> acc)
+      binding acc
+  in
+  let rec loop acc worklist =
+    match FingerTree.front worklist with
+    | None -> acc
+    | Some (rest, node) -> (
+        match node with
+        | MemberOf { target; binding } when target = dep_rel ->
+            loop (add_from_binding acc binding) rest
+        | MemberOf _ -> loop acc rest
+        | Not { body; _ } | Exists { body; _ } | Forall { body; _ } ->
+            loop acc (FingerTree.cons rest body)
+        | And cs | Or cs ->
+            let next = FingerTree.append (FingerTree.of_list cs) rest in
+            loop acc next)
+  in
+  loop [] (FingerTree.singleton c)
 
 (** Substitute transition tuple values into a constraint for universal variable
     substitution. When [dep_rel] is being mutated (deleted from or inserted
@@ -388,85 +419,175 @@ let rec trigger_constants (c : t) (dep_rel : relation_name)
 
     The convention that quantifier attributes are namespaced as [variable.attr]
     (established by [extend_tuple]) means base tuple [Var] references like
-    [Var "dept_id"] are never substituted, only [Var "d.dept_id"] would match
-    a quantifier variable [d] over a deleted [Department] row.
+    [Var "dept_id"] are never substituted, only [Var "d.dept_id"] would match a
+    quantifier variable [d] over a deleted [Department] row.
 
     This transforms the recheck from a full relation evaluation into a targeted
-    expression that tests only the rows affected by the transition tuple.
-    See Technique 2 in docs/incremental_constraint_checking.org. *)
-let substitute_transition
-    (c : t)
-    (dep_rel : relation_name)
-    (transition : (attr_name * Conventions.AbstractValue.t) list)
-  : t =
+    expression that tests only the rows affected by the transition tuple. See
+    Technique 2 in docs/incremental_constraint_checking.org. *)
+let substitute_transition (c : t) (dep_rel : relation_name)
+    (transition : (attr_name * Conventions.AbstractValue.t) list) : t =
+  let namespaced_subs variable =
+    List.fold_left
+      (fun acc (a, v) -> BindingMap.add (variable ^ "." ^ a) v acc)
+      BindingMap.empty transition
+  in
+  let enqueue_visit_then_build visit build rest =
+    FingerTree.cons (FingerTree.cons rest build) visit
+  in
+  let enqueue_children mode cs build_of_count rest =
+    let prefix, count =
+      List.fold_left
+        (fun (acc, n) child ->
+          (FingerTree.snoc acc (Visit (mode, child)), n + 1))
+        (FingerTree.empty, 0) cs
+    in
+    let prefix = FingerTree.snoc prefix (build_of_count count) in
+    FingerTree.append prefix rest
+  in
   let apply_subs subs binding =
-    BindingMap.map (function
-      | Var v -> (match List.assoc_opt v subs with
-                  | Some value -> Const value
-                  | None -> Var v)
-      | Const _ as expr -> expr)
+    BindingMap.map
+      (function
+        | Var v -> (
+            match BindingMap.find_opt v subs with
+            | Some value -> Const value
+            | None -> Var v)
+        | Const _ as expr -> expr)
       binding
   in
-  let rec sub_body subs = function
-    | MemberOf { target; binding } ->
-      MemberOf { target; binding = apply_subs subs binding }
-    | Not { body; universe } -> Not { body = sub_body subs body; universe }
-    | And cs -> And (List.map (sub_body subs) cs)
-    | Or cs  -> Or  (List.map (sub_body subs) cs)
-    | Exists { variable; quantifier; body } ->
-      Exists { variable; quantifier; body = sub_body subs body }
-    | Forall { variable; quantifier; body } ->
-      Forall { variable; quantifier; body = sub_body subs body }
+  let rec pop_n n vals acc =
+    if n = 0 then (acc, vals)
+    else
+      match vals with
+      | [] -> (acc, [])
+      | v :: rest -> pop_n (n - 1) rest (v :: acc)
   in
-  let rec go = function
-    | MemberOf _ as leaf -> leaf
-    | Not { body; universe } -> Not { body = go body; universe }
-    | And cs -> And (List.map go cs)
-    | Or cs  -> Or  (List.map go cs)
-    | Exists { variable; quantifier; body } ->
-      let body' =
-        if quantifier = dep_rel then
-          sub_body (List.map (fun (a, v) -> (variable ^ "." ^ a, v)) transition) body
-        else go body
-      in
-      Exists { variable; quantifier; body = body' }
-    | Forall { variable; quantifier; body } ->
-      let body' =
-        if quantifier = dep_rel then
-          sub_body (List.map (fun (a, v) -> (variable ^ "." ^ a, v)) transition) body
-        else go body
-      in
-      Forall { variable; quantifier; body = body' }
+  let rec loop instrs vals =
+    match FingerTree.front instrs with
+    | None -> ( match vals with [ result ] -> result | _ -> c)
+    | Some (rest, instr) -> (
+        match instr with
+        | Visit (mode, node) -> (
+            match node with
+            | MemberOf { target; binding } ->
+                let binding' =
+                  match mode with
+                  | SubstituteGo -> binding
+                  | SubstituteApply subs -> apply_subs subs binding
+                in
+                loop rest (MemberOf { target; binding = binding' } :: vals)
+            | Not { body; universe } ->
+                loop
+                  (enqueue_visit_then_build
+                     (Visit (mode, body))
+                     (BuildNot universe) rest)
+                  vals
+            | And cs ->
+                let instrs' =
+                  enqueue_children mode cs (fun n -> BuildAnd n) rest
+                in
+                loop instrs' vals
+            | Or cs ->
+                let instrs' =
+                  enqueue_children mode cs (fun n -> BuildOr n) rest
+                in
+                loop instrs' vals
+            | Exists { variable; quantifier; body } ->
+                let body_mode =
+                  match mode with
+                  | SubstituteApply subs -> SubstituteApply subs
+                  | SubstituteGo ->
+                      if quantifier = dep_rel then
+                        SubstituteApply (namespaced_subs variable)
+                      else SubstituteGo
+                in
+                loop
+                  (enqueue_visit_then_build
+                     (Visit (body_mode, body))
+                     (BuildExists (variable, quantifier))
+                     rest)
+                  vals
+            | Forall { variable; quantifier; body } ->
+                let body_mode =
+                  match mode with
+                  | SubstituteApply subs -> SubstituteApply subs
+                  | SubstituteGo ->
+                      if quantifier = dep_rel then
+                        SubstituteApply (namespaced_subs variable)
+                      else SubstituteGo
+                in
+                loop
+                  (enqueue_visit_then_build
+                     (Visit (body_mode, body))
+                     (BuildForall (variable, quantifier))
+                     rest)
+                  vals)
+        | BuildNot universe -> (
+            match vals with
+            | body :: vals' -> loop rest (Not { body; universe } :: vals')
+            | [] -> loop rest vals)
+        | BuildAnd n ->
+            let children, vals' = pop_n n vals [] in
+            loop rest (And children :: vals')
+        | BuildOr n ->
+            let children, vals' = pop_n n vals [] in
+            loop rest (Or children :: vals')
+        | BuildExists (variable, quantifier) -> (
+            match vals with
+            | body :: vals' ->
+                loop rest (Exists { variable; quantifier; body } :: vals')
+            | [] -> loop rest vals)
+        | BuildForall (variable, quantifier) -> (
+            match vals with
+            | body :: vals' ->
+                loop rest (Forall { variable; quantifier; body } :: vals')
+            | [] -> loop rest vals))
   in
-  go c
+  loop (FingerTree.singleton (Visit (SubstituteGo, c))) []
 
 let make_comparison_binding ~left ~right =
-  BindingMap.empty
-  |> BindingMap.add "left" left
-  |> BindingMap.add "right" 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 }
+  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 }
+  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 }
+  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 }
+  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 }
+  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 }
+    [
+      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/constraint.mli b/lib/constraint.mli
new file mode 100644
index 0000000..c86ef89
--- /dev/null
+++ b/lib/constraint.mli
@@ -0,0 +1,91 @@
+type relation_name = string
+type attr_name = string
+type binding_expr = Var of attr_name | Const of Conventions.AbstractValue.t
+
+module BindingMap : Map.S with type key = String.t
+
+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 : attr_name; quantifier : relation_name; body : t }
+  | Forall of { variable : attr_name; quantifier : relation_name; body : t }
+
+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
+
+val vars_in : t -> attr_name list
+val rename_vars : (attr_name * attr_name) list -> t -> t
+val filter_by_attrs : attr_name list -> t -> t option
+val merge : (string * t) list -> (string * t) list -> (string * t) list
+val member_of : target:relation_name -> binding:binding -> t
+val not_ : universe:relation_name -> t -> t
+val and_ : t list -> t
+val or_ : t list -> t
+val exists : variable:attr_name -> quantifier:relation_name -> t -> t
+val forall : variable:attr_name -> quantifier:relation_name -> t -> t
+
+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;
+}
+
+val bind :
+  binding ->
+  Tuple.materialized ->
+  (attr_name * Conventions.AbstractValue.t) list
+
+val evaluate :
+  eval_context -> Tuple.materialized -> t -> (bool, diagnostic) result
+
+val evaluate_named :
+  eval_context ->
+  Tuple.materialized ->
+  (string * t) list ->
+  (bool, diagnostic) result
+
+val evaluate_first_failure :
+  eval_context ->
+  Tuple.materialized ->
+  (string * t) list ->
+  (bool, diagnostic) result
+
+type polarity = Positive | Negative | Both
+type polarity_index
+
+val polarity_of : ?neg:bool -> t -> polarity_index
+val polarity_find : relation_name -> polarity_index -> polarity option
+
+type timing = Immediate | Deferred
+
+val focused_filter :
+  t ->
+  relation_name ->
+  (attr_name * Conventions.AbstractValue.t) list ->
+  (attr_name * Conventions.AbstractValue.t) list
+
+val trigger_constants :
+  t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list
+
+val substitute_transition :
+  t -> relation_name -> (attr_name * Conventions.AbstractValue.t) list -> t
+
+val make_comparison_binding : left:binding_expr -> right:binding_expr -> binding
+val lt : left:binding_expr -> right:binding_expr -> t
+val lte : left:binding_expr -> right:binding_expr -> t
+val gt : left:binding_expr -> right:binding_expr -> t
+val gte : left:binding_expr -> right:binding_expr -> t
+val eq : left:binding_expr -> right:binding_expr -> t
+val neq : left:binding_expr -> right:binding_expr -> t
+val between : value:binding_expr -> low:binding_expr -> high:binding_expr -> t
diff --git a/lib/dune b/lib/dune
index 406749d..9b7462c 100644
--- a/lib/dune
+++ b/lib/dune
@@ -8,6 +8,7 @@
   lwt
   lwt.unix
   lwt-exit
+  batteries
   ppx_protocol_conv_xml_light
   sexplib)
  (preprocess
diff --git a/lib/icl/executor.ml b/lib/icl/executor.ml
index 591f839..07d0978 100644
--- a/lib/icl/executor.ml
+++ b/lib/icl/executor.ml
@@ -1,58 +1,56 @@
 module Make (Storage : Management.Physical.S) = struct
-  module Ops = Manipulation.Make(Storage)
+  module Ops = Manipulation.Make (Storage)
 
   type error =
-    | ParseError        of string
+    | ParseError of string
     | ManipulationError of Manipulation.error
-    | ConversionError   of string
+    | ConversionError of string
 
   let sexp_of_error e =
     let open Sexplib.Sexp in
     match e with
-    | ParseError s        -> List [Atom "parse-error";      Atom s]
+    | ParseError s -> List [ Atom "parse-error"; Atom s ]
     | ManipulationError e -> Manipulation.sexp_of_error e
-    | ConversionError s   -> List [Atom "conversion-error"; Atom s]
+    | ConversionError s -> List [ Atom "conversion-error"; Atom s ]
 
   let wrap_manip = Result.map_error (fun e -> ManipulationError e)
 
-  let convert_binding_expr : Ast.binding_expr -> Constraint.binding_expr = function
+  let convert_binding_expr : Ast.binding_expr -> Constraint.binding_expr =
+    function
     | Ast.Var name -> Constraint.Var name
     | Ast.Const value -> Constraint.Const (Drl.Ast.value_to_abstract value)
 
-  let convert_binding (pairs : (string * Ast.binding_expr) list) : Constraint.binding =
+  let convert_binding (pairs : (string * Ast.binding_expr) list) :
+      Constraint.binding =
     List.fold_left
       (fun acc (key, expr) ->
         Constraint.BindingMap.add key (convert_binding_expr expr) acc)
-      Constraint.BindingMap.empty
-      pairs
+      Constraint.BindingMap.empty pairs
 
   let rec convert_body : Ast.constraint_body -> Constraint.t = function
     | Ast.MemberOf { target; binding } ->
-      Constraint.MemberOf { target; binding = convert_binding binding }
+        Constraint.member_of ~target ~binding:(convert_binding binding)
     | Ast.Not { body; universe } ->
-      Constraint.Not { body = convert_body body; universe }
-    | Ast.And bodies ->
-      Constraint.And (List.map convert_body bodies)
-    | Ast.Or bodies ->
-      Constraint.Or (List.map convert_body bodies)
+        Constraint.not_ ~universe (convert_body body)
+    | Ast.And bodies -> Constraint.and_ (List.map convert_body bodies)
+    | Ast.Or bodies -> Constraint.or_ (List.map convert_body bodies)
     | Ast.Exists { variable; quantifier; body } ->
-      Constraint.Exists { variable; quantifier; body = convert_body body }
+        Constraint.exists ~variable ~quantifier (convert_body body)
     | Ast.Forall { variable; quantifier; body } ->
-      Constraint.Forall { variable; quantifier; body = convert_body body }
+        Constraint.forall ~variable ~quantifier (convert_body body)
 
-  let execute
-      (storage : Storage.t)
-      (db : Management.Database.t)
-      (stmt : Ast.statement)
-    : (Management.Database.t * string, error) result =
+  let execute (storage : Storage.t) (db : Management.Database.t)
+      (stmt : Ast.statement) : (Management.Database.t * string, error) result =
     match stmt with
-    | Ast.RegisterConstraint { constraint_name; relation_name; body } ->
-      let runtime_body = convert_body body in
-      (match Ops.register_constraint storage db
-               ~constraint_name ~relation_name ~body:runtime_body
-             |> wrap_manip with
-       | Ok new_db -> Ok (new_db, "Constraint registered: " ^ constraint_name)
-       | Error e   -> Error e)
+    | Ast.RegisterConstraint { constraint_name; relation_name; body } -> (
+        let runtime_body = convert_body body in
+        match
+          Ops.register_constraint storage db ~constraint_name ~relation_name
+            ~body:runtime_body
+          |> wrap_manip
+        with
+        | Ok new_db -> Ok (new_db, "Constraint registered: " ^ constraint_name)
+        | Error e -> Error e)
 end
 
-module Memory = Make(Management.Physical.Memory)
+module Memory = Make (Management.Physical.Memory)
diff --git a/lib/management/database.ml b/lib/management/database.ml
index c4c6dc3..f4d18e8 100644
--- a/lib/management/database.ml
+++ b/lib/management/database.ml
@@ -1,12 +1,12 @@
 (** Database state: a named collection of relations with a Merkle tree over
-    their hashes, a domain registry, and a history chain of prior hashes.
-    All mutations produce a new value; no in-place update. *)
+    their hashes, a domain registry, and a history chain of prior hashes. All
+    mutations produce a new value; no in-place update. *)
 
 (* TODO: history is an unbounded list of hashes; there is no way to
    reconstruct a past state from a hash alone without a separate snapshot
    store. Either cap the history or make it actually useful. *)
 
-module RelationMap = Map.Make(String)
+module RelationMap = Map.Make (String)
 
 type deferred_entry = {
   relation_name : string;
@@ -25,16 +25,17 @@ type t = {
   deferred : deferred_entry list;
 }
 
-let empty ~name = {
-  hash = "";
-  name;
-  tree = Merkle.empty;
-  relations = RelationMap.empty;
-  domains = RelationMap.empty;
-  history = [];
-  timestamp = Unix.gettimeofday ();
-  deferred = [];
-}
+let empty ~name =
+  {
+    hash = "";
+    name;
+    tree = Merkle.empty;
+    relations = RelationMap.empty;
+    domains = RelationMap.empty;
+    history = [];
+    timestamp = Unix.gettimeofday ();
+    deferred = [];
+  }
 
 let compute_hash db =
   match Merkle.root_hash db.tree with
@@ -44,8 +45,8 @@ let compute_hash db =
 let max_history = 128
 
 let rec take_at_most n = function
-  | []      -> []
-  | _  when n = 0 -> []
+  | [] -> []
+  | _ when n = 0 -> []
   | x :: xs -> x :: take_at_most (n - 1) xs
 
 let update_state db ~relations ~tree =
@@ -58,9 +59,16 @@ let update_state db ~relations ~tree =
     if db.hash = "" then db.history
     else take_at_most max_history (db.hash :: db.history)
   in
-  { hash = new_hash; name = db.name; tree; relations;
-    domains = db.domains; history; timestamp = Unix.gettimeofday ();
-    deferred = db.deferred }
+  {
+    hash = new_hash;
+    name = db.name;
+    tree;
+    relations;
+    domains = db.domains;
+    history;
+    timestamp = Unix.gettimeofday ();
+    deferred = db.deferred;
+  }
 
 let get_relation db name = RelationMap.find_opt name db.relations
 
@@ -74,16 +82,18 @@ let get_relation_names db =
 
 let has_relation db name = RelationMap.mem name db.relations
 
+let relation_hash_or_compute (relation : Relation.t) =
+  match relation.hash with
+  | Some h -> h
+  | None ->
+      let tree = Option.value relation.tree ~default:Merkle.empty in
+      Hashing.hash_relation ~name:relation.name ~schema:relation.schema ~tree
+
 (* TODO: computing the hash here for hash:None relations (ephemeral/prelude)
    is a layering violation — callers should assign the hash before calling
    add_relation, not rely on this fallback. *)
 let add_relation db ~(relation : Relation.t) =
-  let relation_hash = match relation.hash with
-    | Some h -> h
-    | None ->
-      let tree = Option.value relation.tree ~default:Merkle.empty in
-      Hashing.hash_relation ~name:relation.name ~schema:relation.schema ~tree
-  in
+  let relation_hash = relation_hash_or_compute relation in
   let relation = { relation with hash = Some relation_hash } in
   let tree = Merkle.insert relation_hash db.tree in
   let relations = RelationMap.add relation.name relation db.relations in
@@ -93,21 +103,21 @@ let remove_relation db ~name =
   match RelationMap.find_opt name db.relations with
   | None -> db
   | Some relation ->
-    let relation_hash = Option.get relation.hash in
-    let tree = Merkle.delete relation_hash db.tree in
-    let relations = RelationMap.remove name db.relations in
-    update_state db ~relations ~tree
+      let relation_hash = relation_hash_or_compute relation in
+      let tree = Merkle.delete relation_hash db.tree in
+      let relations = RelationMap.remove name db.relations in
+      update_state db ~relations ~tree
 
 let update_relation db ~(relation : Relation.t) =
   let name = relation.name in
   match RelationMap.find_opt name db.relations with
   | None -> db
   | Some old_relation ->
-    let old_hash = Option.get old_relation.hash in
-    let new_hash = Option.get relation.hash in
-    let tree = db.tree |> Merkle.delete old_hash |> Merkle.insert new_hash in
-    let relations = RelationMap.add name relation db.relations in
-    update_state db ~relations ~tree
+      let old_hash = relation_hash_or_compute old_relation in
+      let new_hash = relation_hash_or_compute relation in
+      let tree = db.tree |> Merkle.delete old_hash |> Merkle.insert new_hash in
+      let relations = RelationMap.add name relation db.relations in
+      update_state db ~relations ~tree
 
 let add_domain db (domain : Domain.t) =
   { db with domains = RelationMap.add domain.name domain db.domains }
diff --git a/lib/management/diff.ml b/lib/management/diff.ml
index 865c757..8fca0af 100644
--- a/lib/management/diff.ml
+++ b/lib/management/diff.ml
@@ -1,24 +1,24 @@
-(** Structural delta between two Database.t states.
-    Computes what changed from ancestor → target at the relation level. *)
+(** Structural delta between two Database.t states. Computes what changed from
+    ancestor -> target at the relation level. *)
 
 type relation_diff =
-  | RelationAdded   of Relation.t
+  | RelationAdded of Relation.t
   | RelationRemoved of string
   | RelationModified of {
-      name           : string;
-      added_tuples   : Conventions.Hash.t list;
+      name : string;
+      added_tuples : Conventions.Hash.t list;
       removed_tuples : Conventions.Hash.t list;
       schema_changed : bool;
     }
 
 type t = {
-  ancestor       : Conventions.Hash.t;
-  left           : Conventions.Hash.t;
-  right          : Conventions.Hash.t;
+  ancestor : Conventions.Hash.t;
+  left : Conventions.Hash.t;
+  right : Conventions.Hash.t;
   relation_diffs : relation_diff list;
 }
 
-module StringSet = Set.Make(String)
+module StringSet = Set.Make (String)
 
 let relation_keys rel =
   match rel.Relation.tree with
@@ -30,31 +30,41 @@ let diff ~ancestor ~(target : Database.t) =
   let ancestor_names =
     Database.get_relation_names ancestor |> StringSet.of_list
   in
-  let target_names =
-    Database.get_relation_names target |> StringSet.of_list
-  in
+  let target_names = Database.get_relation_names target |> StringSet.of_list in
   let all_names = StringSet.union ancestor_names target_names in
-  StringSet.fold (fun name acc ->
-    let in_ancestor = StringSet.mem name ancestor_names in
-    let in_target   = StringSet.mem name target_names   in
-    match in_ancestor, in_target with
-    | false, true ->
-      let rel = Option.get (Database.get_relation target name) in
-      RelationAdded rel :: acc
-    | true, false ->
-      RelationRemoved name :: acc
-    | true, true ->
-      let anc_rel = Option.get (Database.get_relation ancestor name) in
-      let tgt_rel = Option.get (Database.get_relation target  name) in
-      (* Compare hashes — if identical, no diff *)
-      if anc_rel.Relation.hash = tgt_rel.Relation.hash then acc
-      else begin
-        let anc_keys = relation_keys anc_rel in
-        let tgt_keys = relation_keys tgt_rel in
-        let added_tuples   = StringSet.diff tgt_keys anc_keys |> StringSet.elements in
-        let removed_tuples = StringSet.diff anc_keys tgt_keys |> StringSet.elements in
-        let schema_changed = anc_rel.Relation.schema <> tgt_rel.Relation.schema in
-        RelationModified { name; added_tuples; removed_tuples; schema_changed } :: acc
-      end
-    | false, false -> acc (* impossible *)
-  ) all_names []
+  StringSet.fold
+    (fun name acc ->
+      let in_ancestor = StringSet.mem name ancestor_names in
+      let in_target = StringSet.mem name target_names in
+      match (in_ancestor, in_target) with
+      | false, true -> (
+          match Database.get_relation target name with
+          | Some rel -> RelationAdded rel :: acc
+          | None -> acc)
+      | true, false -> RelationRemoved name :: acc
+      | true, true -> (
+          match
+            ( Database.get_relation ancestor name,
+              Database.get_relation target name )
+          with
+          | Some anc_rel, Some tgt_rel ->
+              (* Compare hashes — if identical, no diff *)
+              if anc_rel.Relation.hash = tgt_rel.Relation.hash then acc
+              else
+                let anc_keys = relation_keys anc_rel in
+                let tgt_keys = relation_keys tgt_rel in
+                let added_tuples =
+                  StringSet.diff tgt_keys anc_keys |> StringSet.elements
+                in
+                let removed_tuples =
+                  StringSet.diff anc_keys tgt_keys |> StringSet.elements
+                in
+                let schema_changed =
+                  anc_rel.Relation.schema <> tgt_rel.Relation.schema
+                in
+                RelationModified
+                  { name; added_tuples; removed_tuples; schema_changed }
+                :: acc
+          | _ -> acc)
+      | false, false -> acc (* impossible *))
+    all_names []
diff --git a/lib/manipulation.ml b/lib/manipulation.ml
index 58e6cbb..b44cc53 100644
--- a/lib/manipulation.ml
+++ b/lib/manipulation.ml
@@ -9,8 +9,8 @@
     All operations are immutable: they return new database/relation states
     rather than modifying existing ones. The storage layer handles persistence.
 
-    This is a functor that takes a storage backend, ensuring all tuple data
-    is properly persisted to the content-addressed store. *)
+    This is a functor that takes a storage backend, ensuring all tuple data is
+    properly persisted to the content-addressed store. *)
 
 module RelationMap = Management.Database.RelationMap
 
@@ -24,28 +24,28 @@ type error =
   | StorageError of string
 
 let string_of_error = function
-  | RelationNotFound s      -> "RelationNotFound: " ^ s
+  | RelationNotFound s -> "RelationNotFound: " ^ s
   | RelationAlreadyExists s -> "RelationAlreadyExists: " ^ s
-  | TupleNotFound h         -> "TupleNotFound: " ^ h
-  | DuplicateTuple h        -> "DuplicateTuple: " ^ h
-  | ConstraintViolation s   -> "ConstraintViolation: " ^ s
-  | StorageError s          -> "StorageError: " ^ s
+  | TupleNotFound h -> "TupleNotFound: " ^ h
+  | DuplicateTuple h -> "DuplicateTuple: " ^ h
+  | ConstraintViolation s -> "ConstraintViolation: " ^ s
+  | StorageError s -> "StorageError: " ^ s
 
 let sexp_of_error e =
   let open Sexplib.Sexp in
   match e with
-  | RelationNotFound s      -> List [Atom "relation-not-found";      Atom s]
-  | RelationAlreadyExists s -> List [Atom "relation-already-exists"; Atom s]
-  | TupleNotFound h         -> List [Atom "tuple-not-found";         Atom h]
-  | DuplicateTuple h        -> List [Atom "duplicate-tuple";         Atom h]
-  | ConstraintViolation s   -> List [Atom "constraint-violation";    Atom s]
-  | StorageError s          -> List [Atom "storage-error";           Atom s]
+  | RelationNotFound s -> List [ Atom "relation-not-found"; Atom s ]
+  | RelationAlreadyExists s -> List [ Atom "relation-already-exists"; Atom s ]
+  | TupleNotFound h -> List [ Atom "tuple-not-found"; Atom h ]
+  | DuplicateTuple h -> List [ Atom "duplicate-tuple"; Atom h ]
+  | ConstraintViolation s -> List [ Atom "constraint-violation"; Atom s ]
+  | StorageError s -> List [ Atom "storage-error"; Atom s ]
 
-(** Result type for operations *)
 type 'a result = ('a, error) Result.t
+(** Result type for operations *)
 
-(** Re-export Schema for convenience *)
 module Schema = Schema
+(** Re-export Schema for convenience *)
 
 (** Re-export hashing functions for convenience *)
 let hash_tuple = Hashing.hash_tuple
@@ -55,131 +55,161 @@ let build_base_provenance _schema relation_name =
   Relation.Provenance.Base relation_name
 
 (** Build membership criteria from schema (validates type membership) *)
-let build_membership_criteria _schema : (Tuple.t -> bool) =
-  (* For now, accept all tuples. Full implementation would check domain membership. *)
-  fun _ -> true
+let build_membership_criteria _schema : Tuple.t -> bool =
+ (* For now, accept all tuples. Full implementation would check domain membership. *)
+ fun _ ->
+  true
+
+(** Mutation direction for cascade constraint checking *)
+type mutation_kind = Insert | Delete
+
+type mutation_context = {
+  dep_rel : string;
+  transition : (string * Conventions.AbstractValue.t) list;
+  kind : mutation_kind;
+}
+(** Context for a single tuple mutation, used by cascade checking *)
 
 (** Functor to create manipulation operations with a storage backend *)
 module Make (Storage : Management.Physical.S) = struct
   type storage = Storage.t
   type nonrec error = error
+
   let of_string_error s = StorageError s
+  let ( let* ) = Result.bind
+
+  let fold_result (f : 'a -> 'b -> ('a, error) Result.t) (init : 'a)
+      (xs : 'b list) : ('a, error) Result.t =
+    List.fold_left
+      (fun acc x ->
+        let* a = acc in
+        f a x)
+      (Ok init) xs
 
   (* 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 =
+  (** 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
+      | 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)
+          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
-                  (match load_attrs [] stored.Storable.Tuple.attributes with
-                   | None -> None
-                   | Some pairs -> load_all (pairs :: acc) rest))
-            in
-            load_all [] hashes)
-        | _ -> None)
+                  load_all [] hashes)
+          | _ -> None)
     in
     { Constraint.check_membership; iterate_finite }
 
   (* State Persistence - Store relation and database states *)
 
   (** Store a relation state to storage *)
-  let store_relation (storage : storage) (relation : Relation.t) : (unit, error) Result.t =
+  let store_relation (storage : storage) (relation : Relation.t) :
+      (unit, error) Result.t =
     match relation.hash with
     | None -> Error (StorageError "Relation has no hash")
-    | Some rel_hash ->
-      let tree_keys = match relation.tree with
-        | None -> []
-        | Some tree -> Merkle.keys tree
-      in
-      let stored : Storable.Relation.t = {
-        name = relation.name;
-        schema = relation.schema;
-        tree_keys;
-        cardinality = relation.cardinality;
-      } in
-      match Storage.store_raw storage rel_hash (Storable.Relation.to_bytes stored) with
-      | Error _ -> Error (StorageError "Failed to store relation")
-      | Ok () -> Ok ()
+    | Some rel_hash -> (
+        let tree_keys =
+          match relation.tree with None -> [] | Some tree -> Merkle.keys tree
+        in
+        let stored : Storable.Relation.t =
+          {
+            name = relation.name;
+            schema = relation.schema;
+            tree_keys;
+            cardinality = relation.cardinality;
+          }
+        in
+        match
+          Storage.store_raw storage rel_hash (Storable.Relation.to_bytes stored)
+        with
+        | Error _ -> Error (StorageError "Failed to store relation")
+        | Ok () -> Ok ())
 
   (** Store a database state to storage *)
-  let store_database (storage : storage) (db : Management.Database.t) : (unit, error) Result.t =
-    if db.hash = "" then
-      Ok ()  (* Don't store empty/initial database *)
+  let store_database (storage : storage) (db : Management.Database.t) :
+      (unit, error) Result.t =
+    if db.hash = "" then Ok () (* Don't store empty/initial database *)
     else
       (* Extract relation hashes from the actual relations *)
       let relation_hashes =
@@ -188,638 +218,576 @@ module Make (Storage : Management.Physical.S) = struct
             match rel.Relation.hash with
             | Some h -> (name, h) :: acc
             | None -> acc)
-          db.relations
-          []
+          db.relations []
       in
-      let stored : Storable.Database.t = {
-        name = db.name;
-        relations = relation_hashes;
-        tree_keys = Merkle.keys db.tree;
-        history = db.history;
-        timestamp = db.timestamp;
-      } in
-      match Storage.store_raw storage db.hash (Storable.Database.to_bytes stored) with
+      let stored : Storable.Database.t =
+        {
+          name = db.name;
+          relations = relation_hashes;
+          tree_keys = Merkle.keys db.tree;
+          history = db.history;
+          timestamp = db.timestamp;
+        }
+      in
+      match
+        Storage.store_raw storage db.hash (Storable.Database.to_bytes stored)
+      with
       | Error _ -> Error (StorageError "Failed to store database")
       | Ok () -> Ok ()
 
   (** Load a relation state from storage by hash *)
-  let load_relation (storage : storage) (rel_hash : Conventions.Hash.t)
-    : (Relation.t option, error) Result.t =
+  let load_relation (storage : storage) (rel_hash : Conventions.Hash.t) :
+      (Relation.t option, error) Result.t =
     match Storage.load_raw storage rel_hash with
     | Error _ -> Error (StorageError "Failed to load relation")
     | Ok None -> Ok None
     | Ok (Some bytes) ->
-      let stored = Storable.Relation.of_bytes bytes in
-      let tree = List.fold_left (fun t h -> Merkle.insert h t) Merkle.empty stored.tree_keys in
-      let relation = Relation.make
-        ~hash:(Some rel_hash)
-        ~name:stored.name
-        ~schema:stored.schema
-        ~tree:(Some tree)
-        ~constraints:None
-        ~cardinality:stored.cardinality
-        ~generator:None
-        ~membership_criteria:(build_membership_criteria stored.schema)
-        ~provenance:(build_base_provenance stored.schema stored.name)
-        ~lineage:(Relation.Lineage.Base stored.name)
-      in
-      Ok (Some relation)
+        let stored = Storable.Relation.of_bytes bytes in
+        let tree =
+          List.fold_left
+            (fun t h -> Merkle.insert h t)
+            Merkle.empty stored.tree_keys
+        in
+        let relation =
+          Relation.make ~hash:(Some rel_hash) ~name:stored.name
+            ~schema:stored.schema ~tree:(Some tree) ~constraints:None
+            ~cardinality:stored.cardinality ~generator:None
+            ~membership_criteria:(build_membership_criteria stored.schema)
+            ~provenance:(build_base_provenance stored.schema stored.name)
+            ~lineage:(Relation.Lineage.Base stored.name)
+        in
+        Ok (Some relation)
 
-  (** Load a database state from storage by hash.
-      Note: This loads the database structure with relation hashes,
-      but the relations themselves need to be loaded separately. *)
-  let load_database (storage : storage) (db_hash : Conventions.Hash.t)
-    : (Management.Database.t option, error) Result.t =
+  (** Load a database state from storage by hash. Note: This loads the database
+      structure with relation hashes, but the relations themselves need to be
+      loaded separately. *)
+  let load_database (storage : storage) (db_hash : Conventions.Hash.t) :
+      (Management.Database.t option, error) Result.t =
     match Storage.load_raw storage db_hash with
     | Error _ -> Error (StorageError "Failed to load database")
     | Ok None -> Ok None
     | Ok (Some bytes) ->
-      let stored = Storable.Database.of_bytes bytes in
-      let tree = List.fold_left (fun t h -> Merkle.insert h t) Merkle.empty stored.tree_keys in
-      (* Load each relation from storage *)
-      let rec load_relations acc = function
-        | [] -> Ok (List.rev acc)
-        | (name, rel_hash) :: rest ->
-          match load_relation storage rel_hash with
-          | Error e -> Error e
-          | Ok None -> Error (StorageError ("Relation not found: " ^ name))
-          | Ok (Some rel) -> load_relations ((name, rel) :: acc) rest
-      in
-      match load_relations [] stored.relations with
-      | Error e -> Error e
-      | Ok relation_list ->
-        let relations = List.fold_left
-          (fun m (name, rel) -> Management.Database.RelationMap.add name rel m)
-          Management.Database.RelationMap.empty
-          relation_list
+        let stored = Storable.Database.of_bytes bytes in
+        let tree =
+          List.fold_left
+            (fun t h -> Merkle.insert h t)
+            Merkle.empty stored.tree_keys
         in
-        Ok (Some {
-          Management.Database.hash = db_hash;
-          name = stored.name;
-          tree;
-          relations;
-          domains = Management.Database.RelationMap.empty;
-          history = stored.history;
-          timestamp = stored.timestamp;
-          deferred = [];
-        })
+        let rec load_relations acc = function
+          | [] -> Ok (List.rev acc)
+          | (name, rel_hash) :: rest -> (
+              let* rel_opt = load_relation storage rel_hash in
+              match rel_opt with
+              | None -> Error (StorageError ("Relation not found: " ^ name))
+              | Some rel -> load_relations ((name, rel) :: acc) rest)
+        in
+        let* relation_list = load_relations [] stored.relations in
+        let relations =
+          List.fold_left
+            (fun m (name, rel) ->
+              Management.Database.RelationMap.add name rel m)
+            Management.Database.RelationMap.empty relation_list
+        in
+        Ok
+          (Some
+             {
+               Management.Database.hash = db_hash;
+               name = stored.name;
+               tree;
+               relations;
+               domains = Management.Database.RelationMap.empty;
+               history = stored.history;
+               timestamp = stored.timestamp;
+               deferred = [];
+             })
 
   (*   Relation Operations - forward declarations needed by catalog helpers
       *)
 
   (** Create a new empty relation with the given schema *)
-  let create_relation_raw
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(name : string)
-      ~(schema : Schema.t)
-    : (Management.Database.t * Relation.t) result =
+  let create_relation_raw (storage : storage) (db : Management.Database.t)
+      ~(name : string) ~(schema : Schema.t) :
+      (Management.Database.t * Relation.t) result =
     if Management.Database.has_relation db name then
       Error (RelationAlreadyExists name)
     else
       let tree = Merkle.empty in
       let relation_hash = Hashing.hash_relation ~name ~schema ~tree in
-      let relation = Relation.make
-          ~hash:(Some relation_hash)
-          ~name
-          ~schema
-          ~tree:(Some tree)
-          ~constraints:None
-          ~cardinality:(Conventions.Cardinality.Finite 0)
+      let relation =
+        Relation.make ~hash:(Some relation_hash) ~name ~schema ~tree:(Some tree)
+          ~constraints:None ~cardinality:(Conventions.Cardinality.Finite 0)
           ~generator:None
           ~membership_criteria:(build_membership_criteria schema)
           ~provenance:(build_base_provenance schema name)
           ~lineage:(Relation.Lineage.Base name)
       in
       let new_db = Management.Database.add_relation db ~relation in
-      match store_relation storage relation with
-      | Error e -> Error e
-      | Ok () -> Ok (new_db, relation)
+      let* () = store_relation storage relation in
+      Ok (new_db, relation)
 
   (* Tuple Operations - Storage Integrated *)
 
   (** Store each attribute value and return map of attr_name -> attr_hash *)
-  let store_attributes
-      (storage : storage)
-      (tuple : Tuple.materialized)
-    : ((string * Conventions.Hash.t) list, error) Result.t =
+  let store_attributes (storage : storage) (tuple : Tuple.materialized) :
+      ((string * Conventions.Hash.t) list, error) Result.t =
     let attrs = Tuple.AttributeMap.bindings tuple.attributes in
     let rec store_all acc = function
       | [] -> Ok (List.rev acc)
-      | (name, attr) :: rest ->
-        let value_bytes = Marshal.to_bytes attr.Attribute.value [Marshal.Closures] in
-        let value_hash = Conventions.Hash.hash_text (Hashing.bytes_to_hex value_bytes) in
-        match Storage.store_raw storage value_hash value_bytes with
-        | Error _ -> Error (StorageError ("Failed to store attribute: " ^ name))
-        | Ok () -> store_all ((name, value_hash) :: acc) rest
+      | (name, attr) :: rest -> (
+          let value_bytes =
+            Marshal.to_bytes attr.Attribute.value [ Marshal.Closures ]
+          in
+          let value_hash =
+            Conventions.Hash.hash_text (Hashing.bytes_to_hex value_bytes)
+          in
+          match Storage.store_raw storage value_hash value_bytes with
+          | Error _ ->
+              Error (StorageError ("Failed to store attribute: " ^ name))
+          | Ok () -> store_all ((name, value_hash) :: acc) rest)
     in
     store_all [] attrs
 
   (** Load a tuple from storage by its hash *)
-  let load_tuple
-      (storage : storage)
-      (tuple_hash : Conventions.Hash.t)
-    : (Tuple.materialized option, error) Result.t =
+  let load_tuple (storage : storage) (tuple_hash : Conventions.Hash.t) :
+      (Tuple.materialized option, error) Result.t =
     match Storage.load_raw storage tuple_hash with
     | Error _ -> Error (StorageError "Failed to load tuple")
     | Ok None -> Ok None
     | Ok (Some tuple_bytes) ->
-      let stored = Storable.Tuple.of_bytes tuple_bytes in
-      let rec load_attrs acc = function
-        | [] -> Ok (List.rev acc)
-        | (name, attr_hash) :: rest ->
-          match Storage.load_raw storage attr_hash with
-          | Error _ -> Error (StorageError ("Failed to load attribute: " ^ name))
-          | Ok None -> Error (StorageError ("Attribute not found: " ^ name))
-          | Ok (Some value_bytes) ->
-            let value : Conventions.AbstractValue.t = Marshal.from_bytes value_bytes 0 in
-            let attr : Attribute.materialized = { value } in
-            load_attrs ((name, attr) :: acc) rest
-      in
-      match load_attrs [] stored.attributes with
-      | Error e -> Error e
-      | Ok attrs ->
-        let attributes = List.fold_left
+        let stored = Storable.Tuple.of_bytes tuple_bytes in
+        let rec load_attrs acc = function
+          | [] -> Ok (List.rev acc)
+          | (name, attr_hash) :: rest -> (
+              match Storage.load_raw storage attr_hash with
+              | Error _ ->
+                  Error (StorageError ("Failed to load attribute: " ^ name))
+              | Ok None -> Error (StorageError ("Attribute not found: " ^ name))
+              | Ok (Some value_bytes) ->
+                  let value : Conventions.AbstractValue.t =
+                    Marshal.from_bytes value_bytes 0
+                  in
+                  let attr : Attribute.materialized = { value } in
+                  load_attrs ((name, attr) :: acc) rest)
+        in
+        let* attrs = load_attrs [] stored.attributes in
+        let attributes =
+          List.fold_left
             (fun m (k, v) -> Tuple.AttributeMap.add k v m)
             Tuple.AttributeMap.empty attrs
         in
         Ok (Some { Tuple.relation = stored.relation; attributes })
 
   (** Load multiple tuples from storage *)
-  let load_tuples
-      (storage : storage)
-      (hashes : Conventions.Hash.t list)
-    : (Tuple.materialized list, error) Result.t =
+  let load_tuples (storage : storage) (hashes : Conventions.Hash.t list) :
+      (Tuple.materialized list, error) Result.t =
     let rec load_all acc = function
       | [] -> Ok (List.rev acc)
-      | hash :: rest ->
-        match load_tuple storage hash with
-        | Error e -> Error e
-        | Ok None -> Error (TupleNotFound hash)
-        | Ok (Some tuple) -> load_all (tuple :: acc) rest
+      | hash :: rest -> (
+          let* tup_opt = load_tuple storage hash in
+          match tup_opt with
+          | None -> Error (TupleNotFound hash)
+          | Some tuple -> load_all (tuple :: acc) rest)
     in
     load_all [] hashes
 
-  (** Scan every relation in [db] for constraints that reference [dep_rel] with
-      a polarity matched by [polarity_triggers], then re-evaluate those
-      constraints against the affected tuples in each constrained relation.
+  let with_loaded_tuple storage tuple_hash ~on_some =
+    let* tup_opt = load_tuple storage tuple_hash in
+    match tup_opt with
+    | Some tup -> on_some tup
+    | None ->
+        Error
+          (StorageError ("Tuple missing for referenced hash: " ^ tuple_hash))
+
+  let transition_attrs (tuple : Tuple.materialized) =
+    Tuple.AttributeMap.bindings tuple.attributes
+    |> List.map (fun (k, attr) -> (k, attr.Attribute.value))
+
+  let ensure_relation_exists (db : Management.Database.t) name =
+    if Management.Database.has_relation db name then Ok ()
+    else Error (RelationNotFound name)
+
+  let bump_cardinality delta = function
+    | Conventions.Cardinality.Finite n ->
+        Conventions.Cardinality.Finite (max 0 (n + delta))
+    | other -> other
+
+  let rehashed_relation_with_tree ~name ~schema (relation : Relation.t) tree
+      cardinality =
+    let hash = Hashing.hash_relation ~name ~schema ~tree in
+    { relation with hash = Some hash; tree = Some tree; cardinality }
+
+  let validate_tuple_constraints (storage : storage)
+      (db : Management.Database.t) (relation : Relation.t)
+      (tuple : Tuple.materialized) =
+    let eval_result =
+      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 eval_result with
+    | Ok true -> Ok ()
+    | Ok false -> Error (ConstraintViolation "Constraint not satisfied")
+    | Error (Constraint.ConstraintFailures failures) ->
+        let msg =
+          String.concat "; "
+            (List.map (fun (n, _) -> "constraint " ^ n ^ " violated") failures)
+        in
+        Error (ConstraintViolation msg)
+    | Error _ -> Error (ConstraintViolation "Constraint evaluation failed")
+
+  let store_tuple_payload storage tuple_hash (tuple : Tuple.materialized) =
+    let* attr_hashes = store_attributes storage tuple in
+    let stored_tuple : Storable.Tuple.t =
+      { relation = tuple.relation; attributes = attr_hashes }
+    in
+    let tuple_bytes = Storable.Tuple.to_bytes stored_tuple in
+    match Storage.store_raw storage tuple_hash tuple_bytes with
+    | Error _ -> Error (StorageError "Failed to store tuple")
+    | Ok () -> Ok ()
+
+  (* Cascade constraint helpers *)
+
+  let polarity_triggered_by kind pol =
+    match (kind, pol) with
+    | Insert, (Constraint.Negative | Constraint.Both) -> true
+    | Delete, (Constraint.Positive | Constraint.Both) -> true
+    | _ -> false
+
+  let cascade_violation_msg kind dep_rel cname constrained_name =
+    let verb =
+      match kind with Insert -> "inserting into" | Delete -> "deleting from"
+    in
+    Printf.sprintf "cascade: %s %s violates constraint %s on %s" verb dep_rel
+      cname constrained_name
+
+  let is_deferred (db : Management.Database.t) rel_name cname =
+    List.exists
+      (fun (d : Management.Database.deferred_entry) ->
+        d.constraint_name = cname && d.relation_name = rel_name)
+      db.deferred
+
+  let needs_recheck filter (tup : Tuple.materialized) =
+    filter = []
+    || List.for_all
+         (fun (attr, fval) ->
+           match Tuple.AttributeMap.find_opt attr tup.attributes with
+           | Some a -> Stdlib.( = ) a.Attribute.value fval
+           | None -> false)
+         filter
+
+  let recheck_one storage ctx mctx cname cbody constrained_name filter
+      (h : Conventions.Hash.t) : unit result =
+    with_loaded_tuple storage h ~on_some:(fun tup ->
+        if not (needs_recheck filter tup) then Ok ()
+        else
+          let cbody' =
+            Constraint.substitute_transition cbody mctx.dep_rel mctx.transition
+          in
+          match
+            Constraint.evaluate_first_failure ctx tup [ (cname, cbody') ]
+          with
+          | Ok true -> Ok ()
+          | Ok false | Error _ ->
+              Error
+                (ConstraintViolation
+                   (cascade_violation_msg mctx.kind mctx.dep_rel cname
+                      constrained_name)))
+
+  let check_one_constraint storage ctx db mctx constrained_name constrained_rel
+      (cname, cbody) : unit result =
+    if is_deferred db constrained_name cname then Ok ()
+    else
+      let pols = Constraint.polarity_of cbody in
+      match Constraint.polarity_find mctx.dep_rel pols with
+      | None -> Ok ()
+      | Some pol when not (polarity_triggered_by mctx.kind pol) -> Ok ()
+      | Some _ ->
+          let filter =
+            Constraint.focused_filter cbody mctx.dep_rel mctx.transition
+          in
+          let hashes =
+            match constrained_rel.Relation.tree with
+            | None -> []
+            | Some t -> Merkle.keys t
+          in
+          fold_result
+            (fun () h ->
+              recheck_one storage ctx mctx cname cbody constrained_name filter h)
+            () hashes
 
-      [transition] is the inserted or deleted tuple's attributes.
-      [polarity_triggers] returns true for the polarities that the current
-      mutation type can violate:
-        - DELETE: Positive | Both
-        - INSERT: Negative | Both
+  (** Scan every relation in [db] for constraints that reference [mctx.dep_rel]
+      with a polarity matched by the mutation kind, then re-evaluate those
+      constraints against the affected tuples in each constrained relation.
 
       Returns [Ok ()] when all cascade checks pass. *)
-  let check_cascade_constraints
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(dep_rel : string)
-      ~(transition : (string * Conventions.AbstractValue.t) list)
-      ~(polarity_triggers : Constraint.polarity -> bool)
-      ~(violation_msg : string -> string -> string)
-    : unit result =
+  let check_cascade_constraints (storage : storage) (db : Management.Database.t)
+      (mctx : mutation_context) : unit result =
     let ctx = build_eval_context storage db in
     Management.Database.RelationMap.fold
       (fun constrained_name constrained_rel acc ->
-        match acc with Error _ -> acc | Ok () ->
-        let is_deferred cname =
-          List.exists (fun (d : Management.Database.deferred_entry) ->
-            d.constraint_name = cname && d.relation_name = constrained_name)
-            db.deferred
-        in
+        let* () = acc in
         match constrained_rel.Relation.constraints with
         | None | Some [] -> Ok ()
-        | Some named_constraints ->
-          List.fold_left (fun acc (cname, cbody) ->
-            match acc with Error _ -> acc | Ok () ->
-            if is_deferred cname then Ok ()
-            else
-              let pols = Constraint.polarity_of cbody in
-              match List.assoc_opt dep_rel pols with
-              | None -> Ok ()
-              | Some pol when not (polarity_triggers pol) -> Ok ()
-              | Some _ ->
-                let filter = Constraint.focused_filter cbody dep_rel transition in
-                let hashes = match constrained_rel.tree with
-                  | None -> [] | Some t -> Merkle.keys t
-                in
-                let rec check_tuples = function
-                  | [] -> Ok ()
-                  | h :: rest ->
-                    (match load_tuple storage h with
-                     | Error _ | Ok None -> check_tuples rest
-                     | Ok (Some tup) ->
-                       let needs_recheck =
-                         filter = [] ||
-                         List.for_all (fun (attr, fval) ->
-                           match Tuple.AttributeMap.find_opt attr tup.attributes with
-                           | Some a -> Stdlib.(=) a.Attribute.value fval
-                           | None -> false) filter
-                       in
-                       if not needs_recheck then check_tuples rest
-                       else
-                         let cbody' =
-                           Constraint.substitute_transition cbody dep_rel transition
-                         in
-                         match Constraint.evaluate_named ctx tup [(cname, cbody')] with
-                         | Ok true -> check_tuples rest
-                         | Ok false | Error _ ->
-                           Error (ConstraintViolation
-                             (violation_msg cname constrained_name)))
-                in
-                check_tuples hashes)
-            (Ok ()) named_constraints)
+        | Some named ->
+            fold_result
+              (fun () nc ->
+                check_one_constraint storage ctx db mctx constrained_name
+                  constrained_rel nc)
+              () named)
       db.relations (Ok ())
 
   (** Insert a tuple into a relation, storing it in the backend *)
-  let create_tuple
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-      (tuple : Tuple.materialized)
-    : (Management.Database.t * Relation.t * Conventions.Hash.t) result =
+  let create_tuple (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) (tuple : Tuple.materialized) :
+      (Management.Database.t * Relation.t * Conventions.Hash.t) result =
     let name = relation.name in
-    match Management.Database.get_relation db name with
-    | None -> Error (RelationNotFound name)
-    | Some _ ->
-      (* Check membership criteria *)
-      if not (relation.membership_criteria (Tuple.Materialized tuple)) then
-        Error (ConstraintViolation "Tuple does not satisfy membership criteria")
+    let* () = ensure_relation_exists db name in
+    if not (relation.membership_criteria (Tuple.Materialized tuple)) then
+      Error (ConstraintViolation "Tuple does not satisfy membership criteria")
+    else
+      let* () = validate_tuple_constraints storage db relation tuple in
+      let tuple_hash = Hashing.hash_tuple tuple in
+      let current_tree =
+        match relation.tree with Some t -> t | None -> Merkle.empty
+      in
+      if Merkle.member tuple_hash current_tree then
+        Error (DuplicateTuple tuple_hash)
       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
+        let* () = store_tuple_payload storage tuple_hash tuple in
+        let new_tree = Merkle.insert tuple_hash current_tree in
+        let new_relation =
+          rehashed_relation_with_tree ~name ~schema:relation.schema relation
+            new_tree
+            (bump_cardinality 1 relation.cardinality)
         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
-
-        (* Get current tree or create empty one *)
-        let current_tree = match relation.tree with
-          | Some t -> t
-          | None -> Merkle.empty
+        let new_db =
+          Management.Database.update_relation db ~relation:new_relation
         in
-
-        (* Check for duplicate *)
-        if Merkle.member tuple_hash current_tree then
-          Error (DuplicateTuple tuple_hash)
-        else
-          (* Store attribute values in storage *)
-          match store_attributes storage tuple with
-          | Error e -> Error e
-          | Ok attr_hashes ->
-            (* Create stored tuple representation *)
-            let stored_tuple : Storable.Tuple.t = {
-              relation = tuple.relation;
-              attributes = attr_hashes;
-            } in
-
-            (* Store the tuple itself *)
-            let tuple_bytes = Storable.Tuple.to_bytes stored_tuple in
-            (match Storage.store_raw storage tuple_hash tuple_bytes with
-             | Error _ -> Error (StorageError "Failed to store tuple")
-             | Ok () ->
-               (* Insert tuple hash into relation's merkle tree *)
-               let new_tree = Merkle.insert tuple_hash current_tree in
-
-               (* Compute new relation hash *)
-               let new_relation_hash = Hashing.hash_relation ~name ~schema:relation.schema ~tree:new_tree in
-
-               (* Update cardinality *)
-               let new_cardinality = match relation.cardinality with
-                 | Conventions.Cardinality.Finite n -> Conventions.Cardinality.Finite (n + 1)
-                 | other -> other
-               in
-
-               (* Create updated relation *)
-               let new_relation = { relation with
-                 hash = Some new_relation_hash;
-                 tree = Some new_tree;
-                 cardinality = new_cardinality;
-               } in
-
-               (* Update database with the new relation *)
-               let new_db = Management.Database.update_relation db ~relation:new_relation in
-
-               (* Cascade constraint check (INSERT) *)
-               let inserted_attrs =
-                 Tuple.AttributeMap.bindings tuple.attributes
-                 |> List.map (fun (k, attr) -> (k, attr.Attribute.value))
-               in
-               let cascade_ok =
-                 check_cascade_constraints storage new_db
-                   ~dep_rel:name
-                   ~transition:inserted_attrs
-                   ~polarity_triggers:(function
-                     | Constraint.Negative | Constraint.Both -> true
-                     | Constraint.Positive -> false)
-                   ~violation_msg:(fun cname crel ->
-                     Printf.sprintf
-                       "cascade: inserting into %s violates constraint %s on %s"
-                       name cname crel)
-               in
-               match cascade_ok with
-               | Error e -> Error e
-               | Ok () ->
-               (* Persist relation and database state *)
-               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, tuple_hash)))
+        let* () =
+          check_cascade_constraints storage new_db
+            {
+              dep_rel = name;
+              transition = transition_attrs tuple;
+              kind = Insert;
+            }
+        in
+        let* () = store_relation storage new_relation in
+        let* () = store_database storage new_db in
+        Ok (new_db, new_relation, tuple_hash)
 
   (** Insert multiple tuples into a relation *)
-  let create_tuples
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-      (tuples : Tuple.materialized list)
-    : (Management.Database.t * Relation.t * Conventions.Hash.t list) result =
+  let create_tuples (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) (tuples : Tuple.materialized list) :
+      (Management.Database.t * Relation.t * Conventions.Hash.t list) result =
     let rec insert_all db rel hashes = function
       | [] -> Ok (db, rel, List.rev hashes)
       | tuple :: rest ->
-        match create_tuple storage db rel tuple with
-        | Error e -> Error e
-        | Ok (new_db, new_rel, hash) ->
+          let* new_db, new_rel, hash = create_tuple storage db rel tuple in
           insert_all new_db new_rel (hash :: hashes) rest
     in
     insert_all db relation [] tuples
 
   (** Remove a tuple from a relation by its hash *)
-  let retract_tuple
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-      ~(tuple_hash : Conventions.Hash.t)
-    : (Management.Database.t * Relation.t) result =
+  let retract_tuple (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) ~(tuple_hash : Conventions.Hash.t) :
+      (Management.Database.t * Relation.t) result =
     let name = relation.name in
-    match Management.Database.get_relation db name with
-    | None -> Error (RelationNotFound name)
-    | Some _ ->
+    let* () = ensure_relation_exists db name in
+    let* current_tree =
       match relation.tree with
       | None -> Error (TupleNotFound tuple_hash)
-      | Some current_tree ->
-        if not (Merkle.member tuple_hash current_tree) then
-          Error (TupleNotFound tuple_hash)
-        else
-          (* Remove tuple hash from tree *)
-          (* Note: We don't delete from storage - content-addressed storage is append-only.
-             The tuple data remains for historical queries / garbage collection later. *)
-          let new_tree = Merkle.delete tuple_hash current_tree in
-
-          (* Compute new relation hash *)
-          let new_relation_hash = Hashing.hash_relation ~name ~schema:relation.schema ~tree:new_tree in
-
-          (* Update cardinality *)
-          let new_cardinality = match relation.cardinality with
-            | Conventions.Cardinality.Finite n when n > 0 ->
-              Conventions.Cardinality.Finite (n - 1)
-            | other -> other
-          in
-
-          (* Create updated relation *)
-          let new_relation = { relation with
-            hash = Some new_relation_hash;
-            tree = Some new_tree;
-            cardinality = new_cardinality;
-          } in
-
-          (* Update database *)
-          let new_db = Management.Database.update_relation db ~relation:new_relation in
-
-          (* Cascade constraint check (DELETE) *)
-          let cascade_ok =
-            match load_tuple storage tuple_hash with
-            | Error _ | Ok None -> Ok ()  (* can't load the deleted tuple, so just skip *)
-            | Ok (Some deleted_tuple) ->
-              let deleted_attrs =
-                Tuple.AttributeMap.bindings deleted_tuple.attributes
-                |> List.map (fun (k, attr) -> (k, attr.Attribute.value))
-              in
-              check_cascade_constraints storage new_db
-                ~dep_rel:name
-                ~transition:deleted_attrs
-                ~polarity_triggers:(function
-                  | Constraint.Positive | Constraint.Both -> true
-                  | Constraint.Negative -> false)
-                ~violation_msg:(fun cname crel ->
-                  Printf.sprintf "cascade: deleting from %s violates constraint %s on %s"
-                    name cname crel)
-          in
-          (match cascade_ok with
-           | Error e -> Error e
-           | Ok () ->
-          (* Persist relation and database state *)
-          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))
+      | Some tree -> Ok tree
+    in
+    if not (Merkle.member tuple_hash current_tree) then
+      Error (TupleNotFound tuple_hash)
+    else
+      (* Note: We don't delete from storage - content-addressed storage is append-only.
+         The tuple data remains for historical queries / garbage collection later. *)
+      let new_tree = Merkle.delete tuple_hash current_tree in
+      let new_relation =
+        rehashed_relation_with_tree ~name ~schema:relation.schema relation
+          new_tree
+          (bump_cardinality (-1) relation.cardinality)
+      in
+      let new_db =
+        Management.Database.update_relation db ~relation:new_relation
+      in
+      let* () =
+        with_loaded_tuple storage tuple_hash ~on_some:(fun deleted_tuple ->
+            check_cascade_constraints storage new_db
+              {
+                dep_rel = name;
+                transition = transition_attrs deleted_tuple;
+                kind = Delete;
+              })
+      in
+      let* () = store_relation storage new_relation in
+      let* () = store_database storage new_db in
+      Ok (new_db, new_relation)
 
   (*
      System Catalog Maintenance
       *)
 
-  (** Update catalog when a new user relation is created.
-      Skipped if the relation being created is itself a catalog relation. *)
-  let update_catalog_on_create
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-    : (Management.Database.t, error) Result.t =
-    if Prelude.Catalog.is_catalog_relation relation.name then
-      Ok db
+  (** Update catalog when a new user relation is created. Skipped if the
+      relation being created is itself a catalog relation. *)
+  let update_catalog_on_create (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) : (Management.Database.t, error) Result.t =
+    if Prelude.Catalog.is_catalog_relation relation.name then Ok db
     else
       (* Insert into sakura:relation *)
-      match Management.Database.get_relation db Prelude.Catalog.relation_rel_name with
-      | None -> Ok db  (* catalog not yet initialized *)
-      | Some rel_cat ->
-        let rel_tuple = Prelude.Catalog.build_relation_tuple relation.name in
-        match create_tuple storage db rel_cat rel_tuple with
-        | Error e -> Error e
-        | Ok (db, _, _) ->
+      match
+        Management.Database.get_relation db Prelude.Catalog.relation_rel_name
+      with
+      | None -> Ok db (* catalog not yet initialized *)
+      | Some rel_cat -> (
+          let rel_tuple = Prelude.Catalog.build_relation_tuple relation.name in
+          let* db, _, _ = create_tuple storage db rel_cat rel_tuple in
           (* Insert into sakura:attribute for each schema entry *)
-          match Management.Database.get_relation db Prelude.Catalog.attribute_rel_name with
+          match
+            Management.Database.get_relation db
+              Prelude.Catalog.attribute_rel_name
+          with
           | None -> Ok db
           | Some attr_cat ->
-            let attr_tuples =
-              Prelude.Catalog.build_attribute_tuples
-                ~relation_name:relation.name relation.schema
-            in
-            match create_tuples storage db attr_cat attr_tuples with
-            | Error e -> Error e
-            | Ok (db, _, _) -> Ok db
-
-  (** Update catalog when a user relation is retracted.
-      Skipped if the relation being retracted is itself a catalog relation. *)
-  let update_catalog_on_retract
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-    : (Management.Database.t, error) Result.t =
-    if Prelude.Catalog.is_catalog_relation relation.name then
-      Ok db
+              let attr_tuples =
+                Prelude.Catalog.build_attribute_tuples
+                  ~relation_name:relation.name relation.schema
+              in
+              let* db, _, _ = create_tuples storage db attr_cat attr_tuples in
+              Ok db)
+
+  (** Update catalog when a user relation is retracted. Skipped if the relation
+      being retracted is itself a catalog relation. *)
+  let update_catalog_on_retract (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) : (Management.Database.t, error) Result.t =
+    if Prelude.Catalog.is_catalog_relation relation.name then Ok db
     else
-      (* Remove the tuple from sakura:relation *)
-      let step1 db =
-        match Management.Database.get_relation db Prelude.Catalog.relation_rel_name with
+      let* db =
+        match
+          Management.Database.get_relation db Prelude.Catalog.relation_rel_name
+        with
         | None -> Ok db
         | Some rel_cat ->
-          let rel_tuple_hash =
-            Hashing.hash_tuple (Prelude.Catalog.build_relation_tuple relation.name)
-          in
-          let tree = match rel_cat.tree with Some t -> t | None -> Merkle.empty in
-          if Merkle.member rel_tuple_hash tree then
-            match retract_tuple storage db rel_cat ~tuple_hash:rel_tuple_hash with
-            | Error e -> Error e
-            | Ok (new_db, _) -> Ok new_db
-          else
-            Ok db
-      in
-      match step1 db with
-      | Error e -> Error e
-      | Ok db ->
-        (* Remove attribute tuples for this relation from sakura:attribute *)
-        let attr_tuples =
-          Prelude.Catalog.build_attribute_tuples
-            ~relation_name:relation.name relation.schema
-        in
-        let rec remove_attrs db = function
-          | [] -> Ok db
-          | tup :: rest ->
-            let tup_hash = Hashing.hash_tuple tup in
-            match Management.Database.get_relation db Prelude.Catalog.attribute_rel_name with
-            | None -> Ok db
-            | Some attr_cat ->
-              let tree = match attr_cat.tree with Some t -> t | None -> Merkle.empty in
-              if Merkle.member tup_hash tree then
-                match retract_tuple storage db attr_cat ~tuple_hash:tup_hash with
-                | Error e -> Error e
-                | Ok (new_db, _) -> remove_attrs new_db rest
-              else
-                remove_attrs db rest
-        in
-        remove_attrs db attr_tuples
-
-  (** Bootstrap the 6 system catalog relations into a fresh database.
-      Called only from [create_database]; suppresses recursive catalog updates. *)
-  let init_catalog_relations
-      (storage : storage)
-      (db : Management.Database.t)
-    : (Management.Database.t, error) Result.t =
-    (* Step 1: Create all 6 catalog relations bypassing catalog maintenance *)
-    let rec create_all db = function
-      | [] -> Ok db
-      | (name, schema) :: rest ->
-        match create_relation_raw storage db ~name ~schema with
-        | Error e -> Error e
-        | Ok (new_db, _) -> create_all new_db rest
-    in
-    match create_all db Prelude.Catalog.catalog_definitions with
-    | Error e -> Error e
-    | Ok db ->
-      (* Step 5: Seed sakura:relation with one tuple per catalog relation name *)
-      let rel_cat =
-        Option.get (Management.Database.get_relation db Prelude.Catalog.relation_rel_name)
-      in
-      let rel_tuples =
-        List.map Prelude.Catalog.build_relation_tuple Prelude.Catalog.catalog_relation_names
-      in
-      match create_tuples storage db rel_cat rel_tuples with
-      | Error e -> Error e
-      | Ok (db, _, _) ->
-        (* Step 6: Seed sakura:attribute with attribute tuples for each catalog relation *)
-        let all_attr_tuples =
-          List.concat_map (fun (name, schema) ->
-            Prelude.Catalog.build_attribute_tuples ~relation_name:name schema
-          ) Prelude.Catalog.catalog_definitions
-        in
-        let attr_cat =
-          Option.get (Management.Database.get_relation db Prelude.Catalog.attribute_rel_name)
-        in
-        match create_tuples storage db attr_cat all_attr_tuples with
-        | Error e -> Error e
-        | Ok (db, _, _) ->
-          (* Step 7: Seed sakura:on with insert, update, delete *)
-          let on_cat =
-            Option.get (Management.Database.get_relation db Prelude.Catalog.on_rel_name)
-          in
-          let on_tuples =
-            List.map Prelude.Catalog.build_on_tuple ["insert"; "update"; "delete"]
-          in
-          match create_tuples storage db on_cat on_tuples with
-          | Error e -> Error e
-          | Ok (db, _, _) ->
-            (* Step 8: Seed sakura:timing with immediate, deferred *)
-            let timing_cat =
-              Option.get (Management.Database.get_relation db Prelude.Catalog.timing_rel_name)
+            let rel_tuple_hash =
+              Hashing.hash_tuple
+                (Prelude.Catalog.build_relation_tuple relation.name)
             in
-            let timing_tuples =
-              List.map Prelude.Catalog.build_timing_tuple ["immediate"; "deferred"]
+            let tree =
+              match rel_cat.tree with Some t -> t | None -> Merkle.empty
             in
-            match create_tuples storage db timing_cat timing_tuples with
-            | Error e -> Error e
-            | Ok (db, _, _) ->
-              (* Step 9: Seed sakura:domain with the 4 prelude domain names *)
-              let dom_cat =
-                Option.get (Management.Database.get_relation db Prelude.Catalog.domain_rel_name)
+            if Merkle.member rel_tuple_hash tree then
+              let* new_db, _ =
+                retract_tuple storage db rel_cat ~tuple_hash:rel_tuple_hash
               in
-              let dom_tuples =
-                List.map Prelude.Catalog.build_domain_tuple
-                  ["integer"; "natural"; "rational"; "string"]
+              Ok new_db
+            else Ok db
+      in
+      (* Remove attribute tuples for this relation from sakura:attribute *)
+      let attr_tuples =
+        Prelude.Catalog.build_attribute_tuples ~relation_name:relation.name
+          relation.schema
+      in
+      fold_result
+        (fun db tup ->
+          let tup_hash = Hashing.hash_tuple tup in
+          match
+            Management.Database.get_relation db
+              Prelude.Catalog.attribute_rel_name
+          with
+          | None -> Ok db
+          | Some attr_cat ->
+              let tree =
+                match attr_cat.tree with Some t -> t | None -> Merkle.empty
               in
-              match create_tuples storage db dom_cat dom_tuples with
-              | Error e -> Error e
-              | Ok (db, _, _) -> Ok db
+              if Merkle.member tup_hash tree then
+                let* new_db, _ =
+                  retract_tuple storage db attr_cat ~tuple_hash:tup_hash
+                in
+                Ok new_db
+              else Ok db)
+        db attr_tuples
+
+  (** Bootstrap the 6 system catalog relations into a fresh database. Called
+      only from [create_database]; suppresses recursive catalog updates. *)
+  let init_catalog_relations (storage : storage) (db : Management.Database.t) :
+      (Management.Database.t, error) Result.t =
+    let* db =
+      fold_result
+        (fun db (name, schema) ->
+          let* new_db, _ = create_relation_raw storage db ~name ~schema in
+          Ok new_db)
+        db Prelude.Catalog.catalog_definitions
+    in
+    let get_required (db : Management.Database.t) rel_name =
+      match Management.Database.get_relation db rel_name with
+      | Some rel -> Ok rel
+      | None -> Error (StorageError ("Catalog relation missing: " ^ rel_name))
+    in
+    let* relation_rel = get_required db Prelude.Catalog.relation_rel_name in
+    let* db, _, _ =
+      create_tuples storage db relation_rel
+        (List.map Prelude.Catalog.build_relation_tuple
+           Prelude.Catalog.catalog_relation_names)
+    in
+    let* attribute_rel = get_required db Prelude.Catalog.attribute_rel_name in
+    let* db, _, _ =
+      create_tuples storage db attribute_rel
+        (List.concat_map
+           (fun (name, schema) ->
+             Prelude.Catalog.build_attribute_tuples ~relation_name:name schema)
+           Prelude.Catalog.catalog_definitions)
+    in
+    let* on_rel = get_required db Prelude.Catalog.on_rel_name in
+    let* db, _, _ =
+      create_tuples storage db on_rel
+        (List.map Prelude.Catalog.build_on_tuple
+           [ "insert"; "update"; "delete" ])
+    in
+    let* timing_rel = get_required db Prelude.Catalog.timing_rel_name in
+    let* db, _, _ =
+      create_tuples storage db timing_rel
+        (List.map Prelude.Catalog.build_timing_tuple
+           [ "immediate"; "deferred" ])
+    in
+    let* domain_rel = get_required db Prelude.Catalog.domain_rel_name in
+    let* db, _, _ =
+      create_tuples storage db domain_rel
+        (List.map Prelude.Catalog.build_domain_tuple
+           [ "integer"; "natural"; "rational"; "string" ])
+    in
+    Ok db
 
-  (* 
+  (*
      Database Operations
       *)
 
-  (** Register a domain in the database.  Can be called after [create_database]
-      to add user-defined domains (e.g. [money], [email], [uuid]).
-      Also inserts a tuple into [sakura:domain] if the catalog is live. *)
-  let register_domain
-      (storage : storage)
-      (db : Management.Database.t)
-      (domain : Domain.t)
-    : (Management.Database.t, error) Result.t =
+  (** Register a domain in the database. Can be called after [create_database]
+      to add user-defined domains (e.g. [money], [email], [uuid]). Also inserts
+      a tuple into [sakura:domain] if the catalog is live. *)
+  let register_domain (storage : storage) (db : Management.Database.t)
+      (domain : Domain.t) : (Management.Database.t, error) Result.t =
     let db = Management.Database.add_domain db domain in
-    match Management.Database.get_relation db Prelude.Catalog.domain_rel_name with
-    | None -> Ok db  (* catalog not yet initialized *)
+    match
+      Management.Database.get_relation db Prelude.Catalog.domain_rel_name
+    with
+    | None -> Ok db (* catalog not yet initialized *)
     | Some dom_cat ->
-      let dom_tuple = Prelude.Catalog.build_domain_tuple domain.name in
-      match create_tuple storage db dom_cat dom_tuple with
-      | Error e -> Error e
-      | Ok (new_db, _, _) -> Ok new_db
-
-  (** Create a new database pre-seeded with the standard prelude domains and
-      the system catalog relations. *)
-  let create_database (storage : storage) ~name
-    : (Management.Database.t, error) Result.t =
+        let dom_tuple = Prelude.Catalog.build_domain_tuple domain.name in
+        let* new_db, _, _ = create_tuple storage db dom_cat dom_tuple in
+        Ok new_db
+
+  (** Create a new database pre-seeded with the standard prelude domains and the
+      system catalog relations. *)
+  let create_database (storage : storage) ~name :
+      (Management.Database.t, error) Result.t =
     (* Register prelude domains first (catalog does not exist yet, so no catalog update) *)
     let db =
-      List.fold_left
-        Management.Database.add_domain
+      List.fold_left Management.Database.add_domain
         (Management.Database.empty ~name)
-        Prelude.Domains.[integer; natural; rational; string]
+        Prelude.Domains.[ integer; natural; rational; string ]
     in
     (* Bootstrap catalog relations and seed them *)
     init_catalog_relations storage db
@@ -828,315 +796,247 @@ module Make (Storage : Management.Physical.S) = struct
   let database_history (db : Management.Database.t) : Conventions.Hash.t list =
     db.history
 
-  (* 
+  (*
      Relation Operations
       *)
 
-  (** Create a new empty relation with the given schema.
-      Also updates [sakura:relation] and [sakura:attribute] in the system catalog. *)
-  let create_relation
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(name : string)
-      ~(schema : Schema.t)
-    : (Management.Database.t * Relation.t) result =
+  (** Create a new empty relation with the given schema. Also updates
+      [sakura:relation] and [sakura:attribute] in the system catalog. *)
+  let create_relation (storage : storage) (db : Management.Database.t)
+      ~(name : string) ~(schema : Schema.t) :
+      (Management.Database.t * Relation.t) result =
     if Management.Database.has_relation db name then
       Error (RelationAlreadyExists name)
     else
       let tree = Merkle.empty in
       let relation_hash = Hashing.hash_relation ~name ~schema ~tree in
-      let relation = Relation.make
-          ~hash:(Some relation_hash)
-          ~name
-          ~schema
-          ~tree:(Some tree)
-          ~constraints:None
-          ~cardinality:(Conventions.Cardinality.Finite 0)
+      let relation =
+        Relation.make ~hash:(Some relation_hash) ~name ~schema ~tree:(Some tree)
+          ~constraints:None ~cardinality:(Conventions.Cardinality.Finite 0)
           ~generator:None
           ~membership_criteria:(build_membership_criteria schema)
           ~provenance:(build_base_provenance schema name)
           ~lineage:(Relation.Lineage.Base name)
       in
       let new_db = Management.Database.add_relation db ~relation in
-      match store_relation storage relation with
-      | Error e -> Error e
-      | Ok () ->
-        (* Update catalog (handles its own store_database calls internally) *)
-        match update_catalog_on_create storage new_db relation with
-        | Error e -> Error e
-        | Ok final_db ->
-          (* Persist final database state *)
-          match store_database storage final_db with
-          | Error e -> Error e
-          | Ok () -> Ok (final_db, relation)
+      let* () = store_relation storage relation in
+      let* final_db = update_catalog_on_create storage new_db relation in
+      let* () = store_database storage final_db in
+      Ok (final_db, relation)
 
   (** Create an immutable/generator-based relation *)
-  let create_immutable_relation
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(name : string)
-      ~(schema : Schema.t)
-      ~(generator : Generator.t)
+  let create_immutable_relation (storage : storage) (db : Management.Database.t)
+      ~(name : string) ~(schema : Schema.t) ~(generator : Generator.t)
       ~(membership_criteria : Tuple.t -> bool)
-      ~(cardinality : Conventions.Cardinality.t)
-    : (Management.Database.t * Relation.t) result =
+      ~(cardinality : Conventions.Cardinality.t) :
+      (Management.Database.t * Relation.t) result =
     if Management.Database.has_relation db name then
       Error (RelationAlreadyExists name)
     else
-      let relation_hash = Hashing.hash_relation ~name ~schema ~tree:Merkle.empty in
-      let relation = Relation.make
-          ~hash:(Some relation_hash)
-          ~name
-          ~schema
-          ~tree:None  (* No tree for generator-based relations *)
-          ~constraints:None
-          ~cardinality
-          ~generator:(Some generator)
+      let relation_hash =
+        Hashing.hash_relation ~name ~schema ~tree:Merkle.empty
+      in
+      let relation =
+        Relation.make ~hash:(Some relation_hash) ~name ~schema
+          ~tree:None (* No tree for generator-based relations *)
+          ~constraints:None ~cardinality ~generator:(Some generator)
           ~membership_criteria
           ~provenance:(build_base_provenance schema name)
           ~lineage:(Relation.Lineage.Base name)
       in
       let new_db = Management.Database.add_relation db ~relation in
-      (* Persist relation and database state *)
-      match store_relation storage relation with
-      | Error e -> Error e
-      | Ok () ->
-        match update_catalog_on_create storage new_db relation with
-        | Error e -> Error e
-        | Ok final_db ->
-          match store_database storage final_db with
-          | Error e -> Error e
-          | Ok () -> Ok (final_db, relation)
-
-  (** Remove a relation from the database.
-      Also removes its entries from [sakura:relation] and [sakura:attribute]. *)
-  let retract_relation
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(name : string)
-    : Management.Database.t result =
-    if not (Management.Database.has_relation db name) then
-      Error (RelationNotFound name)
-    else
-      let relation = Option.get (Management.Database.get_relation db name) in
-      let new_db = Management.Database.remove_relation db ~name in
-      (* Update catalog on the db state that no longer contains the retracted relation *)
-      match update_catalog_on_retract storage new_db relation with
-      | Error e -> Error e
-      | Ok final_db ->
-        match store_database storage final_db with
-        | Error e -> Error e
-        | Ok () -> Ok final_db
+      let* () = store_relation storage relation in
+      let* final_db = update_catalog_on_create storage new_db relation in
+      let* () = store_database storage final_db in
+      Ok (final_db, relation)
+
+  (** Remove a relation from the database. Also removes its entries from
+      [sakura:relation] and [sakura:attribute]. *)
+  let retract_relation (storage : storage) (db : Management.Database.t)
+      ~(name : string) : Management.Database.t result =
+    match Management.Database.get_relation db name with
+    | None -> Error (RelationNotFound name)
+    | Some relation ->
+        let new_db = Management.Database.remove_relation db ~name in
+        (* Update catalog on the db state that no longer contains the retracted relation *)
+        let* final_db = update_catalog_on_retract storage new_db relation in
+        let* () = store_database storage final_db in
+        Ok final_db
 
   (** Clear all tuples from a relation (truncate) *)
-  let clear_relation
-      (storage : storage)
-      (db : Management.Database.t)
-      (relation : Relation.t)
-    : (Management.Database.t * Relation.t) result =
+  let clear_relation (storage : storage) (db : Management.Database.t)
+      (relation : Relation.t) : (Management.Database.t * Relation.t) result =
     let name = relation.name in
     match Management.Database.get_relation db name with
     | None -> Error (RelationNotFound name)
     | Some _ ->
-      let new_tree = Merkle.empty in
-      let new_hash = Hashing.hash_relation ~name ~schema:relation.schema ~tree:new_tree in
-      let new_relation = { relation with
-        hash = Some new_hash;
-        tree = Some new_tree;
-        cardinality = Conventions.Cardinality.Finite 0;
-      } in
-      let new_db = Management.Database.update_relation db ~relation:new_relation in
-      (* Persist relation and database state *)
-      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)
-
-  (** 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 =
+        let new_tree = Merkle.empty in
+        let new_hash =
+          Hashing.hash_relation ~name ~schema:relation.schema ~tree:new_tree
+        in
+        let new_relation =
+          {
+            relation with
+            hash = Some new_hash;
+            tree = Some new_tree;
+            cardinality = Conventions.Cardinality.Finite 0;
+          }
+        in
+        let new_db =
+          Management.Database.update_relation db ~relation:new_relation
+        in
+        let* () = store_relation storage new_relation in
+        let* () = store_database storage new_db in
+        Ok (new_db, new_relation)
+
+  (** 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
-      (* Do not bake constraint evaluation into membership_criteria.
+        let merged_constraints =
+          match relation.constraints with
+          | None -> constraints
+          | Some existing -> Constraint.merge existing constraints
+        in
+        (* Do not 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 =
-    (* 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)))
+        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
+        let* () = store_relation storage new_relation in
+        let* () = store_database storage new_db in
+        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 =
+    let* db, _ =
+      update_relation_constraints storage db ~relation_name
+        ~constraints:[ (constraint_name, body) ]
+    in
+    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
+        let* new_db, _, _ = create_tuple storage db con_cat con_tuple in
+        Ok new_db
 
   (*Query Operations *)
 
   (** Get all tuple hashes from a relation *)
   let tuple_hashes (relation : Relation.t) : Conventions.Hash.t list =
-    match relation.tree with
-    | None -> []
-    | Some tree -> Merkle.keys tree
+    match relation.tree with None -> [] | Some tree -> Merkle.keys tree
 
   (** Get relation by name from database *)
-  let get_relation (db : Management.Database.t) ~(name : string) : Relation.t option =
+  let get_relation (db : Management.Database.t) ~(name : string) :
+      Relation.t option =
     Management.Database.get_relation db name
 
   (** Count tuples in a relation *)
   let tuple_count (relation : Relation.t) : int =
-    match relation.tree with
-    | None -> 0
-    | Some tree -> Merkle.size tree
+    match relation.tree with None -> 0 | Some tree -> Merkle.size tree
 
   (** Check if a tuple exists in a relation *)
-  let tuple_exists (relation : Relation.t) (tuple_hash : Conventions.Hash.t) : bool =
+  let tuple_exists (relation : Relation.t) (tuple_hash : Conventions.Hash.t) :
+      bool =
     match relation.tree with
     | None -> false
     | Some tree -> Merkle.member tuple_hash tree
 
-  (** Attach a named constraint with timing metadata.
-      Immediate constraints are added to the relation's constraint list.
-      Deferred constraints are recorded in the database's deferred list
-      and also attached to the relation (for schema visibility). *)
-  let attach_constraint
-      (storage : storage)
-      (db : Management.Database.t)
-      ~(constraint_name : string)
-      ~(relation_name : string)
-      ~(body : Constraint.t)
-      ~(timing : Constraint.timing)
-    : (Management.Database.t, error) Result.t =
-    match update_relation_constraints storage db ~relation_name
-            ~constraints:[(constraint_name, body)] with
-    | Error e -> Error e
-    | Ok (db, _) ->
-      match timing with
-      | Constraint.Immediate -> Ok db
-      | Constraint.Deferred ->
-        let entry : Management.Database.deferred_entry = {
-          relation_name; constraint_name; body;
-        } in
+  (** Attach a named constraint with timing metadata. Immediate constraints are
+      added to the relation's constraint list. Deferred constraints are recorded
+      in the database's deferred list and also attached to the relation (for
+      schema visibility). *)
+  let attach_constraint (storage : storage) (db : Management.Database.t)
+      ~(constraint_name : string) ~(relation_name : string)
+      ~(body : Constraint.t) ~(timing : Constraint.timing) :
+      (Management.Database.t, error) Result.t =
+    let* db, _ =
+      update_relation_constraints storage db ~relation_name
+        ~constraints:[ (constraint_name, body) ]
+    in
+    match timing with
+    | Constraint.Immediate -> Ok db
+    | Constraint.Deferred ->
+        let entry : Management.Database.deferred_entry =
+          { relation_name; constraint_name; body }
+        in
         Ok { db with deferred = entry :: db.deferred }
 
-  (** Check all deferred constraints against the current database state.
-      Returns [Ok ()] if all pass, or an error on the first violation. *)
-  let check_deferred_constraints
-      (storage : storage)
-      (db : Management.Database.t)
-    : (unit, error) Result.t =
-    List.fold_left (fun acc (entry : Management.Database.deferred_entry) ->
-      match acc with Error _ -> acc | Ok () ->
-      match Management.Database.get_relation db entry.relation_name with
-      | None -> Ok ()  (* relation gone, nothing to check *)
-      | Some rel ->
-        let ctx = build_eval_context storage db in
-        let hashes = match rel.tree with
-          | None -> [] | Some t -> Merkle.keys t
-        in
-        let rec check = function
-          | [] -> Ok ()
-          | h :: rest ->
-            match load_tuple storage h with
-            | Error _ | Ok None -> check rest
-            | Ok (Some tup) ->
-              match Constraint.evaluate_named ctx tup
-                      [(entry.constraint_name, entry.body)] with
-              | Ok true -> check rest
-              | Ok false | Error _ ->
-                Error (ConstraintViolation
-                  (Printf.sprintf "deferred constraint %s on %s violated"
-                     entry.constraint_name entry.relation_name))
-        in
-        check hashes)
-      (Ok ()) db.deferred
+  (** Check all deferred constraints against the current database state. Returns
+      [Ok ()] if all pass, or an error on the first violation. *)
+  let check_deferred_constraints (storage : storage)
+      (db : Management.Database.t) : (unit, error) Result.t =
+    let ctx = build_eval_context storage db in
+    fold_result
+      (fun () (entry : Management.Database.deferred_entry) ->
+        match Management.Database.get_relation db entry.relation_name with
+        | None -> Ok ()
+        | Some rel ->
+            let hashes =
+              match rel.tree with None -> [] | Some t -> Merkle.keys t
+            in
+            fold_result
+              (fun () h ->
+                with_loaded_tuple storage h ~on_some:(fun tup ->
+                    match
+                      Constraint.evaluate_first_failure ctx tup
+                        [ (entry.constraint_name, entry.body) ]
+                    with
+                    | Ok true -> Ok ()
+                    | Ok false | Error _ ->
+                        Error
+                          (ConstraintViolation
+                             (Printf.sprintf
+                                "deferred constraint %s on %s violated"
+                                entry.constraint_name entry.relation_name))))
+              () hashes)
+      () db.deferred
 
   (** Complete a mutation sequence by evaluating all deferred constraints
       against the current database state.
 
       On success, returns the database with the deferred list cleared.
-      Subsequent mutations start a fresh deferral window. On failure,
-      returns the constraint violation error and leaves the database
-      unchanged so the caller can inspect or roll back.
-
-      Typical usage:
-        let db  = create_tuple storage db rel t1 in
-        let db  = retract_tuple storage db rel t2 in
-        let db  = commit storage db in (* deferred checks run here *)
-        ... *)
-  let commit
-      (storage : storage)
-      (db : Management.Database.t)
-    : (Management.Database.t, error) Result.t =
-    match check_deferred_constraints storage db with
-    | Error e -> Error e
-    | Ok () ->
-      let db' = { db with deferred = [] } in
-      match store_database storage db' with
-      | Error e -> Error e
-      | Ok () -> Ok db'
+      Subsequent mutations start a fresh deferral window. On failure, returns
+      the constraint violation error and leaves the database unchanged so the
+      caller can inspect or roll back.
+
+      Typical usage: let db = create_tuple storage db rel t1 in let db =
+      retract_tuple storage db rel t2 in let db = commit storage db in (*
+      deferred checks run here *) ... *)
+  let commit (storage : storage) (db : Management.Database.t) :
+      (Management.Database.t, error) Result.t =
+    let* () = check_deferred_constraints storage db in
+    let db' = { db with deferred = [] } in
+    let* () = store_database storage db' in
+    Ok db'
 end
 
+module Memory = Make (Management.Physical.Memory)
 (** Default instance using in-memory storage for convenience/testing *)
-module Memory = Make(Management.Physical.Memory)
diff --git a/lib/manipulation.mli b/lib/manipulation.mli
new file mode 100644
index 0000000..2a52b5c
--- /dev/null
+++ b/lib/manipulation.mli
@@ -0,0 +1,137 @@
+type error =
+  | RelationNotFound of string
+  | RelationAlreadyExists of string
+  | TupleNotFound of Conventions.Hash.t
+  | DuplicateTuple of Conventions.Hash.t
+  | ConstraintViolation of string
+  | StorageError of string
+
+val string_of_error : error -> string
+val sexp_of_error : error -> Sexplib.Sexp.t
+
+type 'a result = ('a, error) Result.t
+
+module Schema = Schema
+
+val hash_tuple : Tuple.materialized -> Conventions.Hash.t
+
+module Make (Storage : Management.Physical.S) : sig
+  type storage = Storage.t
+  type nonrec error = error
+
+  val of_string_error : string -> error
+
+  val store_database :
+    storage -> Management.Database.t -> (unit, error) Result.t
+
+  val load_relation :
+    storage -> Conventions.Hash.t -> (Relation.t option, error) Result.t
+
+  val load_database :
+    storage ->
+    Conventions.Hash.t ->
+    (Management.Database.t option, error) Result.t
+
+  val load_tuple :
+    storage -> Conventions.Hash.t -> (Tuple.materialized option, error) Result.t
+
+  val load_tuples :
+    storage ->
+    Conventions.Hash.t list ->
+    (Tuple.materialized list, error) Result.t
+
+  val create_tuple :
+    storage ->
+    Management.Database.t ->
+    Relation.t ->
+    Tuple.materialized ->
+    (Management.Database.t * Relation.t * Conventions.Hash.t, error) Result.t
+
+  val create_tuples :
+    storage ->
+    Management.Database.t ->
+    Relation.t ->
+    Tuple.materialized list ->
+    ( Management.Database.t * Relation.t * Conventions.Hash.t list,
+      error )
+    Result.t
+
+  val retract_tuple :
+    storage ->
+    Management.Database.t ->
+    Relation.t ->
+    tuple_hash:Conventions.Hash.t ->
+    (Management.Database.t * Relation.t, error) Result.t
+
+  val register_domain :
+    storage ->
+    Management.Database.t ->
+    Domain.t ->
+    (Management.Database.t, error) Result.t
+
+  val create_database :
+    storage -> name:string -> (Management.Database.t, error) Result.t
+
+  val database_history : Management.Database.t -> Conventions.Hash.t list
+
+  val create_relation :
+    storage ->
+    Management.Database.t ->
+    name:string ->
+    schema:Schema.t ->
+    (Management.Database.t * Relation.t, error) Result.t
+
+  val create_immutable_relation :
+    storage ->
+    Management.Database.t ->
+    name:string ->
+    schema:Schema.t ->
+    generator:Generator.t ->
+    membership_criteria:(Tuple.t -> bool) ->
+    cardinality:Conventions.Cardinality.t ->
+    (Management.Database.t * Relation.t, error) Result.t
+
+  val retract_relation :
+    storage ->
+    Management.Database.t ->
+    name:string ->
+    Management.Database.t result
+
+  val clear_relation :
+    storage ->
+    Management.Database.t ->
+    Relation.t ->
+    (Management.Database.t * Relation.t, error) Result.t
+
+  val register_constraint :
+    storage ->
+    Management.Database.t ->
+    constraint_name:string ->
+    relation_name:string ->
+    body:Constraint.t ->
+    (Management.Database.t, error) Result.t
+
+  val tuple_hashes : Relation.t -> Conventions.Hash.t list
+  val get_relation : Management.Database.t -> name:string -> Relation.t option
+  val tuple_count : Relation.t -> int
+  val tuple_exists : Relation.t -> Conventions.Hash.t -> bool
+
+  val attach_constraint :
+    storage ->
+    Management.Database.t ->
+    constraint_name:string ->
+    relation_name:string ->
+    body:Constraint.t ->
+    timing:Constraint.timing ->
+    (Management.Database.t, error) Result.t
+
+  val check_deferred_constraints :
+    storage -> Management.Database.t -> (unit, error) Result.t
+
+  val commit :
+    storage -> Management.Database.t -> (Management.Database.t, error) Result.t
+end
+
+module Memory : sig
+  include module type of Make (Management.Physical.Memory)
+end
diff --git a/test/test_relational_engine.ml b/test/test_relational_engine.ml
index 081ed39..619bc27 100644
--- a/test/test_relational_engine.ml
+++ b/test/test_relational_engine.ml
@@ -2863,9 +2863,9 @@ let%test_unit "merge: no-op when both sides are identical" =
       assert (Management.Database.get_relation_names merged =
               Management.Database.get_relation_names base_db))
 
-(* Helper: look up polarity for a relation name in the result list *)
+(* Helper: look up polarity for a relation name in the result map *)
 let find_polarity name pols =
-  List.assoc_opt name pols
+  Constraint.PolarityMap.find_opt name pols
 
 let%test_unit "polarity: MemberOf target is Positive" =
   let c = Constraint.MemberOf {