;; lib/acl/explain.sx — proof-tree reconstruction over the saturated db. ;; ;; lib/datalog/ records derived facts but not their provenance, so the proof is ;; reconstructed here by goal-directed search over the *saturated* db: for a ;; ground goal we find the first ACL rule (in rule order) whose body holds, take ;; the first solution binding its remaining variables, and recurse on each body ;; literal. Negated literals are recorded as verified `:neg-ok` leaves. ;; ;; CANONICAL DERIVATION: the Datalog derivation graph is a DAG (a fact may hold ;; many ways). We pick ONE canonical proof — first matching rule, first solution ;; — matching the rule order in lib/acl/engine.sx (direct/EDB rules first). A ;; depth cap guards against pathological cyclic data producing unbounded search. ;; ;; A proof node is one of: ;; {:fact :via "edb"} — base EDB fact ;; {:fact :rule :body ( ...)} — derived ;; {:neg-ok } — negation verified to fail ;; {:fact :truncated true} — depth cap hit (define acl-proof-max-depth 64) ;; Substitute a body literal, descending into {:neg ...} dicts (dl-apply-subst ;; does not recurse into dicts, which would leak the neg's free vars). (define acl-subst-lit (fn (lit s) (if (and (dict? lit) (has-key? lit :neg)) {:neg (dl-apply-subst (get lit :neg) s)} (dl-apply-subst lit s)))) (define acl-lit-edb? (fn (lit) (and (list? lit) (> (len lit) 0) (symbol? (first lit)) (has-key? acl-edb-arity (symbol->string (first lit)))))) (define acl-subst-zip! (fn (d ks vs) (when (> (len ks) 0) (do (dict-set! d (symbol->string (first ks)) (first vs)) (acl-subst-zip! d (rest ks) (rest vs)))))) ;; Bind a rule head's variables to a ground goal's arguments (positional). (define acl-bind-head (fn (head goal) (let ((d {})) (do (acl-subst-zip! d (rest head) (rest goal)) d)))) (define acl-subst-union (fn (a b) (let ((d {})) (do (for-each (fn (k) (dict-set! d k (get a k))) (keys a)) (for-each (fn (k) (dict-set! d k (get b k))) (keys b)) d)))) (define acl-prove (fn (db goal) (acl-prove-d db goal 0))) (define acl-prove-d (fn (db goal depth) (cond ((> depth acl-proof-max-depth) {:truncated true :fact goal}) ((acl-lit-edb? goal) (if (> (len (dl-query db goal)) 0) {:via "edb" :fact goal} nil)) (else (acl-prove-rules db goal acl-rules depth))))) (define acl-prove-rules (fn (db goal rules depth) (if (= (len rules) 0) nil (let ((p (dl-rule-from-list (first rules)))) (if (= (first (get p :head)) (first goal)) (let ((hs (acl-bind-head (get p :head) goal))) (let ((qbody (map (fn (l) (acl-subst-lit l hs)) (get p :body)))) (let ((sols (dl-query db qbody))) (if (> (len sols) 0) (acl-prove-build db goal p hs (first sols) depth) (acl-prove-rules db goal (rest rules) depth))))) (acl-prove-rules db goal (rest rules) depth)))))) (define acl-prove-build (fn (db goal p hs sol depth) (let ((full (acl-subst-union hs sol))) {:body (map (fn (l) (let ((g (acl-subst-lit l full))) (if (and (dict? g) (has-key? g :neg)) {:neg-ok (get g :neg)} (acl-prove-d db g (+ depth 1))))) (get p :body)) :rule (get p :head) :fact goal}))) ;; Public decision-with-proof. Returns: ;; {:allowed? :proof :reason } ;; When permitted, :proof is the permit derivation. When denied, :proof is nil ;; and :reason carries the blocking eff_deny proof if one exists (an explicit or ;; inherited deny), else nil (simply no grant). (define acl-explain (fn (db subj act res) (let ((proof (acl-prove db (list (quote permit) subj act res)))) (if (= proof nil) {:allowed? false :proof nil :reason (acl-prove db (list (quote eff_deny) subj act res))} {:allowed? true :proof proof :reason nil}))))