This file defines the operators on Cedar Terms. See Term.lean for the definition of the Term language.

There are three kinds of term operators:

1. Operators that map directly to an underlying SMT theory
2. Operators for constructing and destructing core ADTs that are lowered to SMT by a trusted code generation pass. This also includes core operators whose semantics we don't model in the Term language (but rather directly in SMT), such as like.
3. Operators for destructing extension ADTs, also lowered by the trusted pass.

We separate extension operators into their own ADT (ExtOp) to make it easier to add more such operators in the future in a way that's fairly independent of the other operators.

We embed SMT and core ADT operators directly into the top-level Op ADT, to simplify pattern matching against them within rewrite rules.

structure Cedar.SymCC.UUF : Type

• id : String
• arg : TermType
• out : TermType

inductive Cedar.SymCC.ExtOp : Type

• val : ExtOp
• isV4 : ExtOp
• addrV4 : ExtOp
• prefixV4 : ExtOp
• addrV6 : ExtOp
• prefixV6 : ExtOp
• val : ExtOp
• ofBitVec : ExtOp
• val : ExtOp
• ofBitVec : ExtOp

inductive Cedar.SymCC.Op : Type

• not : Op
• and : Op
• or : Op
• eq : Op
• ite : Op
• uuf : UUF → Op
• bvneg : Op
• bvadd : Op
• bvsub : Op
• bvmul : Op
• bvsdiv : Op
• bvudiv : Op
• bvsrem : Op
• bvsmod : Op
• bvurem : Op
• bvshl : Op
• bvlshr : Op
• bvslt : Op
• bvsle : Op
• bvult : Op
• bvule : Op
• bvnego : Op
• bvsaddo : Op
• bvssubo : Op
• bvsmulo : Op
• zero_extend : Nat → Op
• member : Op
• subset : Op
• inter : Op
• get : Op
• get : Spec.Attr → Op
• like : Spec.Pattern → Op
• ext : ExtOp → Op

def Cedar.SymCC.instReprUUF.repr : UUF → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprUUF : Repr UUF

Equations

• Cedar.SymCC.instReprUUF = { reprPrec := Cedar.SymCC.instReprUUF.repr }

instance Cedar.SymCC.instDecidableEqUUF : DecidableEq UUF

Equations

• Cedar.SymCC.instDecidableEqUUF = Cedar.SymCC.instDecidableEqUUF.decEq

def Cedar.SymCC.instDecidableEqUUF.decEq (x✝ x✝¹ : UUF) : Decidable (x✝ = x✝¹)

Equations

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

def Cedar.SymCC.instInhabitedUUF.default : UUF

Equations

• Cedar.SymCC.instInhabitedUUF.default = { id := default, arg := default, out := default }

instance Cedar.SymCC.instInhabitedUUF : Inhabited UUF

Equations

• Cedar.SymCC.instInhabitedUUF = { default := Cedar.SymCC.instInhabitedUUF.default }

def Cedar.SymCC.instReprExtOp.repr : ExtOp → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprExtOp : Repr ExtOp

Equations

• Cedar.SymCC.instReprExtOp = { reprPrec := Cedar.SymCC.instReprExtOp.repr }

instance Cedar.SymCC.instDecidableEqExtOp : DecidableEq ExtOp

Equations

• Cedar.SymCC.instDecidableEqExtOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Cedar.SymCC.instInhabitedExtOp : Inhabited ExtOp

Equations

• Cedar.SymCC.instInhabitedExtOp = { default := Cedar.SymCC.instInhabitedExtOp.default }

def Cedar.SymCC.instInhabitedExtOp.default : ExtOp

Equations

• Cedar.SymCC.instInhabitedExtOp.default = Cedar.SymCC.ExtOp.decimal.val

def Cedar.SymCC.instReprOp.repr : Op → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.not prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.not")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.and prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.and")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.or prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.or")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.eq")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.ite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.ite")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvneg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvneg")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvadd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvadd")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsub")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvmul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvmul")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsdiv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsdiv")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvudiv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvudiv")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsrem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsrem")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsmod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsmod")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvurem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvurem")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvshl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvshl")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvlshr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvlshr")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvslt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvslt")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsle")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvult prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvult")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvule prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvule")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvnego prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvnego")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsaddo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsaddo")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvssubo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvssubo")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.bvsmulo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.bvsmulo")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.set.member prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.set.member")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.set.subset prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.set.subset")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.set.inter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.set.inter")).group prec✝
• Cedar.SymCC.instReprOp.repr Cedar.SymCC.Op.option.get prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Op.option.get")).group prec✝

instance Cedar.SymCC.instReprOp : Repr Op

Equations

• Cedar.SymCC.instReprOp = { reprPrec := Cedar.SymCC.instReprOp.repr }

def Cedar.SymCC.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.SymCC.instDecidableEqOp : DecidableEq Op

Equations

• Cedar.SymCC.instDecidableEqOp = Cedar.SymCC.instDecidableEqOp.decEq

def Cedar.SymCC.instInhabitedOp.default : Op

Equations

• Cedar.SymCC.instInhabitedOp.default = Cedar.SymCC.Op.not

instance Cedar.SymCC.instInhabitedOp : Inhabited Op

Equations

• Cedar.SymCC.instInhabitedOp = { default := Cedar.SymCC.instInhabitedOp.default }

def Cedar.SymCC.UUF.lt (uf uf' : UUF) : Bool

Equations

• uf.lt uf' = (decide (uf.id < uf'.id) || decide (uf.id = uf'.id) && decide (uf.arg < uf'.arg) || decide (uf.id = uf'.id) && decide (uf.arg = uf'.arg) && decide (uf.out < uf'.out))

instance Cedar.SymCC.instLTUUF : LT UUF

Equations

• Cedar.SymCC.instLTUUF = { lt := fun (x y : Cedar.SymCC.UUF) => x.lt y = true }

instance Cedar.SymCC.UUF.decLt (x y : UUF) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

def Cedar.SymCC.ExtOp.lt : ExtOp → ExtOp → Bool

Equations

• x✝¹.lt x✝ = decide (Cedar.SymCC.ExtOp.mkName✝ x✝¹ < Cedar.SymCC.ExtOp.mkName✝¹ x✝)

instance Cedar.SymCC.instLTExtOp : LT ExtOp

Equations

• Cedar.SymCC.instLTExtOp = { lt := fun (x y : Cedar.SymCC.ExtOp) => x.lt y = true }

instance Cedar.SymCC.ExtOp.decLt (x y : ExtOp) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

def Cedar.SymCC.Op.mkName : Op → String

Equations

• Cedar.SymCC.Op.not.mkName = "not"
• Cedar.SymCC.Op.and.mkName = "and"
• Cedar.SymCC.Op.or.mkName = "or"
• Cedar.SymCC.Op.eq.mkName = "eq"
• Cedar.SymCC.Op.ite.mkName = "ite"
• (Cedar.SymCC.Op.uuf a).mkName = "uuf"
• Cedar.SymCC.Op.bvneg.mkName = "bvneg"
• Cedar.SymCC.Op.bvadd.mkName = "bvadd"
• Cedar.SymCC.Op.bvsub.mkName = "bvsub"
• Cedar.SymCC.Op.bvmul.mkName = "bvmul"
• Cedar.SymCC.Op.bvsdiv.mkName = "bvsdiv"
• Cedar.SymCC.Op.bvudiv.mkName = "bvudiv"
• Cedar.SymCC.Op.bvsrem.mkName = "bvsrem"
• Cedar.SymCC.Op.bvsmod.mkName = "bvsmod"
• Cedar.SymCC.Op.bvurem.mkName = "bvurem"
• Cedar.SymCC.Op.bvshl.mkName = "bvshl"
• Cedar.SymCC.Op.bvlshr.mkName = "bvlshr"
• Cedar.SymCC.Op.bvslt.mkName = "bvslt"
• Cedar.SymCC.Op.bvsle.mkName = "bvsle"
• Cedar.SymCC.Op.bvult.mkName = "bvult"
• Cedar.SymCC.Op.bvule.mkName = "bvule"
• Cedar.SymCC.Op.bvnego.mkName = "bvnego"
• Cedar.SymCC.Op.bvsaddo.mkName = "bvsaddo"
• Cedar.SymCC.Op.bvssubo.mkName = "bvssubo"
• Cedar.SymCC.Op.bvsmulo.mkName = "bvsmulo"
• (Cedar.SymCC.Op.zero_extend a).mkName = "zero_extend"
• Cedar.SymCC.Op.set.member.mkName = "set.member"
• Cedar.SymCC.Op.set.subset.mkName = "set.subset"
• Cedar.SymCC.Op.set.inter.mkName = "set.inter"
• Cedar.SymCC.Op.option.get.mkName = "option.get"
• (Cedar.SymCC.Op.record.get a).mkName = "record.get"
• (Cedar.SymCC.Op.string.like a).mkName = "string.like"
• (Cedar.SymCC.Op.ext a).mkName = "ext"

def Cedar.SymCC.Op.lt : Op → Op → Bool

Equations

• (Cedar.SymCC.Op.uuf f₁).lt (Cedar.SymCC.Op.uuf f₂) = decide (f₁ < f₂)
• (Cedar.SymCC.Op.zero_extend n₁).lt (Cedar.SymCC.Op.zero_extend n₂) = decide (n₁ < n₂)
• (Cedar.SymCC.Op.record.get a₁).lt (Cedar.SymCC.Op.record.get a₂) = decide (a₁ < a₂)
• (Cedar.SymCC.Op.string.like p₁).lt (Cedar.SymCC.Op.string.like p₂) = decide (p₁ < p₂)
• (Cedar.SymCC.Op.ext xty₁).lt (Cedar.SymCC.Op.ext xty₂) = decide (xty₁ < xty₂)
• x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

instance Cedar.SymCC.instLTOp : LT Op

Equations

• Cedar.SymCC.instLTOp = { lt := fun (x y : Cedar.SymCC.Op) => x.lt y = true }

instance Cedar.SymCC.Op.decLt (x y : Op) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h