		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-length-width-rec

Signature
(sparseint$-length-width-rec width tail x) → length
Arguments: width — Guard (posp width).; tail — Guard (integerp tail).; x — Guard (sparseint$-p x).
Returns: length — Type (integerp length).

Definitions and Theorems

Function: sparseint$-length-width-rec

(defun sparseint$-length-width-rec (width tail x)
 (declare (xargs :guard (and (posp width)
                             (integerp tail)
                             (sparseint$-p x))))
 (let ((__function__ 'sparseint$-length-width-rec))
  (declare (ignorable __function__))
  (b* ((width (lposfix width)))
   (sparseint$-case
       x :leaf
       (b* ((val (logapp width x.val tail))
            ((when (eql val 0)) 0)
            ((when (eql val -1)) -1))
         (integer-length val))
       :concat
       (b* (((when (<= width x.width))
             (sparseint$-length-width-rec width tail x.lsbs))
            (tail/len (sparseint$-length-width-rec (- width x.width)
                                                   tail x.msbs))
            ((when (< 0 tail/len))
             (+ x.width tail/len)))
         (sparseint$-length-width-rec x.width tail/len x.lsbs))))))

Theorem: integerp-of-sparseint$-length-width-rec

(defthm integerp-of-sparseint$-length-width-rec
  (b* ((length (sparseint$-length-width-rec width tail x)))
    (integerp length))
  :rule-classes :type-prescription)

Theorem: sparseint$-length-width-rec-correct

(defthm sparseint$-length-width-rec-correct
  (b* ((common-lisp::?length
            (sparseint$-length-width-rec width tail x)))
    (and (implies (and (< 0 length)
                       (<= -1 (ifix tail))
                       (<= (ifix tail) 0))
                  (equal length
                         (integer-length (logapp (pos-fix width)
                                                 (sparseint$-val x)
                                                 tail))))
         (implies (and (<= length 0)
                       (<= -1 (ifix tail))
                       (<= (ifix tail) 0))
                  (and (equal length (ifix tail))
                       (equal (logext width (sparseint$-val x))
                              (ifix tail))))
         (<= -1 length))))

Theorem: sparseint$-length-width-rec-of-pos-fix-width

(defthm sparseint$-length-width-rec-of-pos-fix-width
  (equal (sparseint$-length-width-rec (pos-fix width)
                                      tail x)
         (sparseint$-length-width-rec width tail x)))

Theorem: sparseint$-length-width-rec-pos-equiv-congruence-on-width

(defthm sparseint$-length-width-rec-pos-equiv-congruence-on-width
  (implies (pos-equiv width width-equiv)
           (equal (sparseint$-length-width-rec width tail x)
                  (sparseint$-length-width-rec width-equiv tail x)))
  :rule-classes :congruence)

Theorem: sparseint$-length-width-rec-of-ifix-tail

(defthm sparseint$-length-width-rec-of-ifix-tail
  (equal (sparseint$-length-width-rec width (ifix tail)
                                      x)
         (sparseint$-length-width-rec width tail x)))

Theorem: sparseint$-length-width-rec-int-equiv-congruence-on-tail

(defthm sparseint$-length-width-rec-int-equiv-congruence-on-tail
  (implies (int-equiv tail tail-equiv)
           (equal (sparseint$-length-width-rec width tail x)
                  (sparseint$-length-width-rec width tail-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint$-length-width-rec-of-sparseint$-fix-x

(defthm sparseint$-length-width-rec-of-sparseint$-fix-x
  (equal (sparseint$-length-width-rec width tail (sparseint$-fix x))
         (sparseint$-length-width-rec width tail x)))

Theorem: sparseint$-length-width-rec-sparseint$-equiv-congruence-on-x

(defthm sparseint$-length-width-rec-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-length-width-rec width tail x)
                  (sparseint$-length-width-rec width tail x-equiv)))
  :rule-classes :congruence)