		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-q

The Edwards-BLS12 base field prime F_q.

Signature
(edwards-bls12-q) → q
Returns: q — Type (dm::primep q).

This defines the prime field over which Edwards-BLS12 is defined.

It is the same as the scalar field of the BLS12-377 elliptic curve. See bls12-377-scalar-field-prime for the exact value. The reason this number is called q here but r in the BLS12-377 domain parameters, is because the letter is relative to the curve. The Edwards-BLS12 curve's base field prime (here q) is equal to the BLS12-377 curve's scalar field prime (there r).

Definitions and Theorems

Function: edwards-bls12-q

(defun edwards-bls12-q nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-q))
    (declare (ignorable acl2::__function__))
    (bls12-377-scalar-field-prime)))

Theorem: primep-of-edwards-bls12-q

(defthm primep-of-edwards-bls12-q
  (b* ((q (edwards-bls12-q)))
    (dm::primep q))
  :rule-classes :rewrite)

Theorem: edwards-bls12-q-not-two

(defthm edwards-bls12-q-not-two
  (not (equal (edwards-bls12-q) 2)))