This module contains the definition of the `BitVec` fragment that `bv_decide` internally operates on as `BVLogicalExpr`. The preprocessing steps of `bv_decide` reduce all supported `BitVec` operations to the ones provided in this file. For verification purposes `BVLogicalExpr.Sat` and `BVLogicalExpr.Unsat` are provided.

source
structure Std.Tactic.BVDecide.BVBit :
Type

The variable definition used by the bitblaster.

- var : Nat

  A numeric identifier for the BitVec variable.

- w : Nat

  The width of the BitVec variable.

- idx : Fin self.w

  The bit that we take out of the BitVec variable by getLsb.

Instances For

source
instance Std.Tactic.BVDecide.instHashableBVBit :
Hashable BVBit
Equations

- Std.Tactic.BVDecide.instHashableBVBit = { hash := Std.Tactic.BVDecide.instHashableBVBit.hash }

source
def Std.Tactic.BVDecide.instHashableBVBit.hash :
BVBit → UInt64
Equations

- Std.Tactic.BVDecide.instHashableBVBit.hash { var := a, w := a_1, idx := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

Instances For

source
instance Std.Tactic.BVDecide.instDecidableEqBVBit :
DecidableEq BVBit
Equations

- Std.Tactic.BVDecide.instDecidableEqBVBit = Std.Tactic.BVDecide.instDecidableEqBVBit.decEq

source
def Std.Tactic.BVDecide.instDecidableEqBVBit.decEq (x✝ x✝¹ : BVBit) :
Decidable (x✝ = x✝¹)
Equations

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

Instances For

source
def Std.Tactic.BVDecide.instReprBVBit.repr :
BVBit → Nat → Format
Equations

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

Instances For

source
instance Std.Tactic.BVDecide.instReprBVBit :
Repr BVBit
Equations

- Std.Tactic.BVDecide.instReprBVBit = { reprPrec := Std.Tactic.BVDecide.instReprBVBit.repr }

source
instance Std.Tactic.BVDecide.instToStringBVBit :
ToString BVBit
Equations

- Std.Tactic.BVDecide.instToStringBVBit = { toString := fun (b : Std.Tactic.BVDecide.BVBit) => toString "x" ++ toString b.var ++ toString "[" ++ toString ↑b.idx ++ toString "]" }

source
instance Std.Tactic.BVDecide.instInhabitedBVBit :
Inhabited BVBit
Equations

- Std.Tactic.BVDecide.instInhabitedBVBit = { default := { var := 0, w := 1, idx := 0 } }

source
inductive Std.Tactic.BVDecide.BVBinOp :
Type

All supported binary operations on `BVExpr`.

- and : BVBinOp

  Bitwise and.

- or : BVBinOp

  Bitwise or.

- xor : BVBinOp

  Bitwise xor.

- add : BVBinOp

  Addition.

- mul : BVBinOp

  Multiplication.

- udiv : BVBinOp

  Unsigned division.

- umod : BVBinOp

  Unsigned modulo.

Instances For

source
instance Std.Tactic.BVDecide.instHashableBVBinOp :
Hashable BVBinOp
Equations

- Std.Tactic.BVDecide.instHashableBVBinOp = { hash := Std.Tactic.BVDecide.instHashableBVBinOp.hash }

source
def Std.Tactic.BVDecide.instHashableBVBinOp.hash :
BVBinOp → UInt64
Equations

- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.and = 0
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.or = 1
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.xor = 2
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.add = 3
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.mul = 4
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.udiv = 5
- Std.Tactic.BVDecide.instHashableBVBinOp.hash Std.Tactic.BVDecide.BVBinOp.umod = 6

Instances For

source
instance Std.Tactic.BVDecide.instDecidableEqBVBinOp :
DecidableEq BVBinOp
Equations

- Std.Tactic.BVDecide.instDecidableEqBVBinOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
def Std.Tactic.BVDecide.BVBinOp.toString :
BVBinOp → String
Equations

- Std.Tactic.BVDecide.BVBinOp.and.toString = "&&"
- Std.Tactic.BVDecide.BVBinOp.or.toString = "||"
- Std.Tactic.BVDecide.BVBinOp.xor.toString = "^"
- Std.Tactic.BVDecide.BVBinOp.add.toString = "+"
- Std.Tactic.BVDecide.BVBinOp.mul.toString = "*"
- Std.Tactic.BVDecide.BVBinOp.udiv.toString = "/ᵤ"
- Std.Tactic.BVDecide.BVBinOp.umod.toString = "%ᵤ"

Instances For

source
instance Std.Tactic.BVDecide.BVBinOp.instToString :
ToString BVBinOp
Equations

- Std.Tactic.BVDecide.BVBinOp.instToString = { toString := Std.Tactic.BVDecide.BVBinOp.toString }

source
def Std.Tactic.BVDecide.BVBinOp.eval {w : Nat} :
BVBinOp → BitVec w → BitVec w → BitVec w

The semantics for `BVBinOp`.

Equations

- Std.Tactic.BVDecide.BVBinOp.and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2
- Std.Tactic.BVDecide.BVBinOp.or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2
- Std.Tactic.BVDecide.BVBinOp.xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2
- Std.Tactic.BVDecide.BVBinOp.add.eval = fun (x1 x2 : BitVec w) => x1 + x2
- Std.Tactic.BVDecide.BVBinOp.mul.eval = fun (x1 x2 : BitVec w) => x1 * x2
- Std.Tactic.BVDecide.BVBinOp.udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2
- Std.Tactic.BVDecide.BVBinOp.umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_and {w : Nat} :
and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_or {w : Nat} :
or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_xor {w : Nat} :
xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_add {w : Nat} :
add.eval = fun (x1 x2 : BitVec w) => x1 + x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_mul {w : Nat} :
mul.eval = fun (x1 x2 : BitVec w) => x1 * x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_udiv {w : Nat} :
udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinOp.eval_umod {w : Nat} :
umod.eval = fun (x1 x2 : BitVec w) => x1 % x2
source
inductive Std.Tactic.BVDecide.BVUnOp :
Type

All supported unary operators on `BVExpr`.

- not : BVUnOp

  Bitwise not.

- rotateLeft (n : Nat) : BVUnOp

  Rotating left by a constant value.

- rotateRight (n : Nat) : BVUnOp

  Rotating right by a constant value.

- arithShiftRightConst (n : Nat) : BVUnOp

  Arithmetic shift right by a constant value.

  This operation has a dedicated constant representation as shiftRight can take `Nat` as a shift amount. We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a constant `Nat` value.

- reverse : BVUnOp

  Reverse the bits in a bitvector.

- clz : BVUnOp

  Count leading zeros.

Instances For

source
instance Std.Tactic.BVDecide.instHashableBVUnOp :
Hashable BVUnOp
Equations

- Std.Tactic.BVDecide.instHashableBVUnOp = { hash := Std.Tactic.BVDecide.instHashableBVUnOp.hash }

source
def Std.Tactic.BVDecide.instHashableBVUnOp.hash :
BVUnOp → UInt64
Equations

- Std.Tactic.BVDecide.instHashableBVUnOp.hash Std.Tactic.BVDecide.BVUnOp.not = 0
- Std.Tactic.BVDecide.instHashableBVUnOp.hash (Std.Tactic.BVDecide.BVUnOp.rotateLeft a) = mixHash 1 (hash a)
- Std.Tactic.BVDecide.instHashableBVUnOp.hash (Std.Tactic.BVDecide.BVUnOp.rotateRight a) = mixHash 2 (hash a)
- Std.Tactic.BVDecide.instHashableBVUnOp.hash (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst a) = mixHash 3 (hash a)
- Std.Tactic.BVDecide.instHashableBVUnOp.hash Std.Tactic.BVDecide.BVUnOp.reverse = 4
- Std.Tactic.BVDecide.instHashableBVUnOp.hash Std.Tactic.BVDecide.BVUnOp.clz = 5

Instances For

source
def Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (x✝ x✝¹ : BVUnOp) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not Std.Tactic.BVDecide.BVUnOp.not = isTrue ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not (Std.Tactic.BVDecide.BVUnOp.rotateRight n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not Std.Tactic.BVDecide.BVUnOp.reverse = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_6
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.not Std.Tactic.BVDecide.BVUnOp.clz = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_7
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) Std.Tactic.BVDecide.BVUnOp.not = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft a) (Std.Tactic.BVDecide.BVUnOp.rotateLeft b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) (Std.Tactic.BVDecide.BVUnOp.rotateRight n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) Std.Tactic.BVDecide.BVUnOp.reverse = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) Std.Tactic.BVDecide.BVUnOp.clz = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight n) Std.Tactic.BVDecide.BVUnOp.not = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight n) (Std.Tactic.BVDecide.BVUnOp.rotateLeft n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight a) (Std.Tactic.BVDecide.BVUnOp.rotateRight b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight n) (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight n) Std.Tactic.BVDecide.BVUnOp.reverse = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.rotateRight n) Std.Tactic.BVDecide.BVUnOp.clz = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) Std.Tactic.BVDecide.BVUnOp.not = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) (Std.Tactic.BVDecide.BVUnOp.rotateLeft n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) (Std.Tactic.BVDecide.BVUnOp.rotateRight n_1) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) Std.Tactic.BVDecide.BVUnOp.reverse = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) Std.Tactic.BVDecide.BVUnOp.clz = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse Std.Tactic.BVDecide.BVUnOp.not = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_26
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse (Std.Tactic.BVDecide.BVUnOp.rotateRight n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse Std.Tactic.BVDecide.BVUnOp.reverse = isTrue ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.reverse Std.Tactic.BVDecide.BVUnOp.clz = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_30
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz Std.Tactic.BVDecide.BVUnOp.not = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_31
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz (Std.Tactic.BVDecide.BVUnOp.rotateRight n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) = isFalse ⋯
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz Std.Tactic.BVDecide.BVUnOp.reverse = isFalse Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq._proof_35
- Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq Std.Tactic.BVDecide.BVUnOp.clz Std.Tactic.BVDecide.BVUnOp.clz = isTrue ⋯

Instances For

source
instance Std.Tactic.BVDecide.instDecidableEqBVUnOp :
DecidableEq BVUnOp
Equations

- Std.Tactic.BVDecide.instDecidableEqBVUnOp = Std.Tactic.BVDecide.instDecidableEqBVUnOp.decEq

source
def Std.Tactic.BVDecide.BVUnOp.toString :
BVUnOp → String
Equations

- Std.Tactic.BVDecide.BVUnOp.not.toString = "~"
- (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).toString = toString "rotL " ++ toString n
- (Std.Tactic.BVDecide.BVUnOp.rotateRight n).toString = toString "rotR " ++ toString n
- (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).toString = toString ">>a " ++ toString n
- Std.Tactic.BVDecide.BVUnOp.reverse.toString = "rev"
- Std.Tactic.BVDecide.BVUnOp.clz.toString = "clz"

Instances For

source
instance Std.Tactic.BVDecide.BVUnOp.instToString :
ToString BVUnOp
Equations

- Std.Tactic.BVDecide.BVUnOp.instToString = { toString := Std.Tactic.BVDecide.BVUnOp.toString }

source
def Std.Tactic.BVDecide.BVUnOp.eval {w : Nat} :
BVUnOp → BitVec w → BitVec w

The semantics for `BVUnOp`.

Equations

- Std.Tactic.BVDecide.BVUnOp.not.eval = fun (x : BitVec w) => ~~~x
- (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n
- (Std.Tactic.BVDecide.BVUnOp.rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n
- (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n
- Std.Tactic.BVDecide.BVUnOp.reverse.eval = BitVec.reverse
- Std.Tactic.BVDecide.BVUnOp.clz.eval = BitVec.clz

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_not {w : Nat} :
not.eval = fun (x : BitVec w) => ~~~x
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft {n w : Nat} :
(rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateRight {n w : Nat} :
(rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_arithShiftRightConst {n w : Nat} :
(arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_reverse {w : Nat} :
reverse.eval = BitVec.reverse
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_clz {w : Nat} :
clz.eval = BitVec.clz
source
inductive Std.Tactic.BVDecide.BVExpr :
Nat → Type

All supported expressions involving `BitVec` and operations on them.

- var {w : Nat} (idx : Nat) : BVExpr w

  A `BitVec` variable, referred to through an index.

- const {w : Nat} (val : BitVec w) : BVExpr w

  A constant `BitVec` value.

- extract {w : Nat} (start len : Nat) (expr : BVExpr w) : BVExpr len

  Extract a slice from a `BitVec`.

- bin {w : Nat} (lhs : BVExpr w) (op : BVBinOp) (rhs : BVExpr w) : BVExpr w

  A binary operation on two `BVExpr`.

- un {w : Nat} (op : BVUnOp) (operand : BVExpr w) : BVExpr w

  A unary operation on two `BVExpr`.

- append {l r w : Nat} (lhs : BVExpr l) (rhs : BVExpr r) (h : w = l + r) : BVExpr w

  Concatenate two bitvectors.

- replicate {w w' : Nat} (n : Nat) (expr : BVExpr w) (h : w' = w * n) : BVExpr w'

  Concatenate a bitvector with itself `n` times.

- shiftLeft {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift left by another BitVec expression. For constant shifts there exists a `BVUnop`.

- shiftRight {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift right by another BitVec expression. For constant shifts there exists a `BVUnop`.

- arithShiftRight {m n : Nat} (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m

  shift right arithmetically by another BitVec expression. For constant shifts there exists a `BVUnop`.

Instances For

source
@[implemented_by Std.Tactic.BVDecide.BVExpr.hashCode._override]
noncomputable def Std.Tactic.BVDecide.BVExpr.hashCode (w : Nat) :
BVExpr w → UInt64
Equations

- One or more equations did not get rendered due to their size.
- Std.Tactic.BVDecide.BVExpr.hashCode x✝ (Std.Tactic.BVDecide.BVExpr.var idx) = mixHash 5 (mixHash (hash x✝) (hash idx))
- Std.Tactic.BVDecide.BVExpr.hashCode x✝ (Std.Tactic.BVDecide.BVExpr.const val) = mixHash 7 (mixHash (hash x✝) (hash val))
- Std.Tactic.BVDecide.BVExpr.hashCode x✝ (Std.Tactic.BVDecide.BVExpr.extract start x✝ expr) = mixHash 11 (mixHash (hash start) (mixHash (hash x✝) (Std.Tactic.BVDecide.BVExpr.hashCode w_1 expr)))
- Std.Tactic.BVDecide.BVExpr.hashCode x✝ (Std.Tactic.BVDecide.BVExpr.un op operand) = mixHash 17 (mixHash (hash x✝) (mixHash (hash op) (Std.Tactic.BVDecide.BVExpr.hashCode x✝ operand)))
- Std.Tactic.BVDecide.BVExpr.hashCode x✝ (Std.Tactic.BVDecide.BVExpr.replicate n expr h) = mixHash 23 (mixHash (hash x✝) (mixHash (hash n) (Std.Tactic.BVDecide.BVExpr.hashCode w_1 expr)))

Instances For

source
instance Std.Tactic.BVDecide.BVExpr.instHashable {w : Nat} :
Hashable (BVExpr w)
Equations

- Std.Tactic.BVDecide.BVExpr.instHashable = { hash := fun (expr : Std.Tactic.BVDecide.BVExpr w) => Std.Tactic.BVDecide.BVExpr.hashCode w expr }

source
instance Std.Tactic.BVDecide.BVExpr.decEq {w : Nat} :
DecidableEq (BVExpr w)
Equations

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

source
def Std.Tactic.BVDecide.BVExpr.toString {w : Nat} :
BVExpr w → String
Equations

- (Std.Tactic.BVDecide.BVExpr.var idx).toString = toString "var" ++ toString idx
- (Std.Tactic.BVDecide.BVExpr.const val).toString = toString val
- (Std.Tactic.BVDecide.BVExpr.extract start w expr).toString = toString expr.toString ++ toString "[" ++ toString start ++ toString ", " ++ toString w ++ toString "]"
- (lhs.bin op rhs).toString = toString "(" ++ toString lhs.toString ++ toString " " ++ toString op.toString ++ toString " " ++ toString rhs.toString ++ toString ")"
- (Std.Tactic.BVDecide.BVExpr.un op operand).toString = toString "(" ++ toString op.toString ++ toString " " ++ toString operand.toString ++ toString ")"
- (lhs.append rhs h).toString = toString "(" ++ toString lhs.toString ++ toString " ++ " ++ toString rhs.toString ++ toString ")"
- (Std.Tactic.BVDecide.BVExpr.replicate n expr h).toString = toString "(replicate " ++ toString n ++ toString " " ++ toString expr.toString ++ toString ")"
- (lhs.shiftLeft rhs).toString = toString "(" ++ toString lhs.toString ++ toString " << " ++ toString rhs.toString ++ toString ")"
- (lhs.shiftRight rhs).toString = toString "(" ++ toString lhs.toString ++ toString " >> " ++ toString rhs.toString ++ toString ")"
- (lhs.arithShiftRight rhs).toString = toString "(" ++ toString lhs.toString ++ toString " >>a " ++ toString rhs.toString ++ toString ")"

Instances For

source
instance Std.Tactic.BVDecide.BVExpr.instToString {w : Nat} :
ToString (BVExpr w)
Equations

- Std.Tactic.BVDecide.BVExpr.instToString = { toString := Std.Tactic.BVDecide.BVExpr.toString }

source
structure Std.Tactic.BVDecide.BVExpr.PackedBitVec :
Type

Pack a `BitVec` with its width into a single parameter-less structure.

- w : Nat
- bv : BitVec self.w

Instances For

source
@[reducible, inline]
abbrev Std.Tactic.BVDecide.BVExpr.Assignment :
Type

The notion of variable assignments for `BVExpr`.

Equations

- Std.Tactic.BVDecide.BVExpr.Assignment = Lean.RArray Std.Tactic.BVDecide.BVExpr.PackedBitVec

Instances For

source
def Std.Tactic.BVDecide.BVExpr.Assignment.get (assign : Assignment) (idx : Nat) :
PackedBitVec

Get the value of a `BVExpr.var` from an `Assignment`.

Equations

- assign.get idx = Lean.RArray.get assign idx

Instances For

source
def Std.Tactic.BVDecide.BVExpr.eval {w : Nat} (assign : Assignment) :
BVExpr w → BitVec w

The semantics for `BVExpr`.

Equations

- Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) = if h : (assign.get idx).w = w then h ▸ (assign.get idx).bv else BitVec.truncate w (assign.get idx).bv
- Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val
- Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.extract start w expr) = BitVec.extractLsb' start w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
- Std.Tactic.BVDecide.BVExpr.eval assign (lhs.bin op rhs) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
- Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.un op operand) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)
- Std.Tactic.BVDecide.BVExpr.eval assign (lhs.append rhs h) = ⋯ ▸ (Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs)
- Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.replicate n expr h) = ⋯ ▸ BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
- Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftLeft rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs
- Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftRight rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs
- Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) = (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_var {assign : Assignment} {w idx : Nat} :
eval assign (var idx) = BitVec.truncate w (assign.get idx).bv
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_const {assign : Assignment} {w✝ : Nat} {val : BitVec w✝} :
eval assign (const val) = val
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_extract {assign : Assignment} {start len a✝ : Nat} {expr : BVExpr a✝} :
eval assign (extract start len expr) = BitVec.extractLsb' start len (eval assign expr)
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_bin {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinOp} {rhs : BVExpr a✝} :
eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_un {assign : Assignment} {op : BVUnOp} {a✝ : Nat} {operand : BVExpr a✝} :
eval assign (un op operand) = op.eval (eval assign operand)
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_append {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} {h : a✝ + a✝¹ = a✝ + a✝¹} :
eval assign (lhs.append rhs h) = eval assign lhs ++ eval assign rhs
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_replicate {assign : Assignment} {n a✝ : Nat} {expr : BVExpr a✝} {h : a✝ * n = a✝ * n} :
eval assign (replicate n expr h) = BitVec.replicate n (eval assign expr)
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_shiftLeft {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
eval assign (lhs.shiftLeft rhs) = eval assign lhs <<< eval assign rhs
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_shiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
eval assign (lhs.shiftRight rhs) = eval assign lhs >>> eval assign rhs
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_arithShiftRight {assign : Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {a✝¹ : Nat} {rhs : BVExpr a✝¹} :
eval assign (lhs.arithShiftRight rhs) = (eval assign lhs).sshiftRight' (eval assign rhs)
source
inductive Std.Tactic.BVDecide.BVBinPred :
Type

Supported binary predicates on `BVExpr`.

- eq : BVBinPred

  Equality.

- ult : BVBinPred

  Unsigned Less Than

Instances For

source
def Std.Tactic.BVDecide.BVBinPred.toString :
BVBinPred → String
Equations

- Std.Tactic.BVDecide.BVBinPred.eq.toString = "=="
- Std.Tactic.BVDecide.BVBinPred.ult.toString = "<u"

Instances For

source
instance Std.Tactic.BVDecide.BVBinPred.instToString :
ToString BVBinPred
Equations

- Std.Tactic.BVDecide.BVBinPred.instToString = { toString := Std.Tactic.BVDecide.BVBinPred.toString }

source
def Std.Tactic.BVDecide.BVBinPred.eval {w : Nat} :
BVBinPred → BitVec w → BitVec w → Bool

The semantics for `BVBinPred`.

Equations

- Std.Tactic.BVDecide.BVBinPred.eq.eval = fun (x1 x2 : BitVec w) => x1 == x2
- Std.Tactic.BVDecide.BVBinPred.ult.eval = BitVec.ult

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVBinPred.eval_eq {w : Nat} :
eq.eval = fun (x1 x2 : BitVec w) => x1 == x2
source
@[simp]
theorem Std.Tactic.BVDecide.BVBinPred.eval_ult {w : Nat} :
ult.eval = BitVec.ult
source
inductive Std.Tactic.BVDecide.BVPred :
Type

Supported predicates on `BVExpr`.

- bin {w : Nat} (lhs : BVExpr w) (op : BVBinPred) (rhs : BVExpr w) : BVPred

  A binary predicate on `BVExpr`.

- getLsbD {w : Nat} (expr : BVExpr w) (idx : Nat) : BVPred

  Getting a constant LSB from a `BitVec`.

Instances For

source
structure Std.Tactic.BVDecide.BVPred.ExprPair :
Type

Pack two `BVExpr` of equivalent width into one parameter-less structure.

- w : Nat
- lhs : BVExpr self.w
- rhs : BVExpr self.w

Instances For

source
def Std.Tactic.BVDecide.BVPred.toString :
BVPred → String
Equations

- One or more equations did not get rendered due to their size.
- (Std.Tactic.BVDecide.BVPred.getLsbD expr idx).toString = toString expr.toString ++ toString "[" ++ toString idx ++ toString "]"

Instances For

source
instance Std.Tactic.BVDecide.BVPred.instToString :
ToString BVPred
Equations

- Std.Tactic.BVDecide.BVPred.instToString = { toString := Std.Tactic.BVDecide.BVPred.toString }

source
def Std.Tactic.BVDecide.BVPred.eval (assign : BVExpr.Assignment) :
BVPred → Bool

The semantics for `BVPred`.

Equations

- Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.bin lhs op rhs) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
- Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.getLsbD expr idx) = (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVPred.eval_bin {assign : BVExpr.Assignment} {a✝ : Nat} {lhs : BVExpr a✝} {op : BVBinPred} {rhs : BVExpr a✝} :
eval assign (bin lhs op rhs) = op.eval (BVExpr.eval assign lhs) (BVExpr.eval assign rhs)
source
@[simp]
theorem Std.Tactic.BVDecide.BVPred.eval_getLsbD {assign : BVExpr.Assignment} {a✝ : Nat} {expr : BVExpr a✝} {idx : Nat} :
eval assign (getLsbD expr idx) = (BVExpr.eval assign expr).getLsbD idx
source
@[reducible, inline]
abbrev Std.Tactic.BVDecide.BVLogicalExpr :
Type

Boolean substructure of problems involving predicates on BitVec as atoms.

Equations

- Std.Tactic.BVDecide.BVLogicalExpr = Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred

Instances For

source
def Std.Tactic.BVDecide.BVLogicalExpr.eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) :
Bool

The semantics of boolean problems involving BitVec predicates as atoms.

Equations

- Std.Tactic.BVDecide.BVLogicalExpr.eval assign expr = Std.Tactic.BVDecide.BoolExpr.eval (fun (x : Std.Tactic.BVDecide.BVPred) => Std.Tactic.BVDecide.BVPred.eval assign x) expr

Instances For

source
@[simp]
theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_literal {assign : BVExpr.Assignment} {pred : BVPred} :
eval assign (BoolExpr.literal pred) = BVPred.eval assign pred
source
@[simp]
theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_const {assign : BVExpr.Assignment} {b : Bool} :
eval assign (BoolExpr.const b) = b
source
@[simp]
theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_not {assign : BVExpr.Assignment} {x : BoolExpr BVPred} :
eval assign x.not = !eval assign x
source
@[simp]
theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_gate {assign : BVExpr.Assignment} {g : Gate} {x y : BoolExpr BVPred} :
eval assign (BoolExpr.gate g x y) = g.eval (eval assign x) (eval assign y)
source
@[simp]
theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_ite {assign : BVExpr.Assignment} {d l r : BoolExpr BVPred} :
eval assign (d.ite l r) = bif eval assign d then eval assign l else eval assign r
source
def Std.Tactic.BVDecide.BVLogicalExpr.Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) :
Prop
Equations

- x.Sat assign = (Std.Tactic.BVDecide.BVLogicalExpr.eval assign x = true)

Instances For

source
def Std.Tactic.BVDecide.BVLogicalExpr.Unsat (x : BVLogicalExpr) :
Prop
Equations

- x.Unsat = ∀ (f : Std.Tactic.BVDecide.BVExpr.Assignment), Std.Tactic.BVDecide.BVLogicalExpr.eval f x = false

Instances For

source
theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_and {x y : BVLogicalExpr} {assign : BVExpr.Assignment} (hx : x.Sat assign) (hy : y.Sat assign) :
Sat (BoolExpr.gate Gate.and x y) assign
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_true {assign : BVExpr.Assignment} :
Sat (BoolExpr.const true) assign