		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-mask-check

Signature
(a4vec-mask-check mask idx vec upperp) → already-maskedp
Arguments: mask — Guard (4vmask-p mask).; idx — Guard (natp idx).; vec — aig list.
Guard (true-listp vec).; upperp — Guard (booleanp upperp).
Returns: already-maskedp — Type (booleanp already-maskedp).

Definitions and Theorems

Function: a4vec-mask-check

(defun a4vec-mask-check (mask idx vec upperp)
  (declare (xargs :guard (and (4vmask-p mask)
                              (natp idx)
                              (true-listp vec)
                              (booleanp upperp))))
  (let ((__function__ 'a4vec-mask-check))
    (declare (ignorable __function__))
    (b* ((idx (lnfix idx))
         (mask (4vmask-fix mask))
         ((mv first rest endp)
          (gl::first/rest/end vec))
         ((when endp)
          (or (mbe :logic (equal (logtail idx (sparseint-val mask))
                                 -1)
                   :exec (and (<= (sparseint-length mask) idx)
                              (eql 1 (sparseint-bit idx mask))))
              (equal first
                     (mbe :logic (bool-fix upperp)
                          :exec upperp)))))
      (and (or (eql 1 (sparseint-bit idx (4vmask-fix mask)))
               (equal first
                      (mbe :logic (bool-fix upperp)
                           :exec upperp)))
           (a4vec-mask-check mask (1+ (lnfix idx))
                             rest upperp)))))

Theorem: booleanp-of-a4vec-mask-check

(defthm booleanp-of-a4vec-mask-check
  (b* ((already-maskedp (a4vec-mask-check mask idx vec upperp)))
    (booleanp already-maskedp))
  :rule-classes :rewrite)

Theorem: a4vec-mask-check-correct

(defthm a4vec-mask-check-correct
 (and
  (implies (a4vec-mask-check mask 0 vec t)
           (equal (logior (lognot (sparseint-val (4vmask-fix mask)))
                          (aig-list->s vec env))
                  (aig-list->s vec env)))
  (implies (a4vec-mask-check mask 0 vec nil)
           (equal (logand (sparseint-val (4vmask-fix mask))
                          (aig-list->s vec env))
                  (aig-list->s vec env)))))

Theorem: a4vec-mask-check-of-4vmask-fix-mask

(defthm a4vec-mask-check-of-4vmask-fix-mask
  (equal (a4vec-mask-check (4vmask-fix mask)
                           idx vec upperp)
         (a4vec-mask-check mask idx vec upperp)))

Theorem: a4vec-mask-check-4vmask-equiv-congruence-on-mask

(defthm a4vec-mask-check-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (a4vec-mask-check mask idx vec upperp)
                  (a4vec-mask-check mask-equiv idx vec upperp)))
  :rule-classes :congruence)

Theorem: a4vec-mask-check-of-nfix-idx

(defthm a4vec-mask-check-of-nfix-idx
  (equal (a4vec-mask-check mask (nfix idx)
                           vec upperp)
         (a4vec-mask-check mask idx vec upperp)))

Theorem: a4vec-mask-check-nat-equiv-congruence-on-idx

(defthm a4vec-mask-check-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (a4vec-mask-check mask idx vec upperp)
                  (a4vec-mask-check mask idx-equiv vec upperp)))
  :rule-classes :congruence)

Theorem: a4vec-mask-check-of-list-fix-vec

(defthm a4vec-mask-check-of-list-fix-vec
  (equal (a4vec-mask-check mask idx (list-fix vec)
                           upperp)
         (a4vec-mask-check mask idx vec upperp)))

Theorem: a4vec-mask-check-list-equiv-congruence-on-vec

(defthm a4vec-mask-check-list-equiv-congruence-on-vec
  (implies (list-equiv vec vec-equiv)
           (equal (a4vec-mask-check mask idx vec upperp)
                  (a4vec-mask-check mask idx vec-equiv upperp)))
  :rule-classes :congruence)

Theorem: a4vec-mask-check-of-bool-fix-upperp

(defthm a4vec-mask-check-of-bool-fix-upperp
  (equal (a4vec-mask-check mask idx vec (bool-fix upperp))
         (a4vec-mask-check mask idx vec upperp)))

Theorem: a4vec-mask-check-iff-congruence-on-upperp

(defthm a4vec-mask-check-iff-congruence-on-upperp
  (implies (iff upperp upperp-equiv)
           (equal (a4vec-mask-check mask idx vec upperp)
                  (a4vec-mask-check mask idx vec upperp-equiv)))
  :rule-classes :congruence)