• 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
      • Cons-listp
      • Cons-list-listp
      • Signed-byte-listp
        • Signed-byte-list-fix
      • 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
• Signed-byte-listp
• Signed-byte-fix

Signed-byte-list-fix

Fixing function for signed-byte-listp.

Signature

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

Arguments

bits — Guard (posp bits).

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

Returns

fixed-x — Type (signed-byte-listp bits fixed-x), given (posp bits).

This lifts signed-byte-fix to lists. See that function for more information, in particular about the fixing of bits to a positive integer.

Definitions and Theorems

Function: signed-byte-list-fix

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

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

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

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

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

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

(defthm signed-byte-list-fix-when-signed-byte-listp
  (implies (signed-byte-listp (pos-fix bits) x)
           (equal (signed-byte-list-fix bits x)
                  x)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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