		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Int-to-sparseint$-rec

Signature
(int-to-sparseint$-rec x width lsb) → (mv sint height width-out)
Arguments: x — Guard (integerp x).; width — Guard (posp width).; lsb — Guard (natp lsb).
Returns: sint — Type (sparseint$-p sint).; height — Type (equal height (sparseint$-height sint)).; width-out — Type (posp width-out).

Definitions and Theorems

Function: int-to-sparseint$-rec

(defun int-to-sparseint$-rec (x width lsb)
  (declare (xargs :guard (and (integerp x)
                              (posp width)
                              (natp lsb))))
  (let ((__function__ 'int-to-sparseint$-rec))
    (declare (ignorable __function__))
    (b* ((width (lposfix width))
         ((when (< width (sparseint$-leaf-bitlimit)))
          (b* ((end (+ width (lnfix lsb)))
               (bit (logbitp (1- end) x))
               (offset (if bit (trailing-1-count-from x end)
                         (trailing-0-count-from x end))))
            (mv (sparseint$-leaf (fast-part-extend x width lsb))
                0 (+ width offset))))
         (half (logcdr width))
         ((mv lsbs lsbs-height lsbs-width)
          (int-to-sparseint$-rec x half lsb))
         ((when (<= width lsbs-width))
          (mv lsbs lsbs-height lsbs-width))
         (lsbs-width (mbe :logic (max half (pos-fix lsbs-width))
                          :exec lsbs-width))
         ((mv msbs msbs-height msbs-width)
          (int-to-sparseint$-rec x (- width lsbs-width)
                                 (+ (lnfix lsb) lsbs-width)))
         ((mv concat concat-height)
          (sparseint$-concatenate-rebalance
               lsbs-width
               lsbs lsbs-height msbs msbs-height)))
      (mv concat concat-height
          (+ lsbs-width msbs-width)))))

Theorem: sparseint$-p-of-int-to-sparseint$-rec.sint

(defthm sparseint$-p-of-int-to-sparseint$-rec.sint
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (sparseint$-p sint))
  :rule-classes :rewrite)

Theorem: return-type-of-int-to-sparseint$-rec.height

(defthm return-type-of-int-to-sparseint$-rec.height
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (equal height (sparseint$-height sint)))
  :rule-classes :rewrite)

Theorem: posp-of-int-to-sparseint$-rec.width-out

(defthm posp-of-int-to-sparseint$-rec.width-out
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (posp width-out))
  :rule-classes :type-prescription)

Theorem: width-out-gte-width-of-int-to-sparseint$-rec

(defthm width-out-gte-width-of-int-to-sparseint$-rec
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (<= (pos-fix width) width-out))
  :rule-classes :linear)

Theorem: sparseint$-height-correctp-of-int-to-sparseint$-rec

(defthm sparseint$-height-correctp-of-int-to-sparseint$-rec
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (sparseint$-height-correctp sint)))

Theorem: sparseint$-val-of-int-to-sparseint$-rec

(defthm sparseint$-val-of-int-to-sparseint$-rec
  (b* (((mv ?sint ?height ?width-out)
        (int-to-sparseint$-rec x width lsb)))
    (equal (sparseint$-val sint)
           (logext width-out (logtail lsb x)))))

Theorem: int-to-sparseint$-rec-unchanged

(defthm int-to-sparseint$-rec-unchanged
  (implies (and (< width (sparseint$-leaf-bitlimit))
                (< (integer-length x) width)
                (posp width))
           (equal (mv-nth 0 (int-to-sparseint$-rec x width 0))
                  (ifix x))))

Theorem: int-to-sparseint$-rec-of-ifix-x

(defthm int-to-sparseint$-rec-of-ifix-x
  (equal (int-to-sparseint$-rec (ifix x)
                                width lsb)
         (int-to-sparseint$-rec x width lsb)))

Theorem: int-to-sparseint$-rec-int-equiv-congruence-on-x

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

Theorem: int-to-sparseint$-rec-of-pos-fix-width

(defthm int-to-sparseint$-rec-of-pos-fix-width
  (equal (int-to-sparseint$-rec x (pos-fix width)
                                lsb)
         (int-to-sparseint$-rec x width lsb)))

Theorem: int-to-sparseint$-rec-pos-equiv-congruence-on-width

(defthm int-to-sparseint$-rec-pos-equiv-congruence-on-width
  (implies (pos-equiv width width-equiv)
           (equal (int-to-sparseint$-rec x width lsb)
                  (int-to-sparseint$-rec x width-equiv lsb)))
  :rule-classes :congruence)

Theorem: int-to-sparseint$-rec-of-nfix-lsb

(defthm int-to-sparseint$-rec-of-nfix-lsb
  (equal (int-to-sparseint$-rec x width (nfix lsb))
         (int-to-sparseint$-rec x width lsb)))

Theorem: int-to-sparseint$-rec-nat-equiv-congruence-on-lsb

(defthm int-to-sparseint$-rec-nat-equiv-congruence-on-lsb
  (implies (nat-equiv lsb lsb-equiv)
           (equal (int-to-sparseint$-rec x width lsb)
                  (int-to-sparseint$-rec x width lsb-equiv)))
  :rule-classes :congruence)