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_64.c | 183 +++++++++++++++++++++++++++++--------------------------------- 1 file changed, 84 insertions(+), 99 deletions(-) (limited to 'p256_64.c') diff --git a/p256_64.c b/p256_64.c index 1449d3175..56cb29fbc 100644 --- a/p256_64.c +++ b/p256_64.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 = 64 (from "64") */ +/* */ +/* 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; @@ -1159,129 +1166,107 @@ static void fiat_p256_selectznz(uint64_t out1[4], 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 uint64_t arg1[4]) { - uint64_t x1; - fiat_p256_uint1 x2; - fiat_p256_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0xffffffffffffffff)); - uint64_t x3; - fiat_p256_uint1 x4; - fiat_p256_subborrowx_u64(&x3, &x4, x2, (arg1[1]), UINT32_C(0xffffffff)); - uint64_t x5; - fiat_p256_uint1 x6; - fiat_p256_subborrowx_u64(&x5, &x6, x4, (arg1[2]), 0x0); - uint64_t x7; - fiat_p256_uint1 x8; - fiat_p256_subborrowx_u64(&x7, &x8, x6, (arg1[3]), UINT64_C(0xffffffff00000001)); - uint64_t x9; - fiat_p256_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff)); - uint64_t x10; - fiat_p256_uint1 x11; - fiat_p256_addcarryx_u64(&x10, &x11, 0x0, (x9 & UINT64_C(0xffffffffffffffff)), x1); - uint64_t x12; - fiat_p256_uint1 x13; - fiat_p256_addcarryx_u64(&x12, &x13, x11, (x9 & UINT32_C(0xffffffff)), x3); - uint64_t x14; - fiat_p256_uint1 x15; - fiat_p256_addcarryx_u64(&x14, &x15, x13, 0x0, x5); - uint64_t x16; - fiat_p256_uint1 x17; - fiat_p256_addcarryx_u64(&x16, &x17, x15, (x9 & UINT64_C(0xffffffff00000001)), x7); - uint64_t x18 = (x10 >> 8); - uint8_t x19 = (uint8_t)(x10 & UINT8_C(0xff)); - uint64_t x20 = (x18 >> 8); - uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); - uint64_t x22 = (x20 >> 8); - uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + uint64_t x1 = (arg1[3]); + uint64_t x2 = (arg1[2]); + uint64_t x3 = (arg1[1]); + uint64_t x4 = (arg1[0]); + uint64_t x5 = (x4 >> 8); + uint8_t x6 = (uint8_t)(x4 & UINT8_C(0xff)); + uint64_t x7 = (x5 >> 8); + uint8_t x8 = (uint8_t)(x5 & UINT8_C(0xff)); + uint64_t x9 = (x7 >> 8); + uint8_t x10 = (uint8_t)(x7 & UINT8_C(0xff)); + uint64_t x11 = (x9 >> 8); + uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); + uint64_t x13 = (x11 >> 8); + uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); + uint64_t x15 = (x13 >> 8); + uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); + uint8_t x17 = (uint8_t)(x15 >> 8); + uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); + fiat_p256_uint1 x19 = (fiat_p256_uint1)(x17 >> 8); + uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); + uint64_t x21 = (x19 + x3); + uint64_t x22 = (x21 >> 8); + uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff)); uint64_t x24 = (x22 >> 8); uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); uint64_t x26 = (x24 >> 8); uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); uint64_t x28 = (x26 >> 8); uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); - uint8_t x30 = (uint8_t)(x28 >> 8); + uint64_t x30 = (x28 >> 8); uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); - fiat_p256_uint1 x32 = (fiat_p256_uint1)(x30 >> 8); + uint64_t x32 = (x30 >> 8); uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); - uint64_t x34 = (x32 + x12); - uint64_t x35 = (x34 >> 8); - uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); - uint64_t x37 = (x35 >> 8); - uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); - uint64_t x39 = (x37 >> 8); - uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 >> 8); + uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); + fiat_p256_uint1 x36 = (fiat_p256_uint1)(x34 >> 8); + uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); + uint64_t x38 = (x36 + x2); + uint64_t x39 = (x38 >> 8); + uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff)); uint64_t x41 = (x39 >> 8); uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); uint64_t x43 = (x41 >> 8); uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); uint64_t x45 = (x43 >> 8); uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint8_t x47 = (uint8_t)(x45 >> 8); + uint64_t x47 = (x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - fiat_p256_uint1 x49 = (fiat_p256_uint1)(x47 >> 8); + uint64_t x49 = (x47 >> 8); uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint64_t x51 = (x49 + x14); - uint64_t x52 = (x51 >> 8); - uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff)); - uint64_t x54 = (x52 >> 8); - uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); - uint64_t x56 = (x54 >> 8); - uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); + uint8_t x51 = (uint8_t)(x49 >> 8); + uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); + fiat_p256_uint1 x53 = (fiat_p256_uint1)(x51 >> 8); + uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); + uint64_t x55 = (x53 + x1); + uint64_t x56 = (x55 >> 8); + uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); uint64_t x58 = (x56 >> 8); uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); uint64_t x60 = (x58 >> 8); uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); uint64_t x62 = (x60 >> 8); uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); - uint8_t x64 = (uint8_t)(x62 >> 8); + uint64_t x64 = (x62 >> 8); uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); - fiat_p256_uint1 x66 = (fiat_p256_uint1)(x64 >> 8); + uint64_t x66 = (x64 >> 8); uint8_t x67 = (uint8_t)(x64 & UINT8_C(0xff)); - uint64_t x68 = (x66 + x16); - uint64_t x69 = (x68 >> 8); - uint8_t x70 = (uint8_t)(x68 & UINT8_C(0xff)); - uint64_t x71 = (x69 >> 8); - uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); - uint64_t x73 = (x71 >> 8); - uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); - uint64_t x75 = (x73 >> 8); - uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff)); - uint64_t x77 = (x75 >> 8); - uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff)); - uint64_t x79 = (x77 >> 8); - uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff)); - uint8_t x81 = (uint8_t)(x79 >> 8); - uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff)); - out1[0] = x19; - out1[1] = x21; - out1[2] = x23; - out1[3] = x25; - out1[4] = x27; - out1[5] = x29; - out1[6] = x31; - out1[7] = x33; - out1[8] = x36; - out1[9] = x38; - out1[10] = x40; - out1[11] = x42; - out1[12] = x44; - out1[13] = x46; - out1[14] = x48; - out1[15] = x50; - out1[16] = x53; - out1[17] = x55; - out1[18] = x57; - out1[19] = x59; - out1[20] = x61; - out1[21] = x63; - out1[22] = x65; - out1[23] = x67; - out1[24] = x70; - out1[25] = x72; - out1[26] = x74; - out1[27] = x76; - out1[28] = x78; - out1[29] = x80; - out1[30] = x82; - out1[31] = x81; + uint8_t x68 = (uint8_t)(x66 >> 8); + uint8_t x69 = (uint8_t)(x66 & UINT8_C(0xff)); + out1[0] = x6; + out1[1] = x8; + out1[2] = x10; + out1[3] = x12; + out1[4] = x14; + out1[5] = x16; + out1[6] = x18; + out1[7] = x20; + out1[8] = x23; + out1[9] = x25; + out1[10] = x27; + out1[11] = x29; + out1[12] = x31; + out1[13] = x33; + out1[14] = x35; + out1[15] = x37; + out1[16] = x40; + out1[17] = x42; + out1[18] = x44; + out1[19] = x46; + out1[20] = x48; + out1[21] = x50; + out1[22] = x52; + out1[23] = x54; + out1[24] = x57; + out1[25] = x59; + out1[26] = x61; + out1[27] = x63; + out1[28] = x65; + out1[29] = x67; + out1[30] = x69; + out1[31] = x68; } /* -- cgit v1.2.3