@[reducible, inline]

abbrev Cedar.TPE.EntityLoader : Type

Loads everything requested by the set of entity ids, returning Option.none for missing entities. Loading more entities than requested is okay. See EntityLoader.WellBehaved for a formal definition.

Equations

• Cedar.TPE.EntityLoader = (Cedar.Data.Set Cedar.Spec.EntityUID → Cedar.Data.Map Cedar.Spec.EntityUID Cedar.TPE.MaybeEntityData)

def Cedar.TPE.batchedEvaluateLoop (env : Validation.TypeEnv) (residual : Spec.Residual) (req : Spec.Request) (loader : EntityLoader) (store : PartialEntities) : Nat → Spec.Residual

The batched evaluation loop for a single residual expression.

1. Asks for any new entities referenced by the residual
2. Partially evaluates now that new entities are loaded
3. Exits if a value has been found or it hits the maximum iteration limit

Equations

• One or more equations did not get rendered due to their size.
• Cedar.TPE.batchedEvaluateLoop env residual req loader store 0 = residual

def Cedar.TPE.actionEntities (acts : Validation.ActionSchema) : PartialEntities

Equations

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

def Cedar.TPE.batchedEvaluate (env : Validation.TypeEnv) (x : Validation.TypedExpr) (req : Spec.Request) (loader : EntityLoader) (iters : Nat) : Spec.Residual

Evaluate a single cedar expression using an EntityLoader instead of a full Entities store. Performs a maximum of iter number of calls to loader, but may perform fewer when a value is found.

Equations

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

def Cedar.TPE.batchedAuthorizeLoop (env : Validation.TypeEnv) (residuals : List ResidualPolicy) (req : Spec.Request) (loader : EntityLoader) (store : PartialEntities) (n : Nat) : Response

The batched authorization loop for authorization over a list of policies.

Equations

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

def Cedar.TPE.batchedAuthorize (schema : Validation.Schema) (policies : List Spec.Policy) (req : Spec.Request) (loader : EntityLoader) (iters : Nat) : Except Error Response

Evaluate an authorization request using an EntityLoader instead of a full Entities store.

Performs a maximum of iter number of calls to loader, but may perform fewer when an authorization decision is reached early.

Equations

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

def Cedar.TPE.entityLoaderFor (es : Spec.Entities) (uids : Data.Set Spec.EntityUID) : Data.Map Spec.EntityUID (Option Spec.EntityData)

Create an entity loader for a given entity store. This is used for testing.

Equations

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