package tezos-bls12-381-polynomial

allocate_fr_array n allocates an OCaml custom block to hold a C array containing n zeros of blst_fr

• requires: n > 0
• ensures: size res = n and res is initialized with zeros of blst_fr

erase_fr_array 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_fr_array res p n converts a given C array p of at least size n to an OCaml array res of size n

• requires: n <= size p
• ensures: size res = n and res is a prefix of p

get res p i writes i-th element of a given array p in res

• requires: 0 <= i < size p
• ensures: res = p[i]

copy a b offset len starting from position offset copies len elements from array b to array a

requires:

• a and b be disjoint
• len <= size a
• offset + len <= size b

ensures: a[i] = b[offset + i] for i = 0..(len - 1)

of_dense res p n converts an OCaml array p of size n to a C array res of size n

requires:

• size res = n
• size p = n

eq a b size_a size_b checks whether a polynomial a is equal to a polynomial b

requires:

• size a = size_a
• size b = size_b

is_zero p n checks whether a prefix of size n of an array p is filled with zeros of blst_fr

• requires: size p >= n