Documentation

Std.Tactic.BVDecide.Reflect

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 : 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
    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