		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format-int-wfp

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

Signature
(integer-format-int-wfp int-format uchar-format short-format) → yes/no
Arguments: int-format — Guard (integer-formatp int-format).; uchar-format — Guard (uchar-formatp uchar-format).; short-format — Guard (integer-formatp short-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 short, and the possible unsigned values must at least include those of unsigned short [C17:6.2.5/8].

Definitions and Theorems

Function: integer-format-int-wfp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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