From 13aca43ad47253e5ea6acb7acd1ee7d8c92ae0dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 20 Jul 2018 12:51:16 -0400 Subject: Add some primes to be synthesized --- p256_32.c | 247 +++++++++++++++++++++++++++----------------------------------- 1 file changed, 106 insertions(+), 141 deletions(-) (limited to 'p256_32.c') diff --git a/p256_32.c b/p256_32.c index 5fc3d8679..944a7209c 100644 --- a/p256_32.c +++ b/p256_32.c @@ -4,6 +4,13 @@ /* s = 0x10000000000000000000000000000000000000000000000000000000000000000 (from "2^256") */ /* c = [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (6277101735386680763835789423207666416102355444464034512896, -1), (79228162514264337593543950336, -1), (1, 1)] (from "2^224,1;2^192,-1;2^96,-1;1,1") */ /* machine_wordsize = 32 (from "32") */ +/* */ +/* NOTE: In addition to the bounds specified above each function, all */ +/* functions synthesized for this Montgomery arithmetic require the */ +/* input to be strictly less than the prime modulus (s-c), and also */ +/* require the input to be in the unique saturated representation. */ +/* All functions also ensure that these two properties are true of */ +/* return values. */ #include typedef unsigned char fiat_p256_uint1; @@ -3165,157 +3172,115 @@ static void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const ui * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] */ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { - uint32_t x1; - fiat_p256_uint1 x2; - fiat_p256_subborrowx_u32(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0xffffffff)); - uint32_t x3; - fiat_p256_uint1 x4; - fiat_p256_subborrowx_u32(&x3, &x4, x2, (arg1[1]), UINT32_C(0xffffffff)); - uint32_t x5; - fiat_p256_uint1 x6; - fiat_p256_subborrowx_u32(&x5, &x6, x4, (arg1[2]), UINT32_C(0xffffffff)); - uint32_t x7; - fiat_p256_uint1 x8; - fiat_p256_subborrowx_u32(&x7, &x8, x6, (arg1[3]), 0x0); - uint32_t x9; - fiat_p256_uint1 x10; - fiat_p256_subborrowx_u32(&x9, &x10, x8, (arg1[4]), 0x0); - uint32_t x11; - fiat_p256_uint1 x12; - fiat_p256_subborrowx_u32(&x11, &x12, x10, (arg1[5]), 0x0); - uint32_t x13; - fiat_p256_uint1 x14; - fiat_p256_subborrowx_u32(&x13, &x14, x12, (arg1[6]), 0x1); - uint32_t x15; - fiat_p256_uint1 x16; - fiat_p256_subborrowx_u32(&x15, &x16, x14, (arg1[7]), UINT32_C(0xffffffff)); - uint32_t x17; - fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff)); - uint32_t x18; - fiat_p256_uint1 x19; - fiat_p256_addcarryx_u32(&x18, &x19, 0x0, (x17 & UINT32_C(0xffffffff)), x1); - uint32_t x20; - fiat_p256_uint1 x21; - fiat_p256_addcarryx_u32(&x20, &x21, x19, (x17 & UINT32_C(0xffffffff)), x3); - uint32_t x22; - fiat_p256_uint1 x23; - fiat_p256_addcarryx_u32(&x22, &x23, x21, (x17 & UINT32_C(0xffffffff)), x5); - uint32_t x24; - fiat_p256_uint1 x25; - fiat_p256_addcarryx_u32(&x24, &x25, x23, 0x0, x7); - uint32_t x26; - fiat_p256_uint1 x27; - fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, x9); - uint32_t x28; - fiat_p256_uint1 x29; - fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, x11); - uint32_t x30; - fiat_p256_uint1 x31; - fiat_p256_addcarryx_u32(&x30, &x31, x29, (fiat_p256_uint1)(x17 & 0x1), x13); - uint32_t x32; - fiat_p256_uint1 x33; - fiat_p256_addcarryx_u32(&x32, &x33, x31, (x17 & UINT32_C(0xffffffff)), x15); - uint32_t x34 = (x18 >> 8); - uint8_t x35 = (uint8_t)(x18 & UINT8_C(0xff)); - uint32_t x36 = (x34 >> 8); - uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); - uint8_t x38 = (uint8_t)(x36 >> 8); + uint32_t x1 = (arg1[7]); + uint32_t x2 = (arg1[6]); + uint32_t x3 = (arg1[5]); + uint32_t x4 = (arg1[4]); + uint32_t x5 = (arg1[3]); + uint32_t x6 = (arg1[2]); + uint32_t x7 = (arg1[1]); + uint32_t x8 = (arg1[0]); + uint32_t x9 = (x8 >> 8); + uint8_t x10 = (uint8_t)(x8 & UINT8_C(0xff)); + uint32_t x11 = (x9 >> 8); + uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); + uint8_t x13 = (uint8_t)(x11 >> 8); + uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); + fiat_p256_uint1 x15 = (fiat_p256_uint1)(x13 >> 8); + uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); + uint32_t x17 = (x15 + x7); + uint32_t x18 = (x17 >> 8); + uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); + uint32_t x20 = (x18 >> 8); + uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); + uint8_t x22 = (uint8_t)(x20 >> 8); + uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + fiat_p256_uint1 x24 = (fiat_p256_uint1)(x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint32_t x26 = (x24 + x6); + uint32_t x27 = (x26 >> 8); + uint8_t x28 = (uint8_t)(x26 & UINT8_C(0xff)); + uint32_t x29 = (x27 >> 8); + uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); + uint8_t x31 = (uint8_t)(x29 >> 8); + uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); + fiat_p256_uint1 x33 = (fiat_p256_uint1)(x31 >> 8); + uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); + uint32_t x35 = (x33 + x5); + uint32_t x36 = (x35 >> 8); + uint8_t x37 = (uint8_t)(x35 & UINT8_C(0xff)); + uint32_t x38 = (x36 >> 8); uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff)); - fiat_p256_uint1 x40 = (fiat_p256_uint1)(x38 >> 8); + uint8_t x40 = (uint8_t)(x38 >> 8); uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff)); - uint32_t x42 = (x40 + x20); - uint32_t x43 = (x42 >> 8); - uint8_t x44 = (uint8_t)(x42 & UINT8_C(0xff)); - uint32_t x45 = (x43 >> 8); - uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint8_t x47 = (uint8_t)(x45 >> 8); + fiat_p256_uint1 x42 = (fiat_p256_uint1)(x40 >> 8); + uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff)); + uint32_t x44 = (x42 + x4); + uint32_t x45 = (x44 >> 8); + uint8_t x46 = (uint8_t)(x44 & UINT8_C(0xff)); + uint32_t x47 = (x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - fiat_p256_uint1 x49 = (fiat_p256_uint1)(x47 >> 8); + uint8_t x49 = (uint8_t)(x47 >> 8); uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint32_t x51 = (x49 + x22); - uint32_t x52 = (x51 >> 8); - uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff)); - uint32_t x54 = (x52 >> 8); - uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); - uint8_t x56 = (uint8_t)(x54 >> 8); + fiat_p256_uint1 x51 = (fiat_p256_uint1)(x49 >> 8); + uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); + uint32_t x53 = (x51 + x3); + uint32_t x54 = (x53 >> 8); + uint8_t x55 = (uint8_t)(x53 & UINT8_C(0xff)); + uint32_t x56 = (x54 >> 8); uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); - fiat_p256_uint1 x58 = (fiat_p256_uint1)(x56 >> 8); + uint8_t x58 = (uint8_t)(x56 >> 8); uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); - uint32_t x60 = (x58 + x24); - uint32_t x61 = (x60 >> 8); - uint8_t x62 = (uint8_t)(x60 & UINT8_C(0xff)); - uint32_t x63 = (x61 >> 8); - uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); - uint8_t x65 = (uint8_t)(x63 >> 8); + fiat_p256_uint1 x60 = (fiat_p256_uint1)(x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint32_t x62 = (x60 + x2); + uint32_t x63 = (x62 >> 8); + uint8_t x64 = (uint8_t)(x62 & UINT8_C(0xff)); + uint32_t x65 = (x63 >> 8); uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); - fiat_p256_uint1 x67 = (fiat_p256_uint1)(x65 >> 8); + uint8_t x67 = (uint8_t)(x65 >> 8); uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff)); - uint32_t x69 = (x67 + x26); - uint32_t x70 = (x69 >> 8); - uint8_t x71 = (uint8_t)(x69 & UINT8_C(0xff)); - uint32_t x72 = (x70 >> 8); - uint8_t x73 = (uint8_t)(x70 & UINT8_C(0xff)); - uint8_t x74 = (uint8_t)(x72 >> 8); + fiat_p256_uint1 x69 = (fiat_p256_uint1)(x67 >> 8); + uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); + uint32_t x71 = (x69 + x1); + uint32_t x72 = (x71 >> 8); + uint8_t x73 = (uint8_t)(x71 & UINT8_C(0xff)); + uint32_t x74 = (x72 >> 8); uint8_t x75 = (uint8_t)(x72 & UINT8_C(0xff)); - fiat_p256_uint1 x76 = (fiat_p256_uint1)(x74 >> 8); + uint8_t x76 = (uint8_t)(x74 >> 8); uint8_t x77 = (uint8_t)(x74 & UINT8_C(0xff)); - uint32_t x78 = (x76 + x28); - uint32_t x79 = (x78 >> 8); - uint8_t x80 = (uint8_t)(x78 & UINT8_C(0xff)); - uint32_t x81 = (x79 >> 8); - uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff)); - uint8_t x83 = (uint8_t)(x81 >> 8); - uint8_t x84 = (uint8_t)(x81 & UINT8_C(0xff)); - fiat_p256_uint1 x85 = (fiat_p256_uint1)(x83 >> 8); - uint8_t x86 = (uint8_t)(x83 & UINT8_C(0xff)); - uint32_t x87 = (x85 + x30); - uint32_t x88 = (x87 >> 8); - uint8_t x89 = (uint8_t)(x87 & UINT8_C(0xff)); - uint32_t x90 = (x88 >> 8); - uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); - uint8_t x92 = (uint8_t)(x90 >> 8); - uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff)); - fiat_p256_uint1 x94 = (fiat_p256_uint1)(x92 >> 8); - uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); - uint32_t x96 = (x94 + x32); - uint32_t x97 = (x96 >> 8); - uint8_t x98 = (uint8_t)(x96 & UINT8_C(0xff)); - uint32_t x99 = (x97 >> 8); - uint8_t x100 = (uint8_t)(x97 & UINT8_C(0xff)); - uint8_t x101 = (uint8_t)(x99 >> 8); - uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff)); - out1[0] = x35; - out1[1] = x37; - out1[2] = x39; - out1[3] = x41; - out1[4] = x44; - out1[5] = x46; - out1[6] = x48; - out1[7] = x50; - out1[8] = x53; - out1[9] = x55; - out1[10] = x57; - out1[11] = x59; - out1[12] = x62; - out1[13] = x64; - out1[14] = x66; - out1[15] = x68; - out1[16] = x71; - out1[17] = x73; - out1[18] = x75; - out1[19] = x77; - out1[20] = x80; - out1[21] = x82; - out1[22] = x84; - out1[23] = x86; - out1[24] = x89; - out1[25] = x91; - out1[26] = x93; - out1[27] = x95; - out1[28] = x98; - out1[29] = x100; - out1[30] = x102; - out1[31] = x101; + out1[0] = x10; + out1[1] = x12; + out1[2] = x14; + out1[3] = x16; + out1[4] = x19; + out1[5] = x21; + out1[6] = x23; + out1[7] = x25; + out1[8] = x28; + out1[9] = x30; + out1[10] = x32; + out1[11] = x34; + out1[12] = x37; + out1[13] = x39; + out1[14] = x41; + out1[15] = x43; + out1[16] = x46; + out1[17] = x48; + out1[18] = x50; + out1[19] = x52; + out1[20] = x55; + out1[21] = x57; + out1[22] = x59; + out1[23] = x61; + out1[24] = x64; + out1[25] = x66; + out1[26] = x68; + out1[27] = x70; + out1[28] = x73; + out1[29] = x75; + out1[30] = x77; + out1[31] = x76; } /* -- cgit v1.2.3