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)
      theorem BitVec.carry_of_and_eq_zero {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} (h : x &&& y = 0#w) :

      If x &&& y = 0, then the carry bit (x + y + 0) is always false for any index i. Intuitively, this is because a carry is only produced when at least two of x, y, and the previous carry are true. However, since x &&& y = 0, at most one of x, y can be true, and thus we never have a previous carry, which means that the sum cannot produce a carry.

      theorem BitVec.carry_width {w : Nat} {c : Bool} {x : BitVec w} {y : BitVec w} :
      BitVec.carry w x y c = decide (x.toNat + y.toNat + c.toNat 2 ^ w)

      The final carry bit when computing x + y + c is true iff x.toNat + y.toNat + c.toNat ≥ 2^w.

      theorem BitVec.toNat_add_of_and_eq_zero {w : Nat} {x : BitVec w} {y : BitVec w} (h : x &&& y = 0#w) :
      (x + y).toNat = x.toNat + y.toNat

      If x &&& y = 0, then addition does not overflow, and thus (x + y).toNat = x.toNat + y.toNat.

      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

          theorem BitVec.add_eq_or_of_and_eq_zero {w : Nat} (x : BitVec w) (y : BitVec w) (h : x &&& y = 0#w) :
          x + y = x ||| y

          Addition of bitvectors is the same as bitwise or, if bitwise and is zero.

          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)

          mul recurrence for bitblasting #

          def BitVec.mulRec {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) :

          A recurrence that describes multiplication as repeated addition. Is useful for bitblasting multiplication.

          Equations
          • l.mulRec r 0 = if r.getLsb 0 = true then l <<< 0 else 0
          • l.mulRec r s_2.succ = l.mulRec r s_2 + if r.getLsb s_2.succ = true then l <<< s_2.succ else 0
          Instances For
            theorem BitVec.mulRec_zero_eq {w : Nat} (l : BitVec w) (r : BitVec w) :
            l.mulRec r 0 = if r.getLsb 0 = true then l else 0
            theorem BitVec.mulRec_succ_eq {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) :
            l.mulRec r (s + 1) = l.mulRec r s + if r.getLsb (s + 1) = true then l <<< (s + 1) else 0

            Recurrence lemma: truncating to i+1 bits and then zero extending to w equals truncating upto i bits [0..i-1], and then adding the ith bit of x.

            theorem BitVec.mulRec_eq_mul_signExtend_truncate {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) :
            l.mulRec r s = l * BitVec.zeroExtend w (BitVec.truncate (s + 1) r)

            Recurrence lemma: multiplying l with the first s bits of r is the same as truncating r to s bits, then zero extending to the original length, and performing the multplication.

            theorem BitVec.getLsb_mul {w : Nat} (x : BitVec w) (y : BitVec w) (i : Nat) :
            (x * y).getLsb i = (x.mulRec y w).getLsb i

            shiftLeft recurrence for bitblasting #

            def BitVec.shiftLeftRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
            BitVec w₁

            shiftLeftRec x y n shifts x to the left by the first n bits of y.

            The theorem shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and shiftLeftRec.

            Together with equations shiftLeftRec_zero, shiftLeftRec_succ, this allows us to unfold shiftLeft into a circuit for bitblasting.

            Equations
            Instances For
              @[simp]
              theorem BitVec.shiftLeftRec_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :
              x.shiftLeftRec y 0 = x <<< (y &&& BitVec.twoPow w₂ 0)
              @[simp]
              theorem BitVec.shiftLeftRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} {x : BitVec w₁} {y : BitVec w₂} :
              x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& BitVec.twoPow w₂ (n + 1))
              theorem BitVec.shiftLeft_or_of_and_eq_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₂} (h : y &&& z = 0#w₂) :
              x <<< (y ||| z) = x <<< y <<< z

              If y &&& z = 0, x <<< (y ||| z) = x <<< y <<< z. This follows as y &&& z = 0 implies y ||| z = y + z, and thus x <<< (y ||| z) = x <<< (y + z) = x <<< y <<< z.

              theorem BitVec.shiftLeftRec_eq {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
              x.shiftLeftRec y n = x <<< BitVec.zeroExtend w₂ (BitVec.truncate (n + 1) y)

              shiftLeftRec x y n shifts x to the left by the first n bits of y.

              theorem BitVec.shiftLeft_eq_shiftLeftRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :
              x <<< y = x.shiftLeftRec y (w₂ - 1)

              Show that x <<< y can be written in terms of shiftLeftRec. This can be unfolded in terms of shiftLeftRec_zero, shiftLeftRec_succ for bitblasting.

              def BitVec.ushiftRightRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
              BitVec w₁

              ushiftRightRec x y n shifts x logically to the right by the first n bits of y.

              The theorem shiftRight_eq_ushiftRightRec proves the equivalence of (x >>> y) and ushiftRightRec.

              Together with equations ushiftRightRec_zero, ushiftRightRec_succ, this allows us to unfold ushiftRight into a circuit for bitblasting.

              Equations
              Instances For
                @[simp]
                theorem BitVec.ushiftRightRec_zero {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :
                x.ushiftRightRec y 0 = x >>> (y &&& BitVec.twoPow w₂ 0)
                @[simp]
                theorem BitVec.ushiftRightRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} (x : BitVec w₁) (y : BitVec w₂) :
                x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& BitVec.twoPow w₂ (n + 1))
                theorem BitVec.ushiftRight'_or_of_and_eq_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₂} (h : y &&& z = 0#w₂) :
                x >>> (y ||| z) = x >>> y >>> z

                If y &&& z = 0, x >>> (y ||| z) = x >>> y >>> z. This follows as y &&& z = 0 implies y ||| z = y + z, and thus x >>> (y ||| z) = x >>> (y + z) = x >>> y >>> z.

                theorem BitVec.ushiftRightRec_eq {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
                x.ushiftRightRec y n = x >>> BitVec.zeroExtend w₂ (BitVec.truncate (n + 1) y)
                theorem BitVec.shiftRight_eq_ushiftRightRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :
                x >>> y = x.ushiftRightRec y (w₂ - 1)

                Show that x >>> y can be written in terms of ushiftRightRec. This can be unfolded in terms of ushiftRightRec_zero, ushiftRightRec_succ for bitblasting.