		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-sinteger-bit-roles-wfp

Check if a list of roles of unsigned integer bits and a list of roles of signed integer bits are mutually consistent.

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

[C17:6.2.6.2/2] says each signed integer value bit must be the same as the corresponding unsigned integer value bit; but the unsigned integer type may have more value bits. We check this by going through the two lists of bits, and making sure that, every time we encounter a signed value bit, the corresponding unsigned value bit is for the same exponent.

[C17:6.2.5/6] says that corresponding signed and unsigned integer types take the same amount of storage. In our model, it means that they must have the same number of bits. We check this requirement in this recursive predicate, by ensuring that the two lists end at the same time.

We show that this predicate guarantees the inequality M <= N mentioned in [C17:6.2.6.2/2].

Definitions and Theorems

Function: uinteger-sinteger-bit-roles-wfp

(defun uinteger-sinteger-bit-roles-wfp (uroles sroles)
 (declare (xargs :guard (and (uinteger-bit-role-listp uroles)
                             (sinteger-bit-role-listp sroles))))
 (let ((__function__ 'uinteger-sinteger-bit-roles-wfp))
   (declare (ignorable __function__))
   (b* (((when (endp uroles)) (endp sroles))
        ((when (endp sroles)) nil)
        (srole (car sroles))
        ((unless (sinteger-bit-role-case srole :value))
         (uinteger-sinteger-bit-roles-wfp (cdr uroles)
                                          (cdr sroles)))
        (urole (car uroles))
        ((unless (and (uinteger-bit-role-case urole :value)
                      (equal (uinteger-bit-role-value->exp urole)
                             (sinteger-bit-role-value->exp srole))))
         nil))
     (uinteger-sinteger-bit-roles-wfp (cdr uroles)
                                      (cdr sroles)))))

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

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

Theorem: same-len-when-uinteger-sinteger-bit-roles-wfp

(defthm same-len-when-uinteger-sinteger-bit-roles-wfp
  (implies (uinteger-sinteger-bit-roles-wfp uroles sroles)
           (equal (len uroles) (len sroles)))
  :rule-classes (:rewrite :forward-chaining))

Theorem: sinteger-value-bits-leq-uinteger-value-bits

(defthm sinteger-value-bits-leq-uinteger-value-bits
  (implies (uinteger-sinteger-bit-roles-wfp uroles sroles)
           (<= (sinteger-bit-roles-value-count sroles)
               (uinteger-bit-roles-value-count uroles))))

Theorem: uinteger-sinteger-bit-roles-wfp-of-append

(defthm uinteger-sinteger-bit-roles-wfp-of-append
 (implies
   (equal (len uroles1) (len sroles1))
   (equal (uinteger-sinteger-bit-roles-wfp (append uroles1 uroles2)
                                           (append sroles1 sroles2))
          (and (uinteger-sinteger-bit-roles-wfp uroles1 sroles1)
               (uinteger-sinteger-bit-roles-wfp uroles2 sroles2)))))

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

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

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

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

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

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

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

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