The Edwards-BLS12 base field prime
(edwards-bls12-q) → 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, which is defined in our cryptograhic library.
Function:
(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:
(defthm primep-of-edwards-bls12-q (b* ((q (edwards-bls12-q))) (dm::primep q)) :rule-classes :rewrite)
Theorem:
(defthm edwards-bls12-q-not-two (not (equal (edwards-bls12-q) 2)))