Documentation

Init.Data.BitVec.Bitblast

Bitblasting of bitvectors #

This module provides theorems for showing the equivalence between BitVec operations using the Fin 2^n representation and Boolean vectors. It is still under development, but intended to provide a path for converting SAT and SMT solver proofs about BitVectors as vectors of bits into proofs about Lean BitVec values.

The module is named for the bit-blasting operation in an SMT solver that converts bitvector expressions into expressions about individual bits in each vector.

Main results #

Future work #

All other operations are to be PR'ed later and are already proved in https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.

@[reducible, inline]
abbrev Bool.atLeastTwo (a : Bool) (b : Bool) (c : Bool) :

At least two out of three booleans are true.

Equations
Instances For
    @[simp]
    theorem Bool.atLeastTwo_false_left {b : Bool} {c : Bool} :
    false.atLeastTwo b c = (b && c)
    @[simp]
    theorem Bool.atLeastTwo_false_mid {a : Bool} {c : Bool} :
    a.atLeastTwo false c = (a && c)
    @[simp]
    theorem Bool.atLeastTwo_false_right {a : Bool} {b : Bool} :
    a.atLeastTwo b false = (a && b)
    @[simp]
    theorem Bool.atLeastTwo_true_left {b : Bool} {c : Bool} :
    true.atLeastTwo b c = (b || c)
    @[simp]
    theorem Bool.atLeastTwo_true_mid {a : Bool} {c : Bool} :
    a.atLeastTwo true c = (a || c)
    @[simp]
    theorem Bool.atLeastTwo_true_right {a : Bool} {b : Bool} :
    a.atLeastTwo b true = (a || b)

    Preliminaries #

    Addition #

    def BitVec.carry {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) :

    carry i x y c returns true if the i carry bit is true when computing x + y + c.

    Equations
    Instances For
      @[simp]
      theorem BitVec.carry_zero :
      ∀ {w : Nat} {x y : BitVec w} {c : Bool}, BitVec.carry 0 x y c = c
      theorem BitVec.carry_succ {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) :
      BitVec.carry (i + 1) x y c = (x.getLsb i).atLeastTwo (y.getLsb i) (BitVec.carry i x y c)
      def BitVec.adcb (x : Bool) (y : Bool) (c : Bool) :

      Carry function for bitwise addition.

      Equations
      Instances For
        def BitVec.adc {w : Nat} (x : BitVec w) (y : BitVec w) :

        Bitwise addition implemented via a ripple carry adder.

        Equations
        Instances For
          theorem BitVec.getLsb_add_add_bool {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) (c : Bool) :
          (x + y + BitVec.zeroExtend w (BitVec.ofBool c)).getLsb i = (x.getLsb i).xor ((y.getLsb i).xor (BitVec.carry i x y c))
          theorem BitVec.getLsb_add {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) :
          (x + y).getLsb i = (x.getLsb i).xor ((y.getLsb i).xor (BitVec.carry i x y false))
          theorem BitVec.adc_spec {w : Nat} (x : BitVec w) (y : BitVec w) (c : Bool) :
          x.adc y c = (BitVec.carry w x y c, x + y + BitVec.zeroExtend w (BitVec.ofBool c))
          theorem BitVec.add_eq_adc (w : Nat) (x : BitVec w) (y : BitVec w) :
          x + y = (x.adc y false).snd

          add #

          @[simp]
          theorem BitVec.add_not_self {w : Nat} (x : BitVec w) :

          Adding a bitvector to its own complement yields the all ones bitpattern

          Subtracting x from the all ones bitvector is equivalent to taking its complement

          Negation #

          theorem BitVec.bit_not_testBit {w : Nat} (x : BitVec w) (i : Fin w) :
          (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb i)) ()).snd.getLsb i = !x.getLsb i
          theorem BitVec.bit_not_add_self {w : Nat} (x : BitVec w) :
          (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb i)) ()).snd + x = -1
          theorem BitVec.bit_not_eq_not {w : Nat} (x : BitVec w) :
          (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb i)) ()).snd = ~~~x
          theorem BitVec.bit_neg_eq_neg {w : Nat} (x : BitVec w) :
          -x = ((BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb i)) ()).snd.adc (1#w) false).snd

          Inequalities (le / lt) #

          theorem BitVec.ult_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.ult y = !BitVec.carry w x (~~~y) true
          theorem BitVec.ule_eq_not_ult {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.ule y = !y.ult x
          theorem BitVec.ule_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.ule y = BitVec.carry w y (~~~x) true
          theorem BitVec.slt_eq_ult_of_msb_eq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb = y.msb) :
          x.slt y = x.ult y

          If two bitvectors have the same msb, then signed and unsigned comparisons coincide

          theorem BitVec.ult_eq_msb_of_msb_neq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb y.msb) :
          x.ult y = y.msb

          If two bitvectors have different msbs, then unsigned comparison is determined by this bit

          theorem BitVec.slt_eq_not_ult_of_msb_neq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb y.msb) :
          x.slt y = !x.ult y

          If two bitvectors have different msbs, then signed and unsigned comparisons are opposites

          theorem BitVec.slt_eq_ult {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.slt y = (x.msb != y.msb).xor (x.ult y)
          theorem BitVec.slt_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.slt y = (x.msb == y.msb).xor (BitVec.carry w x (~~~y) true)
          theorem BitVec.sle_eq_not_slt {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.sle y = !y.slt x
          theorem BitVec.sle_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) :
          x.sle y = !(x.msb == y.msb).xor (BitVec.carry w y (~~~x) true)