Fix computation of INTX_MIN

The minimum is -2^(bitwidth-1), not -2^bitwidth.  Oops.

14 files changed, 77 insertions, 85 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index b173a7498..5366ec40c 100644
--- a/curve25519_32.c
+++ b/curve25519_32.c
@@ -39,7 +39,7 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia
  */
 static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((int64_t)x1 >> 26);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 26);
   uint32_t x3 = (x1 & UINT32_C(0x3ffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);
@@ -73,7 +73,7 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia
  */
 static void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((int64_t)x1 >> 25);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 25);
   uint32_t x3 = (x1 & UINT32_C(0x1ffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);
@@ -748,7 +748,7 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) {
   uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff));
   uint8_t x82 = (uint8_t)(x80 >> 8);
   uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
-  fiat_25519_uint1 x84 = (fiat_25519_uint1)((int64_t)x82 >> 8);
+  fiat_25519_uint1 x84 = (fiat_25519_uint1)(x82 >> 8);
   uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff));
   uint32_t x86 = (x84 + x32);
   uint32_t x87 = (x86 >> 8);
diff --git a/curve25519_64.c b/curve25519_64.c
index 3a637743e..23bf361d8 100644
--- a/curve25519_64.c
+++ b/curve25519_64.c
@@ -41,7 +41,7 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia
  */
 static 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)((fiat_25519_int128)x1 >> 51);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 51);
   uint64_t x3 = (x1 & UINT64_C(0x7ffffffffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);
diff --git a/p224_32.c b/p224_32.c
index dbe3b4f28..65d26dff1 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -14,8 +14,6 @@
 #include <stdint.h>
 typedef unsigned char fiat_p224_uint1;
 typedef signed char fiat_p224_int1;
-typedef signed __int128 fiat_p224_int128;
-typedef unsigned __int128 fiat_p224_uint128;
 
 
 /*
@@ -46,7 +44,7 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_
  */
 static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p224_int1 x2 = (fiat_p224_int1)((fiat_p224_int128)x1 >> 32);
+  fiat_p224_int1 x2 = (fiat_p224_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p224_uint1)(0x0 - x2);
@@ -2636,7 +2634,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x11 = (uint8_t)(x8 & UINT8_C(0xff));
   uint8_t x12 = (uint8_t)(x10 >> 8);
   uint8_t x13 = (uint8_t)(x10 & UINT8_C(0xff));
-  fiat_p224_uint1 x14 = (fiat_p224_uint1)((int64_t)x12 >> 8);
+  fiat_p224_uint1 x14 = (fiat_p224_uint1)(x12 >> 8);
   uint8_t x15 = (uint8_t)(x12 & UINT8_C(0xff));
   uint32_t x16 = (x14 + x6);
   uint32_t x17 = (x16 >> 8);
@@ -2645,7 +2643,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint8_t x21 = (uint8_t)(x19 >> 8);
   uint8_t x22 = (uint8_t)(x19 & UINT8_C(0xff));
-  fiat_p224_uint1 x23 = (fiat_p224_uint1)((int64_t)x21 >> 8);
+  fiat_p224_uint1 x23 = (fiat_p224_uint1)(x21 >> 8);
   uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff));
   uint32_t x25 = (x23 + x5);
   uint32_t x26 = (x25 >> 8);
@@ -2654,7 +2652,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff));
   uint8_t x30 = (uint8_t)(x28 >> 8);
   uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff));
-  fiat_p224_uint1 x32 = (fiat_p224_uint1)((int64_t)x30 >> 8);
+  fiat_p224_uint1 x32 = (fiat_p224_uint1)(x30 >> 8);
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
   uint32_t x34 = (x32 + x4);
   uint32_t x35 = (x34 >> 8);
@@ -2663,7 +2661,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff));
   uint8_t x39 = (uint8_t)(x37 >> 8);
   uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff));
-  fiat_p224_uint1 x41 = (fiat_p224_uint1)((int64_t)x39 >> 8);
+  fiat_p224_uint1 x41 = (fiat_p224_uint1)(x39 >> 8);
   uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff));
   uint32_t x43 = (x41 + x3);
   uint32_t x44 = (x43 >> 8);
@@ -2672,7 +2670,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff));
   uint8_t x48 = (uint8_t)(x46 >> 8);
   uint8_t x49 = (uint8_t)(x46 & UINT8_C(0xff));
-  fiat_p224_uint1 x50 = (fiat_p224_uint1)((int64_t)x48 >> 8);
+  fiat_p224_uint1 x50 = (fiat_p224_uint1)(x48 >> 8);
   uint8_t x51 = (uint8_t)(x48 & UINT8_C(0xff));
   uint32_t x52 = (x50 + x2);
   uint32_t x53 = (x52 >> 8);
@@ -2681,7 +2679,7 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
   uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff));
   uint8_t x57 = (uint8_t)(x55 >> 8);
   uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff));
-  fiat_p224_uint1 x59 = (fiat_p224_uint1)((int64_t)x57 >> 8);
+  fiat_p224_uint1 x59 = (fiat_p224_uint1)(x57 >> 8);
   uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff));
   uint32_t x61 = (x59 + x1);
   uint32_t x62 = (x61 >> 8);
diff --git a/p224_64.c b/p224_64.c
index ec197db62..d67ee56ca 100644
--- a/p224_64.c
+++ b/p224_64.c
@@ -46,7 +46,7 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_
  */
 static void fiat_p224_subborrowx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p224_int128 x1 = ((arg2 - (fiat_p224_int128)arg1) - arg3);
-  fiat_p224_int1 x2 = (fiat_p224_int1)((fiat_p224_int256)x1 >> 64);
+  fiat_p224_int1 x2 = (fiat_p224_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p224_uint1)(0x0 - x2);
@@ -1183,7 +1183,7 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint8_t x17 = (uint8_t)(x15 >> 8);
   uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
-  fiat_p224_uint1 x19 = (fiat_p224_uint1)((int64_t)x17 >> 8);
+  fiat_p224_uint1 x19 = (fiat_p224_uint1)(x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint64_t x21 = (x19 + x3);
   uint64_t x22 = (x21 >> 8);
@@ -1200,7 +1200,7 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
   uint8_t x34 = (uint8_t)(x32 >> 8);
   uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
-  fiat_p224_uint1 x36 = (fiat_p224_uint1)((int64_t)x34 >> 8);
+  fiat_p224_uint1 x36 = (fiat_p224_uint1)(x34 >> 8);
   uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
   uint64_t x38 = (x36 + x2);
   uint64_t x39 = (x38 >> 8);
@@ -1217,7 +1217,7 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
   uint8_t x51 = (uint8_t)(x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
-  fiat_p224_uint1 x53 = (fiat_p224_uint1)((int64_t)x51 >> 8);
+  fiat_p224_uint1 x53 = (fiat_p224_uint1)(x51 >> 8);
   uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
   uint64_t x55 = (x53 + x1);
   uint64_t x56 = (x55 >> 8);
@@ -1226,13 +1226,13 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
   uint8_t x60 = (uint8_t)(x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
-  fiat_p224_uint1 x62 = (fiat_p224_uint1)((int64_t)x60 >> 8);
+  fiat_p224_uint1 x62 = (fiat_p224_uint1)(x60 >> 8);
   uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff));
-  fiat_p224_uint1 x64 = (fiat_p224_uint1)((int64_t)x62 >> 8);
+  fiat_p224_uint1 x64 = (fiat_p224_uint1)(x62 >> 8);
   fiat_p224_uint1 x65 = (fiat_p224_uint1)(x62 & UINT8_C(0xff));
-  fiat_p224_uint1 x66 = (fiat_p224_uint1)((int64_t)x64 >> 8);
+  fiat_p224_uint1 x66 = (fiat_p224_uint1)(x64 >> 8);
   fiat_p224_uint1 x67 = (fiat_p224_uint1)(x64 & UINT8_C(0xff));
-  fiat_p224_uint1 x68 = (fiat_p224_uint1)((int64_t)x66 >> 8);
+  fiat_p224_uint1 x68 = (fiat_p224_uint1)(x66 >> 8);
   fiat_p224_uint1 x69 = (fiat_p224_uint1)(x66 & UINT8_C(0xff));
   out1[0] = x6;
   out1[1] = x8;
diff --git a/p256_32.c b/p256_32.c
index d10165fce..825a10ca2 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -14,8 +14,6 @@
 #include <stdint.h>
 typedef unsigned char fiat_p256_uint1;
 typedef signed char fiat_p256_int1;
-typedef signed __int128 fiat_p256_int128;
-typedef unsigned __int128 fiat_p256_uint128;
 
 
 /*
@@ -46,7 +44,7 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_
  */
 static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p256_int1 x2 = (fiat_p256_int1)((fiat_p256_int128)x1 >> 32);
+  fiat_p256_int1 x2 = (fiat_p256_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p256_uint1)(0x0 - x2);
@@ -3187,7 +3185,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff));
   uint8_t x13 = (uint8_t)(x11 >> 8);
   uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff));
-  fiat_p256_uint1 x15 = (fiat_p256_uint1)((int64_t)x13 >> 8);
+  fiat_p256_uint1 x15 = (fiat_p256_uint1)(x13 >> 8);
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint32_t x17 = (x15 + x7);
   uint32_t x18 = (x17 >> 8);
@@ -3196,7 +3194,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff));
   uint8_t x22 = (uint8_t)(x20 >> 8);
   uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff));
-  fiat_p256_uint1 x24 = (fiat_p256_uint1)((int64_t)x22 >> 8);
+  fiat_p256_uint1 x24 = (fiat_p256_uint1)(x22 >> 8);
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint32_t x26 = (x24 + x6);
   uint32_t x27 = (x26 >> 8);
@@ -3205,7 +3203,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff));
   uint8_t x31 = (uint8_t)(x29 >> 8);
   uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff));
-  fiat_p256_uint1 x33 = (fiat_p256_uint1)((int64_t)x31 >> 8);
+  fiat_p256_uint1 x33 = (fiat_p256_uint1)(x31 >> 8);
   uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
   uint32_t x35 = (x33 + x5);
   uint32_t x36 = (x35 >> 8);
@@ -3214,7 +3212,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff));
   uint8_t x40 = (uint8_t)(x38 >> 8);
   uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff));
-  fiat_p256_uint1 x42 = (fiat_p256_uint1)((int64_t)x40 >> 8);
+  fiat_p256_uint1 x42 = (fiat_p256_uint1)(x40 >> 8);
   uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
   uint32_t x44 = (x42 + x4);
   uint32_t x45 = (x44 >> 8);
@@ -3223,7 +3221,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff));
   uint8_t x49 = (uint8_t)(x47 >> 8);
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
-  fiat_p256_uint1 x51 = (fiat_p256_uint1)((int64_t)x49 >> 8);
+  fiat_p256_uint1 x51 = (fiat_p256_uint1)(x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint32_t x53 = (x51 + x3);
   uint32_t x54 = (x53 >> 8);
@@ -3232,7 +3230,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
   uint8_t x58 = (uint8_t)(x56 >> 8);
   uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
-  fiat_p256_uint1 x60 = (fiat_p256_uint1)((int64_t)x58 >> 8);
+  fiat_p256_uint1 x60 = (fiat_p256_uint1)(x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint32_t x62 = (x60 + x2);
   uint32_t x63 = (x62 >> 8);
@@ -3241,7 +3239,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff));
   uint8_t x67 = (uint8_t)(x65 >> 8);
   uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff));
-  fiat_p256_uint1 x69 = (fiat_p256_uint1)((int64_t)x67 >> 8);
+  fiat_p256_uint1 x69 = (fiat_p256_uint1)(x67 >> 8);
   uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
   uint32_t x71 = (x69 + x1);
   uint32_t x72 = (x71 >> 8);
diff --git a/p256_64.c b/p256_64.c
index 70b523744..2bd9b8d51 100644
--- a/p256_64.c
+++ b/p256_64.c
@@ -46,7 +46,7 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_
  */
 static void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p256_int128 x1 = ((arg2 - (fiat_p256_int128)arg1) - arg3);
-  fiat_p256_int1 x2 = (fiat_p256_int1)((fiat_p256_int256)x1 >> 64);
+  fiat_p256_int1 x2 = (fiat_p256_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p256_uint1)(0x0 - x2);
@@ -1183,7 +1183,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint8_t x17 = (uint8_t)(x15 >> 8);
   uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
-  fiat_p256_uint1 x19 = (fiat_p256_uint1)((int64_t)x17 >> 8);
+  fiat_p256_uint1 x19 = (fiat_p256_uint1)(x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint64_t x21 = (x19 + x3);
   uint64_t x22 = (x21 >> 8);
@@ -1200,7 +1200,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
   uint8_t x34 = (uint8_t)(x32 >> 8);
   uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
-  fiat_p256_uint1 x36 = (fiat_p256_uint1)((int64_t)x34 >> 8);
+  fiat_p256_uint1 x36 = (fiat_p256_uint1)(x34 >> 8);
   uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
   uint64_t x38 = (x36 + x2);
   uint64_t x39 = (x38 >> 8);
@@ -1217,7 +1217,7 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
   uint8_t x51 = (uint8_t)(x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
-  fiat_p256_uint1 x53 = (fiat_p256_uint1)((int64_t)x51 >> 8);
+  fiat_p256_uint1 x53 = (fiat_p256_uint1)(x51 >> 8);
   uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
   uint64_t x55 = (x53 + x1);
   uint64_t x56 = (x55 >> 8);
diff --git a/p384_32.c b/p384_32.c
index 95b6c73d3..3c8f908af 100644
--- a/p384_32.c
+++ b/p384_32.c
@@ -14,8 +14,6 @@
 #include <stdint.h>
 typedef unsigned char fiat_p384_uint1;
 typedef signed char fiat_p384_int1;
-typedef signed __int128 fiat_p384_int128;
-typedef unsigned __int128 fiat_p384_uint128;
 
 
 /*
@@ -46,7 +44,7 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_
  */
 static void fiat_p384_subborrowx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_p384_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p384_int1 x2 = (fiat_p384_int1)((fiat_p384_int128)x1 >> 32);
+  fiat_p384_int1 x2 = (fiat_p384_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p384_uint1)(0x0 - x2);
@@ -7302,7 +7300,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint8_t x17 = (uint8_t)(x15 >> 8);
   uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
-  fiat_p384_uint1 x19 = (fiat_p384_uint1)((int64_t)x17 >> 8);
+  fiat_p384_uint1 x19 = (fiat_p384_uint1)(x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint32_t x21 = (x19 + x11);
   uint32_t x22 = (x21 >> 8);
@@ -7311,7 +7309,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint8_t x26 = (uint8_t)(x24 >> 8);
   uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff));
-  fiat_p384_uint1 x28 = (fiat_p384_uint1)((int64_t)x26 >> 8);
+  fiat_p384_uint1 x28 = (fiat_p384_uint1)(x26 >> 8);
   uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff));
   uint32_t x30 = (x28 + x10);
   uint32_t x31 = (x30 >> 8);
@@ -7320,7 +7318,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
   uint8_t x35 = (uint8_t)(x33 >> 8);
   uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff));
-  fiat_p384_uint1 x37 = (fiat_p384_uint1)((int64_t)x35 >> 8);
+  fiat_p384_uint1 x37 = (fiat_p384_uint1)(x35 >> 8);
   uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff));
   uint32_t x39 = (x37 + x9);
   uint32_t x40 = (x39 >> 8);
@@ -7329,7 +7327,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
   uint8_t x44 = (uint8_t)(x42 >> 8);
   uint8_t x45 = (uint8_t)(x42 & UINT8_C(0xff));
-  fiat_p384_uint1 x46 = (fiat_p384_uint1)((int64_t)x44 >> 8);
+  fiat_p384_uint1 x46 = (fiat_p384_uint1)(x44 >> 8);
   uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff));
   uint32_t x48 = (x46 + x8);
   uint32_t x49 = (x48 >> 8);
@@ -7338,7 +7336,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint8_t x53 = (uint8_t)(x51 >> 8);
   uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
-  fiat_p384_uint1 x55 = (fiat_p384_uint1)((int64_t)x53 >> 8);
+  fiat_p384_uint1 x55 = (fiat_p384_uint1)(x53 >> 8);
   uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff));
   uint32_t x57 = (x55 + x7);
   uint32_t x58 = (x57 >> 8);
@@ -7347,7 +7345,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint8_t x62 = (uint8_t)(x60 >> 8);
   uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff));
-  fiat_p384_uint1 x64 = (fiat_p384_uint1)((int64_t)x62 >> 8);
+  fiat_p384_uint1 x64 = (fiat_p384_uint1)(x62 >> 8);
   uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff));
   uint32_t x66 = (x64 + x6);
   uint32_t x67 = (x66 >> 8);
@@ -7356,7 +7354,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
   uint8_t x71 = (uint8_t)(x69 >> 8);
   uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff));
-  fiat_p384_uint1 x73 = (fiat_p384_uint1)((int64_t)x71 >> 8);
+  fiat_p384_uint1 x73 = (fiat_p384_uint1)(x71 >> 8);
   uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff));
   uint32_t x75 = (x73 + x5);
   uint32_t x76 = (x75 >> 8);
@@ -7365,7 +7363,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x79 = (uint8_t)(x76 & UINT8_C(0xff));
   uint8_t x80 = (uint8_t)(x78 >> 8);
   uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff));
-  fiat_p384_uint1 x82 = (fiat_p384_uint1)((int64_t)x80 >> 8);
+  fiat_p384_uint1 x82 = (fiat_p384_uint1)(x80 >> 8);
   uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
   uint32_t x84 = (x82 + x4);
   uint32_t x85 = (x84 >> 8);
@@ -7374,7 +7372,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff));
   uint8_t x89 = (uint8_t)(x87 >> 8);
   uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff));
-  fiat_p384_uint1 x91 = (fiat_p384_uint1)((int64_t)x89 >> 8);
+  fiat_p384_uint1 x91 = (fiat_p384_uint1)(x89 >> 8);
   uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff));
   uint32_t x93 = (x91 + x3);
   uint32_t x94 = (x93 >> 8);
@@ -7383,7 +7381,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff));
   uint8_t x98 = (uint8_t)(x96 >> 8);
   uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff));
-  fiat_p384_uint1 x100 = (fiat_p384_uint1)((int64_t)x98 >> 8);
+  fiat_p384_uint1 x100 = (fiat_p384_uint1)(x98 >> 8);
   uint8_t x101 = (uint8_t)(x98 & UINT8_C(0xff));
   uint32_t x102 = (x100 + x2);
   uint32_t x103 = (x102 >> 8);
@@ -7392,7 +7390,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) {
   uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff));
   uint8_t x107 = (uint8_t)(x105 >> 8);
   uint8_t x108 = (uint8_t)(x105 & UINT8_C(0xff));
-  fiat_p384_uint1 x109 = (fiat_p384_uint1)((int64_t)x107 >> 8);
+  fiat_p384_uint1 x109 = (fiat_p384_uint1)(x107 >> 8);
   uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff));
   uint32_t x111 = (x109 + x1);
   uint32_t x112 = (x111 >> 8);
diff --git a/p384_64.c b/p384_64.c
index b4aff4a1e..094f27a92 100644
--- a/p384_64.c
+++ b/p384_64.c
@@ -46,7 +46,7 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_
  */
 static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_p384_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p384_int128 x1 = ((arg2 - (fiat_p384_int128)arg1) - arg3);
-  fiat_p384_int1 x2 = (fiat_p384_int1)((fiat_p384_int256)x1 >> 64);
+  fiat_p384_int1 x2 = (fiat_p384_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p384_uint1)(0x0 - x2);
@@ -2363,7 +2363,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
   uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
   uint8_t x19 = (uint8_t)(x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
-  fiat_p384_uint1 x21 = (fiat_p384_uint1)((int64_t)x19 >> 8);
+  fiat_p384_uint1 x21 = (fiat_p384_uint1)(x19 >> 8);
   uint8_t x22 = (uint8_t)(x19 & UINT8_C(0xff));
   uint64_t x23 = (x21 + x5);
   uint64_t x24 = (x23 >> 8);
@@ -2380,7 +2380,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
   uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
   uint8_t x36 = (uint8_t)(x34 >> 8);
   uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
-  fiat_p384_uint1 x38 = (fiat_p384_uint1)((int64_t)x36 >> 8);
+  fiat_p384_uint1 x38 = (fiat_p384_uint1)(x36 >> 8);
   uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff));
   uint64_t x40 = (x38 + x4);
   uint64_t x41 = (x40 >> 8);
@@ -2397,7 +2397,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint8_t x53 = (uint8_t)(x51 >> 8);
   uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
-  fiat_p384_uint1 x55 = (fiat_p384_uint1)((int64_t)x53 >> 8);
+  fiat_p384_uint1 x55 = (fiat_p384_uint1)(x53 >> 8);
   uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff));
   uint64_t x57 = (x55 + x3);
   uint64_t x58 = (x57 >> 8);
@@ -2414,7 +2414,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
   uint8_t x69 = (uint8_t)(x66 & UINT8_C(0xff));
   uint8_t x70 = (uint8_t)(x68 >> 8);
   uint8_t x71 = (uint8_t)(x68 & UINT8_C(0xff));
-  fiat_p384_uint1 x72 = (fiat_p384_uint1)((int64_t)x70 >> 8);
+  fiat_p384_uint1 x72 = (fiat_p384_uint1)(x70 >> 8);
   uint8_t x73 = (uint8_t)(x70 & UINT8_C(0xff));
   uint64_t x74 = (x72 + x2);
   uint64_t x75 = (x74 >> 8);
@@ -2431,7 +2431,7 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) {
   uint8_t x86 = (uint8_t)(x83 & UINT8_C(0xff));
   uint8_t x87 = (uint8_t)(x85 >> 8);
   uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff));
-  fiat_p384_uint1 x89 = (fiat_p384_uint1)((int64_t)x87 >> 8);
+  fiat_p384_uint1 x89 = (fiat_p384_uint1)(x87 >> 8);
   uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff));
   uint64_t x91 = (x89 + x1);
   uint64_t x92 = (x91 >> 8);
diff --git a/p484_64.c b/p484_64.c
index 22d060e3f..f3c66f1ff 100644
--- a/p484_64.c
+++ b/p484_64.c
@@ -46,7 +46,7 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_
  */
 static void fiat_p484_subborrowx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_p484_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p484_int128 x1 = ((arg2 - (fiat_p484_int128)arg1) - arg3);
-  fiat_p484_int1 x2 = (fiat_p484_int1)((fiat_p484_int256)x1 >> 64);
+  fiat_p484_int1 x2 = (fiat_p484_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p484_uint1)(0x0 - x2);
@@ -2998,7 +2998,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x19 = (uint8_t)(x16 & UINT8_C(0xff));
   uint8_t x20 = (uint8_t)(x18 >> 8);
   uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff));
-  fiat_p484_uint1 x22 = (fiat_p484_uint1)((int64_t)x20 >> 8);
+  fiat_p484_uint1 x22 = (fiat_p484_uint1)(x20 >> 8);
   uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff));
   uint64_t x24 = (x22 + x6);
   uint64_t x25 = (x24 >> 8);
@@ -3015,7 +3015,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff));
   uint8_t x37 = (uint8_t)(x35 >> 8);
   uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff));
-  fiat_p484_uint1 x39 = (fiat_p484_uint1)((int64_t)x37 >> 8);
+  fiat_p484_uint1 x39 = (fiat_p484_uint1)(x37 >> 8);
   uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff));
   uint64_t x41 = (x39 + x5);
   uint64_t x42 = (x41 >> 8);
@@ -3032,7 +3032,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff));
   uint8_t x54 = (uint8_t)(x52 >> 8);
   uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff));
-  fiat_p484_uint1 x56 = (fiat_p484_uint1)((int64_t)x54 >> 8);
+  fiat_p484_uint1 x56 = (fiat_p484_uint1)(x54 >> 8);
   uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
   uint64_t x58 = (x56 + x4);
   uint64_t x59 = (x58 >> 8);
@@ -3049,7 +3049,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
   uint8_t x71 = (uint8_t)(x69 >> 8);
   uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff));
-  fiat_p484_uint1 x73 = (fiat_p484_uint1)((int64_t)x71 >> 8);
+  fiat_p484_uint1 x73 = (fiat_p484_uint1)(x71 >> 8);
   uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff));
   uint64_t x75 = (x73 + x3);
   uint64_t x76 = (x75 >> 8);
@@ -3066,7 +3066,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x87 = (uint8_t)(x84 & UINT8_C(0xff));
   uint8_t x88 = (uint8_t)(x86 >> 8);
   uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff));
-  fiat_p484_uint1 x90 = (fiat_p484_uint1)((int64_t)x88 >> 8);
+  fiat_p484_uint1 x90 = (fiat_p484_uint1)(x88 >> 8);
   uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff));
   uint64_t x92 = (x90 + x2);
   uint64_t x93 = (x92 >> 8);
@@ -3083,7 +3083,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff));
   uint8_t x105 = (uint8_t)(x103 >> 8);
   uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff));
-  fiat_p484_uint1 x107 = (fiat_p484_uint1)((int64_t)x105 >> 8);
+  fiat_p484_uint1 x107 = (fiat_p484_uint1)(x105 >> 8);
   uint8_t x108 = (uint8_t)(x105 & UINT8_C(0xff));
   uint64_t x109 = (x107 + x1);
   uint64_t x110 = (x109 >> 8);
@@ -3098,7 +3098,7 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) {
   uint8_t x119 = (uint8_t)(x116 & UINT8_C(0xff));
   uint8_t x120 = (uint8_t)(x118 >> 8);
   uint8_t x121 = (uint8_t)(x118 & UINT8_C(0xff));
-  fiat_p484_uint1 x122 = (fiat_p484_uint1)((int64_t)x120 >> 8);
+  fiat_p484_uint1 x122 = (fiat_p484_uint1)(x120 >> 8);
   uint8_t x123 = (uint8_t)(x120 & UINT8_C(0xff));
   out1[0] = x9;
   out1[1] = x11;
diff --git a/p521_32.c b/p521_32.c
index 5e2fd8a15..d1ae368c9 100644
--- a/p521_32.c
+++ b/p521_32.c
@@ -41,7 +41,7 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((int64_t)x1 >> 30);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 30);
   uint32_t x3 = (x1 & UINT32_C(0x3fffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -1200,7 +1200,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) {
   uint8_t x130 = (uint8_t)(x127 & UINT8_C(0xff));
   uint8_t x131 = (uint8_t)(x129 >> 8);
   uint8_t x132 = (uint8_t)(x129 & UINT8_C(0xff));
-  fiat_p521_uint1 x133 = (fiat_p521_uint1)((int64_t)x131 >> 8);
+  fiat_p521_uint1 x133 = (fiat_p521_uint1)(x131 >> 8);
   uint8_t x134 = (uint8_t)(x131 & UINT8_C(0xff));
   uint32_t x135 = (x133 + x48);
   uint32_t x136 = (x135 >> 8);
@@ -1252,7 +1252,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) {
   uint8_t x182 = (uint8_t)(x179 & UINT8_C(0xff));
   uint8_t x183 = (uint8_t)(x181 >> 8);
   uint8_t x184 = (uint8_t)(x181 & UINT8_C(0xff));
-  fiat_p521_uint1 x185 = (fiat_p521_uint1)((int64_t)x183 >> 8);
+  fiat_p521_uint1 x185 = (fiat_p521_uint1)(x183 >> 8);
   uint8_t x186 = (uint8_t)(x183 & UINT8_C(0xff));
   uint32_t x187 = (x185 + x60);
   uint32_t x188 = (x187 >> 8);
diff --git a/p521_64.c b/p521_64.c
index 386f6241e..f81fa7967 100644
--- a/p521_64.c
+++ b/p521_64.c
@@ -41,7 +41,7 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((fiat_p521_int128)x1 >> 58);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 58);
   uint64_t x3 = (x1 & UINT64_C(0x3ffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -75,7 +75,7 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((fiat_p521_int128)x1 >> 57);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 57);
   uint64_t x3 = (x1 & UINT64_C(0x1ffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -646,7 +646,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) {
   uint8_t x100 = (uint8_t)(x97 & UINT8_C(0xff));
   uint8_t x101 = (uint8_t)(x99 >> 8);
   uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff));
-  fiat_p521_uint1 x103 = (fiat_p521_uint1)((int64_t)x101 >> 8);
+  fiat_p521_uint1 x103 = (fiat_p521_uint1)(x101 >> 8);
   uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff));
   uint64_t x105 = (x103 + x28);
   uint64_t x106 = (x105 >> 8);
@@ -708,7 +708,7 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) {
   uint8_t x162 = (uint8_t)(x159 & UINT8_C(0xff));
   uint8_t x163 = (uint8_t)(x161 >> 8);
   uint8_t x164 = (uint8_t)(x161 & UINT8_C(0xff));
-  fiat_p521_uint1 x165 = (fiat_p521_uint1)((int64_t)x163 >> 8);
+  fiat_p521_uint1 x165 = (fiat_p521_uint1)(x163 >> 8);
   uint8_t x166 = (uint8_t)(x163 & UINT8_C(0xff));
   uint64_t x167 = (x165 + x36);
   uint64_t x168 = (x167 >> 8);
diff --git a/secp256k1_32.c b/secp256k1_32.c
index 3286161d4..94744d26a 100644
--- a/secp256k1_32.c
+++ b/secp256k1_32.c
@@ -14,8 +14,6 @@
 #include <stdint.h>
 typedef unsigned char fiat_secp256k1_uint1;
 typedef signed char fiat_secp256k1_int1;
-typedef signed __int128 fiat_secp256k1_int128;
-typedef unsigned __int128 fiat_secp256k1_uint128;
 
 
 /*
@@ -46,7 +44,7 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o
  */
 static void fiat_secp256k1_subborrowx_u32(uint32_t* out1, fiat_secp256k1_uint1* out2, fiat_secp256k1_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((fiat_secp256k1_int128)x1 >> 32);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_secp256k1_uint1)(0x0 - x2);
@@ -3847,7 +3845,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff));
   uint8_t x13 = (uint8_t)(x11 >> 8);
   uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x15 = (fiat_secp256k1_uint1)((int64_t)x13 >> 8);
+  fiat_secp256k1_uint1 x15 = (fiat_secp256k1_uint1)(x13 >> 8);
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint32_t x17 = (x15 + x7);
   uint32_t x18 = (x17 >> 8);
@@ -3856,7 +3854,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff));
   uint8_t x22 = (uint8_t)(x20 >> 8);
   uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x24 = (fiat_secp256k1_uint1)((int64_t)x22 >> 8);
+  fiat_secp256k1_uint1 x24 = (fiat_secp256k1_uint1)(x22 >> 8);
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint32_t x26 = (x24 + x6);
   uint32_t x27 = (x26 >> 8);
@@ -3865,7 +3863,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff));
   uint8_t x31 = (uint8_t)(x29 >> 8);
   uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x33 = (fiat_secp256k1_uint1)((int64_t)x31 >> 8);
+  fiat_secp256k1_uint1 x33 = (fiat_secp256k1_uint1)(x31 >> 8);
   uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
   uint32_t x35 = (x33 + x5);
   uint32_t x36 = (x35 >> 8);
@@ -3874,7 +3872,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff));
   uint8_t x40 = (uint8_t)(x38 >> 8);
   uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x42 = (fiat_secp256k1_uint1)((int64_t)x40 >> 8);
+  fiat_secp256k1_uint1 x42 = (fiat_secp256k1_uint1)(x40 >> 8);
   uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
   uint32_t x44 = (x42 + x4);
   uint32_t x45 = (x44 >> 8);
@@ -3883,7 +3881,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff));
   uint8_t x49 = (uint8_t)(x47 >> 8);
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x51 = (fiat_secp256k1_uint1)((int64_t)x49 >> 8);
+  fiat_secp256k1_uint1 x51 = (fiat_secp256k1_uint1)(x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint32_t x53 = (x51 + x3);
   uint32_t x54 = (x53 >> 8);
@@ -3892,7 +3890,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
   uint8_t x58 = (uint8_t)(x56 >> 8);
   uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x60 = (fiat_secp256k1_uint1)((int64_t)x58 >> 8);
+  fiat_secp256k1_uint1 x60 = (fiat_secp256k1_uint1)(x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint32_t x62 = (x60 + x2);
   uint32_t x63 = (x62 >> 8);
@@ -3901,7 +3899,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
   uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff));
   uint8_t x67 = (uint8_t)(x65 >> 8);
   uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x69 = (fiat_secp256k1_uint1)((int64_t)x67 >> 8);
+  fiat_secp256k1_uint1 x69 = (fiat_secp256k1_uint1)(x67 >> 8);
   uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
   uint32_t x71 = (x69 + x1);
   uint32_t x72 = (x71 >> 8);
diff --git a/secp256k1_64.c b/secp256k1_64.c
index 9abfa7910..749e9bc40 100644
--- a/secp256k1_64.c
+++ b/secp256k1_64.c
@@ -46,7 +46,7 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o
  */
 static void fiat_secp256k1_subborrowx_u64(uint64_t* out1, fiat_secp256k1_uint1* out2, fiat_secp256k1_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_secp256k1_int128 x1 = ((arg2 - (fiat_secp256k1_int128)arg1) - arg3);
-  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((fiat_secp256k1_int256)x1 >> 64);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_secp256k1_uint1)(0x0 - x2);
@@ -1255,7 +1255,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint8_t x17 = (uint8_t)(x15 >> 8);
   uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x19 = (fiat_secp256k1_uint1)((int64_t)x17 >> 8);
+  fiat_secp256k1_uint1 x19 = (fiat_secp256k1_uint1)(x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint64_t x21 = (x19 + x3);
   uint64_t x22 = (x21 >> 8);
@@ -1272,7 +1272,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
   uint8_t x34 = (uint8_t)(x32 >> 8);
   uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x36 = (fiat_secp256k1_uint1)((int64_t)x34 >> 8);
+  fiat_secp256k1_uint1 x36 = (fiat_secp256k1_uint1)(x34 >> 8);
   uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
   uint64_t x38 = (x36 + x2);
   uint64_t x39 = (x38 >> 8);
@@ -1289,7 +1289,7 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
   uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
   uint8_t x51 = (uint8_t)(x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
-  fiat_secp256k1_uint1 x53 = (fiat_secp256k1_uint1)((int64_t)x51 >> 8);
+  fiat_secp256k1_uint1 x53 = (fiat_secp256k1_uint1)(x51 >> 8);
   uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff));
   uint64_t x55 = (x53 + x1);
   uint64_t x56 = (x55 >> 8);
diff --git a/src/CStringification.v b/src/CStringification.v
index 2321d3a3d..b61421bc4 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -616,7 +616,7 @@ Module Compilers.
         Definition to_zrange (t : type) : zrange
           := let bw := bitwidth_of t in
              if is_signed t
-             then r[-2^bw ~> 2^(bw-1) - 1]
+             then r[-2^(bw-1) ~> 2^(bw-1) - 1]
              else r[0 ~> 2^bw - 1].
         Definition is_tighter_than (t1 t2 : type)
           := ZRange.is_tighter_than_bool (to_zrange t1) (to_zrange t2).