		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format-long-wfp

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

Signature
(integer-format-long-wfp long-format uchar-format int-format) → yes/no
Arguments: long-format — Guard (integer-formatp long-format).; uchar-format — Guard (uchar-formatp uchar-format).; int-format — Guard (integer-formatp int-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 -2147483647 to +2147483647 (both inclusive) [C17:5.2.4.2.1/1]. The possible unsigned values must cover at least the range from 0 to 4294967295 (both inclusive) [C17:5.2.4.2.1/1].

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

Definitions and Theorems

Function: integer-format-long-wfp

(defun integer-format-long-wfp (long-format uchar-format int-format)
 (declare (xargs :guard (and (integer-formatp long-format)
                             (uchar-formatp uchar-format)
                             (integer-formatp int-format))))
 (let ((__function__ 'integer-format-long-wfp))
   (declare (ignorable __function__))
   (b*
     ((bit-size (integer-format->bit-size long-format))
      (signed-long-min (integer-format->signed-min long-format))
      (signed-long-max (integer-format->signed-max long-format))
      (unsigned-long-max (integer-format->unsigned-max long-format))
      (signed-int-min (integer-format->signed-min int-format))
      (signed-int-max (integer-format->signed-max int-format))
      (unsigned-int-max (integer-format->unsigned-max int-format)))
     (and (integerp (/ bit-size
                       (uchar-format->size uchar-format)))
          (<= signed-long-min -2147483647)
          (<= 2147483647 signed-long-max)
          (<= 4294967295 unsigned-long-max)
          (<= signed-long-min signed-int-min)
          (<= signed-int-max signed-long-max)
          (<= unsigned-int-max unsigned-long-max)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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