[ecp] validation with coverity

1 files changed, 552 insertions, 394 deletions

diff --git a/ecp_id_tc26_gost_3410_2012_256_paramSetA.c b/ecp_id_tc26_gost_3410_2012_256_paramSetA.c
index 1528163..9282fb7 100644
--- a/ecp_id_tc26_gost_3410_2012_256_paramSetA.c
+++ b/ecp_id_tc26_gost_3410_2012_256_paramSetA.c
@@ -32,6 +32,10 @@
 typedef uint64_t fe_t[LIMB_CNT];
 typedef uint64_t limb_t;
 
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_TC26_GOST_3410_2012_256_PARAMSETA_NO_ASM
+#endif
+
 #define fe_copy(d, s) memcpy(d, s, sizeof(fe_t))
 #define fe_set_zero(d) memset(d, 0, sizeof(fe_t))
 
@@ -82,18 +86,19 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: unsaturated_solinas --static id_tc26_gost_3410_2012_256_paramSetA 64 5 '2^256 - 617' */
+/* Autogenerated: unsaturated_solinas --static --use-value-barrier id_tc26_gost_3410_2012_256_paramSetA 64 5 '2^256 - 617' */
 /* curve description: id_tc26_gost_3410_2012_256_paramSetA */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: (all) */
 /* n = 5 (from "5") */
 /* s-c = 2^256 - [(1, 617)] (from "2^256 - 617") */
-/* tight_bounds_multiplier = 1.1 (from "") */
+/* tight_bounds_multiplier = 1 (from "") */
 /*  */
 /* Computed values: */
 /* carry_chain = [0, 1, 2, 3, 4, 0, 1] */
 /* eval z = z[0] + (z[1] << 52) + (z[2] << 103) + (z[3] << 154) + (z[4] << 205) */
 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
+/* balance = [0x1ffffffffffb2e, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */
 
 #include <stdint.h>
 typedef unsigned char fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1;
@@ -105,6 +110,17 @@ typedef unsigned __int128 fiat_id_tc26_gost_3410_2012_256_paramSetA_uint128;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_256_PARAMSETA_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint64_t
+fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u64(uint64_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u64(x) (x)
+#endif
+
 /*
  * The function fiat_id_tc26_gost_3410_2012_256_paramSetA_addcarryx_u52 is an addition with carry.
  * Postconditions:
@@ -238,7 +254,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_cmovznz_u64(
     x1 = (!(!arg1));
     x2 = ((fiat_id_tc26_gost_3410_2012_256_paramSetA_int1)(0x0 - x1) &
           UINT64_C(0xffffffffffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u64(x2) &
+           arg3) |
+          (fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u64((~x2)) &
+           arg2));
     *out1 = x3;
 }
 
@@ -248,10 +267,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_cmovznz_u64(
  *   eval out1 mod m = (eval arg1 * eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- *   arg2: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
+ *   arg2: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(
     uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
@@ -412,9 +431,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(
  *   eval out1 mod m = (eval arg1 * eval arg1) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_square(
     uint64_t out1[5], const uint64_t arg1[5]) {
@@ -539,9 +558,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_square(
  *   eval out1 mod m = eval arg1 mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry(
     uint64_t out1[5], const uint64_t arg1[5]) {
@@ -584,10 +603,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry(
  *   eval out1 mod m = (eval arg1 + eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- *   arg2: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
+ *   arg2: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_add(
     uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
@@ -614,10 +633,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_add(
  *   eval out1 mod m = (eval arg1 - eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- *   arg2: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
+ *   arg2: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_sub(
     uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
@@ -644,9 +663,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_sub(
  *   eval out1 mod m = -eval arg1 mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ *   out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_opp(
     uint64_t out1[5], const uint64_t arg1[5]) {
@@ -710,7 +729,7 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_selectznz(
  *   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  * 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 ~> 0xff]]
  */
@@ -741,70 +760,70 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
     uint64_t x23;
     uint64_t x24;
     uint64_t x25;
-    uint64_t x26;
-    uint8_t x27;
-    uint64_t x28;
-    uint8_t x29;
-    uint64_t x30;
-    uint8_t x31;
-    uint64_t x32;
-    uint8_t x33;
-    uint64_t x34;
-    uint8_t x35;
+    uint8_t x26;
+    uint64_t x27;
+    uint8_t x28;
+    uint64_t x29;
+    uint8_t x30;
+    uint64_t x31;
+    uint8_t x32;
+    uint64_t x33;
+    uint8_t x34;
+    uint64_t x35;
     uint8_t x36;
     uint8_t x37;
     uint64_t x38;
-    uint64_t x39;
-    uint8_t x40;
-    uint64_t x41;
-    uint8_t x42;
-    uint64_t x43;
-    uint8_t x44;
-    uint64_t x45;
-    uint8_t x46;
-    uint64_t x47;
-    uint8_t x48;
+    uint8_t x39;
+    uint64_t x40;
+    uint8_t x41;
+    uint64_t x42;
+    uint8_t x43;
+    uint64_t x44;
+    uint8_t x45;
+    uint64_t x46;
+    uint8_t x47;
+    uint64_t x48;
     uint8_t x49;
     uint8_t x50;
     uint64_t x51;
-    uint64_t x52;
-    uint8_t x53;
-    uint64_t x54;
-    uint8_t x55;
-    uint64_t x56;
-    uint8_t x57;
-    uint64_t x58;
-    uint8_t x59;
-    uint64_t x60;
-    uint8_t x61;
-    uint64_t x62;
-    uint8_t x63;
+    uint8_t x52;
+    uint64_t x53;
+    uint8_t x54;
+    uint64_t x55;
+    uint8_t x56;
+    uint64_t x57;
+    uint8_t x58;
+    uint64_t x59;
+    uint8_t x60;
+    uint64_t x61;
+    uint8_t x62;
+    uint64_t x63;
     uint8_t x64;
     uint8_t x65;
     uint64_t x66;
-    uint64_t x67;
-    uint8_t x68;
-    uint64_t x69;
-    uint8_t x70;
-    uint64_t x71;
-    uint8_t x72;
-    uint64_t x73;
-    uint8_t x74;
-    uint64_t x75;
-    uint8_t x76;
+    uint8_t x67;
+    uint64_t x68;
+    uint8_t x69;
+    uint64_t x70;
+    uint8_t x71;
+    uint64_t x72;
+    uint8_t x73;
+    uint64_t x74;
+    uint8_t x75;
+    uint64_t x76;
     uint8_t x77;
     uint8_t x78;
     uint64_t x79;
-    uint64_t x80;
-    uint8_t x81;
-    uint64_t x82;
-    uint8_t x83;
-    uint64_t x84;
-    uint8_t x85;
-    uint64_t x86;
-    uint8_t x87;
-    uint64_t x88;
-    uint8_t x89;
+    uint8_t x80;
+    uint64_t x81;
+    uint8_t x82;
+    uint64_t x83;
+    uint8_t x84;
+    uint64_t x85;
+    uint8_t x86;
+    uint64_t x87;
+    uint8_t x88;
+    uint64_t x89;
     uint8_t x90;
     uint8_t x91;
     fiat_id_tc26_gost_3410_2012_256_paramSetA_subborrowx_u52(
@@ -833,104 +852,104 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
     x23 = (x18 << 2);
     x24 = (x16 << 7);
     x25 = (x14 << 4);
-    x26 = (x12 >> 8);
-    x27 = (uint8_t)(x12 & UINT8_C(0xff));
-    x28 = (x26 >> 8);
-    x29 = (uint8_t)(x26 & UINT8_C(0xff));
-    x30 = (x28 >> 8);
-    x31 = (uint8_t)(x28 & UINT8_C(0xff));
-    x32 = (x30 >> 8);
-    x33 = (uint8_t)(x30 & UINT8_C(0xff));
-    x34 = (x32 >> 8);
-    x35 = (uint8_t)(x32 & UINT8_C(0xff));
-    x36 = (uint8_t)(x34 >> 8);
-    x37 = (uint8_t)(x34 & UINT8_C(0xff));
-    x38 = (x36 + x25);
-    x39 = (x38 >> 8);
-    x40 = (uint8_t)(x38 & UINT8_C(0xff));
-    x41 = (x39 >> 8);
-    x42 = (uint8_t)(x39 & UINT8_C(0xff));
-    x43 = (x41 >> 8);
-    x44 = (uint8_t)(x41 & UINT8_C(0xff));
-    x45 = (x43 >> 8);
-    x46 = (uint8_t)(x43 & UINT8_C(0xff));
-    x47 = (x45 >> 8);
-    x48 = (uint8_t)(x45 & UINT8_C(0xff));
-    x49 = (uint8_t)(x47 >> 8);
-    x50 = (uint8_t)(x47 & UINT8_C(0xff));
-    x51 = (x49 + x24);
-    x52 = (x51 >> 8);
-    x53 = (uint8_t)(x51 & UINT8_C(0xff));
-    x54 = (x52 >> 8);
-    x55 = (uint8_t)(x52 & UINT8_C(0xff));
-    x56 = (x54 >> 8);
-    x57 = (uint8_t)(x54 & UINT8_C(0xff));
-    x58 = (x56 >> 8);
-    x59 = (uint8_t)(x56 & UINT8_C(0xff));
-    x60 = (x58 >> 8);
-    x61 = (uint8_t)(x58 & UINT8_C(0xff));
-    x62 = (x60 >> 8);
-    x63 = (uint8_t)(x60 & UINT8_C(0xff));
-    x64 = (uint8_t)(x62 >> 8);
-    x65 = (uint8_t)(x62 & UINT8_C(0xff));
-    x66 = (x64 + x23);
-    x67 = (x66 >> 8);
-    x68 = (uint8_t)(x66 & UINT8_C(0xff));
-    x69 = (x67 >> 8);
-    x70 = (uint8_t)(x67 & UINT8_C(0xff));
-    x71 = (x69 >> 8);
-    x72 = (uint8_t)(x69 & UINT8_C(0xff));
-    x73 = (x71 >> 8);
-    x74 = (uint8_t)(x71 & UINT8_C(0xff));
-    x75 = (x73 >> 8);
-    x76 = (uint8_t)(x73 & UINT8_C(0xff));
-    x77 = (uint8_t)(x75 >> 8);
-    x78 = (uint8_t)(x75 & UINT8_C(0xff));
-    x79 = (x77 + x22);
-    x80 = (x79 >> 8);
-    x81 = (uint8_t)(x79 & UINT8_C(0xff));
-    x82 = (x80 >> 8);
-    x83 = (uint8_t)(x80 & UINT8_C(0xff));
-    x84 = (x82 >> 8);
-    x85 = (uint8_t)(x82 & UINT8_C(0xff));
-    x86 = (x84 >> 8);
-    x87 = (uint8_t)(x84 & UINT8_C(0xff));
-    x88 = (x86 >> 8);
-    x89 = (uint8_t)(x86 & UINT8_C(0xff));
-    x90 = (uint8_t)(x88 >> 8);
-    x91 = (uint8_t)(x88 & UINT8_C(0xff));
-    out1[0] = x27;
-    out1[1] = x29;
-    out1[2] = x31;
-    out1[3] = x33;
-    out1[4] = x35;
-    out1[5] = x37;
-    out1[6] = x40;
-    out1[7] = x42;
-    out1[8] = x44;
-    out1[9] = x46;
-    out1[10] = x48;
-    out1[11] = x50;
-    out1[12] = x53;
-    out1[13] = x55;
-    out1[14] = x57;
-    out1[15] = x59;
-    out1[16] = x61;
-    out1[17] = x63;
-    out1[18] = x65;
-    out1[19] = x68;
-    out1[20] = x70;
-    out1[21] = x72;
-    out1[22] = x74;
-    out1[23] = x76;
-    out1[24] = x78;
-    out1[25] = x81;
-    out1[26] = x83;
-    out1[27] = x85;
-    out1[28] = x87;
-    out1[29] = x89;
-    out1[30] = x91;
-    out1[31] = x90;
+    x26 = (uint8_t)(x12 & UINT8_C(0xff));
+    x27 = (x12 >> 8);
+    x28 = (uint8_t)(x27 & UINT8_C(0xff));
+    x29 = (x27 >> 8);
+    x30 = (uint8_t)(x29 & UINT8_C(0xff));
+    x31 = (x29 >> 8);
+    x32 = (uint8_t)(x31 & UINT8_C(0xff));
+    x33 = (x31 >> 8);
+    x34 = (uint8_t)(x33 & UINT8_C(0xff));
+    x35 = (x33 >> 8);
+    x36 = (uint8_t)(x35 & UINT8_C(0xff));
+    x37 = (uint8_t)(x35 >> 8);
+    x38 = (x25 + (uint64_t)x37);
+    x39 = (uint8_t)(x38 & UINT8_C(0xff));
+    x40 = (x38 >> 8);
+    x41 = (uint8_t)(x40 & UINT8_C(0xff));
+    x42 = (x40 >> 8);
+    x43 = (uint8_t)(x42 & UINT8_C(0xff));
+    x44 = (x42 >> 8);
+    x45 = (uint8_t)(x44 & UINT8_C(0xff));
+    x46 = (x44 >> 8);
+    x47 = (uint8_t)(x46 & UINT8_C(0xff));
+    x48 = (x46 >> 8);
+    x49 = (uint8_t)(x48 & UINT8_C(0xff));
+    x50 = (uint8_t)(x48 >> 8);
+    x51 = (x24 + (uint64_t)x50);
+    x52 = (uint8_t)(x51 & UINT8_C(0xff));
+    x53 = (x51 >> 8);
+    x54 = (uint8_t)(x53 & UINT8_C(0xff));
+    x55 = (x53 >> 8);
+    x56 = (uint8_t)(x55 & UINT8_C(0xff));
+    x57 = (x55 >> 8);
+    x58 = (uint8_t)(x57 & UINT8_C(0xff));
+    x59 = (x57 >> 8);
+    x60 = (uint8_t)(x59 & UINT8_C(0xff));
+    x61 = (x59 >> 8);
+    x62 = (uint8_t)(x61 & UINT8_C(0xff));
+    x63 = (x61 >> 8);
+    x64 = (uint8_t)(x63 & UINT8_C(0xff));
+    x65 = (uint8_t)(x63 >> 8);
+    x66 = (x23 + (uint64_t)x65);
+    x67 = (uint8_t)(x66 & UINT8_C(0xff));
+    x68 = (x66 >> 8);
+    x69 = (uint8_t)(x68 & UINT8_C(0xff));
+    x70 = (x68 >> 8);
+    x71 = (uint8_t)(x70 & UINT8_C(0xff));
+    x72 = (x70 >> 8);
+    x73 = (uint8_t)(x72 & UINT8_C(0xff));
+    x74 = (x72 >> 8);
+    x75 = (uint8_t)(x74 & UINT8_C(0xff));
+    x76 = (x74 >> 8);
+    x77 = (uint8_t)(x76 & UINT8_C(0xff));
+    x78 = (uint8_t)(x76 >> 8);
+    x79 = (x22 + (uint64_t)x78);
+    x80 = (uint8_t)(x79 & UINT8_C(0xff));
+    x81 = (x79 >> 8);
+    x82 = (uint8_t)(x81 & UINT8_C(0xff));
+    x83 = (x81 >> 8);
+    x84 = (uint8_t)(x83 & UINT8_C(0xff));
+    x85 = (x83 >> 8);
+    x86 = (uint8_t)(x85 & UINT8_C(0xff));
+    x87 = (x85 >> 8);
+    x88 = (uint8_t)(x87 & UINT8_C(0xff));
+    x89 = (x87 >> 8);
+    x90 = (uint8_t)(x89 & UINT8_C(0xff));
+    x91 = (uint8_t)(x89 >> 8);
+    out1[0] = x26;
+    out1[1] = x28;
+    out1[2] = x30;
+    out1[3] = x32;
+    out1[4] = x34;
+    out1[5] = x36;
+    out1[6] = x39;
+    out1[7] = x41;
+    out1[8] = x43;
+    out1[9] = x45;
+    out1[10] = x47;
+    out1[11] = x49;
+    out1[12] = x52;
+    out1[13] = x54;
+    out1[14] = x56;
+    out1[15] = x58;
+    out1[16] = x60;
+    out1[17] = x62;
+    out1[18] = x64;
+    out1[19] = x67;
+    out1[20] = x69;
+    out1[21] = x71;
+    out1[22] = x73;
+    out1[23] = x75;
+    out1[24] = x77;
+    out1[25] = x80;
+    out1[26] = x82;
+    out1[27] = x84;
+    out1[28] = x86;
+    out1[29] = x88;
+    out1[30] = x90;
+    out1[31] = x91;
 }
 
 /*
@@ -941,7 +960,7 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
  * Input Bounds:
  *   arg1: [[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 ~> 0xff]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ *   out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     uint64_t out1[5], const uint8_t arg1[32]) {
@@ -978,22 +997,44 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     uint64_t x31;
     uint8_t x32;
     uint64_t x33;
-    uint8_t x34;
+    uint64_t x34;
     uint64_t x35;
     uint64_t x36;
     uint64_t x37;
     uint64_t x38;
     uint64_t x39;
-    uint64_t x40;
-    fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1 x41;
+    uint8_t x40;
+    uint64_t x41;
     uint64_t x42;
     uint64_t x43;
-    uint8_t x44;
+    uint64_t x44;
     uint64_t x45;
     uint64_t x46;
-    uint8_t x47;
-    uint64_t x48;
+    uint64_t x47;
+    fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1 x48;
     uint64_t x49;
+    uint64_t x50;
+    uint64_t x51;
+    uint64_t x52;
+    uint64_t x53;
+    uint64_t x54;
+    uint64_t x55;
+    uint64_t x56;
+    uint8_t x57;
+    uint64_t x58;
+    uint64_t x59;
+    uint64_t x60;
+    uint64_t x61;
+    uint64_t x62;
+    uint64_t x63;
+    uint64_t x64;
+    uint8_t x65;
+    uint64_t x66;
+    uint64_t x67;
+    uint64_t x68;
+    uint64_t x69;
+    uint64_t x70;
+    uint64_t x71;
     x1 = ((uint64_t)(arg1[31]) << 43);
     x2 = ((uint64_t)(arg1[30]) << 35);
     x3 = ((uint64_t)(arg1[29]) << 27);
@@ -1026,28 +1067,50 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     x30 = ((uint64_t)(arg1[2]) << 16);
     x31 = ((uint64_t)(arg1[1]) << 8);
     x32 = (arg1[0]);
-    x33 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + x26))))));
-    x34 = (uint8_t)(x33 >> 52);
-    x35 = (x33 & UINT64_C(0xfffffffffffff));
-    x36 = (x6 + (x5 + (x4 + (x3 + (x2 + x1)))));
-    x37 = (x12 + (x11 + (x10 + (x9 + (x8 + x7)))));
-    x38 = (x19 + (x18 + (x17 + (x16 + (x15 + (x14 + x13))))));
-    x39 = (x25 + (x24 + (x23 + (x22 + (x21 + x20)))));
-    x40 = (x34 + x39);
-    x41 = (fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1)(x40 >> 51);
-    x42 = (x40 & UINT64_C(0x7ffffffffffff));
-    x43 = (x41 + x38);
-    x44 = (uint8_t)(x43 >> 51);
-    x45 = (x43 & UINT64_C(0x7ffffffffffff));
-    x46 = (x44 + x37);
-    x47 = (uint8_t)(x46 >> 51);
-    x48 = (x46 & UINT64_C(0x7ffffffffffff));
-    x49 = (x47 + x36);
-    out1[0] = x35;
-    out1[1] = x42;
-    out1[2] = x45;
-    out1[3] = x48;
-    out1[4] = x49;
+    x33 = (x31 + (uint64_t)x32);
+    x34 = (x30 + x33);
+    x35 = (x29 + x34);
+    x36 = (x28 + x35);
+    x37 = (x27 + x36);
+    x38 = (x26 + x37);
+    x39 = (x38 & UINT64_C(0xfffffffffffff));
+    x40 = (uint8_t)(x38 >> 52);
+    x41 = (x25 + (uint64_t)x40);
+    x42 = (x24 + x41);
+    x43 = (x23 + x42);
+    x44 = (x22 + x43);
+    x45 = (x21 + x44);
+    x46 = (x20 + x45);
+    x47 = (x46 & UINT64_C(0x7ffffffffffff));
+    x48 = (fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1)(x46 >> 51);
+    x49 = (x19 + (uint64_t)x48);
+    x50 = (x18 + x49);
+    x51 = (x17 + x50);
+    x52 = (x16 + x51);
+    x53 = (x15 + x52);
+    x54 = (x14 + x53);
+    x55 = (x13 + x54);
+    x56 = (x55 & UINT64_C(0x7ffffffffffff));
+    x57 = (uint8_t)(x55 >> 51);
+    x58 = (x12 + (uint64_t)x57);
+    x59 = (x11 + x58);
+    x60 = (x10 + x59);
+    x61 = (x9 + x60);
+    x62 = (x8 + x61);
+    x63 = (x7 + x62);
+    x64 = (x63 & UINT64_C(0x7ffffffffffff));
+    x65 = (uint8_t)(x63 >> 51);
+    x66 = (x6 + (uint64_t)x65);
+    x67 = (x5 + x66);
+    x68 = (x4 + x67);
+    x69 = (x3 + x68);
+    x70 = (x2 + x69);
+    x71 = (x1 + x70);
+    out1[0] = x39;
+    out1[1] = x47;
+    out1[2] = x56;
+    out1[3] = x64;
+    out1[4] = x71;
 }
 
 /* END verbatim fiat code */
@@ -3455,7 +3518,7 @@ static void scalar_wnaf(int8_t out[257], const unsigned char in[32]) {
 }
 
 /*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
  * NB: not constant time
  */
 static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[32],
@@ -3463,7 +3526,7 @@ static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[32],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[257] = {0};
     int8_t bnaf[257] = {0};
-    pt_prj_t Q;
+    pt_prj_t Q = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -3537,7 +3600,7 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[32],
                            const pt_aff_t *P) {
     int i, j, d, diff, is_neg;
     int8_t rnaf[52] = {0};
-    pt_prj_t Q, lut;
+    pt_prj_t Q = {0}, lut = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -3625,8 +3688,8 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[32],
 static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[52] = {0};
-    pt_prj_t Q, R;
-    pt_aff_t lut;
+    pt_prj_t Q = {0}, R = {0};
+    pt_aff_t lut = {0};
 
     scalar_rwnaf(rnaf, scalar);
 
@@ -3698,6 +3761,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(out->Y, Q.Y, Q.Z);
 }
 
+/*-
+ * Wrapper: simultaneous scalar mutiplication.
+ * outx, outy := a * G + b * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
 static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
                           const unsigned char a[32], const unsigned char b[32],
                           const unsigned char inx[32],
@@ -3713,6 +3782,11 @@ static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
     fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(outy, P.Y);
 }
 
+/*-
+ * Wrapper: fixed scalar mutiplication.
+ * outx, outy := scalar * G
+ * Everything is LE byte ordering.
+ */
 static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
                         const unsigned char scalar[32]) {
     pt_aff_t P;
@@ -3723,6 +3797,12 @@ static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
     fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(outy, P.Y);
 }
 
+/*-
+ * Wrapper: variable point scalar mutiplication.
+ * outx, outy := scalar * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
 static void point_mul(unsigned char outx[32], unsigned char outy[32],
                       const unsigned char scalar[32],
                       const unsigned char inx[32],
@@ -3740,8 +3820,13 @@ static void point_mul(unsigned char outx[32], unsigned char outy[32],
 
 #include <openssl/ec.h>
 
+/* the zero field element */
 static const unsigned char const_zb[32] = {0};
 
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
     int
     point_mul_two_id_tc26_gost_3410_2012_256_paramSetA(
         const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
@@ -3780,6 +3865,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_tc26_gost_3410_2012_256_paramSetA(const EC_GROUP *group,
                                                    EC_POINT *r,
@@ -3819,6 +3908,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_tc26_gost_3410_2012_256_paramSetA(const EC_GROUP *group,
                                                      EC_POINT *r,
@@ -3865,6 +3958,10 @@ err:
 typedef uint32_t fe_t[LIMB_CNT];
 typedef uint32_t limb_t;
 
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_TC26_GOST_3410_2012_256_PARAMSETA_NO_ASM
+#endif
+
 #define fe_copy(d, s) memcpy(d, s, sizeof(fe_t))
 #define fe_set_zero(d) memset(d, 0, sizeof(fe_t))
 
@@ -3915,18 +4012,19 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: unsaturated_solinas --static id_tc26_gost_3410_2012_256_paramSetA 32 '(auto)' '2^256 - 617' */
+/* Autogenerated: unsaturated_solinas --static --use-value-barrier id_tc26_gost_3410_2012_256_paramSetA 32 '(auto)' '2^256 - 617' */
 /* curve description: id_tc26_gost_3410_2012_256_paramSetA */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: (all) */
 /* n = 11 (from "(auto)") */
 /* s-c = 2^256 - [(1, 617)] (from "2^256 - 617") */
-/* tight_bounds_multiplier = 1.1 (from "") */
+/* tight_bounds_multiplier = 1 (from "") */
 /*  */
 /* Computed values: */
 /* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 0, 1] */
 /* eval z = z[0] + (z[1] << 24) + (z[2] << 47) + (z[3] << 70) + (z[4] << 94) + (z[5] << 117) + (z[6] << 140) + (z[7] << 163) + (z[8] << 187) + (z[9] << 210) + (z[10] << 233) */
 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
+/* balance = [0x1fffb2e, 0xfffffe, 0xfffffe, 0x1fffffe, 0xfffffe, 0xfffffe, 0xfffffe, 0x1fffffe, 0xfffffe, 0xfffffe, 0xfffffe] */
 
 #include <stdint.h>
 typedef unsigned char fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1;
@@ -3936,6 +4034,17 @@ typedef signed char fiat_id_tc26_gost_3410_2012_256_paramSetA_int1;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_256_PARAMSETA_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint32_t
+fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u32(uint32_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u32(x) (x)
+#endif
+
 /*
  * The function fiat_id_tc26_gost_3410_2012_256_paramSetA_addcarryx_u24 is an addition with carry.
  * Postconditions:
@@ -4069,7 +4178,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_cmovznz_u32(
     x1 = (!(!arg1));
     x2 = ((fiat_id_tc26_gost_3410_2012_256_paramSetA_int1)(0x0 - x1) &
           UINT32_C(0xffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u32(x2) &
+           arg3) |
+          (fiat_id_tc26_gost_3410_2012_256_paramSetA_value_barrier_u32((~x2)) &
+           arg2));
     *out1 = x3;
 }
 
@@ -4079,10 +4191,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_cmovznz_u32(
  *   eval out1 mod m = (eval arg1 * eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
- *   arg2: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   arg1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
+ *   arg2: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   out1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(
     uint32_t out1[11], const uint32_t arg1[11], const uint32_t arg2[11]) {
@@ -4482,9 +4594,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(
  *   eval out1 mod m = (eval arg1 * eval arg1) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   arg1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   out1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_square(
     uint32_t out1[11], const uint32_t arg1[11]) {
@@ -4781,9 +4893,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_square(
  *   eval out1 mod m = eval arg1 mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   arg1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   out1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry(
     uint32_t out1[11], const uint32_t arg1[11]) {
@@ -4856,10 +4968,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_carry(
  *   eval out1 mod m = (eval arg1 + eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
- *   arg2: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   arg1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
+ *   arg2: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   out1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_add(
     uint32_t out1[11], const uint32_t arg1[11], const uint32_t arg2[11]) {
@@ -4904,10 +5016,10 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_add(
  *   eval out1 mod m = (eval arg1 - eval arg2) mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
- *   arg2: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   arg1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
+ *   arg2: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   out1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_sub(
     uint32_t out1[11], const uint32_t arg1[11], const uint32_t arg2[11]) {
@@ -4952,9 +5064,9 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_sub(
  *   eval out1 mod m = -eval arg1 mod m
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   arg1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x34ccccb], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664], [0x0 ~> 0x1a66664]]
+ *   out1: [[0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x3000000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000], [0x0 ~> 0x1800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_opp(
     uint32_t out1[11], const uint32_t arg1[11]) {
@@ -5060,7 +5172,7 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_selectznz(
  *   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
  *
  * Input Bounds:
- *   arg1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   arg1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  * 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 ~> 0xff]]
  */
@@ -5120,76 +5232,75 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
     uint32_t x52;
     uint32_t x53;
     uint32_t x54;
-    uint32_t x55;
-    uint8_t x56;
+    uint8_t x55;
+    uint32_t x56;
     uint8_t x57;
     uint8_t x58;
     uint8_t x59;
     uint32_t x60;
     uint8_t x61;
     uint8_t x62;
-    uint8_t x63;
-    uint32_t x64;
+    uint32_t x63;
+    uint8_t x64;
     uint32_t x65;
     uint8_t x66;
     uint32_t x67;
     uint8_t x68;
     uint8_t x69;
-    uint8_t x70;
-    uint32_t x71;
+    uint32_t x70;
+    uint8_t x71;
     uint32_t x72;
     uint8_t x73;
     uint32_t x74;
     uint8_t x75;
     uint8_t x76;
-    uint8_t x77;
-    uint32_t x78;
+    uint32_t x77;
+    uint8_t x78;
     uint32_t x79;
     uint8_t x80;
     uint32_t x81;
     uint8_t x82;
     uint8_t x83;
-    uint8_t x84;
-    uint32_t x85;
+    uint32_t x84;
+    uint8_t x85;
     uint32_t x86;
     uint8_t x87;
     uint32_t x88;
     uint8_t x89;
     uint8_t x90;
-    uint8_t x91;
-    uint32_t x92;
+    uint32_t x91;
+    uint8_t x92;
     uint32_t x93;
     uint8_t x94;
     uint32_t x95;
     uint8_t x96;
     uint8_t x97;
-    uint8_t x98;
-    uint32_t x99;
+    uint32_t x98;
+    uint8_t x99;
     uint32_t x100;
     uint8_t x101;
     uint32_t x102;
     uint8_t x103;
     uint8_t x104;
-    uint8_t x105;
-    uint32_t x106;
+    uint32_t x105;
+    uint8_t x106;
     uint32_t x107;
     uint8_t x108;
     uint32_t x109;
     uint8_t x110;
     uint8_t x111;
-    uint8_t x112;
-    uint32_t x113;
+    uint32_t x112;
+    uint8_t x113;
     uint32_t x114;
     uint8_t x115;
     uint32_t x116;
     uint8_t x117;
     fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1 x118;
-    uint8_t x119;
-    uint32_t x120;
+    uint32_t x119;
+    uint8_t x120;
     uint32_t x121;
     uint8_t x122;
     uint8_t x123;
-    uint8_t x124;
     fiat_id_tc26_gost_3410_2012_256_paramSetA_subborrowx_u24(
         &x1, &x2, 0x0, (arg1[0]), UINT32_C(0xfffd97));
     fiat_id_tc26_gost_3410_2012_256_paramSetA_subborrowx_u23(
@@ -5245,107 +5356,106 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
     x52 = (x32 << 6);
     x53 = (x30 << 6);
     x54 = (x28 << 7);
-    x55 = (x24 >> 8);
-    x56 = (uint8_t)(x24 & UINT8_C(0xff));
-    x57 = (uint8_t)(x55 >> 8);
-    x58 = (uint8_t)(x55 & UINT8_C(0xff));
-    x59 = (uint8_t)(x57 & UINT8_C(0xff));
+    x55 = (uint8_t)(x24 & UINT8_C(0xff));
+    x56 = (x24 >> 8);
+    x57 = (uint8_t)(x56 & UINT8_C(0xff));
+    x58 = (uint8_t)(x56 >> 8);
+    x59 = (uint8_t)(x26 & UINT8_C(0xff));
     x60 = (x26 >> 8);
-    x61 = (uint8_t)(x26 & UINT8_C(0xff));
+    x61 = (uint8_t)(x60 & UINT8_C(0xff));
     x62 = (uint8_t)(x60 >> 8);
-    x63 = (uint8_t)(x60 & UINT8_C(0xff));
-    x64 = (x62 + x54);
-    x65 = (x64 >> 8);
-    x66 = (uint8_t)(x64 & UINT8_C(0xff));
+    x63 = (x54 + (uint32_t)x62);
+    x64 = (uint8_t)(x63 & UINT8_C(0xff));
+    x65 = (x63 >> 8);
+    x66 = (uint8_t)(x65 & UINT8_C(0xff));
     x67 = (x65 >> 8);
-    x68 = (uint8_t)(x65 & UINT8_C(0xff));
+    x68 = (uint8_t)(x67 & UINT8_C(0xff));
     x69 = (uint8_t)(x67 >> 8);
-    x70 = (uint8_t)(x67 & UINT8_C(0xff));
-    x71 = (x69 + x53);
-    x72 = (x71 >> 8);
-    x73 = (uint8_t)(x71 & UINT8_C(0xff));
+    x70 = (x53 + (uint32_t)x69);
+    x71 = (uint8_t)(x70 & UINT8_C(0xff));
+    x72 = (x70 >> 8);
+    x73 = (uint8_t)(x72 & UINT8_C(0xff));
     x74 = (x72 >> 8);
-    x75 = (uint8_t)(x72 & UINT8_C(0xff));
+    x75 = (uint8_t)(x74 & UINT8_C(0xff));
     x76 = (uint8_t)(x74 >> 8);
-    x77 = (uint8_t)(x74 & UINT8_C(0xff));
-    x78 = (x76 + x52);
-    x79 = (x78 >> 8);
-    x80 = (uint8_t)(x78 & UINT8_C(0xff));
+    x77 = (x52 + (uint32_t)x76);
+    x78 = (uint8_t)(x77 & UINT8_C(0xff));
+    x79 = (x77 >> 8);
+    x80 = (uint8_t)(x79 & UINT8_C(0xff));
     x81 = (x79 >> 8);
-    x82 = (uint8_t)(x79 & UINT8_C(0xff));
+    x82 = (uint8_t)(x81 & UINT8_C(0xff));
     x83 = (uint8_t)(x81 >> 8);
-    x84 = (uint8_t)(x81 & UINT8_C(0xff));
-    x85 = (x83 + x51);
-    x86 = (x85 >> 8);
-    x87 = (uint8_t)(x85 & UINT8_C(0xff));
+    x84 = (x51 + (uint32_t)x83);
+    x85 = (uint8_t)(x84 & UINT8_C(0xff));
+    x86 = (x84 >> 8);
+    x87 = (uint8_t)(x86 & UINT8_C(0xff));
     x88 = (x86 >> 8);
-    x89 = (uint8_t)(x86 & UINT8_C(0xff));
+    x89 = (uint8_t)(x88 & UINT8_C(0xff));
     x90 = (uint8_t)(x88 >> 8);
-    x91 = (uint8_t)(x88 & UINT8_C(0xff));
-    x92 = (x90 + x50);
-    x93 = (x92 >> 8);
-    x94 = (uint8_t)(x92 & UINT8_C(0xff));
+    x91 = (x50 + (uint32_t)x90);
+    x92 = (uint8_t)(x91 & UINT8_C(0xff));
+    x93 = (x91 >> 8);
+    x94 = (uint8_t)(x93 & UINT8_C(0xff));
     x95 = (x93 >> 8);
-    x96 = (uint8_t)(x93 & UINT8_C(0xff));
+    x96 = (uint8_t)(x95 & UINT8_C(0xff));
     x97 = (uint8_t)(x95 >> 8);
-    x98 = (uint8_t)(x95 & UINT8_C(0xff));
-    x99 = (x97 + x49);
-    x100 = (x99 >> 8);
-    x101 = (uint8_t)(x99 & UINT8_C(0xff));
+    x98 = (x49 + (uint32_t)x97);
+    x99 = (uint8_t)(x98 & UINT8_C(0xff));
+    x100 = (x98 >> 8);
+    x101 = (uint8_t)(x100 & UINT8_C(0xff));
     x102 = (x100 >> 8);
-    x103 = (uint8_t)(x100 & UINT8_C(0xff));
+    x103 = (uint8_t)(x102 & UINT8_C(0xff));
     x104 = (uint8_t)(x102 >> 8);
-    x105 = (uint8_t)(x102 & UINT8_C(0xff));
-    x106 = (x104 + x48);
-    x107 = (x106 >> 8);
-    x108 = (uint8_t)(x106 & UINT8_C(0xff));
+    x105 = (x48 + (uint32_t)x104);
+    x106 = (uint8_t)(x105 & UINT8_C(0xff));
+    x107 = (x105 >> 8);
+    x108 = (uint8_t)(x107 & UINT8_C(0xff));
     x109 = (x107 >> 8);
-    x110 = (uint8_t)(x107 & UINT8_C(0xff));
+    x110 = (uint8_t)(x109 & UINT8_C(0xff));
     x111 = (uint8_t)(x109 >> 8);
-    x112 = (uint8_t)(x109 & UINT8_C(0xff));
-    x113 = (x111 + x47);
-    x114 = (x113 >> 8);
-    x115 = (uint8_t)(x113 & UINT8_C(0xff));
+    x112 = (x47 + (uint32_t)x111);
+    x113 = (uint8_t)(x112 & UINT8_C(0xff));
+    x114 = (x112 >> 8);
+    x115 = (uint8_t)(x114 & UINT8_C(0xff));
     x116 = (x114 >> 8);
-    x117 = (uint8_t)(x114 & UINT8_C(0xff));
+    x117 = (uint8_t)(x116 & UINT8_C(0xff));
     x118 = (fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1)(x116 >> 8);
-    x119 = (uint8_t)(x116 & UINT8_C(0xff));
-    x120 = (x118 + x46);
-    x121 = (x120 >> 8);
-    x122 = (uint8_t)(x120 & UINT8_C(0xff));
+    x119 = (x46 + (uint32_t)x118);
+    x120 = (uint8_t)(x119 & UINT8_C(0xff));
+    x121 = (x119 >> 8);
+    x122 = (uint8_t)(x121 & UINT8_C(0xff));
     x123 = (uint8_t)(x121 >> 8);
-    x124 = (uint8_t)(x121 & UINT8_C(0xff));
-    out1[0] = x56;
-    out1[1] = x58;
-    out1[2] = x59;
-    out1[3] = x61;
-    out1[4] = x63;
-    out1[5] = x66;
-    out1[6] = x68;
-    out1[7] = x70;
-    out1[8] = x73;
-    out1[9] = x75;
-    out1[10] = x77;
-    out1[11] = x80;
-    out1[12] = x82;
-    out1[13] = x84;
-    out1[14] = x87;
-    out1[15] = x89;
-    out1[16] = x91;
-    out1[17] = x94;
-    out1[18] = x96;
-    out1[19] = x98;
-    out1[20] = x101;
-    out1[21] = x103;
-    out1[22] = x105;
-    out1[23] = x108;
-    out1[24] = x110;
-    out1[25] = x112;
-    out1[26] = x115;
-    out1[27] = x117;
-    out1[28] = x119;
-    out1[29] = x122;
-    out1[30] = x124;
+    out1[0] = x55;
+    out1[1] = x57;
+    out1[2] = x58;
+    out1[3] = x59;
+    out1[4] = x61;
+    out1[5] = x64;
+    out1[6] = x66;
+    out1[7] = x68;
+    out1[8] = x71;
+    out1[9] = x73;
+    out1[10] = x75;
+    out1[11] = x78;
+    out1[12] = x80;
+    out1[13] = x82;
+    out1[14] = x85;
+    out1[15] = x87;
+    out1[16] = x89;
+    out1[17] = x92;
+    out1[18] = x94;
+    out1[19] = x96;
+    out1[20] = x99;
+    out1[21] = x101;
+    out1[22] = x103;
+    out1[23] = x106;
+    out1[24] = x108;
+    out1[25] = x110;
+    out1[26] = x113;
+    out1[27] = x115;
+    out1[28] = x117;
+    out1[29] = x120;
+    out1[30] = x122;
     out1[31] = x123;
 }
 
@@ -5357,7 +5467,7 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(
  * Input Bounds:
  *   arg1: [[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 ~> 0xff]]
  * Output Bounds:
- *   out1: [[0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x1199999], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc], [0x0 ~> 0x8ccccc]]
+ *   out1: [[0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x1000000], [0x0 ~> 0x800000], [0x0 ~> 0x800000], [0x0 ~> 0x800000]]
  */
 static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     uint32_t out1[11], const uint8_t arg1[32]) {
@@ -5398,40 +5508,49 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     uint32_t x35;
     uint32_t x36;
     uint32_t x37;
-    uint32_t x38;
+    fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1 x38;
     uint32_t x39;
     uint32_t x40;
     uint32_t x41;
     uint32_t x42;
-    uint32_t x43;
+    uint8_t x43;
     uint32_t x44;
-    fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1 x45;
+    uint32_t x45;
     uint32_t x46;
     uint32_t x47;
     uint8_t x48;
     uint32_t x49;
     uint32_t x50;
-    uint8_t x51;
+    uint32_t x51;
     uint32_t x52;
-    uint32_t x53;
-    uint8_t x54;
+    uint8_t x53;
+    uint32_t x54;
     uint32_t x55;
     uint32_t x56;
-    uint8_t x57;
-    uint32_t x58;
+    uint32_t x57;
+    uint8_t x58;
     uint32_t x59;
-    uint8_t x60;
+    uint32_t x60;
     uint32_t x61;
     uint32_t x62;
     uint8_t x63;
     uint32_t x64;
     uint32_t x65;
-    uint8_t x66;
+    uint32_t x66;
     uint32_t x67;
-    uint32_t x68;
-    uint8_t x69;
+    uint8_t x68;
+    uint32_t x69;
     uint32_t x70;
     uint32_t x71;
+    uint32_t x72;
+    uint8_t x73;
+    uint32_t x74;
+    uint32_t x75;
+    uint32_t x76;
+    uint32_t x77;
+    uint8_t x78;
+    uint32_t x79;
+    uint32_t x80;
     x1 = ((uint32_t)(arg1[31]) << 15);
     x2 = ((uint32_t)(arg1[30]) << 7);
     x3 = ((uint32_t)(arg1[29]) << 22);
@@ -5464,56 +5583,65 @@ static void fiat_id_tc26_gost_3410_2012_256_paramSetA_from_bytes(
     x30 = ((uint32_t)(arg1[2]) << 16);
     x31 = ((uint32_t)(arg1[1]) << 8);
     x32 = (arg1[0]);
-    x33 = (x32 + (x31 + x30));
-    x34 = (x33 & UINT32_C(0xffffff));
-    x35 = (x2 + x1);
-    x36 = (x5 + (x4 + x3));
-    x37 = (x8 + (x7 + x6));
-    x38 = (x11 + (x10 + x9));
-    x39 = (x14 + (x13 + x12));
-    x40 = (x17 + (x16 + x15));
-    x41 = (x20 + (x19 + x18));
-    x42 = (x23 + (x22 + x21));
-    x43 = (x26 + (x25 + x24));
-    x44 = (x29 + (x28 + x27));
-    x45 = (fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1)(x44 >> 23);
-    x46 = (x44 & UINT32_C(0x7fffff));
-    x47 = (x45 + x43);
-    x48 = (uint8_t)(x47 >> 23);
-    x49 = (x47 & UINT32_C(0x7fffff));
-    x50 = (x48 + x42);
-    x51 = (uint8_t)(x50 >> 24);
-    x52 = (x50 & UINT32_C(0xffffff));
-    x53 = (x51 + x41);
-    x54 = (uint8_t)(x53 >> 23);
-    x55 = (x53 & UINT32_C(0x7fffff));
-    x56 = (x54 + x40);
-    x57 = (uint8_t)(x56 >> 23);
-    x58 = (x56 & UINT32_C(0x7fffff));
-    x59 = (x57 + x39);
-    x60 = (uint8_t)(x59 >> 23);
-    x61 = (x59 & UINT32_C(0x7fffff));
-    x62 = (x60 + x38);
-    x63 = (uint8_t)(x62 >> 24);
-    x64 = (x62 & UINT32_C(0xffffff));
-    x65 = (x63 + x37);
-    x66 = (uint8_t)(x65 >> 23);
-    x67 = (x65 & UINT32_C(0x7fffff));
-    x68 = (x66 + x36);
-    x69 = (uint8_t)(x68 >> 23);
-    x70 = (x68 & UINT32_C(0x7fffff));
-    x71 = (x69 + x35);
+    x33 = (x31 + (uint32_t)x32);
+    x34 = (x30 + x33);
+    x35 = (x28 + (uint32_t)x29);
+    x36 = (x27 + x35);
+    x37 = (x36 & UINT32_C(0x7fffff));
+    x38 = (fiat_id_tc26_gost_3410_2012_256_paramSetA_uint1)(x36 >> 23);
+    x39 = (x26 + (uint32_t)x38);
+    x40 = (x25 + x39);
+    x41 = (x24 + x40);
+    x42 = (x41 & UINT32_C(0x7fffff));
+    x43 = (uint8_t)(x41 >> 23);
+    x44 = (x23 + (uint32_t)x43);
+    x45 = (x22 + x44);
+    x46 = (x21 + x45);
+    x47 = (x46 & UINT32_C(0xffffff));
+    x48 = (uint8_t)(x46 >> 24);
+    x49 = (x20 + (uint32_t)x48);
+    x50 = (x19 + x49);
+    x51 = (x18 + x50);
+    x52 = (x51 & UINT32_C(0x7fffff));
+    x53 = (uint8_t)(x51 >> 23);
+    x54 = (x17 + (uint32_t)x53);
+    x55 = (x16 + x54);
+    x56 = (x15 + x55);
+    x57 = (x56 & UINT32_C(0x7fffff));
+    x58 = (uint8_t)(x56 >> 23);
+    x59 = (x14 + (uint32_t)x58);
+    x60 = (x13 + x59);
+    x61 = (x12 + x60);
+    x62 = (x61 & UINT32_C(0x7fffff));
+    x63 = (uint8_t)(x61 >> 23);
+    x64 = (x11 + (uint32_t)x63);
+    x65 = (x10 + x64);
+    x66 = (x9 + x65);
+    x67 = (x66 & UINT32_C(0xffffff));
+    x68 = (uint8_t)(x66 >> 24);
+    x69 = (x8 + (uint32_t)x68);
+    x70 = (x7 + x69);
+    x71 = (x6 + x70);
+    x72 = (x71 & UINT32_C(0x7fffff));
+    x73 = (uint8_t)(x71 >> 23);
+    x74 = (x5 + (uint32_t)x73);
+    x75 = (x4 + x74);
+    x76 = (x3 + x75);
+    x77 = (x76 & UINT32_C(0x7fffff));
+    x78 = (uint8_t)(x76 >> 23);
+    x79 = (x2 + (uint32_t)x78);
+    x80 = (x1 + x79);
     out1[0] = x34;
-    out1[1] = x46;
-    out1[2] = x49;
-    out1[3] = x52;
-    out1[4] = x55;
-    out1[5] = x58;
-    out1[6] = x61;
-    out1[7] = x64;
-    out1[8] = x67;
-    out1[9] = x70;
-    out1[10] = x71;
+    out1[1] = x37;
+    out1[2] = x42;
+    out1[3] = x47;
+    out1[4] = x52;
+    out1[5] = x57;
+    out1[6] = x62;
+    out1[7] = x67;
+    out1[8] = x72;
+    out1[9] = x77;
+    out1[10] = x80;
 }
 
 /* END verbatim fiat code */
@@ -8464,8 +8592,8 @@ static void point_edwards2legacy(pt_prj_t *Q, const pt_prj_t *P) {
     /* temporary variables */
     fe_t t0;
     /* constants */
-    const limb_t *T = const_T;
     const limb_t *S = const_S;
+    const limb_t *T = const_T;
     const limb_t *X1 = P->X;
     const limb_t *Y1 = P->Y;
     const limb_t *Z1 = P->Z;
@@ -8492,8 +8620,8 @@ static void point_edwards2legacy(pt_prj_t *Q, const pt_prj_t *P) {
  */
 static void point_legacy2edwards(pt_prj_t *Q, const pt_aff_t *P) {
     /* constants */
-    const limb_t *T = const_T;
     const limb_t *S = const_S;
+    const limb_t *T = const_T;
     const limb_t *X1 = P->X;
     const limb_t *Y1 = P->Y;
     limb_t *X3 = Q->X;
@@ -8597,7 +8725,7 @@ static void scalar_wnaf(int8_t out[257], const unsigned char in[32]) {
 }
 
 /*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
  * NB: not constant time
  */
 static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[32],
@@ -8605,7 +8733,7 @@ static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[32],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[257] = {0};
     int8_t bnaf[257] = {0};
-    pt_prj_t Q;
+    pt_prj_t Q = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -8679,7 +8807,7 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[32],
                            const pt_aff_t *P) {
     int i, j, d, diff, is_neg;
     int8_t rnaf[52] = {0};
-    pt_prj_t Q, lut;
+    pt_prj_t Q = {0}, lut = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -8767,8 +8895,8 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[32],
 static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[52] = {0};
-    pt_prj_t Q, R;
-    pt_aff_t lut;
+    pt_prj_t Q = {0}, R = {0};
+    pt_aff_t lut = {0};
 
     scalar_rwnaf(rnaf, scalar);
 
@@ -8840,6 +8968,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     fiat_id_tc26_gost_3410_2012_256_paramSetA_carry_mul(out->Y, Q.Y, Q.Z);
 }
 
+/*-
+ * Wrapper: simultaneous scalar mutiplication.
+ * outx, outy := a * G + b * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
 static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
                           const unsigned char a[32], const unsigned char b[32],
                           const unsigned char inx[32],
@@ -8855,6 +8989,11 @@ static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
     fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(outy, P.Y);
 }
 
+/*-
+ * Wrapper: fixed scalar mutiplication.
+ * outx, outy := scalar * G
+ * Everything is LE byte ordering.
+ */
 static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
                         const unsigned char scalar[32]) {
     pt_aff_t P;
@@ -8865,6 +9004,12 @@ static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
     fiat_id_tc26_gost_3410_2012_256_paramSetA_to_bytes(outy, P.Y);
 }
 
+/*-
+ * Wrapper: variable point scalar mutiplication.
+ * outx, outy := scalar * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
 static void point_mul(unsigned char outx[32], unsigned char outy[32],
                       const unsigned char scalar[32],
                       const unsigned char inx[32],
@@ -8882,8 +9027,13 @@ static void point_mul(unsigned char outx[32], unsigned char outy[32],
 
 #include <openssl/ec.h>
 
+/* the zero field element */
 static const unsigned char const_zb[32] = {0};
 
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
     int
     point_mul_two_id_tc26_gost_3410_2012_256_paramSetA(
         const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
@@ -8922,6 +9072,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_tc26_gost_3410_2012_256_paramSetA(const EC_GROUP *group,
                                                    EC_POINT *r,
@@ -8961,6 +9115,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_tc26_gost_3410_2012_256_paramSetA(const EC_GROUP *group,
                                                      EC_POINT *r,