		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format-short-wfp

Check if an integer format is well-formed when used for (signed and unsigned) short.

Signature
(integer-format-short-wfp short-format uchar-format schar-format) → yes/no
Arguments: short-format — Guard (integer-formatp short-format).; uchar-format — Guard (uchar-formatp uchar-format).; schar-format — Guard (schar-formatp schar-format).
Returns: yes/no — Type (booleanp yes/no).

The number of bits must be a multiple of CHAR_BIT [C17:6.2.6.1/4].

The possible signed values must cover at least the range from -32767 to +32767 (both inclusive) [C17:5.2.4.2.1/1]. The possible unsigned values must cover at least the range from 0 to 65535 (both inclusive) [C17:5.2.4.2.1/1].

The possible signed values must at least include those of signed char, and the possible unsigned values must at least include those of unsigned char [C17:6.2.5/8].

Definitions and Theorems

Function: integer-format-short-wfp

(defun integer-format-short-wfp
       (short-format uchar-format schar-format)
 (declare (xargs :guard (and (integer-formatp short-format)
                             (uchar-formatp uchar-format)
                             (schar-formatp schar-format))))
 (let ((__function__ 'integer-format-short-wfp))
   (declare (ignorable __function__))
   (b*
    ((size (integer-format->size short-format))
     (signed-short-min
          (sinteger-format->min
               (uinteger+sinteger-format->signed
                    (integer-format->pair short-format))))
     (signed-short-max
          (sinteger-format->max
               (uinteger+sinteger-format->signed
                    (integer-format->pair short-format))))
     (unsigned-short-max
          (uinteger-format->max
               (uinteger+sinteger-format->unsigned
                    (integer-format->pair short-format))))
     (signed-char-min (schar-format->min schar-format uchar-format))
     (signed-char-max (schar-format->max schar-format uchar-format))
     (unsigned-char-max (uchar-format->max uchar-format)))
    (and (integerp (/ size (uchar-format->size uchar-format)))
         (<= signed-short-min -32767)
         (<= 32767 signed-short-max)
         (<= 65535 unsigned-short-max)
         (<= signed-short-min signed-char-min)
         (<= signed-char-max signed-short-max)
         (<= unsigned-char-max
             unsigned-short-max)))))

Theorem: booleanp-of-integer-format-short-wfp

(defthm booleanp-of-integer-format-short-wfp
 (b* ((yes/no (integer-format-short-wfp short-format
                                        uchar-format schar-format)))
   (booleanp yes/no))
 :rule-classes :rewrite)

Theorem: integer-format-short-wfp-of-integer-format-fix-short-format

(defthm integer-format-short-wfp-of-integer-format-fix-short-format
  (equal (integer-format-short-wfp (integer-format-fix short-format)
                                   uchar-format schar-format)
         (integer-format-short-wfp short-format
                                   uchar-format schar-format)))

Theorem: integer-format-short-wfp-integer-format-equiv-congruence-on-short-format

(defthm
 integer-format-short-wfp-integer-format-equiv-congruence-on-short-format
 (implies
  (integer-format-equiv short-format short-format-equiv)
  (equal
   (integer-format-short-wfp short-format uchar-format schar-format)
   (integer-format-short-wfp short-format-equiv
                             uchar-format schar-format)))
 :rule-classes :congruence)

Theorem: integer-format-short-wfp-of-uchar-format-fix-uchar-format

(defthm integer-format-short-wfp-of-uchar-format-fix-uchar-format
  (equal (integer-format-short-wfp short-format
                                   (uchar-format-fix uchar-format)
                                   schar-format)
         (integer-format-short-wfp short-format
                                   uchar-format schar-format)))

Theorem: integer-format-short-wfp-uchar-format-equiv-congruence-on-uchar-format

(defthm
 integer-format-short-wfp-uchar-format-equiv-congruence-on-uchar-format
 (implies
  (uchar-format-equiv uchar-format uchar-format-equiv)
  (equal
   (integer-format-short-wfp short-format uchar-format schar-format)
   (integer-format-short-wfp short-format
                             uchar-format-equiv schar-format)))
 :rule-classes :congruence)

Theorem: integer-format-short-wfp-of-schar-format-fix-schar-format

(defthm integer-format-short-wfp-of-schar-format-fix-schar-format
  (equal (integer-format-short-wfp short-format uchar-format
                                   (schar-format-fix schar-format))
         (integer-format-short-wfp short-format
                                   uchar-format schar-format)))

Theorem: integer-format-short-wfp-schar-format-equiv-congruence-on-schar-format

(defthm
 integer-format-short-wfp-schar-format-equiv-congruence-on-schar-format
 (implies
  (schar-format-equiv schar-format schar-format-equiv)
  (equal
   (integer-format-short-wfp short-format uchar-format schar-format)
   (integer-format-short-wfp short-format
                             uchar-format schar-format-equiv)))
 :rule-classes :congruence)