@[irreducible]
theorem
Cedar.Thm.reachable_tag_step
{tv : Spec.Value}
{n : Nat}
{euid euid' : Spec.EntityUID}
{start : Data.Set Spec.EntityUID}
{entities : Spec.Entities}
{ed : Spec.EntityData}
{tag : Spec.Tag}
{path : List Spec.Attr}
(hr : ReachableIn entities start euid n)
(he₁ : Data.Map.find? entities euid = some ed)
(he₂ : ed.tags.find? tag = some tv)
(he₃ : Value.EuidViaPath tv path euid')
:
ReachableIn entities start euid' (n + 1)
theorem
Cedar.Thm.checked_eval_entity_reachable_get_tag
{request : Spec.Request}
{nmax : Nat}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e₁ 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 (Spec.Expr.binaryApp Spec.BinaryOp.getTag e₁ e₂) c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path)
(he : Spec.evaluate (Spec.Expr.binaryApp Spec.BinaryOp.getTag e₁ e₂) request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
(ih₁ : CheckedEvalEntityReachable e₁)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)
theorem
Cedar.Thm.binary_op_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{op : Spec.BinaryOp}
{e₁ e₂ : Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(hop : op ≠ Spec.BinaryOp.getTag)
(he : Spec.evaluate (Spec.Expr.binaryApp op e₁ e₂) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.checked_eval_entity_reachable_binary
{request : Spec.Request}
{nmax : Nat}
{v : Spec.Value}
{euid : Spec.EntityUID}
{op : Spec.BinaryOp}
{e₁ 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 (Spec.Expr.binaryApp op e₁ e₂) c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path)
(he : Spec.evaluate (Spec.Expr.binaryApp op e₁ e₂) request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
(ih₁ : CheckedEvalEntityReachable e₁)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)