This file contains the definition of well-formedness of TypeEnv and related definitions.

def Cedar.Validation.ActionSchema.IsActionEntityType (acts : ActionSchema) (ety : Spec.EntityType) : Prop

Equations

• acts.IsActionEntityType ety = ∃ (uid : Cedar.Spec.EntityUID), acts.contains uid = true ∧ uid.ty = ety

def Cedar.Validation.EntityType.WellFormed (env : TypeEnv) (ety : Spec.EntityType) : Prop

Either a non-action entity type in env.ets, or an action entity type in env.acts.

Equations

• Cedar.Validation.EntityType.WellFormed env ety = (env.ets.contains ety = true ∨ env.acts.IsActionEntityType ety)

inductive Cedar.Validation.QualifiedType.WellFormed (env : TypeEnv) : Qualified CedarType → Prop

• optional_wf {env : TypeEnv} {ty : CedarType} (h : CedarType.WellFormed env ty) : WellFormed env (Qualified.optional ty)
• required_wf {env : TypeEnv} {ty : CedarType} (h : CedarType.WellFormed env ty) : WellFormed env (Qualified.required ty)

inductive Cedar.Validation.CedarType.WellFormed (env : TypeEnv) : CedarType → Prop

Defines when a CedarType is well-formed in an TypeEnv.

• bool_wf {env : TypeEnv} {bty : BoolType} : WellFormed env (bool bty)
• int_wf {env : TypeEnv} : WellFormed env int
• string_wf {env : TypeEnv} : WellFormed env string
• entity_wf {env : TypeEnv} {ety : Spec.EntityType} (h : EntityType.WellFormed env ety) : WellFormed env (entity ety)
• set_wf {env : TypeEnv} {ty : CedarType} (h : WellFormed env ty) : WellFormed env ty.set
• record_wf {env : TypeEnv} {rty : RecordType} (h₁ : Data.Map.WellFormed rty) (h₂ : ∀ (attr : Spec.Attr) (qty : QualifiedType), Data.Map.find? rty attr = some qty → QualifiedType.WellFormed env qty) : WellFormed env (record rty)
• ext_wf {env : TypeEnv} {xty : ExtType} : WellFormed env (ext xty)

inductive Cedar.Validation.QualifiedType.IsLifted : Qualified CedarType → Prop

• optional_lifted {ty : CedarType} (h : ty.IsLifted) : IsLifted (Qualified.optional ty)
• required_lifted {ty : CedarType} (h : ty.IsLifted) : IsLifted (Qualified.required ty)

inductive Cedar.Validation.CedarType.IsLifted : CedarType → Prop

Defines when a CedarType does not have any singleton Bool types.

• bool_lifted : (bool BoolType.anyBool).IsLifted
• int_lifted : int.IsLifted
• string_lifted : string.IsLifted
• entity_lifted {ety : Spec.EntityType} : (entity ety).IsLifted
• set_lifted {ty : CedarType} (h : ty.IsLifted) : ty.set.IsLifted
• record_lifted {rty : RecordType} (h₂ : ∀ (attr : Spec.Attr) (qty : QualifiedType), (attr, qty) ∈ Data.Map.toList rty → QualifiedType.IsLifted qty) : (record rty).IsLifted
• ext_lifted {xty : ExtType} : (ext xty).IsLifted

def Cedar.Validation.StandardSchemaEntry.WellFormed (env : TypeEnv) (entry : StandardSchemaEntry) : Prop

Equations

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

def Cedar.Validation.EntitySchemaEntry.WellFormed (env : TypeEnv) (entry : EntitySchemaEntry) : Prop

Equations

• Cedar.Validation.EntitySchemaEntry.WellFormed env (Cedar.Validation.EntitySchemaEntry.standard entry_2) = Cedar.Validation.StandardSchemaEntry.WellFormed env entry_2
• Cedar.Validation.EntitySchemaEntry.WellFormed env (Cedar.Validation.EntitySchemaEntry.enum es) = (es.WellFormed ∧ ¬es.isEmpty = true)

def Cedar.Validation.EntitySchema.WellFormed (env : TypeEnv) (ets : EntitySchema) : Prop

Equations

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

def Cedar.Validation.EntityUID.WellFormed (env : TypeEnv) (uid : Spec.EntityUID) : Prop

Equations

• Cedar.Validation.EntityUID.WellFormed env uid = (env.ets.isValidEntityUID uid = true ∨ env.acts.contains uid = true)

theorem Cedar.Validation.EntitySchema.attrs?_eq_map_find? {ets : EntitySchema} {ety : Spec.EntityType} : ets.attrs? ety = Option.map EntitySchemaEntry.attrs (Data.Map.find? ets ety)

theorem Cedar.Validation.EntitySchemaEntry.tags?_eq {entry : EntitySchemaEntry} : entry.tags? = match entry with | standard ty => ty.tags | enum eids => none

theorem Cedar.Validation.EntitySchema.tags?_eq_map_find? {ets : EntitySchema} {ety : Spec.EntityType} : ets.tags? ety = Option.map EntitySchemaEntry.tags? (Data.Map.find? ets ety)

theorem Cedar.Validation.EntitySchema.isValidEntityUID_implies_contains {ets : EntitySchema} {uid : Spec.EntityUID} : ets.isValidEntityUID uid = true → ets.contains uid.ty = true

def Cedar.Validation.ActionSchemaEntry.WellFormed (env : TypeEnv) (entry : ActionSchemaEntry) : Prop

Equations

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

def Cedar.Validation.ActionSchema.AcyclicActionHierarchy (acts : ActionSchema) : Prop

Equations

• acts.AcyclicActionHierarchy = ∀ (uid : Cedar.Spec.EntityUID) (entry : Cedar.Validation.ActionSchemaEntry), Cedar.Data.Map.find? acts uid = some entry → ¬uid ∈ entry.ancestors

def Cedar.Validation.ActionSchema.TransitiveActionHierarchy (acts : ActionSchema) : Prop

Equations

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

def Cedar.Validation.ActionSchema.WellFormed (env : TypeEnv) (acts : ActionSchema) : Prop

Equations

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

def Cedar.Validation.RequestType.WellFormed (env : TypeEnv) (reqty : RequestType) : Prop

Equations

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

def Cedar.Validation.TypeEnv.WellFormed (env : TypeEnv) : Prop

Equations

• env.WellFormed = (Cedar.Validation.EntitySchema.WellFormed env env.ets ∧ Cedar.Validation.ActionSchema.WellFormed env env.acts ∧ Cedar.Validation.RequestType.WellFormed env env.reqty)

theorem Cedar.Validation.qty_wf_implies_type_of_wf {env : TypeEnv} {qty : Qualified CedarType} (h : QualifiedType.WellFormed env qty) : CedarType.WellFormed env qty.getType

theorem Cedar.Validation.wf_record_type_cons {env : TypeEnv} {hd : Spec.Attr × Qualified CedarType} {tl : List (Spec.Attr × Qualified CedarType)} (hwf : CedarType.WellFormed env (CedarType.record (Data.Map.mk (hd :: tl)))) : CedarType.WellFormed env hd.snd.getType ∧ CedarType.WellFormed env (CedarType.record (Data.Map.mk tl))

theorem Cedar.Validation.wf_record_implies_wf_attr {env : TypeEnv} {rty : RecordType} {attr : Spec.Attr} {qty : QualifiedType} (hwf : CedarType.WellFormed env (CedarType.record rty)) (hqty : Data.Map.find? rty attr = some qty) : QualifiedType.WellFormed env qty

theorem Cedar.Validation.CedarType.WellFormed.mono {env₁ env₂ : TypeEnv} (hety : ∀ (ety : Spec.EntityType), EntityType.WellFormed env₁ ety → EntityType.WellFormed env₂ ety) {ty : CedarType} (h : WellFormed env₁ ty) : WellFormed env₂ ty

A type stays well-formed in an environment that has every entity type of the original.

theorem Cedar.Validation.emptyRecord_wf {env : TypeEnv} : CedarType.WellFormed env (CedarType.record Data.Map.empty)

The empty record type is well-formed.

theorem Cedar.Validation.emptyRecord_lifted : (CedarType.record Data.Map.empty).IsLifted

The empty record type is lifted.

theorem Cedar.Validation.standardEntry_wf {env : TypeEnv} {ancestors : Data.Set Spec.EntityType} {attrs : RecordType} (hwf : ancestors.WellFormed) (hdeclared : ∀ (a : Spec.EntityType), a ∈ ancestors → ∃ (entry : EntitySchemaEntry), Data.Map.find? env.ets a = some entry) (hattrs : CedarType.WellFormed env (CedarType.record attrs)) (hlifted : (CedarType.record attrs).IsLifted) : EntitySchemaEntry.WellFormed env (EntitySchemaEntry.standard { ancestors := ancestors, attrs := attrs, tags := none })

A standard entity type without tags is well-formed when its ancestors and attributes are.

theorem Cedar.Validation.wf_env_implies_wf_entity_schema_entry {env : TypeEnv} {ety : Spec.EntityType} {entry : EntitySchemaEntry} (hwf : env.WellFormed) (hets : Data.Map.find? env.ets ety = some entry) : EntitySchemaEntry.WellFormed env entry

theorem Cedar.Validation.wf_env_implies_wf_tag_type {env : TypeEnv} {ety : Spec.EntityType} {ty : CedarType} (hwf : env.WellFormed) (hety : env.ets.tags? ety = some (some ty)) : CedarType.WellFormed env ty

theorem Cedar.Validation.wf_env_implies_tag_type_lifted {env : TypeEnv} {ety : Spec.EntityType} {ty : CedarType} (hwf : env.WellFormed) (hety : env.ets.tags? ety = some (some ty)) : ty.IsLifted

theorem Cedar.Validation.wf_env_implies_wf_attrs {env : TypeEnv} {ety : Spec.EntityType} {attrs : RecordType} (hwf : env.WellFormed) (hattrs : env.ets.attrs? ety = some attrs) : CedarType.WellFormed env (CedarType.record attrs)

theorem Cedar.Validation.wf_env_implies_attrs_lifted {env : TypeEnv} {ety : Spec.EntityType} {attrs : RecordType} (hwf : env.WellFormed) (hattrs : env.ets.attrs? ety = some attrs) : (CedarType.record attrs).IsLifted

theorem Cedar.Validation.wf_env_implies_action_wf {env : TypeEnv} (hwf : env.WellFormed) : EntityUID.WellFormed env env.reqty.action

theorem Cedar.Validation.wf_env_disjoint_ets_acts {env : TypeEnv} {uid : Spec.EntityUID} {ets_entry : EntitySchemaEntry} {acts_entry : ActionSchemaEntry} (hwf : env.WellFormed) (hets : Data.Map.find? env.ets uid.ty = some ets_entry) (hacts : Data.Map.find? env.acts uid = some acts_entry) : False

theorem Cedar.Validation.wf_env_implies_wf_request {env : TypeEnv} (hwf : env.WellFormed) : EntityType.WellFormed env env.reqty.principal ∧ env.acts.contains env.reqty.action = true ∧ EntityType.WellFormed env env.reqty.resource ∧ CedarType.WellFormed env (CedarType.record env.reqty.context)

More well-formedness properties of env.reqty.

theorem Cedar.Validation.wf_env_implies_ctx_lifted {env : TypeEnv} (hwf : env.WellFormed) : (CedarType.record env.reqty.context).IsLifted

More well-formedness properties of env.reqty.

theorem Cedar.Validation.wf_env_implies_wf_acts_map {env : TypeEnv} (hwf : env.WellFormed) : Data.Map.WellFormed env.acts

theorem Cedar.Validation.wf_env_implies_wf_ets_map {env : TypeEnv} (hwf : env.WellFormed) : Data.Map.WellFormed env.ets

theorem Cedar.Validation.wf_env_implies_wf_entity_entry {env : TypeEnv} {ety : Spec.EntityType} {entry : EntitySchemaEntry} (hwf : env.WellFormed) (hfind : Data.Map.find? env.ets ety = some entry) : EntitySchemaEntry.WellFormed env entry

theorem Cedar.Validation.wf_env_implies_wf_action_entity_entry {env : TypeEnv} {uid : Spec.EntityUID} {entry : ActionSchemaEntry} (hwf : env.WellFormed) (hfind : Data.Map.find? env.acts uid = some entry) : ActionSchemaEntry.WellFormed env entry

theorem Cedar.Validation.wf_env_implies_wf_action_entity_ancestor {env : TypeEnv} {uid anc : Spec.EntityUID} {entry : ActionSchemaEntry} (hwf : env.WellFormed) (hfind : Data.Map.find? env.acts uid = some entry) (hanc : anc ∈ entry.ancestors) : ∃ (anc_entry : ActionSchemaEntry), Data.Map.find? env.acts anc = some anc_entry ∧ ActionSchemaEntry.WellFormed env anc_entry

Ancestor of an action entity should also be an action entity

theorem Cedar.Validation.wf_env_implies_wf_ancestor {env : TypeEnv} {entry : EntitySchemaEntry} {ety anc : Spec.EntityType} (hwf : env.WellFormed) (hfind : Data.Map.find? env.ets ety = some entry) (hanc : anc ∈ entry.ancestors) : EntityType.WellFormed env anc

theorem Cedar.Validation.wf_env_implies_wf_ancestor_set {env : TypeEnv} {entry : EntitySchemaEntry} {ety : Spec.EntityType} (hwf : env.WellFormed) (hfind : Data.Map.find? env.ets ety = some entry) : entry.ancestors.WellFormed

theorem Cedar.Validation.wf_env_implies_wf_action_ancestor_set {env : TypeEnv} {entry : ActionSchemaEntry} {uid : Spec.EntityUID} (hwf : env.WellFormed) (hfind : Data.Map.find? env.acts uid = some entry) : entry.ancestors.WellFormed

theorem Cedar.Validation.wf_env_implies_acyclic_action_hierarchy {env : TypeEnv} (hwf : env.WellFormed) : env.acts.AcyclicActionHierarchy

theorem Cedar.Validation.wf_env_implies_transitive_action_hierarchy {env : TypeEnv} (hwf : env.WellFormed) : env.acts.TransitiveActionHierarchy

theorem Cedar.Validation.wf_env_implies_ancestors_of_standard_ety_exist {env : TypeEnv} {ety : Spec.EntityType} {entry : StandardSchemaEntry} (hwf : env.WellFormed) (hfind : Data.Map.find? env.ets ety = some (EntitySchemaEntry.standard entry)) (anc : Spec.EntityType) : anc ∈ entry.ancestors → ∃ (entry : EntitySchemaEntry), Data.Map.find? env.ets anc = some entry

theorem Cedar.Validation.wf_env_implies_ancestors_of_action_is_action {env : TypeEnv} {uid : Spec.EntityUID} {entry : ActionSchemaEntry} (hwf : env.WellFormed) (hfind : Data.Map.find? env.acts uid = some entry) (uid✝ : Spec.EntityUID) : uid✝ ∈ entry.ancestors → env.acts.contains uid✝ = true

theorem Cedar.Validation.TypeEnv.maps_wf_of_eq {env₁ env₂ : TypeEnv} (hets : env₁.ets = env₂.ets) (hacts : env₁.acts = env₂.acts) (h : EntitySchema.WellFormed env₁ env₁.ets ∧ ActionSchema.WellFormed env₁ env₁.acts) : EntitySchema.WellFormed env₂ env₂.ets ∧ ActionSchema.WellFormed env₂ env₂.acts

Whether an environment's maps are well-formed does not depend on its request type.