|
|
|---|
|
|
|
|---|
Recognizer of the subgroup of a curve.
The subgroup consists of points of the curve that additionally yield the neutral point when multiplied by the scalar prime.
This should be the same as ecurve::edwards-bls12-r-pointp for Edwards BLS12, but that definition uses the non-executable function ecurve::twisted-edwards-point-orderp. We plan to extend the ACL2 elliptic curve library with executable versions of functions such as this, linked by theorems to the non-executable versions; but for now we just redefine the function here in executable form. Note that we just check that multiplying the point by the scalar prime yields the neutral point, without checking that multiplying the point by a smaller positive integer does not yield the neutral point (which is the complete definition of order): for this kind of curve group, the check performed here should suffice, i.e. it should imply the additional one; we plan to formally prove all of this.
Function:
(defun curve-subgroupp (x curve) (declare (xargs :guard (curvep curve))) (let ((__function__ 'curve-subgroupp)) (declare (ignorable __function__)) (and (ecurve::edwards-bls12-pointp x) (equal (ecurve::edwards-bls12-mul-fast (curve-scalar-prime curve) x) (ecurve::twisted-edwards-zero)))))
Theorem:
(defthm booleanp-of-curve-subgroupp (b* ((yes/no (curve-subgroupp x curve))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm curve-subgroupp-of-curve-fix-curve (equal (curve-subgroupp x (curve-fix curve)) (curve-subgroupp x curve)))
Theorem:
(defthm curve-subgroupp-curve-equiv-congruence-on-curve (implies (curve-equiv curve curve-equiv) (equal (curve-subgroupp x curve) (curve-subgroupp x curve-equiv))) :rule-classes :congruence)