This file contains some simple lemmas about the checkLevel and typedAtLevel
functions that do not need reason about the slicing functions.
Equations
Instances For
- var {env : TypeEnv} (v : Spec.Var) (ty : CedarType) (n nmax : Nat) (path : List Spec.Attr) : EntityAccessAtLevel env (TypedExpr.var v ty) n nmax path
- action {env : TypeEnv} (ty : CedarType) (n nmax : Nat) (path : List Spec.Attr) : EntityAccessAtLevel env (lit (Spec.Prim.entityUID env.reqty.action) ty) n nmax path
- ite {env : TypeEnv} (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n nmax : Nat) (path : List Spec.Attr) (hl₁ : AtLevel env tx₁ nmax) (hl₂ : EntityAccessAtLevel env tx₂ n nmax path) (hl₃ : EntityAccessAtLevel env tx₃ n nmax path) : EntityAccessAtLevel env (tx₁.ite tx₂ tx₃ ty) n nmax path
- getTag {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n nmax : Nat) (path : List Spec.Attr) (hl₁ : EntityAccessAtLevel env tx₁ n nmax []) (hl₂ : AtLevel env tx₂ nmax) : EntityAccessAtLevel env (binaryApp Spec.BinaryOp.getTag tx₁ tx₂ ty) (n + 1) nmax path
- getAttr {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) (ety : Spec.EntityType) (n nmax : Nat) {path : List Spec.Attr} (hl₁ : EntityAccessAtLevel env tx₁ n nmax []) (hty : tx₁.typeOf = CedarType.entity ety) : EntityAccessAtLevel env (tx₁.getAttr a ty) (n + 1) nmax path
- getAttrRecord {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) (n nmax : Nat) {path : List Spec.Attr} (hl₁ : EntityAccessAtLevel env tx₁ n nmax (a :: path)) (hty : ∀ (ety : Spec.EntityType), tx₁.typeOf ≠ CedarType.entity ety) : EntityAccessAtLevel env (tx₁.getAttr a ty) n nmax path
- record {env : TypeEnv} {tx : TypedExpr} (attrs : List (Spec.Attr × TypedExpr)) (ty : CedarType) (n nmax : Nat) {a : Spec.Attr} {path : List Spec.Attr} (hl₁ : ∀ (atx : Spec.Attr × TypedExpr), atx ∈ attrs → AtLevel env atx.snd nmax) (hf : (Data.Map.make attrs).find? a = some tx) (hl₂ : EntityAccessAtLevel env tx n nmax path) : EntityAccessAtLevel env (TypedExpr.record attrs ty) n nmax (a :: path)
Instances For
- lit {env : TypeEnv} (p : Spec.Prim) (ty : CedarType) (n : Nat) : AtLevel env (TypedExpr.lit p ty) n
- var {env : TypeEnv} (v : Spec.Var) (ty : CedarType) (n : Nat) : AtLevel env (TypedExpr.var v ty) n
- ite {env : TypeEnv} (tx₁ tx₂ tx₃ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) (hl₂ : AtLevel env tx₂ n) (hl₃ : AtLevel env tx₃ n) : AtLevel env (tx₁.ite tx₂ tx₃ ty) n
- and {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) (hl₂ : AtLevel env tx₂ n) : AtLevel env (tx₁.and tx₂ ty) n
- or {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) (hl₂ : AtLevel env tx₂ n) : AtLevel env (tx₁.or tx₂ ty) n
- unaryApp {env : TypeEnv} (op : Spec.UnaryOp) (tx₁ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) : AtLevel env (TypedExpr.unaryApp op tx₁ ty) n
- mem {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : EntityAccessAtLevel env tx₁ n (n + 1) []) (hl₂ : AtLevel env tx₂ (n + 1)) : AtLevel env (TypedExpr.binaryApp Spec.BinaryOp.mem tx₁ tx₂ ty) (n + 1)
- getTag {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : EntityAccessAtLevel env tx₁ n (n + 1) []) (hl₂ : AtLevel env tx₂ (n + 1)) : AtLevel env (TypedExpr.binaryApp Spec.BinaryOp.getTag tx₁ tx₂ ty) (n + 1)
- hasTag {env : TypeEnv} (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hl₁ : EntityAccessAtLevel env tx₁ n (n + 1) []) (hl₂ : AtLevel env tx₂ (n + 1)) : AtLevel env (TypedExpr.binaryApp Spec.BinaryOp.hasTag tx₁ tx₂ ty) (n + 1)
- binaryApp {env : TypeEnv} (op : Spec.BinaryOp) (tx₁ tx₂ : TypedExpr) (ty : CedarType) (n : Nat) (hop : ¬Thm.DereferencingBinaryOp op) (hl₁ : AtLevel env tx₁ n) (hl₂ : AtLevel env tx₂ n) : AtLevel env (TypedExpr.binaryApp op tx₁ tx₂ ty) n
- getAttr {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) {ety : Spec.EntityType} (n : Nat) (hl₁ : EntityAccessAtLevel env tx₁ n (n + 1) []) (hty : tx₁.typeOf = CedarType.entity ety) : AtLevel env (tx₁.getAttr a ty) (n + 1)
- hasAttr {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) {ety : Spec.EntityType} (n : Nat) (hl₁ : EntityAccessAtLevel env tx₁ n (n + 1) []) (hty : tx₁.typeOf = CedarType.entity ety) : AtLevel env (tx₁.hasAttr a ty) (n + 1)
- getAttrRecord {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) (hty : ∀ (ety : Spec.EntityType), tx₁.typeOf ≠ CedarType.entity ety) : AtLevel env (tx₁.getAttr a ty) n
- hasAttrRecord {env : TypeEnv} (tx₁ : TypedExpr) (a : Spec.Attr) (ty : CedarType) (n : Nat) (hl₁ : AtLevel env tx₁ n) (hty : ∀ (ety : Spec.EntityType), tx₁.typeOf ≠ CedarType.entity ety) : AtLevel env (tx₁.hasAttr a ty) n
- set {env : TypeEnv} (txs : List TypedExpr) (ty : CedarType) (n : Nat) (hl : ∀ (tx : TypedExpr), tx ∈ txs → AtLevel env tx n) : AtLevel env (TypedExpr.set txs ty) n
- record {env : TypeEnv} (attrs : List (Spec.Attr × TypedExpr)) (ty : CedarType) (n : Nat) (hl : ∀ (atx : Spec.Attr × TypedExpr), atx ∈ attrs → AtLevel env atx.snd n) : AtLevel env (TypedExpr.record attrs ty) n
- call {env : TypeEnv} (xfn : Spec.ExtFun) (args : List TypedExpr) (ty : CedarType) (n : Nat) (hl : ∀ (tx : TypedExpr), tx ∈ args → AtLevel env tx n) : AtLevel env (TypedExpr.call xfn args ty) n
Instances For
@[irreducible]
theorem
Cedar.Thm.entity_access_at_level_succ
{path : List Spec.Attr}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{n n' : Nat}
(h₁ : Validation.TypedExpr.EntityAccessAtLevel env tx n n' path)
:
Validation.TypedExpr.EntityAccessAtLevel env tx (n + 1) n' path
@[irreducible]
theorem
Cedar.Thm.entity_access_at_level_then_at_level
{tx : Validation.TypedExpr}
{n : Nat}
{env : Validation.TypeEnv}
{path : List Spec.Attr}
(h₁ : Validation.TypedExpr.EntityAccessAtLevel env tx n (n + 1) path)
:
Validation.TypedExpr.AtLevel env tx (n + 1)
@[irreducible]
theorem
Cedar.Thm.entity_access_level_spec
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{n nmax : Nat}
{path : List Spec.Attr}
:
Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path ↔ tx.checkEntityAccessLevel env n nmax path = true
@[irreducible]