Module PBT.MakeECProperties

Parameters

module G : sig ... end

Signature

val check_bytes_random : unit -> unit

Verify that a random point is valid

val check_bytes_zero : unit -> unit

Verify that the zero point is valid

val check_bytes_one : unit -> unit

Verify that the fixed generator point is valid

val check_bytes_random_double : unit -> unit

Verify that doubling a random point gives a valid point

val check_bytes_random_sum : unit -> unit

Verify that the sum of random points is valid

val check_bytes_random_multiplication : unit -> unit

Verify that multiplying a random point by a scalar gives a valid point

val zero_scalar_nullifier_random : unit -> unit

Verify 0_S * g_EC = 0_EC where 0_S is the zero of the scalar field, 0_EC is the point at infinity and g_EC is an element of the EC

val zero_scalar_nullifier_zero : unit -> unit

Verify 0_S * 0_EC = 0_EC where 0_S is the zero of the scalar field and 0_EC is the point at infinity of the EC

val zero_scalar_nullifier_one : unit -> unit

Verify 0_S * 1_EC = 0_EC where 0_S is the 0 of the scalar field, 1_EC is a fixed generator and 0_EC is the point at infinity of the EC

val multiply_by_one_does_nothing : unit -> unit
val opposite_of_opposite : unit -> unit

Verify -(-g) = g where g is an element of the EC

val opposite_of_opposite_using_scalar : unit -> unit
val opposite_of_zero_is_zero : unit -> unit

Verify -(-0_EC) = 0_EC where 0_EC is the point at infinity of the EC

val opposite_of_opposite_of_zero_is_zero : unit -> unit

Verify -(-0_EC) = 0_EC where 0_EC is the point at infinity of the EC

val opposite_of_opposite_of_one_is_one : unit -> unit

Verify -(-0_EC) = 0_EC where 0_EC is the point at infinity of the EC

val additive_associativity : unit -> unit

Verify g1 + (g2 + g3) = (g1 + g2) + g3

val additive_commutativity : unit -> unit

Verify (g1 + g2) = (g2 + g1)

val opposite_existential_property : unit -> unit

Verify that g + (-g) = 0

val distributivity : unit -> unit

Verify a (g1 + g2) = a * g1 + a * g2 where a is a scalar, g1, g2 two elements of the EC

val opposite_equality : unit -> unit

Verify (a + -a) * g = a * g - a * g = 0

val additive_associativity_with_scalar : unit -> unit

a g + b + g = (a + b) g

val multiplication_properties_on_base_field_element : unit -> unit

(a * b) g = a (b g) = b (a g)

val opposite_of_scalar_is_opposite_of_ec : unit -> unit

Verify (-s) * g = s * (-g)

val generator_is_of_prime_order : unit -> unit
val mul_by_order_of_scalar_field_equals_zero : unit -> unit
val double : unit -> unit

Verify 2*g = g + g

val inverse_on_scalar : unit -> unit
val zero_is_the_identity : unit -> unit
val get_tests : unit -> string * unit Alcotest.test_case list

Returns the tests to be used with Alcotest