Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Basic

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 :

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.

Instances For

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 :

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.
udiv : Std.Tactic.BVDecide.BVBinOp
Unsigned division.
umod : Std.Tactic.BVDecide.BVBinOp
Unsigned modulo.

Instances For

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 = "*"
Std.Tactic.BVDecide.BVBinOp.udiv.toString = "/ᵤ"
Std.Tactic.BVDecide.BVBinOp.umod.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
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

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

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_udiv {w : Nat} :

Std.Tactic.BVDecide.BVBinOp.udiv.eval = fun (x1 x2 : BitVec w) => x1 / x2

@[simp]

theorem Std.Tactic.BVDecide.BVBinOp.eval_umod {w : Nat} :

Std.Tactic.BVDecide.BVBinOp.umod.eval = fun (x1 x2 : BitVec w) => x1 % x2

inductive Std.Tactic.BVDecide.BVUnOp :

All supported unary operators on BVExpr.

not : Std.Tactic.BVDecide.BVUnOp
Bitwise not.
shiftLeftConst (n : 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 (n : 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 (n : Nat) : Std.Tactic.BVDecide.BVUnOp
Rotating left by a constant value.
rotateRight (n : Nat) : Std.Tactic.BVDecide.BVUnOp
Rotating right by a constant value.
arithShiftRightConst (n : 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.

Instances For

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 w : Nat} :

(Std.Tactic.BVDecide.BVUnOp.shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftRightConst {n w : Nat} :

(Std.Tactic.BVDecide.BVUnOp.shiftRightConst n).eval = fun (x : BitVec w) => x >>> n

@[simp]

theorem Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft {n 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 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 w : Nat} :

(Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n).eval = fun (x : BitVec w) => x.sshiftRight n

inductive Std.Tactic.BVDecide.BVExpr :

All supported expressions involving BitVec and operations on them.

var {w : Nat} (idx : Nat) : Std.Tactic.BVDecide.BVExpr w
A BitVec variable, referred to through an index.
const {w : Nat} (val : BitVec w) : Std.Tactic.BVDecide.BVExpr w
A constant BitVec value.
zeroExtend {w : Nat} (v : Nat) (expr : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr v
zero extend a BitVec by some constant amount.
extract {w : Nat} (start len : Nat) (expr : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr len
Extract a slice from a BitVec.
bin {w : Nat} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinOp) (rhs : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr w
A binary operation on two BVExpr.
un {w : Nat} (op : Std.Tactic.BVDecide.BVUnOp) (operand : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr w
A unary operation on two BVExpr.
append {l r : Nat} (lhs : Std.Tactic.BVDecide.BVExpr l) (rhs : Std.Tactic.BVDecide.BVExpr r) : Std.Tactic.BVDecide.BVExpr (l + r)
Concatenate two bit vectors.
replicate {w : Nat} (n : Nat) (expr : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr (w * n)
Concatenate a bit vector with itself n times.
signExtend {w : Nat} (v : Nat) (expr : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVExpr v
sign extend a BitVec by some constant amount.
shiftLeft {m n : Nat} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : 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} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n) : Std.Tactic.BVDecide.BVExpr m
shift right by another BitVec expression. For constant shifts there exists a BVUnop.
arithShiftRight {m n : Nat} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n) : Std.Tactic.BVDecide.BVExpr m
shift right arithmetically by another BitVec expression. For constant shifts there exists a BVUnop.

Instances For

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 ")"
(lhs.arithShiftRight rhs).toString = toString "(" ++ toString lhs.toString ++ toString " >>a " ++ 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 :

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 :

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
Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) = (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.eval_var {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w 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 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 len 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✝¹ : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a✝¹} :

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 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 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✝¹ : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a✝¹} :

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✝¹ : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a✝¹} :

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_arithShiftRight {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a✝ : Nat} {lhs : Std.Tactic.BVDecide.BVExpr a✝} {a✝¹ : Nat} {rhs : Std.Tactic.BVDecide.BVExpr a✝¹} :

Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) = (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)

inductive Std.Tactic.BVDecide.BVBinPred :

Supported binary predicates on BVExpr.

eq : Std.Tactic.BVDecide.BVBinPred
Equality.
ult : Std.Tactic.BVDecide.BVBinPred
Unsigned Less Than

Instances For

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 :

Supported predicates on BVExpr.

bin {w : Nat} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinPred) (rhs : Std.Tactic.BVDecide.BVExpr w) : Std.Tactic.BVDecide.BVPred
A binary predicate on BVExpr.
getLsbD {w : Nat} (expr : Std.Tactic.BVDecide.BVExpr w) (idx : Nat) : Std.Tactic.BVDecide.BVPred
Getting a constant LSB from a BitVec.

Instances For

structure Std.Tactic.BVDecide.BVPred.ExprPair :

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

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 :

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) :

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

@[simp]

theorem Std.Tactic.BVDecide.BVLogicalExpr.eval_ite {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {d l r : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred} :

Std.Tactic.BVDecide.BVLogicalExpr.eval assign (d.ite l r) = if Std.Tactic.BVDecide.BVLogicalExpr.eval assign d = true then Std.Tactic.BVDecide.BVLogicalExpr.eval assign l else Std.Tactic.BVDecide.BVLogicalExpr.eval assign r

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

Equations

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

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

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