This file proves that various *.validateWellFormed functions correctly implement their spec versions.

theorem Cedar.Thm.entity_type_validate_well_formed_is_sound {env : Validation.TypeEnv} {ety : Spec.EntityType} (hok : Validation.EntityType.validateWellFormed env ety = Except.ok ()) : Validation.EntityType.WellFormed env ety

theorem Cedar.Thm.validate_attrs_well_formed_is_sound {env : Validation.TypeEnv} {rty : List (Spec.Attr × Validation.QualifiedType)} {attr : Spec.Attr} {qty : Validation.QualifiedType} (hwf : (Data.Map.mk rty).WellFormed) (hok : Validation.validateAttrsWellFormed env rty = Except.ok ()) (hfind : (Data.Map.mk rty).find? attr = some qty) : Validation.QualifiedType.WellFormed env qty

theorem Cedar.Thm.type_validate_well_formed_is_sound {env : Validation.TypeEnv} {ty : Validation.CedarType} (hok : Validation.CedarType.validateWellFormed env ty = Except.ok ()) : Validation.CedarType.WellFormed env ty

theorem Cedar.Thm.type_validate_lifted_is_sound {ty : Validation.CedarType} (hok : ty.validateLifted = Except.ok ()) : ty.IsLifted

theorem Cedar.Thm.standard_schema_entry_validate_well_formed_is_sound {env : Validation.TypeEnv} {entry : Validation.StandardSchemaEntry} (hok : Validation.StandardSchemaEntry.validateWellFormed env entry = Except.ok ()) : Validation.StandardSchemaEntry.WellFormed env entry

theorem Cedar.Thm.entity_schema_entry_validate_well_formed_is_sound {env : Validation.TypeEnv} {entry : Validation.EntitySchemaEntry} (hok : Validation.EntitySchemaEntry.validateWellFormed env entry = Except.ok ()) : Validation.EntitySchemaEntry.WellFormed env entry

theorem Cedar.Thm.entity_schema_validate_well_formed_is_sound {env : Validation.TypeEnv} {ets : Validation.EntitySchema} (hok : Validation.EntitySchema.validateWellFormed env ets = Except.ok ()) : Validation.EntitySchema.WellFormed env ets

theorem Cedar.Thm.action_schema_entry_validate_well_formed_is_sound {env : Validation.TypeEnv} {entry : Validation.ActionSchemaEntry} (hok : Validation.ActionSchemaEntry.validateWellFormed env entry = Except.ok ()) : Validation.ActionSchemaEntry.WellFormed env entry

theorem Cedar.Thm.action_schema_validate_acyclic_action_hierarchy_is_sound {acts : Validation.ActionSchema} (hok : acts.validateAcyclicActionHierarchy = Except.ok ()) : acts.AcyclicActionHierarchy

theorem Cedar.Thm.action_schema_validate_transitive_action_hierarchy_is_sound {acts : Validation.ActionSchema} (hok : acts.validateTransitiveActionHierarchy = Except.ok ()) : acts.TransitiveActionHierarchy

theorem Cedar.Thm.action_schema_validate_well_formed_is_sound {env : Validation.TypeEnv} {acts : Validation.ActionSchema} (hok : Validation.ActionSchema.validateWellFormed env acts = Except.ok ()) : Validation.ActionSchema.WellFormed env acts

theorem Cedar.Thm.request_type_validate_well_formed_is_sound {env : Validation.TypeEnv} {reqty : Validation.RequestType} (hok : Validation.RequestType.validateWellFormed env reqty = Except.ok ()) : Validation.RequestType.WellFormed env reqty

theorem Cedar.Thm.env_validate_well_formed_is_sound {env : Validation.TypeEnv} (hok : env.validateWellFormed = Except.ok ()) : env.WellFormed

theorem Cedar.Thm.environment_some_mem_environments {schema : Validation.Schema} {principal resource : Spec.EntityType} {action : Spec.EntityUID} {env : Validation.TypeEnv} (h : schema.environment? principal resource action = some env) : env ∈ schema.environments

Completeness: well-formed environments pass the executable checks

theorem Cedar.Thm.entity_type_validate_well_formed_is_complete {env : Validation.TypeEnv} {ety : Spec.EntityType} (hwf : Validation.EntityType.WellFormed env ety) : Validation.EntityType.validateWellFormed env ety = Except.ok ()

theorem Cedar.Thm.validate_attrs_well_formed_is_complete {env : Validation.TypeEnv} {rty : List (Spec.Attr × Validation.QualifiedType)} (hwf : ∀ (attr : Spec.Attr) (qty : Validation.QualifiedType), (attr, qty) ∈ rty → Validation.QualifiedType.WellFormed env qty) : Validation.validateAttrsWellFormed env rty = Except.ok ()

theorem Cedar.Thm.type_validate_well_formed_is_complete {env : Validation.TypeEnv} {ty : Validation.CedarType} (hwf : Validation.CedarType.WellFormed env ty) : Validation.CedarType.validateWellFormed env ty = Except.ok ()

theorem Cedar.Thm.type_validate_lifted_is_complete {ty : Validation.CedarType} (hlifted : ty.IsLifted) : ty.validateLifted = Except.ok ()

theorem Cedar.Thm.standard_schema_entry_validate_well_formed_is_complete {env : Validation.TypeEnv} {entry : Validation.StandardSchemaEntry} (hwf : Validation.StandardSchemaEntry.WellFormed env entry) : Validation.StandardSchemaEntry.validateWellFormed env entry = Except.ok ()

theorem Cedar.Thm.entity_schema_entry_validate_well_formed_is_complete {env : Validation.TypeEnv} {entry : Validation.EntitySchemaEntry} (hwf : Validation.EntitySchemaEntry.WellFormed env entry) : Validation.EntitySchemaEntry.validateWellFormed env entry = Except.ok ()

theorem Cedar.Thm.entity_schema_validate_well_formed_is_complete {env : Validation.TypeEnv} {ets : Validation.EntitySchema} (hwf : Validation.EntitySchema.WellFormed env ets) : Validation.EntitySchema.validateWellFormed env ets = Except.ok ()

theorem Cedar.Thm.action_schema_entry_validate_well_formed_is_complete {env : Validation.TypeEnv} {entry : Validation.ActionSchemaEntry} (hwf : Validation.ActionSchemaEntry.WellFormed env entry) : Validation.ActionSchemaEntry.validateWellFormed env entry = Except.ok ()

theorem Cedar.Thm.action_schema_validate_acyclic_action_hierarchy_is_complete {acts : Validation.ActionSchema} (hmap : Data.Map.WellFormed acts) (hacyclic : acts.AcyclicActionHierarchy) : acts.validateAcyclicActionHierarchy = Except.ok ()

theorem Cedar.Thm.action_schema_validate_transitive_action_hierarchy_is_complete {acts : Validation.ActionSchema} (hmap : Data.Map.WellFormed acts) (htransitive : acts.TransitiveActionHierarchy) : acts.validateTransitiveActionHierarchy = Except.ok ()

theorem Cedar.Thm.action_schema_validate_well_formed_is_complete {env : Validation.TypeEnv} {acts : Validation.ActionSchema} (hwf : Validation.ActionSchema.WellFormed env acts) : Validation.ActionSchema.validateWellFormed env acts = Except.ok ()

theorem Cedar.Thm.request_type_validate_well_formed_is_complete {env : Validation.TypeEnv} {reqty : Validation.RequestType} (hwf : Validation.RequestType.WellFormed env reqty) : Validation.RequestType.validateWellFormed env reqty = Except.ok ()

theorem Cedar.Thm.env_validate_well_formed_is_complete {env : Validation.TypeEnv} (hwf : env.WellFormed) : env.validateWellFormed = Except.ok ()

theorem Cedar.Thm.mem_environments {schema : Validation.Schema} {env : Validation.TypeEnv} (h : env ∈ schema.environments) : env.ets = schema.ets ∧ env.acts = schema.acts ∧ ∃ (entry : Validation.ActionSchemaEntry), (env.reqty.action, entry) ∈ Data.Map.toList schema.acts ∧ env.reqty.principal ∈ entry.appliesToPrincipal ∧ env.reqty.resource ∈ entry.appliesToResource ∧ env.reqty.context = entry.context

Every environment of a schema has the schema's maps and the request type of one of its actions.

theorem Cedar.Thm.schema_validate_well_formed_is_complete {schema : Validation.Schema} (hwf : ∀ (env : Validation.TypeEnv), env ∈ schema.environments → Validation.EntitySchema.WellFormed env env.ets ∧ Validation.ActionSchema.WellFormed env env.acts) : schema.validateWellFormed = Except.ok ()

A schema passes the well-formedness check when its maps are well-formed in each of its environments.