Ashu
Arithmetic shift, unsigned version.
- Signature
(ashu 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).
ashu is a fixed-width version of ash. The integer
i is first coerced to a size-bit signed integer by sign-extension,
then shifted with ash, and finally truncated back to a size-bit
unsigned integer.
See also lshu for a logical (instead of arithmetic) shift.
Definitions and Theorems
Function: ashu
(defun ashu (size i cnt)
(declare (xargs :guard (and (and (integerp size) (< 0 size))
(integerp i)
(integerp cnt))))
(let ((__function__ 'ashu))
(declare (ignorable __function__))
(loghead size (ash (logext size i) cnt))))
Theorem: ashu-type
(defthm ashu-type
(b* ((nat (ashu size i cnt)))
(natp nat))
:rule-classes :type-prescription)
Subtopics
- Ashu-basics
