structure Cedar.TPE.PartialEntityUID : Type

• ty : Spec.EntityType
• id : Option String

@[instance_reducible]

instance Cedar.TPE.instInhabitedPartialEntityUID : Inhabited PartialEntityUID

Equations

• Cedar.TPE.instInhabitedPartialEntityUID = { default := Cedar.TPE.instInhabitedPartialEntityUID.default }

def Cedar.TPE.PartialEntityUID.asEntityUID (self : PartialEntityUID) : Option Spec.EntityUID

Equations

• self.asEntityUID = Option.map (fun (x : String) => { ty := self.ty, eid := x }) self.id

structure Cedar.TPE.PartialRequest : Type

• principal : PartialEntityUID
• action : Spec.EntityUID
• resource : PartialEntityUID
• context : Option (Data.Map Spec.Attr Spec.Value)

@[instance_reducible]

instance Cedar.TPE.instInhabitedPartialRequest : Inhabited PartialRequest

Equations

• Cedar.TPE.instInhabitedPartialRequest = { default := Cedar.TPE.instInhabitedPartialRequest.default }

structure Cedar.TPE.PartialEntityData : Type

• attrs : Option (Data.Map Spec.Attr Spec.Value)
• ancestors : Option (Data.Set Spec.EntityUID)
• tags : Option (Data.Map Spec.Attr Spec.Value)

@[instance_reducible]

instance Cedar.TPE.instInhabitedPartialEntityData : Inhabited PartialEntityData

Equations

• Cedar.TPE.instInhabitedPartialEntityData = { default := Cedar.TPE.instInhabitedPartialEntityData.default }

@[reducible, inline]

abbrev Cedar.TPE.MaybeEntityData : Type

Equations

• Cedar.TPE.MaybeEntityData = Option Cedar.Spec.EntityData

@[reducible, inline]

abbrev Cedar.TPE.PartialEntities : Type

Equations

• Cedar.TPE.PartialEntities = Cedar.Data.Map Cedar.Spec.EntityUID Cedar.TPE.PartialEntityData

@[instance_reducible]

instance Cedar.TPE.instInhabitedPartialEntities : Inhabited PartialEntities

Equations

• Cedar.TPE.instInhabitedPartialEntities = { default := Cedar.Data.instInhabitedMap.default }

@[reducible, inline]

abbrev Cedar.TPE.SlicedEntities : Type

A subset of an Entities store. When a MaybeEntityData is none, it means that the entity is not present in the backing store.

Equations

• Cedar.TPE.SlicedEntities = Cedar.Data.Map Cedar.Spec.EntityUID Cedar.TPE.MaybeEntityData

def Cedar.TPE.PartialEntities.get {α : Type u_1} (es : PartialEntities) (uid : Spec.EntityUID) (f : PartialEntityData → Option α) : Option α

Equations

• es.get uid f = (Cedar.Data.Map.find? es uid).bind f

def Cedar.TPE.PartialEntities.ancestors (es : PartialEntities) (uid : Spec.EntityUID) : Option (Data.Set Spec.EntityUID)

Equations

• es.ancestors uid = es.get uid Cedar.TPE.PartialEntityData.ancestors

def Cedar.TPE.PartialEntities.tags (es : PartialEntities) (uid : Spec.EntityUID) : Option (Data.Map Spec.Tag Spec.Value)

Equations

• es.tags uid = es.get uid Cedar.TPE.PartialEntityData.tags

def Cedar.TPE.PartialEntities.attrs (es : PartialEntities) (uid : Spec.EntityUID) : Option (Data.Map Spec.Tag Spec.Value)

Equations

• es.attrs uid = es.get uid Cedar.TPE.PartialEntityData.attrs

def Cedar.TPE.partialIsValid {α : Type u_1} (o : Option α) (f : α → Bool) : Bool

Equations

• Cedar.TPE.partialIsValid o f = (Option.map f o).getD true

def Cedar.TPE.requestIsValid (env : Validation.TypeEnv) (req : PartialRequest) : Bool

Equations

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

def Cedar.TPE.validatePartialRequest (schema : Validation.Schema) (req : PartialRequest) : Except Validation.RequestValidationError Validation.TypeEnv

Equations

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

def Cedar.TPE.entitiesIsValid (schema : Validation.Schema) (es : PartialEntities) : Bool

Equations

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

def Cedar.TPE.entitiesIsValid.actionEntityIsValid (schema : Validation.Schema) (uid : Spec.EntityUID) (entityData : PartialEntityData) : Bool

Equations

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

def Cedar.TPE.entitiesIsValid.entityIsValid (schema : Validation.Schema) (p : Spec.EntityUID × PartialEntityData) : Bool

Equations

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

def Cedar.TPE.entitiesIsValid.instanceOfActionSchema (schema : Validation.Schema) (es : PartialEntities) (p : Spec.EntityUID × Validation.ActionSchemaEntry) : Bool

Equations

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

def Cedar.TPE.requestIsConsistent (req₁ : Spec.Request) (req₂ : PartialRequest) : Bool

Every known component of req₂ agrees with req₁.

Equations

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

def Cedar.TPE.entitiesIsConsistent (es₁ : Spec.Entities) (es₂ : PartialEntities) : Bool

Every entity of es₂ is in es₁, and every known component of it agrees with es₁.

Equations

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

inductive Cedar.TPE.ConcretizationError : Type

• typeError : ConcretizationError
• requestsDoNotMatch : ConcretizationError
• entitiesDoNotMatch : ConcretizationError
• invalidEnvironment : ConcretizationError

def Cedar.TPE.isValidAndConsistent (schema : Validation.Schema) (req₁ : Spec.Request) (es₁ : Spec.Entities) (req₂ : PartialRequest) (es₂ : PartialEntities) : Except ConcretizationError Unit

Equations

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

def Cedar.TPE.isValidAndConsistent.requestIsValidAndConsistent (req₁ : Spec.Request) (req₂ : PartialRequest) (env : Validation.TypeEnv) : Except ConcretizationError Unit

Equations

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

def Cedar.TPE.isValidAndConsistent.entitiesIsValidAndConsistent (es₁ : Spec.Entities) (es₂ : PartialEntities) (env : Validation.TypeEnv) : Except ConcretizationError Unit

Equations

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

def Cedar.TPE.isValidAndConsistent.envIsWellFormed (env : Validation.TypeEnv) : Except ConcretizationError Unit

Equations

• Cedar.TPE.isValidAndConsistent.envIsWellFormed env = if (!Except.isOk env.validateWellFormed) = true then Except.error Cedar.TPE.ConcretizationError.typeError else Except.ok ()

def Cedar.Spec.Request.asPartialRequest (req : Request) : TPE.PartialRequest

Equations

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

def Cedar.Spec.EntityData.asPartial (data : EntityData) : TPE.PartialEntityData

Equations

• data.asPartial = { attrs := some data.attrs, ancestors := some data.ancestors, tags := some data.tags }

def Cedar.Spec.Entities.asPartial (entities : Entities) : TPE.PartialEntities

Equations

• entities.asPartial = Cedar.Data.Map.mapOnValues Cedar.Spec.EntityData.asPartial entities

def Cedar.TPE.MaybeEntityData.asPartial : MaybeEntityData → PartialEntityData

subtle: a missing entity bahaves the same way as a concrete entity with empty attrs, ancestors, and tags. This is because

1. Cedar doesn't have a way to check for a presence of a particular entity id in the database.
2. Each of the cedar operations behave the same way when encountering a missing entity compared to a empty one.

This is a necessary condition for the soundness of batched entity loading.

Equations

• Cedar.TPE.MaybeEntityData.asPartial none = { attrs := some Cedar.Data.Map.empty, ancestors := some Cedar.Data.Set.empty, tags := some Cedar.Data.Map.empty }
• Cedar.TPE.MaybeEntityData.asPartial (some d) = d.asPartial

def Cedar.TPE.EntitiesWithMissing.asPartial (store : SlicedEntities) : PartialEntities

Equations

• Cedar.TPE.EntitiesWithMissing.asPartial store = Cedar.Data.Map.mapOnValues Cedar.TPE.MaybeEntityData.asPartial store