This file defines the ADTs that represent the symbolic environment. The environment consists of a symbolic request, entity store, and action store. A symbolic environment is literal when it consists of literal terms and interpreted functions (UDFs).

structure Cedar.SymCC.SymRequest : Type

• principal : Term
• action : Term
• resource : Term
• context : Term

def Cedar.SymCC.SymRequest.isLiteral (req : SymRequest) : Bool

Equations

• req.isLiteral = (req.principal.isLiteral && req.action.isLiteral && req.resource.isLiteral && req.context.isLiteral)

instance Cedar.SymCC.instReprSymRequest : Repr SymRequest

Equations

• Cedar.SymCC.instReprSymRequest = { reprPrec := Cedar.SymCC.instReprSymRequest.repr }

def Cedar.SymCC.instReprSymRequest.repr : SymRequest → Nat → Std.Format

Equations

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

def Cedar.SymCC.instInhabitedSymRequest.default : SymRequest

Equations

• Cedar.SymCC.instInhabitedSymRequest.default = { principal := default, action := default, resource := default, context := default }

instance Cedar.SymCC.instInhabitedSymRequest : Inhabited SymRequest

Equations

• Cedar.SymCC.instInhabitedSymRequest = { default := Cedar.SymCC.instInhabitedSymRequest.default }

def Cedar.SymCC.instDecidableEqSymRequest.decEq (x✝ x✝¹ : SymRequest) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.SymCC.instDecidableEqSymRequest : DecidableEq SymRequest

Equations

• Cedar.SymCC.instDecidableEqSymRequest = Cedar.SymCC.instDecidableEqSymRequest.decEq

structure Cedar.SymCC.SymEntityData : Type

Represents the entity data for all entities of a single type

• attrs : UnaryFunction
• ancestors : Data.Map Spec.EntityType UnaryFunction

  Let t₁ be the entity type which this SymEntityData represents the data for. Let t₂ be an entity type in this map's keys. The UnaryFunction here maps entities of type t₁ to the set of entities of type t₂ which are ancestors of that entity. (Of course, the UnaryFunction is on SMT-level values, so the domain is essentially t₁-typed Terms, and the output is essentially a Set<t₂>-typed Term.)

• members : Option (Data.Set String)

  Specifies the EIDs of enum members for this entity type, if applicable

• tags : Option SymTags

  none means this entity type has no tags

def Cedar.SymCC.SymTags.isLiteral (τs : SymTags) : Bool

Equations

• τs.isLiteral = (τs.keys.isLiteral && τs.vals.isLiteral)

def Cedar.SymCC.SymEntityData.isLiteral (δ : SymEntityData) : Bool

Equations

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

def Cedar.SymCC.instReprSymEntityData.repr : SymEntityData → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprSymEntityData : Repr SymEntityData

Equations

• Cedar.SymCC.instReprSymEntityData = { reprPrec := Cedar.SymCC.instReprSymEntityData.repr }

def Cedar.SymCC.instInhabitedSymEntityData.default : SymEntityData

Equations

• Cedar.SymCC.instInhabitedSymEntityData.default = { attrs := default, ancestors := default, members := default, tags := default }

instance Cedar.SymCC.instInhabitedSymEntityData : Inhabited SymEntityData

Equations

• Cedar.SymCC.instInhabitedSymEntityData = { default := Cedar.SymCC.instInhabitedSymEntityData.default }

def Cedar.SymCC.instDecidableEqSymEntityData.decEq (x✝ x✝¹ : SymEntityData) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.SymCC.instDecidableEqSymEntityData : DecidableEq SymEntityData

Equations

• Cedar.SymCC.instDecidableEqSymEntityData = Cedar.SymCC.instDecidableEqSymEntityData.decEq

@[reducible, inline]

abbrev Cedar.SymCC.SymEntities : Type

Equations

• Cedar.SymCC.SymEntities = Cedar.Data.Map Cedar.Spec.EntityType Cedar.SymCC.SymEntityData

instance Cedar.SymCC.instInhabitedSymEntities : Inhabited SymEntities

Equations

• Cedar.SymCC.instInhabitedSymEntities = Cedar.Data.instInhabitedMap

instance Cedar.SymCC.instDecidableEqSymEntities : DecidableEq SymEntities

Equations

• Cedar.SymCC.instDecidableEqSymEntities a b = Cedar.Data.instDecidableEqMap a b

instance Cedar.SymCC.instReprSymEntities : Repr SymEntities

Equations

• Cedar.SymCC.instReprSymEntities = Cedar.Data.instReprMap

def Cedar.SymCC.SymEntities.attrs (εs : SymEntities) (ety : Spec.EntityType) : Option UnaryFunction

Equations

• εs.attrs ety = do let __do_lift ← Cedar.Data.Map.find? εs ety some __do_lift.attrs

def Cedar.SymCC.SymEntities.ancestors (εs : SymEntities) (ety : Spec.EntityType) : Option (Data.Map Spec.EntityType UnaryFunction)

Equations

• εs.ancestors ety = do let __do_lift ← Cedar.Data.Map.find? εs ety some __do_lift.ancestors

def Cedar.SymCC.SymEntities.ancestorsOfType (εs : SymEntities) (ety ancTy : Spec.EntityType) : Option UnaryFunction

Equations

• εs.ancestorsOfType ety ancTy = do let __do_lift ← εs.ancestors ety __do_lift.find? ancTy

def Cedar.SymCC.SymEntities.isValidEntityType (εs : SymEntities) (ety : Spec.EntityType) : Bool

Equations

• εs.isValidEntityType ety = Cedar.Data.Map.contains εs ety

def Cedar.SymCC.SymEntities.isValidEntityUID (εs : SymEntities) (uid : Spec.EntityUID) : Bool

Equations

• εs.isValidEntityUID uid = match Cedar.Data.Map.find? εs uid.ty with | some d => match d.members with | some eids => eids.contains uid.eid | x => true | none => false

def Cedar.SymCC.SymEntities.tags (εs : SymEntities) (ety : Spec.EntityType) : Option (Option SymTags)

Equations

• εs.tags ety = Option.map Cedar.SymCC.SymEntityData.tags (Cedar.Data.Map.find? εs ety)

def Cedar.SymCC.SymEntities.isLiteral (es : SymEntities) : Bool

Equations

• es.isLiteral = (Cedar.Data.Map.toList es).all fun (x : Cedar.Spec.EntityType × Cedar.SymCC.SymEntityData) => match x with | (fst, d) => d.isLiteral

structure Cedar.SymCC.SymEnv : Type

• request : SymRequest
• entities : SymEntities

def Cedar.SymCC.SymEnv.isLiteral (env : SymEnv) : Bool

Equations

• env.isLiteral = (env.request.isLiteral && env.entities.isLiteral)

def Cedar.SymCC.instReprSymEnv.repr : SymEnv → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprSymEnv : Repr SymEnv

Equations

• Cedar.SymCC.instReprSymEnv = { reprPrec := Cedar.SymCC.instReprSymEnv.repr }

def Cedar.SymCC.instInhabitedSymEnv.default : SymEnv

Equations

• Cedar.SymCC.instInhabitedSymEnv.default = { request := default, entities := default }

instance Cedar.SymCC.instInhabitedSymEnv : Inhabited SymEnv

Equations

• Cedar.SymCC.instInhabitedSymEnv = { default := Cedar.SymCC.instInhabitedSymEnv.default }

instance Cedar.SymCC.instDecidableEqSymEnv : DecidableEq SymEnv

Equations

• Cedar.SymCC.instDecidableEqSymEnv = Cedar.SymCC.instDecidableEqSymEnv.decEq

def Cedar.SymCC.instDecidableEqSymEnv.decEq (x✝ x✝¹ : SymEnv) : Decidable (x✝ = x✝¹)

Equations

• Cedar.SymCC.instDecidableEqSymEnv.decEq { request := a, entities := a_1 } { request := b, entities := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Cedar.SymCC.UUF.attrsId (ety : Spec.EntityType) : String

Equations

• Cedar.SymCC.UUF.attrsId ety = toString "attrs[" ++ toString (toString ety) ++ toString "]"

def Cedar.SymCC.UUF.ancsId (ety ancTy : Spec.EntityType) : String

Equations

• Cedar.SymCC.UUF.ancsId ety ancTy = toString "ancs[" ++ toString (toString ety) ++ toString ", " ++ toString (toString ancTy) ++ toString "]"

def Cedar.SymCC.UUF.tagKeysId (ety : Spec.EntityType) : String

Equations

• Cedar.SymCC.UUF.tagKeysId ety = toString "tagKeys[" ++ toString (toString ety) ++ toString "]"

def Cedar.SymCC.UUF.tagValsId (ety : Spec.EntityType) : String

Equations

• Cedar.SymCC.UUF.tagValsId ety = toString "tagVals[" ++ toString (toString ety) ++ toString "]"

def Cedar.SymCC.SymEntityData.ofStandardEntityType (ety : Spec.EntityType) (sch : Validation.StandardSchemaEntry) : SymEntityData

Equations

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

def Cedar.SymCC.SymEntityData.ofStandardEntityType.attrsUUF (ety : Spec.EntityType) (sch : Validation.StandardSchemaEntry) : UnaryFunction

Equations

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

def Cedar.SymCC.SymEntityData.ofStandardEntityType.ancsUUF (ety ancTy : Spec.EntityType) : UnaryFunction

Equations

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

def Cedar.SymCC.SymEntityData.ofStandardEntityType.symTags (ety : Spec.EntityType) (tagTy : Validation.CedarType) : SymTags

Equations

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

def Cedar.SymCC.SymEntityData.emptyAttrs (ety : Spec.EntityType) : UnaryFunction

Equations

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

def Cedar.SymCC.SymEntityData.ofEnumEntityType (ety : Spec.EntityType) (eids : Data.Set String) : SymEntityData

Equations

• Cedar.SymCC.SymEntityData.ofEnumEntityType ety eids = { attrs := Cedar.SymCC.SymEntityData.emptyAttrs ety, ancestors := Cedar.Data.Map.empty, members := some eids, tags := none }

def Cedar.SymCC.SymEntityData.ofEntityType (ety : Spec.EntityType) : Validation.EntitySchemaEntry → SymEntityData

Equations

• Cedar.SymCC.SymEntityData.ofEntityType ety (Cedar.Validation.EntitySchemaEntry.standard sch) = Cedar.SymCC.SymEntityData.ofStandardEntityType ety sch
• Cedar.SymCC.SymEntityData.ofEntityType ety (Cedar.Validation.EntitySchemaEntry.enum eids) = Cedar.SymCC.SymEntityData.ofEnumEntityType ety eids

def Cedar.SymCC.SymEntityData.ofActionType (actTy : Spec.EntityType) (actTys : List Spec.EntityType) (sch : Validation.ActionSchema) : SymEntityData

Equations

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

def Cedar.SymCC.SymEntityData.ofActionType.termOfType? (ety : Spec.EntityType) (uid : Spec.EntityUID) : Option Term

Equations

• Cedar.SymCC.SymEntityData.ofActionType.termOfType? ety uid = if uid.ty = ety then some (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.entity uid)) else none

def Cedar.SymCC.SymEntityData.ofActionType.ancsTerm (ancTy : Spec.EntityType) (ancs : List Spec.EntityUID) : Term

Equations

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

def Cedar.SymCC.SymEntityData.ofActionType.ancsUDF (actTy : Spec.EntityType) (sch : Validation.ActionSchema) (ancTy : Spec.EntityType) : UnaryFunction

Equations

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

def Cedar.SymCC.SymEntityData.ofActionType.acts (actTy : Spec.EntityType) (sch : Validation.ActionSchema) : List String

Equations

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

def Cedar.SymCC.SymEntities.ofSchema (ets : Validation.EntitySchema) (acts : Validation.ActionSchema) : SymEntities

Creates symbolic entities for the given schema. This function assumes that the schemas are well-formed in the following sense:

• All entity types that appear in the attributes or ancestors fields of ets are declared either in ets or acts.
• All entity types that appear in the ancestors fields of acts are declared in acts. An entity type is declared in ets if it's a key in the underlying map; it's declared in acts if it's the type of a key in the underlying map. This function also assumes ets and ats declare disjoint sets of types. This function assumes that no entity types have tags, and that action types have no attributes.

Equations

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

def Cedar.SymCC.SymRequest.ofRequestType (reqTy : Validation.RequestType) : SymRequest

Creates a symbolic request for the given request type.

Equations

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

def Cedar.SymCC.SymEnv.ofEnv (tyEnv : Validation.TypeEnv) : SymEnv

Returns a symbolic environment that conforms to the given type environment.

Equations

• Cedar.SymCC.SymEnv.ofEnv tyEnv = { request := Cedar.SymCC.SymRequest.ofRequestType tyEnv.reqty, entities := Cedar.SymCC.SymEntities.ofSchema tyEnv.ets tyEnv.acts }