		Search-engine friendly clone of the ACL2 documentation.

Bigmem-asymmetric

Xor-mem-region

Signature
(xor-mem-region n sum mem) → (mv * mem)
Arguments: mem — Guard (memp mem).

Definitions and Theorems

Function: xor-mem-region

(defun xor-mem-region (n sum mem)
  (declare (xargs :stobjs (mem)))
  (declare (type (unsigned-byte 60) n)
           (type (unsigned-byte 8) sum))
  (declare (xargs :guard (memp mem)))
  (let ((__function__ 'xor-mem-region))
    (declare (ignorable __function__))
    (let ((n (the (unsigned-byte 60) n))
          (sum (the (unsigned-byte 8) sum)))
      (if (mbe :logic (zp n) :exec (= n 0))
          (mv sum mem)
        (b* ((val (the (unsigned-byte 8)
                       (read-mem n mem)))
             (xor-sum (logxor val sum)))
          (xor-mem-region (the (unsigned-byte 60) (1- n))
                          (the (unsigned-byte 8) xor-sum)
                          mem))))))

Theorem: natp-car-xor-mem-region

(defthm natp-car-xor-mem-region
  (implies (and (natp n)
                (unsigned-byte-p 8 sum)
                (memp mem))
           (natp (car (xor-mem-region n sum mem))))
  :rule-classes :type-prescription)

Theorem: bytep-car-xor-mem-region

(defthm bytep-car-xor-mem-region
  (implies (and (natp n)
                (unsigned-byte-p 8 sum)
                (memp mem))
           (and (<= 0 (car (xor-mem-region n sum mem)))
                (< (car (xor-mem-region n sum mem))
                   256)))
  :rule-classes :linear)

Theorem: memp-cadr-xor-mem-region

(defthm memp-cadr-xor-mem-region
  (implies (and (natp n) (natp sum) (memp mem))
           (memp (cadr (xor-mem-region n sum mem)))))