|
|
|---|
|
|
|
|---|
Leo group arithmetic operations.
These are negation (unary), doubling (unary), addition (binary), subtraction (binary), and scalar multiplication.
These operations are paramterized over the curve; see curve-parameterization. implicitly depend on an elliptic curve.
These ACL2 functions are defined over all possible group values, but they return errors if the underlying points are not in the actual subgroup. It should be an invariant, to be formalized and proved, that the underlying points of the group values in a Leo computation state always belong to the subgroup.