Proofs about various functions applied to allowAll and denyAll policies, and empty policy sets.

theorem Cedar.Thm.wellTypedPolicies_empty (Γ : Validation.TypeEnv) : SymCC.wellTypedPolicies [] Γ = Except.ok []

wellTypedPolicies on the empty policy set

theorem Cedar.Thm.wellTypedPolicies_allowAll (Γ : Validation.TypeEnv) : SymCC.wellTypedPolicies [Spec.Policy.allowAll] Γ = Except.ok [SymCC.verifyAlwaysAllows.allowAll]

wellTypedPolicies on Policy.allowAll

theorem Cedar.Thm.isAuthorized_empty (εnv : SymCC.SymEnv) : SymCC.isAuthorized [] εnv = Except.ok (SymCC.Term.bool false)

SymCC.isAuthorized on the empty policy set

theorem Cedar.Thm.isAuthorized_allowAll (εnv : SymCC.SymEnv) : SymCC.isAuthorized [SymCC.verifyAlwaysAllows.allowAll] εnv = Except.ok (SymCC.Term.bool true)

SymCC.isAuthorized on verifyAlwaysAllows.allowAll

theorem Cedar.Thm.footprint_allowAll (εnv : SymCC.SymEnv) : SymCC.footprint SymCC.verifyAlwaysAllows.allowAll.toExpr εnv = Data.Set.empty

SymCC.footprint on verifyAlwaysAllows.allowAll.toExpr