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.

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
source
instance Std.Tactic.BVDecide.instDecidableEqBVBit :
DecidableEq BVBit
Equations
source
instance Std.Tactic.BVDecide.instReprBVBit :
Repr BVBit
Equations
source
instance Std.Tactic.BVDecide.instToStringBVBit :
ToString BVBit
Equations
source
instance Std.Tactic.BVDecide.instInhabitedBVBit :
Inhabited BVBit
Equations
source
inductive Std.Tactic.BVDecide.BVBinOp :
Type

All supported binary operations on BVExpr.

Instances For
source
def Std.Tactic.BVDecide.BVBinOp.toString :
BVBinOp → String
Equations
source
instance Std.Tactic.BVDecide.BVBinOp.instToString :
ToString BVBinOp
Equations
source
def Std.Tactic.BVDecide.BVBinOp.eval {w : Nat} :
BVBinOp → BitVec w → BitVec w → BitVec w

The semantics for BVBinOp.

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

  • shiftLeftConst (n : Nat) : 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) : 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) : 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.

Instances For
source
def Std.Tactic.BVDecide.BVUnOp.toString :
BVUnOp → String
Equations
source
instance Std.Tactic.BVDecide.BVUnOp.instToString :
ToString BVUnOp
Equations
source
def Std.Tactic.BVDecide.BVUnOp.eval {w : Nat} :
BVUnOp → BitVec w → BitVec w

The semantics for BVUnOp.

Equations
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_shiftLeftConst {n w : Nat} :
(shiftLeftConst n).eval = fun (x : BitVec w) => x <<< n
source
@[simp]
theorem Std.Tactic.BVDecide.BVUnOp.eval_shiftRightConst {n w : Nat} :
(shiftRightConst n).eval = fun (x : BitVec w) => x >>> n
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
inductive Std.Tactic.BVDecide.BVExpr :
Nat → Type

All supported expressions involving BitVec and operations on them.

Instances For
source
def Std.Tactic.BVDecide.BVExpr.toString {w : Nat} :
BVExpr w → String
Equations
source
instance Std.Tactic.BVDecide.BVExpr.instToString {w : Nat} :
ToString (BVExpr w)
Equations
source
structure Std.Tactic.BVDecide.BVExpr.PackedBitVec :
Type

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

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

The notion of variable assignments for BVExpr.

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

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

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

The semantics for BVExpr.

Equations
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_zeroExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} :
eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)
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✝¹} :
eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_replicate {assign : Assignment} {n a✝ : Nat} {expr : BVExpr a✝} :
eval assign (replicate n expr) = BitVec.replicate n (eval assign expr)
source
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.eval_signExtend {assign : Assignment} {v a✝ : Nat} {expr : BVExpr a✝} :
eval assign (signExtend v expr) = BitVec.signExtend v (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.

Instances For
source
def Std.Tactic.BVDecide.BVBinPred.toString :
BVBinPred → String
Equations
source
instance Std.Tactic.BVDecide.BVBinPred.instToString :
ToString BVBinPred
Equations
source
def Std.Tactic.BVDecide.BVBinPred.eval {w : Nat} :
BVBinPred → BitVec w → BitVec w → Bool

The semantics for BVBinPred.

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

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

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

source
def Std.Tactic.BVDecide.BVPred.toString :
BVPred → String
Equations
source
instance Std.Tactic.BVDecide.BVPred.instToString :
ToString BVPred
Equations
source
def Std.Tactic.BVDecide.BVPred.eval (assign : BVExpr.Assignment) :
BVPred → Bool

The semantics for BVPred.

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

The semantics of boolean problems involving BitVec predicates as atoms.

Equations
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
source
def Std.Tactic.BVDecide.BVLogicalExpr.Unsat (x : BVLogicalExpr) :
Prop
Equations
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