inductive Cedar.Spec.Residual : Type

• val (v : Value) (ty : Validation.CedarType) : Residual
• var (v : Var) (ty : Validation.CedarType) : Residual
• ite (cond thenExpr elseExpr : Residual) (ty : Validation.CedarType) : Residual
• and (a b : Residual) (ty : Validation.CedarType) : Residual
• or (a b : Residual) (ty : Validation.CedarType) : Residual
• unaryApp (op : UnaryOp) (expr : Residual) (ty : Validation.CedarType) : Residual
• binaryApp (op : BinaryOp) (a b : Residual) (ty : Validation.CedarType) : Residual
• getAttr (expr : Residual) (attr : Attr) (ty : Validation.CedarType) : Residual
• hasAttr (expr : Residual) (attr : Attr) (ty : Validation.CedarType) : Residual
• extHasAttr (expr : Residual) (attr : Attr) (attrs : List Attr) (ty : Validation.CedarType) : Residual
• set (ls : List Residual) (ty : Validation.CedarType) : Residual
• record (map : List (Attr × Residual)) (ty : Validation.CedarType) : Residual
• call (xfn : ExtFun) (args : List Residual) (ty : Validation.CedarType) : Residual
• error (ty : Validation.CedarType) : Residual

@[instance_reducible]

instance Cedar.Spec.instReprResidual : Repr Residual

Equations

• Cedar.Spec.instReprResidual = { reprPrec := Cedar.Spec.instReprResidual.repr }

partial def Cedar.Spec.instReprResidual.repr : Residual → Nat → Std.Format

@[instance_reducible]

instance Cedar.Spec.instInhabitedResidual : Inhabited Residual

Equations

• Cedar.Spec.instInhabitedResidual = { default := Cedar.Spec.instInhabitedResidual.default }

@[instance_reducible]

instance Cedar.Spec.instCoeBoolResidual : Coe Bool Residual

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cedar.Spec.instCoeStringResidual : Coe String Residual

Equations

• Cedar.Spec.instCoeStringResidual = { coe := fun (s : String) => Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)) Cedar.Validation.CedarType.string }

@[instance_reducible]

instance Cedar.Spec.instCoeEntityUIDResidual : Coe EntityUID Residual

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Spec.Residual.asValue : Residual → Option Value

Equations

• (Cedar.Spec.Residual.val v ty).asValue = some v
• x✝.asValue = none

def Cedar.Spec.Value.toResidual (v : Value) (ty : Validation.CedarType) : Residual

Equations

• v.toResidual ty = Cedar.Spec.Residual.val v ty

def Cedar.Spec.Residual.isError : Residual → Bool

Equations

• (Cedar.Spec.Residual.error ty).isError = true
• x✝.isError = false

def Cedar.Spec.Residual.typeOf : Residual → Validation.CedarType

Equations

• (Cedar.Spec.Residual.val a a_1).typeOf = a_1
• (Cedar.Spec.Residual.var a a_1).typeOf = a_1
• (a.ite a_1 a_2 a_3).typeOf = a_3
• (a.and a_1 a_2).typeOf = a_2
• (a.or a_1 a_2).typeOf = a_2
• (Cedar.Spec.Residual.unaryApp a a_1 a_2).typeOf = a_2
• (Cedar.Spec.Residual.binaryApp a a_1 a_2 a_3).typeOf = a_3
• (a.getAttr a_1 a_2).typeOf = a_2
• (a.hasAttr a_1 a_2).typeOf = a_2
• (a.extHasAttr a_1 a_2 a_3).typeOf = a_3
• (Cedar.Spec.Residual.set a a_1).typeOf = a_1
• (Cedar.Spec.Residual.record a a_1).typeOf = a_1
• (Cedar.Spec.Residual.call a a_1 a_2).typeOf = a_2
• (Cedar.Spec.Residual.error a).typeOf = a

def Cedar.Spec.BinaryOp.canError : BinaryOp → Bool

Equations

• Cedar.Spec.BinaryOp.add.canError = true
• Cedar.Spec.BinaryOp.sub.canError = true
• Cedar.Spec.BinaryOp.mul.canError = true
• Cedar.Spec.BinaryOp.getTag.canError = true
• x✝.canError = false

def Cedar.Spec.UnaryOp.canError : UnaryOp → Bool

Equations

• Cedar.Spec.UnaryOp.neg.canError = true
• x✝.canError = false

@[irreducible]

def Cedar.Spec.Residual.errorFree : Residual → Bool

Equations

• (Cedar.Spec.Residual.val v ty).errorFree = true
• (Cedar.Spec.Residual.var v ty).errorFree = true
• (Cedar.Spec.Residual.binaryApp op x₁ x₂ ty).errorFree = (!op.canError && x₁.errorFree && x₂.errorFree)
• (Cedar.Spec.Residual.unaryApp op x₁ ty).errorFree = (!op.canError && x₁.errorFree)
• (x₁.and x₂ ty).errorFree = (x₁.errorFree && x₂.errorFree)
• (x₁.or x₂ ty).errorFree = (x₁.errorFree && x₂.errorFree)
• (x₁.ite x₂ x₃ ty).errorFree = (x₁.errorFree && x₂.errorFree && x₃.errorFree)
• (x₁.hasAttr attr ty).errorFree = x₁.errorFree
• (x₁.extHasAttr attr attrs ty).errorFree = x₁.errorFree
• (Cedar.Spec.Residual.set xs ty).errorFree = xs.attach.all fun (x : { x : Cedar.Spec.Residual // x ∈ xs }) => have this := ⋯; x.val.errorFree
• (Cedar.Spec.Residual.record xs ty).errorFree = xs.attach₂.all fun (ax : { x : Cedar.Spec.Attr × Cedar.Spec.Residual // sizeOf x.snd < 1 + sizeOf xs }) => ax.val.snd.errorFree
• x✝.errorFree = false

@[irreducible]

def Cedar.Spec.Residual.evaluate (x : Residual) (req : Request) (es : Entities) : Result Value

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Spec.Residual.val v ty).evaluate req es = Except.ok v
• (Cedar.Spec.Residual.var Cedar.Spec.Var.principal ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.principal))
• (Cedar.Spec.Residual.var Cedar.Spec.Var.resource ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.resource))
• (Cedar.Spec.Residual.var Cedar.Spec.Var.action ty).evaluate req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.action))
• (Cedar.Spec.Residual.var Cedar.Spec.Var.context ty).evaluate req es = Except.ok (Cedar.Spec.Value.record req.context)
• (c.ite x_2 y ty).evaluate req es = do let c ← c.evaluate req es let b ← c.asBool if b = true then x_2.evaluate req es else y.evaluate req es
• (Cedar.Spec.Residual.unaryApp op e ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.apply₁ op v
• (Cedar.Spec.Residual.binaryApp op x_2 y ty).evaluate req es = do let v₁ ← x_2.evaluate req es let v₂ ← y.evaluate req es Cedar.Spec.apply₂ op v₁ v₂ es
• (e.hasAttr a ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.hasAttr v a es
• (e.extHasAttr a as ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.hasAttrs v a as es
• (e.getAttr a ty).evaluate req es = do let v ← e.evaluate req es Cedar.Spec.getAttr v a es
• (Cedar.Spec.Residual.error ty).evaluate req es = Except.error Cedar.Spec.Error.extensionError

@[irreducible]

def Cedar.Spec.Residual.allLiteralUIDs (x : Residual) : Data.Set EntityUID

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Spec.Residual.val (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)) _ty).allLiteralUIDs = Cedar.Data.Set.singleton uid
• (Cedar.Spec.Residual.val v ty).allLiteralUIDs = Cedar.Data.Set.empty
• (Cedar.Spec.Residual.error _e).allLiteralUIDs = Cedar.Data.Set.empty
• (Cedar.Spec.Residual.var v ty).allLiteralUIDs = Cedar.Data.Set.empty
• (x₁.ite x₂ x₃ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs ∪ x₃.allLiteralUIDs
• (x₁.and x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
• (x₁.or x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
• (Cedar.Spec.Residual.unaryApp op x_2 ty).allLiteralUIDs = x_2.allLiteralUIDs
• (Cedar.Spec.Residual.binaryApp op x₁ x₂ ty).allLiteralUIDs = x₁.allLiteralUIDs ∪ x₂.allLiteralUIDs
• (x_2.getAttr attr ty).allLiteralUIDs = x_2.allLiteralUIDs
• (x_2.hasAttr attr ty).allLiteralUIDs = x_2.allLiteralUIDs
• (x_2.extHasAttr attr attrs ty).allLiteralUIDs = x_2.allLiteralUIDs
• (Cedar.Spec.Residual.set x_2 ty).allLiteralUIDs = x_2.mapUnion₁ fun (x : { x : Cedar.Spec.Residual // x ∈ x_2 }) => match x with | ⟨v, property⟩ => v.allLiteralUIDs
• (Cedar.Spec.Residual.call xfn x_2 ty).allLiteralUIDs = x_2.mapUnion₁ fun (x : { x : Cedar.Spec.Residual // x ∈ x_2 }) => match x with | ⟨v, property⟩ => v.allLiteralUIDs

def Cedar.Spec.decResidual (x y : Residual) : Decidable (x = y)

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Spec.decProdAttrResidualList (axs ays : List (Attr × Residual)) : Decidable (axs = ays)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.decProdAttrResidualList [] [] = isTrue Cedar.Spec.decProdAttrResidualList._proof_1
• Cedar.Spec.decProdAttrResidualList (head :: tail) [] = isFalse ⋯
• Cedar.Spec.decProdAttrResidualList [] (head :: tail) = isFalse ⋯

def Cedar.Spec.decResidualList (xs ys : List Residual) : Decidable (xs = ys)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.decResidualList [] [] = isTrue Cedar.Spec.decResidualList._proof_1
• Cedar.Spec.decResidualList (head :: tail) [] = isFalse ⋯
• Cedar.Spec.decResidualList [] (head :: tail) = isFalse ⋯

@[instance_reducible]

instance Cedar.Spec.instDecidableEqResidual : DecidableEq Residual

Equations

• Cedar.Spec.instDecidableEqResidual = Cedar.Spec.decResidual

@[irreducible]

def Cedar.Validation.TypedExpr.toResidual : TypedExpr → Spec.Residual

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Validation.TypedExpr.lit p ty).toResidual = Cedar.Spec.Residual.val (Cedar.Spec.Value.prim p) ty
• (Cedar.Validation.TypedExpr.var v ty).toResidual = Cedar.Spec.Residual.var v ty
• (x₁.ite x₂ x₃ ty).toResidual = x₁.toResidual.ite x₂.toResidual x₃.toResidual ty
• (a.and b ty).toResidual = a.toResidual.and b.toResidual ty
• (a.or b ty).toResidual = a.toResidual.or b.toResidual ty
• (Cedar.Validation.TypedExpr.unaryApp op expr ty).toResidual = Cedar.Spec.Residual.unaryApp op expr.toResidual ty
• (Cedar.Validation.TypedExpr.binaryApp op a b ty).toResidual = Cedar.Spec.Residual.binaryApp op a.toResidual b.toResidual ty
• (expr.getAttr attr ty).toResidual = expr.toResidual.getAttr attr ty
• (expr.hasAttr attr ty).toResidual = expr.toResidual.hasAttr attr ty
• (expr.extHasAttr attr attrs ty).toResidual = expr.toResidual.extHasAttr attr attrs ty