Logextu
Logical sign extension, unsigned version. (logextu final-size
ext-size i) "sign-extends" i with (logext ext-size i), then truncates
the result to final-size bits, creating an unsigned integer.
- Signature
(logextu final-size ext-size i) → nat
- Arguments
- final-size — Guard (and (integerp final-size) (<= 0 final-size)).
- ext-size — Guard (and (integerp ext-size) (< 0 ext-size)).
- i — Guard (integerp i).
- Returns
- nat — Type (natp nat).
Definitions and Theorems
Function: logextu$inline
(defun logextu$inline (final-size ext-size i)
(declare
(xargs :guard (and (and (integerp final-size)
(<= 0 final-size))
(and (integerp ext-size) (< 0 ext-size))
(integerp i))))
(let ((__function__ 'logextu))
(declare (ignorable __function__))
(loghead final-size (logext ext-size i))))
Theorem: logextu-type
(defthm logextu-type
(b* ((nat (logextu$inline final-size ext-size i)))
(natp nat))
:rule-classes :type-prescription)
Subtopics
- Ihs/logextu-lemmas
- Lemmas about logextu from the logops-lemmas book.
- Logextu-basics
