Cedar.Thm.Validation.Levels.CheckLevel

This file contains some simple lemmas about the checkLevel and typedAtLevel functions that do not need reason about the slicing functions.

source

def Cedar.Thm.DereferencingBinaryOp :

Spec.BinaryOp → Prop

Equations

Instances For

source

inductive Cedar.Validation.TypedExpr.EntityAccessAtLevel (env : TypeEnv) :

TypedExpr → Nat → Nat → List Spec.Attr → Prop

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

source

inductive Cedar.Validation.TypedExpr.AtLevel (env : TypeEnv) :

TypedExpr → Nat → Prop

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

source

@[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

source

@[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)

source

@[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

source

@[irreducible]

theorem Cedar.Thm.level_spec {tx : Validation.TypedExpr} {env : Validation.TypeEnv} {n : Nat} :

Validation.TypedExpr.AtLevel env tx n ↔ tx.checkLevel env n = true