Facts about Entities.ValidRefsFor.
@[reducible, inline]
abbrev
Cedar.Thm.typeOf_preserves_valid_refs_ih
(Γ : Validation.TypeEnv)
(entities : Spec.Entities)
(e : Spec.Expr)
:
Shorthand form of inductive hypotheses used in the following proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.typeOf_preserves_valid_refs_lit
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{p : Spec.Prim}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.lit p) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.lit p))
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_var
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{var : Spec.Var}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.var var) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.var var))
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_and
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{e₁ e₂ : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (e₁.and e₂) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (e₁.and e₂))
(ih₁ : typeOf_preserves_valid_refs_ih Γ entities e₁)
(ih₂ : typeOf_preserves_valid_refs_ih Γ entities e₂)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_or
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{e₁ e₂ : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (e₁.or e₂) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (e₁.or e₂))
(ih₁ : typeOf_preserves_valid_refs_ih Γ entities e₁)
(ih₂ : typeOf_preserves_valid_refs_ih Γ entities e₂)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_ite
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{e₁ e₂ e₃ : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (e₁.ite e₂ e₃) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (e₁.ite e₂ e₃))
(ih₁ : typeOf_preserves_valid_refs_ih Γ entities e₁)
(ih₂ : typeOf_preserves_valid_refs_ih Γ entities e₂)
(ih₃ : typeOf_preserves_valid_refs_ih Γ entities e₃)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_unaryApp
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{op : Spec.UnaryOp}
{e : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.unaryApp op e) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.unaryApp op e))
(ih : typeOf_preserves_valid_refs_ih Γ entities e)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_binaryApp
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{op : Spec.BinaryOp}
{e₁ e₂ : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.binaryApp op e₁ e₂) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.binaryApp op e₁ e₂))
(ih₁ : typeOf_preserves_valid_refs_ih Γ entities e₁)
(ih₂ : typeOf_preserves_valid_refs_ih Γ entities e₂)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_getAttr
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{e : Spec.Expr}
{attr : Spec.Attr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (e.getAttr attr) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (e.getAttr attr))
(ih : typeOf_preserves_valid_refs_ih Γ entities e)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_hasAttr
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{e : Spec.Expr}
{attr : Spec.Attr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (e.hasAttr attr) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (e.hasAttr attr))
(ih : typeOf_preserves_valid_refs_ih Γ entities e)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_set
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{s : List Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.set s) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.set s))
(ih_xs : ∀ (x : Spec.Expr), x ∈ s → typeOf_preserves_valid_refs_ih Γ entities x)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_call
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{xfn : Spec.ExtFun}
{args : List Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.call xfn args) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.call xfn args))
(ih_args : ∀ (arg : Spec.Expr), arg ∈ args → typeOf_preserves_valid_refs_ih Γ entities arg)
:
entities.ValidRefsFor tx.toExpr
theorem
Cedar.Thm.typeOf_preserves_valid_refs_record
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{rec : List (Spec.Attr × Spec.Expr)}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf (Spec.Expr.record rec) c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor (Spec.Expr.record rec))
(ih_rec : ∀ (attr : Spec.Attr × Spec.Expr), attr ∈ rec → typeOf_preserves_valid_refs_ih Γ entities attr.snd)
:
entities.ValidRefsFor tx.toExpr
@[irreducible]
theorem
Cedar.Thm.typeOf_preserves_valid_refs
{Γ : Validation.TypeEnv}
(entities : Spec.Entities)
{expr : Spec.Expr}
{tx : Validation.TypedExpr}
{c₁ c₂ : Validation.Capabilities}
(hty : Validation.typeOf expr c₁ Γ = Except.ok (tx, c₂))
(hrefs : entities.ValidRefsFor expr)
:
entities.ValidRefsFor tx.toExpr
typeOf preserves Entities.ValidRefsFor.
The converse is not true, due to policies with
invalid UID literals, such as
// entity User enum ["alice"];
permit(principal, action, resource)
when { if true then User::"alice" else User::"bob" };