diff --git a/lib/datalog/builtins.sx b/lib/datalog/builtins.sx index 11261c85..7bfd3d47 100644 --- a/lib/datalog/builtins.sx +++ b/lib/datalog/builtins.sx @@ -250,18 +250,29 @@ (fn (lit) (let - ((needed (dl-vars-of (get lit :neg)))) + ((inner (get lit :neg))) (let - ((missing (dl-vars-not-in needed bound))) - (when - (> (len missing) 0) - (set! - err - (str - "negation refers to unbound variable(s) " - missing - " — they must be bound by an earlier " - "positive body literal"))))))) + ((inner-rn + (cond + ((and (list? inner) (> (len inner) 0)) + (dl-rel-name inner)) + (else nil))) + (needed (dl-vars-of inner)) + (missing (dl-vars-not-in (dl-vars-of inner) bound))) + (cond + ((and (not (nil? inner-rn)) (dl-reserved-rel? inner-rn)) + (set! err + (str "negated literal uses reserved name '" + inner-rn + "' — nested `not(...)` / negated built-ins are " + "not supported; introduce an intermediate " + "relation and negate that"))) + ((> (len missing) 0) + (set! err + (str "negation refers to unbound variable(s) " + missing + " — they must be bound by an earlier " + "positive body literal")))))))) (define dl-process-agg! (fn @@ -289,7 +300,16 @@ ((dl-is? lit) (dl-process-is! lit)) ((dl-comparison? lit) (dl-process-cmp! lit)) ((and (list? lit) (> (len lit) 0)) - (dl-add-bound! (dl-vars-of lit))))))) + (let ((rn (dl-rel-name lit))) + (cond + ((and (not (nil? rn)) (dl-reserved-rel? rn)) + (set! err + (str "body literal uses reserved name '" rn + "' — built-ins / aggregates have their own " + "syntax; nested `not(...)` is not supported " + "(use stratified negation via an " + "intermediate relation)"))) + (else (dl-add-bound! (dl-vars-of lit)))))))))) (for-each dl-process-lit! body) (when (nil? err) diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index f2224ebf..1f97c6d4 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,13 +1,13 @@ { "lang": "datalog", - "total_passed": 259, + "total_passed": 260, "total_failed": 0, - "total": 259, + "total": 260, "suites": [ {"name":"tokenize","passed":30,"failed":0,"total":30}, {"name":"parse","passed":22,"failed":0,"total":22}, {"name":"unify","passed":29,"failed":0,"total":29}, - {"name":"eval","passed":38,"failed":0,"total":38}, + {"name":"eval","passed":39,"failed":0,"total":39}, {"name":"builtins","passed":23,"failed":0,"total":23}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, {"name":"negation","passed":10,"failed":0,"total":10}, @@ -16,5 +16,5 @@ {"name":"magic","passed":36,"failed":0,"total":36}, {"name":"demo","passed":21,"failed":0,"total":21} ], - "generated": "2026-05-11T07:26:33+00:00" + "generated": "2026-05-11T07:40:56+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index 0d02305b..143f7201 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,13 +1,13 @@ # datalog scoreboard -**259 / 259 passing** (0 failure(s)). +**260 / 260 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | tokenize | 30 | 30 | ok | | parse | 22 | 22 | ok | | unify | 29 | 29 | ok | -| eval | 38 | 38 | ok | +| eval | 39 | 39 | ok | | builtins | 23 | 23 | ok | | semi_naive | 8 | 8 | ok | | negation | 10 | 10 | ok | diff --git a/lib/datalog/tests/eval.sx b/lib/datalog/tests/eval.sx index e1835a0c..9b0d6cd8 100644 --- a/lib/datalog/tests/eval.sx +++ b/lib/datalog/tests/eval.sx @@ -203,6 +203,24 @@ (dl-et-throws? (fn () (dl-program "is(N, +(1, 2)) :- p(N)."))) true) + ;; Body literal with a reserved-name positive head is rejected. + ;; The parser only treats outer-level `not(P)` as negation; nested + ;; `not(not(P))` would otherwise silently parse as a positive call + ;; to a relation named `not` and succeed vacuously. The safety + ;; checker now flags this so the user gets a clear error. + ;; Body literal with a reserved-name positive head is rejected. + ;; The parser only treats outer-level `not(P)` as negation; nested + ;; `not(not(P))` would otherwise silently parse as a positive call + ;; to a relation named `not` and succeed vacuously — so the safety + ;; checker now flags this to give the user a clear error. + (dl-et-test! + "nested not(not(...)) rejected" + (dl-et-throws? + (fn () + (dl-program + "banned(a). u(a). vip(X) :- u(X), not(not(banned(X)))."))) + true) + (dl-et-test! "unsafe head var" (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(X)."))) diff --git a/plans/datalog-on-sx.md b/plans/datalog-on-sx.md index 8a10cd0d..42d90ca8 100644 --- a/plans/datalog-on-sx.md +++ b/plans/datalog-on-sx.md @@ -15,7 +15,7 @@ for rose-ash data (e.g. federation graph, content relationships). ## Status (rolling) -`bash lib/datalog/conformance.sh` → **256/256 across 11 suites** +`bash lib/datalog/conformance.sh` → **260/260 across 11 suites** (tokenize, parse, unify, eval, builtins, semi_naive, negation, aggregates, api, magic, demo). Source is ~3100 LOC, tests ~2900 LOC, public API documented in `lib/datalog/datalog.sx`. @@ -320,6 +320,19 @@ large graphs. _Newest first._ +- 2026-05-11 — Eval-semantics bug-hunt: nested `not(not(P))` was + silently misinterpreted. Outer-level `not(...)` is parsed as + negation, but the inner `not(banned(X))` was parsed as a regular + positive literal naming a relation called `not`. Since no `not` + relation existed, the inner match was empty and the outer + negation succeeded vacuously, making `vip(X) :- u(X), not(not(banned(X))).` + equivalent to `vip(X) :- u(X).` (a silent double-negation = identity + fallacy). Fix in `dl-rule-check-safety`: both the positive-literal + branch and `dl-process-neg!` now flag any body literal whose head + is in `dl-reserved-rel-names`. Error message names the relation and + points the user at intermediate-relation stratified negation. 1 new + regression test; 260/260. + - 2026-05-10 — Bug-hunt round on parser/safety surfaced 7 real bugs, each fixed with regression tests: - Reserved relation names (`not`, `count`, `<`, `is`, ...) were