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.schema = 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
theorem
Cedar.Thm.instance_of_type_refl
{v : Spec.Value}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
:
Validation.instanceOfType v ty env.schema = 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
theorem
Cedar.Thm.instanceOfType_mono
{s₁ s₂ : Validation.Schema}
(hmono :
∀ (e : Spec.EntityUID) (ety : Spec.EntityType),
Validation.instanceOfEntityType e ety s₁ = true → Validation.instanceOfEntityType e ety s₂ = true)
(v : Spec.Value)
(ty : Validation.CedarType)
(h : Validation.instanceOfType v ty s₁ = true)
:
instanceOfType depends on its schema only through instanceOfEntityType.
theorem
Cedar.Thm.instanceOfType_record_contains
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{schema : Validation.Schema}
{a : Spec.Attr}
(h : Validation.instanceOfType (Spec.Value.record r) (Validation.CedarType.record rty) schema = true)
(ha : r.contains a = true)
:
A record valid against a record type has only attributes of that type.
theorem
Cedar.Thm.instanceOfType_record_required
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{schema : Validation.Schema}
{a : Spec.Attr}
{ty : Validation.CedarType}
(h : Validation.instanceOfType (Spec.Value.record r) (Validation.CedarType.record rty) schema = true)
(hrequired : Data.Map.find? rty a = some (Validation.Qualified.required ty))
:
A record valid against a record type has each required attribute of that type.
theorem
Cedar.Thm.instanceOfEntitySchemaEntry_mono
{env₁ env₂ : Validation.TypeEnv}
{uid : Spec.EntityUID}
{data : Spec.EntityData}
{entry : Validation.EntitySchemaEntry}
(h : Validation.instanceOfSchema.instanceOfEntitySchemaEntry env₁ uid data entry = Except.ok ())
(hmono :
∀ (e : Spec.EntityUID) (ety : Spec.EntityType),
Validation.instanceOfEntityType e ety env₁.schema = true → Validation.instanceOfEntityType e ety env₂.schema = true)
:
Entity-entry validation depends on its schema only through instanceOfEntityType.
theorem
Cedar.Thm.instanceOfActionSchemaEntry_mono
{env₁ env₂ : Validation.TypeEnv}
{uid : Spec.EntityUID}
{data : Spec.EntityData}
(h : Validation.instanceOfSchema.instanceOfActionSchemaEntry env₁ uid data = Except.ok ())
(hacts :
∀ (entry : Validation.ActionSchemaEntry),
Data.Map.find? env₁.acts uid = some entry →
∃ (entry' : Validation.ActionSchemaEntry), Data.Map.find? env₂.acts uid = some entry' ∧ entry'.ancestors = entry.ancestors)
:
Action-entry validation depends on its schema only through the action's ancestors.
theorem
Cedar.Thm.instanceOfActionSchemaEntry_find?
{env : Validation.TypeEnv}
{uid : Spec.EntityUID}
{data : Spec.EntityData}
(h : Validation.instanceOfSchema.instanceOfActionSchemaEntry env uid data = Except.ok ())
:
A valid action entity is an action of the schema.
theorem
Cedar.Thm.instanceOfSchemaEntry_eq
{env₁ env₂ : Validation.TypeEnv}
(hets : env₁.ets = env₂.ets)
(hacts : env₁.acts = env₂.acts)
:
Validating an entity depends on the environment only through its entity and action schemas.
theorem
Cedar.Thm.instanceOfSchemaEntry_attrs
{env : Validation.TypeEnv}
{uid : Spec.EntityUID}
{data : Spec.EntityData}
{entry : Validation.EntitySchemaEntry}
(h : Validation.instanceOfSchema.instanceOfSchemaEntry env uid data = Except.ok ())
(hfind : Data.Map.find? env.ets uid.ty = some entry)
:
Validation.instanceOfType (Spec.Value.record data.attrs) (Validation.CedarType.record entry.attrs) env.schema = true
A valid entity of a type the schema declares has attributes of that type.
theorem
Cedar.Thm.instanceOfSchemaEntry_actionEntity
{env : Validation.TypeEnv}
{uid : Spec.EntityUID}
{entry : Validation.ActionSchemaEntry}
(hwf : env.WellFormed)
(hmem : (uid, entry) ∈ Data.Map.toList env.acts)
:
In a well-formed environment, the entity of each action is valid.