/-- The summarizer agent may read the codebase. -/ theorem summarizer_may_read_code : evaluate agentPolicy ⟨"summarizer", "read", "/code"⟩ = .permit := by⊢ evaluate agentPolicy { user := "summarizer", action := "read", resource := "/code" } = Decision.permit auth_proveAll goals completed! 🐙 /-- ...but is explicitly forbidden from writing to it. -/ theorem summarizer_cannot_write_code : evaluate agentPolicy ⟨"summarizer", "write", "/code"⟩ = .deny := by⊢ evaluate agentPolicy { user := "summarizer", action := "write", resource := "/code" } = Decision.deny auth_proveAll goals completed! 🐙 /-- The deployer agent may ship to production. -/ theorem deployer_may_deploy : evaluate agentPolicy ⟨"deployer", "deploy", "/prod"⟩ = .permit := by⊢ evaluate agentPolicy { user := "deployer", action := "deploy", resource := "/prod" } = Decision.permit auth_proveAll goals completed! 🐙 /-- An unprovisioned agent matches no rule: the policy has *no opinion* on it. -/ theorem rogue_agent_unspecified : evaluate agentPolicy ⟨"rogue", "read", "/prod"⟩ = .notApplicable := by⊢ evaluate agentPolicy { user := "rogue", action := "read", resource := "/prod" } = Decision.notApplicable auth_proveAll goals completed! 🐙 /-- The auditor is matched *only* by an `abstain` rule: the policy speaks about it and still deliberately says nothing — a state a Bool could never capture. -/ theorem auditor_explicitly_undecided : evaluate agentPolicy ⟨"auditor", "read", "/logs"⟩ = .notApplicable := by⊢ evaluate agentPolicy { user := "auditor", action := "read", resource := "/logs" } = Decision.notApplicable auth_proveAll goals completed! 🐙