		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Unrev-block-index

Signature
(unrev-block-index i nbits blocksz) → idx
Arguments: i — Guard (natp i).; nbits — Guard (natp nbits).; blocksz — Guard (posp blocksz).
Returns: idx — Type (natp idx).

Definitions and Theorems

Function: unrev-block-index

(defun unrev-block-index (i nbits blocksz)
  (declare (xargs :guard (and (natp i)
                              (natp nbits)
                              (posp blocksz))))
  (let ((__function__ 'unrev-block-index))
    (declare (ignorable __function__))
    (b* ((nbits (lnfix nbits))
         (blocksz (mbe :logic (pos-fix blocksz)
                       :exec blocksz))
         (i (lnfix i))
         ((when (< nbits blocksz)) i)
         (next-nbits (- nbits blocksz))
         ((when (< i blocksz)) (+ i next-nbits)))
      (unrev-block-index (- i blocksz)
                         next-nbits blocksz))))

Theorem: natp-of-unrev-block-index

(defthm natp-of-unrev-block-index
  (b* ((idx (unrev-block-index i nbits blocksz)))
    (natp idx))
  :rule-classes :type-prescription)

Theorem: logbitp-of-sparseint-unrev-blocks

(defthm logbitp-of-sparseint-unrev-blocks
 (equal
  (logbitp i
           (sparseint-val (sparseint-unrev-blocks nbits blocksz x)))
  (and (< (nfix i) (nfix nbits))
       (logbitp (unrev-block-index i nbits blocksz)
                (sparseint-val x)))))

Theorem: unrev-of-rev-block-index

(defthm unrev-of-rev-block-index
  (implies
       (< (nfix i) (nfix nbits))
       (equal (unrev-block-index (rev-block-index i nbits blocksz)
                                 nbits blocksz)
              (nfix i))))

Theorem: unrev-block-index-bound

(defthm unrev-block-index-bound
  (implies (< (nfix i) (nfix nbits))
           (< (unrev-block-index i nbits blocksz)
              (nfix nbits)))
  :rule-classes :linear)

Theorem: rev-block-index-bound

(defthm rev-block-index-bound
  (implies (< (nfix i) (nfix nbits))
           (< (rev-block-index i nbits blocksz)
              (nfix nbits)))
  :rule-classes :linear)

Theorem: rev-of-unrev-block-index

(defthm rev-of-unrev-block-index
  (implies
       (< (nfix i) (nfix nbits))
       (equal (rev-block-index (unrev-block-index i nbits blocksz)
                               nbits blocksz)
              (nfix i))))

Theorem: sparseint-unrev-blocks-correct1

(defthm sparseint-unrev-blocks-correct1
 (equal
  (sparseint-val
    (sparseint-unrev-blocks nbits blocksz
                            (sparseint-rev-blocks nbits blocksz x)))
  (loghead nbits (sparseint-val x))))

Theorem: sparseint-unrev-blocks-correct2

(defthm sparseint-unrev-blocks-correct2
 (equal
  (sparseint-val
    (sparseint-rev-blocks nbits blocksz
                          (sparseint-unrev-blocks nbits blocksz x)))
  (loghead nbits (sparseint-val x))))