This file contains well-typedness definitions of TypedExpr

inductive Cedar.Spec.UnaryResidualWellTyped : UnaryOp → Residual → Validation.CedarType → Prop

• not {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : UnaryResidualWellTyped UnaryOp.not x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• neg {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) : UnaryResidualWellTyped UnaryOp.neg x₁ Validation.CedarType.int
• isEmpty {x₁ : Residual} {eltTy : Validation.CedarType} (h₁ : x₁.typeOf = eltTy.set) : UnaryResidualWellTyped UnaryOp.isEmpty x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• like {x₁ : Residual} {p : Pattern} (h₁ : x₁.typeOf = Validation.CedarType.string) : UnaryResidualWellTyped (UnaryOp.like p) x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• is {x₁ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₂) : UnaryResidualWellTyped (UnaryOp.is ety₁) x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)

inductive Cedar.Spec.BinaryResidualWellTyped (env : Validation.TypeEnv) : BinaryOp → Residual → Residual → Validation.CedarType → Prop

• eq_val {env : Validation.TypeEnv} {p₁ p₂ : Value} {ty₁ ty₂ : Validation.CedarType} : BinaryResidualWellTyped env BinaryOp.eq (Residual.val p₁ ty₁) (Residual.val p₂ ty₂) (Validation.CedarType.bool Validation.BoolType.anyBool)
• eq_entity {env : Validation.TypeEnv} {ety₁ ety₂ : EntityType} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : BinaryResidualWellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• eq {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = x₂.typeOf) : BinaryResidualWellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• memₑ {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : BinaryResidualWellTyped env BinaryOp.mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• memₛ {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = (Validation.CedarType.entity ety₂).set) : BinaryResidualWellTyped env BinaryOp.mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_int {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_datetime {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_duration {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_int {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_datetime {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_duration {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• add {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.add x₁ x₂ Validation.CedarType.int
• sub {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.sub x₁ x₂ Validation.CedarType.int
• mul {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.mul x₁ x₂ Validation.CedarType.int
• contains {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = x₂.typeOf.set) : BinaryResidualWellTyped env BinaryOp.contains x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• containsAll {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : BinaryResidualWellTyped env BinaryOp.containsAll x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• containsAny {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : BinaryResidualWellTyped env BinaryOp.containsAny x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• hasTag {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) : BinaryResidualWellTyped env BinaryOp.hasTag x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• getTag {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety : EntityType} {ty : Validation.CedarType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) (h₃ : env.ets.tags? ety = some (some ty)) : BinaryResidualWellTyped env BinaryOp.getTag x₁ x₂ ty.liftBoolTypes

inductive Cedar.Spec.ExtResidualWellTyped : ExtFun → List Residual → Validation.CedarType → Prop

• decimal {s₁ : String} {d₁ : Ext.Decimal} (h₁ : some d₁ = Ext.Decimal.decimal s₁) : ExtResidualWellTyped ExtFun.decimal [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.decimal)
• lessThan {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.lessThan [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessThanOrEqual {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.lessThanOrEqual [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• greaterThan {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.greaterThan [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• greaterThanOrEqual {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.greaterThanOrEqual [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• ip {s₁ : String} {ip₁ : IPAddr} (h₁ : some ip₁ = Ext.IPAddr.ip s₁) : ExtResidualWellTyped ExtFun.ip [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.ipAddr)
• isIpv4 {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isIpv4 [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isIpv6 {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isIpv6 [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isLoopback {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isLoopback [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isMulticast {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isMulticast [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isInRange {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isInRange [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• datetime {s₁ : String} {d₁ : Ext.Datetime} (h₁ : some d₁ = Ext.Datetime.parse s₁) : ExtResidualWellTyped ExtFun.datetime [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.datetime)
• duration {s₁ : String} {d₁ : Duration} (h₁ : some d₁ = Ext.Datetime.Duration.parse s₁) : ExtResidualWellTyped ExtFun.duration [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.duration)
• offset {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.offset [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.datetime)
• durationSince {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.durationSince [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.duration)
• toDate {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.toDate [x₁] (Validation.CedarType.ext Validation.ExtType.datetime)
• toTime {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.toTime [x₁] (Validation.CedarType.ext Validation.ExtType.duration)
• toMilliseconds {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toMilliseconds [x₁] Validation.CedarType.int
• toSeconds {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toSeconds [x₁] Validation.CedarType.int
• toMinutes {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toMinutes [x₁] Validation.CedarType.int
• toHours {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toHours [x₁] Validation.CedarType.int
• toDays {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toDays [x₁] Validation.CedarType.int

inductive Cedar.Thm.Residual.WellTyped (env : Validation.TypeEnv) : Spec.Residual → Prop

Well-typedness definition for Residual expressions

• val {env : Validation.TypeEnv} {v : Spec.Value} {ty : Validation.CedarType} (h₁ : InstanceOfType env v ty) : WellTyped env (Spec.Residual.val v ty)
• var {env : Validation.TypeEnv} {v : Spec.Var} {ty : Validation.CedarType} (h₁ : Spec.Var.WellTyped env v ty) : WellTyped env (Spec.Residual.var v ty)
• ite {env : Validation.TypeEnv} {x₁ x₂ x₃ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : WellTyped env x₃) (h₄ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₅ : x₂.typeOf = x₃.typeOf) : WellTyped env (x₁.ite x₂ x₃ x₂.typeOf)
• and {env : Validation.TypeEnv} {x₁ x₂ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.and x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
• or {env : Validation.TypeEnv} {x₁ x₂ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
• unaryApp {env : Validation.TypeEnv} {op₁ : Spec.UnaryOp} {x₁ : Spec.Residual} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : Spec.UnaryResidualWellTyped op₁ x₁ ty) : WellTyped env (Spec.Residual.unaryApp op₁ x₁ ty)
• binaryApp {env : Validation.TypeEnv} {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Residual} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : Spec.BinaryResidualWellTyped env op₂ x₁ x₂ ty) : WellTyped env (Spec.Residual.binaryApp op₂ x₁ x₂ ty)
• hasAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {x₁ : Spec.Residual} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
• hasAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
• getAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) (h₃ : Option.map Validation.RecordType.liftBoolTypes (env.ets.attrs? ety) = some rty) (h₄ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
• getAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) (h₃ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
• set {env : Validation.TypeEnv} {ls : List Spec.Residual} {ty : Validation.CedarType} (h₁ : ∀ (x : Spec.Residual), x ∈ ls → WellTyped env x) (h₂ : ∀ (x : Spec.Residual), x ∈ ls → x.typeOf = ty) (h₃ : (ls != []) = true) : WellTyped env (Spec.Residual.set ls ty.set)
• record {env : Validation.TypeEnv} {rty : Validation.RecordType} {m : List (Spec.Attr × Spec.Residual)} (h₁ : ∀ (k : Spec.Attr) (v : Spec.Residual), (k, v) ∈ m → WellTyped env v) (h₂ : rty = Data.Map.make (List.map (fun (x : Spec.Attr × Spec.Residual) => match x with | (a, r) => (a, Validation.Qualified.required r.typeOf)) m)) : WellTyped env (Spec.Residual.record m (Validation.CedarType.record rty))
• call {env : Validation.TypeEnv} {xfn : Spec.ExtFun} {args : List Spec.Residual} {ty : Validation.CedarType} (h₁ : ∀ (x : Spec.Residual), x ∈ args → WellTyped env x) (h₂ : Spec.ExtResidualWellTyped xfn args ty) : WellTyped env (Spec.Residual.call xfn args ty)
• error {env : Validation.TypeEnv} {ty : Validation.CedarType} : WellTyped env (Spec.Residual.error ty)

theorem Cedar.Thm.well_typed_bool {env : Validation.TypeEnv} {b : Bool} : Residual.WellTyped env (Spec.Residual.val (Spec.Value.prim (Spec.Prim.bool b)) (Validation.CedarType.bool Validation.BoolType.anyBool))

theorem Cedar.Thm.well_typed_int {env : Validation.TypeEnv} {i : Int64} : Residual.WellTyped env (Spec.Residual.val (Spec.Value.prim (Spec.Prim.int i)) Validation.CedarType.int)

theorem Cedar.Thm.well_typed_string {env : Validation.TypeEnv} {s : String} : Residual.WellTyped env (Spec.Residual.val (Spec.Value.prim (Spec.Prim.string s)) Validation.CedarType.string)

theorem Cedar.Thm.well_typed_entity {env : Validation.TypeEnv} {e : Spec.EntityUID} {ety : Spec.EntityType} : InstanceOfEntityType e ety env → Residual.WellTyped env (Spec.Residual.val (Spec.Value.prim (Spec.Prim.entityUID e)) (Validation.CedarType.entity ety))