This file defines an API for construcing well-formed Terms. In this basic implementation, the factory functions perform only basic partial evaluation---constant folding along with a few other rewrites. In an optimized implementation, the factory functions would include more rewrite rules, and share a cache of partially cannonicalized terms that have been constructed so far.

The factory functions are total. If given well-formed and type-correct arguments, a factory function will return a well-formed and type-correct output. Otherwise, the output is an arbitrary term.

This design lets us minimize the number of error paths in the overall specification of symbolic compilation, which makes for nicer code and proofs, and it more closely tracks the specification of the concrete evaluator.

See Compiler.lean to see how the symbolic compiler uses this API.

@[inline]

def Cedar.SymCC.Factory.noneOf (ty : TermType) : Term

Equations

• Cedar.SymCC.Factory.noneOf ty = Cedar.SymCC.Term.none ty

@[inline]

def Cedar.SymCC.Factory.someOf (t : Term) : Term

Equations

• (⊙t) = t.some

def Cedar.SymCC.Factory.«term⊙_» : Lean.ParserDescr

Equations

• Cedar.SymCC.Factory.«term⊙_» = Lean.ParserDescr.node `Cedar.SymCC.Factory.«term⊙_» 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊙") (Lean.ParserDescr.cat `term 0))

def Cedar.SymCC.Factory.setOf (ts : List Term) (ty : TermType) : Term

Equations

• Cedar.SymCC.Factory.setOf ts ty = Cedar.SymCC.Term.set (Cedar.Data.Set.make ts) ty

def Cedar.SymCC.Factory.recordOf (ats : List (Spec.Attr × Term)) : Term

Equations

• Cedar.SymCC.Factory.recordOf ats = Cedar.SymCC.Term.record (Cedar.Data.Map.make ats)

def Cedar.SymCC.Factory.tagOf (entity tag : Term) : Term

Equations

• Cedar.SymCC.Factory.tagOf entity tag = Cedar.SymCC.Term.record (Cedar.SymCC.EntityTag.mk entity tag)

def Cedar.SymCC.Factory.not : Term → Term

Equations

• Cedar.SymCC.Factory.not (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool b)) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool !b)
• Cedar.SymCC.Factory.not (Cedar.SymCC.Term.app Cedar.SymCC.Op.not [t'] retTy) = t'
• Cedar.SymCC.Factory.not x✝ = Cedar.SymCC.Term.app Cedar.SymCC.Op.not [x✝] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.opposites : Term → Term → Bool

Equations

• Cedar.SymCC.Factory.opposites x✝ (Cedar.SymCC.Term.app Cedar.SymCC.Op.not [t₂] retTy) = decide (x✝ = t₂)
• Cedar.SymCC.Factory.opposites (Cedar.SymCC.Term.app Cedar.SymCC.Op.not [t₁] retTy) x✝ = decide (t₁ = x✝)
• Cedar.SymCC.Factory.opposites x✝¹ x✝ = false

def Cedar.SymCC.Factory.and (t₁ t₂ : Term) : Term

Equations

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

def Cedar.SymCC.Factory.or (t₁ t₂ : Term) : Term

Equations

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

def Cedar.SymCC.Factory.implies (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.implies t₁ t₂ = Cedar.SymCC.Factory.or (Cedar.SymCC.Factory.not t₁) t₂

def Cedar.SymCC.Factory.eq (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.eq t₁'.some t₂'.some = Cedar.SymCC.Factory.eq.simplify t₁' t₂'
• Cedar.SymCC.Factory.eq a.some (Cedar.SymCC.Term.none a_1) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)
• Cedar.SymCC.Factory.eq (Cedar.SymCC.Term.none a) a_1.some = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)
• Cedar.SymCC.Factory.eq t₁ t₂ = Cedar.SymCC.Factory.eq.simplify t₁ t₂

def Cedar.SymCC.Factory.eq.simplify (t₁ t₂ : Term) : Term

Equations

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

def Cedar.SymCC.Factory.ite (t₁ t₂ t₃ : Term) : Term

Equations

• Cedar.SymCC.Factory.ite t₁ t₂'.some t₃'.some = (Cedar.SymCC.Factory.ite.simplify t₁ t₂' t₃').some
• Cedar.SymCC.Factory.ite t₁ t₂ t₃ = Cedar.SymCC.Factory.ite.simplify t₁ t₂ t₃

def Cedar.SymCC.Factory.ite.simplify (t₁ t₂ t₃ : Term) : Term

Equations

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

def Cedar.SymCC.Factory.app : UnaryFunction → Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.app (Cedar.SymCC.UnaryFunction.uuf f) x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.uuf f) [x✝] f.out

def Cedar.SymCC.Factory.bvneg : Term → Term

Equations

• Cedar.SymCC.Factory.bvneg (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec b)) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec b.neg)
• Cedar.SymCC.Factory.bvneg (Cedar.SymCC.Term.app Cedar.SymCC.Op.bvneg [t] retTy) = t
• Cedar.SymCC.Factory.bvneg x✝ = Cedar.SymCC.Term.app Cedar.SymCC.Op.bvneg [x✝] x✝.typeOf

def Cedar.SymCC.Factory.bvapp (op : Op) (fn : {n : Nat} → BitVec n → BitVec n → BitVec n) (t₁ t₂ : Term) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.bvapp op fn t₁ t₂ = Cedar.SymCC.Term.app op [t₁, t₂] t₁.typeOf

def Cedar.SymCC.Factory.bvadd (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvadd = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvadd fun {n : Nat} => BitVec.add

def Cedar.SymCC.Factory.bvsub (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsub = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvsub fun {n : Nat} => BitVec.sub

def Cedar.SymCC.Factory.bvmul (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvmul = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvmul fun {n : Nat} => BitVec.mul

def Cedar.SymCC.Factory.bvsdiv (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsdiv = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvsdiv fun {n : Nat} => BitVec.smtSDiv

def Cedar.SymCC.Factory.bvudiv (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvudiv = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvudiv fun {n : Nat} => BitVec.smtUDiv

def Cedar.SymCC.Factory.bvsrem (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsrem = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvsrem fun {n : Nat} => BitVec.srem

def Cedar.SymCC.Factory.bvsmod (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsmod = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvsmod fun {n : Nat} => BitVec.smod

def Cedar.SymCC.Factory.bvurem (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvurem = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvurem fun {n : Nat} => BitVec.umod

def Cedar.SymCC.Factory.bvshl (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvshl = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvshl fun {n : Nat} (b₁ b₂ : BitVec n) => b₁ <<< b₂

def Cedar.SymCC.Factory.bvlshr (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvlshr = Cedar.SymCC.Factory.bvapp Cedar.SymCC.Op.bvlshr fun {n : Nat} (b₁ b₂ : BitVec n) => b₁ >>> b₂

def Cedar.SymCC.Factory.bvcmp (op : Op) (fn : {n : Nat} → BitVec n → BitVec n → Bool) (t₁ t₂ : Term) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.bvcmp op fn t₁ t₂ = Cedar.SymCC.Term.app op [t₁, t₂] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.bvslt (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvslt = Cedar.SymCC.Factory.bvcmp Cedar.SymCC.Op.bvslt fun {n : Nat} => BitVec.slt

def Cedar.SymCC.Factory.bvsle (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsle = Cedar.SymCC.Factory.bvcmp Cedar.SymCC.Op.bvsle fun {n : Nat} => BitVec.sle

def Cedar.SymCC.Factory.bvult (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvult = Cedar.SymCC.Factory.bvcmp Cedar.SymCC.Op.bvult fun {n : Nat} => BitVec.ult

def Cedar.SymCC.Factory.bvule (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvule = Cedar.SymCC.Factory.bvcmp Cedar.SymCC.Op.bvule fun {n : Nat} => BitVec.ule

def Cedar.SymCC.Factory.bvnego : Term → Term

Equations

• Cedar.SymCC.Factory.bvnego (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec b₁)) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool (BitVec.overflows n (-b₁.toInt)))
• Cedar.SymCC.Factory.bvnego x✝ = Cedar.SymCC.Term.app Cedar.SymCC.Op.bvnego [x✝] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.bvso (op : Op) (fn : Int → Int → Int) (t₁ t₂ : Term) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.bvso op fn t₁ t₂ = Cedar.SymCC.Term.app op [t₁, t₂] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.bvsaddo (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsaddo = Cedar.SymCC.Factory.bvso Cedar.SymCC.Op.bvsaddo fun (x1 x2 : Int) => x1 + x2

def Cedar.SymCC.Factory.bvssubo (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvssubo = Cedar.SymCC.Factory.bvso Cedar.SymCC.Op.bvssubo fun (x1 x2 : Int) => x1 - x2

def Cedar.SymCC.Factory.bvsmulo (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsmulo = Cedar.SymCC.Factory.bvso Cedar.SymCC.Op.bvsmulo fun (x1 x2 : Int) => x1 * x2

def Cedar.SymCC.Factory.zero_extend (n : Nat) : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.zero_extend n (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec b₁)) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (BitVec.zeroExtend (n + n_1) b₁))

def Cedar.SymCC.Factory.set.member (t ts : Term) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.set.member t (Cedar.SymCC.Term.set (Cedar.Data.Set.mk []) eltsTy) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)
• Cedar.SymCC.Factory.set.member t ts = Cedar.SymCC.Term.app Cedar.SymCC.Op.set.member [t, ts] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.set.subset (sub sup : Term) : Term

Equations

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

def Cedar.SymCC.Factory.set.inter (ts₁ ts₂ : Term) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.set.inter ts₁ ts₂ = if ts₁ = ts₂ then ts₁ else Cedar.SymCC.Term.app Cedar.SymCC.Op.set.inter [ts₁, ts₂] ts₁.typeOf

def Cedar.SymCC.Factory.set.isEmpty : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.set.isEmpty (Cedar.SymCC.Term.set s eltsTy) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool s.isEmpty)

def Cedar.SymCC.Factory.set.intersects (ts₁ ts₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.set.intersects ts₁ ts₂ = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.set.isEmpty (Cedar.SymCC.Factory.set.inter ts₁ ts₂))

def Cedar.SymCC.Factory.option.get : Term → Term

Equations

• Cedar.SymCC.Factory.option.get t.some = t
• Cedar.SymCC.Factory.option.get x✝ = match x✝.typeOf with | ty.option => Cedar.SymCC.Term.app Cedar.SymCC.Op.option.get [x✝] ty | x => x✝

def Cedar.SymCC.Factory.record.get (t : Term) (a : Spec.Attr) : Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.record.get (Cedar.SymCC.Term.record r) a = match r.find? a with | some tₐ => tₐ | x => Cedar.SymCC.Term.record r

def Cedar.SymCC.Factory.string.like (t : Term) (p : Spec.Pattern) : Term

Equations

• Cedar.SymCC.Factory.string.like (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.string s)) p = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool (Cedar.Spec.wildcardMatch s p))
• Cedar.SymCC.Factory.string.like t p = Cedar.SymCC.Term.app (Cedar.SymCC.Op.string.like p) [t] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.ext.decimal.val : Term → Term

Equations

• Cedar.SymCC.Factory.ext.decimal.val (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext (Cedar.Spec.Ext.decimal d))) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec (Int64.toBitVec d))
• Cedar.SymCC.Factory.ext.decimal.val x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.decimal.val) [x✝] (Cedar.SymCC.TermType.bitvec 64)

def Cedar.SymCC.Factory.ext.ipaddr.isV4 : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.ipaddr.isV4 x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.ipaddr.isV4) [x✝] Cedar.SymCC.TermType.bool

def Cedar.SymCC.Factory.ext.ipaddr.addrV4 : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.ipaddr.addrV4 x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.ipaddr.addrV4) [x✝] (Cedar.SymCC.TermType.bitvec 32)

def Cedar.SymCC.Factory.ext.ipaddr.prefixV4 : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.ipaddr.prefixV4 x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.ipaddr.prefixV4) [x✝] (Cedar.SymCC.TermType.bitvec 5).option

def Cedar.SymCC.Factory.ext.ipaddr.addrV6 : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.ipaddr.addrV6 x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.ipaddr.addrV6) [x✝] (Cedar.SymCC.TermType.bitvec 128)

def Cedar.SymCC.Factory.ext.ipaddr.prefixV6 : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.ipaddr.prefixV6 x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.ipaddr.prefixV6) [x✝] (Cedar.SymCC.TermType.bitvec 7).option

def Cedar.SymCC.Factory.ext.datetime.val : Term → Term

Equations

• Cedar.SymCC.Factory.ext.datetime.val (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext (Cedar.Spec.Ext.datetime d))) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec d.val.toBitVec)
• Cedar.SymCC.Factory.ext.datetime.val x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.datetime.val) [x✝] (Cedar.SymCC.TermType.bitvec 64)

def Cedar.SymCC.Factory.ext.datetime.ofBitVec : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.datetime.ofBitVec x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.datetime.ofBitVec) [x✝] (Cedar.SymCC.TermType.ext Cedar.Validation.ExtType.datetime)

def Cedar.SymCC.Factory.ext.duration.val : Term → Term

Equations

• Cedar.SymCC.Factory.ext.duration.val (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext (Cedar.Spec.Ext.duration d))) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec d.val.toBitVec)
• Cedar.SymCC.Factory.ext.duration.val x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.duration.val) [x✝] (Cedar.SymCC.TermType.bitvec 64)

def Cedar.SymCC.Factory.ext.duration.ofBitVec : Term → Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.Factory.ext.duration.ofBitVec x✝ = Cedar.SymCC.Term.app (Cedar.SymCC.Op.ext Cedar.SymCC.ExtOp.duration.ofBitVec) [x✝] (Cedar.SymCC.TermType.ext Cedar.Validation.ExtType.duration)

def Cedar.SymCC.Factory.isNone : Term → Term

Equations

• Cedar.SymCC.Factory.isNone (Cedar.SymCC.Term.none a) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true)
• Cedar.SymCC.Factory.isNone a.some = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)
• Cedar.SymCC.Factory.isNone (Cedar.SymCC.Term.app Cedar.SymCC.Op.ite [head, a.some, a_1.some] retTy) = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)
• Cedar.SymCC.Factory.isNone (Cedar.SymCC.Term.app Cedar.SymCC.Op.ite [g, a.some, Cedar.SymCC.Term.none a_1] retTy) = Cedar.SymCC.Factory.not g
• Cedar.SymCC.Factory.isNone (Cedar.SymCC.Term.app Cedar.SymCC.Op.ite [g, Cedar.SymCC.Term.none a, a_1.some] retTy) = g
• Cedar.SymCC.Factory.isNone x✝ = match x✝.typeOf with | ty.option => Cedar.SymCC.Factory.eq x✝ (Cedar.SymCC.Term.none ty) | x => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)

def Cedar.SymCC.Factory.isSome (t : Term) : Term

Equations

• Cedar.SymCC.Factory.isSome t = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.isNone t)

def Cedar.SymCC.Factory.ifFalse (g t : Term) : Term

Equations

• Cedar.SymCC.Factory.ifFalse g t = Cedar.SymCC.Factory.ite g (Cedar.SymCC.Factory.noneOf t.typeOf) (⊙t)

def Cedar.SymCC.Factory.ifTrue (g t : Term) : Term

Equations

• Cedar.SymCC.Factory.ifTrue g t = Cedar.SymCC.Factory.ite g (⊙t) (Cedar.SymCC.Factory.noneOf t.typeOf)

def Cedar.SymCC.Factory.ifSome (g t : Term) : Term

Equations

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

def Cedar.SymCC.Factory.anyTrue (f : Term → Term) (ts : List Term) : Term

Equations

• Cedar.SymCC.Factory.anyTrue f ts = List.foldl (fun (acc t : Cedar.SymCC.Term) => Cedar.SymCC.Factory.or (f t) acc) (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool false)) ts

def Cedar.SymCC.Factory.anyNone (gs : List Term) : Term

Equations

• Cedar.SymCC.Factory.anyNone gs = Cedar.SymCC.Factory.anyTrue Cedar.SymCC.Factory.isNone gs

def Cedar.SymCC.Factory.ifAllSome (gs : List Term) (t : Term) : Term

Equations

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

def Cedar.SymCC.Factory.bvaddChecked (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvaddChecked t₁ t₂ = Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvsaddo t₁ t₂) (Cedar.SymCC.Factory.bvadd t₁ t₂)

def Cedar.SymCC.Factory.bvsubChecked (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvsubChecked t₁ t₂ = Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvssubo t₁ t₂) (Cedar.SymCC.Factory.bvsub t₁ t₂)

def Cedar.SymCC.Factory.bvmulChecked (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.Factory.bvmulChecked t₁ t₂ = Cedar.SymCC.Factory.ifFalse (Cedar.SymCC.Factory.bvsmulo t₁ t₂) (Cedar.SymCC.Factory.bvmul t₁ t₂)