		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-install-bit

Signature
(s32v-install-bit row bitnum val s32v) → new-s32v
Arguments: row — Guard (natp row).; bitnum — Guard (natp bitnum).; val — Guard (bitp val).

Definitions and Theorems

Function: s32v-install-bit

(defun s32v-install-bit (row bitnum val s32v)
 (declare (xargs :stobjs (s32v)))
 (declare (xargs :guard (and (natp row)
                             (natp bitnum)
                             (bitp val))))
 (declare (xargs :guard (and (< row (s32v-nrows s32v))
                             (< bitnum (* 32 (s32v-ncols s32v))))))
 (let ((__function__ 's32v-install-bit))
  (declare (ignorable __function__))
  (b* ((col (ash (lnfix bitnum) -5))
       (bitcol (logand (lnfix bitnum) 31))
       (prev-val (s32v-get2 row col s32v))
       (new-val (fast-logext 32 (install-bit bitcol val prev-val))))
    (s32v-set2 row col new-val s32v))))

Theorem: ncols-of-s32v-install-bit

(defthm ncols-of-s32v-install-bit
  (b* ((?new-s32v (s32v-install-bit row bitnum val s32v)))
    (equal (stobjs::2darr->ncols new-s32v)
           (stobjs::2darr->ncols s32v))))

Theorem: nrows-of-s32v-install-bit

(defthm nrows-of-s32v-install-bit
  (b* ((?new-s32v (s32v-install-bit row bitnum val s32v)))
    (implies (< (nfix row)
                (len (stobjs::2darr->rows s32v)))
             (equal (len (stobjs::2darr->rows new-s32v))
                    (len (stobjs::2darr->rows s32v))))))

Theorem: s32v-install-bit-of-nfix-row

(defthm s32v-install-bit-of-nfix-row
  (equal (s32v-install-bit (nfix row)
                           bitnum val s32v)
         (s32v-install-bit row bitnum val s32v)))

Theorem: s32v-install-bit-nat-equiv-congruence-on-row

(defthm s32v-install-bit-nat-equiv-congruence-on-row
  (implies (nat-equiv row row-equiv)
           (equal (s32v-install-bit row bitnum val s32v)
                  (s32v-install-bit row-equiv bitnum val s32v)))
  :rule-classes :congruence)

Theorem: s32v-install-bit-of-nfix-bitnum

(defthm s32v-install-bit-of-nfix-bitnum
  (equal (s32v-install-bit row (nfix bitnum)
                           val s32v)
         (s32v-install-bit row bitnum val s32v)))

Theorem: s32v-install-bit-nat-equiv-congruence-on-bitnum

(defthm s32v-install-bit-nat-equiv-congruence-on-bitnum
  (implies (nat-equiv bitnum bitnum-equiv)
           (equal (s32v-install-bit row bitnum val s32v)
                  (s32v-install-bit row bitnum-equiv val s32v)))
  :rule-classes :congruence)

Theorem: s32v-install-bit-of-bfix-val

(defthm s32v-install-bit-of-bfix-val
  (equal (s32v-install-bit row bitnum (bfix val)
                           s32v)
         (s32v-install-bit row bitnum val s32v)))

Theorem: s32v-install-bit-bit-equiv-congruence-on-val

(defthm s32v-install-bit-bit-equiv-congruence-on-val
  (implies (bit-equiv val val-equiv)
           (equal (s32v-install-bit row bitnum val s32v)
                  (s32v-install-bit row bitnum val-equiv s32v)))
  :rule-classes :congruence)