theorem
Cedar.Thm.instance_of_bool_type_refl
{b : Bool}
{bty : Validation.BoolType}
:
Validation.instanceOfBoolType b bty = true → InstanceOfBoolType b bty
theorem
Cedar.Thm.instance_of_entity_type_refl
{e : Spec.EntityUID}
{ety : Spec.EntityType}
{env : Validation.TypeEnv}
:
Validation.instanceOfEntityType e ety env = true → InstanceOfEntityType e ety env
theorem
Cedar.Thm.instance_of_ext_type_refl
{ext : Spec.Ext}
{extty : Validation.ExtType}
:
Validation.instanceOfExtType ext extty = true → InstanceOfExtType ext extty
@[irreducible]
theorem
Cedar.Thm.instance_of_type_refl
{v : Spec.Value}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
:
Validation.instanceOfType v ty env = true → InstanceOfType env v ty
theorem
Cedar.Thm.instance_of_request_type_refl
{request : Spec.Request}
{env : Validation.TypeEnv}
:
Validation.instanceOfRequestType request env = true → InstanceOfRequestType request env
theorem
Cedar.Thm.instance_of_schema_refl
{entities : Spec.Entities}
{env : Validation.TypeEnv}
:
Validation.instanceOfSchema entities env = Except.ok () → InstanceOfSchema entities env
theorem
Cedar.Thm.instance_of_well_formed_env
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
:
env.validateWellFormed = Except.ok () →
Validation.requestMatchesEnvironment env request = true →
Validation.entitiesMatchEnvironment env entities = Except.ok () →
InstanceOfWellFormedEnvironment request entities env
theorem
Cedar.Thm.request_and_entities_validate_implies_instance_of_wf_schema
(schema : Validation.Schema)
(request : Spec.Request)
(entities : Spec.Entities)
:
schema.validateWellFormed = Except.ok () →
Validation.validateRequest schema request = Except.ok () →
Validation.validateEntities schema entities = Except.ok () → InstanceOfWellFormedSchema schema request entities