		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vec-from-bitlist

Signature
(4vec-from-bitlist upper-len lower-len bits) → (mv vec rest)
Arguments: upper-len — Guard (natp upper-len).; lower-len — Guard (natp lower-len).; bits — Guard (true-listp bits).
Returns: vec — Type (4vec-p vec).; rest — Type (true-listp rest), given (true-listp bits).

Definitions and Theorems

Function: 4vec-from-bitlist

(defun 4vec-from-bitlist (upper-len lower-len bits)
  (declare (xargs :guard (and (natp upper-len)
                              (natp lower-len)
                              (true-listp bits))))
  (let ((__function__ '4vec-from-bitlist))
    (declare (ignorable __function__))
    (b* ((upper (v2i-first-n upper-len bits))
         (rest (nthcdr upper-len bits))
         (lower (v2i-first-n lower-len rest))
         (rest (nthcdr lower-len rest)))
      (mv (4vec upper lower) rest))))

Theorem: 4vec-p-of-4vec-from-bitlist.vec

(defthm 4vec-p-of-4vec-from-bitlist.vec
  (b* (((mv ?vec common-lisp::?rest)
        (4vec-from-bitlist upper-len lower-len bits)))
    (4vec-p vec))
  :rule-classes :rewrite)

Theorem: true-listp-of-4vec-from-bitlist.rest

(defthm true-listp-of-4vec-from-bitlist.rest
  (implies (true-listp bits)
           (b* (((mv ?vec common-lisp::?rest)
                 (4vec-from-bitlist upper-len lower-len bits)))
             (true-listp rest)))
  :rule-classes :type-prescription)

Theorem: 4vec-from-bitlist-correct

(defthm 4vec-from-bitlist-correct
 (b* (((a4vec x) x))
  (equal
   (4vec-from-bitlist (len x.upper)
                      (len x.lower)
                      (append (aig-eval-list (a4vec->aiglist x) env)
                              rest))
   (mv (a4vec-eval x env) rest))))

Theorem: 4vec-from-bitlist-rest-bits

(defthm 4vec-from-bitlist-rest-bits
  (b* (((mv ?vec common-lisp::?rest)
        (4vec-from-bitlist upper-len lower-len bits)))
    (equal rest
           (nthcdr (+ (nfix upper-len) (nfix lower-len))
                   bits))))

Theorem: 4vec-from-bitlist-of-nfix-upper-len

(defthm 4vec-from-bitlist-of-nfix-upper-len
  (equal (4vec-from-bitlist (nfix upper-len)
                            lower-len bits)
         (4vec-from-bitlist upper-len lower-len bits)))

Theorem: 4vec-from-bitlist-nat-equiv-congruence-on-upper-len

(defthm 4vec-from-bitlist-nat-equiv-congruence-on-upper-len
  (implies
       (nat-equiv upper-len upper-len-equiv)
       (equal (4vec-from-bitlist upper-len lower-len bits)
              (4vec-from-bitlist upper-len-equiv lower-len bits)))
  :rule-classes :congruence)

Theorem: 4vec-from-bitlist-of-nfix-lower-len

(defthm 4vec-from-bitlist-of-nfix-lower-len
  (equal (4vec-from-bitlist upper-len (nfix lower-len)
                            bits)
         (4vec-from-bitlist upper-len lower-len bits)))

Theorem: 4vec-from-bitlist-nat-equiv-congruence-on-lower-len

(defthm 4vec-from-bitlist-nat-equiv-congruence-on-lower-len
  (implies
       (nat-equiv lower-len lower-len-equiv)
       (equal (4vec-from-bitlist upper-len lower-len bits)
              (4vec-from-bitlist upper-len lower-len-equiv bits)))
  :rule-classes :congruence)