Constraint walker and polarity analysis

- Polarity analysis walker on Constraint.t AST
- Cascade constraint re-checking on DELETE and INSERT
- Focused filtering to narrow re-checks to affected tuples only
- Universal variable substitution for targeted constraint re-evaluation
- Constant discovery for early bail-out (trigger_constants)
- Deferred constraint timing with commit boundary
- attach_constraint and commit API in Manipulation
- extend_tuple namespacing fix (variable.attr convention)
- History capping at 128 entries in Database.update_state
- Benchmark binary (bin/bench.ml)
- Design doc (docs/incremental_constraint_checking.org)

1 files changed, 261 insertions, 0 deletions

diff --git a/docs/incremental_constraint_checking.org b/docs/incremental_constraint_checking.org
new file mode 100644
index 0000000..28b9cc5
--- /dev/null
+++ b/docs/incremental_constraint_checking.org
@@ -0,0 +1,261 @@
+#+title: Incremental Constraint Re-checking
+#+date: 2026-03-22
+
+* Background
+
+The naive implementation of assertion-style constraints evaluates the full
+constraint expression on every mutation of every relation it references. This
+is correct but expensive. The state of the art (Oracle's implementation, and
+the PostgreSQL community discussion that informed it) reduces this cost along
+two orthogonal axes:
+
+1. *When* to re-check — polarity analysis eliminates re-checks that cannot
+   possibly produce a violation.
+2. *What* to execute — universal variable substitution replaces the full
+   constraint with a focused incremental expression.
+
+Primary references:
+- Hendrik Decker, /Translating Advanced Integrity Checking Technology to SQL Database/
+- J. M. Nicolas, /Logic for Improving Integrity Checking/
+- Ceri & Widom, /Deriving Production Rules for Constraint Maintenance/
+- Lex de Hann & Toon Koppelaars, /Applied Mathematics for Database Professionals/,
+  ch. 11 (Oracle implementation)
+- PostgreSQL hackers thread (2023):
+  =https://www.postgresql.org/message-id/flat/FD62F1DE-4227-4D67-A1A5-C17350B8CAA1%40elusive.cx=
+
+* Current Sakura State
+
+Constraints are only evaluated inside =create_tuple= against the tuple
+being inserted. =retract_tuple= performs no constraint re-check. This
+means:
+
+- A DELETE from a relation referenced positively in a constraint (e.g. a
+  =Department= relation referenced by an Employee FK constraint) leaves
+  existing tuples in the constrained relation unchecked.
+- Constraints degrade silently into insert-time assertions rather than
+  invariants maintained across all mutations.
+
+Relevant code: =lib/manipulation.ml= (=create_tuple=, =retract_tuple=),
+=lib/constraint.ml= (=evaluate=, =evaluate_named=).
+
+The catalog already seeds =sakura:on= (insert/update/delete) and
+=sakura:timing= (immediate/deferred) relations, indicating that support for
+deferred and per-operation constraint scheduling was anticipated but not
+implemented.
+
+* Technique 1 — Polarity Analysis
+
+** Concept
+
+Every relation reference inside a constraint expression has a *polarity*: the
+set of mutation types that could create a new violation.
+
+| Polarity     | Meaning                                                   |
+|--------------+-----------------------------------------------------------|
+| ⊕ (positive) | A DELETE from this relation could violate the constraint  |
+| ⊖ (negative) | An INSERT into this relation could violate the constraint |
+| ⊕⊖ (both)    | Either mutation type could violate the constraint         |
+
+Polarity is determined by a tree walk toggling sign at each negating node
+(=NOT=, =EXCEPT=, =NOT EXISTS=). References under =OUTER JOIN= carry both
+polarities.
+
+** Mapping to Sakura's =Constraint.t= AST
+
+#+begin_src ocaml
+type t =
+  | MemberOf of { target : relation_name; binding : binding }
+  | Not of { body : t; universe : relation_name }
+  | And of t list | Or of t list
+  | Exists of { variable : attr_name; quantifier : relation_name; body : t }
+  | Forall of { variable : attr_name; quantifier : relation_name; body : t }
+#+end_src
+
+| Constructor             | Relation reference | Polarity | Re-check trigger                            |
+|-------------------------+--------------------+----------+---------------------------------------------|
+| =MemberOf { target }=   | =target=           | ⊕        | DELETE from =target=                        |
+| =Not { body }=          | refs in =body=     | flipped  | opposite of body                            |
+| =Not { universe }=      | =universe=         | ⊕        | (closed-world annotation; no runtime check) |
+| =Exists { quantifier }= | =quantifier=       | ⊕        | DELETE from =quantifier=                    |
+| =Exists { body }=       | refs in =body=     | as-is    | as normal                                   |
+| =Forall { quantifier }= | =quantifier=       | ⊖        | INSERT into =quantifier=                    |
+| =Forall { body }=       | refs in =body=     | flipped  | opposite of body                            |
+| =And= / =Or=            | refs in children   | as-is    | propagated                                  |
+
+Note: =Forall x in Q, P(x)= ≡ =NOT (EXISTS x in Q, NOT P(x))=, so =Q=
+acquires negative polarity (the outer =NOT= flips the positive polarity of
+=Exists=).
+
+** Worked Example (Sakura FK constraint)
+
+#+begin_src
+-- Constraint on Employee: dept_id must exist in Department
+Exists d in Department,
+  MemberOf Department (dept_id = Var "dept_id")
+#+end_src
+
+Polarity walk:
+- =Exists { quantifier = "Department" }= -> =Department= is ⊕ (positive)
+- =MemberOf { target = "Department" }= (inside body) -> also ⊕
+
+Re-check schedule derived:
+- INSERT into =Employee=: check immediately (current behavior).
+- DELETE from =Department=: re-check all =Employee= tuples whose =dept_id=
+  equals the deleted department's =dept_id= (currently NOT done!!!!).
+- INSERT into =Department=: no re-check needed.
+
+** Implementation Sketch
+
+A function =polarity : Constraint.t -> (relation_name * polarity_set) list=
+walks the AST accumulating per-relation polarity sets. The result is stored
+alongside each named constraint in the catalog (or derived on demand maybe?).
+
+When =retract_tuple= removes a tuple from relation =R=:
+- Look up all constraints (across all relations) that reference =R= with ⊕ polarity.
+- For each such constraint =C= on relation =S=: schedule a re-check of =C=
+  against existing tuples in =S= that could be affected (see Technique 2).
+
+When =create_tuple= inserts a tuple into =R=:
+- Current behavior: check constraints on =R= itself.
+- Additionally: look up all constraints referencing =R= with ⊖ polarity and
+  schedule re-checks of those (this covers =Forall= quantifiers).
+
+* Technique 2 — Universal Variable Substitution
+
+** Concept
+
+Universally quantified variables in a constraint (those bound by =Forall= or
+appearing under a =NOT EXISTS=) can be substituted with the concrete values of
+the triggering tuple. This transforms the re-check from a full table scan into
+a targeted query over the minimal set of affected rows.
+
+The "transition tuple" (the inserted or deleted tuple) supplies the concrete
+values (the NEW and OLD on PostgreSQL).
+
+** Mapping to Sakura
+
+In Sakura's =Forall { variable; quantifier; body }=:
+
+- =variable= is universally quantified over =quantifier=.
+- When a new row is inserted into =quantifier=, that specific row supplies the
+  binding for =variable=.
+- Instead of re-checking all tuples in the constrained relation =S=, substitute
+  =variable= with the transition tuple's values and check only tuples in =S=
+  that share the constrained attributes.
+
+For the Employee/Department FK example above, on DELETE of Department row
+={dept_id = 99}=:
+
+#+begin_src
+-- Full re-check (naive):
+For every employee E: Exists d in Department, dept_id = E.dept_id
+
+-- Incremental re-check (substituted):
+Exists E in Employee where E.dept_id = 99:
+  NOT (Exists d in Department where d.dept_id = E.dept_id)
+-- i.e., find employees orphaned by this specific deletion
+#+end_src
+
+This is analogous to the PostgreSQL example in the background section, where
+universally quantified =r.n= is substituted with the transition table value.
+
+** Relation to the =extend_tuple= Namespacing Fix
+
+The namespacing fix for =extend_tuple= (prefixing quantifier attributes as
+=variable.attr=) is a prerequisite for universal variable substitution to be
+correct: the substituted binding must be distinguishable from base tuple
+attributes.  Both fixes must land together.
+
+* Technique 3 — Constant Discovery
+
+Within a constraint expression, constants (=Const v= in =binding_expr=) can be
+used to filter the re-check trigger:
+
+- If =MemberOf { target; binding }= contains =Const v= bound to attribute =a=,
+  then a DELETE from =target= only needs to trigger a re-check if the deleted
+  row has =a = v=.
+
+Sakura's =binding_expr= already distinguishes =Var= from =Const=, so constant
+discovery is a straightforward fold over the binding map.
+
+* Deferred Constraints
+
+The =sakura:timing= catalog relation (seeded with =immediate= /
+=deferred=) anticipates support for deferred constraint checking
+(analogous to SQL's =DEFERRABLE INITIALLY DEFERRED=). Under deferred
+mode:
+
+- Violations discovered during a sequence of mutations are accumulated
+  rather than immediately raised.
+- The full constraint is re-evaluated at commit time (end of the
+  mutation sequence) using the final database state.
+
+In Sakura's functional/immutable model, a mutation sequence is a fold
+over =Database.t= values. Deferred checking would mean accumulating
+pending re-check obligations alongside the database value and
+evaluating them at the end of the fold, rather than at each
+=create_tuple= / =retract_tuple= call.
+
+* Concurrency Considerations
+
+Under =SERIALIZABLE= isolation, incremental re-checking (Technique 2)
+is sound because the focused predicates cover exactly the rows that
+could be newly violated. Under =READ COMMITTED= (weaker isolation),
+additional care is needed; the Oracle paper (Toon Koppelaars)
+describes how to handle this using the universal variable insight.
+Sakura is currently single-threaded (=bin/server.ml= has a TODO on
+this), so concurrency is deferred.
+
+* Coq Proof Opportunities
+
+See =doc/coq_roadmap.org= (Tier 2 — Certified Constraint Evaluator)
+for related proof targets. The following specific lemmas are unlocked
+by this technique:
+
+1. *Polarity soundness*:
+   #+begin_src coq
+   Theorem polarity_sound_positive :
+     forall c r, polarity c r = Positive ->
+     forall db tuple_deleted,
+       eval c db = true ->
+       eval c (db_without r tuple_deleted) = true \/
+       (exists t, affected_by c r tuple_deleted t).
+   #+end_src
+   Meaning: if a relation has positive polarity in a constraint, only
+   deletions from it can create violations, and only for specifically
+   affected tuples.
+
+2. *Universal substitution completeness*:
+   #+begin_src coq
+   Theorem substitution_complete :
+     forall c var q transition_tuple db,
+     universally_quantified c var q ->
+     eval (substitute c var transition_tuple) db = true ->
+     eval c (db_without q transition_tuple) = true.
+   #+end_src
+   Meaning: if the substituted re-check passes for the transition
+   tuple, the full constraint holds in the updated database.
+
+3. *Constant filter soundness*:
+   #+begin_src coq
+   Theorem constant_filter_sound :
+     forall c r a v deleted_tuple,
+     binding_constant c r a v ->
+     deleted_tuple.(a) <> v ->
+     eval c db = eval c (db_without r deleted_tuple).
+   #+end_src
+   Meaning: if the deleted tuple doesn't match the constant, no
+   re-check is needed.
+
+* Implementation Roadmap
+
+| Step | Work item                                                       | Depends on | Status   |
+|------+-----------------------------------------------------------------+------------+----------|
+|    1 | Implement =polarity= walker on =Constraint.t=                   | —          | Done     |
+|    2 | =extend_tuple= namespacing (=variable.attr= convention)         | —          | Done     |
+|    3 | Store polarity metadata in catalog (=sakura:constraint=)        | 1          | —        |
+|    4 | =retract_tuple= triggers polarity-driven re-checks              | 1, 2       | Done     |
+|    5 | Universal variable substitution for focused re-checks           | 2          | —        |
+|    6 | Constant discovery for trigger filtering                        | 1          | Done     |
+|    7 | Deferred constraint scheduling via =sakura:timing=              | 4          | —        |
+|    8 | Coq proofs for polarity soundness and substitution completeness | 1–5        | —        |