		Search-engine friendly clone of the ACL2 documentation.

Integer-arithmetic-operations

Op-int-pow

Leo integer exponentiation operation.

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

Definitions and Theorems

Function: op-int-pow

(defun op-int-pow (left right)
  (declare (xargs :guard (and (int-valuep left)
                              (int-valuep right))))
  (let ((__function__ 'op-int-pow))
    (declare (ignorable __function__))
    (b* ((err (reserrf (list :op-int-pow (value-fix left)
                             (value-fix right))))
         ((unless (member-eq (value-kind right)
                             '(:u8 :u16 :u32)))
          err)
         (left-int (int-value-to-int left))
         (right-int (int-value-to-int right))
         (res (expt left-int right-int)))
      (cond ((value-case left :u8)
             (if (ubyte8p res) (value-u8 res) err))
            ((value-case left :u16)
             (if (ubyte16p res) (value-u16 res) err))
            ((value-case left :u32)
             (if (ubyte32p res) (value-u32 res) err))
            ((value-case left :u64)
             (if (ubyte64p res) (value-u64 res) err))
            ((value-case left :u128)
             (if (ubyte128p res)
                 (value-u128 res)
               err))
            ((value-case left :i8)
             (if (sbyte8p res) (value-i8 res) err))
            ((value-case left :i16)
             (if (sbyte16p res) (value-i16 res) err))
            ((value-case left :i32)
             (if (sbyte32p res) (value-i32 res) err))
            ((value-case left :i64)
             (if (sbyte64p res) (value-i64 res) err))
            ((value-case left :i128)
             (if (sbyte128p res)
                 (value-i128 res)
               err))
            (t (reserrf (impossible)))))))

Theorem: value-resultp-of-op-int-pow

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

Theorem: op-int-pow-of-value-fix-left

(defthm op-int-pow-of-value-fix-left
  (equal (op-int-pow (value-fix left) right)
         (op-int-pow left right)))

Theorem: op-int-pow-value-equiv-congruence-on-left

(defthm op-int-pow-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-int-pow left right)
                  (op-int-pow left-equiv right)))
  :rule-classes :congruence)

Theorem: op-int-pow-of-value-fix-right

(defthm op-int-pow-of-value-fix-right
  (equal (op-int-pow left (value-fix right))
         (op-int-pow left right)))

Theorem: op-int-pow-value-equiv-congruence-on-right

(defthm op-int-pow-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-int-pow left right)
                  (op-int-pow left right-equiv)))
  :rule-classes :congruence)