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
@[irreducible]
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)
(hf : Data.Map.contains entities euid = true)
:
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)
:
@[irreducible]
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.