negation, quantifiers and membership criteria as schema domains

11 files changed, 510 insertions, 79 deletions

diff --git a/bin/main.ml b/bin/main.ml
index 09f96e1..e7df2e2 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -22,9 +22,9 @@ let print_solutions solutions =
         solutions
 
 let run_statements statements =
-  match Sol.World.Standalone.load statements with
+  match Sol.Program.load statements with
   | Error error ->
-      Format.eprintf "%a@." Sol.World.pp_error error;
+      Format.eprintf "%a@." Sol.Program.pp_error error;
       Error ()
   | Ok (world, queries) ->
       List.iter
diff --git a/docs/vm.org b/docs/vm.org
index e104b0f..6f3c454 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -65,6 +65,41 @@ the admission proof becomes a runtime termination measure: the
 witness shrinks structurally at every unfolding and the search
 bottoms out.
 
+* Negation and quantifiers
+
+=:not= is decidable denial. =u :not d= establishes the universe =u=
+and then refutes =d=; the denial only runs when its variables are
+ground, deferring like any other goal, so negation as failure over
+open goals cannot happen.
+
+=Exists= lowers to a conjunction at loading, since query variables
+are existential already; its =variable:= is renamed apart so the
+scope cannot be forged. =ForAll= runs when its quantifier is
+decidable: every solution of the quantifier must satisfy the body. A
+universal over an infinite domain is a non total plan, rejected, as
+decision 10 requires. Variables that live only under a universal are
+not answer variables.
+
+* Membership criteria as domains
+
+A schema attribute is constrained by a primitive domain or by a
+criterion: any relational expression with exactly one free variable,
+the subject, bound to the attribute value at admission.
+
+#+BEGIN_SRC sol
+Relation named: Employee schema: #(
+  [name domain: String]
+  [dept domain: ([Department id: D])]
+  [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
+)
+#+END_SRC
+
+A foreign key is the criterion =([Department id: D])=, nothing more
+special than that. Criteria run against the complete extension, so
+the order facts appear in the source does not matter, the same way a
+committed state is judged whole. A fact whose attribute fails its
+criterion is an integrity violation and the program gets no world.
+
 * Builtins
 
 Domains check membership once ground: Integer, Natural, Rational,
diff --git a/lib/ast.ml b/lib/ast.ml
index 9674664..61ca787 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -15,6 +15,8 @@ type node =
   | Block of string * (string * node) list  (** [[Rel l: n ...]] *)
   | And of node * node
   | Or of node * node
+  | Not of node * node
+      (** [u :not d]: within the universe [u], deny [d]. *)
 
 (** A program is a list of statements. A bare block asserts a fact;
     a directive is a top-level message send such as
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 53ef04a..417369b 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -39,6 +39,7 @@ rule token = parse
   | '|'                       { BAR }
   | ":and"                    { AND }
   | ":or"                     { OR }
+  | ":not"                    { NOT }
   | '-'? digit+ '/' digit+ as s
       { match String.index_opt s '/' with
         | Some i ->
diff --git a/lib/parser.mly b/lib/parser.mly
index c85eccc..4bac905 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -8,7 +8,7 @@ open Ast
 %token <string> NAME
 %token <string> LABEL
 %token LBRACKET RBRACKET LBRACE RBRACE LPAREN RPAREN HASH_LPAREN
-%token BAR AND OR EOF
+%token BAR AND OR NOT EOF
 
 %start <Ast.statement list> program
 
@@ -32,6 +32,7 @@ node:
 
 conjunction:
   | left = conjunction; AND; right = operand { And (left, right) }
+  | left = conjunction; NOT; right = operand { Not (left, right) }
   | operand = operand                        { operand }
 
 operand:
diff --git a/lib/program.ml b/lib/program.ml
new file mode 100644
index 0000000..ac62781
--- /dev/null
+++ b/lib/program.ml
@@ -0,0 +1,40 @@
+type error =
+  | Load of World.error
+  | Integrity of { relation : string; label : string }
+  | Undecidable_criterion of { relation : string; label : string }
+
+let pp_error fmt = function
+  | Load error -> World.pp_error fmt error
+  | Integrity { relation; label } ->
+      Format.fprintf fmt "integrity violation on %s at %s:" relation label
+  | Undecidable_criterion { relation; label } ->
+      Format.fprintf fmt "criterion on %s at %s: is not decidable" relation label
+
+let load statements =
+  match World.Standalone.load statements with
+  | Error error -> Error (Load error)
+  | Ok (world, queries, pendings) ->
+      let rec admit = function
+        | [] -> Ok (world, queries)
+        | pending :: rest -> (
+            let { World.pending_relation; pending_label; pending_body } =
+              pending
+            in
+            match Vm.Standalone.solve world pending_body with
+            | Ok (_ :: _) -> admit rest
+            | Ok [] ->
+                Error
+                  (Integrity
+                     {
+                       relation = pending_relation;
+                       label = Label.to_string pending_label;
+                     })
+            | Error (Vm.Non_total_plan _) ->
+                Error
+                  (Undecidable_criterion
+                     {
+                       relation = pending_relation;
+                       label = Label.to_string pending_label;
+                     }))
+      in
+      admit pendings
diff --git a/lib/program.mli b/lib/program.mli
new file mode 100644
index 0000000..c271212
--- /dev/null
+++ b/lib/program.mli
@@ -0,0 +1,22 @@
+(** Whole-program admission: the entry point hosts use.
+
+    The loader admits what it can decide alone; membership criteria
+    need the solver, so this module finishes admission by running
+    every pending criterion against the fully loaded world. Order of
+    facts in the source does not matter: integrity is judged against
+    the complete extension, the way a committed state would be. *)
+
+type error =
+  | Load of World.error
+  | Integrity of { relation : string; label : string }
+      (** A fact's attribute failed its membership criterion. *)
+  | Undecidable_criterion of { relation : string; label : string }
+      (** The criterion's plan was rejected as non-total. *)
+
+val pp_error : Format.formatter -> error -> unit
+
+val load :
+  Ast.statement list -> (World.Standalone.t * World.expr list, error) result
+(** Parses nothing and solves queries for nobody: admits. Returns
+    the world and the query expressions, ready for
+    {!Vm.Standalone.solve}. *)
diff --git a/lib/vm.ml b/lib/vm.ml
index bde087a..e65cd68 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -10,19 +10,34 @@ type solution = (string * Pattern.t) list
 module Make (W : World.WORLD) = struct
   exception Stuck of string list
 
+  (* A goal is a proposition to establish or a denial to refute.
+     Conjunction flattens; [u :not d] contributes the universe
+     positively and the denial negatively. *)
+  type goal = Positive of World.expr | Negated of World.expr
+
   let rec flatten = function
     | World.And (a, b) -> flatten a @ flatten b
-    | goal -> [ goal ]
+    | World.Not (universe, denial) -> flatten universe @ [ Negated denial ]
+    | expr -> [ Positive expr ]
 
   let rec expr_vars = function
     | World.Apply (_, bindings) ->
         Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []
-    | World.And (a, b) | World.Or (a, b) -> expr_vars a @ expr_vars b
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) | World.Forall (a, b)
+      ->
+        expr_vars a @ expr_vars b
 
   let goal_name = function
-    | World.Apply (name, _) -> name
-    | World.And _ -> ":and"
-    | World.Or _ -> ":or"
+    | Positive (World.Apply (name, _)) -> name
+    | Positive (World.Or _) -> ":or"
+    | Positive (World.And _) -> ":and"
+    | Positive (World.Not _) | Negated _ -> ":not"
+    | Positive (World.Forall _) -> "ForAll"
+
+  let unresolved_vars subst expr =
+    expr_vars expr
+    |> List.filter (fun v ->
+           not (Pattern.is_ground (Pattern.Subst.resolve subst (Pattern.Var v))))
 
   (* Rule variables are renamed apart at every unfolding. The suffix
      character cannot be lexed, so renamed variables are unforgeable
@@ -42,6 +57,8 @@ module Make (W : World.WORLD) = struct
             World.Apply (name, Label.Map.map rename bindings)
         | World.And (a, b) -> World.And (rename_expr a, rename_expr b)
         | World.Or (a, b) -> World.Or (rename_expr a, rename_expr b)
+        | World.Not (a, b) -> World.Not (rename_expr a, rename_expr b)
+        | World.Forall (a, b) -> World.Forall (rename_expr a, rename_expr b)
       in
       (Label.Map.map rename rule.World.head, rename_expr rule.World.body)
 
@@ -59,12 +76,30 @@ module Make (W : World.WORLD) = struct
 
   (* Executing one goal yields branches: an extended substitution
      and the extra goals it owes (rule bodies, disjuncts). [None]
-     means not decidable yet. *)
-  let try_goal world subst goal =
+     means not decidable yet; the planner retries it later, and
+     rejects the plan if nothing ever runs. *)
+  let rec try_goal world subst goal =
     match goal with
-    | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ]
-    | World.And _ -> Some [ (subst, flatten goal) ]
-    | World.Apply (name, bindings) -> (
+    | Negated denial ->
+        if unresolved_vars subst denial = [] then
+          match search world subst (flatten denial) with
+          | [] -> Some [ (subst, []) ]
+          | _ -> Some []
+        else None
+    | Positive (World.Or (a, b)) -> Some [ (subst, flatten a); (subst, flatten b) ]
+    | Positive (World.And _ | World.Not _) ->
+        Some [ (subst, flatten (match goal with Positive e -> e | _ -> assert false)) ]
+    | Positive (World.Forall (quantifier, body)) -> (
+        (* Universal over the quantifier's solutions. Decidable only
+           when the quantifier itself is; a stuck quantifier defers
+           the universal, and an infinite one therefore never runs. *)
+        match search world subst (flatten quantifier) with
+        | exception Stuck _ -> None
+        | quantified ->
+            let holds s = search world s (flatten body) <> [] in
+            if List.for_all holds quantified then Some [ (subst, []) ] else Some []
+        )
+    | Positive (World.Apply (name, bindings)) -> (
         match Builtin.run subst name bindings with
         | Some (Builtin.Solved substs) ->
             Some (List.map (fun s -> (s, [])) substs)
@@ -107,31 +142,42 @@ module Make (W : World.WORLD) = struct
                    rather than a crash. *)
                 None))
 
+  and search world subst goals =
+    match goals with
+    | [] -> [ subst ]
+    | _ -> (
+        let rec select scanned = function
+          | [] -> None
+          | goal :: rest -> (
+              match try_goal world subst goal with
+              | Some branches -> Some (branches, List.rev_append scanned rest)
+              | None -> select (goal :: scanned) rest)
+        in
+        match select [] goals with
+        | Some (branches, remaining) ->
+            List.concat_map
+              (fun (subst, extra) -> search world subst (extra @ remaining))
+              branches
+        | None -> raise (Stuck (List.map goal_name goals)))
+
+  (* Solution variables: the free variables of the query. Whatever
+     occurs only under a universal is bound per quantifier solution
+     and is nobody's answer. *)
+  let rec outer_vars = function
+    | World.Apply (_, bindings) ->
+        Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) ->
+        outer_vars a @ outer_vars b
+    | World.Forall _ -> []
+
   let solve world expr =
-    let rec search subst goals =
-      match goals with
-      | [] -> [ subst ]
-      | _ -> (
-          let rec select scanned = function
-            | [] -> None
-            | goal :: rest -> (
-                match try_goal world subst goal with
-                | Some branches -> Some (branches, List.rev_append scanned rest)
-                | None -> select (goal :: scanned) rest)
-          in
-          match select [] goals with
-          | Some (branches, remaining) ->
-              List.concat_map
-                (fun (subst, extra) -> search subst (extra @ remaining))
-                branches
-          | None -> raise (Stuck (List.map goal_name goals)))
-    in
     let variables =
       List.fold_left
         (fun acc v -> if List.mem v acc then acc else acc @ [ v ])
-        [] (expr_vars expr)
+        [] (outer_vars expr)
+      |> List.filter (fun v -> not (String.contains v '@'))
     in
-    match search Pattern.Subst.empty (flatten expr) with
+    match search world Pattern.Subst.empty (flatten expr) with
     | exception Stuck goals -> Error (Non_total_plan goals)
     | substs ->
         let read subst =
diff --git a/lib/world.ml b/lib/world.ml
index c3d3ef2..6e1e883 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -2,6 +2,8 @@ type expr =
   | Apply of string * Pattern.t Label.Map.t
   | And of expr * expr
   | Or of expr * expr
+  | Not of expr * expr
+  | Forall of expr * expr
 
 type rule = {
   rule_name : string;
@@ -10,7 +12,11 @@ type rule = {
   witness : Label.t option;
 }
 
-type domain = D_integer | D_natural | D_rational | D_string
+type primitive = D_integer | D_natural | D_rational | D_string
+
+type domain =
+  | Primitive of primitive
+  | Criterion of { subject : string; body : expr }
 
 type def =
   | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
@@ -38,6 +44,13 @@ type error =
   | Domain_violation of { relation : string; label : string }
   | Non_total_rule of string
   | Mutual_recursion of string list
+  | Criterion_arity of { relation : string; label : string }
+
+type pending = {
+  pending_relation : string;
+  pending_label : Label.t;
+  pending_body : expr;
+}
 
 let pp_error fmt = function
   | Invalid_label l -> Format.fprintf fmt "invalid label: %s" l
@@ -63,6 +76,10 @@ let pp_error fmt = function
   | Mutual_recursion cycle ->
       Format.fprintf fmt "mutual recursion rejected: %s"
         (String.concat " -> " cycle)
+  | Criterion_arity { relation; label } ->
+      Format.fprintf fmt
+        "criterion on %s at %s: must have exactly one free variable, the subject"
+        relation label
 
 let ( let* ) = Result.bind
 
@@ -114,11 +131,53 @@ let rec pattern_of_node (node : Ast.node) : (Pattern.t, error) result =
   | Ast.Block (head, _) -> Error (Term_expected ("[" ^ head ^ " ...]"))
   | Ast.And _ -> Error (Term_expected ":and")
   | Ast.Or _ -> Error (Term_expected ":or")
+  | Ast.Not _ -> Error (Term_expected ":not")
+
+(* Renaming a quantified variable apart. The stamp cannot be lexed,
+   so quantifier scopes are unforgeable from source text. *)
+let quantifier_counter = ref 0
+
+let rec rename_var ~from ~into = function
+  | Pattern.Var v when String.equal v from -> Pattern.Var into
+  | Pattern.Record map -> Pattern.Record (Label.Map.map (rename_var ~from ~into) map)
+  | other -> other
+
+let rec rename_var_expr ~from ~into = function
+  | Apply (name, bindings) ->
+      Apply (name, Label.Map.map (rename_var ~from ~into) bindings)
+  | And (a, b) -> And (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b)
+  | Or (a, b) -> Or (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b)
+  | Not (a, b) -> Not (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b)
+  | Forall (a, b) ->
+      Forall (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b)
 
 (* Proposition position: blocks apply relations, combinators
-   compose. Terms cannot appear here. *)
+   compose. Terms cannot appear here. Exists and ForAll are the two
+   higher-order forms; their variable is renamed apart, and Exists
+   lowers to a conjunction because query variables are existential
+   already. *)
 let rec expr_of_node (node : Ast.node) : (expr, error) result =
   match node with
+  | Ast.Block (("Exists" | "ForAll") as form, bindings) -> (
+      match
+        ( List.assoc_opt "variable" bindings,
+          List.assoc_opt "quantifier" bindings,
+          List.assoc_opt "body" bindings )
+      with
+      | Some (Ast.Name variable), Some quantifier, Some body
+        when is_uppercase variable && List.length bindings = 3 ->
+          let* quantifier = expr_of_node quantifier in
+          let* body = expr_of_node body in
+          incr quantifier_counter;
+          let fresh = variable ^ "@q" ^ string_of_int !quantifier_counter in
+          let quantifier = rename_var_expr ~from:variable ~into:fresh quantifier
+          and body = rename_var_expr ~from:variable ~into:fresh body in
+          if String.equal form "Exists" then Ok (And (quantifier, body))
+          else Ok (Forall (quantifier, body))
+      | _ ->
+          Error
+            (Malformed_directive
+               (form ^ " variable: Name quantifier: [...] body: [...]")))
   | Ast.Block (head, bindings) ->
       let* map = bindings_to_map ~of_node:pattern_of_node bindings in
       Ok (Apply (head, map))
@@ -130,21 +189,31 @@ let rec expr_of_node (node : Ast.node) : (expr, error) result =
       let* a = expr_of_node a in
       let* b = expr_of_node b in
       Ok (Or (a, b))
+  | Ast.Not (a, b) ->
+      let* a = expr_of_node a in
+      let* b = expr_of_node b in
+      Ok (Not (a, b))
   | Ast.Name n -> Error (Proposition_expected n)
   | Ast.Int _ | Ast.Rat _ | Ast.Str _ | Ast.Record _ | Ast.Seq _ ->
       Error (Proposition_expected "a literal")
 
-let domain_of_name = function
-  | "Integer" -> Ok D_integer
-  | "Natural" -> Ok D_natural
-  | "Rational" -> Ok D_rational
-  | "String" -> Ok D_string
-  | other -> Error (Unknown_domain other)
+let rec expr_free_vars = function
+  | Apply (_, bindings) ->
+      Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []
+  | And (a, b) | Or (a, b) | Not (a, b) | Forall (a, b) ->
+      expr_free_vars a @ expr_free_vars b
+
+let primitive_of_name = function
+  | "Integer" -> Some D_integer
+  | "Natural" -> Some D_natural
+  | "Rational" -> Some D_rational
+  | "String" -> Some D_string
+  | _ -> None
 
-(* Membership of a ground term in a builtin domain. Note the
+(* Membership of a ground term in a primitive domain. Note the
    inclusions of decision 12: a Natural is an Integer, an Integer is
    a Rational, all literally. *)
-let member_of_domain (term : Term.t) = function
+let member_of_primitive (term : Term.t) = function
   | D_integer -> ( match term with Term.Integer _ -> true | _ -> false)
   | D_natural -> (
       match term with Term.Integer z -> Z.geq z Z.zero | _ -> false)
@@ -154,7 +223,8 @@ let member_of_domain (term : Term.t) = function
 
 let rec applications = function
   | Apply (name, bindings) -> [ (name, bindings) ]
-  | And (a, b) | Or (a, b) -> applications a @ applications b
+  | And (a, b) | Or (a, b) | Not (a, b) | Forall (a, b) ->
+      applications a @ applications b
 
 module String_map = Map.Make (String)
 
@@ -163,17 +233,37 @@ module Standalone = struct
 
   let find world name = String_map.find_opt name world
 
-  let schema_of_node = function
+  let schema_of_node ~relation = function
     | Ast.Seq (entries, None) ->
         List.fold_left
           (fun acc entry ->
             let* schema = acc in
             match entry with
-            | Ast.Block (attr, [ ("domain", Ast.Name domain_name) ]) ->
+            | Ast.Block (attr, [ ("domain", domain_node) ]) -> (
                 let* label = label_of_string attr in
-                let* domain = domain_of_name domain_name in
-                Ok ((label, domain) :: schema)
-            | _ -> Error (Malformed_directive "schema entries are [attr domain: Name]"))
+                match domain_node with
+                | Ast.Name name when Option.is_some (primitive_of_name name) ->
+                    let primitive = Option.get (primitive_of_name name) in
+                    Ok ((label, Primitive primitive) :: schema)
+                | Ast.Name other -> Error (Unknown_domain other)
+                | criterion ->
+                    (* A membership criterion: any relational
+                       expression with exactly one free variable,
+                       the subject. *)
+                    let* body = expr_of_node criterion in
+                    let subjects =
+                      List.sort_uniq String.compare (expr_free_vars body)
+                    in
+                    (match subjects with
+                    | [ subject ] ->
+                        Ok ((label, Criterion { subject; body }) :: schema)
+                    | _ ->
+                        Error
+                          (Criterion_arity
+                             { relation; label = Label.to_string label })))
+            | _ ->
+                Error
+                  (Malformed_directive "schema entries are [attr domain: ...]"))
           (Ok []) entries
         |> Result.map List.rev
     | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries")
@@ -221,7 +311,7 @@ module Standalone = struct
             ->
               if String_map.mem name world then Error (Already_defined name)
               else
-                let* schema = schema_of_node schema in
+                let* schema = schema_of_node ~relation:name schema in
                 Ok
                   ( String_map.add name (Table { schema; facts = [] }) world,
                     facts,
@@ -277,11 +367,25 @@ module Standalone = struct
     in
     (* Third pass: admit facts against schemas and domains. This is
        integrity control at loading, the same check membership always
-       is. *)
-    let* world =
+       is. Primitive domains decide here; criteria need the solver,
+       so they are handed to Program as pending checks with the
+       subject already bound to the attribute value. *)
+    let equal_l = Result.get_ok (label_of_string "left")
+    and right_l = Result.get_ok (label_of_string "right") in
+    let bind_subject subject value body =
+      And
+        ( Apply
+            ( "Equal",
+              Label.Map.(
+                empty
+                |> add equal_l (Pattern.Var subject)
+                |> add right_l (Pattern.of_term value)) ),
+          body )
+    in
+    let* world, pendings =
       List.fold_left
         (fun acc node ->
-          let* world = acc in
+          let* world, pendings = acc in
           let* expr = expr_of_node node in
           let* relation, bindings =
             match expr with
@@ -311,27 +415,40 @@ module Standalone = struct
                     (Schema_mismatch
                        { relation; detail = "fact labels must match the schema" })
               in
-              let* () =
+              let* new_pendings =
                 List.fold_left
                   (fun acc (label, domain) ->
-                    let* () = acc in
-                    if member_of_domain (Label.Map.find label tuple) domain then Ok ()
-                    else
-                      Error
-                        (Domain_violation
-                           { relation; label = Label.to_string label }))
-                  (Ok ()) schema
+                    let* pendings = acc in
+                    let value = Label.Map.find label tuple in
+                    match domain with
+                    | Primitive primitive ->
+                        if member_of_primitive value primitive then Ok pendings
+                        else
+                          Error
+                            (Domain_violation
+                               { relation; label = Label.to_string label })
+                    | Criterion { subject; body } ->
+                        Ok
+                          ({
+                             pending_relation = relation;
+                             pending_label = label;
+                             pending_body = bind_subject subject value body;
+                           }
+                          :: pendings))
+                  (Ok []) schema
               in
               Ok
-                (String_map.add relation
-                   (Table { schema; facts = facts @ [ tuple ] })
-                   world)
+                ( String_map.add relation
+                    (Table { schema; facts = facts @ [ tuple ] })
+                    world,
+                  pendings @ List.rev new_pendings )
           | Some (Rules _) ->
               Error
                 (Schema_mismatch
                    { relation; detail = "facts cannot be asserted on a rule-defined relation" })
           | None -> Error (Unknown_relation relation))
-        (Ok world) raw_facts
+        (Ok (world, []))
+        raw_facts
     in
     (* Fourth pass: reference checking and the mutual recursion cut.
        Self recursion is admitted with a witness; longer cycles are
@@ -351,7 +468,14 @@ module Standalone = struct
         (fun _ def acc ->
           let* () = acc in
           match def with
-          | Table _ -> Ok ()
+          | Table { schema; _ } ->
+              List.fold_left
+                (fun acc (_, domain) ->
+                  let* () = acc in
+                  match domain with
+                  | Primitive _ -> Ok ()
+                  | Criterion { body; _ } -> check_refs body)
+                (Ok ()) schema
           | Rules rules ->
               List.fold_left
                 (fun acc rule ->
@@ -406,5 +530,5 @@ module Standalone = struct
         (Ok []) raw_queries
       |> Result.map List.rev
     in
-    Ok (world, queries)
+    Ok (world, queries, pendings)
 end
diff --git a/lib/world.mli b/lib/world.mli
index 76ad316..0a3bb9a 100644
--- a/lib/world.mli
+++ b/lib/world.mli
@@ -9,11 +9,21 @@
     terminate. *)
 
 (** A compiled relational expression: what rule bodies and queries
-    are made of after names are resolved. *)
+    are made of after names are resolved. [Exists] is lowered away
+    at loading: its variable is renamed apart and the form becomes a
+    conjunction. *)
 type expr =
   | Apply of string * Pattern.t Label.Map.t
   | And of expr * expr
   | Or of expr * expr
+  | Not of expr * expr
+      (** [u :not d]: the universe holds and the denial has no
+          solutions. Decidable negation only: the VM runs the denial
+          once its variables are ground. *)
+  | Forall of expr * expr
+      (** Every solution of the quantifier satisfies the body. The
+          VM runs it when the quantifier is decidable, which keeps
+          universals off infinite domains. *)
 
 type rule = {
   rule_name : string;
@@ -26,8 +36,17 @@ type rule = {
           termination. [None] on non-recursive rules. *)
 }
 
-(** The builtin domains a schema may constrain an attribute by. *)
-type domain = D_integer | D_natural | D_rational | D_string
+(** The primitive host-checked domains. *)
+type primitive = D_integer | D_natural | D_rational | D_string
+
+(** What a schema constrains an attribute by: a primitive domain, or
+    a membership criterion, an arbitrary relational expression with
+    exactly one free variable, the subject, bound to the attribute
+    value at admission. Foreign keys are the criterion
+    [([Department id: D])], nothing more special than that. *)
+type domain =
+  | Primitive of primitive
+  | Criterion of { subject : string; body : expr }
 
 (** How a relation is defined. *)
 type def =
@@ -48,6 +67,18 @@ type error
 
 val pp_error : Format.formatter -> error -> unit
 
+(** A fact attribute awaiting a criterion check. The loader cannot
+    run the solver (the solver sits above it), so criterion
+    admission is finished by {!Program}, against the fully loaded
+    world. *)
+type pending = {
+  pending_relation : string;
+  pending_label : Label.t;
+  pending_body : expr;
+      (** The criterion with its subject already bound to the
+          attribute value; admissible iff it has a solution. *)
+}
+
 (** The standalone world: an immutable catalog loaded from program
     text. This is Sol as a separate language; there are no branches,
     no transitions, only the pure fragment. *)
@@ -56,12 +87,13 @@ module Standalone : sig
 
   val find : t -> string -> def option
 
-  val load : Ast.statement list -> (t * expr list, error) result
+  val load : Ast.statement list -> (t * expr list * pending list, error) result
   (** Admits a program: registers relations, checks every fact
-      against its schema and domains, compiles rules and queries,
-      and enforces totality. Rejected, not deferred: a recursive
-      rule without a structural decrease witness, a mutual
+      against its schema and primitive domains, compiles rules and
+      queries, and enforces totality. Rejected, not deferred: a
+      recursive rule without a structural decrease witness, a mutual
       recursion cycle, an unknown relation, or an ill-typed fact is
-      an [error], and no world exists. Returns the world and the
-      query expressions in program order. *)
+      an [error], and no world exists. Returns the world, the query
+      expressions in program order, and the criterion checks for
+      {!Program} to finish. *)
 end
diff --git a/test/test_vm.ml b/test/test_vm.ml
index 3631ee5..e564a83 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -3,11 +3,11 @@
 let load source =
   match Sol.Front.parse_string source with
   | Error message -> Alcotest.failf "parse error: %s" message
-  | Ok statements -> Sol.World.Standalone.load statements
+  | Ok statements -> Sol.Program.load statements
 
 let run source =
   match load source with
-  | Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error
+  | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
   | Ok (world, queries) ->
       List.map
         (fun query ->
@@ -133,7 +133,7 @@ let test_mutual_recursion_rejected () =
 
 let test_unbounded_membership_is_non_total_plan () =
   match load {| Query expression: [Integer value: X] |} with
-  | Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error
+  | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
   | Ok (world, [ query ]) -> (
       match Sol.Vm.Standalone.solve world query with
       | Error (Sol.Vm.Non_total_plan _) -> ()
@@ -145,6 +145,53 @@ let test_domain_constrains_when_ground () =
     {| Query expression: [Between value: X lower: -2 upper: 2] :and [Natural value: X] |}
     "X=0; X=1; X=2"
 
+(* Negation: decidable denial over ground goals. *)
+
+let test_negation () =
+  check_answers "people who are not adults"
+    (people
+   ^ {| Query expression: ([Person name: N age: A]) :not [Adult name: N] |})
+    {|A=12,N="Ana"|}
+
+let test_negation_defers_until_ground () =
+  check_answers "denial waits for its variables"
+    (people
+   ^ {| Query expression: ([Adult name: N] :not [Equal left: N right: "Rui"]) :and [Person name: N age: A] |})
+    {|N="Marcos",A=30|}
+
+(* Quantifiers. *)
+
+let test_forall_holds () =
+  check_answers "every person is at least 10"
+    (people
+   ^ {| Query expression: [ForAll variable: P quantifier: [Person name: P age: B] body: [GreaterEqual left: B right: 10]] |})
+    ""
+
+let test_forall_fails () =
+  match
+    run
+      (people
+     ^ {| Query expression: [ForAll variable: P quantifier: [Person name: P age: B] body: [GreaterEqual left: B right: 18]] |})
+  with
+  | [ [] ] -> ()
+  | [ _ :: _ ] -> Alcotest.fail "the universal must fail: Ana is 12"
+  | _ -> Alcotest.fail "expected one query"
+
+let test_forall_over_infinite_rejected () =
+  match load {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} with
+  | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
+  | Ok (world, [ query ]) -> (
+      match Sol.Vm.Standalone.solve world query with
+      | Error (Sol.Vm.Non_total_plan _) -> ()
+      | Ok _ -> Alcotest.fail "a universal over an infinite domain must be rejected")
+  | Ok _ -> Alcotest.fail "expected one query"
+
+let test_exists () =
+  check_answers "existence lowers to conjunction"
+    (people
+   ^ {| Query expression: [Exists variable: P quantifier: [Person name: P age: B] body: [GreaterThan left: B right: 60]] |})
+    "B=70"
+
 (* Integrity control at loading: facts must satisfy their schema. *)
 
 let test_fact_domain_violation () =
@@ -158,6 +205,63 @@ let test_fact_domain_violation () =
   | Error _ -> ()
   | Ok _ -> Alcotest.fail "a fact violating its domain must be rejected"
 
+(* Membership criteria as domains: refinements and foreign keys. *)
+
+let departments =
+  {|
+  Relation named: Department schema: #( [id domain: Integer] )
+  [Department id: 1]
+  [Department id: 2]
+  Relation named: Employee schema: #(
+    [name domain: String]
+    [dept domain: ([Department id: D])]
+    [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
+  )
+  |}
+
+let test_criterion_admits () =
+  check_answers "a valid employee is admitted"
+    (departments
+   ^ {|
+      [Employee name: "Marcos" dept: 1 score: 90]
+      Query expression: [Employee name: N dept: D score: S]
+      |})
+    {|D=1,N="Marcos",S=90|}
+
+let test_foreign_key_rejected () =
+  match
+    load (departments ^ {| [Employee name: "Ghost" dept: 9 score: 50] |})
+  with
+  | Error (Sol.Program.Integrity { relation = "Employee"; label = "dept" }) -> ()
+  | Error error -> Alcotest.failf "wrong error: %a" Sol.Program.pp_error error
+  | Ok _ -> Alcotest.fail "a dangling foreign key must be rejected"
+
+let test_refinement_rejected () =
+  match
+    load (departments ^ {| [Employee name: "Over" dept: 1 score: 101] |})
+  with
+  | Error (Sol.Program.Integrity { relation = "Employee"; label = "score" }) -> ()
+  | Error error -> Alcotest.failf "wrong error: %a" Sol.Program.pp_error error
+  | Ok _ -> Alcotest.fail "a score beyond the refinement must be rejected"
+
+let test_fact_order_is_irrelevant () =
+  (* The employee arrives before its department; integrity is judged
+     against the complete extension. *)
+  match
+    load
+      {|
+      Relation named: Department schema: #( [id domain: Integer] )
+      Relation named: Employee schema: #(
+        [name domain: String]
+        [dept domain: ([Department id: D])]
+      )
+      [Employee name: "Early" dept: 7]
+      [Department id: 7]
+      |}
+  with
+  | Ok _ -> ()
+  | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
+
 let () =
   Alcotest.run "sol-vm"
     [
@@ -197,4 +301,28 @@ let () =
           Alcotest.test_case "fact domain violation" `Quick
             test_fact_domain_violation;
         ] );
+      ( "negation",
+        [
+          Alcotest.test_case "not adults" `Quick test_negation;
+          Alcotest.test_case "denial defers until ground" `Quick
+            test_negation_defers_until_ground;
+        ] );
+      ( "quantifiers",
+        [
+          Alcotest.test_case "forall holds" `Quick test_forall_holds;
+          Alcotest.test_case "forall fails" `Quick test_forall_fails;
+          Alcotest.test_case "forall over infinite rejected" `Quick
+            test_forall_over_infinite_rejected;
+          Alcotest.test_case "exists" `Quick test_exists;
+        ] );
+      ( "criteria",
+        [
+          Alcotest.test_case "criterion admits" `Quick test_criterion_admits;
+          Alcotest.test_case "foreign key rejected" `Quick
+            test_foreign_key_rejected;
+          Alcotest.test_case "refinement rejected" `Quick
+            test_refinement_rejected;
+          Alcotest.test_case "fact order irrelevant" `Quick
+            test_fact_order_is_irrelevant;
+        ] );
     ]