• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • 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$-finalize-concat

Signature

(sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height) 
  → 
(mv concat height)

Arguments

width — Guard (posp width).

lsbs — Guard (sparseint$-p lsbs).

msbs — Guard (sparseint$-p msbs).

Returns

concat — Type (sparseint$-p concat).

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

Definitions and Theorems

Function: sparseint$-finalize-concat

(defun sparseint$-finalize-concat
       (width lsbs lsbs.height msbs msbs.height)
 (declare (xargs :guard (and (posp width)
                             (sparseint$-p lsbs)
                             (sparseint$-p msbs))))
 (declare
     (xargs :guard (and (sparseint$-height-correctp lsbs)
                        (equal lsbs.height (sparseint$-height lsbs))
                        (sparseint$-height-correctp msbs)
                        (equal msbs.height (sparseint$-height msbs))
                        (within-1 lsbs.height msbs.height))))
 (let ((__function__ 'sparseint$-finalize-concat))
  (declare (ignorable __function__))
  (b*
   ((lsbs.height (mbe :logic (sparseint$-height lsbs)
                      :exec lsbs.height))
    (msbs.height (mbe :logic (sparseint$-height msbs)
                      :exec msbs.height))
    ((unless (and (eql lsbs.height 0)
                  (eql msbs.height 0)))
     (mv (make-sparseint$-concat
              :width width
              :lsbs lsbs
              :msbs msbs
              :lsbs-taller (> lsbs.height msbs.height)
              :msbs-taller (> msbs.height lsbs.height))
         (+ 1 (max lsbs.height msbs.height))))
    ((sparseint$-leaf lsbs))
    ((sparseint$-leaf msbs))
    (width (lposfix width))
    ((when (eql 0 width))
     (mv (sparseint$-fix msbs) 0))
    ((when (or (eql msbs.val 0) (eql msbs.val -1)))
     (b*
      (((when (eql (logbitp (1- width) lsbs.val)
                   (logbitp 0 msbs.val)))
        (if (< (integer-length lsbs.val) width)
            (mv (sparseint$-fix lsbs) 0)
         (mv
          (make-sparseint$-leaf :val (bignum-logext width lsbs.val))
          0)))
       ((when (< width (sparseint$-leaf-bitlimit)))
        (mv (make-sparseint$-leaf
                 :val (logapp width lsbs.val msbs.val))
            0)))
      (mv (make-sparseint$-concat :width width
                                  :lsbs lsbs
                                  :msbs msbs)
          1)))
    ((when (< (+ width (integer-length msbs.val))
              (sparseint$-leaf-bitlimit)))
     (mv
        (make-sparseint$-leaf :val (logapp width lsbs.val msbs.val))
        0)))
   (mv (make-sparseint$-concat :width width
                               :lsbs lsbs
                               :msbs msbs)
       1))))

Theorem: sparseint$-p-of-sparseint$-finalize-concat.concat

(defthm sparseint$-p-of-sparseint$-finalize-concat.concat
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (sparseint$-p concat))
 :rule-classes :rewrite)

Theorem: return-type-of-sparseint$-finalize-concat.height

(defthm return-type-of-sparseint$-finalize-concat.height
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (equal height (sparseint$-height concat)))
 :rule-classes :rewrite)

Theorem: sparseint$-finalize-concat-height-correctp

(defthm sparseint$-finalize-concat-height-correctp
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (implies (and (sparseint$-height-correctp lsbs)
                (sparseint$-height-correctp msbs)
                (within-1 (sparseint$-height lsbs)
                          (sparseint$-height msbs)))
           (sparseint$-height-correctp concat))))

Theorem: sparseint$-finalize-concat-correct

(defthm sparseint$-finalize-concat-correct
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (equal (sparseint$-val concat)
         (logapp (pos-fix width)
                 (sparseint$-val lsbs)
                 (sparseint$-val msbs)))))

Theorem: sparseint$-finalize-concat-height-possibilities

(defthm sparseint$-finalize-concat-height-possibilities
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (equal (sparseint$-height concat)
         (+ (if (sparseint$-mergeable-leaves-p width lsbs msbs)
                0
              1)
            (max (sparseint$-height lsbs)
                 (sparseint$-height msbs))))))

Theorem: sparseint$-finalize-concat-not-leaf-unless-merged

(defthm sparseint$-finalize-concat-not-leaf-unless-merged
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (implies (not (sparseint$-mergeable-leaves-p width lsbs msbs))
           (equal (sparseint$-kind concat)
                  :concat))))

Theorem: sparseint$-finalize-concat-leaf-when-merged

(defthm sparseint$-finalize-concat-leaf-when-merged
 (b*
  (((mv ?concat ?height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))
  (implies (sparseint$-mergeable-leaves-p width lsbs msbs)
           (equal (sparseint$-kind concat)
                  :leaf))))

Theorem: sparseint$-finalize-concat-of-pos-fix-width

(defthm sparseint$-finalize-concat-of-pos-fix-width
 (equal
    (sparseint$-finalize-concat (pos-fix width)
                                lsbs lsbs.height msbs msbs.height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))

Theorem: sparseint$-finalize-concat-pos-equiv-congruence-on-width

(defthm sparseint$-finalize-concat-pos-equiv-congruence-on-width
 (implies
  (pos-equiv width width-equiv)
  (equal
    (sparseint$-finalize-concat
         width lsbs lsbs.height msbs msbs.height)
    (sparseint$-finalize-concat width-equiv
                                lsbs lsbs.height msbs msbs.height)))
 :rule-classes :congruence)

Theorem: sparseint$-finalize-concat-of-sparseint$-fix-lsbs

(defthm sparseint$-finalize-concat-of-sparseint$-fix-lsbs
 (equal
    (sparseint$-finalize-concat width (sparseint$-fix lsbs)
                                lsbs.height msbs msbs.height)
    (sparseint$-finalize-concat width
                                lsbs lsbs.height msbs msbs.height)))

Theorem: sparseint$-finalize-concat-sparseint$-equiv-congruence-on-lsbs

(defthm
     sparseint$-finalize-concat-sparseint$-equiv-congruence-on-lsbs
 (implies
  (sparseint$-equiv lsbs lsbs-equiv)
  (equal (sparseint$-finalize-concat
              width lsbs lsbs.height msbs msbs.height)
         (sparseint$-finalize-concat width lsbs-equiv
                                     lsbs.height msbs msbs.height)))
 :rule-classes :congruence)

Theorem: sparseint$-finalize-concat-of-sparseint$-fix-msbs

(defthm sparseint$-finalize-concat-of-sparseint$-fix-msbs
 (equal
  (sparseint$-finalize-concat width
                              lsbs lsbs.height (sparseint$-fix msbs)
                              msbs.height)
  (sparseint$-finalize-concat width
                              lsbs lsbs.height msbs msbs.height)))

Theorem: sparseint$-finalize-concat-sparseint$-equiv-congruence-on-msbs

(defthm
     sparseint$-finalize-concat-sparseint$-equiv-congruence-on-msbs
 (implies
  (sparseint$-equiv msbs msbs-equiv)
  (equal
   (sparseint$-finalize-concat
        width lsbs lsbs.height msbs msbs.height)
   (sparseint$-finalize-concat width lsbs
                               lsbs.height msbs-equiv msbs.height)))
 :rule-classes :congruence)