This file contains theorems about partial evaluation preserving well-typedness of residuals.
@[reducible, inline]
abbrev
Cedar.Thm.PEWellTyped
(env : Validation.TypeEnv)
(r₁ r₂ : Spec.Residual)
(req : Spec.Request)
(preq : TPE.PartialRequest)
(es : Spec.Entities)
(pes : TPE.PartialEntities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.entity_data_from_partial
{env : Validation.TypeEnv}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid : Spec.EntityUID}
{pe : TPE.PartialEntityData}
:
InstanceOfWellFormedEnvironment req es env →
EntitiesRefine es pes →
Data.Map.find? pes uid = some pe →
∃ (edata : Spec.EntityData), Data.Map.find? es uid = some edata ∧ PartialIsValid (fun (x : Data.Map Spec.Attr Spec.Value) => x = edata.attrs) pe.attrs ∧ PartialIsValid (fun (x : Data.Set Spec.EntityUID) => x = edata.ancestors) pe.ancestors ∧ PartialIsValid (fun (x : Data.Map Spec.Tag Spec.Value) => x = edata.tags) pe.tags ∧ InstanceOfSchemaEntry uid edata env