[ecp] validation with coverity

1 files changed, 727 insertions, 562 deletions

diff --git a/ecp_id_tc26_gost_3410_2012_512_paramSetB.c b/ecp_id_tc26_gost_3410_2012_512_paramSetB.c
index 83f2112..7b0f4d2 100644
--- a/ecp_id_tc26_gost_3410_2012_512_paramSetB.c
+++ b/ecp_id_tc26_gost_3410_2012_512_paramSetB.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_512_PARAMSETB_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))
 
@@ -73,7 +77,7 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: word_by_word_montgomery --static id_tc26_gost_3410_2012_512_paramSetB 64 '2^511 + 111' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier id_tc26_gost_3410_2012_512_paramSetB 64 '2^511 + 111' */
 /* curve description: id_tc26_gost_3410_2012_512_paramSetB */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: (all) */
@@ -100,6 +104,17 @@ typedef unsigned __int128 fiat_id_tc26_gost_3410_2012_512_paramSetB_uint128;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETB_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint64_t
+fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u64(uint64_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u64(x) (x)
+#endif
+
 /*
  * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_addcarryx_u64 is an addition with carry.
  * Postconditions:
@@ -206,7 +221,10 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_cmovznz_u64(
     x1 = (!(!arg1));
     x2 = ((fiat_id_tc26_gost_3410_2012_512_paramSetB_int1)(0x0 - x1) &
           UINT64_C(0xffffffffffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u64(x2) &
+           arg3) |
+          (fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u64((~x2)) &
+           arg2));
     *out1 = x3;
 }
 
@@ -3786,12 +3804,11 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_montgomery(
 static void fiat_id_tc26_gost_3410_2012_512_paramSetB_nonzero(
     uint64_t *out1, const uint64_t arg1[8]) {
     uint64_t x1;
-    x1 = ((arg1[0]) |
-          ((arg1[1]) |
-           ((arg1[2]) |
-            ((arg1[3]) |
-             ((arg1[4]) |
-              ((arg1[5]) | ((arg1[6]) | ((arg1[7]) | (uint64_t)0x0))))))));
+    x1 =
+        ((arg1[0]) |
+         ((arg1[1]) |
+          ((arg1[2]) |
+           ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | (arg1[7]))))))));
     *out1 = x1;
 }
 
@@ -3845,7 +3862,7 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_selectznz(
 }
 
 /*
- * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -3866,18 +3883,18 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint64_t x6;
     uint64_t x7;
     uint64_t x8;
-    uint64_t x9;
-    uint8_t x10;
-    uint64_t x11;
-    uint8_t x12;
-    uint64_t x13;
-    uint8_t x14;
-    uint64_t x15;
-    uint8_t x16;
-    uint64_t x17;
-    uint8_t x18;
-    uint64_t x19;
-    uint8_t x20;
+    uint8_t x9;
+    uint64_t x10;
+    uint8_t x11;
+    uint64_t x12;
+    uint8_t x13;
+    uint64_t x14;
+    uint8_t x15;
+    uint64_t x16;
+    uint8_t x17;
+    uint64_t x18;
+    uint8_t x19;
+    uint64_t x20;
     uint8_t x21;
     uint8_t x22;
     uint8_t x23;
@@ -3895,21 +3912,21 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x35;
     uint8_t x36;
     uint8_t x37;
-    uint8_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;
-    uint64_t x49;
+    uint64_t x38;
+    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;
     uint8_t x51;
-    uint8_t x52;
+    uint64_t x52;
     uint8_t x53;
     uint64_t x54;
     uint8_t x55;
@@ -3921,25 +3938,25 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x61;
     uint64_t x62;
     uint8_t x63;
-    uint64_t x64;
+    uint8_t x64;
     uint8_t x65;
-    uint8_t x66;
+    uint64_t x66;
     uint8_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;
-    uint64_t x77;
+    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;
-    uint8_t x80;
+    uint8_t x79;
+    uint64_t x80;
     uint8_t x81;
-    uint8_t x82;
+    uint64_t x82;
     uint8_t x83;
     uint64_t x84;
     uint8_t x85;
@@ -3949,27 +3966,27 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x89;
     uint64_t x90;
     uint8_t x91;
-    uint64_t x92;
+    uint8_t x92;
     uint8_t x93;
     uint64_t x94;
     uint8_t x95;
-    uint8_t x96;
+    uint64_t x96;
     uint8_t x97;
-    uint8_t x98;
-    uint64_t x99;
-    uint8_t x100;
-    uint64_t x101;
-    uint8_t x102;
-    uint64_t x103;
-    uint8_t x104;
-    uint64_t x105;
+    uint64_t x98;
+    uint8_t x99;
+    uint64_t x100;
+    uint8_t x101;
+    uint64_t x102;
+    uint8_t x103;
+    uint64_t x104;
+    uint8_t x105;
     uint8_t x106;
-    uint64_t x107;
-    uint8_t x108;
-    uint64_t x109;
-    uint8_t x110;
+    uint8_t x107;
+    uint64_t x108;
+    uint8_t x109;
+    uint64_t x110;
     uint8_t x111;
-    uint8_t x112;
+    uint64_t x112;
     uint8_t x113;
     uint64_t x114;
     uint8_t x115;
@@ -3977,14 +3994,7 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x117;
     uint64_t x118;
     uint8_t x119;
-    uint64_t x120;
-    uint8_t x121;
-    uint64_t x122;
-    uint8_t x123;
-    uint64_t x124;
-    uint8_t x125;
-    uint8_t x126;
-    uint8_t x127;
+    uint8_t x120;
     x1 = (arg1[7]);
     x2 = (arg1[6]);
     x3 = (arg1[5]);
@@ -3993,193 +4003,186 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     x6 = (arg1[2]);
     x7 = (arg1[1]);
     x8 = (arg1[0]);
-    x9 = (x8 >> 8);
-    x10 = (uint8_t)(x8 & UINT8_C(0xff));
-    x11 = (x9 >> 8);
-    x12 = (uint8_t)(x9 & UINT8_C(0xff));
-    x13 = (x11 >> 8);
-    x14 = (uint8_t)(x11 & UINT8_C(0xff));
-    x15 = (x13 >> 8);
-    x16 = (uint8_t)(x13 & UINT8_C(0xff));
-    x17 = (x15 >> 8);
-    x18 = (uint8_t)(x15 & UINT8_C(0xff));
-    x19 = (x17 >> 8);
-    x20 = (uint8_t)(x17 & UINT8_C(0xff));
-    x21 = (uint8_t)(x19 >> 8);
-    x22 = (uint8_t)(x19 & UINT8_C(0xff));
-    x23 = (uint8_t)(x21 & UINT8_C(0xff));
+    x9 = (uint8_t)(x8 & UINT8_C(0xff));
+    x10 = (x8 >> 8);
+    x11 = (uint8_t)(x10 & UINT8_C(0xff));
+    x12 = (x10 >> 8);
+    x13 = (uint8_t)(x12 & UINT8_C(0xff));
+    x14 = (x12 >> 8);
+    x15 = (uint8_t)(x14 & UINT8_C(0xff));
+    x16 = (x14 >> 8);
+    x17 = (uint8_t)(x16 & UINT8_C(0xff));
+    x18 = (x16 >> 8);
+    x19 = (uint8_t)(x18 & UINT8_C(0xff));
+    x20 = (x18 >> 8);
+    x21 = (uint8_t)(x20 & UINT8_C(0xff));
+    x22 = (uint8_t)(x20 >> 8);
+    x23 = (uint8_t)(x7 & UINT8_C(0xff));
     x24 = (x7 >> 8);
-    x25 = (uint8_t)(x7 & UINT8_C(0xff));
+    x25 = (uint8_t)(x24 & UINT8_C(0xff));
     x26 = (x24 >> 8);
-    x27 = (uint8_t)(x24 & UINT8_C(0xff));
+    x27 = (uint8_t)(x26 & UINT8_C(0xff));
     x28 = (x26 >> 8);
-    x29 = (uint8_t)(x26 & UINT8_C(0xff));
+    x29 = (uint8_t)(x28 & UINT8_C(0xff));
     x30 = (x28 >> 8);
-    x31 = (uint8_t)(x28 & UINT8_C(0xff));
+    x31 = (uint8_t)(x30 & UINT8_C(0xff));
     x32 = (x30 >> 8);
-    x33 = (uint8_t)(x30 & UINT8_C(0xff));
+    x33 = (uint8_t)(x32 & UINT8_C(0xff));
     x34 = (x32 >> 8);
-    x35 = (uint8_t)(x32 & UINT8_C(0xff));
+    x35 = (uint8_t)(x34 & UINT8_C(0xff));
     x36 = (uint8_t)(x34 >> 8);
-    x37 = (uint8_t)(x34 & UINT8_C(0xff));
-    x38 = (uint8_t)(x36 & UINT8_C(0xff));
-    x39 = (x6 >> 8);
-    x40 = (uint8_t)(x6 & 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 = (x47 >> 8);
-    x50 = (uint8_t)(x47 & UINT8_C(0xff));
-    x51 = (uint8_t)(x49 >> 8);
-    x52 = (uint8_t)(x49 & UINT8_C(0xff));
-    x53 = (uint8_t)(x51 & UINT8_C(0xff));
-    x54 = (x5 >> 8);
-    x55 = (uint8_t)(x5 & UINT8_C(0xff));
+    x37 = (uint8_t)(x6 & UINT8_C(0xff));
+    x38 = (x6 >> 8);
+    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 = (uint8_t)(x5 & UINT8_C(0xff));
+    x52 = (x5 >> 8);
+    x53 = (uint8_t)(x52 & UINT8_C(0xff));
+    x54 = (x52 >> 8);
+    x55 = (uint8_t)(x54 & UINT8_C(0xff));
     x56 = (x54 >> 8);
-    x57 = (uint8_t)(x54 & UINT8_C(0xff));
+    x57 = (uint8_t)(x56 & UINT8_C(0xff));
     x58 = (x56 >> 8);
-    x59 = (uint8_t)(x56 & UINT8_C(0xff));
+    x59 = (uint8_t)(x58 & UINT8_C(0xff));
     x60 = (x58 >> 8);
-    x61 = (uint8_t)(x58 & UINT8_C(0xff));
+    x61 = (uint8_t)(x60 & UINT8_C(0xff));
     x62 = (x60 >> 8);
-    x63 = (uint8_t)(x60 & UINT8_C(0xff));
-    x64 = (x62 >> 8);
-    x65 = (uint8_t)(x62 & UINT8_C(0xff));
-    x66 = (uint8_t)(x64 >> 8);
-    x67 = (uint8_t)(x64 & UINT8_C(0xff));
-    x68 = (uint8_t)(x66 & UINT8_C(0xff));
-    x69 = (x4 >> 8);
-    x70 = (uint8_t)(x4 & 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 = (x75 >> 8);
-    x78 = (uint8_t)(x75 & UINT8_C(0xff));
-    x79 = (x77 >> 8);
-    x80 = (uint8_t)(x77 & UINT8_C(0xff));
-    x81 = (uint8_t)(x79 >> 8);
-    x82 = (uint8_t)(x79 & UINT8_C(0xff));
-    x83 = (uint8_t)(x81 & UINT8_C(0xff));
-    x84 = (x3 >> 8);
-    x85 = (uint8_t)(x3 & UINT8_C(0xff));
+    x63 = (uint8_t)(x62 & UINT8_C(0xff));
+    x64 = (uint8_t)(x62 >> 8);
+    x65 = (uint8_t)(x4 & UINT8_C(0xff));
+    x66 = (x4 >> 8);
+    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 = (uint8_t)(x3 & UINT8_C(0xff));
+    x80 = (x3 >> 8);
+    x81 = (uint8_t)(x80 & UINT8_C(0xff));
+    x82 = (x80 >> 8);
+    x83 = (uint8_t)(x82 & UINT8_C(0xff));
+    x84 = (x82 >> 8);
+    x85 = (uint8_t)(x84 & UINT8_C(0xff));
     x86 = (x84 >> 8);
-    x87 = (uint8_t)(x84 & UINT8_C(0xff));
+    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 = (x88 >> 8);
-    x91 = (uint8_t)(x88 & UINT8_C(0xff));
-    x92 = (x90 >> 8);
-    x93 = (uint8_t)(x90 & UINT8_C(0xff));
-    x94 = (x92 >> 8);
-    x95 = (uint8_t)(x92 & UINT8_C(0xff));
-    x96 = (uint8_t)(x94 >> 8);
-    x97 = (uint8_t)(x94 & UINT8_C(0xff));
-    x98 = (uint8_t)(x96 & UINT8_C(0xff));
-    x99 = (x2 >> 8);
-    x100 = (uint8_t)(x2 & UINT8_C(0xff));
-    x101 = (x99 >> 8);
-    x102 = (uint8_t)(x99 & UINT8_C(0xff));
-    x103 = (x101 >> 8);
-    x104 = (uint8_t)(x101 & UINT8_C(0xff));
-    x105 = (x103 >> 8);
-    x106 = (uint8_t)(x103 & UINT8_C(0xff));
-    x107 = (x105 >> 8);
-    x108 = (uint8_t)(x105 & UINT8_C(0xff));
-    x109 = (x107 >> 8);
-    x110 = (uint8_t)(x107 & UINT8_C(0xff));
-    x111 = (uint8_t)(x109 >> 8);
-    x112 = (uint8_t)(x109 & UINT8_C(0xff));
-    x113 = (uint8_t)(x111 & UINT8_C(0xff));
-    x114 = (x1 >> 8);
-    x115 = (uint8_t)(x1 & UINT8_C(0xff));
+    x91 = (uint8_t)(x90 & UINT8_C(0xff));
+    x92 = (uint8_t)(x90 >> 8);
+    x93 = (uint8_t)(x2 & UINT8_C(0xff));
+    x94 = (x2 >> 8);
+    x95 = (uint8_t)(x94 & UINT8_C(0xff));
+    x96 = (x94 >> 8);
+    x97 = (uint8_t)(x96 & UINT8_C(0xff));
+    x98 = (x96 >> 8);
+    x99 = (uint8_t)(x98 & UINT8_C(0xff));
+    x100 = (x98 >> 8);
+    x101 = (uint8_t)(x100 & UINT8_C(0xff));
+    x102 = (x100 >> 8);
+    x103 = (uint8_t)(x102 & UINT8_C(0xff));
+    x104 = (x102 >> 8);
+    x105 = (uint8_t)(x104 & UINT8_C(0xff));
+    x106 = (uint8_t)(x104 >> 8);
+    x107 = (uint8_t)(x1 & UINT8_C(0xff));
+    x108 = (x1 >> 8);
+    x109 = (uint8_t)(x108 & UINT8_C(0xff));
+    x110 = (x108 >> 8);
+    x111 = (uint8_t)(x110 & UINT8_C(0xff));
+    x112 = (x110 >> 8);
+    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 = (x116 >> 8);
-    x119 = (uint8_t)(x116 & UINT8_C(0xff));
-    x120 = (x118 >> 8);
-    x121 = (uint8_t)(x118 & UINT8_C(0xff));
-    x122 = (x120 >> 8);
-    x123 = (uint8_t)(x120 & UINT8_C(0xff));
-    x124 = (x122 >> 8);
-    x125 = (uint8_t)(x122 & UINT8_C(0xff));
-    x126 = (uint8_t)(x124 >> 8);
-    x127 = (uint8_t)(x124 & UINT8_C(0xff));
-    out1[0] = x10;
-    out1[1] = x12;
-    out1[2] = x14;
-    out1[3] = x16;
-    out1[4] = x18;
-    out1[5] = x20;
-    out1[6] = x22;
-    out1[7] = x23;
-    out1[8] = x25;
-    out1[9] = x27;
-    out1[10] = x29;
-    out1[11] = x31;
-    out1[12] = x33;
-    out1[13] = x35;
-    out1[14] = x37;
-    out1[15] = x38;
-    out1[16] = x40;
-    out1[17] = x42;
-    out1[18] = x44;
-    out1[19] = x46;
-    out1[20] = x48;
-    out1[21] = x50;
-    out1[22] = x52;
-    out1[23] = x53;
-    out1[24] = x55;
-    out1[25] = x57;
-    out1[26] = x59;
-    out1[27] = x61;
-    out1[28] = x63;
-    out1[29] = x65;
-    out1[30] = x67;
-    out1[31] = x68;
-    out1[32] = x70;
-    out1[33] = x72;
-    out1[34] = x74;
-    out1[35] = x76;
-    out1[36] = x78;
-    out1[37] = x80;
-    out1[38] = x82;
-    out1[39] = x83;
-    out1[40] = x85;
-    out1[41] = x87;
-    out1[42] = x89;
-    out1[43] = x91;
-    out1[44] = x93;
-    out1[45] = x95;
-    out1[46] = x97;
-    out1[47] = x98;
-    out1[48] = x100;
-    out1[49] = x102;
-    out1[50] = x104;
-    out1[51] = x106;
-    out1[52] = x108;
-    out1[53] = x110;
-    out1[54] = x112;
-    out1[55] = x113;
-    out1[56] = x115;
-    out1[57] = x117;
-    out1[58] = x119;
-    out1[59] = x121;
-    out1[60] = x123;
-    out1[61] = x125;
-    out1[62] = x127;
-    out1[63] = x126;
+    x119 = (uint8_t)(x118 & UINT8_C(0xff));
+    x120 = (uint8_t)(x118 >> 8);
+    out1[0] = x9;
+    out1[1] = x11;
+    out1[2] = x13;
+    out1[3] = x15;
+    out1[4] = x17;
+    out1[5] = x19;
+    out1[6] = x21;
+    out1[7] = x22;
+    out1[8] = x23;
+    out1[9] = x25;
+    out1[10] = x27;
+    out1[11] = x29;
+    out1[12] = x31;
+    out1[13] = x33;
+    out1[14] = x35;
+    out1[15] = x36;
+    out1[16] = x37;
+    out1[17] = x39;
+    out1[18] = x41;
+    out1[19] = x43;
+    out1[20] = x45;
+    out1[21] = x47;
+    out1[22] = x49;
+    out1[23] = x50;
+    out1[24] = x51;
+    out1[25] = x53;
+    out1[26] = x55;
+    out1[27] = x57;
+    out1[28] = x59;
+    out1[29] = x61;
+    out1[30] = x63;
+    out1[31] = x64;
+    out1[32] = x65;
+    out1[33] = x67;
+    out1[34] = x69;
+    out1[35] = x71;
+    out1[36] = x73;
+    out1[37] = x75;
+    out1[38] = x77;
+    out1[39] = x78;
+    out1[40] = x79;
+    out1[41] = x81;
+    out1[42] = x83;
+    out1[43] = x85;
+    out1[44] = x87;
+    out1[45] = x89;
+    out1[46] = x91;
+    out1[47] = x92;
+    out1[48] = x93;
+    out1[49] = x95;
+    out1[50] = x97;
+    out1[51] = x99;
+    out1[52] = x101;
+    out1[53] = x103;
+    out1[54] = x105;
+    out1[55] = x106;
+    out1[56] = x107;
+    out1[57] = x109;
+    out1[58] = x111;
+    out1[59] = x113;
+    out1[60] = x115;
+    out1[61] = x117;
+    out1[62] = x119;
+    out1[63] = x120;
 }
 
 /*
- * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -4272,6 +4275,47 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes(
     uint64_t x77;
     uint64_t x78;
     uint64_t x79;
+    uint64_t x80;
+    uint64_t x81;
+    uint64_t x82;
+    uint64_t x83;
+    uint64_t x84;
+    uint64_t x85;
+    uint64_t x86;
+    uint64_t x87;
+    uint64_t x88;
+    uint64_t x89;
+    uint64_t x90;
+    uint64_t x91;
+    uint64_t x92;
+    uint64_t x93;
+    uint64_t x94;
+    uint64_t x95;
+    uint64_t x96;
+    uint64_t x97;
+    uint64_t x98;
+    uint64_t x99;
+    uint64_t x100;
+    uint64_t x101;
+    uint64_t x102;
+    uint64_t x103;
+    uint64_t x104;
+    uint64_t x105;
+    uint64_t x106;
+    uint64_t x107;
+    uint64_t x108;
+    uint64_t x109;
+    uint64_t x110;
+    uint64_t x111;
+    uint64_t x112;
+    uint64_t x113;
+    uint64_t x114;
+    uint64_t x115;
+    uint64_t x116;
+    uint64_t x117;
+    uint64_t x118;
+    uint64_t x119;
+    uint64_t x120;
     x1 = ((uint64_t)(arg1[63]) << 56);
     x2 = ((uint64_t)(arg1[62]) << 48);
     x3 = ((uint64_t)(arg1[61]) << 40);
@@ -4336,29 +4380,70 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes(
     x62 = ((uint64_t)(arg1[2]) << 16);
     x63 = ((uint64_t)(arg1[1]) << 8);
     x64 = (arg1[0]);
-    x65 = (x64 + (x63 + (x62 + (x61 + (x60 + (x59 + (x58 + x57)))))));
-    x66 = (x65 & UINT64_C(0xffffffffffffffff));
-    x67 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1)))))));
-    x68 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9)))))));
-    x69 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17)))))));
-    x70 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25)))))));
-    x71 = (x40 + (x39 + (x38 + (x37 + (x36 + (x35 + (x34 + x33)))))));
-    x72 = (x48 + (x47 + (x46 + (x45 + (x44 + (x43 + (x42 + x41)))))));
-    x73 = (x56 + (x55 + (x54 + (x53 + (x52 + (x51 + (x50 + x49)))))));
-    x74 = (x73 & UINT64_C(0xffffffffffffffff));
-    x75 = (x72 & UINT64_C(0xffffffffffffffff));
-    x76 = (x71 & UINT64_C(0xffffffffffffffff));
-    x77 = (x70 & UINT64_C(0xffffffffffffffff));
-    x78 = (x69 & UINT64_C(0xffffffffffffffff));
-    x79 = (x68 & UINT64_C(0xffffffffffffffff));
-    out1[0] = x66;
-    out1[1] = x74;
-    out1[2] = x75;
-    out1[3] = x76;
-    out1[4] = x77;
-    out1[5] = x78;
-    out1[6] = x79;
-    out1[7] = x67;
+    x65 = (x63 + (uint64_t)x64);
+    x66 = (x62 + x65);
+    x67 = (x61 + x66);
+    x68 = (x60 + x67);
+    x69 = (x59 + x68);
+    x70 = (x58 + x69);
+    x71 = (x57 + x70);
+    x72 = (x55 + (uint64_t)x56);
+    x73 = (x54 + x72);
+    x74 = (x53 + x73);
+    x75 = (x52 + x74);
+    x76 = (x51 + x75);
+    x77 = (x50 + x76);
+    x78 = (x49 + x77);
+    x79 = (x47 + (uint64_t)x48);
+    x80 = (x46 + x79);
+    x81 = (x45 + x80);
+    x82 = (x44 + x81);
+    x83 = (x43 + x82);
+    x84 = (x42 + x83);
+    x85 = (x41 + x84);
+    x86 = (x39 + (uint64_t)x40);
+    x87 = (x38 + x86);
+    x88 = (x37 + x87);
+    x89 = (x36 + x88);
+    x90 = (x35 + x89);
+    x91 = (x34 + x90);
+    x92 = (x33 + x91);
+    x93 = (x31 + (uint64_t)x32);
+    x94 = (x30 + x93);
+    x95 = (x29 + x94);
+    x96 = (x28 + x95);
+    x97 = (x27 + x96);
+    x98 = (x26 + x97);
+    x99 = (x25 + x98);
+    x100 = (x23 + (uint64_t)x24);
+    x101 = (x22 + x100);
+    x102 = (x21 + x101);
+    x103 = (x20 + x102);
+    x104 = (x19 + x103);
+    x105 = (x18 + x104);
+    x106 = (x17 + x105);
+    x107 = (x15 + (uint64_t)x16);
+    x108 = (x14 + x107);
+    x109 = (x13 + x108);
+    x110 = (x12 + x109);
+    x111 = (x11 + x110);
+    x112 = (x10 + x111);
+    x113 = (x9 + x112);
+    x114 = (x7 + (uint64_t)x8);
+    x115 = (x6 + x114);
+    x116 = (x5 + x115);
+    x117 = (x4 + x116);
+    x118 = (x3 + x117);
+    x119 = (x2 + x118);
+    x120 = (x1 + x119);
+    out1[0] = x71;
+    out1[1] = x78;
+    out1[2] = x85;
+    out1[3] = x92;
+    out1[4] = x99;
+    out1[5] = x106;
+    out1[6] = x113;
+    out1[7] = x120;
 }
 
 /* END verbatim fiat code */
@@ -6507,7 +6592,7 @@ static void scalar_wnaf(int8_t out[513], const unsigned char in[64]) {
 }
 
 /*-
- * 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[64],
@@ -6515,7 +6600,7 @@ static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[64],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[513] = {0};
     int8_t bnaf[513] = {0};
-    pt_prj_t Q;
+    pt_prj_t Q = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -6581,7 +6666,7 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
                            const pt_aff_t *P) {
     int i, j, d, diff, is_neg;
     int8_t rnaf[103] = {0};
-    pt_prj_t Q, lut;
+    pt_prj_t Q = {0}, lut = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -6657,8 +6742,8 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
 static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[103] = {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);
 
@@ -6719,6 +6804,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                           const unsigned char a[64], const unsigned char b[64],
                           const unsigned char inx[64],
@@ -6738,6 +6829,11 @@ static void point_mul_two(unsigned char outx[64], unsigned char outy[64],
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                         const unsigned char scalar[64]) {
     pt_aff_t P;
@@ -6750,6 +6846,12 @@ static void point_mul_g(unsigned char outx[64], unsigned char outy[64],
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                       const unsigned char scalar[64],
                       const unsigned char inx[64],
@@ -6771,8 +6873,13 @@ static void point_mul(unsigned char outx[64], unsigned char outy[64],
 
 #include <openssl/ec.h>
 
+/* the zero field element */
 static const unsigned char const_zb[64] = {0};
 
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
     int
     point_mul_two_id_tc26_gost_3410_2012_512_paramSetB(
         const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
@@ -6811,6 +6918,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_tc26_gost_3410_2012_512_paramSetB(const EC_GROUP *group,
                                                    EC_POINT *r,
@@ -6850,6 +6961,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_tc26_gost_3410_2012_512_paramSetB(const EC_GROUP *group,
                                                      EC_POINT *r,
@@ -6896,6 +7011,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_512_PARAMSETB_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))
 
@@ -6937,7 +7056,7 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: word_by_word_montgomery --static id_tc26_gost_3410_2012_512_paramSetB 32 '2^511 + 111' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier id_tc26_gost_3410_2012_512_paramSetB 32 '2^511 + 111' */
 /* curve description: id_tc26_gost_3410_2012_512_paramSetB */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: (all) */
@@ -6962,6 +7081,17 @@ typedef signed char fiat_id_tc26_gost_3410_2012_512_paramSetB_int1;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETB_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint32_t
+fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u32(uint32_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u32(x) (x)
+#endif
+
 /*
  * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_addcarryx_u32 is an addition with carry.
  * Postconditions:
@@ -7066,7 +7196,10 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_cmovznz_u32(
     x1 = (!(!arg1));
     x2 = ((fiat_id_tc26_gost_3410_2012_512_paramSetB_int1)(0x0 - x1) &
           UINT32_C(0xffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u32(x2) &
+           arg3) |
+          (fiat_id_tc26_gost_3410_2012_512_paramSetB_value_barrier_u32((~x2)) &
+           arg2));
     *out1 = x3;
 }
 
@@ -18238,22 +18371,20 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_montgomery(
 static void fiat_id_tc26_gost_3410_2012_512_paramSetB_nonzero(
     uint32_t *out1, const uint32_t arg1[16]) {
     uint32_t x1;
-    x1 =
-        ((arg1[0]) |
-         ((arg1[1]) |
-          ((arg1[2]) |
-           ((arg1[3]) |
-            ((arg1[4]) |
-             ((arg1[5]) |
-              ((arg1[6]) |
-               ((arg1[7]) |
-                ((arg1[8]) |
-                 ((arg1[9]) |
-                  ((arg1[10]) |
-                   ((arg1[11]) |
-                    ((arg1[12]) |
-                     ((arg1[13]) |
-                      ((arg1[14]) | ((arg1[15]) | (uint32_t)0x0))))))))))))))));
+    x1 = ((arg1[0]) |
+          ((arg1[1]) |
+           ((arg1[2]) |
+            ((arg1[3]) |
+             ((arg1[4]) |
+              ((arg1[5]) |
+               ((arg1[6]) |
+                ((arg1[7]) |
+                 ((arg1[8]) |
+                  ((arg1[9]) |
+                   ((arg1[10]) |
+                    ((arg1[11]) |
+                     ((arg1[12]) |
+                      ((arg1[13]) | ((arg1[14]) | (arg1[15]))))))))))))))));
     *out1 = x1;
 }
 
@@ -18339,7 +18470,7 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_selectznz(
 }
 
 /*
- * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -18368,10 +18499,10 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint32_t x14;
     uint32_t x15;
     uint32_t x16;
-    uint32_t x17;
-    uint8_t x18;
-    uint32_t x19;
-    uint8_t x20;
+    uint8_t x17;
+    uint32_t x18;
+    uint8_t x19;
+    uint32_t x20;
     uint8_t x21;
     uint8_t x22;
     uint8_t x23;
@@ -18381,39 +18512,39 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x27;
     uint8_t x28;
     uint8_t x29;
-    uint8_t x30;
-    uint32_t x31;
-    uint8_t x32;
-    uint32_t x33;
+    uint32_t x30;
+    uint8_t x31;
+    uint32_t x32;
+    uint8_t x33;
     uint8_t x34;
     uint8_t x35;
-    uint8_t x36;
+    uint32_t x36;
     uint8_t x37;
     uint32_t x38;
     uint8_t x39;
-    uint32_t x40;
+    uint8_t x40;
     uint8_t x41;
-    uint8_t x42;
+    uint32_t x42;
     uint8_t x43;
-    uint8_t x44;
-    uint32_t x45;
+    uint32_t x44;
+    uint8_t x45;
     uint8_t x46;
-    uint32_t x47;
-    uint8_t x48;
+    uint8_t x47;
+    uint32_t x48;
     uint8_t x49;
-    uint8_t x50;
+    uint32_t x50;
     uint8_t x51;
-    uint32_t x52;
+    uint8_t x52;
     uint8_t x53;
     uint32_t x54;
     uint8_t x55;
-    uint8_t x56;
+    uint32_t x56;
     uint8_t x57;
     uint8_t x58;
-    uint32_t x59;
-    uint8_t x60;
-    uint32_t x61;
-    uint8_t x62;
+    uint8_t x59;
+    uint32_t x60;
+    uint8_t x61;
+    uint32_t x62;
     uint8_t x63;
     uint8_t x64;
     uint8_t x65;
@@ -18423,39 +18554,39 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint8_t x69;
     uint8_t x70;
     uint8_t x71;
-    uint8_t x72;
-    uint32_t x73;
-    uint8_t x74;
-    uint32_t x75;
+    uint32_t x72;
+    uint8_t x73;
+    uint32_t x74;
+    uint8_t x75;
     uint8_t x76;
     uint8_t x77;
-    uint8_t x78;
+    uint32_t x78;
     uint8_t x79;
     uint32_t x80;
     uint8_t x81;
-    uint32_t x82;
+    uint8_t x82;
     uint8_t x83;
-    uint8_t x84;
+    uint32_t x84;
     uint8_t x85;
-    uint8_t x86;
-    uint32_t x87;
+    uint32_t x86;
+    uint8_t x87;
     uint8_t x88;
-    uint32_t x89;
-    uint8_t x90;
+    uint8_t x89;
+    uint32_t x90;
     uint8_t x91;
-    uint8_t x92;
+    uint32_t x92;
     uint8_t x93;
-    uint32_t x94;
+    uint8_t x94;
     uint8_t x95;
     uint32_t x96;
     uint8_t x97;
-    uint8_t x98;
+    uint32_t x98;
     uint8_t x99;
     uint8_t x100;
-    uint32_t x101;
-    uint8_t x102;
-    uint32_t x103;
-    uint8_t x104;
+    uint8_t x101;
+    uint32_t x102;
+    uint8_t x103;
+    uint32_t x104;
     uint8_t x105;
     uint8_t x106;
     uint8_t x107;
@@ -18464,21 +18595,6 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     uint32_t x110;
     uint8_t x111;
     uint8_t x112;
-    uint8_t x113;
-    uint8_t x114;
-    uint32_t x115;
-    uint8_t x116;
-    uint32_t x117;
-    uint8_t x118;
-    uint8_t x119;
-    uint8_t x120;
-    uint8_t x121;
-    uint32_t x122;
-    uint8_t x123;
-    uint32_t x124;
-    uint8_t x125;
-    uint8_t x126;
-    uint8_t x127;
     x1 = (arg1[15]);
     x2 = (arg1[14]);
     x3 = (arg1[13]);
@@ -18495,185 +18611,170 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_to_bytes(
     x14 = (arg1[2]);
     x15 = (arg1[1]);
     x16 = (arg1[0]);
-    x17 = (x16 >> 8);
-    x18 = (uint8_t)(x16 & UINT8_C(0xff));
-    x19 = (x17 >> 8);
-    x20 = (uint8_t)(x17 & UINT8_C(0xff));
-    x21 = (uint8_t)(x19 >> 8);
-    x22 = (uint8_t)(x19 & UINT8_C(0xff));
-    x23 = (uint8_t)(x21 & UINT8_C(0xff));
+    x17 = (uint8_t)(x16 & UINT8_C(0xff));
+    x18 = (x16 >> 8);
+    x19 = (uint8_t)(x18 & UINT8_C(0xff));
+    x20 = (x18 >> 8);
+    x21 = (uint8_t)(x20 & UINT8_C(0xff));
+    x22 = (uint8_t)(x20 >> 8);
+    x23 = (uint8_t)(x15 & UINT8_C(0xff));
     x24 = (x15 >> 8);
-    x25 = (uint8_t)(x15 & UINT8_C(0xff));
+    x25 = (uint8_t)(x24 & UINT8_C(0xff));
     x26 = (x24 >> 8);
-    x27 = (uint8_t)(x24 & UINT8_C(0xff));
+    x27 = (uint8_t)(x26 & UINT8_C(0xff));
     x28 = (uint8_t)(x26 >> 8);
-    x29 = (uint8_t)(x26 & UINT8_C(0xff));
-    x30 = (uint8_t)(x28 & UINT8_C(0xff));
-    x31 = (x14 >> 8);
-    x32 = (uint8_t)(x14 & UINT8_C(0xff));
-    x33 = (x31 >> 8);
-    x34 = (uint8_t)(x31 & UINT8_C(0xff));
-    x35 = (uint8_t)(x33 >> 8);
-    x36 = (uint8_t)(x33 & UINT8_C(0xff));
-    x37 = (uint8_t)(x35 & UINT8_C(0xff));
-    x38 = (x13 >> 8);
-    x39 = (uint8_t)(x13 & UINT8_C(0xff));
-    x40 = (x38 >> 8);
-    x41 = (uint8_t)(x38 & UINT8_C(0xff));
-    x42 = (uint8_t)(x40 >> 8);
-    x43 = (uint8_t)(x40 & UINT8_C(0xff));
-    x44 = (uint8_t)(x42 & UINT8_C(0xff));
-    x45 = (x12 >> 8);
-    x46 = (uint8_t)(x12 & 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 = (uint8_t)(x49 & UINT8_C(0xff));
-    x52 = (x11 >> 8);
-    x53 = (uint8_t)(x11 & UINT8_C(0xff));
-    x54 = (x52 >> 8);
-    x55 = (uint8_t)(x52 & UINT8_C(0xff));
-    x56 = (uint8_t)(x54 >> 8);
-    x57 = (uint8_t)(x54 & UINT8_C(0xff));
-    x58 = (uint8_t)(x56 & UINT8_C(0xff));
-    x59 = (x10 >> 8);
-    x60 = (uint8_t)(x10 & UINT8_C(0xff));
-    x61 = (x59 >> 8);
-    x62 = (uint8_t)(x59 & UINT8_C(0xff));
-    x63 = (uint8_t)(x61 >> 8);
-    x64 = (uint8_t)(x61 & UINT8_C(0xff));
-    x65 = (uint8_t)(x63 & UINT8_C(0xff));
-    x66 = (x9 >> 8);
-    x67 = (uint8_t)(x9 & UINT8_C(0xff));
+    x29 = (uint8_t)(x14 & UINT8_C(0xff));
+    x30 = (x14 >> 8);
+    x31 = (uint8_t)(x30 & UINT8_C(0xff));
+    x32 = (x30 >> 8);
+    x33 = (uint8_t)(x32 & UINT8_C(0xff));
+    x34 = (uint8_t)(x32 >> 8);
+    x35 = (uint8_t)(x13 & UINT8_C(0xff));
+    x36 = (x13 >> 8);
+    x37 = (uint8_t)(x36 & UINT8_C(0xff));
+    x38 = (x36 >> 8);
+    x39 = (uint8_t)(x38 & UINT8_C(0xff));
+    x40 = (uint8_t)(x38 >> 8);
+    x41 = (uint8_t)(x12 & UINT8_C(0xff));
+    x42 = (x12 >> 8);
+    x43 = (uint8_t)(x42 & UINT8_C(0xff));
+    x44 = (x42 >> 8);
+    x45 = (uint8_t)(x44 & UINT8_C(0xff));
+    x46 = (uint8_t)(x44 >> 8);
+    x47 = (uint8_t)(x11 & UINT8_C(0xff));
+    x48 = (x11 >> 8);
+    x49 = (uint8_t)(x48 & UINT8_C(0xff));
+    x50 = (x48 >> 8);
+    x51 = (uint8_t)(x50 & UINT8_C(0xff));
+    x52 = (uint8_t)(x50 >> 8);
+    x53 = (uint8_t)(x10 & UINT8_C(0xff));
+    x54 = (x10 >> 8);
+    x55 = (uint8_t)(x54 & UINT8_C(0xff));
+    x56 = (x54 >> 8);
+    x57 = (uint8_t)(x56 & UINT8_C(0xff));
+    x58 = (uint8_t)(x56 >> 8);
+    x59 = (uint8_t)(x9 & UINT8_C(0xff));
+    x60 = (x9 >> 8);
+    x61 = (uint8_t)(x60 & UINT8_C(0xff));
+    x62 = (x60 >> 8);
+    x63 = (uint8_t)(x62 & UINT8_C(0xff));
+    x64 = (uint8_t)(x62 >> 8);
+    x65 = (uint8_t)(x8 & UINT8_C(0xff));
+    x66 = (x8 >> 8);
+    x67 = (uint8_t)(x66 & UINT8_C(0xff));
     x68 = (x66 >> 8);
-    x69 = (uint8_t)(x66 & UINT8_C(0xff));
+    x69 = (uint8_t)(x68 & UINT8_C(0xff));
     x70 = (uint8_t)(x68 >> 8);
-    x71 = (uint8_t)(x68 & UINT8_C(0xff));
-    x72 = (uint8_t)(x70 & UINT8_C(0xff));
-    x73 = (x8 >> 8);
-    x74 = (uint8_t)(x8 & 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 = (uint8_t)(x77 & UINT8_C(0xff));
-    x80 = (x7 >> 8);
-    x81 = (uint8_t)(x7 & UINT8_C(0xff));
-    x82 = (x80 >> 8);
-    x83 = (uint8_t)(x80 & UINT8_C(0xff));
-    x84 = (uint8_t)(x82 >> 8);
-    x85 = (uint8_t)(x82 & UINT8_C(0xff));
-    x86 = (uint8_t)(x84 & UINT8_C(0xff));
-    x87 = (x6 >> 8);
-    x88 = (uint8_t)(x6 & UINT8_C(0xff));
-    x89 = (x87 >> 8);
-    x90 = (uint8_t)(x87 & UINT8_C(0xff));
-    x91 = (uint8_t)(x89 >> 8);
-    x92 = (uint8_t)(x89 & UINT8_C(0xff));
-    x93 = (uint8_t)(x91 & UINT8_C(0xff));
-    x94 = (x5 >> 8);
-    x95 = (uint8_t)(x5 & UINT8_C(0xff));
-    x96 = (x94 >> 8);
-    x97 = (uint8_t)(x94 & UINT8_C(0xff));
-    x98 = (uint8_t)(x96 >> 8);
-    x99 = (uint8_t)(x96 & UINT8_C(0xff));
-    x100 = (uint8_t)(x98 & UINT8_C(0xff));
-    x101 = (x4 >> 8);
-    x102 = (uint8_t)(x4 & UINT8_C(0xff));
-    x103 = (x101 >> 8);
-    x104 = (uint8_t)(x101 & UINT8_C(0xff));
-    x105 = (uint8_t)(x103 >> 8);
-    x106 = (uint8_t)(x103 & UINT8_C(0xff));
-    x107 = (uint8_t)(x105 & UINT8_C(0xff));
-    x108 = (x3 >> 8);
-    x109 = (uint8_t)(x3 & UINT8_C(0xff));
+    x71 = (uint8_t)(x7 & UINT8_C(0xff));
+    x72 = (x7 >> 8);
+    x73 = (uint8_t)(x72 & UINT8_C(0xff));
+    x74 = (x72 >> 8);
+    x75 = (uint8_t)(x74 & UINT8_C(0xff));
+    x76 = (uint8_t)(x74 >> 8);
+    x77 = (uint8_t)(x6 & UINT8_C(0xff));
+    x78 = (x6 >> 8);
+    x79 = (uint8_t)(x78 & UINT8_C(0xff));
+    x80 = (x78 >> 8);
+    x81 = (uint8_t)(x80 & UINT8_C(0xff));
+    x82 = (uint8_t)(x80 >> 8);
+    x83 = (uint8_t)(x5 & UINT8_C(0xff));
+    x84 = (x5 >> 8);
+    x85 = (uint8_t)(x84 & UINT8_C(0xff));
+    x86 = (x84 >> 8);
+    x87 = (uint8_t)(x86 & UINT8_C(0xff));
+    x88 = (uint8_t)(x86 >> 8);
+    x89 = (uint8_t)(x4 & UINT8_C(0xff));
+    x90 = (x4 >> 8);
+    x91 = (uint8_t)(x90 & UINT8_C(0xff));
+    x92 = (x90 >> 8);
+    x93 = (uint8_t)(x92 & UINT8_C(0xff));
+    x94 = (uint8_t)(x92 >> 8);
+    x95 = (uint8_t)(x3 & UINT8_C(0xff));
+    x96 = (x3 >> 8);
+    x97 = (uint8_t)(x96 & UINT8_C(0xff));
+    x98 = (x96 >> 8);
+    x99 = (uint8_t)(x98 & UINT8_C(0xff));
+    x100 = (uint8_t)(x98 >> 8);
+    x101 = (uint8_t)(x2 & UINT8_C(0xff));
+    x102 = (x2 >> 8);
+    x103 = (uint8_t)(x102 & UINT8_C(0xff));
+    x104 = (x102 >> 8);
+    x105 = (uint8_t)(x104 & UINT8_C(0xff));
+    x106 = (uint8_t)(x104 >> 8);
+    x107 = (uint8_t)(x1 & UINT8_C(0xff));
+    x108 = (x1 >> 8);
+    x109 = (uint8_t)(x108 & UINT8_C(0xff));
     x110 = (x108 >> 8);
-    x111 = (uint8_t)(x108 & UINT8_C(0xff));
+    x111 = (uint8_t)(x110 & UINT8_C(0xff));
     x112 = (uint8_t)(x110 >> 8);
-    x113 = (uint8_t)(x110 & UINT8_C(0xff));
-    x114 = (uint8_t)(x112 & UINT8_C(0xff));
-    x115 = (x2 >> 8);
-    x116 = (uint8_t)(x2 & UINT8_C(0xff));
-    x117 = (x115 >> 8);
-    x118 = (uint8_t)(x115 & UINT8_C(0xff));
-    x119 = (uint8_t)(x117 >> 8);
-    x120 = (uint8_t)(x117 & UINT8_C(0xff));
-    x121 = (uint8_t)(x119 & UINT8_C(0xff));
-    x122 = (x1 >> 8);
-    x123 = (uint8_t)(x1 & UINT8_C(0xff));
-    x124 = (x122 >> 8);
-    x125 = (uint8_t)(x122 & UINT8_C(0xff));
-    x126 = (uint8_t)(x124 >> 8);
-    x127 = (uint8_t)(x124 & UINT8_C(0xff));
-    out1[0] = x18;
-    out1[1] = x20;
-    out1[2] = x22;
-    out1[3] = x23;
-    out1[4] = x25;
-    out1[5] = x27;
-    out1[6] = x29;
-    out1[7] = x30;
-    out1[8] = x32;
-    out1[9] = x34;
-    out1[10] = x36;
-    out1[11] = x37;
-    out1[12] = x39;
-    out1[13] = x41;
-    out1[14] = x43;
-    out1[15] = x44;
-    out1[16] = x46;
-    out1[17] = x48;
-    out1[18] = x50;
-    out1[19] = x51;
-    out1[20] = x53;
-    out1[21] = x55;
-    out1[22] = x57;
-    out1[23] = x58;
-    out1[24] = x60;
-    out1[25] = x62;
-    out1[26] = x64;
-    out1[27] = x65;
-    out1[28] = x67;
-    out1[29] = x69;
-    out1[30] = x71;
-    out1[31] = x72;
-    out1[32] = x74;
-    out1[33] = x76;
-    out1[34] = x78;
-    out1[35] = x79;
-    out1[36] = x81;
-    out1[37] = x83;
-    out1[38] = x85;
-    out1[39] = x86;
-    out1[40] = x88;
-    out1[41] = x90;
-    out1[42] = x92;
-    out1[43] = x93;
-    out1[44] = x95;
-    out1[45] = x97;
-    out1[46] = x99;
-    out1[47] = x100;
-    out1[48] = x102;
-    out1[49] = x104;
-    out1[50] = x106;
-    out1[51] = x107;
-    out1[52] = x109;
-    out1[53] = x111;
-    out1[54] = x113;
-    out1[55] = x114;
-    out1[56] = x116;
-    out1[57] = x118;
-    out1[58] = x120;
-    out1[59] = x121;
-    out1[60] = x123;
-    out1[61] = x125;
-    out1[62] = x127;
-    out1[63] = x126;
+    out1[0] = x17;
+    out1[1] = x19;
+    out1[2] = x21;
+    out1[3] = x22;
+    out1[4] = x23;
+    out1[5] = x25;
+    out1[6] = x27;
+    out1[7] = x28;
+    out1[8] = x29;
+    out1[9] = x31;
+    out1[10] = x33;
+    out1[11] = x34;
+    out1[12] = x35;
+    out1[13] = x37;
+    out1[14] = x39;
+    out1[15] = x40;
+    out1[16] = x41;
+    out1[17] = x43;
+    out1[18] = x45;
+    out1[19] = x46;
+    out1[20] = x47;
+    out1[21] = x49;
+    out1[22] = x51;
+    out1[23] = x52;
+    out1[24] = x53;
+    out1[25] = x55;
+    out1[26] = x57;
+    out1[27] = x58;
+    out1[28] = x59;
+    out1[29] = x61;
+    out1[30] = x63;
+    out1[31] = x64;
+    out1[32] = x65;
+    out1[33] = x67;
+    out1[34] = x69;
+    out1[35] = x70;
+    out1[36] = x71;
+    out1[37] = x73;
+    out1[38] = x75;
+    out1[39] = x76;
+    out1[40] = x77;
+    out1[41] = x79;
+    out1[42] = x81;
+    out1[43] = x82;
+    out1[44] = x83;
+    out1[45] = x85;
+    out1[46] = x87;
+    out1[47] = x88;
+    out1[48] = x89;
+    out1[49] = x91;
+    out1[50] = x93;
+    out1[51] = x94;
+    out1[52] = x95;
+    out1[53] = x97;
+    out1[54] = x99;
+    out1[55] = x100;
+    out1[56] = x101;
+    out1[57] = x103;
+    out1[58] = x105;
+    out1[59] = x106;
+    out1[60] = x107;
+    out1[61] = x109;
+    out1[62] = x111;
+    out1[63] = x112;
 }
 
 /*
- * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -18782,6 +18883,23 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes(
     uint32_t x93;
     uint32_t x94;
     uint32_t x95;
+    uint32_t x96;
+    uint32_t x97;
+    uint32_t x98;
+    uint32_t x99;
+    uint32_t x100;
+    uint32_t x101;
+    uint32_t x102;
+    uint32_t x103;
+    uint32_t x104;
+    uint32_t x105;
+    uint32_t x106;
+    uint32_t x107;
+    uint32_t x108;
+    uint32_t x109;
+    uint32_t x110;
+    uint32_t x111;
+    uint32_t x112;
     x1 = ((uint32_t)(arg1[63]) << 24);
     x2 = ((uint32_t)(arg1[62]) << 16);
     x3 = ((uint32_t)(arg1[61]) << 8);
@@ -18846,53 +18964,70 @@ static void fiat_id_tc26_gost_3410_2012_512_paramSetB_from_bytes(
     x62 = ((uint32_t)(arg1[2]) << 16);
     x63 = ((uint32_t)(arg1[1]) << 8);
     x64 = (arg1[0]);
-    x65 = (x64 + (x63 + (x62 + x61)));
-    x66 = (x65 & UINT32_C(0xffffffff));
-    x67 = (x4 + (x3 + (x2 + x1)));
-    x68 = (x8 + (x7 + (x6 + x5)));
-    x69 = (x12 + (x11 + (x10 + x9)));
-    x70 = (x16 + (x15 + (x14 + x13)));
-    x71 = (x20 + (x19 + (x18 + x17)));
-    x72 = (x24 + (x23 + (x22 + x21)));
-    x73 = (x28 + (x27 + (x26 + x25)));
-    x74 = (x32 + (x31 + (x30 + x29)));
-    x75 = (x36 + (x35 + (x34 + x33)));
-    x76 = (x40 + (x39 + (x38 + x37)));
-    x77 = (x44 + (x43 + (x42 + x41)));
-    x78 = (x48 + (x47 + (x46 + x45)));
-    x79 = (x52 + (x51 + (x50 + x49)));
-    x80 = (x56 + (x55 + (x54 + x53)));
-    x81 = (x60 + (x59 + (x58 + x57)));
-    x82 = (x81 & UINT32_C(0xffffffff));
-    x83 = (x80 & UINT32_C(0xffffffff));
-    x84 = (x79 & UINT32_C(0xffffffff));
-    x85 = (x78 & UINT32_C(0xffffffff));
-    x86 = (x77 & UINT32_C(0xffffffff));
-    x87 = (x76 & UINT32_C(0xffffffff));
-    x88 = (x75 & UINT32_C(0xffffffff));
-    x89 = (x74 & UINT32_C(0xffffffff));
-    x90 = (x73 & UINT32_C(0xffffffff));
-    x91 = (x72 & UINT32_C(0xffffffff));
-    x92 = (x71 & UINT32_C(0xffffffff));
-    x93 = (x70 & UINT32_C(0xffffffff));
-    x94 = (x69 & UINT32_C(0xffffffff));
-    x95 = (x68 & UINT32_C(0xffffffff));
-    out1[0] = x66;
-    out1[1] = x82;
-    out1[2] = x83;
-    out1[3] = x84;
-    out1[4] = x85;
-    out1[5] = x86;
-    out1[6] = x87;
+    x65 = (x63 + (uint32_t)x64);
+    x66 = (x62 + x65);
+    x67 = (x61 + x66);
+    x68 = (x59 + (uint32_t)x60);
+    x69 = (x58 + x68);
+    x70 = (x57 + x69);
+    x71 = (x55 + (uint32_t)x56);
+    x72 = (x54 + x71);
+    x73 = (x53 + x72);
+    x74 = (x51 + (uint32_t)x52);
+    x75 = (x50 + x74);
+    x76 = (x49 + x75);
+    x77 = (x47 + (uint32_t)x48);
+    x78 = (x46 + x77);
+    x79 = (x45 + x78);
+    x80 = (x43 + (uint32_t)x44);
+    x81 = (x42 + x80);
+    x82 = (x41 + x81);
+    x83 = (x39 + (uint32_t)x40);
+    x84 = (x38 + x83);
+    x85 = (x37 + x84);
+    x86 = (x35 + (uint32_t)x36);
+    x87 = (x34 + x86);
+    x88 = (x33 + x87);
+    x89 = (x31 + (uint32_t)x32);
+    x90 = (x30 + x89);
+    x91 = (x29 + x90);
+    x92 = (x27 + (uint32_t)x28);
+    x93 = (x26 + x92);
+    x94 = (x25 + x93);
+    x95 = (x23 + (uint32_t)x24);
+    x96 = (x22 + x95);
+    x97 = (x21 + x96);
+    x98 = (x19 + (uint32_t)x20);
+    x99 = (x18 + x98);
+    x100 = (x17 + x99);
+    x101 = (x15 + (uint32_t)x16);
+    x102 = (x14 + x101);
+    x103 = (x13 + x102);
+    x104 = (x11 + (uint32_t)x12);
+    x105 = (x10 + x104);
+    x106 = (x9 + x105);
+    x107 = (x7 + (uint32_t)x8);
+    x108 = (x6 + x107);
+    x109 = (x5 + x108);
+    x110 = (x3 + (uint32_t)x4);
+    x111 = (x2 + x110);
+    x112 = (x1 + x111);
+    out1[0] = x67;
+    out1[1] = x70;
+    out1[2] = x73;
+    out1[3] = x76;
+    out1[4] = x79;
+    out1[5] = x82;
+    out1[6] = x85;
     out1[7] = x88;
-    out1[8] = x89;
-    out1[9] = x90;
-    out1[10] = x91;
-    out1[11] = x92;
-    out1[12] = x93;
-    out1[13] = x94;
-    out1[14] = x95;
-    out1[15] = x67;
+    out1[8] = x91;
+    out1[9] = x94;
+    out1[10] = x97;
+    out1[11] = x100;
+    out1[12] = x103;
+    out1[13] = x106;
+    out1[14] = x109;
+    out1[15] = x112;
 }
 
 /* END verbatim fiat code */
@@ -21941,7 +22076,7 @@ static void scalar_wnaf(int8_t out[513], const unsigned char in[64]) {
 }
 
 /*-
- * 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[64],
@@ -21949,7 +22084,7 @@ static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[64],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[513] = {0};
     int8_t bnaf[513] = {0};
-    pt_prj_t Q;
+    pt_prj_t Q = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -22015,7 +22150,7 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
                            const pt_aff_t *P) {
     int i, j, d, diff, is_neg;
     int8_t rnaf[103] = {0};
-    pt_prj_t Q, lut;
+    pt_prj_t Q = {0}, lut = {0};
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -22091,8 +22226,8 @@ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
 static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[103] = {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);
 
@@ -22153,6 +22288,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                           const unsigned char a[64], const unsigned char b[64],
                           const unsigned char inx[64],
@@ -22172,6 +22313,11 @@ static void point_mul_two(unsigned char outx[64], unsigned char outy[64],
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                         const unsigned char scalar[64]) {
     pt_aff_t P;
@@ -22184,6 +22330,12 @@ static void point_mul_g(unsigned char outx[64], unsigned char outy[64],
     fiat_id_tc26_gost_3410_2012_512_paramSetB_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[64], unsigned char outy[64],
                       const unsigned char scalar[64],
                       const unsigned char inx[64],
@@ -22205,8 +22357,13 @@ static void point_mul(unsigned char outx[64], unsigned char outy[64],
 
 #include <openssl/ec.h>
 
+/* the zero field element */
 static const unsigned char const_zb[64] = {0};
 
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
     int
     point_mul_two_id_tc26_gost_3410_2012_512_paramSetB(
         const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
@@ -22245,6 +22402,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_tc26_gost_3410_2012_512_paramSetB(const EC_GROUP *group,
                                                    EC_POINT *r,
@@ -22284,6 +22445,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_tc26_gost_3410_2012_512_paramSetB(const EC_GROUP *group,
                                                      EC_POINT *r,