theorem Cedar.Validation.PartialSchema.validateEntities_ok_iff {ps : PartialSchema} {entities : Spec.Entities} : ps.validateEntities entities = Except.ok () ↔ ∀ (uid : Spec.EntityUID) (data : Spec.EntityData), (uid, data) ∈ Data.Map.toList entities → (∀ (ancestors : Data.Set Spec.EntityType), Data.Map.find? ps.ets uid.ty ≠ some (PartialEntitySchemaEntry.external ancestors)) ∧ instanceOfSchema.instanceOfSchemaEntry ps.wfEnv uid data = Except.ok ()

Partial entity validation accepts a store exactly when no entity has an external type and every entity is valid in wfEnv.

theorem Cedar.Validation.entity_reference_validation_soundness {p c t : PartialSchema} {uid : Spec.EntityUID} {ety : Spec.EntityType} (hlink : link p c = Except.ok t) (hvalid : instanceOfEntityType uid ety p.validationView = true) : instanceOfEntityType uid ety t.validationView = true

An entity reference valid against a partial schema remains valid after linking.

theorem Cedar.Validation.value_validation_soundness {p c t : PartialSchema} {v : Spec.Value} {ty : CedarType} (hlink : link p c = Except.ok t) (hvalid : instanceOfType v ty p.validationView = true) : instanceOfType v ty t.validationView = true

A value valid against a partial schema remains valid after linking.

theorem Cedar.Validation.request_environment_soundness {p c t : PartialSchema} {env : TypeEnv} (hp : p.WellFormed) (hlink : link p c = Except.ok t) (henv : env ∈ p.validationView.environments) : { ets := t.validationView.ets, acts := t.validationView.acts, reqty := env.reqty } ∈ t.validationView.environments

Linking keeps every request type of a well-formed partial schema: each request environment of its validation view has a counterpart in the result's.

theorem Cedar.Validation.entity_validation_soundness {p c t : PartialSchema} {entities : Spec.Entities} (hlink : link p c = Except.ok t) (hvalid : p.validateEntities entities = Except.ok ()) : t.validateEntities entities = Except.ok ()

Entities valid against a partial schema remain valid after linking.

theorem Cedar.Validation.request_validation_soundness {p c t : PartialSchema} {request : Spec.Request} (hp : p.WellFormed) (hlink : link p c = Except.ok t) (hvalid : p.validateRequest request = Except.ok ()) : t.validateRequest request = Except.ok ()

Requests valid against a partial schema remain valid after linking.

theorem Cedar.Validation.entity_validation_completeness {p : PartialSchema} {entities : Spec.Entities} (hp : p.WellFormed) (hvalid : ∀ (c t : PartialSchema), c.WellFormed → link p c = Except.ok t → t.asSchema?.isSome = true → t.validateEntities entities = Except.ok ()) : p.validateEntities entities = Except.ok ()

Entities valid against every complete linking extension are valid against the partial schema.

theorem Cedar.Validation.request_validation_completeness {p : PartialSchema} {request : Spec.Request} (hp : p.WellFormed) (hvalid : ∀ (c t : PartialSchema), c.WellFormed → link p c = Except.ok t → t.asSchema?.isSome = true → t.validateRequest request = Except.ok ()) : p.validateRequest request = Except.ok ()

Requests valid against every complete linking extension are valid against the partial schema.

theorem Cedar.Validation.complete_request_validation_agreement {t : PartialSchema} {schema : Schema} {request : Spec.Request} (hcomplete : t.asSchema? = some schema) : t.validateRequest request = validateRequest schema request

A complete partial schema validates requests exactly as the schema completing it.

theorem Cedar.Validation.complete_entity_validation_agreement {p c t : PartialSchema} {schema : Schema} {entities : Spec.Entities} (hp : p.WellFormed) (hc : c.WellFormed) (hlink : link p c = Except.ok t) (hcomplete : t.asSchema? = some schema) (hvalid : t.validateEntities entities = Except.ok ()) : validateEntities schema (entities ++ Data.Map.mapOnValues actionSchemaEntryToEntityData schema.acts) = Except.ok ()

At a complete link, partial entity validation implies complete validation after adding the canonical entity for every action.