Module LibResult.Ecc

Addition on ECC curves.

val weierstrass_add : (scalar * scalar) repr -> (scalar * scalar) repr -> (scalar * scalar) repr t

weierstrass_add (px, py) (qx, qy) returns a pair (rx, ry) representing point addition over the Jubjub curve in Weierstrass coordinates of the given input points. Namely, it enforces constraints rx = λ² - (px + qx) and ry = λ * (px - rx) - py, where λ := (qy - py) / (qx - px).

val edwards_add : (scalar * scalar) repr -> (scalar * scalar) repr -> (scalar * scalar) repr t

edwards_add (px, py) (qx, qy) returns a pair (rx, ry) representing point addition over the Jubjub curve in Edwards coordinates of the given input points. Namely, it enforces constraints rx = (px * qy + qx * py) / (1 + d * px * py * qx * qy) and ry = (py * qy - a * px * qx) / (1 - d * px * py * qx * qy) where a := -1 and d are fixed parameters of the Jubjub curve in this representation. See Lib_plonk.Ecc_gates.

val edwards_cond_add : (scalar * scalar) repr -> (scalar * scalar) repr -> bool repr -> (scalar * scalar) repr t

edwards_cond_add p q b returns edwards_add p q if b is true and p otherwise.