• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
      • Std/typed-lists/character-listp
      • Std/typed-lists/symbol-listp
      • Std/typed-lists/boolean-listp
      • Std/typed-lists/string-listp
      • Std/typed-lists/eqlable-listp
      • Theorems-about-true-list-lists
      • Std/typed-lists/atom-listp
      • Unsigned-byte-listp
        • Defbytelist
        • Unsigned-byte-list-fix
      • Cons-listp
      • Cons-list-listp
      • Signed-byte-listp
      • String-or-symbol-listp
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Kestrel-utilities
• Unsigned-byte-listp
• Unsigned-byte-fix

Unsigned-byte-list-fix

Fixing function for unsigned-byte-listp.

Signature

(unsigned-byte-list-fix bits x) → fixed-x

Arguments

bits — Guard (natp bits).

x — Guard (unsigned-byte-listp bits x).

Returns

fixed-x — Type (unsigned-byte-listp bits fixed-x), given (natp bits).

This lifts unsigned-byte-fix to lists. See that function for more information, in particular about the fixing of bits to a natural number.

Definitions and Theorems

Function: unsigned-byte-list-fix

(defun unsigned-byte-list-fix (bits x)
 (declare (xargs :guard (and (natp bits)
                             (unsigned-byte-listp bits x))))
 (let ((__function__ 'unsigned-byte-list-fix))
  (declare (ignorable __function__))
  (mbe
      :logic (cond ((atom x) nil)
                   (t (cons (unsigned-byte-fix bits (car x))
                            (unsigned-byte-list-fix bits (cdr x)))))
      :exec x)))

Theorem: return-type-of-unsigned-byte-list-fix

(defthm return-type-of-unsigned-byte-list-fix
  (implies (natp bits)
           (b* ((fixed-x (unsigned-byte-list-fix bits x)))
             (unsigned-byte-listp bits fixed-x)))
  :rule-classes :rewrite)

Theorem: integer-listp-of-unsigned-byte-list-fix

(defthm integer-listp-of-unsigned-byte-list-fix
  (b* ((fixed-x (unsigned-byte-list-fix bits x)))
    (integer-listp fixed-x))
  :rule-classes :rewrite)

Theorem: unsigned-byte-list-fix-when-unsigned-byte-listp

(defthm unsigned-byte-list-fix-when-unsigned-byte-listp
  (implies (unsigned-byte-listp (nfix bits) x)
           (equal (unsigned-byte-list-fix bits x)
                  x)))

Theorem: unsigned-byte-list-fix-of-nil

(defthm unsigned-byte-list-fix-of-nil
  (equal (unsigned-byte-list-fix bits nil)
         nil))

Theorem: unsigned-byte-list-fix-of-cons

(defthm unsigned-byte-list-fix-of-cons
  (equal (unsigned-byte-list-fix bits (cons x y))
         (cons (unsigned-byte-fix bits x)
               (unsigned-byte-list-fix bits y))))

Theorem: unsigned-byte-list-fix-of-append

(defthm unsigned-byte-list-fix-of-append
  (equal (unsigned-byte-list-fix bits (append x y))
         (append (unsigned-byte-list-fix bits x)
                 (unsigned-byte-list-fix bits y))))

Theorem: len-of-unsigned-byte-list-fix

(defthm len-of-unsigned-byte-list-fix
  (equal (len (unsigned-byte-list-fix bits x))
         (len x)))

Theorem: consp-of-unsigned-byte-list-fix

(defthm consp-of-unsigned-byte-list-fix
  (equal (consp (unsigned-byte-list-fix bits x))
         (consp x)))

Theorem: car-of-unsigned-byte-list-fix

(defthm car-of-unsigned-byte-list-fix
  (implies (consp x)
           (equal (car (unsigned-byte-list-fix bits x))
                  (unsigned-byte-fix bits (car x)))))

Theorem: cdr-of-unsigned-byte-list-fix

(defthm cdr-of-unsigned-byte-list-fix
  (implies (consp x)
           (equal (cdr (unsigned-byte-list-fix bits x))
                  (unsigned-byte-list-fix bits (cdr x)))))

Theorem: rev-of-unsigned-byte-list-fix

(defthm rev-of-unsigned-byte-list-fix
  (equal (rev (unsigned-byte-list-fix bits x))
         (unsigned-byte-list-fix bits (rev x))))