Lshu
Logical shift, unsigned version.
- Signature
(lshu size i cnt) → nat
- Arguments
- size — Guard (and (integerp size) (<= 0 size)).
- i — Guard (integerp i).
- cnt — Guard (integerp cnt).
- Returns
- nat — Type (natp nat).
lshu is a fixed-width logical shift. It shifts i
by cnt bits by first coercing i to an unsigned integer of size
bits, performing the shift, and coercing the result to an size-bit
unsigned integer.
For cnt >= 0, (lshu size i cnt) = (ashu size i cnt).
This is a model of a size-bit logical shift register.
Definitions and Theorems
Function: lshu
(defun lshu (size i cnt)
(declare (xargs :guard (and (and (integerp size) (<= 0 size))
(integerp i)
(integerp cnt))))
(let ((__function__ 'lshu))
(declare (ignorable __function__))
(loghead size (ash (loghead size i) cnt))))
Theorem: lshu-type
(defthm lshu-type
(b* ((nat (lshu size i cnt)))
(natp nat))
:rule-classes :type-prescription)
Subtopics
- Lshu-basics
