theorem
Cedar.Thm.checked_eval_entity_lit_is_action
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{p : Spec.Prim}
{n nmax : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{entities : Spec.Entities}
{path : List Spec.Attr}
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf (Spec.Expr.lit p) c env = Except.ok (tx, c'))
(he : Spec.evaluate (Spec.Expr.lit p) request entities = Except.ok v)
(hel : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path)
(ha : Value.EuidViaPath v path euid)
:
theorem
Cedar.Thm.and_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e₁ e₂ : Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (e₁.and e₂) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.or_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e₁ e₂ : Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (e₁.or e₂) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.unary_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{op : Spec.UnaryOp}
{e₁ : Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (Spec.Expr.unaryApp op e₁) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.has_attr_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e₁ : Spec.Expr}
{a : Spec.Attr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (e₁.hasAttr a) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.set_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{xs : List Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (Spec.Expr.set xs) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.call_not_euid_via_path
{request : Spec.Request}
{v : Spec.Value}
{euid : Spec.EntityUID}
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{entities : Spec.Entities}
{path : List Spec.Attr}
(he : Spec.evaluate (Spec.Expr.call xfn xs) request entities = Except.ok v)
:
¬Value.EuidViaPath v path euid
theorem
Cedar.Thm.checked_eval_entity_reachable
{e : Spec.Expr}
{n nmax : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{v : Spec.Value}
{path : List Spec.Attr}
{euid : Spec.EntityUID}
(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 nmax path)
(he : Spec.evaluate e request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)
If an expression checks at level n and then evaluates an entity (or a record
containing an entity), then that entity must reachable in n + 1 steps.
theorem
Cedar.Thm.in_work_then_in_slice
{entities : Spec.Entities}
{work : Data.Set Spec.EntityUID}
{euid : Spec.EntityUID}
{n : Nat}
(hw : euid ∈ work)
:
theorem
Cedar.Thm.slice_contains_reachable
{n : Nat}
{work : Data.Set Spec.EntityUID}
{euid : Spec.EntityUID}
{entities : Spec.Entities}
(hw : ReachableIn entities work euid (n + 1))
:
If an entity is reachable in n steps, then it must be included in slice at
n. This lemma talks about the inner slicing function, so it's possible that
the entity isn't in the original entities if it's in work.
theorem
Cedar.Thm.reachable_of_mem_slice
{n : Nat}
{work : Data.Set Spec.EntityUID}
{euid : Spec.EntityUID}
{entities : Spec.Entities}
(h : euid ∈ Spec.Entities.sliceAtLevel.sliceAtLevel entities work n)
:
ReachableIn entities work euid n
Converse of slice_contains_reachable: every entity in the level-n slice (the
reachable set computed by Entities.sliceAtLevel) is reachable in n steps.
Together with reachable_then_mem_slice this gives euid ∈ slice ↔ ReachableIn,
the bridge that makes Entities.closedAtLevel decide EntitiesClosedAtLevel.
theorem
Cedar.Thm.reachable_then_mem_slice
{n : Nat}
{work : Data.Set Spec.EntityUID}
{euid : Spec.EntityUID}
{entities : Spec.Entities}
(hr : ReachableIn entities work euid n)
:
ReachableIn at any level implies membership in the level-n slice. Wraps
slice_contains_reachable (the n + 1 case); n = 0 is vacuous since
ReachableIn _ _ _ 0 is uninhabited.