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>
317 lines
10 KiB
Plaintext
317 lines
10 KiB
Plaintext
;; lib/acl/tests/explain.sx — Phase 3: proof correctness + audit completeness.
|
|
|
|
(define acl-et-pass 0)
|
|
(define acl-et-fail 0)
|
|
(define acl-et-failures (list))
|
|
|
|
;; Name-based deep equality. The host `=` compares symbols by interned
|
|
;; identity, which is unstable across substitution/saturation; comparing by
|
|
;; name (as the datalog suite does) makes structural assertions deterministic.
|
|
(define
|
|
acl-et-eq?
|
|
(fn
|
|
(a b)
|
|
(cond
|
|
((and (list? a) (list? b))
|
|
(and (= (len a) (len b)) (acl-et-eq-l? a b 0)))
|
|
((and (dict? a) (dict? b))
|
|
(let
|
|
((ka (keys a)) (kb (keys b)))
|
|
(and (= (len ka) (len kb)) (acl-et-eq-d? a b ka 0))))
|
|
((and (symbol? a) (symbol? b))
|
|
(= (symbol->string a) (symbol->string b)))
|
|
(else (= a b)))))
|
|
|
|
(define
|
|
acl-et-eq-l?
|
|
(fn
|
|
(a b i)
|
|
(cond
|
|
((>= i (len a)) true)
|
|
((not (acl-et-eq? (nth a i) (nth b i))) false)
|
|
(else (acl-et-eq-l? a b (+ i 1))))))
|
|
|
|
(define
|
|
acl-et-eq-d?
|
|
(fn
|
|
(a b ka i)
|
|
(cond
|
|
((>= i (len ka)) true)
|
|
((let ((k (nth ka i))) (not (acl-et-eq? (get a k) (get b k))))
|
|
false)
|
|
(else (acl-et-eq-d? a b ka (+ i 1))))))
|
|
|
|
(define
|
|
acl-et-check!
|
|
(fn
|
|
(name got expected)
|
|
(if
|
|
(acl-et-eq? got expected)
|
|
(set! acl-et-pass (+ acl-et-pass 1))
|
|
(do
|
|
(set! acl-et-fail (+ acl-et-fail 1))
|
|
(append!
|
|
acl-et-failures
|
|
(str name "\n expected: " expected "\n got: " got))))))
|
|
|
|
;; --- proof-tree walkers ---
|
|
|
|
;; True if EDB fact `target` appears as a base leaf anywhere in the proof.
|
|
(define
|
|
acl-et-has-leaf?
|
|
(fn
|
|
(node target)
|
|
(cond
|
|
((= node nil) false)
|
|
((and (dict? node) (has-key? node :via))
|
|
(acl-et-eq? (get node :fact) target))
|
|
((and (dict? node) (has-key? node :body))
|
|
(acl-et-any-leaf? (get node :body) target))
|
|
(else false))))
|
|
|
|
(define
|
|
acl-et-any-leaf?
|
|
(fn
|
|
(nodes target)
|
|
(cond
|
|
((= (len nodes) 0) false)
|
|
((acl-et-has-leaf? (first nodes) target) true)
|
|
(else (acl-et-any-leaf? (rest nodes) target)))))
|
|
|
|
;; True if the proof records a verified negation (deny did not fire).
|
|
(define
|
|
acl-et-has-negok?
|
|
(fn
|
|
(node)
|
|
(cond
|
|
((= node nil) false)
|
|
((and (dict? node) (has-key? node :neg-ok)) true)
|
|
((and (dict? node) (has-key? node :body))
|
|
(acl-et-any-negok? (get node :body)))
|
|
(else false))))
|
|
|
|
(define
|
|
acl-et-any-negok?
|
|
(fn
|
|
(nodes)
|
|
(cond
|
|
((= (len nodes) 0) false)
|
|
((acl-et-has-negok? (first nodes)) true)
|
|
(else (acl-et-any-negok? (rest nodes))))))
|
|
|
|
(define
|
|
acl-et-run-all!
|
|
(fn
|
|
()
|
|
(do
|
|
(let
|
|
((db (acl-build-db (list (acl-grant (quote u) (quote read) (quote p))))))
|
|
(let
|
|
((e (acl-explain db (quote u) (quote read) (quote p))))
|
|
(do
|
|
(acl-et-check! "direct: allowed?" (get e :allowed?) true)
|
|
(acl-et-check!
|
|
"direct: proof root fact"
|
|
(get (get e :proof) :fact)
|
|
(list (quote permit) (quote u) (quote read) (quote p)))
|
|
(acl-et-check!
|
|
"direct: grant leaf present"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote grant) (quote u) (quote read) (quote p)))
|
|
true)
|
|
(acl-et-check!
|
|
"direct: negation verified"
|
|
(acl-et-has-negok? (get e :proof))
|
|
true)
|
|
(acl-et-check!
|
|
"direct: reason nil when allowed"
|
|
(get e :reason)
|
|
nil))))
|
|
(let
|
|
((db (acl-build-db (list (acl-member-of (quote alice) (quote team)) (acl-member-of (quote team) (quote org)) (acl-grant (quote org) (quote read) (quote doc))))))
|
|
(let
|
|
((e (acl-explain db (quote alice) (quote read) (quote doc))))
|
|
(do
|
|
(acl-et-check! "group: allowed?" (get e :allowed?) true)
|
|
(acl-et-check!
|
|
"group: member_of alice leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote member_of) (quote alice) (quote team)))
|
|
true)
|
|
(acl-et-check!
|
|
"group: member_of team leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote member_of) (quote team) (quote org)))
|
|
true)
|
|
(acl-et-check!
|
|
"group: grant org leaf at base"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote grant) (quote org) (quote read) (quote doc)))
|
|
true))))
|
|
(let
|
|
((db (acl-build-db (list (acl-child-of (quote sec) (quote book)) (acl-grant (quote u) (quote read) (quote book))))))
|
|
(let
|
|
((e (acl-explain db (quote u) (quote read) (quote sec))))
|
|
(do
|
|
(acl-et-check! "resource: allowed?" (get e :allowed?) true)
|
|
(acl-et-check!
|
|
"resource: child_of leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote child_of) (quote sec) (quote book)))
|
|
true)
|
|
(acl-et-check!
|
|
"resource: grant on parent leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote grant) (quote u) (quote read) (quote book)))
|
|
true))))
|
|
(let
|
|
((db (acl-build-db (list (acl-member-of (quote bob) (quote editor)) (acl-role-grant (quote editor) (quote edit) (quote page1))))))
|
|
(let
|
|
((e (acl-explain db (quote bob) (quote edit) (quote page1))))
|
|
(do
|
|
(acl-et-check! "role: allowed?" (get e :allowed?) true)
|
|
(acl-et-check!
|
|
"role: member_of leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list (quote member_of) (quote bob) (quote editor)))
|
|
true)
|
|
(acl-et-check!
|
|
"role: role_grant leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :proof)
|
|
(list
|
|
(quote role_grant)
|
|
(quote editor)
|
|
(quote edit)
|
|
(quote page1)))
|
|
true))))
|
|
(let
|
|
((db (acl-build-db (list (acl-grant (quote u) (quote edit) (quote p)) (acl-deny (quote u) (quote edit) (quote p))))))
|
|
(let
|
|
((e (acl-explain db (quote u) (quote edit) (quote p))))
|
|
(do
|
|
(acl-et-check! "deny: not allowed" (get e :allowed?) false)
|
|
(acl-et-check! "deny: no proof" (get e :proof) nil)
|
|
(acl-et-check!
|
|
"deny: reason root is eff_deny"
|
|
(get (get e :reason) :fact)
|
|
(list (quote eff_deny) (quote u) (quote edit) (quote p)))
|
|
(acl-et-check!
|
|
"deny: reason has deny leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :reason)
|
|
(list (quote deny) (quote u) (quote edit) (quote p)))
|
|
true))))
|
|
(let
|
|
((db (acl-build-db (list (acl-member-of (quote alice) (quote team)) (acl-grant (quote alice) (quote read) (quote doc)) (acl-deny (quote team) (quote read) (quote doc))))))
|
|
(let
|
|
((e (acl-explain db (quote alice) (quote read) (quote doc))))
|
|
(do
|
|
(acl-et-check!
|
|
"inherited deny: not allowed"
|
|
(get e :allowed?)
|
|
false)
|
|
(acl-et-check!
|
|
"inherited deny: reason has member_of leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :reason)
|
|
(list (quote member_of) (quote alice) (quote team)))
|
|
true)
|
|
(acl-et-check!
|
|
"inherited deny: reason has group deny leaf"
|
|
(acl-et-has-leaf?
|
|
(get e :reason)
|
|
(list (quote deny) (quote team) (quote read) (quote doc)))
|
|
true))))
|
|
(let
|
|
((db (acl-build-db (list))))
|
|
(let
|
|
((e (acl-explain db (quote u) (quote read) (quote p))))
|
|
(do
|
|
(acl-et-check! "no grant: not allowed" (get e :allowed?) false)
|
|
(acl-et-check! "no grant: proof nil" (get e :proof) nil)
|
|
(acl-et-check! "no grant: reason nil" (get e :reason) nil))))
|
|
(let
|
|
((db (acl-build-db (list (acl-grant (quote u) (quote read) (quote p)) (acl-deny (quote u) (quote edit) (quote p))))))
|
|
(do
|
|
(acl-audit-clear!)
|
|
(acl-et-check! "audit: starts empty" (acl-audit-count) 0)
|
|
(acl-et-check!
|
|
"audit decide allowed returns true"
|
|
(acl-audit-decide! db (quote u) (quote read) (quote p))
|
|
true)
|
|
(acl-et-check!
|
|
"audit decide denied returns false"
|
|
(acl-audit-decide! db (quote u) (quote edit) (quote p))
|
|
false)
|
|
(acl-audit-decide! db (quote u) (quote comment) (quote p))
|
|
(acl-et-check!
|
|
"audit: count after three decisions"
|
|
(acl-audit-count)
|
|
3)
|
|
(acl-et-check!
|
|
"audit: tail size respects n"
|
|
(len (acl-audit-tail 2))
|
|
2)
|
|
(acl-et-check!
|
|
"audit: tail returns most recent"
|
|
(get (first (acl-audit-tail 1)) :act)
|
|
(quote comment))
|
|
(acl-et-check!
|
|
"audit: first record seq is 0"
|
|
(get (first (acl-audit-tail 3)) :seq)
|
|
0)
|
|
(acl-et-check!
|
|
"audit: allowed flag recorded"
|
|
(get (first (acl-audit-tail 3)) :allowed?)
|
|
true)
|
|
(acl-et-check!
|
|
"audit: serialize line count"
|
|
(len (acl-et-lines (acl-audit-serialize)))
|
|
3)
|
|
(acl-audit-clear!)
|
|
(acl-et-check!
|
|
"audit: clear resets count"
|
|
(acl-audit-count)
|
|
0))))))
|
|
|
|
;; count newline-terminated lines in a serialized log
|
|
(define acl-et-lines (fn (s) (acl-et-count-nl s 0 0)))
|
|
(define
|
|
acl-et-count-nl
|
|
(fn
|
|
(s i n)
|
|
(if
|
|
(>= i (len s))
|
|
(if (= n 0) (list) (acl-et-rangelist n))
|
|
(acl-et-count-nl
|
|
s
|
|
(+ i 1)
|
|
(if (= (slice s i (+ i 1)) "\n") (+ n 1) n)))))
|
|
(define
|
|
acl-et-rangelist
|
|
(fn
|
|
(n)
|
|
(if
|
|
(<= n 0)
|
|
(list)
|
|
(cons n (acl-et-rangelist (- n 1))))))
|
|
|
|
(define
|
|
acl-explain-tests-run!
|
|
(fn
|
|
()
|
|
(do
|
|
(set! acl-et-pass 0)
|
|
(set! acl-et-fail 0)
|
|
(set! acl-et-failures (list))
|
|
(acl-et-run-all!)
|
|
{:failures acl-et-failures :total (+ acl-et-pass acl-et-fail) :passed acl-et-pass :failed acl-et-fail})))
|