		Search-engine friendly clone of the ACL2 documentation.

Group-arithmetic-operations

Op-group-mul

Leo group scalar multiplication operation.

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

Here one operand must be a group value and the other operand must be an scalar value. Thus, the inputs to this function are a scalar field value (either the left or the right operand) and a group element value (either the right or the left operand).

Definitions and Theorems

Function: op-group-mul

(defun op-group-mul (left/right right/left curve)
  (declare (xargs :guard (and (valuep left/right)
                              (valuep right/left)
                              (curvep curve))))
  (declare (xargs :guard (and (value-case left/right :scalar)
                              (value-case right/left :group))))
  (let ((__function__ 'op-group-mul))
    (declare (ignorable __function__))
    (b* ((k (value-scalar->get left/right))
         (x (value-group->get right/left))
         ((unless (< k (curve-scalar-prime curve)))
          (reserrf (list :input-not-in-scalar-field k)))
         ((unless (curve-subgroupp x curve))
          (reserrf (list :input-not-in-subgroup x)))
         ((mv okp k*x)
          (curve-subgroup-mul k x curve))
         ((unless okp)
          (reserrf (list :output-not-in-subgroup k*x))))
      (value-group k*x))))

Theorem: value-resultp-of-op-group-mul

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

Theorem: op-group-mul-of-value-fix-left/right

(defthm op-group-mul-of-value-fix-left/right
  (equal (op-group-mul (value-fix left/right)
                       right/left curve)
         (op-group-mul left/right right/left curve)))

Theorem: op-group-mul-value-equiv-congruence-on-left/right

(defthm op-group-mul-value-equiv-congruence-on-left/right
  (implies (value-equiv left/right left/right-equiv)
           (equal (op-group-mul left/right right/left curve)
                  (op-group-mul left/right-equiv right/left curve)))
  :rule-classes :congruence)

Theorem: op-group-mul-of-value-fix-right/left

(defthm op-group-mul-of-value-fix-right/left
  (equal (op-group-mul left/right (value-fix right/left)
                       curve)
         (op-group-mul left/right right/left curve)))

Theorem: op-group-mul-value-equiv-congruence-on-right/left

(defthm op-group-mul-value-equiv-congruence-on-right/left
  (implies (value-equiv right/left right/left-equiv)
           (equal (op-group-mul left/right right/left curve)
                  (op-group-mul left/right right/left-equiv curve)))
  :rule-classes :congruence)

Theorem: op-group-mul-of-curve-fix-curve

(defthm op-group-mul-of-curve-fix-curve
  (equal (op-group-mul left/right right/left (curve-fix curve))
         (op-group-mul left/right right/left curve)))

Theorem: op-group-mul-curve-equiv-congruence-on-curve

(defthm op-group-mul-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (op-group-mul left/right right/left curve)
                  (op-group-mul left/right right/left curve-equiv)))
  :rule-classes :congruence)