		Search-engine friendly clone of the ACL2 documentation.

Integer-formats

Integer-format-llong-wfp

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

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

Definitions and Theorems

Function: integer-format-llong-wfp

(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))))
  (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: booleanp-of-integer-format-llong-wfp

(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: integer-format-llong-wf-bit-size-lower-bound

(defthm integer-format-llong-wf-bit-size-lower-bound
 (implies
     (integer-format-llong-wfp llong-format uchar-format long-fomat)
     (>= (integer-format->bit-size llong-format)
         64))
 :rule-classes :linear)

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

(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: integer-format-llong-wfp-integer-format-equiv-congruence-on-llong-format

(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: integer-format-llong-wfp-of-uchar-format-fix-uchar-format

(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: integer-format-llong-wfp-uchar-format-equiv-congruence-on-uchar-format

(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: integer-format-llong-wfp-of-integer-format-fix-long-format

(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: integer-format-llong-wfp-integer-format-equiv-congruence-on-long-format

(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)