#include <stdint.h>
#ifndef RANDOMBYTES_H
#define RANDOMBYTES_H
void randombytes(uint8_t *x, uint64_t xlen);
#endif