		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-d

The Edwards-BLS12 coefficient d

Signature
(edwards-bls12-d) → d
Returns: d — Type (fep d (edwards-bls12-q)).

We show that this coefficient is not a square using Euler's criterion. We use the fast modular exponentiation operation from the arithmetic-3 library to calculate the modular exponentiation of the coefficient, which must be different from 1 in order for the criterion to apply.

Definitions and Theorems

Function: edwards-bls12-d

(defun edwards-bls12-d nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-d))
    (declare (ignorable acl2::__function__))
    3021))

Theorem: return-type-of-edwards-bls12-d

(defthm return-type-of-edwards-bls12-d
  (b* ((d (edwards-bls12-d)))
    (fep d (edwards-bls12-q)))
  :rule-classes :rewrite)

Theorem: edwards-bls12-d-not-zero

(defthm edwards-bls12-d-not-zero
  (not (equal (edwards-bls12-d) 0)))

Theorem: edwards-bls12-d-not-equal-to-a

(defthm edwards-bls12-d-not-equal-to-a
  (not (equal (edwards-bls12-d)
              (edwards-bls12-a))))

Theorem: not-pfield-squarep-of-edwards-bls12-d

(defthm not-pfield-squarep-of-edwards-bls12-d
  (not (pfield-squarep (edwards-bls12-d)
                       (edwards-bls12-q))))