		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Shl-integer-values

Apply << to integer values [C:6.5.7/3] [C:6.5.7/4].

Signature
(shl-integer-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (value-resultp resval).

By the time we reach this ACL2 function, the values have already been subjected to the arithmetic promotions. We put this condition in the guard.

The type of the result is the same as the left operand [C:6.5.7/3]. We use result-integer-value to return the resulting value, or an error, as documented in that function. The left operand must be non-negative, otherwise it is an error. The right operand must be non-negative and below the number of bits of the left operand, otherwise it is an error.

Definitions and Theorems

Function: shl-integer-values

(defun shl-integer-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (declare (xargs :guard (and (value-integerp val1)
                              (value-integerp val2)
                              (value-promoted-arithmeticp val1)
                              (value-promoted-arithmeticp val2))))
  (let ((__function__ 'shl-integer-values))
    (declare (ignorable __function__))
    (b* ((mathint1 (value-integer->get val1))
         (mathint2 (value-integer->get val2))
         (type1 (type-of-value val1))
         ((unless (<= 0 mathint1))
          (error (list :undefined-shl (value-fix val1)
                       (value-fix val2))))
         ((unless (integer-range-p 0 (integer-type-bits type1)
                                   mathint2))
          (error (list :undefined-shl (value-fix val1)
                       (value-fix val2))))
         (result (* mathint1 (expt 2 mathint2)))
         (resval (result-integer-value result type1))
         ((when (errorp resval))
          (error (list :undefined-shl (value-fix val1)
                       (value-fix val2)))))
      resval)))

Theorem: value-resultp-of-shl-integer-values

(defthm value-resultp-of-shl-integer-values
  (b* ((resval (shl-integer-values val1 val2)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: shl-integer-values-of-value-fix-val1

(defthm shl-integer-values-of-value-fix-val1
  (equal (shl-integer-values (value-fix val1)
                             val2)
         (shl-integer-values val1 val2)))

Theorem: shl-integer-values-value-equiv-congruence-on-val1

(defthm shl-integer-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (shl-integer-values val1 val2)
                  (shl-integer-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: shl-integer-values-of-value-fix-val2

(defthm shl-integer-values-of-value-fix-val2
  (equal (shl-integer-values val1 (value-fix val2))
         (shl-integer-values val1 val2)))

Theorem: shl-integer-values-value-equiv-congruence-on-val2

(defthm shl-integer-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (shl-integer-values val1 val2)
                  (shl-integer-values val1 val2-equiv)))
  :rule-classes :congruence)