Don't cast signed to unsigned before shifting

Unfortunately, signed->unsigned casts do not commute with shifts.  We
take care to only extend the range when it needs extending, now.  This
was previously causing issues with subborrow.

We should really get proofs about casts in C semantics at some point
soon.

Fixes #489

14 files changed, 101 insertions, 83 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index 5e6ee6486..b173a7498 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)((uint32_t)x1 >> 26);
+  fiat_25519_int1 x2 = (fiat_25519_int1)((int64_t)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)((uint32_t)x1 >> 25);
+  fiat_25519_int1 x2 = (fiat_25519_int1)((int64_t)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)(x82 >> 8);
+  fiat_25519_uint1 x84 = (fiat_25519_uint1)((int64_t)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 ed90d1ce3..3a637743e 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)((uint64_t)x1 >> 51);
+  fiat_25519_int1 x2 = (fiat_25519_int1)((fiat_25519_int128)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 98c0ff60b..dbe3b4f28 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -14,6 +14,8 @@
 #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;
 
 
 /*
@@ -44,7 +46,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)((uint64_t)x1 >> 32);
+  fiat_p224_int1 x2 = (fiat_p224_int1)((fiat_p224_int128)x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p224_uint1)(0x0 - x2);
@@ -2634,7 +2636,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)(x12 >> 8);
+  fiat_p224_uint1 x14 = (fiat_p224_uint1)((int64_t)x12 >> 8);
   uint8_t x15 = (uint8_t)(x12 & UINT8_C(0xff));
   uint32_t x16 = (x14 + x6);
   uint32_t x17 = (x16 >> 8);
@@ -2643,7 +2645,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)(x21 >> 8);
+  fiat_p224_uint1 x23 = (fiat_p224_uint1)((int64_t)x21 >> 8);
   uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff));
   uint32_t x25 = (x23 + x5);
   uint32_t x26 = (x25 >> 8);
@@ -2652,7 +2654,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)(x30 >> 8);
+  fiat_p224_uint1 x32 = (fiat_p224_uint1)((int64_t)x30 >> 8);
   uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
   uint32_t x34 = (x32 + x4);
   uint32_t x35 = (x34 >> 8);
@@ -2661,7 +2663,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)(x39 >> 8);
+  fiat_p224_uint1 x41 = (fiat_p224_uint1)((int64_t)x39 >> 8);
   uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff));
   uint32_t x43 = (x41 + x3);
   uint32_t x44 = (x43 >> 8);
@@ -2670,7 +2672,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)(x48 >> 8);
+  fiat_p224_uint1 x50 = (fiat_p224_uint1)((int64_t)x48 >> 8);
   uint8_t x51 = (uint8_t)(x48 & UINT8_C(0xff));
   uint32_t x52 = (x50 + x2);
   uint32_t x53 = (x52 >> 8);
@@ -2679,7 +2681,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)(x57 >> 8);
+  fiat_p224_uint1 x59 = (fiat_p224_uint1)((int64_t)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 6970ece05..ec197db62 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_uint128)x1 >> 64);
+  fiat_p224_int1 x2 = (fiat_p224_int1)((fiat_p224_int256)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)(x17 >> 8);
+  fiat_p224_uint1 x19 = (fiat_p224_uint1)((int64_t)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)(x34 >> 8);
+  fiat_p224_uint1 x36 = (fiat_p224_uint1)((int64_t)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)(x51 >> 8);
+  fiat_p224_uint1 x53 = (fiat_p224_uint1)((int64_t)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)(x60 >> 8);
+  fiat_p224_uint1 x62 = (fiat_p224_uint1)((int64_t)x60 >> 8);
   uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff));
-  fiat_p224_uint1 x64 = (fiat_p224_uint1)(x62 >> 8);
+  fiat_p224_uint1 x64 = (fiat_p224_uint1)((int64_t)x62 >> 8);
   fiat_p224_uint1 x65 = (fiat_p224_uint1)(x62 & UINT8_C(0xff));
-  fiat_p224_uint1 x66 = (fiat_p224_uint1)(x64 >> 8);
+  fiat_p224_uint1 x66 = (fiat_p224_uint1)((int64_t)x64 >> 8);
   fiat_p224_uint1 x67 = (fiat_p224_uint1)(x64 & UINT8_C(0xff));
-  fiat_p224_uint1 x68 = (fiat_p224_uint1)(x66 >> 8);
+  fiat_p224_uint1 x68 = (fiat_p224_uint1)((int64_t)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 f75ede5b4..d10165fce 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -14,6 +14,8 @@
 #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;
 
 
 /*
@@ -44,7 +46,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)((uint64_t)x1 >> 32);
+  fiat_p256_int1 x2 = (fiat_p256_int1)((fiat_p256_int128)x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p256_uint1)(0x0 - x2);
@@ -3185,7 +3187,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)(x13 >> 8);
+  fiat_p256_uint1 x15 = (fiat_p256_uint1)((int64_t)x13 >> 8);
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint32_t x17 = (x15 + x7);
   uint32_t x18 = (x17 >> 8);
@@ -3194,7 +3196,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)(x22 >> 8);
+  fiat_p256_uint1 x24 = (fiat_p256_uint1)((int64_t)x22 >> 8);
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint32_t x26 = (x24 + x6);
   uint32_t x27 = (x26 >> 8);
@@ -3203,7 +3205,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)(x31 >> 8);
+  fiat_p256_uint1 x33 = (fiat_p256_uint1)((int64_t)x31 >> 8);
   uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
   uint32_t x35 = (x33 + x5);
   uint32_t x36 = (x35 >> 8);
@@ -3212,7 +3214,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)(x40 >> 8);
+  fiat_p256_uint1 x42 = (fiat_p256_uint1)((int64_t)x40 >> 8);
   uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
   uint32_t x44 = (x42 + x4);
   uint32_t x45 = (x44 >> 8);
@@ -3221,7 +3223,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)(x49 >> 8);
+  fiat_p256_uint1 x51 = (fiat_p256_uint1)((int64_t)x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint32_t x53 = (x51 + x3);
   uint32_t x54 = (x53 >> 8);
@@ -3230,7 +3232,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)(x58 >> 8);
+  fiat_p256_uint1 x60 = (fiat_p256_uint1)((int64_t)x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint32_t x62 = (x60 + x2);
   uint32_t x63 = (x62 >> 8);
@@ -3239,7 +3241,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)(x67 >> 8);
+  fiat_p256_uint1 x69 = (fiat_p256_uint1)((int64_t)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 47d959fae..70b523744 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_uint128)x1 >> 64);
+  fiat_p256_int1 x2 = (fiat_p256_int1)((fiat_p256_int256)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)(x17 >> 8);
+  fiat_p256_uint1 x19 = (fiat_p256_uint1)((int64_t)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)(x34 >> 8);
+  fiat_p256_uint1 x36 = (fiat_p256_uint1)((int64_t)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)(x51 >> 8);
+  fiat_p256_uint1 x53 = (fiat_p256_uint1)((int64_t)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 113c1db4a..95b6c73d3 100644
--- a/p384_32.c
+++ b/p384_32.c
@@ -14,6 +14,8 @@
 #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;
 
 
 /*
@@ -44,7 +46,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)((uint64_t)x1 >> 32);
+  fiat_p384_int1 x2 = (fiat_p384_int1)((fiat_p384_int128)x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p384_uint1)(0x0 - x2);
@@ -7300,7 +7302,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)(x17 >> 8);
+  fiat_p384_uint1 x19 = (fiat_p384_uint1)((int64_t)x17 >> 8);
   uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff));
   uint32_t x21 = (x19 + x11);
   uint32_t x22 = (x21 >> 8);
@@ -7309,7 +7311,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)(x26 >> 8);
+  fiat_p384_uint1 x28 = (fiat_p384_uint1)((int64_t)x26 >> 8);
   uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff));
   uint32_t x30 = (x28 + x10);
   uint32_t x31 = (x30 >> 8);
@@ -7318,7 +7320,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)(x35 >> 8);
+  fiat_p384_uint1 x37 = (fiat_p384_uint1)((int64_t)x35 >> 8);
   uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff));
   uint32_t x39 = (x37 + x9);
   uint32_t x40 = (x39 >> 8);
@@ -7327,7 +7329,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)(x44 >> 8);
+  fiat_p384_uint1 x46 = (fiat_p384_uint1)((int64_t)x44 >> 8);
   uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff));
   uint32_t x48 = (x46 + x8);
   uint32_t x49 = (x48 >> 8);
@@ -7336,7 +7338,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)(x53 >> 8);
+  fiat_p384_uint1 x55 = (fiat_p384_uint1)((int64_t)x53 >> 8);
   uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff));
   uint32_t x57 = (x55 + x7);
   uint32_t x58 = (x57 >> 8);
@@ -7345,7 +7347,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)(x62 >> 8);
+  fiat_p384_uint1 x64 = (fiat_p384_uint1)((int64_t)x62 >> 8);
   uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff));
   uint32_t x66 = (x64 + x6);
   uint32_t x67 = (x66 >> 8);
@@ -7354,7 +7356,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)(x71 >> 8);
+  fiat_p384_uint1 x73 = (fiat_p384_uint1)((int64_t)x71 >> 8);
   uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff));
   uint32_t x75 = (x73 + x5);
   uint32_t x76 = (x75 >> 8);
@@ -7363,7 +7365,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)(x80 >> 8);
+  fiat_p384_uint1 x82 = (fiat_p384_uint1)((int64_t)x80 >> 8);
   uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
   uint32_t x84 = (x82 + x4);
   uint32_t x85 = (x84 >> 8);
@@ -7372,7 +7374,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)(x89 >> 8);
+  fiat_p384_uint1 x91 = (fiat_p384_uint1)((int64_t)x89 >> 8);
   uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff));
   uint32_t x93 = (x91 + x3);
   uint32_t x94 = (x93 >> 8);
@@ -7381,7 +7383,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)(x98 >> 8);
+  fiat_p384_uint1 x100 = (fiat_p384_uint1)((int64_t)x98 >> 8);
   uint8_t x101 = (uint8_t)(x98 & UINT8_C(0xff));
   uint32_t x102 = (x100 + x2);
   uint32_t x103 = (x102 >> 8);
@@ -7390,7 +7392,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)(x107 >> 8);
+  fiat_p384_uint1 x109 = (fiat_p384_uint1)((int64_t)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 c82ab721c..b4aff4a1e 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_uint128)x1 >> 64);
+  fiat_p384_int1 x2 = (fiat_p384_int1)((fiat_p384_int256)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)(x19 >> 8);
+  fiat_p384_uint1 x21 = (fiat_p384_uint1)((int64_t)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)(x36 >> 8);
+  fiat_p384_uint1 x38 = (fiat_p384_uint1)((int64_t)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)(x53 >> 8);
+  fiat_p384_uint1 x55 = (fiat_p384_uint1)((int64_t)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)(x70 >> 8);
+  fiat_p384_uint1 x72 = (fiat_p384_uint1)((int64_t)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)(x87 >> 8);
+  fiat_p384_uint1 x89 = (fiat_p384_uint1)((int64_t)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 2067de6a0..22d060e3f 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_uint128)x1 >> 64);
+  fiat_p484_int1 x2 = (fiat_p484_int1)((fiat_p484_int256)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)(x20 >> 8);
+  fiat_p484_uint1 x22 = (fiat_p484_uint1)((int64_t)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)(x37 >> 8);
+  fiat_p484_uint1 x39 = (fiat_p484_uint1)((int64_t)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)(x54 >> 8);
+  fiat_p484_uint1 x56 = (fiat_p484_uint1)((int64_t)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)(x71 >> 8);
+  fiat_p484_uint1 x73 = (fiat_p484_uint1)((int64_t)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)(x88 >> 8);
+  fiat_p484_uint1 x90 = (fiat_p484_uint1)((int64_t)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)(x105 >> 8);
+  fiat_p484_uint1 x107 = (fiat_p484_uint1)((int64_t)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)(x120 >> 8);
+  fiat_p484_uint1 x122 = (fiat_p484_uint1)((int64_t)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 d852bb285..5e2fd8a15 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)((uint32_t)x1 >> 30);
+  fiat_p521_int1 x2 = (fiat_p521_int1)((int64_t)x1 >> 30);
   uint32_t x3 = (x1 & UINT32_C(0x3fffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -75,7 +75,7 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u31(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)((uint32_t)x1 >> 31);
+  fiat_p521_int1 x2 = (fiat_p521_int1)((int64_t)x1 >> 31);
   uint32_t x3 = (x1 & UINT32_C(0x7fffffff));
   *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)(x131 >> 8);
+  fiat_p521_uint1 x133 = (fiat_p521_uint1)((int64_t)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)(x183 >> 8);
+  fiat_p521_uint1 x185 = (fiat_p521_uint1)((int64_t)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 e8afff411..386f6241e 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)((uint64_t)x1 >> 58);
+  fiat_p521_int1 x2 = (fiat_p521_int1)((fiat_p521_int128)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)((uint64_t)x1 >> 57);
+  fiat_p521_int1 x2 = (fiat_p521_int1)((fiat_p521_int128)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)(x101 >> 8);
+  fiat_p521_uint1 x103 = (fiat_p521_uint1)((int64_t)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)(x163 >> 8);
+  fiat_p521_uint1 x165 = (fiat_p521_uint1)((int64_t)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 8c3425344..3286161d4 100644
--- a/secp256k1_32.c
+++ b/secp256k1_32.c
@@ -14,6 +14,8 @@
 #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;
 
 
 /*
@@ -44,7 +46,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)((uint64_t)x1 >> 32);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((fiat_secp256k1_int128)x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_secp256k1_uint1)(0x0 - x2);
@@ -3845,7 +3847,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)(x13 >> 8);
+  fiat_secp256k1_uint1 x15 = (fiat_secp256k1_uint1)((int64_t)x13 >> 8);
   uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff));
   uint32_t x17 = (x15 + x7);
   uint32_t x18 = (x17 >> 8);
@@ -3854,7 +3856,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)(x22 >> 8);
+  fiat_secp256k1_uint1 x24 = (fiat_secp256k1_uint1)((int64_t)x22 >> 8);
   uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff));
   uint32_t x26 = (x24 + x6);
   uint32_t x27 = (x26 >> 8);
@@ -3863,7 +3865,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)(x31 >> 8);
+  fiat_secp256k1_uint1 x33 = (fiat_secp256k1_uint1)((int64_t)x31 >> 8);
   uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff));
   uint32_t x35 = (x33 + x5);
   uint32_t x36 = (x35 >> 8);
@@ -3872,7 +3874,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)(x40 >> 8);
+  fiat_secp256k1_uint1 x42 = (fiat_secp256k1_uint1)((int64_t)x40 >> 8);
   uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff));
   uint32_t x44 = (x42 + x4);
   uint32_t x45 = (x44 >> 8);
@@ -3881,7 +3883,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)(x49 >> 8);
+  fiat_secp256k1_uint1 x51 = (fiat_secp256k1_uint1)((int64_t)x49 >> 8);
   uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff));
   uint32_t x53 = (x51 + x3);
   uint32_t x54 = (x53 >> 8);
@@ -3890,7 +3892,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)(x58 >> 8);
+  fiat_secp256k1_uint1 x60 = (fiat_secp256k1_uint1)((int64_t)x58 >> 8);
   uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
   uint32_t x62 = (x60 + x2);
   uint32_t x63 = (x62 >> 8);
@@ -3899,7 +3901,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)(x67 >> 8);
+  fiat_secp256k1_uint1 x69 = (fiat_secp256k1_uint1)((int64_t)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 c78e31453..9abfa7910 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_uint128)x1 >> 64);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((fiat_secp256k1_int256)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)(x17 >> 8);
+  fiat_secp256k1_uint1 x19 = (fiat_secp256k1_uint1)((int64_t)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)(x34 >> 8);
+  fiat_secp256k1_uint1 x36 = (fiat_secp256k1_uint1)((int64_t)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)(x51 >> 8);
+  fiat_secp256k1_uint1 x53 = (fiat_secp256k1_uint1)((int64_t)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 45e0c2eb0..2321d3a3d 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -646,6 +646,9 @@ Module Compilers.
 
         Definition union (t1 t2 : type) : type := of_zrange_relaxed (ZRange.union (to_zrange t1) (to_zrange t2)).
 
+        Definition union_zrange (r : zrange) (t : type) : type
+          := of_zrange_relaxed (ZRange.union r (to_zrange t)).
+
         Fixpoint base_interp (t : base.type) : Set
           := match t with
              | base.type.Z => type
@@ -1100,8 +1103,12 @@ Module Compilers.
                               behavior to shift >= width of the type.
                               We should probably figure out how to not
                               generate these things in the first
-                              place... *)
-                       let '(e', rin') := Zcast_up_if_needed (Some (int.of_zrange_relaxed r[0~>2^offset]%zrange)) (e, rin) in
+                              place...
+
+                              N.B. We must preserve signedness of the
+                              value being shifted, because shift does
+                              not commute with mod. *)
+                       let '(e', rin') := Zcast_up_if_needed (option_map (int.union_zrange r[0~>2^offset]%zrange) rin) (e, rin) in
                        ret (cast_down_if_needed rout (Z_shiftr offset @@ e', rin'))
                      | None => inr ["Invalid right-shift by a non-literal"]%string
                      end
@@ -1117,11 +1124,14 @@ Module Compilers.
                               behavior to shift >= width of the type.
                               We should probably figure out how to not
                               generate these things in the first
-                              place... *)
-                       let rpre_out := int.of_zrange_relaxed r[0~>2^offset]%zrange in
+                              place...
+
+                              N.B. We must preserve signedness of the
+                              value being shifted, because shift does
+                              not commute with mod. *)
                        let rpre_out := match rout with
-                                       | Some rout => Some (ToString.C.int.union rout rpre_out)
-                                       | None => Some rpre_out
+                                       | Some rout => Some (int.union_zrange r[0~>2^offset] rout)
+                                       | None => Some (int.of_zrange_relaxed r[0~>2^offset]%zrange)
                                        end in
                        let '(e', rin') := Zcast_up_if_needed rpre_out (e, rin) in
                        ret (cast_down_if_needed rout (Z_shiftl offset @@ e', rin'))