bignum-extract-opt-tests

(in-package "BITSETS")

(include-book "bignum-extract-opt")

(include-book "std/testing/assert-bang" :dir :system)

(defund bignum-extract-slow
  (x slice)
  (declare (xargs :guard (and (integerp x) (natp slice))))
  (let ((x (ifix x)) (slice (nfix slice)))
    (logand (1- (expt 2 32))
      (ash x (* -32 slice)))))

(defthm bignum-extract-slow-correct
  (equal (bignum-extract-slow x slice)
    (bignum-extract x slice))
  :hints (("Goal" :in-theory (enable bignum-extract-slow
       bignum-extract))))

(defconst *test-numbers*
  (list 1
    0
    -1
    100
    -100
    -127
    -128
    127
    128
    (expt 2 60)
    (+ 1 (expt 2 60))
    (+ 2 (expt 2 60))
    (+ -1 (expt 2 60))
    (+ -2 (expt 2 60))
    (- (expt 2 60))
    (- (+ 1 (expt 2 60)))
    (- (+ 2 (expt 2 60)))
    (- (+ -1 (expt 2 60)))
    (- (+ -2 (expt 2 60)))
    (floor (expt 2 90) 3)
    (floor (expt 2 90) 5)
    (floor (expt 2 90) 7)
    (- (floor (expt 2 90) 3))
    (- (floor (expt 2 90) 5))
    (- (floor (expt 2 90) 7))))

(defconst *test-slice-indices*
  (list 0
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    (expt 2 51)
    (+ 1 (expt 2 52))
    (+ 7 (expt 2 53))
    (+ 9 (expt 2 54))
    (+ 2 (expt 2 55))
    (+ 3 (expt 2 56))
    (- (expt 2 57) 1)
    (expt 2 57)
    (- (expt 2 57) 2)
    (- (expt 2 57) 3)
    (expt 2 60)
    (+ 1 (expt 2 60))
    (+ 2 (expt 2 60))
    (+ 2 (expt 2 61))
    (+ 2 (expt 2 62))
    (+ 2 (expt 2 63))
    (expt 2 90)))

(defun nat-listp
  (l)
  (declare (xargs :guard t))
  (cond ((atom l) (eq l nil))
    (t (and (natp (car l))
        (nat-listp (cdr l))))))

(defun test0
  (num index)
  (declare (xargs :guard (and (integerp num) (natp index))))
  (or (equal (bignum-extract num index)
      (bignum-extract-slow num index))
    (cw "Oops: (bignum-extract ~x0 ~x1): spec = ~x2, impl = ~x3.~%"
      num
      index
      (bignum-extract-slow num index)
      (bignum-extract num index))))

(defun test1
  (num indices)
  (declare (xargs :guard (and (integerp num)
        (nat-listp indices))))
  (if (atom indices)
    t
    (and (test0 num (car indices))
      (test1 num (cdr indices)))))

(defun test2
  (nums indices)
  (declare (xargs :guard (and (integer-listp nums)
        (nat-listp indices))))
  (if (atom nums)
    t
    (and (test1 (car nums) indices)
      (test2 (cdr nums) indices))))

(assert! (test2 *test-numbers*
    *test-slice-indices*))