		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-h

The elliptic curve cofactor.

Signature
(edwards-bls12-h) → h
Returns: h — Type (natp h).

This is the number that, when multiplied by the large subgroup order r, yields the full order of the elliptic curve group.

Definitions and Theorems

Function: edwards-bls12-h

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

Theorem: natp-of-edwards-bls12-h

(defthm natp-of-edwards-bls12-h
  (b* ((h (edwards-bls12-h))) (natp h))
  :rule-classes :rewrite)