bits-between

(in-package "BITSETS")

(include-book "std/util/define" :dir :system)

(include-book "std/osets/top" :dir :system)

(include-book "std/basic/defs" :dir :system)

(local (include-book "centaur/bitops/ihs-extensions" :dir :system))

(local (include-book "std/lists/rev" :dir :system))

(local (include-book "std/lists/append" :dir :system))

(local (in-theory (enable* arith-equiv-forwarding)))

(local (set-default-parents utilities))

(define add-to-each
  ((offset integerp) (x integer-listp))
  :short "Add an offset to each member of a list."
  :long "<p>This is used in the development of @(see bitset-members).</p>"
  (if (atom x)
    nil
    (cons (+ offset (car x))
      (add-to-each offset (cdr x))))
  ///
  (defthm add-to-each-when-atom
    (implies (atom x)
      (equal (add-to-each offset x)
        nil)))
  (defthm add-to-each-of-cons
    (equal (add-to-each offset
        (cons a x))
      (cons (+ offset a)
        (add-to-each offset x))))
  (defthm add-to-each-of-zero
    (implies (integer-listp x)
      (equal (add-to-each 0 x) x)))
  (defthm add-to-each-of-append
    (equal (add-to-each offset
        (append x y))
      (append (add-to-each offset x)
        (add-to-each offset y))))
  (local (defthm rev-of-add-to-each
      (equal (rev (add-to-each offset x))
        (add-to-each offset
          (rev x)))))
  (defthm add-to-each-of-add-to-each
    (equal (add-to-each a
        (add-to-each b x))
      (add-to-each (+ a b) x))))

(define bits-between
  ((n natp "lower bound, inclusive") (m natp "upper bound, exclusive")
    (x integerp "integer to extract bits from"))
  :guard (<= n m)
  :returns set-of-bits
  :short "@(call bits-between) returns a proper, ordered set of all @('i') in
@('[n, m)') such that @('(logbitp i x)')."
  :long "<p>This is a key function in the definition of @(see
bitset-members).</p>"
  :measure (nfix (- (nfix m) (nfix n)))
  (let* ((n (lnfix n)) (m (lnfix m)))
    (cond ((mbe :logic (zp (- m n))
         :exec (= m n)) nil)
      ((logbitp n x) (cons n
          (bits-between (+ n 1)
            m
            x)))
      (t (bits-between (+ n 1)
          m
          x))))
  ///
  (defthm true-listp-of-bits-between
    (true-listp (bits-between n m x))
    :rule-classes :type-prescription)
  (defthm integer-listp-of-bits-between
    (integer-listp (bits-between n m x)))
  (defthm nat-listp-of-bits-between
    (nat-listp (bits-between n m x)))
  (defthm bits-between-when-not-integer
    (implies (not (integerp x))
      (equal (bits-between n m x)
        nil)))
  (defthm member-equal-of-bits-between
    (iff (member-equal a
        (bits-between n m x))
      (and (natp a)
        (<= (nfix n) a)
        (< a (nfix m))
        (logbitp a x)))
    :hints (("Goal" :induct (bits-between n m x))))
  (defthm no-duplicatesp-equal-of-bits-between
    (no-duplicatesp-equal (bits-between n m x)))
  (defthmd bits-between-of-increment-right-index
    (implies (and (force (natp n))
        (force (natp m))
        (force (<= n m)))
      (equal (bits-between n
          (+ 1 m)
          x)
        (if (logbitp m x)
          (append (bits-between n m x)
            (list m))
          (bits-between n m x))))
    :hints (("Goal" :induct (bits-between n m x))))
  (defthm merge-appended-bits-between
    (implies (and (natp n)
        (natp m)
        (natp k)
        (<= n m)
        (<= m k))
      (equal (append (bits-between n m x)
          (bits-between m k x))
        (bits-between n k x)))
    :hints (("Goal" :induct (bits-between n m x))))
  (encapsulate nil
    (local (defun my-induct
        (n m)
        (declare (xargs :measure (nfix (- (nfix m) (nfix n)))
            :hints (("Goal" :in-theory (enable nfix)))))
        (if (zp (- (nfix m) (nfix n)))
          nil
          (my-induct (+ (nfix n) 1)
            m))))
    (local (include-book "arithmetic/top-with-meta" :dir :system))
    (defthm bits-between-of-right-shift
      (implies (and (natp n)
          (natp m)
          (<= n m)
          (integerp k)
          (< k 0))
        (equal (bits-between n
            m
            (ash x k))
          (add-to-each k
            (bits-between (- n k)
              (- m k)
              x))))
      :hints (("Goal" :expand ((bits-between n
            m
            (ash x k)) (bits-between (+ (- k) n)
             (+ (- k) m)
             x))
         :induct (my-induct n m)))))
  (defthm bits-between-of-mod-2^n
    (implies (and (integerp x)
        (natp k)
        (<= m k))
      (equal (bits-between n
          m
          (mod x (expt 2 k)))
        (bits-between n m x)))
    :hints (("Goal" :induct (bits-between n m x)
       :in-theory (e/d (bits-between nfix)))))
  (make-event `(defthm bits-between-of-mod-2^32
      (implies (and (integerp x) (<= m 32))
        (equal (bits-between n
            m
            (mod x ,(EXPT 2 32)))
          (bits-between n m x)))
      :hints (("Goal" :use ((:instance bits-between-of-mod-2^n (k 32)))))))
  (encapsulate nil
    (local (defthm l0
        (implies (and (natp n)
            (natp x)
            (<= (integer-length x) n))
          (not (bits-between n m x)))))
    (defthm bits-between-upper
      (implies (and (syntaxp (not (equal m `(integer-length ,BITSETS::X))))
          (natp n)
          (natp m)
          (natp x)
          (<= (integer-length x) m))
        (equal (bits-between n m x)
          (bits-between n
            (integer-length x)
            x)))
      :hints (("Goal" :induct (bits-between n m x)))))
  (encapsulate nil
    (local (defthm l0
        (implies (and (natp a) (natp b))
          (equal (<< a b)
            (< a b)))
        :hints (("Goal" :in-theory (enable <<
             lexorder
             alphorder)))))
    (local (defthm l1
        (equal (natp (car (bits-between n m x)))
          (if (bits-between n m x)
            t
            nil))))
    (local (defthm l2
        (implies (bits-between n m x)
          (<= (nfix n)
            (car (bits-between n m x))))
        :rule-classes ((:linear))))
    (defthm setp-of-bits-between
      (setp (bits-between n m x))
      :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules))))))
  (encapsulate nil
    (local (defthmd sets-membership-hack
        (implies (and (setp x)
            (syntaxp (not (quotep x))))
          (iff (member-equal a x)
            (in a x)))
        :hints (("Goal" :in-theory (enable in-to-member)))))
    (defthm in-of-bits-between
      (equal (in a
          (bits-between n m x))
        (and (natp a)
          (<= (nfix n) a)
          (< a (nfix m))
          (logbitp a x)))
      :hints (("Goal" :use ((:instance sets-membership-hack
            (a a)
            (x (bits-between n m x)))))))))

(local (defthm rassoc-append
    (equal (append x (append y z))
      (append (append x y) z))))

(local (defthm append-of-add-to-each
    (equal (append (add-to-each a x)
        (add-to-each a y))
      (add-to-each a
        (append x y)))))

(local (in-theory (disable add-to-each-of-append)))

(local (theory-invariant (incompatible (:rewrite append-of-add-to-each)
      (:rewrite add-to-each-of-append))))

(local (deftheory slow-rules
    '(true-listp-append bits-between-upper
      append
      not
      double-containment
      default-+-1
      default-+-2
      default-car
      default-cdr
      normalize-logbitp-when-mods-equal
      (:t logcar-type)
      (:t logcar)
      (:t logbitp)
      (:t binary-append))))

(local (in-theory (disable slow-rules)))

(define bits-0-7
  ((offset :type unsigned-byte) (x :type (unsigned-byte 32))
    (acc))
  :short "Inner loop for @(see bits-0-31)."
  (b* ((acc (if (logbitp 7 x)
         (cons (+ 7 offset) acc)
         acc)) (acc (if (logbitp 6 x)
          (cons (+ 6 offset) acc)
          acc))
      (acc (if (logbitp 5 x)
          (cons (+ 5 offset) acc)
          acc))
      (acc (if (logbitp 4 x)
          (cons (+ 4 offset) acc)
          acc))
      (acc (if (logbitp 3 x)
          (cons (+ 3 offset) acc)
          acc))
      (acc (if (logbitp 2 x)
          (cons (+ 2 offset) acc)
          acc))
      (acc (if (logbitp 1 x)
          (cons (+ 1 offset) acc)
          acc))
      (acc (if (logbitp 0 x)
          (cons offset acc)
          acc)))
    acc)
  ///
  (with-output :gag-mode :goals (defthm bits-0-7-redef
      (implies (force (natp offset))
        (equal (bits-0-7 offset x acc)
          (append (add-to-each offset
              (bits-between 0 8 x))
            acc)))
      :hints (("Goal" :in-theory (enable bits-0-7
           bits-between
           bits-between-of-increment-right-index)
         :expand ((:free (a b c)
            (append (cons a b) c)) (:free (c) (append nil c))))))))

(define bits-0-31
  ((offset :type unsigned-byte) (x :type (unsigned-byte 32))
    (acc))
  "Partially unrolled version of @(see bits-between) that collects the
bits from a 32-bit unsigned @('x') and adds @('offset') to each."
  :long "<p>This is about 2.8x faster than @(see bits-between), according to
the following loops (on fv-1):</p>

@({
 (progn
  (gc$)
  ;; 25.759 seconds
  (time (loop for x fixnum from 1 to 50000000 do
              (bits-between 0 32 x)))
  ;; 8.935 seconds
  (gc$)
  (time (loop for x fixnum from 1 to 50000000 do
              (bits-0-31 0 x nil))))
})

<p>The inner loop is unrolled 8 times.  Unrolling 16 times was a slightly
better, but the case explosion in the equivalence proof ended up causing ACL2 a
lot of problems.  Maybe a better rewriting strategy would solve this, but just
opening the functions is fine for 8 unrolls and it still gives us most of the
benefit.</p>"
  (b* (((when (eql x 0)) acc) (acc (bits-0-7 (+ offset 24)
          (the (unsigned-byte 32) (ash x -24))
          acc))
      (acc (bits-0-7 (+ offset 16)
          (the (unsigned-byte 32) (ash x -16))
          acc))
      (acc (bits-0-7 (+ offset 8)
          (the (unsigned-byte 32) (ash x -8))
          acc)))
    (bits-0-7 offset x acc))
  ///
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthm bits-0-31-redef
    (implies (natp offset)
      (equal (bits-0-31 offset x acc)
        (append (add-to-each offset
            (bits-between 0 32 x))
          acc)))
    :hints (("Goal" :in-theory (e/d (bits-0-31 append)
         (right-shift-to-logtail))))))

(define 60bits-0-7
  ((offset :type unsigned-byte) (x :type (unsigned-byte 60))
    (acc))
  :short "Identical to @(see bits-0-7), but for 60-bit unsigned ints."
  (b* ((acc (if (logbitp 7 x)
         (cons (+ 7 offset) acc)
         acc)) (acc (if (logbitp 6 x)
          (cons (+ 6 offset) acc)
          acc))
      (acc (if (logbitp 5 x)
          (cons (+ 5 offset) acc)
          acc))
      (acc (if (logbitp 4 x)
          (cons (+ 4 offset) acc)
          acc))
      (acc (if (logbitp 3 x)
          (cons (+ 3 offset) acc)
          acc))
      (acc (if (logbitp 2 x)
          (cons (+ 2 offset) acc)
          acc))
      (acc (if (logbitp 1 x)
          (cons (+ 1 offset) acc)
          acc))
      (acc (if (logbitp 0 x)
          (cons offset acc)
          acc)))
    acc)
  ///
  (with-output :gag-mode :goals (defthm 60bits-0-7-redef
      (implies (force (natp offset))
        (equal (60bits-0-7 offset
            x
            acc)
          (append (add-to-each offset
              (bits-between 0 8 x))
            acc)))
      :hints (("Goal" :in-theory (enable 60bits-0-7
           bits-between
           bits-between-of-increment-right-index)
         :expand ((:free (a b c)
            (append (cons a b) c)) (:free (c) (append nil c))))))))

(define 60bits-0-3
  ((offset :type unsigned-byte) (x :type (unsigned-byte 60))
    acc)
  :short "Like @(see bits-0-7), but since 8 doesn't divide 60, we have
 this goofy function for the final bits."
  (b* ((acc (if (logbitp 3 x)
         (cons (+ 3 offset) acc)
         acc)) (acc (if (logbitp 2 x)
          (cons (+ 2 offset) acc)
          acc))
      (acc (if (logbitp 1 x)
          (cons (+ 1 offset) acc)
          acc))
      (acc (if (logbitp 0 x)
          (cons offset acc)
          acc)))
    acc)
  ///
  (with-output :gag-mode :goals (defthm 60bits-0-3-redef
      (implies (force (natp offset))
        (equal (60bits-0-3 offset
            x
            acc)
          (append (add-to-each offset
              (bits-between 0 4 x))
            acc)))
      :hints (("Goal" :in-theory (e/d (60bits-0-3 bits-between
             bits-between-of-increment-right-index))
         :expand ((:free (a b c)
            (append (cons a b) c)) (:free (c) (append nil c))))))))

(define 60bits-0-59
  ((offset :type unsigned-byte) (x :type (unsigned-byte 60))
    acc)
  :short "Partially unrolled version of @(see bits-between) that collects the
bits from a 60-bit unsigned @('x') and adds @('offset') to each."
  :long "<p>In CCL, 60-bit unsigned numbers are fixnums and, according to the
following loops, this is about 3.6x faster than @(see bits-between).</p>

@({
 (progn
  (gc$)
  ;; 21.540 seconds
  (time (loop for x fixnum from 1 to 30000000 do
              (bits-between 0 60 x)))
  ;; 6.013 seconds
  (gc$)
  (time (loop for x fixnum from 1 to 30000000 do
              (60bits-0-59 0 x nil))))
})"
  (b* ((acc (60bits-0-3 (+ offset 56)
         (the (unsigned-byte 60) (ash x -56))
         acc)) (acc (60bits-0-7 (+ offset 48)
          (the (unsigned-byte 60) (ash x -48))
          acc))
      (acc (60bits-0-7 (+ offset 40)
          (the (unsigned-byte 60) (ash x -40))
          acc))
      (acc (60bits-0-7 (+ offset 32)
          (the (unsigned-byte 60) (ash x -32))
          acc))
      (acc (60bits-0-7 (+ offset 24)
          (the (unsigned-byte 60) (ash x -24))
          acc))
      (acc (60bits-0-7 (+ offset 16)
          (the (unsigned-byte 60) (ash x -16))
          acc))
      (acc (60bits-0-7 (+ offset 8)
          (the (unsigned-byte 60) (ash x -8))
          acc)))
    (60bits-0-7 offset
      x
      acc))
  ///
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthm 60bits-0-59-redef
    (implies (natp offset)
      (equal (60bits-0-59 offset
          x
          acc)
        (append (add-to-each offset
            (bits-between 0 60 x))
          acc)))
    :hints (("Goal" :in-theory (e/d (60bits-0-59 append)
         (right-shift-to-logtail))))))