		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Sinteger-format->min

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

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

This is determined by the number M of value bits, the signed format, and possibly the trap representations [C17:6.2.6.2/2]. If the signed format is either sign and magnitude or ones' complement, the minimum value is the negation of the maximum value, i.e. - (2^M - 1). If the signed format is two's complement, there are two possibilities: if the representation with sign bit 1 and all value bits 0 is a trap representation, the minimum value is - (2^M - 1); otherwise, it is - 2^M. As explained in sinteger-format, currently we do not have a detailed model of trap representations; as a placeholder, for now we regard that representation to be a trap one iff the traps component of sinteger-format is not nil.

Since M <= T - 1, where T is the total number of bits, and where the 1 accounts for the sign bit, the minimum value cannot be below - 2^(T-1).

Definitions and Theorems

Function: sinteger-format->min

(defun sinteger-format->min (format)
 (declare (xargs :guard (sinteger-formatp format)))
 (let ((__function__ 'sinteger-format->min))
  (declare (ignorable __function__))
  (if
   (and (equal (signed-format-kind (sinteger-format->signed format))
               :twos-complement)
        (not (sinteger-format->traps format)))
   (- (expt 2
            (sinteger-bit-roles-value-count
                 (sinteger-format->bits format))))
   (- (1- (expt 2
                (sinteger-bit-roles-value-count
                     (sinteger-format->bits format))))))))

Theorem: integerp-of-sinteger-format->min

(defthm integerp-of-sinteger-format->min
  (b* ((min (sinteger-format->min format)))
    (integerp min))
  :rule-classes :rewrite)

Theorem: sinteger-format->min-type-prescription

(defthm sinteger-format->min-type-prescription
  (b* ((common-lisp::?min (sinteger-format->min format)))
    (and (integerp min) (< min 0)))
  :rule-classes :type-prescription)

Theorem: sinteger-format->min-lower-bound

(defthm sinteger-format->min-lower-bound
  (b* ((common-lisp::?min (sinteger-format->min format)))
    (>= min
        (- (expt 2
                 (1- (len (sinteger-format->bits format)))))))
  :rule-classes :linear)

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

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

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

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