		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Llong-format-64tcnt

The (unsigned and signed) long long format defined by 64 bits with increasing values, two's complement, and no trap representations.

Signature
(llong-format-64tcnt) → format
Returns: format — Type (integer-formatp format).

This is the simplest and smallest format for long long integers, with two's complement being the most common signed format. There cannot be any padding bits, otherwise the value bits would not suffice to cover the required ranges of values. With no padding bits, there is only one possible trap representation, namely the one with sign bit 1 and all value bits 0, but the simplest and most common choice is that it is a valid value instead (the smallest signed value representable in the type).

Definitions and Theorems

Function: llong-format-64tcnt

(defun llong-format-64tcnt nil
  (declare (xargs :guard t))
  (let ((__function__ 'llong-format-64tcnt))
    (declare (ignorable __function__))
    (integer-format-inc-sign-tcnpnt 64)))

Theorem: integer-formatp-of-llong-format-64tcnt

(defthm integer-formatp-of-llong-format-64tcnt
  (b* ((format (llong-format-64tcnt)))
    (integer-formatp format))
  :rule-classes :rewrite)

Theorem: integer-format-llong-wfp-of-long-format-64tcnt

(defthm integer-format-llong-wfp-of-long-format-64tcnt
  (integer-format-llong-wfp (llong-format-64tcnt)
                            (uchar-format-8)
                            (long-format-32tcnt)))

Theorem: integer-format->size-of-llong-format-64tcnt

(defthm integer-format->size-of-llong-format-64tcnt
  (equal (integer-format->size (llong-format-64tcnt))
         64))

Theorem: uinteger-format->max-of-llong-format-64tcnt

(defthm uinteger-format->max-of-llong-format-64tcnt
  (equal (uinteger-format->max
              (uinteger+sinteger-format->unsigned
                   (integer-format->pair (llong-format-64tcnt))))
         18446744073709551615))

Theorem: sinteger-format->max-of-llong-format-64tcnt

(defthm sinteger-format->max-of-llong-format-64tcnt
  (equal (sinteger-format->max
              (uinteger+sinteger-format->signed
                   (integer-format->pair (llong-format-64tcnt))))
         9223372036854775807))

Theorem: sinteger-format->min-of-llong-format-64tcnt

(defthm sinteger-format->min-of-llong-format-64tcnt
  (equal (sinteger-format->min
              (uinteger+sinteger-format->signed
                   (integer-format->pair (llong-format-64tcnt))))
         -9223372036854775808))