		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-subgroup-mul

Scalar multiplication in the subgroup.

Signature
(curve-subgroup-mul k x curve) → (mv okp k*x)
Arguments: k — Guard (natp k).; x — Guard (curve-subgroupp x curve).; curve — Guard (curvep curve).
Returns: okp — Type (booleanp okp).; k*x — Type (curve-subgroupp k*x curve).

We limit the scalar to the in the scalar field, although there is no need to do that from the point of view of the operation being well-defined. We expect that this will always be the case though.

We use the same two-result approach as for addition; see curve-subgroup-add.

Definitions and Theorems

Function: curve-subgroup-mul

(defun curve-subgroup-mul (k x curve)
  (declare (xargs :guard (and (natp k)
                              (curvep curve)
                              (curve-subgroupp x curve))))
  (declare (xargs :guard (< k (curve-scalar-prime curve))))
  (let ((__function__ 'curve-subgroup-mul))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic
                 (if (curve-subgroupp x curve)
                     x
                   (curve-zero curve))
                 :exec x))
         (k*x (ecurve::edwards-bls12-mul-fast (nfix k)
                                              x)))
      (if (curve-subgroupp k*x curve)
          (mv t k*x)
        (mv nil (curve-zero curve))))))

Theorem: booleanp-of-curve-subgroup-mul.okp

(defthm booleanp-of-curve-subgroup-mul.okp
  (b* (((mv ?okp ?k*x)
        (curve-subgroup-mul k x curve)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: return-type-of-curve-subgroup-mul.k*x

(defthm return-type-of-curve-subgroup-mul.k*x
  (b* (((mv ?okp ?k*x)
        (curve-subgroup-mul k x curve)))
    (curve-subgroupp k*x curve))
  :rule-classes :rewrite)

Theorem: pointp-of-curve-subgroup-mul.k*x

(defthm pointp-of-curve-subgroup-mul.k*x
  (b* (((mv ?okp ?k*x)
        (curve-subgroup-mul k x curve)))
    (pointp k*x))
  :rule-classes :rewrite)

Theorem: curve-subgroup-mul-of-nfix-k

(defthm curve-subgroup-mul-of-nfix-k
  (equal (curve-subgroup-mul (nfix k) x curve)
         (curve-subgroup-mul k x curve)))

Theorem: curve-subgroup-mul-nat-equiv-congruence-on-k

(defthm curve-subgroup-mul-nat-equiv-congruence-on-k
  (implies (acl2::nat-equiv k k-equiv)
           (equal (curve-subgroup-mul k x curve)
                  (curve-subgroup-mul k-equiv x curve)))
  :rule-classes :congruence)

Theorem: curve-subgroup-mul-of-curve-fix-curve

(defthm curve-subgroup-mul-of-curve-fix-curve
  (equal (curve-subgroup-mul k x (curve-fix curve))
         (curve-subgroup-mul k x curve)))

Theorem: curve-subgroup-mul-curve-equiv-congruence-on-curve

(defthm curve-subgroup-mul-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (curve-subgroup-mul k x curve)
                  (curve-subgroup-mul k x curve-equiv)))
  :rule-classes :congruence)