check_args /* Autogenerated */ /* curve description: p224 */ /* requested operations: (all) */ /* s = 0x100000000000000000000000000000000000000000000000000000000 (from "2^224") */ /* c = [(79228162514264337593543950336, 1), (1, -1)] (from "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_p224_uint1; typedef signed char fiat_p224_int1; typedef signed __int128 fiat_p224_int128; typedef unsigned __int128 fiat_p224_uint128; In fiat_p224_to_bytes: Computed bounds (Some [Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0x1], Some [0x0 ~> 0x1], Some [0x0 ~> 0x1], Some [0x0 ~> 0x0]]) are not tight enough (expected bounds not looser than (Some [Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0]])). The bounds [0x0 ~> 0x1] are looser than the expected bounds [0x0 ~> 0x0] The bounds [0x0 ~> 0x1] are looser than the expected bounds [0x0 ~> 0x0] The bounds [0x0 ~> 0x1] are looser than the expected bounds [0x0 ~> 0x0] When doing bounds analysis on the syntax tree: /* * Input Bounds: * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: None */ void f(uint8_t out1[32], const uint64_t arg1[4]) { uint32_t x1 = (uint32_t)(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)); uint32_t x11 = (uint32_t)(x9 >> 8); uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); uint32_t x13 = (x11 >> 8); uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); uint16_t x15 = (uint16_t)(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)); uint1 x19 = (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)); uint32_t x28 = (uint32_t)(x26 >> 8); uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); uint32_t x30 = (x28 >> 8); uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); uint16_t x32 = (uint16_t)(x30 >> 8); uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); uint8_t x34 = (uint8_t)(x32 >> 8); uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); uint1 x36 = (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)); uint32_t x45 = (uint32_t)(x43 >> 8); uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); uint32_t x47 = (x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); uint16_t x49 = (uint16_t)(x47 >> 8); uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); uint8_t x51 = (uint8_t)(x49 >> 8); uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); uint1 x53 = (uint1)(x51 >> 8); uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); uint32_t x55 = (x53 + x1); uint32_t x56 = (x55 >> 8); uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); uint16_t x58 = (uint16_t)(x56 >> 8); uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); uint8_t x60 = (uint8_t)(x58 >> 8); uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); uint1 x62 = (uint1)(x60 >> 8); uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); uint1 x64 = (uint1)(x62 >> 8); uint1 x65 = (uint1)(x62 & UINT8_C(0xff)); uint1 x66 = (uint1)(x64 >> 8); uint1 x67 = (uint1)(x64 & UINT8_C(0xff)); uint1 x68 = (uint1)(x66 >> 8); uint1 x69 = (uint1)(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; } with input bounds (Some [Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffff]]). In fiat_p224_from_bytes: Computed bounds (Some [Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0x1010101ffffffff]]) are not tight enough (expected bounds not looser than (Some [Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffff]])). The bounds [0x0 ~> 0x1010101ffffffff] are looser than the expected bounds [0x0 ~> 0xffffffff] When doing bounds analysis on the syntax tree: /* * Input Bounds: * arg1: [[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 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0], [0x0 ~> 0x0]] * Output Bounds: * out1: None */ void f(uint64_t out1[4], const uint8_t arg1[32]) { uint64_t x1 = ((uint64_t)(uint1)(arg1[31]) << 56); uint64_t x2 = ((uint64_t)(uint1)(arg1[30]) << 48); uint64_t x3 = ((uint64_t)(uint1)(arg1[29]) << 40); uint64_t x4 = ((uint64_t)(uint1)(arg1[28]) << 32); uint32_t x5 = ((uint32_t)(arg1[27]) << 24); uint32_t x6 = ((uint32_t)(arg1[26]) << 16); uint16_t x7 = (uint16_t)((arg1[25]) << 8); uint8_t x8 = (arg1[24]); uint64_t x9 = ((uint64_t)(arg1[23]) << 56); uint64_t x10 = ((uint64_t)(arg1[22]) << 48); uint64_t x11 = ((uint64_t)(arg1[21]) << 40); uint64_t x12 = ((uint64_t)(arg1[20]) << 32); uint32_t x13 = ((uint32_t)(arg1[19]) << 24); uint32_t x14 = ((uint32_t)(arg1[18]) << 16); uint16_t x15 = (uint16_t)((arg1[17]) << 8); uint8_t x16 = (arg1[16]); uint64_t x17 = ((uint64_t)(arg1[15]) << 56); uint64_t x18 = ((uint64_t)(arg1[14]) << 48); uint64_t x19 = ((uint64_t)(arg1[13]) << 40); uint64_t x20 = ((uint64_t)(arg1[12]) << 32); uint32_t x21 = ((uint32_t)(arg1[11]) << 24); uint32_t x22 = ((uint32_t)(arg1[10]) << 16); uint16_t x23 = (uint16_t)((arg1[9]) << 8); uint8_t x24 = (arg1[8]); uint64_t x25 = ((uint64_t)(arg1[7]) << 56); uint64_t x26 = ((uint64_t)(arg1[6]) << 48); uint64_t x27 = ((uint64_t)(arg1[5]) << 40); uint64_t x28 = ((uint64_t)(arg1[4]) << 32); uint32_t x29 = ((uint32_t)(arg1[3]) << 24); uint32_t x30 = ((uint32_t)(arg1[2]) << 16); uint16_t x31 = (uint16_t)((arg1[1]) << 8); uint8_t x32 = (arg1[0]); uint64_t x33 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25))))))); uint1 x34 = (uint1)((uint128)x33 >> 64); uint64_t x35 = (x33 & UINT64_C(0xffffffffffffffff)); uint64_t x36 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1))))))); uint64_t x37 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9))))))); uint64_t x38 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); uint64_t x39 = (x34 + x38); uint1 x40 = (uint1)((uint128)x39 >> 64); uint64_t x41 = (x39 & UINT64_C(0xffffffffffffffff)); uint64_t x42 = (x40 + x37); uint1 x43 = (uint1)((uint128)x42 >> 64); uint64_t x44 = (x42 & UINT64_C(0xffffffffffffffff)); uint64_t x45 = (x43 + x36); out1[0] = x35; out1[1] = x41; out1[2] = x44; out1[3] = x45; } with input bounds (Some [Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0xff], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0], Some [0x0 ~> 0x0]]).