giles
15c97119e4
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
explain.sx reconstructs a canonical proof tree (first-rule, first-solution)
by goal-directed search over the saturated db, since Datalog keeps no
provenance; depth-capped for cyclic safety. acl-explain returns
{:allowed? :proof :reason} with the blocking eff_deny proof on denial.
audit.sx is an append-only decision log (monotonic seq, disk serializer).
api gains acl/explain, acl/audit, acl/audit-tail.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
126 lines
4.1 KiB
Plaintext
126 lines
4.1 KiB
Plaintext
;; 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 <lit> :via "edb"} — base EDB fact
|
|
;; {:fact <lit> :rule <head> :body (<node|negleaf> ...)} — derived
|
|
;; {:neg-ok <lit>} — negation verified to fail
|
|
;; {:fact <lit> :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? <bool> :proof <node|nil> :reason <eff_deny proof|nil>}
|
|
;; 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}))))
|