def Cedar.Spec.Residual.isTrue : Residual → Bool

Equations

• (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool true)) ty).isTrue = true
• x✝.isTrue = false

def Cedar.Spec.Residual.isFalse : Residual → Bool

Equations

• (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool false)) ty).isFalse = true
• x✝.isFalse = false

structure Cedar.TPE.ResidualPolicy : Type

• id : Spec.PolicyID
• effect : Spec.Effect
• residual : Spec.Residual

def Cedar.TPE.ResidualPolicy.satisfied (policy : ResidualPolicy) : Bool

Equations

• policy.satisfied = policy.residual.isTrue

def Cedar.TPE.ResidualPolicy.hasError (policy : ResidualPolicy) : Bool

Equations

• policy.hasError = policy.residual.isError

def Cedar.TPE.ResidualPolicy.isFalse (policy : ResidualPolicy) : Bool

Equations

• policy.isFalse = policy.residual.isFalse

def Cedar.TPE.ResidualPolicy.isResidual (policy : ResidualPolicy) : Bool

Equations

• policy.isResidual = (!policy.satisfied && !policy.isFalse && !policy.hasError)

def Cedar.TPE.ResidualPolicy.erroredWithEffect (effect : Spec.Effect) (policy : ResidualPolicy) : Option Spec.PolicyID

Equations

• Cedar.TPE.ResidualPolicy.erroredWithEffect effect policy = if (policy.effect == effect && policy.hasError) = true then some policy.id else none

def Cedar.TPE.ResidualPolicy.falseWithEffect (effect : Spec.Effect) (policy : ResidualPolicy) : Option Spec.PolicyID

Equations

• Cedar.TPE.ResidualPolicy.falseWithEffect effect policy = if (policy.effect == effect && policy.isFalse) = true then some policy.id else none

def Cedar.TPE.ResidualPolicy.residualWithEffect (effect : Spec.Effect) (policy : ResidualPolicy) : Option Spec.PolicyID

Equations

• Cedar.TPE.ResidualPolicy.residualWithEffect effect policy = if (policy.effect == effect && policy.isResidual) = true then some policy.id else none

def Cedar.TPE.ResidualPolicy.satisfiedWithEffect (effect : Spec.Effect) (policy : ResidualPolicy) : Option Spec.PolicyID

Equations

• Cedar.TPE.ResidualPolicy.satisfiedWithEffect effect policy = if (policy.effect == effect && policy.satisfied) = true then some policy.id else none

structure Cedar.TPE.Response : Type

• decision : Option Spec.Decision
• satisfiedPermits : Data.Set Spec.PolicyID
• falsePermits : Data.Set Spec.PolicyID
• errorPermits : Data.Set Spec.PolicyID
• residualPermits : Data.Set Spec.PolicyID
• satisfiedForbids : Data.Set Spec.PolicyID
• falseForbids : Data.Set Spec.PolicyID
• errorForbids : Data.Set Spec.PolicyID
• residualForbids : Data.Set Spec.PolicyID
• residuals : List ResidualPolicy

def Cedar.TPE.isAuthorized (schema : Validation.Schema) (policies : List Spec.Policy) (req : PartialRequest) (es : PartialEntities) : Except Error Response

Equations

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

def Cedar.TPE.isAuthorized.satisfiedPolicies (effect : Spec.Effect) (policies : List ResidualPolicy) : Data.Set Spec.PolicyID

Equations

• Cedar.TPE.isAuthorized.satisfiedPolicies effect policies = Cedar.Data.Set.make (List.filterMap (Cedar.TPE.ResidualPolicy.satisfiedWithEffect effect) policies)

def Cedar.TPE.isAuthorized.errorPolicies (effect : Spec.Effect) (policies : List ResidualPolicy) : Data.Set Spec.PolicyID

Equations

• Cedar.TPE.isAuthorized.errorPolicies effect policies = Cedar.Data.Set.make (List.filterMap (Cedar.TPE.ResidualPolicy.erroredWithEffect effect) policies)

def Cedar.TPE.isAuthorized.residualPolicies (effect : Spec.Effect) (policies : List ResidualPolicy) : Data.Set Spec.PolicyID

Equations

• Cedar.TPE.isAuthorized.residualPolicies effect policies = Cedar.Data.Set.make (List.filterMap (Cedar.TPE.ResidualPolicy.residualWithEffect effect) policies)

def Cedar.TPE.isAuthorized.falsePolicies (effect : Spec.Effect) (policies : List ResidualPolicy) : Data.Set Spec.PolicyID

Equations

• Cedar.TPE.isAuthorized.falsePolicies effect policies = Cedar.Data.Set.make (List.filterMap (Cedar.TPE.ResidualPolicy.falseWithEffect effect) policies)

def Cedar.TPE.isAuthorized.isAuthorizedFromResiduals (residuals : List ResidualPolicy) : Response

Equations

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

def Cedar.TPE.Response.reauthorize (response : Response) (req : Spec.Request) (es : Spec.Entities) : Spec.Response

Take a partial authorization Response and fully evaluate it using a concrete requests and entities. This implementation of this function is fully analogous to the concrete isAuthorized function, only working with residuals instead of policies.

Equations

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

def Cedar.TPE.Response.reauthorize.satisfied (rp : ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Bool

Equations

• Cedar.TPE.Response.reauthorize.satisfied rp req entities = decide (rp.residual.evaluate req entities = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool true)))

def Cedar.TPE.Response.reauthorize.satisfiedWithEffect (effect : Spec.Effect) (rp : ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Option Spec.PolicyID

Equations

• Cedar.TPE.Response.reauthorize.satisfiedWithEffect effect rp req entities = if (rp.effect == effect && Cedar.TPE.Response.reauthorize.satisfied rp req entities) = true then some rp.id else none

def Cedar.TPE.Response.reauthorize.satisfiedPolicies (effect : Spec.Effect) (rsp : List ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Data.Set Spec.PolicyID

Equations

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

def Cedar.TPE.Response.reauthorize.hasError (rp : ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Bool

Equations

• Cedar.TPE.Response.reauthorize.hasError rp req entities = match rp.residual.evaluate req entities with | Except.ok a => false | Except.error a => true

def Cedar.TPE.Response.reauthorize.errored (rp : ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Option Spec.PolicyID

Equations

• Cedar.TPE.Response.reauthorize.errored rp req entities = if Cedar.TPE.Response.reauthorize.hasError rp req entities = true then some rp.id else none

def Cedar.TPE.Response.reauthorize.errorPolicies (rps : List ResidualPolicy) (req : Spec.Request) (entities : Spec.Entities) : Data.Set Spec.PolicyID

Equations

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