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

source
theorem Std.Tactic.BVDecide.Reflect.BitVec.and_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' &&& rhs' = lhs &&& rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.or_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ||| rhs' = lhs ||| rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.xor_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ^^^ rhs' = lhs ^^^ rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.not_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
~~~x' = ~~~x
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs <<< rhs = lhs' <<< rhs'
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs >>> rhs = lhs' >>> rhs'
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr (n w : Nat) (x x' : BitVec w) (h : x = x') :
x'.sshiftRight n = x.sshiftRight n
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs.sshiftRight' rhs = lhs'.sshiftRight' rhs'
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.add_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' + rhs' = lhs + rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.append_congr (lw rw : Nat) (lhs lhs' : BitVec lw) (rhs rhs' : BitVec rw) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' ++ rhs' = lhs ++ rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr (n w : Nat) (expr expr' : BitVec w) (h : expr' = expr) :
BitVec.replicate n expr' = BitVec.replicate n expr
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.extract_congr (start len w : Nat) (x x' : BitVec w) (h1 : x = x') :
BitVec.extractLsb' start len x' = BitVec.extractLsb' start len x
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr (n w : Nat) (x x' : BitVec w) (h : x = x') :
x'.rotateLeft n = x.rotateLeft n
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr (n w : Nat) (x x' : BitVec w) (h : x = x') :
x'.rotateRight n = x.rotateRight n
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.mul_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' * rhs' = lhs * rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.beq_congr {w : Nat} (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' == rhs') = (lhs == rhs)
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.ult_congr {w : Nat} (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs'.ult rhs' = lhs.ult rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr (i w : Nat) (e e' : BitVec w) (h : e' = e) :
e'.getLsbD i = e.getLsbD i
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) :
e'.getLsbD 0 = b
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr {w : Nat} (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' / rhs' = lhs / rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.umod_congr {w : Nat} (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
lhs' % rhs' = lhs % rhs
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.cond_true {w : Nat} (discr : Bool) (lhs rhs : BitVec w) :
(!discr || (bif discr then lhs else rhs) == lhs) = true
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.cond_false {w : Nat} (discr : Bool) (lhs rhs : BitVec w) :
(discr || (bif discr then lhs else rhs) == rhs) = true
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
x'.reverse = x.reverse
source
theorem Std.Tactic.BVDecide.Reflect.BitVec.clz_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
x'.clz = x.clz
source
theorem Std.Tactic.BVDecide.Reflect.Bool.not_congr (x x' : Bool) (h : x' = x) :
(!x') = !x
source
theorem Std.Tactic.BVDecide.Reflect.Bool.and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' && rhs') = (lhs && rhs)
source
theorem Std.Tactic.BVDecide.Reflect.Bool.xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' ^^ rhs') = (lhs ^^ rhs)
source
theorem Std.Tactic.BVDecide.Reflect.Bool.beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' == rhs') = (lhs == rhs)
source
theorem Std.Tactic.BVDecide.Reflect.Bool.or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(lhs' || rhs') = (lhs || rhs)
source
theorem Std.Tactic.BVDecide.Reflect.Bool.cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs) (h3 : rhs' = rhs) :
(bif discr' then lhs' else rhs') = bif discr then lhs else rhs
source
theorem Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false {x : Bool} (h₁ : x = true) (h₂ : x = false) :
False
source
theorem Std.Tactic.BVDecide.Reflect.Bool.lemma_congr (x x' : Bool) (h1 : x' = x) (h2 : x = true) :
x' = true
source
def Std.Tactic.BVDecide.Reflect.verifyCert (cnf : Sat.CNF Nat) (cert : String) :
Bool

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

source
theorem Std.Tactic.BVDecide.Reflect.verifyCert_correct (cnf : Sat.CNF Nat) (cert : String) :
verifyCert cnf cert = true → cnf.Unsat
source
def Std.Tactic.BVDecide.Reflect.verifyBVExpr (bv : BVLogicalExpr) (cert : String) :
Bool

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

Equations

- Std.Tactic.BVDecide.Reflect.verifyBVExpr bv cert = Std.Tactic.BVDecide.Reflect.verifyCert (Std.Sat.AIG.toCNF bv.bitblast.relabelNat) cert

Instances For

source
theorem Std.Tactic.BVDecide.Reflect.unsat_of_verifyBVExpr_eq_true (bv : BVLogicalExpr) (c : String) (h : verifyBVExpr bv c = true) :
bv.Unsat