		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Uint-array-read

Read an element from an array of type unsigned int, using a C integer index.

Signature
(uint-array-read array index) → element
Arguments: array — Guard (uint-arrayp array).; index — Guard (cintegerp index).
Returns: element — Type (uintp element).

Definitions and Theorems

Function: uint-array-read

(defun uint-array-read (array index)
  (declare (xargs :guard (and (uint-arrayp array)
                              (cintegerp index))))
  (declare (xargs :guard (uint-array-index-okp array index)))
  (let ((__function__ 'uint-array-read))
    (declare (ignorable __function__))
    (uint-fix (nth (integer-from-cinteger index)
                   (uint-array->elements array)))))

Theorem: uintp-of-uint-array-read

(defthm uintp-of-uint-array-read
  (b* ((element (uint-array-read array index)))
    (uintp element))
  :rule-classes :rewrite)

Theorem: uint-array-read-alt-def

(defthm uint-array-read-alt-def
  (implies (and (uint-arrayp array)
                (cintegerp index)
                (uint-array-index-okp array index))
           (equal (uint-array-read array index)
                  (value-array-read (integer-from-cinteger index)
                                    array))))

Theorem: uint-array-read-of-uint-array-fix-array

(defthm uint-array-read-of-uint-array-fix-array
  (equal (uint-array-read (uint-array-fix array)
                          index)
         (uint-array-read array index)))

Theorem: uint-array-read-uint-array-equiv-congruence-on-array

(defthm uint-array-read-uint-array-equiv-congruence-on-array
  (implies (uint-array-equiv array array-equiv)
           (equal (uint-array-read array index)
                  (uint-array-read array-equiv index)))
  :rule-classes :congruence)

Theorem: uint-array-read-of-cinteger-fix-index

(defthm uint-array-read-of-cinteger-fix-index
  (equal (uint-array-read array (cinteger-fix index))
         (uint-array-read array index)))

Theorem: uint-array-read-cinteger-equiv-congruence-on-index

(defthm uint-array-read-cinteger-equiv-congruence-on-index
  (implies (cinteger-equiv index index-equiv)
           (equal (uint-array-read array index)
                  (uint-array-read array index-equiv)))
  :rule-classes :congruence)