		Search-engine friendly clone of the ACL2 documentation.

Field-arithmetic-operations

Op-field-pow

Leo field exponentiation operation.

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

Here the left operand must be a field element value, while the right operand must be an integer. If the exponent is non-negative, the result is always well defined. If the exponent is negative, the base must not be zero; the result is the inverse of the positive power.

Definitions and Theorems

Function: op-field-pow

(defun op-field-pow (left right curve)
  (declare (xargs :guard (and (valuep left)
                              (valuep right)
                              (curvep curve))))
  (declare (xargs :guard (and (value-case left :field)
                              (value-case right :field))))
  (let ((__function__ 'op-field-pow))
    (declare (ignorable __function__))
    (b* ((err (list :op-field-pow (value-fix left)
                    (value-fix right)))
         (p (curve-base-prime curve))
         (x (value-field->get left))
         ((unless (pfield::fep x p))
          (reserrf err))
         (y (value-field->get right))
         ((unless (pfield::fep y p))
          (reserrf err)))
      (value-field (pfield::pow x y p)))))

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

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

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

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

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

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

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

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

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

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