		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-const-concat-args

Signature
(svex-const-concat-args x) → (mv width lsbs msbs)
Arguments: x — Guard (svex-p x).
Returns: width — Type (4vec-p width).; lsbs — Type (svex-p lsbs).; msbs — Type (svex-p msbs).

Definitions and Theorems

Function: svex-const-concat-args

(defun svex-const-concat-args (x)
  (declare (xargs :guard (svex-p x)))
  (declare (xargs :guard (svex-is-const-concat x)))
  (let ((__function__ 'svex-const-concat-args))
    (declare (ignorable __function__))
    (b* (((svex-call x)))
      (mv (svex-quote->val (mbe :logic (svex-fix (nth 0 x.args))
                                :exec (first x.args)))
          (mbe :logic (svex-fix (nth 1 x.args))
               :exec (second x.args))
          (mbe :logic (svex-fix (nth 2 x.args))
               :exec (third x.args))))))

Theorem: 4vec-p-of-svex-const-concat-args.width

(defthm 4vec-p-of-svex-const-concat-args.width
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (4vec-p width))
  :rule-classes :rewrite)

Theorem: svex-p-of-svex-const-concat-args.lsbs

(defthm svex-p-of-svex-const-concat-args.lsbs
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (svex-p lsbs))
  :rule-classes :rewrite)

Theorem: svex-p-of-svex-const-concat-args.msbs

(defthm svex-p-of-svex-const-concat-args.msbs
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (svex-p msbs))
  :rule-classes :rewrite)

Theorem: svex-const-concat-args-correct-rw

(defthm svex-const-concat-args-correct-rw
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (implies (svex-is-const-concat x)
             (equal (svex-eval x env)
                    (4vec-concat width (svex-eval lsbs env)
                                 (svex-eval msbs env))))))

Theorem: svex-count-of-svex-const-concat-args-lsbs

(defthm svex-count-of-svex-const-concat-args-lsbs
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (implies (svex-is-const-concat x)
             (< (svex-count lsbs) (svex-count x))))
  :rule-classes :linear)

Theorem: svex-count-of-svex-const-concat-args-msbs

(defthm svex-count-of-svex-const-concat-args-msbs
  (b* (((mv ?width ?lsbs ?msbs)
        (svex-const-concat-args x)))
    (implies (svex-is-const-concat x)
             (< (svex-count msbs) (svex-count x))))
  :rule-classes :linear)

Theorem: svex-const-concat-args-of-svex-fix-x

(defthm svex-const-concat-args-of-svex-fix-x
  (equal (svex-const-concat-args (svex-fix x))
         (svex-const-concat-args x)))

Theorem: svex-const-concat-args-svex-equiv-congruence-on-x

(defthm svex-const-concat-args-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-const-concat-args x)
                  (svex-const-concat-args x-equiv)))
  :rule-classes :congruence)