[ecp] validation with coverity

1 files changed, 413 insertions, 280 deletions

diff --git a/ecp_id_GostR3410_2001_TestParamSet.c b/ecp_id_GostR3410_2001_TestParamSet.c
index 410de5a..3163630 100644
--- a/ecp_id_GostR3410_2001_TestParamSet.c
+++ b/ecp_id_GostR3410_2001_TestParamSet.c
@@ -32,6 +32,10 @@
 typedef uint64_t fe_t[LIMB_CNT];
 typedef uint64_t limb_t;
 
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_GOSTR3410_2001_TESTPARAMSET_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_GostR3410_2001_TestParamSet 64 '2^255 + 1073' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier id_GostR3410_2001_TestParamSet 64 '2^255 + 1073' */
 /* curve description: id_GostR3410_2001_TestParamSet */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: (all) */
@@ -100,6 +104,17 @@ typedef unsigned __int128 fiat_id_GostR3410_2001_TestParamSet_uint128;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_GOSTR3410_2001_TESTPARAMSET_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint64_t
+fiat_id_GostR3410_2001_TestParamSet_value_barrier_u64(uint64_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_GostR3410_2001_TestParamSet_value_barrier_u64(x) (x)
+#endif
+
 /*
  * The function fiat_id_GostR3410_2001_TestParamSet_addcarryx_u64 is an addition with carry.
  * Postconditions:
@@ -204,7 +219,9 @@ static void fiat_id_GostR3410_2001_TestParamSet_cmovznz_u64(
     x1 = (!(!arg1));
     x2 = ((fiat_id_GostR3410_2001_TestParamSet_int1)(0x0 - x1) &
           UINT64_C(0xffffffffffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 =
+        ((fiat_id_GostR3410_2001_TestParamSet_value_barrier_u64(x2) & arg3) |
+         (fiat_id_GostR3410_2001_TestParamSet_value_barrier_u64((~x2)) & arg2));
     *out1 = x3;
 }
 
@@ -1461,7 +1478,7 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_montgomery(
 static void fiat_id_GostR3410_2001_TestParamSet_nonzero(
     uint64_t *out1, const uint64_t arg1[4]) {
     uint64_t x1;
-    x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | (uint64_t)0x0))));
+    x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | (arg1[3]))));
     *out1 = x1;
 }
 
@@ -1499,7 +1516,7 @@ static void fiat_id_GostR3410_2001_TestParamSet_selectznz(
 }
 
 /*
- * The function fiat_id_GostR3410_2001_TestParamSet_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_id_GostR3410_2001_TestParamSet_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -1516,18 +1533,18 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_bytes(
     uint64_t x2;
     uint64_t x3;
     uint64_t x4;
-    uint64_t x5;
-    uint8_t x6;
-    uint64_t x7;
-    uint8_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;
+    uint8_t x5;
+    uint64_t x6;
+    uint8_t x7;
+    uint64_t x8;
+    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;
     uint8_t x18;
     uint8_t x19;
@@ -1545,21 +1562,21 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_bytes(
     uint8_t x31;
     uint8_t x32;
     uint8_t x33;
-    uint8_t x34;
-    uint64_t x35;
-    uint8_t x36;
-    uint64_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;
+    uint64_t x34;
+    uint8_t x35;
+    uint64_t x36;
+    uint8_t x37;
+    uint64_t x38;
+    uint8_t x39;
+    uint64_t x40;
+    uint8_t x41;
+    uint64_t x42;
+    uint8_t x43;
+    uint64_t x44;
+    uint8_t x45;
     uint8_t x46;
     uint8_t x47;
-    uint8_t x48;
+    uint64_t x48;
     uint8_t x49;
     uint64_t x50;
     uint8_t x51;
@@ -1571,109 +1588,103 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_bytes(
     uint8_t x57;
     uint64_t x58;
     uint8_t x59;
-    uint64_t x60;
-    uint8_t x61;
-    uint8_t x62;
-    uint8_t x63;
+    uint8_t x60;
     x1 = (arg1[3]);
     x2 = (arg1[2]);
     x3 = (arg1[1]);
     x4 = (arg1[0]);
-    x5 = (x4 >> 8);
-    x6 = (uint8_t)(x4 & UINT8_C(0xff));
-    x7 = (x5 >> 8);
-    x8 = (uint8_t)(x5 & UINT8_C(0xff));
-    x9 = (x7 >> 8);
-    x10 = (uint8_t)(x7 & 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 = (uint8_t)(x15 >> 8);
-    x18 = (uint8_t)(x15 & UINT8_C(0xff));
-    x19 = (uint8_t)(x17 & UINT8_C(0xff));
+    x5 = (uint8_t)(x4 & UINT8_C(0xff));
+    x6 = (x4 >> 8);
+    x7 = (uint8_t)(x6 & UINT8_C(0xff));
+    x8 = (x6 >> 8);
+    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 = (uint8_t)(x16 >> 8);
+    x19 = (uint8_t)(x3 & UINT8_C(0xff));
     x20 = (x3 >> 8);
-    x21 = (uint8_t)(x3 & UINT8_C(0xff));
+    x21 = (uint8_t)(x20 & UINT8_C(0xff));
     x22 = (x20 >> 8);
-    x23 = (uint8_t)(x20 & UINT8_C(0xff));
+    x23 = (uint8_t)(x22 & UINT8_C(0xff));
     x24 = (x22 >> 8);
-    x25 = (uint8_t)(x22 & 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 = (uint8_t)(x30 >> 8);
-    x33 = (uint8_t)(x30 & UINT8_C(0xff));
-    x34 = (uint8_t)(x32 & UINT8_C(0xff));
-    x35 = (x2 >> 8);
-    x36 = (uint8_t)(x2 & UINT8_C(0xff));
-    x37 = (x35 >> 8);
-    x38 = (uint8_t)(x35 & UINT8_C(0xff));
-    x39 = (x37 >> 8);
-    x40 = (uint8_t)(x37 & 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 = (uint8_t)(x45 >> 8);
-    x48 = (uint8_t)(x45 & UINT8_C(0xff));
-    x49 = (uint8_t)(x47 & UINT8_C(0xff));
-    x50 = (x1 >> 8);
-    x51 = (uint8_t)(x1 & UINT8_C(0xff));
+    x33 = (uint8_t)(x2 & UINT8_C(0xff));
+    x34 = (x2 >> 8);
+    x35 = (uint8_t)(x34 & UINT8_C(0xff));
+    x36 = (x34 >> 8);
+    x37 = (uint8_t)(x36 & UINT8_C(0xff));
+    x38 = (x36 >> 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 = (uint8_t)(x44 >> 8);
+    x47 = (uint8_t)(x1 & UINT8_C(0xff));
+    x48 = (x1 >> 8);
+    x49 = (uint8_t)(x48 & UINT8_C(0xff));
+    x50 = (x48 >> 8);
+    x51 = (uint8_t)(x50 & UINT8_C(0xff));
     x52 = (x50 >> 8);
-    x53 = (uint8_t)(x50 & UINT8_C(0xff));
+    x53 = (uint8_t)(x52 & UINT8_C(0xff));
     x54 = (x52 >> 8);
-    x55 = (uint8_t)(x52 & UINT8_C(0xff));
+    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));
-    x60 = (x58 >> 8);
-    x61 = (uint8_t)(x58 & UINT8_C(0xff));
-    x62 = (uint8_t)(x60 >> 8);
-    x63 = (uint8_t)(x60 & UINT8_C(0xff));
-    out1[0] = x6;
-    out1[1] = x8;
-    out1[2] = x10;
-    out1[3] = x12;
-    out1[4] = x14;
-    out1[5] = x16;
-    out1[6] = x18;
-    out1[7] = x19;
-    out1[8] = x21;
-    out1[9] = x23;
-    out1[10] = x25;
-    out1[11] = x27;
-    out1[12] = x29;
-    out1[13] = x31;
-    out1[14] = x33;
-    out1[15] = x34;
-    out1[16] = x36;
-    out1[17] = x38;
-    out1[18] = x40;
-    out1[19] = x42;
-    out1[20] = x44;
-    out1[21] = x46;
-    out1[22] = x48;
-    out1[23] = x49;
-    out1[24] = x51;
-    out1[25] = x53;
-    out1[26] = x55;
-    out1[27] = x57;
-    out1[28] = x59;
-    out1[29] = x61;
-    out1[30] = x63;
-    out1[31] = x62;
+    x59 = (uint8_t)(x58 & UINT8_C(0xff));
+    x60 = (uint8_t)(x58 >> 8);
+    out1[0] = x5;
+    out1[1] = x7;
+    out1[2] = x9;
+    out1[3] = x11;
+    out1[4] = x13;
+    out1[5] = x15;
+    out1[6] = x17;
+    out1[7] = x18;
+    out1[8] = x19;
+    out1[9] = x21;
+    out1[10] = x23;
+    out1[11] = x25;
+    out1[12] = x27;
+    out1[13] = x29;
+    out1[14] = x31;
+    out1[15] = x32;
+    out1[16] = x33;
+    out1[17] = x35;
+    out1[18] = x37;
+    out1[19] = x39;
+    out1[20] = x41;
+    out1[21] = x43;
+    out1[22] = x45;
+    out1[23] = x46;
+    out1[24] = x47;
+    out1[25] = x49;
+    out1[26] = x51;
+    out1[27] = x53;
+    out1[28] = x55;
+    out1[29] = x57;
+    out1[30] = x59;
+    out1[31] = x60;
 }
 
 /*
- * The function fiat_id_GostR3410_2001_TestParamSet_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_id_GostR3410_2001_TestParamSet_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -1726,6 +1737,27 @@ static void fiat_id_GostR3410_2001_TestParamSet_from_bytes(
     uint64_t x37;
     uint64_t x38;
     uint64_t x39;
+    uint64_t x40;
+    uint64_t x41;
+    uint64_t x42;
+    uint64_t x43;
+    uint64_t x44;
+    uint64_t x45;
+    uint64_t x46;
+    uint64_t x47;
+    uint64_t 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;
+    uint64_t x57;
+    uint64_t x58;
+    uint64_t x59;
+    uint64_t x60;
     x1 = ((uint64_t)(arg1[31]) << 56);
     x2 = ((uint64_t)(arg1[30]) << 48);
     x3 = ((uint64_t)(arg1[29]) << 40);
@@ -1758,17 +1790,38 @@ static void fiat_id_GostR3410_2001_TestParamSet_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 + x25)))))));
-    x34 = (x33 & UINT64_C(0xffffffffffffffff));
-    x35 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1)))))));
-    x36 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9)))))));
-    x37 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17)))))));
-    x38 = (x37 & UINT64_C(0xffffffffffffffff));
-    x39 = (x36 & UINT64_C(0xffffffffffffffff));
-    out1[0] = x34;
-    out1[1] = x38;
-    out1[2] = x39;
-    out1[3] = x35;
+    x33 = (x31 + (uint64_t)x32);
+    x34 = (x30 + x33);
+    x35 = (x29 + x34);
+    x36 = (x28 + x35);
+    x37 = (x27 + x36);
+    x38 = (x26 + x37);
+    x39 = (x25 + x38);
+    x40 = (x23 + (uint64_t)x24);
+    x41 = (x22 + x40);
+    x42 = (x21 + x41);
+    x43 = (x20 + x42);
+    x44 = (x19 + x43);
+    x45 = (x18 + x44);
+    x46 = (x17 + x45);
+    x47 = (x15 + (uint64_t)x16);
+    x48 = (x14 + x47);
+    x49 = (x13 + x48);
+    x50 = (x12 + x49);
+    x51 = (x11 + x50);
+    x52 = (x10 + x51);
+    x53 = (x9 + x52);
+    x54 = (x7 + (uint64_t)x8);
+    x55 = (x6 + x54);
+    x56 = (x5 + x55);
+    x57 = (x4 + x56);
+    x58 = (x3 + x57);
+    x59 = (x2 + x58);
+    x60 = (x1 + x59);
+    out1[0] = x39;
+    out1[1] = x46;
+    out1[2] = x53;
+    out1[3] = x60;
 }
 
 /* END verbatim fiat code */
@@ -3872,7 +3925,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],
@@ -3880,7 +3933,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);
@@ -3946,7 +3999,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);
@@ -4022,8 +4075,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);
 
@@ -4081,6 +4134,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     fiat_id_GostR3410_2001_TestParamSet_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],
@@ -4100,6 +4159,11 @@ static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
     fiat_id_GostR3410_2001_TestParamSet_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;
@@ -4112,6 +4176,12 @@ static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
     fiat_id_GostR3410_2001_TestParamSet_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],
@@ -4133,8 +4203,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_GostR3410_2001_TestParamSet(const EC_GROUP *group,
                                                  EC_POINT *r, const BIGNUM *n,
@@ -4174,6 +4249,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_GostR3410_2001_TestParamSet(const EC_GROUP *group, EC_POINT *r,
                                              const EC_POINT *q, const BIGNUM *m,
@@ -4211,6 +4290,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_GostR3410_2001_TestParamSet(const EC_GROUP *group,
                                                EC_POINT *r, const BIGNUM *n,
@@ -4256,6 +4339,10 @@ err:
 typedef uint32_t fe_t[LIMB_CNT];
 typedef uint32_t limb_t;
 
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_GOSTR3410_2001_TESTPARAMSET_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))
 
@@ -4297,7 +4384,7 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: word_by_word_montgomery --static id_GostR3410_2001_TestParamSet 32 '2^255 + 1073' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier id_GostR3410_2001_TestParamSet 32 '2^255 + 1073' */
 /* curve description: id_GostR3410_2001_TestParamSet */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: (all) */
@@ -4322,6 +4409,17 @@ typedef signed char fiat_id_GostR3410_2001_TestParamSet_int1;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_ID_GOSTR3410_2001_TESTPARAMSET_NO_ASM) && \
+    (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint32_t
+fiat_id_GostR3410_2001_TestParamSet_value_barrier_u32(uint32_t a) {
+    __asm__("" : "+r"(a) : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_id_GostR3410_2001_TestParamSet_value_barrier_u32(x) (x)
+#endif
+
 /*
  * The function fiat_id_GostR3410_2001_TestParamSet_addcarryx_u32 is an addition with carry.
  * Postconditions:
@@ -4426,7 +4524,9 @@ static void fiat_id_GostR3410_2001_TestParamSet_cmovznz_u32(
     x1 = (!(!arg1));
     x2 = ((fiat_id_GostR3410_2001_TestParamSet_int1)(0x0 - x1) &
           UINT32_C(0xffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 =
+        ((fiat_id_GostR3410_2001_TestParamSet_value_barrier_u32(x2) & arg3) |
+         (fiat_id_GostR3410_2001_TestParamSet_value_barrier_u32((~x2)) & arg2));
     *out1 = x3;
 }
 
@@ -7831,12 +7931,11 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_montgomery(
 static void fiat_id_GostR3410_2001_TestParamSet_nonzero(
     uint32_t *out1, const uint32_t arg1[8]) {
     uint32_t x1;
-    x1 = ((arg1[0]) |
-          ((arg1[1]) |
-           ((arg1[2]) |
-            ((arg1[3]) |
-             ((arg1[4]) |
-              ((arg1[5]) | ((arg1[6]) | ((arg1[7]) | (uint32_t)0x0))))))));
+    x1 =
+        ((arg1[0]) |
+         ((arg1[1]) |
+          ((arg1[2]) |
+           ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | (arg1[7]))))))));
     *out1 = x1;
 }
 
@@ -7890,7 +7989,7 @@ static void fiat_id_GostR3410_2001_TestParamSet_selectznz(
 }
 
 /*
- * The function fiat_id_GostR3410_2001_TestParamSet_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_id_GostR3410_2001_TestParamSet_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -7911,10 +8010,10 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_bytes(
     uint32_t x6;
     uint32_t x7;
     uint32_t x8;
-    uint32_t x9;
-    uint8_t x10;
-    uint32_t x11;
-    uint8_t x12;
+    uint8_t x9;
+    uint32_t x10;
+    uint8_t x11;
+    uint32_t x12;
     uint8_t x13;
     uint8_t x14;
     uint8_t x15;
@@ -7924,48 +8023,41 @@ static void fiat_id_GostR3410_2001_TestParamSet_to_bytes(
     uint8_t x19;
     uint8_t x20;
     uint8_t x21;
-    uint8_t x22;
-    uint32_t x23;
-    uint8_t x24;
-    uint32_t x25;
+    uint32_t x22;
+    uint8_t x23;
+    uint32_t x24;
+    uint8_t x25;
     uint8_t x26;
     uint8_t x27;
-    uint8_t x28;
+    uint32_t x28;
     uint8_t x29;
     uint32_t x30;
     uint8_t x31;
-    uint32_t x32;
+    uint8_t x32;
     uint8_t x33;
-    uint8_t x34;
+    uint32_t x34;
     uint8_t x35;
-    uint8_t x36;
-    uint32_t x37;
+    uint32_t x36;
+    uint8_t x37;
     uint8_t x38;
-    uint32_t x39;
-    uint8_t x40;
+    uint8_t x39;
+    uint32_t x40;
     uint8_t x41;
-    uint8_t x42;
+    uint32_t x42;
     uint8_t x43;
-    uint32_t x44;
+    uint8_t x44;
     uint8_t x45;
     uint32_t x46;
     uint8_t x47;
-    uint8_t x48;
+    uint32_t x48;
     uint8_t x49;
     uint8_t x50;
-    uint32_t x51;
-    uint8_t x52;
-    uint32_t x53;
-    uint8_t x54;
+    uint8_t x51;
+    uint32_t x52;
+    uint8_t x53;
+    uint32_t x54;
     uint8_t x55;
     uint8_t x56;
-    uint8_t x57;
-    uint32_t x58;
-    uint8_t x59;
-    uint32_t x60;
-    uint8_t x61;
-    uint8_t x62;
-    uint8_t x63;
     x1 = (arg1[7]);
     x2 = (arg1[6]);
     x3 = (arg1[5]);
@@ -7974,97 +8066,90 @@ static void fiat_id_GostR3410_2001_TestParamSet_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 = (uint8_t)(x11 >> 8);
-    x14 = (uint8_t)(x11 & UINT8_C(0xff));
-    x15 = (uint8_t)(x13 & 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 = (uint8_t)(x12 >> 8);
+    x15 = (uint8_t)(x7 & UINT8_C(0xff));
     x16 = (x7 >> 8);
-    x17 = (uint8_t)(x7 & UINT8_C(0xff));
+    x17 = (uint8_t)(x16 & UINT8_C(0xff));
     x18 = (x16 >> 8);
-    x19 = (uint8_t)(x16 & UINT8_C(0xff));
+    x19 = (uint8_t)(x18 & UINT8_C(0xff));
     x20 = (uint8_t)(x18 >> 8);
-    x21 = (uint8_t)(x18 & UINT8_C(0xff));
-    x22 = (uint8_t)(x20 & UINT8_C(0xff));
-    x23 = (x6 >> 8);
-    x24 = (uint8_t)(x6 & UINT8_C(0xff));
-    x25 = (x23 >> 8);
-    x26 = (uint8_t)(x23 & UINT8_C(0xff));
-    x27 = (uint8_t)(x25 >> 8);
-    x28 = (uint8_t)(x25 & UINT8_C(0xff));
-    x29 = (uint8_t)(x27 & UINT8_C(0xff));
-    x30 = (x5 >> 8);
-    x31 = (uint8_t)(x5 & UINT8_C(0xff));
-    x32 = (x30 >> 8);
-    x33 = (uint8_t)(x30 & UINT8_C(0xff));
-    x34 = (uint8_t)(x32 >> 8);
-    x35 = (uint8_t)(x32 & UINT8_C(0xff));
-    x36 = (uint8_t)(x34 & UINT8_C(0xff));
-    x37 = (x4 >> 8);
-    x38 = (uint8_t)(x4 & UINT8_C(0xff));
-    x39 = (x37 >> 8);
-    x40 = (uint8_t)(x37 & UINT8_C(0xff));
-    x41 = (uint8_t)(x39 >> 8);
-    x42 = (uint8_t)(x39 & UINT8_C(0xff));
-    x43 = (uint8_t)(x41 & UINT8_C(0xff));
-    x44 = (x3 >> 8);
-    x45 = (uint8_t)(x3 & UINT8_C(0xff));
-    x46 = (x44 >> 8);
-    x47 = (uint8_t)(x44 & UINT8_C(0xff));
-    x48 = (uint8_t)(x46 >> 8);
-    x49 = (uint8_t)(x46 & UINT8_C(0xff));
-    x50 = (uint8_t)(x48 & UINT8_C(0xff));
-    x51 = (x2 >> 8);
-    x52 = (uint8_t)(x2 & UINT8_C(0xff));
-    x53 = (x51 >> 8);
-    x54 = (uint8_t)(x51 & UINT8_C(0xff));
-    x55 = (uint8_t)(x53 >> 8);
-    x56 = (uint8_t)(x53 & UINT8_C(0xff));
-    x57 = (uint8_t)(x55 & UINT8_C(0xff));
-    x58 = (x1 >> 8);
-    x59 = (uint8_t)(x1 & UINT8_C(0xff));
-    x60 = (x58 >> 8);
-    x61 = (uint8_t)(x58 & UINT8_C(0xff));
-    x62 = (uint8_t)(x60 >> 8);
-    x63 = (uint8_t)(x60 & UINT8_C(0xff));
-    out1[0] = x10;
-    out1[1] = x12;
-    out1[2] = x14;
-    out1[3] = x15;
-    out1[4] = x17;
-    out1[5] = x19;
-    out1[6] = x21;
-    out1[7] = x22;
-    out1[8] = x24;
-    out1[9] = x26;
-    out1[10] = x28;
-    out1[11] = x29;
-    out1[12] = x31;
-    out1[13] = x33;
-    out1[14] = x35;
-    out1[15] = x36;
-    out1[16] = x38;
-    out1[17] = x40;
-    out1[18] = x42;
-    out1[19] = x43;
-    out1[20] = x45;
-    out1[21] = x47;
-    out1[22] = x49;
-    out1[23] = x50;
-    out1[24] = x52;
-    out1[25] = x54;
-    out1[26] = x56;
-    out1[27] = x57;
-    out1[28] = x59;
-    out1[29] = x61;
-    out1[30] = x63;
-    out1[31] = x62;
+    x21 = (uint8_t)(x6 & UINT8_C(0xff));
+    x22 = (x6 >> 8);
+    x23 = (uint8_t)(x22 & UINT8_C(0xff));
+    x24 = (x22 >> 8);
+    x25 = (uint8_t)(x24 & UINT8_C(0xff));
+    x26 = (uint8_t)(x24 >> 8);
+    x27 = (uint8_t)(x5 & UINT8_C(0xff));
+    x28 = (x5 >> 8);
+    x29 = (uint8_t)(x28 & UINT8_C(0xff));
+    x30 = (x28 >> 8);
+    x31 = (uint8_t)(x30 & UINT8_C(0xff));
+    x32 = (uint8_t)(x30 >> 8);
+    x33 = (uint8_t)(x4 & UINT8_C(0xff));
+    x34 = (x4 >> 8);
+    x35 = (uint8_t)(x34 & UINT8_C(0xff));
+    x36 = (x34 >> 8);
+    x37 = (uint8_t)(x36 & UINT8_C(0xff));
+    x38 = (uint8_t)(x36 >> 8);
+    x39 = (uint8_t)(x3 & UINT8_C(0xff));
+    x40 = (x3 >> 8);
+    x41 = (uint8_t)(x40 & UINT8_C(0xff));
+    x42 = (x40 >> 8);
+    x43 = (uint8_t)(x42 & UINT8_C(0xff));
+    x44 = (uint8_t)(x42 >> 8);
+    x45 = (uint8_t)(x2 & UINT8_C(0xff));
+    x46 = (x2 >> 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)(x1 & UINT8_C(0xff));
+    x52 = (x1 >> 8);
+    x53 = (uint8_t)(x52 & UINT8_C(0xff));
+    x54 = (x52 >> 8);
+    x55 = (uint8_t)(x54 & UINT8_C(0xff));
+    x56 = (uint8_t)(x54 >> 8);
+    out1[0] = x9;
+    out1[1] = x11;
+    out1[2] = x13;
+    out1[3] = x14;
+    out1[4] = x15;
+    out1[5] = x17;
+    out1[6] = x19;
+    out1[7] = x20;
+    out1[8] = x21;
+    out1[9] = x23;
+    out1[10] = x25;
+    out1[11] = x26;
+    out1[12] = x27;
+    out1[13] = x29;
+    out1[14] = x31;
+    out1[15] = x32;
+    out1[16] = x33;
+    out1[17] = x35;
+    out1[18] = x37;
+    out1[19] = x38;
+    out1[20] = x39;
+    out1[21] = x41;
+    out1[22] = x43;
+    out1[23] = x44;
+    out1[24] = x45;
+    out1[25] = x47;
+    out1[26] = x49;
+    out1[27] = x50;
+    out1[28] = x51;
+    out1[29] = x53;
+    out1[30] = x55;
+    out1[31] = x56;
 }
 
 /*
- * The function fiat_id_GostR3410_2001_TestParamSet_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_id_GostR3410_2001_TestParamSet_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -8125,6 +8210,15 @@ static void fiat_id_GostR3410_2001_TestParamSet_from_bytes(
     uint32_t x45;
     uint32_t x46;
     uint32_t x47;
+    uint32_t x48;
+    uint32_t x49;
+    uint32_t x50;
+    uint32_t x51;
+    uint32_t x52;
+    uint32_t x53;
+    uint32_t x54;
+    uint32_t x55;
+    uint32_t x56;
     x1 = ((uint32_t)(arg1[31]) << 24);
     x2 = ((uint32_t)(arg1[30]) << 16);
     x3 = ((uint32_t)(arg1[29]) << 8);
@@ -8157,29 +8251,38 @@ static void fiat_id_GostR3410_2001_TestParamSet_from_bytes(
     x30 = ((uint32_t)(arg1[2]) << 16);
     x31 = ((uint32_t)(arg1[1]) << 8);
     x32 = (arg1[0]);
-    x33 = (x32 + (x31 + (x30 + x29)));
-    x34 = (x33 & UINT32_C(0xffffffff));
-    x35 = (x4 + (x3 + (x2 + x1)));
-    x36 = (x8 + (x7 + (x6 + x5)));
-    x37 = (x12 + (x11 + (x10 + x9)));
-    x38 = (x16 + (x15 + (x14 + x13)));
-    x39 = (x20 + (x19 + (x18 + x17)));
-    x40 = (x24 + (x23 + (x22 + x21)));
-    x41 = (x28 + (x27 + (x26 + x25)));
-    x42 = (x41 & UINT32_C(0xffffffff));
-    x43 = (x40 & UINT32_C(0xffffffff));
-    x44 = (x39 & UINT32_C(0xffffffff));
-    x45 = (x38 & UINT32_C(0xffffffff));
-    x46 = (x37 & UINT32_C(0xffffffff));
-    x47 = (x36 & UINT32_C(0xffffffff));
-    out1[0] = x34;
-    out1[1] = x42;
-    out1[2] = x43;
+    x33 = (x31 + (uint32_t)x32);
+    x34 = (x30 + x33);
+    x35 = (x29 + x34);
+    x36 = (x27 + (uint32_t)x28);
+    x37 = (x26 + x36);
+    x38 = (x25 + x37);
+    x39 = (x23 + (uint32_t)x24);
+    x40 = (x22 + x39);
+    x41 = (x21 + x40);
+    x42 = (x19 + (uint32_t)x20);
+    x43 = (x18 + x42);
+    x44 = (x17 + x43);
+    x45 = (x15 + (uint32_t)x16);
+    x46 = (x14 + x45);
+    x47 = (x13 + x46);
+    x48 = (x11 + (uint32_t)x12);
+    x49 = (x10 + x48);
+    x50 = (x9 + x49);
+    x51 = (x7 + (uint32_t)x8);
+    x52 = (x6 + x51);
+    x53 = (x5 + x52);
+    x54 = (x3 + (uint32_t)x4);
+    x55 = (x2 + x54);
+    x56 = (x1 + x55);
+    out1[0] = x35;
+    out1[1] = x38;
+    out1[2] = x41;
     out1[3] = x44;
-    out1[4] = x45;
-    out1[5] = x46;
-    out1[6] = x47;
-    out1[7] = x35;
+    out1[4] = x47;
+    out1[5] = x50;
+    out1[6] = x53;
+    out1[7] = x56;
 }
 
 /* END verbatim fiat code */
@@ -11150,7 +11253,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],
@@ -11158,7 +11261,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);
@@ -11224,7 +11327,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);
@@ -11300,8 +11403,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);
 
@@ -11359,6 +11462,12 @@ static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[32]) {
     fiat_id_GostR3410_2001_TestParamSet_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],
@@ -11378,6 +11487,11 @@ static void point_mul_two(unsigned char outx[32], unsigned char outy[32],
     fiat_id_GostR3410_2001_TestParamSet_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;
@@ -11390,6 +11504,12 @@ static void point_mul_g(unsigned char outx[32], unsigned char outy[32],
     fiat_id_GostR3410_2001_TestParamSet_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],
@@ -11411,8 +11531,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_GostR3410_2001_TestParamSet(const EC_GROUP *group,
                                                  EC_POINT *r, const BIGNUM *n,
@@ -11452,6 +11577,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
     int
     point_mul_id_GostR3410_2001_TestParamSet(const EC_GROUP *group, EC_POINT *r,
                                              const EC_POINT *q, const BIGNUM *m,
@@ -11489,6 +11618,10 @@ err:
     return ret;
 }
 
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
     int
     point_mul_g_id_GostR3410_2001_TestParamSet(const EC_GROUP *group,
                                                EC_POINT *r, const BIGNUM *n,