		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uchar-format->max

The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].

Signature
(uchar-format->max format) → max
Arguments: format — Guard (uchar-formatp format).
Returns: max — Type (posp max).

This directly derives from CHAR_BIT, as discussed in uchar-format, and in footnote 50 of [C17:6.2.6.1//3], which says that unsigned char values range from 0 to 2^{\mathtt{CHAR\_BIT}}-1.

This is at least 255, as required by [C17:5.2.4.2.1/1].

Definitions and Theorems

Function: uchar-format->max

(defun uchar-format->max (format)
  (declare (xargs :guard (uchar-formatp format)))
  (let ((__function__ 'uchar-format->max))
    (declare (ignorable __function__))
    (1- (expt 2 (uchar-format->size format)))))

Theorem: posp-of-uchar-format->max

(defthm posp-of-uchar-format->max
  (b* ((max (uchar-format->max format)))
    (posp max))
  :rule-classes :rewrite)

Theorem: uchar-format->-max-type-prescription

(defthm uchar-format->-max-type-prescription
  (b* ((common-lisp::?max (uchar-format->max format)))
    (and (posp max) (> max 1)))
  :rule-classes :type-prescription)

Theorem: uchar-format->max-lower-bound

(defthm uchar-format->max-lower-bound
  (b* ((common-lisp::?max (uchar-format->max format)))
    (>= max 255))
  :rule-classes :linear)

Theorem: uchar-format->max-of-uchar-format-fix-format

(defthm uchar-format->max-of-uchar-format-fix-format
  (equal (uchar-format->max (uchar-format-fix format))
         (uchar-format->max format)))

Theorem: uchar-format->max-uchar-format-equiv-congruence-on-format

(defthm uchar-format->max-uchar-format-equiv-congruence-on-format
  (implies (uchar-format-equiv format format-equiv)
           (equal (uchar-format->max format)
                  (uchar-format->max format-equiv)))
  :rule-classes :congruence)