;; lib/acl/engine.sx — ACL ruleset + decision reducer over lib/datalog/.
;;
;; The engine is a thin layer: it owns the permit ruleset (SX data rules) and
;; reduces a (subject, action, resource) decision to a Datalog query against a
;; db built from EDB facts. The rule engine itself is Datalog's.
;;
;; Policy — inheritance + federation with deny-overrides:
;;
;;   eff_grant(S,A,R) :- grant(S,A,R).                         ; direct
;;   eff_grant(S,A,R) :- member_of(S,G), eff_grant(G,A,R).     ; group/role chain
;;   eff_grant(S,A,R) :- child_of(R,P), eff_grant(S,A,P).      ; resource tree
;;   eff_grant(S,A,R) :- member_of(S,Role), role_grant(Role,A,R). ; role expansion
;;   eff_grant(S,A,R) :- delegate(Peer,S,A,R),                 ; federated grant
;;                       trust(Peer,L), level_covers(L,A).
;;
;;   eff_deny(S,A,R)  :- deny(S,A,R).                          ; direct
;;   eff_deny(S,A,R)  :- member_of(S,G), eff_deny(G,A,R).      ; group chain
;;   eff_deny(S,A,R)  :- child_of(R,P), eff_deny(S,A,P).       ; resource tree
;;
;;   permit(S,A,R)    :- eff_grant(S,A,R), not eff_deny(S,A,R).
;;
;; DENY-OVERRIDES: an effective deny anywhere in the inheritance closure of
;; (S,A,R) defeats any effective grant — including federated grants. Deny
;; inherits through the *same* group and resource chains as grant, so a
;; group-level or ancestor-resource deny is authoritative for members/
;; descendants. This is the principled, fail-safe reading of "deny wins".
;;
;; FEDERATION — non-transitive trust: a peer's `delegate` fact only grants if a
;; *local* `trust(Peer, L)` exists AND that level `level_covers` the action.
;; Trust is re-checked on every query (it is a body literal), never baked in at
;; fact-ingestion time, so revoking trust or narrowing a level takes effect
;; immediately on the next decision.
;;
;; Termination & stratification:
;;   - eff_grant/eff_deny recurse only over member_of and child_of, which are
;;     EDB relations with no function symbols, so the closure is finite (cyclic
;;     membership/containment just reaches a fixpoint, never loops). The
;;     federation rule is non-recursive.
;;   - permit negates eff_deny; neither eff_grant nor eff_deny depends on
;;     permit, so the program is stratifiable (permit sits in a higher stratum).

(define
  acl-rules
  (quote
    ((eff_grant S A R <- (grant S A R))
      (eff_grant S A R <- (member_of S G) (eff_grant G A R))
      (eff_grant S A R <- (child_of R P) (eff_grant S A P))
      (eff_grant S A R <- (member_of S Role) (role_grant Role A R))
      (eff_grant
        S
        A
        R
        <-
        (delegate Peer S A R)
        (trust Peer L)
        (level_covers L A))
      (eff_deny S A R <- (deny S A R))
      (eff_deny S A R <- (member_of S G) (eff_deny G A R))
      (eff_deny S A R <- (child_of R P) (eff_deny S A P))
      (permit S A R <- (eff_grant S A R) {:neg (eff_deny S A R)}))))

;; Build a Datalog db from a list of EDB facts under the ACL ruleset.
(define acl-build-db (fn (facts) (dl-program-data facts acl-rules)))

;; Core decision: does the db permit subject S to perform action A on
;; resource R? Reduces to a ground Datalog query on the derived `permit`
;; relation — non-empty result means permitted.
(define
  acl-permit?
  (fn
    (db subj act res)
    (> (len (dl-query db (list (quote permit) subj act res))) 0)))