• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
        • Sparseint-impl
          • Sparseint$-binary-bitop-width
          • Sparseint$-plus-width
          • Sparseint$-binary-bitop-offset
          • Sparseint$-binary-bitop-int-width
          • Sparseint$-plus-int-width
          • Sum-with-cin
          • Sparseint$-plus-offset
          • Sparseint$-binary-bitop-int
          • Sparseint$-finalize-concat
          • Sparseint$-plus-int
          • Sparseint$-binary-bittest-width
          • Sparseint$-binary-bittest-int-width
          • Sparseint$-trailing-0-count-width
          • Sparseint$-height
          • Int-to-sparseint$-rec
          • Carry-out
          • Sparseint$-compare-width
          • Sparseint$-binary-bittest-offset
          • Sparseint$-equal-width
          • Sparseint$-binary-bittest-int
          • Sparseint$-compare-int-width
          • Sparseint$-bitcount-width
          • Sparseint$-unary-bittest-width
          • Sparseint$-rightshift-rec
          • Sparseint$-equal-int-width
          • Sparseint$-trailing-0-count-rec
          • Sparseint$-unary-bitop
          • Sparseint$-concatenate
          • Sparseint$-length-width-rec
          • Sparseint$-sign-ext
          • Sparseint$-binary-bitop
          • Binary-bitop
          • Sparseint$-compare-offset
          • Sparseint$-unary-bittest-offset
          • Sparseint$-equal-offset
          • Sparseint$-truncate
          • Sparseint$-mergeable-leaves-p
          • Carry-out-bit
          • Sparseint$-truncate-height
          • Sparseint$-compare-int
          • Sparseint$-binary-bittest
          • Sparseint$-equal-int
          • Sparseint$-rightshift
          • Sparseint$-leaves-mergeable-p
          • Sparseint$-plus
          • Unary-bitop
          • Sparseint$-bitcount-rec
          • Within-1
          • Sparseint$
          • Binary-bitop-cofactor2
          • Binary-bitop-cofactor1
          • Sparseint$-compare
          • Sparseint$-unary-bittest
          • Sparseint$-height-correct-exec
          • Sparseint$-equal
          • Sparseint$-bitnot
          • Sparseint$-unary-minus
          • Sparseint$-bit
          • Int-to-sparseint$
          • Binary-bittest
          • Sparseint$-length-rec
          • Sparseint$-val
          • Binary-bitop-swap
          • Compare
          • Sparseint$-real-height
          • Sparseint$-height-correctp
          • Sparseint$-length
        • Sparseint-p
        • Sparseint-binary-bittest
        • Sparseint-concatenate
        • Sparseint-binary-bitop
        • Sparseint-bitite
        • Sparseint-fix
        • Sparseint$-binary-minus
        • Sparseint-trailing-1-count-from
        • Sparseint-trailing-0-count-from
        • Sparseint-equal
        • Sparseint-test-bitorc2
        • Sparseint-test-bitorc1
        • Sparseint-test-bitnand
        • Sparseint-test-bitandc2
        • Sparseint-test-bitandc1
        • Sparseint-test-bitand
        • Sparseint-rightshift
        • Sparseint-bitcount-from
        • Sparseint-test-bitxor
        • Sparseint-test-bitor
        • Sparseint-test-bitnor
        • Sparseint-test-biteqv
        • Sparseint-compare
        • Sparseint-binary-minus
        • Sparseint-sign-ext
        • Sparseint-plus
        • Sparseint-bitandc2
        • Sparseint-bitandc1
        • Sparseint-bitand
        • Sparseint$-leaf-bitlimit
        • Sparseint-bitxor
        • Sparseint-bitorc2
        • Sparseint-bitorc1
        • Sparseint-bitor
        • Sparseint-bitnor
        • Sparseint-bitnand
        • Sparseint-biteqv
        • Sparseint-ash
        • Sparseint-<
        • Sparseint-bit
        • Sparseint-trailing-1-count
        • Sparseint-trailing-0-count
        • Sparseint-unary-minus
        • Sparseint-length
        • Sparseint-bitnot
        • Sparseint-bitcount
        • Int-to-sparseint
        • Sparseint-val
      • Bitops
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Sparseint-impl

Sparseint$-plus-width

Signature

(sparseint$-plus-width width x x.height y-offset y y.height cin) 
  → 
(mv sum height cout)

Arguments

width — Guard (posp width).

x — Guard (sparseint$-p x).

x.height — Guard (natp x.height).

y-offset — Guard (natp y-offset).

y — Guard (sparseint$-p y).

y.height — Guard (natp y.height).

cin — Guard (bitp cin).

Returns

sum — Type (sparseint$-p sum).

height — Type (equal height (sparseint$-height sum)).

cout — Type (bitp cout).

Definitions and Theorems

Function: sparseint$-plus-width

(defun sparseint$-plus-width
       (width x x.height y-offset y y.height cin)
 (declare (xargs :guard (and (posp width)
                             (sparseint$-p x)
                             (natp x.height)
                             (natp y-offset)
                             (sparseint$-p y)
                             (natp y.height)
                             (bitp cin))))
 (declare
      (xargs :guard (and (sparseint$-height-correctp x)
                         (equal x.height (sparseint$-height x))
                         (sparseint$-height-correctp y)
                         (equal y.height (sparseint$-height y)))))
 (let ((__function__ 'sparseint$-plus-width))
  (declare (ignorable __function__))
  (b* ((x.height (mbe :logic (sparseint$-height x)
                      :exec x.height))
       (y.height (mbe :logic (sparseint$-height y)
                      :exec y.height))
       (width (lposfix width))
       (y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
       y :leaf
       (b* ((yval (bignum-logext width (logtail y-offset y.val)))
            (xval (bignum-logext width x.val))
            (sum (bignum-logext width (sum-with-cin cin xval yval)))
            (cout (carry-out-bit (logbit (1- width) xval)
                                 (logbit (1- width) yval)
                                 (logbit (1- width) sum))))
         (mv (sparseint$-leaf sum) 0 cout))
       :concat (sparseint$-plus-int-width
                    width y-offset
                    y y.height (bignum-logext width x.val)
                    cin))
    :concat
    (sparseint$-case
     y :leaf
     (sparseint$-plus-int-width
          width 0 x x.height
          (bignum-logext width (logtail y-offset y.val))
          cin)
     :concat
     (b*
      ((x.lsbs.height
            (mbe :logic (sparseint$-height x.lsbs)
                 :exec (- x.height (if x.msbs-taller 2 1))))
       ((when (<= width x.width))
        (sparseint$-plus-width
             width x.lsbs
             x.lsbs.height y-offset y y.height cin))
       (y.msbs.height
            (mbe :logic (sparseint$-height y.msbs)
                 :exec (- y.height (if y.lsbs-taller 2 1))))
       ((when (<= y.width y-offset))
        (sparseint$-plus-width width x x.height (- y-offset y.width)
                               y.msbs y.msbs.height cin))
       (y-width1 (- y.width y-offset))
       (y.lsbs.height
            (mbe :logic (sparseint$-height y.lsbs)
                 :exec (- y.height (if y.msbs-taller 2 1))))
       ((when (<= width y-width1))
        (sparseint$-plus-width width x x.height
                               y-offset y.lsbs y.lsbs.height cin))
       ((mv lsbs-sum lsbs-sum.height lsbs-cout)
        (sparseint$-plus-width
             x.width x.lsbs
             x.lsbs.height y-offset y y.height cin))
       (x.msbs.height
            (mbe :logic (sparseint$-height x.msbs)
                 :exec (- x.height (if x.lsbs-taller 2 1))))
       ((mv msbs-sum msbs-sum.height msbs-cout)
        (sparseint$-plus-width (- width x.width)
                               x.msbs
                               x.msbs.height (+ x.width y-offset)
                               y y.height lsbs-cout))
       ((mv sum-concat sum-height)
        (sparseint$-concatenate-rebalance
             x.width lsbs-sum lsbs-sum.height
             msbs-sum msbs-sum.height)))
      (mv sum-concat sum-height msbs-cout)))))))

Theorem: sparseint$-p-of-sparseint$-plus-width.sum

(defthm sparseint$-p-of-sparseint$-plus-width.sum
  (b* (((mv ?sum ?height ?cout)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))
    (sparseint$-p sum))
  :rule-classes :rewrite)

Theorem: return-type-of-sparseint$-plus-width.height

(defthm return-type-of-sparseint$-plus-width.height
  (b* (((mv ?sum ?height ?cout)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))
    (equal height (sparseint$-height sum)))
  :rule-classes :rewrite)

Theorem: bitp-of-sparseint$-plus-width.cout

(defthm bitp-of-sparseint$-plus-width.cout
  (b* (((mv ?sum ?height ?cout)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))
    (bitp cout))
  :rule-classes :type-prescription)

Theorem: sparseint$-height-correctp-of-sparseint$-plus-width

(defthm sparseint$-height-correctp-of-sparseint$-plus-width
  (b* (((mv ?sum ?height ?cout)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))
    (implies (and (sparseint$-height-correctp x)
                  (sparseint$-height-correctp y))
             (sparseint$-height-correctp sum))))

Theorem: sparseint$-val-of-sparseint$-plus-width

(defthm sparseint$-val-of-sparseint$-plus-width
 (b* (((mv ?sum ?height ?cout)
       (sparseint$-plus-width width
                              x x.height y-offset y y.height cin)))
  (and
   (equal
      (sparseint$-val sum)
      (logext width
              (sum-with-cin cin (sparseint$-val x)
                            (logtail y-offset (sparseint$-val y)))))
   (equal cout
          (carry-out width cin (sparseint$-val x)
                     (logtail y-offset (sparseint$-val y)))))))

Theorem: sparseint$-plus-width-of-pos-fix-width

(defthm sparseint$-plus-width-of-pos-fix-width
 (equal (sparseint$-plus-width (pos-fix width)
                               x x.height y-offset y y.height cin)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-pos-equiv-congruence-on-width

(defthm sparseint$-plus-width-pos-equiv-congruence-on-width
 (implies
   (pos-equiv width width-equiv)
   (equal
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)
        (sparseint$-plus-width width-equiv
                               x x.height y-offset y y.height cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-sparseint$-fix-x

(defthm sparseint$-plus-width-of-sparseint$-fix-x
 (equal (sparseint$-plus-width width (sparseint$-fix x)
                               x.height y-offset y y.height cin)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-sparseint$-equiv-congruence-on-x

(defthm sparseint$-plus-width-sparseint$-equiv-congruence-on-x
 (implies
   (sparseint$-equiv x x-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x-equiv
                                 x.height y-offset y y.height cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-nfix-x.height

(defthm sparseint$-plus-width-of-nfix-x.height
 (equal (sparseint$-plus-width width x (nfix x.height)
                               y-offset y y.height cin)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-nat-equiv-congruence-on-x.height

(defthm sparseint$-plus-width-nat-equiv-congruence-on-x.height
 (implies
   (nat-equiv x.height x.height-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x x.height-equiv
                                 y-offset y y.height cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-nfix-y-offset

(defthm sparseint$-plus-width-of-nfix-y-offset
 (equal (sparseint$-plus-width width x x.height (nfix y-offset)
                               y y.height cin)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-nat-equiv-congruence-on-y-offset

(defthm sparseint$-plus-width-nat-equiv-congruence-on-y-offset
 (implies
   (nat-equiv y-offset y-offset-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x x.height
                                 y-offset-equiv y y.height cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-sparseint$-fix-y

(defthm sparseint$-plus-width-of-sparseint$-fix-y
  (equal
       (sparseint$-plus-width width
                              x x.height y-offset (sparseint$-fix y)
                              y.height cin)
       (sparseint$-plus-width width
                              x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-sparseint$-equiv-congruence-on-y

(defthm sparseint$-plus-width-sparseint$-equiv-congruence-on-y
 (implies
   (sparseint$-equiv y y-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x x.height
                                 y-offset y-equiv y.height cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-nfix-y.height

(defthm sparseint$-plus-width-of-nfix-y.height
 (equal (sparseint$-plus-width width
                               x x.height y-offset y (nfix y.height)
                               cin)
        (sparseint$-plus-width width
                               x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-nat-equiv-congruence-on-y.height

(defthm sparseint$-plus-width-nat-equiv-congruence-on-y.height
 (implies
   (nat-equiv y.height y.height-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x x.height
                                 y-offset y y.height-equiv cin)))
 :rule-classes :congruence)

Theorem: sparseint$-plus-width-of-bfix-cin

(defthm sparseint$-plus-width-of-bfix-cin
 (equal
     (sparseint$-plus-width width x
                            x.height y-offset y y.height (bfix cin))
     (sparseint$-plus-width width
                            x x.height y-offset y y.height cin)))

Theorem: sparseint$-plus-width-bit-equiv-congruence-on-cin

(defthm sparseint$-plus-width-bit-equiv-congruence-on-cin
 (implies
   (bit-equiv cin cin-equiv)
   (equal (sparseint$-plus-width width
                                 x x.height y-offset y y.height cin)
          (sparseint$-plus-width width x x.height
                                 y-offset y y.height cin-equiv)))
 :rule-classes :congruence)