Cedar.Validation.Linker

This file implements linker that links two partial schemas (RFC 116).

source

inductive Cedar.Validation.LinkError :

Type

actionEntityTypeDeclared (ety : Spec.EntityType) : LinkError
An entity type has the same name as the type of an action.
duplicateEntityType (ety : Spec.EntityType) : LinkError
Both partial schemas define the entity type.
duplicateAction (uid : Spec.EntityUID) : LinkError
Both partial schemas define the action.
externalIsEnum (ety : Spec.EntityType) : LinkError
An external entity type links to an enumerated entity type.
externalAncestorsNotInDefinition (ety : Spec.EntityType) : LinkError
An external entity has ancestors absent from its definition.
externalAncestorIsEnum (ety : Spec.EntityType) : LinkError
An external entity type has an enumerated entity type among its ancestors.
definedEntityAncestorsChanged (ety : Spec.EntityType) : LinkError
Linking would add ancestors to a defined entity type.
externalActionParentsMismatch (uid : Spec.EntityUID) : LinkError
Two declarations of an action have different parents.

Instances For

source

def Cedar.Validation.instReprLinkError.repr :

LinkError → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Cedar.Validation.instReprLinkError :

Repr LinkError

Equations

Cedar.Validation.instReprLinkError = { reprPrec := Cedar.Validation.instReprLinkError.repr }

source

@[instance_reducible]

instance Cedar.Validation.instDecidableEqLinkError :

DecidableEq LinkError

Equations

Cedar.Validation.instDecidableEqLinkError = Cedar.Validation.instDecidableEqLinkError.decEq

source

def Cedar.Validation.instDecidableEqLinkError.decEq (x✝ x✝¹ : LinkError) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Cedar.Validation.instToStringLinkError :

ToString LinkError

Equations

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

source

def Cedar.Validation.closeAncestorsRound {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (m : Data.Map α (Data.Set α)) :

Data.Map α (Data.Set α)

One round of closure, which adds the current ancestors of every member. The result is well-formed when every set in m is.

Equations

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

Instances For

source

def Cedar.Validation.closeAncestorsIter {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] :

Nat → Data.Map α (Data.Set α) → Data.Map α (Data.Set α)

At most n rounds of closure, stopping as soon as a round changes nothing. Each round looks up ancestors in the previous round's map, so reach doubles and the closure is reached after logarithmically many rounds; the key count closeAncestors passes is a far looser bound.

Equations

Cedar.Validation.closeAncestorsIter 0 x✝ = x✝
Cedar.Validation.closeAncestorsIter n.succ x✝ = if Cedar.Validation.closeAncestorsRound x✝ = x✝ then x✝ else Cedar.Validation.closeAncestorsIter n (Cedar.Validation.closeAncestorsRound x✝)

Instances For

source

def Cedar.Validation.closeAncestors {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (parents : Data.Map α (Data.Set α)) :

Data.Map α (Data.Set α)

Close each set of parents under the parent relation, so it holds all ancestors. The number of keys bounds the rounds needed.

Equations

Cedar.Validation.closeAncestors parents = Cedar.Validation.closeAncestorsIter parents.size parents

Instances For

source

def Cedar.Validation.PartialEntitySchema.closeForLink (ets : PartialEntitySchema) :

Except LinkError PartialEntitySchema

Close entity ancestors if doing so does not change a defined entity. Error if taking closure causes any completed entity ancestor to enlarge. Error if an external entity type has an enumerated ancestor, which no definition of it could list.

Equations

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

Instances For

source

def Cedar.Validation.PartialEntitySchemaEntry.link (ety : Spec.EntityType) :

PartialEntitySchemaEntry → PartialEntitySchemaEntry → Except LinkError PartialEntitySchemaEntry

Link a single PartialEntitySchemaEntry. Error when both are not external. Error when the defined entity is Enum. Error when an external ancestor is absent from the entity's definition.

Equations

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

Instances For

source

def Cedar.Validation.PartialActionSchemaEntry.link (uid : Spec.EntityUID) :

PartialActionSchemaEntry → PartialActionSchemaEntry → Except LinkError PartialActionSchemaEntry

Link a single PartialActionSchemaEntry. Error when both are not external. Error when they do not have the same ancestors.

Equations

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

Instances For

source

def Cedar.Validation.linkMaps {α : Type u_1} {β : Type (max u_2 u_1)} [LT α] [DecidableLT α] [DecidableEq α] (f : α → β → β → Except LinkError β) (m₁ m₂ : Data.Map α β) :

Except LinkError (Data.Map α β)

Entity names from both first and second are linked. Entity names appearing in only one of them are appended.

Equations

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

Instances For

source

def Cedar.Validation.link (p c : PartialSchema) :

Except LinkError PartialSchema

Link two partial schemas. Error if partial schema have colliding names across action types and entity types.

Equations

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

Instances For