Check if an integer format is well-formed
when used for (signed and unsigned)
(integer-format-llong-wfp llong-format uchar-format long-format) → yes/no
The number of bits must be a multiple of
The possible signed values must cover at least the range from -9223372036854775807 to +9223372036854775807 (both inclusive) [C17:5.2.4.2.1/1]. The possible unsigned values must cover at least the range from 0 to 18446744073709551615 (both inclusive) [C17:5.2.4.2.1/1].
The possible signed values must at least include
those of
Function:
(defun integer-format-llong-wfp (llong-format uchar-format long-format) (declare (xargs :guard (and (integer-formatp llong-format) (uchar-formatp uchar-format) (integer-formatp long-format)))) (let ((__function__ 'integer-format-llong-wfp)) (declare (ignorable __function__)) (b* ((bit-size (integer-format->bit-size llong-format)) (signed-llong-min (integer-format->signed-min llong-format)) (signed-llong-max (integer-format->signed-max llong-format)) (unsigned-llong-max (integer-format->unsigned-max llong-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))) (and (integerp (/ bit-size (uchar-format->size uchar-format))) (<= signed-llong-min -9223372036854775807) (<= 9223372036854775807 signed-llong-max) (<= 18446744073709551615 unsigned-llong-max) (<= signed-llong-min signed-long-min) (<= signed-long-max signed-llong-max) (<= unsigned-long-max unsigned-llong-max)))))
Theorem:
(defthm booleanp-of-integer-format-llong-wfp (b* ((yes/no (integer-format-llong-wfp llong-format uchar-format long-format))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm integer-format-llong-wfp-of-integer-format-fix-llong-format (equal (integer-format-llong-wfp (integer-format-fix llong-format) uchar-format long-format) (integer-format-llong-wfp llong-format uchar-format long-format)))
Theorem:
(defthm integer-format-llong-wfp-integer-format-equiv-congruence-on-llong-format (implies (integer-format-equiv llong-format llong-format-equiv) (equal (integer-format-llong-wfp llong-format uchar-format long-format) (integer-format-llong-wfp llong-format-equiv uchar-format long-format))) :rule-classes :congruence)
Theorem:
(defthm integer-format-llong-wfp-of-uchar-format-fix-uchar-format (equal (integer-format-llong-wfp llong-format (uchar-format-fix uchar-format) long-format) (integer-format-llong-wfp llong-format uchar-format long-format)))
Theorem:
(defthm integer-format-llong-wfp-uchar-format-equiv-congruence-on-uchar-format (implies (uchar-format-equiv uchar-format uchar-format-equiv) (equal (integer-format-llong-wfp llong-format uchar-format long-format) (integer-format-llong-wfp llong-format uchar-format-equiv long-format))) :rule-classes :congruence)
Theorem:
(defthm integer-format-llong-wfp-of-integer-format-fix-long-format (equal (integer-format-llong-wfp llong-format uchar-format (integer-format-fix long-format)) (integer-format-llong-wfp llong-format uchar-format long-format)))
Theorem:
(defthm integer-format-llong-wfp-integer-format-equiv-congruence-on-long-format (implies (integer-format-equiv long-format long-format-equiv) (equal (integer-format-llong-wfp llong-format uchar-format long-format) (integer-format-llong-wfp llong-format uchar-format long-format-equiv))) :rule-classes :congruence)