		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Sinteger-format->max

The ACL2 integer value of the maximum value representable in a signed integer format.

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

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

Definitions and Theorems

Function: sinteger-format->max

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

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

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

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

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

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

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