This file proves that level checking for .record expressions is sound.
theorem
Cedar.Thm.level_based_slicing_is_sound_record_attrs
{atxs : List (Spec.Attr × Validation.TypedExpr)}
{rxs : List (Spec.Attr × Spec.Expr)}
{n : Nat}
{c : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : List.Forall₂ (AttrExprHasAttrType c env) rxs atxs)
(hl : ∀ (atx : Spec.Attr × Validation.TypedExpr), atx ∈ atxs → Validation.TypedExpr.AtLevel env atx.snd n)
(ih : ∀ (x : Spec.Attr × Spec.Expr), x ∈ rxs → TypedAtLevelIsSound x.snd)
:
(rxs.mapM₂ fun (x : { x : Spec.Attr × Spec.Expr // sizeOf x.snd < 1 + sizeOf rxs }) => do
let v ← Spec.evaluate x.val.snd request entities
Except.ok (x.val.fst, v)) = rxs.mapM₂ fun (x : { x : Spec.Attr × Spec.Expr // sizeOf x.snd < 1 + sizeOf rxs }) => do
let v ← Spec.evaluate x.val.snd request (entities.sliceAtLevel request n)
Except.ok (x.val.fst, v)
theorem
Cedar.Thm.level_based_slicing_is_sound_record
{tx : Validation.TypedExpr}
{rxs : List (Spec.Attr × 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.record rxs) c₀ env = Except.ok (tx, c₁))
(hl : Validation.TypedExpr.AtLevel env tx n)
(ih : ∀ (x : Spec.Attr × Spec.Expr), x ∈ rxs → TypedAtLevelIsSound x.snd)
:
Spec.evaluate (Spec.Expr.record rxs) request entities = Spec.evaluate (Spec.Expr.record rxs) request (entities.sliceAtLevel request n)