Documentation

Init.Data.BitVec.Basic

We define the basic algebraic structure of bitvectors. We choose the Fin representation over others for its relative efficiency (Lean has special support for Nat), and the fact that bitwise operations on Fin are already defined. Some other possible representations are List Bool, { l : List Bool // l.length = w }, Fin w → Bool.

We define many of the bitvector operations from the QF_BV logic. of SMT-LIBv2.

instance BitVec.natCastInst {w : Nat} :
Equations
@[deprecated BitVec.isLt]
theorem BitVec.toNat_lt {n : Nat} (x : BitVec n) :
x.toNat < 2 ^ n
@[simp]

Theorem for normalizing the bit vector literal representation.

@[simp]
theorem BitVec.natCast_eq_ofNat (w : Nat) (x : Nat) :
x = BitVec.ofNat w x

All empty bitvectors are equal

Equations
@[reducible, inline]
abbrev BitVec.nil :

The empty bitvector

Equations
Instances For
    theorem BitVec.eq_nil (x : BitVec 0) :

    Every bitvector of length 0 is equal to nil, i.e., there is only one empty bitvector

    def BitVec.zero (n : Nat) :

    Return a bitvector 0 of size n. This is the bitvector with all zero bits.

    Equations
    Instances For
      Equations

      Bit vector of size n where all bits are 1s

      Equations
      Instances For
        @[inline]
        def BitVec.getLsb' {w : Nat} (x : BitVec w) (i : Fin w) :

        Return the i-th least significant bit.

        This will be renamed getLsb after the existing deprecated alias is removed.

        Equations
        • x.getLsb' i = x.toNat.testBit i
        Instances For
          @[inline]
          def BitVec.getLsb? {w : Nat} (x : BitVec w) (i : Nat) :

          Return the i-th least significant bit or none if i ≥ w.

          Equations
          • x.getLsb? i = if h : i < w then some (x.getLsb' i, h) else none
          Instances For
            @[inline]
            def BitVec.getMsb' {w : Nat} (x : BitVec w) (i : Fin w) :

            Return the i-th most significant bit.

            This will be renamed getMsb after the existing deprecated alias is removed.

            Equations
            • x.getMsb' i = x.getLsb' w - 1 - i,
            Instances For
              @[inline]
              def BitVec.getMsb? {w : Nat} (x : BitVec w) (i : Nat) :

              Return the i-th most significant bit or none if i ≥ w.

              Equations
              • x.getMsb? i = if h : i < w then some (x.getMsb' i, h) else none
              Instances For
                @[inline]
                def BitVec.getLsbD {w : Nat} (x : BitVec w) (i : Nat) :

                Return the i-th least significant bit or false if i ≥ w.

                Equations
                • x.getLsbD i = x.toNat.testBit i
                Instances For
                  @[deprecated BitVec.getLsbD]
                  def BitVec.getLsb {w : Nat} (x : BitVec w) (i : Nat) :

                  Return the i-th least significant bit or false if i ≥ w.

                  Equations
                  • x.getLsb i = x.getLsbD i
                  Instances For
                    @[inline]
                    def BitVec.getMsbD {w : Nat} (x : BitVec w) (i : Nat) :

                    Return the i-th most significant bit or false if i ≥ w.

                    Equations
                    Instances For
                      @[deprecated BitVec.getMsbD]
                      def BitVec.getMsb {w : Nat} (x : BitVec w) (i : Nat) :

                      Return the i-th most significant bit or false if i ≥ w.

                      Equations
                      • x.getMsb i = x.getMsbD i
                      Instances For
                        @[inline]
                        def BitVec.msb {n : Nat} (x : BitVec n) :

                        Return most-significant bit in bitvector.

                        Equations
                        • x.msb = x.getMsbD 0
                        Instances For
                          instance BitVec.instGetElemNatBoolLt {w : Nat} :
                          GetElem (BitVec w) Nat Bool fun (x : BitVec w) (i : Nat) => i < w
                          Equations
                          • BitVec.instGetElemNatBoolLt = { getElem := fun (xs : BitVec w) (i : Nat) (h : i < w) => xs.getLsb' i, h }
                          @[simp]
                          theorem BitVec.getLsb'_eq_getElem {w : Nat} (x : BitVec w) (i : Fin w) :
                          x.getLsb' i = x[i]

                          We prefer x[i] as the simp normal form for getLsb'

                          @[simp]
                          theorem BitVec.getLsb?_eq_getElem? {w : Nat} (x : BitVec w) (i : Nat) :
                          x.getLsb? i = x[i]?

                          We prefer x[i]? as the simp normal form for getLsb?

                          theorem BitVec.getElem_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) (h : i < w) :
                          x[i] = x.toNat.testBit i
                          theorem BitVec.getLsbD_eq_getElem {w : Nat} {x : BitVec w} {i : Nat} (h : i < w) :
                          x.getLsbD i = x[i]
                          def BitVec.toInt {n : Nat} (x : BitVec n) :

                          Interpret the bitvector as an integer stored in two's complement form.

                          Equations
                          • x.toInt = if 2 * x.toNat < 2 ^ n then x.toNat else x.toNat - (2 ^ n)
                          Instances For
                            def BitVec.ofInt (n : Nat) (i : Int) :

                            The BitVec with value (2^n + (i mod 2^n)) mod 2^n.

                            Equations
                            Instances For
                              instance BitVec.instIntCast {w : Nat} :
                              Equations

                              Notation for bit vector literals. i#n is a shorthand for BitVec.ofNat n i.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Unexpander for bit vector literals.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Notation for bit vector literals without truncation. i#'lt is a shorthand for BitVec.ofNatLt i lt.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Unexpander for bit vector literals without truncation.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def BitVec.toHex {n : Nat} (x : BitVec n) :

                                      Convert bitvector into a fixed-width hex number.

                                      Equations
                                      Instances For
                                        instance BitVec.instRepr {n : Nat} :
                                        Equations
                                        Equations
                                        def BitVec.neg {n : Nat} (x : BitVec n) :

                                        Negation for bit vectors. This can be interpreted as either signed or unsigned negation modulo 2^n.

                                        SMT-Lib name: bvneg.

                                        Equations
                                        Instances For
                                          instance BitVec.instNeg {n : Nat} :
                                          Equations
                                          • BitVec.instNeg = { neg := BitVec.neg }
                                          def BitVec.abs {n : Nat} (x : BitVec n) :

                                          Return the absolute value of a signed bitvector.

                                          Equations
                                          • x.abs = if x.msb = true then x.neg else x
                                          Instances For
                                            def BitVec.mul {n : Nat} (x : BitVec n) (y : BitVec n) :

                                            Multiplication for bit vectors. This can be interpreted as either signed or unsigned multiplication modulo 2^n.

                                            SMT-Lib name: bvmul.

                                            Equations
                                            Instances For
                                              instance BitVec.instMul {n : Nat} :
                                              Equations
                                              • BitVec.instMul = { mul := BitVec.mul }
                                              def BitVec.udiv {n : Nat} (x : BitVec n) (y : BitVec n) :

                                              Unsigned division for bit vectors using the Lean convention where division by zero returns zero.

                                              Equations
                                              • x.udiv y = (x.toNat / y.toNat)#'
                                              Instances For
                                                instance BitVec.instDiv {n : Nat} :
                                                Equations
                                                • BitVec.instDiv = { div := BitVec.udiv }
                                                def BitVec.umod {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                Unsigned modulo for bit vectors.

                                                SMT-Lib name: bvurem.

                                                Equations
                                                • x.umod y = (x.toNat % y.toNat)#'
                                                Instances For
                                                  instance BitVec.instMod {n : Nat} :
                                                  Equations
                                                  • BitVec.instMod = { mod := BitVec.umod }
                                                  def BitVec.smtUDiv {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                  Unsigned division for bit vectors using the SMT-Lib convention where division by zero returns the allOnes bitvector.

                                                  SMT-Lib name: bvudiv.

                                                  Equations
                                                  Instances For
                                                    def BitVec.sdiv {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                    Signed t-division for bit vectors using the Lean convention where division by zero returns zero.

                                                    sdiv 7#4 2 = 3#4
                                                    sdiv (-9#4) 2 = -4#4
                                                    sdiv 5#4 -2 = -2#4
                                                    sdiv (-7#4) (-2) = 3#4
                                                    
                                                    Equations
                                                    Instances For
                                                      def BitVec.smtSDiv {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                      Signed division for bit vectors using SMTLIB rules for division by zero.

                                                      Specifically, smtSDiv x 0 = if x >= 0 then -1 else 1

                                                      SMT-Lib name: bvsdiv.

                                                      Equations
                                                      Instances For
                                                        def BitVec.srem {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                        Remainder for signed division rounding to zero.

                                                        SMT_Lib name: bvsrem.

                                                        Equations
                                                        Instances For
                                                          def BitVec.smod {m : Nat} (x : BitVec m) (y : BitVec m) :

                                                          Remainder for signed division rounded to negative infinity.

                                                          SMT_Lib name: bvsmod.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            Turn a Bool into a bitvector of length 1

                                                            Equations
                                                            Instances For
                                                              def BitVec.fill (w : Nat) (b : Bool) :

                                                              Fills a bitvector with w copies of the bit b.

                                                              Equations
                                                              Instances For
                                                                def BitVec.ult {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                Unsigned less-than for bit vectors.

                                                                SMT-Lib name: bvult.

                                                                Equations
                                                                Instances For
                                                                  def BitVec.ule {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                  Unsigned less-than-or-equal-to for bit vectors.

                                                                  SMT-Lib name: bvule.

                                                                  Equations
                                                                  Instances For
                                                                    def BitVec.slt {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                    Signed less-than for bit vectors.

                                                                    BitVec.slt 6#4 7 = true
                                                                    BitVec.slt 7#4 8 = false
                                                                    

                                                                    SMT-Lib name: bvslt.

                                                                    Equations
                                                                    Instances For
                                                                      def BitVec.sle {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                      Signed less-than-or-equal-to for bit vectors.

                                                                      SMT-Lib name: bvsle.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        def BitVec.cast {n : Nat} {m : Nat} (eq : n = m) (x : BitVec n) :

                                                                        cast eq x embeds x into an equal BitVec type.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem BitVec.cast_ofNat {n : Nat} {m : Nat} (h : n = m) (x : Nat) :
                                                                          @[simp]
                                                                          theorem BitVec.cast_cast {n : Nat} {m : Nat} {k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
                                                                          BitVec.cast h₂ (BitVec.cast h₁ x) = BitVec.cast x
                                                                          @[simp]
                                                                          theorem BitVec.cast_eq {n : Nat} (h : n = n) (x : BitVec n) :
                                                                          def BitVec.extractLsb' {n : Nat} (start : Nat) (len : Nat) (x : BitVec n) :
                                                                          BitVec len

                                                                          Extraction of bits start to start + len - 1 from a bit vector of size n to yield a new bitvector of size len. If start + len > n, then the vector will be zero-padded in the high bits.

                                                                          Equations
                                                                          Instances For
                                                                            def BitVec.extractLsb {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) :
                                                                            BitVec (hi - lo + 1)

                                                                            Extraction of bits hi (inclusive) down to lo (inclusive) from a bit vector of size n to yield a new bitvector of size hi - lo + 1.

                                                                            SMT-Lib name: extract.

                                                                            Equations
                                                                            Instances For
                                                                              def BitVec.setWidth' {n : Nat} {w : Nat} (le : n w) (x : BitVec n) :

                                                                              A version of setWidth that requires a proof, but is a noop.

                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline, deprecated BitVec.setWidth']
                                                                                abbrev BitVec.zeroExtend' {n : Nat} {w : Nat} (le : n w) (x : BitVec n) :

                                                                                A version of setWidth that requires a proof, but is a noop.

                                                                                Equations
                                                                                Instances For
                                                                                  def BitVec.shiftLeftZeroExtend {w : Nat} (msbs : BitVec w) (m : Nat) :
                                                                                  BitVec (w + m)

                                                                                  shiftLeftZeroExtend x n returns zeroExtend (w+n) x <<< n without needing to compute x % 2^(2+n).

                                                                                  Equations
                                                                                  • msbs.shiftLeftZeroExtend m = (msbs.toNat <<< m)#'
                                                                                  Instances For
                                                                                    def BitVec.setWidth {w : Nat} (v : Nat) (x : BitVec w) :

                                                                                    Transform x of length w into a bitvector of length v, by either:

                                                                                    • zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
                                                                                    • truncating the high bits, if v < w.

                                                                                    SMT-Lib name: zero_extend.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline]
                                                                                      abbrev BitVec.zeroExtend {w : Nat} (v : Nat) (x : BitVec w) :

                                                                                      Transform x of length w into a bitvector of length v, by either:

                                                                                      • zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
                                                                                      • truncating the high bits, if v < w.

                                                                                      SMT-Lib name: zero_extend.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline]
                                                                                        abbrev BitVec.truncate {w : Nat} (v : Nat) (x : BitVec w) :

                                                                                        Transform x of length w into a bitvector of length v, by either:

                                                                                        • zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
                                                                                        • truncating the high bits, if v < w.

                                                                                        SMT-Lib name: zero_extend.

                                                                                        Equations
                                                                                        Instances For
                                                                                          def BitVec.signExtend {w : Nat} (v : Nat) (x : BitVec w) :

                                                                                          Sign extend a vector of length w, extending with i additional copies of the most significant bit in x. If x is an empty vector, then the sign is treated as zero.

                                                                                          SMT-Lib name: sign_extend.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def BitVec.and {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                                            Bitwise AND for bit vectors.

                                                                                            0b1010#4 &&& 0b0110#4 = 0b0010#4
                                                                                            

                                                                                            SMT-Lib name: bvand.

                                                                                            Equations
                                                                                            • x.and y = (x.toNat &&& y.toNat)#'
                                                                                            Instances For
                                                                                              instance BitVec.instAndOp {w : Nat} :
                                                                                              Equations
                                                                                              • BitVec.instAndOp = { and := BitVec.and }
                                                                                              def BitVec.or {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                                              Bitwise OR for bit vectors.

                                                                                              0b1010#4 ||| 0b0110#4 = 0b1110#4
                                                                                              

                                                                                              SMT-Lib name: bvor.

                                                                                              Equations
                                                                                              • x.or y = (x.toNat ||| y.toNat)#'
                                                                                              Instances For
                                                                                                instance BitVec.instOrOp {w : Nat} :
                                                                                                Equations
                                                                                                • BitVec.instOrOp = { or := BitVec.or }
                                                                                                def BitVec.xor {n : Nat} (x : BitVec n) (y : BitVec n) :

                                                                                                Bitwise XOR for bit vectors.

                                                                                                0b1010#4 ^^^ 0b0110#4 = 0b1100#4
                                                                                                

                                                                                                SMT-Lib name: bvxor.

                                                                                                Equations
                                                                                                • x.xor y = (x.toNat ^^^ y.toNat)#'
                                                                                                Instances For
                                                                                                  instance BitVec.instXor {w : Nat} :
                                                                                                  Equations
                                                                                                  • BitVec.instXor = { xor := BitVec.xor }
                                                                                                  def BitVec.not {n : Nat} (x : BitVec n) :

                                                                                                  Bitwise NOT for bit vectors.

                                                                                                  ~~~(0b0101#4) == 0b1010
                                                                                                  

                                                                                                  SMT-Lib name: bvnot.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • BitVec.instComplement = { complement := BitVec.not }
                                                                                                    def BitVec.shiftLeft {n : Nat} (x : BitVec n) (s : Nat) :

                                                                                                    Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is equivalent to x * 2^s, modulo 2^n.

                                                                                                    SMT-Lib name: bvshl except this operator uses a Nat shift value.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      • BitVec.instHShiftLeftNat = { hShiftLeft := BitVec.shiftLeft }
                                                                                                      def BitVec.ushiftRight {n : Nat} (x : BitVec n) (s : Nat) :

                                                                                                      (Logical) right shift for bit vectors. The high bits are filled with zeros. As a numeric operation, this is equivalent to x / 2^s, rounding down.

                                                                                                      SMT-Lib name: bvlshr except this operator uses a Nat shift value.

                                                                                                      Equations
                                                                                                      • x.ushiftRight s = (x.toNat >>> s)#'
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        • BitVec.instHShiftRightNat = { hShiftRight := BitVec.ushiftRight }
                                                                                                        def BitVec.sshiftRight {n : Nat} (x : BitVec n) (s : Nat) :

                                                                                                        Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. As a numeric operation, this is equivalent to x.toInt >>> s.

                                                                                                        SMT-Lib name: bvashr except this operator uses a Nat shift value.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          instance BitVec.instHShiftLeft {m : Nat} {n : Nat} :
                                                                                                          Equations
                                                                                                          • BitVec.instHShiftLeft = { hShiftLeft := fun (x : BitVec m) (y : BitVec n) => x <<< y.toNat }
                                                                                                          instance BitVec.instHShiftRight {m : Nat} {n : Nat} :
                                                                                                          Equations
                                                                                                          • BitVec.instHShiftRight = { hShiftRight := fun (x : BitVec m) (y : BitVec n) => x >>> y.toNat }
                                                                                                          def BitVec.sshiftRight' {n : Nat} {m : Nat} (a : BitVec n) (s : BitVec m) :

                                                                                                          Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. As a numeric operation, this is equivalent to a.toInt >>> s.toNat.

                                                                                                          SMT-Lib name: bvashr.

                                                                                                          Equations
                                                                                                          • a.sshiftRight' s = a.sshiftRight s.toNat
                                                                                                          Instances For
                                                                                                            def BitVec.rotateLeftAux {w : Nat} (x : BitVec w) (n : Nat) :

                                                                                                            Auxiliary function for rotateLeft, which does not take into account the case where the rotation amount is greater than the bitvector width.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def BitVec.rotateLeft {w : Nat} (x : BitVec w) (n : Nat) :

                                                                                                              Rotate left for bit vectors. All the bits of x are shifted to higher positions, with the top n bits wrapping around to fill the low bits.

                                                                                                              rotateLeft  0b0011#4 3 = 0b1001
                                                                                                              

                                                                                                              SMT-Lib name: rotate_left except this operator uses a Nat shift amount.

                                                                                                              Equations
                                                                                                              • x.rotateLeft n = x.rotateLeftAux (n % w)
                                                                                                              Instances For
                                                                                                                def BitVec.rotateRightAux {w : Nat} (x : BitVec w) (n : Nat) :

                                                                                                                Auxiliary function for rotateRight, which does not take into account the case where the rotation amount is greater than the bitvector width.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def BitVec.rotateRight {w : Nat} (x : BitVec w) (n : Nat) :

                                                                                                                  Rotate right for bit vectors. All the bits of x are shifted to lower positions, with the bottom n bits wrapping around to fill the high bits.

                                                                                                                  rotateRight 0b01001#5 1 = 0b10100
                                                                                                                  

                                                                                                                  SMT-Lib name: rotate_right except this operator uses a Nat shift amount.

                                                                                                                  Equations
                                                                                                                  • x.rotateRight n = x.rotateRightAux (n % w)
                                                                                                                  Instances For
                                                                                                                    def BitVec.append {n : Nat} {m : Nat} (msbs : BitVec n) (lsbs : BitVec m) :
                                                                                                                    BitVec (n + m)

                                                                                                                    Concatenation of bitvectors. This uses the "big endian" convention that the more significant input is on the left, so 0xAB#8 ++ 0xCD#8 = 0xABCD#16.

                                                                                                                    SMT-Lib name: concat.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      instance BitVec.instHAppendHAddNat {w : Nat} {v : Nat} :
                                                                                                                      HAppend (BitVec w) (BitVec v) (BitVec (w + v))
                                                                                                                      Equations
                                                                                                                      • BitVec.instHAppendHAddNat = { hAppend := BitVec.append }
                                                                                                                      def BitVec.replicate {w : Nat} (i : Nat) :
                                                                                                                      BitVec wBitVec (w * i)

                                                                                                                      replicate i x concatenates i copies of x into a new vector of length w*i.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        Cons and Concat #

                                                                                                                        We give special names to the operations of adding a single bit to either end of a bitvector. We follow the precedent of Vector.cons/Vector.concat both for the name, and for the decision to have the resulting size be n + 1 for both operations (rather than 1 + n, which would be the result of appending a single bit to the front in the naive implementation).

                                                                                                                        def BitVec.concat {n : Nat} (msbs : BitVec n) (lsb : Bool) :
                                                                                                                        BitVec (n + 1)

                                                                                                                        Append a single bit to the end of a bitvector, using big endian order (see append). That is, the new bit is the least significant bit.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def BitVec.shiftConcat {n : Nat} (x : BitVec n) (b : Bool) :

                                                                                                                          x.shiftConcat b shifts all bits of x to the left by 1 and sets the least significant bit to b. It is a non-dependent version of concat that does not change the total bitwidth.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def BitVec.cons {n : Nat} (msb : Bool) (lsbs : BitVec n) :
                                                                                                                            BitVec (n + 1)

                                                                                                                            Prepend a single bit to the front of a bitvector, using big endian order (see append). That is, the new bit is the most significant bit.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              theorem BitVec.append_ofBool {w : Nat} (msbs : BitVec w) (lsb : Bool) :
                                                                                                                              msbs ++ BitVec.ofBool lsb = msbs.concat lsb
                                                                                                                              theorem BitVec.ofBool_append {w : Nat} (msb : Bool) (lsbs : BitVec w) :
                                                                                                                              BitVec.ofBool msb ++ lsbs = BitVec.cast (BitVec.cons msb lsbs)
                                                                                                                              def BitVec.twoPow (w : Nat) (i : Nat) :

                                                                                                                              twoPow w i is the bitvector 2^i if i < w, and 0 otherwise. That is, 2 to the power i. For the bitwise point of view, it has the ith bit as 1 and all other bits as 0.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[irreducible]
                                                                                                                                def BitVec.hash {n : Nat} (bv : BitVec n) :

                                                                                                                                Compute a hash of a bitvector, combining 64-bit words using mixHash.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  Equations
                                                                                                                                  • BitVec.instHashable = { hash := BitVec.hash }

                                                                                                                                  We add simp-lemmas that rewrite bitvector operations into the equivalent notation

                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.append_eq {w : Nat} {v : Nat} (x : BitVec w) (y : BitVec v) :
                                                                                                                                  x.append y = x ++ y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.shiftLeft_eq {w : Nat} (x : BitVec w) (n : Nat) :
                                                                                                                                  x.shiftLeft n = x <<< n
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.ushiftRight_eq {w : Nat} (x : BitVec w) (n : Nat) :
                                                                                                                                  x.ushiftRight n = x >>> n
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.not_eq {w : Nat} (x : BitVec w) :
                                                                                                                                  x.not = ~~~x
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.and_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.and y = x &&& y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.or_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.or y = x ||| y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.xor_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.xor y = x ^^^ y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.neg_eq {w : Nat} (x : BitVec w) :
                                                                                                                                  x.neg = -x
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.add_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.add y = x + y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.sub_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.sub y = x - y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.mul_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.mul y = x * y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.udiv_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.udiv y = x / y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.umod_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
                                                                                                                                  x.umod y = x % y
                                                                                                                                  @[simp]
                                                                                                                                  theorem BitVec.zero_eq {n : Nat} :
                                                                                                                                  def BitVec.ofBoolListBE (bs : List Bool) :
                                                                                                                                  BitVec bs.length

                                                                                                                                  Converts a list of Bools to a big-endian BitVec.

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    def BitVec.ofBoolListLE (bs : List Bool) :
                                                                                                                                    BitVec bs.length

                                                                                                                                    Converts a list of Bools to a little-endian BitVec.

                                                                                                                                    Equations
                                                                                                                                    Instances For