		Search-engine friendly clone of the ACL2 documentation.

Integer-format-templates

Sinteger-bit-roles-wfp

Check if a list of roles of signed integer bits is well-formed.

Signature
(sinteger-bit-roles-wfp roles) → yes/no
Arguments: roles — Guard (sinteger-bit-role-listp roles).
Returns: yes/no — Type (booleanp yes/no).

According to [C17:6.2.6.2/2], there must be exactly one value bit for each exponent in a range from 0 to M-1 for some M. We express that by saying that, after collecting the exponents and sorting them, we must have the list (0 1 ... M-1), where M is the number of collected exponents. Note that this prohibits duplicates. We also require M to be non-zero, although this is not explicated in [C17].

[C17:6.2.6.2/2] also says that there must be exactly one sign bit, i.e. the number of sign bits must be 1.

Definitions and Theorems

Function: sinteger-bit-roles-wfp

(defun sinteger-bit-roles-wfp (roles)
  (declare (xargs :guard (sinteger-bit-role-listp roles)))
  (b* ((exponents (sinteger-bit-roles-exponents roles))
       (m (len exponents))
       ((when (= m 0)) nil)
       (sorted-exponents (insertion-sort exponents))
       ((unless (equal sorted-exponents
                       (integers-from-to 0 (1- m))))
        nil)
       ((unless (= (sinteger-bit-roles-sign-count roles)
                   1))
        nil))
    t))

Theorem: booleanp-of-sinteger-bit-roles-wfp

(defthm booleanp-of-sinteger-bit-roles-wfp
  (b* ((yes/no (sinteger-bit-roles-wfp roles)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: posp-of-sinteger-bit-roles-value-count-when-wfp

(defthm posp-of-sinteger-bit-roles-value-count-when-wfp
  (implies (sinteger-bit-roles-wfp roles)
           (posp (sinteger-bit-roles-value-count roles)))
  :rule-classes (:rewrite :type-prescription))

Theorem: len-gt-1-when-sinteger-bit-roles-wfp

(defthm len-gt-1-when-sinteger-bit-roles-wfp
  (implies (sinteger-bit-roles-wfp roles)
           (> (len roles) 1)))

Theorem: sinteger-bit-roles-wfp-of-sinteger-bit-role-list-fix-roles

(defthm sinteger-bit-roles-wfp-of-sinteger-bit-role-list-fix-roles
  (equal (sinteger-bit-roles-wfp (sinteger-bit-role-list-fix roles))
         (sinteger-bit-roles-wfp roles)))

Theorem: sinteger-bit-roles-wfp-sinteger-bit-role-list-equiv-congruence-on-roles

(defthm
 sinteger-bit-roles-wfp-sinteger-bit-role-list-equiv-congruence-on-roles
 (implies (sinteger-bit-role-list-equiv roles roles-equiv)
          (equal (sinteger-bit-roles-wfp roles)
                 (sinteger-bit-roles-wfp roles-equiv)))
 :rule-classes :congruence)