#include <stdint.h>
#ifndef RANDOMBYTES_H
#define RANDOMBYTES_H

void randombytes(uint8_t *x, uint64_t xlen);

#endif