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.

structure Std.Tactic.BVDecide.BVBit : Type

The variable definition used by the bitblaster.

• w : Nat

  The width of the BitVec variable.

• var : Nat

  A numeric identifier for the BitVec variable.

• idx : Fin self.w

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

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

Equations

• Std.Tactic.BVDecide.instHashableBVBit = { hash := Std.Tactic.BVDecide.hashBVBit✝ }

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

Equations

• Std.Tactic.BVDecide.instDecidableEqBVBit = Std.Tactic.BVDecide.decEqBVBit✝

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

Equations

• Std.Tactic.BVDecide.instReprBVBit = { reprPrec := Std.Tactic.BVDecide.reprBVBit✝ }

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

Equations

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

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

Equations

• Std.Tactic.BVDecide.instInhabitedBVBit = { default := Std.Tactic.BVDecide.BVBit.mk 0 0 }

inductive Std.Tactic.BVDecide.BVBinOp : Type

All supported binary operations on BVExpr.

• and: Std.Tactic.BVDecide.BVBinOp

  Bitwise and.

• or: Std.Tactic.BVDecide.BVBinOp

  Bitwise or.

• xor: Std.Tactic.BVDecide.BVBinOp

  Bitwise xor.

• add: Std.Tactic.BVDecide.BVBinOp

  Addition.

• mul: Std.Tactic.BVDecide.BVBinOp

  Multiplication.

def Std.Tactic.BVDecide.BVBinOp.toString : Std.Tactic.BVDecide.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 = "*"

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

Equations

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

def Std.Tactic.BVDecide.BVBinOp.eval {w : Nat} : Std.Tactic.BVDecide.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

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_and {w : Nat} : Std.Tactic.BVDecide.BVBinOp.and.eval = fun (x1 x2 : BitVec w) => x1 &&& x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_or {w : Nat} : Std.Tactic.BVDecide.BVBinOp.or.eval = fun (x1 x2 : BitVec w) => x1 ||| x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_xor {w : Nat} : Std.Tactic.BVDecide.BVBinOp.xor.eval = fun (x1 x2 : BitVec w) => x1 ^^^ x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_add {w : Nat} : Std.Tactic.BVDecide.BVBinOp.add.eval = fun (x1 x2 : BitVec w) => x1 + x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_mul {w : Nat} : Std.Tactic.BVDecide.BVBinOp.mul.eval = fun (x1 x2 : BitVec w) => x1 * x2

inductive Std.Tactic.BVDecide.BVUnOp : Type

All supported unary operators on BVExpr.

• not: Std.Tactic.BVDecide.BVUnOp

  Bitwise not.

• shiftLeftConst: Nat → Std.Tactic.BVDecide.BVUnOp

  Shifting left by a constant value.

  This operation has a dedicated constant representation as shiftLeft 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.

• shiftRightConst: Nat → Std.Tactic.BVDecide.BVUnOp

  Shifting 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.

• rotateLeft: Nat → Std.Tactic.BVDecide.BVUnOp

  Rotating left by a constant value.

• rotateRight: Nat → Std.Tactic.BVDecide.BVUnOp

  Rotating right by a constant value.

• arithShiftRightConst: Nat → Std.Tactic.BVDecide.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.

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

Equations

• Std.Tactic.BVDecide.BVUnOp.not.toString = "~"
• (Std.Tactic.BVDecide.BVUnOp.shiftLeftConst n).toString = toString "<< " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).toString = toString ">> " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).toString = toString "rotL " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.rotateRight n).toString = toString "rotR " ++ toString n ++ toString ""
• (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).toString = toString ">>a " ++ toString n ++ toString ""

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

Equations

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

def Std.Tactic.BVDecide.BVUnOp.eval {w : Nat} : Std.Tactic.BVDecide.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.shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n
• (Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).eval = fun (x : BitVec w) => x >>> n
• (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

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_not {w : Nat} : Std.Tactic.BVDecide.BVUnOp.not.eval = fun (x : BitVec w) => ~~~x

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftLeftConst {n : Nat} {w : Nat} : (Std.Tactic.BVDecide.BVUnOp.shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftRightConst {n : Nat} {w : Nat} : (Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).eval = fun (x : BitVec w) => x >>> n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft {n : Nat} {w : Nat} : (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).eval = fun (x : BitVec w) => x.rotateLeft n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateRight {n : Nat} {w : Nat} : (Std.Tactic.BVDecide.BVUnOp.rotateRight n).eval = fun (x : BitVec w) => x.rotateRight n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_arithShiftRightConst {n : Nat} {w : Nat} : (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n

inductive Std.Tactic.BVDecide.BVExpr : Nat → Type

All supported expressions involving BitVec and operations on them.

• var: {w : Nat} → Nat → Std.Tactic.BVDecide.BVExpr w

  A BitVec variable, referred to through an index.

• const: {w : Nat} → BitVec w → Std.Tactic.BVDecide.BVExpr w

  A constant BitVec value.

• zeroExtend: {w : Nat} → (v : Nat) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr v

  zero extend a BitVec by some constant amount.

• extract: {w : Nat} → Nat → (len : Nat) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr len

  Extract a slice from a BitVec.

• bin: {w : Nat} → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVBinOp → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr w

  A binary operation on two BVExpr.

• un: {w : Nat} → Std.Tactic.BVDecide.BVUnOp → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr w

  A unary operation on two BVExpr.

• append: {l r : Nat} → Std.Tactic.BVDecide.BVExpr l → Std.Tactic.BVDecide.BVExpr r → Std.Tactic.BVDecide.BVExpr (l + r)

  Concatenate two bit vectors.

• replicate: {w : Nat} → (n : Nat) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr (w * n)

  Concatenate a bit vector with itself n times.

• signExtend: {w : Nat} → (v : Nat) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr v

  sign extend a BitVec by some constant amount.

• shiftLeft: {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m

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

• shiftRight: {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m

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

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

Equations

• (Std.Tactic.BVDecide.BVExpr.var idx).toString = toString "var" ++ toString idx ++ toString ""
• (Std.Tactic.BVDecide.BVExpr.const val).toString = toString val
• (Std.Tactic.BVDecide.BVExpr.zeroExtend w expr).toString = toString "(zext " ++ toString w ++ toString " " ++ toString expr.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.extract start w expr).toString = 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).toString = toString "(" ++ toString lhs.toString ++ toString " ++ " ++ toString rhs.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.replicate n expr).toString = toString "(replicate " ++ toString n ++ toString " " ++ toString expr.toString ++ toString ")"
• (Std.Tactic.BVDecide.BVExpr.signExtend w expr).toString = toString "(sext " ++ toString w ++ 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 ")"

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

Equations

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

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

@[reducible, inline]

abbrev Std.Tactic.BVDecide.BVExpr.Assignment : Type

The notion of variable assignments for BVExpr.

Equations

• Std.Tactic.BVDecide.BVExpr.Assignment = List Std.Tactic.BVDecide.BVExpr.PackedBitVec

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

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

Equations

• assign.getD idx = List.getD assign idx (Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk (BitVec.zero 0))

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

The semantics for BVExpr.

Equations

• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) = match assign.getD idx with | Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk bv => BitVec.truncate w bv
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.zeroExtend w expr) = BitVec.zeroExtend w (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• 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) = 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) = BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
• Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.signExtend w expr) = BitVec.signExtend w (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

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_var {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w : Nat} {idx : Nat} : Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) = BitVec.truncate w (assign.getD idx).bv

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_const {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {w : Nat} {val : BitVec w}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_zeroExtend {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {v : Nat} : ∀ {a : Nat} {expr : Std.Tactic.BVDecide.BVExpr a}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.zeroExtend v expr) = BitVec.zeroExtend v (Std.Tactic.BVDecide.BVExpr.eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_extract {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {start : Nat} {len : Nat} : ∀ {a : Nat} {expr : Std.Tactic.BVDecide.BVExpr a}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.extract start len expr) = BitVec.extractLsb' start len (Std.Tactic.BVDecide.BVExpr.eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_bin {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a} {op : Std.Tactic.BVDecide.BVBinOp} {rhs : Std.Tactic.BVDecide.BVExpr a}, 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)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_un {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {op : Std.Tactic.BVDecide.BVUnOp} : ∀ {a : Nat} {operand : Std.Tactic.BVDecide.BVExpr a}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.un op operand) = op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_append {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a_1}, Std.Tactic.BVDecide.BVExpr.eval assign (lhs.append rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_replicate {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {n : Nat} : ∀ {a : Nat} {expr : Std.Tactic.BVDecide.BVExpr a}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.replicate n expr) = BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_signExtend {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {v : Nat} : ∀ {a : Nat} {expr : Std.Tactic.BVDecide.BVExpr a}, Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.signExtend v expr) = BitVec.signExtend v (Std.Tactic.BVDecide.BVExpr.eval assign expr)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_shiftLeft {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a_1}, Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftLeft rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_shiftRight {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a_1}, Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftRight rhs) = Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs

inductive Std.Tactic.BVDecide.BVBinPred : Type

Supported binary predicates on BVExpr.

• eq: Std.Tactic.BVDecide.BVBinPred

  Equality.

• ult: Std.Tactic.BVDecide.BVBinPred

  Unsigned Less Than

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

Equations

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

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

Equations

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

def Std.Tactic.BVDecide.BVBinPred.eval {w : Nat} : Std.Tactic.BVDecide.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

@[simp]

theorem Std.Tactic.BVDecide.BVBinPred.eval_eq {w : Nat} : Std.Tactic.BVDecide.BVBinPred.eq.eval = fun (x1 x2 : BitVec w) => x1 == x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinPred.eval_ult {w : Nat} : Std.Tactic.BVDecide.BVBinPred.ult.eval = BitVec.ult

inductive Std.Tactic.BVDecide.BVPred : Type

Supported predicates on BVExpr.

• bin: {w : Nat} → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVBinPred → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVPred

  A binary predicate on BVExpr.

• getLsbD: {w : Nat} → Std.Tactic.BVDecide.BVExpr w → Nat → Std.Tactic.BVDecide.BVPred

  Getting a constant LSB from a BitVec.

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

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

• w : Nat
• lhs : Std.Tactic.BVDecide.BVExpr self.w
• rhs : Std.Tactic.BVDecide.BVExpr self.w

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

Equations

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

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

Equations

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

def Std.Tactic.BVDecide.BVPred.eval (assign : Std.Tactic.BVDecide.BVExpr.Assignment) : Std.Tactic.BVDecide.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

@[simp]

theorem Std.Tactic.BVDecide.BVPred.eval_bin {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a} {op : Std.Tactic.BVDecide.BVBinPred} {rhs : Std.Tactic.BVDecide.BVExpr a}, 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)

@[simp]

theorem Std.Tactic.BVDecide.BVPred.eval_getLsbD {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : ∀ {a : Nat} {expr : Std.Tactic.BVDecide.BVExpr a} {idx : Nat}, Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.getLsbD expr idx) = (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx

@[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

def Std.Tactic.BVDecide.BVLogicalExpr.eval (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (expr : Std.Tactic.BVDecide.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

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_literal {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {pred : Std.Tactic.BVDecide.BVPred} : Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.literal pred) = Std.Tactic.BVDecide.BVPred.eval assign pred

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_const {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {b : Bool} : Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.const b) = b

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_not {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {x : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred} : Std.Tactic.BVDecide.BVLogicalExpr.eval assign x.not = !Std.Tactic.BVDecide.BVLogicalExpr.eval assign x

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_gate {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {g : Std.Tactic.BVDecide.Gate} {x : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred} {y : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred} : Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.gate g x y) = g.eval (Std.Tactic.BVDecide.BVLogicalExpr.eval assign x) (Std.Tactic.BVDecide.BVLogicalExpr.eval assign y)

def Std.Tactic.BVDecide.BVLogicalExpr.Sat (x : Std.Tactic.BVDecide.BVLogicalExpr) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) : Prop

Equations

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

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

Equations

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

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

theorem Std.Tactic.BVDecide.BVLogicalExpr.sat_true {assign : Std.Tactic.BVDecide.BVExpr.Assignment} : Std.Tactic.BVDecide.BVLogicalExpr.Sat (Std.Tactic.BVDecide.BoolExpr.const true) assign