		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-trailing-0-count-width

Signature
(sparseint$-trailing-0-count-width width offset negbit x) → count
Arguments: width — Guard (posp width).; offset — Guard (natp offset).; negbit — Guard (bitp negbit).; x — Guard (sparseint$-p x).
Returns: count — Type (acl2::maybe-natp count).

Definitions and Theorems

Function: sparseint$-trailing-0-count-width

(defun sparseint$-trailing-0-count-width (width offset negbit x)
 (declare (xargs :guard (and (posp width)
                             (natp offset)
                             (bitp negbit)
                             (sparseint$-p x))))
 (let ((__function__ 'sparseint$-trailing-0-count-width))
  (declare (ignorable __function__))
  (sparseint$-case
   x :leaf
   (b* (((when (mbe :logic (equal (logtail offset x.val)
                                  (- (lbfix negbit)))
                    :exec (and (<= (integer-length x.val)
                                   (lnfix offset))
                               (eql negbit (logbit offset x.val)))))
         nil)
        (count (if (eql 1 negbit)
                   (trailing-1-count-from x.val offset)
                 (trailing-0-count-from x.val offset))))
     (and (< count (lposfix width)) count))
   :concat
   (b* ((width (lposfix width))
        (offset (lnfix offset))
        ((when (<= x.width offset))
         (sparseint$-trailing-0-count-width width (- offset x.width)
                                            negbit x.msbs))
        (width1 (- x.width offset))
        ((when (<= width width1))
         (sparseint$-trailing-0-count-width
              width offset negbit x.lsbs))
        (lsb-count (sparseint$-trailing-0-count-width
                        width1 offset negbit x.lsbs))
        ((when lsb-count) lsb-count)
        (msb-count
             (sparseint$-trailing-0-count-width (- width width1)
                                                0 negbit x.msbs)))
     (and msb-count (+ width1 msb-count))))))

Theorem: maybe-natp-of-sparseint$-trailing-0-count-width

(defthm maybe-natp-of-sparseint$-trailing-0-count-width
  (b*
   ((count
         (sparseint$-trailing-0-count-width width offset negbit x)))
   (acl2::maybe-natp count))
  :rule-classes :type-prescription)

Theorem: sparseint$-trailing-0-count-width-correct

(defthm sparseint$-trailing-0-count-width-correct
 (b*
  ((common-lisp::?count
        (sparseint$-trailing-0-count-width width offset negbit x)))
  (and
   (iff count
        (not (equal (logext width
                            (logtail offset (sparseint$-val x)))
                    (- (bfix negbit)))))
   (implies
      (not (equal (logext width
                          (logtail offset (sparseint$-val x)))
                  (- (bfix negbit))))
      (equal count
             (trailing-0-count
                  (logxor (- (bfix negbit))
                          (logtail offset (sparseint$-val x)))))))))

Theorem: sparseint$-trailing-0-count-width-of-pos-fix-width

(defthm sparseint$-trailing-0-count-width-of-pos-fix-width
  (equal (sparseint$-trailing-0-count-width (pos-fix width)
                                            offset negbit x)
         (sparseint$-trailing-0-count-width width offset negbit x)))

Theorem: sparseint$-trailing-0-count-width-pos-equiv-congruence-on-width

(defthm
    sparseint$-trailing-0-count-width-pos-equiv-congruence-on-width
 (implies
  (pos-equiv width width-equiv)
  (equal
   (sparseint$-trailing-0-count-width width offset negbit x)
   (sparseint$-trailing-0-count-width width-equiv offset negbit x)))
 :rule-classes :congruence)

Theorem: sparseint$-trailing-0-count-width-of-nfix-offset

(defthm sparseint$-trailing-0-count-width-of-nfix-offset
  (equal (sparseint$-trailing-0-count-width width (nfix offset)
                                            negbit x)
         (sparseint$-trailing-0-count-width width offset negbit x)))

Theorem: sparseint$-trailing-0-count-width-nat-equiv-congruence-on-offset

(defthm
   sparseint$-trailing-0-count-width-nat-equiv-congruence-on-offset
 (implies
  (nat-equiv offset offset-equiv)
  (equal
   (sparseint$-trailing-0-count-width width offset negbit x)
   (sparseint$-trailing-0-count-width width offset-equiv negbit x)))
 :rule-classes :congruence)

Theorem: sparseint$-trailing-0-count-width-of-bfix-negbit

(defthm sparseint$-trailing-0-count-width-of-bfix-negbit
  (equal
       (sparseint$-trailing-0-count-width width offset (bfix negbit)
                                          x)
       (sparseint$-trailing-0-count-width width offset negbit x)))

Theorem: sparseint$-trailing-0-count-width-bit-equiv-congruence-on-negbit

(defthm
   sparseint$-trailing-0-count-width-bit-equiv-congruence-on-negbit
 (implies
  (bit-equiv negbit negbit-equiv)
  (equal
   (sparseint$-trailing-0-count-width width offset negbit x)
   (sparseint$-trailing-0-count-width width offset negbit-equiv x)))
 :rule-classes :congruence)

Theorem: sparseint$-trailing-0-count-width-of-sparseint$-fix-x

(defthm sparseint$-trailing-0-count-width-of-sparseint$-fix-x
  (equal (sparseint$-trailing-0-count-width
              width offset negbit (sparseint$-fix x))
         (sparseint$-trailing-0-count-width width offset negbit x)))

Theorem: sparseint$-trailing-0-count-width-sparseint$-equiv-congruence-on-x

(defthm
 sparseint$-trailing-0-count-width-sparseint$-equiv-congruence-on-x
 (implies
  (sparseint$-equiv x x-equiv)
  (equal
   (sparseint$-trailing-0-count-width width offset negbit x)
   (sparseint$-trailing-0-count-width width offset negbit x-equiv)))
 :rule-classes :congruence)