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.

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

instance Std.Tactic.BVDecide.instHashableBVBit : Hashable BVBit

instance Std.Tactic.BVDecide.instDecidableEqBVBit : DecidableEq BVBit

instance Std.Tactic.BVDecide.instReprBVBit : Repr BVBit

instance Std.Tactic.BVDecide.instToStringBVBit : ToString BVBit

instance Std.Tactic.BVDecide.instInhabitedBVBit : Inhabited BVBit

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.

instance Std.Tactic.BVDecide.instHashableBVBinOp : Hashable BVBinOp

instance Std.Tactic.BVDecide.instDecidableEqBVBinOp : DecidableEq BVBinOp

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

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

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

The semantics for BVBinOp.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_udiv {w : Nat} : udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_umod {w : Nat} : umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

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.

instance Std.Tactic.BVDecide.instHashableBVUnOp : Hashable BVUnOp

instance Std.Tactic.BVDecide.instDecidableEqBVUnOp : DecidableEq BVUnOp

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

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

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

The semantics for BVUnOp.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_reverse {w : Nat} : reverse.eval = BitVec.reverse

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.

@[implemented_by Std.Tactic.BVDecide.BVExpr.hashCode._override]

noncomputable def Std.Tactic.BVDecide.BVExpr.hashCode (w : Nat) : BVExpr w → UInt64

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

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

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

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

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.

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

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

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

The semantics for BVExpr.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

inductive Std.Tactic.BVDecide.BVBinPred : Type

Supported binary predicates on BVExpr.

• eq : BVBinPred

  Equality.

• ult : BVBinPred

  Unsigned Less Than

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

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

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

The semantics for BVBinPred.

@[simp]

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

@[simp]

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

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.

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

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

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

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

The semantics for BVPred.

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

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

@[reducible, inline]

abbrev Std.Tactic.BVDecide.BVLogicalExpr : Type

Boolean substructure of problems involving predicates on BitVec as atoms.

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

The semantics of boolean problems involving BitVec predicates as atoms.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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