structure BitVec.Literal : Type

A bit-vector literal

• n : Nat

  Size.

• value : BitVec self.n

  Actual value.

def BitVec.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option BitVec.Literal)

Try to convert OfNat.ofNat/BitVec.OfNat application into a bitvector literal.

Equations

• BitVec.fromExpr? e = do let __discr ← liftM (Lean.Meta.getBitVecValue? e) match __discr with | some ⟨n, value⟩ => pure (some { n := n, value := value }) | x => pure none

@[inline]

def BitVec.reduceUnary (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogenous unary bitvector operators.

Equations

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

@[inline]

def BitVec.reduceBin (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogenous binary bitvector operators.

Equations

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

@[inline]

def BitVec.reduceExtend (declName : Lake.Name) (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Simplification procedure for zeroExtend and signExtend on BitVecs.

Equations

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

@[inline]

def BitVec.reduceGetBit (declName : Lake.Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as getLsb and getMsb.

Equations

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

@[inline]

def BitVec.reduceShift (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as shiftLeft and rotateRight.

Equations

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

@[inline]

def BitVec.reduceShiftWithBitVecLit (declName : Lake.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing x <<< i and x >>> i where i is a bitvector literal, into one that is a natural number literal.

Equations

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

@[inline]

def BitVec.reduceBinPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing bitvector predicates.

Equations

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

@[inline]

def BitVec.reduceBoolPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Equations

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

def BitVec.reduceNeg : Lean.Meta.Simp.DSimproc

Simplification procedure for negation of BitVecs.

Equations

• BitVec.reduceNeg = BitVec.reduceUnary `Neg.neg 3 fun {n : Nat} (x : BitVec n) => -x

def BitVec.reduceNot : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise not of BitVecs.

Equations

• BitVec.reduceNot = BitVec.reduceUnary `Complement.complement 3 fun {n : Nat} (x : BitVec n) => ~~~x

def BitVec.reduceAbs : Lean.Meta.Simp.DSimproc

Simplification procedure for absolute value of BitVecs.

Equations

• BitVec.reduceAbs = BitVec.reduceUnary `BitVec.abs 2 fun {n : Nat} => BitVec.abs

def BitVec.reduceAnd : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise and of BitVecs.

Equations

• BitVec.reduceAnd = BitVec.reduceBin `HAnd.hAnd 6 fun {n : Nat} (x x_1 : BitVec n) => x &&& x_1

def BitVec.reduceOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise or of BitVecs.

Equations

• BitVec.reduceOr = BitVec.reduceBin `HOr.hOr 6 fun {n : Nat} (x x_1 : BitVec n) => x ||| x_1

def BitVec.reduceXOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise xor of BitVecs.

Equations

• BitVec.reduceXOr = BitVec.reduceBin `HXor.hXor 6 fun {n : Nat} (x x_1 : BitVec n) => x ^^^ x_1

def BitVec.reduceAdd : Lean.Meta.Simp.DSimproc

Simplification procedure for addition of BitVecs.

Equations

• BitVec.reduceAdd = BitVec.reduceBin `HAdd.hAdd 6 fun {n : Nat} (x x_1 : BitVec n) => x + x_1

def BitVec.reduceMul : Lean.Meta.Simp.DSimproc

Simplification procedure for multiplication of BitVecs.

Equations

• BitVec.reduceMul = BitVec.reduceBin `HMul.hMul 6 fun {n : Nat} (x x_1 : BitVec n) => x * x_1

def BitVec.reduceSub : Lean.Meta.Simp.DSimproc

Simplification procedure for subtraction of BitVecs.

Equations

• BitVec.reduceSub = BitVec.reduceBin `HSub.hSub 6 fun {n : Nat} (x x_1 : BitVec n) => x - x_1

def BitVec.reduceDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs.

Equations

• BitVec.reduceDiv = BitVec.reduceBin `HDiv.hDiv 6 fun {n : Nat} (x x_1 : BitVec n) => x / x_1

def BitVec.reduceMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the modulo operation on BitVecs.

Equations

• BitVec.reduceMod = BitVec.reduceBin `HMod.hMod 6 fun {n : Nat} (x x_1 : BitVec n) => x % x_1

def BitVec.reduceUMod : Lean.Meta.Simp.DSimproc

Simplification procedure for for the unsigned modulo operation on BitVecs.

Equations

• BitVec.reduceUMod = BitVec.reduceBin `BitVec.umod 3 fun {n : Nat} => BitVec.umod

def BitVec.reduceUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned division of BitVecs.

Equations

• BitVec.reduceUDiv = BitVec.reduceBin `BitVec.udiv 3 fun {n : Nat} => BitVec.udiv

def BitVec.reduceSMTUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs using the SMT-Lib conventions.

Equations

• BitVec.reduceSMTUDiv = BitVec.reduceBin `BitVec.smtUDiv 3 fun {n : Nat} => BitVec.smtUDiv

def BitVec.reduceSMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the signed modulo operation on BitVecs.

Equations

• BitVec.reduceSMod = BitVec.reduceBin `BitVec.smod 3 fun {n : Nat} => BitVec.smod

def BitVec.reduceSRem : Lean.Meta.Simp.DSimproc

Simplification procedure for signed remainder of BitVecs.

Equations

• BitVec.reduceSRem = BitVec.reduceBin `BitVec.srem 3 fun {n : Nat} => BitVec.srem

def BitVec.reduceSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed t-division of BitVecs.

Equations

• BitVec.reduceSDiv = BitVec.reduceBin `BitVec.sdiv 3 fun {n : Nat} => BitVec.sdiv

def BitVec.reduceSMTSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed division of BitVecs using the SMT-Lib conventions.

Equations

• BitVec.reduceSMTSDiv = BitVec.reduceBin `BitVec.smtSDiv 3 fun {n : Nat} => BitVec.smtSDiv

def BitVec.reduceGetLsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getLsb (lowest significant bit) on BitVec.

Equations

• BitVec.reduceGetLsb = BitVec.reduceGetBit `BitVec.getLsb fun {n : Nat} => BitVec.getLsb

def BitVec.reduceGetMsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getMsb (most significant bit) on BitVec.

Equations

• BitVec.reduceGetMsb = BitVec.reduceGetBit `BitVec.getMsb fun {n : Nat} => BitVec.getMsb

def BitVec.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

Equations

• BitVec.reduceShiftLeft = BitVec.reduceShift `BitVec.shiftLeft 3 fun {n : Nat} => BitVec.shiftLeft

def BitVec.reduceUShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned shift right on BitVec.

Equations

• BitVec.reduceUShiftRight = BitVec.reduceShift `BitVec.ushiftRight 3 fun {n : Nat} => BitVec.ushiftRight

def BitVec.reduceSShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for signed shift right on BitVec.

Equations

• BitVec.reduceSShiftRight = BitVec.reduceShift `BitVec.sshiftRight 3 fun {n : Nat} => BitVec.sshiftRight

def BitVec.reduceHShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

Equations

• BitVec.reduceHShiftLeft = BitVec.reduceShift `HShiftLeft.hShiftLeft 6 fun {n : Nat} (x : BitVec n) (x_1 : Nat) => x <<< x_1

def BitVec.reduceHShiftLeft' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

Equations

• BitVec.reduceHShiftLeft' = BitVec.reduceShiftWithBitVecLit `HShiftLeft.hShiftLeft

def BitVec.reduceHShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for shift right on BitVec.

Equations

• BitVec.reduceHShiftRight = BitVec.reduceShift `HShiftRight.hShiftRight 6 fun {n : Nat} (x : BitVec n) (x_1 : Nat) => x >>> x_1

def BitVec.reduceHShiftRight' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

Equations

• BitVec.reduceHShiftRight' = BitVec.reduceShiftWithBitVecLit `HShiftRight.hShiftRight

def BitVec.reduceRotateLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate left on BitVec.

Equations

• BitVec.reduceRotateLeft = BitVec.reduceShift `BitVec.rotateLeft 3 fun {n : Nat} => BitVec.rotateLeft

def BitVec.reduceRotateRight : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate right on BitVec.

Equations

• BitVec.reduceRotateRight = BitVec.reduceShift `BitVec.rotateRight 3 fun {n : Nat} => BitVec.rotateRight

def BitVec.reduceAppend : Lean.Meta.Simp.DSimproc

Simplification procedure for append on BitVec.

Equations

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

def BitVec.reduceCast : Lean.Meta.Simp.DSimproc

Simplification procedure for casting BitVecs along an equality of the size.

Equations

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

def BitVec.reduceToNat : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toNat.

Equations

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

def BitVec.reduceToInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toInt.

Equations

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

def BitVec.reduceOfInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.ofInt.

Equations

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

def BitVec.reduceOfNat : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring BitVec.ofNat literals are normalized.

Equations

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

def BitVec.reduceLT : Lean.Meta.Simp.Simproc

Simplification procedure for < on BitVecs.

Equations

• BitVec.reduceLT = BitVec.reduceBinPred `LT.lt 4 fun {n : Nat} (x x_1 : BitVec n) => decide (x < x_1)

def BitVec.reduceLE : Lean.Meta.Simp.Simproc

Simplification procedure for ≤ on BitVecs.

Equations

• BitVec.reduceLE = BitVec.reduceBinPred `LE.le 4 fun {n : Nat} (x x_1 : BitVec n) => decide (x ≤ x_1)

def BitVec.reduceGT : Lean.Meta.Simp.Simproc

Simplification procedure for > on BitVecs.

Equations

• BitVec.reduceGT = BitVec.reduceBinPred `GT.gt 4 fun {n : Nat} (x x_1 : BitVec n) => decide (x > x_1)

def BitVec.reduceGE : Lean.Meta.Simp.Simproc

Simplification procedure for ≥ on BitVecs.

Equations

• BitVec.reduceGE = BitVec.reduceBinPred `GE.ge 4 fun {n : Nat} (x x_1 : BitVec n) => decide (x ≥ x_1)

def BitVec.reduceULT : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than ult on BitVecs.

Equations

• BitVec.reduceULT = BitVec.reduceBoolPred `BitVec.ult 3 fun {n : Nat} => BitVec.ult

def BitVec.reduceULE : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than or equal ule on BitVecs.

Equations

• BitVec.reduceULE = BitVec.reduceBoolPred `BitVec.ule 3 fun {n : Nat} => BitVec.ule

def BitVec.reduceSLT : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than slt on BitVecs.

Equations

• BitVec.reduceSLT = BitVec.reduceBoolPred `BitVec.slt 3 fun {n : Nat} => BitVec.slt

def BitVec.reduceSLE : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than or equal sle on BitVecs.

Equations

• BitVec.reduceSLE = BitVec.reduceBoolPred `BitVec.sle 3 fun {n : Nat} => BitVec.sle

def BitVec.reduceZeroExtend' : Lean.Meta.Simp.DSimproc

Simplification procedure for zeroExtend' on BitVecs.

Equations

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

def BitVec.reduceShiftLeftZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for shiftLeftZeroExtend on BitVecs.

Equations

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

def BitVec.reduceExtracLsb' : Lean.Meta.Simp.DSimproc

Simplification procedure for extractLsb' on BitVecs.

Equations

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

def BitVec.reduceReplicate : Lean.Meta.Simp.DSimproc

Simplification procedure for replicate on BitVecs.

Equations

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

def BitVec.reduceZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for zeroExtend on BitVecs.

Equations

• BitVec.reduceZeroExtend = BitVec.reduceExtend `BitVec.zeroExtend fun {n : Nat} => BitVec.zeroExtend

def BitVec.reduceSignExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for signExtend on BitVecs.

Equations

• BitVec.reduceSignExtend = BitVec.reduceExtend `BitVec.signExtend fun {n : Nat} => BitVec.signExtend

def BitVec.reduceAllOnes : Lean.Meta.Simp.DSimproc

Simplification procedure for allOnes

Equations

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

def BitVec.reduceBitVecOfFin : Lean.Meta.Simp.DSimproc

Equations

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

def BitVec.reduceBitVecToFin : Lean.Meta.Simp.DSimproc

Equations

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

@[inline]

def BitVec.reduceShiftShift (declName : Lake.Name) (thmName : Lake.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing (x <<< i) <<< j (and (x >>> i) >>> j) where i and j are natural number literals.

Equations

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

def BitVec.reduceShiftLeftShiftLeft : Lean.Meta.Simp.Simproc

Equations

• BitVec.reduceShiftLeftShiftLeft = BitVec.reduceShiftShift `HShiftLeft.hShiftLeft `BitVec.shiftLeft_add

def BitVec.reduceShiftRightShiftRight : Lean.Meta.Simp.Simproc

Equations

• BitVec.reduceShiftRightShiftRight = BitVec.reduceShiftShift `HShiftRight.hShiftRight `BitVec.shiftRight_add