		Search-engine friendly clone of the ACL2 documentation.

Bitops/extra-defs

Nth-slice512

Extract the nth 512-bit slice of the integer x.

Signature
(nth-slice512 n x) → slice
Arguments: n — Guard (natp n).; x — Guard (integerp x).
Returns: slice — Type (natp slice).

We leave this enabled; we would usually not expect to try to reason about it.

Definitions and Theorems

Function: nth-slice512$inline

(defun acl2::nth-slice512$inline (n x)
 (declare (xargs :guard (and (natp n) (integerp x))))
 (let ((__function__ 'nth-slice512))
  (declare (ignorable __function__))
  (mbe
   :logic (logand (ash (ifix x) (* (nfix n) -512))
                  (1- (expt 2 512)))
   :exec
   (the
    (unsigned-byte 512)
    (logand
     (ash x (the (integer * 0) (* n -512)))
     13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084095)))))

Theorem: natp-of-nth-slice512

(defthm acl2::natp-of-nth-slice512
  (b* ((slice (acl2::nth-slice512$inline n x)))
    (natp slice))
  :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-nth-slice512-1

(defthm nat-equiv-implies-equal-nth-slice512-1
  (implies (nat-equiv n n-equiv)
           (equal (nth-slice512 n x)
                  (nth-slice512 n-equiv x)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-nth-slice512-2

(defthm int-equiv-implies-equal-nth-slice512-2
  (implies (int-equiv x x-equiv)
           (equal (nth-slice512 n x)
                  (nth-slice512 n x-equiv)))
  :rule-classes (:congruence))

Theorem: unsigned-byte-p-512-of-nth-slice512

(defthm unsigned-byte-p-512-of-nth-slice512
  (unsigned-byte-p 512 (nth-slice512 n x)))

Theorem: nth-slice512-is-nth-slice

(defthm nth-slice512-is-nth-slice
  (equal (nth-slice512 n x)
         (nth-slice 512 n x)))