• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
        • Sparseint-impl
          • Sparseint$-binary-bitop-width
          • Sparseint$-plus-width
          • Sparseint$-binary-bitop-offset
          • Sparseint$-binary-bitop-int-width
          • Sparseint$-plus-int-width
          • Sum-with-cin
          • Sparseint$-plus-offset
          • Sparseint$-binary-bitop-int
          • Sparseint$-finalize-concat
          • Sparseint$-plus-int
          • Sparseint$-binary-bittest-width
          • Sparseint$-binary-bittest-int-width
          • Sparseint$-trailing-0-count-width
          • Sparseint$-height
          • Int-to-sparseint$-rec
          • Carry-out
          • Sparseint$-compare-width
          • Sparseint$-binary-bittest-offset
          • Sparseint$-equal-width
          • Sparseint$-binary-bittest-int
          • Sparseint$-compare-int-width
          • Sparseint$-bitcount-width
          • Sparseint$-unary-bittest-width
          • Sparseint$-rightshift-rec
          • Sparseint$-equal-int-width
          • Sparseint$-trailing-0-count-rec
          • Sparseint$-unary-bitop
          • Sparseint$-concatenate
          • Sparseint$-length-width-rec
          • Sparseint$-sign-ext
          • Sparseint$-binary-bitop
          • Binary-bitop
          • Sparseint$-compare-offset
          • Sparseint$-unary-bittest-offset
          • Sparseint$-equal-offset
          • Sparseint$-truncate
          • Sparseint$-mergeable-leaves-p
          • Carry-out-bit
          • Sparseint$-truncate-height
          • Sparseint$-compare-int
          • Sparseint$-binary-bittest
          • Sparseint$-equal-int
          • Sparseint$-rightshift
          • Sparseint$-leaves-mergeable-p
          • Sparseint$-plus
          • Unary-bitop
          • Sparseint$-bitcount-rec
          • Within-1
          • Sparseint$
          • Binary-bitop-cofactor2
          • Binary-bitop-cofactor1
          • Sparseint$-compare
          • Sparseint$-unary-bittest
          • Sparseint$-height-correct-exec
          • Sparseint$-equal
          • Sparseint$-bitnot
          • Sparseint$-unary-minus
          • Sparseint$-bit
          • Int-to-sparseint$
          • Binary-bittest
          • Sparseint$-length-rec
          • Sparseint$-val
          • Binary-bitop-swap
          • Compare
          • Sparseint$-real-height
          • Sparseint$-height-correctp
          • Sparseint$-length
        • Sparseint-p
        • Sparseint-binary-bittest
        • Sparseint-concatenate
        • Sparseint-binary-bitop
        • Sparseint-bitite
        • Sparseint-fix
        • Sparseint$-binary-minus
        • Sparseint-trailing-1-count-from
        • Sparseint-trailing-0-count-from
        • Sparseint-equal
        • Sparseint-test-bitorc2
        • Sparseint-test-bitorc1
        • Sparseint-test-bitnand
        • Sparseint-test-bitandc2
        • Sparseint-test-bitandc1
        • Sparseint-test-bitand
        • Sparseint-rightshift
        • Sparseint-bitcount-from
        • Sparseint-test-bitxor
        • Sparseint-test-bitor
        • Sparseint-test-bitnor
        • Sparseint-test-biteqv
        • Sparseint-compare
        • Sparseint-binary-minus
        • Sparseint-sign-ext
        • Sparseint-plus
        • Sparseint-bitandc2
        • Sparseint-bitandc1
        • Sparseint-bitand
        • Sparseint$-leaf-bitlimit
        • Sparseint-bitxor
        • Sparseint-bitorc2
        • Sparseint-bitorc1
        • Sparseint-bitor
        • Sparseint-bitnor
        • Sparseint-bitnand
        • Sparseint-biteqv
        • Sparseint-ash
        • Sparseint-<
        • Sparseint-bit
        • Sparseint-trailing-1-count
        • Sparseint-trailing-0-count
        • Sparseint-unary-minus
        • Sparseint-length
        • Sparseint-bitnot
        • Sparseint-bitcount
        • Int-to-sparseint
        • Sparseint-val
      • Bitops
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Sparseint-impl

Sparseint$-trailing-0-count-rec

Signature

(sparseint$-trailing-0-count-rec offset negbit x) → count

Arguments

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-rec

(defun sparseint$-trailing-0-count-rec (offset negbit x)
 (declare (xargs :guard (and (natp offset)
                             (bitp negbit)
                             (sparseint$-p x))))
 (let ((__function__ 'sparseint$-trailing-0-count-rec))
  (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))
     (if (eql negbit 1)
         (trailing-1-count-from x.val offset)
       (trailing-0-count-from x.val offset)))
   :concat
   (b*
    ((offset (lnfix offset))
     ((when (<= x.width offset))
      (sparseint$-trailing-0-count-rec (- offset x.width)
                                       negbit x.msbs))
     (width1 (- x.width offset))
     (lsbs-count (sparseint$-trailing-0-count-width
                      width1 offset negbit x.lsbs))
     ((when lsbs-count) lsbs-count)
     (msbs-count (sparseint$-trailing-0-count-rec 0 negbit x.msbs)))
    (and msbs-count (+ width1 msbs-count))))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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