This file proves that level checking for .binaryApp expressions is sound.
theorem
Cedar.Thm.not_dereferencing_apply₂_invariant_entities
{op : Spec.BinaryOp}
{entities entities' : Spec.Entities}
{v₁ v₂ : Spec.Value}
(hop : ¬DereferencingBinaryOp op)
:
theorem
Cedar.Thm.level_based_slicing_is_sound_inₑ
{request : Spec.Request}
{env : Validation.TypeEnv}
{tx₁ : Validation.TypedExpr}
{e₁ : Spec.Expr}
{euid₁ euid₂ : Spec.EntityUID}
{n : Nat}
{c₀ c₁ : Validation.Capabilities}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c₀ request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf e₁ c₀ env = Except.ok (tx₁, c₁))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx₁ n (n + 1) [])
(he : Spec.evaluate e₁ request entities = Except.ok (Spec.Value.prim (Spec.Prim.entityUID euid₁)))
:
theorem
Cedar.Thm.level_based_slicing_is_sound_binary_app
{tx : Validation.TypedExpr}
{op : Spec.BinaryOp}
{e₁ e₂ : Spec.Expr}
{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 (Spec.Expr.binaryApp op e₁ e₂) c₀ env = Except.ok (tx, c₁))
(hl : Validation.TypedExpr.AtLevel env tx n)
(ihe₁ : TypedAtLevelIsSound e₁)
(ihe₂ : TypedAtLevelIsSound e₂)
:
Spec.evaluate (Spec.Expr.binaryApp op e₁ e₂) request entities = Spec.evaluate (Spec.Expr.binaryApp op e₁ e₂) request (entities.sliceAtLevel request n)