datalog: reject body lits with reserved names
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 39s

Nested `not(not(P))` silently misparsed: outer `not(...)` is
recognised as negation, but the inner `not(banned(X))` was parsed
as a positive call to a relation called `not`. With no `not`
relation present, the inner match was empty, the outer negation
succeeded vacuously, and `vip(X) :- u(X), not(not(banned(X))).`
collapsed to `vip(X) :- u(X).` — a silent double-negation = identity
fallacy.

Fix in `dl-rule-check-safety`: the positive-literal branch and
`dl-process-neg!` both reject any body literal whose relation
name is in `dl-reserved-rel-names`. Error message names the
relation and points the user at stratified negation through an
intermediate relation.

1 regression test; conformance 260/260.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-05-11 07:41:49 +00:00
parent dcae125955
commit 285cd530eb
5 changed files with 70 additions and 19 deletions

View File

@@ -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)