Module Gadget.Edwards25519

Parameters

module L : sig ... end

Signature

type nat_mod

Represents an element from a base field

type point = nat_mod * nat_mod

Represents a point on the curve in affine coordinates

val point_encoding : (Curve.t, point L.repr, point) L.Encodings.encoding
val input_point : ?kind:L.input_kind -> (Z.t * Z.t) -> point L.repr L.t

Returns a Plompiler representation of a point

val is_on_curve : point L.repr -> bool L.repr L.t

is_on_curve p checks whether a point p is on the curve

val from_coordinates : nat_mod L.repr -> nat_mod L.repr -> point L.repr L.t

from_coordinates x y constructs a point p = (x, y) from coordinates x and y. The function also checks whether the point is on the curve (but not necessarily in the subgroup)

val unsafe_from_coordinates : nat_mod L.repr -> nat_mod L.repr -> point L.repr L.t

unsafe_from_coordinates x y is similar to from_coordinates but does not verify the point is on the curve. It can be used to build a variable of type point without adding any constraint

val get_x_coordinate : point L.repr -> nat_mod L.repr

get_x_coordinate p returns a first coordinate x of a point p

val get_y_coordinate : point L.repr -> nat_mod L.repr

get_y_coordinate p returns a second coordinate y of a point p

val id : point L.repr L.t

Returns the point at infinity of the curve (additive identity)

val base_point : point L.repr L.t

Returns the base point of the curve (a fixed generator)

add p q computes a point addition p + q

val negate : point L.repr -> point L.repr L.t

negate p computes a point negation -p

val cond_add : point L.repr -> point L.repr -> bool L.repr -> point L.repr L.t

cond_add p q b returns p + b * q, i.e., either a point addition p and q or a point p based on the value b

val double : point L.repr -> point L.repr L.t

double p computes a point doubling p + p

val scalar_mul : bool list L.repr -> point L.repr -> point L.repr L.t

scalar_mul s p computes a point multiplication p by a scalar s. The scalar s is encoded in little-endian order

val multi_scalar_mul : bool list list L.repr -> point list L.repr -> point L.repr L.t

multi_scalar_mul ls lp computes the multi-scalar multiplication s₁·p₁ + s₂·p₂ + … + sₖ·pₖ

val scalar_order : Z.t

Returns the order of the prime-order subgroup of the elliptic curve group

val base_order : Z.t

Returns the prime number defining the underlying field

val to_compressed_bytes : point L.repr -> L.Bytes.tl L.repr L.t

to_compressed_bytes p returns the compressed representation of a point p = (x, y) in little-endian bytes pow2 255 * (x % 2) + y