+
+ /*
+ * Original product was up to (2^256-1)^2, i.e. a 512-bit integer.
+ * This was split into two parts (upper of 257 bits, lower of 255
+ * bits), and the upper was added to the lower with a factor 19,
+ * which means that the intermediate value is less than 77*2^255
+ * (19*2^257 + 2^255). Therefore, the extra bits "t[8] >> 15" are
+ * less than 77, and the initial carry cc is at most 76*19 = 1444.
+ */
+ cc = MUL15(t[8] >> 15, 19);