Bug 1683520 - [lib/freebl/ecl] P-384: allow zero scalars in dual scalar multiplication r=bbeurdouche

Differential Revision: https://phabricator.services.mozilla.com/D102389

1 files changed, 576 insertions, 482 deletions

diff --git a/lib/freebl/ecl/ecp_secp384r1.c b/lib/freebl/ecl/ecp_secp384r1.c
index 87c27425a..1388c6fb4 100644
--- a/lib/freebl/ecl/ecp_secp384r1.c
+++ b/lib/freebl/ecl/ecp_secp384r1.c
@@ -52,7 +52,8 @@ typedef struct {
 /*-
  * MIT License
  *
- * Copyright (c) 2020 the fiat-crypto authors (see the AUTHORS file)
+ * Copyright (c) 2015-2021 the fiat-crypto authors (see the AUTHORS file).
+ * https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy
  * of this software and associated documentation files (the "Software"), to deal
@@ -73,7 +74,7 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: word_by_word_montgomery --static secp384r1 64 '2^384 - 2^128 - 2^96 + 2^32 - 1' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier secp384r1 64 '2^384 - 2^128 - 2^96 + 2^32 - 1' */
 /* curve description: secp384r1 */
 /* machine_wordsize = 64 (from "64") */
 /* requested operations: (all) */
@@ -100,6 +101,19 @@ typedef unsigned __int128 fiat_secp384r1_uint128;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_SECP384R1_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint64_t
+fiat_secp384r1_value_barrier_u64(uint64_t a)
+{
+    __asm__(""
+            : "+r"(a)
+            : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_secp384r1_value_barrier_u64(x) (x)
+#endif
+
 /*
  * The function fiat_secp384r1_addcarryx_u64 is an addition with carry.
  * Postconditions:
@@ -209,7 +223,8 @@ fiat_secp384r1_cmovznz_u64(uint64_t *out1,
     uint64_t x3;
     x1 = (!(!arg1));
     x2 = ((fiat_secp384r1_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_secp384r1_value_barrier_u64(x2) & arg3) |
+          (fiat_secp384r1_value_barrier_u64((~x2)) & arg2));
     *out1 = x3;
 }
 
@@ -1864,12 +1879,9 @@ fiat_secp384r1_sub(uint64_t out1[6], const uint64_t arg1[6],
                                  (x13 & UINT64_C(0xffffffff00000000)));
     fiat_secp384r1_addcarryx_u64(&x18, &x19, x17, x5,
                                  (x13 & UINT64_C(0xfffffffffffffffe)));
-    fiat_secp384r1_addcarryx_u64(&x20, &x21, x19, x7,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
-    fiat_secp384r1_addcarryx_u64(&x22, &x23, x21, x9,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
-    fiat_secp384r1_addcarryx_u64(&x24, &x25, x23, x11,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
+    fiat_secp384r1_addcarryx_u64(&x20, &x21, x19, x7, x13);
+    fiat_secp384r1_addcarryx_u64(&x22, &x23, x21, x9, x13);
+    fiat_secp384r1_addcarryx_u64(&x24, &x25, x23, x11, x13);
     out1[0] = x14;
     out1[1] = x16;
     out1[2] = x18;
@@ -1932,12 +1944,9 @@ fiat_secp384r1_opp(uint64_t out1[6], const uint64_t arg1[6])
                                  (x13 & UINT64_C(0xffffffff00000000)));
     fiat_secp384r1_addcarryx_u64(&x18, &x19, x17, x5,
                                  (x13 & UINT64_C(0xfffffffffffffffe)));
-    fiat_secp384r1_addcarryx_u64(&x20, &x21, x19, x7,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
-    fiat_secp384r1_addcarryx_u64(&x22, &x23, x21, x9,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
-    fiat_secp384r1_addcarryx_u64(&x24, &x25, x23, x11,
-                                 (x13 & UINT64_C(0xffffffffffffffff)));
+    fiat_secp384r1_addcarryx_u64(&x20, &x21, x19, x7, x13);
+    fiat_secp384r1_addcarryx_u64(&x22, &x23, x21, x9, x13);
+    fiat_secp384r1_addcarryx_u64(&x24, &x25, x23, x11, x13);
     out1[0] = x14;
     out1[1] = x16;
     out1[2] = x18;
@@ -3123,9 +3132,7 @@ fiat_secp384r1_nonzero(uint64_t *out1, const uint64_t arg1[6])
 {
     uint64_t x1;
     x1 = ((arg1[0]) |
-          ((arg1[1]) |
-           ((arg1[2]) |
-            ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | (uint64_t)0x0))))));
+          ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | (arg1[5]))))));
     *out1 = x1;
 }
 
@@ -3168,7 +3175,7 @@ fiat_secp384r1_selectznz(uint64_t out1[6],
 }
 
 /*
- * The function fiat_secp384r1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_secp384r1_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -3188,18 +3195,18 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint64_t arg1[6])
     uint64_t x4;
     uint64_t x5;
     uint64_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;
-    uint64_t x17;
-    uint8_t x18;
+    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;
+    uint64_t x18;
     uint8_t x19;
     uint8_t x20;
     uint8_t x21;
@@ -3217,21 +3224,21 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint64_t arg1[6])
     uint8_t x33;
     uint8_t x34;
     uint8_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;
-    uint8_t x46;
-    uint64_t x47;
+    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;
+    uint64_t x46;
+    uint8_t x47;
     uint8_t x48;
     uint8_t x49;
-    uint8_t x50;
+    uint64_t x50;
     uint8_t x51;
     uint64_t x52;
     uint8_t x53;
@@ -3243,25 +3250,25 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint64_t arg1[6])
     uint8_t x59;
     uint64_t x60;
     uint8_t x61;
-    uint64_t x62;
+    uint8_t x62;
     uint8_t x63;
-    uint8_t x64;
+    uint64_t x64;
     uint8_t x65;
-    uint8_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;
+    uint64_t x66;
+    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;
     uint8_t x76;
-    uint64_t x77;
-    uint8_t x78;
+    uint8_t x77;
+    uint64_t x78;
     uint8_t x79;
-    uint8_t x80;
+    uint64_t x80;
     uint8_t x81;
     uint64_t x82;
     uint8_t x83;
@@ -3271,159 +3278,149 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint64_t arg1[6])
     uint8_t x87;
     uint64_t x88;
     uint8_t x89;
-    uint64_t x90;
-    uint8_t x91;
-    uint64_t x92;
-    uint8_t x93;
-    uint8_t x94;
-    uint8_t x95;
+    uint8_t x90;
     x1 = (arg1[5]);
     x2 = (arg1[4]);
     x3 = (arg1[3]);
     x4 = (arg1[2]);
     x5 = (arg1[1]);
     x6 = (arg1[0]);
-    x7 = (x6 >> 8);
-    x8 = (uint8_t)(x6 & 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 = (x15 >> 8);
-    x18 = (uint8_t)(x15 & UINT8_C(0xff));
-    x19 = (uint8_t)(x17 >> 8);
-    x20 = (uint8_t)(x17 & UINT8_C(0xff));
-    x21 = (uint8_t)(x19 & UINT8_C(0xff));
+    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 = (x16 >> 8);
+    x19 = (uint8_t)(x18 & UINT8_C(0xff));
+    x20 = (uint8_t)(x18 >> 8);
+    x21 = (uint8_t)(x5 & UINT8_C(0xff));
     x22 = (x5 >> 8);
-    x23 = (uint8_t)(x5 & 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 = (x30 >> 8);
-    x33 = (uint8_t)(x30 & UINT8_C(0xff));
+    x33 = (uint8_t)(x32 & 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 = (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 = (uint8_t)(x49 & UINT8_C(0xff));
-    x52 = (x3 >> 8);
-    x53 = (uint8_t)(x3 & UINT8_C(0xff));
+    x35 = (uint8_t)(x4 & UINT8_C(0xff));
+    x36 = (x4 >> 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 = (x44 >> 8);
+    x47 = (uint8_t)(x46 & UINT8_C(0xff));
+    x48 = (uint8_t)(x46 >> 8);
+    x49 = (uint8_t)(x3 & UINT8_C(0xff));
+    x50 = (x3 >> 8);
+    x51 = (uint8_t)(x50 & UINT8_C(0xff));
+    x52 = (x50 >> 8);
+    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));
+    x59 = (uint8_t)(x58 & 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 = (uint8_t)(x64 & UINT8_C(0xff));
-    x67 = (x2 >> 8);
-    x68 = (uint8_t)(x2 & 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 = (x75 >> 8);
-    x78 = (uint8_t)(x75 & UINT8_C(0xff));
-    x79 = (uint8_t)(x77 >> 8);
-    x80 = (uint8_t)(x77 & UINT8_C(0xff));
-    x81 = (uint8_t)(x79 & UINT8_C(0xff));
-    x82 = (x1 >> 8);
-    x83 = (uint8_t)(x1 & UINT8_C(0xff));
+    x61 = (uint8_t)(x60 & UINT8_C(0xff));
+    x62 = (uint8_t)(x60 >> 8);
+    x63 = (uint8_t)(x2 & UINT8_C(0xff));
+    x64 = (x2 >> 8);
+    x65 = (uint8_t)(x64 & UINT8_C(0xff));
+    x66 = (x64 >> 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 = (uint8_t)(x74 >> 8);
+    x77 = (uint8_t)(x1 & UINT8_C(0xff));
+    x78 = (x1 >> 8);
+    x79 = (uint8_t)(x78 & UINT8_C(0xff));
+    x80 = (x78 >> 8);
+    x81 = (uint8_t)(x80 & UINT8_C(0xff));
+    x82 = (x80 >> 8);
+    x83 = (uint8_t)(x82 & UINT8_C(0xff));
     x84 = (x82 >> 8);
-    x85 = (uint8_t)(x82 & UINT8_C(0xff));
+    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));
-    x90 = (x88 >> 8);
-    x91 = (uint8_t)(x88 & UINT8_C(0xff));
-    x92 = (x90 >> 8);
-    x93 = (uint8_t)(x90 & UINT8_C(0xff));
-    x94 = (uint8_t)(x92 >> 8);
-    x95 = (uint8_t)(x92 & UINT8_C(0xff));
-    out1[0] = x8;
-    out1[1] = x10;
-    out1[2] = x12;
-    out1[3] = x14;
-    out1[4] = x16;
-    out1[5] = x18;
-    out1[6] = x20;
-    out1[7] = x21;
-    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] = x38;
-    out1[17] = x40;
-    out1[18] = x42;
-    out1[19] = x44;
-    out1[20] = x46;
-    out1[21] = x48;
-    out1[22] = x50;
-    out1[23] = x51;
-    out1[24] = x53;
-    out1[25] = x55;
-    out1[26] = x57;
-    out1[27] = x59;
-    out1[28] = x61;
-    out1[29] = x63;
-    out1[30] = x65;
-    out1[31] = x66;
-    out1[32] = x68;
-    out1[33] = x70;
-    out1[34] = x72;
-    out1[35] = x74;
-    out1[36] = x76;
-    out1[37] = x78;
-    out1[38] = x80;
-    out1[39] = x81;
-    out1[40] = x83;
-    out1[41] = x85;
-    out1[42] = x87;
-    out1[43] = x89;
-    out1[44] = x91;
-    out1[45] = x93;
-    out1[46] = x95;
-    out1[47] = x94;
+    x89 = (uint8_t)(x88 & UINT8_C(0xff));
+    x90 = (uint8_t)(x88 >> 8);
+    out1[0] = x7;
+    out1[1] = x9;
+    out1[2] = x11;
+    out1[3] = x13;
+    out1[4] = x15;
+    out1[5] = x17;
+    out1[6] = x19;
+    out1[7] = x20;
+    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] = x35;
+    out1[17] = x37;
+    out1[18] = x39;
+    out1[19] = x41;
+    out1[20] = x43;
+    out1[21] = x45;
+    out1[22] = x47;
+    out1[23] = x48;
+    out1[24] = x49;
+    out1[25] = x51;
+    out1[26] = x53;
+    out1[27] = x55;
+    out1[28] = x57;
+    out1[29] = x59;
+    out1[30] = x61;
+    out1[31] = x62;
+    out1[32] = x63;
+    out1[33] = x65;
+    out1[34] = x67;
+    out1[35] = x69;
+    out1[36] = x71;
+    out1[37] = x73;
+    out1[38] = x75;
+    out1[39] = x76;
+    out1[40] = x77;
+    out1[41] = x79;
+    out1[42] = x81;
+    out1[43] = x83;
+    out1[44] = x85;
+    out1[45] = x87;
+    out1[46] = x89;
+    out1[47] = x90;
 }
 
 /*
- * The function fiat_secp384r1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_secp384r1_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -3498,6 +3495,37 @@ fiat_secp384r1_from_bytes(uint64_t out1[6],
     uint64_t x57;
     uint64_t x58;
     uint64_t x59;
+    uint64_t x60;
+    uint64_t x61;
+    uint64_t x62;
+    uint64_t x63;
+    uint64_t x64;
+    uint64_t x65;
+    uint64_t x66;
+    uint64_t x67;
+    uint64_t x68;
+    uint64_t x69;
+    uint64_t x70;
+    uint64_t x71;
+    uint64_t x72;
+    uint64_t x73;
+    uint64_t x74;
+    uint64_t x75;
+    uint64_t x76;
+    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;
     x1 = ((uint64_t)(arg1[47]) << 56);
     x2 = ((uint64_t)(arg1[46]) << 48);
     x3 = ((uint64_t)(arg1[45]) << 40);
@@ -3546,23 +3574,54 @@ fiat_secp384r1_from_bytes(uint64_t out1[6],
     x46 = ((uint64_t)(arg1[2]) << 16);
     x47 = ((uint64_t)(arg1[1]) << 8);
     x48 = (arg1[0]);
-    x49 = (x48 + (x47 + (x46 + (x45 + (x44 + (x43 + (x42 + x41)))))));
-    x50 = (x49 & UINT64_C(0xffffffffffffffff));
-    x51 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1)))))));
-    x52 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9)))))));
-    x53 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17)))))));
-    x54 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25)))))));
-    x55 = (x40 + (x39 + (x38 + (x37 + (x36 + (x35 + (x34 + x33)))))));
-    x56 = (x55 & UINT64_C(0xffffffffffffffff));
-    x57 = (x54 & UINT64_C(0xffffffffffffffff));
-    x58 = (x53 & UINT64_C(0xffffffffffffffff));
-    x59 = (x52 & UINT64_C(0xffffffffffffffff));
-    out1[0] = x50;
-    out1[1] = x56;
-    out1[2] = x57;
-    out1[3] = x58;
-    out1[4] = x59;
-    out1[5] = x51;
+    x49 = (x47 + (uint64_t)x48);
+    x50 = (x46 + x49);
+    x51 = (x45 + x50);
+    x52 = (x44 + x51);
+    x53 = (x43 + x52);
+    x54 = (x42 + x53);
+    x55 = (x41 + x54);
+    x56 = (x39 + (uint64_t)x40);
+    x57 = (x38 + x56);
+    x58 = (x37 + x57);
+    x59 = (x36 + x58);
+    x60 = (x35 + x59);
+    x61 = (x34 + x60);
+    x62 = (x33 + x61);
+    x63 = (x31 + (uint64_t)x32);
+    x64 = (x30 + x63);
+    x65 = (x29 + x64);
+    x66 = (x28 + x65);
+    x67 = (x27 + x66);
+    x68 = (x26 + x67);
+    x69 = (x25 + x68);
+    x70 = (x23 + (uint64_t)x24);
+    x71 = (x22 + x70);
+    x72 = (x21 + x71);
+    x73 = (x20 + x72);
+    x74 = (x19 + x73);
+    x75 = (x18 + x74);
+    x76 = (x17 + x75);
+    x77 = (x15 + (uint64_t)x16);
+    x78 = (x14 + x77);
+    x79 = (x13 + x78);
+    x80 = (x12 + x79);
+    x81 = (x11 + x80);
+    x82 = (x10 + x81);
+    x83 = (x9 + x82);
+    x84 = (x7 + (uint64_t)x8);
+    x85 = (x6 + x84);
+    x86 = (x5 + x85);
+    x87 = (x4 + x86);
+    x88 = (x3 + x87);
+    x89 = (x2 + x88);
+    x90 = (x1 + x89);
+    out1[0] = x55;
+    out1[1] = x62;
+    out1[2] = x69;
+    out1[3] = x76;
+    out1[4] = x83;
+    out1[5] = x90;
 }
 
 /* END verbatim fiat code */
@@ -6005,7 +6064,7 @@ scalar_wnaf(int8_t out[385], const unsigned char in[48])
 }
 
 /*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
  * NB: not constant time
  */
 static void
@@ -6015,7 +6074,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[48],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[385] = { 0 };
     int8_t bnaf[385] = { 0 };
-    pt_prj_t Q;
+    pt_prj_t Q = { 0 };
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -6084,14 +6143,14 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[48],
 {
     int i, j, d, diff, is_neg;
     int8_t rnaf[77] = { 0 };
-    pt_prj_t Q, lut;
+    pt_prj_t Q = { 0 }, lut = { 0 };
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
     scalar_rwnaf(rnaf, scalar);
 
 #if defined(_MSC_VER)
-/* result still unsigned: yes we know */
+    /* result still unsigned: yes we know */
 #pragma warning(push)
 #pragma warning(disable : 4146)
 #endif
@@ -6153,8 +6212,8 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
 {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[77] = { 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);
 
@@ -6164,7 +6223,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
     fe_set_zero(Q.Z);
 
 #if defined(_MSC_VER)
-/* result still unsigned: yes we know */
+    /* result still unsigned: yes we know */
 #pragma warning(push)
 #pragma warning(disable : 4146)
 #endif
@@ -6211,6 +6270,12 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
     fiat_secp384r1_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[48], unsigned char outy[48],
               const unsigned char a[48], const unsigned char b[48],
@@ -6232,6 +6297,11 @@ point_mul_two(unsigned char outx[48], unsigned char outy[48],
     fiat_secp384r1_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[48], unsigned char outy[48],
             const unsigned char scalar[48])
@@ -6246,6 +6316,12 @@ point_mul_g(unsigned char outx[48], unsigned char outy[48],
     fiat_secp384r1_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[48], unsigned char outy[48],
           const unsigned char scalar[48],
@@ -6268,6 +6344,7 @@ point_mul(unsigned char outx[48], unsigned char outy[48],
 
 #undef RADIX
 #include "ecp.h"
+#include "mpi-priv.h"
 #include "mplogic.h"
 
 /*-
@@ -6362,7 +6439,7 @@ point_mul_g_secp384r1(const mp_int *n, mp_int *out_x,
     ARGCHK(n != NULL && out_x != NULL && out_y != NULL, MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != 1)
+    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 48));
@@ -6392,7 +6469,7 @@ point_mul_secp384r1(const mp_int *n, const mp_int *in_x,
            MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != 1)
+    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 48));
@@ -6423,20 +6500,20 @@ point_mul_two_secp384r1(const mp_int *n1, const mp_int *n2,
     unsigned char b_n2[48];
     mp_err res;
 
-    /* If n2 == NULL, this is just a base-point multiplication. */
-    if (n2 == NULL)
+    /* If n2 == NULL or 0, this is just a base-point multiplication. */
+    if (n2 == NULL || mp_cmp_z(n2) == MP_EQ)
         return point_mul_g_secp384r1(n1, out_x, out_y, group);
 
-    /* If n1 == NULL, this is just an arbitary-point multiplication. */
-    if (n1 == NULL)
+    /* If n1 == NULL or 0, this is just an arbitary-point multiplication. */
+    if (n1 == NULL || mp_cmp_z(n1) == MP_EQ)
         return point_mul_secp384r1(n2, in_x, in_y, out_x, out_y, group);
 
     ARGCHK(in_x != NULL && in_y != NULL && out_x != NULL && out_y != NULL,
            MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n1) > 384 || mp_cmp_z(n1) != 1 ||
-        mpl_significant_bits(n2) > 384 || mp_cmp_z(n2) != 1)
+    if (mpl_significant_bits(n1) > 384 || mp_cmp_z(n1) != MP_GT ||
+        mpl_significant_bits(n2) > 384 || mp_cmp_z(n2) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n1, b_n1, 48));
@@ -6498,7 +6575,8 @@ typedef struct {
 /*-
  * MIT License
  *
- * Copyright (c) 2020 the fiat-crypto authors (see the AUTHORS file)
+ * Copyright (c) 2015-2021 the fiat-crypto authors (see the AUTHORS file).
+ * https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy
  * of this software and associated documentation files (the "Software"), to deal
@@ -6519,7 +6597,7 @@ typedef struct {
  * SOFTWARE.
  */
 
-/* Autogenerated: word_by_word_montgomery --static secp384r1 32 '2^384 - 2^128 - 2^96 + 2^32 - 1' */
+/* Autogenerated: word_by_word_montgomery --static --use-value-barrier secp384r1 32 '2^384 - 2^128 - 2^96 + 2^32 - 1' */
 /* curve description: secp384r1 */
 /* machine_wordsize = 32 (from "32") */
 /* requested operations: (all) */
@@ -6544,6 +6622,19 @@ typedef signed char fiat_secp384r1_int1;
 #error "This code only works on a two's complement system"
 #endif
 
+#if !defined(FIAT_SECP384R1_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint32_t
+fiat_secp384r1_value_barrier_u32(uint32_t a)
+{
+    __asm__(""
+            : "+r"(a)
+            : /* no inputs */);
+    return a;
+}
+#else
+#define fiat_secp384r1_value_barrier_u32(x) (x)
+#endif
+
 /*
  * The function fiat_secp384r1_addcarryx_u32 is an addition with carry.
  * Postconditions:
@@ -6653,7 +6744,8 @@ fiat_secp384r1_cmovznz_u32(uint32_t *out1,
     uint32_t x3;
     x1 = (!(!arg1));
     x2 = ((fiat_secp384r1_int1)(0x0 - x1) & UINT32_C(0xffffffff));
-    x3 = ((x2 & arg3) | ((~x2) & arg2));
+    x3 = ((fiat_secp384r1_value_barrier_u32(x2) & arg3) |
+          (fiat_secp384r1_value_barrier_u32((~x2)) & arg2));
     *out1 = x3;
 }
 
@@ -12013,28 +12105,19 @@ fiat_secp384r1_sub(uint32_t out1[12], const uint32_t arg1[12],
     fiat_secp384r1_subborrowx_u32(&x21, &x22, x20, (arg1[10]), (arg2[10]));
     fiat_secp384r1_subborrowx_u32(&x23, &x24, x22, (arg1[11]), (arg2[11]));
     fiat_secp384r1_cmovznz_u32(&x25, x24, 0x0, UINT32_C(0xffffffff));
-    fiat_secp384r1_addcarryx_u32(&x26, &x27, 0x0, x1,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x26, &x27, 0x0, x1, x25);
     fiat_secp384r1_addcarryx_u32(&x28, &x29, x27, x3, 0x0);
     fiat_secp384r1_addcarryx_u32(&x30, &x31, x29, x5, 0x0);
-    fiat_secp384r1_addcarryx_u32(&x32, &x33, x31, x7,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x32, &x33, x31, x7, x25);
     fiat_secp384r1_addcarryx_u32(&x34, &x35, x33, x9,
                                  (x25 & UINT32_C(0xfffffffe)));
-    fiat_secp384r1_addcarryx_u32(&x36, &x37, x35, x11,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x38, &x39, x37, x13,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x40, &x41, x39, x15,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x42, &x43, x41, x17,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x44, &x45, x43, x19,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x46, &x47, x45, x21,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x48, &x49, x47, x23,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x36, &x37, x35, x11, x25);
+    fiat_secp384r1_addcarryx_u32(&x38, &x39, x37, x13, x25);
+    fiat_secp384r1_addcarryx_u32(&x40, &x41, x39, x15, x25);
+    fiat_secp384r1_addcarryx_u32(&x42, &x43, x41, x17, x25);
+    fiat_secp384r1_addcarryx_u32(&x44, &x45, x43, x19, x25);
+    fiat_secp384r1_addcarryx_u32(&x46, &x47, x45, x21, x25);
+    fiat_secp384r1_addcarryx_u32(&x48, &x49, x47, x23, x25);
     out1[0] = x26;
     out1[1] = x28;
     out1[2] = x30;
@@ -12127,28 +12210,19 @@ fiat_secp384r1_opp(uint32_t out1[12], const uint32_t arg1[12])
     fiat_secp384r1_subborrowx_u32(&x21, &x22, x20, 0x0, (arg1[10]));
     fiat_secp384r1_subborrowx_u32(&x23, &x24, x22, 0x0, (arg1[11]));
     fiat_secp384r1_cmovznz_u32(&x25, x24, 0x0, UINT32_C(0xffffffff));
-    fiat_secp384r1_addcarryx_u32(&x26, &x27, 0x0, x1,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x26, &x27, 0x0, x1, x25);
     fiat_secp384r1_addcarryx_u32(&x28, &x29, x27, x3, 0x0);
     fiat_secp384r1_addcarryx_u32(&x30, &x31, x29, x5, 0x0);
-    fiat_secp384r1_addcarryx_u32(&x32, &x33, x31, x7,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x32, &x33, x31, x7, x25);
     fiat_secp384r1_addcarryx_u32(&x34, &x35, x33, x9,
                                  (x25 & UINT32_C(0xfffffffe)));
-    fiat_secp384r1_addcarryx_u32(&x36, &x37, x35, x11,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x38, &x39, x37, x13,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x40, &x41, x39, x15,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x42, &x43, x41, x17,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x44, &x45, x43, x19,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x46, &x47, x45, x21,
-                                 (x25 & UINT32_C(0xffffffff)));
-    fiat_secp384r1_addcarryx_u32(&x48, &x49, x47, x23,
-                                 (x25 & UINT32_C(0xffffffff)));
+    fiat_secp384r1_addcarryx_u32(&x36, &x37, x35, x11, x25);
+    fiat_secp384r1_addcarryx_u32(&x38, &x39, x37, x13, x25);
+    fiat_secp384r1_addcarryx_u32(&x40, &x41, x39, x15, x25);
+    fiat_secp384r1_addcarryx_u32(&x42, &x43, x41, x17, x25);
+    fiat_secp384r1_addcarryx_u32(&x44, &x45, x43, x19, x25);
+    fiat_secp384r1_addcarryx_u32(&x46, &x47, x45, x21, x25);
+    fiat_secp384r1_addcarryx_u32(&x48, &x49, x47, x23, x25);
     out1[0] = x26;
     out1[1] = x28;
     out1[2] = x30;
@@ -15598,9 +15672,7 @@ fiat_secp384r1_nonzero(uint32_t *out1, const uint32_t arg1[12])
               ((arg1[5]) |
                ((arg1[6]) |
                 ((arg1[7]) |
-                 ((arg1[8]) |
-                  ((arg1[9]) |
-                   ((arg1[10]) | ((arg1[11]) | (uint32_t)0x0))))))))))));
+                 ((arg1[8]) | ((arg1[9]) | ((arg1[10]) | (arg1[11]))))))))))));
     *out1 = x1;
 }
 
@@ -15661,7 +15733,7 @@ fiat_secp384r1_selectznz(uint32_t out1[12],
 }
 
 /*
- * The function fiat_secp384r1_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order.
+ * The function fiat_secp384r1_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
  * Preconditions:
  *   0 ≤ eval arg1 < m
  * Postconditions:
@@ -15687,10 +15759,10 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint32_t arg1[12])
     uint32_t x10;
     uint32_t x11;
     uint32_t x12;
-    uint32_t x13;
-    uint8_t x14;
-    uint32_t x15;
-    uint8_t x16;
+    uint8_t x13;
+    uint32_t x14;
+    uint8_t x15;
+    uint32_t x16;
     uint8_t x17;
     uint8_t x18;
     uint8_t x19;
@@ -15700,39 +15772,39 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint32_t arg1[12])
     uint8_t x23;
     uint8_t x24;
     uint8_t x25;
-    uint8_t x26;
-    uint32_t x27;
-    uint8_t x28;
-    uint32_t x29;
+    uint32_t x26;
+    uint8_t x27;
+    uint32_t x28;
+    uint8_t x29;
     uint8_t x30;
     uint8_t x31;
-    uint8_t x32;
+    uint32_t x32;
     uint8_t x33;
     uint32_t x34;
     uint8_t x35;
-    uint32_t x36;
+    uint8_t x36;
     uint8_t x37;
-    uint8_t x38;
+    uint32_t x38;
     uint8_t x39;
-    uint8_t x40;
-    uint32_t x41;
+    uint32_t x40;
+    uint8_t x41;
     uint8_t x42;
-    uint32_t x43;
-    uint8_t x44;
+    uint8_t x43;
+    uint32_t x44;
     uint8_t x45;
-    uint8_t x46;
+    uint32_t x46;
     uint8_t x47;
-    uint32_t x48;
+    uint8_t x48;
     uint8_t x49;
     uint32_t x50;
     uint8_t x51;
-    uint8_t x52;
+    uint32_t x52;
     uint8_t x53;
     uint8_t x54;
-    uint32_t x55;
-    uint8_t x56;
-    uint32_t x57;
-    uint8_t x58;
+    uint8_t x55;
+    uint32_t x56;
+    uint8_t x57;
+    uint32_t x58;
     uint8_t x59;
     uint8_t x60;
     uint8_t x61;
@@ -15742,34 +15814,23 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint32_t arg1[12])
     uint8_t x65;
     uint8_t x66;
     uint8_t x67;
-    uint8_t x68;
-    uint32_t x69;
-    uint8_t x70;
-    uint32_t x71;
+    uint32_t x68;
+    uint8_t x69;
+    uint32_t x70;
+    uint8_t x71;
     uint8_t x72;
     uint8_t x73;
-    uint8_t x74;
+    uint32_t x74;
     uint8_t x75;
     uint32_t x76;
     uint8_t x77;
-    uint32_t x78;
+    uint8_t x78;
     uint8_t x79;
-    uint8_t x80;
+    uint32_t x80;
     uint8_t x81;
-    uint8_t x82;
-    uint32_t x83;
+    uint32_t x82;
+    uint8_t x83;
     uint8_t x84;
-    uint32_t x85;
-    uint8_t x86;
-    uint8_t x87;
-    uint8_t x88;
-    uint8_t x89;
-    uint32_t x90;
-    uint8_t x91;
-    uint32_t x92;
-    uint8_t x93;
-    uint8_t x94;
-    uint8_t x95;
     x1 = (arg1[11]);
     x2 = (arg1[10]);
     x3 = (arg1[9]);
@@ -15782,141 +15843,130 @@ fiat_secp384r1_to_bytes(uint8_t out1[48], const uint32_t arg1[12])
     x10 = (arg1[2]);
     x11 = (arg1[1]);
     x12 = (arg1[0]);
-    x13 = (x12 >> 8);
-    x14 = (uint8_t)(x12 & 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));
+    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)(x11 & UINT8_C(0xff));
     x20 = (x11 >> 8);
-    x21 = (uint8_t)(x11 & 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 = (uint8_t)(x22 >> 8);
-    x25 = (uint8_t)(x22 & UINT8_C(0xff));
-    x26 = (uint8_t)(x24 & UINT8_C(0xff));
-    x27 = (x10 >> 8);
-    x28 = (uint8_t)(x10 & UINT8_C(0xff));
-    x29 = (x27 >> 8);
-    x30 = (uint8_t)(x27 & UINT8_C(0xff));
-    x31 = (uint8_t)(x29 >> 8);
-    x32 = (uint8_t)(x29 & UINT8_C(0xff));
-    x33 = (uint8_t)(x31 & UINT8_C(0xff));
-    x34 = (x9 >> 8);
-    x35 = (uint8_t)(x9 & UINT8_C(0xff));
-    x36 = (x34 >> 8);
-    x37 = (uint8_t)(x34 & UINT8_C(0xff));
-    x38 = (uint8_t)(x36 >> 8);
-    x39 = (uint8_t)(x36 & UINT8_C(0xff));
-    x40 = (uint8_t)(x38 & UINT8_C(0xff));
-    x41 = (x8 >> 8);
-    x42 = (uint8_t)(x8 & UINT8_C(0xff));
-    x43 = (x41 >> 8);
-    x44 = (uint8_t)(x41 & UINT8_C(0xff));
-    x45 = (uint8_t)(x43 >> 8);
-    x46 = (uint8_t)(x43 & UINT8_C(0xff));
-    x47 = (uint8_t)(x45 & UINT8_C(0xff));
-    x48 = (x7 >> 8);
-    x49 = (uint8_t)(x7 & UINT8_C(0xff));
-    x50 = (x48 >> 8);
-    x51 = (uint8_t)(x48 & UINT8_C(0xff));
-    x52 = (uint8_t)(x50 >> 8);
-    x53 = (uint8_t)(x50 & UINT8_C(0xff));
-    x54 = (uint8_t)(x52 & UINT8_C(0xff));
-    x55 = (x6 >> 8);
-    x56 = (uint8_t)(x6 & UINT8_C(0xff));
-    x57 = (x55 >> 8);
-    x58 = (uint8_t)(x55 & UINT8_C(0xff));
-    x59 = (uint8_t)(x57 >> 8);
-    x60 = (uint8_t)(x57 & UINT8_C(0xff));
-    x61 = (uint8_t)(x59 & UINT8_C(0xff));
-    x62 = (x5 >> 8);
-    x63 = (uint8_t)(x5 & UINT8_C(0xff));
+    x25 = (uint8_t)(x10 & UINT8_C(0xff));
+    x26 = (x10 >> 8);
+    x27 = (uint8_t)(x26 & UINT8_C(0xff));
+    x28 = (x26 >> 8);
+    x29 = (uint8_t)(x28 & UINT8_C(0xff));
+    x30 = (uint8_t)(x28 >> 8);
+    x31 = (uint8_t)(x9 & UINT8_C(0xff));
+    x32 = (x9 >> 8);
+    x33 = (uint8_t)(x32 & UINT8_C(0xff));
+    x34 = (x32 >> 8);
+    x35 = (uint8_t)(x34 & UINT8_C(0xff));
+    x36 = (uint8_t)(x34 >> 8);
+    x37 = (uint8_t)(x8 & UINT8_C(0xff));
+    x38 = (x8 >> 8);
+    x39 = (uint8_t)(x38 & UINT8_C(0xff));
+    x40 = (x38 >> 8);
+    x41 = (uint8_t)(x40 & UINT8_C(0xff));
+    x42 = (uint8_t)(x40 >> 8);
+    x43 = (uint8_t)(x7 & UINT8_C(0xff));
+    x44 = (x7 >> 8);
+    x45 = (uint8_t)(x44 & UINT8_C(0xff));
+    x46 = (x44 >> 8);
+    x47 = (uint8_t)(x46 & UINT8_C(0xff));
+    x48 = (uint8_t)(x46 >> 8);
+    x49 = (uint8_t)(x6 & UINT8_C(0xff));
+    x50 = (x6 >> 8);
+    x51 = (uint8_t)(x50 & UINT8_C(0xff));
+    x52 = (x50 >> 8);
+    x53 = (uint8_t)(x52 & UINT8_C(0xff));
+    x54 = (uint8_t)(x52 >> 8);
+    x55 = (uint8_t)(x5 & UINT8_C(0xff));
+    x56 = (x5 >> 8);
+    x57 = (uint8_t)(x56 & UINT8_C(0xff));
+    x58 = (x56 >> 8);
+    x59 = (uint8_t)(x58 & UINT8_C(0xff));
+    x60 = (uint8_t)(x58 >> 8);
+    x61 = (uint8_t)(x4 & UINT8_C(0xff));
+    x62 = (x4 >> 8);
+    x63 = (uint8_t)(x62 & UINT8_C(0xff));
     x64 = (x62 >> 8);
-    x65 = (uint8_t)(x62 & UINT8_C(0xff));
+    x65 = (uint8_t)(x64 & 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 = (uint8_t)(x71 >> 8);
-    x74 = (uint8_t)(x71 & UINT8_C(0xff));
-    x75 = (uint8_t)(x73 & UINT8_C(0xff));
-    x76 = (x3 >> 8);
-    x77 = (uint8_t)(x3 & UINT8_C(0xff));
-    x78 = (x76 >> 8);
-    x79 = (uint8_t)(x76 & UINT8_C(0xff));
-    x80 = (uint8_t)(x78 >> 8);
-    x81 = (uint8_t)(x78 & UINT8_C(0xff));
-    x82 = (uint8_t)(x80 & UINT8_C(0xff));
-    x83 = (x2 >> 8);
-    x84 = (uint8_t)(x2 & UINT8_C(0xff));
-    x85 = (x83 >> 8);
-    x86 = (uint8_t)(x83 & UINT8_C(0xff));
-    x87 = (uint8_t)(x85 >> 8);
-    x88 = (uint8_t)(x85 & UINT8_C(0xff));
-    x89 = (uint8_t)(x87 & UINT8_C(0xff));
-    x90 = (x1 >> 8);
-    x91 = (uint8_t)(x1 & UINT8_C(0xff));
-    x92 = (x90 >> 8);
-    x93 = (uint8_t)(x90 & UINT8_C(0xff));
-    x94 = (uint8_t)(x92 >> 8);
-    x95 = (uint8_t)(x92 & UINT8_C(0xff));
-    out1[0] = x14;
-    out1[1] = x16;
-    out1[2] = x18;
-    out1[3] = x19;
-    out1[4] = x21;
-    out1[5] = x23;
-    out1[6] = x25;
-    out1[7] = x26;
-    out1[8] = x28;
-    out1[9] = x30;
-    out1[10] = x32;
-    out1[11] = x33;
-    out1[12] = x35;
-    out1[13] = x37;
-    out1[14] = x39;
-    out1[15] = x40;
-    out1[16] = x42;
-    out1[17] = x44;
-    out1[18] = x46;
-    out1[19] = x47;
-    out1[20] = x49;
-    out1[21] = x51;
-    out1[22] = x53;
-    out1[23] = x54;
-    out1[24] = x56;
-    out1[25] = x58;
-    out1[26] = x60;
-    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] = x75;
-    out1[36] = x77;
-    out1[37] = x79;
-    out1[38] = x81;
-    out1[39] = x82;
-    out1[40] = x84;
-    out1[41] = x86;
-    out1[42] = x88;
-    out1[43] = x89;
-    out1[44] = x91;
-    out1[45] = x93;
-    out1[46] = x95;
-    out1[47] = x94;
+    x67 = (uint8_t)(x3 & UINT8_C(0xff));
+    x68 = (x3 >> 8);
+    x69 = (uint8_t)(x68 & UINT8_C(0xff));
+    x70 = (x68 >> 8);
+    x71 = (uint8_t)(x70 & UINT8_C(0xff));
+    x72 = (uint8_t)(x70 >> 8);
+    x73 = (uint8_t)(x2 & UINT8_C(0xff));
+    x74 = (x2 >> 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)(x1 & UINT8_C(0xff));
+    x80 = (x1 >> 8);
+    x81 = (uint8_t)(x80 & UINT8_C(0xff));
+    x82 = (x80 >> 8);
+    x83 = (uint8_t)(x82 & UINT8_C(0xff));
+    x84 = (uint8_t)(x82 >> 8);
+    out1[0] = x13;
+    out1[1] = x15;
+    out1[2] = x17;
+    out1[3] = x18;
+    out1[4] = x19;
+    out1[5] = x21;
+    out1[6] = x23;
+    out1[7] = x24;
+    out1[8] = x25;
+    out1[9] = x27;
+    out1[10] = x29;
+    out1[11] = x30;
+    out1[12] = x31;
+    out1[13] = x33;
+    out1[14] = x35;
+    out1[15] = x36;
+    out1[16] = x37;
+    out1[17] = x39;
+    out1[18] = x41;
+    out1[19] = x42;
+    out1[20] = x43;
+    out1[21] = x45;
+    out1[22] = x47;
+    out1[23] = x48;
+    out1[24] = x49;
+    out1[25] = x51;
+    out1[26] = x53;
+    out1[27] = x54;
+    out1[28] = x55;
+    out1[29] = x57;
+    out1[30] = x59;
+    out1[31] = x60;
+    out1[32] = x61;
+    out1[33] = x63;
+    out1[34] = x65;
+    out1[35] = x66;
+    out1[36] = x67;
+    out1[37] = x69;
+    out1[38] = x71;
+    out1[39] = x72;
+    out1[40] = x73;
+    out1[41] = x75;
+    out1[42] = x77;
+    out1[43] = x78;
+    out1[44] = x79;
+    out1[45] = x81;
+    out1[46] = x83;
+    out1[47] = x84;
 }
 
 /*
- * The function fiat_secp384r1_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order.
+ * The function fiat_secp384r1_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
  * Preconditions:
  *   0 ≤ bytes_eval arg1 < m
  * Postconditions:
@@ -16003,6 +16053,19 @@ fiat_secp384r1_from_bytes(uint32_t out1[12],
     uint32_t x69;
     uint32_t x70;
     uint32_t x71;
+    uint32_t x72;
+    uint32_t x73;
+    uint32_t x74;
+    uint32_t x75;
+    uint32_t x76;
+    uint32_t x77;
+    uint32_t x78;
+    uint32_t x79;
+    uint32_t x80;
+    uint32_t x81;
+    uint32_t x82;
+    uint32_t x83;
+    uint32_t x84;
     x1 = ((uint32_t)(arg1[47]) << 24);
     x2 = ((uint32_t)(arg1[46]) << 16);
     x3 = ((uint32_t)(arg1[45]) << 8);
@@ -16051,41 +16114,54 @@ fiat_secp384r1_from_bytes(uint32_t out1[12],
     x46 = ((uint32_t)(arg1[2]) << 16);
     x47 = ((uint32_t)(arg1[1]) << 8);
     x48 = (arg1[0]);
-    x49 = (x48 + (x47 + (x46 + x45)));
-    x50 = (x49 & UINT32_C(0xffffffff));
-    x51 = (x4 + (x3 + (x2 + x1)));
-    x52 = (x8 + (x7 + (x6 + x5)));
-    x53 = (x12 + (x11 + (x10 + x9)));
-    x54 = (x16 + (x15 + (x14 + x13)));
-    x55 = (x20 + (x19 + (x18 + x17)));
-    x56 = (x24 + (x23 + (x22 + x21)));
-    x57 = (x28 + (x27 + (x26 + x25)));
-    x58 = (x32 + (x31 + (x30 + x29)));
-    x59 = (x36 + (x35 + (x34 + x33)));
-    x60 = (x40 + (x39 + (x38 + x37)));
-    x61 = (x44 + (x43 + (x42 + x41)));
-    x62 = (x61 & UINT32_C(0xffffffff));
-    x63 = (x60 & UINT32_C(0xffffffff));
-    x64 = (x59 & UINT32_C(0xffffffff));
-    x65 = (x58 & UINT32_C(0xffffffff));
-    x66 = (x57 & UINT32_C(0xffffffff));
-    x67 = (x56 & UINT32_C(0xffffffff));
-    x68 = (x55 & UINT32_C(0xffffffff));
-    x69 = (x54 & UINT32_C(0xffffffff));
-    x70 = (x53 & UINT32_C(0xffffffff));
-    x71 = (x52 & UINT32_C(0xffffffff));
-    out1[0] = x50;
-    out1[1] = x62;
-    out1[2] = x63;
-    out1[3] = x64;
-    out1[4] = x65;
+    x49 = (x47 + (uint32_t)x48);
+    x50 = (x46 + x49);
+    x51 = (x45 + x50);
+    x52 = (x43 + (uint32_t)x44);
+    x53 = (x42 + x52);
+    x54 = (x41 + x53);
+    x55 = (x39 + (uint32_t)x40);
+    x56 = (x38 + x55);
+    x57 = (x37 + x56);
+    x58 = (x35 + (uint32_t)x36);
+    x59 = (x34 + x58);
+    x60 = (x33 + x59);
+    x61 = (x31 + (uint32_t)x32);
+    x62 = (x30 + x61);
+    x63 = (x29 + x62);
+    x64 = (x27 + (uint32_t)x28);
+    x65 = (x26 + x64);
+    x66 = (x25 + x65);
+    x67 = (x23 + (uint32_t)x24);
+    x68 = (x22 + x67);
+    x69 = (x21 + x68);
+    x70 = (x19 + (uint32_t)x20);
+    x71 = (x18 + x70);
+    x72 = (x17 + x71);
+    x73 = (x15 + (uint32_t)x16);
+    x74 = (x14 + x73);
+    x75 = (x13 + x74);
+    x76 = (x11 + (uint32_t)x12);
+    x77 = (x10 + x76);
+    x78 = (x9 + x77);
+    x79 = (x7 + (uint32_t)x8);
+    x80 = (x6 + x79);
+    x81 = (x5 + x80);
+    x82 = (x3 + (uint32_t)x4);
+    x83 = (x2 + x82);
+    x84 = (x1 + x83);
+    out1[0] = x51;
+    out1[1] = x54;
+    out1[2] = x57;
+    out1[3] = x60;
+    out1[4] = x63;
     out1[5] = x66;
-    out1[6] = x67;
-    out1[7] = x68;
-    out1[8] = x69;
-    out1[9] = x70;
-    out1[10] = x71;
-    out1[11] = x51;
+    out1[6] = x69;
+    out1[7] = x72;
+    out1[8] = x75;
+    out1[9] = x78;
+    out1[10] = x81;
+    out1[11] = x84;
 }
 
 /* END verbatim fiat code */
@@ -19202,7 +19278,7 @@ scalar_wnaf(int8_t out[385], const unsigned char in[48])
 }
 
 /*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
  * NB: not constant time
  */
 static void
@@ -19212,7 +19288,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[48],
     int i, d, is_neg, is_inf = 1, flipped = 0;
     int8_t anaf[385] = { 0 };
     int8_t bnaf[385] = { 0 };
-    pt_prj_t Q;
+    pt_prj_t Q = { 0 };
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
@@ -19281,14 +19357,14 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[48],
 {
     int i, j, d, diff, is_neg;
     int8_t rnaf[77] = { 0 };
-    pt_prj_t Q, lut;
+    pt_prj_t Q = { 0 }, lut = { 0 };
     pt_prj_t precomp[DRADIX / 2];
 
     precomp_wnaf(precomp, P);
     scalar_rwnaf(rnaf, scalar);
 
 #if defined(_MSC_VER)
-/* result still unsigned: yes we know */
+    /* result still unsigned: yes we know */
 #pragma warning(push)
 #pragma warning(disable : 4146)
 #endif
@@ -19350,8 +19426,8 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
 {
     int i, j, k, d, diff, is_neg = 0;
     int8_t rnaf[77] = { 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);
 
@@ -19361,7 +19437,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
     fe_set_zero(Q.Z);
 
 #if defined(_MSC_VER)
-/* result still unsigned: yes we know */
+    /* result still unsigned: yes we know */
 #pragma warning(push)
 #pragma warning(disable : 4146)
 #endif
@@ -19408,6 +19484,12 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[48])
     fiat_secp384r1_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[48], unsigned char outy[48],
               const unsigned char a[48], const unsigned char b[48],
@@ -19429,6 +19511,11 @@ point_mul_two(unsigned char outx[48], unsigned char outy[48],
     fiat_secp384r1_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[48], unsigned char outy[48],
             const unsigned char scalar[48])
@@ -19443,6 +19530,12 @@ point_mul_g(unsigned char outx[48], unsigned char outy[48],
     fiat_secp384r1_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[48], unsigned char outy[48],
           const unsigned char scalar[48],
@@ -19465,6 +19558,7 @@ point_mul(unsigned char outx[48], unsigned char outy[48],
 
 #undef RADIX
 #include "ecp.h"
+#include "mpi-priv.h"
 #include "mplogic.h"
 
 /*-
@@ -19559,7 +19653,7 @@ point_mul_g_secp384r1(const mp_int *n, mp_int *out_x,
     ARGCHK(n != NULL && out_x != NULL && out_y != NULL, MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != 1)
+    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 48));
@@ -19589,7 +19683,7 @@ point_mul_secp384r1(const mp_int *n, const mp_int *in_x,
            MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != 1)
+    if (mpl_significant_bits(n) > 384 || mp_cmp_z(n) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 48));
@@ -19620,20 +19714,20 @@ point_mul_two_secp384r1(const mp_int *n1, const mp_int *n2,
     unsigned char b_n2[48];
     mp_err res;
 
-    /* If n2 == NULL, this is just a base-point multiplication. */
-    if (n2 == NULL)
+    /* If n2 == NULL or 0, this is just a base-point multiplication. */
+    if (n2 == NULL || mp_cmp_z(n2) == MP_EQ)
         return point_mul_g_secp384r1(n1, out_x, out_y, group);
 
-    /* If n1 == NULL, this is just an arbitary-point multiplication. */
-    if (n1 == NULL)
+    /* If n1 == NULL or 0, this is just an arbitary-point multiplication. */
+    if (n1 == NULL || mp_cmp_z(n1) == MP_EQ)
         return point_mul_secp384r1(n2, in_x, in_y, out_x, out_y, group);
 
     ARGCHK(in_x != NULL && in_y != NULL && out_x != NULL && out_y != NULL,
            MP_BADARG);
 
     /* fail on out of range scalars */
-    if (mpl_significant_bits(n1) > 384 || mp_cmp_z(n1) != 1 ||
-        mpl_significant_bits(n2) > 384 || mp_cmp_z(n2) != 1)
+    if (mpl_significant_bits(n1) > 384 || mp_cmp_z(n1) != MP_GT ||
+        mpl_significant_bits(n2) > 384 || mp_cmp_z(n2) != MP_GT)
         return MP_RANGE;
 
     MP_CHECKOK(mp_to_fixlen_octets(n1, b_n1, 48));