		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Def-uint/int-comparison

Macro to formalize the Solidity integer comparisons.

This macro takes, as required arguments, the name of the function to define (which formalizes the comparison), an indication of whether the comparison is signed or not, and an untranslated term that defines the comparison on the core values. This term must have x and y as the only free variables, which the boilerplate code generated by the macro binds to the core value of the left and right operand.

This macro also takes optional arguments for XDOC documentation: parents, short string, and long string. The latter may be forms, e.g. involving XDOC constructors.

Macro: def-uint/int-comparison

(defmacro def-uint/int-comparison
          (name &key signedp operation
                (parents 'nil parents-suppliedp)
                (short 'nil short-suppliedp)
                (long 'nil long-suppliedp))
 (cons
  'make-event
  (cons
   (cons
    'def-uint/int-comparison-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons signedp 'nil))
      (cons
       (cons 'quote (cons operation 'nil))
       (cons
        (cons 'quote (cons parents 'nil))
        (cons
          parents-suppliedp
          (cons short
                (cons short-suppliedp
                      (cons long (cons long-suppliedp 'nil))))))))))
   'nil)))

Definitions and Theorems

Function: def-uint/int-comparison-fn

(defun def-uint/int-comparison-fn
       (name signedp operation
             parents parents-suppliedp short
             short-suppliedp long long-suppliedp)
 (declare (xargs :guard (and (symbolp name)
                             (booleanp signedp)
                             (symbol-listp parents)
                             (booleanp parents-suppliedp)
                             (booleanp short-suppliedp)
                             (booleanp long-suppliedp))))
 (let ((__function__ 'def-uint/int-comparison-fn))
  (declare (ignorable __function__))
  (b* ((type (if signedp 'int 'uint))
       (typep (add-suffix type "P"))
       (type->size (add-suffix type "->SIZE"))
       (type->value (add-suffix type "->VALUE")))
   (cons
    'define
    (cons
     name
     (cons
      (cons (cons 'left (cons typep 'nil))
            (cons (cons 'right (cons typep 'nil))
                  'nil))
      (cons
       ':guard
       (cons
        (cons '=
              (cons (cons type->size '(left))
                    (cons (cons type->size '(right)) 'nil)))
        (cons
         ':returns
         (cons
          '(result boolp)
          (append
           (and parents-suppliedp
                (list :parents parents))
           (append
            (and short-suppliedp (list :short short))
            (append
             (and long-suppliedp (list :long long))
             (cons
              (cons
               'b*
               (cons
                (cons
                 (cons 'x
                       (cons (cons type->value '(left)) 'nil))
                 (cons
                      (cons 'y
                            (cons (cons type->value '(right)) 'nil))
                      'nil))
                (cons (cons 'bool (cons operation 'nil))
                      'nil)))
              '(:hooks (:fix)
                       :no-function t)))))))))))))))