@[irreducible]
theorem
Cedar.Thm.reachable_attr_step
{n : Nat}
{euid euid' : Spec.EntityUID}
{start : Data.Set Spec.EntityUID}
{entities : Spec.Entities}
{ed : Spec.EntityData}
{path : List Spec.Attr}
(hr : ReachableIn entities start euid n)
(he₁ : Data.Map.find? entities euid = some ed)
(he₂ : Value.EuidViaPath (Spec.Value.record ed.attrs) path euid')
:
ReachableIn entities start euid' (n + 1)
theorem
Cedar.Thm.checked_eval_entity_reachable_get_attr
{request : Spec.Request}
{a : Spec.Attr}
{nmax : Nat}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e : 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 (e.getAttr a) c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path)
(he : Spec.evaluate (e.getAttr a) request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
(hf : Data.Map.contains entities euid = true)
(ih : CheckedEvalEntityReachable e)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)