		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-format->max

The ACL2 integer value of the maximum value representable in an unsigned integer format.

Signature
(uinteger-format->max format) → max
Arguments: format — Guard (uinteger-formatp format).
Returns: max — Type (posp max).

This is determined by the number N of value bits: the maximum value is 2^N - 1.

Since N <= T, where T is the total number of bits, the maximum value cannot be above 2^T - 1.

Definitions and Theorems

Function: uinteger-format->max

(defun uinteger-format->max (format)
  (declare (xargs :guard (uinteger-formatp format)))
  (let ((__function__ 'uinteger-format->max))
    (declare (ignorable __function__))
    (1- (expt 2
              (uinteger-bit-roles-value-count
                   (uinteger-format->bits format))))))

Theorem: posp-of-uinteger-format->max

(defthm posp-of-uinteger-format->max
  (b* ((max (uinteger-format->max format)))
    (posp max))
  :rule-classes (:rewrite :type-prescription))

Theorem: uinteger-format->max-upper-bound

(defthm uinteger-format->max-upper-bound
  (b* ((common-lisp::?max (uinteger-format->max format)))
    (<= max
        (1- (expt 2
                  (len (uinteger-format->bits format))))))
  :rule-classes :linear)

Theorem: uinteger-format->max-of-uinteger-format-fix-format

(defthm uinteger-format->max-of-uinteger-format-fix-format
  (equal (uinteger-format->max (uinteger-format-fix format))
         (uinteger-format->max format)))

Theorem: uinteger-format->max-uinteger-format-equiv-congruence-on-format

(defthm
    uinteger-format->max-uinteger-format-equiv-congruence-on-format
  (implies (uinteger-format-equiv format format-equiv)
           (equal (uinteger-format->max format)
                  (uinteger-format->max format-equiv)))
  :rule-classes :congruence)