inductive Cedar.Validation.BoolType : Type

• anyBool : BoolType
• tt : BoolType
• ff : BoolType

def Cedar.Validation.instReprBoolType.repr : BoolType → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprBoolType : Repr BoolType

Equations

• Cedar.Validation.instReprBoolType = { reprPrec := Cedar.Validation.instReprBoolType.repr }

def Cedar.Validation.BoolType.not : BoolType → BoolType

Equations

• Cedar.Validation.BoolType.anyBool.not = Cedar.Validation.BoolType.anyBool
• Cedar.Validation.BoolType.tt.not = Cedar.Validation.BoolType.ff
• Cedar.Validation.BoolType.ff.not = Cedar.Validation.BoolType.tt

def Cedar.Validation.BoolType.lift : BoolType → BoolType

Equations

• x✝.lift = Cedar.Validation.BoolType.anyBool

inductive Cedar.Validation.ExtType : Type

• ipAddr : ExtType
• decimal : ExtType
• datetime : ExtType
• duration : ExtType

instance Cedar.Validation.instReprExtType : Repr ExtType

Equations

• Cedar.Validation.instReprExtType = { reprPrec := Cedar.Validation.instReprExtType.repr }

def Cedar.Validation.instReprExtType.repr : ExtType → Nat → Std.Format

Equations

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

inductive Cedar.Validation.Qualified (α : Type u) : Type u

• optional {α : Type u} (a : α) : Qualified α
• required {α : Type u} (a : α) : Qualified α

instance Cedar.Validation.instReprQualified {α✝ : Type u_1} [Repr α✝] : Repr (Qualified α✝)

Equations

• Cedar.Validation.instReprQualified = { reprPrec := Cedar.Validation.instReprQualified.repr }

def Cedar.Validation.instReprQualified.repr {α✝ : Type u_1} [Repr α✝] : Qualified α✝ → Nat → Std.Format

Equations

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

instance Cedar.Validation.Qualified.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Qualified α)

Equations

• Cedar.Validation.Qualified.instInhabited = { default := Cedar.Validation.Qualified.required default }

def Cedar.Validation.Qualified.getType {α : Type u_1} : Qualified α → α

Equations

• (Cedar.Validation.Qualified.optional a).getType = a
• (Cedar.Validation.Qualified.required a).getType = a

def Cedar.Validation.Qualified.isRequired {α : Type u_1} : Qualified α → Bool

Equations

• (Cedar.Validation.Qualified.optional a).isRequired = false
• (Cedar.Validation.Qualified.required a).isRequired = true

def Cedar.Validation.Qualified.map {α : Type u_1} {β : Type u_2} (f : α → β) : Qualified α → Qualified β

Equations

• Cedar.Validation.Qualified.map f (Cedar.Validation.Qualified.optional a) = Cedar.Validation.Qualified.optional (f a)
• Cedar.Validation.Qualified.map f (Cedar.Validation.Qualified.required a) = Cedar.Validation.Qualified.required (f a)

def Cedar.Validation.Qualified.transpose {α : Type u_1} {ε : Type u_2} : Qualified (Except ε α) → Except ε (Qualified α)

Equations

• (Cedar.Validation.Qualified.optional (Except.ok a)).transpose = Except.ok (Cedar.Validation.Qualified.optional a)
• (Cedar.Validation.Qualified.required (Except.ok a)).transpose = Except.ok (Cedar.Validation.Qualified.required a)
• (Cedar.Validation.Qualified.optional (Except.error e)).transpose = Except.error e
• (Cedar.Validation.Qualified.required (Except.error e)).transpose = Except.error e

inductive Cedar.Validation.CedarType : Type

• bool (bty : BoolType) : CedarType
• int : CedarType
• string : CedarType
• entity (ety : Spec.EntityType) : CedarType
• set (ty : CedarType) : CedarType
• record (rty : Data.Map Spec.Attr (Qualified CedarType)) : CedarType
• ext (xty : ExtType) : CedarType

partial def Cedar.Validation.instReprCedarType.repr : CedarType → Nat → Std.Format

instance Cedar.Validation.instReprCedarType : Repr CedarType

Equations

• Cedar.Validation.instReprCedarType = { reprPrec := Cedar.Validation.instReprCedarType.repr }

instance Cedar.Validation.instInhabitedCedarType : Inhabited CedarType

Equations

• Cedar.Validation.instInhabitedCedarType = { default := Cedar.Validation.CedarType.int }

@[reducible, inline]

abbrev Cedar.Validation.QualifiedType : Type

Equations

• Cedar.Validation.QualifiedType = Cedar.Validation.Qualified Cedar.Validation.CedarType

@[reducible, inline]

abbrev Cedar.Validation.RecordType : Type

Equations

• Cedar.Validation.RecordType = Cedar.Data.Map Cedar.Spec.Attr Cedar.Validation.QualifiedType

@[irreducible]

def Cedar.Validation.QualifiedType.liftBoolTypes : QualifiedType → QualifiedType

Equations

• Cedar.Validation.QualifiedType.liftBoolTypes (Cedar.Validation.Qualified.optional ty) = Cedar.Validation.Qualified.optional ty.liftBoolTypes
• Cedar.Validation.QualifiedType.liftBoolTypes (Cedar.Validation.Qualified.required ty) = Cedar.Validation.Qualified.required ty.liftBoolTypes

@[irreducible]

def Cedar.Validation.RecordType.liftBoolTypes : RecordType → RecordType

Equations

• x✝.liftBoolTypes = Cedar.Data.Map.mapOnValues₂ x✝ fun (x : { x : Cedar.Validation.QualifiedType // sizeOf x < sizeOf x✝ }) => match x with | ⟨v, property⟩ => v.liftBoolTypes

@[irreducible]

def Cedar.Validation.CedarType.liftBoolTypes : CedarType → CedarType

Equations

• (Cedar.Validation.CedarType.bool bty).liftBoolTypes = Cedar.Validation.CedarType.bool bty.lift
• s.set.liftBoolTypes = s.liftBoolTypes.set
• (Cedar.Validation.CedarType.record rty).liftBoolTypes = Cedar.Validation.CedarType.record (Cedar.Validation.RecordType.liftBoolTypes rty)
• x✝.liftBoolTypes = x✝

structure Cedar.Validation.StandardSchemaEntry : Type

• ancestors : Data.Set Spec.EntityType
• attrs : RecordType
• tags : Option CedarType

inductive Cedar.Validation.EntitySchemaEntry : Type

• standard (ty : StandardSchemaEntry) : EntitySchemaEntry
• enum (eids : Data.Set String) : EntitySchemaEntry

def Cedar.Validation.EntitySchemaEntry.isValidEntityEID (entry : EntitySchemaEntry) (eid : String) : Bool

Equations

• (Cedar.Validation.EntitySchemaEntry.standard ty).isValidEntityEID eid = true
• (Cedar.Validation.EntitySchemaEntry.enum eids).isValidEntityEID eid = eids.contains eid

def Cedar.Validation.EntitySchemaEntry.tags? : EntitySchemaEntry → Option CedarType

Equations

• (Cedar.Validation.EntitySchemaEntry.standard ty).tags? = ty.tags
• (Cedar.Validation.EntitySchemaEntry.enum eids).tags? = none

def Cedar.Validation.EntitySchemaEntry.attrs : EntitySchemaEntry → RecordType

Equations

• (Cedar.Validation.EntitySchemaEntry.standard ty).attrs = ty.attrs
• (Cedar.Validation.EntitySchemaEntry.enum eids).attrs = Cedar.Data.Map.empty

def Cedar.Validation.EntitySchemaEntry.ancestors : EntitySchemaEntry → Data.Set Spec.EntityType

Equations

• (Cedar.Validation.EntitySchemaEntry.standard ty).ancestors = ty.ancestors
• (Cedar.Validation.EntitySchemaEntry.enum eids).ancestors = Cedar.Data.Set.empty

def Cedar.Validation.EntitySchemaEntry.isStandard : EntitySchemaEntry → Bool

Equations

• (Cedar.Validation.EntitySchemaEntry.standard ty).isStandard = true
• (Cedar.Validation.EntitySchemaEntry.enum eids).isStandard = false

@[reducible, inline]

abbrev Cedar.Validation.EntitySchema : Type

Equations

• Cedar.Validation.EntitySchema = Cedar.Data.Map Cedar.Spec.EntityType Cedar.Validation.EntitySchemaEntry

def Cedar.Validation.EntitySchema.entityTypeMembers? (ets : EntitySchema) (et : Spec.EntityType) : Option (Data.Set String)

Equations

• ets.entityTypeMembers? et = match Cedar.Data.Map.find? ets et with | some (Cedar.Validation.EntitySchemaEntry.enum eids) => some eids | x => none

def Cedar.Validation.EntitySchema.isValidEntityUID (ets : EntitySchema) (uid : Spec.EntityUID) : Bool

Equations

• ets.isValidEntityUID uid = match Cedar.Data.Map.find? ets uid.ty with | some entry => entry.isValidEntityEID uid.eid | none => false

def Cedar.Validation.EntitySchema.contains (ets : EntitySchema) (ety : Spec.EntityType) : Bool

Equations

• ets.contains ety = (Cedar.Data.Map.find? ets ety).isSome

def Cedar.Validation.EntitySchema.attrs? (ets : EntitySchema) (ety : Spec.EntityType) : Option RecordType

Equations

• ets.attrs? ety = Option.map Cedar.Validation.EntitySchemaEntry.attrs (Cedar.Data.Map.find? ets ety)

def Cedar.Validation.EntitySchema.tags? (ets : EntitySchema) (ety : Spec.EntityType) : Option (Option CedarType)

Equations

• ets.tags? ety = Option.map Cedar.Validation.EntitySchemaEntry.tags? (Cedar.Data.Map.find? ets ety)

structure Cedar.Validation.ActionSchemaEntry : Type

• appliesToPrincipal : Data.Set Spec.EntityType
• appliesToResource : Data.Set Spec.EntityType
• ancestors : Data.Set Spec.EntityUID
• context : RecordType

instance Cedar.Validation.instReprActionSchemaEntry : Repr ActionSchemaEntry

Equations

• Cedar.Validation.instReprActionSchemaEntry = { reprPrec := Cedar.Validation.instReprActionSchemaEntry.repr }

def Cedar.Validation.instReprActionSchemaEntry.repr : ActionSchemaEntry → Nat → Std.Format

Equations

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

def Cedar.Validation.instInhabitedActionSchemaEntry.default : ActionSchemaEntry

Equations

• Cedar.Validation.instInhabitedActionSchemaEntry.default = { appliesToPrincipal := default, appliesToResource := default, ancestors := default, context := default }

instance Cedar.Validation.instInhabitedActionSchemaEntry : Inhabited ActionSchemaEntry

Equations

• Cedar.Validation.instInhabitedActionSchemaEntry = { default := Cedar.Validation.instInhabitedActionSchemaEntry.default }

@[reducible, inline]

abbrev Cedar.Validation.ActionSchema : Type

Equations

• Cedar.Validation.ActionSchema = Cedar.Data.Map Cedar.Spec.EntityUID Cedar.Validation.ActionSchemaEntry

def Cedar.Validation.ActionSchema.actionType? (acts : ActionSchema) (ety : Spec.EntityType) : Bool

Equations

• acts.actionType? ety = Cedar.Data.Set.any (fun (x : Cedar.Spec.EntityUID) => x.ty == ety) (Cedar.Data.Map.keys acts)

def Cedar.Validation.ActionSchema.contains (as : ActionSchema) (uid : Spec.EntityUID) : Bool

Equations

• as.contains uid = (Cedar.Data.Map.find? as uid).isSome

def Cedar.Validation.ActionSchema.descendentOf (as : ActionSchema) (uid₁ uid₂ : Spec.EntityUID) : Bool

Equations

• as.descendentOf uid₁ uid₂ = if (uid₁ == uid₂) = true then true else match Cedar.Data.Map.find? as uid₁ with | some entry => entry.ancestors.contains uid₂ | none => false

structure Cedar.Validation.Schema : Type

• ets : EntitySchema
• acts : ActionSchema

structure Cedar.Validation.RequestType : Type

• principal : Spec.EntityType
• action : Spec.EntityUID
• resource : Spec.EntityType
• context : RecordType

instance Cedar.Validation.instInhabitedRequestType : Inhabited RequestType

Equations

• Cedar.Validation.instInhabitedRequestType = { default := Cedar.Validation.instInhabitedRequestType.default }

def Cedar.Validation.instInhabitedRequestType.default : RequestType

Equations

• Cedar.Validation.instInhabitedRequestType.default = { principal := default, action := default, resource := default, context := default }

structure Cedar.Validation.TypeEnv : Type

• ets : EntitySchema
• acts : ActionSchema
• reqty : RequestType

def Cedar.Validation.instInhabitedTypeEnv.default : TypeEnv

Equations

• Cedar.Validation.instInhabitedTypeEnv.default = { ets := default, acts := default, reqty := default }

instance Cedar.Validation.instInhabitedTypeEnv : Inhabited TypeEnv

Equations

• Cedar.Validation.instInhabitedTypeEnv = { default := Cedar.Validation.instInhabitedTypeEnv.default }

def Cedar.Validation.ActionSchema.maybeDescendentOf (as : ActionSchema) (ety₁ ety₂ : Spec.EntityType) : Bool

Equations

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

def Cedar.Validation.TypeEnv.descendentOf (env : TypeEnv) (ety₁ ety₂ : Spec.EntityType) : Bool

Equations

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

def Cedar.Validation.instReprBoolType_1.repr : BoolType → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprBoolType_1 : Repr BoolType

Equations

• Cedar.Validation.instReprBoolType_1 = { reprPrec := Cedar.Validation.instReprBoolType_1.repr }

instance Cedar.Validation.instDecidableEqBoolType : DecidableEq BoolType

Equations

• Cedar.Validation.instDecidableEqBoolType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cedar.Validation.instReprExtType_1.repr : ExtType → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprExtType_1 : Repr ExtType

Equations

• Cedar.Validation.instReprExtType_1 = { reprPrec := Cedar.Validation.instReprExtType_1.repr }

instance Cedar.Validation.instDecidableEqExtType : DecidableEq ExtType

Equations

• Cedar.Validation.instDecidableEqExtType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Cedar.Validation.instInhabitedExtType : Inhabited ExtType

Equations

• Cedar.Validation.instInhabitedExtType = { default := Cedar.Validation.instInhabitedExtType.default }

def Cedar.Validation.instInhabitedExtType.default : ExtType

Equations

• Cedar.Validation.instInhabitedExtType.default = Cedar.Validation.ExtType.ipAddr

instance Cedar.Validation.instReprQualified_1 {α✝ : Type u_1} [Repr α✝] : Repr (Qualified α✝)

Equations

• Cedar.Validation.instReprQualified_1 = { reprPrec := Cedar.Validation.instReprQualified_1.repr }

def Cedar.Validation.instReprQualified_1.repr {α✝ : Type u_1} [Repr α✝] : Qualified α✝ → Nat → Std.Format

Equations

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

instance Cedar.Validation.instDecidableEqQualified {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Qualified α✝)

Equations

• Cedar.Validation.instDecidableEqQualified = Cedar.Validation.instDecidableEqQualified.decEq

def Cedar.Validation.instDecidableEqQualified.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Qualified α✝) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Validation.instDecidableEqQualified.decEq (Cedar.Validation.Qualified.optional a) (Cedar.Validation.Qualified.optional b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Validation.instDecidableEqQualified.decEq (Cedar.Validation.Qualified.optional a) (Cedar.Validation.Qualified.required a_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqQualified.decEq (Cedar.Validation.Qualified.required a) (Cedar.Validation.Qualified.optional a_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqQualified.decEq (Cedar.Validation.Qualified.required a) (Cedar.Validation.Qualified.required b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Validation.instInhabitedQualified {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Qualified a✝)

Equations

• Cedar.Validation.instInhabitedQualified = { default := Cedar.Validation.instInhabitedQualified.default }

def Cedar.Validation.instInhabitedQualified.default {a✝ : Type u_1} [Inhabited a✝] : Qualified a✝

Equations

• Cedar.Validation.instInhabitedQualified.default = Cedar.Validation.Qualified.optional default

partial def Cedar.Validation.instReprCedarType_1.repr : CedarType → Nat → Std.Format

instance Cedar.Validation.instReprCedarType_1 : Repr CedarType

Equations

• Cedar.Validation.instReprCedarType_1 = { reprPrec := Cedar.Validation.instReprCedarType_1.repr }

instance Cedar.Validation.instInhabitedCedarType_1 : Inhabited CedarType

Equations

• Cedar.Validation.instInhabitedCedarType_1 = { default := Cedar.Validation.instInhabitedCedarType_1.default }

def Cedar.Validation.instInhabitedCedarType_1.default : CedarType

Equations

• Cedar.Validation.instInhabitedCedarType_1.default = Cedar.Validation.CedarType.int

instance Cedar.Validation.instReprActionSchemaEntry_1 : Repr ActionSchemaEntry

Equations

• Cedar.Validation.instReprActionSchemaEntry_1 = { reprPrec := Cedar.Validation.instReprActionSchemaEntry_1.repr }

def Cedar.Validation.instReprActionSchemaEntry_1.repr : ActionSchemaEntry → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprStandardSchemaEntry : Repr StandardSchemaEntry

Equations

• Cedar.Validation.instReprStandardSchemaEntry = { reprPrec := Cedar.Validation.instReprStandardSchemaEntry.repr }

def Cedar.Validation.instReprStandardSchemaEntry.repr : StandardSchemaEntry → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprEntitySchemaEntry : Repr EntitySchemaEntry

Equations

• Cedar.Validation.instReprEntitySchemaEntry = { reprPrec := Cedar.Validation.instReprEntitySchemaEntry.repr }

def Cedar.Validation.instReprEntitySchemaEntry.repr : EntitySchemaEntry → Nat → Std.Format

Equations

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

def Cedar.Validation.instReprSchema.repr : Schema → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprSchema : Repr Schema

Equations

• Cedar.Validation.instReprSchema = { reprPrec := Cedar.Validation.instReprSchema.repr }

@[irreducible]

def Cedar.Validation.decCedarType (a b : CedarType) : Decidable (a = b)

Equations

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

instance Cedar.Validation.instDecidableEqCedarType : DecidableEq CedarType

Equations

• Cedar.Validation.instDecidableEqCedarType = Cedar.Validation.decCedarType

def Cedar.Validation.instDecidableEqStandardSchemaEntry.decEq (x✝ x✝¹ : StandardSchemaEntry) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.Validation.instDecidableEqStandardSchemaEntry : DecidableEq StandardSchemaEntry

Equations

• Cedar.Validation.instDecidableEqStandardSchemaEntry = Cedar.Validation.instDecidableEqStandardSchemaEntry.decEq

def Cedar.Validation.decEntitySchemaEntry (e₁ e₂ : EntitySchemaEntry) : Decidable (e₁ = e₂)

Equations

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

instance Cedar.Validation.instDecidableEqEntitySchemaEntry : DecidableEq EntitySchemaEntry

Equations

• Cedar.Validation.instDecidableEqEntitySchemaEntry = Cedar.Validation.decEntitySchemaEntry