Propagators that evaluate structural BitVec operations on literals.

The arguments are matched modulo equalities: given x = 42#64, the propagator for extractLsb' asserts BitVec.extractLsb' 63 32 x = 0#32. The proofs combine the generic congruence theorems Grind.eval_congr₁/Grind.eval_congr₂ with an Eq.refl hypothesis discharged by kernel reduction. Arguments that occur in the result type (widths, extract bounds, replicate counts) must be syntactic literals; the remaining arguments only need to be equal to literals.

We deliberately skip:

• arithmetic operations and comparisons (+, *, -, /, %, division variants, <, ≤): they are handled by cutsat;
• setWidth' and shiftLeftZeroExtend (rare, and their argument order does not fit the suffix-application scheme used by the congruence theorems);
• BitVec.cast, ofFin/toFin.

The table.

def Lean.Meta.Grind.propagateBVNot : Propagator

Equations

• Lean.Meta.Grind.propagateBVNot = Lean.Meta.Grind.unaryBV✝ `Complement.complement 3 fun {n : Nat} (x : BitVec n) => ~~~x

def Lean.Meta.Grind.propagateBVClz : Propagator

Equations

• Lean.Meta.Grind.propagateBVClz = Lean.Meta.Grind.unaryBV✝ `BitVec.clz 2 fun {n : Nat} => BitVec.clz

def Lean.Meta.Grind.propagateBVCpop : Propagator

Equations

• Lean.Meta.Grind.propagateBVCpop = Lean.Meta.Grind.unaryBV✝ `BitVec.cpop 2 fun {n : Nat} => BitVec.cpop

def Lean.Meta.Grind.propagateBVMsb : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVToNat : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVToInt : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVOfNat : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVOfInt : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVSetWidth : Propagator

Equations

• Lean.Meta.Grind.propagateBVSetWidth = Lean.Meta.Grind.extendBV✝ `BitVec.setWidth fun {n : Nat} => BitVec.setWidth

def Lean.Meta.Grind.propagateBVSignExtend : Propagator

Equations

• Lean.Meta.Grind.propagateBVSignExtend = Lean.Meta.Grind.extendBV✝ `BitVec.signExtend fun {n : Nat} => BitVec.signExtend

def Lean.Meta.Grind.propagateBVExtractLsb' : Propagator

Equations

• Lean.Meta.Grind.propagateBVExtractLsb' = Lean.Meta.Grind.extractBV✝ `BitVec.extractLsb' fun {n : Nat} (start len : Nat) (v : BitVec n) => ⟨len, BitVec.extractLsb' start len v⟩

def Lean.Meta.Grind.propagateBVExtractLsb : Propagator

Equations

• Lean.Meta.Grind.propagateBVExtractLsb = Lean.Meta.Grind.extractBV✝ `BitVec.extractLsb fun {n : Nat} (hi lo : Nat) (v : BitVec n) => ⟨hi - lo + 1, BitVec.extractLsb hi lo v⟩

def Lean.Meta.Grind.propagateBVReplicate : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVAnd : Propagator

Equations

• Lean.Meta.Grind.propagateBVAnd = Lean.Meta.Grind.binBV✝ `HAnd.hAnd 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 &&& x2

def Lean.Meta.Grind.propagateBVOr : Propagator

Equations

• Lean.Meta.Grind.propagateBVOr = Lean.Meta.Grind.binBV✝ `HOr.hOr 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 ||| x2

def Lean.Meta.Grind.propagateBVXor : Propagator

Equations

• Lean.Meta.Grind.propagateBVXor = Lean.Meta.Grind.binBV✝ `HXor.hXor 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 ^^^ x2

def Lean.Meta.Grind.propagateBVAppend : Propagator

Equations

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

def Lean.Meta.Grind.propagateBVShiftLeft : Propagator

Equations

• Lean.Meta.Grind.propagateBVShiftLeft = Lean.Meta.Grind.shiftBV✝ `BitVec.shiftLeft 3 fun {n : Nat} => BitVec.shiftLeft

def Lean.Meta.Grind.propagateBVUShiftRight : Propagator

Equations

• Lean.Meta.Grind.propagateBVUShiftRight = Lean.Meta.Grind.shiftBV✝ `BitVec.ushiftRight 3 fun {n : Nat} => BitVec.ushiftRight

def Lean.Meta.Grind.propagateBVSShiftRight : Propagator

Equations

• Lean.Meta.Grind.propagateBVSShiftRight = Lean.Meta.Grind.shiftBV✝ `BitVec.sshiftRight 3 fun {n : Nat} => BitVec.sshiftRight

def Lean.Meta.Grind.propagateBVRotateLeft : Propagator

Equations

• Lean.Meta.Grind.propagateBVRotateLeft = Lean.Meta.Grind.shiftBV✝ `BitVec.rotateLeft 3 fun {n : Nat} => BitVec.rotateLeft

def Lean.Meta.Grind.propagateBVRotateRight : Propagator

Equations

• Lean.Meta.Grind.propagateBVRotateRight = Lean.Meta.Grind.shiftBV✝ `BitVec.rotateRight 3 fun {n : Nat} => BitVec.rotateRight

def Lean.Meta.Grind.propagateBVHShiftLeft : Propagator

Equations

• Lean.Meta.Grind.propagateBVHShiftLeft = Lean.Meta.Grind.hShiftBV✝ `HShiftLeft.hShiftLeft fun {n : Nat} (x1 : BitVec n) (x2 : Nat) => x1 <<< x2

def Lean.Meta.Grind.propagateBVHShiftRight : Propagator

Equations

• Lean.Meta.Grind.propagateBVHShiftRight = Lean.Meta.Grind.hShiftBV✝ `HShiftRight.hShiftRight fun {n : Nat} (x1 : BitVec n) (x2 : Nat) => x1 >>> x2

def Lean.Meta.Grind.propagateBVGetLsbD : Propagator

Equations

• Lean.Meta.Grind.propagateBVGetLsbD = Lean.Meta.Grind.getBitBV✝ `BitVec.getLsbD fun {n : Nat} => BitVec.getLsbD

def Lean.Meta.Grind.propagateBVGetMsbD : Propagator

Equations

• Lean.Meta.Grind.propagateBVGetMsbD = Lean.Meta.Grind.getBitBV✝ `BitVec.getMsbD fun {n : Nat} => BitVec.getMsbD

def Lean.Meta.Grind.propagateBVGetElem : Propagator

Equations

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