		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Rdb

(rdb bsp i) returns the byte of i specified by bsp.

Signature
(rdb bsp i) → nat
Arguments: bsp — Guard (bspp bsp).; i — Guard (integerp i).
Returns: nat — Type (and (integerp nat) (>= nat 0)).

This is analogous to Common Lisp's (ldb bytespec integer).

Definitions and Theorems

Function: rdb

(defun rdb (bsp i)
  (declare (xargs :guard (and (bspp bsp) (integerp i))))
  (let ((__function__ 'rdb))
    (declare (ignorable __function__))
    (loghead (bsp-size bsp)
             (logtail (bsp-position bsp) i))))

Theorem: rdb-type

(defthm rdb-type
  (b* ((nat (rdb bsp i)))
    (and (integerp nat) (>= nat 0)))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-rdb

(defthm unsigned-byte-p-rdb
  (implies (and (>= size (bsp-size bsp))
                (force (>= size 0))
                (force (integerp size))
                (force (bspp bsp)))
           (unsigned-byte-p size (rdb bsp i))))

Theorem: rdb-upper-bound

(defthm rdb-upper-bound
  (implies (force (bspp bsp))
           (< (rdb bsp i) (expt 2 (bsp-size bsp))))
  :rule-classes (:linear :rewrite))

Theorem: bitp-rdb-bsp-1

(defthm bitp-rdb-bsp-1
  (implies (equal (bsp-size bsp) 1)
           (bitp (rdb bsp i))))