		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Edwards-bls12-generator

The point on the edwards-bls12 curve that is used as a generator point.

Signature
(edwards-bls12-generator) → point
Returns: point — Type (ecurve::edwards-bls12-pointp point).

This generator point is used by Leo to define a mapping from integers modulo the group order to points on the edwards-bls12 elliptic curve.

In some sense the generator point is arbitrary, but once chosen, it cannot be changed without changing the semantics of Leo operations on group values.

The generator point is returned by the literal `1group' in the Leo language.

For more information on the edwards bls12 curve, see ecurve::edwards-bls12

Here is a linkto the source code containing these values.

Definitions and Theorems

Function: edwards-bls12-generator

(defun edwards-bls12-generator nil
 (declare (xargs :guard t))
 (let ((__function__ 'edwards-bls12-generator))
  (declare (ignorable __function__))
  (ecurve::point-finite
   7810607721416582242904415504650443951498042435501746664987470571546413371306
   1867362672570137759132108893390349941423731440336755218616442213142473202417)))

Theorem: edwards-bls12-pointp-of-edwards-bls12-generator

(defthm edwards-bls12-pointp-of-edwards-bls12-generator
  (b* ((point (edwards-bls12-generator)))
    (ecurve::edwards-bls12-pointp point))
  :rule-classes :rewrite)