def Cedar.Validation.PartialEntitySchema.AncestorsClosed (schema : PartialEntitySchema) : Prop

Every ancestor set is transitively closed. TODO: it is a bit suprising how this does not already exists. Maybe define it for complete schema and see if it is useful for proving some nice facts about schema.

Equations

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

def Cedar.Validation.PartialEntitySchema.ExternalParentsStandard (schema : PartialEntitySchema) : Prop

No external entity type declaration lists an enum entity type as a parent: a definition of the external must list the parent, so only a declaration of the parent, which an enum definition cannot be, can supply it.

Equations

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

def Cedar.Validation.PartialSchema.WellFormed (schema : PartialSchema) : Prop

A partial schema is well-formed when its definitions satisfy the existing schema conditions, its externals satisfy those conditions using only their known ancestors, and no external lists an enum entity type as a parent.

Equations

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

def Cedar.Validation.PartialSchema.wfEnv (schema : PartialSchema) : TypeEnv

The environment in which PartialSchema.WellFormed checks a partial schema and PartialSchema.validateEntities validates entities: the validation view with the default request type.

Equations

• schema.wfEnv = { ets := schema.validationView.ets, acts := schema.validationView.acts, reqty := default }

structure Cedar.Validation.DeclarationsKept (s t : PartialSchema) : Prop

t keeps every declaration of s: its entity types with their definitions, standard entity types, and listed ancestors, and its actions with their ancestors and definitions.

• entities (ety : Spec.EntityType) : Data.Map.contains s.ets ety = true → Data.Map.contains t.ets ety = true
• definitions (ety : Spec.EntityType) (entry : EntitySchemaEntry) : Data.Map.find? s.ets ety = some (PartialEntitySchemaEntry.defined entry) → Data.Map.find? t.ets ety = some (PartialEntitySchemaEntry.defined entry)
• standard (ety : Spec.EntityType) (entry : PartialEntitySchemaEntry) : Data.Map.find? s.ets ety = some entry → entry.isStandard = true → ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? t.ets ety = some entry' ∧ entry'.isStandard = true
• ancestors (ety : Spec.EntityType) (entry : PartialEntitySchemaEntry) (ancestor : Spec.EntityType) : Data.Map.find? s.ets ety = some entry → ancestor ∈ entry.ancestors → ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? t.ets ety = some entry' ∧ ancestor ∈ entry'.ancestors
• actions (uid : Spec.EntityUID) (entry : PartialActionSchemaEntry) : Data.Map.find? s.acts uid = some entry → ∃ (entry' : PartialActionSchemaEntry), Data.Map.find? t.acts uid = some entry' ∧ entry'.ancestors = entry.ancestors
• actionDefinitions (uid : Spec.EntityUID) (entry : ActionSchemaEntry) : Data.Map.find? s.acts uid = some (PartialActionSchemaEntry.defined entry) → Data.Map.find? t.acts uid = some (PartialActionSchemaEntry.defined entry)

structure Cedar.Validation.EntryKept (x z : PartialEntitySchemaEntry) : Prop

z keeps the definition, the standard kind, and the ancestors of the entity entry x.

• definition (entry : EntitySchemaEntry) : x = PartialEntitySchemaEntry.defined entry → z = PartialEntitySchemaEntry.defined entry
• standard : x.isStandard = true → z.isStandard = true
• ancestors : x.ancestors ⊆ z.ancestors

def Cedar.Validation.PartialEntitySchemaEntry.completeWith (attrs : RecordType) : PartialEntitySchemaEntry → EntitySchemaEntry

The definition that completes an entity entry: its definition, or a standard entity type with its ancestors, the attributes attrs, and no tags.

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.PartialEntitySchemaEntry.completeWith attrs (Cedar.Validation.PartialEntitySchemaEntry.defined entry) = entry

def Cedar.Validation.PartialSchema.completeWith (p : PartialSchema) (attrs : RecordType) : Schema

The schema that completes p: it defines each external entity type of p with the attributes attrs, and each external action by its validation view.

Equations

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

theorem Cedar.Validation.toPartialSchema_asSchema? (schema : Schema) : (↑schema).asSchema? = some schema

Coercing a schema to a partial schema and back preserves it.

theorem Cedar.Validation.toPartialSchema_validationView (schema : Schema) : (↑schema).validationView = schema

Coercing a schema to a partial schema preserves its validation view.

theorem Cedar.Validation.toPartialSchema_ets_find? (schema : Schema) (ety : Spec.EntityType) : Data.Map.find? (↑schema).ets ety = Option.map PartialEntitySchemaEntry.defined (Data.Map.find? schema.ets ety)

Coercing a schema to a partial schema defines each of its entity types.

theorem Cedar.Validation.toPartialSchema_acts_find? (schema : Schema) (uid : Spec.EntityUID) : Data.Map.find? (↑schema).acts uid = Option.map PartialActionSchemaEntry.defined (Data.Map.find? schema.acts uid)

Coercing a schema to a partial schema defines each of its actions.

theorem Cedar.Validation.toPartialSchema_wfEnv (schema : Schema) : (↑schema).wfEnv = { ets := schema.ets, acts := schema.acts, reqty := default }

A coerced schema is checked in the environment with its own maps.

theorem Cedar.Validation.asSchema?_isSome_iff_isComplete (schema : PartialSchema) : schema.asSchema?.isSome = true ↔ schema.isComplete = true

A partial schema converts to a schema exactly when it is complete.

theorem Cedar.Validation.validationView_find?_ets (schema : PartialSchema) (ety : Spec.EntityType) : Data.Map.find? schema.validationView.ets ety = Option.map PartialEntitySchemaEntry.validationView (Data.Map.find? schema.ets ety)

The entity validation view maps the entry found in the partial schema.

theorem Cedar.Validation.validationView_find?_acts (schema : PartialSchema) (uid : Spec.EntityUID) : Data.Map.find? schema.validationView.acts uid = Option.map PartialActionSchemaEntry.validationView (Data.Map.find? schema.acts uid)

The action validation view maps the entry found in the partial schema.

theorem Cedar.Validation.validationView_eq_of_asSchema? {ps : PartialSchema} {schema : Schema} (h : ps.asSchema? = some schema) : ps.validationView = schema

A completed partial schema agrees with its validation view.

theorem Cedar.Validation.PartialActionSchemaEntry.validationView_ancestors (entry : PartialActionSchemaEntry) : entry.validationView.ancestors = entry.ancestors

The validation view keeps an action's ancestors.

theorem Cedar.Validation.PartialEntitySchemaEntry.validationView_isStandard (entry : PartialEntitySchemaEntry) : entry.validationView.isStandard = entry.isStandard

The validation view keeps whether an entity type is standard or external.

theorem Cedar.Validation.PartialEntitySchemaEntry.validationView_isValidEntityEID {entry : PartialEntitySchemaEntry} (h : entry.isStandard = true) (eid : String) : entry.validationView.isValidEntityEID eid = true

A standard or external entity type accepts every entity id in the validation view.

theorem Cedar.Validation.PartialEntitySchemaEntry.withAncestors_isStandard (entry : PartialEntitySchemaEntry) (ancestors : Data.Set Spec.EntityType) : (withAncestors ancestors entry).isStandard = entry.isStandard

Replacing ancestors keeps an entry standard or external.

theorem Cedar.Validation.PartialSchema.WellFormed.etsMap {schema : PartialSchema} (h : schema.WellFormed) : Data.Map.WellFormed schema.ets

A well-formed partial schema has a well-formed entity map.

theorem Cedar.Validation.PartialSchema.WellFormed.actsMap {schema : PartialSchema} (h : schema.WellFormed) : Data.Map.WellFormed schema.acts

A well-formed partial schema has a well-formed action map.

theorem Cedar.Validation.PartialSchema.wellFormed_iff {schema : PartialSchema} : schema.WellFormed ↔ schema.ets.AncestorsClosed ∧ schema.ets.ExternalParentsStandard ∧ EntitySchema.WellFormed schema.wfEnv schema.wfEnv.ets ∧ ActionSchema.WellFormed schema.wfEnv schema.wfEnv.acts

PartialSchema.WellFormed checks the maps in wfEnv.

theorem Cedar.Validation.PartialSchema.wfEnv_ets_find? {schema : PartialSchema} {ety : Spec.EntityType} {entry : EntitySchemaEntry} (h : Data.Map.find? schema.wfEnv.ets ety = some entry) : ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? schema.ets ety = some entry' ∧ entry'.validationView = entry

Each entity entry of wfEnv is the view of an entry of the partial schema.

theorem Cedar.Validation.PartialSchema.wfEnv_acts_find? {schema : PartialSchema} {uid : Spec.EntityUID} {entry : ActionSchemaEntry} (h : Data.Map.find? schema.wfEnv.acts uid = some entry) : ∃ (entry' : PartialActionSchemaEntry), Data.Map.find? schema.acts uid = some entry' ∧ entry'.validationView = entry

Each action entry of wfEnv is the view of an entry of the partial schema.

theorem Cedar.Validation.PartialSchema.wfEnv_ets_contains (schema : PartialSchema) (ety : Spec.EntityType) : schema.wfEnv.ets.contains ety = Data.Map.contains schema.ets ety

wfEnv declares the entity types of the partial schema.

theorem Cedar.Validation.PartialSchema.wfEnv_acts_contains (schema : PartialSchema) (uid : Spec.EntityUID) : schema.wfEnv.acts.contains uid = Data.Map.contains schema.acts uid

wfEnv declares the actions of the partial schema.

theorem Cedar.Validation.PartialSchema.WellFormed.entry {schema : PartialSchema} {ety : Spec.EntityType} {entry : PartialEntitySchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.ets ety = some entry) : EntitySchemaEntry.WellFormed schema.wfEnv entry.validationView

In a well-formed partial schema, the view of each entity entry is well-formed.

theorem Cedar.Validation.PartialSchema.WellFormed.action {schema : PartialSchema} {uid : Spec.EntityUID} {entry : PartialActionSchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.acts uid = some entry) : ActionSchemaEntry.WellFormed schema.wfEnv entry.validationView

In a well-formed partial schema, the view of each action is well-formed.

theorem Cedar.Validation.PartialSchema.WellFormed.external_parent_isStandard {schema : PartialSchema} {ety parent : Spec.EntityType} {parents : Data.Set Spec.EntityType} (h : schema.WellFormed) (hfind : Data.Map.find? schema.ets ety = some (PartialEntitySchemaEntry.external parents)) (hmem : parent ∈ parents) : ∃ (entry : PartialEntitySchemaEntry), Data.Map.find? schema.ets parent = some entry ∧ entry.isStandard = true

In a well-formed partial schema, no parent of an external entity type is an enum.

theorem Cedar.Validation.PartialSchema.WellFormed.ancestor_declared {schema : PartialSchema} {ety ancestor : Spec.EntityType} {entry : PartialEntitySchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.ets ety = some entry) (hmem : ancestor ∈ entry.ancestors) : ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? schema.ets ancestor = some entry'

In a well-formed partial schema, every ancestor of an entity type is declared.

theorem Cedar.Validation.PartialSchema.WellFormed.action_ancestor {schema : PartialSchema} {uid ancestor : Spec.EntityUID} {entry : PartialActionSchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.acts uid = some entry) (hmem : ancestor ∈ entry.ancestors) : Data.Map.contains schema.acts ancestor = true

In a well-formed partial schema, every ancestor of an action is an action.

theorem Cedar.Validation.PartialSchema.WellFormed.acyclic {schema : PartialSchema} {uid : Spec.EntityUID} {entry : PartialActionSchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.acts uid = some entry) : ¬uid ∈ entry.ancestors

A well-formed partial schema has no action among its own ancestors.

theorem Cedar.Validation.PartialSchema.WellFormed.transitive {schema : PartialSchema} {uid₁ uid₂ : Spec.EntityUID} {entry₁ entry₂ : PartialActionSchemaEntry} (h : schema.WellFormed) (hfind₁ : Data.Map.find? schema.acts uid₁ = some entry₁) (hfind₂ : Data.Map.find? schema.acts uid₂ = some entry₂) (hmem : uid₂ ∈ entry₁.ancestors) : entry₂.ancestors ⊆ entry₁.ancestors

A well-formed partial schema has transitively closed action ancestors.

theorem Cedar.Validation.PartialSchema.WellFormed.disjoint {schema : PartialSchema} {uid : Spec.EntityUID} (h : schema.WellFormed) (haction : Data.Map.contains schema.acts uid = true) : ¬Data.Map.contains schema.ets uid.ty = true

A well-formed partial schema declares no action type as an entity type.

theorem Cedar.Validation.PartialSchema.WellFormed.ancestors_wf {schema : PartialSchema} {ety : Spec.EntityType} {entry : PartialEntitySchemaEntry} (h : schema.WellFormed) (hfind : Data.Map.find? schema.ets ety = some entry) : entry.ancestors.WellFormed

In a well-formed partial schema, every entity entry has well-formed ancestors.

theorem Cedar.Validation.PartialEntitySchema.AncestorsClosed.reach {ets : PartialEntitySchema} (h : ets.AncestorsClosed) {ety ancestor : Spec.EntityType} {entry : PartialEntitySchemaEntry} (hfind : Data.Map.find? ets ety = some entry) (hreach : Relation.TransGen (fun (x y : Spec.EntityType) => ∃ (e : PartialEntitySchemaEntry), Data.Map.find? ets x = some e ∧ y ∈ e.ancestors) ety ancestor) : ancestor ∈ entry.ancestors

With closed ancestors, every entity type reachable through listed ancestors is listed.

theorem Cedar.Validation.PartialActionSchemaEntry.external_validationView_wf {env : TypeEnv} {ancestors : Data.Set Spec.EntityUID} (hwf : ancestors.WellFormed) (hactions : ∀ (a : Spec.EntityUID), a ∈ ancestors → env.acts.contains a = true) : ActionSchemaEntry.WellFormed env (external ancestors).validationView

An external action's view is well-formed when its ancestors are a well-formed set of actions.

theorem Cedar.Validation.DeclarationsKept.acts_contains {s t : PartialSchema} (h : DeclarationsKept s t) {uid : Spec.EntityUID} (hs : Data.Map.contains s.acts uid = true) : Data.Map.contains t.acts uid = true

t declares every action of s.

theorem Cedar.Validation.DeclarationsKept.entityType_wf {s t : PartialSchema} (h : DeclarationsKept s t) {ety : Spec.EntityType} (hwf : EntityType.WellFormed s.wfEnv ety) : EntityType.WellFormed t.wfEnv ety

An entity type well-formed for s is well-formed for t.

theorem Cedar.Validation.DeclarationsKept.cedarType_wf {s t : PartialSchema} (h : DeclarationsKept s t) {ty : CedarType} (hwf : CedarType.WellFormed s.wfEnv ty) : CedarType.WellFormed t.wfEnv ty

A type well-formed for s is well-formed for t.

theorem Cedar.Validation.DeclarationsKept.ancestor_declared {s t : PartialSchema} (h : DeclarationsKept s t) (hs : s.WellFormed) {ety ancestor : Spec.EntityType} {entry : PartialEntitySchemaEntry} (hfind : Data.Map.find? s.ets ety = some entry) (hmem : ancestor ∈ entry.ancestors) : ∃ (ventry : EntitySchemaEntry), Data.Map.find? t.wfEnv.ets ancestor = some ventry

An ancestor listed in a well-formed s is declared in t.

theorem Cedar.Validation.DeclarationsKept.definition_wf {s t : PartialSchema} (h : DeclarationsKept s t) (hs : s.WellFormed) {ety : Spec.EntityType} {entry : EntitySchemaEntry} (hfind : Data.Map.find? s.ets ety = some (PartialEntitySchemaEntry.defined entry)) : EntitySchemaEntry.WellFormed t.wfEnv entry

A definition of a well-formed s is well-formed in t.

theorem Cedar.Validation.DeclarationsKept.action_wf {s t : PartialSchema} (h : DeclarationsKept s t) (hs : s.WellFormed) {uid : Spec.EntityUID} {entry : PartialActionSchemaEntry} (hfind : Data.Map.find? s.acts uid = some entry) : ActionSchemaEntry.WellFormed t.wfEnv entry.validationView

An action of a well-formed s is well-formed in t.

theorem Cedar.Validation.DeclarationsKept.transitive {s t : PartialSchema} (h : DeclarationsKept s t) (hs : s.WellFormed) {uid₁ uid₂ : Spec.EntityUID} {entry₁ entry₂ : PartialActionSchemaEntry} (hfind₁ : Data.Map.find? s.acts uid₁ = some entry₁) (hfind₂ : Data.Map.find? t.acts uid₂ = some entry₂) (hmem : uid₂ ∈ entry₁.ancestors) : entry₂.ancestors ⊆ entry₁.ancestors

In t, the ancestors of an ancestor of an action of a well-formed s are ancestors of that action.

theorem Cedar.Validation.DeclarationsKept.trans {s t u : PartialSchema} (hst : DeclarationsKept s t) (htu : DeclarationsKept t u) : DeclarationsKept s u

Keeping declarations is transitive.

theorem Cedar.Validation.DeclarationsKept.entry {s t : PartialSchema} (h : DeclarationsKept s t) {ety : Spec.EntityType} {x z : PartialEntitySchemaEntry} (hx : Data.Map.find? s.ets ety = some x) (hz : Data.Map.find? t.ets ety = some z) : EntryKept x z

The entry of t for an entity type of s keeps the entry of s.

theorem Cedar.Validation.DeclarationsKept.antisymm {s t : PartialSchema} (hs : s.WellFormed) (ht : t.WellFormed) (hst : DeclarationsKept s t) (hts : DeclarationsKept t s) : s = t

Well-formed partial schemas that keep each other's declarations are equal.

theorem Cedar.Validation.DeclarationsKept.eq_toPartialSchema {t : PartialSchema} {schema : Schema} (hets : Data.Map.WellFormed t.ets) (hacts : Data.Map.WellFormed t.acts) (hschema : (↑schema).WellFormed) (hts : DeclarationsKept t ↑schema) (hst : DeclarationsKept (↑schema) t) : t = ↑schema

A partial schema with well-formed maps is a schema that it keeps and that keeps it.

theorem Cedar.Validation.completeWith_ets_find? (p : PartialSchema) (attrs : RecordType) (ety : Spec.EntityType) : Data.Map.find? (p.completeWith attrs).ets ety = Option.map (fun (x : PartialEntitySchemaEntry) => PartialEntitySchemaEntry.completeWith attrs x) (Data.Map.find? p.ets ety)

Completing a partial schema completes each of its entity entries.

theorem Cedar.Validation.completeWith_empty (p : PartialSchema) : p.completeWith Data.Map.empty = p.validationView

Completing with no attributes gives the validation view.

theorem Cedar.Validation.PartialEntitySchemaEntry.completeWith_ancestors (attrs : RecordType) (entry : PartialEntitySchemaEntry) : (completeWith attrs entry).ancestors = entry.ancestors

Completing an entry keeps its ancestors.

theorem Cedar.Validation.PartialEntitySchemaEntry.completeWith_isStandard (attrs : RecordType) (entry : PartialEntitySchemaEntry) : (completeWith attrs entry).isStandard = entry.isStandard

Completing an entry keeps whether it is standard or external.

theorem Cedar.Validation.toPartialSchema_completeWith_ets_find? (p : PartialSchema) (attrs : RecordType) (ety : Spec.EntityType) : Data.Map.find? (↑(p.completeWith attrs)).ets ety = Option.map (fun (entry : PartialEntitySchemaEntry) => PartialEntitySchemaEntry.defined (PartialEntitySchemaEntry.completeWith attrs entry)) (Data.Map.find? p.ets ety)

The partial schema of a completion defines each entity type of p by its completion.

theorem Cedar.Validation.toPartialSchema_completeWith_acts_find? (p : PartialSchema) (attrs : RecordType) (uid : Spec.EntityUID) : Data.Map.find? (↑(p.completeWith attrs)).acts uid = Option.map (fun (entry : PartialActionSchemaEntry) => PartialActionSchemaEntry.defined entry.validationView) (Data.Map.find? p.acts uid)

The partial schema of a completion defines each action of p by its validation view.

theorem Cedar.Validation.DeclarationsKept.completeWith (p : PartialSchema) (attrs : RecordType) : DeclarationsKept p ↑(p.completeWith attrs)

Completing p keeps the declarations of p.

theorem Cedar.Validation.PartialSchema.WellFormed.completeWith {p : PartialSchema} {attrs : RecordType} (hp : p.WellFormed) (hwf : ∀ (env : TypeEnv), CedarType.WellFormed env (CedarType.record attrs)) (hlifted : (CedarType.record attrs).IsLifted) : (↑(p.completeWith attrs)).WellFormed

Completing a well-formed partial schema with well-formed lifted attributes is well-formed.