This file contains generic utility functions shared by SymCC modules.

@[inline]

def BitVec.width {n : Nat} : BitVec n → Nat

Equations

• x✝.width = n

def BitVec.signedMin (n : Nat) : Int

Equations

• BitVec.signedMin n = -2 ^ (n - 1)

def BitVec.signedMax (n : Nat) : Int

Equations

• BitVec.signedMax n = 2 ^ (n - 1) - 1

def BitVec.overflows (n : Nat) (i : Int) : Bool

Equations

• BitVec.overflows n i = (decide (i < BitVec.signedMin n) || decide (i > BitVec.signedMax n))

@[reducible, inline]

abbrev Cedar.SymCC.EntityTag (α : Type u_1) : Type u_1

Equations

• Cedar.SymCC.EntityTag α = Cedar.Data.Map String α

@[reducible, inline]

abbrev Cedar.SymCC.EntityTag.mk {α : Type u_1} (entity tag : α) : EntityTag α

Equations

• Cedar.SymCC.EntityTag.mk entity tag = Cedar.Data.Map.mk [("entity", entity), ("tag", tag)]

@[reducible, inline]

abbrev Cedar.SymCC.EntityTag.wf {α : Type u_1} : EntityTag α → Bool

Equations

• Cedar.SymCC.EntityTag.wf (Cedar.Data.Map.mk [("entity", snd), ("tag", snd_1)]) = true
• x✝.wf = false