theorem
Cedar.Thm.has_attr_false_of_absent_in_record_type
{env : Validation.TypeEnv}
{r : Data.Map Spec.Attr Spec.Value}
{rty : Validation.RecordType}
{a : Spec.Attr}
{es : Spec.Entities}
(hinst : InstanceOfType env (Spec.Value.record r) (Validation.CedarType.record rty))
(hnone : Data.Map.find? rty a = none)
:
A record value whose type does not declare an attribute a does not have a.
theorem
Cedar.Thm.has_attr_false_of_absent_in_entity_type
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{uid : Spec.EntityUID}
{rty : Validation.RecordType}
{a : Spec.Attr}
(hwf : InstanceOfWellFormedEnvironment request entities env)
(hattrs : env.ets.attrs? uid.ty = some rty)
(hnone : Data.Map.find? rty a = none)
:
Spec.hasAttr (Spec.Value.prim (Spec.Prim.entityUID uid)) a entities = Except.ok (Spec.Value.prim (Spec.Prim.bool false))
If the schema does not declare an attribute a for an entity, then it does not have a.
theorem
Cedar.Thm.try_decide_has_residual_sound
{env : Validation.TypeEnv}
{r₁ : Spec.Residual}
{req : Spec.Request}
{es : Spec.Entities}
{attr : Spec.Attr}
{v : Spec.Value}
(hwf : InstanceOfWellFormedEnvironment req es env)
(hwt : Residual.WellTyped env r₁)
(hdec : TPE.tryDecideHasResidual env r₁ attr = some v)
:
If tryDecideHasResidual decides a has expression from the operand's type,
then concrete evaluation agrees.
theorem
Cedar.Thm.partial_evaluate_is_sound_has_attr
{env : Validation.TypeEnv}
{x₁ : Spec.Residual}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{attr : Spec.Attr}
(h₂ : InstanceOfWellFormedEnvironment req es env)
(hwt : Residual.WellTyped env x₁)
(h₄ : RequestAndEntitiesRefine req es preq pes)
(hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate env x₁ preq pes).evaluate req es))
:
Except.toOption ((x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)).evaluate req es) = Except.toOption
((TPE.evaluate env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool)) preq pes).evaluate req
es)