From 3b09972d557e547c26edda4b66f6ea769289a07d Mon Sep 17 00:00:00 2001
From: Sam Rose <samuel@supabase.io>
Date: Sat, 28 Feb 2026 21:02:09 -0500
Subject: [PATCH 1/2] fix: cleanup step

---
 lib/datalox/database.ex        | 146 +++++++++++++++++++++++++++------
 test/datalox/database_test.exs | 139 +++++++++++++++++++++++++++++++
 2 files changed, 259 insertions(+), 26 deletions(-)

diff --git a/lib/datalox/database.ex b/lib/datalox/database.ex
index dc0b25b..84ac5ef 100644
--- a/lib/datalox/database.ex
+++ b/lib/datalox/database.ex
@@ -196,7 +196,13 @@ defmodule Datalox.Database do
         {:reply, {:error, {:safety_violations, errors}}, state}
 
       :ok ->
-        case Evaluator.evaluate(rules, state.storage_state, state.storage_mod) do
+        # Clear all derived predicates before re-evaluating.
+        # Without this, stale derived facts (e.g. from negation changes)
+        # persist because the evaluator only adds, never removes.
+        derived_preds = derived_predicates(rules)
+        clean_storage = clear_predicates(state.storage_mod, state.storage_state, derived_preds)
+
+        case Evaluator.evaluate(rules, clean_storage, state.storage_mod) do
           {:ok, _derived, new_storage_state} ->
             Datalox.Metrics.record_load_rules(state.name, length(rules))
             new_state = %{state | rules: rules, storage_state: new_storage_state}
@@ -330,50 +336,108 @@ defmodule Datalox.Database do
   end
 
   defp incrementally_derive(state, predicate, tuple) do
+    # Check for rules affected by positive body references
     affected = Incremental.affected_rules(state.rules, predicate)
 
-    if affected == [] do
+    # Check for rules that negate this predicate — asserting a negated fact
+    # may invalidate existing derived facts
+    negation_affected = rules_negating(state.rules, predicate)
+
+    if affected == [] and negation_affected == [] do
       state
     else
-      existing_facts = build_facts_map(state)
-
-      new_facts =
-        Enum.flat_map(affected, fn rule ->
-          Incremental.compute_delta(rule, {predicate, tuple}, existing_facts)
-        end)
-        |> Enum.uniq()
+      # If any affected rule has negations, compute_delta can't handle them
+      # correctly, so fall back to full re-derivation for correctness.
+      affected_have_negations =
+        Enum.any?(affected, fn rule -> rule.negations != [] end)
 
-      new_storage =
-        Enum.reduce(new_facts, state.storage_state, fn {pred, args}, st ->
-          {:ok, st} = state.storage_mod.insert(st, pred, args)
-          st
-        end)
-
-      %{state | storage_state: new_storage}
+      if negation_affected != [] or affected_have_negations do
+        full_rederive(state)
+      else
+        # Pure positive derivation with fixpoint iteration
+        derive_to_fixpoint(state, affected, [{predicate, tuple}])
+      end
     end
   end
 
-  defp incrementally_retract(state, predicate, tuple) do
+  defp incrementally_retract(state, predicate, _tuple) do
     affected = Incremental.affected_rules(state.rules, predicate)
+    negation_affected = rules_negating(state.rules, predicate)
 
-    if affected == [] do
+    if affected == [] and negation_affected == [] do
       state
     else
-      existing_facts = build_facts_map(state)
+      # Retraction with recursive rules requires full re-derivation for
+      # correctness. The per-rule compute_retractions approach cannot
+      # correctly handle transitive chains or multi-rule derivation paths.
+      full_rederive(state)
+    end
+  end
+
+  # Iterate delta derivation to a fixpoint for recursive rules.
+  # Each pass may produce new facts that enable further derivations.
+  defp derive_to_fixpoint(state, _affected_rules, []) do
+    state
+  end
+
+  defp derive_to_fixpoint(state, affected_rules, delta_facts) do
+    existing_facts = build_facts_map(state)
 
-      retractions =
-        Enum.flat_map(affected, fn rule ->
-          Incremental.compute_retractions(rule, {predicate, tuple}, existing_facts)
+    new_facts =
+      Enum.flat_map(delta_facts, fn delta ->
+        Enum.flat_map(affected_rules, fn rule ->
+          Incremental.compute_delta(rule, delta, existing_facts)
         end)
-        |> Enum.uniq()
+      end)
+      |> Enum.uniq()
+
+    # Filter out facts that already exist in storage
+    truly_new =
+      Enum.reject(new_facts, fn {pred, args} ->
+        case state.storage_mod.lookup(state.storage_state, pred, args) do
+          {:ok, [_ | _]} -> true
+          _ -> false
+        end
+      end)
 
+    if truly_new == [] do
+      state
+    else
       new_storage =
-        Enum.reduce(retractions, state.storage_state, fn {pred, args}, st ->
-          {:ok, st} = state.storage_mod.delete(st, pred, args)
+        Enum.reduce(truly_new, state.storage_state, fn {pred, args}, st ->
+          {:ok, st} = state.storage_mod.insert(st, pred, args)
           st
         end)
 
-      %{state | storage_state: new_storage}
+      state = %{state | storage_state: new_storage}
+
+      # Recurse: the newly derived facts may trigger further derivations
+      # (for recursive rules). Only check rules affected by the derived predicates.
+      derived_preds = truly_new |> Enum.map(fn {pred, _} -> pred end) |> Enum.uniq()
+
+      next_affected =
+        Enum.filter(state.rules, fn rule ->
+          MapSet.member?(Rule.depends_on(rule), Enum.at(derived_preds, 0)) or
+            Enum.any?(derived_preds, &MapSet.member?(Rule.depends_on(rule), &1))
+        end)
+
+      derive_to_fixpoint(state, next_affected, truly_new)
+    end
+  end
+
+  # Full re-derivation: clear all derived predicates and re-evaluate from
+  # base facts. Used when incremental maintenance cannot guarantee correctness
+  # (negation changes, retraction with recursive rules).
+  defp full_rederive(state) do
+    derived_preds = derived_predicates(state.rules)
+    clean_storage = clear_predicates(state.storage_mod, state.storage_state, derived_preds)
+
+    case Evaluator.evaluate(state.rules, clean_storage, state.storage_mod) do
+      {:ok, _derived, new_storage_state} ->
+        %{state | storage_state: new_storage_state}
+
+      {:error, _reason} ->
+        state
     end
   end
 
@@ -408,4 +472,34 @@ defmodule Datalox.Database do
   end
 
   defp matches_pattern?(_, _), do: false
+
+  # Returns the set of predicates that appear as rule heads (derived predicates).
+  defp derived_predicates(rules) do
+    rules
+    |> Enum.map(fn rule -> elem(rule.head, 0) end)
+    |> Enum.uniq()
+  end
+
+  # Returns rules that have the given predicate in their negations.
+  defp rules_negating(rules, predicate) do
+    Enum.filter(rules, fn rule ->
+      Enum.any?(rule.negations, fn {pred, _} -> pred == predicate end)
+    end)
+  end
+
+  # Clears all facts for the given predicates from storage.
+  defp clear_predicates(storage_mod, storage_state, predicates) do
+    Enum.reduce(predicates, storage_state, fn pred, st ->
+      case storage_mod.all(st, pred) do
+        {:ok, facts} ->
+          Enum.reduce(facts, st, fn tuple, s ->
+            {:ok, s} = storage_mod.delete(s, pred, tuple)
+            s
+          end)
+
+        _ ->
+          st
+      end
+    end)
+  end
 end
diff --git a/test/datalox/database_test.exs b/test/datalox/database_test.exs
index 5ede7ff..a7afd28 100644
--- a/test/datalox/database_test.exs
+++ b/test/datalox/database_test.exs
@@ -82,4 +82,143 @@ defmodule Datalox.DatabaseTest do
       assert {:ancestor, ["alice", "carol"]} in results
     end
   end
+
+  describe "incremental derivation with recursive rules" do
+    setup %{db: db} do
+      rules = [
+        Datalox.Rule.new({:ancestor, [:X, :Y]}, [{:parent, [:X, :Y]}]),
+        Datalox.Rule.new({:ancestor, [:X, :Z]}, [
+          {:parent, [:X, :Y]},
+          {:ancestor, [:Y, :Z]}
+        ])
+      ]
+
+      :ok = Database.load_rules(db, rules)
+      {:ok, rules: rules}
+    end
+
+    test "derives transitive facts when asserting after rules loaded", %{db: db} do
+      :ok = Database.assert(db, {:parent, ["alice", "bob"]})
+      :ok = Database.assert(db, {:parent, ["bob", "carol"]})
+
+      results = Database.query(db, {:ancestor, [:_, :_]})
+
+      assert {:ancestor, ["alice", "bob"]} in results
+      assert {:ancestor, ["bob", "carol"]} in results
+      assert {:ancestor, ["alice", "carol"]} in results
+    end
+
+    test "derives deep transitive facts", %{db: db} do
+      :ok = Database.assert(db, {:parent, ["a", "b"]})
+      :ok = Database.assert(db, {:parent, ["b", "c"]})
+      :ok = Database.assert(db, {:parent, ["c", "d"]})
+
+      results = Database.query(db, {:ancestor, [:_, :_]})
+
+      assert {:ancestor, ["a", "b"]} in results
+      assert {:ancestor, ["a", "c"]} in results
+      assert {:ancestor, ["a", "d"]} in results
+      assert {:ancestor, ["b", "c"]} in results
+      assert {:ancestor, ["b", "d"]} in results
+      assert {:ancestor, ["c", "d"]} in results
+    end
+
+    test "retraction removes transitive derived facts", %{db: db} do
+      :ok = Database.assert(db, {:parent, ["a", "b"]})
+      :ok = Database.assert(db, {:parent, ["b", "c"]})
+
+      # Verify transitive fact exists
+      results = Database.query(db, {:ancestor, [:_, :_]})
+      assert {:ancestor, ["a", "c"]} in results
+
+      # Retract the middle link
+      :ok = Database.retract(db, {:parent, ["b", "c"]})
+
+      results = Database.query(db, {:ancestor, [:_, :_]})
+      assert {:ancestor, ["a", "b"]} in results
+      refute Enum.any?(results, fn {_, [_, y]} -> y == "c" end)
+    end
+
+    test "reload rules clears stale derived facts", %{db: db, rules: rules} do
+      :ok = Database.assert(db, {:parent, ["a", "b"]})
+      :ok = Database.assert(db, {:parent, ["b", "c"]})
+
+      results = Database.query(db, {:ancestor, [:_, :_]})
+      assert {:ancestor, ["a", "c"]} in results
+
+      # Retract a fact and reload rules
+      :ok = Database.retract(db, {:parent, ["b", "c"]})
+      :ok = Database.load_rules(db, rules)
+
+      results = Database.query(db, {:ancestor, [:_, :_]})
+      assert {:ancestor, ["a", "b"]} in results
+      refute {:ancestor, ["a", "c"]} in results
+      refute {:ancestor, ["b", "c"]} in results
+    end
+  end
+
+  describe "negation support" do
+    setup %{db: db} do
+      # active(X) :- user(X), not banned(X)
+      rules = [
+        Datalox.Rule.new({:active, [:X]}, [{:user, [:X]}], negations: [{:banned, [:X]}])
+      ]
+
+      :ok = Database.load_rules(db, rules)
+      {:ok, rules: rules}
+    end
+
+    test "derives facts with negation", %{db: db} do
+      :ok = Database.assert(db, {:user, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      assert {:active, ["alice"]} in results
+    end
+
+    test "asserting negated fact retracts derived fact", %{db: db} do
+      :ok = Database.assert(db, {:user, ["alice"]})
+      :ok = Database.assert(db, {:user, ["bob"]})
+
+      results = Database.query(db, {:active, [:_]})
+      assert {:active, ["alice"]} in results
+      assert {:active, ["bob"]} in results
+
+      # Ban alice
+      :ok = Database.assert(db, {:banned, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      refute {:active, ["alice"]} in results
+      assert {:active, ["bob"]} in results
+    end
+
+    test "retracting negated fact re-derives fact", %{db: db} do
+      :ok = Database.assert(db, {:user, ["alice"]})
+      :ok = Database.assert(db, {:banned, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      refute {:active, ["alice"]} in results
+
+      # Unban alice
+      :ok = Database.retract(db, {:banned, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      assert {:active, ["alice"]} in results
+    end
+
+    test "negation does not affect unrelated users", %{db: db} do
+      :ok = Database.assert(db, {:user, ["alice"]})
+      :ok = Database.assert(db, {:user, ["bob"]})
+      :ok = Database.assert(db, {:banned, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      refute {:active, ["alice"]} in results
+      assert {:active, ["bob"]} in results
+
+      :ok = Database.retract(db, {:banned, ["alice"]})
+
+      results = Database.query(db, {:active, [:_]})
+      assert {:active, ["alice"]} in results
+      assert {:active, ["bob"]} in results
+    end
+  end
 end

From b5981d05a689a5fed22665db0c63d504ae0e1a9d Mon Sep 17 00:00:00 2001
From: Sam Rose <samuel@supabase.io>
Date: Sat, 28 Feb 2026 21:12:13 -0500
Subject: [PATCH 2/2] fix: deletes

---
 lib/datalox/database.ex | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/lib/datalox/database.ex b/lib/datalox/database.ex
index 84ac5ef..deb477b 100644
--- a/lib/datalox/database.ex
+++ b/lib/datalox/database.ex
@@ -491,15 +491,16 @@ defmodule Datalox.Database do
   defp clear_predicates(storage_mod, storage_state, predicates) do
     Enum.reduce(predicates, storage_state, fn pred, st ->
       case storage_mod.all(st, pred) do
-        {:ok, facts} ->
-          Enum.reduce(facts, st, fn tuple, s ->
-            {:ok, s} = storage_mod.delete(s, pred, tuple)
-            s
-          end)
-
-        _ ->
-          st
+        {:ok, facts} -> delete_facts(storage_mod, st, pred, facts)
+        _ -> st
       end
     end)
   end
+
+  defp delete_facts(storage_mod, state, pred, facts) do
+    Enum.reduce(facts, state, fn tuple, s ->
+      {:ok, s} = storage_mod.delete(s, pred, tuple)
+      s
+    end)
+  end
 end