		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-generator

Generator point of the subgroup.

Signature
(curve-generator curve) → gen
Arguments: curve — Guard (curvep curve).
Returns: gen — Type (curve-subgroupp gen curve).

Even though any non-zero element of the subgroup is a generator of the subgroup, here we pick a specific one, which presumably is needed to make certain calculations unambiguous and deterministic.

Definitions and Theorems

Function: curve-generator

(defun curve-generator (curve)
  (declare (xargs :guard (curvep curve)))
  (declare (ignore curve))
  (let ((__function__ 'curve-generator))
    (declare (ignorable __function__))
    (edwards-bls12-generator)))

Theorem: return-type-of-curve-generator

(defthm return-type-of-curve-generator
  (b* ((gen (curve-generator curve)))
    (curve-subgroupp gen curve))
  :rule-classes :rewrite)

Theorem: curve-generator-of-curve-fix-curve

(defthm curve-generator-of-curve-fix-curve
  (equal (curve-generator (curve-fix curve))
         (curve-generator curve)))

Theorem: curve-generator-curve-equiv-congruence-on-curve

(defthm curve-generator-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (curve-generator curve)
                  (curve-generator curve-equiv)))
  :rule-classes :congruence)