		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-curve

The Edwards-BLS12 curve

Signature
(edwards-bls12-curve) → curve
Returns: curve — Type (twisted-edwards-curvep curve).

We show that it is complete.

Definitions and Theorems

Function: edwards-bls12-curve

(defun edwards-bls12-curve nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-curve))
    (declare (ignorable acl2::__function__))
    (make-twisted-edwards-curve :p (edwards-bls12-q)
                                :a (edwards-bls12-a)
                                :d (edwards-bls12-d))))

Theorem: twisted-edwards-curvep-of-edwards-bls12-curve

(defthm twisted-edwards-curvep-of-edwards-bls12-curve
  (b* ((curve (edwards-bls12-curve)))
    (twisted-edwards-curvep curve))
  :rule-classes :rewrite)

Theorem: twisted-edwards-curve-completep-of-edwards-bls12-curve

(defthm twisted-edwards-curve-completep-of-edwards-bls12-curve
  (twisted-edwards-curve-completep (edwards-bls12-curve)))