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

source

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

source

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

source

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

~~~x' = ~~~x

source

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

source

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'

source

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

source

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'

source

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

source

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

source

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

BitVec.zeroExtend n x' = BitVec.zeroExtend n x

source

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

BitVec.signExtend n x' = BitVec.signExtend n x

source

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

source

theorem Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr (n : Nat) (w : Nat) (expr : BitVec w) (expr' : BitVec w) (h : expr' = expr) :

BitVec.replicate n expr' = BitVec.replicate n expr

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

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.Bool.not_congr (x : Bool) (x' : Bool) (h : x' = x) :

(!x') = !x

source

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)

source

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)

source

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)

source

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

False

source

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.

Instances For

source

theorem Std.Tactic.BVDecide.Reflect.verifyCert_correct (cnf : Std.Sat.CNF Nat) (cert : String) :

Std.Tactic.BVDecide.Reflect.verifyCert cnf cert = true → cnf.Unsat

source

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

Instances For

source

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