		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Def-integer-operations-1

Event to generate the ACL2 models of the C integer operations that involve one integer type.

Signature
(def-integer-operations-1 type1) → event
Arguments: type1 — Guard (typep type1).
Returns: event — Type (pseudo-event-formp event).

These include not only the unary operators, but also versions of the shift operators that take ACL2 integers as second operands. The latter are used in the definition of the shift operators whose second operands are C integers; see def-integer-operations-2.

For unary plus, unary minus, and bitwise complement, we generate different definitions based on whether the type has the rank of int or higher, or not: if it does, we generate a definition that performs a direct computation; if it does not, we generate a definition that converts and then calls the function for the promoted type.

Definitions and Theorems

Function: def-integer-operations-1

(defun def-integer-operations-1 (type1)
 (declare (xargs :guard (typep type1)))
 (declare (xargs :guard (type-nonchar-integerp type1)))
 (let ((__function__ 'def-integer-operations-1))
  (declare (ignorable __function__))
  (b* ((type1-string (integer-type-xdoc-string type1))
       (type (promote-type type1))
       (samep (equal type type1))
       (signedp (type-signed-integerp type))
       (<type1>-bits (integer-type-bits-nulfun type1))
       (<type1> (integer-type-to-fixtype type1))
       (<type1>p (pack <type1> 'p))
       (integer-from-<type1> (pack 'integer-from- <type1>))
       (<type1>-from-integer (pack <type1> '-from-integer))
       (<type1>-from-integer-mod (pack <type1>-from-integer '-mod))
       (<type1>-integerp (pack <type1> '-integerp))
       (<type1>-integerp-alt-def (pack <type1>-integerp '-alt-def))
       (<type1>-fix (pack <type1> '-fix))
       (<type1>-dec-const (pack <type1> '-dec-const))
       (<type1>-oct-const (pack <type1> '-oct-const))
       (<type1>-hex-const (pack <type1> '-hex-const))
       (boolean-from-<type1> (pack 'boolean-from- <type1>))
       (<type> (integer-type-to-fixtype type))
       (<type>p (pack <type> 'p))
       (<type>-min (pack <type> '-min))
       (<type>-max (pack <type> '-max))
       (<type>-from-<type1> (pack <type> '-from- <type1>))
       (plus-<type1> (pack 'plus- <type1>))
       (plus-<type> (pack 'plus- <type>))
       (minus-<type1> (pack 'minus- <type1>))
       (minus-<type1>-okp (pack minus-<type1> '-okp))
       (minus-<type> (pack 'minus- <type>))
       (minus-<type>-okp (pack minus-<type> '-okp))
       (bitnot-<type1> (pack 'bitnot- <type1>))
       (bitnot-<type> (pack 'bitnot- <type>))
       (lognot-<type1> (pack 'lognot- <type1>))
       (shl-<type1> (pack 'shl- <type1>))
       (shl-<type1>-okp (pack shl-<type1> '-okp))
       (shl-<type> (pack 'shl- <type>))
       (shl-<type>-okp (pack shl-<type> '-okp))
       (shr-<type1> (pack 'shr- <type1>))
       (shr-<type1>-okp (pack shr-<type1> '-okp))
       (shr-<type> (pack 'shr- <type>))
       (shr-<type>-okp (pack shr-<type> '-okp)))
   (cons
    'progn
    (cons
     '(set-ignore-ok t)
     (cons
      '(set-irrelevant-formals-ok t)
      (append
       (and
        samep
        (cons
         (cons
          'defun-integer
          (cons
           <type1>-dec-const
           (cons
            ':arg-type
            (cons
             'natp
             (cons
              ':guard
              (cons
               (cons <type1>-integerp '(x))
               (cons
                ':res-type
                (cons
                 <type1>p
                 (cons
                  ':short
                  (cons (str::cat "Decimal integer constant of "
                                  type1-string ".")
                        (cons ':body
                              (cons (cons <type1>-from-integer '(x))
                                    '(:no-fix t)))))))))))))
         'nil))
       (append
        (and
         samep
         (cons
          (cons
           'defun-integer
           (cons
            <type1>-oct-const
            (cons
             ':arg-type
             (cons
              'natp
              (cons
               ':guard
               (cons
                (cons <type1>-integerp '(x))
                (cons
                 ':res-type
                 (cons
                  <type1>p
                  (cons
                   ':short
                   (cons
                        (str::cat "Octal integer constant of "
                                  type1-string ".")
                        (cons ':body
                              (cons (cons <type1>-from-integer '(x))
                                    '(:no-fix t)))))))))))))
          'nil))
        (append
         (and
          samep
          (cons
           (cons
            'defun-integer
            (cons
             <type1>-hex-const
             (cons
              ':arg-type
              (cons
               'natp
               (cons
                ':guard
                (cons
                 (cons <type1>-integerp '(x))
                 (cons
                  ':res-type
                  (cons
                   <type1>p
                   (cons
                    ':short
                    (cons
                        (str::cat "Hexadecimal integer constant of "
                                  type1-string ".")
                        (cons ':body
                              (cons (cons <type1>-from-integer '(x))
                                    '(:no-fix t)))))))))))))
           'nil))
         (cons
          (cons
           'defun-integer
           (cons
            boolean-from-<type1>
            (cons
             ':arg-type
             (cons
              <type1>p
              (cons
               ':res-type
               (cons
                'booleanp
                (cons
                 ':short
                 (cons
                  (str::cat "Check if a value of "
                            type1-string " is not 0.")
                  (cons
                   ':body
                   (cons
                        (cons '/=
                              (cons (cons integer-from-<type1> '(x))
                                    '(0)))
                        'nil))))))))))
          (cons
           (cons
            'defun-integer
            (cons
             plus-<type1>
             (cons
              ':arg-type
              (cons
               <type1>p
               (cons
                ':res-type
                (cons
                 <type>p
                 (cons
                  ':short
                  (cons
                   (str::cat "Unary plus of a value of "
                             type1-string " [C17:6.5.3].")
                   (cons
                    ':body
                    (cons
                       (if samep (cons <type1>-fix '(x))
                         (cons plus-<type>
                               (cons (cons <type>-from-<type1> '(x))
                                     'nil)))
                       'nil))))))))))
           (append
            (and
             signedp
             (cons
              (cons
               'defun-integer
               (cons
                minus-<type1>-okp
                (cons
                 ':arg-type
                 (cons
                  <type1>p
                  (cons
                   ':res-type
                   (cons
                    'booleanp
                    (cons
                     ':short
                     (cons
                      (str::cat
                           "Check if the unary minus of a value of "
                           type1-string " is well-defined.")
                      (cons
                       ':body
                       (cons
                        (if samep
                         (cons
                          <type1>-integerp
                          (cons
                           (cons
                              '-
                              (cons (cons integer-from-<type1> '(x))
                                    'nil))
                           'nil))
                         (cons minus-<type>-okp
                               (cons (cons <type>-from-<type1> '(x))
                                     'nil)))
                        'nil))))))))))
              'nil))
            (cons
             (cons
              'defun-integer
              (cons
               minus-<type1>
               (cons
                ':arg-type
                (cons
                 <type1>p
                 (append
                  (and signedp
                       (cons ':guard
                             (cons (cons minus-<type1>-okp '(x))
                                   'nil)))
                  (cons
                   ':res-type
                   (cons
                    <type>p
                    (cons
                     ':short
                     (cons
                      (str::cat "Unary minus of a value of "
                                type1-string " [C17:6.5.3].")
                      (cons
                       ':body
                       (cons
                        (if samep
                         (cons
                          (if signedp <type1>-from-integer
                            <type1>-from-integer-mod)
                          (cons
                           (cons
                              '-
                              (cons (cons integer-from-<type1> '(x))
                                    'nil))
                           'nil))
                         (cons minus-<type>
                               (cons (cons <type>-from-<type1> '(x))
                                     'nil)))
                        (and
                         signedp
                         (cons
                          ':guard-hints
                          (cons
                           (cons
                            (cons
                             '"Goal"
                             (cons
                              ':in-theory
                              (cons
                                (cons 'enable
                                      (cons minus-<type1>-okp 'nil))
                                'nil)))
                            'nil)
                           'nil))))))))))))))
             (cons
              (cons
               'defun-integer
               (cons
                bitnot-<type1>
                (cons
                 ':arg-type
                 (cons
                  <type1>p
                  (cons
                   ':res-type
                   (cons
                    <type>p
                    (cons
                     ':short
                     (cons
                      (str::cat "Bitwise complement of a value of "
                                type1-string " [C17:6.5.3].")
                      (cons
                       ':body
                       (cons
                        (if samep
                         (cons
                          (if signedp <type1>-from-integer
                            <type1>-from-integer-mod)
                          (cons
                           (cons
                              'lognot
                              (cons (cons integer-from-<type1> '(x))
                                    'nil))
                           'nil))
                         (cons bitnot-<type>
                               (cons (cons <type>-from-<type1> '(x))
                                     'nil)))
                        (and
                         samep signedp
                         (cons
                          ':guard-hints
                          (cons
                           (cons
                            (cons
                             '"Goal"
                             (cons
                              ':in-theory
                              (cons
                               (cons
                                'enable
                                (cons
                                 <type1>-integerp-alt-def
                                 (cons
                                  integer-from-<type1>
                                  (cons
                                   <type1>p
                                   (cons
                                    (cons ':e
                                          (cons <type>-min 'nil))
                                    (cons
                                       (cons ':e
                                             (cons <type>-max 'nil))
                                       '(lognot ifix)))))))
                               'nil)))
                            'nil)
                           'nil)))))))))))))
              (cons
               (cons
                'defun-integer
                (cons
                 lognot-<type1>
                 (cons
                  ':arg-type
                  (cons
                   <type1>p
                   (cons
                    ':res-type
                    (cons
                     'sintp
                     (cons
                      ':short
                      (cons
                       (str::cat "Logical complement of a value of "
                                 type1-string " [C17:6.5.3].")
                       (cons
                        ':body
                        (cons
                         (cons
                          'sint-from-boolean
                          (cons
                           (cons
                              '=
                              (cons (cons integer-from-<type1> '(x))
                                    '(0)))
                           'nil))
                         'nil))))))))))
               (cons
                (cons
                 'defun-integer
                 (cons
                  shl-<type1>-okp
                  (cons
                   ':arg1-type
                   (cons
                    <type1>p
                    (cons
                     ':arg2-type
                     (cons
                      'integerp
                      (cons
                       ':res-type
                       (cons
                        'booleanp
                        (cons
                         ':short
                         (cons
                          (str::cat
                            "Check if the left shift of a value of "
                            type1-string
                            " by an integer is well-defined.")
                          (cons
                           ':body
                           (cons
                            (if samep
                             (if signedp
                              (cons
                               'and
                               (cons
                                (cons
                                 'integer-range-p
                                 (cons
                                      '0
                                      (cons (cons <type1>-bits 'nil)
                                            '((ifix y)))))
                                (cons
                                 (cons
                                  '>=
                                  (cons
                                    (cons integer-from-<type1> '(x))
                                    '(0)))
                                 (cons
                                  (cons
                                   <type1>-integerp
                                   (cons
                                    (cons
                                     '*
                                     (cons
                                      (cons
                                          integer-from-<type1> '(x))
                                      '((expt 2 (ifix y)))))
                                    'nil))
                                  'nil))))
                              (cons
                                'integer-range-p
                                (cons '0
                                      (cons (cons <type1>-bits 'nil)
                                            '((ifix y))))))
                             (cons
                               shl-<type>-okp
                               (cons (cons <type>-from-<type1> '(x))
                                     '((ifix y)))))
                            'nil))))))))))))
                (cons
                 (cons
                  'defun-integer
                  (cons
                   shl-<type1>
                   (cons
                    ':arg1-type
                    (cons
                     <type1>p
                     (cons
                      ':arg2-type
                      (cons
                       'integerp
                       (cons
                        ':guard
                        (cons
                         (cons shl-<type1>-okp '(x y))
                         (cons
                          ':res-type
                          (cons
                           <type>p
                           (cons
                            ':short
                            (cons
                             (str::cat
                                  "Left shift of a value of "
                                  type1-string
                                  " by an integer [C17:6.5.7].")
                             (cons
                              ':body
                              (cons
                               (if samep
                                (cons
                                 (if signedp <type1>-from-integer
                                   <type1>-from-integer-mod)
                                 (cons
                                  (cons
                                   '*
                                   (cons
                                    (cons integer-from-<type1> '(x))
                                    '((expt 2 (ifix y)))))
                                  'nil))
                                (cons
                                 shl-<type>
                                 (cons
                                     (cons <type>-from-<type1> '(x))
                                     '(y))))
                               (cons
                                ':guard-hints
                                (cons
                                 (cons
                                  (cons
                                   '"Goal"
                                   (cons
                                    ':in-theory
                                    (cons
                                     (cons
                                          'enable
                                          (cons shl-<type1>-okp
                                                '(integer-range-p)))
                                     'nil)))
                                  'nil)
                                 (and
                                  (not signedp)
                                  '(:prepwork
                                    ((local
                                      (include-book
                                        "arithmetic-3/top"
                                        :dir
                                        :system)))))))))))))))))))))
                 (cons
                  (cons
                   'defun-integer
                   (cons
                    shr-<type1>-okp
                    (cons
                     ':arg1-type
                     (cons
                      <type1>p
                      (cons
                       ':arg2-type
                       (cons
                        'integerp
                        (cons
                         ':res-type
                         (cons
                          'booleanp
                          (cons
                           ':short
                           (cons
                            (str::cat
                             "Check if the right shift of a value of "
                             type1-string
                             " by an integer is well-defined.")
                            (cons
                             ':body
                             (cons
                              (if samep
                               (if signedp
                                (cons
                                 'and
                                 (cons
                                  (cons
                                   'integer-range-p
                                   (cons
                                      '0
                                      (cons (cons <type1>-bits 'nil)
                                            '((ifix y)))))
                                  (cons
                                   (cons
                                    '>=
                                    (cons
                                     (cons
                                          integer-from-<type1> '(x))
                                     '(0)))
                                   'nil)))
                                (cons
                                 'integer-range-p
                                 (cons
                                      '0
                                      (cons (cons <type1>-bits 'nil)
                                            '((ifix y))))))
                               (cons
                                shr-<type>-okp
                                (cons
                                     (cons <type>-from-<type1> '(x))
                                     '((ifix y)))))
                              'nil))))))))))))
                  (cons
                   (cons
                    'defun-integer
                    (cons
                     shr-<type1>
                     (cons
                      ':arg1-type
                      (cons
                       <type1>p
                       (cons
                        ':arg2-type
                        (cons
                         'integerp
                         (cons
                          ':guard
                          (cons
                           (cons shr-<type1>-okp '(x y))
                           (cons
                            ':res-type
                            (cons
                             <type>p
                             (cons
                              ':short
                              (cons
                               (str::cat
                                    "Right shift of a value of "
                                    type1-string
                                    " by an integer [C17:6.5.7].")
                               (cons
                                ':body
                                (cons
                                 (if samep
                                  (cons
                                   (if signedp <type1>-from-integer
                                     <type1>-from-integer-mod)
                                   (cons
                                    (cons
                                     'truncate
                                     (cons
                                      (cons
                                          integer-from-<type1> '(x))
                                      '((expt 2 (ifix y)))))
                                    'nil))
                                  (cons
                                   shr-<type>
                                   (cons
                                     (cons <type>-from-<type1> '(x))
                                     '(y))))
                                 (cons
                                  ':guard-hints
                                  (cons
                                   (cons
                                    (cons
                                     '"Goal"
                                     (cons
                                      ':in-theory
                                      (cons
                                       (cons
                                        'enable
                                        (if
                                         (and samep signedp)
                                         (list
                                             shr-<type1>-okp
                                             <type1>-integerp
                                             integer-from-<type1>
                                             <type1>p 'signed-byte-p
                                             'integer-range-p)
                                         (list shr-<type1>-okp)))
                                       'nil)))
                                    'nil)
                                   (and
                                    signedp
                                    '(:prepwork
                                      ((local
                                        (include-book
                                         "kestrel/arithmetic-light/expt"
                                         :dir :system))
                                       (local
                                        (include-book
                                         "kestrel/arithmetic-light/truncate"
                                         :dir
                                         :system)))))))))))))))))))))
                   'nil)))))))))))))))))))

Theorem: pseudo-event-formp-of-def-integer-operations-1

(defthm pseudo-event-formp-of-def-integer-operations-1
  (b* ((event (def-integer-operations-1 type1)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)