		Search-engine friendly clone of the ACL2 documentation.

Shift-operations

Op-shr-wrapped

Leo wrapped right shift operation.

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

Definitions and Theorems

Function: op-shr-wrapped

(defun op-shr-wrapped (left right)
 (declare (xargs :guard (and (valuep left) (valuep right))))
 (let ((__function__ 'op-shr-wrapped))
  (declare (ignorable __function__))
  (b*
   ((err (list :op-shr-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 (floor left-operand-int
                          (expt 2 right-operand-int))))
   (make-int-value (value-kind left)
                   shifted-value))))

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

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