		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-add-salt

Signature
(s32v-add-salt col packed-vals packed-relevants state) → (mv new-packed-vals new-state)
Arguments: col — Guard (natp col).

Definitions and Theorems

Function: s32v-add-salt

(defun s32v-add-salt (col packed-vals packed-relevants state)
 (declare (xargs :stobjs (packed-vals packed-relevants state)))
 (declare (xargs :guard (natp col)))
 (declare
      (xargs :guard (and (<= (s32v-ncols packed-relevants)
                             (s32v-ncols packed-vals))
                         (<= (s32v-nrows packed-relevants)
                             (s32v-nrows packed-vals))
                         (<= col
                             (* 32 (s32v-ncols packed-relevants)))
                         (< 0 (s32v-nrows packed-relevants)))))
 (let ((__function__ 's32v-add-salt))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (* 32 (s32v-ncols packed-relevants))
                              (nfix col)))
                :exec (eql col
                           (* 32 (s32v-ncols packed-relevants)))))
     (mv packed-vals state))
    (nrelevant (s32v-bitcol-count-set 0 0 col packed-relevants))
    ((when (eql 0 nrelevant))
     (s32v-add-salt (+ 1 (lnfix col))
                    packed-vals packed-relevants state))
    ((mv which-relevant state)
     (random$ nrelevant state))
    (idx
        (s32v-bitcol-nth-set 0 which-relevant col packed-relevants))
    (prev-val (s32v-get-bit idx col packed-vals))
    (packed-vals (s32v-install-bit idx col (b-not prev-val)
                                   packed-vals)))
   (s32v-add-salt (+ 1 (lnfix col))
                  packed-vals packed-relevants state))))

Theorem: nrows-of-s32v-add-salt

(defthm nrows-of-s32v-add-salt
  (b* (((mv ?new-packed-vals ?new-state)
        (s32v-add-salt col
                       packed-vals packed-relevants state)))
    (implies (and (<= (s32v-nrows packed-relevants)
                      (s32v-nrows packed-vals))
                  (< 0 (s32v-nrows packed-relevants)))
             (equal (len (stobjs::2darr->rows new-packed-vals))
                    (len (stobjs::2darr->rows packed-vals))))))

Theorem: ncols-of-s32v-add-salt

(defthm ncols-of-s32v-add-salt
  (b* (((mv ?new-packed-vals ?new-state)
        (s32v-add-salt col
                       packed-vals packed-relevants state)))
    (equal (stobjs::2darr->ncols new-packed-vals)
           (stobjs::2darr->ncols packed-vals))))

Theorem: w-state-of-s32v-add-salt

(defthm w-state-of-s32v-add-salt
  (b* (((mv ?new-packed-vals ?new-state)
        (s32v-add-salt col
                       packed-vals packed-relevants state)))
    (equal (w new-state) (w state))))

Theorem: s32v-add-salt-of-nfix-col

(defthm s32v-add-salt-of-nfix-col
  (equal (s32v-add-salt (nfix col)
                        packed-vals packed-relevants state)
         (s32v-add-salt col
                        packed-vals packed-relevants state)))

Theorem: s32v-add-salt-nat-equiv-congruence-on-col

(defthm s32v-add-salt-nat-equiv-congruence-on-col
  (implies
       (nat-equiv col col-equiv)
       (equal (s32v-add-salt col packed-vals packed-relevants state)
              (s32v-add-salt col-equiv
                             packed-vals packed-relevants state)))
  :rule-classes :congruence)