		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Uint-div

Division of unsigned integer values.

Signature
(uint-div left-operand right-operand) → result
Arguments: left-operand — Guard (uintp left-operand).; right-operand — Guard (uintp right-operand).
Returns: result — Type (uintp result).

Integer division rounds towards 0 in Solidity [SD: Types: Integers: Division], so we use truncate.

Definitions and Theorems

Function: uint-div

(defun uint-div (left-operand right-operand)
  (declare (xargs :guard (and (uintp left-operand)
                              (uintp right-operand))))
  (declare
       (xargs :guard (not (equal (uint->value right-operand) 0))))
  (b* ((size (uint->size left-operand))
       (x (uint->value left-operand))
       (y (uint->value right-operand)))
    (make-uint :size (uint->size left-operand)
               :value (loghead size (truncate x y)))))

Theorem: uintp-of-uint-div

(defthm uintp-of-uint-div
  (b* ((result (uint-div left-operand right-operand)))
    (uintp result))
  :rule-classes :rewrite)

Theorem: uint-div-of-uint-fix-left-operand

(defthm uint-div-of-uint-fix-left-operand
  (equal (uint-div (uint-fix left-operand)
                   right-operand)
         (uint-div left-operand right-operand)))

Theorem: uint-div-uint-equiv-congruence-on-left-operand

(defthm uint-div-uint-equiv-congruence-on-left-operand
  (implies (uint-equiv left-operand left-operand-equiv)
           (equal (uint-div left-operand right-operand)
                  (uint-div left-operand-equiv right-operand)))
  :rule-classes :congruence)

Theorem: uint-div-of-uint-fix-right-operand

(defthm uint-div-of-uint-fix-right-operand
  (equal (uint-div left-operand (uint-fix right-operand))
         (uint-div left-operand right-operand)))

Theorem: uint-div-uint-equiv-congruence-on-right-operand

(defthm uint-div-uint-equiv-congruence-on-right-operand
  (implies (uint-equiv right-operand right-operand-equiv)
           (equal (uint-div left-operand right-operand)
                  (uint-div left-operand right-operand-equiv)))
  :rule-classes :congruence)