		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-bit-roles-wfp

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

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

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

Definitions and Theorems

Function: uinteger-bit-roles-wfp

(defun uinteger-bit-roles-wfp (roles)
  (declare (xargs :guard (uinteger-bit-role-listp roles)))
  (let ((__function__ 'uinteger-bit-roles-wfp))
    (declare (ignorable __function__))
    (b* ((exponents (uinteger-bit-roles-exponents roles))
         (n (len exponents))
         ((when (= n 0)) nil)
         (sorted-exponents (insertion-sort exponents))
         ((unless (equal sorted-exponents
                         (acl2::integers-from-to 0 (1- n))))
          nil))
      t)))

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

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

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

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

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

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