Throwing the KLEE symbolic execution engine against crypto libraries

test.c

#include <stdlib.h>
#include <string.h>
#include <unistd.h>

#include "monocypher/monocypher.c"
#include "tweetnacl/tweetnacl.h"
#include <klee/klee.h>

int
main(int argc, char **argv)
{
	u8 n[32] = {
		0x02, 0x03, 0x05, 0x07, 0x0b, 0x0d, 0x11, 0x13,
		0x17, 0x1d, 0x1f, 0x25, 0x29, 0x2b, 0x2f, 0x35,
		0x3b, 0x3d, 0x43, 0x47, 0x49, 0x4f, 0x53, 0x59,
		0x61, 0x65, 0x67, 0x6b, 0x6d, 0x71, 0x7f, 0x83
	};

	u8 r1[32], r2[32];
	ge p;

	crypto_scalarmult_base(r1, n);
	ge_scalarmult_base(&p, n);
	ge_tobytes(r2, &p);

	/* cmp */
	if (crypto_verify32(r1, r2) != 0)
		abort();	

	return 0;
}