This file contains useful lemmas about the Authorizer functions.

theorem Cedar.Thm.determiningPolicies_wf {policies : Spec.Policies} {request : Spec.Request} {entities : Spec.Entities} : (Spec.isAuthorized request entities policies).determiningPolicies.WellFormed

theorem Cedar.Thm.if_hasError_then_exists_error {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} : Spec.hasError policy request entities = true → ∃ (err : Spec.Error), Spec.evaluate policy.toExpr request entities = Except.error err

theorem Cedar.Thm.satisfiedPolicies_order_and_dup_independent {policies₁ policies₂ : Spec.Policies} (effect : Spec.Effect) (request : Spec.Request) (entities : Spec.Entities) : policies₁ ≡ policies₂ → Spec.satisfiedPolicies effect policies₁ request entities = Spec.satisfiedPolicies effect policies₂ request entities

theorem Cedar.Thm.errorPolicies_order_and_dup_independent {policies₁ policies₂ : Spec.Policies} (request : Spec.Request) (entities : Spec.Entities) : policies₁ ≡ policies₂ → Spec.errorPolicies policies₁ request entities = Spec.errorPolicies policies₂ request entities

theorem Cedar.Thm.satisfied_policies_congr_evaluate {ps : Spec.Policies} {r₁ r₂ : Spec.Request} {es₁ es₂ : Spec.Entities} (effect : Spec.Effect) (heq : ∀ (p : Spec.Policy), p ∈ ps → Spec.evaluate p.toExpr r₁ es₁ = Spec.evaluate p.toExpr r₂ es₂) : Spec.satisfiedPolicies effect ps r₁ es₁ = Spec.satisfiedPolicies effect ps r₂ es₂

theorem Cedar.Thm.error_policies_congr_evaluate {ps : Spec.Policies} {r₁ r₂ : Spec.Request} {es₁ es₂ : Spec.Entities} (heq : ∀ (p : Spec.Policy), p ∈ ps → Spec.evaluate p.toExpr r₁ es₁ = Spec.evaluate p.toExpr r₂ es₂) : Spec.errorPolicies ps r₁ es₁ = Spec.errorPolicies ps r₂ es₂

theorem Cedar.Thm.is_authorized_congr_evaluate {ps : Spec.Policies} {r₁ r₂ : Spec.Request} {es₁ es₂ : Spec.Entities} (heq : ∀ (p : Spec.Policy), p ∈ ps → Spec.evaluate p.toExpr r₁ es₁ = Spec.evaluate p.toExpr r₂ es₂) : Spec.isAuthorized r₁ es₁ ps = Spec.isAuthorized r₂ es₂ ps

def Cedar.Thm.alternateErrorPolicies (policies : Spec.Policies) (request : Spec.Request) (entities : Spec.Entities) : Data.Set Spec.PolicyID

an alternate, proved-equivalent, definition of errorPolicies that's easier to prove things about

Equations

• One or more equations did not get rendered due to their size.

theorem Cedar.Thm.alternate_errorPolicies_equiv_errorPolicies (policies : Spec.Policies) (request : Spec.Request) (entities : Spec.Entities) : Spec.errorPolicies policies request entities = alternateErrorPolicies policies request entities

theorem Cedar.Thm.principal_eval_ok_means_principal_in_uid {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} : Spec.evaluate policy.principalScope.toExpr request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) → policy.principalScope.scope.bound = some uid → Spec.inₑ request.principal uid entities = true

theorem Cedar.Thm.resource_eval_ok_means_resource_in_uid {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} : Spec.evaluate policy.resourceScope.toExpr request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) → policy.resourceScope.scope.bound = some uid → Spec.inₑ request.resource uid entities = true

theorem Cedar.Thm.satisfied_implies_principal_scope {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} : Spec.satisfied policy request entities = true → policy.principalScope.scope.bound = some uid → Spec.inₑ request.principal uid entities = true

theorem Cedar.Thm.satisfied_implies_resource_scope {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} : Spec.satisfied policy request entities = true → policy.resourceScope.scope.bound = some uid → Spec.inₑ request.resource uid entities = true

theorem Cedar.Thm.mapM_evaluate_uids_produces_uids (list : List Spec.EntityUID) (request : Spec.Request) (entities : Spec.Entities) : List.mapM (fun (x : Spec.Expr) => Spec.evaluate x request entities) (List.map (fun (uid : Spec.EntityUID) => Spec.Expr.lit (Spec.Prim.entityUID uid)) list) = Except.ok (List.map (Spec.Value.prim ∘ Spec.Prim.entityUID) list)

theorem Cedar.Thm.asEntityUID_of_uid (uid : Spec.EntityUID) : (Spec.Value.prim (Spec.Prim.entityUID uid)).asEntityUID = Except.ok uid

theorem Cedar.Thm.mapM_asEntityUID_of_uid (uids : List Spec.EntityUID) : List.mapM Spec.Value.asEntityUID (List.map (Spec.Value.prim ∘ Spec.Prim.entityUID) uids) = Except.ok uids

theorem Cedar.Thm.Except.isOk_iff_exists {ε : Type u_1} {α : Type u_2} {x : Except ε α} : x.isOk = true ↔ ∃ (a : α), x = Except.ok a

Batteries has Option.isSome_iff_exists, but not this analogue for Except

theorem Cedar.Thm.if_mapM_doesn't_fail_on_list_then_doesn't_fail_on_set {α : Type u_1} {ε : Type u_2} {β : Type u_3} [LT α] [DecidableLT α] [Data.StrictLT α] {f : α → Except ε β} {as : List α} : (List.mapM f as).isOk = true → (List.mapM f (Data.Set.make as).elts).isOk = true

theorem Cedar.Thm.mapM_asEntityUID_on_set_uids_produces_ok (uids : List Spec.EntityUID) : (List.mapM Spec.Value.asEntityUID (Data.Set.make (List.map (Spec.Value.prim ∘ Spec.Prim.entityUID) uids)).elts).isOk = true

theorem Cedar.Thm.mapOrErr_value_asEntityUID_on_uids_produces_set (list : List Spec.EntityUID) (err : Spec.Error) : Data.Set.mapOrErr Spec.Value.asEntityUID (Data.Set.make (List.map (Spec.Value.prim ∘ Spec.Prim.entityUID) list)) err = Except.ok (Data.Set.make list)

theorem Cedar.Thm.action_in_set_of_euids_produces_boolean (list : List Spec.EntityUID) (request : Spec.Request) (entities : Spec.Entities) : producesBool (Spec.Expr.binaryApp Spec.BinaryOp.mem (Spec.Expr.var Spec.Var.action) (Spec.Expr.set (List.map (fun (uid : Spec.EntityUID) => Spec.Expr.lit (Spec.Prim.entityUID uid)) list))) request entities

theorem Cedar.Thm.principal_scope_produces_boolean (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) : producesBool policy.principalScope.toExpr request entities

Lemma: evaluating the principalScope of any policy produces a boolean (and does not error)

theorem Cedar.Thm.action_scope_produces_boolean (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) : producesBool policy.actionScope.toExpr request entities

Lemma: evaluating the actionScope of any policy produces a boolean (and does not error)

theorem Cedar.Thm.resource_scope_produces_boolean (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) : producesBool policy.resourceScope.toExpr request entities

Lemma: evaluating the resourceScope of any policy produces a boolean (and does not error)

theorem Cedar.Thm.produces_boolean_means_not_non_boolean {e : Spec.Expr} {request : Spec.Request} {entities : Spec.Entities} : producesBool e request entities → ¬producesNonBool e request entities

Lemma: if something produces a boolean, it does not produce a non-boolean

theorem Cedar.Thm.principal_scope_does_not_throw (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) (err : Spec.Error) : ¬Spec.evaluate policy.principalScope.toExpr request entities = Except.error err

theorem Cedar.Thm.action_scope_does_not_throw (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) (err : Spec.Error) : ¬Spec.evaluate policy.actionScope.toExpr request entities = Except.error err

theorem Cedar.Thm.resource_scope_does_not_throw (policy : Spec.Policy) (request : Spec.Request) (entities : Spec.Entities) (err : Spec.Error) : ¬Spec.evaluate policy.resourceScope.toExpr request entities = Except.error err

theorem Cedar.Thm.principal_scope_false_then_policy_false {req : Spec.Request} {entities : Spec.Entities} {p : Spec.Policy} (hp : Spec.evaluate p.principalScope.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))) : Spec.evaluate p.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))

theorem Cedar.Thm.action_scope_false_then_policy_false {req : Spec.Request} {entities : Spec.Entities} {p : Spec.Policy} (ha : Spec.evaluate p.actionScope.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))) : Spec.evaluate p.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))

theorem Cedar.Thm.resource_scope_false_then_policy_false {req : Spec.Request} {entities : Spec.Entities} {p : Spec.Policy} (hr : Spec.evaluate p.resourceScope.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))) : Spec.evaluate p.toExpr req entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))

theorem Cedar.Thm.error_implies_scope_satisfied {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {err : Spec.Error} : Spec.evaluate policy.toExpr request entities = Except.error err → Spec.evaluate policy.principalScope.toExpr request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate policy.actionScope.toExpr request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate policy.resourceScope.toExpr request entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))

For a policy to throw an error, we must have at least gotten past the scope, so the scope constraints must have been satisfied.

theorem Cedar.Thm.error_implies_principal_scope_in {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} {err : Spec.Error} : Spec.evaluate policy.toExpr request entities = Except.error err → policy.principalScope.scope.bound = some uid → Spec.inₑ request.principal uid entities = true

For a policy to throw an error, we must have at least gotten past the scope, so the scope constraints must have been satisfied.

theorem Cedar.Thm.error_implies_resource_scope_in {policy : Spec.Policy} {request : Spec.Request} {entities : Spec.Entities} {uid : Spec.EntityUID} {err : Spec.Error} : Spec.evaluate policy.toExpr request entities = Except.error err → policy.resourceScope.scope.bound = some uid → Spec.inₑ request.resource uid entities = true

For a policy to throw an error, we must have at least gotten past the scope, so the scope constraints must have been satisfied.