This file proves that level checking for .hasAttr expressions is sound.
theorem
Cedar.Thm.level_based_slicing_is_sound_has_attr_entity
{ety : Spec.EntityType}
{e : Spec.Expr}
{tx₁ : Validation.TypedExpr}
{ty : Validation.CedarType}
{a : Spec.Attr}
{n : Nat}
{c₀ c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c₀ request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(hl : Validation.TypedExpr.AtLevel env (tx₁.hasAttr a ty) n)
(ht : Validation.typeOf e c₀ env = Except.ok (tx₁, c₁))
(hety : tx₁.typeOf = Validation.CedarType.entity ety)
(ihe : TypedAtLevelIsSound e)
:
Spec.evaluate (e.hasAttr a) request entities = Spec.evaluate (e.hasAttr a) request (entities.sliceAtLevel request n)
theorem
Cedar.Thm.level_based_slicing_is_sound_has_attr_record
{ty : Validation.CedarType}
{c₁' : Validation.Capabilities}
{rty : Data.Map Spec.Attr (Validation.Qualified Validation.CedarType)}
{e : Spec.Expr}
{tx : Validation.TypedExpr}
{a : Spec.Attr}
{n : Nat}
{c₀ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c₀ request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(hl : Validation.TypedExpr.AtLevel env (tx.hasAttr a ty) n)
(htx : Validation.typeOf e c₀ env = Except.ok (tx, c₁'))
(hrty : tx.typeOf = Validation.CedarType.record rty)
(ihe : TypedAtLevelIsSound e)
:
Spec.evaluate (e.hasAttr a) request entities = Spec.evaluate (e.hasAttr a) request (entities.sliceAtLevel request n)
theorem
Cedar.Thm.level_based_slicing_is_sound_has_attr
{e : Spec.Expr}
{tx : Validation.TypedExpr}
{a : Spec.Attr}
{n : Nat}
{c₀ c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c₀ request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf (e.hasAttr a) c₀ env = Except.ok (tx, c₁))
(hl : Validation.TypedExpr.AtLevel env tx n)
(ihe : TypedAtLevelIsSound e)
:
Spec.evaluate (e.hasAttr a) request entities = Spec.evaluate (e.hasAttr a) request (entities.sliceAtLevel request n)