This file includes boolean definitions for the propositions declared in Cedar/Thm/Validation/Typechecker/Types.lean.

inductive Cedar.Validation.RequestValidationError : Type

• typeError (msg : String) : RequestValidationError

@[reducible, inline]

abbrev Cedar.Validation.RequestValidationResult : Type

Equations

• Cedar.Validation.RequestValidationResult = Except Cedar.Validation.RequestValidationError Unit

inductive Cedar.Validation.EntityValidationError : Type

• typeError (msg : String) : EntityValidationError

@[reducible, inline]

abbrev Cedar.Validation.EntityValidationResult : Type

Equations

• Cedar.Validation.EntityValidationResult = Except Cedar.Validation.EntityValidationError Unit

def Cedar.Validation.instanceOfBoolType (b : Bool) (bty : BoolType) : Bool

Equations

• Cedar.Validation.instanceOfBoolType true Cedar.Validation.BoolType.tt = true
• Cedar.Validation.instanceOfBoolType false Cedar.Validation.BoolType.ff = true
• Cedar.Validation.instanceOfBoolType b Cedar.Validation.BoolType.anyBool = true
• Cedar.Validation.instanceOfBoolType b bty = false

def Cedar.Validation.instanceOfEntityType (e : Spec.EntityUID) (ety : Spec.EntityType) (env : TypeEnv) : Bool

Equations

• Cedar.Validation.instanceOfEntityType e ety env = (ety == e.ty && (env.ets.isValidEntityUID e || env.acts.contains e))

def Cedar.Validation.instanceOfExtType (ext : Spec.Ext) (extty : ExtType) : Bool

Equations

• Cedar.Validation.instanceOfExtType (Cedar.Spec.Ext.decimal d) Cedar.Validation.ExtType.decimal = true
• Cedar.Validation.instanceOfExtType (Cedar.Spec.Ext.ipaddr ip) Cedar.Validation.ExtType.ipAddr = true
• Cedar.Validation.instanceOfExtType (Cedar.Spec.Ext.datetime dt) Cedar.Validation.ExtType.datetime = true
• Cedar.Validation.instanceOfExtType (Cedar.Spec.Ext.duration dur) Cedar.Validation.ExtType.duration = true
• Cedar.Validation.instanceOfExtType ext extty = false

def Cedar.Validation.requiredAttributePresent (r : Data.Map Spec.Attr Spec.Value) (rty : Data.Map Spec.Attr (Qualified CedarType)) (k : Spec.Attr) : Bool

Equations

• Cedar.Validation.requiredAttributePresent r rty k = match rty.find? k with | some qty => if qty.isRequired = true then r.contains k else true | x => true

@[irreducible]

def Cedar.Validation.instanceOfType (v : Spec.Value) (ty : CedarType) (env : TypeEnv) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.instanceOfType (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b)) (Cedar.Validation.CedarType.bool bty) env = Cedar.Validation.instanceOfBoolType b bty
• Cedar.Validation.instanceOfType (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)) Cedar.Validation.CedarType.int env = true
• Cedar.Validation.instanceOfType (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)) Cedar.Validation.CedarType.string env = true
• Cedar.Validation.instanceOfType (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID e)) (Cedar.Validation.CedarType.entity ety) env = Cedar.Validation.instanceOfEntityType e ety env
• Cedar.Validation.instanceOfType (Cedar.Spec.Value.ext x) (Cedar.Validation.CedarType.ext xty) env = Cedar.Validation.instanceOfExtType x xty
• Cedar.Validation.instanceOfType v ty env = false

def Cedar.Validation.instanceOfRequestType (request : Spec.Request) (env : TypeEnv) : Bool

Equations

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

def Cedar.Validation.instanceOfSchema (entities : Spec.Entities) (env : TypeEnv) : EntityValidationResult

For every entity in the store,

1. The entity's type is defined in the type store (either ets or as for action entities).
2. The entity's attributes match the attribute types indicated in the type store.
3. The entity's ancestors' types are consistent with the ancestor information in the type store.
4. The entity's tags' types are consistent with the tags information in the type store.

For every action in the entity store, the action's ancestors are consistent with the ancestor information in the action store.

Equations

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

def Cedar.Validation.instanceOfSchema.instanceOfEntityTags (env : TypeEnv) (data : Spec.EntityData) (entry : EntitySchemaEntry) : Bool

Equations

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

def Cedar.Validation.instanceOfSchema.instanceOfEntitySchemaEntry (env : TypeEnv) (uid : Spec.EntityUID) (data : Spec.EntityData) (entry : EntitySchemaEntry) : Except EntityValidationError PUnit

Equations

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

def Cedar.Validation.instanceOfSchema.instanceOfActionSchemaEntry (env : TypeEnv) (uid : Spec.EntityUID) (data : Spec.EntityData) : Except EntityValidationError PUnit

Equations

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

def Cedar.Validation.instanceOfSchema.instanceOfSchemaEntry (env : TypeEnv) (uid : Spec.EntityUID) (data : Spec.EntityData) : Except EntityValidationError PUnit

Equations

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

def Cedar.Validation.instanceOfSchema.actionExists (entities : Spec.Entities) (uid : Spec.EntityUID) : Except EntityValidationError PUnit

Equations

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

def Cedar.Validation.requestMatchesEnvironment (env : TypeEnv) (request : Spec.Request) : Bool

Equations

• Cedar.Validation.requestMatchesEnvironment env request = Cedar.Validation.instanceOfRequestType request env

def Cedar.Validation.validateRequest (schema : Schema) (request : Spec.Request) : RequestValidationResult

Equations

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

def Cedar.Validation.entitiesMatchEnvironment (env : TypeEnv) (entities : Spec.Entities) : EntityValidationResult

Equations

• Cedar.Validation.entitiesMatchEnvironment env entities = Cedar.Validation.instanceOfSchema entities env

def Cedar.Validation.actionSchemaEntryToEntityData (ase : ActionSchemaEntry) : Spec.EntityData

Equations

• Cedar.Validation.actionSchemaEntryToEntityData ase = { attrs := Cedar.Data.Map.empty, ancestors := ase.ancestors, tags := Cedar.Data.Map.empty }

def Cedar.Validation.validateEntities (schema : Schema) (entities : Spec.Entities) : EntityValidationResult

Equations

• Cedar.Validation.validateEntities schema entities = schema.environments.forM fun (x : Cedar.Validation.TypeEnv) => Cedar.Validation.entitiesMatchEnvironment x entities

def Cedar.Validation.entityValidationErrorToJson : EntityValidationError → Lean.Json

Equations

• Cedar.Validation.entityValidationErrorToJson (Cedar.Validation.EntityValidationError.typeError x_1) = Lean.Json.str x_1

instance Cedar.Validation.instToJsonEntityValidationError : Lean.ToJson EntityValidationError

Equations

• Cedar.Validation.instToJsonEntityValidationError = { toJson := Cedar.Validation.entityValidationErrorToJson }

def Cedar.Validation.requestValidationErrorToJson : RequestValidationError → Lean.Json

Equations

• Cedar.Validation.requestValidationErrorToJson (Cedar.Validation.RequestValidationError.typeError x_1) = Lean.Json.str x_1

instance Cedar.Validation.instToJsonRequestValidationError : Lean.ToJson RequestValidationError

Equations

• Cedar.Validation.instToJsonRequestValidationError = { toJson := Cedar.Validation.requestValidationErrorToJson }