diff --git a/curve25519_64/src/curve25519_64.c b/curve25519_64/src/curve25519_64.c
index 37aae3b..a66d20c 100644
--- a/curve25519_64/src/curve25519_64.c
+++ b/curve25519_64/src/curve25519_64.c
@@ -9,12 +9,7 @@
 /* Computed values: */
 /* carry_chain = [0, 1, 2, 3, 4, 0, 1] */

-#include <stdint.h>
-typedef unsigned char fiat_25519_uint1;
-typedef signed char fiat_25519_int1;
-typedef signed __int128 fiat_25519_int128;
-typedef unsigned __int128 fiat_25519_uint128;
-
+#include "curve25519_64.h"

 /*
  * The function fiat_25519_addcarryx_u51 is an addition with carry.
@@ -30,7 +25,7 @@ typedef unsigned __int128 fiat_25519_uint128;
  *   out1: [0x0 ~> 0x7ffffffffffff]
  *   out2: [0x0 ~> 0x1]
  */
-static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
+void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   uint64_t x1 = ((arg1 + arg2) + arg3);
   uint64_t x2 = (x1 & UINT64_C(0x7ffffffffffff));
   fiat_25519_uint1 x3 = (fiat_25519_uint1)(x1 >> 51);
@@ -52,7 +47,7 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia
  *   out1: [0x0 ~> 0x7ffffffffffff]
  *   out2: [0x0 ~> 0x1]
  */
-static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
+void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
   fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 51);
   uint64_t x3 = (x1 & UINT64_C(0x7ffffffffffff));
@@ -72,7 +67,7 @@ static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fi
  * Output Bounds:
  *   out1: [0x0 ~> 0xffffffffffffffff]
  */
-static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
+void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_25519_uint1 x1 = (!(!arg1));
   uint64_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
   uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2));
@@ -90,7 +85,7 @@ static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64
  * Output Bounds:
  *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
  */
-static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
+void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
   fiat_25519_uint128 x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13)));
   fiat_25519_uint128 x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13)));
   fiat_25519_uint128 x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * (uint64_t)UINT8_C(0x13)));
@@ -160,7 +155,7 @@ static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const
  * Output Bounds:
  *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
  */
-static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) {
+void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) {
   uint64_t x1 = ((arg1[4]) * (uint64_t)UINT8_C(0x13));
   uint64_t x2 = (x1 * (uint64_t)0x2);
   uint64_t x3 = ((arg1[4]) * (uint64_t)0x2);
@@ -228,7 +223,7 @@ static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) {
  * Output Bounds:
  *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
  */
-static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[5]) {
+void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[5]) {
   fiat_25519_uint128 x1 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[4]));
   fiat_25519_uint128 x2 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[3]));
   fiat_25519_uint128 x3 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[2]));
@@ -273,7 +268,7 @@ static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[
  * Output Bounds:
  *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
  */
-static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) {
+void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) {
   uint64_t x1 = (arg1[0]);
   uint64_t x2 = ((x1 >> 51) + (arg1[1]));
   uint64_t x3 = ((x2 >> 51) + (arg1[2]));
@@ -304,7 +299,7 @@ static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) {
  * Output Bounds:
  *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
  */
-static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
+void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
   uint64_t x1 = ((arg1[0]) + (arg2[0]));
   uint64_t x2 = ((arg1[1]) + (arg2[1]));
   uint64_t x3 = ((arg1[2]) + (arg2[2]));
@@ -328,7 +323,7 @@ static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint6
  * Output Bounds:
  *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
  */
-static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
+void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
   uint64_t x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0]));
   uint64_t x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1]));
   uint64_t x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2]));
@@ -351,7 +346,7 @@ static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint6
  * Output Bounds:
  *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
  */
-static void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) {
+void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) {
   uint64_t x1 = (UINT64_C(0xfffffffffffda) - (arg1[0]));
   uint64_t x2 = (UINT64_C(0xffffffffffffe) - (arg1[1]));
   uint64_t x3 = (UINT64_C(0xffffffffffffe) - (arg1[2]));
@@ -376,7 +371,7 @@ static void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) {
  * Output Bounds:
  *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  */
-static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const uint64_t arg2[5], const uint64_t arg3[5]) {
+void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const uint64_t arg2[5], const uint64_t arg3[5]) {
   uint64_t x1;
   fiat_25519_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0]));
   uint64_t x2;
@@ -404,7 +399,7 @@ static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const
  * Output Bounds:
  *   out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
  */
-static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) {
+void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) {
   uint64_t x1;
   fiat_25519_uint1 x2;
   fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed));
@@ -551,7 +546,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) {
  * Output Bounds:
  *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
  */
-static void fiat_25519_from_bytes(uint64_t out1[5], const uint8_t arg1[32]) {
+void fiat_25519_from_bytes(uint64_t out1[5], const uint8_t arg1[32]) {
   uint64_t x1 = ((uint64_t)(arg1[31]) << 44);
   uint64_t x2 = ((uint64_t)(arg1[30]) << 36);
   uint64_t x3 = ((uint64_t)(arg1[29]) << 28);