theorem Cedar.Validation.linker_preserves_definitions {p c t : PartialSchema} (hlink : link p c = Except.ok t) : (∀ (ety : Spec.EntityType) (entry : EntitySchemaEntry), Data.Map.find? p.ets ety = some (PartialEntitySchemaEntry.defined entry) → Data.Map.find? t.ets ety = some (PartialEntitySchemaEntry.defined entry)) ∧ (∀ (ety : Spec.EntityType) (entry : EntitySchemaEntry), Data.Map.find? c.ets ety = some (PartialEntitySchemaEntry.defined entry) → Data.Map.find? t.ets ety = some (PartialEntitySchemaEntry.defined entry)) ∧ (∀ (uid : Spec.EntityUID) (entry : ActionSchemaEntry), Data.Map.find? p.acts uid = some (PartialActionSchemaEntry.defined entry) → Data.Map.find? t.acts uid = some (PartialActionSchemaEntry.defined entry)) ∧ ∀ (uid : Spec.EntityUID) (entry : ActionSchemaEntry), Data.Map.find? c.acts uid = some (PartialActionSchemaEntry.defined entry) → Data.Map.find? t.acts uid = some (PartialActionSchemaEntry.defined entry)

Every entity or action definition from either input appears unchanged in the result.

theorem Cedar.Validation.linker_preserves_entity_declarations {p c t : PartialSchema} (hlink : link p c = Except.ok t) (ety : Spec.EntityType) : Data.Map.contains t.ets ety = true ↔ Data.Map.contains p.ets ety = true ∨ Data.Map.contains c.ets ety = true

The result declares exactly the entity types declared by either input.

theorem Cedar.Validation.linker_preserves_action_declarations {p c t : PartialSchema} (hlink : link p c = Except.ok t) (uid : Spec.EntityUID) : Data.Map.contains t.acts uid = true ↔ Data.Map.contains p.acts uid = true ∨ Data.Map.contains c.acts uid = true

The result declares exactly the action UIDs declared by either input.

theorem Cedar.Validation.linker_preserves_action_ancestors {p c t : PartialSchema} (hlink : link p c = Except.ok t) : (∀ (uid : Spec.EntityUID) (entry : PartialActionSchemaEntry), Data.Map.find? p.acts uid = some entry → ∃ (entry' : PartialActionSchemaEntry), Data.Map.find? t.acts uid = some entry' ∧ entry'.ancestors = entry.ancestors) ∧ ∀ (uid : Spec.EntityUID) (entry : PartialActionSchemaEntry), Data.Map.find? c.acts uid = some entry → ∃ (entry' : PartialActionSchemaEntry), Data.Map.find? t.acts uid = some entry' ∧ entry'.ancestors = entry.ancestors

Every action from either input keeps its ancestors in the result.

theorem Cedar.Validation.linker_preserves_standard_entities {p c t : PartialSchema} (hlink : link p c = Except.ok t) : (∀ (ety : Spec.EntityType) (entry : PartialEntitySchemaEntry), Data.Map.find? p.ets ety = some entry → entry.isStandard = true → ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? t.ets ety = some entry' ∧ entry'.isStandard = true) ∧ ∀ (ety : Spec.EntityType) (entry : PartialEntitySchemaEntry), Data.Map.find? c.ets ety = some entry → entry.isStandard = true → ∃ (entry' : PartialEntitySchemaEntry), Data.Map.find? t.ets ety = some entry' ∧ entry'.isStandard = true

Every standard or external entity type from either input is standard or external in the result. In particular, an external entity type never links to an enumerated entity type.

theorem Cedar.Validation.linker_action_types_not_entity_types {p c t : PartialSchema} {uid : Spec.EntityUID} (hlink : link p c = Except.ok t) (haction : Data.Map.contains t.acts uid = true) : ¬Data.Map.contains t.ets uid.ty = true

The result never declares the entity type of an action as an entity type.

theorem Cedar.Validation.linker_definitions_come_from_inputs {p c t : PartialSchema} {ety : Spec.EntityType} {entry : EntitySchemaEntry} (hlink : link p c = Except.ok t) (hfind : Data.Map.find? t.ets ety = some (PartialEntitySchemaEntry.defined entry)) : Data.Map.find? p.ets ety = some (PartialEntitySchemaEntry.defined entry) ∨ Data.Map.find? c.ets ety = some (PartialEntitySchemaEntry.defined entry)

Every entity definition of the result is a definition from either input.

theorem Cedar.Validation.linker_actions_come_from_inputs {p c t : PartialSchema} {uid : Spec.EntityUID} {entry : PartialActionSchemaEntry} (hlink : link p c = Except.ok t) (hfind : Data.Map.find? t.acts uid = some entry) : Data.Map.find? p.acts uid = some entry ∨ Data.Map.find? c.acts uid = some entry

Every action entry of the result is that action's entry in either input.

theorem Cedar.Validation.linker_entity_ancestors {p c t : PartialSchema} {ety ancestor : Spec.EntityType} {entry : PartialEntitySchemaEntry} (hlink : link p c = Except.ok t) (hfind : Data.Map.find? t.ets ety = some entry) : ancestor ∈ entry.ancestors ↔ Relation.TransGen (fun (x y : Spec.EntityType) => (∃ (e : PartialEntitySchemaEntry), Data.Map.find? p.ets x = some e ∧ y ∈ e.ancestors) ∨ ∃ (e : PartialEntitySchemaEntry), Data.Map.find? c.ets x = some e ∧ y ∈ e.ancestors) ety ancestor

An entity type's ancestors in the result are exactly the entity types reachable from it through the ancestors listed by either input.

theorem Cedar.Validation.linker_keeps_declarations {p c t : PartialSchema} (hlink : link p c = Except.ok t) : DeclarationsKept p t ∧ DeclarationsKept c t

The result keeps every declaration of either input.

theorem Cedar.Validation.linker_result_kept {p c t u : PartialSchema} (hlink : link p c = Except.ok t) (hclosed : u.ets.AncestorsClosed) (hpu : DeclarationsKept p u) (hcu : DeclarationsKept c u) : DeclarationsKept t u

A partial schema with closed ancestors that keeps the declarations of both inputs keeps the declarations of the result.

theorem Cedar.Validation.linker_definitions_disjoint {p c t : PartialSchema} (hlink : link p c = Except.ok t) : (∀ (ety : Spec.EntityType) (e₁ e₂ : EntitySchemaEntry), Data.Map.find? p.ets ety = some (PartialEntitySchemaEntry.defined e₁) → Data.Map.find? c.ets ety ≠ some (PartialEntitySchemaEntry.defined e₂)) ∧ ∀ (uid : Spec.EntityUID) (e₁ e₂ : ActionSchemaEntry), Data.Map.find? p.acts uid = some (PartialActionSchemaEntry.defined e₁) → Data.Map.find? c.acts uid ≠ some (PartialActionSchemaEntry.defined e₂)

No entity type or action is defined by both inputs.

theorem Cedar.Validation.linker_completion {p : PartialSchema} {attrs : RecordType} (hp : p.WellFormed) (hwf : ∀ (env : TypeEnv), CedarType.WellFormed env (CedarType.record attrs)) (hlifted : (CedarType.record attrs).IsLifted) : ∃ (c : PartialSchema), c.WellFormed ∧ link p c = Except.ok ↑(p.completeWith attrs)

A well-formed partial schema links into the schema that completes it with attributes attrs, when these are well-formed and lifted.

theorem Cedar.Validation.linker_completion_validationView {p : PartialSchema} (hp : p.WellFormed) : ∃ (c : PartialSchema), c.WellFormed ∧ link p c = Except.ok ↑p.validationView

A well-formed partial schema links into its validation view.

theorem Cedar.Validation.linker_commutativity {p c t : PartialSchema} (hc : c.WellFormed) (hlink : link p c = Except.ok t) : link c p = Except.ok t

Changing the input order does not change a successful link.

theorem Cedar.Validation.linker_commutativity_error {p c : PartialSchema} (hp : p.WellFormed) (hc : c.WellFormed) : (∃ (err : LinkError), link p c = Except.error err) ↔ ∃ (err : LinkError), link c p = Except.error err

Changing the input order does not change whether linking fails.

theorem Cedar.Validation.linker_preserves_well_formedness {p c t : PartialSchema} (hp : p.WellFormed) (hc : c.WellFormed) (hlink : link p c = Except.ok t) : t.WellFormed

Linking well-formed partial schemas produces a well-formed partial schema.

theorem Cedar.Validation.linker_completed_schema_well_formed {p c t : PartialSchema} {schema : Schema} (hp : p.WellFormed) (hc : c.WellFormed) (hlink : link p c = Except.ok t) (hcomplete : t.asSchema? = some schema) : schema.validateWellFormed = Except.ok ()

A complete link passes the existing schema well-formedness check.

theorem Cedar.Validation.linker_associativity {p c d t₁ t : PartialSchema} (hp : p.WellFormed) (hc : c.WellFormed) (hd : d.WellFormed) (hpc : link p c = Except.ok t₁) (hpcd : link t₁ d = Except.ok t) : ∃ (t₂ : PartialSchema), link c d = Except.ok t₂ ∧ link p t₂ = Except.ok t

Changing the grouping does not change a successful link.

theorem Cedar.Validation.linker_associativity_error {p c d : PartialSchema} (hp : p.WellFormed) (hc : c.WellFormed) (hd : d.WellFormed) : (∃ (err : LinkError), (do let t₁ ← link p c link t₁ d) = Except.error err) ↔ ∃ (err : LinkError), (do let t₂ ← link c d link p t₂) = Except.error err

Changing the grouping does not change whether linking fails.

theorem Cedar.Validation.linker_completion_exists {p : PartialSchema} (hp : p.WellFormed) : ∃ (c : PartialSchema), ∃ (t : PartialSchema), ∃ (schema : Schema), c.WellFormed ∧ link p c = Except.ok t ∧ t.asSchema? = some schema

Every well-formed partial schema has a complete linking extension.

theorem Cedar.Validation.stable_entity_ancestor {p c t : PartialSchema} {ety : Spec.EntityType} {entry : EntitySchemaEntry} (hlink : link p c = Except.ok t) (hentry : Data.Map.find? p.ets ety = some (PartialEntitySchemaEntry.defined entry)) : ∃ (linkedEntry : EntitySchemaEntry), Data.Map.find? t.ets ety = some (PartialEntitySchemaEntry.defined linkedEntry) ∧ linkedEntry.ancestors = entry.ancestors

A defined entity keeps its closed ancestor set after linking.