		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Op-mul

Leo multiplication operation.

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

Definitions and Theorems

Function: op-mul

(defun op-mul (left right curve)
  (declare (xargs :guard (and (valuep left)
                              (valuep right)
                              (curvep curve))))
  (let ((__function__ 'op-mul))
    (declare (ignorable __function__))
    (cond ((and (int-valuep left)
                (int-valuep right))
           (op-int-mul left right))
          ((and (value-case left :field)
                (value-case right :field))
           (op-field-mul left right curve))
          ((and (value-case left :scalar)
                (value-case right :group))
           (op-group-mul left right curve))
          ((and (value-case left :group)
                (value-case right :scalar))
           (op-group-mul right left curve))
          (t (reserrf (list :op-mul (value-fix left)
                            (value-fix right)))))))

Theorem: value-resultp-of-op-mul

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