		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex-lhs-preproc-blkrev

Signature
(svex-lhs-preproc-blkrev nbits blocksz x) → blkrev
Arguments: nbits — Guard (natp nbits).; blocksz — Guard (posp blocksz).; x — Guard (svex-p x).
Returns: blkrev — Type (svex-p blkrev).

Definitions and Theorems

Function: svex-lhs-preproc-blkrev

(defun svex-lhs-preproc-blkrev (nbits blocksz x)
 (declare (xargs :guard (and (natp nbits)
                             (posp blocksz)
                             (svex-p x))))
 (let ((__function__ 'svex-lhs-preproc-blkrev))
  (declare (ignorable __function__))
  (b*
   ((nbits (lnfix nbits))
    (blocksz (lposfix blocksz))
    ((when (< nbits blocksz))
     (svcall concat (svex-int nbits) x 0))
    (next-nbits (- nbits blocksz))
    (rest
       (svex-lhs-preproc-blkrev next-nbits blocksz
                                (svcall rsh (svex-int blocksz) x))))
   (svcall concat (svex-quote (2vec next-nbits))
           rest
           (svcall concat (svex-int blocksz)
                   x 0)))))

Theorem: svex-p-of-svex-lhs-preproc-blkrev

(defthm svex-p-of-svex-lhs-preproc-blkrev
  (b* ((blkrev (svex-lhs-preproc-blkrev nbits blocksz x)))
    (svex-p blkrev))
  :rule-classes :rewrite)

Theorem: svex-lhs-preproc-blkrev-correct

(defthm svex-lhs-preproc-blkrev-correct
  (b* ((?blkrev (svex-lhs-preproc-blkrev nbits blocksz x)))
    (equal (svex-eval blkrev env)
           (4vec-rev-blocks (2vec (nfix nbits))
                            (2vec (pos-fix blocksz))
                            (svex-eval x env)))))

Theorem: svex-lhs-preproc-blkrev-vars

(defthm svex-lhs-preproc-blkrev-vars
  (b* ((?blkrev (svex-lhs-preproc-blkrev nbits blocksz x)))
    (equal (svex-vars blkrev)
           (svex-vars x))))

Theorem: svex-lhs-preproc-blkrev-of-nfix-nbits

(defthm svex-lhs-preproc-blkrev-of-nfix-nbits
  (equal (svex-lhs-preproc-blkrev (nfix nbits)
                                  blocksz x)
         (svex-lhs-preproc-blkrev nbits blocksz x)))

Theorem: svex-lhs-preproc-blkrev-nat-equiv-congruence-on-nbits

(defthm svex-lhs-preproc-blkrev-nat-equiv-congruence-on-nbits
  (implies (nat-equiv nbits nbits-equiv)
           (equal (svex-lhs-preproc-blkrev nbits blocksz x)
                  (svex-lhs-preproc-blkrev nbits-equiv blocksz x)))
  :rule-classes :congruence)

Theorem: svex-lhs-preproc-blkrev-of-pos-fix-blocksz

(defthm svex-lhs-preproc-blkrev-of-pos-fix-blocksz
  (equal (svex-lhs-preproc-blkrev nbits (pos-fix blocksz)
                                  x)
         (svex-lhs-preproc-blkrev nbits blocksz x)))

Theorem: svex-lhs-preproc-blkrev-pos-equiv-congruence-on-blocksz

(defthm svex-lhs-preproc-blkrev-pos-equiv-congruence-on-blocksz
  (implies (pos-equiv blocksz blocksz-equiv)
           (equal (svex-lhs-preproc-blkrev nbits blocksz x)
                  (svex-lhs-preproc-blkrev nbits blocksz-equiv x)))
  :rule-classes :congruence)

Theorem: svex-lhs-preproc-blkrev-of-svex-fix-x

(defthm svex-lhs-preproc-blkrev-of-svex-fix-x
  (equal (svex-lhs-preproc-blkrev nbits blocksz (svex-fix x))
         (svex-lhs-preproc-blkrev nbits blocksz x)))

Theorem: svex-lhs-preproc-blkrev-svex-equiv-congruence-on-x

(defthm svex-lhs-preproc-blkrev-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-lhs-preproc-blkrev nbits blocksz x)
                  (svex-lhs-preproc-blkrev nbits blocksz x-equiv)))
  :rule-classes :congruence)