		Search-engine friendly clone of the ACL2 documentation.

Integer-formats

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))))
  (b*
   ((bit-size (integer-format->bit-size short-format))
    (signed-short-min (integer-format->signed-min short-format))
    (signed-short-max (integer-format->signed-max short-format))
    (unsigned-short-max (integer-format->unsigned-max 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 (/ bit-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-wf-bit-size-lower-bound

(defthm integer-format-short-wf-bit-size-lower-bound
 (implies
    (integer-format-short-wfp short-format uchar-format schar-fomat)
    (>= (integer-format->bit-size short-format)
        16))
 :rule-classes :linear)

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)