		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-types

Types for the secp256k1 elliptic curve.

Here we introduce fixtypes for field elements, point, and keys, along with an operation to represent points as byte lists.

Secp256k1-priv-key: Fixtype of secp256k1 private keys.
Secp256k1-pub-key: Fixtype of secp256k1 public keys.
Secp256k1-field: Fixtype of the elements of the secp256k1 field.
Secp256k1-point: Fixtype of points on the secp256k1 curve.
Secp256k1-point-to-bytes: Represent a secp256k1 point in compressed or uncompressed form.
Secp256k1-point-infinityp: Check if a secp256k1 point is the point at infinity \mathcal{O} of the curve.
Secp256k1-point-generator: The generator point G of the group of the secp256k1 curve.