		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Carry-out

Signature
(carry-out width cin x y) → *
Arguments: width — Guard (posp width).; cin — Guard (bitp cin).; x — Guard (integerp x).; y — Guard (integerp y).

Definitions and Theorems

Function: carry-out

(defun carry-out (width cin x y)
  (declare (xargs :guard (and (posp width)
                              (bitp cin)
                              (integerp x)
                              (integerp y))))
  (let ((__function__ 'carry-out))
    (declare (ignorable __function__))
    (b* ((width (lposfix width))
         (sum (sum-with-cin cin (loghead width x)
                            (loghead width y))))
      (logtail (lposfix width) sum))))

Theorem: carry-out-bit-is-carry-out

(defthm carry-out-bit-is-carry-out
 (implies
   (and (posp width)
        (equal xbit
               (bool->bit (logbitp (+ -1 width) x)))
        (equal ybit
               (bool->bit (logbitp (+ -1 width) y))))
   (equal
        (carry-out-bit xbit ybit
                       (bool->bit (logbitp (+ -1 width)
                                           (sum-with-cin cin x y))))
        (carry-out width cin x y))))

Theorem: bitp-of-carry-out

(defthm bitp-of-carry-out
  (bitp (carry-out width cin x y))
  :rule-classes :type-prescription)

Theorem: carry-out-correct

(defthm carry-out-correct
  (implies (posp width)
           (equal (logapp width (sum-with-cin cin x1 y1)
                          (sum-with-cin (carry-out width cin x1 y1)
                                        x2 y2))
                  (sum-with-cin cin (logapp width x1 x2)
                                (logapp width y1 y2)))))

Theorem: carry-out-of-carry-out

(defthm carry-out-of-carry-out
  (equal (carry-out w2 (carry-out w1 cin x1 y1)
                    x2 y2)
         (carry-out (+ (pos-fix w1) (pos-fix w2))
                    cin (logapp (pos-fix w1) x1 x2)
                    (logapp (pos-fix w1) y1 y2))))

Theorem: carry-out-of-sum

(defthm carry-out-of-sum
  (implies (posp width)
           (equal (logtail width (sum-with-cin cin x y))
                  (sum-with-cin (carry-out width cin x y)
                                (logtail width x)
                                (logtail width y)))))

Theorem: carry-out-simplify-loghead-1

(defthm carry-out-simplify-loghead-1
  (implies (and (equal ww (pos-fix width))
                (equal xx (loghead ww x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w ww)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead ww xxx)
                       (loghead ww xx)))
           (equal (carry-out width cin x y)
                  (carry-out width cin xxx y))))

Theorem: carry-out-simplify-loghead-2

(defthm carry-out-simplify-loghead-2
  (implies (and (equal ww (pos-fix width))
                (equal xx (loghead ww x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w ww)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead ww xxx)
                       (loghead ww xx)))
           (equal (carry-out width cin y x)
                  (carry-out width cin y xxx))))

Theorem: carry-out-of-pos-fix-width

(defthm carry-out-of-pos-fix-width
  (equal (carry-out (pos-fix width) cin x y)
         (carry-out width cin x y)))

Theorem: carry-out-pos-equiv-congruence-on-width

(defthm carry-out-pos-equiv-congruence-on-width
  (implies (pos-equiv width width-equiv)
           (equal (carry-out width cin x y)
                  (carry-out width-equiv cin x y)))
  :rule-classes :congruence)

Theorem: carry-out-of-bfix-cin

(defthm carry-out-of-bfix-cin
  (equal (carry-out width (bfix cin) x y)
         (carry-out width cin x y)))

Theorem: carry-out-bit-equiv-congruence-on-cin

(defthm carry-out-bit-equiv-congruence-on-cin
  (implies (bit-equiv cin cin-equiv)
           (equal (carry-out width cin x y)
                  (carry-out width cin-equiv x y)))
  :rule-classes :congruence)

Theorem: carry-out-of-ifix-x

(defthm carry-out-of-ifix-x
  (equal (carry-out width cin (ifix x) y)
         (carry-out width cin x y)))

Theorem: carry-out-int-equiv-congruence-on-x

(defthm carry-out-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (carry-out width cin x y)
                  (carry-out width cin x-equiv y)))
  :rule-classes :congruence)

Theorem: carry-out-of-ifix-y

(defthm carry-out-of-ifix-y
  (equal (carry-out width cin x (ifix y))
         (carry-out width cin x y)))

Theorem: carry-out-int-equiv-congruence-on-y

(defthm carry-out-int-equiv-congruence-on-y
  (implies (int-equiv y y-equiv)
           (equal (carry-out width cin x y)
                  (carry-out width cin x y-equiv)))
  :rule-classes :congruence)