		Search-engine friendly clone of the ACL2 documentation.

Shift-operations

Op-shl-wrapped

Leo wrapped left shift operation.

Signature
(op-shl-wrapped left right) → result
Arguments: left — Guard (valuep left).; right — Guard (valuep right).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-shl-wrapped

(defun op-shl-wrapped (left right)
 (declare (xargs :guard (and (valuep left) (valuep right))))
 (let ((__function__ 'op-shl-wrapped))
  (declare (ignorable __function__))
  (b*
   ((err (list :op-shl-wrapped (value-fix left)
               (value-fix right)))
    ((unless (int-valuep left))
     (reserrf err))
    ((unless (int-valuep right))
     (reserrf err))
    (left-operand-numbits (int-value-numbits left))
    (left-operand-int (int-value-to-int left))
    ((unless (member-eq (value-kind right)
                        '(:u8 :u16 :u32)))
     (reserrf err))
    (right-operand-int (int-value-to-int right))
    ((unless (natp right-operand-int))
     (reserrf err))
    (right-operand-int (mod right-operand-int left-operand-numbits))
    (shifted-value (* left-operand-int
                      (expt 2 right-operand-int))))
   (cond ((value-case left :u8)
          (value-u8 (loghead 8 shifted-value)))
         ((value-case left :u16)
          (value-u16 (loghead 16 shifted-value)))
         ((value-case left :u32)
          (value-u32 (loghead 32 shifted-value)))
         ((value-case left :u64)
          (value-u64 (loghead 64 shifted-value)))
         ((value-case left :u128)
          (value-u128 (loghead 128 shifted-value)))
         ((value-case left :i8)
          (value-i8 (logext 8 shifted-value)))
         ((value-case left :i16)
          (value-i16 (logext 16 shifted-value)))
         ((value-case left :i32)
          (value-i32 (logext 32 shifted-value)))
         ((value-case left :i64)
          (value-i64 (logext 64 shifted-value)))
         ((value-case left :i128)
          (value-i128 (logext 128 shifted-value)))
         (t (reserrf err))))))

Theorem: value-resultp-of-op-shl-wrapped

(defthm value-resultp-of-op-shl-wrapped
  (b* ((result (op-shl-wrapped left right)))
    (value-resultp result))
  :rule-classes :rewrite)