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

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

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

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

theorem Std.Tactic.BVDecide.Reflect.BitVec.not_congr (w : Nat) (x x' : BitVec w) (h : x = x') : ~~~x' = ~~~x

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'

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'

theorem Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr (n w : Nat) (x x' : BitVec w) (h : x = x') : x'.sshiftRight n = x.sshiftRight n

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'

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

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

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

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

theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr (n w : Nat) (x x' : BitVec w) (h : x = x') : x'.rotateLeft n = x.rotateLeft n

theorem Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr (n w : Nat) (x x' : BitVec w) (h : x = x') : x'.rotateRight n = x.rotateRight n

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

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)

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

theorem Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr (i w : Nat) (e 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.BitVec.udiv_congr {w : Nat} (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : lhs' / rhs' = lhs / rhs

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

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

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

theorem Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr (w : Nat) (x x' : BitVec w) (h : x = x') : x'.reverse = x.reverse

theorem Std.Tactic.BVDecide.Reflect.BitVec.clz_congr (w : Nat) (x x' : BitVec w) (h : x = x') : x'.clz = x.clz

theorem Std.Tactic.BVDecide.Reflect.BitVec.cpop_congr (w : Nat) (x x' : BitVec w) (h : x = x') : x'.cpop = x.cpop

theorem Std.Tactic.BVDecide.Reflect.Bool.not_congr (x x' : Bool) (h : x' = x) : (!x') = !x

theorem Std.Tactic.BVDecide.Reflect.Bool.and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : (lhs' && rhs') = (lhs && rhs)

theorem Std.Tactic.BVDecide.Reflect.Bool.xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : (lhs' ^^ rhs') = (lhs ^^ rhs)

theorem Std.Tactic.BVDecide.Reflect.Bool.beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : (lhs' == rhs') = (lhs == rhs)

theorem Std.Tactic.BVDecide.Reflect.Bool.or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : (lhs' || rhs') = (lhs || rhs)

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

theorem Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false {x : Bool} (h₁ : x = true) (h₂ : x = false) : False

theorem Std.Tactic.BVDecide.Reflect.Bool.lemma_congr (x x' : Bool) (h1 : x' = x) (h2 : x = true) : x' = true

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.

theorem Std.Tactic.BVDecide.Reflect.verifyCert_correct (cnf : Sat.CNF Nat) (cert : String) : verifyCert cnf cert = true → cnf.Unsat

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

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