• 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
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
        • Atj
          • Atj-implementation
            • Atj-types
            • Atj-java-primitive-array-model
              • Atj-def-java-primitive-array-model
              • Short-array
              • Long-array
              • Int-array
              • Char-array
              • Byte-array
              • Boolean-array
              • Float-array
              • Double-array
              • Byte-array-to-sbyte8-list
              • Short-array-to-sbyte16-list
              • Long-array-to-sbyte64-list
              • Int-array-to-sbyte32-list
              • Char-array-to-ubyte16-list
              • Boolean-array-to-boolean-list
              • Double-array-write
              • Boolean-array-write
              • Short-array-write
              • Short-array-from-sbyte16-list
              • Long-array-write
              • Int-array-write
              • Float-array-write
              • Char-array-write
              • Char-array-from-ubyte16-list
              • Byte-array-write
              • Byte-array-from-sbyte8-list
              • Boolean-array-from-boolean-list
              • Long-array-from-sbyte64-list
              • Int-array-from-sbyte32-list
              • Short-array-new-init
              • Double-array-index-in-range-p
              • Byte-array-new-init
              • Boolean-array-new-init
              • Boolean-array-index-in-range-p
              • Short-array-new-len
              • Short-array-index-in-range-p
              • Long-array-new-len
              • Long-array-new-init
              • Long-array-index-in-range-p
              • Int-array-new-init
              • Int-array-index-in-range-p
              • Float-array-new-len
              • Float-array-index-in-range-p
              • Double-array-new-len
              • Char-array-new-len
              • Char-array-new-init
              • Char-array-index-in-range-p
              • Byte-array-new-len
              • Byte-array-index-in-range-p
              • Boolean-array-new-len
              • Short-array-read
              • Long-array-read
              • Int-array-new-len
              • Float-array-read
              • Float-array-new-init
              • Double-array-read
              • Double-array-new-init
              • Char-array-read
              • Byte-array-read
              • Boolean-array-read
              • Int-array-read
              • Short-array-length
              • Float-array-length
              • Double-array-length
              • Boolean-array-length
              • Long-array-length
              • Int-array-length
              • Char-array-length
              • Byte-array-length
            • Atj-java-abstract-syntax
            • Atj-input-processing
            • Atj-java-pretty-printer
            • Atj-code-generation
            • Atj-java-primitives
            • Atj-java-primitive-arrays
            • Atj-type-macros
            • Atj-java-syntax-operations
            • Atj-fn
            • Atj-library-extensions
            • Atj-java-input-types
            • Atj-test-structures
            • Aij-notions
            • Atj-macro-definition
          • Atj-tutorial
        • Aij
        • Language
      • 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

• Atj-java-primitive-array-model

Atj-def-java-primitive-array-model

Macro to define the models of Java primitive arrays.

The models vary slightly across the eight Java primitive array types, but they have a lot of common structure, which is captured via this macro. We define this macro and then we call it eight times.

This macro introduces, for each Java primitive (array) type:

• A fixtype for the arrays of that type. This is a product type with one field, namely the list of primitive values that are the array's components. The fixtype includes the length requirement.
• A predicate to check whether a Java int is a valid index in an array.
• The operations described in atj-java-primitive-array-model.

Macro: atj-def-java-primitive-array-model

(defmacro atj-def-java-primitive-array-model (type)
 (declare
  (xargs
    :guard (member-eq type
                      '(boolean char
                                byte short int long float double))))
 (b* ((type-name (symbol-name type))
      (type-doc (str::cat "@('" (str::downcase-string type-name)
                          "')"))
      (jwit (pkg-witness "JAVA"))
      (type-value (packn-pos (list type '-value) jwit))
      (type-valuep (packn-pos (list type '-valuep) jwit))
      (type-value-fix (packn-pos (list type '-value-fix)
                                 jwit))
      (type-value->get (case type
                         (boolean 'boolean-value->bool)
                         (char 'char-value->nat)
                         (byte 'byte-value->int)
                         (short 'short-value->int)
                         (int 'int-value->int)
                         (long 'long-value->int)
                         (t nil)))
      (type-value-list (packn-pos (list type '-value-list)
                                  jwit))
      (type-value-listp (packn-pos (list type '-value-listp)
                                   jwit))
      (type-array (packn-pos (list type '-array) jwit))
      (type-arrayp (packn-pos (list type-array 'p) jwit))
      (type-array-fix (packn-pos (list type-array '-fix)
                                 jwit))
      (type-array->components
           (packn-pos (list type-array '->components)
                      jwit))
      (type-array-index-in-range-p
           (packn-pos (list type '-array-index-in-range-p)
                      jwit))
      (type-array-read (packn-pos (list type '-array-read)
                                  jwit))
      (type-array-length (packn-pos (list type '-array-length)
                                    jwit))
      (type-array-write (packn-pos (list type '-array-write)
                                   jwit))
      (type-array-new-len (packn-pos (list type '-array-new-len)
                                     jwit))
      (type-array-new-init (packn-pos (list type '-array-new-init)
                                      jwit))
      (acl2type (case type
                  (boolean 'boolean)
                  (char 'ubyte16)
                  (byte 'sbyte8)
                  (short 'sbyte16)
                  (int 'sbyte32)
                  (long 'sbyte64)
                  (t nil)))
      (acl2type-listp (case type
                        (boolean 'boolean-listp)
                        (char 'ubyte16-listp)
                        (byte 'sbyte8-listp)
                        (short 'sbyte16-listp)
                        (int 'sbyte32-listp)
                        (long 'sbyte64-listp)
                        (t nil)))
      (acl2type-doc (case type
                      (boolean "booleans")
                      (char "unsigned 16-bit integers")
                      (byte "signed 8-bit integers")
                      (short "signed 16-bit integers")
                      (int "signed 32-bit integers")
                      (long "signed 64-bit integers")
                      (t "")))
      (type-array-to-list
           (packn-pos (list type-array '-to- acl2type '-list)
                      jwit))
      (type-array-to-list-aux
           (packn-pos (list type-array-to-list '-aux)
                      jwit))
      (type-array-from-list (packn-pos (list type-array '-from-
                                             acl2type '-list)
                                       jwit))
      (type-array-from-list-aux
           (packn-pos (list type-array-from-list '-aux)
                      jwit)))
  (cons
   'progn
   (cons
    (cons
     'fty::defprod
     (cons
      type-array
      (cons
       ':short
       (cons
        (str::cat "Fixtype of (our model of) Java "
                  type-doc " arrays.")
        (cons
         (cons
          (cons 'components
                (cons type-value-list
                      '(:reqfix (if (< (len components) (expt 2 31))
                                    components
                                  nil))))
          'nil)
         (cons
          ':require
          (cons
           '(< (len components) (expt 2 31))
           (cons
            ':layout
            (cons
             ':list
             (cons
              ':tag
              (cons
               (intern (symbol-name type-array)
                       "KEYWORD")
               (cons
                ':pred
                (cons
                 type-arrayp
                 (cons
                  '///
                  (cons
                   (cons
                    'defrule
                    (cons
                     (packn-pos
                         (list 'len-of-
                               type-array->components '-upper-bound)
                         jwit)
                     (cons
                      (cons
                       '<
                       (cons
                        (cons
                         'len
                         (cons
                              (cons type-array->components '(array))
                              'nil))
                        '((expt 2 31))))
                      (cons
                       ':rule-classes
                       (cons
                        ':linear
                        (cons
                            ':enable
                            (cons type-array->components 'nil)))))))
                   'nil)))))))))))))))
    (cons
     (cons
      'define
      (cons
       type-array-index-in-range-p
       (cons
        (cons (cons 'array (cons type-arrayp 'nil))
              '((index int-valuep)))
        (cons
         ':returns
         (cons
          '(yes/no booleanp)
          (cons
           ':short
           (cons
            (str::cat
             "Check if a Java @('int') is a valid index
                              (i.e. in range) for a "
             type-doc " array.")
            (cons
             (cons
              'integer-range-p
              (cons
               '0
               (cons
                  (cons 'len
                        (cons (cons type-array->components '(array))
                              'nil))
                  '((int-value->int index)))))
             'nil))))))))
     (cons
      (cons
       'define
       (cons
        type-array-read
        (cons
         (cons (cons 'array (cons type-arrayp 'nil))
               '((index int-valuep)))
         (cons
          ':guard
          (cons
           (cons type-array-index-in-range-p
                 '(array index))
           (cons
            ':returns
            (cons
             (cons 'component
                   (cons type-valuep 'nil))
             (cons
              ':short
              (cons
               (str::cat "Read a component from a Java "
                         type-doc " array.")
               (cons
                (cons
                 type-value-fix
                 (cons
                  (cons
                   'nth
                   (cons
                        '(int-value->int index)
                        (cons (cons type-array->components '(array))
                              'nil)))
                  'nil))
                (cons
                 ':guard-hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons 'enable
                            (cons type-array-index-in-range-p 'nil))
                      'nil)))
                   'nil)
                  (cons
                   ':prepwork
                   (cons
                    (cons
                     '(local (include-book "std/lists/nth"
                                           :dir :system))
                     (cons
                      (cons
                       'local
                       (cons
                        (cons
                         'fty::deflist
                         (cons
                          type-value-list
                          (cons
                           ':elt-type
                           (cons
                            type-value
                            (cons
                             ':true-listp
                             (cons
                              't
                              (cons
                               ':elementp-of-nil
                               (cons
                                'nil
                                (cons
                                 ':pred
                                 (cons
                                     type-value-listp 'nil))))))))))
                        'nil))
                      'nil))
                    'nil))))))))))))))
      (cons
       (cons
        'define
        (cons
         type-array-length
         (cons
          (cons (cons 'array (cons type-arrayp 'nil))
                'nil)
          (cons
           ':returns
           (cons
            '(length int-valuep)
            (cons
             ':short
             (cons
              (str::cat "Obtain the length of a Java "
                        type-doc " array.")
              (cons
               (cons
                'int-value
                (cons
                  (cons 'len
                        (cons (cons type-array->components '(array))
                              'nil))
                  'nil))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                          'enable
                          (cons type-array->components '(sbyte32p)))
                     'nil)))
                  'nil)
                 'nil))))))))))
       (cons
        (cons
         'define
         (cons
          type-array-write
          (cons
           (cons (cons 'array (cons type-arrayp 'nil))
                 (cons '(index int-valuep)
                       (cons (cons 'component
                                   (cons type-valuep 'nil))
                             'nil)))
           (cons
            ':guard
            (cons
             (cons type-array-index-in-range-p
                   '(array index))
             (cons
              ':returns
              (cons
               (cons 'new-array
                     (cons type-arrayp 'nil))
               (cons
                ':short
                (cons
                 (str::cat "Write a component to a Java "
                           type-doc " array.")
                 (cons
                  (cons
                   'if
                   (cons
                    (cons 'mbt
                          (cons (cons type-array-index-in-range-p
                                      '(array index))
                                'nil))
                    (cons
                     (cons
                      type-array
                      (cons
                       (cons
                        'update-nth
                        (cons
                         '(int-value->int index)
                         (cons
                          'component
                          (cons
                              (cons type-array->components '(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->components
                           (cons type-array-index-in-range-p 'nil)))
                        'nil)))
                     'nil)
                    (cons
                     ':prepwork
                     (cons
                      (cons
                       '(local (include-book "std/lists/update-nth"
                                             :dir :system))
                       (cons
                        (cons
                         'local
                         (cons
                          (cons
                           'fty::deflist
                           (cons
                            type-value-list
                            (cons
                             ':elt-type
                             (cons
                              type-value
                              (cons
                               ':true-listp
                               (cons
                                't
                                (cons
                                 ':elementp-of-nil
                                 (cons
                                  'nil
                                  (cons
                                   ':pred
                                   (cons
                                     type-value-listp 'nil))))))))))
                          'nil))
                        'nil))
                      (cons
                       '///
                       (cons
                        (cons
                         'defret
                         (cons
                          (packn-pos (list 'len-of-components-of-
                                           type-array-write)
                                     jwit)
                          (cons
                           (cons
                            'equal
                            (cons
                             (cons
                              'len
                              (cons
                               (cons
                                type-array->components '(new-array))
                               'nil))
                             (cons
                              (cons
                               'len
                               (cons
                                (cons
                                    type-array->components '(array))
                                'nil))
                              'nil)))
                           (cons
                            ':hints
                            (cons
                             (cons
                              (cons
                               '"Goal"
                               (cons
                                ':in-theory
                                (cons
                                 (cons
                                  'enable
                                  (cons
                                   type-array->components
                                   (cons
                                    type-array-index-in-range-p
                                    (cons
                                      type-array
                                      (cons type-array-fix 'nil)))))
                                 'nil)))
                              'nil)
                             'nil)))))
                        (cons
                         (cons
                          'defret
                          (cons
                           (packn-pos
                             (list type-array-index-in-range-p '-of-
                                   type-array-write)
                             jwit)
                           (cons
                            (cons
                             'equal
                             (cons
                              (cons type-array-index-in-range-p
                                    '(new-array index1))
                              (cons
                                   (cons type-array-index-in-range-p
                                         '(array index1))
                                   'nil)))
                            (cons
                             ':hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':in-theory
                                 (cons
                                  (cons
                                   'enable
                                   (cons type-array-index-in-range-p
                                         'nil))
                                  'nil)))
                               'nil)
                              'nil)))))
                         'nil)))))))))))))))))
        (cons
         (cons
          'define
          (cons
           type-array-new-len
           (cons
            '((length int-valuep))
            (cons
             ':guard
             (cons
              '(>= (int-value->int length) 0)
              (cons
               ':returns
               (cons
                (cons 'array (cons type-arrayp 'nil))
                (cons
                 ':short
                 (cons
                  (str::cat
                   "Construct a Java " type-doc
                   " array
                              with the given length
                              and with default components.")
                  (cons
                   (cons
                    type-array
                    (cons
                     (cons
                      'repeat
                      (cons
                       '(int-value->int length)
                       (cons
                        (case type
                         (boolean '(boolean-value nil))
                         (char '(char-value 0))
                         (byte '(byte-value 0))
                         (short '(short-value 0))
                         (int '(int-value 0))
                         (long '(long-value 0))
                         (float
                          '(float-value (float-value-abs-pos-zero)))
                         (double '(double-value
                                       (double-value-abs-pos-zero)))
                         (t (impossible)))
                        'nil)))
                     'nil))
                   (cons
                    ':prepwork
                    (cons
                     (cons
                      '(local (include-book "std/lists/repeat"
                                            :dir :system))
                      (cons
                       (cons
                        'local
                        (cons
                         (cons
                          'fty::deflist
                          (cons
                           type-value-list
                           (cons
                            ':elt-type
                            (cons
                             type-value
                             (cons
                              ':true-listp
                              (cons
                               't
                               (cons
                                ':elementp-of-nil
                                (cons
                                 'nil
                                 (cons
                                  ':pred
                                  (cons
                                     type-value-listp 'nil))))))))))
                         'nil))
                       'nil))
                     'nil))))))))))))
         (cons
          (cons
           'define
           (cons
            type-array-new-init
            (cons
             (cons (cons 'comps
                         (cons type-value-listp 'nil))
                   'nil)
             (cons
              ':guard
              (cons
               '(< (len comps) (expt 2 31))
               (cons
                ':returns
                (cons
                 (cons 'array (cons type-arrayp 'nil))
                 (cons
                  ':short
                  (cons
                   (str::cat
                    "Construct a Java " type-doc
                    " array
                              with the given initializer (i.e. components).")
                   (cons (cons type-array '(comps))
                         'nil))))))))))
          (append
           (and
            acl2type
            (cons
             (cons
              'define
              (cons
               type-array-to-list
               (cons
                (cons (cons 'array (cons type-arrayp 'nil))
                      'nil)
                (cons
                 ':returns
                 (cons
                  (cons 'list (cons acl2type-listp 'nil))
                  (cons
                   ':short
                   (cons
                    (str::cat
                     "Convert a Java " type-doc
                     " array to
                              an ACL2 list of "
                     acl2type-doc ".")
                    (cons
                     (cons
                        type-array-to-list-aux
                        (cons (cons type-array->components '(array))
                              'nil))
                     (cons
                      ':prepwork
                      (cons
                       (cons
                        (cons
                         'define
                         (cons
                          type-array-to-list-aux
                          (cons
                           (cons (cons 'comps
                                       (cons type-value-listp 'nil))
                                 'nil)
                           (cons
                            ':returns
                            (cons
                             (cons 'list (cons acl2type-listp 'nil))
                             (cons
                              ':parents
                              (cons
                               'nil
                               (cons
                                (cons
                                 'cond
                                 (cons
                                  '((endp comps) nil)
                                  (cons
                                   (cons
                                    't
                                    (cons
                                     (cons
                                      'cons
                                      (cons
                                       (cons type-value->get
                                             '((car comps)))
                                       (cons
                                        (cons type-array-to-list-aux
                                              '((cdr comps)))
                                        'nil)))
                                     'nil))
                                   'nil)))
                                (cons
                                 '///
                                 (cons
                                  (cons
                                   'defret
                                   (cons
                                    (packn-pos
                                       (list 'len-of-
                                             type-array-to-list-aux)
                                       jwit)
                                    '((equal (len list)
                                             (len comps)))))
                                  'nil))))))))))
                        'nil)
                       (cons
                        '///
                        (cons
                         (cons
                          'defret
                          (cons
                           (packn-pos
                                (list 'len-of- type-array-to-list)
                                jwit)
                           (cons
                            (cons
                             'equal
                             (cons
                              '(len list)
                              (cons
                               (cons
                                'len
                                (cons
                                 (cons
                                    type-array->components '(array))
                                 'nil))
                               'nil)))
                            'nil)))
                         'nil))))))))))))
             'nil))
           (and
            acl2type
            (cons
             (cons
              'define
              (cons
               type-array-from-list
               (cons
                (cons (cons 'list (cons acl2type-listp 'nil))
                      'nil)
                (cons
                 ':guard
                 (cons
                  '(< (len list) (expt 2 31))
                  (cons
                   ':returns
                   (cons
                    (cons 'array (cons type-arrayp 'nil))
                    (cons
                     ':short
                     (cons
                      (str::cat
                           "Convert an ACL2 list of " acl2type-doc
                           " to a Java @('boolean') array.")
                      (cons
                       (cons
                        type-array
                        (cons
                             (cons type-array-from-list-aux '(list))
                             'nil))
                       (cons
                        ':prepwork
                        (cons
                         (cons
                          (cons
                           'define
                           (cons
                            type-array-from-list-aux
                            (cons
                             (cons (cons 'list
                                         (cons acl2type-listp 'nil))
                                   'nil)
                             (cons
                              ':returns
                              (cons
                               (cons 'comps
                                     (cons type-value-listp 'nil))
                               (cons
                                ':parents
                                (cons
                                 'nil
                                 (cons
                                  (cons
                                   'cond
                                   (cons
                                    '((endp list) nil)
                                    (cons
                                     (cons
                                      't
                                      (cons
                                       (cons
                                        'cons
                                        (cons
                                         (cons
                                           type-value '((car list)))
                                         (cons
                                          (cons
                                            type-array-from-list-aux
                                            '((cdr list)))
                                          'nil)))
                                       'nil))
                                     'nil)))
                                  (cons
                                   '///
                                   (cons
                                    (cons
                                     'defret
                                     (cons
                                      (packn-pos
                                       (list
                                           'len-of-
                                           type-array-from-list-aux)
                                       jwit)
                                      '((equal (len comps)
                                               (len list)))))
                                    'nil))))))))))
                          'nil)
                         'nil))))))))))))
             'nil)))))))))))))