theorem
Cedar.Thm.find_lifted_type
{attr : Spec.Attr}
{ty₁ ty₂ : Validation.QualifiedType}
{m : Validation.RecordType}
:
Data.Map.find? m attr = some ty₁ → Data.Map.find? m.liftBoolTypes attr = some ty₂ → ty₂ = ty₁.liftBoolTypes
theorem
Cedar.Thm.attrs_if_partial_attrs
{env : Validation.TypeEnv}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid : Spec.EntityUID}
{m : Data.Map Spec.Attr Spec.Value}
(h_wf : InstanceOfWellFormedEnvironment req es env)
(h_eref : EntitiesRefine es pes)
(h_attrs : pes.attrs uid = some m)
:
theorem
Cedar.Thm.entity_attr_well_typed
{preq : TPE.PartialRequest}
{env : Validation.TypeEnv}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
{uid : Spec.EntityUID}
{ety : Spec.EntityType}
{rty : Validation.RecordType}
{m : Data.Map Spec.Attr Spec.Value}
{attr : Spec.Attr}
{v : Spec.Value}
{ty : Validation.CedarType}
:
InstanceOfWellFormedEnvironment req es env →
RequestAndEntitiesRefine req es preq pes →
InstanceOfEntityType uid ety env →
pes.attrs uid = some m →
m.find? attr = some v →
Option.map Validation.RecordType.liftBoolTypes (env.ets.attrs? ety) = some rty →
Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty → InstanceOfType env v ty
theorem
Cedar.Thm.partial_eval_well_typed_getAttr
{env : Validation.TypeEnv}
{expr : Spec.Residual}
{attr : Spec.Attr}
{ty : Validation.CedarType}
{req : Spec.Request}
{preq : TPE.PartialRequest}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
:
Residual.WellTyped env (TPE.evaluate env expr preq pes) →
PEWellTyped env (expr.getAttr attr ty) (TPE.evaluate env (expr.getAttr attr ty) preq pes) req preq es pes