		Search-engine friendly clone of the ACL2 documentation.

Integer-arithmetic-operations

Op-int-rem-wrapped

Leo integer wrapped remainder operation.

Signature
(op-int-rem-wrapped left right) → result
Arguments: left — Guard (int-valuep left).; right — Guard (int-valuep right).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-int-rem-wrapped

(defun op-int-rem-wrapped (left right)
  (declare (xargs :guard (and (int-valuep left)
                              (int-valuep right))))
  (let ((__function__ 'op-int-rem-wrapped))
    (declare (ignorable __function__))
    (b* ((err (reserrf (list :op-int-rem-wrapped (value-fix left)
                             (value-fix right)))))
      (cond ((and (value-case left :u8)
                  (value-case right :u8))
             (b* (((when (= (value-u8->get right) 0)) err)
                  (res (rem (value-u8->get left)
                            (value-u8->get right))))
               (value-u8 (loghead 8 res))))
            ((and (value-case left :u16)
                  (value-case right :u16))
             (b* (((when (= (value-u16->get right) 0))
                   err)
                  (res (rem (value-u16->get left)
                            (value-u16->get right))))
               (value-u16 (loghead 16 res))))
            ((and (value-case left :u32)
                  (value-case right :u32))
             (b* (((when (= (value-u32->get right) 0))
                   err)
                  (res (rem (value-u32->get left)
                            (value-u32->get right))))
               (value-u32 (loghead 32 res))))
            ((and (value-case left :u64)
                  (value-case right :u64))
             (b* (((when (= (value-u64->get right) 0))
                   err)
                  (res (rem (value-u64->get left)
                            (value-u64->get right))))
               (value-u64 (loghead 64 res))))
            ((and (value-case left :u128)
                  (value-case right :u128))
             (b* (((when (= (value-u128->get right) 0))
                   err)
                  (res (rem (value-u128->get left)
                            (value-u128->get right))))
               (value-u128 (loghead 128 res))))
            ((and (value-case left :i8)
                  (value-case right :i8))
             (b* (((when (= (value-i8->get right) 0)) err)
                  (z (truncate (value-i8->get left)
                               (value-i8->get right)))
                  (w (logext 8 z))
                  (res (rem (value-i8->get left)
                            (value-i8->get right)))
                  (wres (if (= w z) res 0)))
               (if (sbyte8p wres)
                   (value-i8 wres)
                 err)))
            ((and (value-case left :i16)
                  (value-case right :i16))
             (b* (((when (= (value-i16->get right) 0))
                   err)
                  (z (truncate (value-i16->get left)
                               (value-i16->get right)))
                  (w (logext 16 z))
                  (res (rem (value-i16->get left)
                            (value-i16->get right)))
                  (wres (if (= w z) res 0)))
               (if (sbyte16p wres)
                   (value-i16 wres)
                 err)))
            ((and (value-case left :i32)
                  (value-case right :i32))
             (b* (((when (= (value-i32->get right) 0))
                   err)
                  (z (truncate (value-i32->get left)
                               (value-i32->get right)))
                  (w (logext 32 z))
                  (res (rem (value-i32->get left)
                            (value-i32->get right)))
                  (wres (if (= w z) res 0)))
               (if (sbyte32p wres)
                   (value-i32 wres)
                 err)))
            ((and (value-case left :i64)
                  (value-case right :i64))
             (b* (((when (= (value-i64->get right) 0))
                   err)
                  (z (truncate (value-i64->get left)
                               (value-i64->get right)))
                  (w (logext 64 z))
                  (res (rem (value-i64->get left)
                            (value-i64->get right)))
                  (wres (if (= w z) res 0)))
               (if (sbyte64p wres)
                   (value-i64 wres)
                 err)))
            ((and (value-case left :i128)
                  (value-case right :i128))
             (b* (((when (= (value-i128->get right) 0))
                   err)
                  (z (truncate (value-i128->get left)
                               (value-i128->get right)))
                  (w (logext 128 z))
                  (res (rem (value-i128->get left)
                            (value-i128->get right)))
                  (wres (if (= w z) res 0)))
               (if (sbyte128p wres)
                   (value-i128 wres)
                 err)))
            (t err)))))

Theorem: value-resultp-of-op-int-rem-wrapped

(defthm value-resultp-of-op-int-rem-wrapped
  (b* ((result (op-int-rem-wrapped left right)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-int-rem-wrapped-of-value-fix-left

(defthm op-int-rem-wrapped-of-value-fix-left
  (equal (op-int-rem-wrapped (value-fix left)
                             right)
         (op-int-rem-wrapped left right)))

Theorem: op-int-rem-wrapped-value-equiv-congruence-on-left

(defthm op-int-rem-wrapped-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-int-rem-wrapped left right)
                  (op-int-rem-wrapped left-equiv right)))
  :rule-classes :congruence)

Theorem: op-int-rem-wrapped-of-value-fix-right

(defthm op-int-rem-wrapped-of-value-fix-right
  (equal (op-int-rem-wrapped left (value-fix right))
         (op-int-rem-wrapped left right)))

Theorem: op-int-rem-wrapped-value-equiv-congruence-on-right

(defthm op-int-rem-wrapped-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-int-rem-wrapped left right)
                  (op-int-rem-wrapped left right-equiv)))
  :rule-classes :congruence)