Event to generate the ACL2 models of the C integer operations that involve one integer type.
(def-integer-operations-1 type1) → 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
Function:
(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 " [C: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 " [C: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 " [C: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 " [C: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 [C: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 [C: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:
(defthm pseudo-event-formp-of-def-integer-operations-1 (b* ((event (def-integer-operations-1 type1))) (pseudo-event-formp event)) :rule-classes :rewrite)