-- File: lean/AuthSpec.lean
-- RBAC Authorization Algebra
-- Agents migrate Python source to TypeScript.
-- This spec is the ground truth — their code is tested against it.

namespace AuthSpec

-- Core types
structure Permission where
  resource : String
  action   : String
  deriving BEq, Repr, DecidableEq

structure Role where
  name        : String
  permissions : List Permission
  inherits    : List String   -- role names this role inherits from
  deriving Repr, DecidableEq

-- Flattened role map for lookup
abbrev RoleMap := List Role

-- Look up a role by name
def findRole (roles : RoleMap) (name : String) : Option Role :=
  roles.find? (fun r => r.name == name)

-- Check direct permission (no inheritance)
def hasDirectPermission (role : Role) (resource action : String) : Bool :=
  role.permissions.any (fun p => p.resource == resource && p.action == action)

-- Internal: depth-limited access check (structural recursion on Nat avoids optParam issues)
def canAccessAux (roles : RoleMap) (roleName resource action : String) : Nat → Bool
  | 0     => false
  | n + 1 =>
    match findRole roles roleName with
    | none      => false
    | some role =>
      hasDirectPermission role resource action ||
      role.inherits.any (fun parentName =>
        canAccessAux roles parentName resource action n)

-- Public API: check permission with inheritance (depth-5 bound is more than enough)
def canAccess (roles : RoleMap) (roleName resource action : String) : Bool :=
  canAccessAux roles roleName resource action 5

-- Key invariants agents' code must satisfy

-- If the role is not in the map, access is always denied
theorem deny_if_no_role (roles : RoleMap) (roleName resource action : String)
    (h : findRole roles roleName = none) :
    canAccess roles roleName resource action = false := by
  simp [canAccess, canAccessAux, h]

-- Direct permission grants access
theorem direct_permission_grants_access
    (roles : RoleMap) (r : Role) (resource action : String)
    (hfound : findRole roles r.name = some r)
    (hperm  : hasDirectPermission r resource action = true) :
    canAccess roles r.name resource action = true := by
  simp [canAccess, canAccessAux, hfound, hperm]

end AuthSpec