;; 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})))