Documentation

Std.Tactic.BVDecide.Reflect

This file contains theorems used for justifying the reflection procedure of bv_decide.

theorem Std.Tactic.BVDecide.Reflect.BitVec.and_congr (w : Nat) (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' &&& rhs' = lhs &&& rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.or_congr (w : Nat) (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ||| rhs' = lhs ||| rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.xor_congr (w : Nat) (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ^^^ rhs' = lhs ^^^ rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.not_congr (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
~~~x' = ~~~x
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr (n : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
x' <<< n = x <<< n
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr (m : Nat) (n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs <<< rhs = lhs' <<< rhs'
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr (n : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
x' >>> n = x >>> n
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr (m : Nat) (n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs >>> rhs = lhs' >>> rhs'
theorem Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr (n : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
x'.sshiftRight n = x.sshiftRight n
theorem Std.Tactic.BVDecide.Reflect.BitVec.add_congr (w : Nat) (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' + rhs' = lhs + rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.append_congr (lw : Nat) (rw : Nat) (lhs : BitVec lw) (lhs' : BitVec lw) (rhs : BitVec rw) (rhs' : BitVec rw) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ++ rhs' = lhs ++ rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr (n : Nat) (w : Nat) (expr : BitVec w) (expr' : BitVec w) (h : expr' = expr) :
theorem Std.Tactic.BVDecide.Reflect.BitVec.extract_congr (start : Nat) (len : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h1 : x = x') :
BitVec.extractLsb' start len x' = BitVec.extractLsb' start len x
theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr (n : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
x'.rotateLeft n = x.rotateLeft n
theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr (n : Nat) (w : Nat) (x : BitVec w) (x' : BitVec w) (h : x = x') :
x'.rotateRight n = x.rotateRight n
theorem Std.Tactic.BVDecide.Reflect.BitVec.mul_congr (w : Nat) (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' * rhs' = lhs * rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.beq_congr {w : Nat} (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' == rhs') = (lhs == rhs)
theorem Std.Tactic.BVDecide.Reflect.BitVec.ult_congr {w : Nat} (lhs : BitVec w) (rhs : BitVec w) (lhs' : BitVec w) (rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs'.ult rhs' = lhs.ult rhs
theorem Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr (i : Nat) (w : Nat) (e : BitVec w) (e' : BitVec w) (h : e' = e) :
e'.getLsbD i = e.getLsbD i
theorem Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) :
e'.getLsbD 0 = b
theorem Std.Tactic.BVDecide.Reflect.Bool.not_congr (x : Bool) (x' : Bool) (h : x' = x) :
(!x') = !x
theorem Std.Tactic.BVDecide.Reflect.Bool.and_congr (lhs : Bool) (rhs : Bool) (lhs' : Bool) (rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' && rhs') = (lhs && rhs)
theorem Std.Tactic.BVDecide.Reflect.Bool.xor_congr (lhs : Bool) (rhs : Bool) (lhs' : Bool) (rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' ^^ rhs') = (lhs ^^ rhs)
theorem Std.Tactic.BVDecide.Reflect.Bool.beq_congr (lhs : Bool) (rhs : Bool) (lhs' : Bool) (rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' == rhs') = (lhs == rhs)

Verify that a proof certificate is valid for a given formula.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Verify that cert is an UNSAT proof for the SAT problem obtained by bitblasting bv.

    Equations
    Instances For