• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
        • Language
        • Representation
          • Representation-of-integer-operations
          • Atc-arrays
            • Atc-def-integer-arrays
            • Ushort-array-write
            • Ushort-array-integer-write
            • Ulong-array-integer-write
            • Ullong-array-write
            • Ullong-array-integer-write
            • Uchar-array-integer-write
            • Sshort-array-write
            • Sshort-array-integer-write
            • Slong-array-integer-write
            • Sllong-array-write
            • Sllong-array-integer-write
            • Schar-array-integer-write
            • Ulong-array-write
            • Uchar-array-write
            • Slong-array-write
            • Schar-array-write
            • Uint-array-write
            • Uint-array-integer-write
            • Sint-array-write
            • Sint-array-integer-write
            • Ushort-array
            • Ullong-array
            • Sshort-array
            • Sllong-array
            • Ulong-array
            • Uint-array
            • Uchar-array
            • Slong-array
            • Sint-array
            • Schar-array
            • Ushort-array-integer-read
            • Ushort-array-integer-index-okp
            • Ullong-array-integer-read
            • Ullong-array-integer-index-okp
            • Sshort-array-integer-read
            • Sshort-array-integer-index-okp
            • Sllong-array-integer-read
            • Sllong-array-integer-index-okp
            • Ulong-array-integer-read
            • Ulong-array-integer-index-okp
            • Ullong-array-read
            • Uint-array-integer-read
            • Uint-array-integer-index-okp
            • Uchar-array-integer-read
            • Uchar-array-integer-index-okp
            • Slong-array-integer-read
            • Slong-array-integer-index-okp
            • Sllong-array-read
            • Sint-array-integer-read
            • Sint-array-integer-index-okp
            • Schar-array-integer-read
            • Schar-array-integer-index-okp
            • Ushort-array-read
            • Ushort-array-index-okp
            • Ulong-array-read
            • Ulong-array-index-okp
            • Ullong-array-index-okp
            • Uint-array-read
            • Uchar-array-read
            • Uchar-array-index-okp
            • Sshort-array-read
            • Sshort-array-index-okp
            • Slong-array-read
            • Slong-array-index-okp
            • Sllong-array-index-okp
            • Sint-array-read
            • Schar-array-read
            • Schar-array-index-okp
            • Uint-array-index-okp
            • Sint-array-index-okp
            • Ushort-array-of
            • Ullong-array-of
            • Uchar-array-length
            • Sshort-array-of
            • Sllong-array-of
            • Ulong-array-of
            • Uint-array-of
            • Uchar-array-of
            • Slong-array-of
            • Sint-array-of
            • Schar-array-of
            • Ushort-array-length
            • Ulong-array-length
            • Ullong-array-length
            • Sshort-array-length
            • Sllong-array-length
            • Uint-array-length
            • Slong-array-length
            • Sint-array-length
            • Schar-array-length
            • Atc-def-integer-arrays-loop
          • Representation-of-integers
          • Representation-of-integer-conversions
          • Pointed-integers
          • Shallow-deep-embedding-relation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atc-arrays

Atc-def-integer-arrays

Event to generate the model of arrays of an integer type.

Signature

(atc-def-integer-arrays type) → event

Arguments

type — Guard (typep type).

Returns

event — Type (pseudo-event-formp event).

We generate the fixtype and the operatiosn that take indices of any C integer types. Note that indices are 0-based. We also generate the function that returns the length of an array, as an ACL2 integer.

We also generate theorems ...-alt-def that provide alternative definitions for the functions related to arrays. We plan to reformulate the definition of these shallowly embedded arrays to be like the aforementioned ...-alt-def theorems, in which case the theorems will be of course eliminated. We use the ...-alt-def theorems in certain proofs.

Definitions and Theorems

Function: atc-def-integer-arrays

(defun atc-def-integer-arrays (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'atc-def-integer-arrays))
  (declare (ignorable __function__))
  (b*
   ((type-string (integer-type-xdoc-string type))
    (<type> (integer-type-to-fixtype type))
    (<type>p (pack <type> 'p))
    (<type>-fix (pack <type> '-fix))
    (<type>-from-integer (pack <type> '-from-integer))
    (<type>-list (pack <type> '-list))
    (<type>-listp (pack <type> '-listp))
    (<type>-array (pack <type> '-array))
    (<type>-arrayp (pack <type>-array 'p))
    (<type>-arrayp-alt-def (pack <type>-arrayp '-alt-def))
    (<type>-array-of (pack <type>-array '-of))
    (<type>-array-of-alt-def (pack <type>-array-of '-alt-def))
    (<type>-array-fix (pack <type>-array '-fix))
    (<type>-array->elemtype (pack <type>-array '->elemtype))
    (<type>-array->elements (pack <type>-array '->elements))
    (<type>-array->elements-alt-def
         (pack <type>-array->elements '-alt-def))
    (<type>-array-length (pack <type>-array '-length))
    (<type>-array-length-alt-def
         (pack <type>-array-length '-alt-def))
    (<type>-array-integer-index-okp
         (pack <type> '-array-integer-index-okp))
    (<type>-array-integer-read (pack <type>-array '-integer-read))
    (<type>-array-integer-read-alt-def
         (pack <type>-array-integer-read '-alt-def))
    (<type>-array-integer-write (pack <type>-array '-integer-write))
    (<type>-array-integer-write-alt-def
         (pack <type>-array-integer-write '-alt-def))
    (<type>-array-index-okp (pack <type> '-array-index-okp))
    (<type>-array-read (pack <type>-array '-read))
    (<type>-array-read-alt-def (pack <type>-array '-read-alt-def))
    (<type>-array-write (pack <type>-array '-write))
    (<type>-array-write-alt-def (pack <type>-array '-write-alt-def))
    (<type>-array-of-of-<type>-array->elements
         (pack <type>-array-of '-of-
               <type>-array->elements))
    (len-of-<type>-array->elements-of-<type>-array-integer-write
         (pack 'len-of-
               <type>-array->elements '-of-
               <type>-array-integer-write))
    (len-of-<type>-array->elements-of-<type>-array-write
         (pack 'len-of-
               <type>-array->elements '-of-
               <type>-array-write))
    (<type>-array-length-of-<type>-array-integer-write
         (pack <type> '-array-length-of-
               <type>-array-integer-write))
    (<type>-array-length-of-<type>-array-write
         (pack <type> '-array-length-of-
               <type>-array-write))
    (type-of-value-when-<type>p (pack 'type-of-value-when- <type>p))
    (<type>-array-write-to-integer-write
         (pack <type>-array-write '-to-integer-write))
    (value-listp-when-<type>-listp
         (pack 'value-listp-when- <type>-listp))
    (valuep-when-<type>p (pack 'valuep-when- <type>p)))
   (cons
    'progn
    (append
     (and (type-case type :char)
          (raise "Type ~x0 not supported." type))
     (cons
      (cons
       'fty::defprod
       (cons
        <type>-array
        (cons
         ':short
         (cons
          (str::cat "Fixtype of (ATC's model of) arrays of "
                    type-string ".")
          (cons
           (cons
            (cons
             'elemtype
             (cons
              'type
              (cons
               ':reqfix
               (cons
                (cons
                    'if
                    (cons (cons 'type-case
                                (cons 'elemtype
                                      (cons (type-kind type) 'nil)))
                          (cons 'elemtype
                                (cons (type-to-maker type) 'nil))))
                'nil))))
            (cons
             (cons
              'elements
              (cons
               <type>-list
               (cons
                ':reqfix
                (cons
                 (cons
                  'if
                  (cons
                   '(consp elements)
                   (cons
                    'elements
                    (cons
                         (cons 'list
                               (cons (cons <type>-from-integer '(0))
                                     'nil))
                         'nil))))
                 'nil))))
             'nil))
           (cons
            ':require
            (cons
             (cons 'and
                   (cons (cons 'type-case
                               (cons 'elemtype
                                     (cons (type-kind type) 'nil)))
                         '((consp elements))))
             (cons
              ':layout
              (cons
               ':list
               (cons
                   ':tag
                   (cons ':array
                         (cons ':pred
                               (cons <type>-arrayp 'nil)))))))))))))
      (cons
       (cons
        'defsection
        (cons
         (pack <type>-array '-ext)
         (cons
          ':extension
          (cons
           <type>-array
           (cons
            (cons
             'defruled
             (cons
              <type>-arrayp-alt-def
              (cons
               (cons
                'equal
                (cons
                 (cons <type>-arrayp '(x))
                 (cons
                  (cons
                   'and
                   (cons
                    '(valuep x)
                    (cons
                     '(value-case x :array)
                     (cons
                      (cons 'equal
                            (cons '(value-array->elemtype x)
                                  (cons (type-to-maker type) 'nil)))
                      (cons (cons <type>-listp
                                  '((value-array->elements x)))
                            'nil)))))
                  'nil)))
               (cons
                ':enable
                (cons
                     (cons <type>-arrayp
                           '(valuep value-kind value-array->elemtype
                                    value-array->elements))
                     'nil)))))
            (cons
             (cons
              'defruled
              (cons
               <type>-array->elements-alt-def
               (cons
                (cons
                 'implies
                 (cons
                  (cons <type>-arrayp '(array))
                  (cons
                   (cons
                        'equal
                        (cons (cons <type>-array->elements '(array))
                              '((value-array->elements array))))
                   'nil)))
                (cons
                 ':enable
                 (cons
                  (cons
                   <type>-array->elements
                   (cons
                    'value-array->elements
                    (cons
                     <type>-arrayp
                     (cons
                      'valuep
                      (cons
                       'value-kind
                       (cons
                            value-listp-when-<type>-listp 'nil))))))
                  'nil)))))
             'nil))))))
       (cons
        (cons
         'define
         (cons
          <type>-array-of
          (cons
           (cons (cons 'elements
                       (cons <type>-listp 'nil))
                 'nil)
           (cons
            ':guard
            (cons
             '(consp elements)
             (cons
              ':returns
              (cons
               (cons 'array (cons <type>-arrayp 'nil))
               (cons
                ':short
                (cons
                 (str::cat "Build an array of " type-string
                           "from a list of its elements.")
                 (cons
                  (cons <type>-array
                        (cons (type-to-maker type) '(elements)))
                  (cons
                   ':hooks
                   (cons
                    '(:fix)
                    (cons
                     '///
                     (cons
                      (cons
                       'defrule
                       (cons
                        <type>-array-of-of-<type>-array->elements
                        (cons
                         (cons
                          'equal
                          (cons
                           (cons
                            <type>-array-of
                            (cons
                              (cons <type>-array->elements '(array))
                              'nil))
                           (cons (cons <type>-array-fix '(array))
                                 'nil)))
                         (cons
                              ':enable
                              (cons <type>-array->elemtype 'nil)))))
                      (cons
                       (cons
                        'defruled
                        (cons
                         <type>-array-of-alt-def
                         (cons
                          (cons
                           'implies
                           (cons
                            (cons 'and
                                  (cons (cons <type>-listp '(elems))
                                        '((consp elems))))
                            (cons
                             (cons
                              'equal
                              (cons
                               (cons <type>-array-of '(elems))
                               (cons
                                (cons
                                   'make-value-array
                                   (cons ':elemtype
                                         (cons (type-to-maker type)
                                               '(:elements elems))))
                                'nil)))
                             'nil)))
                          (cons
                           ':enable
                           (cons
                             (cons <type>-array-of
                                   (cons <type>-array
                                         '(value-array->elemtype
                                               value-array->elements
                                               valuep value-kind)))
                             'nil)))))
                       'nil)))))))))))))))
        (cons
         (cons
          'define
          (cons
           <type>-array-length
           (cons
            (cons (cons 'array (cons <type>-arrayp 'nil))
                  'nil)
            (cons
             ':returns
             (cons
              '(length posp
                       :rule-classes (:rewrite :type-prescription)
                       :hints (("Goal" :in-theory (enable posp))))
              (cons
               ':short
               (cons
                (str::cat "Length of an array of "
                          type-string ".")
                (cons
                 (cons 'len
                       (cons (cons <type>-array->elements '(array))
                             'nil))
                 (cons
                  ':hooks
                  (cons
                   '(:fix)
                   (cons
                    '///
                    (cons
                     '(more-returns (length natp))
                     (cons
                      (cons
                       'defruled
                       (cons
                        <type>-array-length-alt-def
                        (cons
                         (cons
                          'implies
                          (cons
                           (cons <type>-arrayp '(array))
                           (cons
                            (cons
                             'equal
                             (cons
                                 (cons <type>-array-length '(array))
                                 '((value-array->length array))))
                            'nil)))
                         (cons
                          ':enable
                          (cons
                           (cons
                            <type>-array-length
                            (cons
                             'value-array->length
                             (cons
                              <type>-array->elements-alt-def 'nil)))
                           'nil)))))
                      'nil)))))))))))))
         (cons
          (cons
           'define
           (cons
            <type>-array-integer-index-okp
            (cons
             (cons (cons 'array (cons <type>-arrayp 'nil))
                   '((index integerp)))
             (cons
              ':returns
              (cons
               '(yes/no booleanp)
               (cons
                ':short
                (cons
                 (str::cat
                  "Check if an ACL2 integer is
                            a valid index (i.e. in range)
                            for an array of "
                  type-string ".")
                 (cons
                  (cons
                     'integer-range-p
                     (cons '0
                           (cons (cons <type>-array-length '(array))
                                 '((ifix index)))))
                  '(:hooks (:fix))))))))))
          (cons
           (cons
            'define
            (cons
             <type>-array-index-okp
             (cons
              (cons (cons 'array (cons <type>-arrayp 'nil))
                    '((index cintegerp)))
              (cons
               ':returns
               (cons
                '(yes/no booleanp)
                (cons
                 ':short
                 (cons
                  (str::cat
                   "Check if a C integer is
                            a valid index (i.e. in range)
                            for an array of "
                   type-string ".")
                  (cons
                   (cons
                     'integer-range-p
                     (cons '0
                           (cons (cons <type>-array-length '(array))
                                 '((integer-from-cinteger index)))))
                   '(:hooks (:fix))))))))))
           (cons
            (cons
             'define
             (cons
              <type>-array-integer-read
              (cons
               (cons (cons 'array (cons <type>-arrayp 'nil))
                     '((index integerp)))
               (cons
                ':guard
                (cons
                 (cons <type>-array-integer-index-okp
                       '(array index))
                 (cons
                  ':returns
                  (cons
                   (cons 'element (cons <type>p 'nil))
                   (cons
                    ':short
                    (cons
                     (str::cat "Read an element from an array of "
                               type-string
                               ", using an ACL2 integer index.")
                     (cons
                      (cons
                       <type>-fix
                       (cons
                        (cons
                         'nth
                         (cons
                          'index
                          (cons
                              (cons <type>-array->elements '(array))
                              'nil)))
                        'nil))
                      (cons
                       ':guard-hints
                       (cons
                        (cons
                         (cons
                          '"Goal"
                          (cons
                           ':in-theory
                           (cons
                            (cons
                             'enable
                             (cons
                               <type>-array-integer-index-okp
                               (cons <type>-array-length
                                     '(nfix ifix integer-range-p))))
                            'nil)))
                         'nil)
                        (cons
                         '///
                         (cons
                          (cons
                           'fty::deffixequiv
                           (cons
                            <type>-array-integer-read
                            '(:hints
                              (("Goal"
                                   :in-theory (enable ifix nth))))))
                          (cons
                           (cons
                            'defruled
                            (cons
                             <type>-array-integer-read-alt-def
                             (cons
                              (cons
                               'implies
                               (cons
                                (cons
                                 'and
                                 (cons
                                  (cons <type>-arrayp '(array))
                                  (cons
                                   '(integerp index)
                                   (cons
                                    (cons
                                      <type>-array-integer-index-okp
                                      '(array index))
                                    'nil))))
                                (cons
                                 (cons
                                  'equal
                                  (cons
                                     (cons <type>-array-integer-read
                                           '(array index))
                                     '((value-array-read
                                            index array))))
                                 'nil)))
                              (cons
                               ':enable
                               (cons
                                (cons
                                 <type>-array-integer-read
                                 (cons
                                  'value-array-read
                                  (cons
                                   <type>-array->elements-alt-def
                                   (cons
                                    <type>-array-integer-index-okp
                                    (cons
                                     <type>-array-length-alt-def
                                     (cons
                                      'value-array->length
                                      (cons
                                       <type>-arrayp-alt-def
                                       '(nfix
                                             ifix
                                             integer-range-p))))))))
                                'nil)))))
                           'nil)))))))))))))))
            (cons
             (cons
              'define
              (cons
               <type>-array-read
               (cons
                (cons (cons 'array (cons <type>-arrayp 'nil))
                      '((index cintegerp)))
                (cons
                 ':guard
                 (cons
                  (cons <type>-array-index-okp '(array index))
                  (cons
                   ':returns
                   (cons
                    (cons 'element (cons <type>p 'nil))
                    (cons
                     ':short
                     (cons
                      (str::cat "Read an element from an array of "
                                type-string
                                ", using a C integer index.")
                      (cons
                       (cons
                        <type>-fix
                        (cons
                         (cons
                          'nth
                          (cons
                           '(integer-from-cinteger index)
                           (cons
                              (cons <type>-array->elements '(array))
                              'nil)))
                         'nil))
                       (cons
                        ':guard-hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons 'enable
                                   (cons <type>-array-index-okp
                                         (cons <type>-array-length
                                               '(integer-range-p))))
                             'nil)))
                          'nil)
                         (cons
                          ':hooks
                          (cons
                           '(:fix)
                           (cons
                            '///
                            (cons
                             (cons
                              'defruled
                              (cons
                               <type>-array-read-alt-def
                               (cons
                                (cons
                                 'implies
                                 (cons
                                  (cons
                                   'and
                                   (cons
                                    (cons <type>-arrayp '(array))
                                    (cons
                                     '(cintegerp index)
                                     (cons
                                        (cons <type>-array-index-okp
                                              '(array index))
                                        'nil))))
                                  (cons
                                   (cons
                                    'equal
                                    (cons
                                     (cons <type>-array-read
                                           '(array index))
                                     '((value-array-read (integer-from-cinteger
                                                              index)
                                                         array))))
                                   'nil)))
                                (cons
                                 ':enable
                                 (cons
                                  (cons
                                   <type>-array-read
                                   (cons
                                    'value-array-read
                                    (cons
                                     <type>-array->elements-alt-def
                                     (cons
                                      <type>-array-index-okp
                                      (cons
                                       <type>-array-length-alt-def
                                       (cons
                                        'value-array->length
                                        (cons
                                           <type>-arrayp-alt-def
                                           '(integer-range-p))))))))
                                  'nil)))))
                             'nil))))))))))))))))
             (cons
              (cons
               'define
               (cons
                <type>-array-integer-write
                (cons
                 (cons
                     (cons 'array (cons <type>-arrayp 'nil))
                     (cons '(index integerp)
                           (cons (cons 'element (cons <type>p 'nil))
                                 'nil)))
                 (cons
                  ':guard
                  (cons
                   (cons <type>-array-integer-index-okp
                         '(array index))
                   (cons
                    ':returns
                    (cons
                     (cons 'new-array
                           (cons <type>-arrayp 'nil))
                     (cons
                      ':short
                      (cons
                       (str::cat "Write an element to an array of "
                                 type-string
                                 ", using an ACL2 integer index.")
                       (cons
                        (cons
                         'b*
                         (cons
                          (cons
                           (cons
                              'array
                              (cons (cons <type>-array-fix '(array))
                                    'nil))
                           (cons
                            '(index (ifix index))
                            (cons
                             (cons
                                  'element
                                  (cons (cons <type>-fix '(element))
                                        'nil))
                             'nil)))
                          (cons
                           (cons
                            'if
                            (cons
                             (cons
                              'mbt
                              (cons
                                (cons <type>-array-integer-index-okp
                                      '(array index))
                                'nil))
                             (cons
                              (cons
                               <type>-array-of
                               (cons
                                (cons
                                 'update-nth
                                 (cons
                                  'index
                                  (cons
                                   'element
                                   (cons
                                        (cons <type>-array->elements
                                              '(array))
                                        'nil))))
                                'nil))
                              '(array))))
                           'nil)))
                        (cons
                         ':guard-hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'enable
                               (cons
                                    <type>-array-integer-index-okp
                                    (cons <type>-array-length
                                          '(nfix integer-range-p))))
                              'nil)))
                           'nil)
                          (cons
                           ':hooks
                           (cons
                            '(:fix)
                            (cons
                             '///
                             (cons
                              (cons
                               'defrule
                               (cons
                                len-of-<type>-array->elements-of-<type>-array-integer-write
                                (cons
                                 (cons
                                  'equal
                                  (cons
                                   (cons
                                    'len
                                    (cons
                                     (cons
                                      <type>-array->elements
                                      (cons
                                       (cons
                                          <type>-array-integer-write
                                          '(array index element))
                                       'nil))
                                     'nil))
                                   (cons
                                    (cons
                                     'len
                                     (cons
                                        (cons <type>-array->elements
                                              '(array))
                                        'nil))
                                    'nil)))
                                 (cons
                                  ':enable
                                  (cons
                                   (cons
                                    <type>-array-integer-index-okp
                                    (cons
                                     <type>-array-length
                                     (cons
                                      <type>-array-of
                                      '(nfix
                                        ifix integer-range-p max))))
                                   'nil)))))
                              (cons
                               (cons
                                'defrule
                                (cons
                                 <type>-array-length-of-<type>-array-integer-write
                                 (cons
                                  (cons
                                   'equal
                                   (cons
                                    (cons
                                     <type>-array-length
                                     (cons
                                      (cons
                                          <type>-array-integer-write
                                          '(array index element))
                                      'nil))
                                    (cons
                                     (cons
                                       <type>-array-length '(array))
                                     'nil)))
                                  (cons
                                   ':enable
                                   (cons
                                    (cons
                                     <type>-array-integer-index-okp
                                     (cons
                                      <type>-array-length
                                      (cons
                                       <type>-array-of
                                       '(nfix
                                             ifix
                                             integer-range-p max))))
                                    'nil)))))
                               (cons
                                (cons
                                 'defruled
                                 (cons
                                  <type>-array-integer-write-alt-def
                                  (cons
                                   (cons
                                    'implies
                                    (cons
                                     (cons
                                      'and
                                      (cons
                                       (cons <type>-arrayp '(array))
                                       (cons
                                        '(integerp index)
                                        (cons
                                         (cons <type>p '(elem))
                                         (cons
                                          (cons
                                           <type>-array-integer-index-okp
                                           '(array index))
                                          'nil)))))
                                     (cons
                                      (cons
                                       'equal
                                       (cons
                                        (cons
                                          <type>-array-integer-write
                                          '(array index elem))
                                        '((value-array-write
                                               index elem array))))
                                      'nil)))
                                   (cons
                                    ':enable
                                    (cons
                                     (cons
                                      <type>-array-integer-write
                                      (cons
                                       'value-array-write
                                       (cons
                                        <type>-arrayp-alt-def
                                        (cons
                                         <type>-array-of-alt-def
                                         (cons
                                          <type>-array-length-alt-def
                                          (cons
                                           <type>-array->elements-alt-def
                                           (cons
                                            <type>-array-integer-index-okp
                                            (cons
                                             'value-array->length
                                             (cons
                                              type-of-value-when-<type>p
                                              (cons
                                               'remove-flexible-array-member
                                               (cons
                                                'flexible-array-member-p
                                                (cons
                                                 'nfix
                                                 (cons
                                                  'ifix
                                                  (cons
                                                   'integer-range-p
                                                   (cons
                                                    valuep-when-<type>p
                                                    'nil)))))))))))))))
                                     'nil)))))
                                'nil))))))))))))))))))
              (cons
               (cons
                'define
                (cons
                 <type>-array-write
                 (cons
                  (cons
                     (cons 'array (cons <type>-arrayp 'nil))
                     (cons '(index cintegerp)
                           (cons (cons 'element (cons <type>p 'nil))
                                 'nil)))
                  (cons
                   ':guard
                   (cons
                    (cons <type>-array-index-okp '(array index))
                    (cons
                     ':returns
                     (cons
                      (cons 'new-array
                            (cons <type>-arrayp 'nil))
                      (cons
                       ':short
                       (cons
                        (str::cat "Write an element to an array of "
                                  type-string
                                  ", using a c integer index.")
                        (cons
                         (cons
                          'if
                          (cons
                           (cons
                            'mbt
                            (cons
                             (cons
                              <type>-array-index-okp '(array index))
                             'nil))
                           (cons
                            (cons
                             <type>-array-of
                             (cons
                              (cons
                               'update-nth
                               (cons
                                '(integer-from-cinteger index)
                                (cons
                                 (cons <type>-fix '(element))
                                 (cons
                                  (cons
                                    <type>-array->elements '(array))
                                  'nil))))
                              'nil))
                            (cons (cons <type>-array-fix '(array))
                                  'nil))))
                         (cons
                          ':guard-hints
                          (cons
                           (cons
                            (cons
                             '"Goal"
                             (cons
                              ':in-theory
                              (cons
                               (cons
                                   'enable
                                   (cons <type>-array-index-okp
                                         (cons <type>-array-length
                                               '(integer-range-p))))
                               'nil)))
                            'nil)
                           (cons
                            ':hooks
                            (cons
                             '(:fix)
                             (cons
                              '///
                              (cons
                               (cons
                                'defrule
                                (cons
                                 len-of-<type>-array->elements-of-<type>-array-write
                                 (cons
                                  (cons
                                   'equal
                                   (cons
                                    (cons
                                     'len
                                     (cons
                                      (cons
                                       <type>-array->elements
                                       (cons
                                        (cons
                                             <type>-array-write
                                             '(array index element))
                                        'nil))
                                      'nil))
                                    (cons
                                     (cons
                                      'len
                                      (cons
                                        (cons <type>-array->elements
                                              '(array))
                                        'nil))
                                     'nil)))
                                  (cons
                                   ':enable
                                   (cons
                                    (cons
                                     <type>-array-index-okp
                                     (cons
                                      <type>-array-length
                                      (cons
                                           <type>-array-of
                                           '(integer-range-p max))))
                                    'nil)))))
                               (cons
                                (cons
                                 'defrule
                                 (cons
                                  <type>-array-length-of-<type>-array-write
                                  (cons
                                   (cons
                                    'equal
                                    (cons
                                     (cons
                                      <type>-array-length
                                      (cons
                                       (cons <type>-array-write
                                             '(array index element))
                                       'nil))
                                     (cons
                                      (cons
                                       <type>-array-length '(array))
                                      'nil)))
                                   (cons
                                    ':enable
                                    (cons
                                     (cons
                                      <type>-array-index-okp
                                      (cons
                                       <type>-array-length
                                       (cons
                                           <type>-array-of
                                           '(integer-range-p max))))
                                     'nil)))))
                                (cons
                                 (cons
                                  'defruled
                                  (cons
                                   <type>-array-write-to-integer-write
                                   (cons
                                    (cons
                                     'equal
                                     (cons
                                      (cons <type>-array-write
                                            '(array index val))
                                      (cons
                                       (cons
                                          <type>-array-integer-write
                                          '(array (integer-from-cinteger
                                                       index)
                                                  val))
                                       'nil)))
                                    (cons
                                     ':enable
                                     (cons
                                      (cons
                                       <type>-array-integer-write
                                       (cons
                                        <type>-array-index-okp
                                        (cons
                                         <type>-array-integer-index-okp
                                         '(ifix))))
                                      'nil)))))
                                 (cons
                                  (cons
                                   'defruled
                                   (cons
                                    <type>-array-write-alt-def
                                    (cons
                                     (cons
                                      'implies
                                      (cons
                                       (cons
                                        'and
                                        (cons
                                         (cons
                                             <type>-arrayp '(array))
                                         (cons
                                          '(cintegerp index)
                                          (cons
                                           (cons <type>p '(elem))
                                           (cons
                                            (cons
                                              <type>-array-index-okp
                                              '(array index))
                                            'nil)))))
                                       (cons
                                        (cons
                                         'equal
                                         (cons
                                          (cons <type>-array-write
                                                '(array index elem))
                                          '((value-array-write
                                                 (integer-from-cinteger
                                                      index)
                                                 elem array))))
                                        'nil)))
                                     (cons
                                      ':enable
                                      (cons
                                       (cons
                                        <type>-array-write
                                        (cons
                                         'value-array-write
                                         (cons
                                          <type>-arrayp-alt-def
                                          (cons
                                           <type>-array-of-alt-def
                                           (cons
                                            <type>-array-length-alt-def
                                            (cons
                                             <type>-array->elements-alt-def
                                             (cons
                                              <type>-array-index-okp
                                              (cons
                                               'value-array->length
                                               (cons
                                                type-of-value-when-<type>p
                                                (cons
                                                 'remove-flexible-array-member
                                                 (cons
                                                  'flexible-array-member-p
                                                  (cons
                                                   'integer-range-p
                                                   (cons
                                                    value-listp-when-<type>-listp
                                                    (cons
                                                     valuep-when-<type>p
                                                     'nil))))))))))))))
                                       'nil)))))
                                  'nil)))))))))))))))))))
               'nil)))))))))))))))

Theorem: pseudo-event-formp-of-atc-def-integer-arrays

(defthm pseudo-event-formp-of-atc-def-integer-arrays
  (b* ((event (atc-def-integer-arrays type)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)