		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-scalar-prime

Scalar field prime of a curve.

Signature
(curve-scalar-prime curve) → prime
Arguments: curve — Guard (curvep curve).
Returns: prime — Type (primep prime).

Definitions and Theorems

Function: curve-scalar-prime

(defun curve-scalar-prime (curve)
  (declare (xargs :guard (curvep curve)))
  (declare (ignore curve))
  (let ((__function__ 'curve-scalar-prime))
    (declare (ignorable __function__))
    (ecurve::edwards-bls12-r)))

Theorem: primep-of-curve-scalar-prime

(defthm primep-of-curve-scalar-prime
  (b* ((prime (curve-scalar-prime curve)))
    (primep prime))
  :rule-classes :rewrite)

Theorem: curve-scalar-prime-of-curve-fix-curve

(defthm curve-scalar-prime-of-curve-fix-curve
  (equal (curve-scalar-prime (curve-fix curve))
         (curve-scalar-prime curve)))

Theorem: curve-scalar-prime-curve-equiv-congruence-on-curve

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