package tezos-bls12-381-polynomial

erase_t p n writes n zeros of blst_fr in a given array p

• requires: n <= size p
• ensures: a prefix of size n of an array p is filled with zeros

of_sparse res p n converts the sparse representation of a polynomial p to the dense representation, from an OCaml array p of size n to a C array res of size degree p + 1

requires:

• degree of each coeff d_i >= 0 and d_i are unique
• the result must be initialized with zero (as done by Fr_carray.allocate)
• size res = degree p + 1
• size p = n

add res a b size_a size_b writes the result of polynomial addition of a and b in res

requires:

• size a = size_a
• size b = size_b
• size res = max (size_a, size_b)
• res, a and b are either pairwise disjoint or equal

sub res a b size_a size_b writes the result of polynomial subtraction of b from a in res

requires:

• size a = size_a
• size b = size_b
• size res = max (size_a, size_b)
• res, a and b are either pairwise disjoint or equal

mul res a b size_a size_b writes the result of polynomial multiplication of a by b in res

requires:

• the result must be initialized with zero (as done by Fr_carray.allocate)
• size a = size_a
• size b = size_b
• size res = size_a + size_b - 1

mul_by_scalar res b a size_a writes the result of multiplying a polynomial a by a blst_fr element b in res

requires:

• size a = size_a
• size res = size_a
• res and a either disjoint or equal

linear res poly_polylen_coeff nb_polys writes the result of computing λ₁·p₁(x) + λ₂·p₂(x) + … + λₖ·pₖ(x) in res, where

• poly_polylen_coeff.[i] = (pᵢ, size_p_i, λᵢ)
• nb_polys is a number of polynomials, i.e., i = 1..nb_polys

requires:

• the result must be initialized with zero (as done by Fr_carray.allocate)
• size res = max (size_p_i)
• size poly_polylen_coeff = nb_polys
• size p_i = size_p_i

linear_with_powers res c poly_polylen nb_polys writes the result of computing c⁰·p₀(x) + c¹·p₁(x) + … + cᵏ·pₖ(x) in res, where

• poly_polylen.[i] = (pᵢ, size_p_i)
• nb_polys is a number of polynomials

requires:

• the result must be initialized with zero (as done by Fr_carray.allocate)
• size res = max (size_p_i)
• size poly_polylen = nb_polys
• size p_i = size_p_i

negate res p n writes the result of negating a polynomial p in res

requires:

• size p = n
• size res = n
• res and p either disjoint or equal

evaluate res p n x writes the result of evaluating a polynomial p at x in res

• requires: size p = n and n > 0

division_xn res_q res_r p size_p (n, c) writes the quotient and remainder of the division of a polynomial p by (X^n + c) in res

requires:

• size p = size_p and size_p > n
• size res_q = size_p - n
• size res_r = n

mul_xn res p size_p n c writes the result of multiplying a polynomial p by (X^n + c) in res

requires:

• res is initialized with bls-fr zeros
• size p = size_p
• size res = size_p + n