src/field_10x26_impl.h

   1 /**********************************************************************
   2  * Copyright (c) 2013, 2014 Pieter Wuille                             *
   3  * Distributed under the MIT software license, see the accompanying   *
   4  * file COPYING or http://www.opensource.org/licenses/mit-license.php.*
   5  **********************************************************************/
   6
   7 #ifndef _SECP256K1_FIELD_REPR_IMPL_H_
   8 #define _SECP256K1_FIELD_REPR_IMPL_H_
   9
  10 #include <stdio.h>
  11 #include <string.h>
  12 #include "util.h"
  13 #include "num.h"
  14 #include "field.h"
  15
  16 #ifdef VERIFY
  17 static void secp256k1_fe_verify(const secp256k1_fe *a) {
  18     const uint32_t *d = a->n;
  19     int m = a->normalized ? 1 : 2 * a->magnitude, r = 1;
  20     r &= (d[0] <= 0x3FFFFFFUL * m);
  21     r &= (d[1] <= 0x3FFFFFFUL * m);
  22     r &= (d[2] <= 0x3FFFFFFUL * m);
  23     r &= (d[3] <= 0x3FFFFFFUL * m);
  24     r &= (d[4] <= 0x3FFFFFFUL * m);
  25     r &= (d[5] <= 0x3FFFFFFUL * m);
  26     r &= (d[6] <= 0x3FFFFFFUL * m);
  27     r &= (d[7] <= 0x3FFFFFFUL * m);
  28     r &= (d[8] <= 0x3FFFFFFUL * m);
  29     r &= (d[9] <= 0x03FFFFFUL * m);
  30     r &= (a->magnitude >= 0);
  31     r &= (a->magnitude <= 32);
  32     if (a->normalized) {
  33         r &= (a->magnitude <= 1);
  34         if (r && (d[9] == 0x03FFFFFUL)) {
  35             uint32_t mid = d[8] & d[7] & d[6] & d[5] & d[4] & d[3] & d[2];
  36             if (mid == 0x3FFFFFFUL) {
  37                 r &= ((d[1] + 0x40UL + ((d[0] + 0x3D1UL) >> 26)) <= 0x3FFFFFFUL);
  38             }
  39         }
  40     }
  41     VERIFY_CHECK(r == 1);
  42 }
  43 #else
  44 static void secp256k1_fe_verify(const secp256k1_fe *a) {
  45     (void)a;
  46 }
  47 #endif
  48
  49 static void secp256k1_fe_normalize(secp256k1_fe *r) {
  50     uint32_t t0 = r->n[0], t1 = r->n[1], t2 = r->n[2], t3 = r->n[3], t4 = r->n[4],
  51              t5 = r->n[5], t6 = r->n[6], t7 = r->n[7], t8 = r->n[8], t9 = r->n[9];
  52
  53     /* Reduce t9 at the start so there will be at most a single carry from the first pass */
  54     uint32_t m;
  55     uint32_t x = t9 >> 22; t9 &= 0x03FFFFFUL;
  56
  57     /* The first pass ensures the magnitude is 1, ... */
  58     t0 += x * 0x3D1UL; t1 += (x << 6);
  59     t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL;
  60     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL;
  61     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL; m = t2;
  62     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL; m &= t3;
  63     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL; m &= t4;
  64     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL; m &= t5;
  65     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL; m &= t6;
  66     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL; m &= t7;
  67     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL; m &= t8;
  68
  69     /* ... except for a possible carry at bit 22 of t9 (i.e. bit 256 of the field element) */
  70     VERIFY_CHECK(t9 >> 23 == 0);
  71
  72     /* At most a single final reduction is needed; check if the value is >= the field characteristic */
  73     x = (t9 >> 22) | ((t9 == 0x03FFFFFUL) & (m == 0x3FFFFFFUL)
  74         & ((t1 + 0x40UL + ((t0 + 0x3D1UL) >> 26)) > 0x3FFFFFFUL));
  75
  76     /* Apply the final reduction (for constant-time behaviour, we do it always) */
  77     t0 += x * 0x3D1UL; t1 += (x << 6);
  78     t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL;
  79     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL;
  80     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL;
  81     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL;
  82     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL;
  83     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL;
  84     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL;
  85     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL;
  86     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL;
  87
  88     /* If t9 didn't carry to bit 22 already, then it should have after any final reduction */
  89     VERIFY_CHECK(t9 >> 22 == x);
  90
  91     /* Mask off the possible multiple of 2^256 from the final reduction */
  92     t9 &= 0x03FFFFFUL;
  93
  94     r->n[0] = t0; r->n[1] = t1; r->n[2] = t2; r->n[3] = t3; r->n[4] = t4;
  95     r->n[5] = t5; r->n[6] = t6; r->n[7] = t7; r->n[8] = t8; r->n[9] = t9;
  96
  97 #ifdef VERIFY
  98     r->magnitude = 1;
  99     r->normalized = 1;
 100     secp256k1_fe_verify(r);
 101 #endif
 102 }
 103
 104 static void secp256k1_fe_normalize_weak(secp256k1_fe *r) {
 105     uint32_t t0 = r->n[0], t1 = r->n[1], t2 = r->n[2], t3 = r->n[3], t4 = r->n[4],
 106              t5 = r->n[5], t6 = r->n[6], t7 = r->n[7], t8 = r->n[8], t9 = r->n[9];
 107
 108     /* Reduce t9 at the start so there will be at most a single carry from the first pass */
 109     uint32_t x = t9 >> 22; t9 &= 0x03FFFFFUL;
 110
 111     /* The first pass ensures the magnitude is 1, ... */
 112     t0 += x * 0x3D1UL; t1 += (x << 6);
 113     t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL;
 114     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL;
 115     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL;
 116     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL;
 117     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL;
 118     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL;
 119     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL;
 120     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL;
 121     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL;
 122
 123     /* ... except for a possible carry at bit 22 of t9 (i.e. bit 256 of the field element) */
 124     VERIFY_CHECK(t9 >> 23 == 0);
 125
 126     r->n[0] = t0; r->n[1] = t1; r->n[2] = t2; r->n[3] = t3; r->n[4] = t4;
 127     r->n[5] = t5; r->n[6] = t6; r->n[7] = t7; r->n[8] = t8; r->n[9] = t9;
 128
 129 #ifdef VERIFY
 130     r->magnitude = 1;
 131     secp256k1_fe_verify(r);
 132 #endif
 133 }
 134
 135 static void secp256k1_fe_normalize_var(secp256k1_fe *r) {
 136     uint32_t t0 = r->n[0], t1 = r->n[1], t2 = r->n[2], t3 = r->n[3], t4 = r->n[4],
 137              t5 = r->n[5], t6 = r->n[6], t7 = r->n[7], t8 = r->n[8], t9 = r->n[9];
 138
 139     /* Reduce t9 at the start so there will be at most a single carry from the first pass */
 140     uint32_t m;
 141     uint32_t x = t9 >> 22; t9 &= 0x03FFFFFUL;
 142
 143     /* The first pass ensures the magnitude is 1, ... */
 144     t0 += x * 0x3D1UL; t1 += (x << 6);
 145     t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL;
 146     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL;
 147     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL; m = t2;
 148     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL; m &= t3;
 149     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL; m &= t4;
 150     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL; m &= t5;
 151     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL; m &= t6;
 152     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL; m &= t7;
 153     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL; m &= t8;
 154
 155     /* ... except for a possible carry at bit 22 of t9 (i.e. bit 256 of the field element) */
 156     VERIFY_CHECK(t9 >> 23 == 0);
 157
 158     /* At most a single final reduction is needed; check if the value is >= the field characteristic */
 159     x = (t9 >> 22) | ((t9 == 0x03FFFFFUL) & (m == 0x3FFFFFFUL)
 160         & ((t1 + 0x40UL + ((t0 + 0x3D1UL) >> 26)) > 0x3FFFFFFUL));
 161
 162     if (x) {
 163         t0 += 0x3D1UL; t1 += (x << 6);
 164         t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL;
 165         t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL;
 166         t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL;
 167         t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL;
 168         t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL;
 169         t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL;
 170         t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL;
 171         t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL;
 172         t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL;
 173
 174         /* If t9 didn't carry to bit 22 already, then it should have after any final reduction */
 175         VERIFY_CHECK(t9 >> 22 == x);
 176
 177         /* Mask off the possible multiple of 2^256 from the final reduction */
 178         t9 &= 0x03FFFFFUL;
 179     }
 180
 181     r->n[0] = t0; r->n[1] = t1; r->n[2] = t2; r->n[3] = t3; r->n[4] = t4;
 182     r->n[5] = t5; r->n[6] = t6; r->n[7] = t7; r->n[8] = t8; r->n[9] = t9;
 183
 184 #ifdef VERIFY
 185     r->magnitude = 1;
 186     r->normalized = 1;
 187     secp256k1_fe_verify(r);
 188 #endif
 189 }
 190
 191 static int secp256k1_fe_normalizes_to_zero(secp256k1_fe *r) {
 192     uint32_t t0 = r->n[0], t1 = r->n[1], t2 = r->n[2], t3 = r->n[3], t4 = r->n[4],
 193              t5 = r->n[5], t6 = r->n[6], t7 = r->n[7], t8 = r->n[8], t9 = r->n[9];
 194
 195     /* z0 tracks a possible raw value of 0, z1 tracks a possible raw value of P */
 196     uint32_t z0, z1;
 197
 198     /* Reduce t9 at the start so there will be at most a single carry from the first pass */
 199     uint32_t x = t9 >> 22; t9 &= 0x03FFFFFUL;
 200
 201     /* The first pass ensures the magnitude is 1, ... */
 202     t0 += x * 0x3D1UL; t1 += (x << 6);
 203     t1 += (t0 >> 26); t0 &= 0x3FFFFFFUL; z0  = t0; z1  = t0 ^ 0x3D0UL;
 204     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL; z0 |= t1; z1 &= t1 ^ 0x40UL;
 205     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL; z0 |= t2; z1 &= t2;
 206     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL; z0 |= t3; z1 &= t3;
 207     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL; z0 |= t4; z1 &= t4;
 208     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL; z0 |= t5; z1 &= t5;
 209     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL; z0 |= t6; z1 &= t6;
 210     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL; z0 |= t7; z1 &= t7;
 211     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL; z0 |= t8; z1 &= t8;
 212                                          z0 |= t9; z1 &= t9 ^ 0x3C00000UL;
 213
 214     /* ... except for a possible carry at bit 22 of t9 (i.e. bit 256 of the field element) */
 215     VERIFY_CHECK(t9 >> 23 == 0);
 216
 217     return (z0 == 0) | (z1 == 0x3FFFFFFUL);
 218 }
 219
 220 static int secp256k1_fe_normalizes_to_zero_var(secp256k1_fe *r) {
 221     uint32_t t0, t1, t2, t3, t4, t5, t6, t7, t8, t9;
 222     uint32_t z0, z1;
 223     uint32_t x;
 224
 225     t0 = r->n[0];
 226     t9 = r->n[9];
 227
 228     /* Reduce t9 at the start so there will be at most a single carry from the first pass */
 229     x = t9 >> 22;
 230
 231     /* The first pass ensures the magnitude is 1, ... */
 232     t0 += x * 0x3D1UL;
 233
 234     /* z0 tracks a possible raw value of 0, z1 tracks a possible raw value of P */
 235     z0 = t0 & 0x3FFFFFFUL;
 236     z1 = z0 ^ 0x3D0UL;
 237
 238     /* Fast return path should catch the majority of cases */
 239     if ((z0 != 0UL) & (z1 != 0x3FFFFFFUL)) {
 240         return 0;
 241     }
 242
 243     t1 = r->n[1];
 244     t2 = r->n[2];
 245     t3 = r->n[3];
 246     t4 = r->n[4];
 247     t5 = r->n[5];
 248     t6 = r->n[6];
 249     t7 = r->n[7];
 250     t8 = r->n[8];
 251
 252     t9 &= 0x03FFFFFUL;
 253     t1 += (x << 6);
 254
 255     t1 += (t0 >> 26);
 256     t2 += (t1 >> 26); t1 &= 0x3FFFFFFUL; z0 |= t1; z1 &= t1 ^ 0x40UL;
 257     t3 += (t2 >> 26); t2 &= 0x3FFFFFFUL; z0 |= t2; z1 &= t2;
 258     t4 += (t3 >> 26); t3 &= 0x3FFFFFFUL; z0 |= t3; z1 &= t3;
 259     t5 += (t4 >> 26); t4 &= 0x3FFFFFFUL; z0 |= t4; z1 &= t4;
 260     t6 += (t5 >> 26); t5 &= 0x3FFFFFFUL; z0 |= t5; z1 &= t5;
 261     t7 += (t6 >> 26); t6 &= 0x3FFFFFFUL; z0 |= t6; z1 &= t6;
 262     t8 += (t7 >> 26); t7 &= 0x3FFFFFFUL; z0 |= t7; z1 &= t7;
 263     t9 += (t8 >> 26); t8 &= 0x3FFFFFFUL; z0 |= t8; z1 &= t8;
 264                                          z0 |= t9; z1 &= t9 ^ 0x3C00000UL;
 265
 266     /* ... except for a possible carry at bit 22 of t9 (i.e. bit 256 of the field element) */
 267     VERIFY_CHECK(t9 >> 23 == 0);
 268
 269     return (z0 == 0) | (z1 == 0x3FFFFFFUL);
 270 }
 271
 272 SECP256K1_INLINE static void secp256k1_fe_set_int(secp256k1_fe *r, int a) {
 273     r->n[0] = a;
 274     r->n[1] = r->n[2] = r->n[3] = r->n[4] = r->n[5] = r->n[6] = r->n[7] = r->n[8] = r->n[9] = 0;
 275 #ifdef VERIFY
 276     r->magnitude = 1;
 277     r->normalized = 1;
 278     secp256k1_fe_verify(r);
 279 #endif
 280 }
 281
 282 SECP256K1_INLINE static int secp256k1_fe_is_zero(const secp256k1_fe *a) {
 283     const uint32_t *t = a->n;
 284 #ifdef VERIFY
 285     VERIFY_CHECK(a->normalized);
 286     secp256k1_fe_verify(a);
 287 #endif
 288     return (t[0] | t[1] | t[2] | t[3] | t[4] | t[5] | t[6] | t[7] | t[8] | t[9]) == 0;
 289 }
 290
 291 SECP256K1_INLINE static int secp256k1_fe_is_odd(const secp256k1_fe *a) {
 292 #ifdef VERIFY
 293     VERIFY_CHECK(a->normalized);
 294     secp256k1_fe_verify(a);
 295 #endif
 296     return a->n[0] & 1;
 297 }
 298
 299 SECP256K1_INLINE static void secp256k1_fe_clear(secp256k1_fe *a) {
 300     int i;
 301 #ifdef VERIFY
 302     a->magnitude = 0;
 303     a->normalized = 1;
 304 #endif
 305     for (i=0; i<10; i++) {
 306         a->n[i] = 0;
 307     }
 308 }
 309
 310 static int secp256k1_fe_cmp_var(const secp256k1_fe *a, const secp256k1_fe *b) {
 311     int i;
 312 #ifdef VERIFY
 313     VERIFY_CHECK(a->normalized);
 314     VERIFY_CHECK(b->normalized);
 315     secp256k1_fe_verify(a);
 316     secp256k1_fe_verify(b);
 317 #endif
 318     for (i = 9; i >= 0; i--) {
 319         if (a->n[i] > b->n[i]) {
 320             return 1;
 321         }
 322         if (a->n[i] < b->n[i]) {
 323             return -1;
 324         }
 325     }
 326     return 0;
 327 }
 328
 329 static int secp256k1_fe_set_b32(secp256k1_fe *r, const unsigned char *a) {
 330     int i;
 331     r->n[0] = r->n[1] = r->n[2] = r->n[3] = r->n[4] = 0;
 332     r->n[5] = r->n[6] = r->n[7] = r->n[8] = r->n[9] = 0;
 333     for (i=0; i<32; i++) {
 334         int j;
 335         for (j=0; j<4; j++) {
 336             int limb = (8*i+2*j)/26;
 337             int shift = (8*i+2*j)%26;
 338             r->n[limb] |= (uint32_t)((a[31-i] >> (2*j)) & 0x3) << shift;
 339         }
 340     }
 341     if (r->n[9] == 0x3FFFFFUL && (r->n[8] & r->n[7] & r->n[6] & r->n[5] & r->n[4] & r->n[3] & r->n[2]) == 0x3FFFFFFUL && (r->n[1] + 0x40UL + ((r->n[0] + 0x3D1UL) >> 26)) > 0x3FFFFFFUL) {
 342         return 0;
 343     }
 344 #ifdef VERIFY
 345     r->magnitude = 1;
 346     r->normalized = 1;
 347     secp256k1_fe_verify(r);
 348 #endif
 349     return 1;
 350 }
 351
 352 /** Convert a field element to a 32-byte big endian value. Requires the input to be normalized */
 353 static void secp256k1_fe_get_b32(unsigned char *r, const secp256k1_fe *a) {
 354     int i;
 355 #ifdef VERIFY
 356     VERIFY_CHECK(a->normalized);
 357     secp256k1_fe_verify(a);
 358 #endif
 359     for (i=0; i<32; i++) {
 360         int j;
 361         int c = 0;
 362         for (j=0; j<4; j++) {
 363             int limb = (8*i+2*j)/26;
 364             int shift = (8*i+2*j)%26;
 365             c |= ((a->n[limb] >> shift) & 0x3) << (2 * j);
 366         }
 367         r[31-i] = c;
 368     }
 369 }
 370
 371 SECP256K1_INLINE static void secp256k1_fe_negate(secp256k1_fe *r, const secp256k1_fe *a, int m) {
 372 #ifdef VERIFY
 373     VERIFY_CHECK(a->magnitude <= m);
 374     secp256k1_fe_verify(a);
 375 #endif
 376     r->n[0] = 0x3FFFC2FUL * 2 * (m + 1) - a->n[0];
 377     r->n[1] = 0x3FFFFBFUL * 2 * (m + 1) - a->n[1];
 378     r->n[2] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[2];
 379     r->n[3] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[3];
 380     r->n[4] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[4];
 381     r->n[5] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[5];
 382     r->n[6] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[6];
 383     r->n[7] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[7];
 384     r->n[8] = 0x3FFFFFFUL * 2 * (m + 1) - a->n[8];
 385     r->n[9] = 0x03FFFFFUL * 2 * (m + 1) - a->n[9];
 386 #ifdef VERIFY
 387     r->magnitude = m + 1;
 388     r->normalized = 0;
 389     secp256k1_fe_verify(r);
 390 #endif
 391 }
 392
 393 SECP256K1_INLINE static void secp256k1_fe_mul_int(secp256k1_fe *r, int a) {
 394     r->n[0] *= a;
 395     r->n[1] *= a;
 396     r->n[2] *= a;
 397     r->n[3] *= a;
 398     r->n[4] *= a;
 399     r->n[5] *= a;
 400     r->n[6] *= a;
 401     r->n[7] *= a;
 402     r->n[8] *= a;
 403     r->n[9] *= a;
 404 #ifdef VERIFY
 405     r->magnitude *= a;
 406     r->normalized = 0;
 407     secp256k1_fe_verify(r);
 408 #endif
 409 }
 410
 411 SECP256K1_INLINE static void secp256k1_fe_add(secp256k1_fe *r, const secp256k1_fe *a) {
 412 #ifdef VERIFY
 413     secp256k1_fe_verify(a);
 414 #endif
 415     r->n[0] += a->n[0];
 416     r->n[1] += a->n[1];
 417     r->n[2] += a->n[2];
 418     r->n[3] += a->n[3];
 419     r->n[4] += a->n[4];
 420     r->n[5] += a->n[5];
 421     r->n[6] += a->n[6];
 422     r->n[7] += a->n[7];
 423     r->n[8] += a->n[8];
 424     r->n[9] += a->n[9];
 425 #ifdef VERIFY
 426     r->magnitude += a->magnitude;
 427     r->normalized = 0;
 428     secp256k1_fe_verify(r);
 429 #endif
 430 }
 431
 432 #if defined(USE_EXTERNAL_ASM)
 433
 434 /* External assembler implementation */
 435 void secp256k1_fe_mul_inner(uint32_t *r, const uint32_t *a, const uint32_t * SECP256K1_RESTRICT b);
 436 void secp256k1_fe_sqr_inner(uint32_t *r, const uint32_t *a);
 437
 438 #else
 439
 440 #ifdef VERIFY
 441 #define VERIFY_BITS(x, n) VERIFY_CHECK(((x) >> (n)) == 0)
 442 #else
 443 #define VERIFY_BITS(x, n) do { } while(0)
 444 #endif
 445
 446 SECP256K1_INLINE static void secp256k1_fe_mul_inner(uint32_t *r, const uint32_t *a, const uint32_t * SECP256K1_RESTRICT b) {
 447     uint64_t c, d;
 448     uint64_t u0, u1, u2, u3, u4, u5, u6, u7, u8;
 449     uint32_t t9, t1, t0, t2, t3, t4, t5, t6, t7;
 450     const uint32_t M = 0x3FFFFFFUL, R0 = 0x3D10UL, R1 = 0x400UL;
 451
 452     VERIFY_BITS(a[0], 30);
 453     VERIFY_BITS(a[1], 30);
 454     VERIFY_BITS(a[2], 30);
 455     VERIFY_BITS(a[3], 30);
 456     VERIFY_BITS(a[4], 30);
 457     VERIFY_BITS(a[5], 30);
 458     VERIFY_BITS(a[6], 30);
 459     VERIFY_BITS(a[7], 30);
 460     VERIFY_BITS(a[8], 30);
 461     VERIFY_BITS(a[9], 26);
 462     VERIFY_BITS(b[0], 30);
 463     VERIFY_BITS(b[1], 30);
 464     VERIFY_BITS(b[2], 30);
 465     VERIFY_BITS(b[3], 30);
 466     VERIFY_BITS(b[4], 30);
 467     VERIFY_BITS(b[5], 30);
 468     VERIFY_BITS(b[6], 30);
 469     VERIFY_BITS(b[7], 30);
 470     VERIFY_BITS(b[8], 30);
 471     VERIFY_BITS(b[9], 26);
 472
 473     /** [... a b c] is a shorthand for ... + a<<52 + b<<26 + c<<0 mod n.
 474      *  px is a shorthand for sum(a[i]*b[x-i], i=0..x).
 475      *  Note that [x 0 0 0 0 0 0 0 0 0 0] = [x*R1 x*R0].
 476      */
 477
 478     d  = (uint64_t)a[0] * b[9]
 479        + (uint64_t)a[1] * b[8]
 480        + (uint64_t)a[2] * b[7]
 481        + (uint64_t)a[3] * b[6]
 482        + (uint64_t)a[4] * b[5]
 483        + (uint64_t)a[5] * b[4]
 484        + (uint64_t)a[6] * b[3]
 485        + (uint64_t)a[7] * b[2]
 486        + (uint64_t)a[8] * b[1]
 487        + (uint64_t)a[9] * b[0];
 488     /* VERIFY_BITS(d, 64); */
 489     /* [d 0 0 0 0 0 0 0 0 0] = [p9 0 0 0 0 0 0 0 0 0] */
 490     t9 = d & M; d >>= 26;
 491     VERIFY_BITS(t9, 26);
 492     VERIFY_BITS(d, 38);
 493     /* [d t9 0 0 0 0 0 0 0 0 0] = [p9 0 0 0 0 0 0 0 0 0] */
 494
 495     c  = (uint64_t)a[0] * b[0];
 496     VERIFY_BITS(c, 60);
 497     /* [d t9 0 0 0 0 0 0 0 0 c] = [p9 0 0 0 0 0 0 0 0 p0] */
 498     d += (uint64_t)a[1] * b[9]
 499        + (uint64_t)a[2] * b[8]
 500        + (uint64_t)a[3] * b[7]
 501        + (uint64_t)a[4] * b[6]
 502        + (uint64_t)a[5] * b[5]
 503        + (uint64_t)a[6] * b[4]
 504        + (uint64_t)a[7] * b[3]
 505        + (uint64_t)a[8] * b[2]
 506        + (uint64_t)a[9] * b[1];
 507     VERIFY_BITS(d, 63);
 508     /* [d t9 0 0 0 0 0 0 0 0 c] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 509     u0 = d & M; d >>= 26; c += u0 * R0;
 510     VERIFY_BITS(u0, 26);
 511     VERIFY_BITS(d, 37);
 512     VERIFY_BITS(c, 61);
 513     /* [d u0 t9 0 0 0 0 0 0 0 0 c-u0*R0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 514     t0 = c & M; c >>= 26; c += u0 * R1;
 515     VERIFY_BITS(t0, 26);
 516     VERIFY_BITS(c, 37);
 517     /* [d u0 t9 0 0 0 0 0 0 0 c-u0*R1 t0-u0*R0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 518     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 519
 520     c += (uint64_t)a[0] * b[1]
 521        + (uint64_t)a[1] * b[0];
 522     VERIFY_BITS(c, 62);
 523     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p10 p9 0 0 0 0 0 0 0 p1 p0] */
 524     d += (uint64_t)a[2] * b[9]
 525        + (uint64_t)a[3] * b[8]
 526        + (uint64_t)a[4] * b[7]
 527        + (uint64_t)a[5] * b[6]
 528        + (uint64_t)a[6] * b[5]
 529        + (uint64_t)a[7] * b[4]
 530        + (uint64_t)a[8] * b[3]
 531        + (uint64_t)a[9] * b[2];
 532     VERIFY_BITS(d, 63);
 533     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 534     u1 = d & M; d >>= 26; c += u1 * R0;
 535     VERIFY_BITS(u1, 26);
 536     VERIFY_BITS(d, 37);
 537     VERIFY_BITS(c, 63);
 538     /* [d u1 0 t9 0 0 0 0 0 0 0 c-u1*R0 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 539     t1 = c & M; c >>= 26; c += u1 * R1;
 540     VERIFY_BITS(t1, 26);
 541     VERIFY_BITS(c, 38);
 542     /* [d u1 0 t9 0 0 0 0 0 0 c-u1*R1 t1-u1*R0 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 543     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 544
 545     c += (uint64_t)a[0] * b[2]
 546        + (uint64_t)a[1] * b[1]
 547        + (uint64_t)a[2] * b[0];
 548     VERIFY_BITS(c, 62);
 549     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 550     d += (uint64_t)a[3] * b[9]
 551        + (uint64_t)a[4] * b[8]
 552        + (uint64_t)a[5] * b[7]
 553        + (uint64_t)a[6] * b[6]
 554        + (uint64_t)a[7] * b[5]
 555        + (uint64_t)a[8] * b[4]
 556        + (uint64_t)a[9] * b[3];
 557     VERIFY_BITS(d, 63);
 558     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 559     u2 = d & M; d >>= 26; c += u2 * R0;
 560     VERIFY_BITS(u2, 26);
 561     VERIFY_BITS(d, 37);
 562     VERIFY_BITS(c, 63);
 563     /* [d u2 0 0 t9 0 0 0 0 0 0 c-u2*R0 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 564     t2 = c & M; c >>= 26; c += u2 * R1;
 565     VERIFY_BITS(t2, 26);
 566     VERIFY_BITS(c, 38);
 567     /* [d u2 0 0 t9 0 0 0 0 0 c-u2*R1 t2-u2*R0 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 568     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 569
 570     c += (uint64_t)a[0] * b[3]
 571        + (uint64_t)a[1] * b[2]
 572        + (uint64_t)a[2] * b[1]
 573        + (uint64_t)a[3] * b[0];
 574     VERIFY_BITS(c, 63);
 575     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 576     d += (uint64_t)a[4] * b[9]
 577        + (uint64_t)a[5] * b[8]
 578        + (uint64_t)a[6] * b[7]
 579        + (uint64_t)a[7] * b[6]
 580        + (uint64_t)a[8] * b[5]
 581        + (uint64_t)a[9] * b[4];
 582     VERIFY_BITS(d, 63);
 583     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 584     u3 = d & M; d >>= 26; c += u3 * R0;
 585     VERIFY_BITS(u3, 26);
 586     VERIFY_BITS(d, 37);
 587     /* VERIFY_BITS(c, 64); */
 588     /* [d u3 0 0 0 t9 0 0 0 0 0 c-u3*R0 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 589     t3 = c & M; c >>= 26; c += u3 * R1;
 590     VERIFY_BITS(t3, 26);
 591     VERIFY_BITS(c, 39);
 592     /* [d u3 0 0 0 t9 0 0 0 0 c-u3*R1 t3-u3*R0 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 593     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 594
 595     c += (uint64_t)a[0] * b[4]
 596        + (uint64_t)a[1] * b[3]
 597        + (uint64_t)a[2] * b[2]
 598        + (uint64_t)a[3] * b[1]
 599        + (uint64_t)a[4] * b[0];
 600     VERIFY_BITS(c, 63);
 601     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 602     d += (uint64_t)a[5] * b[9]
 603        + (uint64_t)a[6] * b[8]
 604        + (uint64_t)a[7] * b[7]
 605        + (uint64_t)a[8] * b[6]
 606        + (uint64_t)a[9] * b[5];
 607     VERIFY_BITS(d, 62);
 608     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 609     u4 = d & M; d >>= 26; c += u4 * R0;
 610     VERIFY_BITS(u4, 26);
 611     VERIFY_BITS(d, 36);
 612     /* VERIFY_BITS(c, 64); */
 613     /* [d u4 0 0 0 0 t9 0 0 0 0 c-u4*R0 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 614     t4 = c & M; c >>= 26; c += u4 * R1;
 615     VERIFY_BITS(t4, 26);
 616     VERIFY_BITS(c, 39);
 617     /* [d u4 0 0 0 0 t9 0 0 0 c-u4*R1 t4-u4*R0 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 618     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 619
 620     c += (uint64_t)a[0] * b[5]
 621        + (uint64_t)a[1] * b[4]
 622        + (uint64_t)a[2] * b[3]
 623        + (uint64_t)a[3] * b[2]
 624        + (uint64_t)a[4] * b[1]
 625        + (uint64_t)a[5] * b[0];
 626     VERIFY_BITS(c, 63);
 627     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 628     d += (uint64_t)a[6] * b[9]
 629        + (uint64_t)a[7] * b[8]
 630        + (uint64_t)a[8] * b[7]
 631        + (uint64_t)a[9] * b[6];
 632     VERIFY_BITS(d, 62);
 633     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 634     u5 = d & M; d >>= 26; c += u5 * R0;
 635     VERIFY_BITS(u5, 26);
 636     VERIFY_BITS(d, 36);
 637     /* VERIFY_BITS(c, 64); */
 638     /* [d u5 0 0 0 0 0 t9 0 0 0 c-u5*R0 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 639     t5 = c & M; c >>= 26; c += u5 * R1;
 640     VERIFY_BITS(t5, 26);
 641     VERIFY_BITS(c, 39);
 642     /* [d u5 0 0 0 0 0 t9 0 0 c-u5*R1 t5-u5*R0 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 643     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 644
 645     c += (uint64_t)a[0] * b[6]
 646        + (uint64_t)a[1] * b[5]
 647        + (uint64_t)a[2] * b[4]
 648        + (uint64_t)a[3] * b[3]
 649        + (uint64_t)a[4] * b[2]
 650        + (uint64_t)a[5] * b[1]
 651        + (uint64_t)a[6] * b[0];
 652     VERIFY_BITS(c, 63);
 653     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 654     d += (uint64_t)a[7] * b[9]
 655        + (uint64_t)a[8] * b[8]
 656        + (uint64_t)a[9] * b[7];
 657     VERIFY_BITS(d, 61);
 658     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 659     u6 = d & M; d >>= 26; c += u6 * R0;
 660     VERIFY_BITS(u6, 26);
 661     VERIFY_BITS(d, 35);
 662     /* VERIFY_BITS(c, 64); */
 663     /* [d u6 0 0 0 0 0 0 t9 0 0 c-u6*R0 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 664     t6 = c & M; c >>= 26; c += u6 * R1;
 665     VERIFY_BITS(t6, 26);
 666     VERIFY_BITS(c, 39);
 667     /* [d u6 0 0 0 0 0 0 t9 0 c-u6*R1 t6-u6*R0 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 668     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 669
 670     c += (uint64_t)a[0] * b[7]
 671        + (uint64_t)a[1] * b[6]
 672        + (uint64_t)a[2] * b[5]
 673        + (uint64_t)a[3] * b[4]
 674        + (uint64_t)a[4] * b[3]
 675        + (uint64_t)a[5] * b[2]
 676        + (uint64_t)a[6] * b[1]
 677        + (uint64_t)a[7] * b[0];
 678     /* VERIFY_BITS(c, 64); */
 679     VERIFY_CHECK(c <= 0x8000007C00000007ULL);
 680     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 681     d += (uint64_t)a[8] * b[9]
 682        + (uint64_t)a[9] * b[8];
 683     VERIFY_BITS(d, 58);
 684     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 685     u7 = d & M; d >>= 26; c += u7 * R0;
 686     VERIFY_BITS(u7, 26);
 687     VERIFY_BITS(d, 32);
 688     /* VERIFY_BITS(c, 64); */
 689     VERIFY_CHECK(c <= 0x800001703FFFC2F7ULL);
 690     /* [d u7 0 0 0 0 0 0 0 t9 0 c-u7*R0 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 691     t7 = c & M; c >>= 26; c += u7 * R1;
 692     VERIFY_BITS(t7, 26);
 693     VERIFY_BITS(c, 38);
 694     /* [d u7 0 0 0 0 0 0 0 t9 c-u7*R1 t7-u7*R0 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 695     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 696
 697     c += (uint64_t)a[0] * b[8]
 698        + (uint64_t)a[1] * b[7]
 699        + (uint64_t)a[2] * b[6]
 700        + (uint64_t)a[3] * b[5]
 701        + (uint64_t)a[4] * b[4]
 702        + (uint64_t)a[5] * b[3]
 703        + (uint64_t)a[6] * b[2]
 704        + (uint64_t)a[7] * b[1]
 705        + (uint64_t)a[8] * b[0];
 706     /* VERIFY_BITS(c, 64); */
 707     VERIFY_CHECK(c <= 0x9000007B80000008ULL);
 708     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 709     d += (uint64_t)a[9] * b[9];
 710     VERIFY_BITS(d, 57);
 711     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 712     u8 = d & M; d >>= 26; c += u8 * R0;
 713     VERIFY_BITS(u8, 26);
 714     VERIFY_BITS(d, 31);
 715     /* VERIFY_BITS(c, 64); */
 716     VERIFY_CHECK(c <= 0x9000016FBFFFC2F8ULL);
 717     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 t4 t3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 718
 719     r[3] = t3;
 720     VERIFY_BITS(r[3], 26);
 721     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 t4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 722     r[4] = t4;
 723     VERIFY_BITS(r[4], 26);
 724     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 725     r[5] = t5;
 726     VERIFY_BITS(r[5], 26);
 727     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 728     r[6] = t6;
 729     VERIFY_BITS(r[6], 26);
 730     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 731     r[7] = t7;
 732     VERIFY_BITS(r[7], 26);
 733     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 734
 735     r[8] = c & M; c >>= 26; c += u8 * R1;
 736     VERIFY_BITS(r[8], 26);
 737     VERIFY_BITS(c, 39);
 738     /* [d u8 0 0 0 0 0 0 0 0 t9+c-u8*R1 r8-u8*R0 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 739     /* [d 0 0 0 0 0 0 0 0 0 t9+c r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 740     c   += d * R0 + t9;
 741     VERIFY_BITS(c, 45);
 742     /* [d 0 0 0 0 0 0 0 0 0 c-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 743     r[9] = c & (M >> 4); c >>= 22; c += d * (R1 << 4);
 744     VERIFY_BITS(r[9], 22);
 745     VERIFY_BITS(c, 46);
 746     /* [d 0 0 0 0 0 0 0 0 r9+((c-d*R1<<4)<<22)-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 747     /* [d 0 0 0 0 0 0 0 -d*R1 r9+(c<<22)-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 748     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 749
 750     d    = c * (R0 >> 4) + t0;
 751     VERIFY_BITS(d, 56);
 752     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1 d-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 753     r[0] = d & M; d >>= 26;
 754     VERIFY_BITS(r[0], 26);
 755     VERIFY_BITS(d, 30);
 756     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1+d r0-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 757     d   += c * (R1 >> 4) + t1;
 758     VERIFY_BITS(d, 53);
 759     VERIFY_CHECK(d <= 0x10000003FFFFBFULL);
 760     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 d-c*R1>>4 r0-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 761     /* [r9 r8 r7 r6 r5 r4 r3 t2 d r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 762     r[1] = d & M; d >>= 26;
 763     VERIFY_BITS(r[1], 26);
 764     VERIFY_BITS(d, 27);
 765     VERIFY_CHECK(d <= 0x4000000ULL);
 766     /* [r9 r8 r7 r6 r5 r4 r3 t2+d r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 767     d   += t2;
 768     VERIFY_BITS(d, 27);
 769     /* [r9 r8 r7 r6 r5 r4 r3 d r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 770     r[2] = d;
 771     VERIFY_BITS(r[2], 27);
 772     /* [r9 r8 r7 r6 r5 r4 r3 r2 r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 773 }
 774
 775 SECP256K1_INLINE static void secp256k1_fe_sqr_inner(uint32_t *r, const uint32_t *a) {
 776     uint64_t c, d;
 777     uint64_t u0, u1, u2, u3, u4, u5, u6, u7, u8;
 778     uint32_t t9, t0, t1, t2, t3, t4, t5, t6, t7;
 779     const uint32_t M = 0x3FFFFFFUL, R0 = 0x3D10UL, R1 = 0x400UL;
 780
 781     VERIFY_BITS(a[0], 30);
 782     VERIFY_BITS(a[1], 30);
 783     VERIFY_BITS(a[2], 30);
 784     VERIFY_BITS(a[3], 30);
 785     VERIFY_BITS(a[4], 30);
 786     VERIFY_BITS(a[5], 30);
 787     VERIFY_BITS(a[6], 30);
 788     VERIFY_BITS(a[7], 30);
 789     VERIFY_BITS(a[8], 30);
 790     VERIFY_BITS(a[9], 26);
 791
 792     /** [... a b c] is a shorthand for ... + a<<52 + b<<26 + c<<0 mod n.
 793      *  px is a shorthand for sum(a[i]*a[x-i], i=0..x).
 794      *  Note that [x 0 0 0 0 0 0 0 0 0 0] = [x*R1 x*R0].
 795      */
 796
 797     d  = (uint64_t)(a[0]*2) * a[9]
 798        + (uint64_t)(a[1]*2) * a[8]
 799        + (uint64_t)(a[2]*2) * a[7]
 800        + (uint64_t)(a[3]*2) * a[6]
 801        + (uint64_t)(a[4]*2) * a[5];
 802     /* VERIFY_BITS(d, 64); */
 803     /* [d 0 0 0 0 0 0 0 0 0] = [p9 0 0 0 0 0 0 0 0 0] */
 804     t9 = d & M; d >>= 26;
 805     VERIFY_BITS(t9, 26);
 806     VERIFY_BITS(d, 38);
 807     /* [d t9 0 0 0 0 0 0 0 0 0] = [p9 0 0 0 0 0 0 0 0 0] */
 808
 809     c  = (uint64_t)a[0] * a[0];
 810     VERIFY_BITS(c, 60);
 811     /* [d t9 0 0 0 0 0 0 0 0 c] = [p9 0 0 0 0 0 0 0 0 p0] */
 812     d += (uint64_t)(a[1]*2) * a[9]
 813        + (uint64_t)(a[2]*2) * a[8]
 814        + (uint64_t)(a[3]*2) * a[7]
 815        + (uint64_t)(a[4]*2) * a[6]
 816        + (uint64_t)a[5] * a[5];
 817     VERIFY_BITS(d, 63);
 818     /* [d t9 0 0 0 0 0 0 0 0 c] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 819     u0 = d & M; d >>= 26; c += u0 * R0;
 820     VERIFY_BITS(u0, 26);
 821     VERIFY_BITS(d, 37);
 822     VERIFY_BITS(c, 61);
 823     /* [d u0 t9 0 0 0 0 0 0 0 0 c-u0*R0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 824     t0 = c & M; c >>= 26; c += u0 * R1;
 825     VERIFY_BITS(t0, 26);
 826     VERIFY_BITS(c, 37);
 827     /* [d u0 t9 0 0 0 0 0 0 0 c-u0*R1 t0-u0*R0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 828     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p10 p9 0 0 0 0 0 0 0 0 p0] */
 829
 830     c += (uint64_t)(a[0]*2) * a[1];
 831     VERIFY_BITS(c, 62);
 832     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p10 p9 0 0 0 0 0 0 0 p1 p0] */
 833     d += (uint64_t)(a[2]*2) * a[9]
 834        + (uint64_t)(a[3]*2) * a[8]
 835        + (uint64_t)(a[4]*2) * a[7]
 836        + (uint64_t)(a[5]*2) * a[6];
 837     VERIFY_BITS(d, 63);
 838     /* [d 0 t9 0 0 0 0 0 0 0 c t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 839     u1 = d & M; d >>= 26; c += u1 * R0;
 840     VERIFY_BITS(u1, 26);
 841     VERIFY_BITS(d, 37);
 842     VERIFY_BITS(c, 63);
 843     /* [d u1 0 t9 0 0 0 0 0 0 0 c-u1*R0 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 844     t1 = c & M; c >>= 26; c += u1 * R1;
 845     VERIFY_BITS(t1, 26);
 846     VERIFY_BITS(c, 38);
 847     /* [d u1 0 t9 0 0 0 0 0 0 c-u1*R1 t1-u1*R0 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 848     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p11 p10 p9 0 0 0 0 0 0 0 p1 p0] */
 849
 850     c += (uint64_t)(a[0]*2) * a[2]
 851        + (uint64_t)a[1] * a[1];
 852     VERIFY_BITS(c, 62);
 853     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 854     d += (uint64_t)(a[3]*2) * a[9]
 855        + (uint64_t)(a[4]*2) * a[8]
 856        + (uint64_t)(a[5]*2) * a[7]
 857        + (uint64_t)a[6] * a[6];
 858     VERIFY_BITS(d, 63);
 859     /* [d 0 0 t9 0 0 0 0 0 0 c t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 860     u2 = d & M; d >>= 26; c += u2 * R0;
 861     VERIFY_BITS(u2, 26);
 862     VERIFY_BITS(d, 37);
 863     VERIFY_BITS(c, 63);
 864     /* [d u2 0 0 t9 0 0 0 0 0 0 c-u2*R0 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 865     t2 = c & M; c >>= 26; c += u2 * R1;
 866     VERIFY_BITS(t2, 26);
 867     VERIFY_BITS(c, 38);
 868     /* [d u2 0 0 t9 0 0 0 0 0 c-u2*R1 t2-u2*R0 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 869     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 0 p2 p1 p0] */
 870
 871     c += (uint64_t)(a[0]*2) * a[3]
 872        + (uint64_t)(a[1]*2) * a[2];
 873     VERIFY_BITS(c, 63);
 874     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 875     d += (uint64_t)(a[4]*2) * a[9]
 876        + (uint64_t)(a[5]*2) * a[8]
 877        + (uint64_t)(a[6]*2) * a[7];
 878     VERIFY_BITS(d, 63);
 879     /* [d 0 0 0 t9 0 0 0 0 0 c t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 880     u3 = d & M; d >>= 26; c += u3 * R0;
 881     VERIFY_BITS(u3, 26);
 882     VERIFY_BITS(d, 37);
 883     /* VERIFY_BITS(c, 64); */
 884     /* [d u3 0 0 0 t9 0 0 0 0 0 c-u3*R0 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 885     t3 = c & M; c >>= 26; c += u3 * R1;
 886     VERIFY_BITS(t3, 26);
 887     VERIFY_BITS(c, 39);
 888     /* [d u3 0 0 0 t9 0 0 0 0 c-u3*R1 t3-u3*R0 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 889     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 0 p3 p2 p1 p0] */
 890
 891     c += (uint64_t)(a[0]*2) * a[4]
 892        + (uint64_t)(a[1]*2) * a[3]
 893        + (uint64_t)a[2] * a[2];
 894     VERIFY_BITS(c, 63);
 895     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 896     d += (uint64_t)(a[5]*2) * a[9]
 897        + (uint64_t)(a[6]*2) * a[8]
 898        + (uint64_t)a[7] * a[7];
 899     VERIFY_BITS(d, 62);
 900     /* [d 0 0 0 0 t9 0 0 0 0 c t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 901     u4 = d & M; d >>= 26; c += u4 * R0;
 902     VERIFY_BITS(u4, 26);
 903     VERIFY_BITS(d, 36);
 904     /* VERIFY_BITS(c, 64); */
 905     /* [d u4 0 0 0 0 t9 0 0 0 0 c-u4*R0 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 906     t4 = c & M; c >>= 26; c += u4 * R1;
 907     VERIFY_BITS(t4, 26);
 908     VERIFY_BITS(c, 39);
 909     /* [d u4 0 0 0 0 t9 0 0 0 c-u4*R1 t4-u4*R0 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 910     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 0 p4 p3 p2 p1 p0] */
 911
 912     c += (uint64_t)(a[0]*2) * a[5]
 913        + (uint64_t)(a[1]*2) * a[4]
 914        + (uint64_t)(a[2]*2) * a[3];
 915     VERIFY_BITS(c, 63);
 916     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 917     d += (uint64_t)(a[6]*2) * a[9]
 918        + (uint64_t)(a[7]*2) * a[8];
 919     VERIFY_BITS(d, 62);
 920     /* [d 0 0 0 0 0 t9 0 0 0 c t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 921     u5 = d & M; d >>= 26; c += u5 * R0;
 922     VERIFY_BITS(u5, 26);
 923     VERIFY_BITS(d, 36);
 924     /* VERIFY_BITS(c, 64); */
 925     /* [d u5 0 0 0 0 0 t9 0 0 0 c-u5*R0 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 926     t5 = c & M; c >>= 26; c += u5 * R1;
 927     VERIFY_BITS(t5, 26);
 928     VERIFY_BITS(c, 39);
 929     /* [d u5 0 0 0 0 0 t9 0 0 c-u5*R1 t5-u5*R0 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 930     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 0 p5 p4 p3 p2 p1 p0] */
 931
 932     c += (uint64_t)(a[0]*2) * a[6]
 933        + (uint64_t)(a[1]*2) * a[5]
 934        + (uint64_t)(a[2]*2) * a[4]
 935        + (uint64_t)a[3] * a[3];
 936     VERIFY_BITS(c, 63);
 937     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 938     d += (uint64_t)(a[7]*2) * a[9]
 939        + (uint64_t)a[8] * a[8];
 940     VERIFY_BITS(d, 61);
 941     /* [d 0 0 0 0 0 0 t9 0 0 c t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 942     u6 = d & M; d >>= 26; c += u6 * R0;
 943     VERIFY_BITS(u6, 26);
 944     VERIFY_BITS(d, 35);
 945     /* VERIFY_BITS(c, 64); */
 946     /* [d u6 0 0 0 0 0 0 t9 0 0 c-u6*R0 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 947     t6 = c & M; c >>= 26; c += u6 * R1;
 948     VERIFY_BITS(t6, 26);
 949     VERIFY_BITS(c, 39);
 950     /* [d u6 0 0 0 0 0 0 t9 0 c-u6*R1 t6-u6*R0 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 951     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 0 p6 p5 p4 p3 p2 p1 p0] */
 952
 953     c += (uint64_t)(a[0]*2) * a[7]
 954        + (uint64_t)(a[1]*2) * a[6]
 955        + (uint64_t)(a[2]*2) * a[5]
 956        + (uint64_t)(a[3]*2) * a[4];
 957     /* VERIFY_BITS(c, 64); */
 958     VERIFY_CHECK(c <= 0x8000007C00000007ULL);
 959     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 960     d += (uint64_t)(a[8]*2) * a[9];
 961     VERIFY_BITS(d, 58);
 962     /* [d 0 0 0 0 0 0 0 t9 0 c t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 963     u7 = d & M; d >>= 26; c += u7 * R0;
 964     VERIFY_BITS(u7, 26);
 965     VERIFY_BITS(d, 32);
 966     /* VERIFY_BITS(c, 64); */
 967     VERIFY_CHECK(c <= 0x800001703FFFC2F7ULL);
 968     /* [d u7 0 0 0 0 0 0 0 t9 0 c-u7*R0 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 969     t7 = c & M; c >>= 26; c += u7 * R1;
 970     VERIFY_BITS(t7, 26);
 971     VERIFY_BITS(c, 38);
 972     /* [d u7 0 0 0 0 0 0 0 t9 c-u7*R1 t7-u7*R0 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 973     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 0 p7 p6 p5 p4 p3 p2 p1 p0] */
 974
 975     c += (uint64_t)(a[0]*2) * a[8]
 976        + (uint64_t)(a[1]*2) * a[7]
 977        + (uint64_t)(a[2]*2) * a[6]
 978        + (uint64_t)(a[3]*2) * a[5]
 979        + (uint64_t)a[4] * a[4];
 980     /* VERIFY_BITS(c, 64); */
 981     VERIFY_CHECK(c <= 0x9000007B80000008ULL);
 982     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 983     d += (uint64_t)a[9] * a[9];
 984     VERIFY_BITS(d, 57);
 985     /* [d 0 0 0 0 0 0 0 0 t9 c t7 t6 t5 t4 t3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 986     u8 = d & M; d >>= 26; c += u8 * R0;
 987     VERIFY_BITS(u8, 26);
 988     VERIFY_BITS(d, 31);
 989     /* VERIFY_BITS(c, 64); */
 990     VERIFY_CHECK(c <= 0x9000016FBFFFC2F8ULL);
 991     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 t4 t3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 992
 993     r[3] = t3;
 994     VERIFY_BITS(r[3], 26);
 995     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 t4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 996     r[4] = t4;
 997     VERIFY_BITS(r[4], 26);
 998     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 t5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
 999     r[5] = t5;
1000     VERIFY_BITS(r[5], 26);
1001     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 t6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1002     r[6] = t6;
1003     VERIFY_BITS(r[6], 26);
1004     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 t7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1005     r[7] = t7;
1006     VERIFY_BITS(r[7], 26);
1007     /* [d u8 0 0 0 0 0 0 0 0 t9 c-u8*R0 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1008
1009     r[8] = c & M; c >>= 26; c += u8 * R1;
1010     VERIFY_BITS(r[8], 26);
1011     VERIFY_BITS(c, 39);
1012     /* [d u8 0 0 0 0 0 0 0 0 t9+c-u8*R1 r8-u8*R0 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1013     /* [d 0 0 0 0 0 0 0 0 0 t9+c r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1014     c   += d * R0 + t9;
1015     VERIFY_BITS(c, 45);
1016     /* [d 0 0 0 0 0 0 0 0 0 c-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1017     r[9] = c & (M >> 4); c >>= 22; c += d * (R1 << 4);
1018     VERIFY_BITS(r[9], 22);
1019     VERIFY_BITS(c, 46);
1020     /* [d 0 0 0 0 0 0 0 0 r9+((c-d*R1<<4)<<22)-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1021     /* [d 0 0 0 0 0 0 0 -d*R1 r9+(c<<22)-d*R0 r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1022     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1 t0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1023
1024     d    = c * (R0 >> 4) + t0;
1025     VERIFY_BITS(d, 56);
1026     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1 d-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1027     r[0] = d & M; d >>= 26;
1028     VERIFY_BITS(r[0], 26);
1029     VERIFY_BITS(d, 30);
1030     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 t1+d r0-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1031     d   += c * (R1 >> 4) + t1;
1032     VERIFY_BITS(d, 53);
1033     VERIFY_CHECK(d <= 0x10000003FFFFBFULL);
1034     /* [r9+(c<<22) r8 r7 r6 r5 r4 r3 t2 d-c*R1>>4 r0-c*R0>>4] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1035     /* [r9 r8 r7 r6 r5 r4 r3 t2 d r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1036     r[1] = d & M; d >>= 26;
1037     VERIFY_BITS(r[1], 26);
1038     VERIFY_BITS(d, 27);
1039     VERIFY_CHECK(d <= 0x4000000ULL);
1040     /* [r9 r8 r7 r6 r5 r4 r3 t2+d r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1041     d   += t2;
1042     VERIFY_BITS(d, 27);
1043     /* [r9 r8 r7 r6 r5 r4 r3 d r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1044     r[2] = d;
1045     VERIFY_BITS(r[2], 27);
1046     /* [r9 r8 r7 r6 r5 r4 r3 r2 r1 r0] = [p18 p17 p16 p15 p14 p13 p12 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 p0] */
1047 }
1048 #endif
1049
1050 static void secp256k1_fe_mul(secp256k1_fe *r, const secp256k1_fe *a, const secp256k1_fe * SECP256K1_RESTRICT b) {
1051 #ifdef VERIFY
1052     VERIFY_CHECK(a->magnitude <= 8);
1053     VERIFY_CHECK(b->magnitude <= 8);
1054     secp256k1_fe_verify(a);
1055     secp256k1_fe_verify(b);
1056     VERIFY_CHECK(r != b);
1057 #endif
1058     secp256k1_fe_mul_inner(r->n, a->n, b->n);
1059 #ifdef VERIFY
1060     r->magnitude = 1;
1061     r->normalized = 0;
1062     secp256k1_fe_verify(r);
1063 #endif
1064 }
1065
1066 static void secp256k1_fe_sqr(secp256k1_fe *r, const secp256k1_fe *a) {
1067 #ifdef VERIFY
1068     VERIFY_CHECK(a->magnitude <= 8);
1069     secp256k1_fe_verify(a);
1070 #endif
1071     secp256k1_fe_sqr_inner(r->n, a->n);
1072 #ifdef VERIFY
1073     r->magnitude = 1;
1074     r->normalized = 0;
1075     secp256k1_fe_verify(r);
1076 #endif
1077 }
1078
1079 static SECP256K1_INLINE void secp256k1_fe_cmov(secp256k1_fe *r, const secp256k1_fe *a, int flag) {
1080     uint32_t mask0, mask1;
1081     mask0 = flag + ~((uint32_t)0);
1082     mask1 = ~mask0;
1083     r->n[0] = (r->n[0] & mask0) | (a->n[0] & mask1);
1084     r->n[1] = (r->n[1] & mask0) | (a->n[1] & mask1);
1085     r->n[2] = (r->n[2] & mask0) | (a->n[2] & mask1);
1086     r->n[3] = (r->n[3] & mask0) | (a->n[3] & mask1);
1087     r->n[4] = (r->n[4] & mask0) | (a->n[4] & mask1);
1088     r->n[5] = (r->n[5] & mask0) | (a->n[5] & mask1);
1089     r->n[6] = (r->n[6] & mask0) | (a->n[6] & mask1);
1090     r->n[7] = (r->n[7] & mask0) | (a->n[7] & mask1);
1091     r->n[8] = (r->n[8] & mask0) | (a->n[8] & mask1);
1092     r->n[9] = (r->n[9] & mask0) | (a->n[9] & mask1);
1093 #ifdef VERIFY
1094     if (a->magnitude > r->magnitude) {
1095         r->magnitude = a->magnitude;
1096     }
1097     r->normalized &= a->normalized;
1098 #endif
1099 }
1100
1101 static SECP256K1_INLINE void secp256k1_fe_storage_cmov(secp256k1_fe_storage *r, const secp256k1_fe_storage *a, int flag) {
1102     uint32_t mask0, mask1;
1103     mask0 = flag + ~((uint32_t)0);
1104     mask1 = ~mask0;
1105     r->n[0] = (r->n[0] & mask0) | (a->n[0] & mask1);
1106     r->n[1] = (r->n[1] & mask0) | (a->n[1] & mask1);
1107     r->n[2] = (r->n[2] & mask0) | (a->n[2] & mask1);
1108     r->n[3] = (r->n[3] & mask0) | (a->n[3] & mask1);
1109     r->n[4] = (r->n[4] & mask0) | (a->n[4] & mask1);
1110     r->n[5] = (r->n[5] & mask0) | (a->n[5] & mask1);
1111     r->n[6] = (r->n[6] & mask0) | (a->n[6] & mask1);
1112     r->n[7] = (r->n[7] & mask0) | (a->n[7] & mask1);
1113 }
1114
1115 static void secp256k1_fe_to_storage(secp256k1_fe_storage *r, const secp256k1_fe *a) {
1116 #ifdef VERIFY
1117     VERIFY_CHECK(a->normalized);
1118 #endif
1119     r->n[0] = a->n[0] | a->n[1] << 26;
1120     r->n[1] = a->n[1] >> 6 | a->n[2] << 20;
1121     r->n[2] = a->n[2] >> 12 | a->n[3] << 14;
1122     r->n[3] = a->n[3] >> 18 | a->n[4] << 8;
1123     r->n[4] = a->n[4] >> 24 | a->n[5] << 2 | a->n[6] << 28;
1124     r->n[5] = a->n[6] >> 4 | a->n[7] << 22;
1125     r->n[6] = a->n[7] >> 10 | a->n[8] << 16;
1126     r->n[7] = a->n[8] >> 16 | a->n[9] << 10;
1127 }
1128
1129 static SECP256K1_INLINE void secp256k1_fe_from_storage(secp256k1_fe *r, const secp256k1_fe_storage *a) {
1130     r->n[0] = a->n[0] & 0x3FFFFFFUL;
1131     r->n[1] = a->n[0] >> 26 | ((a->n[1] << 6) & 0x3FFFFFFUL);
1132     r->n[2] = a->n[1] >> 20 | ((a->n[2] << 12) & 0x3FFFFFFUL);
1133     r->n[3] = a->n[2] >> 14 | ((a->n[3] << 18) & 0x3FFFFFFUL);
1134     r->n[4] = a->n[3] >> 8 | ((a->n[4] << 24) & 0x3FFFFFFUL);
1135     r->n[5] = (a->n[4] >> 2) & 0x3FFFFFFUL;
1136     r->n[6] = a->n[4] >> 28 | ((a->n[5] << 4) & 0x3FFFFFFUL);
1137     r->n[7] = a->n[5] >> 22 | ((a->n[6] << 10) & 0x3FFFFFFUL);
1138     r->n[8] = a->n[6] >> 16 | ((a->n[7] << 16) & 0x3FFFFFFUL);
1139     r->n[9] = a->n[7] >> 10;
1140 #ifdef VERIFY
1141     r->magnitude = 1;
1142     r->normalized = 1;
1143 #endif
1144 }
1145
1146 #endif