		Search-engine friendly clone of the ACL2 documentation.

4vec-rev-blocks

Rev-blocks

Reverses blocks, like the streaming concatenation operator in SystemVerilog.

Signature
(rev-blocks nbits blocksz x) → res
Arguments: nbits — Guard (natp nbits).; blocksz — Guard (posp blocksz).; x — Guard (integerp x).
Returns: res — Type (natp res).

Example:

(equal (rev-blocks 28 8 #xaabbccdd) #xddccbba)

This essentially truncates x to nbits bits, then divides this into blocks of size blocksz, starting from least significant bits, where the last block (corresponding to the most significant bits of x) may be smaller. Then it reverses the order of these blocks. So in the example above, the most significant #xa is dropped, and the rest is divided into the blocks a bb cc dd, which are then reversed.

Definitions and Theorems

Function: rev-blocks

(defun rev-blocks (nbits blocksz x)
  (declare (xargs :guard (and (natp nbits)
                              (posp blocksz)
                              (integerp x))))
  (let ((__function__ 'rev-blocks))
    (declare (ignorable __function__))
    (b* ((nbits (lnfix nbits))
         (blocksz (mbe :logic (pos-fix blocksz)
                       :exec blocksz))
         ((when (< nbits blocksz))
          (loghead nbits x))
         (next-nbits (- nbits blocksz))
         (rest (rev-blocks next-nbits
                           blocksz (ash x (- blocksz)))))
      (logapp next-nbits rest (loghead blocksz x)))))

Theorem: natp-of-rev-blocks

(defthm natp-of-rev-blocks
  (b* ((res (rev-blocks nbits blocksz x)))
    (natp res))
  :rule-classes :type-prescription)

Theorem: rev-blocks-of-nfix-nbits

(defthm rev-blocks-of-nfix-nbits
  (equal (rev-blocks (nfix nbits) blocksz x)
         (rev-blocks nbits blocksz x)))

Theorem: rev-blocks-nat-equiv-congruence-on-nbits

(defthm rev-blocks-nat-equiv-congruence-on-nbits
  (implies (nat-equiv nbits nbits-equiv)
           (equal (rev-blocks nbits blocksz x)
                  (rev-blocks nbits-equiv blocksz x)))
  :rule-classes :congruence)

Theorem: rev-blocks-of-pos-fix-blocksz

(defthm rev-blocks-of-pos-fix-blocksz
  (equal (rev-blocks nbits (pos-fix blocksz) x)
         (rev-blocks nbits blocksz x)))

Theorem: rev-blocks-pos-equiv-congruence-on-blocksz

(defthm rev-blocks-pos-equiv-congruence-on-blocksz
  (implies (pos-equiv blocksz blocksz-equiv)
           (equal (rev-blocks nbits blocksz x)
                  (rev-blocks nbits blocksz-equiv x)))
  :rule-classes :congruence)

Theorem: rev-blocks-of-ifix-x

(defthm rev-blocks-of-ifix-x
  (equal (rev-blocks nbits blocksz (ifix x))
         (rev-blocks nbits blocksz x)))

Theorem: rev-blocks-int-equiv-congruence-on-x

(defthm rev-blocks-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (rev-blocks nbits blocksz x)
                  (rev-blocks nbits blocksz x-equiv)))
  :rule-classes :congruence)