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.shiftLeftNat_congr (n w : Nat) (x x' : BitVec w) (h : x = x') : x' <<< n = x <<< n

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.shiftRightNat_congr (n w : Nat) (x x' : BitVec w) (h : x = x') : x' >>> n = x >>> n

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.zeroExtend_congr (n w : Nat) (x x' : BitVec w) (h1 : x = x') : BitVec.zeroExtend n x' = BitVec.zeroExtend n x

theorem Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr (n w : Nat) (x x' : BitVec w) (h1 : x = x') : BitVec.signExtend n x' = BitVec.signExtend n x

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.if_true {w : Nat} (discr : Bool) (lhs rhs : BitVec w) : decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true

theorem Std.Tactic.BVDecide.Reflect.BitVec.if_false {w : Nat} (discr : Bool) (lhs rhs : BitVec w) : decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true

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.imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) : decide (lhs' = true → rhs' = true) = decide (lhs = true → rhs = true)

theorem Std.Tactic.BVDecide.Reflect.Bool.ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs) (h3 : rhs' = rhs) : (if discr' = true then lhs' else rhs') = if discr = true 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 : Std.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 : Std.Sat.CNF Nat) (cert : String) : Std.Tactic.BVDecide.Reflect.verifyCert cnf cert = true → cnf.Unsat

def Std.Tactic.BVDecide.Reflect.verifyBVExpr (bv : Std.Tactic.BVDecide.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 : Std.Tactic.BVDecide.BVLogicalExpr) (c : String) (h : Std.Tactic.BVDecide.Reflect.verifyBVExpr bv c = true) : bv.Unsat