diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/constraint.ml | 191 | ||||
| -rw-r--r-- | lib/management/database.ml | 23 | ||||
| -rw-r--r-- | lib/manipulation.ml | 294 |
3 files changed, 437 insertions, 71 deletions
diff --git a/lib/constraint.ml b/lib/constraint.ml index 0ba7d4f..527a7dc 100644 --- a/lib/constraint.ml +++ b/lib/constraint.ml @@ -243,25 +243,18 @@ and extend_tuple (tuple : Tuple.materialized) (variable : attr_name) (row : (attr_name * Conventions.AbstractValue.t) list) : Tuple.materialized = - (* TODO: Provenance for tuples at the relation level. - Attributes from quantifier rows are namespaced by the variable name - (e.g. "d.dept_id") to avoid silent overwriting of same-named attributes - from the base tuple or other quantifiers. Without namespacing, the - following FK constraint silently passes for an invalid insertion: - - Employee { emp_id=1, dept_id=99 } is being inserted. - - Constraint: Exists d in Department, MemberOf Department (dept_id = Var "dept_id"). - - Department contains only { dept_id=1, dept_name="Engineering" }. - - extend_tuple overwrites dept_id=99 with dept_id=1 from the Department row. - - Var "dept_id" resolves to 1, check_membership succeeds trivially. - - The insertion is accepted even though dept_id=99 does not exist. - Namespacing is a syntactic encoding of provenance: the variable prefix - records which quantifier scope each value came from. A more principled - solution would attach provenance metadata directly to each attribute in - the relation, making the origin of every value explicit and queryable - without relying on name conventions. This would also eliminate the - ambiguity that arises when two quantifiers range over relations sharing - attribute names — currently resolved by namespacing, but ideally enforced - structurally by the type system or relation schema. *) + (* 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 + Exists d in Department, MemberOf Department (dept_id = Var "dept_id") + would potentially overwrite the base tuple's dept_id with the Department row's dept_id, + causing Var "dept_id" to resolve to the wrong value and accept invalid inserts. + Constraints reference quantifier attributes as Var "variable.attr" + (for example Var "d.dept_id") and base tuple attributes as Var "attr" (like Var "dept_id"). + This convention is the prerequisite for universal variable substitution + (see docs/incremental_constraint_checking.org, specifically Technique 2). + A better long-term solution would attach provenance metadata directly + to each attribute rather than relying on name conventions, but we don't have that yet. *) let extra_attrs = List.fold_left (fun acc (k, v) -> @@ -287,6 +280,166 @@ let evaluate_named (ctx : eval_context) (tuple : Tuple.materialized) | [] -> Ok true | fs -> Error (ConstraintFailures fs) +(** 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 + +let merge_polarity a b = + match a, b with + | Positive, Positive -> Positive + | Negative, Negative -> Negative + | _ -> 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) + +(** Constraint timing: immediate (checked on every mutation) or deferred + (checked at transaction commit). *) +type timing = Immediate | Deferred + +(** 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. + + 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 + +(** 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 + +(** Substitute transition tuple values into a constraint for universal variable + substitution. When [dep_rel] is being mutated (deleted from or inserted + into), any [Exists] or [Forall] that quantifies over [dep_rel] has its body + rewritten: occurrences of [Var "variable.attr"] are replaced by + [Const value] using the transition tuple's attribute values. + + 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. + + 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 = + 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) + 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 } + 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' } + in + go c + let make_comparison_binding ~left ~right = BindingMap.empty |> BindingMap.add "left" left diff --git a/lib/management/database.ml b/lib/management/database.ml index 2dc0ae6..c4c6dc3 100644 --- a/lib/management/database.ml +++ b/lib/management/database.ml @@ -8,6 +8,12 @@ module RelationMap = Map.Make(String) +type deferred_entry = { + relation_name : string; + constraint_name : string; + body : Constraint.t; +} + type t = { hash : Conventions.Hash.t; name : Conventions.Name.t; @@ -16,6 +22,7 @@ type t = { domains : Domain.t RelationMap.t; history : Conventions.Hash.t list; timestamp : float; + deferred : deferred_entry list; } let empty ~name = { @@ -26,6 +33,7 @@ let empty ~name = { domains = RelationMap.empty; history = []; timestamp = Unix.gettimeofday (); + deferred = []; } let compute_hash db = @@ -33,15 +41,26 @@ let compute_hash db = | Some root -> root | None -> Conventions.Hash.hash_text db.name +let max_history = 128 + +let rec take_at_most n = function + | [] -> [] + | _ when n = 0 -> [] + | x :: xs -> x :: take_at_most (n - 1) xs + let update_state db ~relations ~tree = let new_hash = match Merkle.root_hash tree with | Some root -> root | None -> Conventions.Hash.hash_text db.name in - let history = if db.hash = "" then db.history else db.hash :: db.history in + let history = + 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 () } + domains = db.domains; history; timestamp = Unix.gettimeofday (); + deferred = db.deferred } let get_relation db name = RelationMap.find_opt name db.relations diff --git a/lib/manipulation.ml b/lib/manipulation.ml index be77c02..58e6cbb 100644 --- a/lib/manipulation.ml +++ b/lib/manipulation.ml @@ -261,6 +261,7 @@ module Make (Storage : Management.Physical.S) = struct domains = Management.Database.RelationMap.empty; history = stored.history; timestamp = stored.timestamp; + deferred = []; }) (* Relation Operations - forward declarations needed by catalog helpers @@ -314,6 +315,123 @@ module Make (Storage : Management.Physical.S) = struct 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 = + 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 + (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 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 + 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. + + [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 + + 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 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 + 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) + db.relations (Ok ()) + (** Insert a tuple into a relation, storing it in the backend *) let create_tuple (storage : storage) @@ -398,6 +516,26 @@ module Make (Storage : Management.Physical.S) = struct (* 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 @@ -423,53 +561,6 @@ module Make (Storage : Management.Physical.S) = struct in insert_all db relation [] tuples - (** Load a tuple from storage by its hash *) - 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 - (* Load each attribute value *) - 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 - (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 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 - in - load_all [] hashes - (** Remove a tuple from a relation by its hash *) let retract_tuple (storage : storage) @@ -512,15 +603,37 @@ module Make (Storage : Management.Physical.S) = struct (* 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) + | Ok () -> Ok (new_db, new_relation)) - (* + (* System Catalog Maintenance *) @@ -858,7 +971,7 @@ module Make (Storage : Management.Physical.S) = struct | None -> constraints | Some existing -> Constraint.merge existing constraints in - (* Don't bake constraint evaluation into membership_criteria — + (* 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 = @@ -942,6 +1055,87 @@ module Make (Storage : Management.Physical.S) = struct 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 + 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 + + (** 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' end (** Default instance using in-memory storage for convenience/testing *) |