theorem
Cedar.Thm.typed_record_contains_typed_attrs
{tx : Validation.TypedExpr}
{rxs : List (Spec.Attr × Spec.Expr)}
{a : Spec.Attr}
{x : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
(ht : Validation.typeOf (Spec.Expr.record rxs) c env = Except.ok (tx, c'))
(hx : (Data.Map.make rxs).find? a = some x)
:
theorem
Cedar.Thm.record_entity_access_implies_attr_entity_access
{env : Validation.TypeEnv}
{atx : Validation.TypedExpr}
{rtxs : List (Spec.Attr × Validation.TypedExpr)}
{ty : Validation.CedarType}
{n nmax : Nat}
{a : Spec.Attr}
{path : List Spec.Attr}
(hl : Validation.TypedExpr.EntityAccessAtLevel env (Validation.TypedExpr.record rtxs ty) n nmax (a :: path))
(hatx : (Data.Map.make rtxs).find? a = some atx)
:
Validation.TypedExpr.EntityAccessAtLevel env atx n nmax path
theorem
Cedar.Thm.checked_eval_entity_reachable_record
{request : Spec.Request}
{nmax : Nat}
{v : Spec.Value}
{euid : Spec.EntityUID}
{rxs : List (Spec.Attr × Spec.Expr)}
{n : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{entities : Spec.Entities}
{path : List Spec.Attr}
(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.EntityAccessAtLevel env tx n nmax path)
(he : Spec.evaluate (Spec.Expr.record rxs) request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
(hf : Data.Map.contains entities euid = true)
(ih : ∀ (a : Spec.Attr) (x : Spec.Expr), (Data.Map.make rxs).find? a = some x → CheckedEvalEntityReachable x)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)