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
@[irreducible]
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)
:
@[irreducible]
theorem
Cedar.Thm.type_validate_well_formed_is_sound
{env : Validation.TypeEnv}
{ty : Validation.CedarType}
(hok : Validation.CedarType.validateWellFormed env ty = Except.ok ())
:
@[irreducible]
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 ())
:
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 ())
:
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 ())
:
theorem
Cedar.Thm.action_schema_validate_transitive_action_hierarchy_is_sound
{acts : Validation.ActionSchema}
(hok : acts.validateTransitiveActionHierarchy = Except.ok ())
:
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